Asm gen proof for aarch64 from Asmblock is complete.

1 files changed, 35 insertions, 116 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index eed185a0..f28bcb2e 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -1413,7 +1413,7 @@ Proof.
     - rewrite <- Nat2Z.inj_le; eapply is_tail_bound; eauto.
   }
   exploit internal_functions_unfold; eauto.
-  intros (tc & FINDtf & TRANStf & _). 
+  intros (tc & FINDtf & TRANStf & _).
   exploit find_basic_instructions_alt; eauto.
   intros (tbi & (bi & (NTHBI & TRANSBI & FIND_INSTR))).
   exploit is_tail_list_nth_z; eauto.
@@ -1595,9 +1595,9 @@ Lemma header_size_cons_nil: forall (l0: label) (l1: list label)
   l1 = nil.
 Proof.
   intros.
-  destruct l1 as [l2|l1]; try congruence. rewrite !list_length_z_cons in HSIZE.
-  assert (list_length_z l2 >= 0) by eapply list_length_z_pos.
-  assert (list_length_z l2 + 1 + 1 >= 2) by omega.
+  destruct l1; try congruence. rewrite !list_length_z_cons in HSIZE.
+  assert (list_length_z l1 >= 0) by eapply list_length_z_pos.
+  assert (list_length_z l1 + 1 + 1 >= 2) by omega.
   assert (2 <= 1) by omega. contradiction H1. omega.
 Qed.
 
@@ -1665,7 +1665,7 @@ Lemma next_inst_incr_pc_preserved bb rs1 m1 rs1' m1' rs2 m2 f tf: forall
   (BOUNDED: size bb <= Ptrofs.max_unsigned)
   (MATCHI: match_internal (size bb - 1) (State rs1 m1) (State rs2 m2))
   (NEXT: Next (incrPC (Ptrofs.repr (size bb)) rs1) m2 = Next rs1' m1'),
-  exists (rs2' : regset) (m2' : mem), 
+  exists (rs2' : regset) (m2' : mem),
   Next (Asm.nextinstr rs2) m2 = Next rs2' m2'
   /\ match_states (State rs1' m1') (State rs2' m2').
 Proof.
@@ -1930,11 +1930,14 @@ Proof.
   induction res; simpl; intros; unfold Pregmap.set; try rewrite AG; eauto.
 Qed.
 
-Lemma set_builtin_res_dont_move_pc_gen res: forall vres rs _rs v
+Lemma set_builtin_res_dont_move_pc_gen res: forall vres rs _rs v1 v2
+  (HV: v1 = v2)
   (AG : forall r : preg, r <> PC -> rs r = _rs r),
-  (set_res res vres rs) # PC <- v =
-  (set_res res vres _rs) # PC <- v.
+  (set_res res vres rs) # PC <- v1 =
+  (set_res res vres _rs) # PC <- v2.
 Proof.
+  intros. rewrite HV. generalize res vres rs _rs AG v2.
+  clear res vres rs _rs AG v1 v2 HV.
   induction res.
   - simpl; intros. apply pc_both_sides; intros.
     unfold Pregmap.set; try rewrite AG; eauto.
@@ -1953,13 +1956,16 @@ Proof.
   - intros; simpl in *. rewrite IHres2. rewrite IHres1. reflexivity.
 Qed.
 
-(*Unset Printing Notations.*)
-(*Lemma undef_map_preg_not_pc (l: list mreg): forall rs,*)
-  (*undef_regs (map preg_of l) rs PC = rs PC.*)
-(*Proof.*)
-  (*induction l.*)
-  (*- simpl; reflexivity.*)
-  (*- simpl.*)
+Lemma undef_reg_preserved (rl: list mreg): forall rs _rs r
+  (NPC: r <> PC)
+  (AG : forall r : preg, r <> PC -> rs r = _rs r),
+  undef_regs (map preg_of rl) rs r = undef_regs (map preg_of rl) _rs r.
+Proof.
+  induction rl.
+  - simpl; auto.
+  - simpl; intros. erewrite IHrl; eauto.
+    intros. unfold Pregmap.set. destruct (PregEq.eq r0 (preg_of a)); try rewrite AG; eauto.
+Qed.
 
 Lemma undef_regs_other:
   forall r rl rs,
@@ -2060,110 +2066,23 @@ Proof.
       - eapply eval_builtin_args_match; eauto.
       - inv MATCHI; eauto.
       - inv MATCHI.
-        (* TODO lemmas for set_res, undef_regs ... *)
         unfold Asm.nextinstr, incrPC.
