diff --git a/src/analyses/apron/linearTwoVarEqualityAnalysisPentagon.apron.ml b/src/analyses/apron/linearTwoVarEqualityAnalysisPentagon.apron.ml new file mode 100644 index 0000000000..1a7fe4a106 --- /dev/null +++ b/src/analyses/apron/linearTwoVarEqualityAnalysisPentagon.apron.ml @@ -0,0 +1,40 @@ +(** {{!RelationAnalysis} Relational integer value analysis} using an OCaml implementation of the linear two-variable equalities domain ([lin2vareq]). + + @see A. Flexeder, M. Petter, and H. Seidl Fast Interprocedural Linear Two-Variable Equalities. *) + +open Analyses +include RelationAnalysis + +module NoIneq = LinearTwoVarEqualityDomainPentagon.D2(RepresentantDomains.NoInequalties) +module PentagonIneq = LinearTwoVarEqualityDomainPentagon.D2(RepresentantDomains.InequalityFunctor(RepresentantDomains.PentagonCoeffs)) +module PentagonOffsetIneq = LinearTwoVarEqualityDomainPentagon.D2(RepresentantDomains.InequalityFunctor(RepresentantDomains.PentagonOffsetCoeffs)) +module FullIneq = LinearTwoVarEqualityDomainPentagon.D2(RepresentantDomains.InequalityFunctor(RepresentantDomains.TwoVarInequalitySet)) + +let spec_module: (module MCPSpec) Lazy.t = + lazy ( + let (module AD) = match GobConfig.get_string "ana.lin2vareq_p.inequalities" with + | "none" -> (module NoIneq : RelationDomain.RD) + | "pentagon" -> (module PentagonIneq : RelationDomain.RD) + | "pentagon_offset" -> (module PentagonOffsetIneq : RelationDomain.RD) + | _ -> (module FullIneq : RelationDomain.RD) (*Other options differ only in the limit function*) + in + let module Priv = (val RelationPriv.get_priv ()) in + let module Spec = + struct + include SpecFunctor (Priv) (AD) (RelationPrecCompareUtil.DummyUtil) + let name () = "lin2vareq_p" + 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/linearTwoVarEqualityAnalysisPentagon.no-apron.ml b/src/analyses/apron/linearTwoVarEqualityAnalysisPentagon.no-apron.ml new file mode 100644 index 0000000000..0a444baa9b --- /dev/null +++ b/src/analyses/apron/linearTwoVarEqualityAnalysisPentagon.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/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index 10a0e9b31f..cfeedbfaf7 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -559,8 +559,8 @@ struct Priv.thread_join ~force:true ask man.global id st | Rand, _ -> Option.map_default (fun lv -> - let st = invalidate_one ask man st lv in - assert_fn {man with local = st} (BinOp (Ge, Lval lv, zero, intType)) true + let st = invalidate_one ask man st lv in + assert_fn {man with local = st} (BinOp (Ge, Lval lv, zero, intType)) true ) st r | _, _ -> let st' = special_unknown_invalidate man f args in diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 067fbeb1ac..f9fc48f96e 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -202,21 +202,23 @@ struct | Mult -> ID.mul | Div -> fun x y -> - (match ID.equal_to Z.zero y with - | `Eq -> - M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of division is zero" - | `Top -> - M.warn ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of division might be zero" - | `Neq -> ()); + if not !AnalysisState.executing_speculative_computations then + (match ID.equal_to Z.zero y with + | `Eq -> + M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of division is zero" + | `Top -> + M.warn ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of division might be zero" + | `Neq -> ()); ID.div x y | Mod -> fun x y -> - (match ID.equal_to Z.zero y with - | `Eq -> - M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of modulo is zero" - | `Top -> - M.warn ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of modulo might be zero" - | `Neq -> ()); + if not !AnalysisState.executing_speculative_computations then + (match ID.equal_to Z.zero y with + | `Eq -> + M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of modulo is zero" + | `Top -> + M.warn ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of modulo might be zero" + | `Neq -> ()); ID.rem x y | Lt -> ID.lt | Gt -> ID.gt diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 51bc436348..ad05aee7e5 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -286,7 +286,7 @@ struct let inv_bin_int (a, b) ikind c op = let warn_and_top_on_zero x = if GobOption.exists (Z.equal Z.zero) (ID.to_int x) then - (M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Must Undefined Behavior: Second argument of div or mod is 0, continuing with top"; + (if not !AnalysisState.executing_speculative_computations then M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Must Undefined Behavior: Second argument of div or mod is 0, continuing with top"; ID.top_of ikind) else x diff --git a/src/autoTune.ml b/src/autoTune.ml index 3bd81edda8..ec8259fff4 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -248,12 +248,12 @@ let focusOnMemSafetySpecification () = let focusOnTermination (spec: Svcomp.Specification.t) = match spec with | Termination -> - let terminationAnas = ["threadflag"; "apron"] in + let terminationAnas = ["threadflag"; get_string "ana.autotune.extraTerminationDomain"] in enableAnalyses "Specification: Termination" "termination analyses" terminationAnas; set_string "sem.int.signed_overflow" "assume_none"; set_bool "ana.int.interval" true; - set_string "ana.apron.domain" "polyhedra"; (* TODO: Needed? *) - () + if get_string "ana.autotune.extraTerminationDomain" = "apron" then + set_string "ana.apron.domain" "polyhedra"; (* TODO: Needed? *) | _ -> () let focusOnTermination () = diff --git a/src/cdomain/value/cdomains/int/congruenceDomain.ml b/src/cdomain/value/cdomains/int/congruenceDomain.ml index 843949c254..6b4da992d4 100644 --- a/src/cdomain/value/cdomains/int/congruenceDomain.ml +++ b/src/cdomain/value/cdomains/int/congruenceDomain.ml @@ -1,8 +1,11 @@ open IntDomain0 open GoblintCil +module type Norm = sig + val normalize : ikind -> (Z.t * Z.t) option -> (Z.t * Z.t) option +end -module Congruence : S with type int_t = Z.t and type t = (Z.t * Z.t) option = +module CongruenceFunctor (Norm : Norm): S with type int_t = Z.t and type t = (Z.t * Z.t) option = struct let name () = "congruences" type int_t = Z.t @@ -24,22 +27,7 @@ struct let ( |: ) a b = if a =: Z.zero then false else (b %: a) =: Z.zero - let normalize ik x = - match x with - | None -> None - | Some (c, m) -> - if m =: Z.zero then - if should_wrap ik then - Some (Size.cast ik c, m) - else - Some (c, m) - else - let m' = Z.abs m in - let c' = c %: m' in - if c' <: Z.zero then - Some (c' +: m', m') - else - Some (c' %: m', m') + let normalize = Norm.normalize let range ik = Size.range ik @@ -540,3 +528,52 @@ struct let project ik p t = t end + +module Wrapping : Norm = struct + + let (%:) = Z.rem + let (=:) = Z.equal + let (+:) = Z.add + let (<:) x y = Z.compare x y < 0 + + let normalize ik x = + match x with + | None -> None + | Some (c, m) -> + if m =: Z.zero then + if should_wrap ik then + Some (Size.cast ik c, m) + else + Some (c, m) + else + let m' = Z.abs m in + let c' = c %: m' in + if c' <: Z.zero then + Some (c' +: m', m') + else + Some (c' %: m', m') +end + +module NoWrapping : Norm = struct + + let (%:) = Z.rem + let (=:) = Z.equal + let (+:) = Z.add + let (<:) x y = Z.compare x y < 0 + + let normalize ik x = + match x with + | None -> None + | Some (c, m) -> + if m =: Z.zero then + Some (c, m) + else + let m' = Z.abs m in + let c' = c %: m' in + if c' <: Z.zero then + Some (c' +: m', m') + else + Some (c' %: m', m') +end + +module Congruence = CongruenceFunctor(Wrapping) \ No newline at end of file diff --git a/src/cdomain/value/cdomains/int/intDomTuple.ml b/src/cdomain/value/cdomains/int/intDomTuple.ml index 1ea6be9c96..0e0e1fe233 100644 --- a/src/cdomain/value/cdomains/int/intDomTuple.ml +++ b/src/cdomain/value/cdomains/int/intDomTuple.ml @@ -124,6 +124,7 @@ module IntDomTupleImpl = struct let ending ?(suppress_ovwarn=false) ik = create2_ovc ik { fi2_ovc = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.ending ~suppress_ovwarn ik } let of_interval ?(suppress_ovwarn=false) ik = create2_ovc ik { fi2_ovc = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_interval ~suppress_ovwarn ik } let of_congruence ik = create2 { fi2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_congruence ik } + let to_congruence (_,_,_,c,_,_) = match c with Some c -> c | None -> I4.top_of IChar (*ikind is ignored, so choose an arbitrary one *) let of_bitfield ik = create2 { fi2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_bitfield ik } let refine_with_congruence ik ((a, b, c, d, e, f) : t) (cong : (int_t * int_t) option) : t= @@ -556,6 +557,8 @@ struct let no_intervalSet (x: I.t) = {x with v = IntDomTupleImpl.no_intervalSet x.v} let no_bitfield (x: I.t) = {x with v = IntDomTupleImpl.no_bitfield x.v} + + let to_congruence (x: I.t) = IntDomTupleImpl.to_congruence x.v end let of_const (i, ik, str) = IntDomTuple.of_int ik i \ No newline at end of file diff --git a/src/cdomain/value/cdomains/int/intervalDomain.ml b/src/cdomain/value/cdomains/int/intervalDomain.ml index 93d2d034b8..833a251a81 100644 --- a/src/cdomain/value/cdomains/int/intervalDomain.ml +++ b/src/cdomain/value/cdomains/int/intervalDomain.ml @@ -1,28 +1,30 @@ open IntDomain0 -module IntervalFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) option = -struct - let name () = "intervals" - type int_t = Ints_t.t - type t = (Ints_t.t * Ints_t.t) option [@@deriving eq, ord, hash] - module IArith = IntervalArith (Ints_t) +(**TODO Better Naming!*) +module type BoundedIntOps = sig + include IntOps.IntOps + + type t_interval = (t * t) option + val range : GoblintCil.ikind -> t * t + val top_of : GoblintCil.ikind -> t_interval + val bot_of : GoblintCil.ikind -> t_interval + + + val norm : ?suppress_ovwarn:bool -> ?cast:bool -> GoblintCil.ikind -> t_interval -> t_interval * overflow_info +end + +module Bounded (Ints_t : IntOps.IntOps): BoundedIntOps with type t = Ints_t.t and type t_interval = (Ints_t.t * Ints_t.t) option = struct + include Ints_t + type t_interval = (Ints_t.t * Ints_t.t) option let range ik = BatTuple.Tuple2.mapn Ints_t.of_bigint (Size.range ik) let top_of ik = Some (range ik) - let bot () = None - let bot_of ik = bot () (* TODO: improve *) + let bot_of ik = None (* TODO: improve *) - let show = function None -> "bottom" | Some (x,y) -> "["^Ints_t.to_string x^","^Ints_t.to_string y^"]" - include Std (struct type nonrec t = t let name = name let top_of = top_of let bot_of = bot_of let show = show let equal = equal end) - let equal_to i = function - | None -> failwith "unsupported: equal_to with bottom" - | Some (a, b) -> - if a = b && b = i then `Eq else if Ints_t.compare a i <= 0 && Ints_t.compare i b <=0 then `Top else `Neq - - let norm ?(suppress_ovwarn=false) ?(cast=false) ik : (t -> t * overflow_info) = function None -> (None, {underflow=false; overflow=false}) | Some (x,y) -> + let norm ?(suppress_ovwarn=false) ?(cast=false) ik : (t_interval -> t_interval * overflow_info) = function None -> (None, {underflow=false; overflow=false}) | Some (x,y) -> if Ints_t.compare x y > 0 then (None,{underflow=false; overflow=false}) else ( @@ -58,6 +60,31 @@ struct (v, ov_info) ) +end + +module BoundedIntervalFunctor (Ints_t : BoundedIntOps): SOverflow with type int_t = Ints_t.t and type t = Ints_t.t_interval = +struct + let name () = "intervals bounds injected" + type int_t = Ints_t.t + type t = (Ints_t.t * Ints_t.t) option [@@deriving eq, ord, hash] + module IArith = IntervalArith (Ints_t) + + let range = Ints_t.range + let top_of = Ints_t.top_of + let norm = Ints_t.norm + let bot_of = Ints_t.bot_of + + let bot () = None + + let show = function None -> "bottom" | Some (x,y) -> "["^Ints_t.to_string x^","^Ints_t.to_string y^"]" + + include Std (struct type nonrec t = t let name = name let top_of = top_of let bot_of = bot_of let show = show let equal = equal end) + + let equal_to i = function + | None -> failwith "unsupported: equal_to with bottom" + | Some (a, b) -> + if a = b && b = i then `Eq else if Ints_t.compare a i <= 0 && Ints_t.compare i b <=0 then `Top else `Neq + let leq (x:t) (y:t) = match x, y with | None, _ -> true @@ -444,5 +471,7 @@ struct let project ik p t = t end +module IntervalFunctor (Ints_t : IntOps.IntOps) = BoundedIntervalFunctor (Bounded(Ints_t)) + module Interval = IntervalFunctor (IntOps.BigIntOps) module Interval32 = IntDomWithDefaultIkind (IntDomLifter (SOverflowUnlifter (IntervalFunctor (IntOps.Int64Ops)))) (IntIkind) diff --git a/src/cdomain/value/cdomains/intDomain_intf.ml b/src/cdomain/value/cdomains/intDomain_intf.ml index 061f3f7d88..501f884214 100644 --- a/src/cdomain/value/cdomains/intDomain_intf.ml +++ b/src/cdomain/value/cdomains/intDomain_intf.ml @@ -381,6 +381,7 @@ sig val no_intervalSet: t -> t val no_bitfield: t -> t val ikind: t -> ikind + val to_congruence : t -> (Z.t * Z.t) option end val of_const: Z.t * Cil.ikind * string option -> IntDomTuple.t diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 34aff68706..e2e9871d23 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -97,8 +97,9 @@ module EqualitiesConjunction = struct (** add/remove new variables to domain with particular indices; translates old indices to keep consistency add if op = (+), remove if op = (-) the semantics of indexes can be retrieved from apron: https://antoinemine.github.io/Apron/doc/api/ocaml/Dim.html *) - let modify_variables_in_domain (dim,map) indexes op = - if Array.length indexes = 0 then (dim,map) else + + let modify_variables_in_domain_general map map_value indexes op = + if Array.length indexes = 0 then map else let offsetlist = Array.to_list indexes in let rec bumpvar delta i = function (* bump the variable i by delta; find delta by counting indices in offsetlist until we reach a larger index then our current parameter *) | head::rest when i>=head -> bumpvar (delta+1) i rest (* rec call even when =, in order to correctly interpret double bumps *) @@ -115,13 +116,18 @@ module EqualitiesConjunction = struct IntHashtbl.add h x r; r) in - let rec bumpentry k (refvar,offset,divi) = function (* directly bumps lhs-variable during a run through indexes, bumping refvar explicitly with a new lookup in indexes *) + let rec bumpentry k value = function (* directly bumps lhs-variable during a run through indexes, bumping refvar explicitly with a new lookup in indexes *) - | (tbl,delta,head::rest) when k>=head -> bumpentry k (refvar,offset,divi) (tbl,delta+1,rest) (* rec call even when =, in order to correctly interpret double bumps *) - | (tbl,delta,lyst) (* k (IntMap.add (op k delta) (BatOption.map (fun (c,v) -> (c,memobumpvar v)) refvar,offset,divi) tbl, delta, lyst) + | (tbl,delta,head::rest) when k>=head -> bumpentry k value (tbl,delta+1,rest) (* rec call even when =, in order to correctly interpret double bumps *) + | (tbl,delta,lyst) (* k (IntMap.add (op k delta) (map_value memobumpvar value) tbl, delta, lyst) in let (a,_,_) = IntMap.fold bumpentry map (IntMap.empty,0,offsetlist) in (* Build new map during fold with bumped key/vals *) - (op dim (Array.length indexes), a) + a + + let modify_variables_in_domain (dim,map) indexes op = + let map_value bumpvar (refvar,offset,divi) = (BatOption.map (fun (c,v) -> (c,bumpvar v)) refvar,offset,divi) in + (op dim (Array.length indexes), modify_variables_in_domain_general map map_value indexes op) + let modify_variables_in_domain m cols op = let res = modify_variables_in_domain m cols op in if M.tracing then M.tracel "modify_dims" "dimarray bumping with (fun x -> x + %d) at positions [%s] in { %s } -> { %s }" diff --git a/src/cdomains/apron/linearTwoVarEqualityDomainPentagon.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomainPentagon.apron.ml new file mode 100644 index 0000000000..9803bda710 --- /dev/null +++ b/src/cdomains/apron/linearTwoVarEqualityDomainPentagon.apron.ml @@ -0,0 +1,1374 @@ +(**TODO short description*) + +open Batteries +open GoblintCil +open Pretty +open GobApron +open RepresentantDomains + +module EqualitiesConjunctionWithIntervals (Ineq : TwoVarInequalities) = +struct + type t = EConj.t * (Value.t IntMap.t ) * Ineq.t [@@deriving eq, ord] + + let hash (econj, v, ineq) = 5 * EConj.hash econj + 13* IntMap.fold (fun k value acc -> 13 * 13 * acc + 31 * k + Value.hash value) v 0 + 7 * Ineq.hash ineq + + let show_values formatter is = + if IntMap.is_empty is then "{}" + else + let str = IntMap.fold (fun k v acc -> Printf.sprintf "%s=%s , %s" (formatter k) (Value.show v) acc) is "" in + "{" ^ String.sub str 0 (String.length str - 3) ^ "}" + + let show_formatted formatter ((dim, econj), is, ineq) = Printf.sprintf "(%s, %s, %s)" (EConj.show_formatted formatter econj) (show_values formatter is) (Ineq.show_formatted formatter ineq) + + let show = show_formatted (Printf.sprintf "var_%d") + + let copy = identity + + let empty () = (EConj.empty (), IntMap.empty, Ineq.empty) + let is_empty (e,is, ineq) = EConj.is_empty e && IntMap.is_empty is && Ineq.is_empty ineq + let make_empty_with_size size = (EConj.make_empty_conj size, IntMap.empty, Ineq.empty) + + let is_top_con (e, is, ineq) = EConj.is_top_con e && IntMap.is_empty is && Ineq.is_empty ineq + + let modify_variables_in_domain_values map indexes op = + let map_value _ = identity in EConj.modify_variables_in_domain_general map map_value indexes op + + let modify_variables_in_domain_values map indexes op = + let res = modify_variables_in_domain_values map indexes op in if M.tracing then + M.tracel "modify_dims" "dimarray bumping with (fun x -> x + %d) at positions [%s] in { %s } -> { %s }" + (op 0 1) + (Array.fold_right (fun i str -> (string_of_int i) ^ ", " ^ str) indexes "") + (show_values (Printf.sprintf "var_%d") map) + (show_values (Printf.sprintf "var_%d") res); + res + + (*TODO we now potentially create the memo_bumpvar function three times (using it twice)-> inefficient?*) + let dim_add (ch: Apron.Dim.change) (econj, i, ineq) = + (EConj.dim_add ch econj, modify_variables_in_domain_values i ch.dim (+), Ineq.modify_variables_in_domain ineq ch.dim (+)) + + let get_rhs (econ, _, _) = EConj.get_rhs econ + + let get_value ((econ, vs, _) as t) lhs = + match IntMap.find_opt lhs vs with + Some i -> i + | None -> (*If there is no value saved, we have calculate it*) + let (v,o,d) = get_rhs t lhs in + if (v,o,d) = Rhs.var_zero lhs then Value.top (*no relation -> Top*) + else match v with + None -> Value.of_bigint @@ Z.divexact o d (*constant*) + | Some (coeff,v) -> + let i = match IntMap.find_opt v vs with + None -> Value.top (*uninitialised. Still translate it with the Rhs for congruence information*) + | Some i -> i + in Value.div (Value.add (Value.of_bigint o) @@ Value.mul (Value.of_bigint coeff) i) (Value.of_bigint d) + + + (*Does not check the values directly, only the inequality domain, so we can use this to detect contradictions *) + let get_relations ((_,vs,ineq) as t) x' y' = + match get_rhs t x', get_rhs t y' with + | (Some (c_x, x),o_x,d_x), (Some (c_y, y),o_y,d_y) -> Ineq.get_relations ((c_x, x,o_x,d_x), get_value t x) ((c_y, y,o_y,d_y), get_value t y) ineq + | _, _ -> [] (*One of the variables is a constant -> there are no inequalities*) + + + let constrain_with_congruence_from_rhs econ lhs i =(**TODO do not recalculate this every time?*) + (*calculate the congruence constraint for x from a single equation (cx + o) / d *) + let congruence_of_rhs (c, o, d) = + (*adapted euclids extended algorithm for calculating the modular multiplicative inverse*) + let rec inverse t r t_old r_old = + if Z.equal r Z.zero + then t_old + else + let q = Z.div r_old r in + inverse (Z.sub t_old (Z.mul q t)) (Z.sub r_old (Z.mul q r)) t r + in let inverse a n = + let a = Z.rem a n in + let a = if Z.lt a Z.zero then Z.add a n else a + in inverse Z.one a Z.zero n + (* x = -o c^-1 (mod d) *) + in Value.of_congruence @@ (Z.mul (Z.neg o) (inverse c d), d) + in + let meet_with_rhs _ rhs i = match rhs with + | (Some (c, v), o, d) when v = lhs -> begin + let cong = (congruence_of_rhs (c, o, d)) in + let res = Value.meet i cong in + if M.tracing then M.tracel "refine_pentagon" "refining %s with rhs %s (constraint: %s) -> %s" (Value.show i) (Rhs.show rhs) (Value.show cong) (Value.show res); + res + end + | _ -> i + in + IntMap.fold meet_with_rhs (snd econ) i + + let constrain_with_congruence_from_rhs econ lhs i =(**TODO do not recalculate this every time?*) + Timing.wrap "congruence" (constrain_with_congruence_from_rhs econ lhs) i + + (*TODO make this configureable with options*) + let refine_depth = 5 + + let rec set_value ((econ, is, ineq) as t:t) lhs i = + if Value.is_bot i then raise EConj.Contradiction; + let set_value_for_root lhs i = + let i = constrain_with_congruence_from_rhs econ lhs i in + if i = Value.top then (econ, IntMap.remove lhs is, ineq) (*stay sparse*) + else if Value.is_bot i then raise EConj.Contradiction + else match Value.to_int i with + | Some (Int x) -> meet_with_one_conj t lhs (None, x, Z.one) (*constant value*) + | _ -> (econ, IntMap.add lhs i is, ineq) + in + let (v,o,d) = get_rhs t lhs in + if (v,o,d) = Rhs.var_zero lhs then + set_value_for_root lhs i + else + match v with + | None -> + if not @@ Value.contains i @@ Z.div o d then raise EConj.Contradiction; + (econ, is, ineq) (*For a constant, we do not need to save an value*) + | Some (coeff, v) -> + let i1 = Value.mul (Value.of_bigint d) i in + let i2 = Value.sub i1 (Value.of_bigint o) in + let i3 = Value.div i2 (Value.of_bigint coeff) in + let i_transformed = i3 in + set_value_for_root v i_transformed + + and set_rhs (econ, is, ineq) lhs rhs = + let econ' = EConj.set_rhs econ lhs rhs in + match rhs with + | (None, o, d) -> + if not @@ Z.equal d Z.one then + raise EConj.Contradiction; + let ineq', refinements = Ineq.set_constant lhs o ineq in + let t' = econ', IntMap.remove lhs is, ineq' in (*when setting as a constant, we do not need a separate value *) + apply_refinements refinements t' (*TODO limit depth ?*) + | _ -> + let new_constraint = get_value (econ', is, ineq) lhs in + let old_constraint = get_value (econ, is, ineq) lhs in + let new_value = Value.meet new_constraint old_constraint in + if Value.is_bot new_value then raise EConj.Contradiction + else set_value (econ', is, ineq) lhs new_value + + + and meet_with_one_value var value t narrow = + let meet_function = if narrow then Value.narrow else Value.meet in + let new_value = meet_function (get_value t var) value + in if Value.is_bot new_value then raise EConj.Contradiction else + let res = set_value t var new_value (*TODO because we meet with an already saved values, we already confirm to the congruence constraints -> skip calculating them again!*) + in if M.tracing then M.tracel "meet_value" "meet var_%d: before: %s meeting: %s -> %s, total: %s-> %s" (var) (Value.show @@ get_value t var) (Value.show value) (Value.show new_value) (show t) (show res); + res + + and meet_with_one_conj ?(refine_depth = refine_depth) ((ts, is, ineq) as t:t) i (var, offs, divi) = + let (var,offs,divi) = Rhs.canonicalize (var,offs,divi) in (* make sure that the one new conj is properly canonicalized *) + let res : t = + let subst_var (((dim,econj), is, ineq) as t) x (vary, o, d) = + let (vary, o, d) = Rhs.canonicalize (vary, o, d) in + (* [[x substby (cy+o)/d ]] ((c'x+o')/d') *) + (* =====> (c'cy + c'o+o'd)/(dd') *) + let adjust = function + | (Some (c',varx), o',d') when varx = x -> + let open Z in Rhs.canonicalize (BatOption.map (fun (c, y)-> (c * c', y)) vary, c'*o + o'*d, d'*d) + | e -> e + in + let value = get_value t x in + if vary = None then begin + if d <> Z.one then + (if M.tracing then M.tracel "meet_with_one_conj" "meet_with_one_conj substituting var_%d with constant %s, which is not an integer" i (Rhs.show (vary,o,d)); + raise EConj.Contradiction); + if not @@ Value.contains value (Z.div o d) then + (if M.tracing then M.tracel "meet_with_one_conj" "meet_with_one_conj substituting var_%d with constant %s, Contradicts %s" (i) (Rhs.show (vary,o,d)) (Value.show value); + raise EConj.Contradiction) + end; + let econj' = (dim, IntMap.add x (vary, o, d) @@ IntMap.map adjust econj) in (* in case of sparse representation, make sure that the equality is now included in the conjunction *) + match vary with + | Some (c,y) -> (*x was a representant but is not anymore*) + let ineq', refinements = Ineq.substitute (get_value (econj', is, ineq)) ineq x (c, y, o, d) + in let is' = IntMap.remove x is in (*remove value and add it back in the new econj *) + let t' = econj', is', ineq' in + let t'' = set_value t' x value in + apply_refinements ~refine_depth refinements t'' + | None -> + let ineq', refinements = Ineq.set_constant x (Z.div o d) ineq in + let t' = econj', IntMap.remove x is, ineq' in (*we replaced x (and all connected vars) by a constant -> do not save a value and inequality anymore*) + apply_refinements ~refine_depth refinements t' + in + (match var, (EConj.get_rhs ts i) with + (*| new conj , old conj *) + | None , (None , o1, divi1) -> if not @@ (Z.equal offs o1 && Z.equal divi divi1) then raise EConj.Contradiction else t + (* o/d = x_i = (c1*x_h1+o1)/d1 *) + (* ======> x_h1 = (o*d1-o1*d)/(d*c1) /\ x_i = o/d *) + | None , (Some (coeff1,h1), o1, divi1) -> + subst_var t h1 (None, Z.(offs*divi1 - o1*divi),Z.(divi*coeff1)) + (* (c*x_j+o)/d = x_i = o1/d1 *) + (* ======> x_j = (o1*d-o*d1)/(d1*c) /\ x_i = o1/d1 *) + | Some (coeff,j), (None , o1, divi1) -> subst_var t j (None, Z.(o1*divi - offs*divi1),Z.(divi1*coeff)) + (* (c*x_j+o)/d = x_i = (c1*x_h1+o1)/d1 *) + (* ======> x_j needs normalization wrt. ts *) + | Some (coeff,j), ((Some (coeff1,h1), o1, divi1) as oldi)-> + (match EConj.get_rhs ts j with + (* ts[x_j]=o2/d2 ========> ... *) + | (None , o2, divi2) -> + let newxi = Rhs.subst (None,o2,divi2) j (Some (coeff,j),offs,divi) in + let newxh1 = snd @@ EConj.inverse i (coeff1,h1,o1,divi1) in + let newxh1 = Rhs.subst newxi i newxh1 in + subst_var t h1 newxh1 + (* ts[x_j]=(c2*x_h2+o2)/d2 ========> ... *) + | (Some (coeff2,h2), o2, divi2) as normalizedj -> + if h1 = h2 then (* this is the case where x_i and x_j already where in the same equivalence class; let's see whether the new equality contradicts the old one *) + let normalizedi= Rhs.subst normalizedj j (Some(coeff,j),offs,divi) in + if not @@ Rhs.equal normalizedi oldi then raise EConj.Contradiction else t + else if h1 < h2 (* good, we now unite the two equvalence classes; let's decide upon the representative *) + then (* express h2 in terms of h1: *) + let (_,newh2)= EConj.inverse j (coeff2,h2,o2,divi2) in + let newh2 = Rhs.subst oldi i (Rhs.subst (snd @@ EConj.inverse i (coeff,j,offs,divi)) j newh2) in + subst_var t h2 newh2 + else (* express h1 in terms of h2: *) + let (_,newh1)= EConj.inverse i (coeff1,h1,o1,divi1) in + let newh1 = Rhs.subst normalizedj j (Rhs.subst (Some(coeff,j),offs,divi) i newh1) in + subst_var t h1 newh1)) in + if M.tracing then M.tracel "meet_with_one_conj" "meet_with_one_conj conj: %s eq: var_%d=%s -> %s " (show t) i (Rhs.show (var,offs,divi)) (show res) + ; res + + and apply_refinements ?(refine_depth = refine_depth) (refs : Refinement.t) (t:t) = + let apply_single t = function + | var, Either.Left value -> + begin try + meet_with_one_value var value t false + with EConj.Contradiction -> + if M.tracing then M.trace "refinements" "Contradiction when applying var_%d=%s in %s" var (Value.show value) (show t); + raise EConj.Contradiction + end + | var, Right rhs -> + begin try + meet_with_one_conj ~refine_depth:(refine_depth-1) t var rhs + with EConj.Contradiction -> + if M.tracing then M.trace "refinements" "Contradiction when applying var_%d=%s in %s" var (Rhs.show rhs) (show t); + raise EConj.Contradiction + end + in + if refine_depth > 0 then begin + let res = List.fold apply_single t refs in + res + end else begin + t + end + + let forget_variable ((econj, _, _) as d) var = + let rhs_var = get_rhs d var in + (*Forgetting EConj, but also return relation of new representative to the old if this changes*) + let (econj', vs', ineq'), newRoot = + (let ref_var_opt = Tuple3.first rhs_var in + match ref_var_opt with + | Some (_,ref_var) when ref_var = var -> + if M.tracing then M.trace "forget" "headvar var_%d" var; + (* var is the reference variable of its connected component *) + (let cluster = List.sort (Int.compare) @@ IntMap.fold + (fun i (refe,_,_) l -> BatOption.map_default (fun (coeff,refe) -> if (refe=ref_var) then i::l else l) l refe) (snd econj) [] in + if M.tracing then M.trace "forget" "cluster varindices: [%s]" (String.concat ", " (List.map (string_of_int) cluster)); + (* obtain cluster with common reference variable ref_var*) + match cluster with (* new ref_var is taken from head of the cluster *) + | head :: clusterrest -> + (* head: divi*x = coeff*y + offs *) + (* divi*x = coeff*y + offs =inverse=> y =( divi*x - offs)/coeff *) + let (newref,offs,divi) = (get_rhs d head) in + let (coeff,y) = BatOption.get newref in + let (y,yrhs) = EConj.inverse head (coeff,y,offs,divi) in (* reassemble yrhs out of components *) + let shifted_cluster = (List.fold (fun map i -> + let irhs = (get_rhs d i) in (* old entry is i = irhs *) + Rhs.subst yrhs y irhs |> (* new entry for i is irhs [yrhs/y] *) + set_rhs map i + ) d clusterrest) in + set_rhs shifted_cluster head (Rhs.var_zero head), Some yrhs (* finally make sure that head is now trivial *) + | [] -> d, None) (* empty cluster means no work for us *) + | _ -> d, None) (* variable is either a constant or expressed by another refvar *) in + (*Forget old information*) + let econj'' = (fst econj', IntMap.remove var (snd econj')) in + let vs'' = IntMap.remove var vs' in + match newRoot with + | None -> (econj'', vs'', Ineq.forget_variable ineq' var) + | Some (Some (coeff,y),offs,divi) -> + (*modify inequalities. We ignore refinements as they should not matter in this case*) + let ineq'', _ = Ineq.substitute (get_value (econj'', vs'', ineq')) ineq' var (coeff,y,offs,divi) + (*restoring value information*) + in set_value (econj'', vs'', ineq'') y @@ get_value d y + | _ -> failwith "Should not happen" (*transformation can not be a constant*) + + + let dim_remove (ch: Apron.Dim.change) (econj, v, ineq) = + if Array.length ch.dim = 0 || is_empty (econj, v, ineq) then + (econj, v, ineq) + else ( + let (econj', v', ineq') = Array.fold_lefti (fun y i x -> forget_variable y (x)) (econj, v, ineq) ch.dim in (* clear m' from relations concerning ch.dim *) + let econj'' = EConj.modify_variables_in_domain econj' ch.dim (-) in + let v'' = modify_variables_in_domain_values v' ch.dim (-) in + let ineq'' = Ineq.modify_variables_in_domain ineq' ch.dim (-) in + (econj'', v'', ineq'')) + + + let affine_transform (econ, vs, ineq) i rhs = + (*This is a place we want to use the original set_rhs (therefore use EConj directly), as the implied congruence might contradict each other during the transformation*) + (*e.g. with 2x = y and 2z = y, and the assignment y = y+1 *) + (*This is only called in assign_texpr, after which the value will be set correctly.*) + let (_, (m,o,d)) = EConj.inverse i rhs in + let c,_ = BatOption.get m in + let ineq', refinements = + if EConj.nontrivial econ i + then ineq, [] + else Ineq.substitute (get_value (econ, vs, ineq)) ineq i (c,i,o,d) + in + apply_refinements refinements (EConj.affine_transform econ i rhs, vs, ineq') + +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 (Ineq : TwoVarInequalities) = +struct + module EConjI = EqualitiesConjunctionWithIntervals(Ineq) + include SharedFunctions.VarManagementOps (EqualitiesConjunctionWithIntervals(Ineq)) + + let dim_add = EConjI.dim_add + let size t = BatOption.map_default (fun ((d,_),_,_) -> d) 0 t.d + + let eval_texpr (t:t) texp = + let open Apron.Texpr1 in + let binop_function = function + | Add -> Value.add + | Sub -> Value.sub + | Mul -> Value.mul + | Div -> Value.div + | Mod -> Value.rem + | Pow -> failwith "power is not supported" + in let unop_function = function + | Neg -> Value.neg + | Cast -> identity + | Sqrt -> failwith "sqrt is not supported" + in let rec eval = function + | Cst (Scalar x) -> + begin match SharedFunctions.int_of_scalar ?round:None x with + | Some x -> Value.of_bigint x + | None -> Value.top + end + | Cst (Interval _) -> failwith "constant was an interval; this is not supported" + | Var x -> + let var_dim = Environment.dim_of_var t.env x in + begin match t.d with + | None -> Value.top + | Some d -> EConjI.get_value d var_dim + end + | Binop (Sub, Var a , Var b, Int, _) -> + let dim_a = Environment.dim_of_var t.env a in + let dim_b = Environment.dim_of_var t.env b in + begin match t.d with + | None -> Value.top + | Some d -> + let v = Value.sub (EConjI.get_value d dim_a) (EConjI.get_value d dim_b) in + let relations = EConjI.get_relations d dim_a dim_b in + let meet_relation v = function + | Relation.Lt, o -> Value.meet v @@ Value.ending @@ Z.pred o + | Relation.Gt, o -> Value.meet v @@ Value.starting @@ Z.succ o + in List.fold meet_relation v relations + end + | Binop (op, a, b, Int, _) -> (binop_function op) (eval a) (eval b) + | Unop (op, a, Int, _) -> (unop_function op) (eval a) + | _ -> Value.top (*not integers*) + in + let res = eval texp in + if M.tracing then M.tracel "eval_texp" "%s %a -> %s" (match t.d with None -> "⊥" | Some d ->EConjI.show d) Texpr1.Expr.pretty texp (Value.show res); + res + + (** Parses a Texpr to obtain a (coefficient, variable) pair 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 (t: t) 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 t.env x in + begin match t.d with + | None -> [(Some (Z.one,var_dim),Z.zero,Z.one)] + | Some d -> + (match (EConjI.get_rhs d var_dim) with + | (Some (coeff,i), k,divi) -> [(Some (coeff,i),Z.zero,divi); (None,k,divi)] + | (None, k,divi) -> [ (None,k,divi)]) + end + | Unop (Neg, e, _, _) -> negate (convert_texpr e) + | Unop (Cast, e, _, _) -> convert_texpr e (* Ignore since casts in apron are used for floating point nums and rounding in contrast to CIL casts *) + | 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 (Div, e1, e2, _, _) -> begin + match convert_texpr e2 with + | [(None,coeff, divi)] -> + if Z.equal (Z.rem coeff divi) Z.zero then + let d = Z.divexact coeff divi in + let e1_val = eval_texpr t e1 in + if Value.leq e1_val (Value.of_congruence (Z.zero, d)) then + (*the division is exact -> the expression is still linear*) + List.map (fun (monom, offs, divi) -> Rhs.canonicalize Z.(monom, offs, divi*d) ) (convert_texpr e1) + else + raise NotLinearExpr + else + raise NotLinearExpr + | _ -> raise NotLinearExpr + end + | Binop _ -> raise NotLinearExpr end + in match convert_texpr texp with + | exception NotLinearExpr -> None + | exception ScalarIsInfinity -> None + | x -> Some(x) + + (** convert and simplify (wrt. reference variables) a texpr into a tuple of a list of monomials (coeff,varidx,divi) and a (constant/divi) *) + let simplified_monomials_from_texp (t: t) texp = + BatOption.bind (monomials_from_texp t texp) + (fun monomiallist -> + let d = Option.get t.d in + let module IMap = IntMap in + let accumulate_constants (exprcache,(aconst,adiv)) (v,offs,divi) = match v with + | None -> let gcdee = Z.gcd adiv divi in exprcache,(Z.(aconst*divi/gcdee + offs*adiv/gcdee),Z.lcm adiv divi) + | Some (coeff,idx) -> let (somevar,someoffs,somedivi)=Rhs.subst (EConjI.get_rhs d idx) idx (v,offs,divi) in (* normalize! *) + let newcache = Option.map_default (fun (coef,ter) -> IMap.add ter Q.((IMap.find_default zero ter exprcache) + make coef somedivi) exprcache) exprcache somevar in + let gcdee = Z.gcd adiv divi in + (newcache,(Z.(aconst*divi/gcdee + offs*adiv/gcdee),Z.lcm adiv divi)) + in + let (expr,constant) = List.fold_left accumulate_constants (IMap.empty,(Z.zero,Z.one)) monomiallist in (* abstract simplification of the guard wrt. reference variables *) + Some (IMap.fold (fun v c acc -> if Q.equal c Q.zero then acc else (Q.num c,v,Q.den c)::acc) expr [], constant) ) + + let simplified_monomials_from_texp (t: t) texp = + let res = simplified_monomials_from_texp t texp in + if M.tracing then M.tracel "from_texp" "%s %a -> %s" (EConjI.show @@ BatOption.get t.d) Texpr1.Expr.pretty texp + (BatOption.map_default (fun (l,(o,d)) -> List.fold_right (fun (a,x,b) acc -> Printf.sprintf "%s*var_%d/%s + %s" (Z.to_string a) x (Z.to_string b) acc) l ((Z.to_string o)^"/"^(Z.to_string d))) "" res); + res + + let simplify_to_ref_and_offset (t: t) texp = + BatOption.bind (simplified_monomials_from_texp t texp ) + (fun (sum_of_terms, (constant,divisor)) -> + (match sum_of_terms with + | [] -> Some (None, constant,divisor) + | [(coeff,var,divi)] -> Some (Rhs.canonicalize (Some (Z.mul divisor coeff,var), Z.mul constant divi,Z.mul divisor divi)) + |_ -> None)) + + let simplify_to_ref_and_offset t texp = Timing.wrap "coeff_vec" (simplify_to_ref_and_offset t) texp + + (*TODO We also only catch variables on the first level, but miss e.g. (x+7)+7 -> use more recursion similar to negate?*) + let rec to_inequalities (t:t) texpr = + let open Apron.Texpr1 in + let inequality_from_add var expr = + let v = eval_texpr t expr in (*TODO we evaluate some subexpressions twice when calling this in assign_texpr -> bad for performance??*) + match Value.minimal v, Value.maximal v with + | Some (Int min), Some (Int maxi) when min = maxi -> [] (*Should be caught by the lin2var domain -> do not repeat that information*) + | Some (Int min), Some (Int maxi) -> [(Relation.Gt, Z.pred min), var; (Relation.Lt, Z.succ maxi), var] + | Some (Int min), _ -> [(Relation.Gt, Z.pred min), var] + | _,Some (Int maxi) -> [(Relation.Lt, Z.succ maxi), var] + | _,_ -> [] + in let inequality_from_mul var expr = + let v_expr = eval_texpr t expr in + let v_var = eval_texpr t (Var var) in + if Value.leq v_expr (Value.of_bigint Z.one) + || Value.leq v_var (Value.of_bigint Z.zero) + then [] (*Should be caught by the lin2var domain -> do not repeat that information*) + else + match Value.must_be_pos v_expr, Value.must_be_neg v_expr, Value.must_be_pos v_var, Value.must_be_neg v_var with + | true, _ , true, _ -> if Value.contains v_expr Z.one then [(Relation.Gt, Z.minus_one), var] else [(Relation.Gt, Z.zero), var] + | _, true, _ , true -> [(Relation.Gt, Z.zero), var] + | true, _ , _ , true -> if Value.contains v_expr Z.one then [(Relation.Lt, Z.one), var] else [(Relation.Lt, Z.zero), var] + | _ , true, true, _ -> [(Relation.Lt, Z.zero), var] + | _ , _ , _ , _ -> [] + in match texpr with + | Binop (Add, Var x, Var y, _, _) -> inequality_from_add x (Var y) @ inequality_from_add y (Var x) + | Binop (Add, e, Var y, _, _) + | Binop (Add, Var y, e, _, _) -> inequality_from_add y e + | Binop (Mul, Var x, Var y, _, _) -> inequality_from_mul x (Var y) @ inequality_from_mul y (Var x) + | Binop (Mul, e, Var y, _, _) + | Binop (Mul, Var y, e, _, _) -> inequality_from_mul y e + | Binop (Sub, Var y, e, _, _) -> + let v = eval_texpr t e in begin + match Value.minimal v, Value.maximal v with + | Some (Int min), Some (Int maxi) when min = maxi -> [] (*Should be caught by the lin2var domain -> do not repeat that information*) + | Some (Int min), Some (Int maxi) -> [(Relation.Lt, Z.succ @@ Z.neg min), y; (Relation.Gt, Z.pred @@ Z.neg maxi), y] + | Some (Int min), _ -> [(Relation.Lt, Z.succ @@ Z.neg min), y] + | _,Some (Int maxi) -> [(Relation.Gt, Z.pred @@ Z.neg maxi), y] + | _,_ -> [] + end + | Binop (Div, Var y, e, _, _) -> begin + let v_expr = eval_texpr t e in + let v_var = eval_texpr t (Var y) in + if Value.leq v_expr (Value.of_bigint Z.one) + || Value.leq v_var (Value.of_bigint Z.zero) + then [] (*Should be caught by the lin2var domain -> do not repeat that information*) + else + match Value.must_be_pos v_expr, Value.must_be_neg v_expr, Value.must_be_pos v_var, Value.must_be_neg v_var with + | true, _ , true, _ -> if Value.contains v_expr Z.one then [(Relation.Lt, Z.one), y] else [(Relation.Lt, Z.zero), y] + | _, true, _ , true -> [(Relation.Gt, Z.zero), y] + | true, _ , _ , true -> if Value.contains v_expr Z.one then [(Relation.Gt, Z.minus_one), y] else [(Relation.Gt, Z.zero), y] + | _ , true, true, _ -> [(Relation.Lt, Z.zero), y] + | _ , _ , _ , _ -> [] + end + | Binop (Mod, e, Var y, _, _) -> + let v_var = eval_texpr t (Var y) in + if Value.must_be_pos v_var then + [(Relation.Lt, Z.zero), y] + else if Value.must_be_neg v_var then + [(Relation.Gt, Z.zero), y] + else [] + | Unop (Neg, e, _, _) -> + let v = eval_texpr t e in begin + match Value.minimal v, Value.maximal v with + | Some (Int min), _ when Z.geq min Z.zero -> + let neg_cond = (Relation.Lt, Z.sub Z.one @@ Z.add min min ) in (*relation of -x to x*) + List.filter_map (fun (old_cond,var) -> BatOption.map (fun x -> x,var) @@ Relation.combine neg_cond old_cond) (to_inequalities t e) + | _, Some (Int maxi) when Z.leq maxi Z.zero -> + let neg_cond = (Relation.Gt, Z.sub Z.minus_one @@ Z.add maxi maxi ) in (*relation of -x to x*) + List.filter_map (fun (old_cond,var) -> BatOption.map (fun x -> x,var) @@ Relation.combine neg_cond old_cond) (to_inequalities t e) + | _,_ -> [] + end + | Unop (Cast, e, _, _) -> to_inequalities t e + | Var x -> [] (*Should be caught by the lin2var domain -> do not repeat that information*) + | _ -> [] + + let to_inequalities (t:t) texpr = + let res = to_inequalities t texpr in + let show_ineq (cond, var) = Relation.show "expr" cond (Var.show var) ^ ", " + in if M.tracing then M.tracel "inequalities" "expr: %a ineq: %s" Texpr1.Expr.pretty texpr (List.fold (^) "" @@ List.map show_ineq res); + res + + + let assign_const t var const divi = match t.d with + | None -> t + | Some t_d -> {d = Some (EConjI.set_rhs t_d var @@ Rhs.canonicalize (None, const, divi)); env = t.env} + + +end + + +module ExpressionBounds (Ineq : TwoVarInequalities): (SharedFunctions.ConvBounds with type t = VarManagement(Ineq).t) = +struct + include VarManagement (Ineq) + + let bound_texpr t texpr = + let v = eval_texpr t (Texpr1.to_expr texpr) in + let from_top = function + | TopIntOps.Int x -> Some x + | _ -> None + in let min = BatOption.bind (Value.minimal v) (from_top) + in let max = BatOption.bind (Value.maximal v) (from_top) in + (if M.tracing then M.tracel "bounds" "min: %s max: %s" (BatOption.map_default Z.to_string "None" min) (BatOption.map_default Z.to_string "None" max); + min, max) + + let bound_texpr d texpr1 = Timing.wrap "bounds calculation" (bound_texpr d) texpr1 +end + +module D (Ineq : TwoVarInequalities) = +struct + include Printable.Std + include RatOps.ConvenienceOps (SharedFunctions.Mpqf) + module VarManagement = VarManagement(Ineq) + include VarManagement + + module Bounds = ExpressionBounds(Ineq) + module V = RelationDomain.V + module Arg = struct + let allow_global = true + end + module Convert = SharedFunctions.Convert (V) (Bounds) (Arg) (SharedFunctions.Tracked) + + type var = V.t + + let name () = "lin2vareq_pentagon" + + let to_yojson _ = failwith "ToDo Implement in future" + + (** t.d is some empty array and env is empty *) + let is_bot t = equal t (bot ()) + + (** forall x_i in env, x_i:=X_i+0 *) + let top_of env = {d = Some (EConjI.make_empty_with_size (Environment.size env)); env = env} + + (** env = \emptyset, d = Some([||]) *) + let top () = {d = Some (EConjI.empty()); env = empty_env} + + (** is_top returns true for top_of array and empty array; precondition: t.env and t.d are of same size *) + let is_top t = GobOption.exists EConjI.is_top_con t.d + + let is_top_env t = (not @@ Environment.equal empty_env t.env) && GobOption.exists EConjI.is_top_con t.d + + let to_subscript i = + let transl = [|"₀";"₁";"₂";"₃";"₄";"₅";"₆";"₇";"₈";"₉"|] in + let rec subscr i = + if i = 0 then "" + else (subscr (i/10)) ^ transl.(i mod 10) in + subscr i + + let show_var env i = + let res = Var.to_string (Environment.var_of_dim env i) in + match String.split_on_char '#' res with + | varname::rest::[] -> varname ^ (try to_subscript @@ int_of_string rest with _ -> "#" ^ rest) + | _ -> res + + (** prints the current variable equalities with resolved variable names *) + let show varM = + match varM.d with + | None -> "⊥\n" + | Some (((dim,_), _, _) as arr) -> + if is_bot varM then + "Bot \n" + else + EConjI.show_formatted (show_var varM.env) arr ^ (to_subscript dim) + + let pretty () (x:t) = text (show x) + let printXml f x = BatPrintf.fprintf f "\n\n\nequalities\n\n\n%s\n\nenv\n\n\n%a\n\n\n" (XmlUtil.escape (show x)) Environment.printXml x.env + let eval_interval ask t texpr = + let from_top = function + | TopIntOps.Int x -> Some x + | _ -> None + in let i = eval_texpr t (Texpr1.to_expr texpr) + in if M.tracing then M.tracel "eval_interval" "evaluating %a in %s to %s" Texpr1.pretty texpr (show t) (Value.show i); + match fst i with + | None -> (None, None) + | Some (l, u) -> (from_top l, from_top u) + + let refine_with_tcons t tcons = + match t.d with + | None -> t + | Some d -> + let initial_value = match Tcons1.get_typ tcons with + | EQ | DISEQ -> Value.of_bigint Z.zero + | SUP -> Some (Int Z.one, Top Pos), Value.C.top_of IChar + | SUPEQ -> Some (Int Z.zero, Top Pos), Value.C.top_of IChar + | EQMOD (n) -> + begin match SharedFunctions.int_of_scalar ?round:None n with + None -> Value.top + | Some n -> Value.of_congruence (Z.zero, n) + end + in + let is_inequality = Tcons1.get_typ tcons = DISEQ in + let refine_var d var value = + let dim = Environment.dim_of_var t.env var in + if is_inequality then begin + (*If the value is at the bounds of the interval of var, we can make it smaller*) + match Value.to_int value with + | Some (Int v) -> let old_value = (EConjI.get_value d dim) in + if Value.minimal old_value = Some (Int v) then + EConjI.meet_with_one_value dim (Value.starting @@ Z.succ v) d false + else if Value.maximal old_value = Some (Int v) then + EConjI.meet_with_one_value dim (Value.ending @@ Z.pred v) d false + else d + | _-> d + end else ( + if M.tracing then M.trace "refine_tcons" "refining var %s with %s" (Var.to_string var) (Value.show value) ; + EConjI.meet_with_one_value dim value d false ) + in + let eval d texpr = eval_texpr {d= Some d; env = t.env} texpr in + let open Texpr1 in + let rec refine_values d value expr = + if M.tracing then M.trace "refine_tcons" "refining expr %s with %s" (GobFormat.asprint print_expr expr) (Value.show value) ; + match expr with + | Binop (op,a,b,_,_) -> + let refine_both op_a op_b = + let b_val = eval d b in + let d' = refine_values d (op_a value b_val) a in + let a_val = eval d' a in + refine_values d' (op_b value a_val) b + in begin + match op with + | Add -> refine_both (Value.sub) (Value.sub) + | Sub -> refine_both (Value.add) (Fun.flip Value.sub) + (*Because the overflow handeling in SharedFunctions guarantees us no wrapping behaviour, this is always invertible *) + | Mul -> refine_both (Value.div) (Value.div) + (*DIV and MOD are largely adapted from BaseInvariant*) + | Div -> + (* Integer division means we need to add the remainder, so instead of just `a = c*b` we have `a = c*b + a%b`. + * However, a%b will give [-b+1, b-1] for a=top, but we only want the positive/negative side depending on the sign of c*b. + * If c*b = 0 or it can be positive or negative, we need the full range for the remainder. *) + let b_val = eval d b in + if Value.to_int b_val = Some (Int Z.zero) then begin + if not !AnalysisState.executing_speculative_computations then M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Must Undefined Behavior: Second argument of div or mod is 0"; + d + end else + let a_val = eval d a in + let b_c = Value.mul b_val value in + let rem = + let is_pos = Value.must_be_pos b_c in + let is_neg = Value.must_be_neg b_c in + let full = Value.rem a_val b_val in + if is_pos then Value.meet (Value.starting Z.zero) full + else if is_neg then Value.meet (Value.ending Z.zero) full + else full + in let d' = refine_values d (Value.add b_c rem) a in + if Value.contains value Z.zero then d' else (*do not divide by zero for our refinements*) + refine_values d' (Value.div (Value.sub a_val rem) value) b + | Mod -> + (* a' = a/b*b + c and derived from it b' = (a-c)/(a/b) + * The idea is to formulate a' as quotient * divisor + remainder. *) + let a_val = eval d a in + let b_val = eval d b in + if Value.to_int b_val = Some (Int Z.zero) then begin + if not !AnalysisState.executing_speculative_computations then M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Must Undefined Behavior: Second argument of div or mod is 0"; + d + end else + let a' = Value.add (Value.mul (Value.div a_val b_val) b_val) value in + let a_c = (Value.div a_val value) in + let b' = Value.div (Value.sub a_val value) a_c in + (* However, for [2,4]%2 == 1 this only gives [3,4]. + * If the upper bound of a is divisible by b, we can also meet with the result of a/b*b - c to get the precise [3,3]. + * If b is negative we have to look at the lower bound. *) + let is_divisible bound = + match bound a_val with + | Some (TopIntOps.Int ba) -> Value.rem (Value.of_bigint ba) b_val |> Value.to_int = Some (Int Z.zero) + | _ -> false + in + let max_pos = match Value.maximal b_val with None -> true | Some x -> TopIntOps.compare x TopIntOps.zero >= 0 in + let min_neg = match Value.minimal b_val with None -> true | Some x -> TopIntOps.compare x TopIntOps.zero < 0 in + let implies a b = not a || b in + let a'' = + if implies max_pos (is_divisible Value.maximal) && implies min_neg (is_divisible Value.minimal) then + Value.meet a' (Value.sub (Value.mul (Value.div a_val b_val) b_val) value) + else a' + in + let a''' = + (* if both b and c are definite, we can get a precise value in the congruence domain *) + match Value.to_int b_val, Value.to_int value with + | Some (TopIntOps.Int b), Some (TopIntOps.Int c) -> + (* a%b == c -> a: c+bℤ *) + let t = Value.of_congruence (c, b) in + (*If the calculated congruence implies this one, we have a contradiction*) + if is_inequality && Value.leq a_val (Value.of_congruence (c,b)) then raise EConj.Contradiction; + Value.meet a'' t + | _, _ -> a'' + in + let d' = if Value.contains b' Z.zero || Value.contains a_c Z.zero then d else refine_values d (b') b in + refine_values d' (a''') a + | Pow -> failwith "refine_with tcons: pow unsupported" + end + | Unop (op, e,_,_) -> begin match op with + | Neg -> refine_values d (Value.neg value) e + | Cast -> refine_values d value e + | Sqrt -> failwith "sqrt is not supported" + end + | Cst (Scalar x) -> + begin match SharedFunctions.int_of_scalar ?round:None x with + | Some x -> (if Value.contains value x || is_inequality then d else raise EConj.Contradiction) + | None -> d + end + | Cst (Interval _) -> failwith "constant was an interval; this is not supported" + | Var v -> refine_var d v value + in let refine_inequalities ((econ, vs, ineq) as d) expr = + let rhss = EConjI.get_rhs d in + let vss = EConjI.get_value d in + (*a - b + interval (in arbitrary order)*) + let meet_relation a b value = + if M.tracing then M.tracel "refine_tcons" "meet_relation: %s - %s + %s" (Var.show a) (Var.show b) (Value.show value); + let dim_a = Environment.dim_of_var t.env a in + let dim_b = Environment.dim_of_var t.env b in + if M.tracing then M.tracel "meet_relation" "calling from refine with %s inside %s" (Tcons1.show tcons) (EConjI.show d); + let ineq', value_refinements = match Value.minimal value, Value.maximal value, Tcons1.get_typ tcons with + | _, Some (Int max), SUP -> Ineq.meet_relation dim_b dim_a (Relation.Lt, max) rhss vss ineq + | _, Some (Int max), SUPEQ -> Ineq.meet_relation dim_b dim_a (Relation.Lt, Z.succ max) rhss vss ineq + | Some min, Some max, EQ -> begin + if TopIntOps.equal min max then ineq, [] else (*If this is a constant, we have a equality that the lin2vareq domain should handle*) + let ineq, refine = match min with + | Int min -> Ineq.meet_relation dim_b dim_a (Relation.Gt, Z.pred min) rhss vss ineq + | _ -> ineq, [] + in match max with + | Int max -> BatTuple.Tuple2.map2 ((@) refine) @@ Ineq.meet_relation dim_b dim_a (Relation.Lt, Z.succ max) rhss vss ineq + | _ -> ineq, refine + end + | _, _,_ -> ineq, [] + in EConjI.apply_refinements value_refinements (econ, vs, ineq') + in match expr with (*TODO we could do this in a more general way -> normalisation??*) + (*currently only hits if two variables are at the first two levels. Also, we only choose one pattern even if multiple are possible + e.g. x + y - z arbitrarily selects x or y to convert into an interval, instead we could meet for both*) + | Binop (Add, Var a, (Binop (Sub, exp, Var b,_,_)),_,_) + | Binop (Add, exp, (Binop (Sub, Var a, Var b,_,_)),_,_) + | Binop (Add, (Binop (Sub, exp, Var b,_,_)), Var a, _,_) + | Binop (Add, (Binop (Sub, Var a, Var b,_,_)), exp, _,_) + | Binop (Sub, (Binop (Add, Var a, exp,_,_)), Var b, _,_) + | Binop (Sub, (Binop (Add, exp, Var a,_,_)), Var b, _,_) + | Binop (Sub, exp, (Binop (Sub, Var b, Var a,_,_)),_,_) -> meet_relation a b (eval_texpr {d=Some d;env=t.env} exp) + | Binop (Sub, Var a, Var b, _, _) -> meet_relation a b (Value.of_bigint Z.zero) + | Binop (Sub, (Binop (Sub, Var a, Var b,_,_)), exp, _,_) + | Binop (Sub, (Binop (Sub, Var a, exp,_,_)), Var b, _,_) + | Binop (Sub, Var a, (Binop (Add, Var b, exp,_,_)),_,_) + | Binop (Sub, Var a, (Binop (Add, exp, Var b,_,_)),_,_) -> meet_relation a b (Value.neg @@ eval_texpr {d=Some d;env=t.env} exp) + | _ -> d + in try + let expr = to_expr @@ Tcons1.get_texpr1 tcons in + let d' = refine_values d initial_value expr in + let d'' = refine_inequalities d' expr in + {d=Some d'';env=t.env} + with EConj.Contradiction -> bot_env + + let refine_with_tcons t tcons = + if M.tracing then M.tracel "refine_tcons" "refining %s with %s" (show t) (Tcons1.show tcons); + let res = refine_with_tcons t tcons in + if M.tracing then M.tracel "refine_tcons" "result: %s" (show res) ; + res + + let meet_with_one_conj t i (var, o, divi) = + match t.d with + | None -> t + | Some d -> + try + { d = Some (EConjI.meet_with_one_conj d i (var, o, divi)); env = t.env} + with EConj.Contradiction -> + if M.tracing then M.trace "meet" " -> Contradiction with conj\n"; + { d = None; env = t.env} + + let meet_with_one_conj t i e = + let res = meet_with_one_conj t i e in + if M.tracing then M.tracel "meet" "%s with single eq %s=%s -> %s" (show t) (Z.(to_string @@ Tuple3.third e)^ show_var t.env i) (Rhs.show_rhs_formatted (show_var t.env) e) (show res); + res + + let meet_with_one_value narrow i value t = + let res = match t.d with + | None -> t + | Some d -> + try + { d = Some (EConjI.meet_with_one_value i value d narrow); env = t.env} + with EConj.Contradiction -> + if M.tracing then M.trace "meet" " -> Contradiction with value\n"; + { d = None; env = t.env} + in + if M.tracing then M.tracel "meet" "%s with single value %s=%s -> %s" (show t) (show_var t.env i) (Value.show value) (show res); + res + + let meet_with_inequalities narrow t_ineq t = + match t_ineq.d, t.d with + | _, None + | None, _ -> t + | Some (_,_,ineq), Some ((econ, vs, ineq2) as d) -> + try + let new_ineqs, refinements = (if narrow then Ineq.narrow else Ineq.meet) (EConjI.get_value d) ineq ineq2 + in let new_ineqs = Ineq.limit econ new_ineqs + in let d' = (econ, vs, new_ineqs) + in let d''= EConjI.apply_refinements refinements d' + in { d = Some d''; env = t.env} + with EConj.Contradiction -> + if M.tracing then M.trace "meet" " -> Contradiction with inequalities\n"; + { d = None; env = t.env} + + let meet_with_inequalities narrow ineq t = + let res = meet_with_inequalities narrow ineq t in + if M.tracing then M.tracel "meet" "%s with inequalities from %s -> %s" (show t) (show ineq) (show res); + res + + let meet' t1 t2 narrow = + 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 (econ, vs, _), Some (econ2, vs2, _) -> + let t1_conj = IntMap.fold (fun lhs rhs map -> meet_with_one_conj map lhs rhs) (snd econ2) t1 (* even on sparse d2, this will chose the relevant conjs to meet with*) + in let t1_val = IntMap.fold (meet_with_one_value narrow) vs2 t1_conj + (*meet conj with t2 as well so that for both the inequalities refer to the correct roots*) + in let t2_conj = IntMap.fold (fun lhs rhs map -> meet_with_one_conj map lhs rhs) (snd econ) t2 + in meet_with_inequalities narrow t2_conj t1_val + | _ -> {d = None; env = sup_env} + + let meet t1 t2 = + meet' t1 t2 false + + let meet t1 t2 = + let res = meet t1 t2 in + if M.tracing then M.tracel "meet" "meet a: %s\n U \n b: %s \n -> %s" (show t1) (show t2) (show res) ; + res + + let meet t1 t2 = Timing.wrap "meet" (meet t1) t2 + + let leq t1 t2 = + let env_comp = Environment.cmp t1.env t2.env in (* Apron's Environment.cmp has defined return values. *) + let implies ts i (var, offs, divi) = + let tuple_cmp = Tuple3.eq (Option.eq ~eq:(Tuple2.eq (Z.equal) (Int.equal))) (Z.equal) (Z.equal) in + match var with + (* directly compare in case of constant value *) + | None -> tuple_cmp (var, offs, divi) (EConj.get_rhs ts i) + (* normalize in case of a full blown equality *) + | Some (coeffj,j) -> tuple_cmp (EConj.get_rhs ts i) @@ Rhs.subst (EConj.get_rhs ts j) j (var, offs, divi) + in + let implies_value v i value = Value.leq (EConjI.get_value v i) value + in + if is_bot t1 then true else + if BatOption.is_none t1.d then true else (*This kind of bot does not require the environment to be a superset*) + if env_comp = -2 || env_comp > 0 then false else + if is_bot_env t1 || is_top_env t2 then true + else if is_bot_env t2 || is_top_env t1 then false else + let m1, (econ2, vs2, ineq2) = Option.get t1.d, Option.get t2.d in + let (econ1, vs1, ineq1) = if env_comp = 0 then m1 else VarManagement.dim_add (Environment.dimchange t1.env t2.env) m1 in + (*make ineq1 refer to the new representants*) + let transform_non_representant var (m,o,d) ineq_acc = + match m with + | None -> ineq_acc + | Some (c,v) -> + match EConj.get_rhs econ1 var with + | Some (_,v),_,_ when v <> var -> ineq_acc + | _ -> let ineq', _ = Ineq.substitute (EConjI.get_value (econ1, vs1, ineq1)) ineq_acc var (c,v,o,d) in ineq' + in + let ineq1' = IntMap.fold transform_non_representant (snd econ2) ineq1 in + (*further, econ2 might have some new representants -> transform further*) + let ineq1' = Ineq.copy_to_new_representants econ1 econ2 (EConjI.get_value (econ2, vs2, ineq2)) ineq1' in + if M.tracing then M.trace "leq" "transformed %s into %s" (Ineq.show_formatted (fun i -> Var.show @@ Environment.var_of_dim t2.env i) ineq1) (Ineq.show_formatted (fun i -> Var.show @@ Environment.var_of_dim t2.env i) ineq1'); + (*Normally, we do not apply closure to the intervals because it is too expensive (O(n^3)), but if we do not do it here, we get some actually implied elements being not leq, failing verifying*) + let rec refine_intervals_until_fixpoint t = + let refinements = Ineq.interval_refinements (EConjI.get_value t) (Tuple3.third t) in + if M.tracing then M.trace "leq" "refined with %s" (Refinement.show_formatted (fun i -> Var.show @@ Environment.var_of_dim t2.env i) refinements); + let t' = EConjI.apply_refinements ~refine_depth:1 refinements t in + if t = t' then t else refine_intervals_until_fixpoint t' + in + try + let (econ1', _, ineq1') as m1' = Timing.wrap "leq_refine" refine_intervals_until_fixpoint (econ1, vs1, ineq1') in + if M.tracing then M.trace "leq" "refined into %s" (EConjI.show_formatted (fun i -> Var.show @@ Environment.var_of_dim t2.env i) m1'); + (*TODO the transformations are likely the most expensive part. -> only do it when econj did not rule it out*) + IntMap.for_all (implies econ1') (snd econ2) (* even on sparse m2, it suffices to check the non-trivial equalities, still present in sparse m2 *) + && (if M.tracing then M.trace "leq" "econj true"; + IntMap.for_all (implies_value m1') (vs2)) + && (if M.tracing then M.trace "leq" "values true"; Ineq.leq ineq1' (EConjI.get_value m1') ineq2) + with EConj.Contradiction -> + if M.tracing then M.trace "leq" "refinement showed contradiction"; + true (*t1 was secretely bot -> leq all*) + + + let leq a b = Timing.wrap "leq" (leq a) b + + let leq t1 t2 = + let res = leq t1 t2 in + if M.tracing then M.tracel "leq" "leq a: %s b: %s -> %b" (show t1) (show t2) res ; + res + + let join' widen a b = + let join_econj ad bd env = (LinearTwoVarEqualityDomain.D.join {d = Some ad; env} {d = Some bd; env}).d + in + (*Check all variables (up to index vars) if we need to save an value for them*) + let rec collect_values x y econj_joined vars t = + if vars < 0 then t + else if EConj.nontrivial econj_joined vars then collect_values x y econj_joined (vars-1) t (*we only need values for roots of the connected components*) + else let joined_value = (if widen then Value.widen else Value.join) (EConjI.get_value x vars) (EConjI.get_value y vars) in + collect_values x y econj_joined (vars-1) (EConjI.meet_with_one_value vars joined_value t false) + in + let join_d ((econ_x, _, ineq_x) as x) ((econ_y, _, ineq_y) as y) env = + let econj' = join_econj (econ_x) (econ_y) env in + match econj' with + None -> None + | Some econj'' -> + if M.tracing then M.tracel "join" "join_econj of %s, %s resulted in %s" (EConjI.show x) (EConjI.show y) (EConj.show @@ snd econj''); + let (e,v,i) = collect_values x y econj'' ((Environment.size env)-1) (econj'', IntMap.empty, ineq_x) in (*ineq_x doesn't matter*) + (*transform the inequalities to represent only representants, and make the inequalities for new representants explicit*) + let transform_non_representant get_value var rhs ineq_acc = + match rhs with + | (Some (c,v), o, d) when v <> var -> let ineq', _ = Ineq.substitute get_value ineq_acc var (c,v,o,d) in ineq' + | _ -> ineq_acc + in + let ineq_x_split = IntMap.fold (transform_non_representant (EConjI.get_value x)) (snd econj'') @@ Ineq.copy_to_new_representants econ_x econj'' (EConjI.get_value x) ineq_x in + let ineq_y_split = IntMap.fold (transform_non_representant (EConjI.get_value y)) (snd econj'') @@ Ineq.copy_to_new_representants econ_y econj'' (EConjI.get_value y) ineq_y in + let ineq' = (if widen then Ineq.widen else Ineq.join) ineq_x_split (EConjI.get_value x) ineq_y_split (EConjI.get_value y) in + Some (e,v, Ineq.limit e ineq') + in + (*This is a different kind of bot that we need to catch*) + if is_bot a then b else + if is_bot b then a else + (*Normalize the two domains a and b such that both talk about the same variables*) + match a.d, b.d with + | None, _ -> b + | _, None -> a + | Some x, Some y when is_top_env a || is_top_env b -> + let new_env = Environment.lce a.env b.env in + top_of new_env + | Some x, Some y when (Environment.cmp a.env b.env <> 0) -> + let sup_env = Environment.lce a.env b.env in + let mod_x = dim_add (Environment.dimchange a.env sup_env) x in + let mod_y = dim_add (Environment.dimchange b.env sup_env) y in + {d = join_d mod_x mod_y sup_env; env = sup_env} + | Some x, Some y when EConjI.equal x y -> {d = Some x; env = a.env} + | Some x, Some y -> {d = join_d x y a.env; env = a.env} + + + let join = join' false + 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.tracel "join" "join a: %s b: %s -> %s" (show a) (show b) (show res) ; + (*assert(leq a res); + assert(leq b res);*) + res + + let widen = join' true + + let widen a b = + let res = widen a b in + if M.tracing then M.tracel "widen" "widen a: %s b: %s -> %s" (show a) (show b) (show res) ; + res + + let narrow a b = meet' a b true + + let narrow a b = + let res = narrow a b in + if M.tracing then M.tracel "narrow" "narrow a: %s b: %s -> %s" (show a) (show b) (show res) ; + res + + let pretty_diff () (x, y) = + dprintf "%s: %a not leq %a" (name ()) pretty x pretty y + + let forget_var t var = + if is_bot_env t || is_top_env t then t + else + {d = Some (EConjI.forget_variable (Option.get t.d) (Environment.dim_of_var t.env var)); env = t.env} + + let forget_vars t vars = + if is_bot_env t || is_top_env t || List.is_empty vars then + t + else + let newm = List.fold (fun map i -> EConjI.forget_variable map (Environment.dim_of_var t.env i)) (Option.get t.d) vars in + {d = Some newm; env = t.env} + + let forget_vars t vars = + let res = forget_vars t vars in + if M.tracing then M.tracel "ops" "forget_vars %s -> %s" (show t) (show res); + res + + let forget_vars t vars = Timing.wrap "forget_vars" (forget_vars t) vars + + (** implemented as described on page 10 in the paper about Fast Interprocedural Linear Two-Variable Equalities in the Section "Abstract Effect of Statements" + This makes a copy of the data structure, it doesn't change it in-place. *) + let assign_texpr (t: VarManagement.t) var texp assign_value = + match t.d with + | Some ((econj, vs, ineq_old) as d) -> + let var_i = Environment.dim_of_var t.env var (* this is the variable we are assigning to *) in + let t' = match simplify_to_ref_and_offset t texp with + | None -> + (* Statement "assigned_var = ?" (non-linear assignment) *) + forget_var t var + | Some (None, off, divi) -> + (* Statement "assigned_var = off" (constant assignment) *) + assign_const (forget_var t var) var_i off divi + | Some (Some (coeff_var,exp_var), off, divi) when var_i = exp_var -> + (* Statement "assigned_var = (coeff_var*assigned_var + off) / divi" *) + let econji' = econj, IntMap.remove var_i vs, ineq_old in + {d=Some (EConjI.affine_transform econji' var_i (coeff_var, var_i, off, divi)); env=t.env } + | Some (Some monomial, off, divi) -> + (* Statement "assigned_var = (monomial) + off / divi" (assigned_var is not the same as exp_var) *) + meet_with_one_conj (forget_var t var) var_i (Some (monomial), off, divi) + in + let t' = if assign_value then meet_with_one_value false var_i (eval_texpr t texp) t' else t' (*value will be updated afterwards with query*) in + begin match t'.d with + None -> if M.tracing then M.tracel "ops" "assign_texpr resulted in bot (before: %s, expr: %s) " (show t) (Texpr1.show (Texpr1.of_expr t.env texp)); + bot_env + | Some d' -> + if M.tracing then M.tracel "assign_texpr" "assigning %s = %s before inequality: %s" (Var.show var) (Texpr1.show (Texpr1.of_expr t.env texp)) (show {d = Some d'; env = t.env}); + let meet_cond (e,v,ineq) (cond, var) = + let dim = Environment.dim_of_var t.env var in + if dim <> var_i then + let ineq', refinements = Ineq.meet_relation var_i dim cond (EConjI.get_rhs d') (EConjI.get_value d') ineq + in EConjI.apply_refinements refinements (e,v,ineq') + else + let ineq', refinements = Ineq.transfer dim cond ineq_old (EConjI.get_rhs d) (EConjI.get_value d) ineq (EConjI.get_rhs d') (EConjI.get_value d') + (*TODO value for i will be overwritten -> delay refinement?*) + in EConjI.apply_refinements (Refinement.rhs_only refinements) (e,v,ineq') + in + let d'' = List.fold meet_cond d' (VarManagement.to_inequalities t texp) in + if M.tracing then M.tracel "assign_texpr" "after inequality: %s" (show {d = Some d''; env = t.env}); + {d = Some d''; env = t'.env} + end + | None -> bot_env + + let assign_texpr t var texp assign_value = + if M.tracing then M.tracel "assign_texpr" "before assign: %s, assign_value= %b" (show t) assign_value; + Timing.wrap "assign_texpr" (assign_texpr t var texp) assign_value + + (* no_ov -> no overflow + if it's true then there is no overflow + -> Convert.texpr1_expr_of_cil_exp handles overflow *) + 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 + let t = match Convert.texpr1_expr_of_cil_exp ask t t.env exp no_ov with + | texp -> if M.tracing then M.trace "assign_exp" "conversion success"; assign_texpr t var texp false + | exception Convert.Unsupported_CilExp _ -> if M.tracing then M.trace "assign_exp" "conversion failed"; forget_var t var + in + (*evaluate in the same way as is used for simplification*) + if M.tracing then M.trace "assign_exp" "assign_exp after EConjI + ineqs: %s" (show t); + match t.d with + | None -> t + | Some d -> + if exp = MyCFG.unknown_exp then + t + else + let value = + try Value.of_IntDomTuple + (GobRef.wrap AnalysisState.executing_speculative_computations true ( fun () -> + let ikind = Cilfacade.get_ikind_exp exp in + match ask.f (EvalInt exp) with + | `Bot (* This happens when called on a pointer type; -> we can safely return top *) + | `Top -> IntDomain.IntDomTuple.top_of ikind + | `Lifted x -> + if M.tracing then M.trace "assign_exp" "Query for %a returned %s" d_exp exp (IntDomain.IntDomTuple.show x); + x (* Cast should be unnecessary because it should be taken care of by EvalInt. *) + )) + with Invalid_argument _ -> Value.top (*get_ikind_exp failed*) + in + if M.tracing then M.trace "assign_exp" "value for %a set to %s" Var.pretty var (Value.show value); + (*TODO If the newly assigned value must be greater / lower than the old, we can restore some conditions?*) + let d' = if Value.is_bot value then Some ((EConjI.make_empty_with_size (Environment.size t.env))) + else Some (EConjI.set_value d (Environment.dim_of_var t.env var) value) + in {d= d'; env = t.env} + + + let assign_exp ask t var exp no_ov = + let res = assign_exp ask t var exp no_ov in + if M.tracing then M.tracel "ops" "assign_exp t:\n %s \n var: %a \n exp: %a\n no_ov: %b -> \n %s" + (show t) Var.pretty var d_exp exp (Lazy.force no_ov) (show res); + res + + let assign_var (t: VarManagement.t) v v' = + let t = add_vars t [v; v'] in + assign_texpr t v (Var v') true + + let assign_var t v v' = + let res = assign_var t v v' in + if M.tracing then M.tracel "ops" "assign_var t:\n %s \n v: %a \n v': %a\n -> %s" (show t) Var.pretty v Var.pretty v' (show res); + res + + (** Parallel assignment of variables. + First apply the assignments to temporary variables x' and y' to keep the old dependencies of x and y + and in a second round assign x' to x and y' to y + *) + let assign_var_parallel t vv's = + let assigned_vars = List.map fst vv's 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 (* TODO: we use primed vars in analysis, conflict? *) + 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 vv's in + match multi_t.d with + | Some arr when not @@ is_top_env 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 vv's = + let res = assign_var_parallel t vv's in + if M.tracing then M.tracel "ops" "assign_var parallel: %s -> %s" (show t) (show res); + res + + let assign_var_parallel t vv's = Timing.wrap "var_parallel" (assign_var_parallel t) vv's + + let assign_var_parallel_with t vv's = + (* TODO: If we are angling for more performance, this might be a good place ot try. `assign_var_parallel_with` is used whenever a function is entered (body), + in unlock, at sync edges, and when entering multi-threaded mode. *) + let t' = assign_var_parallel t vv's in + t.d <- t'.d; + t.env <- t'.env + + let assign_var_parallel_with t vv's = + if M.tracing then M.tracel "var_parallel" "assign_var parallel'"; + assign_var_parallel_with t vv's + + let assign_var_parallel' t vs1 vs2 = + let vv's = List.combine vs1 vs2 in + assign_var_parallel t vv's + + let assign_var_parallel' t vv's = + let res = assign_var_parallel' t vv's in + if M.tracing then M.tracel "ops" "assign_var parallel'"; + res + + let substitute_exp ask 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_var res var + + let substitute_exp ask t var exp no_ov = + let res = substitute_exp ask t var exp no_ov in + if M.tracing then M.tracel "ops" "Substitute_expr t: \n %s \n var: %a \n exp: %a \n -> \n %s" (show t) Var.pretty var d_exp exp (show res); + res + + let substitute_exp ask t var exp no_ov = Timing.wrap "substitution" (substitute_exp ask t var exp) no_ov + + (** Assert a constraint expression. + The overflow is completely handled by the flag "no_ov", + which is set in relationAnalysis.ml via the function no_overflow. + In case of a potential overflow, "no_ov" is set to false + and Convert.tcons1_of_cil_exp will raise the exception Unsupported_CilExp Overflow + + meet_tcons -> meet with guard in if statement + texpr -> tree expr (right hand side of equality) + -> expression used to derive tcons -> used to check for overflow + tcons -> tree constraint (expression < 0) + -> does not have types (overflow is type dependent) + *) + let meet_tcons ask t tcons original_expr no_ov = + match t.d with + | None -> t + | Some d -> + let expr = (Texpr1.to_expr @@ Tcons1.get_texpr1 tcons) in + (* meet EConj*) + let t' = match simplified_monomials_from_texp t expr with + | None -> t + | Some (sum_of_terms, (constant,divisor)) ->( + match sum_of_terms with + | [] -> (* no reference variables in the guard, so check constant for zero *) + begin match Tcons1.get_typ tcons with + | EQ when Z.equal constant Z.zero -> t + | SUPEQ when Z.geq constant Z.zero -> t + | SUP when Z.gt constant Z.zero -> t + | DISEQ when not @@ Z.equal constant Z.zero -> t + | EQMOD _ -> t + | _ -> bot_env (* all other results are violating the guard *) + end + | [(coeff, index, divi)] -> (* guard has a single reference variable only *) + if Tcons1.get_typ tcons = EQ then begin + meet_with_one_conj t index (Rhs.canonicalize (None, Z.neg @@ Z.(divi*constant),Z.(coeff*divisor))) + end else + t (* only EQ is supported in equality based domains *) + | [(c1,var1,d1); (c2,var2,d2)] -> (* two variables in relation needs a little sorting out *) + begin match Tcons1.get_typ tcons with + | EQ -> (* c1*var1/d1 + c2*var2/d2 +constant/divisor = 0*) + (* ======> c1*divisor*d2 * var1 = -c2*divisor*d1 * var2 +constant*-d1*d2*) + (* \/ c2*divisor*d1 * var2 = -c1*divisor*d2 * var1 +constant*-d1*d2*) + if M.tracing then M.tracel "meet_tcons" "meet_one_conj case 2"; + let open Z in + if var1 < var2 then + meet_with_one_conj t var2 (Rhs.canonicalize (Some (neg @@ c1*divisor,var1),neg @@ constant*d2*d1,c2*divisor*d1)) + else + meet_with_one_conj t var1 (Rhs.canonicalize (Some (neg @@ c2*divisor,var2),neg @@ constant*d2*d1,c1*divisor*d2)) + | _-> t (* Not supported in equality based 2vars without coeffiients *) + end + | _ -> t (* For equalities of more then 2 vars we just return t *)) + in if t'.d = None then (if M.tracing then M.tracel "meet_tcons" "meet_conj resulted in None (expr: %s)" (Tcons1.show tcons); t') else begin + if M.tracing then M.tracel "meet_tcons" "after conj: %s (expr: %s)" (show t') (Tcons1.show tcons); + refine_with_tcons t' tcons + end + + + let meet_tcons ask t tcons original_expr no_ov = + let res = meet_tcons ask t tcons original_expr no_ov + in if M.tracing then M.tracel "meet_tcons" "meet_tcons with expr: %a no_ov:%b : %s -> %s" d_exp original_expr (Lazy.force no_ov) (show t) (show res); + res + + + let meet_tcons t tcons expr = Timing.wrap "meet_tcons" (meet_tcons t tcons) expr + + let unify a b = + meet a b + + let unify a b = + let res = unify a b in + if M.tracing then M.tracel "ops" "unify: %s\n U\n %s -> %s" (show a) (show b) (show res); + res + + (** Assert a constraint expression. Defined in apronDomain.apron.ml + + If the constraint is never fulfilled, then return bottom. + Else the domain can be modified with the new information given by the constraint. + + It basically just calls the function meet_tcons. + + It is called by eval (defined in sharedFunctions), but also when a guard in + e.g. an if statement is encountered in the C code. + + *) + let assert_constraint ask d e negate (no_ov: bool Lazy.t) = + match Convert.tcons1_of_cil_exp ask d d.env e negate no_ov with + | tcons1 -> meet_tcons ask d tcons1 e no_ov + | exception Convert.Unsupported_CilExp _ -> d + + let assert_constraint ask d e negate no_ov = Timing.wrap "assert_constraint" (assert_constraint ask d e negate) no_ov + + let relift t = t + + (** representation as C expression + + This function returns all the equalities that are saved in our datastructure t. + + Lincons -> linear constraint *) + let invariant t = + let of_coeff xi coeffs o = + let typ = (Option.get @@ V.to_cil_varinfo xi).vtype in + let ikind = Cilfacade.get_ikind typ in + let cst = Coeff.s_of_z (IntDomain.Size.cast ikind o) in + let lincons = Lincons1.make (Linexpr1.make t.env) Lincons1.EQ in + Lincons1.set_list lincons coeffs (Some cst); + lincons + in + let get_const acc i = function + | (None, o, d) -> + let xi = Environment.var_of_dim t.env i in + of_coeff xi [(GobApron.Coeff.s_of_z @@ Z.neg d, xi)] o :: acc + | (Some (c,r), _,_) when r = i -> acc + | (Some (c,r), o, d) -> + let xi = Environment.var_of_dim t.env i in + let ri = Environment.var_of_dim t.env r in + of_coeff xi [(GobApron.Coeff.s_of_z @@ Z.neg d, xi); (GobApron.Coeff.s_of_z c, ri)] o :: acc + in + match t.d with + | None -> [] + | Some ((_,map),vs,ineq) -> + let from_ineq = Ineq.invariant ineq t.env in + let with_eq = IntMap.fold (fun lhs rhs list -> get_const list lhs rhs) map from_ineq in + IntMap.fold (Value.invariant t.env) vs with_eq + + let cil_exp_of_lincons1 = Convert.cil_exp_of_lincons1 + + let env t = t.env + + type marshal = t + (* marshal is not compatible with apron, therefore we don't have to implement it *) + let marshal t = t + + let unmarshal t = t + +end + +module D2 (Ineq : TwoVarInequalities): RelationDomain.RD with type var = Var.t = +struct + module D = D(Ineq) + module ConvArg = struct + let allow_global = false + end + include SharedFunctions.AssertionModule (D.V) (D) (ConvArg) + include D + + (*We can be more precise than the function from the AssertionModule by including congruence information*) + let eval_int ask d e no_ov = + let module ID = Queries.ID in + match Cilfacade.get_ikind_exp e with + | exception Cilfacade.TypeOfError _ + | exception Invalid_argument _ -> + ID.top () (* real top, not a top of any ikind because we don't even know the ikind *) + | ik -> + if M.tracing then M.trace "relation" "eval_int: exp_is_constraint %a = %B" d_plainexp e (exp_is_constraint e); + if exp_is_constraint e then + match check_assert ask d e no_ov with + | `True -> ID.of_bool ik true + | `False -> ID.of_bool ik false + | `Top -> ID.top_of ik + else + (*TODO we could also provide information for non-linear expressions*) + match Convert.texpr1_of_cil_exp ask d (env d) e no_ov with + | texpr1 -> + let (i, c) = eval_texpr d (Texpr1.to_expr texpr1) in + let (min, max) = IntDomain.Size.range ik in + let c = match c with + | None -> ID.bot_of ik + | Some c -> ID.of_congruence ik c + in let i = match i with + | None -> ID.bot_of ik + | Some (TopIntOps.Int l, TopIntOps.Int u) -> ID.of_interval ~suppress_ovwarn:true ik ((Z.max l min),(Z.min u max)) + | Some (TopIntOps.Int l, _) -> ID.starting ~suppress_ovwarn:true ik (Z.max l min) + | Some (_, TopIntOps.Int u) -> ID.ending ~suppress_ovwarn:true ik (Z.min u max) + | _ -> ID.top_of ik + in ID.meet c i + | exception Convert.Unsupported_CilExp _ -> ID.top_of ik + +end \ No newline at end of file diff --git a/src/cdomains/apron/linearTwoVarEqualityDomainPentagon.no-apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomainPentagon.no-apron.ml new file mode 100644 index 0000000000..5fed2c883c --- /dev/null +++ b/src/cdomains/apron/linearTwoVarEqualityDomainPentagon.no-apron.ml @@ -0,0 +1,5 @@ +(* 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. *) + +let reset_lazy () = () diff --git a/src/cdomains/apron/representantDomains.apron.ml b/src/cdomains/apron/representantDomains.apron.ml new file mode 100644 index 0000000000..88c7b51a07 --- /dev/null +++ b/src/cdomains/apron/representantDomains.apron.ml @@ -0,0 +1,1760 @@ +open Batteries +open GoblintCil +open GobApron + +module M = Messages + +module Rhs = LinearTwoVarEqualityDomain.Rhs + +module EConj = LinearTwoVarEqualityDomain.EqualitiesConjunction + +module IntMap = EConj.IntMap + +(*Modules for creating an unbounded interval arithmethic with the existing interval domain*) +module TopIntBase (Int_t : IntOps.IntOpsBase) = +struct + type sign = Pos | Neg [@@deriving eq, hash] + type t = Int of Int_t.t + | Top of sign [@@deriving eq, hash] + + let compare a b = match a, b with + | Int a, Int b -> Int_t.compare a b + | Top Neg, Top Neg + | Top Pos, Top Pos -> 0 + | _ , Top Pos + | Top Neg, _ -> -1 + | _ , Top Neg + | Top Pos, _ -> 1 + + let max_val = Int_t.add Int_t.one @@ Int_t.of_bigint @@ snd @@ IntDomain0.Size.range IULongLong + let min_val = Int_t.add (Int_t.of_int @@ -1) @@ Int_t.of_bigint @@ fst @@ IntDomain0.Size.range ILongLong + + let get_int_t = function + | Int i -> i + | Top Pos -> max_val (*needed so that we can call to_bigint on Top (e.g. for widening constants)*) + | Top Neg -> min_val + + let neg_s = function + | Pos -> Neg + | Neg -> Pos + + + let lift2 op t1 t2 = match t1, t2 with + Int t1, Int t2 -> Int (op t1 t2) + | Top Neg, Top Pos + | Top Pos, Top Neg -> Top Neg + | Top s, _ + | _, Top s -> Top s + + let lift2_1 op t1 t2 = match t1 with + | Int t1 -> Int (op t1 t2) + | t -> t + + let name () = Int_t.name () ^ " with top" + + let zero = Int (Int_t.zero) + let one = Int (Int_t.one) + + let lower_bound = Some (Top Neg) + let upper_bound = Some (Top Pos) + + let neg = function + | Int i -> Int (Int_t.neg i) + | Top Pos -> Top Neg + | Top Neg -> Top Pos + let abs = function + | Int i -> Int (Int_t.abs i) + | Top _ -> Top Pos + + let add a b = match a,b with + | Int a, Int b -> Int (Int_t.add a b) + | Top s, _ + | _, Top s -> Top s + let sub a b = match a,b with + | Int a, Int b -> Int (Int_t.sub a b) + | Top s, _ -> Top s + | Int _, Top Pos -> Top Neg + | Int _, Top Neg -> Top Pos + + + let mul a b = match a,b with + | Int a, Int b -> Int (Int_t.mul a b) + | Top s, Int x + | Int x, Top s -> + let comp = Int_t.compare x Int_t.zero in + if comp = 0 then Int (Int_t.zero) + else if comp < 0 then Top (neg_s s) + else Top s + | Top _, Top _ -> Top Pos (*TODO: Does not make sense. Does it need to?*) + let div a b = match a,b with + | Int a, Int b -> Int (Int_t.div a b) + | Top s, Int x -> + let comp = Int_t.compare x Int_t.zero in + if comp = 0 then Int (Int_t.zero) + else if comp < 0 then Top (neg_s s) + else Top s + | Int x, Top s -> Int (Int_t.zero) + | Top _, Top _ -> Top Pos (*TODO: Does not make sense. Does it need to?*) + + (*TODO will rem/gcd/shift/logical functions lead to problems??*) + let rem = lift2 Int_t.rem + let gcd = lift2 Int_t.gcd + + let shift_left = lift2_1 Int_t.shift_left + let shift_right = lift2_1 Int_t.shift_right + let logand = lift2 Int_t.logand + let logor = lift2 Int_t.logor + let logxor = lift2 Int_t.logxor + let lognot = function + | Int i -> Int (Int_t.lognot i) + | t -> t + + (**TODO not clear what this should do*) + let top_range _ _ = false + let max a b = + match a,b with + | Top Neg, m + | m, Top Neg -> m + | Top Pos, _ + | _, Top Pos -> Top Pos + | Int a, Int b -> Int (Int_t.max a b) + let min a b = + match a,b with + | Top Pos, m + | m, Top Pos -> m + | Top Neg, _ + | _, Top Neg -> Top Neg + | Int a, Int b -> Int (Int_t.min a b) + + let of_int i = Int (Int_t.of_int i) + let to_int t = Int_t.to_int @@ get_int_t t + + let of_int64 i = Int (Int_t.of_int64 i) + let to_int64 t = Int_t.to_int64 @@ get_int_t t + + let of_string s = if s = "+∞" then Top Pos else (if s = "-∞" then Top Pos else Int (Int_t.of_string s)) + let to_string = function + | Int i -> Int_t.to_string i + | Top Pos -> "+∞" + | Top Neg -> "-∞" + + (*Normalizes values outside the maximum range. Normalization is not done anywhere else + because we may temporarily have values outside that range e.g. when applying an equations*) + let of_bigint i = let i = Int_t.of_bigint i in + if Int_t.compare i max_val >= 0 + then Top Pos + else if Int_t.compare i min_val <= 0 + then Top Neg + else Int i + let to_bigint t = Int_t.to_bigint @@ get_int_t t + + let arbitrary () = failwith "arbitrary not implemented" +end + +(*TODO this is a copy of the IntOpsDecorator, but we keep the constructor of type t -> is there a better way??*) +module TopIntOps = struct + + include Printable.StdLeaf + include TopIntBase(IntOps.BigIntOpsBase) + let show = to_string + include Printable.SimpleShow ( + struct + type nonrec t = t + let show = to_string + end + ) + let pred x = sub x one + let of_bool x = if x then one else zero + let to_bool x = x <> zero + + (* These are logical operations in the C sense! *) + let log_op op a b = of_bool @@ op (to_bool a) (to_bool b) + let c_lognot x = of_bool (x = zero) + let c_logand = log_op (&&) + let c_logor = log_op (||) + let c_logxor = log_op (<>) + + let lt x y = of_bool (compare x y < 0) + let gt x y = of_bool (compare x y > 0) + let le x y = of_bool (compare x y <= 0) + let ge x y = of_bool (compare x y >= 0) + +end + +module Unbounded : IntervalDomain.BoundedIntOps with type t = TopIntOps.t = struct + include TopIntOps + + type t_interval = (t * t) option [@@deriving eq, ord, hash] + + let range _ = (Top Neg, Top Pos) + let top_of ik = Some (range ik) + let bot_of _ = None + + let norm ?(suppress_ovwarn=false) ?(cast=false) ik t = + let t = match t with + | Some (Top Pos, Top Neg) -> Some (Top Neg, Top Pos) + | Some (l, Top Neg) -> Some (l, Top Pos) + | Some (Top Pos, u) -> Some (Top Neg, u) + | Some (Int a, Int b) when Z.compare a b > 0 -> None + | _ -> t + in (t,IntDomain0.{underflow=false; overflow=false}) +end + +(*Combining operations into one reduced product for values*) +module IntervalAndCongruence = struct + module I = IntDomain0.SOverflowUnlifter(IntervalDomain.BoundedIntervalFunctor(Unbounded)) + module C = CongruenceDomain.CongruenceFunctor(CongruenceDomain.NoWrapping) + + type t = I.t * C.t [@@deriving eq, ord, hash] + + let show (i,c) = I.show i ^ "," ^ C.show c + + let ik = IChar (*Placeholder for all functions that need one. Should not matter, but choosen small so that errors are detected with smaller numbers already*) + + let top = I.top_of ik, C.top_of ik + + let is_top = equal top + + let is_bot = function + | None, None -> true + | _,_ -> false + + let of_bigint x = (I.of_int ik (TopIntOps.of_bigint x), C.of_int ik x) + + let leq (i1,c1) (i2,c2) = I.leq i1 i2 && C.leq c1 c2 + + let contains t v = leq (of_bigint v) t + + let contains t v = + let res = contains t v in + if M.tracing then M.tracel "contains" "is %s conained in %s -> %b" (Z.to_string v) (show t) (res); + res + + let refine t = + let refine_step (i,c) = + let c' = match i with + | Some (TopIntOps.Int x, TopIntOps.Int y) -> C.refine_with_interval ik c (Some (x,y)) + | Some _ -> c (*No refinement possible if one side is infinite*) + | _ -> None + in + (I.refine_with_congruence ik i (BatOption.map (fun (x,y) -> (TopIntOps.Int x,TopIntOps.Int y)) c) ), c' + in + let t' = refine_step t in + if t' = t then t else refine_step t' (*The second refinement is necessary if the refinement leads to a constant, otherwise not*) + + let add (i1,c1) (i2,c2) = refine (I.add ~no_ov:true ik i1 i2, C.add ~no_ov:true ik c1 c2) + + let sub (i1,c1) (i2,c2) = refine (I.sub ~no_ov:true ik i1 i2, C.sub ~no_ov:true ik c1 c2) + + let mul (i1,c1) (i2,c2) = refine (I.mul ~no_ov:true ik i1 i2, C.mul ~no_ov:true ik c1 c2) + + let div (i1,c1) (i2,c2) = refine (I.div ~no_ov:true ik i1 i2, C.div ~no_ov:true ik c1 c2) + + let rem (i1,c1) (i2,c2) = refine (I.rem ik i1 i2, C.rem ik c1 c2) + + let neg (i,c) = refine (I.neg ~no_ov:true ik i, C.neg ~no_ov:true ik c) + + let to_int (i,_) = I.to_int i + + let meet (i1,c1) (i2,c2) = refine (I.meet ik i1 i2, C.meet ik c1 c2) + + let narrow (i1,c1) (i2,c2) = refine (I.narrow ik i1 i2, C.narrow ik c1 c2) + + let join (i1,c1) (i2,c2) = refine (I.join ik i1 i2, C.join ik c1 c2) + let widen (i1,c1) (i2,c2) = refine (I.widen ik i1 i2, C.widen ik c1 c2) + + let of_congruence c = refine (I.top_of ik, C.of_congruence ik c) + + let must_be_pos (i,_) = I.leq i (I.starting ik (Int Z.one)) + + let must_be_neg (i,_) = I.leq i (I.ending ik (Int (Z.neg Z.one))) + + let starting x = refine (I.starting ik (Int x), C.top_of ik) + + let ending x = refine (I.ending ik (Int x), C.top_of ik) + + let maximal (i,_) = I.maximal i + let minimal (i,_) = I.minimal i + + let of_IntDomTuple tuple = + let interval = match IntDomain.IntDomTuple.minimal tuple, IntDomain.IntDomTuple.maximal tuple with + | Some min, Some max -> Some ( TopIntOps.Int min, TopIntOps.Int max) + | _ -> None + in refine (interval, IntDomain.IntDomTuple.to_congruence tuple) + + let invariant env var ((i,c):t) acc = + let with_i = + let lower l = + (*x - l >= 0*) + let expr = Linexpr1.make env in + Linexpr1.set_coeff expr (Environment.var_of_dim env var) (GobApron.Coeff.s_of_int 1); + Linexpr1.set_cst expr (GobApron.Coeff.s_of_z @@ Z.neg l); + Lincons1.make expr Lincons0.SUPEQ + in + let higher u = + (*-x + u >= 0*) + let expr = Linexpr1.make env in + Linexpr1.set_coeff expr (Environment.var_of_dim env var) (GobApron.Coeff.s_of_int (-1)); + Linexpr1.set_cst expr (GobApron.Coeff.s_of_z u); + Lincons1.make expr Lincons0.SUPEQ + in + match i with + | Some (TopIntOps.Int l, TopIntOps.Int u) -> lower l :: higher u :: acc + | Some (TopIntOps.Int l, _) -> lower l :: acc + | Some (_, TopIntOps.Int u) -> higher u :: acc + | _ -> acc + in match c with + | Some (o, m) -> + (*x-o % m = 0*) + let expr = Linexpr1.make env in + Linexpr1.set_coeff expr (Environment.var_of_dim env var) (GobApron.Coeff.s_of_int 1); + Linexpr1.set_cst expr (GobApron.Coeff.s_of_z @@ Z.neg o); + Lincons1.make expr (Lincons0.EQMOD (Mpqf (Z_mlgmpidl.mpqf_of_q @@ Q.of_bigint m))) :: with_i + | _ -> Lincons1.make_unsat env :: with_i +end + +module Value = IntervalAndCongruence + +(*The type used for the simulated domain*) +module Relation = struct + type cond = Lt | Gt + type t = cond * Z.t + + let show_cond c = match c with + | Lt -> "<" + | Gt -> ">" + + let show x (c,o) y = x ^ show_cond c ^ y ^ " + " ^ Z.to_string o + + let swap_sides (cond, o) = + let o' = Z.neg o in + match cond with + | Lt -> Gt, o' + | Gt -> Lt, o' + + (*Tries to combine two relations, with the variable on the rhs of the first condition being equal to the one at the lhs of the second*) + let combine (c1, o1) (c2, o2) = match c1, c2 with + | Lt, Lt -> Some ( Lt, Z.add o1 @@ Z.succ o2 ) + | Gt, Gt -> Some ( Gt, Z.add o1 @@ Z.succ o2 ) + | Lt, Gt + | Gt, Lt -> None + + + let value_with_const_right (cond,o) const = + let open Z in + match cond with + | Lt -> Value.ending (o + const - one) + | Gt -> Value.starting (o + const + one) + + let value_with_const_left t const = value_with_const_right (swap_sides t) const + +end + +module Refinement = struct + type t = (int * (Value.t, Rhs.t) Either.t) list + + let show_formatted_single formatter (var, ref) = + let rhs = match ref with + | Either.Left x -> Value.show x + | Right x -> Rhs.show_rhs_formatted formatter x + in + Printf.sprintf "%s = %s" (formatter var) rhs + + let show_formatted formatter t = "[" ^ List.fold (fun acc r -> Printf.sprintf "%s, %s" (show_formatted_single formatter r) acc) "]" t + + let show = show_formatted (fun x -> "var_"^Int.to_string x) + + let of_value var v = (var, Either.Left v) + let of_rhs var r = (var, Either.right r) + + let rhs_only t = List.filter (fun x -> BatEither.is_right (snd x)) t + +end + +module type TwoVarInequalities = sig + type t + + (*returns the best lower and upper bound for the relation between variables with the given Rhs*) + val get_relations : ((Z.t * int * Z.t * Z.t) * Value.t) -> ((Z.t * int * Z.t * Z.t) * Value.t) -> t -> Relation.t list + + (*meet a single relation between two variables.*) + val meet_relation : int -> int -> Relation.t -> (int -> Rhs.t) -> (int -> Value.t) -> t -> t * Refinement.t + + (*substitutes all occurences of a variable by a rhs*) + val substitute : (int -> Value.t) -> t -> int -> Z.t * int * Z.t * Z.t -> t * Refinement.t + + (*called after every operation to limit the inequalities to the most relevant*) + val limit : EConj.t -> t -> t + + val meet : (int -> Value.t) -> t -> t -> t * Refinement.t + val narrow : (int -> Value.t) -> t -> t -> t * Refinement.t + + val leq : t -> (int -> Value.t) -> t -> bool + + val join : t -> (int -> Value.t) -> t -> (int -> Value.t) -> t + val widen : t -> (int -> Value.t) -> t -> (int -> Value.t) -> t + + (*second loop of transform: e.g. a join can split groups of variables. This function copies the relevant inequalities to all new representants*) + val copy_to_new_representants : EConj.t -> EConj.t -> (int -> Value.t) -> t -> t + + (*restore inequalities after an assignment that makes the assigned-to variable have a known relation to before the assignment*) + val transfer : int -> Relation.t -> t -> (int -> Rhs.t) -> (int -> Value.t) -> t -> (int -> Rhs.t) -> (int -> Value.t) -> t * Refinement.t + + val show_formatted : (int -> string) -> t -> string + val hash : t -> int + val empty : t + val is_empty : t -> bool + val equal : t -> t -> bool + val compare : t -> t -> int + val modify_variables_in_domain : t -> int array -> (int -> int -> int) -> t + val forget_variable : t -> int -> t + + val interval_refinements : (int -> Value.t) -> t -> Refinement.t + val set_constant : int -> Z.t -> t -> t * Refinement.t + + val invariant : t -> Environment.t -> Lincons1.t list + +end + +module NoInequalties : TwoVarInequalities = struct + type t = unit + + let get_relations _ _ _ = [] + let meet_relation _ _ _ _ _ _ = (), [] + + let limit _ _ = () + + let meet _ _ _ = () , [] + let narrow _ _ _ = () , [] + + let leq _ _ _ = true + let join _ _ _ _ = () + let widen _ _ _ _ = () + + let show_formatted _ _ = "{}" + let hash _ = 3 + let empty = () + let is_empty _ = true + let equal _ _ = true + let compare _ _ = 0 + let modify_variables_in_domain _ _ _ = () + let forget_variable _ _ = () + + let substitute _ _ _ _ = (), [] + + let copy_to_new_representants _ _ _ _ = () + + let transfer _ _ _ _ _ _ _ _ = (), [] + + let interval_refinements _ _ = [] + + let set_constant _ _ _ = (), [] + + let invariant _ _ = [] + +end + +let qhash q = Z.hash (Q.num q) + 13 * Z.hash (Q.den q) +let round_up q = Z.cdiv (Q.num q) (Q.den q) +let round_down q = Z.fdiv (Q.num q) (Q.den q) + +module LinearInequality = struct + (*Normalised representation of an inequality through the origin + a/b x <= y (or >=) bzw. slope and direction. infinite slope represents 0 <= x / 0 >= x*) + module OriginInequality = struct (*Separate module so we can use it as key in a map*) + type t = LE of Q.t | GE of Q.t (*TODO rename into LE / GE*) + + (*make the representation of inequalities without y unique*) + let norm = function + | GE s when Q.equal s Q.minus_inf -> LE Q.inf + | LE s when Q.equal s Q.minus_inf -> GE Q.inf + | t -> t + + + (*We want the inequalities to be ordered by angle (with arbitrary start point and direction), which is tan(slope) (+ pi for other direction) *) + (*TODO: this is called very often -> performance optimisation?*) + let compare t1 t2 = + let classify t = + let a,b = match t with + | LE s when Q.equal s Q.inf -> (Q.one,Q.zero) + | GE s when Q.equal s Q.inf -> (Q.minus_one, Q.zero) + | LE s -> (s,Q.minus_one) + | GE s -> (Q.neg s, Q.one) + in let open Q in + let c = if a < zero then + Int.(-) 7 (sign b) + else if a = zero then + (if b <= zero then 1 else 5) + else + Int.(+) 3 (sign b) + in a, b, c + in + let a1, b1, class1 = classify t1 in + let a2, b2, class2 = classify t2 in + if class1 <> class2 then + class1 - class2 + else + let open Q in compare (a2*b1) (a1 * b2) (*different from paper , but otherwise wrong?*) + + let equal t1 t2 = 0 = compare t1 t2 + + let hash = function LE q -> qhash q | GE q -> 7 * qhash q + + let get_slope = function LE a -> a | GE a -> a + + let negate = function + | LE s -> GE s + | GE s -> LE s + + end + + (*add an offset to the inequalities*) + type t = OriginInequality.t * Q.t [@@deriving eq] + + let show x y (k,c) = + let show_var coeff var show_zero = + let open Z in + if coeff = zero then (if show_zero then "0 " else "") + else if coeff = one then var ^ " " + else to_string coeff ^ var ^ " " + in + let show_offset o = + let open Q in + if o = zero then "" + else if o > zero then "+ " ^ to_string o + else "- " ^ to_string (abs o) + in + let s = OriginInequality.get_slope k in + Printf.sprintf "%s%s %s%s" + (show_var (Q.num s) x true) + (match k with LE _ -> "<=" | GE _ -> ">=") + (show_var (Q.den s) y (Q.equal c Q.zero)) + (show_offset @@ if Q.equal s Q.inf then c else Q.mul c @@ Q.of_bigint @@ Q.den s ) + + (*Convert into coefficients of inequality ax + by <= c + Useful because the TVLI paper (DOI: 10.1007/3-540-45013-0_7) uses this representation *) + let to_coeffs = function + | OriginInequality.LE s, c when Q.equal s Q.inf -> (Q.one,Q.zero,c) + | GE s, c when Q.equal s Q.inf -> (Q.minus_one, Q.zero, Q.neg c) + | LE s, c -> (s,Q.minus_one,c) + | GE s, c -> (Q.neg s, Q.one, Q.neg c) + + let to_coeffs t = + let a,b,c as res = to_coeffs t in + if M.tracing then M.trace "entails" "slope %s, whole: %s -> %s,%s,%s" (Q.to_string @@ OriginInequality.get_slope @@ fst t) (show "x" "y" t) (Q.to_string a) (Q.to_string b) (Q.to_string c); + res + + (*From TVLI: check if one or two inequalities imply an inequality*) + let entails1 (s1,c1) (s2,c2) = OriginInequality.equal s1 s2 && match s1 with LE _ -> Q.leq c1 c2 | GE _ -> Q.geq c1 c2 + + let entails1 t1 t2 = + let res = entails1 t1 t2 in + if M.tracing then M.trace "entails" "%s |= %s ? %b" (show "x" "y" t1) (show "x" "y" t2) res; + res + + let entails2 t1 t2 t = + let (a1,b1,c1) = to_coeffs t1 in + let (a2,b2,c2) = to_coeffs t2 in + let (a ,b ,c ) = to_coeffs t in + if M.tracing then M.trace "entails" "coeffs: %s,%s,%s %s,%s,%s %s,%s,%s" (Q.to_string a1) (Q.to_string b1) (Q.to_string c1) (Q.to_string a2) (Q.to_string b2) (Q.to_string c2) (Q.to_string a) (Q.to_string b) (Q.to_string c); + let open Q in + let d = a1 * b2 - a2 * b1 in + if equal d zero then + entails1 t1 t || entails1 t2 t + else + let l1 = (a * b2 - a2 * b) / d in + let l2 = (a1 * b - a * b1) / d in + geq l1 zero && geq l2 zero && geq c @@ l1 * c1 + l2 * c2 + + let entails2 t1 t2 t = + let res = entails2 t1 t2 t in + if M.tracing then M.trace "entails" "%s , %s |= %s ? %b" (show "x" "y" t1) (show "x" "y" t2) (show "x" "y" t) res; + res + + (*Calculate the best inequality with a fixed slope implied by two inequalities. Assumes the searched slope to be different to the known ones*) + let best_entailed t1 t2 k = + let (a1,b1,c1) = to_coeffs t1 in + let (a2,b2,c2) = to_coeffs t2 in + let (a ,b ,_ ) = to_coeffs (k,Q.zero) in + let open Q in + let d = a1 * b2 - a2 * b1 in + if equal d zero then + None + else + let l1 = (a * b2 - a2 * b) / d in + let l2 = (a1 * b - a * b1) / d in + if not (geq l1 zero && geq l2 zero) + then None + else + let c = l1 * c1 + l2 * c2 in + let c' = match k with LE _ -> c | GE _ -> neg c in + Some c' + + (*convert interval information into inequalities*) + let from_values x_val y_val = + let open OriginInequality in + let ineqs = match Value.maximal x_val with + | Some (Int z) -> (*x <= z *) [LE Q.inf, Q.of_bigint z] + | _ -> [] + in let ineqs = match Value.minimal x_val with + | Some (Int z) -> (*x >= z *) (GE Q.inf, Q.of_bigint z) :: ineqs + | _ -> ineqs + in let ineqs = match Value.maximal y_val with + | Some (Int z) -> (*y <= z *) (GE Q.zero, Q.neg @@ Q.of_bigint z ) :: ineqs + | _ -> ineqs + in let ineqs = match Value.minimal y_val with + | Some (Int z) -> (*y >= z *) (LE Q.zero, Q.neg @@ Q.of_bigint z ) :: ineqs + | _ -> ineqs + in ineqs + + (*Convert two righthandsides into an inequality isLessThan is the direction of the inequality and needed for making the inequality non-strict while we still know that all variables are integers*) + let from_rhss (cx, ox, dx) (cy, oy, dy) isLessThan_opt = + let non_strict_offset = match isLessThan_opt with None -> Q.zero | Some isLessThan -> if isLessThan then Q.minus_one else Q.one in + let a,b,c = (Q.make cx dx, Q.make cy dy, Q.add non_strict_offset @@ Q.sub (Q.make oy dy) (Q.make ox dx)) in (*subtracting one to convert it into a nonstrict inequality*) + let s = Q.div a b in + if Q.equal b Q.zero + then OriginInequality.norm (LE s), Q.div c a + else if Q.gt b Q.zero + then LE s, Q.div c b + else GE s, Q.div c b + + + (*apply the transformation to the variable on the left side*) + let substitute_left (coeff, offs, divi) (k,o) = + let open OriginInequality in + let s = get_slope k in + let s' = Q.mul s (Q.make coeff divi) in + let o' = Q.sub o @@ Q.mul s @@ Q.make offs divi in + match k with + | LE _ -> LE s', o' + | GE _ -> GE s', o' + + (*apply the transformation to the variable on the right side*) + let substitute_right (coeff, offs, divi) (k,o) = + let open OriginInequality in + let s = get_slope k in + let f = Q.make coeff divi in + let s' = Q.div s f in + let o' = Q.add (Q.div o f) @@ Q.make offs coeff in + let k' = match k with + | LE _ -> LE s' + | GE _ -> GE s' + in if Q.lt f Q.zero + then (negate k', o') + else k', o' + + let swap_sides (k,o) = + let open Q in + let open OriginInequality in + match k with + | LE s when s < zero -> (LE (inv s), - (o / s)) + | LE s -> (GE (inv s), - (o / s)) + | GE s when s < zero -> (GE (inv s), - (o / s)) + | GE s -> (LE (inv s), - (o / s)) + + (*combine an inequaliy x_old -> x_new with x_old -> y to x_new -> y*) + let combine_left (k_rel, o_rel) (k, o) = + let open OriginInequality in + (*factor we need to multiply rel with so that x_old has the same coefficient in both inequalities *) + let f = Q.div (get_slope k) (get_slope k_rel) in + let k_rel' = if Q.geq f Q.zero then k_rel else negate k_rel in + match k_rel', k with + | LE _, LE _ + | GE _, GE _ -> None (*no useable inequality x_new -> y*) + | GE _, LE _ -> Some (LE f, Q.sub o (Q.mul f o_rel)) + | LE _, GE _ -> Some (GE f, Q.sub o (Q.mul f o_rel)) + + let combine_left rel t = + let res = combine_left rel t in + if M.tracing then M.trace "combine" "combine_left %s with %s -> %s" (show "x_old" "x_new" rel) (show "x_old" "y" t) (BatOption.map_default (fun res -> show "x_new" "y" res) "Nothing" res); + res + + (*combine an inequaliy y_old -> y_new with x -> y_old to x-> y_new*) + let combine_right (k_rel, o_rel) (k, o) = + let open OriginInequality in + (*factor we need to multiply the inequality x -> y_old with so that y_old has the same coefficient in both inequalities *) + let f = get_slope k_rel in + let k' = if Q.geq f Q.zero then k else negate k in + match k_rel, k' with + | LE _, GE _ + | GE _, LE _ -> None + | LE s_rel, LE s -> Some (LE (Q.mul s f), Q.add o_rel @@ Q.mul f o) + | GE s_rel, GE s -> Some (GE (Q.mul s f), Q.add o_rel @@ Q.mul f o) + + let combine_right rel t = + let res = combine_right rel t in + if M.tracing then M.trace "combine" "combine_right %s with %s -> %s" (show "y_old" "y_new" rel) (show "x" "y_old" t) (BatOption.map_default (fun res -> show "x" "y_new" res) "Nothing" res); + res + + let set_constant_lhs rhs_var const (k,o) ref_acc = + let open Q in + let s = OriginInequality.get_slope k in + let bound = s * of_bigint const - o in + let new_ref = match k with + | LE _ -> Refinement.of_value rhs_var @@ Value.starting @@ round_up bound + | GE _ -> Refinement.of_value rhs_var @@ Value.ending @@ round_down bound + in new_ref :: ref_acc + + let set_constant_rhs lhs_var const (k,o) ref_acc = + let open Q in + let s = OriginInequality.get_slope k in + let bound = (of_bigint const + o) / s in + let is_leq = match k with + | LE _ -> s > zero + | GE _ -> s < zero + in let new_ref = + if is_leq then + Refinement.of_value lhs_var @@ Value.ending @@ round_down bound + else + Refinement.of_value lhs_var @@ Value.starting @@ round_up bound + + in new_ref :: ref_acc + + let invariant env x y k o acc = + (*for LE, we need to swap signs of all coefficients*) + let s, o = match k with + | OriginInequality.LE s -> Q.neg s, Q.neg o + | GE s -> s, o + in + let o' = if Q.equal s Q.inf then Q.neg o else Q.neg @@ Q.mul o @@ Q.of_bigint @@ Q.den s in + let coeffs = [ + GobApron.Coeff.s_of_z (Q.num s), Environment.var_of_dim env x; + GobApron.Coeff.s_of_z @@ Z.neg @@ Q.den s, Environment.var_of_dim env y + ] in + let expr = Linexpr1.make env in + Linexpr1.set_list expr coeffs (Some (GobApron.Coeff.s_of_mpq @@ Z_mlgmpidl.mpq_of_q o')); + Lincons1.make expr Lincons0.SUPEQ :: acc + +end + +(*very small wrapper to make the following code clearer to me*) +module MultiSet = struct + module M = BatHashtbl + + type 'a t = ('a, int) M.t + + let create ?(initial_size = 5) () = M.create initial_size + + let change_member_count (ms : 'a t) (x : 'a) (count : int) = M.modify_def 0 x ((+) count) ms + + let iter = M.iter + +end + +let coeffs_from_econj (dim, map) = + let m = BatHashtbl.create @@ IntMap.cardinal map in (*This is an overestimation*) + let add_rhs _ = function + | (Some (cy,y),oy,dy) -> + let s = Q.make cy dy in + begin + match BatHashtbl.find_option m y with + | None -> + let set = MultiSet.create () in + MultiSet.change_member_count set s 1; + BatHashtbl.add m y set; + | Some set -> MultiSet.change_member_count set s 1; + end + | _ -> () (*ignore constants*) + in + IntMap.iter add_rhs map; + m + +let coeffs_from_econj = Timing.wrap "coeffs" coeffs_from_econj + +(*assumes x < y*) +let slopes_from_coeffs mapping (x,y) = + let x_coeffs = BatHashtbl.find_default mapping x (MultiSet.create ~initial_size:1 ()) in + let y_coeffs = BatHashtbl.find_default mapping y (MultiSet.create ~initial_size:1 ()) in + (*We do not explicetly store the representants coefficient -> add it here*) + MultiSet.change_member_count x_coeffs Q.one 1; + MultiSet.change_member_count y_coeffs Q.one 1; + let slopes = MultiSet.create ~initial_size:(BatHashtbl.length x_coeffs * BatHashtbl.length y_coeffs) () in + MultiSet.iter (fun cx cx_count -> MultiSet.iter (fun cy cy_count -> let s = Q.div cx cy in MultiSet.change_member_count slopes s (cx_count * cy_count)) y_coeffs) x_coeffs; + slopes + +let slopes_from_coeffs = Timing.wrap "slopes" slopes_from_coeffs + +(*List of inequalities ax < by + c, mapping a and b to c*) +(*We need to make sure that x has lower index than y to keep this representation unique! *) +module TwoVarInequalitySet = struct + module Key = LinearInequality.OriginInequality + module CoeffMap = Map.Make(Key) + + type t = Q.t CoeffMap.t [@@deriving eq, ord] + + let hash t = CoeffMap.fold (fun k c acc -> qhash c + 17 * Key.hash k ) t 0 + + let show_formatted x y t = + CoeffMap.fold (fun k c acc -> Printf.sprintf "%s , %s" (LinearInequality.show x y (k,c)) acc) t "" + + let empty = CoeffMap.empty + + + let ignore_empty ls = + if CoeffMap.is_empty ls then None + else Some ls + + (*limit how many inequalities we are saving: only keep inequalities with slopes that correspond to variables. + optionally, limit it further to the slopes that correspond to the most inequalities *) + let limit slopes t = + let opt = GobConfig.get_string "ana.lin2vareq_p.inequalities" in + if opt = "unlimited" then ignore_empty t else + let open LinearInequality.OriginInequality in + let filtered = CoeffMap.filter (fun k c -> BatHashtbl.mem slopes (get_slope k) ) t in + let keep = + if opt = "coeffs_count" then + GobConfig.get_int "ana.lin2vareq_p.coeffs_count" (*TODO for a fixed number, we do not need to sort but could instead use an O(n algorithm!)*) + else + let f = GobConfig.get_int "ana.lin2vareq_p.coeffs_threshold" in + let total = BatHashtbl.fold (fun _ c acc -> c + acc) slopes 0 in + max 4 @@ (total * f) / 100 (*allow a minimum of 4 inequality angles *) + in + let comp (k1,_) (k2,_) = + let v1 = BatHashtbl.find_default slopes (get_slope k1) 0 in + let v2 = BatHashtbl.find_default slopes (get_slope k2) 0 in + v2 - v1 (*list sorts ascending, we need descending -> inverted comparison*) + in + (*skip sorting if we keep all inequalities*) + if keep >= CoeffMap.cardinal filtered then + ignore_empty filtered + else + ignore_empty @@ CoeffMap.of_list @@ List.take keep @@ List.sort comp @@ CoeffMap.bindings filtered + + (*get the next key in anti-clockwise order*) + let get_previous k t = + match CoeffMap.find_first_opt (fun key -> Key.compare key k > 0) t with + | None -> CoeffMap.min_binding_opt t (*there is no larger key -> take the first one*) + | s -> s + + (*get the next key in clockwise order*) + let get_next k t = + match CoeffMap.find_last_opt (fun key -> Key.compare key k < 0) t with + | None -> CoeffMap.max_binding_opt t (*there is no smaller key -> take the last one*) + | s -> s + + (*adds the inequality while removing redundant ones. assumes that there is no inequality with this key already in the map*) + let add_inequality k c t = + match get_previous k t, get_next k t with + | None, None -> CoeffMap.add k c t (* the map is empty *) + | Some prev, Some next -> + if LinearInequality.entails2 prev next (k,c) then ( + if M.tracing then M.trace "add_ineq" "new %s entailed by prev: %s, next %s" (LinearInequality.show "x" "y" (k,c)) (LinearInequality.show "x" "y" prev) (LinearInequality.show "x" "y" next); + t) (*new inequality is already implied*) + else (*check in both direction if the next inequality is now implied, and remove those that are. recursive because multiple may now be implied*) + let rec remove_prev prev t = + match get_previous (fst prev) t with + | None -> + if M.tracing then M.trace "add_ineq" "remove_prev?: none left to remove"; + t + | Some prev_prev -> + if LinearInequality.equal prev prev_prev then begin + if M.tracing then M.trace "add_ineq" "remove_prev?: only one left in %s -> no removal" (show_formatted "x" "y" t); + t + end else if LinearInequality.entails2 prev_prev (k,c) prev then begin + if M.tracing then M.trace "add_ineq" "remove_prev?: new: %s and prev_prev: %s imply prev %s -> removing and continuing" (LinearInequality.show "x" "y" (k,c)) (LinearInequality.show "x" "y" prev_prev) (LinearInequality.show "x" "y" prev); + remove_prev prev_prev @@ CoeffMap.remove (fst prev) t + end else begin + if M.tracing then M.trace "add_ineq" "remove_prev?: new: %s and prev_prev: %s do not imply prev %s -> stop" (LinearInequality.show "x" "y" (k,c)) (LinearInequality.show "x" "y" prev_prev) (LinearInequality.show "x" "y" prev); + t + end + in let rec remove_next next t = + match get_next (fst next) t with + | None -> + if M.tracing then M.trace "add_ineq" "remove_next?: none left to remove"; + t + | Some next_next -> + if LinearInequality.equal next next_next then begin + if M.tracing then M.trace "add_ineq" "remove_next?: only one left in %s -> no removal" (show_formatted "x" "y" t); + t + end else if LinearInequality.entails2 next_next (k,c) next then begin + if M.tracing then M.trace "add_ineq" "remove_next?: new: %s and next_next: %s imply next %s -> removing and continuing" (LinearInequality.show "x" "y" (k,c)) (LinearInequality.show "x" "y" next_next) (LinearInequality.show "x" "y" next); + remove_next next_next @@ CoeffMap.remove (fst next) t + end else begin + if M.tracing then M.trace "add_ineq" "remove_next?: new: %s and next_next: %s do not imply next %s -> stop" (LinearInequality.show "x" "y" (k,c)) (LinearInequality.show "x" "y" next_next) (LinearInequality.show "x" "y" next); + t + end + in CoeffMap.add k c @@ remove_prev prev @@ remove_next next t + | _,_ -> failwith "impossible state" + + let add_inequality k c t = + let res = add_inequality k c t in + if M.tracing then M.trace "add_ineq" "adding %s to %s -> %s" (LinearInequality.show "x" "y" (k,c)) (show_formatted "x" "y" t) (show_formatted "x" "y" res); + res + + (*get the thightest offset for an inequality with a given slope that is implied by the current set of inequalities*) + let get_best_offset k t = + match CoeffMap.find_opt k t with + | Some c -> Some c + | None -> + if CoeffMap.cardinal t < 2 then None + else LinearInequality.best_entailed (BatOption.get @@ get_next k t) (BatOption.get @@ get_previous k t) k + + let get_best_offset k t = + let res = get_best_offset k t in + if M.tracing then M.trace "get_offset" "%s implies %s" (show_formatted "x" "y" t) (BatOption.map_default (fun c -> LinearInequality.show "x" "y" (k,c)) "Nothing for this slope" res); + res + + (*lookup the best interval bounds from the inequalities!*) + let interval_refinements (x,x_val) (y,y_val) t ref_acc = + let ineqs = LinearInequality.from_values x_val y_val in + let t = List.fold (fun t (k,c) -> add_inequality k c t) t ineqs in + let ref_acc = match get_best_offset (LE Q.inf) t with + | Some upper -> (Refinement.of_value x @@ Value.ending @@ round_down upper ):: ref_acc + | _ -> ref_acc + in + let ref_acc = match get_best_offset (GE Q.inf) t with + | Some lower -> (Refinement.of_value x @@ Value.starting @@ round_up lower ):: ref_acc + | _ -> ref_acc + in + let ref_acc = match get_best_offset (GE Q.zero) t with + | Some upper -> (Refinement.of_value y @@ Value.ending @@ round_down @@ Q.neg upper ):: ref_acc + | _ -> ref_acc + in + match get_best_offset (LE Q.zero) t with + | Some lower -> (Refinement.of_value y @@ Value.starting @@ round_up @@ Q.neg lower ):: ref_acc + | _ -> ref_acc + + let meet_single_inequality (x,x_val) (y,y_val) k c (t,ref_acc) = + (*calculate value refinement. If one of the coefficients is zero, we should not add the inequality to the map*) + let refinements, skip_adding = + let x_refine = + let upper_bound s = (*x <= y / s + c / s*) + let max_y = match Value.maximal (Value.mul y_val (Value.of_bigint (round_down (Q.inv s)))) , Value.maximal @@ Value.mul y_val (Value.of_bigint (round_up (Q.inv s))) with + | Some a, Some b -> TopIntOps.max a b + | _,_ -> failwith "trying to refine bot in inequalities" + in match max_y with + | Int max -> [Refinement.of_value x (Value.ending @@ Z.add max @@ round_down @@ Q.div c s)] + | _ -> [] + in let lower_bound s = (*x >= y / s + c / s*) + let min_y = match Value.minimal (Value.mul y_val (Value.of_bigint (round_down (Q.inv s)))) , Value.minimal @@ Value.mul y_val (Value.of_bigint (round_up (Q.inv s))) with + | Some a, Some b -> TopIntOps.min a b + | _,_ -> failwith "trying to refine bot in inequalities" + in match min_y with + | Int min -> [Refinement.of_value x (Value.starting @@ Z.add min @@ round_up @@ Q.div c s)] + | _ -> [] + in + match k with + | LinearInequality.OriginInequality.LE s when Q.sign s > 0 -> upper_bound s + | GE s when Q.sign s < 0 -> upper_bound s + | LE s when Q.sign s < 0 -> lower_bound s + | GE s when Q.sign s > 0 -> lower_bound s + | _ -> [] (*Should never be used in this case*) + in let y_refine = + match k with + | LE s -> begin (*sx -c <= y*) + let min_x = match Value.minimal (Value.mul x_val (Value.of_bigint (round_down s))) , Value.minimal @@ Value.mul x_val (Value.of_bigint (round_up s)) with + | Some a, Some b -> TopIntOps.min a b + | _,_ -> failwith "trying to refine bot in inequalities" + in match min_x with + | Int min -> [Refinement.of_value y (Value.starting @@ Z.sub min @@ round_up c)] + | _ -> [] + end + | GE s -> (*s x - c >= y*) + let max_x = match Value.maximal (Value.mul x_val (Value.of_bigint (round_down s))) , Value.maximal @@ Value.mul x_val (Value.of_bigint (round_up s)) with + | Some a, Some b -> TopIntOps.max a b + | _,_ -> failwith "trying to refine bot in inequalities" + in match max_x with + | Int max -> [Refinement.of_value y (Value.ending @@ Z.sub max @@ round_down c)] + | _ -> [] + in match k with + | LinearInequality.OriginInequality.LE s when Q.equal Q.zero s -> (* -c >= y *) [Refinement.of_value y @@ Value.ending @@ round_down @@ Q.neg c] , true + | GE s when Q.equal Q.zero s -> (* -c <= y *) [Refinement.of_value y @@ Value.starting @@ round_up @@ Q.neg c] , true + | LE s when Q.equal Q.inf s -> (*x >= c*) [Refinement.of_value x @@ Value.starting @@ round_up c ], true + | GE s when Q.equal Q.minus_inf s -> (*x >= c*) [Refinement.of_value x @@ Value.starting @@ round_up c ], true + | LE s when Q.equal Q.minus_inf s -> (*x <= c*) [Refinement.of_value x @@ Value.ending @@ round_down c], true + | GE s when Q.equal Q.inf s -> (*x <= c*) [Refinement.of_value x @@ Value.ending @@ round_down c], true + | k -> (*an actual inequality *) x_refine @ y_refine, false + in + let ref_acc = refinements @ ref_acc in + if skip_adding then t, ref_acc + else (*Look for contradicting inequality*) + let contradicts c' = match k with + | LE _ -> Q.gt c' c + | GE _ -> Q.lt c' c + in + match get_best_offset (Key.negate k) t with + | Some c' when contradicts c' -> + if M.tracing then M.trace "meet" "single_ineq new: %s contradicts existing information %s" (LinearInequality.show "x" "y" (k,c)) (show_formatted "x" "y" t); + raise EConj.Contradiction + (*we have an equality -> update the econj domain sn / sd x = y + cn/cd -> x = (sd y cd + sd cn) / sn cd *) + | Some c' when c = c' -> begin + let s = Key.get_slope k in + let sn, sd = Q.num s, Q.den s in + let cn, cd = Q.num c, Q.den c in + let open Z in + if M.tracing then begin + let show_var = (fun x -> "var_"^Int.to_string x) in + M.trace "refinements" "single_ineq new: %s with %s results in equality" + (LinearInequality.show (show_var x) (show_var y) (k,c)) + (show_formatted (show_var x) (show_var y) t) + end; + t, (Refinement.of_rhs x @@ Rhs.canonicalize (Some (sd * cd, y), sd*cn, sn * cd)) :: ref_acc + end + | _ -> + (*add the inequality, while making sure that we do not save redundant inequalities*) + let t' = match CoeffMap.find_opt k t with + | Some c_old when LinearInequality.entails1 (k,c_old) (k,c) -> t (*saved inequality is already thighter than new one*) + | _ -> add_inequality k c @@ CoeffMap.remove k t (*we replace the current value with a new one *) + in + let ref_acc = interval_refinements (x,x_val) (y,y_val) t' ref_acc in + t', ref_acc + + let meet x_val y_val t1 t2 ref_acc = CoeffMap.fold (meet_single_inequality x_val y_val) t1 (t2,ref_acc) + + let narrow x_val y_val t1 t2 ref_acc = + let narrow_single_inequality k c ((t,_) as acc) = + if CoeffMap.mem k t then + acc (*accelerated narowing: only restrict top bounds to only have finite number of narrowings*) + else + fst @@ meet_single_inequality x_val y_val k c acc, [] + in + CoeffMap.fold narrow_single_inequality t2 (t1,ref_acc) + + let narrow x_val y_val t1 t2 ref_acc = + let res = narrow x_val y_val t1 t2 ref_acc in + if M.tracing then M.trace "narrow" "narrow for coeffs a: %s b: %s -> %s" (show_formatted "x" "y" t1) (show_formatted "x" "y" t2) (show_formatted "x" "y" @@ fst res); + res + + + let implies x_val y_val t1_opt t2 = + let t1 = match t1_opt with + | None -> CoeffMap.empty + | Some t -> t + in let interval_ineqs = LinearInequality.from_values x_val y_val in + let t1 = List.fold (fun t (k,c) -> add_inequality k c t) t1 interval_ineqs (*makes this O(n log n) instead of O(n)*) + in if M.tracing then M.trace "implies" "after adding intervals: %s" (show_formatted "x" "y" t1); + if CoeffMap.is_empty t2 then true + else if CoeffMap.is_empty t1 then false + else(*functional version of the entailment check from TVLI*) + let ts1 = CoeffMap.bindings t1 in + let ts2 = CoeffMap.bindings t2 in + let min_t1 = List.hd ts1 in + let max_t1 = CoeffMap.max_binding t1 in + let rec entails t1 t2 = match t1, t2 with + | _, [] -> true + | [], _ -> false (*should never happen, but makes this matching complete*) + | (tl::tu::t1s), ti::t2s when Key.compare (fst tu) (fst ti) < 0 -> entails (tu::t1s) (ti::t2s) + | ((tl::tu::_) as t1s), ti::t2s -> LinearInequality.entails2 tl tu ti && entails t1s t2s + | [tl], ti::t2s -> LinearInequality.entails2 tl min_t1 ti && entails [tl] t2s + in entails (max_t1::ts1) ts2 + + let implies x_val y_val t1_opt t2 = + let res = implies x_val y_val t1_opt t2 in + if M.tracing then M.trace "implies" "x = %s, y = %s, %s implies %s ? -> %b" (Value.show x_val) (Value.show y_val) (BatOption.map_default (show_formatted "x" "y") "{}" t1_opt) (show_formatted "x" "y" t2) res; + res + + let join x y get_val_t1 get_val_t2 t1 t2 = + let t1 = match t1 with None -> CoeffMap.empty | Some t1 -> t1 in + let t2 = match t2 with None -> CoeffMap.empty | Some t2 -> t2 in + (*add interval inequalities to copies*) + let t1_with_interval = + (*Do not do this work if we never need it*) + if CoeffMap.is_empty t2 then + CoeffMap.empty + else + let ineqs = LinearInequality.from_values (get_val_t1 x) (get_val_t1 y) in + List.fold (fun t (k,c) -> add_inequality k c t) t1 ineqs + in let t2_with_interval = + if CoeffMap.is_empty t1 then + CoeffMap.empty + else + let ineqs = LinearInequality.from_values (get_val_t2 x) (get_val_t2 y) in + List.fold (fun t (k,c) -> add_inequality k c t) t2 ineqs + in + (*Keep slopes where the other element implies some inequality for the same slope *) + let relax t k c = + let res = match get_best_offset k t with + | None -> None (*drop if nothing is implied *) + | Some c' -> (* in this case, we need to take the more relaxed bound*) + if LinearInequality.entails1 (k, c') (k,c) then + Some c + else + Some c' + in + if M.tracing then M.trace "relax" "%s with %s relaxed to %s" (show_formatted "x" "y" t) (LinearInequality.show "x" "y" (k,c)) (BatOption.map_default (fun c -> LinearInequality.show "x" "y" (k,c)) "Nothing" res); + res + in + let t1_mapped = CoeffMap.filter_map (relax t2_with_interval) t1 in + let t2_mapped = CoeffMap.filter_map (relax t1_with_interval) t2 in + (* merge the two sets *) + (*the existing add assumes there to be no inequality with this key. this happens only if both have the same offset now *) + let add_inequality k c t = if CoeffMap.mem k t then t else add_inequality k c t in + let merged = CoeffMap.fold add_inequality t2_mapped t1_mapped + in ignore_empty merged + + let widen _ _ _ _ t1 t2 = + let open GobOption.Syntax in + (*only keep inequalities that the same are in both equations*) + let keep_same k c1 c2 = if c1 = c2 then c1 else None in + let* t1 = t1 in + let* t2 = t2 in + ignore_empty @@ CoeffMap.merge (keep_same) t1 t2 + + let substitute_left (coeff, offs, divi) t = + let f k c t_acc = + let (k',c') = LinearInequality.substitute_left (coeff, offs, divi) (k,c) in + CoeffMap.add k' c' t_acc (*affine transformation does not make a non redundant inequality redundant -> add directly*) + in + CoeffMap.fold f t CoeffMap.empty + + let substitute_right (coeff, offs, divi) t = + let f k c t_acc = + let (k',c') = LinearInequality.substitute_right (coeff, offs, divi) (k,c) in + CoeffMap.add k' c' t_acc + in + CoeffMap.fold f t CoeffMap.empty + + (*combine two inequalities into a single one if possible*) + let combine_left rel t = + let fold_fun k c acc = + match LinearInequality.combine_left rel (k,c) with + | Some (k', c') -> CoeffMap.add k' c' acc + | None -> acc + in + let t' = CoeffMap.fold fold_fun t CoeffMap.empty in + if CoeffMap.is_empty t' then None else Some t' + + let combine_right rel t = + let fold_fun k c acc = + match LinearInequality.combine_right rel (k,c) with + | Some (k', c') -> CoeffMap.add k' c' acc + | None -> acc + in + let t' = CoeffMap.fold fold_fun t CoeffMap.empty in + if CoeffMap.is_empty t' then None else Some t' + + let swap_sides t = + let fold_fun k c acc = + let (k', c') = LinearInequality.swap_sides (k,c) in + CoeffMap.add k' c' acc + in + CoeffMap.fold fold_fun t CoeffMap.empty + + let set_constant_lhs rhs_var const t ref_acc = CoeffMap.fold (fun k c ref_acc -> LinearInequality.set_constant_lhs rhs_var const (k,c) ref_acc) t ref_acc + let set_constant_rhs lhs_var const t ref_acc = CoeffMap.fold (fun k c ref_acc -> LinearInequality.set_constant_rhs lhs_var const (k,c) ref_acc) t ref_acc + + + let invariant env x y t acc = CoeffMap.fold (LinearInequality.invariant env x y) t acc + + let to_set t = t + + let of_set _ _ t = ignore_empty t + +end + +module TVIS = TwoVarInequalitySet + +module type Coeffs = sig + type t + + val join : int -> int -> (int -> Value.t) -> (int -> Value.t) -> t option -> t option -> t option + val widen : int -> int -> (int -> Value.t) -> (int -> Value.t) -> t option -> t option -> t option + + val limit : (Q.t, int) Hashtbl.t -> t -> t option + + val hash : t -> int + val equal : t -> t -> bool + val compare : t -> t -> int + val show_formatted : string -> string -> t -> string + + val to_set : t -> TwoVarInequalitySet.t + + val of_set : Value.t -> Value.t -> TwoVarInequalitySet.t -> t option + +end + + +module InequalityFunctor (Coeffs : Coeffs): TwoVarInequalities = struct + + type t = Coeffs.t IntMap.t IntMap.t [@@deriving eq, ord ] + + let empty = IntMap.empty + let is_empty = IntMap.is_empty + let hash t = IntMap.fold (fun _ ys acc -> IntMap.fold (fun _ coeff acc -> Coeffs.hash coeff + 3*acc) ys (5*acc)) t 0 + + let ignore_empty ls = + if IntMap.is_empty ls then None + else Some ls + + let show_map formatter elem_formatter t = + if IntMap.is_empty t then "{}" else + let str = IntMap.fold (fun x ys acc -> IntMap.fold (fun y coeff acc -> Printf.sprintf "%s , %s" (elem_formatter (formatter x) (formatter y) coeff) acc) ys acc) t "" + in "{" ^ String.sub str 0 (String.length str - 3) ^ "}" + + let show_formatted formatter t = show_map formatter Coeffs.show_formatted t + + let show = show_formatted (Printf.sprintf "var_%d") + + let forget_variable t v = + IntMap.filter_map (fun _ ys -> let ys' = IntMap.remove v ys in if IntMap.is_empty ys' then None else Some ys') (IntMap.remove v t) + + let modify_variables_in_domain map indexes op = + let map_fun bump_var ys = IntMap.fold (fun y -> IntMap.add (bump_var y) ) ys IntMap.empty in + EConj.modify_variables_in_domain_general map map_fun indexes op + + let get_coeff x y t = BatOption.bind (IntMap.find_opt x t) (fun ys -> IntMap.find_opt y ys) + + let set_coeff x y coeff t = + IntMap.add x (IntMap.add y coeff @@ IntMap.find_default IntMap.empty x t ) t + + let remove_coeff x y t = + let new_map = IntMap.remove y @@ IntMap.find_default IntMap.empty x t in + if IntMap.is_empty new_map then t + else IntMap.add x new_map t + + let leq t1 get_value_t1 t2 = + let implies x y t2_coeff = + let t1_coeff = get_coeff x y t1 in + TVIS.implies (get_value_t1 x) (get_value_t1 y) (BatOption.map Coeffs.to_set t1_coeff) (Coeffs.to_set t2_coeff) + in + IntMap.for_all (fun x ys -> IntMap.for_all (implies x) ys) t2 + + let meet_one_coeff narrow get_value x y coeff (t,ref_acc) = + let coeff_t = get_coeff x y t in + let coeff_met, ref_acc' = match coeff_t with + | None -> coeff, ref_acc (*also fine for narrow if t is the one on the righthandside*) + | Some coeff_t -> (if narrow then TVIS.narrow else TVIS.meet) (x, get_value x) (y, get_value y) (Coeffs.to_set coeff_t) coeff ref_acc + in match (Coeffs.of_set (get_value x) (get_value y)) coeff_met with + | None -> remove_coeff x y t, ref_acc' + | Some coeff_met -> set_coeff x y coeff_met t, ref_acc' + + let meet get_value t1 t2 = + IntMap.fold (fun x ys acc -> IntMap.fold (fun y coeff acc -> meet_one_coeff false get_value x y (Coeffs.to_set coeff) acc) ys acc) t1 (t2,[]) + + let narrow get_value t1 t2 = + IntMap.fold (fun x ys acc -> IntMap.fold (fun y coeff acc -> meet_one_coeff true get_value x y (Coeffs.to_set coeff) acc) ys acc) t1 (t2,[]) + + let join t1 get_val_t1 t2 get_val_t2 = + let merge_y x y = Coeffs.join x y get_val_t1 get_val_t2 in + let merge_x x ys1 ys2 = + match ys1, ys2 with + | Some ys1, None -> ignore_empty (IntMap.filter_map (fun y coeff1 -> merge_y x y (Some coeff1) None) ys1) + | None, Some ys2 -> ignore_empty (IntMap.filter_map (fun y coeff2 -> merge_y x y None (Some coeff2)) ys2) + | Some ys1, Some ys2 -> ignore_empty (IntMap.merge (merge_y x) ys1 ys2) + | _, _ -> None + in IntMap.merge (merge_x) t1 t2 + + let join t1 get_val_t1 t2 get_val_t2 = + let res = Timing.wrap "join_ineq" (join t1 get_val_t1 t2 ) get_val_t2 in + if M.tracing then M.trace "join'" "a: %s b: %s -> %s" (show t1) (show t2) (show res); + res + + let widen t1 get_val_t1 t2 get_val_t2 = + let merge_x x ys1 ys2 = + match ys1, ys2 with + | _, None + | None, _ -> None + | Some ys1, Some ys2 -> ignore_empty (IntMap.merge (fun y cs1 cs2 -> Coeffs.widen x y get_val_t1 get_val_t2 cs1 cs2) ys1 ys2) + in IntMap.merge (merge_x) t1 t2 + + let widen a b c d = + let res = widen a b c d in + if M.tracing then M.trace "widen" "called for inequalities"; + res + + let interval_refinements get_value t = IntMap.fold (fun x ys acc -> + IntMap.fold (fun y cs acc -> + TVIS.interval_refinements + (x, get_value x) + (y, get_value y) + (Coeffs.to_set cs) + acc + ) ys acc + ) t [] + + let set_constant var const t = IntMap.fold (fun x ys (t_acc, ref_acc) -> + if x = var then + t_acc, IntMap.fold (fun y cs ref_acc -> TVIS.set_constant_lhs y const (Coeffs.to_set cs) ref_acc) ys ref_acc + else + match IntMap.find_opt var ys with + | None -> IntMap.add x ys t_acc, ref_acc + | Some cs -> + let ys' = IntMap.remove var ys in + let ref_acc = TVIS.set_constant_rhs x const (Coeffs.to_set cs) ref_acc in + if IntMap.is_empty ys' then t_acc, ref_acc else (IntMap.add x ys' t_acc, ref_acc) + ) t (IntMap.empty,[]) + + let invariant t env = IntMap.fold (fun x ys acc -> IntMap.fold (fun y cs acc -> TVIS.invariant env x y (Coeffs.to_set cs) acc) ys acc) t [] + + let ignore_empty ls = + if IntMap.is_empty ls then None + else Some ls + + let rec get_relations (((c_x, x,o_x,d_x), x_val) as x') (((c_y, y,o_y,d_y), y_val) as y') t = + if x > y then + (*We save information only in one of the directions -> check the other one*) + List.map Relation.swap_sides @@ get_relations y' x' t + else begin + if M.tracing then M.trace "get_relations" "checking x'=%s, y'=%s" (Rhs.show (Some (c_x, x), o_x, d_x)) (Rhs.show (Some (c_y, y), o_y, d_y)); + match get_coeff x y t with + | None -> begin if M.tracing then M.trace "get_relations" "no inequality for roots"; [] end (*No information*) + | Some coeff -> + let coeff = Coeffs.to_set coeff in + let interval_ineqs = LinearInequality.from_values x_val y_val in + let coeff = List.fold (fun t (k,c) -> TVIS.add_inequality k c t) coeff interval_ineqs in + let (k,c_rhs) = LinearInequality.from_rhss (c_x,o_x,d_x) (c_y,o_y,d_y) None in + let factor = (*we need to muliply c' with this factor because LinearInequalities scales them down*) + let a = Q.make c_x d_x in + let b = Q.make c_y d_y in + if Q.equal b Q.zero then a else b + in + let upper_bound = match TVIS.get_best_offset k coeff with + | None -> [] + | Some c_ineq -> + let c' = Q.mul factor @@ Q.sub c_ineq c_rhs in + [Relation.Lt, Z.succ @@ Z.fdiv (Q.num c') (Q.den c')] (*add one to make it a strict inequality*) + in match TVIS.get_best_offset (TVIS.Key.negate k) coeff with (*lower bound*) + | None -> upper_bound + | Some c_ineq -> + let c' = Q.mul factor ( Q.add c_ineq c_rhs) in + (Gt, Z.pred @@ Z.cdiv (Q.num c') (Q.den c')) :: upper_bound + end + + let get_relations x y t = + let res = get_relations x y t in + if M.tracing then M.trace "get_relations" "result: %s" (BatList.fold (fun acc c -> acc ^ ", " ^ Relation.show "x'" c "y'") "" res); + res + + let meet_relation x' y' cond get_rhs get_value t = + let rec meet_relation_roots x y k c (t, ref_acc) = + if x > y then + let k', c' = LinearInequality.swap_sides (k,c) in + meet_relation_roots y x k' c' (t, ref_acc) + else begin + if M.tracing then M.tracel "meet_relation" "meet_relation_roots: %s" @@ LinearInequality.show ("var_" ^ Int.to_string x) ("var_" ^ Int.to_string y) (k,c); + if x = y then + let s = TVIS.Key.get_slope k in + if Q.equal Q.one s then (* x <= x + c (or >=) *) + match k with + | LE _ -> if Q.lt c Q.zero then raise EConj.Contradiction else (t, []) (*trivially true*) + | GE _ -> if Q.gt c Q.zero then raise EConj.Contradiction else (t, []) (*trivially true*) + else (* sx <= x + c (or =>) -> refine the value in this case*) + let s' = Q.sub s Q.one in + let s', c' = match k with LE _ -> s',c | GE _ -> Q.neg s', Q.neg c in + (*s'x <= c' *) + if Q.gt s' Q.zero then + let max = Q.div c' s' in + t, (x, Either.Left (Value.ending @@ Z.cdiv (Q.num max) (Q.den max))) :: ref_acc + else + let min = Q.div c' s' in + t, (x, Left (Value.starting @@ Z.fdiv (Q.num min) (Q.den min))) :: ref_acc + else + let coeffs = match get_coeff x y t with + | None -> TVIS.empty + | Some c -> Coeffs.to_set c + in let coeffs', ref_acc = TVIS.meet_single_inequality (x,get_value x) (y,get_value y) k c (coeffs,ref_acc) + in match Coeffs.of_set (get_value x) (get_value y) coeffs' with + | None -> remove_coeff x y t , ref_acc + | Some c -> set_coeff x y c t, ref_acc + end in + let apply_transivity x y k c t = + if x = y then begin + if M.tracing then M.tracel "transitivity" "transitivity between same variable %d -> skip" x; + t, [] + end else begin + if M.tracing then M.tracel "transitivity" "transitivity with %s and %s" (LinearInequality.show ("var_" ^ Int.to_string x) ("var_" ^ Int.to_string y) (k,c)) (show t); + IntMap.fold (fun w zs acc -> + if w = x then + IntMap.fold (fun z cs acc -> + match TVIS.combine_left (k,c) @@ Coeffs.to_set cs with + | None -> + if M.tracing then M.tracel "transitivity" "case 1, combined with %s into Nothing " (Coeffs.show_formatted ("var_" ^ Int.to_string w) ("var_" ^ Int.to_string z) cs); + acc + | Some cs' -> + if M.tracing then M.tracel "transitivity" "case 1, combined with %s into %s " (Coeffs.show_formatted ("var_" ^ Int.to_string w) ("var_" ^ Int.to_string z) cs) (TVIS.show_formatted ("var_" ^ Int.to_string y) ("var_" ^ Int.to_string z) cs'); + TVIS.CoeffMap.fold (fun k c acc -> meet_relation_roots y z k c acc) cs' acc + ) zs acc + else if w = y then + IntMap.fold (fun z cs acc -> + match TVIS.combine_left (LinearInequality.swap_sides (k,c)) @@ Coeffs.to_set cs with + | None -> + if M.tracing then M.tracel "transitivity" "case 2, combined with %s into Nothing " (Coeffs.show_formatted ("var_" ^ Int.to_string w) ("var_" ^ Int.to_string z) cs); + acc + | Some cs' -> + if M.tracing then M.tracel "transitivity" "case 2, combined with %s into %s " (Coeffs.show_formatted ("var_" ^ Int.to_string w) ("var_" ^ Int.to_string z) cs) (TVIS.show_formatted ("var_" ^ Int.to_string x) ("var_" ^ Int.to_string z) cs'); + TVIS.CoeffMap.fold (fun k c acc -> meet_relation_roots x z k c acc) cs' acc + ) zs acc + else + IntMap.fold (fun z cs acc -> + if z = x then + match TVIS.combine_right (k,c) @@ Coeffs.to_set cs with + | None -> + if M.tracing then M.tracel "transitivity" "case 3, combined with %s into Nothing " (Coeffs.show_formatted ("var_" ^ Int.to_string w) ("var_" ^ Int.to_string z) cs); + acc + | Some cs' -> + if M.tracing then M.tracel "transitivity" "case 3, combined with %s into %s " (Coeffs.show_formatted ("var_" ^ Int.to_string w) ("var_" ^ Int.to_string z) cs) (TVIS.show_formatted ("var_" ^ Int.to_string w) ("var_" ^ Int.to_string y) cs'); + TVIS.CoeffMap.fold (fun k c acc -> meet_relation_roots w y k c acc) cs' acc + else if z = y then + match TVIS.combine_right (LinearInequality.swap_sides (k,c)) @@ Coeffs.to_set cs with + | None -> + if M.tracing then M.tracel "transitivity" "case 4, combined with %s into Nothing " (Coeffs.show_formatted ("var_" ^ Int.to_string w) ("var_" ^ Int.to_string z) cs); + acc + | Some cs' -> + if M.tracing then M.tracel "transitivity" "case 4, combined with %s into %s " (Coeffs.show_formatted ("var_" ^ Int.to_string w) ("var_" ^ Int.to_string z) cs) (TVIS.show_formatted ("var_" ^ Int.to_string w) ("var_" ^ Int.to_string x) cs'); + TVIS.CoeffMap.fold (fun k c acc -> meet_relation_roots w x k c acc) cs' acc + else + acc + ) zs acc + ) t (t, []) + end in + match get_rhs x', get_rhs y' with + | (Some (c_x, x),o_x,d_x), (Some (c_y, y),o_y,d_y) -> begin + let (k,c) = LinearInequality.from_rhss (c_x,o_x,d_x) (c_y,o_y,d_y) (Some (match fst cond with Relation.Lt -> true | _ -> false)) + in let factor = (*we need to divide o by this factor because LinearInequalities normalises it.*) + let a = Q.make c_x d_x in + let b = Q.make c_y d_y in + if Q.equal b Q.zero then a else b + in match cond with + | Relation.Lt, o -> + let c' = (Q.add c @@ Q.div (Q.of_bigint o) factor) in + let t, ref_acc = apply_transivity x y k c' t in + meet_relation_roots x y k c' (t, ref_acc) + | Gt, o -> + let k = TVIS.Key.negate k in + let c' = (Q.add c @@ Q.div (Q.of_bigint o) factor) in + let t, ref_acc = apply_transivity x y k c' t in + meet_relation_roots x y k c' (t,ref_acc) + end + (*Cases where one of the variables is a constant -> refine value*) + | (None, o_x, _), (Some _,_,_) -> t, [Refinement.of_value y' @@ Relation.value_with_const_left cond o_x] + | (Some _,_,_), (None, o_y, _) -> t, [Refinement.of_value x' @@ Relation.value_with_const_right cond o_y] + | (None, o_x, _), (None, o_y, _) -> + let v = Relation.value_with_const_right cond o_y in + if Value.contains v o_x then + t, [] + else + raise EConj.Contradiction + + + let meet_relation x y c r v t = + if M.tracing then M.tracel "meet_relation" "meeting %s with %s" (show t) (Relation.show ("var_"^Int.to_string x) c ("var_"^Int.to_string y)); + let res, refine_acc = meet_relation x y c r v t in + if M.tracing then M.tracel "meet_relation" "result: %s, refinements: %s " (show res) (Refinement.show refine_acc); + res, refine_acc + + (*We want to be lazy and only convert to TVIS if necessary. To be able to reuse this function in transfer, + we also need to be able to work with an already converted Map -> add functions for conversion*) + let substitute' t i (coeff, j, offs, divi) to_set of_set = + (*if both sides refer to the same variable: check for contradictions or refine the value*) + let constraints_same_variable cs = + let check_single k c value = + let s = TVIS.Key.get_slope k in + if Q.equal Q.one s then (* x <= x + c (or >=) *) + match k with + | LE _ -> if Q.lt c Q.zero then raise EConj.Contradiction else value (*trivially true*) + | GE _ -> if Q.gt c Q.zero then raise EConj.Contradiction else value (*trivially true*) + else (* sx <= x + c (or =>) -> refine the value in this case*) + let s' = Q.sub s Q.one in + let s', c' = match k with LE _ -> s',c | GE _ -> Q.neg s', Q.neg c in + (*s'x <= c' *) + if Q.gt s' Q.zero then + let max = Q.div c' s' in + Value.meet value @@ Value.ending @@ Z.cdiv (Q.num max) (Q.den max) + else + let min = Q.div c' s' in + Value.meet value @@ Value.starting @@ Z.fdiv (Q.num min) (Q.den min) + in TVIS.CoeffMap.fold check_single cs Value.top + in + let without_i = forget_variable t i in + (*add to bindings, meeting with existing if necessary*) + let merge_single x y cs_new (t,ref_acc) = + let cs_curr = BatOption.default TVIS.empty @@ BatOption.map to_set @@ get_coeff x y t in + let cs_combined, ref_acc = TVIS.meet (x,Value.top) (y,Value.top) cs_new cs_curr ref_acc in + match of_set x y cs_combined with + | None -> t,ref_acc + | Some cs_combined -> set_coeff x y cs_combined t, ref_acc + in + let fold_x x ys acc = + if x < i then + match IntMap.find_opt i ys with + | None -> acc + | Some cs -> + let cs = to_set cs in + let cs' = TVIS.substitute_right (coeff, offs, divi) cs in + if x = j then (*We now have inequalities with the same variable on both sides *) + let t,ref_acc = acc in + let v = constraints_same_variable cs' in + t, Refinement.of_value x v :: ref_acc + else if x < j then + merge_single x j cs' acc + else (*x > j -> swap sides*) + let cs'' = TVIS.swap_sides cs' in + merge_single j x cs'' acc + else if x = i then + let fold_y y cs acc = + let cs' = TVIS.substitute_left (coeff, offs, divi) cs in + if j < y then + merge_single j y cs' acc + else if j = y then begin + let t,ref_acc = acc in + let v = constraints_same_variable cs' in + t, Refinement.of_value x v :: ref_acc + end else + let cs'' = TVIS.swap_sides cs' in + merge_single y j cs'' acc + in + IntMap.fold fold_y (IntMap.map to_set ys) acc + else + acc + in IntMap.fold fold_x t (without_i, []) + + let substitute get_value t i (c,j,o,d) = + if M.tracing then M.trace "substitute" "substituting var_%d in %s with %s" i (show t) (Rhs.show (Some (c,j), o, d)); + let t, ref_acc = substitute' t i (c,j,o,d) Coeffs.to_set (fun x y s -> Coeffs.of_set (get_value x) (get_value y) s) in + if M.tracing then M.trace "substitute" "resulting in %s, refinements: %s" (show t) (Refinement.show ref_acc); + t, ref_acc + + let transfer x cond t_old get_rhs_old get_value_old t get_rhs get_value = + match get_rhs_old x, get_rhs x with + | (Some (coeff_old,x_root_old), off_old, divi_old), ((Some (coeff,x_root), off, divi) as rhs) -> + (*convert the relation to a linear inequality refering to the old root *) + let (k,c) = LinearInequality.from_rhss (coeff_old, off_old, divi_old) (coeff_old, off_old, divi_old) (Some (match fst cond with Relation.Lt -> true | _ -> false)) + in let factor = Q.make coeff_old divi_old (*we need to divide o by this factor because LinearInequalities normalizes*) + in let ineq_from_cond = match cond with + | Relation.Lt, o -> k, (Q.add c @@ Q. div (Q.of_bigint o) factor) + | Gt, o -> (TVIS.Key.negate k), (Q.add c @@ Q. div (Q.of_bigint o) factor) + in + (*combine the inequality from cond with all inequalities*) + (*throw out all inequalities that do not contain the representative of x*) + let combine_1 v1 v2s = + if v1 = x_root_old then ignore_empty @@ IntMap.filter_map (fun _ c -> TVIS.combine_left ineq_from_cond @@ Coeffs.to_set c) v2s + else + let combine_2 v2 c = if v2 = x_root_old then TVIS.combine_right ineq_from_cond @@ Coeffs.to_set c else None in + ignore_empty @@ IntMap.filter_map combine_2 v2s + in + let filtered = IntMap.filter_map combine_1 t_old in + if M.tracing then M.tracel "transfer" "filtered + combined %s" (show_map (Printf.sprintf "var_%d") TVIS.show_formatted filtered); + (*transform all inequalities to refer to new root of x*) + (*invert old rhs, then substitute the new rhs for x*) + let (m, o, d) = Rhs.subst rhs x @@ snd @@ EConj.inverse x (coeff_old,x_root_old, off_old, divi_old) in + let c, v = BatOption.get m in + let transformed, ref_acc = substitute' filtered x_root (c, v, o, d) identity (fun _ _ c -> TVIS.ignore_empty c) in + if M.tracing then M.tracel "transfer" "transformed: %s, refinements: %s" (show_map (Printf.sprintf "var_%d") TVIS.show_formatted transformed) (Refinement.show ref_acc); + (*meet with this set of equations*) + let meet' t1 t2 = IntMap.fold (fun x ys acc -> IntMap.fold (fun y coeff acc -> meet_one_coeff true get_value x y coeff acc) ys acc) t1 (t2,ref_acc) in + meet' transformed t + | _,_ -> t, [] (*ignore constants*) + + let transfer x cond t_old get_rhs_old get_value_old t get_rhs get_value = + let cond = Relation.swap_sides cond in (*The interface changed, but I do not want to reimplement this function*) + if M.tracing then M.tracel "transfer" "transfering with %s from %s into %s" (Relation.show ("var_" ^ Int.to_string x ^ "_old") cond ("var_" ^ Int.to_string x ^ "_new") ) (show t_old) (show t); + let res, ref_acc = transfer x cond t_old get_rhs_old get_value_old t get_rhs get_value in + if M.tracing then M.tracel "transfer" "result: %s, refinements: %s" (show res) (Refinement.show ref_acc); + res, ref_acc + + let limit econj t = + let conf = GobConfig.get_string "ana.lin2vareq_p.inequalities" in + if conf <> "coeffs_count" && conf <> "coeffs_threshold" then t else + let coeffs = coeffs_from_econj econj in + let limit_single x y cs = + Coeffs.limit ( slopes_from_coeffs coeffs (min x y, max x y)) cs + in IntMap.filter_map (fun x ys -> ignore_empty @@ IntMap.filter_map (fun y cs -> limit_single x y cs) ys) t + + let limit e t = Timing.wrap "limit" (limit e) t + + let copy_to_new_representants econj_old econj_new get_value t = + let coeffs = coeffs_from_econj econj_new in + (*a var is representant if it does not show up in the sparse map*) + let all_representants_in_new = + let rec aux acc n = + if n > (fst econj_new) then acc + else if IntMap.mem n (snd econj_new) then aux acc (n + 1) + else aux (n :: acc) (n + 1) + in aux [] 0 + in let new_representants_in_new = List.filter (fun v -> IntMap.mem v (snd econj_old)) all_representants_in_new + in if M.tracing then M.trace "new_reps" "all_in_new: %s, new_in_new: %s" (List.fold (fun a i -> Int.to_string i ^ ", " ^ a) "" all_representants_in_new) (List.fold (fun a i -> Int.to_string i ^ ", " ^ a) "" new_representants_in_new); + let add_new v_new t_acc other_var = + if v_new = other_var then t_acc else + (*get the old rhs*) + match IntMap.find v_new (snd econj_old) with + | None,_,_ -> t_acc (*skip constants*) + | (Some (c,old_rep), o, d) -> + let allowed_slopes = Hashtbl.to_seq_keys @@ slopes_from_coeffs coeffs (min v_new other_var, max v_new other_var) in + (*inverse rhs so that we can translate the inequalities of the old representant to slopes corresponding to the new representant*) + let (_, (mi,oi,di)) = EConj.inverse v_new (c,old_rep,o,d) in + let ci,_ = BatOption.get mi in + (*convert the slope from new representant to old*) + let convert_to_old ineq = + if v_new < other_var then + LinearInequality.substitute_left (c,o,d) ineq + else + let ineq' = LinearInequality.substitute_right (c,o,d) ineq in + if old_rep < other_var then + LinearInequality.swap_sides ineq' + else ineq' + (*convert back*) + in let convert_to_new ineq = + if v_new < other_var then + LinearInequality.substitute_left (ci,oi,di) ineq + else + let ineq' = if old_rep < other_var then LinearInequality.swap_sides ineq else ineq + in LinearInequality.substitute_right (ci,oi,di) ineq' + (*relations between the old representant and the other variable*) + in let coeffs_old = BatOption.default TVIS.empty @@ BatOption.map Coeffs.to_set @@ get_coeff (min old_rep other_var) (max old_rep other_var) t in + if M.tracing then M.trace "new_reps" "coeffs_old for old %d other %d new %d: %s" old_rep other_var v_new (TVIS.show_formatted "min" "max" coeffs_old); + if TVIS.CoeffMap.is_empty coeffs_old then t_acc else (*skip the rest if there is no need *) + let add_single_slope c_acc s = + let ineqs = [LinearInequality.OriginInequality.LE s, Q.zero; GE s, Q.zero;] + in let copy_single_ineq c_acc ineq = + let k_old = fst @@ convert_to_old ineq in + (*TODO maybe this introduces too many new inequalities -> only take explicit stored ones?*) + match TVIS.get_best_offset k_old coeffs_old with + | None -> c_acc + | Some o -> + let k_neq, o_new = convert_to_new (k_old, o) in + TVIS.add_inequality k_neq o_new c_acc + in List.fold copy_single_ineq c_acc ineqs + in let coeffs_new = Seq.fold_left add_single_slope TVIS.empty allowed_slopes + in let x, y = min v_new other_var , max v_new other_var + in match Coeffs.of_set (get_value x) (get_value y) coeffs_new with + | Some coeffs_new -> set_coeff x y coeffs_new t_acc + | _ -> t_acc + in List.fold (fun acc v_new -> List.fold (add_new v_new ) acc all_representants_in_new ) t new_representants_in_new + + let copy_to_new_representants econj_old econj_new t = Timing.wrap "new_reps" (copy_to_new_representants econj_old econj_new) t + +end + +module PentagonCoeffs : Coeffs = struct + (*true -> x < y *) + (*false -> x > y *) + type t = bool [@@deriving eq, hash, ord] + + let join x y get_val_t1 get_val_t2 t1 t2 = + match t1, t2 with + | None, None -> None + | Some d1, Some d2 -> if d1 = d2 then Some d1 else None + | Some true, None -> if Value.must_be_neg @@ Value.sub (get_val_t2 x) (get_val_t2 y) then Some true else None + | Some false, None -> if Value.must_be_pos @@ Value.sub (get_val_t2 x) (get_val_t2 y) then Some false else None + | None, Some true -> if Value.must_be_neg @@ Value.sub (get_val_t1 x) (get_val_t1 y) then Some true else None + | None, Some false -> if Value.must_be_pos @@ Value.sub (get_val_t1 x) (get_val_t1 y) then Some false else None + + let widen x y get_val_t1 get_val_t2 t1 t2 = t2 + + let limit _ t = Some t + + let show_formatted x y t = x ^ (if t then "<" else ">") ^ y + + let to_set t = + let open LinearInequality.OriginInequality in + let i = if t then LE Q.one else GE Q.one in + (*x < y <==> x <= y - 1*) + let o = if t then Q.minus_one else Q.one in + TVIS.CoeffMap.singleton i o + + let to_set = Timing.wrap "to_set" to_set + + let of_set x_val y_val s = + let open LinearInequality.OriginInequality in + let s' = List.fold (fun t (k,c) -> TVIS.add_inequality k c t) s @@ LinearInequality.from_values x_val y_val in + match TVIS.get_best_offset (LE Q.one) s' with + | Some c when Q.(<=) c Q.minus_one -> Some true + | _ -> match TVIS.get_best_offset (GE Q.one) s' with + | Some c when Q.(>=) c Q.one -> Some false + | _ -> None + + let of_set x_val y_val = Timing.wrap "of_set" (of_set x_val y_val) + +end + +module PentagonOffsetCoeffs : Coeffs = struct + (*x <= y + c, x >= y + c, None = Top *) + type t = Z.t option * Z.t option [@@deriving eq, hash, ord] + + let flatten (u,l) = if u = None && l = None then None else Some (u,l) + + let join x y get_val_t1 get_val_t2 t1 t2 = + let l_of_values get_values = + let diff = Value.sub (get_values x) (get_values y) in + match Value.minimal diff with + | Some (Int i) -> Some i + | _ -> None + in + let u_of_values get_values = + let diff = Value.sub (get_values x) (get_values y) in + match Value.maximal diff with + | Some (Int i) -> Some i + | _ -> None + in + let open BatOption in + let lift2 f a b = bind a (fun a -> bind b (fun b -> Some (f a b))) in + match t1, t2 with + | None, None -> None + | None, Some (u,l) -> + let u = lift2 max u @@ u_of_values get_val_t1 in + let l = lift2 min l @@ l_of_values get_val_t1 in + flatten (u,l) + | Some (u,l), None -> + let u = lift2 max u @@ u_of_values get_val_t2 in + let l = lift2 min l @@ l_of_values get_val_t2 in + flatten (u,l) + | Some (u1,l1), Some (u2,l2) -> + let u1 = lift2 min u1 @@ u_of_values get_val_t1 in + let u2 = lift2 min u2 @@ u_of_values get_val_t2 in + let u = lift2 max u1 u2 in + let l1 = lift2 max l1 @@ l_of_values get_val_t1 in + let l2 = lift2 max l2 @@ l_of_values get_val_t2 in + let l = lift2 min l1 l2 in + flatten (u,l) + + let show_formatted x y (u,l) = + let u = match u with + | None -> "" + | Some u -> x ^ " <= " ^ y ^ " + " ^ Z.to_string u + in let l = match l with + | None -> "" + | Some l -> x ^ " >= " ^ y ^ " + " ^ Z.to_string l + in u ^ " , " ^ l + + let join x y get_val_t1 get_val_t2 t1 t2 = + let res = join x y get_val_t1 get_val_t2 t1 t2 in + if M.tracing then M.trace "joinc" "\na: %s, x=%s,y=%s\nb: %s, x=%s,y=%s\n -> %s" + (BatOption.map_default (show_formatted "x" "y") "None" t1) + (Value.show @@ get_val_t1 x) + (Value.show @@ get_val_t1 y) + (BatOption.map_default (show_formatted "x" "y") "None" t2) + (Value.show @@ get_val_t2 x) + (Value.show @@ get_val_t2 y) + (BatOption.map_default (show_formatted "x" "y") "None" res); + res + + let widen x y get_val_t1 get_val_t2 t1 t2 = + match t1, t2 with + | None, None + | None, Some _ + | Some _, None -> None + | Some (u1,l1), Some (u2,l2) -> + let l = if l1 = l2 then l2 else None in + let u = if u1 = u2 then u2 else None in + flatten (u,l) + + let limit _ t = Some t + + let to_set (u,l) = + let open LinearInequality.OriginInequality in + let s = TVIS.empty in + let s = match u with + | None -> s + | Some u -> TVIS.add_inequality (LE Q.one) (Q.of_bigint u) s + in + match l with + | None -> s + | Some l -> TVIS.add_inequality (GE Q.one) (Q.of_bigint l) s + + let to_set = Timing.wrap "to_set" to_set + + let of_set x_val y_val s = + let open LinearInequality.OriginInequality in + let s' = List.fold (fun t (k,c) -> TVIS.add_inequality k c t) s @@ LinearInequality.from_values x_val y_val in + let u = BatOption.map round_down @@ TVIS.get_best_offset (LE Q.one) s' in + let l = BatOption.map round_up @@ TVIS.get_best_offset (GE Q.one) s' in + flatten (u,l) + + let of_set x_val y_val = Timing.wrap "of_set" (of_set x_val y_val) + +end + +(* limit: use linear time algorithm for coeffs_count instead of sorting??*) +(* widening thresholds: from offsets of rhs?*) +(* store information about representants to avoid recalculating them: congruence information, group size/ coefficients ??*) +(* rename Coeff projection?*) \ No newline at end of file diff --git a/src/cdomains/apron/representantDomains.no-apron.ml b/src/cdomains/apron/representantDomains.no-apron.ml new file mode 100644 index 0000000000..76eb4a698a --- /dev/null +++ b/src/cdomains/apron/representantDomains.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. *) diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index 8ccf411b4e..d020d51187 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -227,6 +227,12 @@ struct let tcons1_of_cil_exp ask d env e negate no_ov = let e = Cil.constFold false e in + let rec unwrap_inversion e negate = + match e with + | UnOp (LNot,e',_) -> unwrap_inversion e' (not negate) + | _ -> e, negate + in + let e, negate = unwrap_inversion e negate in let (texpr1_plus, texpr1_minus, typ) = match e with | BinOp (r, e1, e2, _) -> diff --git a/src/common/framework/analysisState.ml b/src/common/framework/analysisState.ml index 4dd4744967..308e354186 100644 --- a/src/common/framework/analysisState.ml +++ b/src/common/framework/analysisState.ml @@ -4,7 +4,7 @@ This is set to true in control.ml before we verify the result (or already before solving if warn = 'early') *) let should_warn = ref false -(** If this is true, any overflows happening in IntDomains will not lead to warnings being produced or +(** If this is true, any overflows and potential division by zero happening in IntDomains will not lead to warnings being produced or {!svcomp_may_overflow} being set to true. This is useful when, e.g., {!BaseInvariant.Make.invariant} executes computations that are not in the actual program *) diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 23a85e7045..3083c6a224 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -580,7 +580,13 @@ "termination", "tmpSpecialAnalysis" ] - } + }, + "extraTerminationDomain": { + "title": "ana.autotune.extraTerminationDomain", + "description": "Domain activated by the 'termination' autotuner. Specifying 'apron' also selects the polyhedra domain", + "type": "string", + "default": "apron" + } }, "additionalProperties": false }, @@ -1029,6 +1035,32 @@ }, "additionalProperties": false }, + "lin2vareq_p": { + "title": "ana.lin2vareq_p", + "type": "object", + "properties": { + "inequalities": { + "title": "ana.lin2vareq_p.inequalities", + "description": "Which domain to use to detect inequalities", + "type": "string", + "enum": ["none","pentagon", "pentagon_offset", "coeffs_count", "coeffs_threshold", "unlimited"], + "default": "coeffs_threshold" + }, + "coeffs_count": { + "title": "ana.lin2vareq_p.coeffs_count", + "description": "How many inequalities to keep for every representant pair when using coeffs_count. ", + "type": "integer", + "default": 14 + }, + "coeffs_threshold": { + "title": "ana.lin2vareq_p.coeffs_threshold", + "description": "Percentage of inequalities to keep for every representant pair when using coeffs_threshold. Larger connected groups are allowed more coefficients.", + "type": "integer", + "default": 100 + } + }, + "additionalProperties": false + }, "context": { "title": "ana.context", "type": "object", diff --git a/src/dune b/src/dune index 964e23a5f7..6fec8243cd 100644 --- a/src/dune +++ b/src/dune @@ -47,6 +47,18 @@ (apron -> linearTwoVarEqualityDomain.apron.ml) (-> linearTwoVarEqualityDomain.no-apron.ml) ) + (select linearTwoVarEqualityAnalysisPentagon.ml from + (apron -> linearTwoVarEqualityAnalysisPentagon.apron.ml) + (-> linearTwoVarEqualityAnalysisPentagon.no-apron.ml) + ) + (select representantDomains.ml from + (apron -> representantDomains.apron.ml) + (-> representantDomains.no-apron.ml) + ) + (select linearTwoVarEqualityDomainPentagon.ml from + (apron -> linearTwoVarEqualityDomainPentagon.apron.ml) + (-> linearTwoVarEqualityDomainPentagon.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 5c83be6e3c..4077148c7b 100644 --- a/src/goblint_lib.ml +++ b/src/goblint_lib.ml @@ -77,6 +77,8 @@ module RelationAnalysis = RelationAnalysis module ApronAnalysis = ApronAnalysis module AffineEqualityAnalysis = AffineEqualityAnalysis module LinearTwoVarEqualityAnalysis = LinearTwoVarEqualityAnalysis +module LinearTwoVarEqualityAnalysisPentagon = LinearTwoVarEqualityAnalysisPentagon +module RepresentantDomains = RepresentantDomains module VarEq = VarEq module CondVars = CondVars module TmpSpecial = TmpSpecial @@ -264,6 +266,8 @@ module ApronDomain = ApronDomain module AffineEqualityDomain = AffineEqualityDomain module AffineEqualityDenseDomain = AffineEqualityDenseDomain module LinearTwoVarEqualityDomain = LinearTwoVarEqualityDomain +module LinearTwoVarEqualityDomainPentagon = LinearTwoVarEqualityDomainPentagon + (** {5 2-Pointer Logic} diff --git a/tests/regression/88-lin2vareq_p/01-loop.c b/tests/regression/88-lin2vareq_p/01-loop.c new file mode 100644 index 0000000000..c55215c998 --- /dev/null +++ b/tests/regression/88-lin2vareq_p/01-loop.c @@ -0,0 +1,23 @@ +//SKIP PARAM: --set ana.activated[+] lin2vareq_p --set sem.int.signed_overflow assume_none + +// Adapted example from https://link.springer.com/content/pdf/10.1007/BF00268497.pdf + +#include + +void main(void) { + int i; + int j; + int k; + if(k > 200){ + return 0; + } + j = k + 5; + + while (j < 100) { + __goblint_check(j - k == 5); //SUCCESS + j = j + 3; + k = k + 3; + } + __goblint_check(j - k == 5); //SUCCESS + +} diff --git a/tests/regression/88-lin2vareq_p/02-iteration.c b/tests/regression/88-lin2vareq_p/02-iteration.c new file mode 100644 index 0000000000..838034646b --- /dev/null +++ b/tests/regression/88-lin2vareq_p/02-iteration.c @@ -0,0 +1,17 @@ +//SKIP PARAM: --set ana.activated[+] lin2vareq_p +#include + +int main() { + int i, j; + int size = 5; + + for (i = 0; i < size; ++i) { + j = i; + + __goblint_check(i == j); //SUCCESS + } + + return 0; +} + +//This test case checks whether the value of variable i is always equal to the value of variable j within the loop. diff --git a/tests/regression/88-lin2vareq_p/03-loop_increment.c b/tests/regression/88-lin2vareq_p/03-loop_increment.c new file mode 100644 index 0000000000..b92c0cb843 --- /dev/null +++ b/tests/regression/88-lin2vareq_p/03-loop_increment.c @@ -0,0 +1,23 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq_p --set sem.int.signed_overflow assume_none +#include + +int main() { + int i, j, k; + int size; //with a fixed size, the inequalities lead to a discovery of exact constants and no relations + i = 0; + j = 0; + k = 5; + + if (size > 0) { + for (i = 1; i < size; ++i) { + j = i; + k = j + 5; + } + + __goblint_check(j + 1 == i); // SUCCESS + + __goblint_check(k == i + 4); // SUCCESS + + } + return 0; +} diff --git a/tests/regression/88-lin2vareq_p/04-complicated_expression.c b/tests/regression/88-lin2vareq_p/04-complicated_expression.c new file mode 100644 index 0000000000..ebe41061e5 --- /dev/null +++ b/tests/regression/88-lin2vareq_p/04-complicated_expression.c @@ -0,0 +1,24 @@ +// SKIP PARAM: --set sem.int.signed_overflow assume_none --set ana.int.enums false --set ana.int.interval false --set ana.int.interval_set false --set ana.int.congruence false --set ana.activated[+] lin2vareq_p + +#include +#include + + +int main() { + int x; + int k; + if (x < 300 && k < 300) { + int y = 5; + + int result1 = 3 * (x + y) - 2 * x + 6; + int result2 = 3 * (x + y) - 2 * k + 6; + int result3 = x * 3 - x * 2; + int result4 = x * 3 - x * k * x; + + __goblint_check(result1 == x + 21); // SUCCESS + __goblint_check(result2 == x + 21); // UNKNOWN! + __goblint_check(result3 == x); // SUCCES + __goblint_check(result4 == x * 3 - x * k * x); // UNKNOWN + } + return 0; +} diff --git a/tests/regression/88-lin2vareq_p/05-overflow.c b/tests/regression/88-lin2vareq_p/05-overflow.c new file mode 100644 index 0000000000..aef5f04b6c --- /dev/null +++ b/tests/regression/88-lin2vareq_p/05-overflow.c @@ -0,0 +1,23 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq_p + +#include + +int main() { + int x; + int k; + int y; + + x = k + 1; + //there might be an overflow + __goblint_check(x == k + 1); // UNKNOWN! + + int unknown; + + if (unknown < 300 && unknown > 0) { + x = unknown; + // an overflow is not possible + __goblint_check(x == unknown); // SUCCESS + } + + return 0; +} diff --git a/tests/regression/88-lin2vareq_p/06-join-non-constant.c b/tests/regression/88-lin2vareq_p/06-join-non-constant.c new file mode 100644 index 0000000000..bd1bf20d38 --- /dev/null +++ b/tests/regression/88-lin2vareq_p/06-join-non-constant.c @@ -0,0 +1,25 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq_p --set sem.int.signed_overflow assume_none + +#include + +int main(void) { + int a, b, c, d; + + int t; + + if (t) { + b = a + 2; + c = a + 7; + d = a + 1; + } else { + b = a + 30; + c = a + 35; + d = a + 10; + } + __goblint_check(c == b + 5); // SUCCESS + __goblint_check(c == b + 3); // FAILURE + __goblint_check(d == b - 1); // UNKNOWN! + __goblint_check(b == a + 2); // UNKNOWN! + + return 0; +} diff --git a/tests/regression/88-lin2vareq_p/07-coeff_vec.c b/tests/regression/88-lin2vareq_p/07-coeff_vec.c new file mode 100644 index 0000000000..06a1bfdc7d --- /dev/null +++ b/tests/regression/88-lin2vareq_p/07-coeff_vec.c @@ -0,0 +1,22 @@ +//SKIP PARAM: --set ana.activated[+] lin2vareq_p +// This was problematic earlier where both branches were dead with lin2vareq +// Thus worth having even if it can be answered by base alone +int main() { + + unsigned int a = 1; + + unsigned int b = -a; + + __goblint_check(b == 4294967295); + + unsigned short int allbits = -1; + + short int signedallbits = allbits; + + __goblint_check(signedallbits == -1); + + short c = 32767; + c = c + 2; + + __goblint_check(c == -32767); +} diff --git a/tests/regression/88-lin2vareq_p/08-partitioning.c b/tests/regression/88-lin2vareq_p/08-partitioning.c new file mode 100644 index 0000000000..b6a8b1025c --- /dev/null +++ b/tests/regression/88-lin2vareq_p/08-partitioning.c @@ -0,0 +1,39 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq_p --set sem.int.signed_overflow assume_none +// example from https://dl.acm.org/doi/10.1145/2049706.2049710 + +#include +#include +#include + +int main() { + + int x, x1, x2, x3, x4, x5, x6, x7; + + if (x1 > INT_MAX - 5 || x2 > INT_MAX - 5 || x2 > INT_MIN + 5) { + return -1; + } + + if (x > 5) { + x1 = x1; + x2 = x2; + x3 = x1; + x4 = x2 + 5; + x5 = x1 + 5; + x6 = x1 + 3; + x7 = x1 + 2; + } else { + x1 = x1; + x2 = x2; + x3 = x2 - 5; + x4 = x2 + 5; + x5 = x2; + x6 = x2 + 1; + x7 = x2; + } + + __goblint_check(x4 == x2 + 5); // SUCCESS + __goblint_check(x5 == x3 + 5); // SUCCESS + __goblint_check(x7 == x6 - 1); // SUCCESS + + return 0; +} diff --git a/tests/regression/88-lin2vareq_p/09-loop_relational.c b/tests/regression/88-lin2vareq_p/09-loop_relational.c new file mode 100644 index 0000000000..dcdcfd8cb2 --- /dev/null +++ b/tests/regression/88-lin2vareq_p/09-loop_relational.c @@ -0,0 +1,22 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq_p --set sem.int.signed_overflow assume_none + + +#include +#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); // SUCCESS + z = 2; + __goblint_check(y == i); // SUCCESS + __goblint_check(z == 2); // SUCCESS + } + + return 0; +} diff --git a/tests/regression/88-lin2vareq_p/10-linear_loop.c b/tests/regression/88-lin2vareq_p/10-linear_loop.c new file mode 100644 index 0000000000..75df99d858 --- /dev/null +++ b/tests/regression/88-lin2vareq_p/10-linear_loop.c @@ -0,0 +1,21 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq_p --set sem.int.signed_overflow assume_none + +#include +#include + +int main() { + int x = 1; + int y = 1; + int z = 1; + int k; + + for (int i = 1; i <= 3; i++) { + x = x * i; + y = x; + z = y + (y - x) + 2; + __goblint_check(x == y); // SUCCESS + __goblint_check(z == y + 2); // SUCCESS + } + + return 0; +} diff --git a/tests/regression/88-lin2vareq_p/11-overflow_ignored.c b/tests/regression/88-lin2vareq_p/11-overflow_ignored.c new file mode 100644 index 0000000000..4e14c8aed2 --- /dev/null +++ b/tests/regression/88-lin2vareq_p/11-overflow_ignored.c @@ -0,0 +1,27 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq_p --set sem.int.signed_overflow assume_none + +#include +#include + +int main() { + int x; + int k; + int y; + + if (k > INT_MAX - 8) { + printf("Potential overflow detected.\n"); + return -1; + } + + x = k + 1; + __goblint_check(x == k + 1); // SUCCESS + + for (int i = 0; i < 7; i++) { + x++; + k++; + } + + __goblint_check(x == k + 1); // SUCCESS + + return 0; +} diff --git a/tests/regression/88-lin2vareq_p/12-bounds_guards_ov.c b/tests/regression/88-lin2vareq_p/12-bounds_guards_ov.c new file mode 100644 index 0000000000..350b8a23ce --- /dev/null +++ b/tests/regression/88-lin2vareq_p/12-bounds_guards_ov.c @@ -0,0 +1,19 @@ +//SKIP PARAM: --set ana.activated[+] lin2vareq_p +// same test as 63-affeq/10-bounds_guards.ov.c + +int main() { + int x, y; + int p = 0; + + if (x - 2 == __INT32_MAX__) { + __goblint_check(x == __INT32_MAX__ + 2); //UNKNOWN! + p = 1; + } + + __goblint_check(p == 0); //UNKNOWN! + + if (x + y == __INT32_MAX__) { + __goblint_check(1); + } + +} diff --git a/tests/regression/88-lin2vareq_p/13-meet-tcons.c b/tests/regression/88-lin2vareq_p/13-meet-tcons.c new file mode 100644 index 0000000000..b612acbfbd --- /dev/null +++ b/tests/regression/88-lin2vareq_p/13-meet-tcons.c @@ -0,0 +1,15 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq_p --set sem.int.signed_overflow assume_none + + +int main(void) { + int x, y, z; + + if (x == 0) { + __goblint_check(x == 0); // SUCCESS + } else if (y - x == 3) { + __goblint_check(y == x + 0); // FAILURE + __goblint_check(y - x == 3); // SUCCESS + } + + return 0; +} diff --git a/tests/regression/88-lin2vareq_p/14-function-call.c b/tests/regression/88-lin2vareq_p/14-function-call.c new file mode 100644 index 0000000000..ec4867875b --- /dev/null +++ b/tests/regression/88-lin2vareq_p/14-function-call.c @@ -0,0 +1,19 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq_p --set sem.int.signed_overflow assume_none + + +int myfunction(int x, int y){ + if (x == 0) { + __goblint_check(x == 0); // SUCCESS + } else if (y - x == 3) { + __goblint_check(y == x + 0); // FAILURE + __goblint_check(y - x == 3); // SUCCESS + } + + return 5; +} + +int main(void) { + int x, y, z; + z = myfunction(x,y); + return 0; +} diff --git a/tests/regression/88-lin2vareq_p/15-join_all_cases.c b/tests/regression/88-lin2vareq_p/15-join_all_cases.c new file mode 100644 index 0000000000..b6a05e3e93 --- /dev/null +++ b/tests/regression/88-lin2vareq_p/15-join_all_cases.c @@ -0,0 +1,31 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq_p --set ana.relation.privatization top --set sem.int.signed_overflow assume_none + +void main(void) { + int x1, x2, x3, x4, x5, x6, x7, x8, x9; + int t; + if (x6 < 300 && x6 > -300) { + if (t) { + x2 = 2; + x1 = 3; + x3 = 4; + x4 = 5; + x5 = x6 + 6; + x7 = x6 + 3; + x8 = x6 - 55; + } else { + x1 = 3; + x2 = 3; + x3 = 4; + x4 = 5; + x5 = x6 + 11; + x7 = x6 + 8; + x8 = x6 - 50; + } + __goblint_check(x1 == 3); + __goblint_check(x2 == 2); // UNKNOWN! + __goblint_check(x3 == 4); + __goblint_check(x4 == 5); + __goblint_check(x7 == x5 - 3); + __goblint_check(x8 == x7 - 58); + } +} diff --git a/tests/regression/88-lin2vareq_p/16-sum-of-two-vars.c b/tests/regression/88-lin2vareq_p/16-sum-of-two-vars.c new file mode 100644 index 0000000000..13f25ca581 --- /dev/null +++ b/tests/regression/88-lin2vareq_p/16-sum-of-two-vars.c @@ -0,0 +1,24 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq_p --set sem.int.signed_overflow assume_none + + +#include + +int main() { + int x, y, z, w, k; + + z = y; + x = y; + w = y; + + __goblint_check(z == 2 * x - y); // SUCCESS + + k = z + w - x + 5; + + __goblint_check(k == y + 5); //SUCCESS + + y = 3; + __goblint_check(k == y + 5); // UNKNOWN! + + + return 0; +} diff --git a/tests/regression/88-lin2vareq_p/17-svcomp-signextension.c b/tests/regression/88-lin2vareq_p/17-svcomp-signextension.c new file mode 100644 index 0000000000..f6b3f6103e --- /dev/null +++ b/tests/regression/88-lin2vareq_p/17-svcomp-signextension.c @@ -0,0 +1,28 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq_p --set sem.int.signed_overflow assume_none +// This was problematic earlier where we were unsound with lin2vareq +// Thus worth having even if it can be answered by base alone + +#include +int main() { + + unsigned short int allbits = -1; + short int signedallbits = allbits; + int unsignedtosigned = allbits; + unsigned int unsignedtounsigned = allbits; + int signedtosigned = signedallbits; + unsigned int signedtounsigned = signedallbits; + + /* + printf ("unsignedtosigned: %d\n", unsignedtosigned); + printf ("unsignedtounsigned: %u\n", unsignedtounsigned); + printf ("signedtosigned: %d\n", signedtosigned); + printf ("signedtounsigned: %u\n", signedtounsigned); + */ + + if (signedtounsigned == 4294967295) { + __goblint_check(1); // reachable + return (-1); + } +__goblint_check(0); // NOWARN (unreachable) + return (0); +} diff --git a/tests/regression/88-lin2vareq_p/18-forget_var.c b/tests/regression/88-lin2vareq_p/18-forget_var.c new file mode 100644 index 0000000000..6f18ac6b5d --- /dev/null +++ b/tests/regression/88-lin2vareq_p/18-forget_var.c @@ -0,0 +1,16 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq_p --set sem.int.signed_overflow assume_none +#include + +int main() { + int x, y, z; + + z = x; + + __goblint_check(z == x); // SUCCESS + + x = y * y; + + __goblint_check(x == z); // UNKNOWN! + + return 0; +} \ No newline at end of file diff --git a/tests/regression/88-lin2vareq_p/19-cast-to-short.c b/tests/regression/88-lin2vareq_p/19-cast-to-short.c new file mode 100644 index 0000000000..65601943f0 --- /dev/null +++ b/tests/regression/88-lin2vareq_p/19-cast-to-short.c @@ -0,0 +1,29 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq_p --set sem.int.signed_overflow assume_none +// This was problematic earlier where we were unsound with lin2vareq +// Thus worth having even if it can be answered by base alone + +#include +int main() { + + unsigned int allbits = -1; + int signedallbits = allbits; + short unsignedtosigned = allbits; + unsigned short unsignedtounsigned = allbits; + +// printf("allbits: %u\n", allbits); +// printf("signedallbits: %d\n", signedallbits); +// printf("unsignedtosigned: %hd\n", unsignedtosigned); +// printf("unsignedtounsigned: %hu\n", unsignedtounsigned); + + if (unsignedtounsigned == 4294967295) { + __goblint_check(0); // NOWARN (unreachable) + return (-1); + } + if (allbits == 4294967295 && signedallbits == -1 && unsignedtosigned == -1 && + unsignedtounsigned == 65535) { + __goblint_check(1); // reachable + return (-1); + } + __goblint_check(0); // NOWARN (unreachable) + return (0); +} diff --git a/tests/regression/88-lin2vareq_p/20-function_call2.c b/tests/regression/88-lin2vareq_p/20-function_call2.c new file mode 100644 index 0000000000..653051dbe4 --- /dev/null +++ b/tests/regression/88-lin2vareq_p/20-function_call2.c @@ -0,0 +1,21 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq_p --set sem.int.signed_overflow assume_none + +#include + +int check_equal(int x, int y, int z) { + __goblint_check(x == y); + __goblint_check(z == y); + __goblint_check(x == z); + return 8; +} + +int main(void) { + int x, y, z; + + y = x; + z = y; + + check_equal(x, y, z); + + return 0; +} diff --git a/tests/regression/88-lin2vareq_p/21-global-variables.c b/tests/regression/88-lin2vareq_p/21-global-variables.c new file mode 100644 index 0000000000..daadd96f29 --- /dev/null +++ b/tests/regression/88-lin2vareq_p/21-global-variables.c @@ -0,0 +1,21 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq_p --set sem.int.signed_overflow assume_none +#include +#include + +int x; +int y; + +void setY() { y = x + 3; } + +int main() { + int k; + x = k * k; + + if (x < INT_MAX - 3) { + setY(); + + __goblint_check(y == x + 3); // SUCCESS + } + + return 0; +} diff --git a/tests/regression/88-lin2vareq_p/22-cast-to-short2.c b/tests/regression/88-lin2vareq_p/22-cast-to-short2.c new file mode 100644 index 0000000000..79081e073a --- /dev/null +++ b/tests/regression/88-lin2vareq_p/22-cast-to-short2.c @@ -0,0 +1,29 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq_p --set sem.int.signed_overflow assume_none +// This was problematic earlier where both branches were dead with lin2vareq +// Thus worth having even if it can be answered by base alone + +#include +int main() { + + unsigned int allbits = -255 - 25; // choose a value which is not representable in short + int signedallbits = allbits; + short unsignedtosigned = allbits; + unsigned short unsignedtounsigned = allbits; + + printf("allbits: %u\n", allbits); + printf("signedallbits: %d\n", signedallbits); + printf("unsignedtosigned: %hd\n", unsignedtosigned); + printf("unsignedtounsigned: %hu\n", unsignedtounsigned); + + if (unsignedtounsigned == 4294967295) { + __goblint_check(0); // NOWARN (unreachable) + return (-1); + } + if (allbits == 4294967295 && signedallbits == -1 && unsignedtosigned == -1 && + unsignedtounsigned == 65535) { + __goblint_check(0); // NOWARN (unreachable) + return (-1); + } + + return (0); +} diff --git a/tests/regression/88-lin2vareq_p/23-function-return-value.c b/tests/regression/88-lin2vareq_p/23-function-return-value.c new file mode 100644 index 0000000000..60f070aff8 --- /dev/null +++ b/tests/regression/88-lin2vareq_p/23-function-return-value.c @@ -0,0 +1,18 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq_p --set sem.int.signed_overflow assume_none + +#include + +int k; + +int x_plus_three(int x) { + return x + 3; +} + +int main(void) { + int y, z; + z = x_plus_three(k); + + __goblint_check(z == k + 3); + + return 0; +} diff --git a/tests/regression/88-lin2vareq_p/24-narrowing-on-steroids.c b/tests/regression/88-lin2vareq_p/24-narrowing-on-steroids.c new file mode 100644 index 0000000000..f7592898a3 --- /dev/null +++ b/tests/regression/88-lin2vareq_p/24-narrowing-on-steroids.c @@ -0,0 +1,29 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq_p --enable ana.int.interval --set solver slr3tp +#include + +int main() { + short a; + a = a % 10; + int b; + int c; + b = a + 1; + c = a + 2; + int x, g; + + for(x=0; x < 50; x++){ + g = 1; + } + b = a + x; + + // x = [50, 50] after narrow + if(b - a > 50){ // live after widen, but dead after narrow + // node after Pos(x>50) is marked dead at the end + // but the loop is not with x = [51,2147483647] + for(int i=0; i<=0 && i > -1000; i--){ + b = 8; + } + assert(1); // NOWARN (unreachable) + } + __goblint_check(b == c + 48); + return 0; +} diff --git a/tests/regression/88-lin2vareq_p/25-different_types.c b/tests/regression/88-lin2vareq_p/25-different_types.c new file mode 100644 index 0000000000..bfecec61f4 --- /dev/null +++ b/tests/regression/88-lin2vareq_p/25-different_types.c @@ -0,0 +1,31 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq_p +#include + +int x = 42; +long y; +short z; + +int main() { + + y = (long)x; + z = (short)x; + + int a = (int)y; + short b = (short)y; + + int c = (int)z; + long d = (long)z; + + unsigned int u1 = (unsigned int)x; + unsigned long u2 = (unsigned long)y; + unsigned short u3 = (unsigned short)z; + + __goblint_check(x == a); + __goblint_check(x == c); + __goblint_check(y == d); + __goblint_check(x == (int)u1); + __goblint_check(y == (long)u2); + __goblint_check(z == (short)u3); + + return 0; +} diff --git a/tests/regression/88-lin2vareq_p/26-termination-overflow.c b/tests/regression/88-lin2vareq_p/26-termination-overflow.c new file mode 100644 index 0000000000..a1103c9be7 --- /dev/null +++ b/tests/regression/88-lin2vareq_p/26-termination-overflow.c @@ -0,0 +1,13 @@ +// SKIP TERM PARAM: --set "ana.activated[+]" lin2vareq_p + +#include + +int main() { + int i = 2147483647; + i++; + while (i <= 10) { + printf("%d\n", i); + } + + return 0; +} diff --git a/tests/regression/88-lin2vareq_p/27-overflow-unknown.c b/tests/regression/88-lin2vareq_p/27-overflow-unknown.c new file mode 100644 index 0000000000..475be3746c --- /dev/null +++ b/tests/regression/88-lin2vareq_p/27-overflow-unknown.c @@ -0,0 +1,19 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq_p +#include +#include + +int main(void) { + int x = 10; + + if (x + 2147483647 == 2147483657) { + return 0; + } + + __goblint_check(1); + + // Overflow + int c = 2147483647; + c = c + 1; + + __goblint_check(c < 2147483647); // UNKNOWN! +} diff --git a/tests/regression/88-lin2vareq_p/28-overflow-on-steroids.c b/tests/regression/88-lin2vareq_p/28-overflow-on-steroids.c new file mode 100644 index 0000000000..ee99b27240 --- /dev/null +++ b/tests/regression/88-lin2vareq_p/28-overflow-on-steroids.c @@ -0,0 +1,43 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq_p --enable ana.int.interval +#include + +int main(void) { + int b; + int a; + int c; // c is an unknown value + a = a % 8; // a is in the interval [-7, 7] + + b = c; // no overflow + __goblint_check(b == c);// SUCCESS + + b = c * 1; // no overflow + __goblint_check(b == c);// SUCCESS + + b = c ? c : c; // no overflow + __goblint_check(b == c);// SUCCESS + + b = a + 2; // no overflow + __goblint_check(b == a + 2);// SUCCESS + + b = c + 2; // might overflow + __goblint_check(b == c + 2);// UNKNOWN! + + b = a - 2; // no overflow + __goblint_check(b == a - 2);// SUCCESS + + b = c - 2; // might overflow + __goblint_check(b == c - 2);// UNKNOWN! + + b = a * 2 - a * 1; // no overflow + __goblint_check(b == a);// SUCCESS + + b = c * 2 - c * 1; // might overflow + __goblint_check(b == c); // UNKNOWN! + + b = (-a) + a; // no overflow + __goblint_check(b == 0); // SUCCESS + + b = (-c) + c; // might overflow + __goblint_check(b == 0); // UNKNOWN! + +} diff --git a/tests/regression/88-lin2vareq_p/29-meet-tcons-on-steroids.c b/tests/regression/88-lin2vareq_p/29-meet-tcons-on-steroids.c new file mode 100644 index 0000000000..ccdb955fb6 --- /dev/null +++ b/tests/regression/88-lin2vareq_p/29-meet-tcons-on-steroids.c @@ -0,0 +1,19 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq_p --enable ana.int.interval +#include + +int main(void) { + short b; + short a; + int c = a; + int d = b; + int cc = c + 20; + int dd = d - 30; + a = 3 * 1543; + if (a*(c - cc) == a*(d -dd - 50)){ + __goblint_check(1);// (reachable) + return 0; + }else{ + __goblint_check(0);// NOWARN (unreachable) + return -1; + } +} diff --git a/tests/regression/88-lin2vareq_p/30-cast-non-int.c b/tests/regression/88-lin2vareq_p/30-cast-non-int.c new file mode 100644 index 0000000000..6657d86ff1 --- /dev/null +++ b/tests/regression/88-lin2vareq_p/30-cast-non-int.c @@ -0,0 +1,11 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq_p --set sem.int.signed_overflow assume_none +#include +//#include +int main(void) { + float b = 2.5; + float a = 1.5; + int c = (int) a; + int d = (int) b; + //printf("c: %d\nd: %d\n", c, d); + __goblint_check(d -c -1 == 0); // UNKNOWN +} diff --git a/tests/regression/88-lin2vareq_p/31-careful.c b/tests/regression/88-lin2vareq_p/31-careful.c new file mode 100644 index 0000000000..ff5dc4cc8c --- /dev/null +++ b/tests/regression/88-lin2vareq_p/31-careful.c @@ -0,0 +1,23 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq_p --enable ana.int.interval +#include +#include + +int main(void) { + int top; + unsigned int i; + unsigned int j; + + if(top) { + i = 3; + j = i + UINT_MAX; + } else { + i = 2; + j = i + UINT_MAX; + } + + + // Both hold in the concrete + // First is SUCCESS here and not for lin2vareq because the interval domain is queried when assigning (but not yet in the condition) + __goblint_check(j == i-1); //SUCCESS + __goblint_check(j == i + UINT_MAX); //UNKNOWN +} diff --git a/tests/regression/88-lin2vareq_p/32-divbzero-in-overflow.c b/tests/regression/88-lin2vareq_p/32-divbzero-in-overflow.c new file mode 100644 index 0000000000..5d13057099 --- /dev/null +++ b/tests/regression/88-lin2vareq_p/32-divbzero-in-overflow.c @@ -0,0 +1,16 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq_p + +/** + * This test shows an instance where MaySignedOverflow raised + * an uncaught division by zero in the treatment of main's sole statement + * + * Fixed in #1419 + */ +int a; +char b; +int main() +{ + 0 == a && 1 / b; + __goblint_check(1); // (reachable) + return 0; +} diff --git a/tests/regression/88-lin2vareq_p/33-dimarray.c b/tests/regression/88-lin2vareq_p/33-dimarray.c new file mode 100644 index 0000000000..8b48d2f3b6 --- /dev/null +++ b/tests/regression/88-lin2vareq_p/33-dimarray.c @@ -0,0 +1,13 @@ +//SKIP PARAM: --set ana.activated[+] lin2vareq_p --set sem.int.signed_overflow assume_none +// special input triggering add_dimarray of [0,0] at line 10; visible via --trace modify_dims +// both occurances of variables need to be bumped/shifted by 2 indices +// in our case, d = c still needs to hold +#include +int a; +b() {} +void main() { + int c; + int d = c; + b(); + __goblint_check(d == c); //SUCCESS +} diff --git a/tests/regression/88-lin2vareq_p/34-coefficient-features.c b/tests/regression/88-lin2vareq_p/34-coefficient-features.c new file mode 100644 index 0000000000..1f1fe82d4f --- /dev/null +++ b/tests/regression/88-lin2vareq_p/34-coefficient-features.c @@ -0,0 +1,62 @@ +//SKIP PARAM: --set ana.activated[+] lin2vareq_p --set sem.int.signed_overflow assume_none +// this test checks basic coefficient handing in main and join capabilities in loop + +#include + +void loop() { + int random; + int i = 0; + int x = 0; + int y = 0; + + x=x+4; + y=y+8; + i=i+1; + + if (random) { + x=x+4; + y=y+8; + i=i+1; + } + + __goblint_check(x == 4*i); //SUCCESS + + x=0; + y=0; + + for(i = 1; i < 100; i++) { + x=x+4; + y=y+8; + + __goblint_check(y == 2*x); //SUCCESS + __goblint_check(x == 4*i); //SUCCESS + } +} + +void main() { + int a; + int b; + int c; + int unknown; + a = 4; + + b = 4*c; + + __goblint_check(b == 4*c); //SUCCESS + + b = a*c; + + __goblint_check(b == 4*c); //SUCCESS + + if (7*b == 20*unknown + a){ + + __goblint_check(7*b == 20*unknown + a); //SUCCESS + } + + b = unknown ? a*c : 4*c; + + __goblint_check(b == 4*c); //SUCCESS + + loop(); + +} \ No newline at end of file diff --git a/tests/regression/88-lin2vareq_p/36-relations-overflow.c b/tests/regression/88-lin2vareq_p/36-relations-overflow.c new file mode 100644 index 0000000000..91cf369ebc --- /dev/null +++ b/tests/regression/88-lin2vareq_p/36-relations-overflow.c @@ -0,0 +1,24 @@ +//SKIP PARAM: --enable ana.int.interval --set sem.int.signed_overflow assume_none --set ana.activated[+] lin2vareq_p + +#include + +int nondet() { + int x; + return x; +} +int SIZE = 1; +int rand; + +int main() { + unsigned int n=2,i=8; + n = i%(SIZE+2); //NOWARN + + rand=nondet(); + + if (rand>5 && rand<10) { + n= i%(rand+2); //NOWARN + } + + return 0; +} + diff --git a/tests/regression/88-lin2vareq_p/37-intervals_propagation.c b/tests/regression/88-lin2vareq_p/37-intervals_propagation.c new file mode 100644 index 0000000000..607ce634a4 --- /dev/null +++ b/tests/regression/88-lin2vareq_p/37-intervals_propagation.c @@ -0,0 +1,12 @@ +//SKIP PARAM: --set ana.activated[+] lin2vareq_p --set sem.int.signed_overflow assume_none + +int main() { + int x, y, z; + x = 3*y + 1; // a + z = 5*x + 7; // b + if (x>0) { + __goblint_check( x > 0 ); //SUCCESS + __goblint_check( y > -1 ); //SUCCESS + __goblint_check( z > 7 ); //SUCCESS + } +} \ No newline at end of file diff --git a/tests/regression/88-lin2vareq_p/38-simple_congruence.c b/tests/regression/88-lin2vareq_p/38-simple_congruence.c new file mode 100644 index 0000000000..5936b73d09 --- /dev/null +++ b/tests/regression/88-lin2vareq_p/38-simple_congruence.c @@ -0,0 +1,16 @@ +//SKIP PARAM: --set ana.activated[+] lin2vareq_p --set sem.int.signed_overflow assume_none + +int main() { + int x, y, z; + x = 3 * y + 1; // a + z = 5 * x + 7; // b + if (y < 14) + { + __goblint_check( x <= 42); //SUCCESS + __goblint_check(y < 14); //SUCCESS + __goblint_check(z != 500); //SUCCESS + __goblint_check(z != 14); //SUCCESS // Because of eqution for z + __goblint_check(z != 17); //SUCCESS // Because of combination of equation for z and x + + } +} \ No newline at end of file diff --git a/tests/regression/88-lin2vareq_p/39-congruence_from_equation.c b/tests/regression/88-lin2vareq_p/39-congruence_from_equation.c new file mode 100644 index 0000000000..2a1e2e4230 --- /dev/null +++ b/tests/regression/88-lin2vareq_p/39-congruence_from_equation.c @@ -0,0 +1,10 @@ +//SKIP PARAM: --set ana.activated[+] lin2vareq_p --set sem.int.signed_overflow assume_none + +int main() { + int x, y, z; + if (4 * x == 3 * y + 1) { + __goblint_check( y % 4 == 1); //SUCCESS + __goblint_check( x % 3 == 1); //SUCCESS + + } +} \ No newline at end of file diff --git a/tests/regression/88-lin2vareq_p/40-join-splitting-group.c b/tests/regression/88-lin2vareq_p/40-join-splitting-group.c new file mode 100644 index 0000000000..35bf3f40ad --- /dev/null +++ b/tests/regression/88-lin2vareq_p/40-join-splitting-group.c @@ -0,0 +1,41 @@ +//SKIP PARAM: --set ana.activated[+] lin2vareq_p --set sem.int.signed_overflow assume_none + +int main() { + //Test if inequality information is conserved correctly when a equality grouping is split + //Tested with x and y to be resitant against changes to the indexes of variables + { + int x, y, z; + + if (z) { + y = 2 * x; + if (y < z) + ; + else + return 0; + // y = 2x, 2x <= z - 1 + } else { + x = 0; + y = 1; + z = 10; + } + // 2x <= z - 1 would no longer prove what we want, as the relation y = 2x no longer holds + __goblint_check( y < z); //SUCCESS + } + { + int x, y, z; + + if (z) { + y = 2 * x; + if (x < z) + ; + else + return 0; + } else { + x = 0; + y = 1; + z = 10; + } + + __goblint_check( x < z); //SUCCESS + } +} \ No newline at end of file diff --git a/tests/regression/88-lin2vareq_p/dune b/tests/regression/88-lin2vareq_p/dune new file mode 100644 index 0000000000..f8e68307a1 --- /dev/null +++ b/tests/regression/88-lin2vareq_p/dune @@ -0,0 +1,10 @@ +(rule + (aliases runtest runaprontest) + (enabled_if %{lib-available:apron}) + (deps + (package goblint) + ../../../goblint ; update_suite calls local goblint + (:update_suite ../../../scripts/update_suite.rb) + (glob_files ??-*.c)) + (locks /update_suite) + (action (chdir ../../.. (run %{update_suite} group lin2vareq_p -q)))) \ No newline at end of file