Generals lemmas for asmblockgenproof

1 files changed, 28 insertions, 12 deletions

diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v
index d68cd7ac..96e7db4b 100644
--- a/aarch64/Asmblockgen.v
+++ b/aarch64/Asmblockgen.v
@@ -1159,11 +1159,11 @@ Definition it1_is_parent (before: bool) (i: Machblock.basic_inst) : bool :=
   | _ => false
   end.
 
-Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) (k: bcode):=
+Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) :=
   match il with
-  | nil => OK (k)
+  | nil => OK (nil)
   | i1 :: il' =>
-      do k1 <- transl_basic_code f il' (it1_is_parent it1p i1) k;
+      do k1 <- transl_basic_code f il' (it1_is_parent it1p i1);
       transl_instr_basic f i1 it1p k1
   end.
 
@@ -1196,12 +1196,29 @@ Program Definition gen_bblocks (hd: list label) (c: bcode) (ctl: list instructio
 
 (* XXX: the simulation proof may be complex with this pattern. We may fix this later *)
 Program Definition cons_bblocks (ll: list label) (bdy: list basic) (ex: option control): bblocks :=
-  match non_empty_bblockb bdy ex with
-  | true => {| header := ll; body:= bdy; exit := ex |} :: nil
-  | false => {| header := ll; body:= Pnop::nil; exit := None |} :: nil
+  match ex with
+  | None =>
+    match bdy with
+    | nil => {| header := ll; body:= Pnop::nil; exit := None |} :: nil
+    | _ => {| header := ll; body:= bdy; exit := None |} :: nil
+    end
+  | _ =>
+    match bdy with
+    | nil => {| header := ll; body:= nil; exit := ex |} :: nil
+    | _ => {| header := ll; body:= bdy; exit := ex |} :: nil
+    end
   end.
-Obligation 1.
-  rewrite <- Heq_anonymous. constructor.
+Next Obligation.
+  induction bdy. congruence.
+  simpl. auto.
+Qed.
+Next Obligation.
+  destruct ex. simpl. auto.
+  congruence.
+Qed.
+Next Obligation.
+  induction bdy. congruence.
+  simpl. auto.
 Qed.
 
 Definition transl_control (f: Machblock.function) (ctl: control_flow_inst) : res (bcode*control) :=
@@ -1227,10 +1244,9 @@ Definition transl_exit (f: Machblock.function) (ext: option control_flow_inst) :
   end.
 
 Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool) : res (list bblock) :=
-  let stub := false in
-  do (bdy, ex) <- transl_exit f fb.(Machblock.exit);
-  do bdy' <- transl_basic_code f fb.(Machblock.body) ep bdy;
-  OK (cons_bblocks fb.(Machblock.header) bdy' ex) 
+  do (bdy2, ex) <- transl_exit f fb.(Machblock.exit);
+  do bdy1 <- transl_basic_code f fb.(Machblock.body) ep;
+  OK (cons_bblocks fb.(Machblock.header) (bdy1 @@ bdy2) ex) 
   .
 
 Fixpoint transl_blocks (f: Machblock.function) (lmb: list Machblock.bblock) (ep: bool) :=