Machsem: no longer useful.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2150 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

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).