Removing the PseudoAsm IR

1 files changed, 29 insertions, 10 deletions

diff --git a/aarch64/Asmblockgenproof.v b/aarch64/Asmblockgenproof.v
index 41082772..bd96ff3b 100644
--- a/aarch64/Asmblockgenproof.v
+++ b/aarch64/Asmblockgenproof.v
@@ -5,8 +5,8 @@ CURRENTLY A STUB !
 Require Import Coqlib Errors.
 Require Import Integers Floats AST Linking.
 Require Import Values Memory Events Globalenvs Smallstep.
-Require Import Op Locations Machblock Conventions PseudoAsmblock Asmblock IterList.
-Require Import PseudoAsmblockproof Asmblockgen.
+Require Import Op Locations Machblock Conventions Asmblock IterList.
+Require Import Asmblockgen Asmblockgenproof0.
 
 Module MB := Machblock.
 Module AB := Asmblock.
@@ -20,13 +20,8 @@ Proof.
   intros. eapply match_transform_partial_program; eauto.
 Qed.
 
-Parameter next: MB.function -> Z -> Z.
-
 Section PRESERVATION.
 
-Lemma next_progress: forall (f:MB.function) (pos:Z), (pos < (next f pos))%Z.
-Admitted.
-
 Variable lk: aarch64_linker.
 Variable prog: Machblock.program.
 Variable tprog: Asmblock.program.
@@ -38,15 +33,39 @@ Let tge := Genv.globalenv tprog.
 Hypothesis symbol_high_low: forall (id: ident) (ofs: ptrofs),
   Val.addl (symbol_high lk id ofs) (symbol_low lk id ofs) = Genv.symbol_address tge id ofs.
 
-Lemma functions_bound_max_pos: forall fb f,
+(*Lemma functions_bound_max_pos: forall fb f,
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
   (max_pos next f) <= Ptrofs.max_unsigned.
-Admitted.
+Admitted.*)
+
+Lemma transf_function_no_overflow:
+  forall f tf,
+  transf_function f = OK tf -> size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned.
+Proof.
+  intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0.
+  omega.
+Qed.
 
+(** Existence of return addresses *)
+
+Lemma return_address_exists:
+  forall b f c, is_tail (b :: c) f.(MB.fn_code) ->
+  exists ra, return_address_offset f c ra.
+Proof.
+  intros. eapply Asmblockgenproof0.return_address_exists; eauto.
+
+- intros. monadInv H0.
+  destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0. monadInv EQ. simpl.
+  exists x; exists true; split; auto.
+  repeat constructor.
+- exact transf_function_no_overflow.
+Qed.
 
+Definition return_address_offset : Machblock.function -> Machblock.code -> ptrofs -> Prop := 
+  Asmblockgenproof0.return_address_offset.
 
 Lemma transf_program_correct:
-  forward_simulation (PseudoAsmblock.semantics next prog) (AB.semantics lk tprog).
+  forward_simulation (MB.semantics return_address_offset prog) (AB.semantics lk tprog).
 Admitted.
 
 End PRESERVATION.