diff --git a/conf/pentagon-svcomp25.json b/conf/pentagon-svcomp25.json new file mode 100644 index 0000000000..45ca5ca613 --- /dev/null +++ b/conf/pentagon-svcomp25.json @@ -0,0 +1,114 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": false, + "interval": true + }, + "float": { + "interval": true, + "evaluate_math_functions": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless", + "pentagon" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "partitioned" + } + }, + "race": { + "free": false, + "call": false + }, + "autotune": { + "enabled": true, + "activated": [ + "reduceAnalyses", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "noOverflows", + "termination", + "tmpSpecialAnalysis" + ] + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "yaml": { + "enabled": true, + "format-version": "2.0", + "entry-types": [ + "invariant_set" + ], + "invariant-types": [ + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": false, + "other": false, + "accessed": false, + "exact": true + } + }, + "pre": { + "enabled": false + } +} diff --git a/conf/pentagon.json b/conf/pentagon.json new file mode 100644 index 0000000000..6d46ec32a9 --- /dev/null +++ b/conf/pentagon.json @@ -0,0 +1,19 @@ +{ + "ana": { + "activated": [ + "assert", + "pentagon" + ] + }, + "result": "none", + "solver": "td3", + "solvers": { + "td3": { + "term": true, + "space": false, + "space_cache": true, + "space_restore": true + } + }, + "verify": true +} diff --git a/src/analyses/apron/pentagonAnalysis.apron.ml b/src/analyses/apron/pentagonAnalysis.apron.ml new file mode 100644 index 0000000000..4321b87f91 --- /dev/null +++ b/src/analyses/apron/pentagonAnalysis.apron.ml @@ -0,0 +1,32 @@ +(** Analysis using the pentagon domain (pntg) + @see + "Pentagons: A weakly relational abstract domain for the efficient validation of array accesses" + -- Francesco Logozzo, Manuel Fähndrich (2010) *) + +open Analyses +include RelationAnalysis + +let spec_module: (module MCPSpec) Lazy.t = + lazy ( + let module AD = PentagonDomain.D2 + in + let module Priv = (val RelationPriv.get_priv ()) in + let module Spec = + struct + include SpecFunctor (Priv) (AD) (RelationPrecCompareUtil.DummyUtil) + let name () = "pentagon" + end + in + (module Spec) + ) + +let get_spec (): (module MCPSpec) = + Lazy.force spec_module + +let after_config () = + let module Spec = (val get_spec ()) in + MCP.register_analysis (module Spec : MCPSpec); + GobConfig.set_string "ana.path_sens[+]" (Spec.name ()) + +let _ = + AfterConfig.register after_config diff --git a/src/analyses/apron/pentagonAnalysis.no-apron.ml b/src/analyses/apron/pentagonAnalysis.no-apron.ml new file mode 100644 index 0000000000..0a444baa9b --- /dev/null +++ b/src/analyses/apron/pentagonAnalysis.no-apron.ml @@ -0,0 +1,3 @@ +(* This analysis is empty on purpose. It serves only as an alternative dependency + in cases where the actual domain can't be used because of a missing library. + It was added because we don't want to fully depend on Apron. *) diff --git a/src/cdomains/apron/pentagonDomain.apron.ml b/src/cdomains/apron/pentagonDomain.apron.ml new file mode 100644 index 0000000000..28a28c66a4 --- /dev/null +++ b/src/cdomains/apron/pentagonDomain.apron.ml @@ -0,0 +1,1089 @@ +(** + 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 +module M = Messages +open GobApron +open BatList +open Pretty + +(* Pentagon specific modules *) +open StringUtils +open ZExt +open Intv +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 + (* Rhs represents coefficient*var_i + offset / divisor + depending on whether coefficient is 0, the monomial term may disappear completely, not refering to any var_i, thus: + (Some (coefficient, i), offset, divisor ) with coefficient != 0 , or + (None , offset, divisor ) *) + type t = ((GobZ.t * int) option * GobZ.t * GobZ.t) [@@deriving eq, ord, hash] + let var_zero i = (Some (Z.one,i), Z.zero, Z.one) + let show_coeff c = + if Z.equal c Z.one then "" + else if Z.equal c Z.minus_one then "-" + else (Z.to_string c) ^"·" + let show_rhs_formatted formatter = let ztostring n = (if Z.(geq n zero) then "+" else "") ^ Z.to_string n in + function + | (Some (coeff,v), o,_) when Z.equal o Z.zero -> Printf.sprintf "%s%s" (show_coeff coeff) (formatter v) + | (Some (coeff,v), o,_) -> Printf.sprintf "%s%s %s" (show_coeff coeff) (formatter v) (ztostring o) + | (None, o,_) -> Printf.sprintf "%s" (Z.to_string o) + let show (v,o,d) = + let rhs=show_rhs_formatted (Printf.sprintf "var_%d") (v,o,d) in + if not (Z.equal d Z.one) then "(" ^ rhs ^ ")/" ^ (Z.to_string d) else rhs + + (** factor out gcd from all terms, i.e. ax=by+c with a positive is the canonical form for adx+bdy+cd *) + let canonicalize (v,o,d) = + let gcd = Z.gcd o d in (* gcd of coefficients *) + let gcd = Option.map_default (fun (c,_) -> Z.gcd c gcd) gcd v in (* include monomial in gcd computation *) + let commondivisor = if Z.(lt d zero) then Z.neg gcd else gcd in (* canonical form dictates d being positive *) + (BatOption.map (fun (coeff,i) -> (Z.div coeff commondivisor,i)) v, Z.div o commondivisor, Z.div d commondivisor) + + (** Substitute rhs for varx in rhs' *) + let subt rhs varx rhs' = + match rhs,rhs' with + | (monom, o, d), (Some (c', x'), o', d') when x'=varx -> canonicalize (Option.map (fun (c,x) -> (Z.mul c c',x)) monom, Z.((o*c')+(d*o')), Z.mul d d') + | _ -> rhs' + +end + +module type Tracked = +sig + val type_tracked: typ -> bool + val varinfo_tracked: varinfo -> bool +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 = +struct + include SharedFunctions.VarManagementOps (Pntg) +end + +(* 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 + let boxes = d.boxes in + let rec aux texpr = + match texpr with + | 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 "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) + | 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 + +(* 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, _)) = + 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_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 + +(* We assume that the divisor is always 1, so we omit it and that t is not bottom. *) +let rec eval_monoms_to_ext_intv boxes (terms, (constant, _)) : ext_intv = + match terms with + | [] -> ((ZExt.Arb constant, []), (ZExt.Arb constant, [])) + | (coeff, x, _)::terms -> ( + let terms_intv_infty_list = eval_monoms_to_ext_intv boxes (terms, (constant, Z.one)) in + let x_intv = Boxes.get_value x boxes in + + let ub = match snd terms_intv_infty_list with + | (NegInfty, _) -> failwith "This should not happen :)" + | (PosInfty, l ) -> (ZExt.PosInfty, l) + | (c, l) -> + + + let coeff_x_ub = + if Z.sign coeff > 0 then + ZExt.mul (Arb coeff) (Intv.sup x_intv) + else + ZExt.mul (Arb coeff) (Intv.inf x_intv) + in + + match coeff_x_ub with + | ZExt.NegInfty -> failwith "This should not happen :)" + | ZExt.PosInfty -> ( + if Z.abs coeff = Z.one then + if List.compare_length_with l 2 >= 0 then + (ZExt.PosInfty, []) + else + c, (x :: l) + else + PosInfty, l + ) + | ub -> ZExt.add c ub, l + in + + let lb = match fst terms_intv_infty_list with + | (PosInfty, _) -> failwith "This should not happen :)" + | (NegInfty, l ) -> (ZExt.NegInfty, l) + | (c, l) -> + + let coeff_x_lb = + if Z.sign coeff > 0 then + ZExt.mul (Arb coeff) (Intv.inf x_intv) + else + ZExt.mul (Arb coeff) (Intv.sup x_intv) + in + + match coeff_x_lb with + | ZExt.PosInfty -> failwith "This should not happen :)" + | ZExt.NegInfty -> ( + if Z.abs coeff = Z.one then + if List.compare_length_with l 2 >= 0 then + (ZExt.NegInfty, []) + else + c, (x :: l) + else + NegInfty, l + ) + | lb -> ZExt.add c lb, l + in + (lb, ub) + + ) + +(* let eval_monoms_to_ext_intv 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 + let ub = ZExt.add c_ub (if infty_list_ub = [] then ZExt.zero else PosInfty) in + (lb, ub) + + +let ext_intv_plus_x (coeff_x, x, x_intv) (ext_intv: ext_intv) = + let (const_lb, lb_list), (const_ub, ub_list) = ext_intv in + + let lb_correction_term = if Z.sign coeff_x < 0 then Intv.sup x_intv else Intv.inf x_intv in + let ub_correction_term = if Z.sign coeff_x < 0 then Intv.inf x_intv else Intv.sup x_intv in + + let ext_lb = + if const_lb = NegInfty then ZExt.NegInfty, [] else + match lb_list with + | [] -> (ZExt.add const_lb lb_correction_term, []) + | x'::l when x = x'-> + if lb_correction_term = PosInfty then (const_lb, l) else (ZExt.add const_lb lb_correction_term, l) + | [y; x'] when x = x' -> + if lb_correction_term = PosInfty then (const_lb, [y]) else (ZExt.add const_lb lb_correction_term, [y]) + | l -> ( + if lb_correction_term = PosInfty then + failwith "This should not happen." + else + (ZExt.add const_lb lb_correction_term, l) + ) + in + + let ext_ub = + if const_ub = PosInfty then ZExt.PosInfty, [] else + match ub_list with + | [] -> (ZExt.add const_ub ub_correction_term, []) + | x'::l when x = x'-> + if ub_correction_term = NegInfty then (const_ub, l) else (ZExt.add const_ub ub_correction_term, l) + | [y; x'] when x = x' -> + if ub_correction_term = NegInfty then (const_ub, [y]) else (ZExt.add const_ub ub_correction_term, [y]) + | l -> ( + if ub_correction_term = NegInfty then + failwith "This should not happen." + else + (ZExt.add const_ub ub_correction_term, l) + ) + in + (ext_lb, ext_ub) + +(* +First argument: Values of a variable corresponding to a term in the associated expr of the extended intv. +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) + +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) + +let neg_ext_intv ((c1, lst1), (c2, lst2)) = (ZExt.neg c2, lst2), (ZExt.neg c1, lst1) + +let string_of_infty_list (c, infty_list : intv_infty_list) = + let list_string = String.concat " +- " (List.map (fun i -> "∞" ^ (string_of_int i)) infty_list) in + ZExt.to_string c ^ " + " ^ list_string + +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 = + 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 -> + let constant, _ = snd monoms in + let numeric_intv = eval_monoms_to_intv d.boxes monoms in + match fst monoms with + | [(a1, x1, _); (a2, x2, _)] when a1 = Z.one && a2 = Z.of_int (-1) -> + let symbolic_intv = + if Subs.gt x1 x2 d.subs then (ZExt.add (Arb constant) (ZExt.of_int 1), ZExt.PosInfty) else (ZExt.NegInfty, ZExt.add (Arb constant) (ZExt.of_int (-1))) + in Intv.to_z_opt_intv (Intv.inter symbolic_intv numeric_intv) + | [(a1, x1, _); (a2, x2, _)] when a1 = Z.of_int (-1) && a2 = Z.one -> + let symbolic_intv = + if Subs.gt x2 x1 d.subs then (ZExt.add (Arb constant) (ZExt.of_int 1), ZExt.PosInfty) else (ZExt.NegInfty, ZExt.add (Arb constant) (ZExt.of_int (-1))) + in Intv.to_z_opt_intv (Intv.inter symbolic_intv numeric_intv) + | _ -> Intv.to_z_opt_intv numeric_intv + + + (* let bound_texpr d texpr1 = timing_wrap "bound_texpr" (bound_texpr d) texpr1 *) +end + +module D = +struct + include ZExtOps + include Printable.Std + include VarManagement + module Bounds = ExpressionBounds + module V = RelationDomain.V + module Arg = struct + let allow_global = true + end + + module Convert = SharedFunctions.Convert (V) (Bounds) (Arg) (SharedFunctions.Tracked) + + type t = VarManagement.t + + type var = V.t + let name () = "pentagon" + + let is_bot t = + match t.d with + | 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 + "⊥" + else if is_top t then + "⊤" + else + (* d = None should have been handled by is_bot. *) + let d = Option.get t.d in + let vars = Array.map (StringUtils.string_of_var) (fst (Environment.vars t.env)) in + let res = Pntg.to_string d in + let key_re = Str.regexp {|\([0-9]+\)->|} in + let subs_re = Str.regexp {|\([0-9]+\)#|} in + let varname_and_append = fun postfix m -> ( + let idx = int_of_string (Str.matched_group 1 m) in + if idx < Array.length vars then + vars.(idx) ^ postfix + else + failwith "D.to_string hit unknown variable!" + ) in + (* 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 "") + + (* let to_string t = timing_wrap "to_string" (to_string) t *) + + 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 + + + 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 + + + let to_yojson t = failwith "TODO" + + (** + Bottom creation does not make sense if we do not know anything about our variables. + We assume no variables have been encountered when this funciton is called. + It therefore holds that: bot = top. + *) + let bot () = {d = None; env = empty_env} + + let bot_of_env env = ({ d = None; env = env }:t) + + + (** + Top creation does not make sense if we do not know anything about our variables. + We assume no variables have been encountered when this funciton is called. + It therefore holds that: top = bot. + *) + let top () = {d = Some {boxes = []; subs = []}; env = empty_env} + + let top_of_env env = dimchange2_add (top ()) env + + let meet 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.meet d1'.boxes d2'.boxes; subs = Subs.meet d1'.subs d2'.subs}; env = sup_env}: t) + | _ -> {d = None; env = sup_env} + + let meet t1 t2 = + let res = meet t1 t2 in + 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 leq 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' -> + let boxes_1, boxes_2 = d1'.boxes, d2'.boxes in + let sub1, sub2 = d1'.subs, d2'.subs in + let for_all_i f lst = + List.for_all (fun (i, x) -> f i x) (List.mapi (fun i x -> (i, x)) lst) in + let bool1 = Boxes.leq boxes_1 boxes_2 in + let bool2 = for_all_i(fun x s2x -> + Subs.VarSet.for_all(fun y -> + let s1x = Subs.VarList.at sub1 x in + let b1x = BatList.at boxes_1 x in + let b1y = BatList.at boxes_1 y in + Subs.VarSet.mem y s1x || + Intv.sup b1x <* Intv.inf b1y + ) s2x + ) sub2 in + bool1 && bool2 + | Some d1', None -> Boxes.is_bot d1'.boxes || Subs.is_bot d1'.subs + | _ -> true + + let leq t1 t2 = + let res = leq t1 t2 in + 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 join 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' -> + let joined_boxes = Boxes.join d1'.boxes d2'.boxes in + let s' x s1x = Subs.VarSet.inter s1x (List.at d2'.subs x) in + let s'' x s1x = Subs.VarSet.filter (fun y -> Intv.sup (List.at d2'.boxes x) <* Intv.inf (List.at d2'.boxes y)) s1x in + let s''' x = Subs.VarSet.filter (fun y -> Intv.sup (List.at d1'.boxes x) <* Intv.inf (List.at d1'.boxes y)) (List.at d2'.subs x) in + let joined_subs = List.mapi (fun x s1x -> Subs.VarSet.union (s' x s1x) (Subs.VarSet.union (s'' x s1x) (s''' x))) d1'.subs in + ({d = Some {boxes = joined_boxes; subs = joined_subs}; env = sup_env}: t) + | Some d1', None -> {d = Some d1'; env = sup_env} + | None, Some d2' -> {d = Some d2'; env = sup_env} + | _ -> {d = None; env = sup_env} + + 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 + let t2 = dimchange2_add t2 sup_env in + match t1.d, t2.d with + | Some d1', Some d2' -> + ({d = Some {boxes = Boxes.widen d1'.boxes d2'.boxes; subs = Subs.widen d1'.subs d2'.subs}; env = sup_env}: t) + | _ -> {d = None; env = sup_env} + + let widen a b = + let res = widen a b in + 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 = + 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 + 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 + + let forget_vars t vars = + if is_bot t || is_bot_env t || vars = [] then t + 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} + + (* let forget_vars t vars = timing_wrap "forget_vars" (forget_vars t) vars *) + + + 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 + match t.d with + | None -> t + | Some d -> + match simplified_monomials_from_texp t.env texp with + | None -> ( + match texp with + (* x:= u % div + Implemented like the paper suggests: If the divisor is positive, it is a strict upper bound for x'. *) + | Binop(Mod, e1, Var(d'), _, _) as rem_op -> ( + let rem_intv = eval_texpr_to_intv t rem_op in + let boxes = Boxes.set_value x rem_intv d.boxes in + + let subs: Subs.t = + (* + We remove any subs of x. + We could add a special case for x' := x % d, x >= 0 ==> x' <= x ==> SUBs(x) can stay. + *) + Subs.forget_vars [x] d.subs |> + let dim_d = Environment.dim_of_var t.env d' in + let d_intv = Boxes.get_value dim_d d.boxes in + + (* Check if all possible divisors are positive. *) + if (Intv.inf d_intv) >* ZExt.zero then + (* We can set SUBs(x) := {d} *) + Subs.set_value x (Subs.VarSet.singleton dim_d) + else if Intv.sup d_intv <* ZExt.zero then + (* We can set SUBs(d) := SUBs(d) u {x} *) + let subs_d = Subs.get_value dim_d d.subs in + Subs.set_value dim_d (Subs.VarSet.add x subs_d) (* BUG WAS HERE *) + else + (* We cannot add any subs. Potentially div-by-zero. *) + Fun.id + in + wrap boxes subs + ) + (* Non-Linear cases. We only do interval analysis and forget all relational information. *) + | expr -> + let boxes = (Boxes.set_value x (eval_texpr_to_intv t expr) d.boxes) in + let subs = (Subs.forget_vars [x] d.subs) in + wrap boxes subs + ) + | Some(sum_of_terms, (constant,divisor)) as monoms -> + + if divisor <> Z.one then failwith "assign_texpr: DIVISOR WAS NOT ONE" + else + let monoms = Option.get monoms in + let expr_ext_intv = eval_monoms_to_ext_intv d.boxes monoms in + let expr_intv = ext_intv_to_intv expr_ext_intv in + + let x_intv = Boxes.get_value x d.boxes in + + match sum_of_terms with + | [(a1, x1, _); (a2, x2, _)] when a1 = Z.one && a2 = Z.of_int (-1) -> + let symbolic_intv = + if Subs.gt x1 x2 d.subs then (ZExt.add (Arb constant) (ZExt.of_int 1), ZExt.PosInfty) else (ZExt.NegInfty, ZExt.add (Arb constant) (ZExt.of_int (-1))) + in + let intersected = (Intv.inter symbolic_intv expr_intv) in + if Intv.is_bot intersected then bot_of_env t.env else + let boxes = Boxes.set_value x intersected d.boxes + in wrap boxes d.subs + | [(a1, x1, _); (a2, x2, _)] when a1 = Z.of_int (-1) && a2 = Z.one -> + let symbolic_intv = + if Subs.gt x2 x1 d.subs then (ZExt.add (Arb constant) (ZExt.of_int 1), ZExt.PosInfty) else (ZExt.NegInfty, ZExt.add (Arb constant) (ZExt.of_int (-1))) + in + let intersected = (Intv.inter symbolic_intv expr_intv) in + if Intv.is_bot intersected then bot_of_env t.env else + let boxes = Boxes.set_value x intersected d.boxes + in wrap boxes d.subs + + | _ -> + + 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. *) + | [] -> + + (* 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 + + (* 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 + + 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 + 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. + *) + 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 = + 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_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 + match Convert.texpr1_expr_of_cil_exp ask t t.env exp no_ov with + | 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') + + (* 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 + let primed_vars = List.init (List.length assigned_vars) (fun i -> Var.of_string (Int.to_string i ^"'")) in + let t_primed = add_vars t primed_vars in + let multi_t = List.fold_left2 (fun t' v_prime (_,v') -> assign_var t' v_prime v') t_primed primed_vars var_tuples in + match multi_t.d with + | Some m when not @@ is_top multi_t -> + let switched_arr = List.fold_left2 (fun multi_t assigned_var primed_var-> assign_var multi_t assigned_var primed_var) multi_t assigned_vars primed_vars in + 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 + *) + let assign_var_parallel' t vs1 vs2 = + 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 + + (* 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 + match t.d with + | None -> t + | Some d -> + match Tcons1.get_typ tcons with + (* Reduction of all Tcons1 comparison operators to SUPEQ, analogous to Miné dissertation, section 3.6.3 *) + | EQ -> ( + let e = Texpr1.to_expr @@ Tcons1.get_texpr1 tcons in + let e = Texpr1.of_expr t.env (Texpr1.Unop(Texpr1.Neg, e, Texpr1.Int, Texpr1.Near)) in + let tcons1 = Tcons1.make e Tcons1.SUPEQ in + + let expr2 = Tcons1.get_texpr1 tcons in + let tcons2 = Tcons1.make expr2 Tcons1.SUPEQ in + let t1 = assert_constraint ask t tcons1 negate no_ov in + let t2 = assert_constraint ask t tcons2 negate no_ov in + meet t1 t2 + ) + | SUP -> ( + let e = Texpr1.to_expr @@ Tcons1.get_texpr1 tcons in + let e = Texpr1.of_expr t.env (Texpr1.Binop(Texpr1.Sub, e, Cst(Scalar(Scalar.of_int 1)) ,Texpr1.Int, Texpr1.Near)) in + let tcons1 = Tcons1.make e Tcons1.SUPEQ in + assert_constraint ask t tcons1 negate no_ov) + | DISEQ -> ( + let e = Texpr1.to_expr @@ Tcons1.get_texpr1 tcons in + let e = Texpr1.of_expr t.env (Texpr1.Unop(Texpr1.Neg, e, Texpr1.Int, Texpr1.Near)) in + let tcons1 = Tcons1.make e Tcons1.SUP in + + let expr2 = Tcons1.get_texpr1 tcons in + let tcons2 = Tcons1.make expr2 Tcons1.SUP in + + let t1 = assert_constraint ask t tcons1 negate no_ov in + let t2 = assert_constraint ask t tcons2 negate no_ov in + join t1 t2 + ) + | EQMOD (s) -> t + (* Base case :) *) + | SUPEQ -> ( + (* e >= 0 *) + let monoms = simplified_monomials_from_texp t.env (Texpr1.to_expr @@ Tcons1.get_texpr1 tcons) in + match monoms with + | None -> t + | Some (sum_of_terms, (constant,_)) -> ( + let monoms = Option.get monoms in + + let expr_ext_intv = eval_monoms_to_ext_intv 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 + + 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 + + (* 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 + | [] -> Some(subs_acc) + + | (coeff_y, y, _) :: rem_terms -> + + let y_intv = Boxes.get_value y d.boxes in + let y_term_intv = (coeff_y, y, y_intv) in + + 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 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 + ) + ) + + + let assert_constraint ask t e negate no_ov ~trace = + let (res, tcons_opt, exn_opt) = + match Convert.tcons1_of_cil_exp ask t t.env e negate no_ov with + | exception Convert.Unsupported_CilExp exn -> (t, None, Some exn) + | tcons -> (assert_constraint ask t tcons negate no_ov, Some tcons, None) + in + if M.tracing && trace then ( + let tcons_str = + match exn_opt, tcons_opt with + | Some exn, None -> Printf.sprintf + "Failed to convert cil expression: exception %s" + (SharedFunctions.show_unsupported_cilExp exn) (* Might cause memory problems. *) + | None, Some tcons-> StringUtils.string_of_tcons1 tcons + | _ -> "" (* Should never be hit. *) + in + M.trace "pntg" "D.assert_constraint:\ntcons:\t%s\nt:\t%s\nres:\t%s\n\n" tcons_str (show t) (show res)); + res + + let assert_constraint ask t e negate no_ov = + match e with + (* + We remove clutter here: + Do not trace interger bound checking assertions. + *) + | BinOp(Le,Lval(_),Const(CInt(i, _, _)),_) when Z.equal i (Z.of_int (Int32.to_int Int32.max_int)) -> assert_constraint ask t e negate no_ov ~trace:false + | BinOp(Ge,Lval(_),Const(CInt(i, _, _)),_) when Z.equal i (Z.of_int (Int32.to_int Int32.min_int)) -> assert_constraint ask t e negate no_ov ~trace:false + | _ -> 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 + + (* + This function returns linear constraints of form: + y - x > 0 for all x in t.env and y in SUBS(x) + and + z - a >= 0, -z + b >= 0 for all z in t.env with z in [a, b] + *) + let invariant (t:t) : GobApron.Lincons1Set.elt list = + (* It`s safe to assume that t.d <> None. *) + let ({boxes; subs}: Pntg.t) = Option.get t.d in + let s_of_int i: Coeff.union_5 = (GobApron.Coeff.s_of_int i) in + let s_of_zext (z: ZExt.t): Coeff.union_5 = + match z with + | NegInfty -> Scalar (Scalar.of_infty (-1)) + | PosInfty -> Scalar (Scalar.of_infty (1)) + | Arb z -> Scalar (Scalar.of_z z) + in + (* + Creates a lincons of the form: + 0*x_1 + ... + coeff * var + ... + 0*x_n + cst >= 0 + *) + let create_supeq_lincons (var: Var.t) ~coeff ~cst= + (* Create a "empty" lincons: 0*x_1 + ... + 0 * var + ... + 0*x_n + 0 >= 0 *) + let lincons = Lincons1.make (Linexpr1.make t.env) Lincons1.SUPEQ in + (* Set the coefficient for the given x to 1. *) + Lincons1.set_coeff lincons var (s_of_int coeff); + (* Add the constant. *) + Lincons1.set_cst lincons (s_of_zext cst); + (* Return the side-effected lincons. *) + lincons + in + + (* + Creates a lincons of the form: + 0*x_1 + ... + (-1) * var1 + 1 * var2 ... + 0*x_n + 0 > 0 + *) + let create_sup_lincons (var1: Var.t) (var2: Var.t) = + (* Create a "empty" lincons: 0*x_1 + ... + 0 * var + ... + 0*x_n + 0 >= 0 *) + let lincons = Lincons1.make (Linexpr1.make t.env) Lincons1.SUP in + (* Set the coefficient for the given var1 to -1. *) + Lincons1.set_coeff lincons var1 (s_of_int (-1)); + (* Set the coefficient for the given var2 to 1. *) + Lincons1.set_coeff lincons var2 (s_of_int 1); + (* Return the side-effected lincons. *) + lincons + in + + (** Create a list of constraints x >= lb, x <= ub, i.e. x - lb >= 0, -x + ub >= 0. *) + let constraints_of_intv var intv = + let lb, ub = intv in + [ + create_supeq_lincons var ~coeff:(1) ~cst:(ZExt.neg lb); + create_supeq_lincons var ~coeff:(-1) ~cst:(lb) + ] + in + + let constraints_of_subs x subs = + (* Creation of constraints y > x, i.e. y - x > 0 forall y in SUBS(x). *) + List.map (create_sup_lincons x) subs + in + (* Zip variables, intervals and subs into one list and transform the subs into variables. *) + List.map2i (fun i intv subs -> ( + Tuple3.make + (Environment.var_of_dim t.env i) + intv + (List.map (Environment.var_of_dim t.env) (Subs.VarSet.to_list subs)) + + )) boxes subs |> + List.fold_left ( + 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 + + let relift t = t + + let cil_exp_of_lincons1 = Convert.cil_exp_of_lincons1 + + let env t = t.env + + let eval_interval (ask) = Bounds.bound_texpr + + let to_string t = + if is_bot t then + "⊥" + else if is_top t then + "⊤" + else + match t.d with + | None -> failwith "is_bot should take care of that" + | Some(d) -> Pntg.to_string d + +end + + +module D2: RelationDomain.RD with type var = Var.t = +struct + module D = D + module ConvArg = struct + let allow_global = false + end + include SharedFunctions.AssertionModule (D.V) (D) (ConvArg) + include D +end diff --git a/src/cdomains/apron/pentagonDomain.no-apron.ml b/src/cdomains/apron/pentagonDomain.no-apron.ml new file mode 100644 index 0000000000..584b720fa5 --- /dev/null +++ b/src/cdomains/apron/pentagonDomain.no-apron.ml @@ -0,0 +1,3 @@ +(* This domain is empty on purpose. It serves only as an alternative dependency + in cases where the actual domain can't be used because of a missing library. + It was added because we don't want to fully depend on Apron. *) \ No newline at end of file diff --git a/src/cdomains/pentagon/boxes.ml b/src/cdomains/pentagon/boxes.ml new file mode 100644 index 0000000000..8752a83429 --- /dev/null +++ b/src/cdomains/pentagon/boxes.ml @@ -0,0 +1,84 @@ +open ZExt +open Intv +open Batteries +open StringUtils + +(** Provides functions and types for collections of Intv. *) +module Boxes = +struct + type t = Intv.t list [@@deriving eq, ord, hash] + include ZExtOps + let is_bot (i: t) = + BatList.exists Intv.is_bot i + + let is_top i = + BatList.for_all Intv.is_top i + + let to_string (intervals: t) = + let string_of_interval i intv = + Printf.sprintf "%i->%s" i (Intv.to_string intv) + in + let bot_or_top = + if is_bot intervals then + StringUtils.bot_str + else if is_top intervals then + StringUtils.top_str + else + " " + |> Printf.sprintf "(%s)" + in + Printf.sprintf "%s { %s }" bot_or_top (String.concat "; " (List.mapi string_of_interval intervals)) + + let leq i1 i2 = + BatList.for_all2 Intv.leq i1 i2 + + let join (i1: t) (i2: t) = + BatList.map2 Intv.union i1 i2 + + let meet (i1: t) (i2: t) = + BatList.map2 Intv.inter i1 i2 + + let widen (i1: t) (i2: t) = + BatList.map2 Intv.widen i1 i2 + + let narrow (i1: t) (i2: t) = + BatList.map2 Intv.narrow i1 i2 + + let dim_add (dim_change: Apron.Dim.change) (intervals: t) = + if dim_change.realdim != 0 then + failwith "Pentagons are defined over integers: \ + extension with real domain is nonsensical" + else + let change_arr = Array.rev dim_change.dim in + let rec insert_dimensions intervals dim_changes = + match dim_changes with + | [||] -> intervals + | _ -> + let k = dim_changes.(0) in + let left, right = BatList.split_at k intervals in + let new_array = (BatArray.sub dim_changes 1 (BatArray.length dim_changes - 1)) in + insert_dimensions (left @ [Intv.top ()] @ right) new_array + in + insert_dimensions intervals change_arr + + (* precondition: dim_change is sorted and has unique elements *) + let dim_remove (dim_change: Apron.Dim.change) (intervals : t) = + if dim_change.realdim != 0 then + failwith "Pentagons are defined over integers: \ + extension with real domain is nonsensical" + else + let rec aux lst_i arr_i = function + | [] -> [] + | x::xs -> if arr_i = BatArray.length dim_change.dim then x::xs + else if dim_change.dim.(arr_i) = lst_i then aux (lst_i + 1) (arr_i + 1) xs + else x :: aux (lst_i + 1) arr_i xs + in + aux 0 0 intervals + + let forget_vars (vars: int BatList.t) = + BatList.mapi (fun x intv -> if BatList.mem x vars then Intv.top() else intv) + + let set_value (var: int) (value: Intv.t) = BatList.modify_at var (fun _ -> value) + + let get_value (var:int) boxes = BatList.at boxes var +end \ No newline at end of file diff --git a/src/cdomains/pentagon/intv.ml b/src/cdomains/pentagon/intv.ml new file mode 100644 index 0000000000..57db487a11 --- /dev/null +++ b/src/cdomains/pentagon/intv.ml @@ -0,0 +1,175 @@ +open ZExt +open Batteries +open StringUtils + +(** + Stores functions and types for single intervals $\mathbb{Z}^\infty$ + according to the pentagon domains semantics. Beware, this module is NOT generic. +*) +module Intv = +struct + include ZExtOps + + type t = (ZExt.t * ZExt.t) [@@deriving eq, hash, ord] + + let to_string ((lb, ub): t) = Printf.sprintf "[%s,%s]" (StringUtils.string_of_zext lb) (StringUtils.string_of_zext ub) + + let top () = ((ZExt.NegInfty, ZExt.PosInfty): t) + + let bot () = ((ZExt.PosInfty, ZExt.NegInfty): t) + + let is_top (x:t) = ((ZExt.NegInfty, ZExt.PosInfty) = x) + + let is_bot ((l, u): t) = u <* l + + let mem a (l, u) = l <=* a && u >=* a + + (** Checks for bot interval. *) + let sup (i: t) = if is_bot i then ZExt.NegInfty else snd i + + (** Checks for bot interval. *) + let inf (i: t) = if is_bot i then ZExt.PosInfty else fst i + + (** Intv intersection *) + let inter ((l1, u1): t) ((l2, u2): t) = + let max_lb = if l1 <=* l2 then l2 else l1 in + let min_ub = if u1 <=* u2 then u1 else u2 in + ((max_lb, min_ub): t) + + let add ((l1, u1): t) ((l2, u2): t) = + let ( + ) = ZExt.add_opt in + ((Option.default ZExt.NegInfty (l1 + l2), Option.default ZExt.PosInfty (u1 + u2)): t) + + let neg intv = (ZExt.neg (sup intv), ZExt.neg (inf intv)) + + let sub intv_1 intv_2 = + let intv_2 = neg intv_2 in + add intv_1 intv_2 + + (** Taken from module IArith *) + let mul ((x1, x2): t) ((y1, y2): t) = + let ( * ) = ZExt.mul in + (( + ZExt.min4 (x1 * y1) (x1 * y2) (x2 * y1) (x2 * y2), + ZExt.max4 (x1 * y1) (x1 * y2) (x2 * y1) (x2 * y2) + ): t) + + (** Taken from module IArith *) + let div ((x1, x2): t) ((y1, y2): t) = + if y1 <=* ZExt.zero && y2 >=* ZExt.zero then top() else + let ( / ) = ZExt.div in + (( + ZExt.min4 (x1 / y1) (x1 / y2) (x2 / y1) (x2 / y2), + ZExt.max4 (x1 / y1) (x1 / y2) (x2 / y1) (x2 / y2) + ): t) + + let no_lowerbound (i: t) = ZExt.NegInfty = inf i + + let no_upperbound (i: t) = ZExt.PosInfty = sup i + + (* taken from https://people.eng.unimelb.edu.au/pstuckey/papers/toplas15.pdf *) + let rec rem (i1: t) i2 = + let (l2, u2) = i2 in + let zero = ZExt.zero in + if inf i2 <=* zero && sup i2 >=* zero then top () (* cannot rule out division by zero *) + else if no_lowerbound i2 || no_upperbound i2 then i1 + else if inf i1 <* zero && sup i1 >* zero then (* split the interval into negative and nonnegative parts *) + let (l, _), (_, u) = (rem (inf i1, ZExt.of_int (-1)) i2), (rem (zero, sup i1) i2) + in (l, u) + else + let ( - ), ( * ), ( / ) = sub, mul, div in + let quotient = i1 / i2 in + if inf quotient =* sup quotient (* if every possible division yields the same result, we can use the remainders *) + then i1 - (quotient * i2) + else + let ub_minus_1 = ZExt.sub (ZExt.max (ZExt.abs l2) (ZExt.abs u2)) (ZExt.of_int 1) in + if ZExt.sign (sup i1) <= 0 then (ZExt.max (ZExt.neg ub_minus_1) (inf i1), zero) + else (zero, ZExt.min ub_minus_1 (sup i1)) + + + (** + We assume that i1 and i2 are well-formed, i.e. not bot/empty. + *) + let pow ((l1, u1): t) ((l2, u2): t) = + if l2 <* ZExt.zero then top () (* x ^ (-1) is unsupported operation on ints ==> we treat it as undefined behavior, same as division by 0 *) + else + match u2 with + | PosInfty -> if l1 <=* ZExt.of_int (-2) then top () (* can create arbitrarily big numbers with (-2) ^ x *) + else if l1 >=* ZExt.zero then (ZExt.pow l1 l2, ZExt.pow u1 PosInfty) + else (* l1 = -1 *) + if u1 =* ZExt.of_int (-1) then (ZExt.of_int (-1), ZExt.of_int 1) + else (ZExt.of_int (-1), ZExt.pow u1 PosInfty) + | NegInfty -> failwith "Intv.pow should not happen" + | Arb u2z when l1 <* ZExt.zero -> + if l2 =* u2 then (* special case because we don't have an even AND an odd number ==> either impossible to mirror negative numbers or everything gets nonnegative *) + let exp = l2 in + if exp =* ZExt.zero then (ZExt.of_int 1, ZExt.of_int 1) else + if Z.is_even u2z then + if u1 >=* ZExt.zero then + (* i1 contains negative and nonnegative numbers, exp != 0 is even ==> lb = 0, ub depends on greater abs value of bounds *) + let max_abs = ZExt.max (ZExt.abs l1) u1 in + let u = ZExt.pow max_abs exp in + (ZExt.zero, u) else + (* x -> x ^ n is monotonically decreasing for even n and negative x *) + let l = ZExt.pow u1 exp in + let u = ZExt.pow l1 exp in + (l, u) + else (* exp is odd *) + (* x -> x ^ n is monotonically increasing for odd n *) + (ZExt.pow l1 exp, ZExt.pow u1 exp) + else + (* we have at least one even and one odd number in the exponent ==> negative numbers can be mirrored if needed *) + let greatest_even = if Z.is_even u2z then u2 else ZExt.sub u2 (ZExt.of_int 1) in + let greatest_odd = if Z.is_odd u2z then u2 else ZExt.sub u2 (ZExt.of_int 1) in + let l = ZExt.pow l1 greatest_odd in + let u' = ZExt.pow l1 greatest_even in + let u'' = if ZExt.sign u1 > 0 then ZExt.pow u1 u2 else u' in + (l, ZExt.max u' u'') + | _ -> (* i1 is nonnegative ==> no special cases here :) *) + let l = ZExt.pow l1 l2 in + let u = ZExt.pow u1 u2 in + (l, u) + + + (** + Creates a single interval from the supplied integer values. + *) + let create i1 i2 = (ZExt.of_int i1, ZExt.of_int i2) + + let create_const i = (ZExt.of_int i, ZExt.of_int i) + + let create_const_of_z z = (ZExt.Arb z, ZExt.Arb z) + + let leq ((l1, u1): t) ((l2, u2): t) = l2 <=* l1 && u1 <=* u2 + + let union ((l1, u1): t) ((l2, u2): t) = (ZExt.min l1 l2, ZExt.max u1 u2) + + let widen (l1, u1) (l2, u2) = + let l = if l1 <=* l2 then l2 else ZExt.NegInfty in + 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 + (l, u) + + let lt ((_, ub1):t) ((lb2, _):t) = + ub1 < lb2 + + 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/pntg.ml b/src/cdomains/pentagon/pntg.ml new file mode 100644 index 0000000000..fe65680c37 --- /dev/null +++ b/src/cdomains/pentagon/pntg.ml @@ -0,0 +1,74 @@ +open StringUtils +open GobApron +module M = Messages + +open Boxes +open Subs + + +module Pntg = +struct + type t = { boxes: Boxes.t; subs: Subs.t } [@@deriving eq, ord, hash] + + let copy (x: t) = x + let empty () = { boxes = []; subs = [] } + let is_empty pntg = + match pntg.boxes, pntg.subs with + | [], [] -> true + | _ -> false + + let to_string pntg = + Printf.sprintf "{ boxes = %s; subs = %s }" (Boxes.to_string pntg.boxes) (Subs.to_string pntg.subs) + + + (** + See https://antoinemine.github.io/Apron/doc/api/ocaml/Dim.html + for the semantic of Dim.change + *) + let dim_add (dim_change: Apron.Dim.change) pntg = + if dim_change.realdim != 0 then + failwith "Pentagons are defined over integers: \ + extension with real domain is nonsensical" + else + let intv, subs = + Boxes.dim_add dim_change pntg.boxes, + Subs.dim_add dim_change pntg.subs + 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" + (StringUtils.string_of_dim_change dim_change) + (to_string pntg) + (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 + for the semantic of Dim.change + *) + let dim_remove (dim_change: Apron.Dim.change) pntg = + if dim_change.realdim != 0 then + failwith "Pentagons are defined over integers: \ + extension with real domain is nonsensical" + else + let boxes, subs = + Boxes.dim_remove dim_change pntg.boxes, + Subs.dim_remove dim_change pntg.subs + in + ({boxes = boxes; subs = subs}: t) + + let dim_remove (dim_change: Apron.Dim.change) pntg = + let res = dim_remove dim_change pntg in + if M.tracing then M.trace "pntg_dim" "PNTG.dim_remove:\ndim_change:\t%s\npntg:\t\t%s\nres:\t\t%s\n\n" + (StringUtils.string_of_dim_change dim_change) + (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/stringUtils.ml b/src/cdomains/pentagon/stringUtils.ml new file mode 100644 index 0000000000..4f02114664 --- /dev/null +++ b/src/cdomains/pentagon/stringUtils.ml @@ -0,0 +1,84 @@ +open GobApron +open ZExt + +module StringUtils = +struct + + (* Symbol for top. *) + let top_str = "⊤" + + (* Symbol for bot. *) + let bot_str = "⊥" + + (* Symbol for a 32 bit integer. *) + let int32_str = "I32" + + let string_of_dim_change (dim_change:Apron.Dim.change) = + let dim = dim_change.dim in + let real_dim = dim_change.realdim in + let int_dim = dim_change.intdim in + Printf.sprintf "{ real_dim=%i; int_dim=%i; dim=[|%s|]}" real_dim int_dim (String.concat ", " (Array.to_list (Array.map Int.to_string (dim)))) + + let string_of_var (var: Var.t) = + let s = (Var.to_string var) in + match String.index_opt s '#' with + | Some i -> + (* Environment might contain variable names like #ret *) + if i = 0 then + let len = String.length s in + String.sub s 1 (len-1) + else + String.sub s 0 i + | None -> s + + let string_of_texpr1 (texpr: Texpr1.expr) = + let rec aux texpr = + match texpr with + | Texpr1.Cst (Interval inv) -> "Cst(Interval inv)" + | Cst (Scalar s) -> Scalar.to_string s + | Var x -> string_of_var x + | Unop (Neg, e, _, _) -> "(-" ^ aux e ^ ")" + | Unop (Cast, e, _, _) -> "((cast)" ^ aux e ^ ")" + | Unop (Sqrt, e, _, _) -> "(sqrt(" ^ aux e ^ "))" + | Binop (Add, e1, e2, _, _) -> "(" ^ aux e1 ^ " + " ^ aux e2 ^ ")" + | Binop (Sub, e1, e2, _, _) -> "(" ^ aux e1 ^ " - " ^ aux e2 ^ ")" + | Binop (Mul, e1, e2, _, _) -> "(" ^ aux e1 ^ " * " ^ aux e2 ^ ")" + | Binop (Div, e1, e2, _, _) -> "(" ^ aux e1 ^ " / " ^ aux e2 ^ ")" + | Binop (Mod, e1, e2, _, _) -> "(" ^ aux e1 ^ " % " ^ aux e2 ^ ")" + | Binop (Pow, e1, e2, _, _) -> "(" ^ aux e1 ^ " ^ " ^ aux e2 ^ ")" + in + aux texpr + + let string_of_tcons1 tcons1 = + (string_of_texpr1 @@ Texpr1.to_expr @@ Tcons1.get_texpr1 @@ tcons1) ^ " " ^ Tcons1.string_of_typ (Tcons1.get_typ tcons1) ^ " 0" + + (** Returns "-I32" or "+I32" if z is bound, else just the string of z. *) + let string_of_zext z = + let (=*) = ZExtOps.(=*) in + let min_int = Int32.to_int Int32.min_int in + let max_int = Int32.to_int Int32.max_int in + if z =* (ZExt.of_int min_int) then + "-" ^ int32_str + else if z =* (ZExt.of_int max_int) then + "+" ^ 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 diff --git a/src/cdomains/pentagon/subs.ml b/src/cdomains/pentagon/subs.ml new file mode 100644 index 0000000000..36124042c6 --- /dev/null +++ b/src/cdomains/pentagon/subs.ml @@ -0,0 +1,177 @@ +open Batteries +open GobApron + +open StringUtils + +(** Stores functions and types for strict upper bounds. *) +module Subs = +struct + + module Idx = Int + 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 + include BatMap.Make(Idx) + type t = Idx.t BatMap.Make(Idx).t + end + + 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 + failwith "Pentagons are defined over integers: \ + dim_change should not contain `realdim`" + else + (* + This is basically a fold_lefti with rev at the end. + Could not use fold_lefti directly because I might need to append at the end of the list. + This would have forced me to use List.length, which is \theta(n). + *) + let rec aux (dim_change: Apron.Dim.change) i subs (moved: MoveMap.t) acc = + (** Computes the number by which the current index/variable will be shifted/moved *) + let moved_by = + Array.count_matching (fun k -> k <= i) dim_change.dim + in + (** Counts the number of empty sets to prepend at the current index. *) + let append_count = + Array.count_matching (fun k -> k == i) dim_change.dim + in + (** Prepends n many empty sets to the accumulator. *) + let rec prepend_dim n acc = + if n == 0 then + acc + else prepend_dim (n-1) (VarSet.empty :: acc) + in + match subs with + | h::t -> + (** Store the new index mappings to later adjust the sets. *) + let moved = (MoveMap.add i (i+moved_by) moved) in + (** Insert `append_count` many dimensions before `h`, then append `h` *) + let acc = (h :: (prepend_dim append_count acc)) in + aux dim_change (i+1) t moved acc + | [] -> + (** Complete subs prepending the last dimensions and reversing *) + let subs = (List.rev (prepend_dim append_count acc)) in + (** Adjust the stored indices in our sets *) + VarList.map ( + fun set -> + VarSet.map ( + fun v -> MoveMap.find_default v v moved + ) set + ) subs + in + aux dim_change 0 subs MoveMap.empty [] + + let dim_remove (dim_change: Apron.Dim.change) (subs: t) = + (* This implementation assumes, that dim_change.dim is well-formed, i.e., does not contain duplicates. *) + let move_or_delete_var y = + if Array.mem y dim_change.dim then None + else Some (y - Array.count_matching (fun k -> k < y) dim_change.dim) + in + let move_or_delete_set x ys = + if Array.mem x dim_change.dim then None + else Some (VarSet.filter_map move_or_delete_var ys) + in + List.filteri_map move_or_delete_set subs + + (** + This isn't precise: we might return false even if there are transitive contradictions; + Other possibility: compute transitive closure first (would be expensive) + *) + let is_bot (subs: t) = + (* exists function for lists where the predicate f also gets the index of a list element *) + let existsi f lst = + let rec aux i = function + | [] -> false + | x :: xs -> if f i x then true else aux (i + 1) xs + in aux 0 lst + in + (* If we don't know any variables, i.e. subs = [], then bot = top holds. *) + subs = [] || + existsi ( + fun i set -> + (* direct contradiction *) + VarSet.mem i set || + (* We assume that the sets inside subs only contain values < length of the list.*) + VarSet.exists (fun y -> VarSet.mem i (List.at subs y)) set + ) subs + + + let is_top (sub: t) = VarList.for_all VarSet.is_empty sub + + (** + The inequalities map s1 is less than or equal to s2 iff + forall x in s2. + s2(x) VarSet.subset s1(x) + *) + let leq (sub1: t) (sub2: t) = + BatList.for_all2 VarSet.subset sub2 sub1 + + let join (sub1: t) (sub2: t) = BatList.map2 VarSet.inter sub1 sub2 + + let meet (sub1: t) (sub2: t) = BatList.map2 VarSet.union sub1 sub2 + + let widen (sub1: t) (sub2: t) = BatList.map2 (fun s1x s2x -> if VarSet.subset s1x s2x then s2x else VarSet.empty) sub1 sub2 + + let forget_vars (vars : int BatList.t) = + BatList.mapi (fun x ys -> + if BatList.mem x vars then + VarSet.empty + else + VarSet.filter (fun y -> not (BatList.mem y vars)) ys + ) + + let set_value (index: Idx.t) (value: VarSet.t) = BatList.modify_at index (fun _ -> value) + + (* Adds to index i a strict upper bound j, i.e., i < j.*) + let add_lt (index: Idx.t) (sub: Idx.t) = BatList.modify_at index (VarSet.add sub) + + (* Adds to index j a strict upper bound i, i.e., i > j.*) + let add_gt (index: Idx.t) (sub: Idx.t) = add_lt sub index + + let get_value (index: Idx.t) (subs: t) = BatList.at subs index + + let to_string (sub: t) = + (* The following results in: { y1#, y2#, ..., yn# }*) + let set_string set = + if VarSet.cardinal set = 0 then "∅" else "{" ^ ( + VarSet.to_list set |> + (* Marking for later variable name replacement *) + List.map (fun v -> Idx.to_string v ^ "#") |> + String.concat ", " + ) ^ "}" in + (* The following results in: x_1 -> {y1#, y2#, ..., yn#}; ... ; x_n -> {y1#, ..., yn#} *) + String.concat "; " ( + VarList.mapi ( + fun i set -> + Printf.sprintf "%s->%s" (Idx.to_string i) (set_string set) + ) sub + ) + + let to_string (subs: t) = + let bot_or_top = + if is_bot subs then + StringUtils.bot_str + else if is_top subs then + StringUtils.top_str + else + " " + |> Printf.sprintf "(%s)" + in + Printf.sprintf "%s { %s }" bot_or_top (to_string subs) + + (* x_i < x_j <== x_j \in SUBs(x_i) *) + let lt i j subs = + let subs_i = List.at subs i in + VarSet.mem j subs_i + + let gt i j = + lt j i + +end \ No newline at end of file diff --git a/src/cdomains/pentagon/zExt.ml b/src/cdomains/pentagon/zExt.ml new file mode 100644 index 0000000000..5122913ed2 --- /dev/null +++ b/src/cdomains/pentagon/zExt.ml @@ -0,0 +1,176 @@ +open Z +(** + Extension of the Zarith types and funcitons. + The values represent arbitrary precision integers and also negative or positive infinity. +*) +module ZExt = +struct + type t = PosInfty | NegInfty | Arb of Z.t + + let hash (z: t) = + match z with + | PosInfty -> 0x186e81bd (* random constant *) + | NegInfty -> 0xc8590e8 (* random constant *) + | Arb(z) -> Z.hash z + + let equal (z1: t) (z2: t) = + match z1, z2 with + | PosInfty, PosInfty -> true + | NegInfty, NegInfty -> true + | Arb(z1), Arb(z2) -> Z.equal z1 z2 + | _ -> false + + let compare (z1: t) (z2: t) = + match z1, z2 with + | NegInfty, NegInfty -> 0 + | PosInfty, PosInfty -> 0 + | NegInfty, _ -> -1 + | _, NegInfty -> 1 + | PosInfty, _ -> 1 + | _, PosInfty -> -1 + | Arb(z1), Arb(z2) -> Z.compare z1 z2 + + let (<*) z1 z2 = compare z1 z2 < 0 + let (>*) z1 z2 = compare z1 z2 > 0 + let (=*) z1 z2 = compare z1 z2 = 0 + let (<=*) z1 z2 = compare z1 z2 <= 0 + let (>=*) z1 z2 = compare z1 z2 >= 0 + let (<>*) z1 z2 = compare z1 z2 <> 0 + + + let of_int i = Arb(Z.of_int i) + + let of_float f = + if Float.is_nan f then + failwith "ZExt.of_float: Tried to convert Nan." + else if Float.is_finite f then + Arb(Z.of_float f) + else if Float.sign_bit f then + NegInfty + else + PosInfty + + let zero = Arb(Z.zero) + + let one = Arb(Z.one) + + let to_string = function + | NegInfty -> "-∞" + | PosInfty -> "+∞" + | Arb z -> Z.to_string z + + let neg = function + | NegInfty -> PosInfty + | PosInfty -> NegInfty + | Arb z -> Arb(Z.neg z) + + let sign = function + | NegInfty -> -1 + | PosInfty -> +1 + | Arb z -> Z.sign z + + let add_opt z1 z2 = + match z1, z2 with + | PosInfty, NegInfty -> None + | NegInfty, PosInfty -> None + | Arb z1, Arb z2 -> Some(Arb(Z.add z1 z2)) + | PosInfty, _ -> Some(PosInfty) + | NegInfty, _ -> Some(NegInfty) + | _, PosInfty -> Some(PosInfty) + | _, NegInfty -> Some(NegInfty) + + let add_unsafe z1 z2 = + match add_opt z1 z2 with + | None -> failwith "ZExt.add_unsafe: Cannot add PosInfty and NegInfty or vice versa." + | Some(s) -> s + + (** Alias for add_unsafe *) + let add = add_unsafe + + (** Alias for add z1 (neg z2) *) + let sub z1 z2 = add z1 (neg z2) + + 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 + | Arb z1, Arb z2 -> Arb(Z.mul z1 z2) + | Arb(z1), z2 -> mul z2 (Arb z1) + (** z1 is definitely a infty *) + | z1, z2 -> + if sign z2 < 0 then + neg z1 + else + if z2 =* zero then + zero + else + z1 + + let rec div z1 z2 = + match z1, z2 with + | Arb z1, Arb z2 -> Arb(Z.div z1 z2) + | Arb(z1), z2 -> div z2 (Arb z1) + (** z1 is definitely a infty *) + | z1, z2 -> + if sign z2 < 0 then + neg z1 + else + if z2 =* zero then + zero + else + z1 + + let pow z1 z2 = + if sign z2 < 0 then failwith "ZExt.pow: z2 should be non negative" else + match z1, z2 with + | Arb z1, Arb z2 when Z.sign z1 < 0 && not (Z.fits_nativeint z2) -> + if Z.is_even z2 then PosInfty else NegInfty + | Arb z1, Arb z2 when Z.sign z1 > 0 && not (Z.fits_nativeint z2) -> PosInfty + | _, Arb z when Z.zero = z -> one + | Arb z, _ when Z.zero = z -> zero + | Arb z, _ when Z.one = z -> one + | Arb z1, Arb z2 -> (Arb(Z.pow z1 (Z.to_int z2))) + | z1, PosInfty when sign z1 < 0 -> failwith "ZExt.pow: Cannot determine whether result is NegInfty or PosInfty (or -1 or 1 for z1 = -1) -> depends on the side of the interval" + | PosInfty, _ | _, PosInfty -> PosInfty + | NegInfty, Arb z -> if Z.is_even z then PosInfty else NegInfty + | _, NegInfty -> failwith "This shouldn't happen (caught in second line of ZExt.pow)" + + let abs z1 = if z1 <* zero then neg z1 else z1 + + let max z1 z2 = if z1 >* z2 then z1 else z2 + + let min z1 z2 = if z1 <* z2 then z1 else z2 + + (** Taken from module IArith *) + let min4 a b c d = min (min a b) (min c d) + + (** Taken from module IArith *) + let max4 a b c d = max (max a b) (max c d) + +end + +module ZExtOps = +struct + + let (<*) = ZExt.(<*) + let (>*) = ZExt.(>*) + let (=*) = ZExt.(=*) + let (<=*) = ZExt.(<=*) + let (>=*) = ZExt.(>=*) + let (<>*) = ZExt.(<>*) + +end \ No newline at end of file diff --git a/src/dune b/src/dune index 964e23a5f7..2fa478bb1e 100644 --- a/src/dune +++ b/src/dune @@ -47,6 +47,14 @@ (apron -> linearTwoVarEqualityDomain.apron.ml) (-> linearTwoVarEqualityDomain.no-apron.ml) ) + (select pentagonDomain.ml from + (apron -> pentagonDomain.apron.ml) + (-> pentagonDomain.no-apron.ml) + ) + (select pentagonAnalysis.ml from + (apron -> pentagonAnalysis.apron.ml) + (-> pentagonAnalysis.no-apron.ml) + ) (select relationAnalysis.ml from (apron -> relationAnalysis.apron.ml) (-> relationAnalysis.no-apron.ml) diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml index 60dd07f68d..e04485d3a3 100644 --- a/src/goblint_lib.ml +++ b/src/goblint_lib.ml @@ -77,6 +77,7 @@ module RelationAnalysis = RelationAnalysis module ApronAnalysis = ApronAnalysis module AffineEqualityAnalysis = AffineEqualityAnalysis module LinearTwoVarEqualityAnalysis = LinearTwoVarEqualityAnalysis +module PentagonAnalysis = PentagonAnalysis module VarEq = VarEq module CondVars = CondVars module TmpSpecial = TmpSpecial @@ -265,6 +266,15 @@ module ApronDomain = ApronDomain module AffineEqualityDomain = AffineEqualityDomain module AffineEqualityDenseDomain = AffineEqualityDenseDomain module LinearTwoVarEqualityDomain = LinearTwoVarEqualityDomain +module PentagonDomain = PentagonDomain + +(** Domain specific *) +module StringUtils = StringUtils +module Boxes = Boxes +module ZExt = ZExt +module Intv = Intv +module Pntg = Pntg +module Subs = Subs (** {5 2-Pointer Logic} diff --git a/tests/regression/89-pentagon/00-even_simpler.c b/tests/regression/89-pentagon/00-even_simpler.c new file mode 100644 index 0000000000..28b330ad5f --- /dev/null +++ b/tests/regression/89-pentagon/00-even_simpler.c @@ -0,0 +1,8 @@ +// SKIP PARAM: --conf ./conf/pentagon.json + +#include + +void main(void) { + int x; + __goblint_check(x >= 0); // UNKNOWN +} diff --git a/tests/regression/89-pentagon/01-pentagon-simple.c b/tests/regression/89-pentagon/01-pentagon-simple.c new file mode 100644 index 0000000000..22cc4dbda6 --- /dev/null +++ b/tests/regression/89-pentagon/01-pentagon-simple.c @@ -0,0 +1,10 @@ +// SKIP PARAM: --conf ./conf/pentagon.json + +#include + +void main(void) { + int x = rand(), y = x, z = x; + y = x - 1; + z = y - 1; + __goblint_check(z < x); // SUCC +} diff --git a/tests/regression/89-pentagon/02-simple-loop.c b/tests/regression/89-pentagon/02-simple-loop.c new file mode 100644 index 0000000000..9d1e9d204a --- /dev/null +++ b/tests/regression/89-pentagon/02-simple-loop.c @@ -0,0 +1,25 @@ +// SKIP PARAM: --conf ./conf/pentagon.json + +#include + +int main(void) { + int x = 0; + + + /* + Only run this test with either of the while loops commented in. + If both are commented in, the first check will proof the second. + */ + + while(x < 42 || x > 42) { + x++; + __goblint_check(x >= 1); // SUCC + } + + + // while(x != 42) { + // x++; + // __goblint_check(x >= 1); // UNKNOWN + // } + +} \ No newline at end of file diff --git a/tests/regression/89-pentagon/03-lhs-more-than-just-var.c b/tests/regression/89-pentagon/03-lhs-more-than-just-var.c new file mode 100644 index 0000000000..f8f3a02384 --- /dev/null +++ b/tests/regression/89-pentagon/03-lhs-more-than-just-var.c @@ -0,0 +1,13 @@ +// SKIP PARAM: --conf ./conf/pentagon.json + +#include + +int main(void) { + int x; + __goblint_assume(x != __INT32_MAX__); + int one = 1; + int two = 2; + if(x + one == two){ + __goblint_check(x == one); // SUCC + } +} \ No newline at end of file diff --git a/tests/regression/89-pentagon/04-function-call.c b/tests/regression/89-pentagon/04-function-call.c new file mode 100644 index 0000000000..e807647d38 --- /dev/null +++ b/tests/regression/89-pentagon/04-function-call.c @@ -0,0 +1,15 @@ +// SKIP PARAM: --conf ./conf/pentagon.json + +#include + +int main(void) { + int x = -1; + int y = 42; + double z = 0; + x = f(x, y, z); + __goblint_check(x == 48); // SUCC +} + +int f(int x, int y, double z) { + return 48; +} \ No newline at end of file diff --git a/tests/regression/89-pentagon/05-loop.c b/tests/regression/89-pentagon/05-loop.c new file mode 100644 index 0000000000..0996c1302f --- /dev/null +++ b/tests/regression/89-pentagon/05-loop.c @@ -0,0 +1,20 @@ +// SKIP PARAM: --conf ./conf/pentagon.json + +#include + +int main() { + int x = 0; + int y = 10; + int z = 5; + + for (int i = 0; i < 3; i++) { + x = z; + y = i; + __goblint_check(x == z); // UNKNOWN + z = 2; + __goblint_check(y == i); // UNKNOWN + __goblint_check(z == 2); // SUCCESS + } + + return 0; +} \ No newline at end of file diff --git a/tests/regression/89-pentagon/06-subs.c b/tests/regression/89-pentagon/06-subs.c new file mode 100644 index 0000000000..d01bcd8894 --- /dev/null +++ b/tests/regression/89-pentagon/06-subs.c @@ -0,0 +1,30 @@ +// SKIP PARAM: --conf ./conf/pentagon.json + +#include + +int main() { + int x = rand(), y = x, z = x; // we can't store equalities ==> this just adds less tmp vars than (x = rand(), y = rand(), z = rand();), but is otherwise equivalent + __goblint_assume(x > y); + + __goblint_check(y < __INT32_MAX__); // SUCCESS + __goblint_check(y < x); // SUCCESS + __goblint_check(x - y > 0); // SUCCESS + + __goblint_assume(x <= 1000); + __goblint_assume(y <= 10000); + z = x - y + 4; + __goblint_check(z > 0); // SUCCESS + __goblint_check(z > 4); // SUCCESS + + x = rand(), y = x, z = x; + __goblint_assume(x <= 11); + __goblint_assume(y <= 1); + __goblint_assume(z >= 5); + __goblint_assume(z <= 10); + + if (9*x + 10*y > 20*z - 1) { + __goblint_check(x >= 10); // UNKNOWN (we might want to implement this to be more precise, or just use the interval domain) + __goblint_check(y == 1); // UNKNOWN + __goblint_check(x >= 2); // SUCCESS + } +} \ No newline at end of file diff --git a/tests/regression/89-pentagon/07-several-ana.c b/tests/regression/89-pentagon/07-several-ana.c new file mode 100644 index 0000000000..d7d2b52955 --- /dev/null +++ b/tests/regression/89-pentagon/07-several-ana.c @@ -0,0 +1,24 @@ +// SKIP PARAM: --enable ana.int.interval --set ana.activated[+] pentagon + +#include + +void main(void) { + int X = 0; + int N = rand(); + if(N < 0) { N = 0; } + + while(X < N) { + X++; + } + + __goblint_check(X-N == 0); + __goblint_check(X == N); + + if(X == N) { + N = 8; + } else { + // is dead code but if that is detected or not depends on what we do in branch + // currently we can't detect this + N = 42; + } +} \ No newline at end of file diff --git a/tests/unit/mainTest.ml b/tests/unit/mainTest.ml index 3ab350d0fe..0d7eb2a4ae 100644 --- a/tests/unit/mainTest.ml +++ b/tests/unit/mainTest.ml @@ -19,4 +19,4 @@ let all_tests = let () = print_string "\027[0;1munit: \027[0;0;00m"; - run_test_tt_main all_tests + run_test_tt_main all_tests \ No newline at end of file diff --git a/wrong_verdicts.md b/wrong_verdicts.md new file mode 100644 index 0000000000..26d814a933 --- /dev/null +++ b/wrong_verdicts.md @@ -0,0 +1,15 @@ +# Wrong Verdicts + +Hier ist die Liste der Wrong Verdicts: + +## Termination + +- [termination](https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/termination-crafted/Bangalore_v2.c) +- [termination](https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/termination-restricted-15/NO_24.c) + +## Valid Memorysafety + +- [valid-memsafety](https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/termination-15/cstrcat_reverse_alloca.c) + +## Unreach Call +- [unreach-call](https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/loops/verisec_OpenSER_cases1_stripFullBoth_arr.c)