summaryrefslogtreecommitdiff
path: root/backend/Mach.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Mach.v')
-rw-r--r--backend/Mach.v247
1 files changed, 236 insertions, 11 deletions
diff --git a/backend/Mach.v b/backend/Mach.v
index 56c0369..12c6c9d 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -21,10 +21,14 @@ Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Values.
+Require Import Memory.
Require Import Globalenvs.
+Require Import Events.
+Require Import Smallstep.
Require Import Op.
Require Import Locations.
Require Import Conventions.
+Require Stacklayout.
(** * Abstract syntax *)
@@ -89,13 +93,39 @@ Definition funsig (fd: fundef) :=
Definition genv := Genv.t fundef unit.
-(** * Elements of dynamic semantics *)
-
-(** The operational semantics is in module [Machsem]. *)
+(** * Operational semantics *)
+
+(** 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. *)
Definition chunk_of_type (ty: typ) :=
match ty with Tint => Mint32 | Tfloat => Mfloat64al32 end.
+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.
+
Module RegEq.
Definition t := mreg.
Definition eq := mreg_eq.
@@ -170,15 +200,210 @@ Proof.
destruct (is_label lbl a). inv H. auto with coqlib. eauto with coqlib.
Qed.
-Definition find_function_ptr
- (ge: genv) (ros: mreg + ident) (rs: regset) : option block :=
+Section RELSEM.
+
+Variable ge: genv.
+
+Definition find_function (ros: mreg + ident) (rs: regset) : option fundef :=
match ros with
- | inl r =>
- match rs r with
- | Vptr b ofs => if Int.eq ofs Int.zero then Some b else None
- | _ => None
- end
+ | inl r => Genv.find_funct ge (rs r)
| inr symb =>
- Genv.find_symbol ge symb
+ match Genv.find_symbol ge symb with
+ | None => None
+ | Some b => Genv.find_funct_ptr ge b
+ end
+ end.
+
+(** 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: function) (**r calling function *)
+ (sp: val) (**r stack pointer in calling function *)
+ (c: code), (**r program point in calling function *)
+ stackframe.
+
+Inductive state: Type :=
+ | State:
+ forall (stack: list stackframe) (**r call stack *)
+ (f: function) (**r current function *)
+ (sp: val) (**r stack pointer *)
+ (c: code) (**r current program point *)
+ (rs: regset) (**r register state *)
+ (m: mem), (**r memory state *)
+ state
+ | Callstate:
+ forall (stack: list stackframe) (**r call stack *)
+ (fd: fundef) (**r function to call *)
+ (rs: regset) (**r register state *)
+ (m: mem), (**r memory state *)
+ state
+ | Returnstate:
+ forall (stack: list stackframe) (**r call stack *)
+ (rs: regset) (**r register state *)
+ (m: mem), (**r memory state *)
+ state.
+
+Definition parent_sp (s: list stackframe) : val :=
+ match s with
+ | nil => Vptr Mem.nullptr Int.zero
+ | Stackframe f sp c :: s' => sp
end.
+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 f sp ofs ty dst c rs m v,
+ 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 f sp (Mgetparam ofs ty dst :: c) rs m)
+ E0 (State s f 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 f sp sig ros c rs m fd,
+ find_function ros rs = Some fd ->
+ step (State s f sp (Mcall sig ros :: c) rs m)
+ E0 (Callstate (Stackframe f sp c :: s)
+ fd rs m)
+ | exec_Mtailcall:
+ forall s f stk soff sig ros c rs m fd m' m'',
+ find_function ros rs = Some fd ->
+ load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
+ Mem.free m stk 0 (Int.unsigned f.(fn_retaddr_ofs)) = Some m' ->
+ Mem.free m' stk (Int.unsigned f.(fn_retaddr_ofs) + 4) f.(fn_stacksize) = Some m'' ->
+ step (State s f (Vptr stk soff) (Mtailcall sig ros :: c) rs m)
+ E0 (Callstate s fd 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 f sp lbl c rs m c',
+ find_label lbl f.(fn_code) = Some c' ->
+ step (State s f sp (Mgoto lbl :: c) rs m)
+ E0 (State s f sp c' rs m)
+ | exec_Mcond_true:
+ forall s f sp cond args lbl c rs m c',
+ eval_condition cond rs##args m = Some true ->
+ find_label lbl f.(fn_code) = Some c' ->
+ step (State s f sp (Mcond cond args lbl :: c) rs m)
+ E0 (State s f 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 f sp arg tbl c rs m n lbl c',
+ rs arg = Vint n ->
+ list_nth_z tbl (Int.unsigned n) = Some lbl ->
+ find_label lbl f.(fn_code) = Some c' ->
+ step (State s f sp (Mjumptable arg tbl :: c) rs m)
+ E0 (State s f sp c' (undef_temps rs) m)
+ | exec_Mreturn:
+ forall s f stk soff c rs m m' m'',
+ load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
+ Mem.free m stk 0 (Int.unsigned f.(fn_retaddr_ofs)) = Some m' ->
+ Mem.free m' stk (Int.unsigned f.(fn_retaddr_ofs) + 4) f.(fn_stacksize) = Some m'' ->
+ step (State s f (Vptr stk soff) (Mreturn :: c) rs m)
+ E0 (Returnstate s rs m'')
+ | exec_function_internal:
+ forall s f rs m m1 m2 m3 stk,
+ Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) ->
+ Mem.free m1 stk (Int.unsigned f.(fn_retaddr_ofs)) (Int.unsigned f.(fn_retaddr_ofs) + 4) = Some m2 ->
+ let sp := Vptr stk Int.zero in
+ store_stack m2 sp Tint f.(fn_link_ofs) (parent_sp s) = Some m3 ->
+ (4 | Int.unsigned f.(fn_retaddr_ofs)) ->
+ step (Callstate s (Internal f) rs m)
+ E0 (State s f sp f.(fn_code) (undef_temps rs) m3)
+ | exec_function_external:
+ forall s ef rs m t rs' args res m',
+ 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 (External ef) rs m)
+ t (Returnstate s rs' m')
+ | exec_return:
+ forall s f sp c rs m,
+ step (Returnstate (Stackframe f sp 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 b fd 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 fd ->
+ initial_state p (Callstate nil fd (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).
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-07 15:11:24 +0000