SMTValidation.v 5.05 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135
(**
    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.