Simplifications using ltacs and XZR special case

1 files changed, 150 insertions, 33 deletions

diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v
index 571e511f..ae4e12b2 100644
--- a/aarch64/Asmblockdeps.v
+++ b/aarch64/Asmblockdeps.v
@@ -75,7 +75,15 @@ Inductive control_op :=
 .
 
 Inductive arith_op :=
+  | OArithP (n: arith_p)
+  | OArithPP (n: arith_pp)
   | OArithPPP (n: arith_ppp)
+  | OArithRR0R (n: arith_rr0r)
+  | OArithRR0R_XZR (n: arith_rr0r) (vz: val)
+  | OArithRR0 (n: arith_rr0)
+  | OArithRR0_XZR (n: arith_rr0) (vz: val)
+  | OArithARRRR0 (n: arith_arrrr0)
+  | OArithARRRR0_XZR (n: arith_arrrr0) (vz: val)
 .
 
 Inductive op_wrap :=
@@ -88,7 +96,15 @@ Definition op:=op_wrap.
 
 Definition arith_op_eval (op: arith_op) (l: list value) :=
   match op, l with
+  | OArithP n, [] => Some (Val (arith_eval_p Ge.(_lk) n))
+  | OArithPP n, [Val v] => Some (Val (arith_eval_pp Ge.(_lk) n v))
   | OArithPPP n, [Val v1; Val v2] => Some (Val (arith_eval_ppp n v1 v2))
+  | OArithRR0R n, [Val v1; Val v2] => Some (Val (arith_eval_rr0r n v1 v2))
+  | OArithRR0R_XZR n vz, [Val v] => Some (Val (arith_eval_rr0r n vz v))
+  | OArithRR0 n, [Val v] => Some (Val (arith_eval_rr0 n v))
+  | OArithRR0_XZR n vz, [] => Some (Val (arith_eval_rr0 n vz))
+  | OArithARRRR0 n, [Val v1; Val v2; Val v3] => Some (Val (arith_eval_arrrr0 n v1 v2 v3))
+  | OArithARRRR0_XZR n vz, [Val v1; Val v2] => Some (Val (arith_eval_arrrr0 n v1 v2 vz))
   | _, _ => None
   end.
 
@@ -119,8 +135,24 @@ Definition op_eval (op: op) (l:list value) :=
 
 Definition arith_op_eq (o1 o2: arith_op): ?? bool :=
   match o1 with
+  | OArithP n1 =>
+      match o2 with OArithP n2 => phys_eq n1 n2 | _ => RET false end
+  | OArithPP n1 =>
+      match o2 with OArithPP n2 => phys_eq n1 n2 | _ => RET false end
   | OArithPPP n1 =>
-      match o2 with OArithPPP n2 => struct_eq n1 n2 (*| _ => RET false*) end
+      match o2 with OArithPPP n2 => phys_eq n1 n2 | _ => RET false end
+  | OArithRR0R n1 =>
+      match o2 with OArithRR0R n2 => phys_eq n1 n2 | _ => RET false end
+  | OArithRR0R_XZR n1 vz1 =>
+      match o2 with OArithRR0R_XZR n2 vz2 => iandb (phys_eq n1 n2) (phys_eq vz1 vz2) | _ => RET false end
+  | OArithRR0 n1 =>
+      match o2 with OArithRR0 n2 => phys_eq n1 n2 | _ => RET false end
+  | OArithRR0_XZR n1 vz1 =>
+      match o2 with OArithRR0_XZR n2 vz2 => iandb (phys_eq n1 n2) (phys_eq vz1 vz2) | _ => RET false end
+  | OArithARRRR0 n1 =>
+      match o2 with OArithARRRR0 n2 => phys_eq n1 n2 | _ => RET false end
+  | OArithARRRR0_XZR n1 vz1 =>
+      match o2 with OArithARRRR0_XZR n2 vz2 => iandb (phys_eq n1 n2) (phys_eq vz1 vz2) | _ => RET false end
   (*| OArithRR n1 => *)
      (*match o2 with OArithRR n2 => phys_eq n1 n2 | _ => RET false end*)
   (*| OArithRI32 n1 i1 =>*)
@@ -274,6 +306,13 @@ Definition ppos (r: preg) : R.t :=
   end
 .
 
+(*Definition ppos_ireg0 (r: ireg0) : R.t :=*)
+  (*match r with*)
+  (*| RR0 p => ppos p*)
+  (*| XZR => 71*)
+  (*end*)
+(*.*)
+
 Notation "# r" := (ppos r) (at level 100, right associativity). 
 
 Lemma not_eq_add:
@@ -369,7 +408,36 @@ Definition trans_exit (ex: option control) : L.inst :=
 
 Definition trans_arith (ai: ar_instruction) : inst :=
   match ai with
