return_address suite

4 files changed, 137 insertions, 17 deletions

diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 79c28fe9..cc3038ca 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -872,20 +872,28 @@ Fixpoint transl_blocks (f: Machblock.function) (lmb: list Machblock.bblock) :=
   end
 .
 
-Definition transf_function (f: Machblock.function) :=
+
+
+Definition transl_function (f: Machblock.function) :=
   do lb <- transl_blocks f f.(Machblock.fn_code);
   OK (mkfunction f.(Machblock.fn_sig)
         (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::b
          Pget GPR8 RA ::b
          storeind_ptr GPR8 SP f.(fn_retaddr_ofs) ::b lb)).
 
-(* TODO TODO - move this check to Asm *)
-(* Definition transf_function (f: Machblock.function) : res Asmblock.function :=
+Fixpoint size_blocks (l: bblocks): Z :=
+  match l with
+  | nil => 0
+  | b :: l =>
+     (size b) + (size_blocks l)
+  end
+  .
+
+Definition transf_function (f: Machblock.function) : res Asmblock.function :=
   do tf <- transl_function f;
-  if zlt Ptrofs.max_unsigned (list_length_z tf.(fn_code))
+  if zlt Ptrofs.max_unsigned (size_blocks tf.(fn_blocks))
   then Error (msg "code size exceeded")
   else OK tf.
- *)
 
 
 Definition transf_fundef (f: Machblock.fundef) : res Asmblock.fundef :=
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index 0476e76a..92d813b2 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -479,14 +479,17 @@ Proof.
   generalize (transf_function_no_overflow _ _ H0). omega.
   intros. apply Pregmap.gso; auto.
 Qed.
+*)
 
 (** Existence of return addresses *)
 
 Lemma return_address_exists:
-  forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) ->
+  forall b f sg ros c, b.(MB.exit) = Some (MBcall sg ros) -> is_tail (b :: c) f.(MB.fn_code) ->
   exists ra, return_address_offset f c ra.
 Proof.
