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

Require Import Mach.

Require Import CUAST Footprint MemOpFP Op_fp String val_casted helpers.
Require IS_local GAST.

Require Import loadframe.

Local Notation footprint := FP.t.
Local Notation empfp := FP.emp.

Abstract syntax

Operational semantics

Notation "a ## b" := (List.map a b) (at level 1).
Notation "a # b <- c" := (Regmap.set b c a) (at level 1, b at next level).


Section RELSEM.

Variable return_address_offset: function -> code -> ptrofs -> Prop.

Variable ge: genv.

Local Notation find_function_ptr := (find_function_ptr ge).


Inductive extcall_arg_fp (sp: val) : loc -> footprint -> Prop :=
| extcall_arg_reg_fp: forall r,
    extcall_arg_fp sp (R r) empfp
| extcall_arg_stack_fp: forall ofs ty fp,
    load_stack_fp sp ty (Ptrofs.repr (Stacklayout.fe_ofs_arg + 4 * ofs)) = fp ->
    extcall_arg_fp sp (S Outgoing ofs ty) fp.

Inductive extcall_arg_pair_fp (sp: val) : rpair loc -> footprint -> Prop :=
| extcall_arg_one_fp: forall l fp,
    extcall_arg_fp sp l fp ->
    extcall_arg_pair_fp sp (One l) fp
| extcall_arg_twolong_fp: forall hi lo fp1 fp2 fp,
    extcall_arg_fp sp hi fp1 ->
    extcall_arg_fp sp lo fp2 ->
    FP.union fp1 fp2 = fp ->
    extcall_arg_pair_fp sp (Twolong hi lo) fp.

Inductive load_arguments_fp (sp: val) : list (rpair loc) -> footprint -> Prop :=
| load_arguments_nil_fp:
    load_arguments_fp sp nil empfp
| load_arguments_cons_fp:
    forall pl ll fp1 fp2 fp,
      extcall_arg_pair_fp sp pl fp1 ->
      load_arguments_fp sp ll fp2 ->
      FP.union fp1 fp2 = fp ->
      load_arguments_fp sp (pl :: ll) fp.
    
Definition extcall_arguments_fp
           (sp: val) (sg: signature) (fp: footprint) : Prop :=
  load_arguments_fp sp (loc_arguments sg) fp.

Lemma tailcall_possible_extcall_arguments:
  forall sg rs m stk vl,
    tailcall_possible sg ->
    extcall_arguments rs m stk sg vl ->
    forall m' stk', extcall_arguments rs m' stk' sg vl.

Lemma tailcall_possible_extcall_arguments_fp:
  forall sg stk fp,
    tailcall_possible sg ->
    extcall_arguments_fp stk sg fp ->
    forall stk', extcall_arguments_fp stk' sg fp.



Inductive core: Type :=
| Core_State:
    forall (stack: list stackframe) (* call stack *)
      (f: block) (* pointer to current function *)
      (sp: val) (* stack pointer *)
      (c: code) (* current program point *)
      (rs: regset) (* register state *)
      (loader: load_frame),
      core
| Core_Callstate:
    forall (stack: list stackframe) (* call stack *)
      (f: block) (* pointer to function to call *)
      (rs: regset) (* register state *)
      (loader: load_frame),
      core
| Core_Returnstate:
    forall (stack: list stackframe) (* call stack *)
      (rs: regset) (* register state *)
      (loader: load_frame),
      core
        
| Core_CallstateIn:
    forall (f: block) (* pointer to function to call *)
      (args: list val) (* arguments passed to initial_core *)
      (tys: list typ) (* argument types *)
      (sigres: option typ),
      core

| Core_CallstateOut:
    forall (stack: list stackframe) (* call stack *)
      (b: block) (* global block address of the external function to be called *)
      (f: external_function) (* external function to be called *)
      (vals: list val) (* at_external arguments *)
      (rs: regset) (* register state *)
      (loader: load_frame),
      core.