+  | PArithP n rd => [(#rd, Op(Arith (OArithP n)) Enil)]
+  | PArithPP n rd r1 => [(#rd, Op(Arith (OArithPP n)) (PReg(#r1) @ Enil))]
   | PArithPPP n rd r1 r2 => [(#rd, Op(Arith (OArithPPP n)) (PReg(#r1) @ PReg(#r2) @ Enil))]
+  | PArithRR0R n rd r1 r2 => let lr := match r1 with
+                                       | RR0 r1' => Op(Arith (OArithRR0R n)) (PReg(#r1') @ PReg(#r2) @ Enil)
+                                       | XZR => let vz := match arith_rr0r_isize n with
+                                                          | W => Vint Int.zero
+                                                          | X => Vlong Int64.zero
+                                                          end in
+                                                          Op(Arith (OArithRR0R_XZR n vz)) (PReg(#r2) @ Enil)
+                                       end in
+                                       [(#rd,  lr)]
+  | PArithRR0 n rd r1 => let lr := match r1 with
+                                   | RR0 r1' => Op(Arith (OArithRR0 n)) (PReg(#r1') @ Enil)
+                                   | XZR => let vz := match arith_rr0_isize n with
+                                                      | W => Vint Int.zero
+                                                      | X => Vlong Int64.zero
+                                                      end in
+                                                      Op(Arith (OArithRR0_XZR n vz)) (Enil)
+                                   end in
+                                   [(#rd, lr)]
+  | PArithARRRR0 n rd r1 r2 r3 => let lr := match r3 with
+                                            | RR0 r3' => Op(Arith (OArithARRRR0 n)) (PReg(#r1) @ PReg (#r2) @ PReg(#r3') @ Enil)
+                                            | XZR => let vz := match arith_arrrr0_isize n with
+                                                               | W => Vint Int.zero
+                                                               | X => Vlong Int64.zero
+                                                               end in
+                                                               Op(Arith (OArithARRRR0_XZR n vz)) (PReg(#r1) @ PReg(#r2) @ Enil)
+                                            end in
+                                            [(#rd, lr)]
   | _ => []
   (*| PArithR n d => [(#d, Op (Arith (OArithR n)) Enil)]*)
   (*| PArithRR n d s => [(#d, Op (Arith (OArithRR n)) (PReg(#s) @ Enil))]*)
@@ -587,25 +655,72 @@ Qed.
 
 (*Import PChk.*)
 
-Ltac Simplif :=
-  (*((rewrite nextblock_inv by eauto with asmgen)*)
-  (*|| (rewrite nextblock_inv1 by eauto with asmgen)*)
-  ((rewrite Pregmap.gss)
-  (*|| (rewrite nextblock_pc)*)
-  || (rewrite Pregmap.gso by eauto with asmgen)
-  || (rewrite assign_diff by (auto; try discriminate; try (apply ppos_discr; try discriminate; congruence); try (apply ppos_pmem_discr); 
-                                    try (apply not_eq_sym; apply ppos_discr; try discriminate; congruence); try (apply not_eq_sym; apply ppos_pmem_discr); auto))
-  || (rewrite assign_eq)
-  ); auto with asmgen.
+(*Ltac Simplif :=*)
+  (*[>((rewrite nextblock_inv by eauto with asmgen)<]*)
+  (*[>|| (rewrite nextblock_inv1 by eauto with asmgen)<]*)
+  (*((rewrite Pregmap.gss)*)
+  (*[>|| (rewrite nextblock_pc)<]*)
+  (*|| (rewrite Pregmap.gso by eauto with asmgen)*)
+  (*|| (rewrite assign_diff by (auto; try discriminate; try (apply ppos_discr; try discriminate; congruence); try (apply ppos_pmem_discr); *)
+                                    (*try (apply not_eq_sym; apply ppos_discr; try discriminate; congruence); try (apply not_eq_sym; apply ppos_pmem_discr); auto))*)
+  (*|| (rewrite assign_eq)*)
+  (*); auto with asmgen.*)
+
+(*Ltac Simpl := repeat Simplif.*)
+
+Ltac sr_val_rwrt :=
+  repeat match goal with
+  | [H: forall r: preg, ?sr (# r) = Val (?rsr r) |- _ ]
+      => rewrite H
+  end.
+
+Ltac sr_memstate_rwrt :=
+  repeat match goal with
+  | [H: ?sr pmem = Memstate ?mr |- _ ]
+      => rewrite <- H
+  end.
+
+Ltac replace_ppos :=
+  try erewrite !ireg_pos_ppos;
+  try erewrite !freg_pos_ppos.
+
+Ltac DI0N0 ir0 := destruct ir0 as [rr0DIRN0|]; subst; simpl.
+
+Ltac DIRN1 ir := destruct ir as [irrDIRN1|]; subst; try destruct irrDIRN1; simpl.
+
+Ltac DDRN2 dr := destruct dr as [irDDRN2|frDDRN2]; subst; try destruct irDDRN2; simpl.
+
+Ltac DPRF pr :=
+  destruct pr as [drDPRF|crDPRF|]; 
+      [destruct drDPRF as [irDPRF|frDPRF]; [destruct irDPRF as [irrDPRF|]; [destruct irrDPRF|]
+      | destruct frDPRF]
+      | destruct crDPRF|].
+
+Ltac DPRI pr :=
+  destruct pr as [drDPRI|crDPRI|]; 
+      [destruct drDPRI as [irDPRI|frDPRI]; [destruct irDPRI as [irrDPRI|]; [destruct irrDPRI|]|]
+      | idtac
+      | idtac ].
+
+Ltac TARITH :=
+  replace_ppos;
+  try replace (7) with (ppos XSP) by eauto;
+  try sr_val_rwrt;
+  try (eexists; split; [| split]); eauto;
+  try (sr_memstate_rwrt; rewrite assign_diff;
+      try reflexivity; try apply ireg_not_pmem;
+      try apply freg_not_pmem).
 
-Ltac Simpl := repeat Simplif.
+Ltac SRVUPDATE :=
+  try eapply sr_ireg_update_both; eauto;
+  try eapply sr_freg_update_both; eauto;
+  try eapply sr_xsp_update_both; eauto.
 
 (*Arguments Pos.add: simpl never.*)
 (*Arguments ppos: simpl never.*)
 
 Variable Ge: genv.
 
-(*Lemma trans_arith_par_correct o rs m m' old:*)
 Lemma trans_arith_correct rsr mr sr rsw' old i:
   (*Ge = Genv ge fn ->*)
   (*match_states (State rs m) m' ->*)
@@ -619,26 +734,28 @@ Lemma trans_arith_correct rsr mr sr rsw' old i:
   /\ match_states (State rsw' mr) sw.
 Proof.
   induction i.
-  3: { intros MS EARITH. subst. inv MS.
-       unfold exec_arith_instr.
-       (*eexists; split; [| split]. *)
-       - simpl. destruct r1 eqn:EQR1; subst; try destruct i0; simpl;
-         destruct r2 eqn:EQR2; subst; try destruct i0; simpl;
-         (*destruct (sr 8).*) destruct rd eqn:EQRD; subst; try destruct i0; simpl;
-         try erewrite !ireg_pos_ppos;
-         try erewrite !freg_pos_ppos;
-         try replace (7) with (ppos XSP) by eauto;
-         try rewrite !H0;
-         try (eexists; split; [| split]); eauto;
-         try (rewrite <- H; rewrite assign_diff;
-              try reflexivity; try apply ireg_not_pmem;
-              try apply freg_not_pmem).
-         all: intros rr; destruct rr as [dr|cr|]; try destruct dr as [ir|fr]; try destruct ir as [irr|];
-         try destruct irr; try destruct fr;
-         try eapply sr_ireg_update_both; eauto;
-         try eapply sr_freg_update_both; eauto;
-         try eapply sr_xsp_update_both; eauto.
-         }
+  all: intros MS EARITH; subst; inv MS; unfold exec_arith_instr.
+  - (* PArithP *)
+    DDRN2 rd; TARITH; intros rr; DPRF rr; SRVUPDATE.
+  - (* PArithPP *)
+    DIRN1 rs; DIRN1 rd; TARITH;
+    intros rr; DPRI rr; SRVUPDATE.
+  - (* PArithPPP *)
+    DIRN1 r1; DIRN1 r2; DIRN1 rd; TARITH;
+    intros rr; DPRI rr; SRVUPDATE.
+  - (* PArithRR0R *) 
+    simpl. destruct r1.
+    + (* OArithRR0R *) simpl; TARITH; intros rr; DPRI rr; SRVUPDATE.
+    + (* OArithRR0R_XZR *) simpl; destruct (arith_rr0r_isize _); TARITH; intros rr; DPRI rr; SRVUPDATE.
+  - (* PArithRR0 *)
+    simpl. destruct r1.
+    + (* OArithRR0 *) simpl; TARITH; intros rr; DPRI rr; SRVUPDATE.
+    + (* OArithRR0_XZR *) simpl; destruct (arith_rr0_isize _); TARITH; intros rr; DPRI rr; SRVUPDATE.
+  - (* PArithARRRR0 *)
+    simpl. destruct r3.
+    + (* OArithARRRR0 *) simpl; TARITH; intros rr; DPRI rr; SRVUPDATE.
+    + (* OArithARRRR0_XZR *) simpl; destruct (arith_arrrr0_isize _); TARITH; intros rr; DPRI rr; SRVUPDATE.
+  - (* PArithComparisonPP *)
   all:admit.
 
   (*