Commit 9a055ff5 authored by Joachim Bard's avatar Joachim Bard

tightening on FMA

parent 0c1dfc5f
......@@ -235,10 +235,10 @@ Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: precond)
&& (validSMTIntervalbounds f2 A P Q L validVars)
&& (validSMTIntervalbounds f3 A P Q L validVars))
then
(* TODO: tightening *)
match FloverMap.find f1 A, FloverMap.find f2 A, FloverMap.find f3 A with
| Some (iv1, _), Some (iv2, _), Some (iv3, _) =>
let new_iv := addIntv iv1 (multIntv iv2 iv3) in
let mult_iv := tightenBounds (Binop Mult f2 f3) (multIntv iv2 iv3) Q P L in
let new_iv := tightenBounds e (addIntv iv1 mult_iv) Q P L in
isSupersetIntv new_iv intv
| _, _, _ => false
end
......@@ -455,23 +455,34 @@ Proof.
destruct valid_f3 as [iv_f3 [err3 [vF3 [env3 [eval_f3 valid_f3]]]]].
Flover_compute; try congruence.
kill_trivial_exists.
exists (perturb (evalFma vF1 vF2 vF3) REAL 0); split; try auto.
pose (v := perturb (evalFma vF1 vF2 vF3) REAL 0).
exists v; split; auto.
assert (Heval: eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR
(Fma (toREval (toRExp f1)) (toREval (toRExp f2))
(toREval (toRExp f3))) v REAL).
{ eapply Fma_dist' with (delta := 0%R); try congruence; cbn;
try rewrite Rabs_R0; try auto; try lra; eauto. }
inversion env1; inversion env2; inversion env3; subst.
split; [auto | ].
* eapply Fma_dist' with (delta := 0%R); try congruence; cbn;
try rewrite Rabs_R0; try auto; try lra; eauto.
* pose proof (interval_multiplication_valid (Q2R (fst iv_f2),Q2R (snd iv_f2)) (Q2R (fst iv_f3), Q2R (snd iv_f3))) as valid_mul.
specialize (valid_mul vF2 vF3 valid_f2 valid_f3).
remember (multInterval (Q2R (fst iv_f2), Q2R (snd iv_f2)) (Q2R (fst iv_f3), Q2R (snd iv_f3))) as iv_f23prod.
pose proof (interval_addition_valid (Q2R (fst iv_f1),Q2R (snd iv_f1)) (fst iv_f23prod, snd iv_f23prod)) as valid_add.
rewrite Heqiv_f23prod in valid_add, valid_mul.
unfold multIntv in valid_add.
canonize_hyps.
cbn in *.
rewrite <- ?Q2R_mult, <- ?Q2R_min4 , <- ?Q2R_max4 in *.
rewrite <- ?Q2R_plus, <- ?Q2R_min4, <- ?Q2R_max4 in *.
specialize (valid_add vF1 (vF2 * vF3)%R valid_f1 valid_mul).
eapply Rle_trans2; eauto.
pose proof (interval_multiplication_valid (Q2R (fst iv_f2),Q2R (snd iv_f2)) (Q2R (fst iv_f3), Q2R (snd iv_f3))) as valid_mul.
specialize (valid_mul vF2 vF3 valid_f2 valid_f3).
pose (mult_interval := tightenBounds (Binop Mult f2 f3) (multIntv iv_f2 iv_f3) Q P L).
pose proof (@interval_addition_valid (Q2R (fst iv_f1), Q2R (snd iv_f1))
(Q2R (fst mult_interval), Q2R (snd mult_interval))
vF1 (vF2 * vF3)) as valid_add.
unfold mult_interval in valid_add.
canonize_hyps.
eapply Rle_trans2; eauto.
eapply tightenBounds_sound; eauto using inlineLets_sound.
cbn in *. rewrite ?Q2R_min4, ?Q2R_max4, ?Q2R_plus.
apply valid_add; auto.
assert (Heval_mult: eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR
(Binop Mult (toREval (toRExp f2)) (toREval (toRExp f3)))
(vF2 * vF3) REAL).
{ eapply Binop_dist' with (delta := 0%R); try congruence;
try rewrite Rabs_R0; cbn; try lra; try reflexivity; eauto. }
eapply tightenBounds_sound; eauto using inlineLets_sound.
cbn. now rewrite ?Q2R_min4, ?Q2R_max4, ?Q2R_mult.
- destruct types_defined
as [mG [find_mG [[validt_f _] _]]].
assert (validRanges f A E (toRTMap (toRExpMap Gamma))) as valid_f1
......
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