Commit 32ed187d authored by Joachim Bard's avatar Joachim Bard

implemented first version of the interval checker

parent 9f02d71b
......@@ -42,6 +42,18 @@ Inductive SMTLogic :=
Definition FalseQ := NotQ TrueQ.
Definition getPrecond q :=
match q with
| AndQ p _ => Some p
| _ => None
end.
Definition getBound q :=
match q with
| AndQ _ (AndQ b _) => Some b
| _ => None
end.
(* TODO: broken (div by 0); remove it *)
Fixpoint evalArith (f: nat -> R) (e: SMTArith) : R :=
match e with
......@@ -111,6 +123,54 @@ Fixpoint SMTArith2Expr (e: SMTArith) : expr Q :=
| DivQ e1 e2 => Binop Div (SMTArith2Expr e1) (SMTArith2Expr e2)
end.
Lemma SMTArith2Expr_exact e : toREval (toRExp (SMTArith2Expr e)) = toRExp (SMTArith2Expr e).
Proof.
induction e; cbn; auto; now rewrite ?IHe, ?IHe1, ?IHe2.
Qed.
Fixpoint smt_expr_eq (e: SMTArith) (e': expr Q) : bool :=
match e, e' with
| ConstQ r, Expressions.Const _ r' => Qeq_bool r r'
| VarQ x, Var _ x' => beq_nat x x'
| UMinusQ e, Unop Neg e' => smt_expr_eq e e'
| PlusQ e1 e2, Binop Plus e1' e2' => (smt_expr_eq e1 e1') && (smt_expr_eq e2 e2')
| MinusQ e1 e2, Binop Sub e1' e2' => (smt_expr_eq e1 e1') && (smt_expr_eq e2 e2')
| TimesQ e1 e2, Binop Mult e1' e2' => (smt_expr_eq e1 e1') && (smt_expr_eq e2 e2')
| DivQ e1 e2, Binop Div e1' e2' => (smt_expr_eq e1 e1') && (smt_expr_eq e2 e2')
| _, _ => false
end.
Lemma smt_expr_eq_sound e : smt_expr_eq e (SMTArith2Expr e) = true.
Proof.
induction e; cbn; auto using Qeq_bool_refl, beq_nat_refl; intuition.
Qed.
Lemma eval_smt_expr_complete e e' :
smt_expr_eq e e' = true -> toREval (toRExp e') = toRExp (SMTArith2Expr e).
Proof.
induction e in e' |- *; destruct e'; cbn; try discriminate.
- intros H. apply Qeq_bool_eq in H. apply Qeq_eqR in H. now rewrite H.
- intros H. apply beq_nat_true in H. now rewrite H.
- destruct u; [intuition | discriminate].
now rewrite (IHe e').
- destruct b; try discriminate.
intros H. apply andb_prop in H as [H1 H2].
rewrite <- (IHe1 e'1); auto.
now rewrite <- (IHe2 e'2).
- destruct b; try discriminate.
intros H. apply andb_prop in H as [H1 H2].
rewrite <- (IHe1 e'1); auto.
now rewrite <- (IHe2 e'2).
- destruct b; try discriminate.
intros H. apply andb_prop in H as [H1 H2].
rewrite <- (IHe1 e'1); auto.
now rewrite <- (IHe2 e'2).
- destruct b; try discriminate.
intros H. apply andb_prop in H as [H1 H2].
rewrite <- (IHe1 e'1); auto.
now rewrite <- (IHe2 e'2).
Qed.
Lemma eval_smt_expr E e v :
eval_smt E e v -> eval_expr E (fun _ => Some REAL) (toRExp (SMTArith2Expr e)) v REAL.
Proof with try (right; apply Rabs_R0).
......
(**
SMT arithmetic checker and its soundness proof.
The function validSMTIntervalbounds checks wether the given analysis result is
a valid range arithmetic for each sub term of the given expression e.
The computation is done using our formalized SMT arithmetic.
The function is used in CertificateChecker.v to build the full checker.
**)
From Coq
Require Import QArith.QArith QArith.Qreals QArith.Qminmax Lists.List
micromega.Psatz.
From Flover
Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
Infra.Ltacs Infra.RealSimps TypeValidator.
From Flover
Require Export SMTArith2 IntervalArithQ ssaPrgs RealRangeArith.
Definition tightenLowerBound (e: expr Q) (lo: Q) (q: SMTLogic) :=
match getBound q with
| Some (LessQ e' (ConstQ v)) => if smt_expr_eq e' e then Qmax lo v else lo
| _ => lo
end.
Definition tightenUpperBound (e: expr Q) (hi: Q) (q: SMTLogic) :=
match getBound q with
| Some (LessQ (ConstQ v) e') => if smt_expr_eq e' e then Qmin hi v else hi
| _ => hi
end.
Definition tightenBounds (e: expr Q) (iv: intv) (qMap: FloverMap.t (SMTLogic * SMTLogic)) :=
match FloverMap.find e qMap with
| None => iv
| Some (loQ, hiQ) => (tightenLowerBound e (ivlo iv) loQ, tightenUpperBound e (ivhi iv) hiQ)
end.
Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: FloverMap.t intv)
(Q: FloverMap.t (SMTLogic * SMTLogic)) (validVars: NatSet.t) : bool:=
match FloverMap.find e A with
| None => false
| Some (intv, _) =>
match e with
| Var _ x =>
if NatSet.mem x validVars
then true
else
match FloverMap.find e P with
| None => false
| Some (lo, hi) => (Qleb lo (ivlo intv)) && (Qleb (ivhi intv) hi)
(* && (Qleb lo hi) *)
end
| Const _ n => (Qleb (ivlo intv) n) && (Qleb n (ivhi intv))
| Unop o f =>
if validSMTIntervalbounds f A P Q validVars
then
match FloverMap.find f A with
| None => false
| Some (iv, _) =>
match o with
| Neg =>
let new_iv := negateIntv iv in
isSupersetIntv new_iv intv
| Inv =>
if (((Qleb (ivhi iv) 0) && (negb (Qeq_bool (ivhi iv) 0))) ||
((Qleb 0 (ivlo iv)) && (negb (Qeq_bool (ivlo iv) 0))))
then
let new_iv := tightenBounds e (invertIntv iv) Q in
isSupersetIntv new_iv intv
else false
end
end
else false
| Binop op f1 f2 =>
if ((validSMTIntervalbounds f1 A P Q validVars)
&& (validSMTIntervalbounds f2 A P Q validVars))
then
match FloverMap.find f1 A, FloverMap.find f2 A with
| Some (iv1, _), Some (iv2, _) =>
match op with
| Plus =>
let new_iv := tightenBounds e (addIntv iv1 iv2) Q in
isSupersetIntv new_iv intv
| Sub =>
let new_iv := tightenBounds e (subtractIntv iv1 iv2) Q in
isSupersetIntv new_iv intv
| Mult =>
let new_iv := tightenBounds e (multIntv iv1 iv2) Q in
isSupersetIntv new_iv intv
| Div =>
if (((Qleb (ivhi iv2) 0) && (negb (Qeq_bool (ivhi iv2) 0))) ||
((Qleb 0 (ivlo iv2)) && (negb (Qeq_bool (ivlo iv2) 0))))
then
let new_iv := tightenBounds e (divideIntv iv1 iv2) Q in
isSupersetIntv new_iv intv
else false
end
| _, _ => false
end
else false
| Fma f1 f2 f3 =>
if ((validSMTIntervalbounds f1 A P Q validVars)
&& (validSMTIntervalbounds f2 A P Q validVars)
&& (validSMTIntervalbounds f3 A P Q validVars))
then
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
isSupersetIntv new_iv intv
| _, _, _ => false
end
else false
| Downcast _ f1 =>
if (validSMTIntervalbounds f1 A P Q validVars)
then
match FloverMap.find f1 A with
| None => false
| Some (iv1, _) =>
(isSupersetIntv intv iv1) && (isSupersetIntv iv1 intv)
end
else
false
end
end.
Theorem validSMTIntervalbounds_sound (f: expr Q) (A: analysisResult) (P: FloverMap.t intv)
(Q: FloverMap.t (SMTLogic * SMTLogic)) fVars dVars (E: env) Gamma :
(forall e loQ hiQ, FloverMap.find e Q = Some (loQ, hiQ) -> ~ eval_smt_logic E loQ /\ ~ eval_smt_logic E hiQ) ->
validSMTIntervalbounds f A P Q dVars = true ->
dVars_range_valid dVars E A ->
NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars ->
eval_precond E P ->
validTypes f Gamma ->
validRanges f A E (toRTMap (toRExpMap Gamma)).
Proof.
Abort.
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