Commit 65eea069 authored by Joachim Bard's avatar Joachim Bard

added tightening on vars and negation

also: simplified check for downcast
parent a959dd8c
...@@ -97,7 +97,7 @@ Fixpoint validIntervalbounds (e:expr Q) (A:analysisResult) (P: FloverMap.t intv) ...@@ -97,7 +97,7 @@ Fixpoint validIntervalbounds (e:expr Q) (A:analysisResult) (P: FloverMap.t intv)
match FloverMap.find f1 A with match FloverMap.find f1 A with
| None => false | None => false
| Some (iv1, _) => | Some (iv1, _) =>
(isSupersetIntv intv iv1) && (isSupersetIntv iv1 intv) isSupersetIntv iv1 intv
end end
else else
false false
...@@ -381,12 +381,11 @@ Proof. ...@@ -381,12 +381,11 @@ Proof.
inversion env_f; subst. inversion env_f; subst.
kill_trivial_exists. kill_trivial_exists.
exists (perturb vF REAL 0). exists (perturb vF REAL 0).
split; [destruct i; try auto |]. split; [destruct i; auto |].
split; [eapply Downcast_dist'; try eauto; cbn; try rewrite Rabs_R0 |];
try lra; try auto.
canonize_hyps. canonize_hyps.
unfold perturb. split; [| cbn in *; lra].
simpl in *; lra. eapply Downcast_dist'; try eassumption; auto; auto.
cbn; rewrite Rabs_R0. lra.
Qed. Qed.
Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult): Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult):
......
...@@ -120,8 +120,9 @@ Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: precond) ...@@ -120,8 +120,9 @@ Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: precond)
else else
match FloverMap.find e P with match FloverMap.find e P with
| None => false | None => false
| Some new_iv => isSupersetIntv new_iv intv | Some iv =>
(* && (Qleb lo hi) *) let new_iv := tightenBounds e iv Q P in
isSupersetIntv new_iv intv
end end
| Const _ n => (Qleb (ivlo intv) n) && (Qleb n (ivhi intv)) | Const _ n => (Qleb (ivlo intv) n) && (Qleb n (ivhi intv))
| Unop o f => | Unop o f =>
...@@ -132,7 +133,7 @@ Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: precond) ...@@ -132,7 +133,7 @@ Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: precond)
| Some (iv, _) => | Some (iv, _) =>
match o with match o with
| Neg => | Neg =>
let new_iv := negateIntv iv in let new_iv := tightenBounds e (negateIntv iv) Q P in
isSupersetIntv new_iv intv isSupersetIntv new_iv intv
| Inv => | Inv =>
if (((Qleb (ivhi iv) 0) && (negb (Qeq_bool (ivhi iv) 0))) || if (((Qleb (ivhi iv) 0) && (negb (Qeq_bool (ivhi iv) 0))) ||
...@@ -176,6 +177,7 @@ Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: precond) ...@@ -176,6 +177,7 @@ Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: precond)
&& (validSMTIntervalbounds f2 A P Q validVars) && (validSMTIntervalbounds f2 A P Q validVars)
&& (validSMTIntervalbounds f3 A P Q validVars)) && (validSMTIntervalbounds f3 A P Q validVars))
then then
(* TODO: tightening *)
match FloverMap.find f1 A, FloverMap.find f2 A, FloverMap.find f3 A with match FloverMap.find f1 A, FloverMap.find f2 A, FloverMap.find f3 A with
| Some (iv1, _), Some (iv2, _), Some (iv3, _) => | Some (iv1, _), Some (iv2, _), Some (iv3, _) =>
let new_iv := addIntv iv1 (multIntv iv2 iv3) in let new_iv := addIntv iv1 (multIntv iv2 iv3) in
...@@ -189,7 +191,8 @@ Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: precond) ...@@ -189,7 +191,8 @@ Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: precond)
match FloverMap.find f1 A with match FloverMap.find f1 A with
| None => false | None => false
| Some (iv1, _) => | Some (iv1, _) =>
(isSupersetIntv intv iv1) && (isSupersetIntv iv1 intv) (* TODO: need tightening here or will f1 be tightened? *)
isSupersetIntv iv1 intv
end end
else else
false false
...@@ -221,16 +224,19 @@ Proof. ...@@ -221,16 +224,19 @@ Proof.
eapply toRExpMap_some in find_m; cbn; eauto. eapply toRExpMap_some in find_m; cbn; eauto.
match_simpl; auto. match_simpl; auto.
+ Flover_compute. + Flover_compute.
destruct (valid_precond n i0) as [free_n [vR [env_valid bounds_valid]]]; destruct (valid_precond n i0) as [vR [env_valid bounds_valid]];
auto using find_in_precond; set_tac. auto using find_in_precond; set_tac.
canonize_hyps. canonize_hyps.
kill_trivial_exists. kill_trivial_exists.
eexists; split; [auto | split]. assert (Heval: eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR
* econstructor; try eauto. (Var Rdefinitions.R n) vR REAL).
{ constructor; auto.
destruct types_defined as [m [find_m _]]. destruct types_defined as [m [find_m _]].
eapply toRExpMap_some in find_m; cbn; eauto. eapply toRExpMap_some in find_m; cbn; eauto.
match_simpl; auto. match_simpl; auto. }
* cbn in *. lra. eexists; split; [auto | split; eauto].
eapply Rle_trans2; eauto.
eapply tightenBounds_sound; eauto.
- split; [auto |]. - split; [auto |].
Flover_compute; canonize_hyps; cbn in *. Flover_compute; canonize_hyps; cbn in *.
kill_trivial_exists. kill_trivial_exists.
...@@ -250,12 +256,16 @@ Proof. ...@@ -250,12 +256,16 @@ Proof.
inversion iveq_f; subst. inversion iveq_f; subst.
destruct u; try andb_to_prop R; cbn in *. destruct u; try andb_to_prop R; cbn in *.
+ kill_trivial_exists. + kill_trivial_exists.
exists (evalUnop Neg vF); split; pose (v := ((evalUnop Neg vF) )).
[auto | split ; [econstructor; eauto | ]]. exists v; split; auto.
* cbn; auto. assert (Heval: eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR
* canonize_hyps. (Unop Neg (toREval (toRExp f))) v REAL)
rewrite Q2R_opp in *. by (econstructor; try eassumption; auto).
cbn; lra. split; auto.
canonize_hyps.
eapply Rle_trans2; eauto.
eapply tightenBounds_sound; eauto.
cbn. rewrite !Q2R_opp. lra.
+ rename L0 into nodiv0. + rename L0 into nodiv0.
apply le_neq_bool_to_lt_prop in nodiv0. apply le_neq_bool_to_lt_prop in nodiv0.
kill_trivial_exists. kill_trivial_exists.
...@@ -411,11 +421,11 @@ Proof. ...@@ -411,11 +421,11 @@ Proof.
inversion env_f; subst. inversion env_f; subst.
kill_trivial_exists. kill_trivial_exists.
exists (perturb vF REAL 0). exists (perturb vF REAL 0).
split; [destruct i; try auto |]. split; [destruct i; auto |].
split; [eapply Downcast_dist'; try eauto; cbn; try rewrite Rabs_R0 |];
try lra; try auto.
canonize_hyps. canonize_hyps.
cbn in *; lra. split; [| cbn in *; lra].
eapply Downcast_dist'; try eassumption; auto; auto.
cbn; rewrite Rabs_R0. lra.
Qed. Qed.
Fixpoint validSMTIntervalboundsCmd (f:cmd Q) (A:analysisResult) (P: precond) Fixpoint validSMTIntervalboundsCmd (f:cmd Q) (A:analysisResult) (P: precond)
......
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