Require Import Coqlib.
Require Import AST Integers Values Memory Events Globalenvs Smallstep.
Require Import Op Locations LTL Conventions.

Definition label := positive.

Inductive instruction: Type :=
  | Lgetstack: slot → Z → typ → mreg → instruction
  | Lsetstack: mreg → slot → Z → typ → instruction
  | Lop: operation → list mreg → mreg → instruction
  | Lload: memory_chunk → addressing → list mreg → mreg → instruction
  | Lstore: memory_chunk → addressing → list mreg → mreg → instruction
  | Lcall: signature → mreg + ident → instruction
  | Ltailcall: signature → mreg + ident → instruction
  | Lbuiltin: external_function → list (builtin_arg loc) → builtin_res mreg → instruction
  | Llabel: label → instruction
  | Lgoto: label → instruction
  | Lcond: condition → list mreg → label → instruction
  | Ljumptable: mreg → list label → instruction
  | Lreturn: instruction.

Definition code: Type := list instruction.

Record function: Type := mkfunction {
  fn_sig: signature;
  fn_stacksize: Z;
  fn_code: code
}.

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.

Definition genv := Genv.t fundef unit.
Definition locset := Locmap.t.

Definition is_label (lbl: label) (instr: instruction) : bool :=
  match instr with
  | Llabel lbl' ⇒ if peq lbl lbl' then true else false
  | _ ⇒ false
  end.

Lemma is_label_correct:
  ∀ lbl instr,
  if is_label lbl instr then instr = Llabel lbl else instr ≠ Llabel lbl.
Proof.
  intros. destruct instr; simpl; try discriminate.
  case (peq lbl l); intro; congruence.
Qed.

Fixpoint find_label (lbl: label) (c: code) {struct c} : option code :=
  match c with
  | nil ⇒ None
  | i1 :: il ⇒ if is_label lbl i1 then Some il else find_label lbl il
  end.

Definition find_function (ge: genv) (ros: mreg + ident) (rs: locset) : option fundef :=
  match ros with
  | inl r ⇒ Genv.find_funct ge (rs (R r))
  | inr symb ⇒
      match Genv.find_symbol ge symb with
      | None ⇒ None
      | Some b ⇒ Genv.find_funct_ptr ge b
      end
  end.

Inductive stackframe: Type :=
  | Stackframe:
      ∀ (f: function)
             (sp: val)
             (rs: locset)
             (c: code),
      stackframe.

Inductive state `{memory_model_ops: Mem.MemoryModelOps}: Type :=
  | State:
      ∀ (stack: list stackframe)
             (f: function)
             (sp: val)
             (c: code)
             (rs: locset)
             (m: mem),
      state
  | Callstate:
      ∀ (stack: list stackframe)
             (f: fundef)
             (rs: locset)
             (m: mem),
      state
  | Returnstate:
      ∀ (stack: list stackframe)
             (rs: locset)
             (m: mem),
      state.

Section WITHEXTERNALCALLSOPS.
Context `{external_calls_prf: ExternalCalls}.

Section RELSEM.

Variable parent_lm: locset.

Definition parent_locset (stack: list stackframe) : locset :=
  match stack with
  | nil ⇒ parent_lm
  | Stackframe f sp ls c :: stack' ⇒ ls
  end.

Variable ge: genv.

