a more general way to manage special registers before introducing SP

1 files changed, 73 insertions, 69 deletions

diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index 6e5cc531..1e17c4e2 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -494,124 +494,128 @@ Proof.
   split. rewrite V; destruct normal, b; reflexivity.
      intros; Simpl.
 
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
   unfold zero32, Op.zero32 in *;
-  eexists; eexists; eauto; split; constructor; auto;
+  destruct (rs x) eqn:EQRS; simpl in *; try congruence;
+  inv EQ2; eexists; eexists; eauto; split; constructor; auto;
   simpl in *.
-  + destruct (rs x); simpl in *; try congruence.
+  + rewrite EQRS;
     assert (HB: (Int.eq Int.zero i) = b) by congruence.
     rewrite HB; destruct b; simpl; auto.
-  + destruct (rs x); simpl in *; try congruence.
+  + rewrite EQRS;
     assert (HB: (Int.eq i Int.zero) = b) by congruence.
-    rewrite HB; destruct b; simpl; auto.
-  + destruct (rs x); simpl in *; try congruence.
+    rewrite <- HB; destruct b; simpl; auto.
+  + rewrite EQRS;
     destruct (rs x0); try congruence.
     assert (HB: (Int.eq i i0) = b) by congruence.
-    rewrite HB; destruct b; simpl; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
+    rewrite <- HB; destruct b; simpl; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
   unfold zero32, Op.zero32 in *;
-  eexists; eexists; eauto; split; constructor; auto;
+  destruct (rs x) eqn:EQRS; simpl in *; try congruence;
+  inv EQ2; eexists; eexists; eauto; split; constructor; auto;
   simpl in *.
-  + destruct (rs x); simpl in *; try congruence.
+  + rewrite EQRS;
     assert (HB: negb (Int.eq Int.zero i) = b) by congruence.
     rewrite HB; destruct b; simpl; auto.
-  + destruct (rs x); simpl in *; try congruence.
+  + rewrite EQRS;
     assert (HB: negb (Int.eq i Int.zero) = b) by congruence.
-    rewrite HB; destruct b; simpl; auto.
-  + destruct (rs x); simpl in *; try congruence.
+    rewrite <- HB; destruct b; simpl; auto.
+  + rewrite EQRS;
     destruct (rs x0); try congruence.
     assert (HB: negb (Int.eq i i0) = b) by congruence.
-    rewrite HB; destruct b; simpl; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero32, Op.zero32 in *;
+    rewrite <- HB; destruct b; simpl; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *; inv EQ2;
   eexists; eexists; eauto; split; constructor;
   simpl in *; try rewrite EVAL'; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero32, Op.zero32 in *;
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *; inv EQ2;
   eexists; eexists; eauto; split; constructor;
   simpl in *; try rewrite EVAL'; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero32, Op.zero32 in *;
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *; inv EQ2;
   eexists; eexists; eauto; split; constructor;
   simpl in *; try rewrite EVAL'; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero32, Op.zero32 in *;
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *; inv EQ2;
   eexists; eexists; eauto; split; constructor;
   simpl in *; try rewrite EVAL'; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero32, Op.zero32 in *;
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *; inv EQ2;
   eexists; eexists; eauto; split; constructor;
   simpl in *; try rewrite EVAL'; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero32, Op.zero32 in *;
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *; inv EQ2;
   eexists; eexists; eauto; split; constructor;
   simpl in *; try rewrite EVAL'; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero64, Op.zero64 in *;
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *; inv EQ2;
+  destruct (rs x) eqn:EQRS; simpl in *; try congruence;
   eexists; eexists; eauto; split; constructor;
   simpl in *; auto.
-  + destruct (rs x); simpl in *; try congruence.
+  + rewrite EQRS;
     assert (HB: (Int64.eq Int64.zero i) = b) by congruence.
     rewrite HB; destruct b; simpl; auto.
-  + destruct (rs x); simpl in *; try congruence.
+  + rewrite EQRS;
     assert (HB: (Int64.eq i Int64.zero) = b) by congruence.
-    rewrite HB; destruct b; simpl; auto.
-  + destruct (rs x); simpl in *; try congruence.
+    rewrite <- HB; destruct b; simpl; auto.
+  + rewrite EQRS;
     destruct (rs x0); try congruence.
     assert (HB: (Int64.eq i i0) = b) by congruence.
-    rewrite HB; destruct b; simpl; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero64, Op.zero64 in *;
+    rewrite <- HB; destruct b; simpl; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32 in *; inv EQ2;
+  destruct (rs x) eqn:EQRS; simpl in *; try congruence;
   eexists; eexists; eauto; split; constructor;
   simpl in *; auto.
-  + destruct (rs x); simpl in *; try congruence.
+  + rewrite EQRS;
     assert (HB: negb (Int64.eq Int64.zero i) = b) by congruence.
     rewrite HB; destruct b; simpl; auto.
-  + destruct (rs x); simpl in *; try congruence.
+  + rewrite EQRS;
     assert (HB: negb (Int64.eq i Int64.zero) = b) by congruence.
-    rewrite HB; destruct b; simpl; auto.
-  + destruct (rs x); simpl in *; try congruence.
+    rewrite <- HB; destruct b; simpl; auto.
+  + rewrite EQRS;
     destruct (rs x0); try congruence.
     assert (HB: negb (Int64.eq i i0) = b) by congruence.
-    rewrite HB; destruct b; simpl; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero64, Op.zero64 in *;
+    rewrite <- HB; destruct b; simpl; auto.
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
   eexists; eexists; eauto; split; constructor;
   simpl in *; try rewrite EVAL'; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero64, Op.zero64 in *;
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
   eexists; eexists; eauto; split; constructor;
   simpl in *; try rewrite EVAL'; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero64, Op.zero64 in *;
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
   eexists; eexists; eauto; split; constructor;
   simpl in *; try rewrite EVAL'; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero64, Op.zero64 in *;
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
   eexists; eexists; eauto; split; constructor;
   simpl in *; try rewrite EVAL'; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero64, Op.zero64 in *;
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
   eexists; eexists; eauto; split; constructor;
   simpl in *; try rewrite EVAL'; auto.
-- destruct optR0 as [[]|];
-  unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *;
-  unfold zero64, Op.zero64 in *;
+- destruct optR as [[]|];
+  unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
+  unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
   eexists; eexists; eauto; split; constructor;
   simpl in *; try rewrite EVAL'; auto.
 Qed.
@@ -1273,7 +1277,7 @@ Opaque Int.eq.
     try rewrite Int64.or_commut;
     try rewrite Int.or_commut; auto.
   1-12:
-    destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0;
+    destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; inv EQ3;
     econstructor; split; try apply exec_straight_one; simpl; eauto;
     split; intros; Simpl;
     destruct (rs x0); auto;