From c6d19a977d7671354b4daf7bb870b295d69091b0 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Wed, 15 May 2024 12:30:01 +0200 Subject: [PATCH 01/53] initial components for coefficients added --- .../apron/linearTwoVarEqualityDomain.apron.ml | 31 +++++++++++-------- 1 file changed, 18 insertions(+), 13 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 67bd67f4e5..ebe973536a 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -17,15 +17,20 @@ 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 + (* (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 * GobZ.t * GobZ.t) [@@deriving eq, ord, hash] + let var_zero i = (Some i, Z.zero, Z.one, Z.one) + let show_coeff c = + if Z.equal c Z.one then "" + else (Z.to_string c) ^"*" + let show_rhs_formatted formatter = function + | (Some v, o,coeff,_) when Z.equal o Z.zero -> Printf.sprintf "%s%s" (show_coeff coeff) (formatter v) + | (Some v, o,coeff,_) -> Printf.sprintf "%s%s%+Ld" (show_coeff coeff) (formatter v) (Z.to_int64 o) + | (None, o,_,_) -> Printf.sprintf "%Ld" (Z.to_int64 o) + let show (v,o,c,d) = + let rhs=show_rhs_formatted (Printf.sprintf "var_%d") (v,o,c,d) in + if not (Z.equal d Z.one) then "(" ^ rhs ^ ")/" ^ (Z.to_string d) else rhs end module EqualitiesConjunction = struct @@ -36,7 +41,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 (refvar,off,coeff,divi) acc -> Printf.sprintf "%s%s=%s ∧ %s" (Rhs.show_coeff divi) (formatter i) (Rhs.show_rhs_formatted formatter (refvar,off,coeff,divi)) acc) econ "" in "{" ^ String.sub str 0 (String.length str - 4) ^ "}" let show econ = show_formatted (Printf.sprintf "var_%d") econ @@ -86,9 +91,9 @@ 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,coeff,divi) = 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,coeff,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 (memobumpvar) refvar,offset,coeff,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) From d2ce1755e394d15e67f44c7cbc7c877ae55406ea Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Wed, 15 May 2024 13:36:49 +0200 Subject: [PATCH 02/53] adaptation of forget_variable to coefficients --- .../apron/linearTwoVarEqualityDomain.apron.ml | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index ebe973536a..ffccecb05f 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -116,17 +116,23 @@ 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 = Tuple4.first (get_rhs d var) in match ref_var_opt with | Some ref_var when ref_var = 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 + (fun i (ref,_,_,_) l -> if ref = ref_var_opt then i::l else l) (snd d) [] in (* 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 :: _ -> + (* ax = by + c /\ a'z = b'y + c' *) + (* ==[[ y:=? ]]==> (a'b)z = (b'a)x + c' -(b'c) *) + let (_,c,b,a) = (get_rhs d head) in (* take offset between old and new reference variable *) + List.fold (fun map i -> + let (_,c',b',a') = (get_rhs d i) in + let newrhs = (Some head, Z.(c' - (b' * c)), Z.(b'*a), Z.(a'*b)) in + set_rhs map i newrhs + ) d cluster (* shift offset to match new reference variable *) | [] -> 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 *) From 889161995918736447ff54803286b26d040d88cb Mon Sep 17 00:00:00 2001 From: Michael Petter Date: Wed, 15 May 2024 17:20:55 +0200 Subject: [PATCH 03/53] more accurate representation and canonicalization --- .../apron/linearTwoVarEqualityDomain.apron.ml | 59 ++++++++++++------- 1 file changed, 38 insertions(+), 21 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index ffccecb05f..8fb799804f 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -17,20 +17,30 @@ 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 * GobZ.t * GobZ.t) [@@deriving eq, ord, hash] - let var_zero i = (Some i, Z.zero, Z.one, Z.one) + (* 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 (Z.to_string c) ^"*" let show_rhs_formatted formatter = function - | (Some v, o,coeff,_) when Z.equal o Z.zero -> Printf.sprintf "%s%s" (show_coeff coeff) (formatter v) - | (Some v, o,coeff,_) -> Printf.sprintf "%s%s%+Ld" (show_coeff coeff) (formatter v) (Z.to_int64 o) - | (None, o,_,_) -> Printf.sprintf "%Ld" (Z.to_int64 o) - let show (v,o,c,d) = - let rhs=show_rhs_formatted (Printf.sprintf "var_%d") (v,o,c,d) in + | (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%+Ld" (show_coeff coeff) (formatter v) (Z.to_int64 o) + | (None, o,_) -> Printf.sprintf "%Ld" (Z.to_int64 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 is the canonical form for adx+bdy+cd *) + let canonicalize (v,o,d) = + let gcd = Z.gcd o d in + let gcd = match v with + | Some (c,_) -> Z.gcd c gcd + | None -> gcd + in (BatOption.map (fun (coeff,i) -> (Z.div coeff gcd,i)) v,Z.div o gcd, Z.div d gcd) end module EqualitiesConjunction = struct @@ -41,7 +51,7 @@ module EqualitiesConjunction = struct let show_formatted formatter econ = if IntMap.is_empty econ then "{}" else - let str = IntMap.fold (fun i (refvar,off,coeff,divi) acc -> Printf.sprintf "%s%s=%s ∧ %s" (Rhs.show_coeff divi) (formatter i) (Rhs.show_rhs_formatted formatter (refvar,off,coeff,divi)) acc) econ "" in + let str = IntMap.fold (fun i (ref,off,divi) acc -> Printf.sprintf "%s%s=%s ∧ %s" (Rhs.show_coeff divi) (formatter i) (Rhs.show_rhs_formatted formatter (ref,off,divi)) acc) econ "" in "{" ^ String.sub str 0 (String.length str - 4) ^ "}" let show econ = show_formatted (Printf.sprintf "var_%d") econ @@ -60,13 +70,18 @@ module EqualitiesConjunction = struct (** 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) + + (** add a new equality to the domain *) let copy = identity @@ -91,9 +106,9 @@ module EqualitiesConjunction = struct IntHashtbl.add h x r; r) in - let rec bumpentry k (refvar,offset,coeff,divi) = 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,coeff,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 (memobumpvar) refvar,offset,coeff,divi) tbl, delta, lyst) + let rec bumpentry k (refvar,offset,divi) = 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,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) @@ -116,22 +131,24 @@ module EqualitiesConjunction = struct (* Forget information about variable i *) let forget_variable d var = let res = - (let ref_var_opt = Tuple4.first (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 -> (* var is the reference variable of its connected component *) (let cluster = IntMap.fold - (fun i (ref,_,_,_) l -> if ref = ref_var_opt then i::l else l) (snd d) [] in + (fun i (ref,_,_) l -> if ref = ref_var_opt then i::l else l) (snd d) [] in (* obtain cluster with common reference variable ref_var*) match cluster with (* new ref_var is taken from head of the cluster *) | head :: _ -> (* ax = by + c /\ a'z = b'y + c' *) (* ==[[ y:=? ]]==> (a'b)z = (b'a)x + c' -(b'c) *) - let (_,c,b,a) = (get_rhs d head) in (* take offset between old and new reference variable *) + let (newref,c,a) = (get_rhs d head) in (* take offset between old and new reference variable *) + let (b,_) = BatOption.get newref in List.fold (fun map i -> - let (_,c',b',a') = (get_rhs d i) in - let newrhs = (Some head, Z.(c' - (b' * c)), Z.(b'*a), Z.(a'*b)) in - set_rhs map i newrhs + let (oldref,c',a') = (get_rhs d i) in + let (b',_) = BatOption.get oldref in + let newrhs = (Some (Z.(b'*a),head), Z.(c' - (b' * c)), Z.(a'*b)) in + canonicalize_and_set map i newrhs ) d cluster (* shift offset to match new reference variable *) | [] -> d) (* empty cluster means no work for us *) | _ -> d) (* variable is either a constant or expressed by another refvar *) in From 19c43f6f7e9b78cfe7fd0015f25b86e60743739e Mon Sep 17 00:00:00 2001 From: Michael Petter Date: Wed, 15 May 2024 17:55:37 +0200 Subject: [PATCH 04/53] conversion to lincons --- src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 8fb799804f..6fa7d9423d 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -725,14 +725,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 [(Coeff.s_of_int (- (Z.to_int 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 [(Coeff.s_of_int (- (Z.to_int d)), xi); (Coeff.s_of_int @@ Z.to_int c, ri)] o :: acc in BatOption.get t.d |> fun (_,map) -> EConj.IntMap.fold (fun lhs rhs list -> get_const list lhs rhs) map [] From 5c2e7410da4d996ecdb255cdc0a00c5b4063242d Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Thu, 16 May 2024 09:25:08 +0200 Subject: [PATCH 05/53] [skip ci] generate coefficient-carrying monomials from texp --- .../apron/linearTwoVarEqualityDomain.apron.ml | 21 +++++++++++-------- 1 file changed, 12 insertions(+), 9 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 6fa7d9423d..620dd307b2 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -223,14 +223,17 @@ 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 (function + | (Some(coeff,i),offs,divi) -> (Some(Z.neg coeff,i),Z.neg offs,divi) + | (None ,offs,divi) -> (None ,Z.neg offs,divi)) coeff_var_list in + let multiply_with_Z number divisor coeff_var_list = List.map (function + | (Some (coeff, var),offs,divi) -> Rhs.canonicalize (Some(Z.mul number coeff,var),Z.(number * offs),Z.mul divi divisor) + | (None,offs,divi) -> Rhs.canonicalize (None,Z.mul number offs,Z.mul 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,a_coeff, divi)], b -> multiply_with_Z a_coeff divi b + | a, [(None,b_coeff, divi)] -> multiply_with_Z b_coeff divi a | _ -> raise NotLinearExpr in let rec convert_texpr texp = @@ -239,16 +242,16 @@ struct | 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,Z.one); (None,k,Z.one)] + | (None, k,divi) -> [ (None,k,Z.one)]) 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 *) From e97e26e175ab430dac47e5e92cd42212e6bc83a5 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Fri, 17 May 2024 15:28:02 +0200 Subject: [PATCH 06/53] [skip ci] migrated meet_with_one_conj --- .../apron/linearTwoVarEqualityDomain.apron.ml | 68 ++++++++++++++----- 1 file changed, 51 insertions(+), 17 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 620dd307b2..1793f38de8 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -41,6 +41,14 @@ module Rhs = struct | Some (c,_) -> Z.gcd c gcd | None -> gcd in (BatOption.map (fun (coeff,i) -> (Z.div coeff gcd,i)) v,Z.div o gcd, Z.div d gcd) + + (** Substitute rhs for varx in rhs' *) + let subst rhs varx rhs' = + match rhs,rhs' with + | (Some (c,x),o,d),(Some (c',x'),o',d') when x'=varx -> canonicalize (Some (Z.mul c c',x),Z.((o*c')+(d*o')),Z.mul d d') + | (None ,o,d),(Some (c',x'),o',d') when x'=varx -> canonicalize (None ,Z.((o*c')+(d*o')),Z.mul d d') + | _ -> rhs' + end module EqualitiesConjunction = struct @@ -67,6 +75,9 @@ 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 reverse 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 @@ -181,29 +192,52 @@ 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 tsi 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 -> Rhs.canonicalize (BatOption.map (fun (c,y)->(Z.mul c c',y)) vary, Z.((c'*o)+(o'*d)),Z.(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 *) + (fst tsi, IntMap.add x (vary, o, d) @@ IntMap.map adjust (snd tsi)) (* 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 @@ reverse 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 no unite the two equvalence classes; let's decide upon the representant *) + then (* express h2 in terms of h1: *) + let (_,newh2)= reverse j (coeff2,h2,o2,divi2) in + let newh2 = Rhs.subst oldi i (Rhs.subst (snd @@ reverse i (coeff,j,offs,divi)) j newh2) in + subst_var ts h2 newh2 + else (* express h1 in terms of h2: *) + let (_,newh1)= reverse 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.trace "meet" "meet_with_one_conj conj: { %s } eq: var_%d=%s -> { %s } " (show (snd ts)) i (Rhs.show (var,offs,divi)) (show (snd ts)) ; res end From a9248db7e355c7dfa74182acaa8eeab55abfb866 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Fri, 17 May 2024 15:38:23 +0200 Subject: [PATCH 07/53] [skip ci] tiny migration steps, low hanging fruit --- .../apron/linearTwoVarEqualityDomain.apron.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 1793f38de8..6d6363329b 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -327,7 +327,7 @@ struct (* Copy because function is not "with" so should not mutate inputs *) let assign_const t var const = match t.d with | None -> t - | Some t_d -> {d = Some (EConj.set_rhs t_d var (None, const)); env = t.env} + | Some t_d -> {d = Some (EConj.set_rhs t_d var (None, const,Z.one)); env = t.env} let subtract_const_from_var t var const = match t.d with @@ -419,12 +419,12 @@ struct let printXml f x = BatPrintf.fprintf f "\n\n\nequalities\n\n\n%s\n\nenv\n\n\n%s\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} @@ -585,7 +585,7 @@ struct 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) + meet_with_one_conj (forget_var t var) var_i (Some (Z.one,exp_var), off, Z.one) end | None -> bot_env @@ -702,13 +702,13 @@ struct 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))) + meet_with_one_conj t index (None, (Z.(-(constant) / varexpr)),Z.one) else t (* only EQ is supported in equality based domains *) | [(a1,var1); (a2,var2)] -> (* 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) + meet_with_one_conj t var2 (Some (Z.one,var1), Z.mul a1 constant,Z.one) | _-> t (* Not supported in equality based 2vars without coeffiients *) end | _ -> t (* For equalities of more then 2 vars we just return t *)) From 1257b680109575bf79157d33f503eb23c7413fb1 Mon Sep 17 00:00:00 2001 From: Michael Petter Date: Sun, 19 May 2024 23:23:50 +0200 Subject: [PATCH 08/53] [skip ci] dealt with simplifying linear expressions to lin2vars with coeffs --- .../apron/linearTwoVarEqualityDomain.apron.ml | 47 ++++++++++--------- 1 file changed, 25 insertions(+), 22 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 6d6363329b..1e60f28e8f 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -260,14 +260,14 @@ struct let negate coeff_var_list = List.map (function | (Some(coeff,i),offs,divi) -> (Some(Z.neg coeff,i),Z.neg offs,divi) | (None ,offs,divi) -> (None ,Z.neg offs,divi)) coeff_var_list in - let multiply_with_Z number divisor coeff_var_list = List.map (function - | (Some (coeff, var),offs,divi) -> Rhs.canonicalize (Some(Z.mul number coeff,var),Z.(number * offs),Z.mul divi divisor) - | (None,offs,divi) -> Rhs.canonicalize (None,Z.mul number offs,Z.mul divi divisor)) coeff_var_list in + let multiply_with_Q dividend divisor coeff_var_list = List.map (function + | (Some (coeff, var),offs,divi) -> Rhs.canonicalize (Some(Z.mul dividend coeff,var),Z.(dividend * offs),Z.mul divi divisor) + | (None,offs,divi) -> Rhs.canonicalize (None,Z.mul dividend offs,Z.mul 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 - | [(None,a_coeff, divi)], b -> multiply_with_Z a_coeff divi b - | a, [(None,b_coeff, divi)] -> multiply_with_Z b_coeff divi a + | [(None,coeff, divi)], c + | c, [(None,coeff, divi)] -> multiply_with_Q coeff divi c | _ -> raise NotLinearExpr in let rec convert_texpr texp = @@ -284,8 +284,8 @@ struct | None -> [(Some (Z.one,var_dim),Z.zero,Z.one)] | Some d -> (match (EConj.get_rhs d var_dim) with - | (Some (coeff,i), k,divi) -> [(Some (coeff,i),Z.zero,Z.one); (None,k,Z.one)] - | (None, k,divi) -> [ (None,k,Z.one)]) + | (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 *) @@ -299,27 +299,27 @@ 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 *) + (** 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 expr = Array.make (Environment.size t.env) (Q.zero) in (*TODO*: migrate to map; array of coeff/divisor per var idx*) + let accumulate_constants (aconst,adiv) (v,offs,divi) = match v with + | None -> let gcdee = Z.gcd adiv divi in (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! *) + (Option.may (fun (coef,ter) -> expr.(ter) <- Q.(expr.(ter) + Q.make coef somedivi)) somevar; + let gcdee = Z.gcd adiv divi in (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 constant = List.fold_left accumulate_constants (Z.zero,Z.one) monomiallist in (* abstract simplification of the guard wrt. reference variables *) + Some (Array.fold_lefti (fun list v (c) -> if Q.equal c Q.zero then list else (c.num,v,c.den)::list) [] expr, constant) ) 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)] when Z.equal coeff Z.one -> 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 @@ -364,9 +364,12 @@ 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) + | Some (None, offset, divisor) -> 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 (Z.add res Z.one)); + Some res, Some (Z.add res Z.one); failwith "ToDo: Rethink interval bounds (add or subtract depending on sign of res)") | _ -> None, None let bound_texpr d texpr1 = timing_wrap "bounds calculation" (bound_texpr d) texpr1 From 034492e12c4772f0d06af8f8de305b66703a0839 Mon Sep 17 00:00:00 2001 From: Michael Petter Date: Mon, 20 May 2024 23:32:21 +0200 Subject: [PATCH 09/53] [skip ci] replaced overspecialized subtract_with_constant by affine_transform --- .../apron/linearTwoVarEqualityDomain.apron.ml | 70 ++++++++----------- 1 file changed, 31 insertions(+), 39 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 1e60f28e8f..b296a3420d 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -76,7 +76,7 @@ module EqualitiesConjunction = struct let nontrivial (_,econmap) lhs = IntMap.mem lhs econmap (** turn x = (cy+o)/d into y = (dx-o)/c*) - let reverse x (c,y,o,d) = (y,(Some (d,x),Z.neg 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 @@ -220,7 +220,7 @@ module EqualitiesConjunction = struct (* 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 @@ reverse i (coeff1,h1,o1,divi1) 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 ========> ... *) @@ -230,16 +230,32 @@ module EqualitiesConjunction = struct (if not @@ Rhs.equal normalizedi oldi then raise Contradiction else ts) else if h1 < h2 (* good, we no unite the two equvalence classes; let's decide upon the representant *) then (* express h2 in terms of h1: *) - let (_,newh2)= reverse j (coeff2,h2,o2,divi2) in - let newh2 = Rhs.subst oldi i (Rhs.subst (snd @@ reverse i (coeff,j,offs,divi)) j newh2) in + 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)= reverse i (coeff1,h1,o1,divi1) in + 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.trace "meet" "meet_with_one_conj conj: { %s } eq: var_%d=%s -> { %s } " (show (snd ts)) i (Rhs.show (var,offs,divi)) (show (snd ts)) ; res + (** affine transform variable i allover conj with transformer (Some (coeff,i)+offs)/divi *) + let affine_transform econ i (var,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 (var,offs,divi)) + else (* var_i = var_i, i.e. it may occur on the rhs of other equalities *) + match var with + | None -> failwith "this is not a valid affine transformation" + | Some (coeff,j) -> + (* 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]. @@ -325,33 +341,9 @@ struct 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 - | None -> t - | Some t_d -> {d = Some (EConj.set_rhs t_d var (None, const,Z.one)); env = t.env} - - let subtract_const_from_var t var const = - match t.d with + let assign_const t var const divi = 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 @@ -580,15 +572,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 (Z.one,exp_var), off, Z.one) + 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 (Some (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 From 4d2668177c4bde52a89897253c2327806954b22c Mon Sep 17 00:00:00 2001 From: Michael Petter Date: Tue, 21 May 2024 08:52:54 +0200 Subject: [PATCH 10/53] [skip ci] bounds --- src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index b296a3420d..a0bbcbce39 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -360,8 +360,12 @@ struct (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) | Some (None, offset, divisor) -> 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 (Z.add res Z.one)); - Some res, Some (Z.add res Z.one); failwith "ToDo: Rethink interval bounds (add or subtract depending on sign of res)") + let (lower,upper) = if Z.lt res Z.zero then + (Z.sub res Z.one,res) + else + (res,Z.add res Z.one) in + (if M.tracing then M.tracel "bounds" "min: %s max: %s" (IntOps.BigIntOps.to_string lower) (IntOps.BigIntOps.to_string upper); + Some lower, Some upper) | _ -> None, None let bound_texpr d texpr1 = timing_wrap "bounds calculation" (bound_texpr d) texpr1 From fa58e2e301432c85c89b596d1c87b0923816c833 Mon Sep 17 00:00:00 2001 From: Michael Petter Date: Tue, 21 May 2024 09:24:25 +0200 Subject: [PATCH 11/53] [skip ci] leq/implies now also for coefficients --- src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index a0bbcbce39..5234f8d2fa 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -451,11 +451,13 @@ 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 From ba485801970de0bf25618b8516b8ef4a89549523 Mon Sep 17 00:00:00 2001 From: Michael Petter Date: Tue, 21 May 2024 10:42:15 +0200 Subject: [PATCH 12/53] [skip ci] migrated meet_tcons --- .../apron/linearTwoVarEqualityDomain.apron.ml | 21 ++++++++++++------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 5234f8d2fa..51c6d702ef 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -690,9 +690,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 @@ -701,15 +701,20 @@ 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)),Z.one) + | [(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.(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 (Z.one,var1), Z.mul a1 constant,Z.one) + | 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*) + if var1 < var2 then + meet_with_one_conj t var2 (Rhs.canonicalize (Some (Z.neg @@ Z.(c1*divisor),var1),Z.neg @@ Z.(constant*d2*d1),Z.(c2*divisor*d1))) + else + meet_with_one_conj t var1 (Rhs.canonicalize (Some (Z.neg @@ Z.(c2*divisor),var2),Z.neg @@ Z.(constant*d2*d1),Z.(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 *)) From 80ef4bd311de6fb433683c042de56706e8cc7db8 Mon Sep 17 00:00:00 2001 From: Michael Petter Date: Tue, 21 May 2024 17:51:05 +0200 Subject: [PATCH 13/53] [skip ci] formulated new join sorting criterium --- .../apron/linearTwoVarEqualityDomain.apron.ml | 36 ++++++++++--------- 1 file changed, 20 insertions(+), 16 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 51c6d702ef..8e6a97d18c 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -478,32 +478,36 @@ 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 + - the affine transformation from refvar1 to refvar2, i.E. the parameters A and B of the general affine transformer Ax+B - 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 coeff = Option.map_default fst Z.one in match rhs1, rhs2 with + (* Compute Ax+B such that (coeff1*(Ax+B)+off1)/d1 = (coeff2*x+off2)/d2 *) + (* ====> A = (coeff2*d1)/(coeff1*d2) /\ B = (off2*d1-off1*d2)/(c1*c2) *) + (* lhs A B rhs1 rhs2 *) + (*TODO*: if this works, make it more concise *) + | Some (ai,aj,ak), Some (bi,bj,bk) -> Some (lhs,Q.make Z.(ak*coeff bi) Z.(bk* coeff ai),Q.make Z.(bj*ak-aj*bk) Z.(bk*coeff ai), (ai,aj,ak) , (bi,bj,bk)) (* this is explicitely what we want *) + | None , Some (bi,bj,bk) -> Some (lhs,Q.make Z.( coeff bi) Z.(bk ),Q.make Z.(bj ) Z.(bk ), Rhs.var_zero lhs, (bi,bj,bk)) (* account for the sparseity of binding 1 *) + | Some (ai,aj,ak), None -> Some (lhs,Q.make Z.(ak ) Z.( coeff ai),Q.make Z.( neg aj) Z.( coeff ai), (ai,aj,ak), 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 *) 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))) + (* Adjust the domain map to represent the new components *) + let modify map idx_h offs_h (idx, _, _, (opt1, z1, d1), (opt2, z2, d2)) = EConj.set_rhs map (idx) + (if opt1 = opt2 && Z.equal z1 z2 && Z.equal d1 d2 then (opt1, z1, d1) + else (Some idx_h, Z.(z1 - offs_h))) 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 + | (idx_h, _, _, (_, offs_h, divi_h), _) :: t -> List.fold (fun map' e -> modify map' idx_h offs_h e) map l | [] -> let exception EmptyComponent in raise EmptyComponent in Some (List.fold iterate (EConj.make_empty_conj @@ fst ad) new_components) From 7e5b727373e27d3cd0565ccb9f44fc9936934197 Mon Sep 17 00:00:00 2001 From: Michael Petter Date: Tue, 21 May 2024 18:03:23 +0200 Subject: [PATCH 14/53] [skip ci] satisfy semgrep --- src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 8e6a97d18c..6c12744228 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -361,9 +361,9 @@ struct Some res, Some res) | Some (None, offset, divisor) -> let res = Z.div offset divisor in let (lower,upper) = if Z.lt res Z.zero then - (Z.sub res Z.one,res) + (Z.pred res,res) else - (res,Z.add res Z.one) in + (res,Z.succ res) in (if M.tracing then M.tracel "bounds" "min: %s max: %s" (IntOps.BigIntOps.to_string lower) (IntOps.BigIntOps.to_string upper); Some lower, Some upper) | _ -> None, None From ad01be4ebe8012ee02bd1537386dbf00bd3cad1c Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Wed, 22 May 2024 10:27:40 +0200 Subject: [PATCH 15/53] [skip ci] finally affine transform the reference variables in join --- .../apron/linearTwoVarEqualityDomain.apron.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 6c12744228..cff8cab293 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -501,13 +501,16 @@ struct (* Calculate new components as groups *) let new_components = BatList.group cmp_z table in (* Adjust the domain map to represent the new components *) - let modify map idx_h offs_h (idx, _, _, (opt1, z1, d1), (opt2, z2, d2)) = EConj.set_rhs map (idx) - (if opt1 = opt2 && Z.equal z1 z2 && Z.equal d1 d2 then (opt1, z1, d1) - else (Some idx_h, Z.(z1 - offs_h))) + let modify map x (refmonom, offs, divi) (idx, _, _, (monom1, z1, d1), (monom2, z2, d2)) = EConj.set_rhs map (idx) + (if monom1 = monom2 && Z.equal z1 z2 && Z.equal d1 d2 then (monom1, z1, d1) + else + let refcoeff = Option.map_default fst Z.one refmonom in + let coeff1 = Option.map_default fst Z.one monom1 in + (Some (Z.(coeff1*divi),x), Z.((z1*refcoeff)-(offs*coeff1)), Z.(refcoeff*d1)) ) in let iterate map l = match l with - | (idx_h, _, _, (_, offs_h, divi_h), _) :: t -> List.fold (fun map' e -> modify map' idx_h offs_h e) map l + | (idx_h, _, _, rhs_h, _) :: t -> List.fold (fun acc e -> modify acc idx_h rhs_h e) map l | [] -> let exception EmptyComponent in raise EmptyComponent in Some (List.fold iterate (EConj.make_empty_conj @@ fst ad) new_components) From 9923eafdc167b0453cfad0cff3d4fffdc5617c0c Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Wed, 22 May 2024 11:28:29 +0200 Subject: [PATCH 16/53] cosmetics --- .../apron/linearTwoVarEqualityDomain.apron.ml | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index cff8cab293..6346dc0975 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -25,7 +25,8 @@ module Rhs = struct let var_zero i = (Some (Z.one,i), Z.zero, Z.one) let show_coeff c = if Z.equal c Z.one then "" - else (Z.to_string c) ^"*" + else if Z.equal c Z.minus_one then "-" + else (Z.to_string c) ^"·" let show_rhs_formatted formatter = 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%+Ld" (show_coeff coeff) (formatter v) (Z.to_int64 o) @@ -404,7 +405,13 @@ struct (** 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 + let lookup i = + let transl = [|"₀";"₁";"₂";"₃";"₄";"₅";"₆";"₇";"₈";"₉"|] in + let res = Var.to_string (Environment.var_of_dim varM.env i) in + match String.split_on_char '#' res with + | varname::rest::[] -> varname ^ (try String.fold_left (fun acc c -> acc ^ transl.(Char.code c - Char.code '0')) "" rest with _ -> "#"^rest) + | _ -> failwith "Variable name not found" + in match varM.d with | None -> "⊥\n" | Some arr when EConj.is_top_con arr -> "⊤\n" From dfeb71537c731b2c839afe04df1379f799f74fb5 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Wed, 22 May 2024 14:59:16 +0200 Subject: [PATCH 17/53] sign errors corrected --- .../apron/linearTwoVarEqualityDomain.apron.ml | 40 +++++++++++++------ 1 file changed, 27 insertions(+), 13 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 6346dc0975..d51bebb332 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -41,7 +41,8 @@ module Rhs = struct let gcd = match v with | Some (c,_) -> Z.gcd c gcd | None -> gcd - in (BatOption.map (fun (coeff,i) -> (Z.div coeff gcd,i)) v,Z.div o gcd, Z.div d gcd) + in let gcd = if (Z.(lt d Z.zero)) then Z.neg gcd else gcd in + (BatOption.map (fun (coeff,i) -> (Z.div coeff gcd,i)) v,Z.div o gcd, Z.div d gcd) (** Substitute rhs for varx in rhs' *) let subst rhs varx rhs' = @@ -238,7 +239,7 @@ module EqualitiesConjunction = struct 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.trace "meet" "meet_with_one_conj conj: { %s } eq: var_%d=%s -> { %s } " (show (snd ts)) i (Rhs.show (var,offs,divi)) (show (snd ts)) + if M.tracing then M.trace "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 ts)) ; res (** affine transform variable i allover conj with transformer (Some (coeff,i)+offs)/divi *) @@ -331,6 +332,12 @@ struct let constant = List.fold_left accumulate_constants (Z.zero,Z.one) monomiallist in (* abstract simplification of the guard wrt. reference variables *) Some (Array.fold_lefti (fun list v (c) -> if Q.equal c Q.zero then list else (c.num,v,c.den)::list) [] 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,divisor)) -> @@ -403,15 +410,22 @@ struct (** 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 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 transl = [|"₀";"₁";"₂";"₃";"₄";"₅";"₆";"₇";"₈";"₉"|] in + let res = Var.to_string (Environment.var_of_dim env i) in + match String.split_on_char '#' res with + | varname::rest::[] -> varname ^ (try String.fold_left (fun acc c -> acc ^ transl.(Char.code c - Char.code '0')) "" rest with _ -> "#"^rest) + | _ -> failwith "Variable name not found" + (** prints the current variable equalities with resolved variable names *) let show varM = - let lookup i = - let transl = [|"₀";"₁";"₂";"₃";"₄";"₅";"₆";"₇";"₈";"₉"|] in - let res = Var.to_string (Environment.var_of_dim varM.env i) in - match String.split_on_char '#' res with - | varname::rest::[] -> varname ^ (try String.fold_left (fun acc c -> acc ^ transl.(Char.code c - Char.code '0')) "" rest with _ -> "#"^rest) - | _ -> failwith "Variable name not found" - in match varM.d with | None -> "⊥\n" | Some arr when EConj.is_top_con arr -> "⊤\n" @@ -419,7 +433,7 @@ 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\nequalities\n\n\n%s\n\nenv\n\n\n%s\n\n\n" (XmlUtil.escape (Format.asprintf "%s" (show x) )) (XmlUtil.escape (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (x.env))) @@ -437,7 +451,7 @@ struct 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.trace "meet" "%s with single eq %s=%s -> %s" (show t) (show_var t.env i) (Rhs.show_rhs_formatted (show_var t.env) e) (show res); res let meet t1 t2 = @@ -517,7 +531,7 @@ struct in let iterate map l = match l with - | (idx_h, _, _, rhs_h, _) :: t -> List.fold (fun acc e -> modify acc idx_h rhs_h e) map l + | (idx_h, _, _, rhs_h, _) :: t -> List.fold (fun acc e -> modify acc idx_h rhs_h e) map l | [] -> let exception EmptyComponent in raise EmptyComponent in Some (List.fold iterate (EConj.make_empty_conj @@ fst ad) new_components) @@ -717,7 +731,7 @@ struct 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.(divi*constant),Z.(coeff*divisor))) + 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 *) | [(c1,var1,d1); (c2,var2,d2)] -> (* two variables in relation needs a little sorting out *) From c6928c58a426674077bd38a5a02149edefc89745 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Wed, 22 May 2024 15:10:02 +0200 Subject: [PATCH 18/53] do not enforce pattern on variable names --- src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index d51bebb332..60e8f50d9d 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -422,7 +422,7 @@ struct let res = Var.to_string (Environment.var_of_dim env i) in match String.split_on_char '#' res with | varname::rest::[] -> varname ^ (try String.fold_left (fun acc c -> acc ^ transl.(Char.code c - Char.code '0')) "" rest with _ -> "#"^rest) - | _ -> failwith "Variable name not found" + | _ -> res (** prints the current variable equalities with resolved variable names *) let show varM = From ada7065af6bd9c276a0de59e96822bdf0ff4e504 Mon Sep 17 00:00:00 2001 From: Michael Petter Date: Wed, 22 May 2024 22:44:09 +0200 Subject: [PATCH 19/53] migration to appendix A - join (part 1) --- .../apron/linearTwoVarEqualityDomain.apron.ml | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 60e8f50d9d..8f9694de2c 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -503,7 +503,21 @@ struct - 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 = let coeff = Option.map_default fst Z.one in match rhs1, rhs2 with + let joinfunction lhs rhs1 rhs2 = + let pairing = match rhs1,rhs2 with (* first of all re-instantiate implicit sparse elements *) + | Some a, Some b -> Some (a,b) + | None, Some b -> Some (Rhs.var_zero lhs,b) + | Some a, None -> Some (a,Rhs.var_zero lhs) + | _ -> None + in let _= BatOption.map (function + | (Some (c1,var1),o1,d1) as r1 ,(Some (c2,var2),o2,d2) as r2 -> lhs, Q.one, Q.one, r1, r2 + | (None, o1,d1) as r1, (Some (c2,var2),o2,d2) as r2 -> lhs, Q.one, Q.one, r1, r2 + | (Some (c1,var1),o1,d1) as r1, (None ,o2,d2) as r2 -> lhs, Q.one, Q.one, r1, r2 + | (None, o1,d1) as r1, (None ,o2,d2) as r2 -> + let magicnumber=Z.((o1/d1)-(o2/d2)) in + lhs, Q.make Z.(o1/magicnumber) Z.one,Q.make Z.(o1 mod magicnumber) Z.one,r1, r2 + ) pairing in () ; + let coeff = Option.map_default fst Z.one in match rhs1, rhs2 with (* Compute Ax+B such that (coeff1*(Ax+B)+off1)/d1 = (coeff2*x+off2)/d2 *) (* ====> A = (coeff2*d1)/(coeff1*d2) /\ B = (off2*d1-off1*d2)/(c1*c2) *) (* lhs A B rhs1 rhs2 *) From 366b04c2e2244276fde4963089da372c26439451 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Wed, 22 May 2024 15:39:15 +0200 Subject: [PATCH 20/53] error in tracing --- src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 8f9694de2c..e953a420a4 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -239,7 +239,7 @@ module EqualitiesConjunction = struct 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.trace "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 ts)) + if M.tracing then M.trace "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 *) @@ -451,7 +451,7 @@ struct 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" "%s with single eq %s=%s -> %s" (show t) (show_var t.env i) (Rhs.show_rhs_formatted (show_var t.env) 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 = From cb3b486b680ceff271afc0afda68a9b639bfb01d Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Thu, 23 May 2024 09:19:21 +0200 Subject: [PATCH 21/53] join of two different constants still remains in one equivalence class --- src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index e953a420a4..a5d27fec39 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -343,7 +343,7 @@ struct (fun (sum_of_terms, (constant,divisor)) -> (match sum_of_terms with | [] -> Some (None, constant,divisor) - | [(coeff,var,divi)] when Z.equal coeff Z.one -> Some (Rhs.canonicalize (Some (Z.mul divisor coeff,var), Z.mul constant divi,Z.mul divisor divi)) + | [(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 @@ -514,8 +514,7 @@ struct | (None, o1,d1) as r1, (Some (c2,var2),o2,d2) as r2 -> lhs, Q.one, Q.one, r1, r2 | (Some (c1,var1),o1,d1) as r1, (None ,o2,d2) as r2 -> lhs, Q.one, Q.one, r1, r2 | (None, o1,d1) as r1, (None ,o2,d2) as r2 -> - let magicnumber=Z.((o1/d1)-(o2/d2)) in - lhs, Q.make Z.(o1/magicnumber) Z.one,Q.make Z.(o1 mod magicnumber) Z.one,r1, r2 + lhs, Q.make Z.((o1*d2)-(o2*d1)) Z.(d1*d2), Q.zero, r1, r2 ) pairing in () ; let coeff = Option.map_default fst Z.one in match rhs1, rhs2 with (* Compute Ax+B such that (coeff1*(Ax+B)+off1)/d1 = (coeff2*x+off2)/d2 *) @@ -543,9 +542,9 @@ struct let coeff1 = Option.map_default fst Z.one monom1 in (Some (Z.(coeff1*divi),x), Z.((z1*refcoeff)-(offs*coeff1)), Z.(refcoeff*d1)) ) in - let iterate map l = + let iterate map l = match l with - | (idx_h, _, _, rhs_h, _) :: t -> List.fold (fun acc e -> modify acc idx_h rhs_h e) map l + | (idx_h, a, b, rhs_h, _) :: t -> M.trace "join" " join me in dept %s %s" (Q.to_string a) (Q.to_string b); List.fold (fun acc e -> modify acc idx_h rhs_h e) map l | [] -> let exception EmptyComponent in raise EmptyComponent in Some (List.fold iterate (EConj.make_empty_conj @@ fst ad) new_components) From 58c4e7dc08079b10fbe553b69e359485dfc4f930 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Thu, 23 May 2024 10:33:52 +0200 Subject: [PATCH 22/53] made join criteria much more legible --- .../apron/linearTwoVarEqualityDomain.apron.ml | 37 +++++++------------ 1 file changed, 14 insertions(+), 23 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index a5d27fec39..ff4d19414f 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -499,32 +499,23 @@ 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 affine transformation from refvar1 to refvar2, i.E. the parameters A and B of the general affine transformer Ax+B + - 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 = - let pairing = match rhs1,rhs2 with (* first of all re-instantiate implicit sparse elements *) - | Some a, Some b -> Some (a,b) - | None, Some b -> Some (Rhs.var_zero lhs,b) - | Some a, None -> Some (a,Rhs.var_zero lhs) - | _ -> None - in let _= BatOption.map (function - | (Some (c1,var1),o1,d1) as r1 ,(Some (c2,var2),o2,d2) as r2 -> lhs, Q.one, Q.one, r1, r2 - | (None, o1,d1) as r1, (Some (c2,var2),o2,d2) as r2 -> lhs, Q.one, Q.one, r1, r2 - | (Some (c1,var1),o1,d1) as r1, (None ,o2,d2) as r2 -> lhs, Q.one, Q.one, r1, r2 - | (None, o1,d1) as r1, (None ,o2,d2) as r2 -> - lhs, Q.make Z.((o1*d2)-(o2*d1)) Z.(d1*d2), Q.zero, r1, r2 - ) pairing in () ; - let coeff = Option.map_default fst Z.one in match rhs1, rhs2 with - (* Compute Ax+B such that (coeff1*(Ax+B)+off1)/d1 = (coeff2*x+off2)/d2 *) - (* ====> A = (coeff2*d1)/(coeff1*d2) /\ B = (off2*d1-off1*d2)/(c1*c2) *) - (* lhs A B rhs1 rhs2 *) - (*TODO*: if this works, make it more concise *) - | Some (ai,aj,ak), Some (bi,bj,bk) -> Some (lhs,Q.make Z.(ak*coeff bi) Z.(bk* coeff ai),Q.make Z.(bj*ak-aj*bk) Z.(bk*coeff ai), (ai,aj,ak) , (bi,bj,bk)) (* this is explicitely what we want *) - | None , Some (bi,bj,bk) -> Some (lhs,Q.make Z.( coeff bi) Z.(bk ),Q.make Z.(bj ) Z.(bk ), Rhs.var_zero lhs, (bi,bj,bk)) (* account for the sparseity of binding 1 *) - | Some (ai,aj,ak), None -> Some (lhs,Q.make Z.(ak ) Z.( coeff ai),Q.make Z.( neg aj) Z.( coeff ai), (ai,aj,ak), 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 *) + (match rhs1,rhs2 with (* first of all re-instantiate implicit sparse elements *) + | Some a, Some b -> Some (a,b) + | None, Some b -> Some (Rhs.var_zero lhs,b) + | Some a, None -> Some (a,Rhs.var_zero lhs) + | _ -> None) + |> + 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 affine function parameters a, b and reference variable indices *) @@ -544,7 +535,7 @@ struct in let iterate map l = match l with - | (idx_h, a, b, rhs_h, _) :: t -> M.trace "join" " join me in dept %s %s" (Q.to_string a) (Q.to_string b); List.fold (fun acc e -> modify acc idx_h rhs_h e) map l + | (idx_h, a, b, rhs_h, _) :: t -> M.trace "join" " iterate through equivalence group with a=%s and b=%s" (Q.to_string a) (Q.to_string b); List.fold (fun acc e -> modify acc idx_h rhs_h e) map l | [] -> let exception EmptyComponent in raise EmptyComponent in Some (List.fold iterate (EConj.make_empty_conj @@ fst ad) new_components) From b5fed0874204e5f12e90eceaa23601653c35dae8 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Thu, 23 May 2024 16:32:21 +0200 Subject: [PATCH 23/53] added case distinction for equivalence classes --- src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index ff4d19414f..e49b3a0f93 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -535,7 +535,11 @@ struct in let iterate map l = match l with - | (idx_h, a, b, rhs_h, _) :: t -> M.trace "join" " iterate through equivalence group with a=%s and b=%s" (Q.to_string a) (Q.to_string b); List.fold (fun acc e -> modify acc idx_h rhs_h e) map l + | (x, a, b, ((Some _,_,_) as rhs), ((Some _,_,_) as rhs')) :: t -> M.trace "join" "handle var-var equivalence group"; List.fold (fun acc e -> modify acc x rhs e) map l + | (x, a, b, ((Some _,_,_) as rhs), ((None,_,_) as rhs')) :: t -> M.trace "join" "handle var-const equivalence group"; List.fold (fun acc e -> modify acc x rhs e) map l + | (x, a, b, ((None,_,_) as rhs), ((Some _,_,_) as rhs')) :: t -> M.trace "join" "handle const-var equivalence group"; List.fold (fun acc e -> modify acc x rhs e) map l + | (x, a, b, ((None,o1,d1) as rhs), ((None,o2,d2) )) :: t when (o1,d1)=(o2,d2) -> M.trace "join" "handle const-const equivalence group" ; List.fold (fun acc e -> modify acc x rhs e) map l + | (x, a, b, ((None,_,_) as rhs), ((None,_,_) as rhs')) :: t -> M.trace "join" "handle const1-const2 equivalence group" ; List.fold (fun acc e -> modify acc x rhs e) map l | [] -> let exception EmptyComponent in raise EmptyComponent in Some (List.fold iterate (EConj.make_empty_conj @@ fst ad) new_components) From 083d1ea88a95cf0277ae8cbfeff07c658ff4b83c Mon Sep 17 00:00:00 2001 From: Michael Petter Date: Thu, 23 May 2024 20:13:37 +0200 Subject: [PATCH 24/53] satisfy semgrep --- src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index e49b3a0f93..89cead570b 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -535,11 +535,11 @@ struct in let iterate map l = match l with - | (x, a, b, ((Some _,_,_) as rhs), ((Some _,_,_) as rhs')) :: t -> M.trace "join" "handle var-var equivalence group"; List.fold (fun acc e -> modify acc x rhs e) map l - | (x, a, b, ((Some _,_,_) as rhs), ((None,_,_) as rhs')) :: t -> M.trace "join" "handle var-const equivalence group"; List.fold (fun acc e -> modify acc x rhs e) map l - | (x, a, b, ((None,_,_) as rhs), ((Some _,_,_) as rhs')) :: t -> M.trace "join" "handle const-var equivalence group"; List.fold (fun acc e -> modify acc x rhs e) map l - | (x, a, b, ((None,o1,d1) as rhs), ((None,o2,d2) )) :: t when (o1,d1)=(o2,d2) -> M.trace "join" "handle const-const equivalence group" ; List.fold (fun acc e -> modify acc x rhs e) map l - | (x, a, b, ((None,_,_) as rhs), ((None,_,_) as rhs')) :: t -> M.trace "join" "handle const1-const2 equivalence group" ; List.fold (fun acc e -> modify acc x rhs e) map l + | (x, a, b, ((Some _,_,_) as rhs), ((Some _,_,_) as rhs')) :: t -> if M.tracing then M.trace "join" "handle var-var equivalence group"; List.fold (fun acc e -> modify acc x rhs e) map l + | (x, a, b, ((Some _,_,_) as rhs), ((None,_,_) as rhs')) :: t -> if M.tracing then M.trace "join" "handle var-const equivalence group"; List.fold (fun acc e -> modify acc x rhs e) map l + | (x, a, b, ((None,_,_) as rhs), ((Some _,_,_) as rhs')) :: t -> if M.tracing then M.trace "join" "handle const-var equivalence group"; List.fold (fun acc e -> modify acc x rhs e) map l + | (x, a, b, ((None,o1,d1) as rhs), ((None,o2,d2) )) :: t when (o1,d1)=(o2,d2) -> if M.tracing then M.trace "join" "handle const-const equivalence group" ; List.fold (fun acc e -> modify acc x rhs e) map l + | (x, a, b, ((None,_,_) as rhs), ((None,_,_) as rhs')) :: t -> if M.tracing then M.trace "join" "handle const1-const2 equivalence group" ; List.fold (fun acc e -> modify acc x rhs e) map l | [] -> let exception EmptyComponent in raise EmptyComponent in Some (List.fold iterate (EConj.make_empty_conj @@ fst ad) new_components) From c6336515f17183f95e9dfc8a20e225067f94cc06 Mon Sep 17 00:00:00 2001 From: Michael Petter Date: Thu, 23 May 2024 22:13:41 +0200 Subject: [PATCH 25/53] join carried out for const cases --- .../apron/linearTwoVarEqualityDomain.apron.ml | 26 +++++++++---------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 89cead570b..6967d0371d 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -525,21 +525,21 @@ struct in (* Calculate new components as groups *) let new_components = BatList.group cmp_z table in - (* Adjust the domain map to represent the new components *) - let modify map x (refmonom, offs, divi) (idx, _, _, (monom1, z1, d1), (monom2, z2, d2)) = EConj.set_rhs map (idx) - (if monom1 = monom2 && Z.equal z1 z2 && Z.equal d1 d2 then (monom1, z1, d1) - else - let refcoeff = Option.map_default fst Z.one refmonom in - let coeff1 = Option.map_default fst Z.one monom1 in - (Some (Z.(coeff1*divi),x), Z.((z1*refcoeff)-(offs*coeff1)), Z.(refcoeff*d1)) ) - in + + (* 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 + let anum=a.num and aden=a.den and bnum=b.num and bden=b.den in + Rhs.canonicalize (Some (Z.(anum*bden),xh),Z.(bnum*aden) ,Z.(aden*bden) ) in let iterate map l = match l with - | (x, a, b, ((Some _,_,_) as rhs), ((Some _,_,_) as rhs')) :: t -> if M.tracing then M.trace "join" "handle var-var equivalence group"; List.fold (fun acc e -> modify acc x rhs e) map l - | (x, a, b, ((Some _,_,_) as rhs), ((None,_,_) as rhs')) :: t -> if M.tracing then M.trace "join" "handle var-const equivalence group"; List.fold (fun acc e -> modify acc x rhs e) map l - | (x, a, b, ((None,_,_) as rhs), ((Some _,_,_) as rhs')) :: t -> if M.tracing then M.trace "join" "handle const-var equivalence group"; List.fold (fun acc e -> modify acc x rhs e) map l - | (x, a, b, ((None,o1,d1) as rhs), ((None,o2,d2) )) :: t when (o1,d1)=(o2,d2) -> if M.tracing then M.trace "join" "handle const-const equivalence group" ; List.fold (fun acc e -> modify acc x rhs e) map l - | (x, a, b, ((None,_,_) as rhs), ((None,_,_) as rhs')) :: t -> if M.tracing then M.trace "join" "handle const1-const2 equivalence group" ; List.fold (fun acc e -> modify acc x rhs e) map l + | (h, _, _, ((Some (ch,_),oh,dh)), ((Some _,_,_) )) :: t -> if M.tracing then M.trace "join" "handle var-var class"; List.fold (fun acc e -> acc) map t + | (h, _, _, ((Some (ch,_),oh,dh)), ((None,_,_) )) :: t -> if M.tracing then M.trace "join" "handle var-const class"; List.fold (fun acc e -> acc) map t + | (h, _, _, ((None,_,_) ), ((Some (ch,_),oh,dh))) :: t -> if M.tracing then M.trace "join" "handle const-var class"; List.fold (fun acc e -> acc) map t + | (_, _, _, rhs , rhs' ) :: t when rhs=rhs' -> if M.tracing then M.trace "join" "handle const-const class" ; List.fold (fun acc (x,_,_,rh,_) -> EConj.set_rhs acc x rh) map l + | (h, _, _, ((None,oh1,dh1) ), ((None),oh2,dh2) ) :: t -> if M.tracing then M.trace "join" "handle const1-const2 class" ; 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) From 9e4cd5892b9ba8f9ed1d0c97e4d16586b7bdfcc8 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Fri, 24 May 2024 09:53:34 +0200 Subject: [PATCH 26/53] migration to appendix A - join (part 2) --- .../apron/linearTwoVarEqualityDomain.apron.ml | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 6967d0371d..2e3b473fcc 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -525,21 +525,25 @@ struct in (* Calculate new components as groups *) let new_components = BatList.group cmp_z table in - + 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 (* 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 + let b = Q.(ci2 - a*ch2) in let anum=a.num and aden=a.den and bnum=b.num and bden=b.den in Rhs.canonicalize (Some (Z.(anum*bden),xh),Z.(bnum*aden) ,Z.(aden*bden) ) in let iterate map l = match l with - | (h, _, _, ((Some (ch,_),oh,dh)), ((Some _,_,_) )) :: t -> if M.tracing then M.trace "join" "handle var-var class"; List.fold (fun acc e -> acc) map t - | (h, _, _, ((Some (ch,_),oh,dh)), ((None,_,_) )) :: t -> if M.tracing then M.trace "join" "handle var-const class"; List.fold (fun acc e -> acc) map t - | (h, _, _, ((None,_,_) ), ((Some (ch,_),oh,dh))) :: t -> if M.tracing then M.trace "join" "handle const-var class"; List.fold (fun acc e -> acc) map t - | (_, _, _, rhs , rhs' ) :: t when rhs=rhs' -> if M.tracing then M.trace "join" "handle const-const class" ; List.fold (fun acc (x,_,_,rh,_) -> EConj.set_rhs acc x rh) map l - | (h, _, _, ((None,oh1,dh1) ), ((None),oh2,dh2) ) :: t -> if M.tracing then M.trace "join" "handle const1-const2 class" ; 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 + | (h, _, _, ((Some (ch,_),oh,dh)), ((Some _,_,_) )) :: t -> List.fold (fun acc (i,_,_,(Some (ci,_),oi,di),_) -> EConj.set_rhs acc i (varentry Q.(make ci 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,_,_,(Some (ci,_),oi,di),_) -> EConj.set_rhs acc i (varentry Q.(make ci 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,_,_,_,(Some (ci,_),oi,di)) -> EConj.set_rhs acc i (varentry Q.(make ci di) Q.(make oi di) Q.(make ch dh) Q.(make oh dh) h)) map t + | (_, _, _, rhs , rhs' ) :: t when rhs=rhs' -> List.fold (fun acc (x,_,_,rh,_) -> EConj.set_rhs acc x rh) map l + | (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) From e290d3c2556fc91ec4a5f3371c65f8e2d23b5036 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Fri, 24 May 2024 10:07:28 +0200 Subject: [PATCH 27/53] added regression test for coefficient-heavy transactions --- .../77-lin2vareq/34-coefficient-features.c | 69 +++++++++++++++++++ 1 file changed, 69 insertions(+) create mode 100644 tests/regression/77-lin2vareq/34-coefficient-features.c 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..4a0469a40d --- /dev/null +++ b/tests/regression/77-lin2vareq/34-coefficient-features.c @@ -0,0 +1,69 @@ +//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 + + for(i = 1; i < 100; i++) { + x=x+4; + y=y+8; + + __goblint_check(y == 2*x); //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 (5*b == 20*unknown + a){ + + __goblint_check(5*b == 20*unknown + a); //SUCCESS + } + + b = unknown ? a*c : 4*c; + + __goblint_check(b == 4*c); //SUCCESS + + loop(); + +} \ No newline at end of file From 9de6f858fcdf8526208e5041aba22036517365ee Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Fri, 24 May 2024 10:59:26 +0200 Subject: [PATCH 28/53] make coefficents in regression coprime, and flex with propagation of 2var relations --- tests/regression/77-lin2vareq/34-coefficient-features.c | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/tests/regression/77-lin2vareq/34-coefficient-features.c b/tests/regression/77-lin2vareq/34-coefficient-features.c index 4a0469a40d..b415f4398a 100644 --- a/tests/regression/77-lin2vareq/34-coefficient-features.c +++ b/tests/regression/77-lin2vareq/34-coefficient-features.c @@ -26,6 +26,10 @@ void loop() { y=y+8; __goblint_check(y == 2*x); //SUCCESS + + int res = (y==2*x )+ 1; + + __goblint_check(res); //SUCCESS } x=0; @@ -55,9 +59,9 @@ void main() { __goblint_check(b == 4*c); //SUCCESS - if (5*b == 20*unknown + a){ + if (7*b == 20*unknown + a){ - __goblint_check(5*b == 20*unknown + a); //SUCCESS + __goblint_check(7*b == 20*unknown + a); //SUCCESS } b = unknown ? a*c : 4*c; From 3291633f1a1dde4fff71751ac567f5986b05d0e1 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Fri, 24 May 2024 11:00:06 +0200 Subject: [PATCH 29/53] wave through var-var equivalences if var1=var2 --- src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 2e3b473fcc..8dc4a71e90 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -539,10 +539,10 @@ struct Rhs.canonicalize (Some (Z.(anum*bden),xh),Z.(bnum*aden) ,Z.(aden*bden) ) in let iterate map l = match l with + | (_, _, _, rhs , rhs' ) :: t when 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,_,_,(Some (ci,_),oi,di),_) -> EConj.set_rhs acc i (varentry Q.(make ci 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,_,_,(Some (ci,_),oi,di),_) -> EConj.set_rhs acc i (varentry Q.(make ci 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,_,_,_,(Some (ci,_),oi,di)) -> EConj.set_rhs acc i (varentry Q.(make ci di) Q.(make oi di) Q.(make ch dh) Q.(make oh dh) h)) map t - | (_, _, _, rhs , rhs' ) :: t when rhs=rhs' -> List.fold (fun acc (x,_,_,rh,_) -> EConj.set_rhs acc x rh) map l | (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 From 83d7fb8f263a64b71e10872ae5691d56e08ee327 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Fri, 24 May 2024 11:05:21 +0200 Subject: [PATCH 30/53] removed warning 8 --- src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 8dc4a71e90..9d744ad926 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -540,9 +540,9 @@ struct let iterate map l = match l with | (_, _, _, rhs , rhs' ) :: t when 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,_,_,(Some (ci,_),oi,di),_) -> EConj.set_rhs acc i (varentry Q.(make ci 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,_,_,(Some (ci,_),oi,di),_) -> EConj.set_rhs acc i (varentry Q.(make ci 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,_,_,_,(Some (ci,_),oi,di)) -> EConj.set_rhs acc i (varentry Q.(make ci di) Q.(make oi di) Q.(make ch dh) Q.(make oh dh) h)) map t + | (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 From 16c8e6567a09836a684e56c0a3fcd8a5a55a0933 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Fri, 24 May 2024 13:25:47 +0200 Subject: [PATCH 31/53] got rid of unnecessarily largearray --- .../apron/linearTwoVarEqualityDomain.apron.ml | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 9d744ad926..d3beadbb9f 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -290,7 +290,6 @@ struct 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 @@ -322,15 +321,15 @@ struct BatOption.bind (monomials_from_texp t texp) (fun monomiallist -> let d = Option.get t.d in - let expr = Array.make (Environment.size t.env) (Q.zero) in (*TODO*: migrate to map; array of coeff/divisor per var idx*) - let accumulate_constants (aconst,adiv) (v,offs,divi) = match v with - | None -> let gcdee = Z.gcd adiv divi in (Z.(aconst*divi/gcdee + offs*adiv/gcdee),Z.lcm adiv divi) + 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! *) - (Option.may (fun (coef,ter) -> expr.(ter) <- Q.(expr.(ter) + Q.make coef somedivi)) somevar; - let gcdee = Z.gcd adiv divi in (Z.(aconst*divi/gcdee + offs*adiv/gcdee),Z.lcm adiv divi)) + let newcache = Option.map_default (fun (coef,ter) -> EConj.IntMap.add ter Q.((EConj.IntMap.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,Z.one) monomiallist in (* abstract simplification of the guard wrt. reference variables *) - Some (Array.fold_lefti (fun list v (c) -> if Q.equal c Q.zero then list else (c.num,v,c.den)::list) [] expr, constant) ) + let (expr,constant) = List.fold_left accumulate_constants (EConj.IntMap.empty,(Z.zero,Z.one)) monomiallist in (* abstract simplification of the guard wrt. reference variables *) + Some (EConj.IntMap.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 @@ -348,7 +347,6 @@ struct 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 divi = match t.d with | None -> t | Some t_d -> {d = Some (EConj.set_rhs t_d var (None, const, divi)); env = t.env} From aded7d59eaa7153134b6f71ed89aae85e9eea893 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Fri, 24 May 2024 14:03:46 +0200 Subject: [PATCH 32/53] rm redundancies --- src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index d3beadbb9f..5bd68cc858 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -416,10 +416,9 @@ struct subscr i let show_var env i = - let transl = [|"₀";"₁";"₂";"₃";"₄";"₅";"₆";"₇";"₈";"₉"|] in let res = Var.to_string (Environment.var_of_dim env i) in match String.split_on_char '#' res with - | varname::rest::[] -> varname ^ (try String.fold_left (fun acc c -> acc ^ transl.(Char.code c - Char.code '0')) "" rest with _ -> "#"^rest) + | varname::rest::[] -> varname ^ (try to_subscript @@ int_of_string rest with _ -> "#" ^ rest) | _ -> res (** prints the current variable equalities with resolved variable names *) From 26419aa1bd1645cbb766be67464f60b7c2e73610 Mon Sep 17 00:00:00 2001 From: Michael Petter Date: Fri, 24 May 2024 15:30:28 +0200 Subject: [PATCH 33/53] Update src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml make repopulation of the sparse conjunction more concise Co-authored-by: Michael Schwarz --- src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 5bd68cc858..d73d9cf783 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -501,11 +501,11 @@ struct - 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 (* first of all re-instantiate implicit sparse elements *) - | Some a, Some b -> Some (a,b) - | None, Some b -> Some (Rhs.var_zero lhs,b) - | Some a, None -> Some (a,Rhs.var_zero lhs) - | _ -> None) + ( + 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 From 49895fe04666fdfa4a82d3a7323c7692931ccbfd Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Fri, 24 May 2024 15:25:25 +0200 Subject: [PATCH 34/53] replace = with more specialized Rhs.equal --- src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index d73d9cf783..b2beb9fab9 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -536,7 +536,7 @@ struct Rhs.canonicalize (Some (Z.(anum*bden),xh),Z.(bnum*aden) ,Z.(aden*bden) ) in let iterate map l = match l with - | (_, _, _, rhs , rhs' ) :: t when rhs=rhs' -> List.fold (fun acc (x,_,_,rh,_) -> EConj.set_rhs acc x rh) 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 From 7e2a741eedcb942c16720181ebd37f7d1a849cf3 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Fri, 24 May 2024 15:27:52 +0200 Subject: [PATCH 35/53] gotten rid of silly record deconstruction --- src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index b2beb9fab9..090f31718e 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -532,8 +532,7 @@ struct let constentry ci1 ci2 ch1 ch2 xh = let a = Q.((ci1-ci2) / (ch1-ch2)) in let b = Q.(ci2 - a*ch2) in - let anum=a.num and aden=a.den and bnum=b.num and bden=b.den in - Rhs.canonicalize (Some (Z.(anum*bden),xh),Z.(bnum*aden) ,Z.(aden*bden) ) 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 | (_, _, _, rhs , rhs' ) :: t when Rhs.equal rhs rhs' -> List.fold (fun acc (x,_,_,rh,_) -> EConj.set_rhs acc x rh) map l From 62e569b0767332a8321d735f91b213977629171d Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Fri, 24 May 2024 15:34:53 +0200 Subject: [PATCH 36/53] make indentation happy again --- src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 090f31718e..23ee5056be 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -504,8 +504,8 @@ struct ( 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)) + | 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 From 4810b5da346eb66ae59d59063a6961710b0138b4 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Fri, 24 May 2024 15:39:19 +0200 Subject: [PATCH 37/53] make gcd more compact --- src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 23ee5056be..266f8e0505 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -38,10 +38,8 @@ module Rhs = struct (** factor out gcd from all terms, i.e. ax=by+c is the canonical form for adx+bdy+cd *) let canonicalize (v,o,d) = let gcd = Z.gcd o d in - let gcd = match v with - | Some (c,_) -> Z.gcd c gcd - | None -> gcd - in let gcd = if (Z.(lt d Z.zero)) then Z.neg gcd else gcd in + let gcd = Option.map_default (fun (c,_) -> Z.gcd c gcd) gcd v in + let gcd = if (Z.(lt d Z.zero)) then Z.neg gcd else gcd in (BatOption.map (fun (coeff,i) -> (Z.div coeff gcd,i)) v,Z.div o gcd, Z.div d gcd) (** Substitute rhs for varx in rhs' *) From 98ae9a4bb46b0976e9491b91f3bb2d50b6c0319a Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Fri, 24 May 2024 15:49:00 +0200 Subject: [PATCH 38/53] explain canonicalization --- src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 266f8e0505..5aef1b1371 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -37,10 +37,10 @@ module Rhs = struct (** factor out gcd from all terms, i.e. ax=by+c is the canonical form for adx+bdy+cd *) let canonicalize (v,o,d) = - let gcd = Z.gcd o d in - let gcd = Option.map_default (fun (c,_) -> Z.gcd c gcd) gcd v in - let gcd = if (Z.(lt d Z.zero)) then Z.neg gcd else gcd in - (BatOption.map (fun (coeff,i) -> (Z.div coeff gcd,i)) v,Z.div o gcd, Z.div d gcd) + 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 (* cannonical 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' = From 55c15f74bcffa6adc5d8360b1a9d88be1f7b0a31 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Fri, 24 May 2024 16:21:23 +0200 Subject: [PATCH 39/53] printf tuning --- src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 5aef1b1371..50fdf54d99 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -29,7 +29,7 @@ module Rhs = struct else (Z.to_string c) ^"·" let show_rhs_formatted formatter = 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%+Ld" (show_coeff coeff) (formatter v) (Z.to_int64 o) + | (Some (coeff,v), o,_) -> Printf.sprintf "%s%s%+Lu" (show_coeff coeff) (formatter v) (Z.to_int64_unsigned o) | (None, o,_) -> Printf.sprintf "%Ld" (Z.to_int64 o) let show (v,o,d) = let rhs=show_rhs_formatted (Printf.sprintf "var_%d") (v,o,d) in From 9078c2a6e087e8ae7ef5bf30d2d01f6caee168da Mon Sep 17 00:00:00 2001 From: Michael Petter Date: Sat, 25 May 2024 22:33:36 +0200 Subject: [PATCH 40/53] oversight of %+, so lets do it the affeq way --- src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 50fdf54d99..81ae290f66 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -27,9 +27,10 @@ module Rhs = struct 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 = function + 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%+Lu" (show_coeff coeff) (formatter v) (Z.to_int64_unsigned o) + | (Some (coeff,v), o,_) -> Printf.sprintf "%s%s %s" (show_coeff coeff) (formatter v) (ztostring o) | (None, o,_) -> Printf.sprintf "%Ld" (Z.to_int64 o) let show (v,o,d) = let rhs=show_rhs_formatted (Printf.sprintf "var_%d") (v,o,d) in From e0e9c3436e8652df23476e177b22e6e507e9ab7e Mon Sep 17 00:00:00 2001 From: Michael Petter Date: Sat, 25 May 2024 23:02:13 +0200 Subject: [PATCH 41/53] point out IMap has nothing directly to do with EConj --- src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 81ae290f66..f89a8d39ba 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -316,19 +316,20 @@ struct | x -> Some(x) (** 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 = + 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 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) -> EConj.IntMap.add ter Q.((EConj.IntMap.find_default zero ter exprcache) + make coef somedivi) exprcache) exprcache somevar in + 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 (expr,constant) = List.fold_left accumulate_constants (EConj.IntMap.empty,(Z.zero,Z.one)) monomiallist in (* abstract simplification of the guard wrt. reference variables *) - Some (EConj.IntMap.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 (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 From c6ec44bb6686c0123cfd819892fa15607a024cb2 Mon Sep 17 00:00:00 2001 From: Michael Petter Date: Sat, 25 May 2024 23:13:37 +0200 Subject: [PATCH 42/53] more concise subst --- src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index f89a8d39ba..87446a7b6b 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -46,8 +46,7 @@ module Rhs = struct (** Substitute rhs for varx in rhs' *) let subst rhs varx rhs' = match rhs,rhs' with - | (Some (c,x),o,d),(Some (c',x'),o',d') when x'=varx -> canonicalize (Some (Z.mul c c',x),Z.((o*c')+(d*o')),Z.mul d d') - | (None ,o,d),(Some (c',x'),o',d') when x'=varx -> canonicalize (None ,Z.((o*c')+(d*o')),Z.mul d d') + | (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 From 6f02c2ab45d901bc78eedf35908b1bc9f7dd71ce Mon Sep 17 00:00:00 2001 From: Michael Petter Date: Sat, 25 May 2024 23:24:20 +0200 Subject: [PATCH 43/53] rm faulty eval_int answer --- .../apron/linearTwoVarEqualityDomain.apron.ml | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 87446a7b6b..99fc69a0a5 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -158,8 +158,8 @@ module EqualitiesConjunction = struct List.fold (fun map i -> let (oldref,c',a') = (get_rhs d i) in let (b',_) = BatOption.get oldref in - let newrhs = (Some (Z.(b'*a),head), Z.(c' - (b' * c)), Z.(a'*b)) in - canonicalize_and_set map i newrhs + (Some (Z.(b'*a),head), Z.(c' - (b' * c)), Z.(a'*b)) |> + canonicalize_and_set map i ) d cluster (* shift offset to match new reference variable *) | [] -> d) (* empty cluster means no work for us *) | _ -> d) (* variable is either a constant or expressed by another refvar *) in @@ -364,13 +364,6 @@ struct | 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) - | Some (None, offset, divisor) -> let res = Z.div offset divisor in - let (lower,upper) = if Z.lt res Z.zero then - (Z.pred res,res) - else - (res,Z.succ res) in - (if M.tracing then M.tracel "bounds" "min: %s max: %s" (IntOps.BigIntOps.to_string lower) (IntOps.BigIntOps.to_string upper); - Some lower, Some upper) | _ -> None, None let bound_texpr d texpr1 = timing_wrap "bounds calculation" (bound_texpr d) texpr1 From 31bb80289111c688bbfc04cbf27a9965d1c43ca8 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Mon, 27 May 2024 16:11:30 +0200 Subject: [PATCH 44/53] rm Z.t->int conv issues --- src/cdomains/apron/gobApron.apron.ml | 7 +++++++ src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 6 +++--- 2 files changed, 10 insertions(+), 3 deletions(-) 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 99fc69a0a5..08358005b4 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -31,7 +31,7 @@ module Rhs = struct 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 "%Ld" (Z.to_int64 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 @@ -798,12 +798,12 @@ struct let get_const acc i = function | (None, o, d) -> let xi = Environment.var_of_dim t.env i in - of_coeff xi [(Coeff.s_of_int (- (Z.to_int d)), xi)] o :: acc + 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 (- (Z.to_int d)), xi); (Coeff.s_of_int @@ Z.to_int c, 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 [] From ec3deedeef7eba8f2e6f8f8d03c71cb1e500910e Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Tue, 28 May 2024 14:59:19 +0200 Subject: [PATCH 45/53] wrong brackets --- src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 08358005b4..0a110a5999 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -27,7 +27,7 @@ module Rhs = struct 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 + 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) From 075f2e858293e899f6f27f066629d27a2f62b306 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Tue, 28 May 2024 15:57:04 +0200 Subject: [PATCH 46/53] fix unmatched monom in forget_variable --- .../apron/linearTwoVarEqualityDomain.apron.ml | 6 ++++-- .../regression/77-lin2vareq/34-coefficient-features.c | 11 ----------- 2 files changed, 4 insertions(+), 13 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 0a110a5999..2da7deb5cc 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -104,7 +104,7 @@ module EqualitiesConjunction = struct let offsetlist = Array.to_list indexes in let rec bumpvar delta i = function (* bump the variable i by delta; find delta by counting indices in offsetlist until we reach a larger index then our current parameter *) | head::rest when i>=head -> bumpvar (delta+1) i rest (* rec call even when =, in order to correctly interpret double bumps *) - | _ (* i op i delta + | _ (* i let res = op i delta in res in let memobumpvar = (* Memoized version of bumpvar *) let module IntHash = struct type t = int [@@deriving eq,hash] end in @@ -145,9 +145,11 @@ module EqualitiesConjunction = struct (let ref_var_opt = Tuple3.first (get_rhs d var) in match ref_var_opt with | 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,_,_) l -> if ref = ref_var_opt then i::l else l) (snd d) [] in + (fun i (ref,_,_) l -> BatOption.map_default (fun (coeff,ref) -> if (ref=ref_var) then i::l else l) l ref) (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 :: _ -> diff --git a/tests/regression/77-lin2vareq/34-coefficient-features.c b/tests/regression/77-lin2vareq/34-coefficient-features.c index b415f4398a..561eccf0af 100644 --- a/tests/regression/77-lin2vareq/34-coefficient-features.c +++ b/tests/regression/77-lin2vareq/34-coefficient-features.c @@ -21,17 +21,6 @@ void loop() { __goblint_check(x == 4*i); //SUCCESS - for(i = 1; i < 100; i++) { - x=x+4; - y=y+8; - - __goblint_check(y == 2*x); //SUCCESS - - int res = (y==2*x )+ 1; - - __goblint_check(res); //SUCCESS - } - x=0; y=0; From 94ebf865fc261825d3d137f4d8203a5da8be1ba3 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Wed, 29 May 2024 10:57:03 +0200 Subject: [PATCH 47/53] fixed broken is_top --- src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 2da7deb5cc..f6ae9b2c51 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -400,7 +400,7 @@ 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 @@ -472,8 +472,8 @@ struct | 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 *) From 9663b1c772277fc3eb80b1a0ce4e3b7fd19bf46d Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Wed, 29 May 2024 13:17:04 +0200 Subject: [PATCH 48/53] make combine tracing in relational analysis more specific --- src/analyses/apron/relationAnalysis.apron.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index 6c118dac7a..97fd66d676 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) = From caa8437fcbdbd2182c2f8a6aa50ea33a72ad58cb Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Wed, 29 May 2024 13:18:04 +0200 Subject: [PATCH 49/53] forget did not forget about the actual head-variable of the new cluster --- src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index f6ae9b2c51..d2489689e1 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -152,17 +152,18 @@ module EqualitiesConjunction = struct 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 :: _ -> + | head :: clusterrest -> (* ax = by + c /\ a'z = b'y + c' *) (* ==[[ y:=? ]]==> (a'b)z = (b'a)x + c' -(b'c) *) let (newref,c,a) = (get_rhs d head) in (* take offset between old and new reference variable *) let (b,_) = BatOption.get newref in - List.fold (fun map i -> + let shifted_cluster = (List.fold (fun map i -> (* shift offset to match new reference variable *) let (oldref,c',a') = (get_rhs d i) in let (b',_) = BatOption.get oldref in (Some (Z.(b'*a),head), Z.(c' - (b' * c)), Z.(a'*b)) |> canonicalize_and_set map i - ) d cluster (* shift offset to match new reference variable *) + ) 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 *) From e1462b308d7695b37ac9041b1a465c70bdc15657 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Wed, 29 May 2024 14:58:40 +0200 Subject: [PATCH 50/53] fixed forget_variable by a) sorting vars in cluster and b) rehauling cluster transformation with subst/inverse convenience functions --- .../apron/linearTwoVarEqualityDomain.apron.ml | 22 +++++++++---------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index d2489689e1..923229ca96 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -147,21 +147,21 @@ module EqualitiesConjunction = struct | 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 + (let cluster = List.sort (Int.compare) @@ IntMap.fold (fun i (ref,_,_) l -> BatOption.map_default (fun (coeff,ref) -> if (ref=ref_var) then i::l else l) l ref) (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 :: clusterrest -> - (* ax = by + c /\ a'z = b'y + c' *) - (* ==[[ y:=? ]]==> (a'b)z = (b'a)x + c' -(b'c) *) - let (newref,c,a) = (get_rhs d head) in (* take offset between old and new reference variable *) - let (b,_) = BatOption.get newref in - let shifted_cluster = (List.fold (fun map i -> (* shift offset to match new reference variable *) - let (oldref,c',a') = (get_rhs d i) in - let (b',_) = BatOption.get oldref in - (Some (Z.(b'*a),head), Z.(c' - (b' * c)), Z.(a'*b)) |> - canonicalize_and_set map i + (* 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 *) @@ -240,7 +240,7 @@ module EqualitiesConjunction = struct 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.trace "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)) + 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 *) From aed4cec86fb4c66c8b134ff9ea7a420327e49fb3 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Mon, 10 Jun 2024 14:00:18 +0200 Subject: [PATCH 51/53] added treatment of speculative computations in relational analyses --- src/cdomains/apron/sharedFunctions.apron.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index 827dc252fc..e163ebf8ff 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -104,12 +104,13 @@ struct let texpr1_expr_of_cil_exp (ask:Queries.ask) d env exp no_ov = let conv exp = let query e ik = + if M.tracing then M.trace "relation-query" "before: texpr1_expr_of_cil_exp/query: %a" d_plainexp e; let res = match ask.f (EvalInt e) with | `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 *) @@ -138,10 +139,12 @@ struct 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 *) let simplify e = + AnalysisState.executing_speculative_computations := true; 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 if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp/simplify: %a -> %a" d_plainexp e IntDomain.IntDomTuple.pretty simp; + AnalysisState.executing_speculative_computations := false; BatOption.map_default (fun c -> Const (CInt (c, ikind, None))) e const in let texpr1 e = texpr1_expr_of_cil_exp (simplify e) in From 3df598090095223e6c4394bb271fa21e440861f8 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Tue, 11 Jun 2024 10:22:39 +0200 Subject: [PATCH 52/53] tweaks from MS' PR comments --- .../apron/linearTwoVarEqualityDomain.apron.ml | 61 +++++++++---------- src/cdomains/apron/sharedFunctions.apron.ml | 4 +- 2 files changed, 30 insertions(+), 35 deletions(-) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 923229ca96..069983344e 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -36,17 +36,17 @@ module Rhs = struct 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 is the canonical form for adx+bdy+cd *) + (** 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 (* cannonical form dictates d being positive *) - (BatOption.map (fun (coeff,i) -> (Z.div coeff commondivisor,i)) v,Z.div o commondivisor, Z.div d commondivisor) + 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') + | (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 @@ -59,7 +59,7 @@ module EqualitiesConjunction = struct let show_formatted formatter econ = if IntMap.is_empty econ then "{}" else - let str = IntMap.fold (fun i (ref,off,divi) acc -> Printf.sprintf "%s%s=%s ∧ %s" (Rhs.show_coeff divi) (formatter i) (Rhs.show_rhs_formatted formatter (ref,off,divi)) 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 @@ -76,7 +76,7 @@ module EqualitiesConjunction = struct 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)) + 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 @@ -89,10 +89,9 @@ module EqualitiesConjunction = struct IntMap.add lhs rhs map ) - (** canonicalize equation, and set_rhs, staying loyal to immutable, sparse map underneath,*) + (** 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) - (** add a new equality to the domain *) let copy = identity @@ -104,7 +103,7 @@ module EqualitiesConjunction = struct let offsetlist = Array.to_list indexes in let rec bumpvar delta i = function (* bump the variable i by delta; find delta by counting indices in offsetlist until we reach a larger index then our current parameter *) | head::rest when i>=head -> bumpvar (delta+1) i rest (* rec call even when =, in order to correctly interpret double bumps *) - | _ (* i let res = op i delta in res + | _ (* i op i delta in let memobumpvar = (* Memoized version of bumpvar *) let module IntHash = struct type t = int [@@deriving eq,hash] end in @@ -117,7 +116,8 @@ module EqualitiesConjunction = struct IntHashtbl.add h x r; r) in - let rec bumpentry k (refvar,offset,divi) = function (* directly bumps lhs-variable during a run through indexes, bumping refvar explicitely with a new lookup in indexes *) + 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 @@ -148,7 +148,7 @@ module EqualitiesConjunction = struct if M.tracing then M.trace "forget" "headvar var_%d" var; (* var is the reference variable of its connected component *) (let cluster = List.sort (Int.compare) @@ IntMap.fold - (fun i (ref,_,_) l -> BatOption.map_default (fun (coeff,ref) -> if (ref=ref_var) then i::l else l) l ref) (snd d) [] in + (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 *) @@ -157,7 +157,7 @@ module EqualitiesConjunction = struct (* 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 (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] *) @@ -198,14 +198,15 @@ module EqualitiesConjunction = struct 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 (vary, o, d) = + 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 (c',varx), o',d') when varx = x -> Rhs.canonicalize (BatOption.map (fun (c,y)->(Z.mul c c',y)) vary, Z.((c'*o)+(o'*d)),Z.(d'*d)) + | (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 (vary, o, d) @@ 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 (match var, (get_rhs ts i) with (*| new conj , old conj *) @@ -230,8 +231,8 @@ module EqualitiesConjunction = struct | (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 no unite the two equvalence classes; let's decide upon the representant *) + 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 @@ -244,13 +245,10 @@ module EqualitiesConjunction = struct ; res (** affine transform variable i allover conj with transformer (Some (coeff,i)+offs)/divi *) - let affine_transform econ i (var,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 (var,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 *) - match var with - | None -> failwith "this is not a valid affine transformation" - | Some (coeff,j) -> (* 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 -> @@ -276,12 +274,10 @@ struct let open Apron.Texpr1 in let exception NotLinearExpr in let exception ScalarIsInfinity in - let negate coeff_var_list = List.map (function - | (Some(coeff,i),offs,divi) -> (Some(Z.neg coeff,i),Z.neg offs,divi) - | (None ,offs,divi) -> (None ,Z.neg offs,divi)) coeff_var_list in - let multiply_with_Q dividend divisor coeff_var_list = List.map (function - | (Some (coeff, var),offs,divi) -> Rhs.canonicalize (Some(Z.mul dividend coeff,var),Z.(dividend * offs),Z.mul divi divisor) - | (None,offs,divi) -> Rhs.canonicalize (None,Z.mul dividend offs,Z.mul divi divisor)) 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 @@ -614,7 +610,7 @@ struct 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 (Some (coeff_var, var_i), off, divi)); env=t.env } + {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) @@ -742,10 +738,11 @@ struct | 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 (Z.neg @@ Z.(c1*divisor),var1),Z.neg @@ Z.(constant*d2*d1),Z.(c2*divisor*d1))) + 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 (Z.neg @@ Z.(c2*divisor),var2),Z.neg @@ Z.(constant*d2*d1),Z.(c1*divisor*d2))) + 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 *)) diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index e163ebf8ff..6b1993d381 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -104,7 +104,6 @@ struct let texpr1_expr_of_cil_exp (ask:Queries.ask) d env exp no_ov = let conv exp = let query e ik = - if M.tracing then M.trace "relation-query" "before: texpr1_expr_of_cil_exp/query: %a" d_plainexp e; let res = match ask.f (EvalInt e) with | `Bot -> raise (Unsupported_CilExp Exp_not_supported) (* This should never happen according to Michael Schwarz *) @@ -139,12 +138,11 @@ struct 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 *) let simplify e = - AnalysisState.executing_speculative_computations := true; + 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 if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp/simplify: %a -> %a" d_plainexp e IntDomain.IntDomTuple.pretty simp; - AnalysisState.executing_speculative_computations := false; BatOption.map_default (fun c -> Const (CInt (c, ikind, None))) e const in let texpr1 e = texpr1_expr_of_cil_exp (simplify e) in From ca31b6e0eb0b7be74c359fd127e1267274836fef Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Tue, 11 Jun 2024 10:27:29 +0200 Subject: [PATCH 53/53] added explanation --- src/cdomains/apron/sharedFunctions.apron.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index 6b1993d381..8c94c996b0 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -136,7 +136,13 @@ 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