Adding fp init expansions

1 files changed, 15 insertions, 0 deletions

diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v
index 6a0297e9..29389850 100644
--- a/riscV/RTLpathSE_simplify.v
+++ b/riscV/RTLpathSE_simplify.v
@@ -368,6 +368,14 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca
       let is_inv := is_inv_cmp_float c in
       let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
       Some (expanse_cond_fp true cond_single c lhsv)
+  | Ofloatconst f, nil =>
+      let bits_const := fSop (Olongconst (Float.to_bits f)) fSnil in
+      let hl := make_lhsv_single bits_const in
+      Some (fSop (Ofloat_of_bits) hl)
+  | Osingleconst f, nil =>
+      let bits_const := fSop (Ointconst (Float32.to_bits f)) fSnil in
+      let hl := make_lhsv_single bits_const in
+      Some (fSop (Osingle_of_bits) hl)
   | _, _ => None
   end.
 
@@ -1211,6 +1219,13 @@ Proof.
   unfold target_op_simplify; simpl.
   intros H (LREF & SREF & SREG & SMEM) ? ? ?.
   destruct op; try congruence.
+  (* FP const expansions *)
+  1,2:
+    repeat (destruct lr; simpl; try congruence);
+    simpl in OK1; inv OK1; inv H; simpl;
+    try rewrite Float.of_to_bits;
+    try rewrite Float32.of_to_bits; trivial.
+  (* Ocmp expansions *)
   destruct cond; repeat (destruct lr; simpl; try congruence);
   simpl in OK1;
   try (destruct (seval_sval ge sp (si_sreg st r) rs0 m0) eqn:OKv1; try congruence);