From 26237d093b9f8faa2ca97078d50cd3a567f9957d Mon Sep 17 00:00:00 2001 From: Philip Feniuk Date: Wed, 16 Jul 2025 22:16:56 +0200 Subject: [PATCH 01/10] Deriving hash and eq function; Verify in config set to true; removed ';;' --- conf/pentagon.json | 2 +- src/cdomains/apron/pentagonDomain.apron.ml | 145 +++++++++------------ src/cdomains/pentagon/boxes.ml | 5 +- src/cdomains/pentagon/pntg.ml | 4 +- src/cdomains/pentagon/subs.ml | 11 +- src/cdomains/pentagon/zExt.ml | 27 ++-- 6 files changed, 89 insertions(+), 105 deletions(-) diff --git a/conf/pentagon.json b/conf/pentagon.json index 93ef7536dd..6d46ec32a9 100644 --- a/conf/pentagon.json +++ b/conf/pentagon.json @@ -15,5 +15,5 @@ "space_restore": true } }, - "verify": false + "verify": true } diff --git a/src/cdomains/apron/pentagonDomain.apron.ml b/src/cdomains/apron/pentagonDomain.apron.ml index 89b5d5539c..f7c7353ad2 100644 --- a/src/cdomains/apron/pentagonDomain.apron.ml +++ b/src/cdomains/apron/pentagonDomain.apron.ml @@ -3,10 +3,6 @@ "Pentagons: A weakly relational abstract domain for the efficient validation of array accesses" -- Francesco Logozzo, Manuel Fähndrich (2010) *) -(* -TODO: Timing Wrap für alle Funktionen -*) - open Batteries open GoblintCil module M = Messages @@ -22,6 +18,9 @@ open Boxes open Subs open Pntg +(* Global function to enable or disable timing wrap. *) +let timing_wrap s f a = Timing.wrap s f a +(* let timing_wrap s f a = f a *) module Rhs = struct @@ -59,7 +58,6 @@ module Rhs = struct end - module type Tracked = sig val type_tracked: typ -> bool @@ -67,7 +65,6 @@ sig 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]. Furthermore, it provides the function [simplified_monomials_from_texp] that converts an apron expression into a list of monomials of reference variables and a constant offset *) module VarManagement = @@ -82,6 +79,7 @@ let z_ext_of_scalar (s: Scalar.t) = | Mpqf(mpqf) -> ZExt.of_float (Mpqf.to_float mpqf) | Mpfrf(mpfrf) -> ZExt.of_float (Mpfrf.to_float mpfrf) +(* Returns the current best approximation using the provided pentagon for the given texpr. *) let eval_texpr_to_intv (t: VarManagement.t) (texpr:Texpr1.expr) : Intv.t = let get_dim var = Environment.dim_of_var t.env var in let d = Option.get t.d in @@ -101,41 +99,9 @@ let eval_texpr_to_intv (t: VarManagement.t) (texpr:Texpr1.expr) : Intv.t = | Binop (Mod, e1, e2, _, _) -> Intv.rem (aux e1) (aux e2) | Binop (Pow, e1, e2, _, _) -> Intv.pow (aux e1) (aux e2) in - aux texpr;; - -(* We assume that the divisor is always 1, so we omit it and that t is not bottom. *) -let rec eval_monoms_to_intv boxes (terms, (constant, _)) = - match terms with - | [] -> Intv.create_const_of_z constant - | (coeff, index, _)::terms -> ( - let intv_coeff = Intv.create_const_of_z coeff in - Intv.add (Intv.mul intv_coeff (Boxes.get_value index boxes)) (eval_monoms_to_intv boxes (terms, (constant, Z.one))) - );; - - - -let eval_texpr_to_intv (t: VarManagement.t) (texpr:Texpr1.expr) : Intv.t = - let get_dim var = Environment.dim_of_var t.env var in - let d = Option.get t.d in - let boxes = d.boxes in - let rec aux texpr = - match texpr with - | Texpr1.Cst (Interval inv) -> (z_ext_of_scalar inv.inf, z_ext_of_scalar inv.sup) - | Cst (Scalar s) -> let s = z_ext_of_scalar s in (s, s) - | Var y -> List.at boxes (get_dim y) - | Unop (Cast, e, _, _) -> aux e - | Unop (Sqrt, e, _, _) -> failwith "Do the sqrt. :)" - | Unop (Neg, e, _, _) -> Intv.neg (aux e) - | Binop (Add, e1, e2, _, _) -> Intv.add (aux e1) (aux e2) - | Binop (Sub, e1, e2, _, _) -> Intv.sub (aux e1) (aux e2) - | Binop (Mul, e1, e2, _, _) -> Intv.mul (aux e1) (aux e2) - | Binop (Div, e1, e2, _, _) -> Intv.div (aux e1) (aux e2) - | Binop (Mod, e1, e2, _, _) -> Intv.rem (aux e1) (aux e2) - | Binop (Pow, e1, e2, _, _) -> Intv.pow (aux e1) (aux e2) - in - aux texpr;; - + aux texpr +(* let eval_texpr_to_intv t texpr = timing_wrap "eval_texpr_to_intv" (eval_texpr_to_intv t) texpr *) (* We assume that the divisor is always 1, so we omit it and that t is not bottom. *) let rec eval_monoms_to_intv boxes (terms, (constant, _)) = @@ -144,8 +110,9 @@ let rec eval_monoms_to_intv boxes (terms, (constant, _)) = | (coeff, index, _)::terms -> ( let intv_coeff = Intv.create_const_of_z coeff in Intv.add (Intv.mul intv_coeff (Boxes.get_value index boxes)) (eval_monoms_to_intv boxes (terms, (constant, Z.one))) - );; + ) +(* let eval_monoms_to_intv boxes monoms = timing_wrap "eval_monoms_to_intv" (eval_monoms_to_intv boxes) monoms *) type intv_infty_list = ZExt.t * Int.t list type ext_intv = intv_infty_list * intv_infty_list @@ -215,11 +182,11 @@ let rec eval_monoms_to_intv_infty_list boxes (terms, (constant, _)) : ext_intv = ) | lb -> ZExt.add c lb, l in - - (lb, ub) - );; + ) + +(* let eval_monoms_to_intv_infty_list boxes monoms = timing_wrap "eval_monoms_to_intv_infty_list" (eval_monoms_to_intv_infty_list boxes) monoms *) let ext_intv_to_intv (((c_lb, infty_list_lb), (c_ub, infty_list_ub)) : ext_intv) : Intv.t = let lb = ZExt.add c_lb (if infty_list_lb = [] then ZExt.zero else NegInfty) in @@ -271,10 +238,10 @@ First argument: Values of a variable corresponding to a term in the associated e Second argument: The evaluation of an expression as an extended intv. *) let eval_ext_intv_plus_x x ext_intv = - ext_intv_to_intv (ext_intv_plus_x x ext_intv);; + ext_intv_to_intv (ext_intv_plus_x x ext_intv) let eval_ext_intv_minus_x (coeff_x, x, x_intv) (ext_intv: ext_intv) = - eval_ext_intv_plus_x (Z.neg coeff_x, x, Intv.neg x_intv) (ext_intv);; + eval_ext_intv_plus_x (Z.neg coeff_x, x, Intv.neg x_intv) (ext_intv) let neg_ext_intv ((c1, lst1), (c2, lst2)) = (ZExt.neg c2, lst2), (ZExt.neg c1, lst1) @@ -289,19 +256,16 @@ module ExpressionBounds: (SharedFunctions.ConvBounds with type t = VarManagement struct include VarManagement - (* - TODO: Check if s1 > s2 to check for bot values. - *) let bound_texpr t texpr = let intv = (eval_texpr_to_intv t (Texpr1.to_expr texpr)) in if Intv.is_bot intv then failwith "BOT DETECTED!" else match intv with - | Arb s1, Arb s2 -> Some(s1), Some(s2) - | Arb s1, _ -> Some(s1), None - | _, Arb s2 -> None, Some(s2) + | ZExt.Arb s1, ZExt.Arb s2 -> Some(s1), Some(s2) + | ZExt.Arb s1, _ -> Some(s1), None + | _, ZExt.Arb s2 -> None, Some(s2) | _, _ -> None, None - let bound_texpr d texpr1 = Timing.wrap "bounds calculation" (bound_texpr d) texpr1 + (* let bound_texpr d texpr1 = timing_wrap "bound_texpr" (bound_texpr d) texpr1 *) end module D = @@ -327,11 +291,15 @@ struct | None -> true | Some d -> Boxes.is_bot d.boxes || Subs.is_bot d.subs + (* let is_bot t = timing_wrap "is_bot" (is_bot) t *) + let is_top t = match t.d with | None -> false | Some d -> Boxes.is_top d.boxes && Subs.is_top d.subs + (* let is_top t = timing_wrap "is_top" (is_top) t *) + let to_string t = if is_bot t then "⊥" @@ -354,22 +322,14 @@ struct (* First pass substitutes the variable names for the keys left to the arrow. *) Str.global_substitute key_re (varname_and_append "->") res |> (* Second pass adjusts the variable name for the subs sets. *) - Str.global_substitute subs_re (varname_and_append "");; + Str.global_substitute subs_re (varname_and_append "") - let show = to_string + (* let to_string t = timing_wrap "to_string" (to_string) t *) - let equal t1 t2 = - Environment.equal t1.env t2.env - && - match t1.d, t2.d with - | None, None -> true - | None, _ -> false - | _ , None -> false - | Some(d1), Some(d2) -> Pntg.equal d1 d2 + let show = to_string let pretty () (t:t) = text (show t) - let pretty_diff () (x, y) = dprintf "%s: %a not leq %a" (name ()) pretty x pretty y @@ -377,9 +337,6 @@ struct let printXml f (t:t) = BatPrintf.fprintf f "\n\n\npntg\n\n\n%s\n\nenv\n\n\n%a\n\n\n" (XmlUtil.escape (show t)) Environment.printXml t.env - (* - TODO: - *) let to_yojson t = failwith "TODO" (** @@ -415,7 +372,7 @@ struct if M.tracing then M.trace "pntg" "D.meet:\nt1:\t%s\nt2:\t%s\nres:\t%s\n\n" (show t1) (show t2) (show res); res - let meet t1 t2 = Timing.wrap "meet" (meet t1) t2 + let meet t1 t2 = timing_wrap "meet" (meet t1) t2 let leq t1 t2 = let sup_env = Environment.lce t1.env t2.env in @@ -446,7 +403,7 @@ struct if M.tracing then M.trace "pntg" "D.leq:\nt1:\t%s\nt2:\t%s\nres:\t%b\n\n" (show t1) (show t2) res; res - let leq a b = Timing.wrap "leq" (leq a) b + let leq a b = timing_wrap "leq" (leq a) b let join t1 t2 = let sup_env = Environment.lce t1.env t2.env in @@ -465,13 +422,13 @@ struct | None, Some d2' -> {d = Some d2'; env = sup_env} | _ -> {d = None; env = sup_env} - let join a b = Timing.wrap "join" (join a) b - let join a b = let res = join a b in if M.tracing then M.trace "pntg" "D.join:\nt1:\t%s\nt2:\t%s\nres:\t%s\n\n" (show a) (show b) (show res) ; res + let join a b = timing_wrap "join" (join a) b + let widen t1 t2 = let sup_env = Environment.lce t1.env t2.env in let t1 = dimchange2_add t1 sup_env in @@ -486,6 +443,8 @@ struct if M.tracing then M.trace "pntg" "D.widen:\nt1:\t%s\nt2:\t%s\nres:\t%s\n\n" (show a) (show b) (show res) ; res + let widen a b = timing_wrap "widen" (widen a) b + let narrow t1 t2 = meet t1 t2 let narrow a b = @@ -493,6 +452,8 @@ struct if M.tracing then M.trace "pntg" "D.narrow:\nt1:\t%s\nt2:\t%s\nres:\t%s\n\n" (show a) (show b) (show res) ; res + let narrow a b = timing_wrap "narrow" (narrow a) b + (* S2 Specific functions of RelationDomain *) let is_bot_env t = t.d = None @@ -501,7 +462,9 @@ struct else let (pntg: Pntg.t) = Option.get t.d in let int_vars = List.map (fun v -> Environment.dim_of_var t.env v) vars in - {d = Some({boxes = Boxes.forget_vars int_vars pntg.boxes; subs = Subs.forget_vars int_vars pntg.subs}); env=t.env};; + {d = Some({boxes = Boxes.forget_vars int_vars pntg.boxes; subs = Subs.forget_vars int_vars pntg.subs}); env=t.env} + + (* let forget_vars t vars = timing_wrap "forget_vars" (forget_vars t) vars *) (** Taken from lin2var and modified for our domain. *) (** Parses a Texpr to obtain a Rhs.t list to repr. a sum of a variables that have a coefficient. If variable is None, the coefficient represents a constant offset. *) @@ -541,7 +504,8 @@ struct | exception NotLinearExpr -> None | exception ScalarIsInfinity -> None | x -> Some(x) - ;; + + (* let monomials_from_texp env texp = timing_wrap "monomials_from_texp" (monomials_from_texp env) texp *) (** Taken from lin2var and modified for our domain. *) (** convert and simplify (wrt. reference variables) a texpr into a tuple of a list of monomials (coeff,varidx,divi) and a (constant/divi) *) @@ -558,12 +522,14 @@ struct in 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 env texp = timing_wrap "simplified_monomials_from_texp" (simplified_monomials_from_texp env) texp *) + (* TODO: discuss whether to implement the subtraction like the pentagon paper - (special case? different eval_monoms_to_intv that also uses relational information?) *) + (special case? different eval_monoms_to_intv that also uses relational information?) + *) let assign_texpr (t: t) x (texp: Texpr1.expr) : t = let wrap b s = {d=Some({boxes = b; subs = s}); env=t.env} in let x = Environment.dim_of_var t.env x in @@ -733,14 +699,14 @@ struct aux rem_terms subs_acc slbs_acc delete_subs_flag delete_slbs_flag in aux sum_of_terms Subs.VarSet.empty Subs.VarSet.empty true true - ;; + let assign_texpr t x texp = let res = assign_texpr t x texp in if M.tracing then M.trace "pntg" "D.assign_texpr:\nassign:\t%s := %s\nt:\t%s\nres:\t%s\n\n" (StringUtils.string_of_var x) (StringUtils.string_of_texpr1 texp) (show t) (show res); res - let assign_texpr t x texp = Timing.wrap "assign_texpr" (assign_texpr t x) texp + let assign_texpr t x texp = timing_wrap "assign_texpr" (assign_texpr t x) texp let assign_exp ask (t: VarManagement.t) var exp (no_ov: bool Lazy.t) = let t = if not @@ Environment.mem_var t.env var then add_vars t [var] else t in @@ -748,9 +714,13 @@ struct | texp -> assign_texpr t var texp | exception Convert.Unsupported_CilExp _ -> forget_vars t [var] + (* let assign_exp ask t var exp no_ov = timing_wrap "assign_exp" (assign_exp ask t var exp) no_ov *) + let assign_var t v v' = let t = add_vars t [v; v'] in - assign_texpr t v (Var v');; + assign_texpr t v (Var v') + + (* let assign_var t v v' = timing_wrap "assign_var" (assign_var t v) v' *) let assign_var_parallel (t: t) (var_tuples: (var * var) list) : t = @@ -765,6 +735,7 @@ struct remove_vars switched_arr primed_vars | _ -> t + (* let assign_var_parallel t var_tuples = timing_wrap "assign_var_parallel" (assign_var_parallel t) var_tuples *) (** Combines two var lists into a list of tuples and runs assign_var_parallel @@ -773,10 +744,14 @@ struct let var_tuples = List.combine vs1 vs2 in assign_var_parallel t var_tuples + (* let assign_var_parallel' t vs1 vs2 = timing_wrap "assign_var_parallel'" (assign_var_parallel' t vs1) vs2 *) + let assign_var_parallel_with t (var_tuples: (var * var) list) : unit = let t' = assign_var_parallel t var_tuples in t.d <- t'.d; - t.env <- t'.env;; + t.env <- t'.env + + (* let assign_var_parallel_with t var_tuples = timing_wrap "assign_var_parallel_with" (assign_var_parallel_with t) var_tuples *) let rec assert_constraint ask t tcons negate (no_ov: bool Lazy.t) = let wrap b s = {d=Some({boxes = b; subs=s}); env=t.env} in @@ -959,7 +934,7 @@ struct | _ -> assert_constraint ask t e negate no_ov ~trace:true - let assert_constraint ask t e negate no_ov = Timing.wrap "assert_constraint" (assert_constraint ask t e negate) no_ov + let assert_constraint ask t e negate no_ov = timing_wrap "assert_constraint" (assert_constraint ask t e negate) no_ov (* This function returns linear constraints of form: @@ -1032,19 +1007,23 @@ struct fun acc (var,intv,subs) -> acc @ (constraints_of_intv var intv) @ (constraints_of_subs var subs) ) [] - ;; + (* let invariant t = timing_wrap "invariant" invariant t *) (** Taken from lin2var. *) let substitute_exp ask (t:t) var exp no_ov = let t = if not @@ Environment.mem_var t.env var then add_vars t [var] else t in let res = assign_exp ask t var exp no_ov in forget_vars res [var] - ;; + + (* let substitute_exp ask t var exp no_ov = timing_wrap "substitute_exp" (substitute_exp ask t var exp) no_ov *) + (** Taken from lin2var. *) let unify pntg1 pntg2 = meet pntg1 pntg2 + (* let unify pntg1 pntg2 = timing_wrap "unify" (unify pntg1) pntg2 *) + type marshal = t let marshal t = t let unmarshal t = t @@ -1065,7 +1044,7 @@ struct else match t.d with | None -> failwith "is_bot should take care of that" - | Some(d) -> Pntg.to_string d;; + | Some(d) -> Pntg.to_string d end diff --git a/src/cdomains/pentagon/boxes.ml b/src/cdomains/pentagon/boxes.ml index 21bd2b0981..76441e9385 100644 --- a/src/cdomains/pentagon/boxes.ml +++ b/src/cdomains/pentagon/boxes.ml @@ -6,7 +6,7 @@ open StringUtils (** Provides functions and types for collections of Intv. *) module Boxes = struct - type t = Intv.t list [@@deriving eq, ord] + type t = Intv.t list [@@deriving eq, ord, hash] include ZExtOps let is_bot (i: t) = BatList.exists Intv.is_bot i @@ -29,9 +29,6 @@ struct in Printf.sprintf "%s { %s }" bot_or_top (String.concat "; " (List.mapi string_of_interval intervals)) - let equal boxes1 boxes2 = - BatList.for_all2 (Intv.equal) boxes1 boxes2 - let leq i1 i2 = BatList.for_all2 Intv.leq i1 i2 diff --git a/src/cdomains/pentagon/pntg.ml b/src/cdomains/pentagon/pntg.ml index e736210e60..ae21dc621a 100644 --- a/src/cdomains/pentagon/pntg.ml +++ b/src/cdomains/pentagon/pntg.ml @@ -8,10 +8,8 @@ open Subs module Pntg = struct - type t = { boxes: Boxes.t; subs: Subs.t } [@@deriving eq, ord] + type t = { boxes: Boxes.t; subs: Subs.t } [@@deriving eq, ord, hash] - let hash : (t -> int) = fun _ -> 1 - let equal pntg1 pntg2 = Boxes.equal pntg1.boxes pntg2.boxes && Subs.equal pntg1.subs pntg2.subs;; let copy (x: t) = x let empty () = { boxes = []; subs = [] } let is_empty pntg = diff --git a/src/cdomains/pentagon/subs.ml b/src/cdomains/pentagon/subs.ml index f79161a833..bce5c6abe7 100644 --- a/src/cdomains/pentagon/subs.ml +++ b/src/cdomains/pentagon/subs.ml @@ -8,7 +8,12 @@ module Subs = struct module Idx = Int - module VarSet = BatSet.Make(Idx) + module VarSet = struct + module IdxSet = BatSet.Make(Idx) + include IdxSet + let hash t = IdxSet.fold (fun idx acc -> acc lxor (19 * idx + 0x9e3779b9)) t 0 + end + module VarList = BatList module MoveMap = struct @@ -16,7 +21,7 @@ struct type t = Idx.t BatMap.Make(Idx).t end - type t = VarSet.t VarList.t [@@deriving eq, ord] + type t = VarSet.t list [@@deriving eq, ord, hash] let dim_add (dim_change: Apron.Dim.change) (subs: t) = if dim_change.realdim != 0 then @@ -77,8 +82,6 @@ struct in List.filteri_map move_or_delete_set subs - let equal (sub1: t) (sub2: t) = VarList.equal VarSet.equal sub1 sub2 - (** This isn't precise: we might return false even if there are transitive contradictions; Other possibility: compute transitive closure first (would be expensive) diff --git a/src/cdomains/pentagon/zExt.ml b/src/cdomains/pentagon/zExt.ml index d3df56ce41..073e9617a6 100644 --- a/src/cdomains/pentagon/zExt.ml +++ b/src/cdomains/pentagon/zExt.ml @@ -9,8 +9,8 @@ struct let hash (z: t) = match z with - | PosInfty -> failwith "ZExt.pow: TODO" - | NegInfty -> failwith "ZExt.pow: TODO" + | PosInfty -> 0x186e81bd (* random constant *) + | NegInfty -> 0xc8590e8 (* random constant *) | Arb(z) -> Z.hash z;; let equal (z1: t) (z2: t) = @@ -88,14 +88,21 @@ struct (** Alias for add z1 (neg z2) *) let sub z1 z2 = add z1 (neg z2) - let rem (Arb z1) (Arb z2) = Arb (Z.rem z1 z2) - - let rem_add (Arb z1) (Arb z2) = - let rem = Z.rem z1 z2 in - if Z.sign rem < 0 then - Arb (Z.add rem z2) - else - Arb(rem) + let rem zext1 zext2 = + match zext1, zext2 with + | Arb(z1), Arb(z2) -> + Arb (Z.rem z1 z2) + | _ -> failwith "ZExt.rem: Only applicable for two Arb values." + + let rem_add zext1 zext2 = + match zext1, zext2 with + | Arb(z1), Arb(z2) -> + let rem = Z.rem z1 z2 in + if Z.sign rem < 0 then + Arb (Z.add rem z2) + else + Arb(rem) + | _ -> failwith "ZExt.rem_add: Only applicable for two Arb values." let rec mul z1 z2 = match z1, z2 with From 3003524a1f4def43f9d69b1643f87a89cc93f10c Mon Sep 17 00:00:00 2001 From: Philip Feniuk Date: Wed, 16 Jul 2025 22:22:03 +0200 Subject: [PATCH 02/10] Add a todo to bound_texpr --- src/cdomains/apron/pentagonDomain.apron.ml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/cdomains/apron/pentagonDomain.apron.ml b/src/cdomains/apron/pentagonDomain.apron.ml index f7c7353ad2..ec1fe74c7f 100644 --- a/src/cdomains/apron/pentagonDomain.apron.ml +++ b/src/cdomains/apron/pentagonDomain.apron.ml @@ -257,6 +257,11 @@ struct include VarManagement let bound_texpr t texpr = + (* + TODO: Find out why this fixes things? + + None,None + *) let intv = (eval_texpr_to_intv t (Texpr1.to_expr texpr)) in if Intv.is_bot intv then failwith "BOT DETECTED!" else match intv with @@ -265,6 +270,7 @@ struct | _, ZExt.Arb s2 -> None, Some(s2) | _, _ -> None, None + (* let bound_texpr d texpr1 = timing_wrap "bound_texpr" (bound_texpr d) texpr1 *) end From d98722dd07fc5ae65ad64f70053c7be9ff21b11c Mon Sep 17 00:00:00 2001 From: Philip Feniuk Date: Wed, 16 Jul 2025 22:45:29 +0200 Subject: [PATCH 03/10] Printing texpr and intv for bound_texpr --- src/cdomains/apron/pentagonDomain.apron.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/cdomains/apron/pentagonDomain.apron.ml b/src/cdomains/apron/pentagonDomain.apron.ml index ec1fe74c7f..a5669a0e05 100644 --- a/src/cdomains/apron/pentagonDomain.apron.ml +++ b/src/cdomains/apron/pentagonDomain.apron.ml @@ -257,12 +257,15 @@ struct include VarManagement let bound_texpr t texpr = + let texpr = Texpr1.to_expr texpr in (* TODO: Find out why this fixes things? None,None *) - let intv = (eval_texpr_to_intv t (Texpr1.to_expr texpr)) in + Printf.printf "%s\n" (StringUtils.string_of_texpr1 texpr); + let intv = eval_texpr_to_intv t texpr in + Printf.printf "%s\n" (Intv.to_string intv); if Intv.is_bot intv then failwith "BOT DETECTED!" else match intv with | ZExt.Arb s1, ZExt.Arb s2 -> Some(s1), Some(s2) From 3e0821adf5bb450ed3f59617127ca155e8d0ab5d Mon Sep 17 00:00:00 2001 From: Alexander Mazur Date: Thu, 17 Jul 2025 13:52:24 +0200 Subject: [PATCH 04/10] work in progress --- src/cdomains/apron/pentagonDomain.apron.ml | 152 +++++++++++---------- 1 file changed, 81 insertions(+), 71 deletions(-) diff --git a/src/cdomains/apron/pentagonDomain.apron.ml b/src/cdomains/apron/pentagonDomain.apron.ml index a5669a0e05..da9ea4ce13 100644 --- a/src/cdomains/apron/pentagonDomain.apron.ml +++ b/src/cdomains/apron/pentagonDomain.apron.ml @@ -252,26 +252,96 @@ let string_of_infty_list (c, infty_list : intv_infty_list) = let string_of_ext_intv (ext_intv : intv_infty_list * intv_infty_list) = "[" ^ string_of_infty_list (fst ext_intv) ^ ", " ^ string_of_infty_list (snd ext_intv) ^ "]" +(** Taken from lin2var and modified for our domain. *) +(** Parses a Texpr to obtain a Rhs.t list to repr. a sum of a variables that have a coefficient. If variable is None, the coefficient represents a constant offset. *) +let monomials_from_texp env texp = + let open Apron.Texpr1 in + let exception NotLinearExpr in + let exception ScalarIsInfinity 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 + | [(None,coeff, divi)], c + | c, [(None,coeff, divi)] -> multiply_with_Q coeff divi c + | _ -> raise NotLinearExpr + in + let rec convert_texpr texp = + begin match texp with + | 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 -> [(None,x,Z.one)] + | None -> raise ScalarIsInfinity end + | Var x -> + let var_dim = Environment.dim_of_var env x in + [(Some (Z.one,var_dim),Z.zero,Z.one)] + | 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 *) + | Unop (Sqrt, e, _, _) -> raise NotLinearExpr + | Binop (Add, e1, e2, _, _) -> convert_texpr e1 @ convert_texpr e2 + | Binop (Sub, e1, e2, _, _) -> convert_texpr e1 @ negate (convert_texpr e2) + | Binop (Mul, e1, e2, _, _) -> multiply (convert_texpr e1) (convert_texpr e2) + | Binop _ -> raise NotLinearExpr end + in match convert_texpr texp with + | exception NotLinearExpr -> None + | exception ScalarIsInfinity -> None + | x -> Some(x) + +(* let monomials_from_texp env texp = timing_wrap "monomials_from_texp" (monomials_from_texp env) texp *) + +(** Taken from lin2var and modified for our domain. *) +(** 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 env texp = + BatOption.bind (monomials_from_texp env texp) + (fun monomiallist -> + let module IMap = BatMap.Make(Int) 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)= v,offs,divi in (* normalize! *) + let newcache = Option.map_default (fun (coef,ter) -> IMap.add ter Q.((IMap.find_default zero ter exprcache) + make coef somedivi) exprcache) exprcache somevar in + let gcdee = Z.gcd adiv divi in + (newcache,(Z.(aconst*divi/gcdee + offs*adiv/gcdee),Z.lcm adiv divi)) + in + let (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 env texp = timing_wrap "simplified_monomials_from_texp" (simplified_monomials_from_texp env) texp *) + module ExpressionBounds: (SharedFunctions.ConvBounds with type t = VarManagement.t) = struct include VarManagement let bound_texpr t texpr = let texpr = Texpr1.to_expr texpr in - (* - TODO: Find out why this fixes things? - - None,None - *) + (* Without linearisation *) Printf.printf "%s\n" (StringUtils.string_of_texpr1 texpr); let intv = eval_texpr_to_intv t texpr in Printf.printf "%s\n" (Intv.to_string intv); - if Intv.is_bot intv then failwith "BOT DETECTED!" else - match intv with - | ZExt.Arb s1, ZExt.Arb s2 -> Some(s1), Some(s2) - | ZExt.Arb s1, _ -> Some(s1), None - | _, ZExt.Arb s2 -> None, Some(s2) - | _, _ -> None, None + if Intv.is_bot intv then failwith "BOT DETECTED!" + else + + match t.d with + | None -> None, None + | Some d -> + match simplified_monomials_from_texp t.env texpr with + | None -> + (match intv with + | ZExt.Arb s1, ZExt.Arb s2 -> Some(s1), Some(s2) + | ZExt.Arb s1, _ -> Some(s1), None + | _, ZExt.Arb s2 -> None, Some(s2) + | _, _ -> None, None) + | Some monoms -> + let intv_lin = eval_monoms_to_intv d.boxes monoms in + match intv with + | ZExt.Arb s1, ZExt.Arb s2 -> Some(s1), Some(s2) + | ZExt.Arb s1, _ -> Some(s1), None + | _, ZExt.Arb s2 -> None, Some(s2) + | _, _ -> None, None (* let bound_texpr d texpr1 = timing_wrap "bound_texpr" (bound_texpr d) texpr1 *) @@ -475,66 +545,6 @@ struct (* let forget_vars t vars = timing_wrap "forget_vars" (forget_vars t) vars *) - (** Taken from lin2var and modified for our domain. *) - (** Parses a Texpr to obtain a Rhs.t list to repr. a sum of a variables that have a coefficient. If variable is None, the coefficient represents a constant offset. *) - let monomials_from_texp env texp = - let open Apron.Texpr1 in - let exception NotLinearExpr in - let exception ScalarIsInfinity 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 - | [(None,coeff, divi)], c - | c, [(None,coeff, divi)] -> multiply_with_Q coeff divi c - | _ -> raise NotLinearExpr - in - let rec convert_texpr texp = - begin match texp with - | 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 -> [(None,x,Z.one)] - | None -> raise ScalarIsInfinity end - | Var x -> - let var_dim = Environment.dim_of_var env x in - [(Some (Z.one,var_dim),Z.zero,Z.one)] - | 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 *) - | Unop (Sqrt, e, _, _) -> raise NotLinearExpr - | Binop (Add, e1, e2, _, _) -> convert_texpr e1 @ convert_texpr e2 - | Binop (Sub, e1, e2, _, _) -> convert_texpr e1 @ negate (convert_texpr e2) - | Binop (Mul, e1, e2, _, _) -> multiply (convert_texpr e1) (convert_texpr e2) - | Binop _ -> raise NotLinearExpr end - in match convert_texpr texp with - | exception NotLinearExpr -> None - | exception ScalarIsInfinity -> None - | x -> Some(x) - - (* let monomials_from_texp env texp = timing_wrap "monomials_from_texp" (monomials_from_texp env) texp *) - - (** Taken from lin2var and modified for our domain. *) - (** 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 env texp = - BatOption.bind (monomials_from_texp env texp) - (fun monomiallist -> - let module IMap = BatMap.Make(Int) 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)= v,offs,divi in (* normalize! *) - let newcache = Option.map_default (fun (coef,ter) -> IMap.add ter Q.((IMap.find_default zero ter exprcache) + make coef somedivi) exprcache) exprcache somevar in - let gcdee = Z.gcd adiv divi in - (newcache,(Z.(aconst*divi/gcdee + offs*adiv/gcdee),Z.lcm adiv divi)) - in - let (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 env texp = timing_wrap "simplified_monomials_from_texp" (simplified_monomials_from_texp env) texp *) - (* TODO: discuss whether to implement the subtraction like the pentagon paper (special case? different eval_monoms_to_intv that also uses relational information?) From 8e8bed2648c06d697bf8ac1d70ec997c832db8e7 Mon Sep 17 00:00:00 2001 From: Alexander Mazur Date: Thu, 17 Jul 2025 13:58:19 +0200 Subject: [PATCH 05/10] added consistency check between linearized and non-linearized interval evaluation --- src/cdomains/apron/pentagonDomain.apron.ml | 26 +++++++++++----------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/src/cdomains/apron/pentagonDomain.apron.ml b/src/cdomains/apron/pentagonDomain.apron.ml index da9ea4ce13..2e06020952 100644 --- a/src/cdomains/apron/pentagonDomain.apron.ml +++ b/src/cdomains/apron/pentagonDomain.apron.ml @@ -312,36 +312,36 @@ let simplified_monomials_from_texp env texp = (* let simplified_monomials_from_texp env texp = timing_wrap "simplified_monomials_from_texp" (simplified_monomials_from_texp env) texp *) +let to_z_intv (z_ext_intv : Intv.t) = + match z_ext_intv with + | ZExt.Arb s1, ZExt.Arb s2 -> Some(s1), Some(s2) + | ZExt.Arb s1, _ -> Some(s1), None + | _, ZExt.Arb s2 -> None, Some(s2) + | _, _ -> None, None + module ExpressionBounds: (SharedFunctions.ConvBounds with type t = VarManagement.t) = struct include VarManagement let bound_texpr t texpr = let texpr = Texpr1.to_expr texpr in - (* Without linearisation *) Printf.printf "%s\n" (StringUtils.string_of_texpr1 texpr); + (* Without linearization *) let intv = eval_texpr_to_intv t texpr in Printf.printf "%s\n" (Intv.to_string intv); if Intv.is_bot intv then failwith "BOT DETECTED!" else - match t.d with | None -> None, None | Some d -> match simplified_monomials_from_texp t.env texpr with - | None -> - (match intv with - | ZExt.Arb s1, ZExt.Arb s2 -> Some(s1), Some(s2) - | ZExt.Arb s1, _ -> Some(s1), None - | _, ZExt.Arb s2 -> None, Some(s2) - | _, _ -> None, None) + | None -> to_z_intv intv | Some monoms -> let intv_lin = eval_monoms_to_intv d.boxes monoms in - match intv with - | ZExt.Arb s1, ZExt.Arb s2 -> Some(s1), Some(s2) - | ZExt.Arb s1, _ -> Some(s1), None - | _, ZExt.Arb s2 -> None, Some(s2) - | _, _ -> None, None + let intersected_intvs = Intv.inter intv intv_lin in + if Intv.is_bot intersected_intvs + then failwith "Conflict between linearized and non-linearized evaluation" + else to_z_intv intv_lin (* let bound_texpr d texpr1 = timing_wrap "bound_texpr" (bound_texpr d) texpr1 *) From 538c94aff5619606a526f87880313eb708d11f34 Mon Sep 17 00:00:00 2001 From: DP Date: Thu, 17 Jul 2025 14:43:58 +0200 Subject: [PATCH 06/10] adapted narrowing for intb --- src/cdomains/pentagon/intv.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/cdomains/pentagon/intv.ml b/src/cdomains/pentagon/intv.ml index 8b00955b63..159e157ae2 100644 --- a/src/cdomains/pentagon/intv.ml +++ b/src/cdomains/pentagon/intv.ml @@ -149,8 +149,10 @@ struct let u = if u2 <=* u1 then u2 else ZExt.PosInfty in (l, u) - let narrow (i1: t) (i2: t) = - inter i1 i2 + let narrow (l1, u1) (l2, u2) = + let l = if l1 =* ZExt.NegInfty then l2 else l1 in + let u = if u2 =* ZExt.PosInfty then u2 else u1 in + (l, u) let lt ((_, ub1):t) ((lb2, _):t) = ub1 < lb2 From 51e1f83a9eaa138c24dec695db988db2088b9d45 Mon Sep 17 00:00:00 2001 From: DP Date: Thu, 17 Jul 2025 14:45:07 +0200 Subject: [PATCH 07/10] adapted boses --- src/cdomains/pentagon/boxes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdomains/pentagon/boxes.ml b/src/cdomains/pentagon/boxes.ml index 76441e9385..78b28922c5 100644 --- a/src/cdomains/pentagon/boxes.ml +++ b/src/cdomains/pentagon/boxes.ml @@ -42,7 +42,7 @@ struct BatList.map2 Intv.widen i1 i2 let narrow (i1: t) (i2: t) = - meet i1 i2 + BatList.map2 Intv.narrow i1 i2 let dim_add (dim_change: Apron.Dim.change) (intervals: t) = if dim_change.realdim != 0 then From 040f5dad894f7c3de271c3a75f9a721d377b0ee9 Mon Sep 17 00:00:00 2001 From: Philip Feniuk Date: Thu, 17 Jul 2025 16:27:50 +0200 Subject: [PATCH 08/10] Fixed conversion from scalar to zext; Fixed narrowing for Pntg; Added some explaining comments; Minor performance stuff; --- src/cdomains/apron/pentagonDomain.apron.ml | 464 ++++++++++----------- src/cdomains/pentagon/intv.ml | 12 + src/cdomains/pentagon/stringUtils.ml | 18 + 3 files changed, 257 insertions(+), 237 deletions(-) diff --git a/src/cdomains/apron/pentagonDomain.apron.ml b/src/cdomains/apron/pentagonDomain.apron.ml index 2e06020952..52bd375300 100644 --- a/src/cdomains/apron/pentagonDomain.apron.ml +++ b/src/cdomains/apron/pentagonDomain.apron.ml @@ -1,7 +1,12 @@ -(** Implementation of the pentagon domain (pntg) - @see - "Pentagons: A weakly relational abstract domain for the efficient validation of array accesses" - -- Francesco Logozzo, Manuel Fähndrich (2010) *) +(** + Implementation of the pentagon domain (pntg) + "Pentagons: A weakly relational abstract domain for the efficient validation of array accesses" + -- Francesco Logozzo, Manuel Fähndrich (2010) @see + + + We additionally took some inspiration from "Weakly Relational Numerical Abstract Domains" + -- Antoine MINÉ @see . +*) open Batteries open GoblintCil @@ -22,7 +27,6 @@ open Pntg let timing_wrap s f a = Timing.wrap s f a (* let timing_wrap s f a = f a *) - module Rhs = struct (* 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: @@ -72,13 +76,6 @@ struct include SharedFunctions.VarManagementOps (Pntg) end -(* Helper functions *) -let z_ext_of_scalar (s: Scalar.t) = - match s with - | Float(f) -> ZExt.of_float f - | Mpqf(mpqf) -> ZExt.of_float (Mpqf.to_float mpqf) - | Mpfrf(mpfrf) -> ZExt.of_float (Mpfrf.to_float mpfrf) - (* Returns the current best approximation using the provided pentagon for the given texpr. *) let eval_texpr_to_intv (t: VarManagement.t) (texpr:Texpr1.expr) : Intv.t = let get_dim var = Environment.dim_of_var t.env var in @@ -86,11 +83,24 @@ let eval_texpr_to_intv (t: VarManagement.t) (texpr:Texpr1.expr) : Intv.t = let boxes = d.boxes in let rec aux texpr = match texpr with - | Texpr1.Cst (Interval inv) -> (z_ext_of_scalar inv.inf, z_ext_of_scalar inv.sup) - | Cst (Scalar s) -> let s = z_ext_of_scalar s in (s, s) + | Texpr1.Cst (Interval inv) -> ( + let lb = SharedFunctions.int_of_scalar inv.inf in + let ub = SharedFunctions.int_of_scalar inv.sup in + match lb, ub with + | None, None -> Intv.top () + | None, Some(ub) -> ZExt.NegInfty, Arb ub + | Some(lb), None -> Arb lb, ZExt.PosInfty + | Some(lb), Some(ub) -> Arb lb, Arb ub + ) + | Cst (Scalar s) -> ( + let s = SharedFunctions.int_of_scalar s in + match s with + | None -> Intv.top () + | Some(s) -> (Arb s, Arb s) + ) | Var y -> List.at boxes (get_dim y) | Unop (Cast, e, _, _) -> aux e - | Unop (Sqrt, e, _, _) -> failwith "Do the sqrt. :)" + | Unop (Sqrt, e, _, _) -> failwith "We can not do the sqrt. :)" | Unop (Neg, e, _, _) -> Intv.neg (aux e) | Binop (Add, e1, e2, _, _) -> Intv.add (aux e1) (aux e2) | Binop (Sub, e1, e2, _, _) -> Intv.sub (aux e1) (aux e2) @@ -312,36 +322,20 @@ let simplified_monomials_from_texp env texp = (* let simplified_monomials_from_texp env texp = timing_wrap "simplified_monomials_from_texp" (simplified_monomials_from_texp env) texp *) -let to_z_intv (z_ext_intv : Intv.t) = - match z_ext_intv with - | ZExt.Arb s1, ZExt.Arb s2 -> Some(s1), Some(s2) - | ZExt.Arb s1, _ -> Some(s1), None - | _, ZExt.Arb s2 -> None, Some(s2) - | _, _ -> None, None - module ExpressionBounds: (SharedFunctions.ConvBounds with type t = VarManagement.t) = struct include VarManagement let bound_texpr t texpr = - let texpr = Texpr1.to_expr texpr in - Printf.printf "%s\n" (StringUtils.string_of_texpr1 texpr); - (* Without linearization *) - let intv = eval_texpr_to_intv t texpr in - Printf.printf "%s\n" (Intv.to_string intv); - if Intv.is_bot intv then failwith "BOT DETECTED!" - else - match t.d with - | None -> None, None - | Some d -> - match simplified_monomials_from_texp t.env texpr with - | None -> to_z_intv intv - | Some monoms -> - let intv_lin = eval_monoms_to_intv d.boxes monoms in - let intersected_intvs = Intv.inter intv intv_lin in - if Intv.is_bot intersected_intvs - then failwith "Conflict between linearized and non-linearized evaluation" - else to_z_intv intv_lin + match t.d with + | None -> None, None + | Some d -> + let texpr = Texpr1.to_expr texpr in + match simplified_monomials_from_texp t.env texpr with + | None -> + Intv.to_z_opt_intv (eval_texpr_to_intv t texpr) + | Some monoms -> + Intv.to_z_opt_intv (eval_monoms_to_intv d.boxes monoms) (* let bound_texpr d texpr1 = timing_wrap "bound_texpr" (bound_texpr d) texpr1 *) @@ -524,7 +518,14 @@ struct let widen a b = timing_wrap "widen" (widen a) b - let narrow t1 t2 = meet t1 t2 + let narrow t1 t2 = + let sup_env = Environment.lce t1.env t2.env in + let t1 = dimchange2_add t1 sup_env in + let t2 = dimchange2_add t2 sup_env in + match t1.d, t2.d with + | Some d1', Some d2' -> + ({d = Some {boxes = Boxes.narrow d1'.boxes d2'.boxes; subs =d1'.subs}; env = sup_env}: t) + | _ -> {d = None; env = sup_env} let narrow a b = let res = narrow a b in @@ -545,6 +546,7 @@ struct (* let forget_vars t vars = timing_wrap "forget_vars" (forget_vars t) vars *) + (* TODO: discuss whether to implement the subtraction like the pentagon paper (special case? different eval_monoms_to_intv that also uses relational information?) @@ -596,128 +598,124 @@ struct if divisor <> Z.one then failwith "assign_texpr: DIVISOR WAS NOT ONE" else let monoms = Option.get monoms in - let expr_intv = eval_monoms_to_intv d.boxes monoms in let expr_ext_intv = eval_monoms_to_intv_infty_list d.boxes monoms in + let expr_intv = ext_intv_to_intv expr_ext_intv in - if expr_intv <> ext_intv_to_intv expr_ext_intv then - failwith "ext_intv <> expr_intv" - else + let x_intv = Boxes.get_value x d.boxes in - let x_intv = Boxes.get_value x d.boxes in + let rec aux sum_of_terms (subs_acc : Subs.VarSet.t) (slbs_acc : Subs.VarSet.t) delete_subs_flag delete_slbs_flag = + match sum_of_terms with + | (_, _, div) :: _ when div <> Z.one -> failwith "assign_texpr: DIVISOR WAS NOT ONE" - let rec aux sum_of_terms (subs_acc : Subs.VarSet.t) (slbs_acc : Subs.VarSet.t) delete_subs_flag delete_slbs_flag = - match sum_of_terms with - | (_, _, div) :: _ when div <> Z.one -> failwith "assign_texpr: DIVISOR WAS NOT ONE" + (* We finished recursion through the linear expression. Time to set the subs and boxes for our pentagon. *) + | [] -> - (* We finished recursion through the linear expression. Time to set the subs and boxes for our pentagon. *) - | [] -> + (* If x after the assignment can be greater than the value of x before the assignment, we must delete its subs. *) + let delete_subs_flag = delete_subs_flag && Intv.sup expr_intv >* Intv.inf x_intv in - (* If x after the assignment can be greater than the value of x before the assignment, we must delete its subs. *) - let delete_subs_flag = delete_subs_flag && Intv.sup expr_intv >* Intv.inf x_intv in + (* If x after the assignment can be lower than the value of x before the assignment, we must delete its slbs. *) + let delete_slbs_flag = delete_slbs_flag && Intv.inf expr_intv <* Intv.sup x_intv in - (* If x after the assignment can be lower than the value of x before the assignment, we must delete its slbs. *) - let delete_slbs_flag = delete_slbs_flag && Intv.inf expr_intv <* Intv.sup x_intv in + (* Variables which are the upper bound of x. Remove x which might be wrongfully added. *) + let new_subs = Subs.VarSet.remove x subs_acc in - (* Variables which are the upper bound of x. Remove x which might be wrongfully added. *) - let new_subs = Subs.VarSet.remove x subs_acc in + (* Variables where x is the upper bound. *) + let new_slbs = slbs_acc in - (* Variables where x is the upper bound. *) - let new_slbs = slbs_acc in - - let update_subs y subs_y = - if y = x then (* y = x ==> update Subs(x) *) - if delete_subs_flag then - new_subs - else - Subs.VarSet.union subs_y new_subs - else (* y <> x ==> possibly add x to / delete x from Subs(y) *) - if Subs.VarSet.mem y new_slbs then - Subs.VarSet.add x subs_y else - if delete_slbs_flag then - Subs.VarSet.remove x subs_y + let update_subs y subs_y = + if y = x then (* y = x ==> update Subs(x) *) + if delete_subs_flag then + new_subs else - subs_y - in - wrap (Boxes.set_value x expr_intv d.boxes) (List.mapi update_subs d.subs) - - | (coefficient, x', _) :: rem_terms when x' = x -> (* x' := ax + ... *) - (* We analyze 0 >< (a-1)x + [c,d] because it is more precise than x >< ax + [c,d] *) - let (cmp_lb, cmp_ub) = - eval_ext_intv_minus_x (coefficient, x, x_intv) expr_ext_intv - in - (* x could have got greater *) - let delete_subs_flag = delete_subs_flag && cmp_ub >* ZExt.zero in - (* x could have got lower *) - let delete_slbs_flag = delete_slbs_flag && cmp_lb <* ZExt.zero - in - aux rem_terms subs_acc slbs_acc delete_subs_flag delete_slbs_flag - - | (coefficient, y, _) :: rem_terms -> (* x' := ay + ... *) - let y_intv = Boxes.get_value y d.boxes in (* BUG WAS HERE *) - - (* We analyze 0 >< (a-1)y + [c,d] because it is more precise than y >< ay + [c,d] *) - let (cmp_lb, cmp_ub) = - eval_ext_intv_minus_x (coefficient, y, y_intv) expr_ext_intv - in - - (* - x >= y + 1 (by Subs) - y + 1 >= x' (by cmp) - ==> x >= x' ==> we can keep Subs(x) - *) - let keep_subs_flag = - Subs.gt x y d.subs && ZExt.of_int 1 >=* cmp_ub in - let delete_subs_flag = - (* x could have got greater / we can't rule out x' > x *) - delete_subs_flag && not keep_subs_flag in - (* If x' is guaranteed to be less then / equal to x, we can keep the subs. - We want to know x' > x? - - In this case x' := ay + [c,d], therefore we get: - ay + [c, d] > x <===> -x + ay + [c,d] > 0 - - From x < y (y \in Subs(x)) we can derive - -x + ay + [c,d] > (a-1)y + [c,d] - - So if (a-1)y + [c,d] >= 0 is possible, x' > x is possible. *) - - (*if Subs.lt d.subs x y - then cmp_ub >=* ZExt.zero - else true in*) - - let keep_slbs_flag = - Subs.lt x y d.subs && ZExt.of_int (-1) <=* cmp_ub in - let delete_slbs_flag = - (* x could have got lower / we can't rule out x' < x *) - delete_slbs_flag && not keep_slbs_flag in - (*if Subs.gt d.subs x y - then cmp_lb <=* ZExt.zero - else true in*) - (* - analyze 0 >< (a-1)y + [c,d] - x' < y known: SUBs(x') := SUBs(x') u SUBs(y) u {y} - x' <= y known: SUBs(x') := SUBs(x') u SUBs(y) - x' > y known: SLBs(x') := SLBs(x') u {y} - - *) - let subs_y = Subs.get_value y d.subs in - (* - Caution: New subs can contain the old x. - This is not a contradiction, it just has to be deleted afterwards. + Subs.VarSet.union subs_y new_subs + else (* y <> x ==> possibly add x to / delete x from Subs(y) *) + if Subs.VarSet.mem y new_slbs then + Subs.VarSet.add x subs_y else + if delete_slbs_flag then + Subs.VarSet.remove x subs_y + else + subs_y + in + wrap (Boxes.set_value x expr_intv d.boxes) (List.mapi update_subs d.subs) + + | (coefficient, x', _) :: rem_terms when x' = x -> (* x' := ax + ... *) + (* We analyze 0 >< (a-1)x + [c,d] because it is more precise than x >< ax + [c,d] *) + let (cmp_lb, cmp_ub) = + eval_ext_intv_minus_x (coefficient, x, x_intv) expr_ext_intv + in + (* x could have got greater *) + let delete_subs_flag = delete_subs_flag && cmp_ub >* ZExt.zero in + (* x could have got lower *) + let delete_slbs_flag = delete_slbs_flag && cmp_lb <* ZExt.zero + in + aux rem_terms subs_acc slbs_acc delete_subs_flag delete_slbs_flag + + | (coefficient, y, _) :: rem_terms -> (* x' := ay + ... *) + let y_intv = Boxes.get_value y d.boxes in (* BUG WAS HERE *) + + (* We analyze 0 >< (a-1)y + [c,d] because it is more precise than y >< ay + [c,d] *) + let (cmp_lb, cmp_ub) = + eval_ext_intv_minus_x (coefficient, y, y_intv) expr_ext_intv + in + + (* + x >= y + 1 (by Subs) + y + 1 >= x' (by cmp) + ==> x >= x' ==> we can keep Subs(x) *) - let new_subs = - if cmp_ub <* ZExt.zero then - Subs.VarSet.union subs_y (Subs.VarSet.singleton y) - else if cmp_ub =* ZExt.zero then - subs_y - else - Subs.VarSet.empty - in - let subs_acc = Subs.VarSet.union subs_acc new_subs in - let slbs_acc = if cmp_lb >* ZExt.zero then Subs.VarSet.add y slbs_acc else slbs_acc in - aux rem_terms subs_acc slbs_acc delete_subs_flag delete_slbs_flag + let keep_subs_flag = + Subs.gt x y d.subs && ZExt.of_int 1 >=* cmp_ub in + let delete_subs_flag = + (* x could have got greater / we can't rule out x' > x *) + delete_subs_flag && not keep_subs_flag in + (* If x' is guaranteed to be less then / equal to x, we can keep the subs. + We want to know x' > x? + + In this case x' := ay + [c,d], therefore we get: + ay + [c, d] > x <===> -x + ay + [c,d] > 0 + + From x < y (y \in Subs(x)) we can derive + -x + ay + [c,d] > (a-1)y + [c,d] + + So if (a-1)y + [c,d] >= 0 is possible, x' > x is possible. *) + + (*if Subs.lt d.subs x y + then cmp_ub >=* ZExt.zero + else true in*) + + let keep_slbs_flag = + Subs.lt x y d.subs && ZExt.of_int (-1) <=* cmp_ub in + let delete_slbs_flag = + (* x could have got lower / we can't rule out x' < x *) + delete_slbs_flag && not keep_slbs_flag in + (*if Subs.gt d.subs x y + then cmp_lb <=* ZExt.zero + else true in*) + (* + analyze 0 >< (a-1)y + [c,d] + x' < y known: SUBs(x') := SUBs(x') u SUBs(y) u {y} + x' <= y known: SUBs(x') := SUBs(x') u SUBs(y) + x' > y known: SLBs(x') := SLBs(x') u {y} - in aux sum_of_terms Subs.VarSet.empty Subs.VarSet.empty true true + *) + let subs_y = Subs.get_value y d.subs in + (* + Caution: New subs can contain the old x. + This is not a contradiction, it just has to be deleted afterwards. + *) + let new_subs = + if cmp_ub <* ZExt.zero then + Subs.VarSet.union subs_y (Subs.VarSet.singleton y) + else if cmp_ub =* ZExt.zero then + subs_y + else + Subs.VarSet.empty + in + let subs_acc = Subs.VarSet.union subs_acc new_subs in + let slbs_acc = if cmp_lb >* ZExt.zero then Subs.VarSet.add y slbs_acc else slbs_acc in + aux rem_terms subs_acc slbs_acc delete_subs_flag delete_slbs_flag + + in aux sum_of_terms Subs.VarSet.empty Subs.VarSet.empty true true let assign_texpr t x texp = @@ -741,7 +739,6 @@ struct (* let assign_var t v v' = timing_wrap "assign_var" (assign_var t v) v' *) - let assign_var_parallel (t: t) (var_tuples: (var * var) list) : t = let assigned_vars = List.map fst var_tuples in let t = add_vars t assigned_vars in @@ -817,105 +814,98 @@ struct | Some (sum_of_terms, (constant,_)) -> ( let monoms = Option.get monoms in - let expr_intv = eval_monoms_to_intv d.boxes monoms in - let neg_expr_intv = Intv.neg expr_intv in - let expr_ext_intv = eval_monoms_to_intv_infty_list d.boxes monoms in let neg_expr_ext_intv = neg_ext_intv expr_ext_intv in + let expr_intv = ext_intv_to_intv expr_ext_intv in - if expr_intv <> ext_intv_to_intv expr_ext_intv || - neg_expr_intv <> ext_intv_to_intv neg_expr_ext_intv then - failwith "ext_intv <> expr_intv" - else - - let rec aux sum_of_terms subs_acc boxes = - - match sum_of_terms with - | [] -> (* no reference variables in the guard, so check if we can rule out expr_intv >= 0 *) - - if Intv.sup expr_intv <* ZExt.zero (* added bot check *) - then bot_of_env t.env - else - wrap boxes subs_acc - - | (coeff_x, x, _) :: rem_terms -> - - let x_intv = Boxes.get_value x d.boxes in - let (lb_x, ub_x) = x_intv in + let rec aux sum_of_terms subs_acc boxes = - (* We receive x from the outer recursion. It stays fixed. *) - let rec inner x_term_intv sum_of_terms subs_acc = + match sum_of_terms with + | [] -> (* no reference variables in the guard, so check if we can rule out expr_intv >= 0 *) - match sum_of_terms with - | [] -> Some(subs_acc) - - | (coeff_y, y, _) :: rem_terms -> + if Intv.sup expr_intv <* ZExt.zero (* added bot check *) + then bot_of_env t.env + else + wrap boxes subs_acc - let y_intv = Boxes.get_value y d.boxes in - let y_term_intv = (coeff_y, y, y_intv) in + | (coeff_x, x, _) :: rem_terms -> - let helper (coeff_x, x, x_intv) (coeff_y, y, y_intv) subs_acc_opt = - match subs_acc_opt with - | None -> None - | Some(subs_acc) -> + let x_intv = Boxes.get_value x d.boxes in + let (lb_x, ub_x) = x_intv in - let neg_expr_plus_x_ext_intv = ext_intv_plus_x (Z.neg coeff_x, x, x_intv) neg_expr_ext_intv in + (* We receive x from the outer recursion. It stays fixed. *) + let rec inner x_term_intv sum_of_terms subs_acc = - let (constraint_lb,_) = eval_ext_intv_minus_x (Z.neg coeff_y, y, y_intv) neg_expr_plus_x_ext_intv in + match sum_of_terms with + | [] -> Some(subs_acc) - let (_, numeric_ub) = Intv.sub x_intv y_intv in + | (coeff_y, y, _) :: rem_terms -> - (* Checking for contradictions first. *) - if numeric_ub <* constraint_lb then - None (* Contradiction! *) - else if (ZExt.sign constraint_lb) >= 0 && Subs.lt x y subs_acc then - None (* Contradiction! *) - else if (ZExt.sign constraint_lb) > 0 then - Some(Subs.add_gt x y subs_acc) - else - Some(subs_acc) - in + let y_intv = Boxes.get_value y d.boxes in + let y_term_intv = (coeff_y, y, y_intv) in - let subs = - helper x_term_intv y_term_intv (Some subs_acc) |> - helper y_term_intv x_term_intv - in - match subs with + let helper (coeff_x, x, x_intv) (coeff_y, y, y_intv) subs_acc_opt = + match subs_acc_opt with | None -> None - | Some(subs) -> - inner x_term_intv rem_terms subs - in - - - (* Setting BOXES *) - (* ax + [c,d] >= 0 ==> x >= x - (ax + [c,d]) = (1-a)x - [c,d] >= (1-a)x - d - x <= x + (ax + [c,d]) = (1+a)x + [c,d] <= (1+a)x + d *) - let constraint_lb_x, _ = - eval_ext_intv_plus_x (Z.neg coeff_x, x, x_intv) neg_expr_ext_intv - in - - let _, constraint_ub_x = - eval_ext_intv_plus_x (coeff_x, x, x_intv) expr_ext_intv - in - - let intv' = (ZExt.max lb_x constraint_lb_x, ZExt.min ub_x constraint_ub_x) in - (*Printf.printf "constraint: %s, constraint': %s\n" (Intv.to_string (a, b)) (Intv.to_string (constraint_lb_x, constraint_ub_x));*) - if Intv.is_bot intv' then - bot_of_env t.env - - else - let boxes = Boxes.set_value x intv' boxes in - - (* Setting SUBS *) - match inner (coeff_x, x, intv') rem_terms subs_acc with - | None -> ( - bot_of_env t.env - ) - | Some(subs) -> - aux rem_terms subs boxes - in - aux sum_of_terms d.subs d.boxes + | Some(subs_acc) -> + + let neg_expr_plus_x_ext_intv = ext_intv_plus_x (Z.neg coeff_x, x, x_intv) neg_expr_ext_intv in + + let (constraint_lb,_) = eval_ext_intv_minus_x (Z.neg coeff_y, y, y_intv) neg_expr_plus_x_ext_intv in + + let (_, numeric_ub) = Intv.sub x_intv y_intv in + + (* Checking for contradictions first. *) + if numeric_ub <* constraint_lb then + None (* Contradiction! *) + else if (ZExt.sign constraint_lb) >= 0 && Subs.lt x y subs_acc then + None (* Contradiction! *) + else if (ZExt.sign constraint_lb) > 0 then + Some(Subs.add_gt x y subs_acc) + else + Some(subs_acc) + in + + let subs = + helper x_term_intv y_term_intv (Some subs_acc) |> + helper y_term_intv x_term_intv + in + match subs with + | None -> None + | Some(subs) -> + inner x_term_intv rem_terms subs + in + + + (* Setting BOXES *) + (* ax + [c,d] >= 0 ==> x >= x - (ax + [c,d]) = (1-a)x - [c,d] >= (1-a)x - d + x <= x + (ax + [c,d]) = (1+a)x + [c,d] <= (1+a)x + d *) + let constraint_lb_x, _ = + eval_ext_intv_plus_x (Z.neg coeff_x, x, x_intv) neg_expr_ext_intv + in + + let _, constraint_ub_x = + eval_ext_intv_plus_x (coeff_x, x, x_intv) expr_ext_intv + in + + let intv' = (ZExt.max lb_x constraint_lb_x, ZExt.min ub_x constraint_ub_x) in + (*Printf.printf "constraint: %s, constraint': %s\n" (Intv.to_string (a, b)) (Intv.to_string (constraint_lb_x, constraint_ub_x));*) + if Intv.is_bot intv' then + bot_of_env t.env + + else + let boxes = Boxes.set_value x intv' boxes in + + (* Setting SUBS *) + match inner (coeff_x, x, intv') rem_terms subs_acc with + | None -> ( + bot_of_env t.env + ) + | Some(subs) -> + aux rem_terms subs boxes + in + aux sum_of_terms d.subs d.boxes ) ) diff --git a/src/cdomains/pentagon/intv.ml b/src/cdomains/pentagon/intv.ml index 159e157ae2..f3a2860687 100644 --- a/src/cdomains/pentagon/intv.ml +++ b/src/cdomains/pentagon/intv.ml @@ -149,6 +149,10 @@ struct let u = if u2 <=* u1 then u2 else ZExt.PosInfty in (l, u) + (* + Taken from Compiler Design: Analysis and Transformation - + https://link.springer.com/book/10.1007/978-3-642-17548-0. + *) let narrow (l1, u1) (l2, u2) = let l = if l1 =* ZExt.NegInfty then l2 else l1 in let u = if u2 =* ZExt.PosInfty then u2 else u1 in @@ -160,4 +164,12 @@ struct let gt ((lb1, _):t) ((_, ub2):t) = lb1 > ub2 + + let to_z_opt_intv (z_ext_intv : t) = + match z_ext_intv with + | ZExt.Arb s1, ZExt.Arb s2 -> Some(s1), Some(s2) + | ZExt.Arb s1, _ -> Some(s1), None + | _, ZExt.Arb s2 -> None, Some(s2) + | _, _ -> None, None + end \ No newline at end of file diff --git a/src/cdomains/pentagon/stringUtils.ml b/src/cdomains/pentagon/stringUtils.ml index b5861906f0..4d437eca42 100644 --- a/src/cdomains/pentagon/stringUtils.ml +++ b/src/cdomains/pentagon/stringUtils.ml @@ -63,4 +63,22 @@ struct "+" ^ int32_str else ZExt.to_string z + + let string_of_monoms env (sum_of_terms, (constant,divisor)) = + if divisor <> Z.one then + failwith "DIVISOR WAS NOT ONE" + else + let term_str_list = BatList.map (fun (coefficient, x', divisor) -> + if divisor <> Z.one then + failwith "DIVISOR WAS NOT ONE" + else + let var_str = Var.to_string @@ Environment.var_of_dim env x' in + let output_str = (Z.to_string coefficient) ^ "*" ^ var_str in + if Z.sign coefficient < 0 then + "("^output_str^")" + else + output_str + ) sum_of_terms + in + String.concat " + " term_str_list ^ " + " ^ (Z.to_string constant) end \ No newline at end of file From 1a8d3ce343e4a9ac945b556db7af806a7180467b Mon Sep 17 00:00:00 2001 From: Philip Feniuk Date: Tue, 22 Jul 2025 16:57:39 +0200 Subject: [PATCH 09/10] Add gcc to creduce script --- scripts/creduce/simple.sh | 2 ++ 1 file changed, 2 insertions(+) diff --git a/scripts/creduce/simple.sh b/scripts/creduce/simple.sh index e6af7de5d5..41e799aeab 100755 --- a/scripts/creduce/simple.sh +++ b/scripts/creduce/simple.sh @@ -6,10 +6,12 @@ GOBLINTDIR="/home/feniuk/University-Coding/analyzer-pentagon/goblint" INPUTFILE="/home/feniuk/University-Coding/bench/coreutils/cut_comb.minimized.c" +OUTPUTFILE="fe8f7af3a.out" PARAMS="--set ana.activated[+] pentagon --enable allglobs --enable dbg.timing.enabled" $GOBLINTDIR $INPUTFILE $PARAMS -v &> out.txt; if [ $? -eq 2 ]; then + gcc $INPUTFILE -o $OUTPUTFILE && rm $OUTPUTFILE &> /dev/null && grep "Fatal error: exception IntDomain0.ArithmeticOnIntegerBot(\"Error int op 8\")" "out.txt" >/dev/null 2>&1 else exit 5 From 62fc11565a811c61cd556f82e67bcddf356c6e2e Mon Sep 17 00:00:00 2001 From: Philip Feniuk Date: Wed, 23 Jul 2025 15:18:47 +0200 Subject: [PATCH 10/10] Remove narrow for Subs; Timing.wrap for dim_add and dim_remove; --- src/cdomains/pentagon/pntg.ml | 6 ++++-- src/cdomains/pentagon/subs.ml | 3 --- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/src/cdomains/pentagon/pntg.ml b/src/cdomains/pentagon/pntg.ml index ae21dc621a..fe65680c37 100644 --- a/src/cdomains/pentagon/pntg.ml +++ b/src/cdomains/pentagon/pntg.ml @@ -36,8 +36,6 @@ struct in ({boxes = intv; subs = subs}: t) - - let dim_add (dim_change: Apron.Dim.change) pntg = let res = dim_add dim_change pntg in if M.tracing then M.trace "pntg_dim" "PNTG.dim_add:\ndim_change:\t%s\npntg:\t\t%s\nres:\t\t%s\n\n" @@ -46,6 +44,7 @@ struct (to_string res); res + let dim_add dim_change pntg = Timing.wrap "dim_add" (dim_add dim_change) pntg (** See https://antoinemine.github.io/Apron/doc/api/ocaml/Dim.html @@ -69,4 +68,7 @@ struct (to_string pntg) (to_string res); res + + + let dim_remove dim_change pntg = Timing.wrap "dim_remove" (dim_remove dim_change) pntg end \ No newline at end of file diff --git a/src/cdomains/pentagon/subs.ml b/src/cdomains/pentagon/subs.ml index bce5c6abe7..eefd451cfe 100644 --- a/src/cdomains/pentagon/subs.ml +++ b/src/cdomains/pentagon/subs.ml @@ -123,9 +123,6 @@ struct let widen (sub1: t) (sub2: t) = BatList.map2 (fun s1x s2x -> if subseteq s1x s2x then s2x else VarSet.empty) sub1 sub2 - (** No narrowing mentioned in the paper. *) - let narrow sub1 sub2 = meet sub1 sub2 - let forget_vars (vars : int BatList.t) = BatList.mapi (fun x ys -> if BatList.mem x vars then