summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-03-14 08:18:42 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-03-14 08:18:42 +0000
commite44df4563f1cb893ab25b2a8b25d5b83095205be (patch)
treee7b440e4fb6b0d941e477bfc87962f39d1943dee
parent8bc231b13803a3d9d5e1f90a7f8d768b202a66b3 (diff)
Machsem: no longer useful.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2150 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r--backend/Machsem.v259
1 files changed, 0 insertions, 259 deletions
diff --git a/backend/Machsem.v b/backend/Machsem.v
deleted file mode 100644
index 60762c0..0000000
--- a/backend/Machsem.v
+++ /dev/null
@@ -1,259 +0,0 @@
-(* *********************************************************************)
-(* *)
-(* The Compcert verified compiler *)
-(* *)
-(* Xavier Leroy, INRIA Paris-Rocquencourt *)
-(* *)
-(* Copyright Institut National de Recherche en Informatique et en *)
-(* Automatique. All rights reserved. This file is distributed *)
-(* under the terms of the INRIA Non-Commercial License Agreement. *)
-(* *)
-(* *********************************************************************)
-
-(** The Mach intermediate language: operational semantics. *)
-
-Require Import Coqlib.
-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.
-
-(** 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: 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.
-
-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 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 ge 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 ge 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).