some bugfix

2 files changed, 20 insertions, 15 deletions

diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index 103285b4..07999b05 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -370,7 +370,7 @@ let rec write_tree exp current code' new_order =
   | _ -> failwith "ExpansionOracle.write_tree: inconsistent instruction."
 
 let expanse (sb : superblock) code pm =
-  (*debug_flag := true;*)
+  debug_flag := true;
   let new_order = ref [] in
   let liveins = ref sb.liveins in
   let exp = ref [] in
@@ -436,12 +436,12 @@ let expanse (sb : superblock) code pm =
           debug "Icond/Ccomp\n";
           exp := cbranch_int32s false c a1 a2 info succ1 succ2 [];
           was_branch := true;
-          was_exp := true
+          was_exp := true*)
       | Icond (Ccompu c, a1 :: a2 :: nil, succ1, succ2, info) ->
           debug "Icond/Ccompu\n";
           exp := cbranch_int32u false c a1 a2 info succ1 succ2 [];
           was_branch := true;
-          was_exp := true
+          was_exp := true(*
       | Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) ->
           debug "Icond/Ccompimm\n";
           exp := expanse_cbranchimm_int32s c a1 imm info succ1 succ2 [];
@@ -511,7 +511,7 @@ let expanse (sb : superblock) code pm =
   sb.instructions <- Array.of_list (List.rev !new_order);
   sb.liveins <- !liveins;
   print_ptree_regset !liveins;
-  (*debug_flag := false;*)
+  debug_flag := false;
   (!code', !pm')
 
 let rec find_last_node_reg = function
diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v
index f17dfe7d..f1f44331 100644
--- a/riscV/RTLpathSE_simplify.v
+++ b/riscV/RTLpathSE_simplify.v
@@ -373,14 +373,14 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args
       let hv2 := fsi_sreg_get prev a2 in
       let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
        Some (cond, lhsv)*)
-      (*| (Ccompu c), (a1 :: a2 :: nil) =>
+  | (Ccompu c), (a1 :: a2 :: nil) =>
       let is_inv := is_inv_cmp_int c in
       let cond := transl_cbranch_int32u c (make_optR0 false is_inv) in
       let hv1 := fsi_sreg_get prev a1 in
       let hv2 := fsi_sreg_get prev a2 in
       let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
       Some (cond, lhsv)
-  | (Ccompimm c n), (a1 :: nil) =>
+      (*| (Ccompimm c n), (a1 :: nil) =>
       let is_inv := is_inv_cmp_int c in
       let hv1 := fsi_sreg_get prev a1 in
       (if Int.eq n Int.zero then
@@ -388,7 +388,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args
         let cond := transl_cbranch_int32s c (make_optR0 true is_inv) in
         Some (cond, lhsv)
       else
-        let hvs := loadimm32 n in
+        let hvs := loadimm32 hv1 n false in
         let lhsv := make_lhsv_cmp is_inv hv1 hvs in
         let cond := transl_cbranch_int32s c (make_optR0 false is_inv) in
         Some (cond, lhsv))
@@ -400,7 +400,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args
         let cond := transl_cbranch_int32u c (make_optR0 true is_inv) in
         Some (cond, lhsv)
       else
-        let hvs := loadimm32 n in
+        let hvs := loadimm32 hv1 n false in
         let lhsv := make_lhsv_cmp is_inv hv1 hvs in
         let cond := transl_cbranch_int32u c (make_optR0 false is_inv) in
          Some (cond, lhsv))
@@ -426,7 +426,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args
         let cond := transl_cbranch_int64s c (make_optR0 true is_inv) in
         Some (cond, lhsv)
       else
-        let hvs := loadimm64 n in
+        let hvs := loadimm64 hv1 n in
         let lhsv := make_lhsv_cmp is_inv hv1 hvs in
         let cond := transl_cbranch_int64s c (make_optR0 false is_inv) in
         Some (cond, lhsv))
@@ -438,7 +438,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args
         let cond := transl_cbranch_int64u c (make_optR0 true is_inv) in
         Some (cond, lhsv)
       else
-        let hvs := loadimm64 n in
+        let hvs := loadimm64 hv1 n in
         let lhsv := make_lhsv_cmp is_inv hv1 hvs in
         let cond := transl_cbranch_int64u c (make_optR0 false is_inv) in
         Some (cond, lhsv))
@@ -465,7 +465,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args
       let hv2 := fsi_sreg_get prev f2 in
       let is_inv := is_inv_cmp_float c in
       let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
-         expanse_cbranch_fp true cond_single c lhsv*)
+           expanse_cbranch_fp true cond_single c lhsv*)
   | _, _ => None
    end.
 
@@ -1245,15 +1245,20 @@ Proof.
   (*unfold target_cbranch_expanse, seval_condition; simpl.
   intros H (LREF & SREF & SREG & SMEM) ?.
   destruct c; try congruence.
-
   all:
-    repeat (destruct l; simpl in H; try congruence);
-    destruct c; inv H; simpl;
-    erewrite !fsi_sreg_get_correct; eauto;
+    repeat (destruct l; simpl in H; try congruence).
+    inv H; simpl.
+    try erewrite !fsi_sreg_get_correct; eauto.
+
+  - simpl. 
+    destruct c; inv H; simpl.
+    try erewrite !fsi_sreg_get_correct; eauto;
     try (destruct (seval_sval ge sp (si_sreg st r) rs0 m0) eqn:OKv1; try congruence);
     try (destruct (seval_sval ge sp (si_sreg st r0) rs0 m0) eqn:OKv2; try congruence);
     try (destruct (seval_smem ge sp (si_smem st) rs0 m0) eqn:OKmem; try congruence).
 
+    try destruct (Int.eq n Int.zero) eqn: EQIMM;
+    try apply Int.same_if_eq in EQIMM;
   all:
     try replace (Cle) with (swap_comparison Cge) by auto;
     try replace (Clt) with (swap_comparison Cgt) by auto;