Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Events.
Require Import Memory.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Op.
Require Import Registers.
Require Import Floats.

Require Import Kildall.
Require Import Utils.
Require Import Relation_Operators.
Require Import Classical.
Require Import Relations.Relation_Definitions.
Require Import DLib.
Require Import SSA.
Require Import CSSApar.
Require Parmov.
Require Import Dom.

Abstract syntax

Record function: Type := mkfunction {
  fn_sig: signature;
  fn_params: list reg;
  fn_stacksize: Z;

  fn_code: code;
  fn_parcopycode: parcopycode;

  fn_max_indice: nat;
  fn_entrypoint: node
}.

Definition fundef := AST.fundef function.
Definition program := AST.program fundef unit.

Definition funsig (fd: fundef) :=
  match fd with
  | Internal f => fn_sig f
  | External ef => ef_sig ef
  end.

Notation preds :=
  (fun f pc => (make_predecessors (fn_code f) successors_instr) !!! pc).

Inductive join_point (jp: node) (f:function) : Prop :=
  | jp_cons : forall l,
              forall (Hpreds: (make_predecessors (fn_code f) successors_instr) ! jp = Some l)
                     (Hl: (length l > 1)%nat),
                join_point jp f.

Definition successors (f: function) : PTree.t (list positive) :=
  PTree.map1 successors_instr (fn_code f).
Notation succs := (fun f pc => (successors f) !!! pc).

Section CFG.

  Variable f : function.

  Definition entry := (fn_entrypoint f).
  Notation code := (fn_code f).

  Inductive _cfg (i j:node) : Prop :=
  | CFG : forall ins
    (HCFG_ins: code !i = Some ins)
    (HCFG_in : In j (successors_instr ins)),
    _cfg i j.

  Definition exit (pc: node) : Prop :=
  match code ! pc with
  | Some (SSA.Itailcall _ _ _)
  | Some (SSA.Ireturn _) => True
  | Some (SSA.Ijumptable _ succs) => succs = nil
  | _ => False
  end.

  Definition cfg := _cfg.

End CFG.

Notation reached := (fun f => (reached (cfg f) (entry f))).

