diff --git a/src/analyses/apron/linearTwoVarEqualityAnalysis.apron.ml b/src/analyses/apron/linearTwoVarEqualityAnalysis.apron.ml index 8b38679a09..62f30db64c 100644 --- a/src/analyses/apron/linearTwoVarEqualityAnalysis.apron.ml +++ b/src/analyses/apron/linearTwoVarEqualityAnalysis.apron.ml @@ -14,6 +14,21 @@ let spec_module: (module MCPSpec) Lazy.t = struct include SpecFunctor (Priv) (AD) (RelationPrecCompareUtil.DummyUtil) let name () = "lin2vareq" + let branch ctx e b = + if M.tracing then M.trace "lin2vareq" "Branching"; + let res = branch ctx e b in + let st = ctx.local in + let ask = Analyses.ask_of_ctx ctx in + let _ = assign_from_globals_wrapper ask ctx.global st e (fun d e' -> + try + let tcons = AD.tcons1_of_cil_exp ask d d.env e (not b) (no_overflow ask e) in + let constraintlist = AD.refine_value_domains ctx d tcons in + List.iter (fun e -> ctx.emit (Events.Assert e)) constraintlist; + d + with _ -> d) + in + res + end in (module Spec) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 3a9e2d3e11..4ecb6e92bf 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -244,6 +244,18 @@ module EqualitiesConjunction = struct if M.tracing then M.tracel "meet_with_one_conj" "meet_with_one_conj conj: %s eq: var_%d=%s -> %s " (show (snd ts)) i (Rhs.show (var,offs,divi)) (show (snd res)) ; res + let get_equivalent_expressions econ i = + let ropt,_,_ = get_rhs econ i in + let clusterrefvar = snd @@ BatOption.get ropt in + List.filter (fun (_,(refvaropt,_,_)) -> BatOption.map_default (fun (_,x) -> x = clusterrefvar) true refvaropt) (IntMap.bindings (snd econ)) (* obtain all variables in the equivalence clas *) + + let get_equivalent_expressions econ i = timing_wrap "get_eq_expressions" (get_equivalent_expressions econ) i + + let get_equivalent_expressions econ i = + let res = get_equivalent_expressions econ i in + if M.tracing then M.tracel "equivalencegroup" "get_eq_expressions var_%d : { %s }" i (String.concat ", " @@ List.map (fun (i,rhs) -> Printf.sprintf "var_%d = %s" i (Rhs.show rhs)) res); + res + (** affine transform variable i allover conj with transformer (Some (coeff,i)+offs)/divi *) let affine_transform econ i (coeff, j, offs, divi) = if nontrivial econ i then (* i cannot occur on any other rhs apart from itself *) @@ -698,6 +710,65 @@ struct let substitute_exp ask t var exp no_ov = timing_wrap "substitution" (substitute_exp ask t var exp) no_ov + let refine_value_domains (ctx:('a,'b,'c,'d) Analyses.ctx) t tcons = + match t.d with + | None -> [] + | Some d -> + let constyp = Tcons1.get_typ tcons in + let match_compa = if constyp = SUP then Gt else Ge in + let mkconstraint coff index cst = + let varifo = Option.get @@ V.to_cil_varinfo (Environment.var_of_dim t.env index) in + let ik = Cilfacade.get_ikind (varifo.vtype) in + let lval = Lval (Var varifo, NoOffset) in + let monom = BinOp (Mult,Cil.kintegerCilint ik coff,lval,TInt (ik,[])) in + BinOp (match_compa, monom ,Cil.kintegerCilint ik cst,Cil.intType) + in + match simplified_monomials_from_texp t (Texpr1.to_expr @@ Tcons1.get_texpr1 tcons) with + | None -> [] + | Some (sum_of_terms, (constant,divisor)) ->( + match sum_of_terms,constyp with + | [(coeff, index, divi)], SUP + | [(coeff, index, divi)], SUPEQ -> + + let coeff = Z.(mul coeff divisor) in + let constant = Z.(mul constant divi) in + (* let constant = Z.(if constyp = SUP then sub constant one else constant) in + let constyp = Lincons0.SUPEQ in *) + + (* now we have coeff*var_index + constant SUP(EQ) 0 *) + let opstr =Lincons0.string_of_typ constyp in + M.trace "refinevalues" "Refining due to %d: %s*%s + %s %s 0" index (Z.to_string (coeff)) (Var.to_string @@ Environment.var_of_dim t.env index) (Z.to_string (constant)) opstr; + + (* make var_index = var_index explicit in conlist *) + let conlist = (index,(Some(Z.one,index),Z.zero,Z.one))::EConj.get_equivalent_expressions d index in + let conlist = List.map (fun (var,(rhsrep,rhsoffs,rhsdivi)) -> + let rhscoeff = BatOption.map_default (fst) Z.zero rhsrep in + let zsign z = Z.sign z |> Z.of_int in + let inverse vv tt= + let xx,yy,zz = snd @@ EqualitiesConjunction.inverse vv tt in + BatOption.map_default (fst) Z.zero xx ,yy,zz + in + + (* coeff*var_index + constant SUP(EQ) 0 *) + (* and rhsdivi*var_var - rhsoffs = rhscoeff *var_index*) + (* establish the 2vareq for var_index: *) + let (newcoeff,newoffs,newdivi) = inverse 0(*var_var*) (rhscoeff,0(*var_index*),rhsoffs,rhsdivi) in + if M.tracing then M.trace "refinevalues" "2linvareq: var_%s = (%s*var_%s + %s)/%s" (Var.to_string @@ Environment.var_of_dim t.env index) (Z.to_string newcoeff) (Var.to_string @@ Environment.var_of_dim t.env var) (Z.to_string newoffs) (Z.to_string newdivi); + (* multiply with var_index's old coefficient (i.e. substitute /var_index): *) + let (newcoeff,newoffs,newdivi) = Z.(coeff*newcoeff,coeff*newoffs,newdivi) in + (* and add the constant: *) + let (newcoeff,newoffs,newdivi) = Z.(newcoeff,newoffs+(constant*newdivi),newdivi) in + (* Now get rid of divisor, except for sign: *) + let (newcoeff,newoffs,newdivi) = Z.(newcoeff*abs newdivi,newoffs * abs newdivi,of_int (sign newdivi)) in + (* Do the division, respecting the sign *) + let (newcoeff,newoffs,newdivi) = Z.(zsign newcoeff,(div newoffs (abs newcoeff))+ zsign (rem newoffs (abs newcoeff)),newdivi) in + (* multiply with the divisor, which is only ever 1 or -1 anyway *) + let (newcoeff,newoffs,newdivi) = Z.(newdivi*newcoeff,newoffs*newdivi,one) in + if M.tracing then M.trace "refinevalues" "=> (%s*var_%s +%s) / %s %s 0" (Z.to_string newcoeff) (Var.to_string @@ Environment.var_of_dim t.env var) (Z.to_string newoffs) (Z.to_string newdivi) opstr; + mkconstraint newcoeff var (Z.neg newoffs)) conlist in + M.trace "refinevalues" "Resulting refining assertions %s" (String.concat " ; " (List.map (fun c -> Pretty.sprint ~width:80 (d_exp () c)) conlist)); + conlist + | _ -> [] ) (** Assert a constraint expression. The overflow is completely handled by the flag "no_ov", @@ -729,10 +800,10 @@ struct | _ -> bot_env (* all other results are violating the guard *) end | [(coeff, index, divi)] -> (* guard has a single reference variable only *) - if Tcons1.get_typ tcons = EQ then - meet_with_one_conj t index (Rhs.canonicalize (None, Z.neg @@ Z.(divi*constant),Z.(coeff*divisor))) - else - t (* only EQ is supported in equality based domains *) + begin match Tcons1.get_typ tcons with + | EQ -> meet_with_one_conj t index (Rhs.canonicalize (None, Z.neg @@ Z.(divi*constant),Z.(coeff*divisor))) + | _ -> t (* only EQ is supported in equality based domains *) + end | [(c1,var1,d1); (c2,var2,d2)] -> (* two variables in relation needs a little sorting out *) begin match Tcons1.get_typ tcons with | EQ -> (* c1*var1/d1 + c2*var2/d2 +constant/divisor = 0*) @@ -748,7 +819,6 @@ struct | _ -> t (* For equalities of more then 2 vars we just return t *)) let meet_tcons ask t tcons original_expr no_ov = - if M.tracing then M.tracel "meet_tcons" "meet_tcons with expr: %a no_ov:%b" d_exp original_expr (Lazy.force no_ov); meet_tcons ask t tcons original_expr no_ov let meet_tcons t tcons expr = timing_wrap "meet_tcons" (meet_tcons t tcons) expr @@ -809,6 +879,8 @@ struct let cil_exp_of_lincons1 = Convert.cil_exp_of_lincons1 + let tcons1_of_cil_exp = Convert.tcons1_of_cil_exp + let env t = t.env type marshal = t @@ -819,7 +891,7 @@ struct end -module D2: RelationDomain.RD with type var = Var.t = +module D2 = struct module D = D module ConvArg = struct diff --git a/tests/regression/77-lin2vareq/35-refinement.c b/tests/regression/77-lin2vareq/35-refinement.c new file mode 100644 index 0000000000..1d791d6e4f --- /dev/null +++ b/tests/regression/77-lin2vareq/35-refinement.c @@ -0,0 +1,63 @@ +//SKIP PARAM: --enable ana.int.interval --set ana.activated[+] lin2vareq --set sem.int.signed_overflow assume_none +// initial test for interval-refinement by lin2vareq + +#include + +void main() { + int a; + int b = -7*a+3; + int c = -5*a+5; + int d = 13*a+11; + int e = a; + + if (b < 5){ // a < 1 + + __goblint_check(1 == 1); //SUCCESS + __goblint_check(a > -1); //SUCCESS + __goblint_check(c < 7); //SUCCESS + __goblint_check(d > 8); //SUCCESS + __goblint_check(e > -1); //SUCCESS + + if (a < 1){ + + __goblint_check(1 == 1); //SUCCESS + + // for invariants that solely depend on the reference variable without a factor, we get: + // short node: 2linvar does not know this, we get this from the interval domain + __goblint_check(a == 0); //SUCCESS + __goblint_check(e == 0); //SUCCESS + + // TODO: a==0 is not fed back to 2linvar, + // thus 2linvar can not infer abcde being constant + + // for all the others, we can not infer their constant value + __goblint_check(b > -4); //SUCCESS + __goblint_check(c > 0); //SUCCESS + __goblint_check(d < 24); //SUCCESS + + // in theory, if we knew about a being constant, we could infer the following: + __goblint_check(b == 3); //UNKNOWN + __goblint_check(c == 5); //UNKNOWN + __goblint_check(d ==11); //UNKNOWN + + b=42; + } + + a=69; + } + else { + + __goblint_check(1 == 1); //SUCCESS + __goblint_check(a <=-1); //SUCCESS + __goblint_check(a <=-1); //SUCCESS + __goblint_check(c >= 7); //SUCCESS + __goblint_check(d <= 8); //SUCCESS + __goblint_check(e <=-1); //SUCCESS + + a = 6; + } + // + //if (a<1) { + //// __goblint_assert(b<5); //SUCCESS + //} +} \ No newline at end of file