From 801cd27eb78a9ba9dce6f62626288531905fcfed Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Tue, 2 Mar 2021 18:48:53 +0100
Subject: [Admitted checker] Oracle expansion for float/float32 constant init

---
 riscV/ExpansionOracle.ml | 25 +++++++++++++++++++++++--
 riscV/PrintOp.ml         |  8 ++++----
 2 files changed, 27 insertions(+), 6 deletions(-)

(limited to 'riscV')

diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index 95a300c5..c6710a95 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -379,7 +379,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
@@ -393,6 +393,7 @@ let expanse (sb : superblock) code pm =
       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 [];
@@ -441,6 +442,7 @@ 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
+      (* 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 [];
@@ -502,6 +504,25 @@ let expanse (sb : superblock) code pm =
           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;
@@ -521,7 +542,7 @@ let expanse (sb : superblock) code pm =
     sb.instructions;
   sb.instructions <- Array.of_list (List.rev !new_order);
   sb.liveins <- !liveins;
-  (*debug_flag := false;*)
+  debug_flag := false;
   (!code', !pm')
 
 let rec find_last_node_reg = function
diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml
index 84380251..4734795a 100644
--- a/riscV/PrintOp.ml
+++ b/riscV/PrintOp.ml
@@ -97,10 +97,10 @@ let print_condition reg pp = function
 
 let print_operation reg pp = function
   | Omove, [r1] -> reg pp r1
-  | Ointconst n, [] -> fprintf pp "%ld" (camlint_of_coqint n)
-  | Olongconst n, [] -> fprintf pp "%LdL" (camlint64_of_coqint n)
-  | Ofloatconst n, [] -> fprintf pp "%F" (camlfloat_of_coqfloat n)
-  | Osingleconst n, [] -> fprintf pp "%Ff" (camlfloat_of_coqfloat32 n)
+  | Ointconst n, [] -> fprintf pp "Ointconst(%ld)" (camlint_of_coqint n)
+  | Olongconst n, [] -> fprintf pp "Olongconst(%LdL)" (camlint64_of_coqint n)
+  | Ofloatconst n, [] -> fprintf pp "Ofloatconst(%F)" (camlfloat_of_coqfloat n)
+  | Osingleconst n, [] -> fprintf pp "Osingleconst(%Ff)" (camlfloat_of_coqfloat32 n)
   | Oaddrsymbol(id, ofs), [] ->
       fprintf pp "\"%s\" + %Ld" (extern_atom id) (camlint64_of_ptrofs ofs)
   | Oaddrstack ofs, [] ->
-- 
cgit