Inductive step: state → trace → state → Prop :=
  | exec_Lgetstack:
      ∀ s f sp sl ofs ty dst b rs m rs',
      rs' = Locmap.set (R dst) (rs (S sl ofs ty)) (undef_regs (destroyed_by_getstack sl) rs) →
      step (State s f sp (Lgetstack sl ofs ty dst :: b) rs m)
        E0 (State s f sp b rs' m)
  | exec_Lsetstack:
      ∀ s f sp src sl ofs ty b rs m rs',
      rs' = Locmap.set (S sl ofs ty) (rs (R src)) (undef_regs (destroyed_by_setstack ty) rs) →
      step (State s f sp (Lsetstack src sl ofs ty :: b) rs m)
        E0 (State s f sp b rs' m)
  | exec_Lop:
      ∀ s f sp op args res b rs m v rs',
      eval_operation ge sp op (reglist rs args) m = Some v →
      rs' = Locmap.set (R res) v (undef_regs (destroyed_by_op op) rs) →
      step (State s f sp (Lop op args res :: b) rs m)
        E0 (State s f sp b rs' m)
  | exec_Lload:
      ∀ s f sp chunk addr args dst b rs m a v rs',
      eval_addressing ge sp addr (reglist rs args) = Some a →
      Mem.loadv chunk m a = Some v →
      rs' = Locmap.set (R dst) v (undef_regs (destroyed_by_load chunk addr) rs) →
      step (State s f sp (Lload chunk addr args dst :: b) rs m)
        E0 (State s f sp b rs' m)
  | exec_Lstore:
      ∀ s f sp chunk addr args src b rs m m' a rs',
      eval_addressing ge sp addr (reglist rs args) = Some a →
      Mem.storev chunk m a (rs (R src)) = Some m' →
      rs' = undef_regs (destroyed_by_store chunk addr) rs →
      step (State s f sp (Lstore chunk addr args src :: b) rs m)
        E0 (State s f sp b rs' m')
  | exec_Lcall:
      ∀ s f sp sig ros b rs m f',
      find_function ge ros rs = Some f' →
      sig = funsig f' →
      step (State s f sp (Lcall sig ros :: b) rs m)
        E0 (Callstate (Stackframe f sp rs b:: s) f' rs m)
  | exec_Ltailcall:
      ∀ s f stk sig ros b rs m rs' f' m',
      rs' = return_regs (parent_locset s) rs →
      find_function ge ros rs' = Some f' →
      sig = funsig f' →
      Mem.free m stk 0 f.(fn_stacksize) = Some m' →
      step (State s f (Vptr stk Ptrofs.zero) (Ltailcall sig ros :: b) rs m)
        E0 (Callstate s f' rs' m')
  | exec_Lbuiltin:
      ∀ s f sp rs m ef args res b vargs t vres rs' m',
      eval_builtin_args ge rs sp m args vargs →
      external_call ef ge vargs m t vres m' →
      rs' = Locmap.setres res vres (undef_regs (destroyed_by_builtin ef) rs) →
      ∀ BUILTIN_ENABLED : builtin_enabled ef,
        step (State s f sp (Lbuiltin ef args res :: b) rs m)
             t (State s f sp b rs' m')
  | exec_Llabel:
      ∀ s f sp lbl b rs m,
      step (State s f sp (Llabel lbl :: b) rs m)
        E0 (State s f sp b rs m)
  | exec_Lgoto:
      ∀ s f sp lbl b rs m b',
      find_label lbl f.(fn_code) = Some b' →
      step (State s f sp (Lgoto lbl :: b) rs m)
        E0 (State s f sp b' rs m)
  | exec_Lcond_true:
      ∀ s f sp cond args lbl b rs m rs' b',
      eval_condition cond (reglist rs args) m = Some true →
      rs' = undef_regs (destroyed_by_cond cond) rs →
      find_label lbl f.(fn_code) = Some b' →
      step (State s f sp (Lcond cond args lbl :: b) rs m)
        E0 (State s f sp b' rs' m)
  | exec_Lcond_false:
      ∀ s f sp cond args lbl b rs m rs',
      eval_condition cond (reglist rs args) m = Some false →
      rs' = undef_regs (destroyed_by_cond cond) rs →
      step (State s f sp (Lcond cond args lbl :: b) rs m)
        E0 (State s f sp b rs' m)
  | exec_Ljumptable:
      ∀ s f sp arg tbl b rs m n lbl b' rs',
      rs (R arg) = Vint n →
      list_nth_z tbl (Int.unsigned n) = Some lbl →
      find_label lbl f.(fn_code) = Some b' →
      rs' = undef_regs (destroyed_by_jumptable) rs →
      step (State s f sp (Ljumptable arg tbl :: b) rs m)
        E0 (State s f sp b' rs' m)
  | exec_Lreturn:
      ∀ s f stk b rs m m',
      Mem.free m stk 0 f.(fn_stacksize) = Some m' →
      step (State s f (Vptr stk Ptrofs.zero) (Lreturn :: b) rs m)
        E0 (Returnstate s (return_regs (parent_locset s) rs) m')
  | exec_function_internal:
      ∀ s f rs m rs' m' stk,
      Mem.alloc m 0 f.(fn_stacksize) = (m', stk) →
      rs' = undef_regs destroyed_at_function_entry (call_regs rs) →
      step (Callstate s (Internal f) rs m)
        E0 (State s f (Vptr stk Ptrofs.zero) f.(fn_code) rs' m')
  | exec_function_external:
      ∀ s ef args res rs1 rs2 m t m',
      args = map (fun p ⇒ Locmap.getpair p rs1) (loc_arguments (ef_sig ef)) →
      external_call ef ge args m t res m' →
      rs2 = Locmap.setpair (loc_result (ef_sig ef)) res rs1 →
      step (Callstate s (External ef) rs1 m)
         t (Returnstate s rs2 m')
  | exec_return:
      ∀ s f sp rs0 c rs m,
      step (Returnstate (Stackframe f sp rs0 c :: s) rs m)
        E0 (State s f sp c rs m).

End RELSEM.

Inductive initial_state (p: program): state → Prop :=
  | initial_state_intro: ∀ 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 = signature_main →
      initial_state p (Callstate nil f (Locmap.init Vundef) m0).

Inductive final_state: state → int → Prop :=
  | final_state_intro: ∀ rs m retcode,
      Locmap.getpair (map_rpair R (loc_result signature_main)) rs = Vint retcode →
      final_state (Returnstate nil rs m) retcode.

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

End WITHEXTERNALCALLSOPS.