-  intros. eapply Asmgenproof0.return_address_exists; eauto.
+  intros. eapply Asmblockgenproof0.return_address_exists; eauto.
+Admitted.
+(*
 - intros. exploit transl_instr_label; eauto.
   destruct i; try (intros [A B]; apply A). intros. subst c0. repeat constructor.
 - intros. monadInv H0.
@@ -496,7 +499,8 @@ Proof.
   constructor. apply is_tail_cons. apply (storeind_ptr_label GPR8 GPR12 (fn_retaddr_ofs f0) x).
 - exact transf_function_no_overflow.
 Qed.
- *)
+*)
+
 (** * Proof of semantic preservation *)
 
 (** Semantic preservation is proved using simulation diagrams
diff --git a/mppa_k1c/Asmblockgenproof0.v b/mppa_k1c/Asmblockgenproof0.v
index b1c71f42..18e00601 100644
--- a/mppa_k1c/Asmblockgenproof0.v
+++ b/mppa_k1c/Asmblockgenproof0.v
@@ -60,7 +60,62 @@ Proof.
   eauto.
 Qed.
 
-(* ... skip ... *)
+
+Local Hint Resolve code_tail_0 code_tail_S.
+
+Lemma code_tail_next:
+  forall fn ofs c0,
+  code_tail ofs fn c0 ->
+  forall bi c1, c0 = bi :: c1 -> code_tail (ofs + (size bi)) fn c1.
+Proof.
+  induction 1; intros.
+  - subst; eauto.
+  - replace (pos + size bi + size bi0) with ((pos + size bi0) + size bi); eauto.
+    omega.
+Qed.
+
+Lemma size_blocks_pos c: size_blocks c >= 0.
+Proof.
+  induction c as [| a l ]; simpl; try omega.
+  generalize (size_positive a); omega.
+Qed.
+
+Remark code_tail_bounds_1:
+  forall fn ofs c,
+  code_tail ofs fn c -> 0 <= ofs <= size_blocks fn.
+Proof.
+  induction 1; intros; simpl.
+  generalize (size_blocks_pos c). omega.
+  generalize (size_positive bi). omega.
+Qed.
+
+
+Remark code_tail_bounds_2:
+  forall fn ofs i c,
+  code_tail ofs fn (i :: c) -> 0 <= ofs < size_blocks fn.
+Admitted.
+(*
+  assert (forall ofs fn c, code_tail ofs fn c ->
+          forall i c', c = i :: c' -> 0 <= ofs < list_length_z fn).
+  induction 1; intros; simpl.
+  rewrite H. rewrite list_length_z_cons. generalize (list_length_z_pos c'). omega.
+  rewrite list_length_z_cons. generalize (IHcode_tail _ _ H0). omega.
+  eauto.
+Qed.
+*)
+
+(* TODO: adapt this lemma -- needs  Ptrofs.one -> size bi
+Lemma code_tail_next_int:
+  forall fn ofs bi c,
+  size_blocks fn <= Ptrofs.max_unsigned ->
+  code_tail (Ptrofs.unsigned ofs) fn (bi :: c) ->
+  code_tail (Ptrofs.unsigned (Ptrofs.add ofs Ptrofs.one)) fn c.
+Proof.
+  intros. rewrite Ptrofs.add_unsigned, Ptrofs.unsigned_one.
+  rewrite Ptrofs.unsigned_repr. apply code_tail_next with i; auto.
+  generalize (code_tail_bounds_2 _ _ _ _ H0). omega.
+Qed.
+*)
 
 
 (** Predictor for return addresses in generated Asm code.
@@ -94,6 +149,59 @@ Definition return_address_offset (f: MB.function) (c: MB.code) (ofs: ptrofs) : P
   transl_blocks f c = OK tc ->
   code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) tc.
 
-Axiom return_address_exists:
+(* NB: this lemma should go into [Coqlib.v] *) 
+Lemma is_tail_app A (l1: list A): forall l2, is_tail l2 (l1 ++ l2).
+Proof.
+  induction l1; simpl; auto with coqlib.
+Qed.
+Hint Resolve is_tail_app: coqlib.
+
+Lemma transl_blocks_tail:
+  forall f c1 c2, is_tail c1 c2 ->
+  forall tc2, transl_blocks f c2 = OK tc2 ->
+  exists tc1, transl_blocks f c1 = OK tc1 /\ is_tail tc1 tc2.
+Proof.
+  induction 1; simpl; intros.
+  exists tc2; split; auto with coqlib.
+  monadInv H0. exploit IHis_tail; eauto. intros (tc1 & A & B).
+  exists tc1; split. auto.
+  eapply is_tail_trans; eauto with coqlib. 
+Qed.
+
+
+Section RETADDR_EXISTS.
+
+Hypothesis transf_function_inv:
+  forall f tf, transf_function f = OK tf ->
+  exists tc, transl_blocks f (Machblock.fn_code f) = OK tc /\ is_tail tc (fn_blocks tf).
+
+Hypothesis transf_function_len:
+  forall f tf, transf_function f = OK tf -> size_blocks (fn_blocks tf) <= Ptrofs.max_unsigned.
+
+Lemma return_address_exists:
   forall b f sg ros c, b.(MB.exit) = Some (MBcall sg ros) -> is_tail (b :: c) f.(MB.fn_code) ->
-  exists ra, return_address_offset f c ra.
\ No newline at end of file
+  exists ra, return_address_offset f c ra.
+Proof.
+  intros. destruct (transf_function f) as [tf|] eqn:TF.
++ exploit transf_function_inv; eauto. intros (tc1 & TR1 & TL1).
+  exploit transl_blocks_tail; eauto. intros (tc2 & TR2 & TL2).
+  unfold return_address_offset.
+  (* exploit code_tail_next_int; eauto.*)
+Admitted.
+
+(*
+Opaque transl_instr.
+  monadInv TR2.
+  assert (TL3: is_tail x (fn_code tf)).
+  { apply is_tail_trans with tc1; auto.
+    apply is_tail_trans with tc2; auto.
+    eapply transl_instr_tail; eauto. }
+  exploit is_tail_code_tail. eexact TL3. intros [ofs CT].
+  exists (Ptrofs.repr ofs). red; intros.
+  rewrite Ptrofs.unsigned_repr. congruence.
+  exploit code_tail_bounds_1; eauto.
+  apply transf_function_len in TF. omega.
++ exists Ptrofs.zero; red; intros. congruence.
+Qed.
+*)
+End RETADDR_EXISTS.
\ No newline at end of file
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index 94f3e531..980b9576 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -16,7 +16,7 @@ Require Import Coqlib Errors.
 Require Import Integers Floats AST Linking.
 Require Import Values Memory Events Globalenvs Smallstep.
 Require Import Op Locations Mach Conventions Asm Asmgen Machblockgen Asmblockgen.
-Require Import Machblockgenproof Asmblockgenproof0 Asmblockgenproof.
+Require Import Machblockgenproof Asmblockgenproof.
 
 Local Open Scope linking_scope.
 
@@ -43,13 +43,13 @@ Qed.
 (** Return Address Offset *)
 
 Definition return_address_offset (f: Mach.function) (c: Mach.code) (ofs: ptrofs) : Prop :=
-  Asmblockgenproof0.return_address_offset (Machblockgen.transf_function f) (Machblockgen.trans_code c) ofs.
+  Asmblockgenproof.return_address_offset (Machblockgen.transf_function f) (Machblockgen.trans_code c) ofs.
 
 
 Lemma Mach_Machblock_tail:
   forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) ->
-  exists b, MB.exit b = Some (Machblock.MBcall sg ros)
-    /\ is_tail (b :: trans_code c) (MB.fn_code (Machblockgen.transf_function f)).
+  exists b, Machblock.exit b = Some (Machblock.MBcall sg ros)
+    /\ is_tail (b :: trans_code c) (Machblock.fn_code (Machblockgen.transf_function f)).
 Admitted.
 
 Lemma return_address_exists:
@@ -59,8 +59,8 @@ Proof.
   intros.
   exploit Mach_Machblock_tail; eauto.
   destruct 1 as [b [H1 H2]].
-  eapply Asmblockgenproof0.return_address_exists; eauto.
-Qed.
+  eapply Asmblockgenproof.return_address_exists; eauto.
+Admitted.
 
 
 Section PRESERVATION.