Definition parent_sp0 (sp0: block) (s: list stackframe) : val :=
  match s with
  | nil => Vptr sp0 Ptrofs.zero
  | Stackframe f sp ra c :: s' => sp
  end.

Inductive step: core -> mem -> footprint -> core -> mem -> Prop :=
| exec_Mlabel:
    forall s f sp lbl c rs m lf,
      step (Core_State s f sp (Mlabel lbl :: c) rs lf) m
           empfp (Core_State s f sp c rs lf) m
| exec_Mgetstack:
    forall s f sp ofs ty dst c rs m v lf fp,
      load_stack m sp ty ofs = Some v ->
      load_stack_fp sp ty ofs = fp ->
      step (Core_State s f sp (Mgetstack ofs ty dst :: c) rs lf) m
           fp (Core_State s f sp c (rs#dst <- v) lf) m
| exec_Msetstack:
    forall s f sp src ofs ty c rs m m' rs' lf fp,
      store_stack m sp ty ofs (rs src) = Some m' ->
      store_stack_fp sp ty ofs = fp ->
      rs' = undef_regs (destroyed_by_setstack ty) rs ->
      step (Core_State s f sp (Msetstack src ofs ty :: c) rs lf) m
           fp (Core_State s f sp c rs' lf) m'
           
| exec_Mgetparam:
    forall s fb f sp ofs ty dst c rs m v rs' sp0 args0 tyl0 sigres0 fp1 fp2 fp,
      Genv.find_funct_ptr ge fb = Some (Internal f) ->
      load_stack m sp Tptr f.(fn_link_ofs) = Some (parent_sp0 sp0 s) ->
      load_stack_fp sp Tptr f.(fn_link_ofs) = fp1 ->
      load_stack m (parent_sp0 sp0 s) ty ofs = Some v ->
      load_stack_fp (parent_sp0 sp0 s) ty ofs = fp2 ->
      rs' = (rs # temp_for_parent_frame <- Vundef # dst <- v) ->
      FP.union fp1 fp2 = fp ->
      step (Core_State s fb sp (Mgetparam ofs ty dst :: c) rs (mk_load_frame sp0 args0 tyl0 sigres0)) m
           fp (Core_State s fb sp c rs' (mk_load_frame sp0 args0 tyl0 sigres0)) m

| exec_Mop:
    forall s f sp op args res c rs m v rs' lf fp,
      eval_operation ge sp op rs##args m = Some v ->
      eval_operation_fp ge sp op rs##args m = Some fp ->
      rs' = ((undef_regs (destroyed_by_op op) rs)#res <- v) ->
      step (Core_State s f sp (Mop op args res :: c) rs lf) m
           fp (Core_State s f sp c rs' lf) m
| exec_Mload:
    forall s f sp chunk addr args dst c rs m a v rs' lf fp,
      eval_addressing ge sp addr rs##args = Some a ->
      Mem.loadv chunk m a = Some v ->
      loadv_fp chunk a = fp ->
      rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- v) ->
      step (Core_State s f sp (Mload chunk addr args dst :: c) rs lf) m
           fp (Core_State s f sp c rs' lf) m
| exec_Mstore:
    forall s f sp chunk addr args src c rs m m' a rs' lf fp,
      eval_addressing ge sp addr rs##args = Some a ->
      Mem.storev chunk m a (rs src) = Some m' ->
      storev_fp chunk a = fp ->
      rs' = undef_regs (destroyed_by_store chunk addr) rs ->
      step (Core_State s f sp (Mstore chunk addr args src :: c) rs lf) m
           fp (Core_State s f sp c rs' lf) m'
           
| exec_Mgoto:
    forall s fb f sp lbl c rs m c' lf,
      Genv.find_funct_ptr ge fb = Some (Internal f) ->
      find_label lbl f.(fn_code) = Some c' ->
      step (Core_State s fb sp (Mgoto lbl :: c) rs lf) m
           empfp (Core_State s fb sp c' rs lf) m

| exec_Mcond_true:
    forall s fb f sp cond args lbl c rs m c' rs' lf fp,
      eval_condition cond rs##args m = Some true ->
      eval_condition_fp cond rs##args m = Some fp ->
      Genv.find_funct_ptr ge fb = Some (Internal f) ->
      find_label lbl f.(fn_code) = Some c' ->
      rs' = undef_regs (destroyed_by_cond cond) rs ->
      step (Core_State s fb sp (Mcond cond args lbl :: c) rs lf) m
           fp (Core_State s fb sp c' rs' lf) m
| exec_Mcond_false:
    forall s f sp cond args lbl c rs m rs' lf fp,
      eval_condition cond rs##args m = Some false ->
      eval_condition_fp cond rs##args m = Some fp ->
      rs' = undef_regs (destroyed_by_cond cond) rs ->
      step (Core_State s f sp (Mcond cond args lbl :: c) rs lf) m
           fp (Core_State s f sp c rs' lf) m
| exec_Mjumptable:
    forall s fb f sp arg tbl c rs m n lbl c' rs' lf,
      rs arg = Vint n ->
      list_nth_z tbl (Int.unsigned n) = Some lbl ->
      Genv.find_funct_ptr ge fb = Some (Internal f) ->
      find_label lbl f.(fn_code) = Some c' ->
      rs' = undef_regs destroyed_by_jumptable rs ->
      step (Core_State s fb sp (Mjumptable arg tbl :: c) rs lf) m
           empfp (Core_State s fb sp c' rs' lf) m

| exec_Minitcall:
    forall fb args tyl sigres z m m' m'' sp0 fp1 fp2 fp,
      args_len_rec args tyl = Some z ->
      Mem.alloc m 0 (4 * z) = (m', sp0) ->
      alloc_fp m 0 (4 * z) = fp1 ->
      store_args m' sp0 args tyl = Some m'' ->
      store_args_fp sp0 tyl = fp2 ->
      FP.union fp1 fp2 = fp ->
      step (Core_CallstateIn fb args tyl sigres) m
           fp
           (Core_Callstate nil fb (Regmap.init Vundef)
                           (mk_load_frame sp0 args tyl sigres)) m''
| exec_Mcall_internal:
    forall s fb sp sig ros c rs m f f' ra callee lf,
      find_function_ptr ros rs = Some f' ->
      Genv.find_funct_ptr ge fb = Some (Internal f) ->
      return_address_offset f c ra ->
      Genv.find_funct_ptr ge f' = Some (Internal callee) ->
      step (Core_State s fb sp (Mcall sig ros :: c) rs lf) m
           empfp (Core_Callstate (Stackframe fb sp (Vptr fb ra) c :: s)
                                 f' rs lf) m
| exec_Mcall_external:
    forall s fb sp sig ros c rs m f f' ra callee args lf fp,
      find_function_ptr ros rs = Some f' ->
      Genv.find_funct_ptr ge fb = Some (Internal f) ->
      return_address_offset f c ra ->
      Genv.find_funct_ptr ge f' = Some (External callee) ->
      extcall_arguments rs m sp (ef_sig callee) args ->
      extcall_arguments_fp sp (ef_sig callee) fp ->
      step (Core_State s fb sp (Mcall sig ros :: c) rs lf) m
           fp (Core_CallstateOut (Stackframe fb sp (Vptr fb ra) c :: s)
                                 f' callee args rs lf) m
| Mach_exec_Mtailcall_internal:
    forall s fb stk soff sig ros c rs m f f' m' callee sp0 args0 tys0 retty fp1 fp2 fp3 fp,
      find_function_ptr ros rs = Some f' ->
      Genv.find_funct_ptr ge fb = Some (Internal f) ->
      load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp0 sp0 s) ->
      load_stack_fp (Vptr stk soff) Tint f.(fn_link_ofs) = fp1 ->
      load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
      load_stack_fp (Vptr stk soff) Tint f.(fn_retaddr_ofs) = fp2 ->
      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
      free_fp stk 0 f.(fn_stacksize) = fp3 ->
      FP.union (FP.union fp1 fp2) fp3 = fp ->
      Genv.find_funct_ptr ge f' = Some (Internal callee) ->
      step (Core_State s fb (Vptr stk soff) (Mtailcall sig ros :: c) rs
                       (mk_load_frame sp0 args0 tys0 retty)) m
           fp
           (Core_Callstate s f' rs (mk_load_frame sp0 args0 tys0 retty)) m'

| Mach_exec_Mtailcall_external:
    forall s fb stk soff sig ros c rs m f f' m' callee args sp0 args0 tys0 retty fp1 fp2 fp3 fp4 fp,
      find_function_ptr ros rs = Some f' ->
      Genv.find_funct_ptr ge fb = Some (Internal f) ->
      load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp0 sp0 s) ->
      load_stack_fp (Vptr stk soff) Tint f.(fn_link_ofs) = fp1 ->
      load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
      load_stack_fp (Vptr stk soff) Tint f.(fn_retaddr_ofs) = fp2 ->
      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
      free_fp stk 0 f.(fn_stacksize) = fp3 ->
      Genv.find_funct_ptr ge f' = Some (External callee) ->
      tailcall_possible (ef_sig callee) ->
      extcall_arguments rs m' (Vptr stk soff) (ef_sig callee) args ->
      extcall_arguments_fp (Vptr stk soff) (ef_sig callee) fp4 ->
      FP.union (FP.union (FP.union fp1 fp2) fp3) fp4 = fp ->

      step (Core_State s fb (Vptr stk soff) (Mtailcall sig ros :: c) rs
                       (mk_load_frame sp0 args0 tys0 retty)) m
           fp
           (Core_CallstateOut s f' callee args rs
                              (mk_load_frame sp0 args0 tys0 retty)) m'

| exec_Mbuiltin:
    forall s f sp rs m ef args res b vargs fp vres rs' lf,
      eval_builtin_args ge rs sp m args vargs ->
      eval_builtin_args_fp ge rs sp args fp ->
      i64ext ef ->
      external_call ef ge vargs m E0 vres m ->
      rs' = set_res res vres (undef_regs (destroyed_by_builtin ef) rs) ->
      step (Core_State s f sp (Mbuiltin ef args res :: b) rs lf) m
           fp (Core_State s f sp b rs' lf) m

| exec_Mreturn:
    forall s fb stk soff c rs m f m' sp0 args0 tys0 retty fp1 fp2 fp3 fp,
      Genv.find_funct_ptr ge fb = Some (Internal f) ->
      load_stack m (Vptr stk soff) Tptr f.(fn_link_ofs) = Some (parent_sp0 sp0 s) ->
      load_stack_fp (Vptr stk soff) Tint f.(fn_link_ofs) = fp1 ->
      load_stack m (Vptr stk soff) Tptr f.(fn_retaddr_ofs) = Some (parent_ra s) ->
      load_stack_fp (Vptr stk soff) Tint f.(fn_retaddr_ofs) = fp2 ->
      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
      free_fp stk 0 f.(fn_stacksize) = fp3 ->
      FP.union (FP.union fp1 fp2) fp3 = fp ->
      step (Core_State s fb (Vptr stk soff) (Mreturn :: c) rs (mk_load_frame sp0 args0 tys0 retty)) m
           fp (Core_Returnstate s rs (mk_load_frame sp0 args0 tys0 retty)) m'
           
| exec_function_internal:
    forall s fb rs m f m1 m2 m3 stk rs' sp0 args0 tys0 retty fp1 fp2 fp3 fp,
      Genv.find_funct_ptr ge fb = Some (Internal f) ->
      Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) ->
      alloc_fp m 0 f.(fn_stacksize) = fp1 ->
      let sp := Vptr stk Ptrofs.zero in
      store_stack m1 sp Tptr f.(fn_link_ofs) (parent_sp0 sp0 s) = Some m2 ->
      store_stack_fp sp Tptr f.(fn_link_ofs) = fp2 ->
      store_stack m2 sp Tptr f.(fn_retaddr_ofs) (parent_ra s) = Some m3 ->
      store_stack_fp sp Tptr f.(fn_retaddr_ofs) = fp3 ->
      FP.union (FP.union fp1 fp2) fp3 = fp ->
      rs' = undef_regs destroyed_at_function_entry rs ->
      step (Core_Callstate s fb rs (mk_load_frame sp0 args0 tys0 retty)) m
           fp (Core_State s fb sp f.(fn_code) rs' (mk_load_frame sp0 args0 tys0 retty)) m3

| exec_function_external:
    forall s fb rs m rs' callee args res lf,
      Genv.find_funct_ptr ge fb = Some (External callee) ->
      i64ext callee ->
      external_call callee ge args m E0 res m ->
      rs' = set_pair (loc_result (ef_sig callee)) res rs ->
      step (Core_CallstateOut s fb callee args rs lf) m
           empfp (Core_Returnstate s rs' lf) m
           
| exec_return:
    forall s f sp ra c rs m lf,
      step (Core_Returnstate (Stackframe f sp ra c :: s) rs lf) m
           empfp (Core_State s f sp c rs lf) m.

End RELSEM.

Definition Mach_comp_unit := @comp_unit_generic fundef unit.

Definition init_genv (cu: Mach_comp_unit) (ge G: genv): Prop :=
  ge = G /\ globalenv_generic cu ge.

Definition init_mem : genv -> mem -> Prop := init_mem_generic.


Definition fundef_init (fb: block) (sig: signature) (args: list val) : option core :=
  let tyl := sig_args sig in
  if wd_args args tyl
  then Some (Core_CallstateIn fb args tyl (sig_res sig))
  else None.


Definition init_core (ge : Genv.t fundef unit) (fnid: ident) (args: list val): option core :=
  match Genv.find_symbol ge fnid with
  | Some fb => match Genv.find_funct_ptr ge fb with
              | Some cfd =>
                match cfd with
                | Internal fd => fundef_init fb (funsig cfd) args
                | External _ => None
                end
              | None => None
              end
  | None => None
  end.


Definition at_external (ge: Genv.t fundef unit) (c: core) :
  option (ident * signature * list val) :=
  match c with
  | Core_CallstateOut s fb (EF_external name sig) args rs lf =>
    match invert_symbol_from_string ge name with
    | Some fnid =>
      if peq fnid GAST.ent_atom || peq fnid GAST.ext_atom
      then None
      else Some (fnid, sig, args)
    | _ => None
    end
  | _ => None
 end.

Definition after_external (c: core) (vret: option val) : option core :=
  match c with
    Core_CallstateOut s fb (EF_external name sig) args rs lf =>
    match vret, (sig_res sig) with
      None, None => Some (Core_Returnstate s (set_pair (loc_result sig) Vundef rs) lf)
    | Some v, Some ty =>
      if val_has_type_func v ty
      then Some (Core_Returnstate s (set_pair (loc_result sig) v rs) lf)
      else None
    | _, _ => None
    end
  | _ => None
  end.


Definition halted (c : core): option val :=
  match c with
  | Core_Returnstate nil rs (mk_load_frame _ _ _ sigres) =>
    Some (match (loc_result (mksignature nil sigres cc_default)) with
          | One r => rs r
          | Twolong r1 r2 => Val.longofwords (rs r1) (rs r2)
          end)
  | _ => None
  end.


Section IS.
Variable return_address_offset: function -> code -> ptrofs -> Prop.

Definition Mach_IS :=
  IS_local.Build_sem_local fundef unit genv Mach_comp_unit core init_genv init_mem
                           init_core halted (step return_address_offset) at_external after_external.

End IS.