Adding a flag to test fp_init_exp

3 files changed, 159 insertions, 150 deletions

diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 4cff3f28..8d85e93a 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -106,6 +106,7 @@ let option_div_i32 = ref "stsud"
 let option_div_i64 = ref "stsud" 
 let option_fcoalesce_mem = ref true
 let option_fexpanse_rtlcond = ref true
+let option_fexpanse_fpconst = ref true
 let option_fforward_moves = ref false
 let option_fmove_loop_invariants = ref false
 let option_fnontrap_loads = ref true
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 0c5d9cb4..9750981e 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -445,6 +445,7 @@ let cmdline_actions =
   @ f_opt "nontrap-loads" option_fnontrap_loads
   @ f_opt "coalesce-mem" option_fcoalesce_mem
   @ f_opt "expanse-rtlcond" option_fexpanse_rtlcond
+  @ f_opt "expanse-fpconst" option_fexpanse_fpconst
   @ f_opt "all-loads-nontrap" option_all_loads_nontrap
   @ f_opt "forward-moves" option_fforward_moves
  (* Code generation options *)
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index c6710a95..23e3c38e 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -389,156 +389,163 @@ let expanse (sb : superblock) code pm =
   let pm' = ref pm in
   Array.iter
     (fun n ->
-      was_branch := false;
-      was_exp := false;
-      let inst = get_some @@ PTree.get n code in
-      (match inst with
-      (* Expansion of conditions - Ocmp *)
-      | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) ->
-          debug "Iop/Ccomp\n";
-          exp := cond_int32s false c a1 a2 dest succ [];
-          was_exp := true
-      | Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) ->
-          debug "Iop/Ccompu\n";
-          exp := cond_int32u false c a1 a2 dest succ [];
-          was_exp := true
-      | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) ->
-          debug "Iop/Ccompimm\n";
-          exp := expanse_condimm_int32s c a1 imm dest succ [];
-          was_exp := true
-      | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) ->
-          debug "Iop/Ccompuimm\n";
-          exp := expanse_condimm_int32u c a1 imm dest succ [];
-          was_exp := true
-      | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) ->
-          debug "Iop/Ccompl\n";
-          exp := cond_int64s false c a1 a2 dest succ [];
-          was_exp := true
-      | Iop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, succ) ->
-          debug "Iop/Ccomplu\n";
-          exp := cond_int64u false c a1 a2 dest succ [];
-          was_exp := true
-      | Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) ->
-          debug "Iop/Ccomplimm\n";
-          exp := expanse_condimm_int64s c a1 imm dest succ [];
-          was_exp := true
-      | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) ->
-          debug "Iop/Ccompluimm\n";
-          exp := expanse_condimm_int64u c a1 imm dest succ [];
-          was_exp := true
-      | Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, succ) ->
-          debug "Iop/Ccompf\n";
-          exp := expanse_cond_fp false cond_float c f1 f2 dest succ [];
-          was_exp := true
-      | Iop (Ocmp (Cnotcompf c), f1 :: f2 :: nil, dest, succ) ->
-          debug "Iop/Cnotcompf\n";
-          exp := expanse_cond_fp true cond_float c f1 f2 dest succ [];
-          was_exp := true
-      | Iop (Ocmp (Ccompfs c), f1 :: f2 :: nil, dest, succ) ->
-          debug "Iop/Ccompfs\n";
-          exp := expanse_cond_fp false cond_single c f1 f2 dest succ [];
-          was_exp := true
-      | Iop (Ocmp (Cnotcompfs c), f1 :: f2 :: nil, dest, succ) ->
-          debug "Iop/Cnotcompfs\n";
-          exp := expanse_cond_fp true cond_single c f1 f2 dest succ [];
-          was_exp := true
-      (* Expansion of branches - Ccomp *)
-      | 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
-      | 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
-      | Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) ->
-          debug "Icond/Ccompimm\n";
-          exp := expanse_cbranchimm_int32s c a1 imm info succ1 succ2 [];
-          was_branch := true;
-          was_exp := true
-      | Icond (Ccompuimm (c, imm), a1 :: nil, succ1, succ2, info) ->
-          debug "Icond/Ccompuimm\n";
-          exp := expanse_cbranchimm_int32u c a1 imm info succ1 succ2 [];
-          was_branch := true;
-          was_exp := true
-      | Icond (Ccompl c, a1 :: a2 :: nil, succ1, succ2, info) ->
-          debug "Icond/Ccompl\n";
-          exp := cbranch_int64s false c a1 a2 info succ1 succ2 [];
-          was_branch := true;
-          was_exp := true
-      | Icond (Ccomplu c, a1 :: a2 :: nil, succ1, succ2, info) ->
-          debug "Icond/Ccomplu\n";
-          exp := cbranch_int64u false c a1 a2 info succ1 succ2 [];
-          was_branch := true;
-          was_exp := true
-      | Icond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, info) ->
-          debug "Icond/Ccomplimm\n";
-          exp := expanse_cbranchimm_int64s c a1 imm info succ1 succ2 [];
-          was_branch := true;
-          was_exp := true
-      | Icond (Ccompluimm (c, imm), a1 :: nil, succ1, succ2, info) ->
-          debug "Icond/Ccompluimm\n";
-          exp := expanse_cbranchimm_int64u c a1 imm info succ1 succ2 [];
-          was_branch := true;
-          was_exp := true
-      | Icond (Ccompf c, f1 :: f2 :: nil, succ1, succ2, info) ->
-          debug "Icond/Ccompf\n";
-          exp := expanse_cbranch_fp false cond_float c f1 f2 info succ1 succ2 [];
-          was_branch := true;
-          was_exp := true
-      | Icond (Cnotcompf c, f1 :: f2 :: nil, succ1, succ2, info) ->
-          debug "Icond/Cnotcompf\n";
-          exp := expanse_cbranch_fp true cond_float c f1 f2 info succ1 succ2 [];
-          was_branch := true;
-          was_exp := true
-      | Icond (Ccompfs c, f1 :: f2 :: nil, succ1, succ2, info) ->
-          debug "Icond/Ccompfs\n";
-          exp :=
-            expanse_cbranch_fp false cond_single c f1 f2 info succ1 succ2 [];
-          was_branch := true;
-          was_exp := true
-      | Icond (Cnotcompfs c, f1 :: f2 :: nil, succ1, succ2, info) ->
-          debug "Icond/Cnotcompfs\n";
-          exp := expanse_cbranch_fp true cond_single c f1 f2 info succ1 succ2 [];
-          was_branch := true;
-          was_exp := true
-      (* Expansion of fp constants *)
-      | Iop (Ofloatconst f, nil, dest, succ) ->
-          debug "Iop/Ofloatconst\n";
-          let r = r2pi () in
-          exp :=
-            [
-              Iop (Olongconst (Floats.Float.to_bits f), [], r, n2pi ());
-              Iop (Ofloat_of_bits, [ r ], dest, succ);
-            ];
-          was_exp := true
-      | Iop (Osingleconst f, nil, dest, succ) ->
-          debug "Iop/Osingleconst\n";
-          let r = r2pi () in
-          exp :=
-            [
-              Iop (Ointconst (Floats.Float32.to_bits f), [], r, n2pi ());
-              Iop (Osingle_of_bits, [ r ], dest, succ);
-            ];
-          was_exp := true
-      | _ -> new_order := n :: !new_order);
-      if !was_exp then (
-        node := !node + 1;
-        (if !was_branch then
-         let lives = PTree.get n !liveins in
-         match lives with
-         | Some lives ->
-             let new_branch_pc =
-               Camlcoq.P.of_int (!node - (List.length !exp - 1))
-             in
-             liveins := PTree.set new_branch_pc lives !liveins;
-             liveins := PTree.remove n !liveins
-         | _ -> ());
-        write_pathmap sb.instructions.(0) (List.length !exp) pm';
-        write_initial_node n code' new_order;
-        write_tree !exp !node code' new_order))
+      begin (
+        was_branch := false;
+        was_exp := false;
+        let inst = get_some @@ PTree.get n code in
+        if !Clflags.option_fexpanse_rtlcond then (
+        match inst with
+        (* Expansion of conditions - Ocmp *)
+        | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) ->
+            debug "Iop/Ccomp\n";
+            exp := cond_int32s false c a1 a2 dest succ [];
+            was_exp := true
+        | Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) ->
+            debug "Iop/Ccompu\n";
+            exp := cond_int32u false c a1 a2 dest succ [];
+            was_exp := true
+        | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) ->
+            debug "Iop/Ccompimm\n";
+            exp := expanse_condimm_int32s c a1 imm dest succ [];
+            was_exp := true
+        | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) ->
+            debug "Iop/Ccompuimm\n";
+            exp := expanse_condimm_int32u c a1 imm dest succ [];
+            was_exp := true
+        | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) ->
+            debug "Iop/Ccompl\n";
+            exp := cond_int64s false c a1 a2 dest succ [];
+            was_exp := true
+        | Iop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, succ) ->
+            debug "Iop/Ccomplu\n";
+            exp := cond_int64u false c a1 a2 dest succ [];
+            was_exp := true
+        | Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) ->
+            debug "Iop/Ccomplimm\n";
+            exp := expanse_condimm_int64s c a1 imm dest succ [];
+            was_exp := true
+        | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) ->
+            debug "Iop/Ccompluimm\n";
+            exp := expanse_condimm_int64u c a1 imm dest succ [];
+            was_exp := true
+        | Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, succ) ->
+            debug "Iop/Ccompf\n";
+            exp := expanse_cond_fp false cond_float c f1 f2 dest succ [];
+            was_exp := true
+        | Iop (Ocmp (Cnotcompf c), f1 :: f2 :: nil, dest, succ) ->
+            debug "Iop/Cnotcompf\n";
+            exp := expanse_cond_fp true cond_float c f1 f2 dest succ [];
+            was_exp := true
+        | Iop (Ocmp (Ccompfs c), f1 :: f2 :: nil, dest, succ) ->
+            debug "Iop/Ccompfs\n";
+            exp := expanse_cond_fp false cond_single c f1 f2 dest succ [];
+            was_exp := true
+        | Iop (Ocmp (Cnotcompfs c), f1 :: f2 :: nil, dest, succ) ->
+            debug "Iop/Cnotcompfs\n";
+            exp := expanse_cond_fp true cond_single c f1 f2 dest succ [];
+            was_exp := true
+        (* Expansion of branches - Ccomp *)
+        | 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
+        | 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
+        | Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) ->
+            debug "Icond/Ccompimm\n";
+            exp := expanse_cbranchimm_int32s c a1 imm info succ1 succ2 [];
+            was_branch := true;
+            was_exp := true
+        | Icond (Ccompuimm (c, imm), a1 :: nil, succ1, succ2, info) ->
+            debug "Icond/Ccompuimm\n";
+            exp := expanse_cbranchimm_int32u c a1 imm info succ1 succ2 [];
+            was_branch := true;
+            was_exp := true
+        | Icond (Ccompl c, a1 :: a2 :: nil, succ1, succ2, info) ->
+            debug "Icond/Ccompl\n";
+            exp := cbranch_int64s false c a1 a2 info succ1 succ2 [];
+            was_branch := true;
+            was_exp := true
+        | Icond (Ccomplu c, a1 :: a2 :: nil, succ1, succ2, info) ->
+            debug "Icond/Ccomplu\n";
+            exp := cbranch_int64u false c a1 a2 info succ1 succ2 [];
+            was_branch := true;
+            was_exp := true
+        | Icond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, info) ->
+            debug "Icond/Ccomplimm\n";
+            exp := expanse_cbranchimm_int64s c a1 imm info succ1 succ2 [];
+            was_branch := true;
+            was_exp := true
+        | Icond (Ccompluimm (c, imm), a1 :: nil, succ1, succ2, info) ->
+            debug "Icond/Ccompluimm\n";
+            exp := expanse_cbranchimm_int64u c a1 imm info succ1 succ2 [];
+            was_branch := true;
+            was_exp := true
+        | Icond (Ccompf c, f1 :: f2 :: nil, succ1, succ2, info) ->
+            debug "Icond/Ccompf\n";
+            exp := expanse_cbranch_fp false cond_float c f1 f2 info succ1 succ2 [];
+            was_branch := true;
+            was_exp := true
+        | Icond (Cnotcompf c, f1 :: f2 :: nil, succ1, succ2, info) ->
+            debug "Icond/Cnotcompf\n";
+            exp := expanse_cbranch_fp true cond_float c f1 f2 info succ1 succ2 [];
+            was_branch := true;
+            was_exp := true
+        | Icond (Ccompfs c, f1 :: f2 :: nil, succ1, succ2, info) ->
+            debug "Icond/Ccompfs\n";
+            exp :=
+              expanse_cbranch_fp false cond_single c f1 f2 info succ1 succ2 [];
+            was_branch := true;
+            was_exp := true
+        | Icond (Cnotcompfs c, f1 :: f2 :: nil, succ1, succ2, info) ->
+            debug "Icond/Cnotcompfs\n";
+            exp := expanse_cbranch_fp true cond_single c f1 f2 info succ1 succ2 [];
+            was_branch := true;
+            was_exp := true
+        | _ -> ());
+        if (!Clflags.option_fexpanse_fpconst && not !was_exp) then (
+        match inst with
+        (* Expansion of fp constants *)
+        | Iop (Ofloatconst f, nil, dest, succ) ->
+            debug "Iop/Ofloatconst\n";
+            let r = r2pi () in
+            exp :=
+              [
+                Iop (Olongconst (Floats.Float.to_bits f), [], r, n2pi ());
+                Iop (Ofloat_of_bits, [ r ], dest, succ);
+              ];
+            was_exp := true
+        | Iop (Osingleconst f, nil, dest, succ) ->
+            debug "Iop/Osingleconst\n";
+            let r = r2pi () in
+            exp :=
+              [
+                Iop (Ointconst (Floats.Float32.to_bits f), [], r, n2pi ());
+                Iop (Osingle_of_bits, [ r ], dest, succ);
+              ];
+            was_exp := true
+        | _ -> ());
+        if !was_exp then (
+          node := !node + 1;
+          (if !was_branch then
+           let lives = PTree.get n !liveins in
+           match lives with
+           | Some lives ->
+               let new_branch_pc =
+                 Camlcoq.P.of_int (!node - (List.length !exp - 1))
+               in
+               liveins := PTree.set new_branch_pc lives !liveins;
+               liveins := PTree.remove n !liveins
+           | _ -> ());
+          write_pathmap sb.instructions.(0) (List.length !exp) pm';
+          write_initial_node n code' new_order;
+          write_tree !exp !node code' new_order)
+          else new_order := n :: !new_order)
+      end)
     sb.instructions;
   sb.instructions <- Array.of_list (List.rev !new_order);
   sb.liveins <- !liveins;