Require Ast RTL.
Require Import Coqlib Op Maps.
Require Import Mem Pointers Values.
Require Import Integers Registers.

Require Export Utils.

Syntax of MIR. A high-level managed intermediate representation.

Inductive operation : Type :=
| OpIntConst (cst:int) (* integer constant. *)
| OpNull (* null pointer constant. *)
| OpAdd (* addition. *)
| OpMov (* duplicate the content of a register. *)
| OpNeg (* arithmetic negation *)
| OpShri (imm:int) (* bitwise right-shift *)
.


Definition node := positive.

Inductive field_kind : Type :=
| FNonVolatile | FVolatile.
Definition is_volatile (k:field_kind) : bool :=
  match k with
    | FNonVolatile => false
    | FVolatile => true
  end.

Inductive field_type : Type :=
| FPointer | FInteger.

Inductive field : Type :=
| Field (f: N) (k:field_kind) (typ: field_type).
Definition is_field_volatile (f:field) : bool :=
  match f with
    | Field _ k _ => is_volatile k
  end.
Definition is_ptr_field (f:field) : bool :=
  match f with
    | Field _ _ FInteger => false
    | Field _ _ FPointer => true
  end.

Definition header := int.

Record signature : Type := mksignature
{ sig_res: field_type
; sig_args: list field_type
; sig_ext: bool (* is this function external? *)
}.

Definition signature_eq_dec : forall s s' : signature, { s = s' } + { s <> s' }.

Inductive instruction : Type :=
| Mnop (succ:node)
| Mop (dst:reg) (op: operation) (args: list reg) (succ:node)
| Mif (cmp: condition) (args: list reg) (if_so: node) (if_not: node)
| Mget (dst:reg) (src:reg) (fld:field) (succ:node)
| Mput (dst:reg) (fld:field) (src:reg) (succ:node)
| Mget_global (dst:reg) (src:Ast.ident) (succ:node)
| Mput_global (dst:Ast.ident) (src:reg) (succ:node)
| Mnew (dst:reg) (hdr: header) (succ:node)
| Mfence (succ:node)
| Mspawn (sig: signature) (func:Ast.ident) (arg:reg) (succ:node)
| Mlock (mon:reg) (succ:node)
| Munlock (mon:reg) (succ:node)
| Mcall (dst:reg) (sig: signature) (func:Ast.ident) (args: list reg) (succ:node)
| Mret (res:reg)
.

Definition successors_instr (i: instruction) : list node :=
  match i with
    | Mnop s
    | Mop _ _ _ s
    | Mget _ _ _ s
    | Mput _ _ _ s
    | Mget_global _ _ s
    | Mput_global _ _ s
    | Mnew _ _ s
    | Mfence s
    | Mspawn _ _ _ s
    | Mlock _ s
    | Munlock _ s
    | Mcall _ _ _ _ s => s :: nil
    | Mif _ _ s s' => s :: s' :: nil
    | Mret _ => nil
  end.

Definition code: Type := PTree.t instruction.

Definition max_reg_i (r: reg) (k: node) (i: instruction) : reg :=
  match i with
    | Mnop _
    | Mfence _ => r
    | Mop dst _ args _
    | Mcall dst _ _ args _ => list_max args (Pmax dst r)
    | Mif _ args _ _ => list_max args r
    | Mget dst src _ _
    | Mput dst _ src _ => Pmax (Pmax dst src) r
    | Mget_global dst _ _
    | Mput_global _ dst _
    | Mnew dst _ _
    | Mspawn _ _ dst _
    | Mlock dst _
    | Munlock dst _
    | Mret dst => Pmax dst r
  end.

Definition fresh_register (c: code) : reg :=
  Psucc (PTree.fold max_reg_i c xH).

Definition register_in_instr (i: instruction) (r: reg) : Prop :=
  match i with
    | Mnop _
    | Mfence _ => False
    | Mop dst _ args _
    | Mcall dst _ _ args _ => In r args \/ r = dst
    | Mif _ args _ _ => In r args
    | Mget dst src _ _
    | Mput dst _ src _ => r = dst \/ r = src
    | Mget_global dst _ _
    | Mput_global _ dst _
    | Mnew dst _ _
    | Mspawn _ _ dst _
    | Mlock dst _
    | Munlock dst _
    | Mret dst => r = dst
  end.

Lemma max_reg_i_ple z k i r :
  register_in_instr i r \/ Ple r z ->
  Ple r (max_reg_i z k i).

Lemma fresh_register_aux :
  forall l z k r i,
    (In (k,i) l /\ register_in_instr i r) \/ Ple r z ->
    Ple r (fold_left (fun a p => max_reg_i a (fst p) (snd p)) l z).

Lemma Ple_Plt_succ p q :
  Ple p q ->
  Plt p (Psucc q).

Lemma fresh_register_plt :
  forall (c: code) (pc: node) (i : instruction),
    c ! pc = Some i ->
    forall r,
      register_in_instr i r ->
      Plt r (fresh_register c).

Record function: Type := mkfunction {
  fn_sig: signature;
  fn_params: list reg;
  fn_roots: N; (* number of registers holding pointers. *)
  fn_code: code;
  fn_entrypoint: node
}.

Definition is_ptr_reg (b:N) (r: reg) : bool :=
  zle (Zpos r) (Z_of_N b).

Definition successors (f: function) : PTree.t (list node) :=
  PTree.map (fun _ i => successors_instr i) f.(fn_code).

Definition fundef := Ast.fundef function.

Record program := mk_program
{ prog_funct : PTree.t fundef (* function definitions; keys are Ast.ident. *)
; prog_entry : Ast.ident (* entry point *)
; prog_vars : PTree.t (field_kind * field_type) (* global variables *)
}.

Inductive abort_msg : Type :=
| Abort_OOM (* no space left in the heap *)
| Abort_OCS (* overfull collector stack *)
| Abort_Spawn (* cannot spawn a new thread *)
| Abort_WB (* overfull bucket in write barrier *)
| Abort_RS (* overfull bucket in root scan *)
.