Commit 6f71a2a3 authored by Léo Gourdin's avatar Léo Gourdin
Browse files

Adding fp init expansions

parent ef67224a
......@@ -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);
......
......@@ -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;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment