From 2ae43be7b9d4118335c9d2cef6e098f9b9f807fe Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Thu, 9 Feb 2006 14:55:48 +0000
Subject: Initial import of compcert

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/Machabstr.v | 371 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 371 insertions(+)
 create mode 100644 backend/Machabstr.v

(limited to 'backend/Machabstr.v')

diff --git a/backend/Machabstr.v b/backend/Machabstr.v
new file mode 100644
index 00000000..25458dcc
--- /dev/null
+++ b/backend/Machabstr.v
@@ -0,0 +1,371 @@
+(** Alternate semantics for the Mach intermediate language. *)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Mem.
+Require Import Integers.
+Require Import Values.
+Require Import Mem.
+Require Import Globalenvs.
+Require Import Op.
+Require Import Locations.
+Require Conventions.
+Require Import Mach.
+
+(** This file defines an alternate semantics for the Mach intermediate
+  language, which differ from the standard semantics given in file [Mach]
+  as follows: the stack access instructions [Mgetstack], [Msetstack]
+  and [Mgetparam] are interpreted not as memory accesses, but as
+  accesses in a frame environment, not resident in memory.  The evaluation
+  relations take two such frame environments as parameters and results,
+  one for the current function and one for its caller. 
+
+  Not having the frame data in memory facilitates the proof of
+  the [Stacking] pass, which shows that the generated code executes
+  correctly with the alternate semantics.  In file [Machabstr2mach],
+  we show an implication from this alternate semantics to
+  the standard semantics, thus establishing that the [Stacking] pass
+  generates code that behaves correctly against the standard [Mach]
+  semantics as well. *)
+
+(** * Structure of abstract stack frames *)
+
+(** A frame has the same structure as the contents of a memory block. *)
+
+Definition frame := block_contents.
+
+Definition empty_frame := empty_block 0 0.
+
+Definition mem_type (ty: typ) :=
+  match ty with Tint => Size32 | Tfloat => Size64 end.
+
+(** [get_slot fr ty ofs v] holds if the frame [fr] contains value [v]
+  with type [ty] at word offset [ofs]. *)
+
+Inductive get_slot: frame -> typ -> Z -> val -> Prop :=
+  | get_slot_intro:
+      forall fr ty ofs v,
+      0 <= ofs ->
+      fr.(low) + ofs + 4 * typesize ty <= 0 ->
+      v = load_contents (mem_type ty) fr.(contents) (fr.(low) + ofs) -> 
+      get_slot fr ty ofs v.
+
+Remark size_mem_type:
+  forall ty, size_mem (mem_type ty) = 4 * typesize ty.
+Proof.
+  destruct ty; reflexivity.
+Qed.
+
+Remark set_slot_undef_outside:
+  forall fr ty ofs v,
+  fr.(high) = 0 ->
+  0 <= ofs ->
+  fr.(low) + ofs + 4 * typesize ty <= 0 ->
+  (forall x, x < fr.(low) \/ x >= fr.(high) -> fr.(contents) x = Undef) ->
+  (forall x, x < fr.(low) \/ x >= fr.(high) ->
+     store_contents (mem_type ty) fr.(contents) (fr.(low) + ofs) v x = Undef).
+Proof.
+  intros. apply store_contents_undef_outside with fr.(low) fr.(high).
+  rewrite <- size_mem_type in H1. omega. assumption. assumption.
+Qed.  
+
+(** [set_slot fr ty ofs v fr'] holds if frame [fr'] is obtained from
+  frame [fr] by storing value [v] with type [ty] at word offset [ofs]. *)
+
+Inductive set_slot: frame -> typ -> Z -> val -> frame -> Prop :=
+  | set_slot_intro:
+      forall fr ty ofs v
+      (A: fr.(high) = 0)
+      (B: 0 <= ofs)
+      (C: fr.(low) + ofs + 4 * typesize ty <= 0),
+      set_slot fr ty ofs v
+        (mkblock fr.(low) fr.(high)
+          (store_contents (mem_type ty) fr.(contents) (fr.(low) + ofs) v)
+          (set_slot_undef_outside fr ty ofs v A B C fr.(undef_outside))).
+
+Definition init_frame (f: function) :=
+  empty_block (- f.(fn_framesize)) 0.
+
+Section RELSEM.
+
+Variable ge: genv.
+
+(** Execution of one instruction has the form
+  [exec_instr ge f sp parent c rs fr m c' rs' fr' m'],
+  where [parent] is the caller's frame (read-only)
+  and [fr], [fr'] are the current frame, before and after execution
+  of one instruction.  The other parameters are as in the Mach semantics. *)
+
+Inductive exec_instr:
+      function -> val -> frame ->
+      code -> regset -> frame -> mem ->
+      code -> regset -> frame -> mem -> Prop :=
+  | exec_Mlabel:
+      forall f sp parent lbl c rs fr m,
+      exec_instr f sp parent
+                 (Mlabel lbl :: c) rs fr m
+                 c rs fr m
+  | exec_Mgetstack:
+      forall f sp parent ofs ty dst c rs fr m v,
+      get_slot fr ty (Int.signed ofs) v ->
+      exec_instr f sp parent
+                 (Mgetstack ofs ty dst :: c) rs fr m
+                 c (rs#dst <- v) fr m
+  | exec_Msetstack:
+     forall f sp parent src ofs ty c rs fr m fr',
+      set_slot fr ty (Int.signed ofs) (rs src) fr' ->
+      exec_instr f sp parent
+                 (Msetstack src ofs ty :: c) rs fr m
+                 c rs fr' m
+  | exec_Mgetparam:
+      forall f sp parent ofs ty dst c rs fr m v,
+      get_slot parent ty (Int.signed ofs) v ->
+      exec_instr f sp parent
+                 (Mgetparam ofs ty dst :: c) rs fr m
+                 c (rs#dst <- v) fr m
+  | exec_Mop:
+      forall f sp parent op args res c rs fr m v,
+      eval_operation ge sp op rs##args = Some v ->
+      exec_instr f sp parent
+                 (Mop op args res :: c) rs fr m
+                 c (rs#res <- v) fr m
+  | exec_Mload:
+      forall f sp parent chunk addr args dst c rs fr m a v,
+      eval_addressing ge sp addr rs##args = Some a ->
+      Mem.loadv chunk m a = Some v ->
+      exec_instr f sp parent
+                 (Mload chunk addr args dst :: c) rs fr m
+                 c (rs#dst <- v) fr m
+  | exec_Mstore:
+      forall f sp parent chunk addr args src c rs fr m m' a,
+      eval_addressing ge sp addr rs##args = Some a ->
+      Mem.storev chunk m a (rs src) = Some m' ->
+      exec_instr f sp parent
+                 (Mstore chunk addr args src :: c) rs fr m
+                 c rs fr m'
+  | exec_Mcall:
+      forall f sp parent sig ros c rs fr m f' rs' m',
+      find_function ge ros rs = Some f' ->
+      exec_function f' fr rs m rs' m' ->
+      exec_instr f sp parent
+                 (Mcall sig ros :: c) rs fr m
+                 c rs' fr m'
+  | exec_Mgoto:
+      forall f sp parent lbl c rs fr m c',
+      find_label lbl f.(fn_code) = Some c' ->
+      exec_instr f sp parent
+                 (Mgoto lbl :: c) rs fr m
+                 c' rs fr m
+  | exec_Mcond_true:
+      forall f sp parent cond args lbl c rs fr m c',
+      eval_condition cond rs##args = Some true ->
+      find_label lbl f.(fn_code) = Some c' ->
+      exec_instr f sp parent
+                 (Mcond cond args lbl :: c) rs fr m
+                 c' rs fr m
+  | exec_Mcond_false:
+      forall f sp parent cond args lbl c rs fr m,
+      eval_condition cond rs##args = Some false ->
+      exec_instr f sp parent
+                 (Mcond cond args lbl :: c) rs fr m
+                 c rs fr m
+
+with exec_instrs:
+      function -> val -> frame ->
+      code -> regset -> frame -> mem ->
+      code -> regset -> frame -> mem -> Prop :=
+  | exec_refl:
+      forall f sp parent c rs fr m,
+      exec_instrs f sp parent  c rs fr m  c rs fr m
+  | exec_one:
+      forall f sp parent c rs fr m c' rs' fr' m',
+      exec_instr f sp parent  c rs fr m  c' rs' fr' m' ->
+      exec_instrs f sp parent  c rs fr m  c' rs' fr' m'
+  | exec_trans:
+      forall f sp parent c1 rs1 fr1 m1 c2 rs2 fr2 m2 c3 rs3 fr3 m3,
+      exec_instrs f sp parent  c1 rs1 fr1 m1  c2 rs2 fr2 m2 ->
+      exec_instrs f sp parent  c2 rs2 fr2 m2  c3 rs3 fr3 m3 ->
+      exec_instrs f sp parent  c1 rs1 fr1 m1  c3 rs3 fr3 m3
+
+with exec_function_body:
+      function -> frame -> val -> val ->
+      regset -> mem -> regset -> mem -> Prop :=
+  | exec_funct_body:
+      forall f parent link ra rs m rs' m1 m2 stk fr1 fr2 fr3 c,
+      Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) ->
+      set_slot (init_frame f) Tint 0 link fr1 ->
+      set_slot fr1 Tint 4 ra fr2 ->
+      exec_instrs f (Vptr stk (Int.repr (-f.(fn_framesize)))) parent
+                  f.(fn_code) rs fr2 m1
+                  (Mreturn :: c) rs' fr3 m2 ->
+      exec_function_body f parent link ra rs m rs' (Mem.free m2 stk)
+
+with exec_function:
+      function -> frame -> regset -> mem -> regset -> mem -> Prop :=
+  | exec_funct:
+      forall f parent rs m rs' m',
+      (forall link ra, 
+         Val.has_type link Tint ->
+         Val.has_type ra Tint ->
+         exec_function_body f parent link ra rs m rs' m') ->
+      exec_function f parent rs m rs' m'.
+
+Scheme exec_instr_ind4 := Minimality for exec_instr Sort Prop
+  with exec_instrs_ind4 := Minimality for exec_instrs Sort Prop
+  with exec_function_body_ind4 := Minimality for exec_function_body Sort Prop
+  with exec_function_ind4 := Minimality for exec_function Sort Prop.
+
+(** Ugly mutual induction principle over evaluation derivations.
+  Coq is not able to generate it directly, even though it is
+  an immediate consequence of the 4 induction principles generated
+  by the [Scheme] command above. *)
+
+Lemma exec_mutual_induction:
+  forall (P
+          P0 : function ->
+               val ->
+               frame ->
+               code ->
+               regset ->
+               frame -> mem -> code -> regset -> frame -> mem -> Prop)
+         (P1 : function ->
+               frame -> val -> val -> regset -> mem -> regset -> mem -> Prop)
+         (P2 : function -> frame -> regset -> mem -> regset -> mem -> Prop),
+       (forall (f : function) (sp : val) (parent : frame) (lbl : label)
+          (c : list instruction) (rs : regset) (fr : frame) (m : mem),
+        P f sp parent (Mlabel lbl :: c) rs fr m c rs fr m) ->
+       (forall (f : function) (sp : val) (parent : frame) (ofs : int)
+          (ty : typ) (dst : mreg) (c : list instruction) (rs : regset)
+          (fr : frame) (m : mem) (v : val),
+        get_slot fr ty (Int.signed ofs) v ->
+        P f sp parent (Mgetstack ofs ty dst :: c) rs fr m c rs # dst <- v fr
+          m) ->
+       (forall (f : function) (sp : val) (parent : frame) (src : mreg)
+          (ofs : int) (ty : typ) (c : list instruction) (rs : mreg -> val)
+          (fr : frame) (m : mem) (fr' : frame),
+        set_slot fr ty (Int.signed ofs) (rs src) fr' ->
+        P f sp parent (Msetstack src ofs ty :: c) rs fr m c rs fr' m) ->
+       (forall (f : function) (sp : val) (parent : frame) (ofs : int)
+          (ty : typ) (dst : mreg) (c : list instruction) (rs : regset)
+          (fr : frame) (m : mem) (v : val),
+        get_slot parent ty (Int.signed ofs) v ->
+        P f sp parent (Mgetparam ofs ty dst :: c) rs fr m c rs # dst <- v fr
+          m) ->
+       (forall (f : function) (sp : val) (parent : frame) (op : operation)
+          (args : list mreg) (res : mreg) (c : list instruction)
+          (rs : mreg -> val) (fr : frame) (m : mem) (v : val),
+        eval_operation ge sp op rs ## args = Some v ->
+        P f sp parent (Mop op args res :: c) rs fr m c rs # res <- v fr m) ->
+       (forall (f : function) (sp : val) (parent : frame)
+          (chunk : memory_chunk) (addr : addressing) (args : list mreg)
+          (dst : mreg) (c : list instruction) (rs : mreg -> val) (fr : frame)
+          (m : mem) (a v : val),
+        eval_addressing ge sp addr rs ## args = Some a ->
+        loadv chunk m a = Some v ->
+        P f sp parent (Mload chunk addr args dst :: c) rs fr m c
+          rs # dst <- v fr m) ->
+       (forall (f : function) (sp : val) (parent : frame)
+          (chunk : memory_chunk) (addr : addressing) (args : list mreg)
+          (src : mreg) (c : list instruction) (rs : mreg -> val) (fr : frame)
+          (m m' : mem) (a : val),
+        eval_addressing ge sp addr rs ## args = Some a ->
+        storev chunk m a (rs src) = Some m' ->
+        P f sp parent (Mstore chunk addr args src :: c) rs fr m c rs fr m') ->
+       (forall (f : function) (sp : val) (parent : frame) (sig : signature)
+          (ros : mreg + ident) (c : list instruction) (rs : regset)
+          (fr : frame) (m : mem) (f' : function) (rs' : regset) (m' : mem),
+        find_function ge ros rs = Some f' ->
+        exec_function f' fr rs m rs' m' ->
+        P2 f' fr rs m rs' m' ->
+        P f sp parent (Mcall sig ros :: c) rs fr m c rs' fr m') ->
+       (forall (f : function) (sp : val) (parent : frame) (lbl : label)
+          (c : list instruction) (rs : regset) (fr : frame) (m : mem)
+          (c' : code),
+        find_label lbl (fn_code f) = Some c' ->
+        P f sp parent (Mgoto lbl :: c) rs fr m c' rs fr m) ->
+       (forall (f : function) (sp : val) (parent : frame)
+          (cond : condition) (args : list mreg) (lbl : label)
+          (c : list instruction) (rs : mreg -> val) (fr : frame) (m : mem)
+          (c' : code),
+        eval_condition cond rs ## args = Some true ->
+        find_label lbl (fn_code f) = Some c' ->
+        P f sp parent (Mcond cond args lbl :: c) rs fr m c' rs fr m) ->
+       (forall (f : function) (sp : val) (parent : frame)
+          (cond : condition) (args : list mreg) (lbl : label)
+          (c : list instruction) (rs : mreg -> val) (fr : frame) (m : mem),
+        eval_condition cond rs ## args = Some false ->
+        P f sp parent (Mcond cond args lbl :: c) rs fr m c rs fr m) ->
+       (forall (f : function) (sp : val) (parent : frame) (c : code)
+          (rs : regset) (fr : frame) (m : mem),
+        P0 f sp parent c rs fr m c rs fr m) ->
+       (forall (f : function) (sp : val) (parent : frame) (c : code)
+          (rs : regset) (fr : frame) (m : mem) (c' : code) (rs' : regset)
+          (fr' : frame) (m' : mem),
+        exec_instr f sp parent c rs fr m c' rs' fr' m' ->
+        P f sp parent c rs fr m c' rs' fr' m' ->
+        P0 f sp parent c rs fr m c' rs' fr' m') ->
+       (forall (f : function) (sp : val) (parent : frame) (c1 : code)
+          (rs1 : regset) (fr1 : frame) (m1 : mem) (c2 : code) (rs2 : regset)
+          (fr2 : frame) (m2 : mem) (c3 : code) (rs3 : regset) (fr3 : frame)
+          (m3 : mem),
+        exec_instrs f sp parent c1 rs1 fr1 m1 c2 rs2 fr2 m2 ->
+        P0 f sp parent c1 rs1 fr1 m1 c2 rs2 fr2 m2 ->
+        exec_instrs f sp parent c2 rs2 fr2 m2 c3 rs3 fr3 m3 ->
+        P0 f sp parent c2 rs2 fr2 m2 c3 rs3 fr3 m3 ->
+        P0 f sp parent c1 rs1 fr1 m1 c3 rs3 fr3 m3) ->
+       (forall (f : function) (parent : frame) (link ra : val) (rs : regset)
+          (m : mem) (rs' : regset) (m1 m2 : mem) (stk : block)
+          (fr1 fr2 fr3 : frame) (c : list instruction),
+        alloc m 0 (fn_stacksize f) = (m1, stk) ->
+        set_slot (init_frame f) Tint 0 link fr1 ->
+        set_slot fr1 Tint 4 ra fr2 ->
+        exec_instrs f (Vptr stk (Int.repr (-f.(fn_framesize)))) parent (fn_code f) rs fr2 m1 (Mreturn :: c) rs' fr3
+          m2 ->
+        P0 f (Vptr stk (Int.repr (-f.(fn_framesize)))) parent (fn_code f) rs fr2 m1 (Mreturn :: c) rs' fr3 m2 ->
+        P1 f parent link ra rs m rs' (free m2 stk)) ->
+       (forall (f : function) (parent : frame) (rs : regset) (m : mem)
+          (rs' : regset) (m' : mem),
+        (forall link ra : val,
+         Val.has_type link Tint ->
+         Val.has_type ra Tint ->
+         exec_function_body f parent link ra rs m rs' m') ->
+        (forall link ra : val,
+         Val.has_type link Tint ->
+         Val.has_type ra Tint -> P1 f parent link ra rs m rs' m') ->
+        P2 f parent rs m rs' m') ->
+       (forall (f15 : function) (sp : val) (f16 : frame) (c : code)
+         (r : regset) (f17 : frame) (m : mem) (c0 : code) (r0 : regset)
+         (f18 : frame) (m0 : mem),
+       exec_instr f15 sp f16 c r f17 m c0 r0 f18 m0 ->
+       P f15 sp f16 c r f17 m c0 r0 f18 m0)
+   /\  (forall (f15 : function) (sp : val) (f16 : frame) (c : code)
+         (r : regset) (f17 : frame) (m : mem) (c0 : code) (r0 : regset)
+         (f18 : frame) (m0 : mem),
+       exec_instrs f15 sp f16 c r f17 m c0 r0 f18 m0 ->
+       P0 f15 sp f16 c r f17 m c0 r0 f18 m0)
+   /\  (forall (f15 : function) (f16 : frame) (v1 v2 : val) (r : regset) (m : mem)
+         (r0 : regset) (m0 : mem),
+       exec_function_body f15 f16 v1 v2 r m r0 m0 -> P1 f15 f16 v1 v2 r m r0 m0)
+   /\  (forall (f15 : function) (f16 : frame) (r : regset) (m : mem)
+         (r0 : regset) (m0 : mem),
+       exec_function f15 f16 r m r0 m0 -> P2 f15 f16 r m r0 m0).
+Proof.
+  intros. split. apply (exec_instr_ind4 P P0 P1 P2); assumption.
+  split. apply (exec_instrs_ind4 P P0 P1 P2); assumption.
+  split. apply (exec_function_body_ind4 P P0 P1 P2); assumption.
+  apply (exec_function_ind4 P P0 P1 P2); assumption.
+Qed.
+
+End RELSEM.
+
+Definition exec_program (p: program) (r: val) : Prop :=
+  let ge := Genv.globalenv p in
+  let m0 := Genv.init_mem p in
+  exists b, exists f, exists rs, exists m,
+  Genv.find_symbol ge p.(prog_main) = Some b /\
+  Genv.find_funct_ptr ge b = Some f /\
+  f.(fn_sig) = mksignature nil (Some Tint) /\
+  exec_function ge f empty_frame (Regmap.init Vundef) m0 rs m /\
+  rs (Conventions.loc_result f.(fn_sig)) = r.
+
-- 
cgit