-        (*induction res.*)
-        (*-- erewrite !set_builtin_map_not_pc.*)
-           
-           (*eapply set_builtin_res_dont_move_pc_gen.*)
-        
-
-           assert (HPC: Val.offset_ptr (rs PC) (Ptrofs.repr (size bb))
-                      = Val.offset_ptr (_rs PC) Ptrofs.one).
-           { rewrite <- AGPC. rewrite ATPC. unfold Val.offset_ptr.
-             rewrite Ptrofs.add_assoc. unfold Ptrofs.add.
-             assert (BBPOS: size bb >= 1) by eapply bblock_size_pos.
-             rewrite (Ptrofs.unsigned_repr (size bb - 1)); try omega.
-             rewrite Ptrofs.unsigned_one.
-             replace (size bb - 1 + 1) with (size bb) by omega.
-             reflexivity. }
-
-
-
-
-
-        destruct destroyed_by_builtin.
-        -- unfold map. simpl.
-           induction res.
-           ++ simpl; intros. update_x_access_r; try congruence.
-              rewrite HPC.
-              apply (pc_both_sides (rs # x <- vres) (_rs # x <- vres)
-                    (Val.offset_ptr (_rs PC) Ptrofs.one)); intros.
-              unfold Pregmap.set; try rewrite AG; eauto.
-           ++ simpl; intros. rewrite HPC.
-              apply pc_both_sides; eauto.
-           ++ simpl; intros.
-              erewrite !set_builtin_map_not_pc. rewrite HPC.
-              eapply set_builtin_res_dont_move_pc_gen; intros.
-              eapply set_buitin_res_sym; eauto.
-        -- simpl.
-           assert (HPC': (undef_regs (map preg_of l)
-                         rs # (preg_of m) <- Vundef) PC = rs PC).
-           { erewrite undef_regs_other_2.
-             2: eapply preg_notin_charact; intros; discriminate.
-             erewrite Pregmap.gso; eauto; try discriminate. }
-
-
-             ++ simpl. update_x_access_r; try discriminate.
-             ++ simpl. 
-                assert (rs # (preg_of m) <- Vundef = _rs # (preg_of m) <- Vundef).
-                { destruct (PregEq.eq PC (preg_of m)). rewrite <- e.
-                  { unfold Pregmap.set; apply functional_extensionality; intros.
-                  destruct (PregEq.eq x PC); try rewrite AG; eauto. }
-                  { unfold Pregmap.set; apply functional_extensionality; intros.
-                  destruct (PregEq.eq x PC); try rewrite AG; eauto }
-
-                rewrite (Pregmap.gso (i := PC) (j := (preg_of a)) Vundef (rs # (preg_of m) <- Vundef)).
-                rewrite IHl. update_x_access_r; try discriminate.
-
-   (Ptrofs.repr (size bb))
-           induction res.
-           ++ erewrite !set_builtin_map_not_pc.
-              
-              eapply set_builtin_res_dont_move_pc_gen.
-erewrite !set_builtin_map_not_pc.
-              update_x_access_r; try congruence.
-              
-
-           
-        all:admit. 
-Admitted.
-
-Lemma set_builtin_res_pc_overwrite res: forall (bb: bblock) vres rs _rs
-  (AG : forall r : preg, r <> PC -> rs r = _rs r)
-  (HPC : Val.offset_ptr (rs PC) (Ptrofs.repr (size bb)) =
-        Val.offset_ptr (_rs PC) Ptrofs.one),
-  (set_res (map_builtin_res DR res) vres rs) # PC <-
-  (Val.offset_ptr (set_res (map_builtin_res DR res) vres rs PC)
-     (Ptrofs.repr (size bb))) =
-  (set_res (map_builtin_res DR res) vres _rs) # PC <-
-  (Val.offset_ptr (set_res (map_builtin_res DR res) vres _rs PC) Ptrofs.one).
-Proof.
-  induction res.
-  - simpl; intros. update_x_access_r; try congruence. rewrite HPC.
-    apply (pc_both_sides (rs # x <- vres) (_rs # x <- vres) (Val.offset_ptr (_rs PC) Ptrofs.one)); intros. unfold Pregmap.set; try rewrite AG; eauto.
-  - simpl; intros. rewrite HPC.
-    apply pc_both_sides; eauto.
-  - simpl; intros.
-    (*rewrite <- (IHres2 bb (Val.loword vres) rs (set_res (map_builtin_res DR res1) (Val.hiword vres) _rs)).*)
-    (*+ rewrite (IHres2 bb (Val.loword vres) (set_res (map_builtin_res DR res1) (Val.hiword vres) rs) _rs).*)
-      (** rewrite (IHres2 bb (Val.loword vres) rs _rs); eauto.*)
-      (** intros. induction res1. 3: { simpl.*)
-
-    (*assert ((Val.offset_ptr*)
-   (*(set_res (map_builtin_res DR res2) (Val.loword vres)*)
-      (*(set_res (map_builtin_res DR res1) (Val.hiword vres) rs) PC)*)
-   (*(Ptrofs.repr (size bb))) =*)
-  (*(Val.offset_ptr*)
-   (*(set_res (map_builtin_res DR res2) (Val.loword vres)*)
-      (*(set_res (map_builtin_res DR res1) (Val.hiword vres) _rs) PC)*)
-   (*Ptrofs.one)). {*)
-     erewrite !set_builtin_map_not_pc. rewrite HPC.
-     eapply set_builtin_res_dont_move_pc_gen; intros.
-     eapply set_buitin_res_sym; eauto.
+        assert (HPC: Val.offset_ptr (rs PC) (Ptrofs.repr (size bb))
+                   = Val.offset_ptr (_rs PC) Ptrofs.one).
+        { rewrite <- AGPC. rewrite ATPC. unfold Val.offset_ptr.
+          rewrite Ptrofs.add_assoc. unfold Ptrofs.add.
+          assert (BBPOS: size bb >= 1) by eapply bblock_size_pos.
+          rewrite (Ptrofs.unsigned_repr (size bb - 1)); try omega.
+          rewrite Ptrofs.unsigned_one.
+          replace (size bb - 1 + 1) with (size bb) by omega.
+          reflexivity. }
+        apply set_builtin_res_dont_move_pc_gen.
+        -- erewrite !set_builtin_map_not_pc.
+           erewrite !undef_regs_other_2.
+           rewrite HPC; auto. all: rewrite preg_notin_charact; intros; try discriminate.
+        -- intros. eapply undef_reg_preserved; eauto.
 Qed.
 
-
 Lemma exec_exit_simulation_star b ofs f bb s2 t rs m rs' m': forall
   (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
   (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb)