Some optimizations again

1 files changed, 30 insertions, 27 deletions

diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v
index 71b7c317..8ec862da 100644
--- a/aarch64/Asmblockdeps.v
+++ b/aarch64/Asmblockdeps.v
@@ -1485,27 +1485,26 @@ Ltac replace_regs_cond_force :=
   try replace (2) with (#CN) in * by auto.
   
 Ltac validate_crbit_flags rr v1 v2 :=
-  destruct (R.eq_dec 5 (#rr)) as [eCV|eCV]; subst;
-  [ destruct v1; destruct v2; simpl;
-    replace_regs_cond_force; apply ppos_equal in eCV; subst;
-    rewrite Pregmap.gss; auto |
-  destruct (R.eq_dec 4 (#rr)) as [eCC|eCC]; subst;
-  [ destruct v1; destruct v2; simpl;
-      replace_regs_cond_force; apply ppos_equal in eCC; subst;
-      rewrite Pregmap.gso, Pregmap.gss; auto; try discriminate |
-  destruct (R.eq_dec 3 (#rr)) as [eCZ|eCZ]; subst;
-  [ destruct v1; destruct v2; simpl;
-      replace_regs_cond_force; apply ppos_equal in eCZ; subst;
-      rewrite 2Pregmap.gso, Pregmap.gss; auto; try discriminate |
-  destruct (R.eq_dec 2 (#rr)) as [eCN|eCN]; subst;
-  [ destruct v1; destruct v2; simpl;
-      replace_regs_cond_force; apply ppos_equal in eCN; subst;
-      rewrite 3Pregmap.gso, Pregmap.gss; auto; try discriminate |
-  destruct v1; destruct v2; simpl;
+  destruct (R.eq_dec 5 (#rr)) as [e0|n0];
+  destruct (R.eq_dec 4 (#rr)) as [e1|n1];
+  destruct (R.eq_dec 3 (#rr)) as [e2|n2];
+  destruct (R.eq_dec 2 (#rr)) as [e3|n3];
   replace_regs_cond_force;
-  apply ppos_discr in eCV; apply ppos_discr in eCC;
-  apply ppos_discr in eCZ; apply ppos_discr in eCN;
-  rewrite 4Pregmap.gso; auto; try discriminate ]]]].
+  try apply ppos_equal in e0;
+  try apply ppos_equal in e1;
+  try apply ppos_equal in e2;
+  try apply ppos_equal in e3;
+  try apply ppos_discr in n0;
+  try apply ppos_discr in n1;
+  try apply ppos_discr in n2;
+  try apply ppos_discr in n3;
+  subst.
+
+Ltac Simpl_flags :=
+  try (rewrite Pregmap.gss; reflexivity);
+  try (rewrite Pregmap.gso, Pregmap.gss; [reflexivity|]; try auto);
+  try (rewrite Pregmap.gso; try auto); 
+  try (rewrite !Pregmap.gso; try auto).
 
 Lemma compare_single_res: forall sr mr rsr rr v1 v2
   (HMEM: sr pmem = Memstate mr)
@@ -1519,6 +1518,7 @@ Val
 Proof.
   intros. unfold v_compare_single, compare_single, assign.
   validate_crbit_flags rr v1 v2.
+  all: destruct v1; destruct v2; Simpl_flags.
 Qed.
 
 Lemma compare_float_res: forall sr mr rsr rr v1 v2
@@ -1533,6 +1533,7 @@ Val
 Proof.
   intros. unfold v_compare_float, compare_float, assign.
   validate_crbit_flags rr v1 v2.
+  all: destruct v1; destruct v2; Simpl_flags.
 Qed.
 
 Lemma compare_long_res: forall sr mr rsr rr v1 v2
@@ -1547,6 +1548,7 @@ Val
 Proof.
   intros. unfold v_compare_long, compare_long, assign.
   validate_crbit_flags rr v1 v2.
+  all: Simpl_flags.
 Qed.
 
 Lemma compare_int_res: forall sr mr rsr rr v1 v2
@@ -1561,6 +1563,7 @@ Val
 Proof.
   intros. unfold v_compare_int, compare_int, assign.
   validate_crbit_flags rr v1 v2.
+  all: Simpl_flags.
 Qed.
 
 Section SECT_SEQ.
@@ -1612,13 +1615,13 @@ Proof.
     try (eapply compare_long_res; eauto);
     try (eapply compare_float_res; eauto).
   - (* PArithComparisonR0R *)
-    simpl. destruct r1; (
-      simpl; destruct i;
-      repeat Simpl_rep sr; Simpl_exists sr;
-      unfold arith_eval_comparison_r0r, arith_comparison_r0r_isize; destruct arith_prepare_comparison_r0r; destruct is;
-      simpl; intros rr; try destruct sz;
-      try (eapply compare_long_res; eauto);
-      try (eapply compare_int_res; eauto)).
+    simpl; destruct r1; simpl; destruct i;
+    repeat (replace_regs_cond_force; try fold (ppos r); try fold(ppos r2);
+    try rewrite !assign_diff; discriminate_ppos; try rewrite !H0);
+    Simpl sr; unfold arith_eval_comparison_r0r, arith_comparison_r0r_isize;
+    destruct arith_prepare_comparison_r0r; destruct is;
+    try (eapply compare_long_res; eauto);
+    try (eapply compare_int_res; eauto).
   - (* PArithComparisonP *)
     simpl; destruct i;
     unfold arith_eval_comparison_p, arith_prepare_comparison_p; simpl;