Adding more expansions, improving miniCSE, and tuning prepass

1 files changed, 8 insertions, 4 deletions

diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index 0be56e47..639c9a64 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -1258,11 +1258,15 @@ Opaque Int.eq.
   { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
      exists rs'; split. eexact A. eauto with asmgen. }
   (* Expanded instructions from RTL *)
-  7,14:
+  7,8,9,10,17,18,19,20:
     econstructor; split; try apply exec_straight_one; simpl; eauto;
-    split; intros; Simpl; simpl;
-    try rewrite Int.add_commut; try rewrite Int64.add_commut;
-    auto.
+    split; intros; Simpl; try destruct (rs x0);
+    try rewrite Int64.add_commut;
+    try rewrite Int.add_commut; auto;
+    try rewrite Int64.and_commut;
+    try rewrite Int.and_commut; auto;
+    try rewrite Int64.or_commut;
+    try rewrite Int.or_commut; auto.
   1-12:
     destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0;
     econstructor; split; try apply exec_straight_one; simpl; eauto;