diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-02 20:07:50 +0100 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-02 20:07:50 +0100 |
commit | 6f71a2a369d07a8e812fb3893f30be528b28d3ee (patch) | |
tree | d12323efa719226e072abd955a7302eaa3b546c7 | |
parent | ef67224a0ec3ef67db98198008e7f9d5bfc79ca8 (diff) | |
download | compcert-kvx-6f71a2a369d07a8e812fb3893f30be528b28d3ee.tar.gz compcert-kvx-6f71a2a369d07a8e812fb3893f30be528b28d3ee.zip |
Adding fp init expansions
-rw-r--r-- | riscV/RTLpathSE_simplify.v | 15 | ||||
-rw-r--r-- | scheduling/RTLpathScheduler.v | 6 |
2 files changed, 18 insertions, 3 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); diff --git a/scheduling/RTLpathScheduler.v b/scheduling/RTLpathScheduler.v index 79129872..31680256 100644 --- a/scheduling/RTLpathScheduler.v +++ b/scheduling/RTLpathScheduler.v @@ -158,7 +158,7 @@ Definition verified_scheduler (f: RTLpath.function) : res (RTLpath.function * (P let (tc, te) := tcte in let tfr := mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te in do tf <- proj1_sig (function_builder tfr tpm); - (*do tt <- function_equiv_checker dm f tf; *) + do tt <- function_equiv_checker dm f tf; OK (tf, dm). Theorem verified_scheduler_correct f tf dm: @@ -171,7 +171,7 @@ Theorem verified_scheduler_correct f tf dm: /\ (forall pc1 pc2, dm ! pc2 = Some pc1 -> path_entry (fn_path tf) pc2) /\ (forall pc1 pc2, dm ! pc2 = Some pc1 -> sexec_simu dm f tf pc1 pc2) . -Proof. Admitted. (* +Proof. intros VERIF. unfold verified_scheduler in VERIF. explore. Local Hint Resolve function_equiv_checker_entrypoint function_equiv_checker_pathentry1 function_equiv_checker_pathentry2 @@ -180,7 +180,7 @@ Proof. Admitted. (* apply H in EQ2. rewrite EQ2. simpl. repeat (constructor; eauto). exploit function_equiv_checker_entrypoint. eapply EQ4. rewrite EQ2. intuition. - Qed. *) +Qed. Record match_function (dupmap: PTree.t node) (f1 f2: RTLpath.function): Prop := { preserv_fnsig: fn_sig f1 = fn_sig f2; |