Commit de26c52a authored by Joachim Bard's avatar Joachim Bard

implementing coverega checker

parent ebfb8b71
......@@ -2,7 +2,7 @@ From Flover
Require Import Infra.RealSimps Infra.RationalSimps Infra.RealRationalProps
Infra.Ltacs RealRangeArith RealRangeValidator RoundoffErrorValidator
Environments TypeValidator FPRangeValidator ExpressionAbbrevs ResultChecker
IntervalArithQ.
IntervalArithQ Expressions.
(*
From Flover
Require Import Infra.RealRationalProps Environments ExpressionSemantics
......@@ -95,28 +95,6 @@ Proof.
Qed.
(*
Fixpoint merge_subdivs_step (e: expr Q) (acc A1 A2: analysisResult) :=
match FloverMap.find e A1, FloverMap.find e A2 with
| Some (iv1, err1), Some (iv2, err2) =>
let acc1 := FloverMap.add e (unionIntv iv1 iv2, Qmax err1 err2) acc in
match e with
| Unop _ e1 | Downcast _ e1 => merge_subdivs_step e1 acc1 A1 A2
| Binop _ e1 e2 | Let _ _ e1 e2 => let acc2 := merge_subdivs_step e1 acc1 A1 A2 in
merge_subdivs_step e2 acc2 A1 A2
| Fma e1 e2 e3 => let acc2 := merge_subdivs_step e1 acc1 A1 A2 in
let acc3 := merge_subdivs_step e2 acc2 A1 A2 in
merge_subdivs_step e3 acc3 A1 A2
| _ => acc1
end
| _, _ => FloverMap.empty (intv * error)
end.
(* TODO: it might be better to merge all results for one specific expression,
instead of merging 2 results for all expressions *)
Definition merge_subdivs e hd tl : analysisResult :=
fold_left (merge_subdivs_step e (FloverMap.empty (intv * error))) tl hd.
*)
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".
......@@ -160,6 +138,7 @@ Proof.
induction P as [|p P]; auto.
destruct p as [e iv]. destruct e; auto.
Qed.
*)
Fixpoint coverIntv iv intvs :=
match intvs with
......@@ -196,47 +175,108 @@ Proof.
* exists intv. auto.
Qed.
Fixpoint mergeDim x Ps bs :=
Definition addToBucketResb x ivO P :=
match P with
| nil => Fail _ "var not found in precond"
| (e, ivE) :: P =>
match Q_orderedExps.exprCompare e (Var Q x) with
| Eq =>
match ivO with
| Some iv =>
if isSupersetIntv iv ivE then Succes (ivO, Some P) else Succes (Some ivE, None)
| None => Succes (Some ivE, Some P)
end
| _ => Fail _ "var not found in precond"
end
end.
Fixpoint mergeDim x Ps ivO b :=
match Ps with
| nil =>
| nil => match ivO with
| Some iv => Succes ((iv, rev b) :: nil)
| None => Fail _ "no interval for bucket"
end
| P :: Ps =>
match addToBucketResb x ivO P with
| Succes (ivN, Some P') => mergeDim x Ps ivN (P' :: b)
| Succes (ivN, None) => resultBind (mergeDim x Ps ivN nil)
(fun rest => match ivO with
| Some iv => Succes ((iv, rev b) :: rest)
| None => Fail _ "no interval for bucket"
end)
| Fail _ msg | FailDet msg _ => Fail _ msg
end
end.
Fixpoint covers P Ps :=
Lemma mergeDim_sound x Ps ivO iv b Psb res :
mergeDim x Ps ivO b = Succes res ->
In (iv, Psb) res ->
forall P, In P Psb -> exists iv', In ((Var Q x, iv') :: P) Ps /\ isSupersetIntv iv iv' = true.
Proof.
induction Ps.
- cbn; intros H; inversion H.
Abort.
Fixpoint covers (P: list (expr Q * intv)) Ps :=
match P with
| nil => match Ps with nil :: nil => true | _ => false end
| (Var _ x, iv) :: P =>
let (intvs, buckets) := mergeDim x Ps in
forallb (covers P) buckets && coverIntv iv intvs
| _ :: P => covers P Ps
match mergeDim x Ps None nil with
| Succes res =>
let intvs := map fst res in
let buckets := map snd res in
forallb (covers P) buckets && coverIntv iv intvs
| _ => false
end
| _ :: P => false
end.
Lemma in_subdivs_intv (Ps: list precondIntv) E (P: precondIntv) :
checkAllDimensions (FloverMap.elements P) Ps = Succes true ->
P_intv_sound E P ->
exists P', In P' Ps /\ P_intv_sound E P'.
Lemma in_subdivs_intv P Ps E :
covers P Ps = true ->
(forall (x : nat) (iv : intv),
In (Var Q x, iv) P ->
exists vR : R, E x = Some vR /\ (Q2R (fst iv) <= vR <= Q2R (snd iv))%R) ->
exists P', In P' Ps /\
(forall (x : nat) (iv : intv),
In (Var Q x, iv) P' ->
exists vR : R, E x = Some vR /\ (Q2R (fst iv) <= vR <= Q2R (snd iv))%R).
Proof.
intros chk H.
unfold P_intv_sound in H.
induction (FloverMap.elements P).
- cbn in chk. discriminate chk.
induction P as [|[e iv] P] in Ps |- *; intros chk H.
- destruct Ps as [|P' Ps]; cbn in chk; try discriminate chk.
exists P'; split; [now constructor |].
destruct P'; try discriminate chk. auto.
- cbn in chk.
destruct (checkAllDimensionsStep Ps (Succes false) a) eqn:Heq;
try (rewrite ?checkAllDimensionsStep_fail_fp, ?checkAllDimensionsStep_faildet_fp in chk;
discriminate chk).
destruct b.
+ destruct a as [e iv].
destruct e; try discriminate Heq.
cbn in Heq.
admit. (* this might not work *)
+ apply IHl; auto.
intros x iv inl. apply H. now right.
Abort.
destruct e; try discriminate chk.
destruct (mergeDim n Ps None nil) as [res| |] eqn:Hres; try discriminate chk.
apply andb_prop in chk as [rec curr].
destruct (H n iv) as [v [Hf Hc]]; try now constructor.
(* destruct (coverIntv_sound *)
admit.
Admitted.
Definition checkCoverage (subdivs: list precond) (P: precond) :=
let Piv := FloverMap.elements (fst P) in
let Ps := map (fun P => FloverMap.elements (fst P)) subdivs in
covers Piv Ps && true. (* TODO check additional constraints *)
(* TODO: needs more assumptions, i.e. checker for precond *)
Lemma in_subdivs (subdivs: list (precond * analysisResult)) E P :
checkCoverage (map fst subdivs) P = true ->
eval_precond E P ->
exists P' A, In (P', A) subdivs /\ eval_precond E P'.
exists PA, In PA subdivs /\ eval_precond E (fst PA).
Proof.
intros H [Pintv Hadd].
andb_to_prop H.
eapply in_subdivs_intv in L; eauto.
destruct L as [Pl1 [Hin H]].
apply in_map_iff in Hin as [P1 [Heq1 Hin]].
apply in_map_iff in Hin as [PA1 [Heq2 Hin]].
exists PA1. split; auto.
split.
- rewrite Heq2.
now rewrite <- Heq1 in H.
- rewrite Heq2. admit.
Admitted.
(* TODO: check precond sound wrt. subdivs *)
......@@ -245,6 +285,7 @@ Admitted.
Definition SubdivsChecker (e: expr Q) (absenv: analysisResult)
(P: precond) hd tl (defVars: FloverMap.t mType) Gamma :=
validSSA e (preVars P) &&
checkCoverage (map fst (hd :: tl)) P &&
checkSubdivs e absenv (hd :: tl) defVars Gamma.
(**
......@@ -267,11 +308,10 @@ Theorem subdivs_checking_sound (e: expr Q) (absenv: analysisResult) P hd_subdivs
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m ->
(Rabs (vR - vF) <= Q2R err))%R.
Proof.
intros * deltas_matched P_valid valid_typeMap subdivs_valid.
andb_to_prop subdivs_valid.
rename L into valid_ssa.
rename R into valid_subdivs.
apply (in_subdivs (hd_subdivs :: tl_subdivs)) in P_valid as [P' [A [in_subdivs P_valid]]].
intros * deltas_matched P_valid valid_typeMap chk.
apply andb_prop in chk as [chk valid_subdivs].
apply andb_prop in chk as [valid_ssa valid_cover].
apply (in_subdivs (hd_subdivs :: tl_subdivs)) in P_valid as [[P' A] [in_subdivs P_valid]]; auto.
(* preVars P == preVars P' should hold *)
assert (validSSA e (preVars P') = true) as valid_ssa' by admit.
pose proof (checkSubdivs_sound e _ _ _ _ _ _ valid_subdivs in_subdivs) as [range_err_check A_leq].
......
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