premier jet Asmblockgenproof.return_address_offset

4 files changed, 98 insertions, 10 deletions

diff --git a/Makefile b/Makefile
index 02cb3cc3..255c43db 100644
--- a/Makefile
+++ b/Makefile
@@ -96,7 +96,7 @@ BACKEND=\
   Mach.v \
   Bounds.v Stacklayout.v Stacking.v Stackingproof.v \
   Machblock.v Machblockgen.v Machblockgenproof.v \
-  Asmblock.v Asmblockgen.v Asmblockgenproof.v \
+  Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof.v \
   Asm.v Asmgen.v Asmgenproof.v
 
 # C front-end modules (in cfrontend/)
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index de00218e..0476e76a 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -17,7 +17,7 @@ Require Import Integers Floats AST Linking.
 Require Import Values Memory Events Globalenvs Smallstep.
 Require Import Op Locations Machblock Conventions Asmblock.
 (* Require Import Asmgen Asmgenproof0 Asmgenproof1. *)
-Require Import Asmblockgen.
+Require Import Asmblockgen Asmblockgenproof0.
 
 Definition match_prog (p: Machblock.program) (tp: Asmblock.program) :=
   match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
@@ -1104,7 +1104,7 @@ Qed.
  *)
 
 Definition return_address_offset : Machblock.function -> Machblock.code -> ptrofs -> Prop := 
-  (fun a b c => False).
+  Asmblockgenproof0.return_address_offset.
 
 Axiom transf_program_correct:
   forward_simulation (Machblock.semantics return_address_offset prog) (Asmblock.semantics tprog).
diff --git a/mppa_k1c/Asmblockgenproof0.v b/mppa_k1c/Asmblockgenproof0.v
new file mode 100644
index 00000000..374ae0d1
--- /dev/null
+++ b/mppa_k1c/Asmblockgenproof0.v
@@ -0,0 +1,95 @@
+Require Import Coqlib.
+Require Intv.
+Require Import AST.
+Require Import Errors.
+Require Import Integers.
+Require Import Floats.
+Require Import Values.
+Require Import Memory.
+Require Import Globalenvs.
+Require Import Events.
+Require Import Smallstep.
+Require Import Locations.
+Require Import Machblock.
+Require Import Asmblock.
+Require Import Asmblockgen.
+
+Module MB:=Machblock.
+Module AB:=Asmblock.
+
+(* inspired from Mach *)
+
+Lemma find_label_tail:
+  forall lbl c c', MB.find_label lbl c = Some c' -> is_tail c' c.
+Proof.
+  induction c; simpl; intros. discriminate.
+  destruct (MB.is_label lbl a). inv H. auto with coqlib. eauto with coqlib.
+Qed.
+
+(* inspired from Asmgenproof0 *)
+
+(* ... skip ... *)
+
+(** The ``code tail'' of an instruction list [c] is the list of instructions
+  starting at PC [pos]. *)
+
+Inductive code_tail: Z -> bblocks -> bblocks -> Prop :=
+  | code_tail_0: forall c,
+      code_tail 0 c c
+  | code_tail_S: forall pos bi c1 c2,
+      code_tail pos c1 c2 ->
+      code_tail (pos + (size bi)) (bi :: c1) c2.
+
+Lemma code_tail_pos:
+  forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0.
+Proof.
+  induction 1. omega. generalize (size_positive bi); intros; omega.
+Qed.
+
+Lemma find_bblock_tail:
+  forall c1 bi c2 pos,
+  code_tail pos c1 (bi :: c2) ->
+  find_bblock pos c1 = Some bi.
+Proof.
+  induction c1; simpl; intros.
+  inversion H.  
+  destruct (zlt pos 0). generalize (code_tail_pos _ _ _ H); intro; omega.
+  destruct (zeq pos 0). subst pos.
+  inv H. auto. generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; omega.
+  inv H. congruence. replace (pos0 + size a - size a) with pos0 by omega.
+  eauto.
+Qed.
+
+(* ... skip ... *)
+
+
+(** Predictor for return addresses in generated Asm code.
+
+  The [return_address_offset] predicate defined here is used in the
+  semantics for Mach to determine the return addresses that are
+  stored in activation records. *)
+
+(** Consider a Mach function [f] and a sequence [c] of Mach instructions
+  representing the Mach code that remains to be executed after a
+  function call returns.  The predicate [return_address_offset f c ofs]
+  holds if [ofs] is the integer offset of the PPC instruction
+  following the call in the Asm code obtained by translating the
+  code of [f]. Graphically:
+<<
+     Mach function f    |--------- Mcall ---------|
+         Mach code c    |                |--------|
+                        |                 \        \
+                        |                  \        \
+                        |                   \        \
+     Asm code           |                    |--------|
+     Asm function       |------------- Pcall ---------|
+
+                        <-------- ofs ------->
+>>
+*)
+
+Definition return_address_offset (f: MB.function) (c: MB.code) (ofs: ptrofs) : Prop :=
+  forall tf  tc,
+  transf_function f = OK tf ->
+  transl_blocks f c = OK tc ->
+  code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) tc.
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index 32e8e8a8..f85445f2 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -42,13 +42,6 @@ Qed.
 
 (** Return Address Offset *)
 
-Inductive code_tail: Z -> code -> code -> Prop :=
-  | code_tail_0: forall c,
-      code_tail 0 c c
-  | code_tail_S: forall pos i c1 c2,
-      code_tail pos c1 c2 ->
-      code_tail (pos + 1) (i :: c1) c2.
-
 Definition return_address_offset (f: Mach.function) (c: Mach.code) (ofs: ptrofs) : Prop :=
   Asmblockgenproof.return_address_offset (Machblockgen.transf_function f) (Machblockgen.trans_code c) ofs.