Module Machsem

The Mach intermediate language: operational semantics.

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

The semantics for Mach is close to that of Linear: they differ only on the interpretation of stack slot accesses. In Mach, these accesses are interpreted as memory accesses relative to the stack pointer. More precisely:

Mgetstack ofs ty r is a memory load at offset ofs * 4 relative to the stack pointer.
Msetstack r ofs ty is a memory store at offset ofs * 4 relative to the stack pointer.
Mgetparam ofs ty r is a memory load at offset ofs * 4 relative to the pointer found at offset 0 from the stack pointer. The semantics maintain a linked structure of activation records, with the current record containing a pointer to the record of the caller function at offset 0.

In addition to this linking of activation records, the semantics also make provisions for storing a back link at offset f.(fn_link_ofs) from the stack pointer, and a return address at offset f.(fn_retaddr_ofs). The latter stack location will be used by the Asm code generated by Asmgen to save the return address into the caller at the beginning of a function, then restore it and jump to it at the end of a function. The Mach concrete semantics does not attach any particular meaning to the pointer stored in this reserved location, but makes sure that it is preserved during execution of a function. The return_address_offset predicate from module Asmgenretaddr is used to guess the value of the return address that the Asm code generated later will store in the reserved location.

Definition load_stack (m: mem) (sp: val) (ty: typ) (ofs: int) :=
Mem.loadv (chunk_of_type ty) m (Val.add sp (Vint ofs)).

Definition store_stack (m: mem) (sp: val) (ty: typ) (ofs: int) (v: val) :=
Mem.storev (chunk_of_type ty) m (Val.add sp (Vint ofs)) v.

Extract the values of the arguments to an external call.

Inductive extcall_arg: regset -> mem -> val -> loc -> val -> Prop :=
  | extcall_arg_reg: forall rs m sp r,
      extcall_arg rs m sp (R r) (rs r)
  | extcall_arg_stack: forall rs m sp ofs ty v,
      load_stack m sp ty (Int.repr (Stacklayout.fe_ofs_arg + 4 * ofs)) = Some v ->
      extcall_arg rs m sp (S (Outgoing ofs ty)) v.

Definition extcall_arguments
    (rs: regset) (m: mem) (sp: val) (sg: signature) (args: list val) : Prop :=
  list_forall2 (extcall_arg rs m sp) (loc_arguments sg) args.

Extract the values of the arguments to an annotation.

Inductive annot_arg: regset -> mem -> val -> annot_param -> val -> Prop :=
  | annot_arg_reg: forall rs m sp r,
      annot_arg rs m sp (APreg r) (rs r)
  | annot_arg_stack: forall rs m stk base chunk ofs v,
      Mem.load chunk m stk (Int.unsigned base + ofs) = Some v ->
      annot_arg rs m (Vptr stk base) (APstack chunk ofs) v.

Definition annot_arguments
   (rs: regset) (m: mem) (sp: val) (params: list annot_param) (args: list val) : Prop :=
  list_forall2 (annot_arg rs m sp) params args.

Mach execution states.

Inductive stackframe: Type :=
  | Stackframe:
      forall (f: block) (* pointer to calling function *)
             (sp: val) (* stack pointer in calling function *)
             (retaddr: val) (* Asm return address in calling function *)
             (c: code), (* program point in calling function *)
      stackframe.

Inductive state: Type :=
  | 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 *)
             (m: mem), (* memory state *)
      state
  | Callstate:
      forall (stack: list stackframe) (* call stack *)
             (f: block) (* pointer to function to call *)
             (rs: regset) (* register state *)
             (m: mem), (* memory state *)
      state
  | Returnstate:
      forall (stack: list stackframe) (* call stack *)
             (rs: regset) (* register state *)
             (m: mem), (* memory state *)
      state.

Definition parent_sp (s: list stackframe) : val :=
  match s with
  | nil => Vptr Mem.nullptr Int.zero
  | Stackframe f sp ra c :: s' => sp
  end.

Definition parent_ra (s: list stackframe) : val :=
  match s with
  | nil => Vzero
  | Stackframe f sp ra c :: s' => ra
  end.

Section RELSEM.

Variable ge: genv.