Record wf_function (f:function) : Prop := {

  fn_entry : exists s, (fn_code f) ! (fn_entrypoint f) = Some (Inop s);
  fn_entry_pred: forall pc, ~ cfg f pc (fn_entrypoint f);
  
  fn_normalized : forall jp pc,
                   join_point jp f ->
                   In jp (succs f pc) -> (fn_code f) ! pc = Some (Inop jp);
  
  fn_normalized_jp : forall pc pc',
                       join_point pc' f ->
                       cfg f pc pc' ->
                       ~ join_point pc f ;

  fn_parcb_jp: forall pc pc' parcb,
            (fn_code f) ! pc = Some (Inop pc') ->
            (fn_parcopycode f) ! pc = Some parcb ->
            ~ join_point pc' f ->
            join_point pc f;

  fn_parcb_inop: forall pc,
            (fn_parcopycode f) ! pc <> None ->
            exists s, (fn_code f) ! pc = Some (Inop s);

 fn_code_closed: forall pc pc' instr, (fn_code f) ! pc = Some instr ->
                                       In pc' (successors_instr instr) ->
                                       exists instr', (fn_code f) ! pc' = Some instr'
}.

Inductive wf_fundef: fundef -> Prop :=
  | wf_fundef_external: forall ef,
      wf_fundef (External ef)
  | wf_function_internal: forall f,
      wf_function f ->
      wf_fundef (Internal f).

Definition wf_program (p: program) : Prop :=
  forall f id, In (id, Gfun f) (prog_defs p) -> wf_fundef f.


Definition parcb_to_moves :=
  map (fun parc => match parc with Iparcopy src dst => (src, dst) end).

Definition mill_function (f: function) : Prop :=
  forall pc parcb,
    (fn_parcopycode f) ! pc = Some parcb ->
    Parmov.is_mill _ (parcb_to_moves parcb).

Inductive mill_fundef: fundef -> Prop :=
  | mill_fundef_external: forall ef,
      mill_fundef (External ef)
  | mill_function_internal: forall f,
      mill_function f ->
      mill_fundef (Internal f).

Definition mill_program (p: program) : Prop :=
  forall f id, In (id, Gfun f) (prog_defs p) -> mill_fundef f.

Operational semantics

Definition genv := Genv.t fundef unit.


Inductive stackframe : Type :=
  | Stackframe:
      forall (res: reg) (* where to store the result *)
             (f: function) (* calling function *)
             (sp: val) (* stack pointer in calling function *)
             (pc: node) (* program point in calling function *)
             (rs: regset), (* register state in calling function *)
      stackframe.

Inductive state : Type :=
  | State:
      forall (stack: list stackframe) (* call stack *)
             (f: function) (* current function *)
             (sp: val) (* stack pointer *)
             (pc: node) (* current program point in c *)
             (rs: regset) (* register state *)
             (m: mem), (* memory state *)
      state
  | Callstate:
      forall (stack: list stackframe) (* call stack *)
             (f: fundef) (* function to call *)
             (args: list val) (* arguments to the call *)
             (m: mem), (* memory state *)
      state
  | Returnstate:
      forall (stack: list stackframe) (* call stack *)
             (v: val) (* return value for the call *)
             (m: mem), (* memory state *)
      state.

Section RELSEM.

Variable ge: genv.

Definition find_function
  (ros: reg + ident) (rs: regset) : option fundef :=
  match ros with
  | inl r => Genv.find_funct ge (rs #2 r)
  | inr symb =>
      match Genv.find_symbol ge symb with
      | None => None
      | Some b => Genv.find_funct_ptr ge b
      end
  end.


Inductive step: state -> trace -> state -> Prop :=
| exec_Inop_njp:
    forall s f sp pc rs m pc',
    (fn_code f)!pc = Some(SSA.Inop pc') ->
    ~ join_point pc' f ->

    step (State s f sp pc rs m)
      E0 (State s f sp pc' rs m)
| exec_Inop_jp:
    forall s f sp pc rs m pc' parcb parcb',
    (fn_code f)!pc = Some(SSA.Inop pc') ->
    join_point pc' f ->

    (fn_parcopycode f)!pc = Some parcb ->
    (fn_parcopycode f)!pc' = Some parcb' ->
    step (State s f sp pc rs m)
      E0 (State s f sp pc'
          (parcopy_store parcb'
              (parcopy_store parcb rs))
          m)
| exec_Iop:
    forall s f sp pc rs m op args res pc' v,
    (fn_code f)!pc = Some(SSA.Iop op args res pc') ->
    eval_operation ge sp op rs##2 args m = Some v ->
    step (State s f sp pc rs m)
      E0 (State s f sp pc' (rs#2 res <- v) m)
| exec_Iload:
    forall s f sp pc rs m chunk addr args dst pc' a v,
    (fn_code f)!pc = Some(SSA.Iload chunk addr args dst pc') ->
    eval_addressing ge sp addr rs##2 args = Some a ->
    Mem.loadv chunk m a = Some v ->
    step (State s f sp pc rs m)
      E0 (State s f sp pc' (rs#2 dst <- v) m)
| exec_Istore:
    forall s f sp pc rs m chunk addr args src pc' a m',
    (fn_code f)!pc = Some(SSA.Istore chunk addr args src pc') ->
    eval_addressing ge sp addr rs##2 args = Some a ->
    Mem.storev chunk m a rs#2 src = Some m' ->
    step (State s f sp pc rs m)
      E0 (State s f sp pc' rs m')
| exec_Icall:
    forall s f sp pc rs m sig ros args res pc' fd,
    (fn_code f)!pc = Some(SSA.Icall sig ros args res pc') ->
    find_function ros rs = Some fd ->
    funsig fd = sig ->
    step (State s f sp pc rs m)
      E0 (Callstate (Stackframe res f sp pc' rs :: s) fd rs##2 args m)
| exec_Itailcall:
    forall s f stk pc rs m sig ros args fd m',
    (fn_code f)!pc = Some(SSA.Itailcall sig ros args) ->
    find_function ros rs = Some fd ->
    funsig fd = sig ->
    Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
    step (State s f (Vptr stk Int.zero) pc rs m)
      E0 (Callstate s fd rs##2 args m')
| exec_Ibuiltin:
    forall s f sp pc rs m ef args res pc' t v m',
    (fn_code f)!pc = Some(SSA.Ibuiltin ef args res pc') ->
    external_call ef ge rs##2 args m t v m' ->
    step (State s f sp pc rs m)
    t (State s f sp pc' (rs#2 res <- v) m')
| exec_Icond_true:
    forall s f sp pc rs m cond args ifso ifnot,
    (fn_code f)!pc = Some(SSA.Icond cond args ifso ifnot) ->
    eval_condition cond rs##2 args m = Some true ->
    step (State s f sp pc rs m)
      E0 (State s f sp ifso rs m)
| exec_Icond_false:
    forall s f sp pc rs m cond args ifso ifnot,
    (fn_code f)!pc = Some(SSA.Icond cond args ifso ifnot) ->
    eval_condition cond rs##2 args m = Some false ->
    step (State s f sp pc rs m)
      E0 (State s f sp ifnot rs m)
| exec_Ijumptable:
    forall s f sp pc rs m arg tbl n pc',
    (fn_code f)!pc = Some(SSA.Ijumptable arg tbl) ->
    rs#2 arg = Vint n ->
    list_nth_z tbl (Int.unsigned n) = Some pc' ->
    step (State s f sp pc rs m)
      E0 (State s f sp pc' rs m)
| exec_Ireturn:
    forall s f stk pc rs m or m',
    (fn_code f)!pc = Some(SSA.Ireturn or) ->
    Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
    step (State s f (Vptr stk Int.zero) pc rs m)
      E0 (Returnstate s (regmap2_optget or Vundef rs) m')
| exec_function_internal:
    forall s f args m m' stk,
    Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
    step (Callstate s (Internal f) args m)
      E0 (State s
        f
        (Vptr stk Int.zero)
        f.(fn_entrypoint)
        (init_regs args f.(fn_params))
        m')
| exec_function_external:
    forall s ef args res t m m',
    external_call ef ge args m t res m' ->
    step (Callstate s (External ef) args m)
      t (Returnstate s res m')
| exec_return:
    forall res f sp pc rs s vres m,
    step (Returnstate (Stackframe res f sp pc rs :: s) vres m)
      E0 (State s f sp pc (rs#2 res <- vres) m).

Hint Constructors step.

End RELSEM.


Inductive initial_state (p: program): state -> Prop :=
  | initial_state_intro: forall b f m0,
      let ge := Genv.globalenv p in
      Genv.init_mem p = Some m0 ->
      Genv.find_symbol ge p.(prog_main) = Some b ->
      Genv.find_funct_ptr ge b = Some f ->
      funsig f = mksignature nil (Some Tint) ->
      initial_state p (Callstate nil f nil m0).


Inductive final_state: state -> int -> Prop :=
  | final_state_intro: forall r m, final_state (Returnstate nil (Vint r) m) r.


Definition semantics (p: program) :=
  Semantics step (initial_state p) final_state (Genv.globalenv p).

Notation RTLpath := (fun f => Dom.path (cfg f) (exit f) (entry f)).