Commit d9364172 authored by Joachim Bard's avatar Joachim Bard

implementing cover check for subdivs

parent ae671726
...@@ -11,11 +11,11 @@ From Flover ...@@ -11,11 +11,11 @@ From Flover
Require Import List. Require Import List.
Fixpoint result_leq e (A1 A2: analysisResult) := Fixpoint resultLeq e (A1 A2: analysisResult) :=
match e with match e with
| Unop _ e1 | Downcast _ e1 => result_leq e1 A1 A2 | Unop _ e1 | Downcast _ e1 => resultLeq e1 A1 A2
| Binop _ e1 e2 | Let _ _ e1 e2 => result_leq e1 A1 A2 && result_leq e2 A1 A2 | Binop _ e1 e2 | Let _ _ e1 e2 => resultLeq e1 A1 A2 && resultLeq e2 A1 A2
| Fma e1 e2 e3 => result_leq e1 A1 A2 && result_leq e2 A1 A2 && result_leq e3 A1 A2 | Fma e1 e2 e3 => resultLeq e1 A1 A2 && resultLeq e2 A1 A2 && resultLeq e3 A1 A2
| _ => true | _ => true
end && end &&
match FloverMap.find e A1, FloverMap.find e A2 with match FloverMap.find e A1, FloverMap.find e A2 with
...@@ -23,8 +23,8 @@ Fixpoint result_leq e (A1 A2: analysisResult) := ...@@ -23,8 +23,8 @@ Fixpoint result_leq e (A1 A2: analysisResult) :=
| _, _ => false | _, _ => false
end. end.
Lemma result_leq_sound e A1 A2 : Lemma resultLeq_sound e A1 A2 :
result_leq e A1 A2 = true -> resultLeq e A1 A2 = true ->
exists iv1 err1 iv2 err2, exists iv1 err1 iv2 err2,
FloverMap.find e A1 = Some (iv1, err1) /\ FloverMap.find e A1 = Some (iv1, err1) /\
FloverMap.find e A2 = Some (iv2, err2) /\ FloverMap.find e A2 = Some (iv2, err2) /\
...@@ -37,7 +37,7 @@ Proof. ...@@ -37,7 +37,7 @@ Proof.
| Some (ivA1, errA1), Some (ivA2, errA2) => isSupersetIntv ivA1 ivA2 && (Qleb errA1 errA2) | Some (ivA1, errA1), Some (ivA2, errA2) => isSupersetIntv ivA1 ivA2 && (Qleb errA1 errA2)
| _, _ => false | _, _ => false
end = true). end = true).
{ unfold result_leq in H. destruct e; { unfold resultLeq in H. destruct e;
apply andb_prop in H as [_ H]; auto. } apply andb_prop in H as [_ H]; auto. }
Flover_compute. Flover_compute.
repeat eexists; auto. repeat eexists; auto.
...@@ -58,41 +58,42 @@ Proof. ...@@ -58,41 +58,42 @@ Proof.
- exfalso. eapply He. set_tac. - exfalso. eapply He. set_tac.
Qed. Qed.
Definition check_subdivs_step e absenv defVars Gamma (b: bool) (PA: precond * analysisResult) := Definition checkSubdivsStep e absenv defVars Gamma (b: bool) (PA: precond * analysisResult) :=
let (P, A) := PA in let (P, A) := PA in
b && (RangeErrorChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma) && b && (RangeErrorChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma) &&
result_leq e A absenv. resultLeq e A absenv.
Definition check_subdivs e absenv subdivs defVars Gamma := Definition checkSubdivs e absenv subdivs defVars Gamma :=
fold_left (check_subdivs_step e absenv defVars Gamma) subdivs true. fold_left (checkSubdivsStep e absenv defVars Gamma) subdivs true.
Lemma check_subdivs_false_fp e absenv subdivs defVars Gamma : Lemma checkSubdivs_false_fp e absenv subdivs defVars Gamma :
fold_left (check_subdivs_step e absenv defVars Gamma) subdivs false = false. fold_left (checkSubdivsStep e absenv defVars Gamma) subdivs false = false.
Proof. Proof.
induction subdivs as [|[P A] subdivs]; auto. induction subdivs as [|[P A] subdivs]; auto.
Qed. Qed.
Lemma check_subdivs_sound e absenv subdivs defVars Gamma P A : Lemma checkSubdivs_sound e absenv subdivs defVars Gamma P A :
check_subdivs e absenv subdivs defVars Gamma = true -> checkSubdivs e absenv subdivs defVars Gamma = true ->
In (P, A) subdivs -> In (P, A) subdivs ->
RangeErrorChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma = true /\ RangeErrorChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma = true /\
result_leq e A absenv = true. resultLeq e A absenv = true.
Proof. Proof.
intros H Hin. intros H Hin.
induction subdivs; cbn in Hin; auto. induction subdivs; cbn in Hin; auto.
destruct Hin; subst; auto. destruct Hin; subst; auto.
- cbn in *. - cbn in *.
destruct (RangeErrorChecker e A P (FloverMap.empty (SMTLogic * SMTLogic)) defVars Gamma) eqn:?; destruct (RangeErrorChecker e A P (FloverMap.empty (SMTLogic * SMTLogic)) defVars Gamma) eqn:?;
try (rewrite check_subdivs_false_fp in H; discriminate H). try (rewrite checkSubdivs_false_fp in H; discriminate H).
split; auto. split; auto.
destruct (result_leq e A absenv) eqn: ?; auto. destruct (resultLeq e A absenv) eqn: ?; auto.
rewrite check_subdivs_false_fp in H; auto. rewrite checkSubdivs_false_fp in H; auto.
- apply IHsubdivs; auto. cbn in H. - apply IHsubdivs; auto. cbn in H.
unfold check_subdivs. unfold checkSubdivs.
destruct (check_subdivs_step e absenv defVars Gamma true a) eqn:?; auto. destruct (checkSubdivsStep e absenv defVars Gamma true a) eqn:?; auto.
rewrite check_subdivs_false_fp in H. discriminate H. rewrite checkSubdivs_false_fp in H. discriminate H.
Qed. Qed.
(*
Fixpoint merge_subdivs_step (e: expr Q) (acc A1 A2: analysisResult) := Fixpoint merge_subdivs_step (e: expr Q) (acc A1 A2: analysisResult) :=
match FloverMap.find e A1, FloverMap.find e A2 with match FloverMap.find e A1, FloverMap.find e A2 with
| Some (iv1, err1), Some (iv2, err2) => | Some (iv1, err1), Some (iv2, err2) =>
...@@ -113,6 +114,66 @@ Fixpoint merge_subdivs_step (e: expr Q) (acc A1 A2: analysisResult) := ...@@ -113,6 +114,66 @@ Fixpoint merge_subdivs_step (e: expr Q) (acc A1 A2: analysisResult) :=
instead of merging 2 results for all expressions *) instead of merging 2 results for all expressions *)
Definition merge_subdivs e hd tl : analysisResult := Definition merge_subdivs e hd tl : analysisResult :=
fold_left (merge_subdivs_step e (FloverMap.empty (intv * error))) tl hd. fold_left (merge_subdivs_step e (FloverMap.empty (intv * error))) tl hd.
*)
(* TODO: joining of subintervals *)
Definition joinIntv iv1 iv2 : result (option intv) :=
if isSupersetIntv iv2 iv1 then Succes (Some iv1) else
if Qeqb (ivhi iv1) (ivlo iv2) then Succes (Some (ivlo iv1, ivhi iv2)) else Fail _ "intervals don't align".
Definition checkDimensionStep x (ivAcc: result (option intv)) P (* (ivNew: option intv) *) :=
let ivNew := FloverMap.find (Var Q x) P in
match ivAcc with
| Succes ivAcc => match ivNew with
| Some ivNew => optionBind ivAcc (fun iv => joinIntv iv ivNew) (Succes (Some ivNew))
| None => Fail _ "var not found in precond"
end
| f => f
end.
Definition checkDimension x iv Ps :=
match fold_left (checkDimensionStep x) Ps (Succes None) with
| Succes (Some ivU) => isSupersetIntv iv ivU
| _ => false
(*
| Succes None => Fail _ "no subdivisions given"
| Fail _ msg | FailDet msg _ => Fail _ msg
*)
end.
Definition checkAllDimensionsStep Ps b (p: expr Q * intv) :=
match p with
| (Var _ x, iv) => b && checkDimension x iv Ps
| _ => b
end.
Definition checkAllDimensions P Ps :=
fold_left (checkAllDimensionsStep Ps) P true.
Lemma in_subdivs_intv (Ps: list precondIntv) E (P: precondIntv) :
checkAllDimensions (FloverMap.elements P) Ps = true ->
P_intv_sound E P ->
exists P', In P' Ps /\ P_intv_sound E P'.
Proof.
intros chk H.
unfold P_intv_sound in H.
induction (FloverMap.elements P).
- admit.
- cbn in chk.
assert (checkAllDimensionsStep Ps true a = true) as Heq by admit.
rewrite Heq in chk.
apply IHl; auto.
intros x iv.
intros ?. apply H. now right.
(*
assert (a = (Var Q x, iv) \/ a <> (Var Q x, iv)) as CA by admit.
destruct CA as [? | Hneq].
+ subst.
cbn in Heq.
intros ?. apply H. now right.
+ intros ?. apply H. now right.
*)
Abort.
(* TODO: needs more assumptions, i.e. checker for precond *) (* TODO: needs more assumptions, i.e. checker for precond *)
Lemma in_subdivs (subdivs: list (precond * analysisResult)) E P : Lemma in_subdivs (subdivs: list (precond * analysisResult)) E P :
...@@ -126,7 +187,7 @@ Admitted. ...@@ -126,7 +187,7 @@ Admitted.
Definition SubdivsChecker (e: expr Q) (absenv: analysisResult) Definition SubdivsChecker (e: expr Q) (absenv: analysisResult)
(P: precond) hd tl (defVars: FloverMap.t mType) Gamma := (P: precond) hd tl (defVars: FloverMap.t mType) Gamma :=
validSSA e (preVars P) && validSSA e (preVars P) &&
check_subdivs e absenv (hd :: tl) defVars Gamma. checkSubdivs e absenv (hd :: tl) defVars Gamma.
(** (**
Soundness proof for the interval subdivs checker. Soundness proof for the interval subdivs checker.
...@@ -155,7 +216,7 @@ Proof. ...@@ -155,7 +216,7 @@ Proof.
apply (in_subdivs (hd_subdivs :: tl_subdivs)) in P_valid as [P' [A [in_subdivs P_valid]]]. apply (in_subdivs (hd_subdivs :: tl_subdivs)) in P_valid as [P' [A [in_subdivs P_valid]]].
(* preVars P == preVars P' should hold *) (* preVars P == preVars P' should hold *)
assert (validSSA e (preVars P') = true) as valid_ssa' by admit. assert (validSSA e (preVars P') = true) as valid_ssa' by admit.
pose proof (check_subdivs_sound e _ _ _ _ _ _ valid_subdivs in_subdivs) as [range_err_check A_leq]. pose proof (checkSubdivs_sound e _ _ _ _ _ _ valid_subdivs in_subdivs) as [range_err_check A_leq].
assert (ResultChecker e A P' (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma = true) as res_check assert (ResultChecker e A P' (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma = true) as res_check
by (unfold ResultChecker; now rewrite valid_ssa', range_err_check). by (unfold ResultChecker; now rewrite valid_ssa', range_err_check).
exists Gamma; intros approxE1E2. exists Gamma; intros approxE1E2.
...@@ -171,7 +232,7 @@ Proof. ...@@ -171,7 +232,7 @@ Proof.
destruct validRange as [iv [err [vR [Hfind [eval_real validRange]]]]]. destruct validRange as [iv [err [vR [Hfind [eval_real validRange]]]]].
eapply validErrorBounds_single in Hsound; eauto. eapply validErrorBounds_single in Hsound; eauto.
destruct Hsound as [[vF [mF eval_float]] err_bounded]; auto. destruct Hsound as [[vF [mF eval_float]] err_bounded]; auto.
destruct (result_leq_sound _ _ _ A_leq) as [iv1 [err1 [iv2 [err2 H]]]]. destruct (resultLeq_sound _ _ _ A_leq) as [iv1 [err1 [iv2 [err2 H]]]].
destruct H as [F1 [F2 [sub err_leq]]]. destruct H as [F1 [F2 [sub err_leq]]].
exists iv2, err2, vR, vF, mF; repeat split; auto. exists iv2, err2, vR, vF, mF; repeat split; auto.
assert (err = err1) by congruence; subst. assert (err = err1) by congruence; subst.
......
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