Inductive step: state -> trace -> state -> Prop :=
  | exec_Mlabel:
      forall s f sp lbl c rs m,
      step (State s f sp (Mlabel lbl :: c) rs m)
        E0 (State s f sp c rs m)
  | exec_Mgetstack:
      forall s f sp ofs ty dst c rs m v,
      load_stack m sp ty ofs = Some v ->
      step (State s f sp (Mgetstack ofs ty dst :: c) rs m)
        E0 (State s f sp c (rs#dst <- v) m)
  | exec_Msetstack:
      forall s f sp src ofs ty c rs m m',
      store_stack m sp ty ofs (rs src) = Some m' ->
      step (State s f sp (Msetstack src ofs ty :: c) rs m)
        E0 (State s f sp c (undef_setstack rs) m')
  | exec_Mgetparam:
      forall s fb f sp ofs ty dst c rs m v,
      Genv.find_funct_ptr ge fb = Some (Internal f) ->
      load_stack m sp Tint f.(fn_link_ofs) = Some (parent_sp s) ->
      load_stack m (parent_sp s) ty ofs = Some v ->
      step (State s fb sp (Mgetparam ofs ty dst :: c) rs m)
        E0 (State s fb sp c (rs # IT1 <- Vundef # dst <- v) m)
  | exec_Mop:
      forall s f sp op args res c rs m v,
      eval_operation ge sp op rs##args m = Some v ->
      step (State s f sp (Mop op args res :: c) rs m)
        E0 (State s f sp c ((undef_op op rs)#res <- v) m)
  | exec_Mload:
      forall s f sp chunk addr args dst c rs m a v,
      eval_addressing ge sp addr rs##args = Some a ->
      Mem.loadv chunk m a = Some v ->
      step (State s f sp (Mload chunk addr args dst :: c) rs m)
        E0 (State s f sp c ((undef_temps rs)#dst <- v) m)
  | exec_Mstore:
      forall s f sp chunk addr args src c rs m m' a,
      eval_addressing ge sp addr rs##args = Some a ->
      Mem.storev chunk m a (rs src) = Some m' ->
      step (State s f sp (Mstore chunk addr args src :: c) rs m)
        E0 (State s f sp c (undef_temps rs) m')
  | exec_Mcall:
      forall s fb sp sig ros c rs m f f' ra,
      find_function_ptr ge ros rs = Some f' ->
      Genv.find_funct_ptr ge fb = Some (Internal f) ->
      Asmgenretaddr.return_address_offset f c ra ->
      step (State s fb sp (Mcall sig ros :: c) rs m)
        E0 (Callstate (Stackframe fb sp (Vptr fb ra) c :: s)
                       f' rs m)
  | exec_Mtailcall:
      forall s fb stk soff sig ros c rs m f f' m',
      find_function_ptr ge 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_sp s) ->
      load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
      step (State s fb (Vptr stk soff) (Mtailcall sig ros :: c) rs m)
        E0 (Callstate s f' rs m')
  | exec_Mbuiltin:
      forall s f sp rs m ef args res b t v m',
      external_call ef ge rs##args m t v m' ->
      step (State s f sp (Mbuiltin ef args res :: b) rs m)
         t (State s f sp b ((undef_temps rs)#res <- v) m')
  | exec_Mannot:
      forall s f sp rs m ef args b vargs t v m',
      annot_arguments rs m sp args vargs ->
      external_call ef ge vargs m t v m' ->
      step (State s f sp (Mannot ef args :: b) rs m)
         t (State s f sp b rs m')
  | exec_Mgoto:
      forall s fb f sp lbl c rs m c',
      Genv.find_funct_ptr ge fb = Some (Internal f) ->
      find_label lbl f.(fn_code) = Some c' ->
      step (State s fb sp (Mgoto lbl :: c) rs m)
        E0 (State s fb sp c' rs m)
  | exec_Mcond_true:
      forall s fb f sp cond args lbl c rs m c',
      eval_condition cond rs##args m = Some true ->
      Genv.find_funct_ptr ge fb = Some (Internal f) ->
      find_label lbl f.(fn_code) = Some c' ->
      step (State s fb sp (Mcond cond args lbl :: c) rs m)
        E0 (State s fb sp c' (undef_temps rs) m)
  | exec_Mcond_false:
      forall s f sp cond args lbl c rs m,
      eval_condition cond rs##args m = Some false ->
      step (State s f sp (Mcond cond args lbl :: c) rs m)
        E0 (State s f sp c (undef_temps rs) m)
  | exec_Mjumptable:
      forall s fb f sp arg tbl c rs m n lbl c',
      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' ->
      step (State s fb sp (Mjumptable arg tbl :: c) rs m)
        E0 (State s fb sp c' (undef_temps rs) m)
  | exec_Mreturn:
      forall s fb stk soff c rs m f m',
      Genv.find_funct_ptr ge fb = Some (Internal f) ->
      load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
      load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
      step (State s fb (Vptr stk soff) (Mreturn :: c) rs m)
        E0 (Returnstate s rs m')
  | exec_function_internal:
      forall s fb rs m f m1 m2 m3 stk,
      Genv.find_funct_ptr ge fb = Some (Internal f) ->
      Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) ->
      let sp := Vptr stk Int.zero in
      store_stack m1 sp Tint f.(fn_link_ofs) (parent_sp s) = Some m2 ->
      store_stack m2 sp Tint f.(fn_retaddr_ofs) (parent_ra s) = Some m3 ->
      step (Callstate s fb rs m)
        E0 (State s fb sp f.(fn_code) (undef_temps rs) m3)
  | exec_function_external:
      forall s fb rs m t rs' ef args res m',
      Genv.find_funct_ptr ge fb = Some (External ef) ->
      external_call ef ge args m t res m' ->
      extcall_arguments rs m (parent_sp s) (ef_sig ef) args ->
      rs' = (rs#(loc_result (ef_sig ef)) <- res) ->
      step (Callstate s fb rs m)
         t (Returnstate s rs' m')
  | exec_return:
      forall s f sp ra c rs m,
      step (Returnstate (Stackframe f sp ra c :: s) rs m)
        E0 (State s f sp c rs m).

End RELSEM.

Inductive initial_state (p: program): state -> Prop :=
  | initial_state_intro: forall fb m0,
      let ge := Genv.globalenv p in
      Genv.init_mem p = Some m0 ->
      Genv.find_symbol ge p.(prog_main) = Some fb ->
      initial_state p (Callstate nil fb (Regmap.init Vundef) m0).

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

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