[Draft] Improvements on buitin cfi proof and new lemmas for set_res.

1 files changed, 143 insertions, 1 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 1d13fa7e..0ea37a38 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -1913,6 +1913,45 @@ Proof.
     + eauto.
 Qed.
 
+Lemma pc_both_sides: forall (rs _rs: regset) v
+  (AG : forall r : preg, r <> PC -> rs r = _rs r),
+  rs # PC <- v = _rs # PC <- v.
+Proof.
+  intros; unfold Pregmap.set; apply functional_extensionality; intros y.
+  destruct (PregEq.eq y PC); try rewrite AG; eauto.
+Qed.
+
+Lemma set_buitin_res_sym res: forall vres rs _rs r
+  (NPC: r <> PC)
+  (AG : forall r : preg, r <> PC -> rs r = _rs r),
+  set_res res vres rs r = set_res res vres _rs r.
+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
+  (AG : forall r : preg, r <> PC -> rs r = _rs r),
+  (set_res res vres rs) # PC <- v =
+  (set_res res vres _rs) # PC <- v.
+Proof.
+  induction res.
+  - simpl; intros. apply pc_both_sides; intros.
+    unfold Pregmap.set; try rewrite AG; eauto.
+  - simpl; intros; apply pc_both_sides; eauto.
+  - simpl; intros.
+    erewrite IHres2; eauto; intros.
+    eapply set_buitin_res_sym; eauto.
+Qed.
+
+Lemma set_builtin_map_not_pc (res: builtin_res dreg): forall vres rs,
+  set_res (map_builtin_res DR res) vres rs PC = rs PC.
+Proof.
+  induction res.
+  - intros; simpl. unfold Pregmap.set. destruct (PregEq.eq PC x); try congruence.
+  - intros; simpl; congruence.
+  - intros; simpl in *. rewrite IHres2. rewrite IHres1. reflexivity.
+Qed.
+
 Lemma exec_exit_simulation_plus 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)
@@ -1972,9 +2011,112 @@ Proof.
       - eapply find_instr_ofs_somei; eauto.
       - eapply eval_builtin_args_match; eauto.
       - inv MATCHI; eauto.
-      - rewrite H11. (* TODO lemmas for set_res, undef_regs ... *) admit.
+      - 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': Val.offset_ptr (set_res (map_builtin_res DR res)*)
+                          (*vres (undef_regs (map preg_of l)*)
+                          (*rs # (preg_of m) <- Vundef) PC) (Ptrofs.repr (size bb))*)
+                      (*= Val.offset_ptr (set_res (map_builtin_res DR res)*)
+                          (*vres (undef_regs (map preg_of l)*)
+                          (*_rs # (preg_of m) <- Vundef) PC) Ptrofs.one).*)
+           (*{ rewrite !set_builtin_map_not_pc.*)
+             (*induction l.*)
+             (*++ 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.
+
+
+  
 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)