Commit d4df3d07 authored by Joachim Bard's avatar Joachim Bard
Browse files

adding some comments and removing unneeded stuff

parent 1f194f2e
......@@ -11,6 +11,7 @@ Require Import Flover.RealRangeArith.
Open Scope R.
(* Restricted functions: cast, fma, and let are disallowed *)
Inductive SMTArith :=
| ConstQ (r: Q) : SMTArith
| VarQ (x: nat) : SMTArith
......@@ -20,7 +21,7 @@ Inductive SMTArith :=
| TimesQ (e1 e2: SMTArith) : SMTArith
| DivQ (e1 e2: SMTArith) : SMTArith.
(* comparisons of restricted functions, as well as usual boolean connectives *)
Inductive SMTLogic :=
| LessQ (e1 e2: SMTArith) : SMTLogic
| LessEqQ (e1 e2: SMTArith) : SMTLogic
......@@ -44,6 +45,7 @@ Definition getBound q :=
| _ => None
end.
(* semantics for restricted functions *)
Inductive eval_smt (E: env) : SMTArith -> R -> Prop :=
| VarQ_load x v : E x = Some v -> eval_smt E (VarQ x) v
| ConstQ_eval r : eval_smt E (ConstQ r) (Q2R r)
......@@ -57,6 +59,7 @@ Inductive eval_smt (E: env) : SMTArith -> R -> Prop :=
| DivQ_eval e1 e2 v1 v2 :
v2 <> 0 -> eval_smt E e1 v1 -> eval_smt E e2 v2 -> eval_smt E (DivQ e1 e2) (v1 / v2).
(* semantics for SMT-statements *)
Fixpoint eval_smt_logic (E: env) (q: SMTLogic) : Prop :=
match q with
| LessQ e1 e2 => exists v1 v2, eval_smt E e1 v1 /\ eval_smt E e2 v2 /\ v1 < v2
......@@ -183,7 +186,8 @@ Proof.
induction e; cbn; auto; now rewrite ?IHe, ?IHe1, ?IHe2.
Qed.
(* TODO handle Let and Cond *)
(* comparison of functions and restricted functions as given above *)
(* let's are handled separately *)
Fixpoint smt_expr_eq (e: SMTArith) (e': expr Q) : bool :=
match e', e with
| Expressions.Const _ r', ConstQ r => Qeq_bool r r'
......@@ -458,6 +462,7 @@ Definition addVarConstraint (el: expr Q * intv) q :=
| _ => q
end.
(* a precondition can be transformed into and equivalent SMT-statement *)
Definition precond2SMT (P: precond) :=
List.fold_right addVarConstraint (snd P) (FloverMap.elements (fst P)).
......@@ -501,62 +506,10 @@ Proof.
cbn in H. tauto.
Qed.
(* checker for precondition *)
(* not needed
Fixpoint checkPrelist (lP: list (FloverMap.key * intv)) C q : bool :=
match lP, q with
| List.nil, _ => SMTLogic_eqb C q
| List.cons (Var _ x, (lo, hi)) lP', AndQ (LessEqQ (ConstQ lo') (VarQ y)) (AndQ (LessEqQ (VarQ z) (ConstQ hi')) q') => (x =? y) && (x =? z) && Qeq_bool lo lo' && Qeq_bool hi hi' && checkPrelist lP' C q'
| List.cons (Var _ x, _) _, _ => false
| List.cons el lP', _ => checkPrelist lP' C q
end.
*)
(*
Lemma checkPrelist_LessQ lP C e1 e2 : checkPrelist lP C (LessQ e1 e2) = false.
Proof.
induction lP as [|[e [lo hi]] l IHl]; auto.
destruct e; auto.
Qed.
Lemma checkPrelist_LessEqQ lP e1 e2 : checkPrelist lP (LessEqQ e1 e2) = false.
Proof.
induction lP as [|[e [lo hi]] l IHl]; auto.
destruct e; auto.
Qed.
Lemma checkPrelist_EqualsQ lP e1 e2 : checkPrelist lP (EqualsQ e1 e2) = false.
Proof.
induction lP as [|[e [lo hi]] l IHl]; auto.
destruct e; auto.
Qed.
Lemma checkPrelist_NotQ lP q : checkPrelist lP (NotQ q) = false.
Proof.
induction lP as [|[e [lo hi]] l IHl]; auto.
destruct e; auto.
Qed.
Lemma checkPrelist_OrQ lP q1 q2 : checkPrelist lP (OrQ q1 q2) = false.
Proof.
induction lP as [|[e [lo hi]] l IHl]; auto.
destruct e; auto.
Qed.
*)
(* Definition checkPre (P: precond) q := checkPrelist (FloverMap.elements (fst P)) (snd P) q. *)
Definition checkPre (P: precond) q := SMTLogic_eqb (precond2SMT P) q.
Lemma checkPre_precond P : checkPre P (precond2SMT P) = true.
Proof.
(*
unfold precond2SMT, checkPre.
destruct P as [Piv C]. cbn.
induction (FloverMap.elements Piv) as [|[e [lo hi]] l IHl]; cbn.
- apply SMTLogic_eqb_refl.
- destruct e; cbn; auto.
now rewrite Nat.eqb_refl, !Qeq_bool_refl, IHl.
*)
unfold checkPre. apply SMTLogic_eqb_refl.
Qed.
......@@ -569,39 +522,6 @@ Proof.
apply (SMTLogic_eqb_sound _ _ _ Heq).
now apply pre_to_smt_correct.
Qed.
(*
Proof with try discriminate.
unfold checkPre, eval_precond, eval_preIntv.
destruct P as [Piv C]. cbn.
induction (FloverMap.elements Piv) as [|[e [lo hi]] l IHl] in q |- *.
- cbn. intros Heq [_ H]. now apply (SMTLogic_eqb_sound _ C).
- destruct e as [x| | | | | |].
all: try now (cbn; intros Heq [H1 H2]; apply IHl; auto).
cbn.
destruct q as [? ?|? ?|? ?| |?|q1 q2|? ?]...
destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
destruct e1 as [r| | | | | |]... destruct e2 as [|y| | | | |]...
destruct q2 as [? ?|? ?|? ?| |?|q1 q2|? ?]...
destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
destruct e1 as [|z| | | | |]... destruct e2 as [r'| | | | | |]...
intros chk [H HC].
apply andb_prop in chk as [chk chk0].
apply andb_prop in chk as [chk chk1].
apply andb_prop in chk as [chk chk2].
apply andb_prop in chk as [chk4 chk3].
apply beq_nat_true in chk4. apply beq_nat_true in chk3.
apply Qeq_bool_eq in chk2. apply Qeq_bool_eq in chk1.
rewrite <- chk3, <- chk4.
apply Qeq_sym in chk2. apply Qeq_sym in chk1.
(* assert (x fVars) as fx by (subst; set_tac; set_tac). *)
repeat split.
+ destruct (H x (lo, hi)) as [v [H0 [H1 H2]]]; cbn; auto.
exists (Q2R r), v. repeat split; try now constructor. erewrite Qeq_eqR; now eauto.
+ destruct (H x (lo, hi)) as [v [H0 [H1 H2]]]; cbn; auto.
exists v, (Q2R r'). repeat split; try now constructor. erewrite Qeq_eqR; now eauto.
+ apply IHl; auto.
Qed.
*)
Lemma checkPre_smt_pre E P q :
checkPre P q = true ->
......@@ -612,40 +532,6 @@ Proof.
apply smt_to_pre_correct.
now apply (SMTLogic_eqb_sound _ _ _ Heq).
Qed.
(*
Proof with try discriminate.
unfold P_intv_sound, checkPre.
induction (FloverMap.elements P) as [|[e [lo hi]] l IHl] in q |- *.
- destruct q; cbn; intros chk; try discriminate. tauto.
- destruct e as [x| | | | |];
try (intros chk H ? ? [?|?]; [discriminate| apply (IHl _ chk); auto]).
destruct q as [? ?|? ?|? ?| |?|q1 q2|? ?]...
destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
destruct e1 as [r| | | | | |]... destruct e2 as [|y| | | | |]...
destruct q2 as [? ?|? ?|? ?| |?|q1 q2|? ?]...
destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
destruct e1 as [|z| | | | |]... destruct e2 as [r'| | | | | |]...
cbn. intros chk H x' [lo' hi'] [eq|inl].
+ apply andb_prop in chk. destruct chk as [chk chk0].
apply andb_prop in chk. destruct chk as [chk chk1].
apply andb_prop in chk. destruct chk as [chk chk2].
apply andb_prop in chk. destruct chk as [chk4 chk3].
apply beq_nat_true in chk4. apply beq_nat_true in chk3.
apply Qeq_bool_eq in chk2. apply Qeq_bool_eq in chk1.
destruct H as [[v1 [v2 [H1 [H2 H3]]]] [[v1' [v2' [H1' [H2' H3']]]] H]].
symmetry in chk4. symmetry in chk3.
assert (x' = x) by congruence.
assert (lo' = lo) by congruence.
assert (hi' = hi) by congruence.
subst.
inversion H1. inversion H2. inversion H1'. inversion H2'.
assert (v2 = v1') by congruence.
subst. cbn. rewrite (Qeq_eqR _ _ chk2). rewrite (Qeq_eqR _ _ chk1).
exists v1'. repeat split; auto.
+ apply andb_prop in chk. destruct chk as [chk chk0].
apply (IHl _ chk0); tauto.
Qed.
*)
Lemma precond_bound_correct E P preQ bound :
eval_precond E P ->
......
......@@ -43,6 +43,7 @@ Fixpoint inlineLets (L: let_env) (e: expr Q) :=
(* | Cond e1 e2 e3 => Cond (inlineLets L e1) (inlineLets L e2) (inlineLets L e3) *)
end.
(* inlineLets preserves evaluation for reasonable let_env *)
Lemma inlineLets_sound L E Gamma inVars outVars e v :
lets_sound L E Gamma ->
(forall x e, L x = Some e -> NatSet.Subset (NatSet.add x (freeVars e)) inVars) ->
......@@ -112,19 +113,6 @@ Proof.
apply H4. eapply LfVars_valid; eauto.
set_tac. }
* now extended_ssa.
(*
- inversion H; subst.
+ assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
inversion ssa_e; subst.
subst.
assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst. eapply Cond_then; eauto.
+ assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
inversion ssa_e; subst.
subst.
assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst. eapply Cond_else; eauto.
*)
Qed.
Definition tightenLowerBound (e: expr Q) (lo: Q) (q: SMTLogic) P L :=
......@@ -141,6 +129,7 @@ Definition tightenUpperBound (e: expr Q) (hi: Q) (q: SMTLogic) P L :=
| _ => hi
end.
(* try to tighten the given interval using correct encoded queries *)
Definition tightenBounds (e: expr Q) (iv: intv) (qMap: usedQueries) P L :=
match FloverMap.find e qMap with
| None => iv
......@@ -220,6 +209,8 @@ Proof.
intros. edestruct unsatQ; eauto.
Qed.
(* the final validator is essentially the interval arithmetic validator,
except that in each step 'tightenBounds' is applied *)
Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: precond)
(Q: usedQueries) L (validVars: NatSet.t) : bool :=
match FloverMap.find e A with
......@@ -336,6 +327,8 @@ Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: precond)
end
end.
(* soundness proof is essnetially the same as the one for interval arithmetic,
except in each step 'tightenBounds_sound' is applied *)
Theorem validSMTIntervalbounds_sound (f: expr Q) (A: analysisResult) (P: precond)
(Q: usedQueries) L fVars dVars outVars (E: env) Gamma :
unsat_queries Q ->
......
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