From 6f71a2a369d07a8e812fb3893f30be528b28d3ee Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 2 Mar 2021 20:07:50 +0100 Subject: Adding fp init expansions --- riscV/RTLpathSE_simplify.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'riscV') 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); -- cgit