diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index 4a6b266c25..72b91d71b7 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -388,11 +388,11 @@ struct
let st = ctx.local in
let reachable_from_args = reachable_from_args ctx args in
let fundec = Node.find_fundec ctx.node in
- if M.tracing then M.tracel "combine" "relation f: %a" CilType.Varinfo.pretty f.svar;
- if M.tracing then M.tracel "combine" "relation formals: %a" (d_list "," CilType.Varinfo.pretty) f.sformals;
- if M.tracing then M.tracel "combine" "relation args: %a" (d_list "," d_exp) args;
- if M.tracing then M.tracel "combine" "relation st: %a" D.pretty st;
- if M.tracing then M.tracel "combine" "relation fun_st: %a" D.pretty fun_st;
+ if M.tracing then M.tracel "combine-rel" "relation f: %a" CilType.Varinfo.pretty f.svar;
+ if M.tracing then M.tracel "combine-rel" "relation formals: %a" (d_list "," CilType.Varinfo.pretty) f.sformals;
+ if M.tracing then M.tracel "combine-rel" "relation args: %a" (d_list "," d_exp) args;
+ if M.tracing then M.tracel "combine-rel" "relation st: %a" D.pretty st;
+ if M.tracing then M.tracel "combine-rel" "relation fun_st: %a" D.pretty fun_st;
let new_fun_rel = RD.add_vars fun_st.rel (RD.vars st.rel) in
let arg_substitutes =
let filter_actuals (x,e) =
@@ -418,7 +418,7 @@ struct
in
let any_local_reachable = any_local_reachable fundec reachable_from_args in
let arg_vars = f.sformals |> List.filter (RD.Tracked.varinfo_tracked) |> List.map RV.arg in
- if M.tracing then M.tracel "combine" "relation remove vars: %a" (docList (fun v -> Pretty.text (Apron.Var.to_string v))) arg_vars;
+ if M.tracing then M.tracel "combine-rel" "relation remove vars: %a" (docList (fun v -> Pretty.text (Apron.Var.to_string v))) arg_vars;
RD.remove_vars_with new_fun_rel arg_vars; (* fine to remove arg vars that also exist in caller because unify from new_rel adds them back with proper constraints *)
let tainted = f_ask.f Queries.MayBeTainted in
let tainted_vars = TaintPartialContexts.conv_varset tainted in
@@ -432,7 +432,7 @@ struct
)
in
let unify_rel = RD.unify new_rel new_fun_rel in (* TODO: unify_with *)
- if M.tracing then M.tracel "combine" "relation unifying %a %a = %a" RD.pretty new_rel RD.pretty new_fun_rel RD.pretty unify_rel;
+ if M.tracing then M.tracel "combine-rel" "relation unifying %a %a = %a" RD.pretty new_rel RD.pretty new_fun_rel RD.pretty unify_rel;
{fun_st with rel = unify_rel}
let combine_assign ctx r fe f args fc fun_st (f_ask : Queries.ask) =
diff --git a/src/cdomains/apron/gobApron.apron.ml b/src/cdomains/apron/gobApron.apron.ml
index c39a3e42db..e202a88c60 100644
--- a/src/cdomains/apron/gobApron.apron.ml
+++ b/src/cdomains/apron/gobApron.apron.ml
@@ -1,6 +1,13 @@
open Batteries
include Apron
+module Coeff =
+struct
+ include Coeff
+
+ let s_of_z z = Coeff.s_of_mpqf (Mpqf.of_mpz (Z_mlgmpidl.mpz_of_z z))
+end
+
module Var =
struct
include Var
diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
index 67bd67f4e5..069983344e 100644
--- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
+++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
@@ -17,15 +17,38 @@ open VectorMatrix
module Mpqf = SharedFunctions.Mpqf
module Rhs = struct
- (* (Some i, k) represents a sum of a variable with index i and the number k.
- (None, k) represents the number k. *)
- type t = (int option * GobZ.t) [@@deriving eq, ord, hash]
- let var_zero i = (Some i, Z.zero)
- let show_formatted formatter = function
- | (Some v, o) when Z.equal o Z.zero -> formatter v
- | (Some v, o) -> Printf.sprintf "%s%+Ld" (formatter v) (Z.to_int64 o)
- | (None, o) -> Printf.sprintf "%Ld" (Z.to_int64 o)
- let show rhs = show_formatted (Printf.sprintf "var_%d") rhs
+ (* Rhs represents coefficient*var_i + offset / divisor
+ depending on whether coefficient is 0, the monomial term may disappear completely, not refering to any var_i, thus:
+ (Some (coefficient, i), offset, divisor ) with coefficient != 0 , or
+ (None , offset, divisor ) *)
+ type t = ((GobZ.t * int) option * GobZ.t * GobZ.t) [@@deriving eq, ord, hash]
+ let var_zero i = (Some (Z.one,i), Z.zero, Z.one)
+ let show_coeff c =
+ if Z.equal c Z.one then ""
+ else if Z.equal c Z.minus_one then "-"
+ else (Z.to_string c) ^"·"
+ let show_rhs_formatted formatter = let ztostring n = (if Z.(geq n zero) then "+" else "") ^ Z.to_string n in
+ function
+ | (Some (coeff,v), o,_) when Z.equal o Z.zero -> Printf.sprintf "%s%s" (show_coeff coeff) (formatter v)
+ | (Some (coeff,v), o,_) -> Printf.sprintf "%s%s %s" (show_coeff coeff) (formatter v) (ztostring o)
+ | (None, o,_) -> Printf.sprintf "%s" (Z.to_string o)
+ let show (v,o,d) =
+ let rhs=show_rhs_formatted (Printf.sprintf "var_%d") (v,o,d) in
+ if not (Z.equal d Z.one) then "(" ^ rhs ^ ")/" ^ (Z.to_string d) else rhs
+
+ (** factor out gcd from all terms, i.e. ax=by+c with a positive is the canonical form for adx+bdy+cd *)
+ let canonicalize (v,o,d) =
+ let gcd = Z.gcd o d in (* gcd of coefficients *)
+ let gcd = Option.map_default (fun (c,_) -> Z.gcd c gcd) gcd v in (* include monomial in gcd computation *)
+ let commondivisor = if Z.(lt d zero) then Z.neg gcd else gcd in (* canonical form dictates d being positive *)
+ (BatOption.map (fun (coeff,i) -> (Z.div coeff commondivisor,i)) v, Z.div o commondivisor, Z.div d commondivisor)
+
+ (** Substitute rhs for varx in rhs' *)
+ let subst rhs varx rhs' =
+ match rhs,rhs' with
+ | (monom, o, d), (Some (c', x'), o', d') when x'=varx -> canonicalize (Option.map (fun (c,x) -> (Z.mul c c',x)) monom, Z.((o*c')+(d*o')), Z.mul d d')
+ | _ -> rhs'
+
end
module EqualitiesConjunction = struct
@@ -36,7 +59,7 @@ module EqualitiesConjunction = struct
let show_formatted formatter econ =
if IntMap.is_empty econ then "{}"
else
- let str = IntMap.fold (fun i (refvar,off) acc -> Printf.sprintf "%s=%s ∧ %s" (formatter i) (Rhs.show_formatted formatter (refvar,off)) acc) econ "" in
+ let str = IntMap.fold (fun i (refmonom,off,divi) acc -> Printf.sprintf "%s%s=%s ∧ %s" (Rhs.show_coeff divi) (formatter i) (Rhs.show_rhs_formatted formatter (refmonom,off,divi)) acc) econ "" in
"{" ^ String.sub str 0 (String.length str - 4) ^ "}"
let show econ = show_formatted (Printf.sprintf "var_%d") econ
@@ -52,16 +75,23 @@ module EqualitiesConjunction = struct
(** trivial equalities are of the form var_i = var_i and are not kept explicitely in the sparse representation of EquanlitiesConjunction *)
let nontrivial (_,econmap) lhs = IntMap.mem lhs econmap
+ (** turn x = (cy+o)/d into y = (dx-o)/c*)
+ let inverse x (c,y,o,d) = (y, (Some (d, x), Z.neg o, c))
+
(** sparse implementation of get rhs for lhs, but will default to no mapping for sparse entries *)
let get_rhs (_,econmap) lhs = IntMap.find_default (Rhs.var_zero lhs) lhs econmap
- (** set_rhs, staying loyal to immutable, sparse map underneath *)
+ (** set_rhs, staying loyal to immutable, sparse map underneath; do not attempt any normalization *)
let set_rhs (dim,map) lhs rhs = (dim,
if Rhs.equal rhs Rhs.(var_zero lhs) then
IntMap.remove lhs map
else
IntMap.add lhs rhs map
)
+
+ (** canonicalize equation, and set_rhs, staying loyal to immutable, sparse map underneath *)
+ let canonicalize_and_set (dim,map) lhs rhs = set_rhs (dim,map) lhs (Rhs.canonicalize rhs)
+
let copy = identity
@@ -86,9 +116,10 @@ module EqualitiesConjunction = struct
IntHashtbl.add h x r;
r)
in
- let rec bumpentry k (refvar,offset) = function (* directly bumps lhs-variable during a run through indexes, bumping refvar explicitely with a new lookup in indexes *)
- | (tbl,delta,head::rest) when k>=head -> bumpentry k (refvar,offset) (tbl,delta+1,rest) (* rec call even when =, in order to correctly interpret double bumps *)
- | (tbl,delta,lyst) (* k (IntMap.add (op k delta) (BatOption.map (memobumpvar) refvar, offset) tbl, delta, lyst)
+ let rec bumpentry k (refvar,offset,divi) = function (* directly bumps lhs-variable during a run through indexes, bumping refvar explicitly with a new lookup in indexes *)
+
+ | (tbl,delta,head::rest) when k>=head -> bumpentry k (refvar,offset,divi) (tbl,delta+1,rest) (* rec call even when =, in order to correctly interpret double bumps *)
+ | (tbl,delta,lyst) (* k (IntMap.add (op k delta) (BatOption.map (fun (c,v) -> (c,memobumpvar v)) refvar,offset,divi) tbl, delta, lyst)
in
let (a,_,_) = IntMap.fold bumpentry map (IntMap.empty,0,offsetlist) in (* Build new map during fold with bumped key/vals *)
(op dim (Array.length indexes), a)
@@ -111,17 +142,28 @@ module EqualitiesConjunction = struct
(* Forget information about variable i *)
let forget_variable d var =
let res =
- (let ref_var_opt = fst (get_rhs d var) in
+ (let ref_var_opt = Tuple3.first (get_rhs d var) in
match ref_var_opt with
- | Some ref_var when ref_var = var ->
+ | Some (_,ref_var) when ref_var = var ->
+ if M.tracing then M.trace "forget" "headvar var_%d" var;
(* var is the reference variable of its connected component *)
- (let cluster = IntMap.fold
- (fun i (ref, offset) l -> if ref = ref_var_opt then i::l else l) (snd d) [] in
+ (let cluster = List.sort (Int.compare) @@ IntMap.fold
+ (fun i (refe,_,_) l -> BatOption.map_default (fun (coeff,refe) -> if (refe=ref_var) then i::l else l) l refe) (snd d) [] in
+ if M.tracing then M.trace "forget" "cluster varindices: [%s]" (String.concat ", " (List.map (string_of_int) cluster));
(* obtain cluster with common reference variable ref_var*)
match cluster with (* new ref_var is taken from head of the cluster *)
- | head :: tail ->
- let headconst = snd (get_rhs d head) in (* take offset between old and new reference variable *)
- List.fold (fun map i -> set_rhs map i Z.(Some head, snd (get_rhs d i) - headconst)) d cluster (* shift offset to match new reference variable *)
+ | head :: clusterrest ->
+ (* head: divi*x = coeff*y + offs *)
+ (* divi*x = coeff*y + offs =inverse=> y =( divi*x - offs)/coeff *)
+ let (newref,offs,divi) = (get_rhs d head) in
+ let (coeff,y) = BatOption.get newref in
+ let (y,yrhs) = inverse head (coeff,y,offs,divi) in (* reassemble yrhs out of components *)
+ let shifted_cluster = (List.fold (fun map i ->
+ let irhs = (get_rhs d i) in (* old entry is i = irhs *)
+ Rhs.subst yrhs y irhs |> (* new entry for i is irhs [yrhs/y] *)
+ set_rhs map i
+ ) d clusterrest) in
+ set_rhs shifted_cluster head (Rhs.var_zero head) (* finally make sure that head is now trivial *)
| [] -> d) (* empty cluster means no work for us *)
| _ -> d) (* variable is either a constant or expressed by another refvar *) in
let res = (fst res, IntMap.remove var (snd res)) in (* set d(var) to unknown, finally *)
@@ -153,31 +195,68 @@ module EqualitiesConjunction = struct
exception Contradiction
- let meet_with_one_conj ts i (var, b) =
+ let meet_with_one_conj ts i (var, offs, divi) =
+ let (var,offs,divi) = Rhs.canonicalize (var,offs,divi) in (* make sure that the one new conj is properly canonicalized *)
let res =
- let subst_var tsi x (vart, bt) =
+ let subst_var (dim,econj) x (vary, o, d) =
+ (* [[x substby (cy+o)/d ]] ((c'x+o')/d') *)
+ (* =====> (c'cy + c'o+o'd)/(dd') *)
let adjust = function
- | (Some vare, b') when vare = x -> (vart, Z.(b' + bt))
+ | (Some (c',varx), o',d') when varx = x ->
+ let open Z in Rhs.canonicalize (BatOption.map (fun (c, y)-> (c * c', y)) vary, c'*o + o'*d, d'*d)
| e -> e
in
- (fst tsi, IntMap.add x (vart, bt) @@ IntMap.map adjust (snd tsi)) (* in case of sparse representation, make sure that the equality is now included in the conjunction *)
+ (dim, IntMap.add x (vary, o, d) @@ IntMap.map adjust econj) (* in case of sparse representation, make sure that the equality is now included in the conjunction *)
in
- let (var1, b1) = get_rhs ts i in
- (match var, var1 with
- | None , None -> if not @@ Z.equal b b1 then raise Contradiction else ts
- | None , Some h1 -> subst_var ts h1 (None, Z.(b - b1))
- | Some j, None -> subst_var ts j (None, Z.(b1 - b))
- | Some j, Some h1 ->
+ (match var, (get_rhs ts i) with
+ (*| new conj , old conj *)
+ | None , (None , o1, divi1) -> if not @@ (Z.equal offs o1 && Z.equal divi divi1) then raise Contradiction else ts
+ (* o/d = x_i = (c1*x_h1+o1)/d1 *)
+ (* ======> x_h1 = (o*d1-o1*d)/(d*c1) /\ x_i = o/d *)
+ | None , (Some (coeff1,h1), o1, divi1) -> subst_var ts h1 (None, Z.(offs*divi1 - o1*divi),Z.(divi*coeff1))
+ (* (c*x_j+o)/d = x_i = o1/d1 *)
+ (* ======> x_j = (o1*d-o*d1)/(d1*c) /\ x_i = o1/d1 *)
+ | Some (coeff,j), (None , o1, divi1) -> subst_var ts j (None, Z.(o1*divi - offs*divi1),Z.(divi1*coeff))
+ (* (c*x_j+o)/d = x_i = (c1*x_h1+o1)/d1 *)
+ (* ======> x_j needs normalization wrt. ts *)
+ | Some (coeff,j), ((Some (coeff1,h1), o1, divi1) as oldi)->
(match get_rhs ts j with
- | (None, b2) -> subst_var ts i (None, Z.(b2 + b))
- | (Some h2, b2) ->
- if h1 = h2 then
- (if not @@ Z.equal b1 Z.(b2 + b) then raise Contradiction else ts)
- else if h1 < h2 then subst_var ts h2 (Some h1, Z.(b1 - (b + b2)))
- else subst_var ts h1 (Some h2, Z.(b + (b2 - b1))))) in
- if M.tracing then M.trace "meet" "meet_with_one_conj conj: { %s } eq: var_%d=%s -> { %s } " (show (snd ts)) i (Rhs.show (var,b)) (show (snd ts))
+ (* ts[x_j]=o2/d2 ========> ... *)
+ | (None , o2, divi2) ->
+ let newxi = Rhs.subst (None,o2,divi2) j (Some (coeff,j),offs,divi) in
+ let newxh1 = snd @@ inverse i (coeff1,h1,o1,divi1) in
+ let newxh1 = Rhs.subst newxi i newxh1 in
+ subst_var ts h1 newxh1
+ (* ts[x_j]=(c2*x_h2+o2)/d2 ========> ... *)
+ | (Some (coeff2,h2), o2, divi2) as normalizedj ->
+ if h1 = h2 then (* this is the case where x_i and x_j already where in the same equivalence class; let's see whether the new equality contradicts the old one *)
+ let normalizedi= Rhs.subst normalizedj j (Some(coeff,j),offs,divi) in
+ if not @@ Rhs.equal normalizedi oldi then raise Contradiction else ts
+ else if h1 < h2 (* good, we now unite the two equvalence classes; let's decide upon the representative *)
+ then (* express h2 in terms of h1: *)
+ let (_,newh2)= inverse j (coeff2,h2,o2,divi2) in
+ let newh2 = Rhs.subst oldi i (Rhs.subst (snd @@ inverse i (coeff,j,offs,divi)) j newh2) in
+ subst_var ts h2 newh2
+ else (* express h1 in terms of h2: *)
+ let (_,newh1)= inverse i (coeff1,h1,o1,divi1) in
+ let newh1 = Rhs.subst normalizedj j (Rhs.subst (Some(coeff,j),offs,divi) i newh1) in
+ subst_var ts h1 newh1)) in
+ 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
+ (** 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 *)
+ set_rhs econ i (Rhs.subst (get_rhs econ i) i (Some (coeff,j), offs, divi))
+ else (* var_i = var_i, i.e. it may occur on the rhs of other equalities *)
+ (* so now, we transform with the inverse of the transformer: *)
+ let inv = snd (inverse i (coeff,j,offs,divi)) in
+ IntMap.fold (fun k v acc ->
+ match v with
+ | (Some (c,x),o,d) when x=i-> set_rhs acc k (Rhs.subst inv i v)
+ | _ -> acc
+ ) (snd econ) econ
+
end
(** [VarManagement] defines the type t of the affine equality domain (a record that contains an optional matrix and an apron environment) and provides the functions needed for handling variables (which are defined by [RelationDomain.D2]) such as [add_vars], [remove_vars].
@@ -195,32 +274,32 @@ struct
let open Apron.Texpr1 in
let exception NotLinearExpr in
let exception ScalarIsInfinity in
- let negate coeff_var_list = List.map (fun (coeff, var) -> (Z.(-coeff), var)) coeff_var_list in
- let multiply_with_Z number coeff_var_list =
- List.map (fun (coeff, var) -> (Z.(number * coeff, var))) coeff_var_list in
+ let negate coeff_var_list =
+ List.map (fun (monom, offs, divi) -> Z.(BatOption.map (fun (coeff,i) -> (neg coeff, i)) monom, neg offs, divi)) coeff_var_list in
+ let multiply_with_Q dividend divisor coeff_var_list =
+ List.map (fun (monom, offs, divi) -> Rhs.canonicalize Z.(BatOption.map (fun (coeff,i) -> (dividend*coeff,i)) monom, dividend*offs, divi*divisor) ) coeff_var_list in
let multiply a b =
(* if one of them is a constant, then multiply. Otherwise, the expression is not linear *)
match a, b with
- | [(a_coeff, None)], b -> multiply_with_Z a_coeff b
- | a, [(b_coeff, None)] -> multiply_with_Z b_coeff a
+ | [(None,coeff, divi)], c
+ | c, [(None,coeff, divi)] -> multiply_with_Q coeff divi c
| _ -> raise NotLinearExpr
in
let rec convert_texpr texp =
begin match texp with
- (* If x is a constant, replace it with its const. val. immediately *)
| Cst (Interval _) -> failwith "constant was an interval; this is not supported"
| Cst (Scalar x) ->
begin match SharedFunctions.int_of_scalar ?round:None x with
- | Some x -> [(x, None)]
+ | Some x -> [(None,x,Z.one)]
| None -> raise ScalarIsInfinity end
| Var x ->
let var_dim = Environment.dim_of_var t.env x in
begin match t.d with
- | None -> [(Z.one, Some var_dim)]
+ | None -> [(Some (Z.one,var_dim),Z.zero,Z.one)]
| Some d ->
(match (EConj.get_rhs d var_dim) with
- | (Some i, k) -> [(Z.one, Some i); (k, None)]
- | (None, k) -> [(k, None)])
+ | (Some (coeff,i), k,divi) -> [(Some (coeff,i),Z.zero,divi); (None,k,divi)]
+ | (None, k,divi) -> [ (None,k,divi)])
end
| Unop (Neg, e, _, _) -> negate (convert_texpr e)
| Unop (Cast, e, _, _) -> convert_texpr e (* Ignore since casts in apron are used for floating point nums and rounding in contrast to CIL casts *)
@@ -234,59 +313,41 @@ struct
| exception ScalarIsInfinity -> None
| x -> Some(x)
- (** convert and simplify (wrt. reference variables) a texpr into a tuple of a list of monomials and a constant *)
- let simplified_monomials_from_texp (t: t) texp =
+ (** convert and simplify (wrt. reference variables) a texpr into a tuple of a list of monomials (coeff,varidx,divi) and a (constant/divi) *)
+ let simplified_monomials_from_texp (t: t) texp =
BatOption.bind (monomials_from_texp t texp)
(fun monomiallist ->
let d = Option.get t.d in
- let expr = Array.make (Environment.size t.env) Z.zero in
- let accumulate_constants a (c, v) = match v with
- | None -> Z.(a + c)
- | Some idx -> let (term,con) = (EConj.get_rhs d idx) in
- (Option.may (fun ter -> expr.(ter) <- Z.(expr.(ter) + c)) term;
- Z.(a + c * con))
+ let module IMap = EConj.IntMap in
+ let accumulate_constants (exprcache,(aconst,adiv)) (v,offs,divi) = match v with
+ | None -> let gcdee = Z.gcd adiv divi in exprcache,(Z.(aconst*divi/gcdee + offs*adiv/gcdee),Z.lcm adiv divi)
+ | Some (coeff,idx) -> let (somevar,someoffs,somedivi)=Rhs.subst (EConj.get_rhs d idx) idx (v,offs,divi) in (* normalize! *)
+ let newcache = Option.map_default (fun (coef,ter) -> IMap.add ter Q.((IMap.find_default zero ter exprcache) + make coef somedivi) exprcache) exprcache somevar in
+ let gcdee = Z.gcd adiv divi in
+ (newcache,(Z.(aconst*divi/gcdee + offs*adiv/gcdee),Z.lcm adiv divi))
in
- let constant = List.fold_left accumulate_constants Z.zero monomiallist in (* abstract simplification of the guard wrt. reference variables *)
- Some (Array.fold_lefti (fun list v (c) -> if Z.equal c Z.zero then list else (c,v)::list) [] expr, constant) )
+ let (expr,constant) = List.fold_left accumulate_constants (IMap.empty,(Z.zero,Z.one)) monomiallist in (* abstract simplification of the guard wrt. reference variables *)
+ Some (IMap.fold (fun v c acc -> if Q.equal c Q.zero then acc else (Q.num c,v,Q.den c)::acc) expr [], constant) )
+
+ let simplified_monomials_from_texp (t: t) texp =
+ let res = simplified_monomials_from_texp t texp in
+ if M.tracing then M.tracel "from_texp" "%s %s -> %s" (EConj.show @@ snd @@ BatOption.get t.d) (Format.asprintf "%a" Texpr1.print_expr texp)
+ (BatOption.map_default (fun (l,(o,d)) -> List.fold_right (fun (a,x,b) acc -> Printf.sprintf "%s*var_%d/%s + %s" (Z.to_string a) x (Z.to_string b) acc) l ((Z.to_string o)^"/"^(Z.to_string d))) "" res);
+ res
let simplify_to_ref_and_offset (t: t) texp =
BatOption.bind (simplified_monomials_from_texp t texp )
- (fun (sum_of_terms, constant) ->
+ (fun (sum_of_terms, (constant,divisor)) ->
(match sum_of_terms with
- | [] -> Some (None, constant)
- | [(coeff,var)] when Z.equal coeff Z.one -> Some (Some var, constant)
+ | [] -> Some (None, constant,divisor)
+ | [(coeff,var,divi)] -> Some (Rhs.canonicalize (Some (Z.mul divisor coeff,var), Z.mul constant divi,Z.mul divisor divi))
|_ -> None))
let simplify_to_ref_and_offset t texp = timing_wrap "coeff_vec" (simplify_to_ref_and_offset t) texp
- (* Copy because function is not "with" so should not mutate inputs *)
- let assign_const t var const = match t.d with
+ let assign_const t var const divi = match t.d with
| None -> t
- | Some t_d -> {d = Some (EConj.set_rhs t_d var (None, const)); env = t.env}
-
- let subtract_const_from_var t var const =
- match t.d with
- | None -> t
- | Some t_d ->
- let subtract_const_from_var_for_single_equality index (eq_var_opt, off2) econ =
- if index <> var then
- begin match eq_var_opt with
- | Some eq_var when eq_var = var ->
- EConj.set_rhs econ index (eq_var_opt, Z.(off2 - const))
- | _ -> econ
- end
- else econ
- in
- let d =
- if not @@ EConj.nontrivial t_d var
- (* var is a reference variable -> it can appear on the right-hand side of an equality *)
- then
- (EConj.IntMap.fold (subtract_const_from_var_for_single_equality) (snd t_d) t_d)
- else
- (* var never appears on the right hand side-> we only need to modify the array entry at index var *)
- EConj.set_rhs t_d var (Tuple2.map2 (Z.add const) (EConj.get_rhs t_d var))
- in
- {d = Some d; env = t.env}
+ | Some t_d -> {d = Some (EConj.set_rhs t_d var (None, const, divi)); env = t.env}
end
@@ -299,9 +360,9 @@ struct
if t.d = None then None, None
else
match simplify_to_ref_and_offset t (Texpr1.to_expr texpr) with
- | Some (None, offset) ->
- (if M.tracing then M.tracel "bounds" "min: %s max: %s" (IntOps.BigIntOps.to_string offset) (IntOps.BigIntOps.to_string offset);
- Some offset, Some offset)
+ | Some (None, offset, divisor) when Z.equal (Z.rem offset divisor) Z.zero -> let res = Z.div offset divisor in
+ (if M.tracing then M.tracel "bounds" "min: %s max: %s" (IntOps.BigIntOps.to_string res) (IntOps.BigIntOps.to_string res);
+ Some res, Some res)
| _ -> None, None
let bound_texpr d texpr1 = timing_wrap "bounds calculation" (bound_texpr d) texpr1
@@ -336,11 +397,23 @@ struct
let top () = {d = Some (EConj.empty()); env = empty_env}
(** is_top returns true for top_of array and empty array; precondition: t.env and t.d are of same size *)
- let is_top t = Environment.equal empty_env t.env && GobOption.exists EConj.is_top_con t.d
+ let is_top t = GobOption.exists EConj.is_top_con t.d
+
+ let to_subscript i =
+ let transl = [|"₀";"₁";"₂";"₃";"₄";"₅";"₆";"₇";"₈";"₉"|] in
+ let rec subscr i =
+ if i = 0 then ""
+ else (subscr (i/10)) ^ transl.(i mod 10) in
+ subscr i
+
+ let show_var env i =
+ let res = Var.to_string (Environment.var_of_dim env i) in
+ match String.split_on_char '#' res with
+ | varname::rest::[] -> varname ^ (try to_subscript @@ int_of_string rest with _ -> "#" ^ rest)
+ | _ -> res
(** prints the current variable equalities with resolved variable names *)
let show varM =
- let lookup i = Var.to_string (Environment.var_of_dim varM.env i) in
match varM.d with
| None -> "⊥\n"
| Some arr when EConj.is_top_con arr -> "⊤\n"
@@ -348,25 +421,25 @@ struct
if is_bot varM then
"Bot \n"
else
- EConj.show_formatted lookup (snd arr) ^ (" with dimension " ^ (string_of_int @@ fst arr))
+ EConj.show_formatted (show_var varM.env) (snd arr) ^ (to_subscript @@ fst arr)
let pretty () (x:t) = text (show x)
let printXml f x = BatPrintf.fprintf f "\n\n\n" (XmlUtil.escape (Format.asprintf "%s" (show x) )) (XmlUtil.escape (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (x.env)))
let eval_interval ask = Bounds.bound_texpr
- let meet_with_one_conj t i (var, b) =
+ let meet_with_one_conj t i (var, o, divi) =
match t.d with
| None -> t
| Some d ->
try
- { d = Some (EConj.meet_with_one_conj d i (var, b)); env = t.env}
+ { d = Some (EConj.meet_with_one_conj d i (var, o, divi)); env = t.env}
with EConj.Contradiction ->
if M.tracing then M.trace "meet" " -> Contradiction\n";
{ d = None; env = t.env}
let meet_with_one_conj t i e =
let res = meet_with_one_conj t i e in
- if M.tracing then M.trace "meet" "meet_with_one_conj %s with var_%d=%s -> %s" (show t) i (Rhs.show e) (show res);
+ if M.tracing then M.tracel "meet" "%s with single eq %s=%s -> %s" (show t) (Z.(to_string @@ Tuple3.third e)^ show_var t.env i) (Rhs.show_rhs_formatted (show_var t.env) e) (show res);
res
let meet t1 t2 =
@@ -387,15 +460,17 @@ struct
let leq t1 t2 =
let env_comp = Environment.compare t1.env t2.env in (* Apron's Environment.compare has defined return values. *)
- let implies ts i (var, b) =
- let tuple_cmp = Tuple2.eq (Option.eq ~eq:Int.equal) (Z.equal) in
+ let implies ts i (var, offs, divi) =
+ let tuple_cmp = Tuple3.eq (Option.eq ~eq:(Tuple2.eq (Z.equal) (Int.equal))) (Z.equal) (Z.equal) in
match var with
- | None -> tuple_cmp (var, b) (EConj.get_rhs ts i)
- | Some j -> tuple_cmp (EConj.get_rhs ts i) @@ Tuple2.map2 (Z.add b) (EConj.get_rhs ts j)
+ (* directly compare in case of constant value *)
+ | None -> tuple_cmp (var, offs, divi) (EConj.get_rhs ts i)
+ (* normalize in case of a full blown equality *)
+ | Some (coeffj,j) -> tuple_cmp (EConj.get_rhs ts i) @@ Rhs.subst (EConj.get_rhs ts j) j (var, offs, divi)
in
if env_comp = -2 || env_comp > 0 then false else
- if is_bot_env t1 || is_top t2 then true else
- if is_bot_env t2 || is_top t1 then false else
+ if is_bot_env t1 || is_top t2 then true
+ else if is_bot_env t2 || is_top t1 then false else
let m1, m2 = Option.get t1.d, Option.get t2.d in
let m1' = if env_comp = 0 then m1 else VarManagement.dim_add (Environment.dimchange t1.env t2.env) m1 in
EConj.IntMap.for_all (implies m1') (snd m2) (* even on sparse m2, it suffices to check the non-trivial equalities, still present in sparse m2 *)
@@ -412,32 +487,50 @@ struct
(* joinfunction handles the dirty details of performing an "inner join" on the lhs of both bindings;
in the resulting binding, the lhs is then mapped to values that are later relevant for sorting/grouping, i.e.
- lhs itself
- - the difference of both offsets
+ - criteria A and B that characterize equivalence class, depending on the reference variable and the affine expression parameters wrt. each EConj
- rhs1
- rhs2
however, we have to account for the sparseity of EConj maps by manually patching holes with default values *)
- let joinfunction lhs rhs1 rhs2 = match rhs1, rhs2 with
- | Some (ai,aj),Some (bi,bj) -> Some (lhs,Z.(aj - bj),(ai,aj),(bi,bj)) (* this is explicitely what we want *)
- | None, Some (bi,bj) -> Some (lhs,Z.neg bj ,Rhs.var_zero lhs,(bi,bj)) (* account for the sparseity of binding 1 *)
- | Some (ai,aj), None -> Some (lhs,aj ,(ai,aj),Rhs.var_zero lhs) (* account for the sparseity of binding 2 *)
- | _,_ -> None (* no binding for lhs in both maps is replicated implicitely in a sparse result map *)
+ let joinfunction lhs rhs1 rhs2 =
+ (
+ let e = Option.default (Rhs.var_zero lhs) in
+ match rhs1,rhs2 with (* first of all re-instantiate implicit sparse elements *)
+ | None, None -> None
+ | a, b -> Some (e a, e b))
+ |>
+ BatOption.map (fun (r1,r2) -> match (r1,r2) with (* criterion A , criterion B *)
+ | (Some (c1,_),o1,d1), (Some (c2,_),o2,d2)-> lhs, Q.make Z.((o1*d2)-(o2*d1)) Z.(c1*d2), Q.make Z.(c2*d2) Z.(c1*d1), r1, r2
+ | (None, oc,dc), (Some (cv,_),ov,dv)
+ | (Some (cv,_),ov,dv), (None ,oc,dc)-> lhs, Q.make Z.((oc*dv)-(ov*dc)) Z.(dc*cv), Q.one , r1, r2 (* equivalence class defined by (oc/dc-ov/dv)/(cv/dv) *)
+ | (None, o1,d1), (None ,o2,d2)-> lhs, (if Z.(zero = ((o1*d2)-(o2*d1))) then Q.one else Q.zero), Q.zero, r1, r2 (* only two equivalence classes: constants with matching values or constants with different values *)
+ )
in
let table = List.of_enum @@ EConj.IntMap.values @@ EConj.IntMap.merge joinfunction (snd ad) (snd bd) in
- (*compare two variables for grouping depending on delta function and reference index*)
- let cmp_z (_, t0i, t1i, t2i) (_, t0j, t1j, t2j) =
- let cmp_ref = Option.compare ~cmp:Int.compare in
- Tuple3.compare ~cmp1:cmp_ref ~cmp2:cmp_ref ~cmp3:Z.compare (fst t1i, fst t2i, t0i) (fst t1j, fst t2j, t0j)
+ (* compare two variables for grouping depending on affine function parameters a, b and reference variable indices *)
+ let cmp_z (_, ai, bi, t1i, t2i) (_, aj, bj, t1j, t2j) =
+ let cmp_ref = Option.compare ~cmp:(fun x y -> Int.compare (snd x) (snd y)) in
+ Tuple4.compare ~cmp1:cmp_ref ~cmp2:cmp_ref ~cmp3:Q.compare ~cmp4:Q.compare (Tuple3.first t1i, Tuple3.first t2i, ai, bi) (Tuple3.first t1j, Tuple3.first t2j, aj, bj)
in
- (*Calculate new components as groups*)
+ (* Calculate new components as groups *)
let new_components = BatList.group cmp_z table in
- (*Adjust the domain array to represent the new components*)
- let modify map idx_h b_h (idx, _, (opt1, z1), (opt2, z2)) = EConj.set_rhs map (idx)
- (if opt1 = opt2 && Z.equal z1 z2 then (opt1, z1)
- else (Some idx_h, Z.(z1 - b_h)))
+ let varentry ci offi ch offh xh =
+ let (coeff,off,d) = Q.(ci,(offi*ch)-(ci*offh),ch) in (* compute new rhs in Q *)
+ let (coeff,off,d) = Z.(coeff.num*d.den*off.den,off.num*d.den*coeff.den,d. num*coeff.den*off.den) in (* convert that back into Z *)
+ Rhs.canonicalize (Some(coeff,xh),off,d)
in
- let iterate map l =
+ (* ci1 = a*ch1+b /\ ci2 = a*ch2+b *)
+ (* ===> a = (ci1-ci2)/(ch1-ch2) b = ci2-a*ch2 *)
+ let constentry ci1 ci2 ch1 ch2 xh =
+ let a = Q.((ci1-ci2) / (ch1-ch2)) in
+ let b = Q.(ci2 - a*ch2) in
+ Rhs.canonicalize (Some (Z.(a.num*b.den),xh),Z.(b.num*a.den) ,Z.(a.den*b.den) ) in
+ let iterate map l =
match l with
- | (idx_h, _, (_, b_h), _) :: t -> List.fold (fun map' e -> modify map' idx_h b_h e) map l
+ | (_, _, _, rhs , rhs' ) :: t when Rhs.equal rhs rhs' -> List.fold (fun acc (x,_,_,rh,_) -> EConj.set_rhs acc x rh) map l
+ | (h, _, _, ((Some (ch,_),oh,dh)), ((Some _,_,_) )) :: t -> List.fold (fun acc (i,_,_,(monom,oi,di),_) -> EConj.set_rhs acc i (varentry Q.(make (fst@@Option.get monom) di) Q.(make oi di) Q.(make ch dh) Q.(make oh dh) h)) map t
+ | (h, _, _, ((Some (ch,_),oh,dh)), ((None,_,_) )) :: t -> List.fold (fun acc (i,_,_,(monom,oi,di),_) -> EConj.set_rhs acc i (varentry Q.(make (fst@@Option.get monom) di) Q.(make oi di) Q.(make ch dh) Q.(make oh dh) h)) map t
+ | (h, _, _, ((None,_,_) ), ((Some (ch,_),oh,dh))) :: t -> List.fold (fun acc (i,_,_,_,(monom,oi,di)) -> EConj.set_rhs acc i (varentry Q.(make (fst@@Option.get monom) di) Q.(make oi di) Q.(make ch dh) Q.(make oh dh) h)) map t
+ | (h, _, _, ((None,oh1,dh1) ), ((None),oh2,dh2) ) :: t -> List.fold (fun acc (i,_,_,(_,oi1,di1),(_,oi2,di2)) -> EConj.set_rhs acc i (constentry Q.(make oi1 di1) Q.(make oi2 di2) Q.(make oh1 dh1) Q.(make oh2 dh2) h)) map t
| [] -> let exception EmptyComponent in raise EmptyComponent
in
Some (List.fold iterate (EConj.make_empty_conj @@ fst ad) new_components)
@@ -512,15 +605,15 @@ struct
| None ->
(* Statement "assigned_var = ?" (non-linear assignment) *)
forget_var t var
- | Some (None, off) ->
+ | Some (None, off, divi) ->
(* Statement "assigned_var = off" (constant assignment) *)
- assign_const (forget_var t var) var_i off
- | Some (Some exp_var, off) when var_i = exp_var ->
- (* Statement "assigned_var = assigned_var + off" *)
- subtract_const_from_var t var_i off
- | Some (Some exp_var, off) ->
- (* Statement "assigned_var = exp_var + off" (assigned_var is not the same as exp_var) *)
- meet_with_one_conj (forget_var t var) var_i (Some exp_var, off)
+ assign_const (forget_var t var) var_i off divi
+ | Some (Some (coeff_var,exp_var), off, divi) when var_i = exp_var ->
+ (* Statement "assigned_var = (coeff_var*assigned_var + off) / divi" *)
+ {d=Some (EConj.affine_transform d var_i (coeff_var, var_i, off, divi)); env=t.env }
+ | Some (Some monomial, off, divi) ->
+ (* Statement "assigned_var = (monomial) + off / divi" (assigned_var is not the same as exp_var) *)
+ meet_with_one_conj (forget_var t var) var_i (Some (monomial), off, divi)
end
| None -> bot_env
@@ -624,9 +717,9 @@ struct
| Some d ->
match simplified_monomials_from_texp t (Texpr1.to_expr @@ Tcons1.get_texpr1 tcons) with
| None -> t
- | Some (sum_of_terms, constant) ->(
+ | Some (sum_of_terms, (constant,divisor)) ->(
match sum_of_terms with
- | [] -> (* no reference variables in the guard *)
+ | [] -> (* no reference variables in the guard, so check constant for zero *)
begin match Tcons1.get_typ tcons with
| EQ when Z.equal constant Z.zero -> t
| SUPEQ when Z.geq constant Z.zero -> t
@@ -635,15 +728,21 @@ struct
| EQMOD _ -> t
| _ -> bot_env (* all other results are violating the guard *)
end
- | [(varexpr, index)] -> (* guard has a single reference variable only *)
- if Tcons1.get_typ tcons = EQ && Z.divisible constant varexpr then
- meet_with_one_conj t index (None, (Z.(-(constant) / varexpr)))
+ | [(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 *)
- | [(a1,var1); (a2,var2)] -> (* two variables in relation needs a little sorting out *)
+ | [(c1,var1,d1); (c2,var2,d2)] -> (* two variables in relation needs a little sorting out *)
begin match Tcons1.get_typ tcons with
- | EQ when Z.(a1 * a2 = -one) -> (* var1-var1 or var2-var1 *)
- meet_with_one_conj t var2 (Some var1, Z.mul a1 constant)
+ | EQ -> (* c1*var1/d1 + c2*var2/d2 +constant/divisor = 0*)
+ (* ======> c1*divisor*d2 * var1 = -c2*divisor*d1 * var2 +constant*-d1*d2*)
+ (* \/ c2*divisor*d1 * var2 = -c1*divisor*d2 * var1 +constant*-d1*d2*)
+ let open Z in
+ if var1 < var2 then
+ meet_with_one_conj t var2 (Rhs.canonicalize (Some (neg @@ c1*divisor,var1),neg @@ constant*d2*d1,c2*divisor*d1))
+ else
+ meet_with_one_conj t var1 (Rhs.canonicalize (Some (neg @@ c2*divisor,var2),neg @@ constant*d2*d1,c1*divisor*d2))
| _-> t (* Not supported in equality based 2vars without coeffiients *)
end
| _ -> t (* For equalities of more then 2 vars we just return t *))
@@ -697,14 +796,14 @@ struct
lincons
in
let get_const acc i = function
- | (None, o) ->
+ | (None, o, d) ->
let xi = Environment.var_of_dim t.env i in
- of_coeff xi [(Coeff.s_of_int (-1), xi)] o :: acc
- | (Some r, _) when r = i -> acc
- | (Some r, o) ->
+ of_coeff xi [(GobApron.Coeff.s_of_z @@ Z.neg d, xi)] o :: acc
+ | (Some (c,r), _,_) when r = i -> acc
+ | (Some (c,r), o, d) ->
let xi = Environment.var_of_dim t.env i in
let ri = Environment.var_of_dim t.env r in
- of_coeff xi [(Coeff.s_of_int (-1), xi); (Coeff.s_of_int 1, ri)] o :: acc
+ of_coeff xi [(GobApron.Coeff.s_of_z @@ Z.neg d, xi); (GobApron.Coeff.s_of_z c, ri)] o :: acc
in
BatOption.get t.d |> fun (_,map) -> EConj.IntMap.fold (fun lhs rhs list -> get_const list lhs rhs) map []
diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index 827dc252fc..8c94c996b0 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -109,7 +109,7 @@ struct
| `Bot -> raise (Unsupported_CilExp Exp_not_supported) (* This should never happen according to Michael Schwarz *)
| `Top -> IntDomain.IntDomTuple.top_of ik
| `Lifted x -> x (* Cast should be unnecessary because it should be taken care of by EvalInt. *) in
- if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp/query: %a -> %a" d_plainexp e IntDomain.IntDomTuple.pretty res;
+ if M.tracing then M.trace "relation-query" "texpr1_expr_of_cil_exp/query: %a -> %a" d_plainexp e IntDomain.IntDomTuple.pretty res;
res
in
(* recurse without env and ask arguments *)
@@ -136,8 +136,15 @@ struct
let expr =
(** simplify asks for a constant value of some subexpression e, similar to a constant fold. In particular but not exclusively
this query is answered by the 2 var equalities domain itself. This normalizes arbitrary expressions to a point where they
- might be able to be represented by means of 2 var equalities *)
+ might be able to be represented by means of 2 var equalities
+
+ This simplification happens during a time, when there are temporary variables a#in and a#out part of the expression,
+ but are not represented in the ctx, thus queries may result in top for these variables. Wrapping this in speculative
+ mode is a stop-gap measure to avoid flagging overflows. We however should address simplification in a more generally useful way.
+ outside of the apron-related expression conversion.
+ *)
let simplify e =
+ GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () ->
let ikind = try (Cilfacade.get_ikind_exp e) with Invalid_argument _ -> raise (Unsupported_CilExp Exp_not_supported) in
let simp = query e ikind in
let const = IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to ikind simp in
diff --git a/tests/regression/77-lin2vareq/34-coefficient-features.c b/tests/regression/77-lin2vareq/34-coefficient-features.c
new file mode 100644
index 0000000000..561eccf0af
--- /dev/null
+++ b/tests/regression/77-lin2vareq/34-coefficient-features.c
@@ -0,0 +1,62 @@
+//SKIP PARAM: --set ana.activated[+] lin2vareq --set sem.int.signed_overflow assume_none
+// this test checks basic coefficient handing in main and join capabilities in loop
+
+#include
+
+void loop() {
+ int random;
+ int i = 0;
+ int x = 0;
+ int y = 0;
+
+ x=x+4;
+ y=y+8;
+ i=i+1;
+
+ if (random) {
+ x=x+4;
+ y=y+8;
+ i=i+1;
+ }
+
+ __goblint_check(x == 4*i); //SUCCESS
+
+ x=0;
+ y=0;
+
+ for(i = 1; i < 100; i++) {
+ x=x+4;
+ y=y+8;
+
+ __goblint_check(y == 2*x); //SUCCESS
+ __goblint_check(x == 4*i); //SUCCESS
+ }
+}
+
+void main() {
+ int a;
+ int b;
+ int c;
+ int unknown;
+ a = 4;
+
+ b = 4*c;
+
+ __goblint_check(b == 4*c); //SUCCESS
+
+ b = a*c;
+
+ __goblint_check(b == 4*c); //SUCCESS
+
+ if (7*b == 20*unknown + a){
+
+ __goblint_check(7*b == 20*unknown + a); //SUCCESS
+ }
+
+ b = unknown ? a*c : 4*c;
+
+ __goblint_check(b == 4*c); //SUCCESS
+
+ loop();
+
+}
\ No newline at end of file