Debugging fake values finished

2 files changed, 20 insertions, 14 deletions

diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index 07999b05..39b8f367 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
@@ -432,16 +432,16 @@ let expanse (sb : superblock) code pm =
           debug "Iop/Cnotcompfs\n";
           exp := expanse_cond_fp true cond_single c f1 f2 dest succ [];
           was_exp := true
-      (*| Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) ->
+      | Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) ->
           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 [];
@@ -492,7 +492,7 @@ let expanse (sb : superblock) code pm =
           debug "Icond/Cnotcompfs\n";
           exp := expanse_cbranch_fp true cond_single c f1 f2 info succ1 succ2 [];
           was_branch := true;
-          was_exp := true*)
+          was_exp := true
       | _ -> new_order := n :: !new_order);
       if !was_exp then (
         node := !node + 1;
@@ -510,8 +510,7 @@ let expanse (sb : superblock) code pm =
     sb.instructions;
   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 f1f44331..f6d96d06 100644
--- a/riscV/RTLpathSE_simplify.v
+++ b/riscV/RTLpathSE_simplify.v
@@ -293,6 +293,13 @@ Definition transl_cbranch_int64u (cmp: comparison) (optR0: option bool) :=
   | Cge => CEbgeul optR0
   end.
 
+Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) : (condition * list_hsval) :=
+  let normal := is_normal_cmp cmp in
+  let normal' := if cnot then negb normal else normal in
+  let hvs := fn_cond cmp lhsv in
+  let hl := make_lhsv_cmp false hvs hvs in
+  if normal' then ((CEbnew (Some false)), hl) else ((CEbeqw (Some false)), hl).
+
 (** Target op simplifications using "fake" values *)
 
 Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval :=
@@ -366,13 +373,13 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca
 
 Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg) : option (condition * list_hsval) :=
   match cond, args with
-    (*| (Ccomp c), (a1 :: a2 :: nil) =>
+  | (Ccomp c), (a1 :: a2 :: nil) =>
       let is_inv := is_inv_cmp_int c in
       let cond := transl_cbranch_int32s 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)*)
+      Some (cond, lhsv)
   | (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
@@ -380,7 +387,7 @@ 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)
-      (*| (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
@@ -447,25 +454,25 @@ 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 false cond_float c lhsv
+      Some (expanse_cbranch_fp false cond_float c lhsv)
   | (Cnotcompf c), (f1 :: f2 :: nil) =>
       let hv1 := fsi_sreg_get prev f1 in
       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_float c lhsv
+      Some (expanse_cbranch_fp true cond_float c lhsv)
   | (Ccompfs c), (f1 :: f2 :: nil) =>
       let hv1 := fsi_sreg_get prev f1 in
       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 false cond_single c lhsv
+      Some (expanse_cbranch_fp false cond_single c lhsv)
   | (Cnotcompfs c), (f1 :: f2 :: nil) =>
       let hv1 := fsi_sreg_get prev f1 in
       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*)
+      Some (expanse_cbranch_fp true cond_single c lhsv)
   | _, _ => None
    end.