From e44df4563f1cb893ab25b2a8b25d5b83095205be Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 14 Mar 2013 08:18:42 +0000 Subject: Machsem: no longer useful. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2150 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Machsem.v | 259 ------------------------------------------------------ 1 file changed, 259 deletions(-) delete mode 100644 backend/Machsem.v (limited to 'backend') 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). -- cgit v1.2.3