diff --git a/conf/svcomp2var.json b/conf/svcomp2var.json new file mode 100644 index 0000000000..7df6a3579c --- /dev/null +++ b/conf/svcomp2var.json @@ -0,0 +1,146 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": false, + "interval": true + }, + "float": { + "interval": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins" , + "lin2vareq" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag" + ], + "context": { + "widen": false + }, + "malloc": { + "wrappers": [ + "kmalloc", + "__kmalloc", + "usb_alloc_urb", + "__builtin_alloca", + "kzalloc", + + "ldv_malloc", + + "kzalloc_node", + "ldv_zalloc", + "kmalloc_array", + "kcalloc", + + "ldv_xmalloc", + "ldv_xzalloc", + "ldv_calloc", + "ldv_kzalloc" + ] + }, + "base": { + "arrays": { + "domain": "partitioned" + } + }, + "race": { + "free": false, + "call": false + }, + "autotune": { + "enabled": true, + "activated": [ + "singleThreaded", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "termination", + "tmpSpecialAnalysis" + ] + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "graphml": { + "enabled": true, + "id": "enumerate", + "unknown": false + }, + "yaml": { + "enabled": true, + "format-version": "2.0", + "entry-types": [ + "invariant_set" + ], + "invariant-types": [ + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": false, + "other": false, + "accessed": false, + "exact": true, + "exclude-vars": [ + "tmp\\(___[0-9]+\\)?", + "cond", + "RETURN", + "__\\(cil_\\)?tmp_?[0-9]*\\(_[0-9]+\\)?", + ".*____CPAchecker_TMP_[0-9]+", + "__VERIFIER_assert__cond", + "__ksymtab_.*", + "\\(ldv_state_variable\\|ldv_timer_state\\|ldv_timer_list\\|ldv_irq_\\(line_\\|data_\\)?[0-9]+\\|ldv_retval\\)_[0-9]+" + ] + } + }, + "pre": { + "enabled": false + } +} diff --git a/src/analyses/apron/linearTwoVarEqualityAnalysis.apron.ml b/src/analyses/apron/linearTwoVarEqualityAnalysis.apron.ml new file mode 100644 index 0000000000..8b38679a09 --- /dev/null +++ b/src/analyses/apron/linearTwoVarEqualityAnalysis.apron.ml @@ -0,0 +1,31 @@ +(** {{!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 + +let spec_module: (module MCPSpec) Lazy.t = + lazy ( + let module AD = LinearTwoVarEqualityDomain.D2 + in + let module Priv = (val RelationPriv.get_priv ()) in + let module Spec = + struct + include SpecFunctor (Priv) (AD) (RelationPrecCompareUtil.DummyUtil) + let name () = "lin2vareq" + 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/linearTwoVarEqualityAnalysis.no-apron.ml b/src/analyses/apron/linearTwoVarEqualityAnalysis.no-apron.ml new file mode 100644 index 0000000000..0a444baa9b --- /dev/null +++ b/src/analyses/apron/linearTwoVarEqualityAnalysis.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 b74b6d2fae..0cb1cbb6c4 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -177,7 +177,7 @@ struct let no_overflow (ask: Queries.ask) exp = match Cilfacade.get_ikind_exp exp with - | exception Invalid_argument _ -> false (* TODO: why this? *) + | exception Invalid_argument _ -> false (* is thrown by get_ikind_exp when the type of the expression is not an integer type *) | exception Cilfacade.TypeOfError _ -> false | ik -> if IntDomain.should_wrap ik then @@ -185,7 +185,7 @@ struct else if IntDomain.should_ignore_overflow ik then true else - not (Queries.ID.is_top_of ik (ask.f (EvalInt exp))) + not (ask.f (MaySignedOverflow exp)) let no_overflow ctx exp = lazy ( let res = no_overflow ctx exp in @@ -193,7 +193,6 @@ struct res ) - let assert_type_bounds ask rel x = assert (RD.Tracked.varinfo_tracked x); match Cilfacade.get_ikind x.vtype with @@ -202,8 +201,9 @@ struct (* TODO: don't go through CIL exp? *) let e1 = BinOp (Le, Lval (Cil.var x), (Cil.kintegerCilint ik type_max), intType) in let e2 = BinOp (Ge, Lval (Cil.var x), (Cil.kintegerCilint ik type_min), intType) in - let rel = RD.assert_inv rel e1 false (no_overflow ask e1) in (* TODO: how can be overflow when asserting type bounds? *) - let rel = RD.assert_inv rel e2 false (no_overflow ask e2) in + (* TODO: do not duplicate no_overflow defined via ask: https://github.com/goblint/analyzer/pull/1297#discussion_r1477281950 *) + let rel = RD.assert_inv ask rel e1 false (no_overflow ask e1) in (* TODO: how can be overflow when asserting type bounds? *) + let rel = RD.assert_inv ask rel e2 false (no_overflow ask e2) in rel | exception Invalid_argument _ -> rel @@ -243,7 +243,6 @@ struct inner e (* Basic transfer functions. *) - let assign ctx (lv:lval) e = let st = ctx.local in if !AnalysisState.global_initialization && e = MyCFG.unknown_exp then @@ -256,7 +255,7 @@ struct assign_from_globals_wrapper ask ctx.global st simplified_e (fun apr' e' -> if M.tracing then M.traceli "relation" "assign inner %a = %a (%a)\n" CilType.Varinfo.pretty v d_exp e' d_plainexp e'; if M.tracing then M.trace "relation" "st: %a\n" RD.pretty apr'; - let r = RD.assign_exp apr' (RV.local v) e' (no_overflow ask simplified_e) in + let r = RD.assign_exp ask apr' (RV.local v) e' (no_overflow ask simplified_e) in if M.tracing then M.traceu "relation" "-> %a\n" RD.pretty r; r ) @@ -271,7 +270,7 @@ struct let ask = Analyses.ask_of_ctx ctx in let res = assign_from_globals_wrapper ask ctx.global st e (fun rel' e' -> (* not an assign, but must remove g#in-s still *) - RD.assert_inv rel' e' (not b) (no_overflow ask e) + RD.assert_inv ask rel' e' (not b) (no_overflow ask e) ) in if RD.is_bot_env res then raise Deadcode; @@ -322,7 +321,7 @@ struct let ask = Analyses.ask_of_ctx ctx in List.fold_left (fun new_rel (var, e) -> assign_from_globals_wrapper ask ctx.global {st with rel = new_rel} e (fun rel' e' -> - RD.assign_exp rel' var e' (no_overflow ask e) + RD.assign_exp ask rel' var e' (no_overflow ask e) ) ) new_rel arg_assigns in @@ -365,7 +364,7 @@ struct match e with | Some e -> assign_from_globals_wrapper ask ctx.global {st with rel = rel'} e (fun rel' e' -> - RD.assign_exp rel' RV.return e' (no_overflow ask e) + RD.assign_exp ask rel' RV.return e' (no_overflow ask e) ) | None -> rel' (* leaves V.return unconstrained *) @@ -413,7 +412,9 @@ struct let new_fun_rel = List.fold_left (fun new_fun_rel (var, e) -> assign_from_globals_wrapper ask ctx.global {st with rel = new_fun_rel} e (fun rel' e' -> (* not an assign, but still works? *) - RD.substitute_exp rel' var e' (no_overflow ask e) + (* substitute is the backwards semantics of assignment *) + (* https://antoinemine.github.io/Apron/doc/papers/expose_CEA_2007.pdf *) + RD.substitute_exp ask rel' var e' (no_overflow ask e) ) ) new_fun_rel arg_substitutes in @@ -506,7 +507,7 @@ struct let ask = Analyses.ask_of_ctx ctx in let res = assign_from_globals_wrapper ask ctx.global st e (fun apr' e' -> (* not an assign, but must remove g#in-s still *) - RD.assert_inv apr' e' false (no_overflow ask e) + RD.assert_inv ask apr' e' false (no_overflow ask e) ) in if RD.is_bot_env res then raise Deadcode; @@ -634,8 +635,6 @@ struct |> Enum.fold (fun acc x -> Invariant.(acc && of_exp x)) Invariant.none let query ctx (type a) (q: a Queries.t): a Queries.result = - let no_overflow ctx' exp' = - IntDomain.should_ignore_overflow (Cilfacade.get_ikind_exp exp') in (* TODO: separate no_overflow? *) let open Queries in let st = ctx.local in let eval_int e no_ov = @@ -643,13 +642,13 @@ struct read_from_globals_wrapper (Analyses.ask_of_ctx ctx) ctx.global st esimple - (fun rel' e' -> RD.eval_int rel' e' no_ov) + (fun rel' e' -> RD.eval_int (Analyses.ask_of_ctx ctx) rel' e' no_ov) in match q with | EvalInt e -> if M.tracing then M.traceli "evalint" "relation query %a (%a)\n" d_exp e d_plainexp e; if M.tracing then M.trace "evalint" "relation st: %a\n" D.pretty ctx.local; - let r = eval_int e (lazy(no_overflow ctx e)) in + let r = eval_int e (no_overflow (Analyses.ask_of_ctx ctx) e) in if M.tracing then M.traceu "evalint" "relation query %a -> %a\n" d_exp e ID.pretty r; r | Queries.IterSysVars (vq, vf) -> @@ -708,7 +707,29 @@ struct let vars = Basetype.CilExp.get_vars e |> List.unique ~eq:CilType.Varinfo.equal |> List.filter RD.Tracked.varinfo_tracked in let rel = RD.forget_vars rel (List.map RV.local vars) in (* havoc *) let rel = List.fold_left (assert_type_bounds ask) rel vars in (* add type bounds to avoid overflow in top state *) - let rel = RD.assert_inv rel e false (no_overflow ask e_orig) in (* assume *) + let rec dummyask = + (* assert_inv calls texpr1_expr_of_cil_exp, which simplifies the constraint based on the pre-state of the transition; + this does not reflect the state after RD.forget_vars rel .... has been performed; to prevent this aggressive + simplification, we restrict read_int queries to a local dummy ask, that only dispatches to rel instead of the + full state *) + let f (type a) (q : a Queries.t) : a = + let eval_int e no_ov = + let esimple = replace_deref_exps dummyask.f e in + read_from_globals_wrapper + (dummyask) + ctx.global { st with rel } esimple + (fun rel' e' -> RD.eval_int (dummyask) rel' e' no_ov) + in + match q with + | EvalInt e -> + if M.tracing then M.traceli "relation" "evalint query %a (%a), ctx %a\n" d_exp e d_plainexp e D.pretty ctx.local; + let r = eval_int e (no_overflow (dummyask) e) in + if M.tracing then M.trace "relation" "evalint response %a -> %a\n" d_exp e ValueDomainQueries.ID.pretty r; + r + |_ -> Queries.Result.top q + in + ({ f } : Queries.ask) in + let rel = RD.assert_inv dummyask rel e false (no_overflow ask e_orig) in (* assume *) let rel = RD.keep_vars rel (List.map RV.local vars) in (* restrict *) (* TODO: parallel write_global? *) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 9aca9e2079..43e37c346c 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1105,7 +1105,7 @@ struct | Bot -> Queries.ID.top () (* out-of-scope variables cause bot, but query result should then be unknown *) | Top -> Queries.ID.top () (* some float computations cause top (57-float/01-base), but query result should then be unknown *) | v -> M.debug ~category:Analyzer "Base EvalInt %a query answering bot instead of %a" d_exp e VD.pretty v; Queries.ID.bot () - | exception (IntDomain.ArithmeticOnIntegerBot _) when not !AnalysisState.should_warn -> Queries.ID.top () (* for some privatizations, values can intermediately be bot because side-effects have not happened yet *) + | exception (IntDomain.ArithmeticOnIntegerBot _) when not !AnalysisState.should_warn -> Queries.ID.bot () in if M.tracing then M.traceu "evalint" "base query_evalint %a -> %a\n" d_exp e Queries.ID.pretty r; r @@ -1250,6 +1250,103 @@ struct else Invariant.none + (** + This query returns false if the expression [exp] will definitely not result in an overflow. + + Each subexpression is analyzed to see if an overflow happened. + For each operator in the expression, we use the query EvalInt to approximate the bounds of each + operand and we compute if in the worst case there could be an overflow. + + For now we return true if the expression contains a shift left. + *) + (* TODO: deduplicate https://github.com/goblint/analyzer/pull/1297#discussion_r1477804502 *) + let rec exp_may_signed_overflow ctx exp = + let res = match Cilfacade.get_ikind_exp exp with + | exception _ -> BoolDomain.MayBool.top () + | ik -> + let checkBinop e1 e2 binop = + match ctx.ask (EvalInt e1), ctx.ask (EvalInt e2) with + | `Bot, _ -> false + | _, `Bot -> false + | `Lifted i1, `Lifted i2 -> + ( let (min_ik, max_ik) = IntDomain.Size.range ik in + let (min_i1, max_i1) = (IntDomain.IntDomTuple.minimal i1, IntDomain.IntDomTuple.maximal i1) in + let (min_i2, max_i2) = (IntDomain.IntDomTuple.minimal i2, IntDomain.IntDomTuple.maximal i2) in + let possible_combinations = [binop min_i1 min_i2; binop min_i1 max_i2; binop max_i1 min_i2; binop max_i1 max_i2] in + let min_exp = List.min possible_combinations in + let max_exp = List.max possible_combinations in + match min_exp, max_exp with + | Some min, Some max when min >= min_ik && max <= max_ik -> false + | _ -> true) + | _ -> true in + let checkPredicate e pred = + match ctx.ask (EvalInt e) with + | `Bot -> false + | `Lifted i -> + (let (min_ik, _) = IntDomain.Size.range ik in + let (min_i, max_i) = (IntDomain.IntDomTuple.minimal i, IntDomain.IntDomTuple.maximal i) in + match min_i with + | Some min when pred min min_ik -> false + | _ -> true) + | _ -> true + in + match exp with + | Const _ + | SizeOf _ + | SizeOfStr _ + | AlignOf _ + | AddrOfLabel _ -> false + | Real e + | Imag e + | SizeOfE e + | AlignOfE e + | CastE (_, e) -> exp_may_signed_overflow ctx e + | UnOp (unop, e, _) -> + (* check if the current operation causes a signed overflow *) + begin match unop with + | Neg -> (* an overflow happens when the lower bound of the interval is less than MIN_INT *) + Cil.isSigned ik && checkPredicate e (Z.gt) + (* operations that do not result in overflow in C: *) + | BNot|LNot -> false + end + (* look for overflow in subexpression *) + || exp_may_signed_overflow ctx e + | BinOp (binop, e1, e2, _) -> + (* check if the current operation causes a signed overflow *) + (Cil.isSigned ik && begin match binop with + | PlusA|PlusPI|IndexPI -> checkBinop e1 e2 (GobOption.map2 Z.(+)) + | MinusA|MinusPI|MinusPP -> checkBinop e1 e2 (GobOption.map2 Z.(-)) + | Mult -> checkBinop e1 e2 (GobOption.map2 Z.mul) + | Div -> checkBinop e1 e2 (GobOption.map2 Z.div) + | Mod -> (* an overflow happens when the second operand is negative *) + checkPredicate e2 (fun interval_bound _ -> Z.gt interval_bound Z.zero) + (* operations that do not result in overflow in C: *) + | Eq|Shiftrt|BAnd|BOr|BXor|Lt|Gt|Le|Ge|Ne|LAnd|LOr -> false + (* Shiftlt can cause overflow and also undefined behaviour in case the second operand is non-positive*) + | Shiftlt -> true end) + (* look for overflow in subexpression *) + || exp_may_signed_overflow ctx e1 || exp_may_signed_overflow ctx e2 + | Question (e1, e2, e3, _) -> + (* does not result in overflow in C *) + exp_may_signed_overflow ctx e1 || exp_may_signed_overflow ctx e2 || exp_may_signed_overflow ctx e3 + | Lval lval + | AddrOf lval + | StartOf lval -> lval_may_signed_overflow ctx lval + in + if M.tracing then M.trace "signed_overflow" "base exp_may_signed_overflow %a. Result = %b\n" d_plainexp exp res; res + and lval_may_signed_overflow ctx (lval : lval) = + let (host, offset) = lval in + let host_may_signed_overflow = function + | Var v -> false + | Mem e -> exp_may_signed_overflow ctx e + in + let rec offset_may_signed_overflow = function + | NoOffset -> false + | Index (e, o) -> exp_may_signed_overflow ctx e || offset_may_signed_overflow o + | Field (f, o) -> offset_may_signed_overflow o + in + host_may_signed_overflow host || offset_may_signed_overflow offset + let query ctx (type a) (q: a Q.t): a Q.result = match q with | Q.EvalFunvar e -> @@ -1415,6 +1512,9 @@ struct | Q.InvariantGlobal g -> let g: V.t = Obj.obj g in query_invariant_global ctx g + | Q.MaySignedOverflow e -> (let res = exp_may_signed_overflow ctx e in + if M.tracing then M.trace "signed_overflow" "base exp_may_signed_overflow %a. Result = %b\n" d_plainexp e res; res + ) | _ -> Q.Result.top q let update_variable variable typ value cpa = diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml index a3943651c0..5c14d4bf4b 100644 --- a/src/analyses/mCP.ml +++ b/src/analyses/mCP.ml @@ -272,7 +272,9 @@ struct } in (* meet results so that precision from all analyses is combined *) - Result.meet a @@ S.query ctx' q + let res = S.query ctx' q in + if M.tracing then M.trace "queryanswers" "analysis %s query %a -> answer %a\n" (S.name ()) Queries.Any.pretty anyq Result.pretty res; + Result.meet a @@ res in match q with | Queries.WarnGlobal g -> diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index 944515f4ec..f6d5f6ece2 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -13,129 +13,39 @@ module M = Messages open GobApron open VectorMatrix -module Mpqf = struct - include Mpqf - let compare = cmp - let zero = of_int 0 - let one = of_int 1 - let mone = of_int (-1) +module Mpqf = SharedFunctions.Mpqf - let get_den x = Z_mlgmpidl.z_of_mpzf @@ Mpqf.get_den x - - let get_num x = Z_mlgmpidl.z_of_mpzf @@ Mpqf.get_num x - let hash x = 31 * (Z.hash (get_den x)) + Z.hash (get_num x) -end - -(** It defines the type t of the affine equality domain (a struct 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 get_coeff_vec that parses an apron expression into a vector of coefficients if the apron expression has an affine form. *) -module VarManagement (Vec: AbstractVector) (Mx: AbstractMatrix)= +module AffineEqualityMatrix (Vec: AbstractVector) (Mx: AbstractMatrix) = struct - module Vector = Vec (Mpqf) - module Matrix = Mx(Mpqf) (Vec) - - type t = { - mutable d : Matrix.t option; - mutable env : Environment.t - } - [@@deriving eq, ord, hash] - - let empty_env = Environment.make [||] [||] - - let bot () = - {d = Some (Matrix.empty ()); env = empty_env} - - let bot_env = {d = None; env = empty_env} - - let is_bot_env t = t.d = None - - let copy t = {t with d = Option.map Matrix.copy t.d} - + include Mx(Mpqf) (Vec) let dim_add (ch: Apron.Dim.change) m = - Array.modifyi (fun i x -> x + i) ch.dim; (* could be written Array.modifyi (+) ch.dim; but that's too smart *) - Matrix.add_empty_columns m ch.dim + Array.modifyi (+) ch.dim; + add_empty_columns m ch.dim let dim_add ch m = timing_wrap "dim add" (dim_add ch) m - let dim_remove (ch: Apron.Dim.change) m del = - if Array.length ch.dim = 0 || Matrix.is_empty m then + + let dim_remove (ch: Apron.Dim.change) m ~del = + if Array.length ch.dim = 0 || is_empty m then m else ( - Array.modifyi (fun i x -> x + i) ch.dim; - let m' = if not del then let m = Matrix.copy m in Array.fold_left (fun y x -> Matrix.reduce_col_with y x; y) m ch.dim else m in - Matrix.remove_zero_rows @@ Matrix.del_cols m' ch.dim) - - let dim_remove ch m del = timing_wrap "dim remove" (dim_remove ch m) del - - let change_d t new_env add del = - if Environment.equal t.env new_env then - t - else - match t.d with - | None -> bot_env - | Some m -> - let dim_change = - if add then - Environment.dimchange t.env new_env - else - Environment.dimchange new_env t.env - in - {d = Some (if add then dim_add dim_change m else dim_remove dim_change m del); env = new_env} - - let change_d t new_env add del = timing_wrap "dimension change" (change_d t new_env add) del - - let vars x = Environment.ivars_only x.env - - let add_vars t vars = - let t = copy t in - let env' = Environment.add_vars t.env vars in - change_d t env' true false - - let add_vars t vars = timing_wrap "add_vars" (add_vars t) vars - - let drop_vars t vars del = - let t = copy t in - let env' = Environment.remove_vars t.env vars in - change_d t env' false del - - let drop_vars t vars = timing_wrap "drop_vars" (drop_vars t) vars - - let remove_vars t vars = drop_vars t vars false - - let remove_vars t vars = timing_wrap "remove_vars" (remove_vars t) vars - - let remove_vars_with t vars = - let t' = remove_vars t vars in - t.d <- t'.d; - t.env <- t'.env - - let remove_filter t f = - let env' = Environment.remove_filter t.env f in - change_d t env' false false - - let remove_filter t f = timing_wrap "remove_filter" (remove_filter t) f - - let remove_filter_with t f = - let t' = remove_filter t f in - t.d <- t'.d; - t.env <- t'.env - - let keep_filter t f = - let t = copy t in - let env' = Environment.keep_filter t.env f in - change_d t env' false false - - let keep_filter t f = timing_wrap "keep_filter" (keep_filter t) f + Array.modifyi (+) ch.dim; + let m' = if not del then let m = copy m in Array.fold_left (fun y x -> reduce_col_with y x; y) m ch.dim else m in + remove_zero_rows @@ del_cols m' ch.dim) - let keep_vars t vs = - let t = copy t in - let env' = Environment.keep_vars t.env vs in - change_d t env' false false - - let keep_vars t vs = timing_wrap "keep_vars" (keep_vars t) vs + let dim_remove ch m ~del = VectorMatrix.timing_wrap "dim remove" (fun del -> dim_remove ch m ~del:del) del +end +(** It defines the type t of the affine equality domain (a struct 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 get_coeff_vec that parses an apron expression into a vector of coefficients if the apron expression has an affine form. *) +module VarManagement (Vec: AbstractVector) (Mx: AbstractMatrix)= +struct + module Vector = Vec (Mpqf) + module Matrix = AffineEqualityMatrix (Vec) (Mx) - let mem_var t var = Environment.mem_var t.env var + let dim_add = Matrix.dim_add + include SharedFunctions.VarManagementOps(AffineEqualityMatrix (Vec) (Mx)) include ConvenienceOps(Mpqf) (** Get the constant from the vector if it is a constant *) @@ -239,7 +149,11 @@ struct module Bounds = ExpressionBounds (Vc) (Mx) module V = RelationDomain.V - module Convert = SharedFunctions.Convert (V) (Bounds) (struct let allow_global = true end) (SharedFunctions.Tracked) + module Arg = struct + let allow_global = true + end + module Convert = SharedFunctions.Convert (V) (Bounds) (Arg) (SharedFunctions.Tracked) + type var = V.t @@ -294,6 +208,8 @@ struct let pretty () (x:t) = text (show x) let printXml f x = BatPrintf.fprintf f "\n\n\nmatrix\n\n\n%s\n\nenv\n\n\n%s\n\n\n" (XmlUtil.escape (Format.asprintf "%s" (show x) )) (XmlUtil.escape (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (x.env))) + let eval_interval ask = Bounds.bound_texpr + let name () = "affeq" let to_yojson _ = failwith "ToDo Implement in future" @@ -313,11 +229,13 @@ struct let meet t1 t2 = let sup_env = Environment.lce t1.env t2.env in - let t1, t2 = change_d t1 sup_env true false, change_d t2 sup_env true false in + + let t1, t2 = change_d t1 sup_env ~add:true ~del:false, change_d t2 sup_env ~add:true ~del:false in if is_bot t1 || is_bot t2 then bot () else - (* TODO: Why can I be sure that m1 && m2 are all Some here? *) + (* TODO: Why can I be sure that m1 && m2 are all Some here? + Answer: because is_bot checks if t1.d is None and we checked is_bot before. *) let m1, m2 = Option.get t1.d, Option.get t2.d in if is_top_env t1 then {d = Some (dim_add (Environment.dimchange t2.env sup_env) m2); env = sup_env} @@ -502,16 +420,16 @@ struct let assign_texpr t var texp = timing_wrap "assign_texpr" (assign_texpr t var) texp - let assign_exp (t: VarManagement(Vc)(Mx).t) var exp (no_ov: bool Lazy.t) = + let assign_exp ask (t: VarManagement(Vc)(Mx).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 (* TODO: Do we need to do a constant folding here? It happens for texpr1_of_cil_exp *) - match Convert.texpr1_expr_of_cil_exp t t.env exp (Lazy.force no_ov) with + match Convert.texpr1_expr_of_cil_exp ask t t.env exp no_ov with | exp -> assign_texpr t var exp | exception Convert.Unsupported_CilExp _ -> if is_bot t then t else forget_vars t [var] - let assign_exp t var exp no_ov = - let res = assign_exp t var exp no_ov in + 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: %s \n exp: %a\n no_ov: %b -> \n %s\n" (show t) (Var.to_string var) d_exp exp (Lazy.force no_ov) (show res) ; res @@ -541,7 +459,7 @@ struct in let m_cp = Matrix.copy m in let switched_m = List.fold_left2 replace_col m_cp primed_vars assigned_vars in - let res = drop_vars {d = Some switched_m; env = multi_t.env} primed_vars true in + let res = drop_vars {d = Some switched_m; env = multi_t.env} primed_vars ~del:true in let x = Option.get res.d in if Matrix.normalize_with x then {d = Some x; env = res.env} @@ -574,86 +492,60 @@ struct if M.tracing then M.tracel "ops" "assign_var parallel'\n"; res - let substitute_exp t var exp no_ov = + 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 t var exp no_ov in + let res = assign_exp ask t var exp no_ov in forget_vars res [var] - let substitute_exp t var exp ov = - let res = substitute_exp t var exp ov in + 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: %s \n exp: %a \n -> \n %s\n" (show t) (Var.to_string var) d_exp exp (show res); res - let substitute_exp t var exp ov = timing_wrap "substitution" (substitute_exp t var exp) ov + let substitute_exp ask t var exp no_ov = timing_wrap "substitution" (substitute_exp ask t var exp) no_ov (** Assert a constraint expression. - Additionally, we now also refine after positive guards when overflows might occur and there is only one variable inside the expression and the expression is an equality constraint check (==). - We check after the refinement if the new value of the variable is outside its integer bounds and if that is the case, either revert to the old state or set it to bottom. *) + 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 *) - exception NotRefinable - - let meet_tcons_one_var_eq res expr = - let overflow_res res = if IntDomain.should_ignore_overflow (Cilfacade.get_ikind_exp expr) then res else raise NotRefinable in - match Convert.find_one_var expr with - | None -> overflow_res res - | Some v -> - let ik = Cilfacade.get_ikind v.vtype in - if not (Cil.isSigned ik) then - raise NotRefinable - else - match Bounds.bound_texpr res (Convert.texpr1_of_cil_exp res res.env (Lval (Cil.var v)) true) with - | Some min, Some max -> - assert (Z.equal min max); (* other bounds impossible in affeq *) - let (min_ik, max_ik) = IntDomain.Size.range ik in - if Z.lt min min_ik || Z.gt max max_ik then - if IntDomain.should_ignore_overflow ik then - bot () - else - raise NotRefinable - else res - | exception Convert.Unsupported_CilExp _ - | _ -> overflow_res res - - let meet_tcons t tcons expr = + let meet_tcons ask t tcons expr = let check_const cmp c = if cmp c Mpqf.zero then bot_env else t in let meet_vec e = (* Flip the sign of the const. val in coeff vec *) let coeff = Vector.nth e (Vector.length e - 1) in Vector.set_val_with e (Vector.length e - 1) (Mpqf.neg coeff); - let res = - if is_bot t then - bot () - else - let opt_m = Matrix.rref_vec_with (Matrix.copy @@ Option.get t.d) e in - if Option.is_none opt_m then bot () else {d = opt_m; env = t.env} - in - meet_tcons_one_var_eq res expr + if is_bot t then + bot () + else + let opt_m = Matrix.rref_vec_with (Matrix.copy @@ Option.get t.d) e in + if Option.is_none opt_m then bot () else {d = opt_m; env = t.env} + in - try - match get_coeff_vec t (Texpr1.to_expr @@ Tcons1.get_texpr1 tcons) with - | Some v -> - begin match to_constant_opt v, Tcons1.get_typ tcons with - | Some c, DISEQ -> check_const (=:) c - | Some c, SUP -> check_const (<=:) c - | Some c, EQ -> check_const (<>:) c - | Some c, SUPEQ -> check_const (<:) c - | None, DISEQ - | None, SUP -> - if equal (meet_vec v) t then - bot_env - else - t - | None, EQ -> - let res = meet_vec v in - if is_bot res then - bot_env - else - res - | _ -> t - end - | None -> t - with NotRefinable -> t + match get_coeff_vec t (Texpr1.to_expr @@ Tcons1.get_texpr1 tcons) with + | Some v -> + begin match to_constant_opt v, Tcons1.get_typ tcons with + | Some c, DISEQ -> check_const (=:) c + | Some c, SUP -> check_const (<=:) c + | Some c, EQ -> check_const (<>:) c + | Some c, SUPEQ -> check_const (<:) c + | None, DISEQ + | None, SUP -> + if equal (meet_vec v) t then + bot_env + else + t + | None, EQ -> + let res = meet_vec v in + if is_bot res then + bot_env + else + res + | _ -> t + end + | None -> t let meet_tcons t tcons expr = timing_wrap "meet_tcons" (meet_tcons t tcons) expr @@ -665,14 +557,13 @@ struct if M.tracing then M.tracel "ops" "unify: %s %s -> %s\n" (show a) (show b) (show res); res - let assert_cons d e negate no_ov = - let no_ov = Lazy.force no_ov in - if M.tracing then M.tracel "assert_cons" "assert_cons with expr: %a %b" d_exp e no_ov; - match Convert.tcons1_of_cil_exp d d.env e negate no_ov with - | tcons1 -> meet_tcons d tcons1 e + let assert_constraint ask d e negate no_ov = + if M.tracing then M.tracel "assert_constraint" "assert_constraint with expr: %a %b" d_exp e (Lazy.force no_ov); + match Convert.tcons1_of_cil_exp ask d d.env e negate no_ov with + | tcons1 -> meet_tcons ask d tcons1 e | exception Convert.Unsupported_CilExp _ -> d - let assert_cons d e negate no_ov = timing_wrap "assert_cons" (assert_cons d e negate) no_ov + 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 @@ -692,9 +583,9 @@ struct let cil_exp_of_lincons1 = Convert.cil_exp_of_lincons1 - let env (t: Bounds.t) = t.env + let env t = t.env - type marshal = Bounds.t + type marshal = t let marshal t = t @@ -704,6 +595,9 @@ end module D2(Vc: AbstractVector) (Mx: AbstractMatrix): RelationDomain.RD with type var = Var.t = struct module D = D (Vc) (Mx) - include SharedFunctions.AssertionModule (D.V) (D) + module ConvArg = struct + let allow_global = false + end + include SharedFunctions.AssertionModule (D.V) (D) (ConvArg) include D end diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml index 198708775c..20536df0b1 100644 --- a/src/cdomains/apron/apronDomain.apron.ml +++ b/src/cdomains/apron/apronDomain.apron.ml @@ -125,9 +125,9 @@ sig val keep_vars : t -> Var.t list -> t val keep_filter : t -> (Var.t -> bool) -> t val forget_vars : t -> Var.t list -> t - val assign_exp : t -> Var.t -> exp -> bool Lazy.t -> t + val assign_exp : Queries.ask -> t -> Var.t -> exp -> bool Lazy.t -> t val assign_var : t -> Var.t -> Var.t -> t - val substitute_exp : t -> Var.t -> exp -> bool Lazy.t -> t + val substitute_exp : Queries.ask-> t -> Var.t -> exp -> bool Lazy.t -> t end (** Imperative in-place environment and transfer functions. *) @@ -140,13 +140,13 @@ sig val keep_vars_with : t -> Var.t list -> unit val keep_filter_with : t -> (Var.t -> bool) -> unit val forget_vars_with : t -> Var.t list -> unit - val assign_exp_with : t -> Var.t -> exp -> bool Lazy.t -> unit - val assign_exp_parallel_with : t -> (Var.t * exp) list -> bool -> unit (* TODO: why this one isn't lazy? *) + val assign_exp_with : Queries.ask -> t -> Var.t -> exp -> bool Lazy.t -> unit + val assign_exp_parallel_with : Queries.ask -> t -> (Var.t * exp) list -> bool -> unit (* TODO: why this one isn't lazy? *) val assign_var_with : t -> Var.t -> Var.t -> unit val assign_var_parallel_with : t -> (Var.t * Var.t) list -> unit - val substitute_exp_with : t -> Var.t -> exp -> bool Lazy.t-> unit + val substitute_exp_with : Queries.ask -> t -> Var.t -> exp -> bool Lazy.t-> unit val substitute_exp_parallel_with : - t -> (Var.t * exp) list -> bool Lazy.t -> unit + Queries.ask -> t -> (Var.t * exp) list -> bool Lazy.t -> unit val substitute_var_with : t -> Var.t -> Var.t -> unit end @@ -186,17 +186,17 @@ struct let nd = copy d in forget_vars_with nd vs; nd - let assign_exp d v e no_ov = + let assign_exp ask d v e no_ov = let nd = copy d in - assign_exp_with nd v e no_ov; + assign_exp_with ask nd v e no_ov; nd let assign_var d v v' = let nd = copy d in assign_var_with nd v v'; nd - let substitute_exp d v e no_ov = + let substitute_exp ask d v e no_ov = let nd = copy d in - substitute_exp_with nd v e no_ov; + substitute_exp_with ask nd v e no_ov; nd end @@ -212,7 +212,7 @@ sig val mem_var : t -> Var.t -> bool val assign_var_parallel' : t -> Var.t list -> Var.t list -> t - val meet_tcons : t -> Tcons1.t -> exp -> t + val meet_tcons : Queries.ask -> t -> Tcons1.t -> exp -> t val to_lincons_array : t -> Lincons1.earray val of_lincons_array : Lincons1.earray -> t @@ -227,13 +227,17 @@ sig include AOpsPure with type t := t end - (** Convenience operations on A. *) module AOps0 (Tracked: Tracked) (Man: Manager) = struct open SharedFunctions module Bounds = Bounds (Man) - module Convert = Convert (V) (Bounds) (struct let allow_global = false end) (Tracked) + module Arg = struct + let allow_global = false + end + module Convert = Convert (V) (Bounds) (Arg) (Tracked) + + type t = Man.mt A.t @@ -276,8 +280,8 @@ struct let vs' = Array.of_list vs in A.forget_array_with Man.mgr nd vs' false - let assign_exp_with nd v e no_ov = - match Convert.texpr1_of_cil_exp nd (A.env nd) e (Lazy.force no_ov) with + let assign_exp_with ask nd v e no_ov = + match Convert.texpr1_of_cil_exp ask nd (A.env nd) e no_ov with | texpr1 -> if M.tracing then M.trace "apron" "assign_exp converted: %s\n" (Format.asprintf "%a" Texpr1.print texpr1); A.assign_texpr_with Man.mgr nd v texpr1 None @@ -285,7 +289,7 @@ struct if M.tracing then M.trace "apron" "assign_exp unsupported\n"; forget_vars_with nd [v] - let assign_exp_parallel_with nd ves no_ov = + let assign_exp_parallel_with ask nd ves no_ov = (* TODO: non-_with version? *) let env = A.env nd in (* partition assigns with supported and unsupported exps *) @@ -293,7 +297,7 @@ struct ves |> List.enum |> Enum.map (Tuple2.map2 (fun e -> - match Convert.texpr1_of_cil_exp nd env e no_ov with + match Convert.texpr1_of_cil_exp ask nd env e (Lazy.from_val no_ov) with | texpr1 -> Some texpr1 | exception Convert.Unsupported_CilExp _ -> None )) @@ -343,14 +347,14 @@ struct in A.assign_texpr_array Man.mgr d vs texpr1s None - let substitute_exp_with nd v e no_ov = - match Convert.texpr1_of_cil_exp nd (A.env nd) e (Lazy.force no_ov) with + let substitute_exp_with ask nd v e no_ov = + match Convert.texpr1_of_cil_exp ask nd (A.env nd) e no_ov with | texpr1 -> A.substitute_texpr_with Man.mgr nd v texpr1 None | exception Convert.Unsupported_CilExp _ -> forget_vars_with nd [v] - let substitute_exp_parallel_with nd ves no_ov = + let substitute_exp_parallel_with ask nd ves no_ov = (* TODO: non-_with version? *) let env = A.env nd in (* partition substitutes with supported and unsupported exps *) @@ -358,7 +362,7 @@ struct ves |> List.enum |> Enum.map (Tuple2.map2 (fun e -> - match Convert.texpr1_of_cil_exp nd env e (Lazy.force no_ov) with + match Convert.texpr1_of_cil_exp ask nd env e no_ov with | texpr1 -> Some texpr1 | exception Convert.Unsupported_CilExp _ -> None )) @@ -385,31 +389,10 @@ struct let texpr1 = Texpr1.of_expr (A.env nd) (Var v') in A.substitute_texpr_with Man.mgr nd v texpr1 None - (** Special affeq one variable logic to match AffineEqualityDomain. *) - let meet_tcons_affeq_one_var d res e = - let overflow_res res = if IntDomain.should_ignore_overflow (Cilfacade.get_ikind_exp e) then res else d in - match Convert.find_one_var e with - | None -> overflow_res res - | Some v -> - let ik = Cilfacade.get_ikind v.vtype in - match Bounds.bound_texpr res (Convert.texpr1_of_cil_exp res res.env (Lval (Cil.var v)) true) with - | Some _, Some _ when not (Cil.isSigned ik) -> d (* TODO: unsigned w/o bounds handled differently? *) - | Some min, Some max -> - assert (Z.equal min max); (* other bounds impossible in affeq *) - let (min_ik, max_ik) = IntDomain.Size.range ik in - if Z.compare min min_ik < 0 || Z.compare max max_ik > 0 then - if IntDomain.should_ignore_overflow ik then A.bottom (A.manager d) (A.env d) else d - else res - (* TODO: Unsupported_CilExp check? *) - | _, _ -> overflow_res res - - let meet_tcons d tcons1 e = + let meet_tcons _ d tcons1 e = let earray = Tcons1.array_make (A.env d) 1 in Tcons1.array_set earray 0 tcons1; - let res = A.meet_tcons_array Man.mgr d earray in - match Man.name () with - | "ApronAffEq" -> meet_tcons_affeq_one_var d res e (* TODO: don't hardcode by name, move to manager *) - | _ -> res + A.meet_tcons_array Man.mgr d earray let to_lincons_array d = A.to_lincons_array Man.mgr d @@ -511,50 +494,53 @@ struct include AOps (Tracked) (Man) include Tracked + let eval_interval ask = Bounds.bound_texpr + (** Assert a constraint expression. LAnd, LOr, LNot are directly supported by Apron domain in order to confirm logic-containing Apron invariants from witness while deep-query is disabled *) - let rec assert_cons d e negate (ov: bool Lazy.t) = - let no_ov = IntDomain.should_ignore_overflow (Cilfacade.get_ikind_exp e) in (* TODO: why ignores no_ov argument? *) + let rec assert_constraint ask d e negate (no_ov: bool Lazy.t) = + if M.tracing then M.trace "assert_constraint_apron" "%a ;;; %a\n" d_exp e d_plainexp e; match e with (* Apron doesn't properly meet with DISEQ constraints: https://github.com/antoinemine/apron/issues/37. Join Gt and Lt versions instead. *) | BinOp (Ne, lhs, rhs, intType) when not negate -> - let assert_gt = assert_cons d (BinOp (Gt, lhs, rhs, intType)) negate ov in - let assert_lt = assert_cons d (BinOp (Lt, lhs, rhs, intType)) negate ov in + let assert_gt = assert_constraint ask d (BinOp (Gt, lhs, rhs, intType)) negate no_ov in + let assert_lt = assert_constraint ask d (BinOp (Lt, lhs, rhs, intType)) negate no_ov in join assert_gt assert_lt | BinOp (Eq, lhs, rhs, intType) when negate -> - let assert_gt = assert_cons d (BinOp (Gt, lhs, rhs, intType)) (not negate) ov in - let assert_lt = assert_cons d (BinOp (Lt, lhs, rhs, intType)) (not negate) ov in + let assert_gt = assert_constraint ask d (BinOp (Gt, lhs, rhs, intType)) (not negate) no_ov in + let assert_lt = assert_constraint ask d (BinOp (Lt, lhs, rhs, intType)) (not negate) no_ov in join assert_gt assert_lt | BinOp (LAnd, lhs, rhs, intType) when not negate -> - let assert_l = assert_cons d lhs negate ov in - let assert_r = assert_cons d rhs negate ov in + let assert_l = assert_constraint ask d lhs negate no_ov in + let assert_r = assert_constraint ask d rhs negate no_ov in meet assert_l assert_r | BinOp (LAnd, lhs, rhs, intType) when negate -> - let assert_l = assert_cons d lhs negate ov in - let assert_r = assert_cons d rhs negate ov in + let assert_l = assert_constraint ask d lhs negate no_ov in + let assert_r = assert_constraint ask d rhs negate no_ov in join assert_l assert_r (* de Morgan *) | BinOp (LOr, lhs, rhs, intType) when not negate -> - let assert_l = assert_cons d lhs negate ov in - let assert_r = assert_cons d rhs negate ov in + let assert_l = assert_constraint ask d lhs negate no_ov in + let assert_r = assert_constraint ask d rhs negate no_ov in join assert_l assert_r | BinOp (LOr, lhs, rhs, intType) when negate -> - let assert_l = assert_cons d lhs negate ov in - let assert_r = assert_cons d rhs negate ov in + let assert_l = assert_constraint ask d lhs negate no_ov in + let assert_r = assert_constraint ask d rhs negate no_ov in meet assert_l assert_r (* de Morgan *) - | UnOp (LNot,e,_) -> assert_cons d e (not negate) ov + | UnOp (LNot,e,_) -> assert_constraint ask d e (not negate) no_ov | _ -> - begin match Convert.tcons1_of_cil_exp d (A.env d) e negate no_ov with + begin match Convert.tcons1_of_cil_exp ask d (A.env d) e negate no_ov with | tcons1 -> - if M.tracing then M.trace "apron" "assert_cons %a %s\n" d_exp e (Format.asprintf "%a" Tcons1.print tcons1); - if M.tracing then M.trace "apron" "assert_cons st: %a\n" D.pretty d; - let r = meet_tcons d tcons1 e in - if M.tracing then M.trace "apron" "assert_cons r: %a\n" D.pretty r; + if M.tracing then M.trace "apron" "assert_constraint %a %s\n" d_exp e (Format.asprintf "%a" Tcons1.print tcons1); + if M.tracing then M.trace "apron" "assert_constraint st: %a\n" D.pretty d; + if M.tracing then M.trace "apron" "assert_constraint tcons1: %s\n" (Format.asprintf "%a" Tcons1.print tcons1); + let r = meet_tcons ask d tcons1 e in + if M.tracing then M.trace "apron" "assert_constraint r: %a\n" D.pretty r; r | exception Convert.Unsupported_CilExp reason -> - if M.tracing then M.trace "apron" "assert_cons %a unsupported: %s\n" d_exp e (SharedFunctions.show_unsupported_cilExp reason); + if M.tracing then M.trace "apron" "assert_constraint %a unsupported: %s\n" d_exp e (SharedFunctions.show_unsupported_cilExp reason); d end @@ -728,11 +714,21 @@ struct ) else ( let exps = ResettableLazy.force WideningThresholds.exps in - let module Convert = SharedFunctions.Convert (V) (Bounds(Man)) (struct let allow_global = true end) (Tracked) in + let module Arg = struct + let allow_global = true + end in + let module Convert = SharedFunctions.Convert (V) (Bounds(Man)) (Arg) (Tracked) in (* this implements widening_threshold with Tcons1 instead of Lincons1 *) let tcons1s = List.filter_map (fun e -> - let no_ov = IntDomain.should_ignore_overflow (Cilfacade.get_ikind_exp e) in - match Convert.tcons1_of_cil_exp y y_env e false no_ov with + let no_ov = lazy(IntDomain.should_ignore_overflow (Cilfacade.get_ikind_exp e)) in + let dummyask = let f (type a) (q : a Queries.t) : a = + (* Convert.tcons1_of_cil_exp supports fancy aggressive simplifications of expressions + via querying the context for int constants that replace subexpressions; + we do not have a context here, so we just use a dummy ask replying top all the time *) + Queries.Result.top q + in + ({ f } : Queries.ask) in + match Convert.tcons1_of_cil_exp dummyask y y_env e false no_ov with | tcons1 when A.sat_tcons Man.mgr y tcons1 -> Some tcons1 | _ @@ -798,7 +794,7 @@ end module D (Man: Manager)= struct module DWO = DWithOps (Man) (DHetero (Man)) - include SharedFunctions.AssertionModule (V) (DWO) + include SharedFunctions.AssertionModule (V) (DWO) (DWO.Arg) include DWO module Tracked = Tracked module Man = Man @@ -815,8 +811,8 @@ sig module V: RV module Tracked: RelationDomain.Tracked - val assert_inv : t -> exp -> bool -> bool Lazy.t -> t - val eval_int : t -> exp -> bool Lazy.t -> Queries.ID.t + val assert_inv : Queries.ask -> t -> exp -> bool -> bool Lazy.t -> t + val eval_int : Queries.ask -> t -> exp -> bool Lazy.t -> Queries.ID.t end @@ -898,12 +894,12 @@ struct let forget_vars_with (b, d) vs = BoxD.forget_vars_with b vs; D.forget_vars_with d vs - let assign_exp_with (b, d) v e no_ov = - BoxD.assign_exp_with b v e no_ov; - D.assign_exp_with d v e no_ov - let assign_exp_parallel_with (b, d) ves no_ov = - BoxD.assign_exp_parallel_with b ves no_ov; - D.assign_exp_parallel_with d ves no_ov + let assign_exp_with ask (b, d) v e no_ov = + BoxD.assign_exp_with ask b v e no_ov; + D.assign_exp_with ask d v e no_ov + let assign_exp_parallel_with ask (b, d) ves no_ov = + BoxD.assign_exp_parallel_with ask b ves no_ov; + D.assign_exp_parallel_with ask d ves no_ov let assign_var_with (b, d) v e = BoxD.assign_var_with b v e; D.assign_var_with d v e @@ -912,22 +908,22 @@ struct D.assign_var_parallel_with d vvs let assign_var_parallel' (b, d) vs v's = (BoxD.assign_var_parallel' b vs v's, D.assign_var_parallel' d vs v's) - let substitute_exp_with (b, d) v e no_ov = - BoxD.substitute_exp_with b v e no_ov; - D.substitute_exp_with d v e no_ov - let substitute_exp_parallel_with (b, d) ves no_ov = - BoxD.substitute_exp_parallel_with b ves no_ov; - D.substitute_exp_parallel_with d ves no_ov + let substitute_exp_with ask (b, d) v e no_ov = + BoxD.substitute_exp_with ask b v e no_ov; + D.substitute_exp_with ask d v e no_ov + let substitute_exp_parallel_with ask (b, d) ves no_ov = + BoxD.substitute_exp_parallel_with ask b ves no_ov; + D.substitute_exp_parallel_with ask d ves no_ov let substitute_var_with (b, d) v1 v2 = BoxD.substitute_var_with b v1 v2; D.substitute_var_with d v1 v2 - let meet_tcons (b, d) c e = (BoxD.meet_tcons b c e, D.meet_tcons d c e) + let meet_tcons ask (b, d) c e = (BoxD.meet_tcons ask b c e, D.meet_tcons ask d c e) let to_lincons_array (_, d) = D.to_lincons_array d let of_lincons_array a = (BoxD.of_lincons_array a, D.of_lincons_array a) let cil_exp_of_lincons1 = D.cil_exp_of_lincons1 - let assert_inv (b, d) e n no_ov = (BoxD.assert_inv b e n no_ov, D.assert_inv d e n no_ov) - let eval_int (_, d) = D.eval_int d + let assert_inv ask (b, d) e n no_ov = (BoxD.assert_inv ask b e n no_ov, D.assert_inv ask d e n no_ov) + let eval_int ask (_, d) = D.eval_int ask d let invariant (b, d) = (* diff via lincons *) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml new file mode 100644 index 0000000000..b4bf5a7616 --- /dev/null +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -0,0 +1,698 @@ +(** OCaml implementation of the linear two-variable equality domain. + + @see A. Flexeder, M. Petter, and H. Seidl Fast Interprocedural Linear Two-Variable Equalities. *) + +(** Abstract states in this domain are represented by structs containing an array and an apron environment. + The arrays are modeled as proposed in the paper: Each variable is assigned to an index and each array element represents a linear relationship that must hold at the corresponding program point. + The apron environment is hereby used to organize the order of columns and variables. +*) + +open Batteries +open GoblintCil +open Pretty +module M = Messages +open Apron +open VectorMatrix + +module Mpqf = SharedFunctions.Mpqf + +module Equality = struct + (* (Some i, k) represents a sum of a variable with index i and the number k. + (None, k) represents the number k. *) + type t = (int option * (Z.t [@printer Z.pp_print])) [@@deriving eq, ord, hash, show] + let zero = (None, Z.zero) + let var_zero i = (Some i, Z.zero) + let to_int x = Z.to_int @@ snd x +end + +module EqualitiesArray = struct + include Array + type t = Equality.t Array.t [@@deriving eq, ord] + + let show m = + Array.fold_right (fun k result -> Equality.show k ^ "\n" ^ result) m "" + + let hash : t -> int = Array.fold_left (fun acc a -> 31 * acc + Equality.hash a) 0 (* TODO: derive *) + + let empty () = [||] + + let make_empty_array len = Array.init len (fun i -> (Some i, Z.zero)) + + (** add new variables to domain with particular indices; translates old indices to keep consistency + the semantics of indexes can be retrieved from apron: https://antoinemine.github.io/Apron/doc/api/ocaml/Dim.html *) + let add_variables_to_domain m indexes = + if length indexes = 0 then m else + let offset_map = Array.make (Array.length m) 0 (* maps each variable to the number of variables that are added before this variable *) + in + let _ = + let rec shift (offset, list) index = (* bumps offset & pops list, if/while index is heading the list *) + match list with + | hd::tl when hd = index -> shift (offset+1, tl) index + | _ -> (offset, list) + in + (* TODO: https://github.com/goblint/analyzer/pull/1297#discussion_r1479505621 *) + Array.fold_lefti (* this is not a textbook fold. We rather use it as a means to iterate over the range + of all indices of offset_map, initializing the array at these indices as a side-effect. + We use fold here as a means of having an accumulator to keep track of the current offset + and the rest of the offset list. In case of more frequent use of this pattern, consider this as + a candidate template for a new library function *) + (fun offsetcontext index _ -> + let newoffset, newlist = shift offsetcontext index in + offset_map.(index) <- newoffset; + (newoffset, newlist)) + (0, Array.to_list indexes) offset_map + in + let add_offset_to_array_entry (var, offs) = (* uses offset_map to obtain a new var_index, that is consistent with the new reference indices *) + Option.map (fun var_index -> var_index + offset_map.(var_index)) var, offs in + let m' = make_empty_array (length m + length indexes) + in Array.iteri (fun j eq -> m'.(j + offset_map.(j)) <- add_offset_to_array_entry eq) m; + m'(* produces a consistent new conj. of equalities *) + + let remove_variables_from_domain m indexes = + let nr_removed_colums = length indexes in + if nr_removed_colums = 0 || length m = 0 then m + else + if length m = nr_removed_colums then [||] else + let offset_map = Array.make (Array.length m) 0 + (* maps each variable to the number of variables that are removed before this variable *) + in let _ = Array.fold_lefti + (fun offset index _ -> + if offset < nr_removed_colums && indexes.(offset) = index then offset + 1 + else (offset_map.(index) <- offset; offset)) + 0 offset_map in + let remove_offset_from_array_entry (var, offs) = + Option.map (fun var_index -> var_index - offset_map.(var_index)) var, offs in + Array.(filteri (fun i _ -> not @@ Array.mem i indexes) m (* filter out removed variables*) + |> map remove_offset_from_array_entry) (* adjust variable indexes *) + + let remove_variables_from_domain m cols = timing_wrap "del_cols" (remove_variables_from_domain m) cols + + let is_empty m = length m = 0 + + let is_top_array = GobArray.for_alli (fun i (a, e) -> GobOption.exists ((=) i) a && Z.equal e Z.zero) + + (* Forget information about variable var in-place. *) + let forget_variable_with d var = + (let ref_var_opt = fst d.(var) in + match ref_var_opt with + | Some ref_var when ref_var = var -> + (* var is the reference variable of its connected component *) + (let cluster = List.tl @@ fold_righti + (fun i (ref, offset) l -> if ref = ref_var_opt then i::l else l) d [] in + (* obtain cluster with common reference variable ref_var*) + match cluster with (* new ref_var is taken from head of the cluster *) + | head :: tail -> let headconst = snd d.(head) in (* take offset between old and new reference variable *) + List.iter (fun i -> d.(i) <- Z.(Some head, snd d.(i) - headconst)) cluster (* shift offset to match new reference variable *) + | _ -> ()) (* empty cluster means no work for us *) + | _ -> ()) (* variable is either a constant or expressed by another refvar *) + ; d.(var) <- Equality.var_zero var (* set d(var) to unknown, finally *) + + (* Forget information about variable i but not in-place *) + let forget_variable m j = + let copy = copy m in + forget_variable_with copy j; + copy + + let dim_add (ch: Apron.Dim.change) m = + add_variables_to_domain m ch.dim + + let dim_add ch m = timing_wrap "dim add" (dim_add ch) m + + let dim_remove (ch: Apron.Dim.change) m ~del = + if Array.length ch.dim = 0 || is_empty m then + m + else ( + Array.modifyi (+) ch.dim; + let m' = Array.fold_left (fun y x -> forget_variable_with y x; y) (copy m) ch.dim in + remove_variables_from_domain m' ch.dim) + + let dim_remove ch m ~del = VectorMatrix.timing_wrap "dim remove" (fun del -> dim_remove ch m ~del:del) del + + +end + +(** [VarManagement] defines the type t of the affine equality domain (a record that contains an optional matrix and an apron environment) and provides the functions needed for handling variables (which are defined by [RelationDomain.D2]) such as [add_vars], [remove_vars]. + Furthermore, it provides the function [simplified_monomials_from_texp] that converts an apron expression into a list of monomials of reference variables and a constant offset *) +module VarManagement = +struct + module EArray = EqualitiesArray + include SharedFunctions.VarManagementOps (EArray) + + let dim_add = EArray.dim_add + let size t = BatOption.map_default (fun d -> EArray.length d) 0 t.d + + (** 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 (coeff, var) -> (Z.(-coeff), var)) coeff_var_list in + let multiply_with_Z number coeff_var_list = + List.map (fun (coeff, var) -> (Z.(number * coeff, var))) coeff_var_list in + let multiply a b = + (* if one of them is a constant, then multiply. Otherwise, the expression is not linear *) + match a, b with + | [(a_coeff, None)], b -> multiply_with_Z a_coeff b + | a, [(b_coeff, None)] -> multiply_with_Z b_coeff a + | _ -> raise NotLinearExpr + in + let rec convert_texpr texp = + begin match texp with + (* If x is a constant, replace it with its const. val. immediately *) + | Cst (Interval _) -> failwith "constant was an interval; this is not supported" + | Cst (Scalar x) -> + begin match SharedFunctions.int_of_scalar ?round:None x with + | Some x -> [(x, None)] + | None -> raise ScalarIsInfinity end + | Var x -> + let var_dim = Environment.dim_of_var t.env x in + begin match t.d with + | None -> [(Z.one, Some var_dim)] + | Some d -> + (match d.(var_dim) with + | (Some i, k) -> [(Z.one, Some i); (k, None)] + | (None, k) -> [(k, None)]) + 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 _ -> 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 and a constant *) + let simplified_monomials_from_texp (t: t) texp = + BatOption.bind (monomials_from_texp t texp) + (fun monomiallist -> + let d = Option.get t.d in + let expr = Array.make (Environment.size t.env) Z.zero in + let accumulate_constants a (c, v) = match v with + | None -> Z.(a + c) + | Some idx -> let (term,con) = d.(idx) in + (Option.may (fun ter -> expr.(ter) <- Z.(expr.(ter) + c)) term; + Z.(a + c * con)) + in + let constant = List.fold_left accumulate_constants Z.zero monomiallist in (* abstract simplification of the guard wrt. reference variables *) + Some (Array.fold_lefti (fun list v (c) -> if Z.equal c Z.zero then list else (c,v)::list) [] expr, constant) ) + + let simplify_to_ref_and_offset (t: t) texp = + BatOption.bind (simplified_monomials_from_texp t texp ) + (fun (sum_of_terms, constant) -> + (match sum_of_terms with + | [] -> Some (None, constant) + | [(coeff,var)] when Z.equal coeff Z.one -> Some (Some var, constant) + |_ -> None)) + + let simplify_to_ref_and_offset t texp = timing_wrap "coeff_vec" (simplify_to_ref_and_offset t) texp + + (* Copy because function is not "with" so should not mutate inputs *) + let assign_const t var const = match t.d with + | None -> t + | Some t_d -> + let d = EArray.copy t_d in d.(var) <- (None, const); {d = Some d; env = t.env} + + let subtract_const_from_var t var const = + match t.d with + | None -> t + | Some t_d -> + let d = EArray.copy t_d in + let subtract_const_from_var_for_single_equality index (eq_var_opt, off2) = + if index <> var then + begin match eq_var_opt with + | Some eq_var when eq_var = var -> + d.(index) <- (eq_var_opt, Z.(off2 - const)) + | _ -> () + end + in + begin if d.(var) = (Some var, Z.zero) + (* var is a reference variable -> it can appear on the right-hand side of an equality *) + then + EArray.iteri (subtract_const_from_var_for_single_equality) d + else + (* var never appears on the right hand side-> we only need to modify the array entry at index var *) + d.(var) <- Tuple2.map2 (Z.add const) d.(var) + end; + {d = Some d; env = t.env} + +end + + +module ExpressionBounds: (SharedFunctions.ConvBounds with type t = VarManagement.t) = +struct + include VarManagement + + let bound_texpr t texpr = + match simplify_to_ref_and_offset t (Texpr1.to_expr texpr) with + | Some (None, offset) -> + (if M.tracing then M.tracel "bounds" "min: %s max: %s" (IntOps.BigIntOps.to_string offset) (IntOps.BigIntOps.to_string offset); + Some offset, Some offset) + | _ -> None, None + + let bound_texpr d texpr1 = timing_wrap "bounds calculation" (bound_texpr d) texpr1 +end + +module D = +struct + include Printable.Std + include ConvenienceOps (Mpqf) + include VarManagement + + module Bounds = ExpressionBounds + module V = RelationDomain.V + module Arg = struct + let allow_global = true + end + module Convert = SharedFunctions.Convert (V) (Bounds) (Arg) (SharedFunctions.Tracked) + + type var = V.t + + let name () = "lin2vareq" + + 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 (EArray.make_empty_array (Environment.size env)); env = env} + + (** env = \emptyset, d = Some([||]) *) + let top () = {d = Some (EArray.empty()); env = empty_env} + + (** is_top returns true for top_of array and empty array; precondition: t.env and t.d are of same size *) + let is_top t = Environment.equal empty_env t.env && GobOption.exists EArray.is_top_array t.d + + (** prints the current variable equalities with resolved variable names *) + let show varM = + let lookup i = Var.to_string (Environment.var_of_dim varM.env i) in + let show_offs o = if Z.equal o Z.zero then "" else " + " ^ Z.to_string o in + let show_var i = function + | (None, o) -> (lookup i) ^ " = " ^ Z.to_string o ^ ";\n" + | (Some index, o) when i <> index -> + (lookup i) ^ " = " ^ lookup index ^ show_offs o ^ ";\n" + | _ -> "" + in + match varM.d with + | None -> "⊥\n" + | Some arr when EArray.is_top_array arr -> "⊤\n" + | Some arr -> + if is_bot varM then + "Bot \n" + else + Array.fold_lefti (fun acc i elem -> acc ^ show_var i elem) "" arr + + let pretty () (x:t) = text (show x) + let printXml f x = BatPrintf.fprintf f "\n\n\nequalities-array\n\n\n%s\n\nenv\n\n\n%s\n\n\n" (XmlUtil.escape (Format.asprintf "%s" (show x) )) (XmlUtil.escape (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (x.env))) + let eval_interval ask = Bounds.bound_texpr + + exception Contradiction + + let meet_with_one_conj_with ts i (var, b) = + let subst_var ts x (vart, bt) = + let adjust = function + | (Some vare, b') when vare = x -> (vart, Z.(b' + bt)) + | e -> e + in + BatArray.modify adjust ts + in + let (var1, b1) = ts.(i) in + (match var, var1 with + | None, None -> if not @@ Z.equal b b1 then raise Contradiction + | None, Some h1 -> subst_var ts h1 (None, Z.(b - b1)) + | Some j, None -> subst_var ts j (None, Z.(b1 - b)) + | Some j, Some h1 -> + (match ts.(j) with + | (None, b2) -> subst_var ts i (None, Z.(b2 + b)) + | (Some h2, b2) -> + if h1 = h2 then + (if not @@ Z.equal b1 Z.(b2 + b) then raise Contradiction) + else if h1 < h2 then subst_var ts h2 (Some h1, Z.(b1 - (b + b2))) + else subst_var ts h1 (Some h2, Z.(b + (b2 - b1))))) + + let meet_with_one_conj t i e = + match t.d with + | None -> t + | Some d -> + let res_d = Array.copy d in + try + meet_with_one_conj_with res_d i e; + {d = Some res_d; env = t.env} + with Contradiction -> + {d = None; env = t.env} + + let meet t1 t2 = + let sup_env = Environment.lce t1.env t2.env in + let t1 = change_d t1 sup_env ~add:true ~del:false in + let t2 = change_d t2 sup_env ~add:true ~del:false in + match t1.d, t2.d with + | Some d1', Some d2' -> ( + try + let res_d = Array.copy d1' in + Array.iteri (meet_with_one_conj_with res_d) d2'; + {d = Some res_d; env = sup_env} + with Contradiction -> + {d = None; env = sup_env} + ) + | _ -> {d = None; env = sup_env} + + let meet t1 t2 = + let res = meet t1 t2 in + if M.tracing then M.tracel "meet" "meet a: %s b: %s -> %s \n" (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.compare t1.env t2.env in (* Apron's Environment.compare has defined return values. *) + let implies ts (var, b) i = + let tuple_cmp = Tuple2.eq (Option.eq ~eq:Int.equal) (Z.equal) in + match var with + | None -> tuple_cmp (var, b) ts.(i) + | Some j -> tuple_cmp ts.(i) @@ Tuple2.map2 (Z.add b) ts.(j) + in + if env_comp = -2 || env_comp > 0 then false else + if is_bot_env t1 || is_top t2 then true else + if is_bot_env t2 || is_top t1 then false else + let m1, m2 = Option.get t1.d, Option.get t2.d in + let m1' = if env_comp = 0 then m1 else VarManagement.dim_add (Environment.dimchange t1.env t2.env) m1 in + GobArray.for_alli (fun i t -> implies m1' t i) m2 + + 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 \n" (show t1) (show t2) res ; + res + + let join a b = + let join_d ad bd = + (*use copy of ad because result is later saved in there*) + let ad = Array.copy ad in + (*This is the table which is later grouped*) + let table = BatList.map2i (fun i (ai, aj) (bi,bj) -> (i, Z.(aj - bj), (ai, aj), (bi,bj))) (Array.to_list ad) (Array.to_list bd) in + (*compare two variables for grouping depending on delta function and reference index*) + let cmp_z (_, t0i, t1i, t2i) (_, t0j, t1j, t2j) = + let cmp_ref = Option.compare ~cmp:Int.compare in + Tuple3.compare ~cmp1:cmp_ref ~cmp2:cmp_ref ~cmp3:Z.compare (fst t1i, fst t2i, t0i) (fst t1j, fst t2j, t0j) + in + (*Calculate new components as groups*) + let new_components = BatList.group cmp_z table in + (*Adjust the domain array to represent the new components*) + let modify idx_h b_h (idx, _, (opt1, z1), (opt2, z2)) = + if opt1 = opt2 && Z.equal z1 z2 then () + else ad.(idx) <- (Some idx_h, Z.(z1 - b_h)) + in + let iterate l = + match l with + | (idx_h, _, (_, b_h), _) :: t -> List.iter (modify idx_h b_h) l + | [] -> let exception EmptyComponent in raise EmptyComponent + in + List.iter iterate new_components; Some ad + in + (*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 a || is_top b -> + let new_env = Environment.lce a.env b.env in + top_of new_env + | Some x, Some y when (Environment.compare 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; env = sup_env} + | Some x, Some y when EArray.equal x y -> {d = Some x; env = a.env} + | Some x, Some y -> {d = join_d x y; env = a.env} + + let join a b = timing_wrap "join" (join a) b + + let join a b = + let res = join a b in + if M.tracing then M.tracel "join" "join a: %s b: %s -> %s \n" (show a) (show b) (show res) ; + res + + let widen a b = + join a b + + let widen a b = + let res = widen a b in + if M.tracing then M.tracel "widen" "widen a: %s b: %s -> %s \n" (show a) (show b) (show res) ; + res + + let narrow a b = meet a b + + let narrow a b = + let res = narrow a b in + if M.tracing then M.tracel "narrow" "narrow a: %s b: %s -> %s \n" (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_vars t vars = + if is_bot_env t || is_top t || List.is_empty vars then + t + else + let m = EArray.copy @@ Option.get t.d in + List.iter + (fun var -> + EArray.forget_variable_with m (Environment.dim_of_var t.env var)) + vars; + {d = Some m; 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\n" (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 = + match t.d with + | Some d -> + let var_i = Environment.dim_of_var t.env var (* this is the variable we are assigning to *) in + begin match simplify_to_ref_and_offset t texp with + | None -> + (* Statement "assigned_var = ?" (non-linear assignment) *) + forget_vars t [var] + | Some (None, off) -> + (* Statement "assigned_var = off" (constant assignment) *) + assign_const (forget_vars t [var]) var_i off + | Some (Some exp_var, off) when var_i = exp_var -> + (* Statement "assigned_var = assigned_var + off" *) + subtract_const_from_var t var_i off + | Some (Some exp_var, off) -> + (* Statement "assigned_var = exp_var + off" (assigned_var is not the same as exp_var) *) + meet_with_one_conj (forget_vars t [var]) var_i (Some exp_var, off) + end + | None -> bot_env + + let assign_texpr t var texp = timing_wrap "assign_texpr" (assign_texpr t var) texp + + (* 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 + match Convert.texpr1_expr_of_cil_exp ask t t.env exp no_ov with + | texp -> assign_texpr t var texp + | exception Convert.Unsupported_CilExp _ -> forget_vars t [var] + + let assign_exp ask t var exp no_ov = + 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: %s \n exp: %a\n no_ov: %b -> \n %s\n" + (show t) (Var.to_string 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') + + 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: %s \n v': %s\n -> %s\n" (show t) (Var.to_string v) (Var.to_string 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 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 + drop_vars switched_arr primed_vars ~del:true + | _ -> 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 \n" (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'\n"; + 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'\n"; + 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_vars 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: %s \n exp: %a \n -> \n %s\n" (show t) (Var.to_string 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 -> + match simplified_monomials_from_texp t (Texpr1.to_expr @@ Tcons1.get_texpr1 tcons) with + | None -> t + | Some (sum_of_terms, constant) ->( + match sum_of_terms with + | [] -> (* no reference variables in the guard *) + 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 + | [(varexpr, index)] -> (* guard has a single reference variable only *) + if Tcons1.get_typ tcons = EQ && Z.divisible constant varexpr then + meet_with_one_conj t index (None, (Z.(-(constant) / varexpr))) + else + t (* only EQ is supported in equality based domains *) + | [(a1,var1); (a2,var2)] -> (* two variables in relation needs a little sorting out *) + begin match Tcons1.get_typ tcons with + | EQ when Z.(a1 * a2 = -one) -> (* var1-var1 or var2-var1 *) + meet_with_one_conj t var2 (Some var1, Z.mul a1 constant) + | _-> t (* Not supported in equality based 2vars without coeffiients *) + end + | _ -> t (* For equalities of more then 2 vars we just return t *)) + + 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 %s -> %s\n" (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) = + if M.tracing then M.tracel "assert_constraint" "assert_constraint with expr: %a %b\n" d_exp e (Lazy.force no_ov); + 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_mpqf @@ Mpqf.of_mpz (Z_mlgmpidl.mpz_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) -> + let xi = Environment.var_of_dim t.env i in + of_coeff xi [(Coeff.s_of_int (-1), xi)] o :: acc + | (Some r, _) when r = i -> acc + | (Some r, o) -> + let xi = Environment.var_of_dim t.env i in + let ri = Environment.var_of_dim t.env r in + of_coeff xi [(Coeff.s_of_int (-1), xi); (Coeff.s_of_int 1, ri)] o :: acc + in + BatOption.map_default (Array.fold_lefti get_const []) [] t.d + + 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: RelationDomain.RD with type var = Var.t = +struct + module D = D + module ConvArg = struct + let allow_global = false + end + include SharedFunctions.AssertionModule (D.V) (D) (ConvArg) + include D +end diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.no-apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.no-apron.ml new file mode 100644 index 0000000000..5fed2c883c --- /dev/null +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.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/relationDomain.apron.ml b/src/cdomains/apron/relationDomain.apron.ml index 82e7e20d20..afadfd39c4 100644 --- a/src/cdomains/apron/relationDomain.apron.ml +++ b/src/cdomains/apron/relationDomain.apron.ml @@ -109,20 +109,20 @@ sig val keep_filter : t -> (var -> bool) -> t val forget_vars : t -> var list -> t - (** Lazy bool ov parameter has been added to functions where functions of the Convert module are used. + (** Lazy bool no_ov parameter has been added to functions where functions of the Convert module are used. This is to also to make used of the improved overflow handling. *) - val assign_exp : t -> var -> exp -> bool Lazy.t -> t + val assign_exp : Queries.ask -> t -> var -> exp -> bool Lazy.t -> t val assign_var : t -> var -> var -> t val assign_var_parallel_with : t -> (var * var) list -> unit val assign_var_parallel' : t -> var list -> var list -> t - val substitute_exp : t -> var -> exp -> bool Lazy.t -> t + val substitute_exp : Queries.ask -> t -> var -> exp -> bool Lazy.t -> t val unify: t -> t -> t val marshal: t -> marshal val unmarshal: marshal -> t val mem_var: t -> var -> bool - val assert_inv : t -> exp -> bool -> bool Lazy.t -> t - val eval_int : t -> exp -> bool Lazy.t -> Queries.ID.t + val assert_inv : Queries.ask -> t -> exp -> bool -> bool Lazy.t -> t + val eval_int : Queries.ask -> t -> exp -> bool Lazy.t -> Queries.ID.t end module type S3 = diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index f7b800a404..1e17074088 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -1,8 +1,8 @@ (** Relational value domain utilities. *) - open GoblintCil open Batteries -open Apron + +open GobApron module M = Messages @@ -55,6 +55,7 @@ type unsupported_cilExp = | BinOp_not_supported (** BinOp constructor not supported. *) [@@deriving show { with_path = false }] + (** Interface for Bounds which calculates bounds for expressions and is used inside the - Convert module. *) module type ConvBounds = sig @@ -62,7 +63,11 @@ sig val bound_texpr: t -> Texpr1.t -> Z.t option * Z.t option end -(** Conversion from CIL expressions to Apron. *) +(** Conversion from CIL expressions to Apron. + This is used by the domains "affine equalities" and "linear two variable equalities". + It also handles the overflow through the flag "no_ov". + For this reason it was divided from the Convert module for the pure apron domains "ApronOfCilForApronDomains", +*) module ApronOfCil (V: SV) (Bounds: ConvBounds) (Arg: ConvertArg) (Tracked: RelationDomain.Tracked) = struct open Texpr1 @@ -75,81 +80,129 @@ struct | _ -> None (* for other exception *) ) - let texpr1_expr_of_cil_exp d env exp no_ov = - (* recurse without env argument *) - let rec texpr1_expr_of_cil_exp = function - | Lval (Var v, NoOffset) when Tracked.varinfo_tracked v -> - if not v.vglob || Arg.allow_global then - let var = - if v.vglob then - V.global v + (** This still tries to establish bounds via Bounds.bound_texpr, which may be more precise in case ana.int.interval + is disabled and the relational analysis manages to evaluate a value to an interval, which can then not be represented + as the result of an EvalInt query. This is a workaround and works as long as only one relational domain is used. + With multiple domains and disabled interval domain, the queries will not be able to exchange interval information, + and each analysis will only be able to establish constant bounds, but only its own interval bounds and not interval bounds + established by other analyses.*) + let overflow_handling no_ov ik env expr d exp = + match Cilfacade.get_ikind_exp exp with + | exception Invalid_argument e -> raise (Unsupported_CilExp Exp_not_supported) (* expression is not an integer expression, i.e. float *) + | ik -> + if IntDomain.should_wrap ik || not (Lazy.force no_ov) then ( + let (type_min, type_max) = IntDomain.Size.range ik in + let texpr1 = Texpr1.of_expr env expr in + match Bounds.bound_texpr d texpr1 with + | Some min, Some max when Z.compare type_min min <= 0 && Z.compare max type_max <= 0 -> + () + | min_opt, max_opt -> + if M.tracing then M.trace "apron" "may overflow: %a (%a, %a)\n" CilType.Exp.pretty exp (Pretty.docOpt (IntOps.BigIntOps.pretty ())) min_opt (Pretty.docOpt (IntOps.BigIntOps.pretty ())) max_opt; + raise (Unsupported_CilExp Overflow) + ) + + let texpr1_expr_of_cil_exp (ask:Queries.ask) d env exp no_ov = + let conv exp = + let query e ik = + let res = + match ask.f (EvalInt e) with + | `Bot -> raise (Unsupported_CilExp Exp_not_supported) (* This should never happen according to Michael Schwarz *) + | `Top -> IntDomain.IntDomTuple.top_of ik + | `Lifted x -> x (* Cast should be unnecessary because it should be taken care of by EvalInt. *) in + if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp/query: %a -> %a\n" d_plainexp e IntDomain.IntDomTuple.pretty res; + res + in + (* recurse without env and ask arguments *) + let rec texpr1_expr_of_cil_exp = function + | Lval (Var v, NoOffset) when Tracked.varinfo_tracked v -> + if not v.vglob || Arg.allow_global then + let var = + if v.vglob then + V.global v + else + V.local v + in + if Environment.mem_var env var then + Var var else - V.local v - in - if Environment.mem_var env var then - Var var + raise (Unsupported_CilExp (Var_not_found v)) else - raise (Unsupported_CilExp (Var_not_found v)) - else - failwith "texpr1_expr_of_cil_exp: globals must be replaced with temporary locals" - | Const (CInt (i, _, _)) -> - Cst (Coeff.s_of_mpqf (Mpqf.of_mpz (Z_mlgmpidl.mpz_of_z i))) - | exp -> - match Cilfacade.get_ikind_exp exp with - | ik -> - let expr = - match exp with - | UnOp (Neg, e, _) -> - Unop (Neg, texpr1_expr_of_cil_exp e, Int, Near) - | BinOp (PlusA, e1, e2, _) -> - Binop (Add, texpr1_expr_of_cil_exp e1, texpr1_expr_of_cil_exp e2, Int, Near) - | BinOp (MinusA, e1, e2, _) -> - Binop (Sub, texpr1_expr_of_cil_exp e1, texpr1_expr_of_cil_exp e2, Int, Near) - | BinOp (Mult, e1, e2, _) -> - Binop (Mul, texpr1_expr_of_cil_exp e1, texpr1_expr_of_cil_exp e2, Int, Near) - | BinOp (Div, e1, e2, _) -> - Binop (Div, texpr1_expr_of_cil_exp e1, texpr1_expr_of_cil_exp e2, Int, Zero) - | BinOp (Mod, e1, e2, _) -> - Binop (Mod, texpr1_expr_of_cil_exp e1, texpr1_expr_of_cil_exp e2, Int, Near) - | CastE (TInt (t_ik, _) as t, e) -> - begin match IntDomain.should_ignore_overflow t_ik || IntDomain.Size.is_cast_injective ~from_type:(Cilfacade.typeOf e) ~to_type:t with (* TODO: unnecessary cast check due to overflow check below? or maybe useful in general to also assume type bounds based on argument types? *) - | true -> - Unop (Cast, texpr1_expr_of_cil_exp e, Int, Zero) (* TODO: what does Apron Cast actually do? just for floating point and rounding? *) - | false - | exception Cilfacade.TypeOfError _ (* typeOf inner e, not outer exp *) - | exception Invalid_argument _ -> (* get_ikind in is_cast_injective *) - raise (Unsupported_CilExp (Cast_not_injective t)) - end - | _ -> - raise (Unsupported_CilExp Exp_not_supported) - in - if not no_ov then ( - let (type_min, type_max) = IntDomain.Size.range ik in - let texpr1 = Texpr1.of_expr env expr in - match Bounds.bound_texpr d texpr1 with - | Some min, Some max when Z.compare type_min min <= 0 && Z.compare max type_max <= 0 -> () - | min_opt, max_opt -> - if M.tracing then M.trace "apron" "may overflow: %a (%a, %a)\n" CilType.Exp.pretty exp (Pretty.docOpt (IntOps.BigIntOps.pretty ())) min_opt (Pretty.docOpt (IntOps.BigIntOps.pretty ())) max_opt; - raise (Unsupported_CilExp Overflow) - ); - expr - | exception (Cilfacade.TypeOfError _ as e) - | exception (Invalid_argument _ as e) -> - raise (Unsupported_CilExp (Exp_typeOf e)) + failwith "texpr1_expr_of_cil_exp: globals must be replaced with temporary locals" + | Const (CInt (i, _, _)) -> + Cst (Coeff.s_of_mpqf (Mpqf.of_mpz (Z_mlgmpidl.mpz_of_z i))) + | exp -> + match Cilfacade.get_ikind_exp exp with + | ik -> + let expr = + (** simplify asks for a constant value of some subexpression e, similar to a constant fold. In particular but not exclusively + this query is answered by the 2 var equalities domain itself. This normalizes arbitrary expressions to a point where they + might be able to be represented by means of 2 var equalities *) + let simplify e = + let ikind = try (Cilfacade.get_ikind_exp e) with Invalid_argument _ -> raise (Unsupported_CilExp Exp_not_supported) in + let simp = query e ikind in + let const = IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to ikind simp in + if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp/simplify: %a -> %a\n" d_plainexp e IntDomain.IntDomTuple.pretty simp; + BatOption.map_default (fun c -> Const (CInt (c, ikind, None))) e const + in + let texpr1 e = texpr1_expr_of_cil_exp (simplify e) in + let bop_near op e1 e2 = Binop (op, texpr1 e1, texpr1 e2, Int, Near) in + match exp with + | UnOp (Neg, e, _) -> Unop (Neg, texpr1 e, Int, Near) + | BinOp (PlusA, e1, e2, _) -> bop_near Add e1 e2 + | BinOp (MinusA, e1, e2, _) -> bop_near Sub e1 e2 + | BinOp (Mult, e1, e2, _) -> bop_near Mul e1 e2 + | BinOp (Mod, e1, e2, _) -> bop_near Mod e1 e2 + | BinOp (Div, e1, e2, _) -> + Binop (Div, texpr1 e1, texpr1 e2, Int, Zero) + | CastE (TInt (t_ik, _) as t, e) -> + begin match IntDomain.Size.is_cast_injective ~from_type:(Cilfacade.typeOf e) ~to_type:t with (* TODO: unnecessary cast check due to overflow check below? or maybe useful in general to also assume type bounds based on argument types? *) + | exception Invalid_argument _ -> raise (Unsupported_CilExp Exp_not_supported) + | true -> texpr1 e + | false -> (* Cast is not injective - we now try to establish suitable ranges manually *) + (* try to evaluate e by EvalInt Query *) + let res = try (query e @@ Cilfacade.get_ikind_exp e) with Invalid_argument _ -> raise (Unsupported_CilExp Exp_not_supported) in + (* convert response to a constant *) + let const = IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to t_ik res in + match const with + | Some c -> Cst (Coeff.s_of_mpqf (Mpqf.of_mpz (Z_mlgmpidl.mpz_of_z c))) (* Got a constant value -> use it straight away *) + (* I gotten top, we can not guarantee injectivity *) + | None -> if IntDomain.IntDomTuple.is_top_of t_ik res then raise (Unsupported_CilExp (Cast_not_injective t)) + else ( (* Got a ranged value different from top, so let's check bounds manually *) + let (ik_min, ik_max) = IntDomain.Size.range t_ik in + match IntDomain.IntDomTuple.minimal res, IntDomain.IntDomTuple.maximal res with + | Some min, Some max when min >= ik_min && max <= ik_max -> texpr1_expr_of_cil_exp e + | _ -> raise (Unsupported_CilExp (Cast_not_injective t))) + | exception Cilfacade.TypeOfError _ (* typeOf inner e, not outer exp *) + | exception Invalid_argument _ -> + raise (Unsupported_CilExp (Cast_not_injective t)) + end + | _ -> + raise (Unsupported_CilExp Exp_not_supported) + in + overflow_handling no_ov ik env expr d exp; + expr + | exception (Cilfacade.TypeOfError _ as e) + | exception (Invalid_argument _ as e) -> + raise (Unsupported_CilExp (Exp_typeOf e)) + in + texpr1_expr_of_cil_exp exp in - texpr1_expr_of_cil_exp exp + let exp = Cil.constFold false exp in + let res = conv exp in + if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp: %a -> %s (%b)\n" d_plainexp exp (Format.asprintf "%a" Texpr1.print_expr res) (Lazy.force no_ov); + res - let texpr1_of_cil_exp d env e no_ov = - let e = Cil.constFold false e in - Texpr1.of_expr env (texpr1_expr_of_cil_exp d env e no_ov) + let texpr1_of_cil_exp ask d env e no_ov = + let res = texpr1_expr_of_cil_exp ask d env e no_ov in + Texpr1.of_expr env res - let tcons1_of_cil_exp d env e negate no_ov = + let tcons1_of_cil_exp ask d env e negate no_ov = let e = Cil.constFold false e in let (texpr1_plus, texpr1_minus, typ) = match e with | BinOp (r, e1, e2, _) -> - let texpr1_1 = texpr1_expr_of_cil_exp d env e1 no_ov in - let texpr1_2 = texpr1_expr_of_cil_exp d env e2 no_ov in + let texpr1_1 = texpr1_expr_of_cil_exp ask d env e1 no_ov in + let texpr1_2 = texpr1_expr_of_cil_exp ask d env e2 no_ov in (* Apron constraints always compare with 0 and only have comparisons one way *) begin match r with | Lt -> (texpr1_2, texpr1_1, SUP) (* e1 < e2 ==> e2 - e1 > 0 *) @@ -178,12 +231,6 @@ struct let texpr1' = Binop (Sub, texpr1_plus, texpr1_minus, Int, Near) in Tcons1.make (Texpr1.of_expr env texpr1') typ - let find_one_var e = - Basetype.CilExp.get_vars e - |> List.filter Tracked.varinfo_tracked - |> function - | [v] -> Some v - | _ -> None end (** Conversion from Apron to CIL expressions. *) @@ -253,18 +300,130 @@ struct include CilOfApron (V) end -(** A more specific module type for RelationDomain.RelD2 with ConvBounds integrated and various apron elements. + +(* Abstraction for the domain representations of the relational analyses: + affineEqualityDomain (uses a matrix) and linearTwoVarEqualityDomain (uses an Array)*) +module type AbstractRelationalDomainRepresentation = +sig + type t + val equal : t -> t -> bool + val compare : t -> t -> int + val hash : t -> int + val empty : unit -> t + val copy : t -> t + val is_empty : t -> bool + val dim_add : Apron.Dim.change -> t -> t + val dim_remove : Apron.Dim.change -> t -> del:bool-> t +end + +(* Shared operations for the management of the Matrix or Array representations of the domains, + used by affineEqualityDomain and linearTwoVarEqualityDomain *) +module VarManagementOps (RelDomain : AbstractRelationalDomainRepresentation) = +struct + type t = { + mutable d : RelDomain.t option; + mutable env : Environment.t + } + [@@deriving eq, ord, hash] + + let empty_env = Environment.make [||] [||] + + let bot () = + {d = Some (RelDomain.empty ()); env = empty_env} + + let get_env t = t.env + let bot_env = {d = None; env = empty_env} + + let is_bot_env t = t.d = None + + let copy t = {t with d = Option.map RelDomain.copy t.d} + + let change_d t new_env ~add ~del = + if Environment.equal t.env new_env then + t + else + match t.d with + | None -> bot_env + | Some m -> + let dim_change = + if add then + Environment.dimchange t.env new_env + else + Environment.dimchange new_env t.env + in + {d = Some (if add then RelDomain.dim_add dim_change m else RelDomain.dim_remove dim_change m ~del:del); env = new_env} + + let change_d t new_env ~add ~del = VectorMatrix.timing_wrap "dimension change" (fun del -> change_d t new_env ~add:add ~del:del) del + + let vars x = Environment.ivars_only x.env + + let add_vars t vars = + let t = copy t in + let env' = Environment.add_vars t.env vars in + change_d t env' ~add:true ~del:false + + let add_vars t vars = VectorMatrix.timing_wrap "add_vars" (add_vars t) vars + + let drop_vars t vars ~del = + let t = copy t in + let env' = Environment.remove_vars t.env vars in + change_d t env' ~add:false ~del:del + + let drop_vars t vars = VectorMatrix.timing_wrap "drop_vars" (drop_vars t) vars + + let remove_vars t vars = drop_vars t vars ~del:false + + let remove_vars t vars = VectorMatrix.timing_wrap "remove_vars" (remove_vars t) vars + + let remove_vars_with t vars = + let t' = remove_vars t vars in + t.d <- t'.d; + t.env <- t'.env + + let remove_filter t f = + let env' = Environment.remove_filter t.env f in + change_d t env' ~add:false ~del:false + + let remove_filter t f = VectorMatrix.timing_wrap "remove_filter" (remove_filter t) f + + let remove_filter_with t f = + let t' = remove_filter t f in + t.d <- t'.d; + t.env <- t'.env + + let keep_filter t f = + let t = copy t in + let env' = Environment.keep_filter t.env f in + change_d t env' ~add:false ~del:false + + let keep_filter t f = VectorMatrix.timing_wrap "keep_filter" (keep_filter t) f + + let keep_vars t vs = + let t = copy t in + let env' = Environment.keep_vars t.env vs in + change_d t env' ~add:false ~del:false + + let keep_vars t vs = VectorMatrix.timing_wrap "keep_vars" (keep_vars t) vs + + let mem_var t var = Environment.mem_var t.env var + +end + + + +(** A more specific module type for RelationDomain.RelD2 with various apron elements. It is designed to be the interface for the D2 modules in affineEqualityDomain and apronDomain and serves as a functor argument for AssertionModule. *) module type AssertionRelS = sig type t - module Bounds: ConvBounds with type t = t + module Bounds: ConvBounds with type t = t val is_bot_env: t -> bool val env: t -> Environment.t - val assert_cons: t -> exp -> bool -> bool Lazy.t -> t + val assert_constraint: Queries.ask -> t -> exp -> bool -> bool Lazy.t -> t + val eval_interval : Queries.ask -> t -> Texpr1.t -> Z.t option * Z.t option end module Tracked: RelationDomain.Tracked = @@ -282,70 +441,84 @@ struct type_tracked vi.vtype && (not @@ GobConfig.get_bool "annotation.goblint_relation_track" || hasTrackAttribute vi.vattr) end -module AssertionModule (V: SV) (AD: AssertionRelS) = +module AssertionModule (V: SV) (AD: AssertionRelS) (Arg: ConvertArg) = struct include AD type nonrec var = V.t module Tracked = Tracked + module Convert = Convert (V) (Bounds) (Arg) (Tracked) - module Convert = Convert (V) (Bounds) (struct let allow_global = false end) (Tracked) - - let rec exp_is_cons = function + let rec exp_is_constraint = function (* constraint *) | BinOp ((Lt | Gt | Le | Ge | Eq | Ne), _, _, _) -> true - | BinOp ((LAnd | LOr), e1, e2, _) -> exp_is_cons e1 && exp_is_cons e2 - | UnOp (LNot,e,_) -> exp_is_cons e + | BinOp ((LAnd | LOr), e1, e2, _) -> exp_is_constraint e1 && exp_is_constraint e2 + | UnOp (LNot,e,_) -> exp_is_constraint e (* expression *) | _ -> false - (* TODO: move logic-handling assert_cons from Apron back to here, after fixing affeq bot-bot join *) + (* TODO: move logic-handling assert_constraint from Apron back to here, after fixing affeq bot-bot join *) (** Assert any expression. *) - let assert_inv d e negate no_ov = + let assert_inv ask d e negate no_ov = let e' = - if exp_is_cons e then + if exp_is_constraint e then e else (* convert non-constraint expression, such that we assert(e != 0) *) BinOp (Ne, e, zero, intType) in - assert_cons d e' negate no_ov + assert_constraint ask d e' negate no_ov - let check_assert d e no_ov = - if is_bot_env (assert_inv d e false no_ov) then + let check_assert ask d e no_ov = + if is_bot_env (assert_inv ask d e false no_ov) then `False - else if is_bot_env (assert_inv d e true no_ov) then + else if is_bot_env (assert_inv ask d e true no_ov) then `True else `Top (** Evaluate non-constraint expression as interval. *) - let eval_interval_expr d e = - match Convert.texpr1_of_cil_exp d (env d) e false with (* why implicit false no_ov false here? *) + let eval_interval_expr ask d e no_ov = + match Convert.texpr1_of_cil_exp ask d (env d) e no_ov with | texpr1 -> - Bounds.bound_texpr d texpr1 + eval_interval ask d texpr1 | exception Convert.Unsupported_CilExp _ -> (None, None) (** Evaluate constraint or non-constraint expression as integer. *) - let eval_int d e no_ov = + 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_cons %a = %B\n" d_plainexp e (exp_is_cons e); - if exp_is_cons e then - match check_assert d e no_ov with + if M.tracing then M.trace "relation" "eval_int: exp_is_constraint %a = %B\n" 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 - match eval_interval_expr d e with + match eval_interval_expr ask d e no_ov with | (Some min, Some max) -> ID.of_interval ~suppress_ovwarn:true ik (min, max) | (Some min, None) -> ID.starting ~suppress_ovwarn:true ik min | (None, Some max) -> ID.ending ~suppress_ovwarn:true ik max | (None, None) -> ID.top_of ik end + +(* Multi-precision rational numbers, defined by Apron. + Used by affineEqualityDomain and linearTwoVarEqualityDomain *) +module Mpqf = struct + include Mpqf + let compare = cmp + let zero = of_int 0 + let one = of_int 1 + let mone = of_int (-1) + + let get_den x = Z_mlgmpidl.z_of_mpzf @@ Mpqf.get_den x + + let get_num x = Z_mlgmpidl.z_of_mpzf @@ Mpqf.get_num x + let hash x = 31 * (Z.hash (get_den x)) + Z.hash (get_num x) +end diff --git a/src/cdomains/pthreadDomain.ml b/src/cdomains/pthreadDomain.ml index 8cef57bdbd..2c12689dcf 100644 --- a/src/cdomains/pthreadDomain.ml +++ b/src/cdomains/pthreadDomain.ml @@ -25,8 +25,7 @@ end module D = struct include Printable.StdLeaf - type domain = { tid : Tid.t; pred : Pred.t; ctx : Ctx.t } [@@deriving to_yojson] - type t = domain + type t = { tid : Tid.t; pred : Pred.t; ctx : Ctx.t } [@@deriving eq, ord, hash, to_yojson] (** printing *) let show x = @@ -36,28 +35,10 @@ module D = struct (Pred.show x.pred) (Ctx.show x.ctx) - include Printable.SimpleShow(struct type t = domain let show = show end) + include Printable.SimpleShow(struct type nonrec t = t let show = show end) (* TODO: overrides derived to_yojson *) let name () = "pthread state" - (** let equal = Util.equals *) - let equal x y = - Tid.equal x.tid y.tid && Pred.equal x.pred y.pred && Ctx.equal x.ctx y.ctx - - - (** compare all fields with correspoding compare operators *) - let compare x y = - List.fold_left - (fun acc v -> if acc = 0 && v <> 0 then v else acc) - 0 - [ Tid.compare x.tid y.tid - ; Pred.compare x.pred y.pred - ; Ctx.compare x.ctx y.ctx - ] - - - (** let hash = Hashtbl.hash *) - let hash x = Hashtbl.hash (Tid.hash x.tid, Pred.hash x.pred, Ctx.hash x.ctx) let make tid pred ctx = { tid; pred; ctx } let bot () = { tid = Tid.bot (); pred = Pred.bot (); ctx = Ctx.bot () } let is_bot x = Tid.is_bot x.tid && Pred.is_bot x.pred && Ctx.is_bot x.ctx diff --git a/src/cdomains/vectorMatrix.ml b/src/cdomains/vectorMatrix.ml index 64d5c5e35d..bfd623652c 100644 --- a/src/cdomains/vectorMatrix.ml +++ b/src/cdomains/vectorMatrix.ml @@ -137,8 +137,6 @@ sig val show: t -> string - val add_empty_column: t -> int -> t - val add_empty_columns: t -> int array -> t val append_row: t -> vec -> t @@ -313,15 +311,6 @@ module ArrayMatrix: AbstractMatrix = let copy m = timing_wrap "copy" (copy) m - let add_empty_column m n = - if is_empty m then m else - let nc = Array.length m.(0) in - if n > nc then failwith "n too large" else - let new_matrix = make_matrix (Array.length m) (Array.length m.(0) + 1) A.zero in - Array.iteri (fun i r -> if n = 0 then Array.blit r 0 new_matrix.(i) 1 (nc - 1) else - Array.blit r 0 new_matrix.(i) 0 n; if n <> nc then Array.blit r n new_matrix.(i) (n + 1) (nc - n)) m; - new_matrix - let add_empty_columns m cols = let nnc = Array.length cols in if is_empty m || nnc = 0 then m else diff --git a/src/common/util/intOps.ml b/src/common/util/intOps.ml index fa9a96f465..5138a3c158 100644 --- a/src/common/util/intOps.ml +++ b/src/common/util/intOps.ml @@ -83,7 +83,7 @@ end * -------------------------------------------------------------- *) module NIntOpsBase : IntOpsBase with type t = int = struct - type t = int [@@deriving hash] + type t = int [@@deriving eq, ord, hash] let name () = "int" let zero = 0 let one = 1 @@ -108,9 +108,6 @@ struct let logxor = (lxor) let lognot = (lnot) - - let compare = compare - let equal = Int.equal let top_range a b = (a = min_int) && (b = max_int) let max = Int.max let min = Int.min @@ -129,7 +126,7 @@ end module Int32OpsBase : IntOpsBase with type t = int32 = struct - type t = int32 [@@deriving hash] + type t = int32 [@@deriving eq, ord, hash] let name () = "int32" let zero = 0l let one = 1l @@ -155,9 +152,6 @@ struct let lognot = Int32.lognot (* Int32 calls bitwise operations 'log' *) - let compare = Int32.compare - let equal = Int32.equal - let top_range a b = (0 = compare a Int32.min_int) && (0 = compare b Int32.max_int) let max = Int32.max @@ -177,7 +171,7 @@ end module Int64OpsBase : IntOpsBase with type t = int64 = struct - type t = int64 [@@deriving hash] + type t = int64 [@@deriving eq, ord, hash] let name () = "int64" let zero = 0L let one = 1L @@ -203,9 +197,6 @@ struct let lognot = Int64.lognot (* Int64 calls bitwise operations 'log' *) - let compare = Int64.compare - let equal = Int64.equal - let top_range a b = (0 = compare a Int64.min_int) && (0 = compare b Int64.max_int) let max = Int64.max @@ -225,7 +216,7 @@ end module BigIntOpsBase : IntOpsBase with type t = Z.t = struct - type t = Z.t + type t = Z.t [@@deriving eq, ord, hash] let name () = "Z" let zero = Z.zero let one = Z.one @@ -241,9 +232,6 @@ struct let rem = Z.rem let gcd = Z.gcd - let compare = Z.compare - let equal = Z.equal - let hash = Z.hash let top_range _ _ = false diff --git a/src/domain/mapDomain.ml b/src/domain/mapDomain.ml index 5f3c324317..a62fcb98e4 100644 --- a/src/domain/mapDomain.ml +++ b/src/domain/mapDomain.ml @@ -110,8 +110,7 @@ struct module Group = struct - type t = D.group - let compare = D.compare_group + type t = D.group [@@deriving ord] end module GroupMap = Map.Make (Group) diff --git a/src/domains/queries.ml b/src/domains/queries.ml index f5fc832a9e..0733d40516 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -126,6 +126,7 @@ type _ t = | MustTermAllLoops: MustBool.t t | IsEverMultiThreaded: MayBool.t t | TmpSpecial: Mval.Exp.t -> ML.t t + | MaySignedOverflow: exp -> MayBool.t t type 'a result = 'a @@ -195,6 +196,7 @@ struct | MustTermAllLoops -> (module MustBool) | IsEverMultiThreaded -> (module MayBool) | TmpSpecial _ -> (module ML) + | MaySignedOverflow _ -> (module MayBool) (** Get bottom result for query. *) let bot (type a) (q: a t): a result = @@ -263,6 +265,7 @@ struct | MustTermAllLoops -> MustBool.top () | IsEverMultiThreaded -> MayBool.top () | TmpSpecial _ -> ML.top () + | MaySignedOverflow _ -> MayBool.top () end (* The type any_query can't be directly defined in Any as t, @@ -328,6 +331,7 @@ struct | Any IsEverMultiThreaded -> 55 | Any (TmpSpecial _) -> 56 | Any (IsAllocVar _) -> 57 + | Any (MaySignedOverflow _) -> 58 let rec compare a b = let r = Stdlib.compare (order a) (order b) in @@ -381,6 +385,7 @@ struct | Any (MayBeModifiedSinceSetjmp e1), Any (MayBeModifiedSinceSetjmp e2) -> JmpBufDomain.BufferEntry.compare e1 e2 | Any (MustBeSingleThreaded {since_start=s1;}), Any (MustBeSingleThreaded {since_start=s2;}) -> Stdlib.compare s1 s2 | Any (TmpSpecial lv1), Any (TmpSpecial lv2) -> Mval.Exp.compare lv1 lv2 + | Any (MaySignedOverflow e1), Any (MaySignedOverflow e2) -> CilType.Exp.compare e1 e2 (* only argumentless queries should remain *) | _, _ -> Stdlib.compare (order a) (order b) @@ -422,6 +427,7 @@ struct | Any (MayBeModifiedSinceSetjmp e) -> JmpBufDomain.BufferEntry.hash e | Any (MustBeSingleThreaded {since_start}) -> Hashtbl.hash since_start | Any (TmpSpecial lv) -> Mval.Exp.hash lv + | Any (MaySignedOverflow e) -> CilType.Exp.hash e (* IterSysVars: *) (* - argument is a function and functions cannot be compared in any meaningful way. *) (* - doesn't matter because IterSysVars is always queried from outside of the analysis, so MCP's query caching is not done for it. *) @@ -484,6 +490,7 @@ struct | Any MustTermAllLoops -> Pretty.dprintf "MustTermAllLoops" | Any IsEverMultiThreaded -> Pretty.dprintf "IsEverMultiThreaded" | Any (TmpSpecial lv) -> Pretty.dprintf "TmpSpecial %a" Mval.Exp.pretty lv + | Any (MaySignedOverflow e) -> Pretty.dprintf "MaySignedOverflow %a" CilType.Exp.pretty e end let to_value_domain_ask (ask: ask) = diff --git a/src/dune b/src/dune index e7226466ad..f3a7636b78 100644 --- a/src/dune +++ b/src/dune @@ -35,6 +35,14 @@ (apron -> affineEqualityDomain.apron.ml) (-> affineEqualityDomain.no-apron.ml) ) + (select linearTwoVarEqualityAnalysis.ml from + (apron -> linearTwoVarEqualityAnalysis.apron.ml) + (-> linearTwoVarEqualityAnalysis.no-apron.ml) + ) + (select linearTwoVarEqualityDomain.ml from + (apron -> linearTwoVarEqualityDomain.apron.ml) + (-> linearTwoVarEqualityDomain.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 e06cc8fa08..62abcbcb60 100644 --- a/src/goblint_lib.ml +++ b/src/goblint_lib.ml @@ -76,6 +76,7 @@ module Base = Base module RelationAnalysis = RelationAnalysis module ApronAnalysis = ApronAnalysis module AffineEqualityAnalysis = AffineEqualityAnalysis +module LinearTwoVarEqualityAnalysis = LinearTwoVarEqualityAnalysis module VarEq = VarEq module CondVars = CondVars module TmpSpecial = TmpSpecial @@ -240,6 +241,7 @@ module ValueDomainQueries = ValueDomainQueries module RelationDomain = RelationDomain module ApronDomain = ApronDomain module AffineEqualityDomain = AffineEqualityDomain +module LinearTwoVarEqualityDomain = LinearTwoVarEqualityDomain (** {3 Concurrency} *) diff --git a/src/incremental/compareCIL.ml b/src/incremental/compareCIL.ml index befaee6c58..ea22e02a56 100644 --- a/src/incremental/compareCIL.ml +++ b/src/incremental/compareCIL.ml @@ -29,8 +29,7 @@ let get_varinfo gc = match gc.decls, gc.def with module GlobalColMap = Map.Make( struct - type t = global_col - let compare = compare_global_col + type t = global_col [@@deriving ord] end) let name_of_global g = match g with diff --git a/src/util/std/gobArray.ml b/src/util/std/gobArray.ml new file mode 100644 index 0000000000..c88e3d8184 --- /dev/null +++ b/src/util/std/gobArray.ml @@ -0,0 +1,30 @@ +open BatArray + +(** Implementations here are from batteries and slightly modified. They are tuned for performance and not necessarily the same style non-library code should be written. *) + +let existsi p xs = + let n = length xs in + let rec loop i = + if i = n then false + else if p i (unsafe_get xs i) then true + else loop (succ i) + in + loop 0 + +let for_alli p xs = + let n = length xs in + let rec loop i = + if i = n then true + else if p i (unsafe_get xs i) then loop (succ i) + else false + in + loop 0 + +let count_matchingi p xs = + let n = length xs in + let count = ref 0 in + for i = 0 to n - 1 do + if p i (unsafe_get xs i) then + incr count + done; + !count diff --git a/src/util/std/gobFpath.ml b/src/util/std/gobFpath.ml index cd09657e77..dfe7b3fb9d 100644 --- a/src/util/std/gobFpath.ml +++ b/src/util/std/gobFpath.ml @@ -1,7 +1,5 @@ -type t = Fpath.t [@@deriving show] +type t = Fpath.t [@@deriving eq, ord, show] -let equal = Fpath.equal -let compare = Fpath.compare let hash p = Hashtbl.hash (Fpath.to_string p) let pretty () p = GoblintCil.Pretty.text (Fpath.to_string p) diff --git a/src/util/std/gobOption.ml b/src/util/std/gobOption.ml index 3602575317..55597a8e50 100644 --- a/src/util/std/gobOption.ml +++ b/src/util/std/gobOption.ml @@ -6,6 +6,10 @@ let for_all p = function | Some x -> p x | None -> true +let map2 binop opt1 opt2 = + match opt1, opt2 with + | Some x1, Some x2 -> Some (binop x1 x2) + | _ -> None (** Open this to use applicative functor/monad syntax for {!option}. *) module Syntax = diff --git a/src/util/std/goblint_std.ml b/src/util/std/goblint_std.ml index 0d548cac08..5b623ead30 100644 --- a/src/util/std/goblint_std.ml +++ b/src/util/std/goblint_std.ml @@ -4,6 +4,7 @@ OCaml standard library extensions which are not provided by {!Batteries}. *) +module GobArray = GobArray module GobGc = GobGc module GobHashtbl = GobHashtbl module GobList = GobList diff --git a/src/witness/argTools.ml b/src/witness/argTools.ml index 2d65911a5f..7ec9dfbfc8 100644 --- a/src/witness/argTools.ml +++ b/src/witness/argTools.ml @@ -62,19 +62,7 @@ struct module Node = struct - type t = MyCFG.node * Spec.C.t * int - - let equal (n1, c1, i1) (n2, c2, i2) = - EQSys.LVar.equal (n1, c1) (n2, c2) && i1 = i2 - - let compare (n1, c1, i1) (n2, c2, i2) = - let r = EQSys.LVar.compare (n1, c1) (n2, c2) in - if r <> 0 then - r - else - Int.compare i1 i2 - - let hash (n, c, i) = 31 * EQSys.LVar.hash (n, c) + i + type t = Node.t * Spec.C.t * int [@@deriving eq, ord, hash] let cfgnode (n, c, i) = n let context_id (n, c, i) = Spec.C.tag c diff --git a/tests/regression/46-apron2/01-realfixpoint.c b/tests/regression/46-apron2/01-realfixpoint.c new file mode 100644 index 0000000000..ca39a074a3 --- /dev/null +++ b/tests/regression/46-apron2/01-realfixpoint.c @@ -0,0 +1,18 @@ +// SKIP PARAM: --set ana.base.arrays.domain partitioned --enable ana.int.interval --set ana.activated[+] apron +#include +int main () +{ + char A [3]; + + A[2] = 0; + + char *str = A; + int i = 0; + + while (str[i] != 0) { + __goblint_check(1); // reachable + i++; + } + + return 0; +} diff --git a/tests/regression/46-apron2/81-overflow-caching.c b/tests/regression/46-apron2/81-overflow-caching.c new file mode 100644 index 0000000000..720e63877c --- /dev/null +++ b/tests/regression/46-apron2/81-overflow-caching.c @@ -0,0 +1,17 @@ +// SKIP PARAM: --set ana.activated[+] apron --set ana.relation.privatization top + +#include +#include + + int num = 1; + + +int main() { + + while(num > 0) + num++; // Here num overflows + + __goblint_check(1); // reachable + + return 0; +} diff --git a/tests/regression/46-apron2/82-fixpoint-not-reached.c b/tests/regression/46-apron2/82-fixpoint-not-reached.c new file mode 100644 index 0000000000..582734025b --- /dev/null +++ b/tests/regression/46-apron2/82-fixpoint-not-reached.c @@ -0,0 +1,7 @@ +//PARAM: --set sem.int.signed_overflow assume_none --set ana.activated[+] apron + +int main() { + int minInt = -2147483647 + -1; + int x = (minInt + -1) +1; + return 0; +} \ No newline at end of file diff --git a/tests/regression/46-apron2/83-reachable_bodies.c b/tests/regression/46-apron2/83-reachable_bodies.c new file mode 100644 index 0000000000..3157df2eca --- /dev/null +++ b/tests/regression/46-apron2/83-reachable_bodies.c @@ -0,0 +1,26 @@ +// SKIP PARAM: --set ana.base.arrays.domain partitioned --enable ana.int.interval --set ana.activated[+] apron +#include +int main () +{ + char A [3]; + + A[2] = 0; + + char *str = A; + int i = 0; + + if (str[i] != 0) { + __goblint_check(1); // reachable + i++; + } + if (str[i] != 0) { + __goblint_check(1); // reachable + i++; + } + if (str[i] != 0) { + __goblint_check(1); // reachable + i++; + } + + return 0; +} diff --git a/tests/regression/63-affeq/20-svcomp-signextension.c b/tests/regression/63-affeq/20-svcomp-signextension.c new file mode 100644 index 0000000000..15c8def185 --- /dev/null +++ b/tests/regression/63-affeq/20-svcomp-signextension.c @@ -0,0 +1,25 @@ +// SKIP PARAM: --set ana.activated[+] affeq --set sem.int.signed_overflow assume_none +#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/77-lin2vareq/01-loop.c b/tests/regression/77-lin2vareq/01-loop.c new file mode 100644 index 0000000000..703b6b0bbb --- /dev/null +++ b/tests/regression/77-lin2vareq/01-loop.c @@ -0,0 +1,23 @@ +//SKIP PARAM: --set ana.activated[+] lin2vareq --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/77-lin2vareq/02-iteration.c b/tests/regression/77-lin2vareq/02-iteration.c new file mode 100644 index 0000000000..f960b144fe --- /dev/null +++ b/tests/regression/77-lin2vareq/02-iteration.c @@ -0,0 +1,17 @@ +//SKIP PARAM: --set ana.activated[+] lin2vareq +#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/77-lin2vareq/03-loop_increment.c b/tests/regression/77-lin2vareq/03-loop_increment.c new file mode 100644 index 0000000000..b5b1b965ab --- /dev/null +++ b/tests/regression/77-lin2vareq/03-loop_increment.c @@ -0,0 +1,21 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq --set sem.int.signed_overflow assume_none +#include + +int main() { + int i, j, k; + int size = 5; + i = 0; + j = 0; + k = 5; + + 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/77-lin2vareq/04-complicated_expression.c b/tests/regression/77-lin2vareq/04-complicated_expression.c new file mode 100644 index 0000000000..02f17d16ab --- /dev/null +++ b/tests/regression/77-lin2vareq/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 + +#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/77-lin2vareq/05-overflow.c b/tests/regression/77-lin2vareq/05-overflow.c new file mode 100644 index 0000000000..c9d820c64f --- /dev/null +++ b/tests/regression/77-lin2vareq/05-overflow.c @@ -0,0 +1,23 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq + +#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/77-lin2vareq/06-join-non-constant.c b/tests/regression/77-lin2vareq/06-join-non-constant.c new file mode 100644 index 0000000000..c5e93e0b54 --- /dev/null +++ b/tests/regression/77-lin2vareq/06-join-non-constant.c @@ -0,0 +1,25 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq --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/77-lin2vareq/07-coeff_vec.c b/tests/regression/77-lin2vareq/07-coeff_vec.c new file mode 100644 index 0000000000..86e6aa121c --- /dev/null +++ b/tests/regression/77-lin2vareq/07-coeff_vec.c @@ -0,0 +1,22 @@ +//SKIP PARAM: --set ana.activated[+] lin2vareq +// 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/77-lin2vareq/08-partitioning.c b/tests/regression/77-lin2vareq/08-partitioning.c new file mode 100644 index 0000000000..3d6463af8b --- /dev/null +++ b/tests/regression/77-lin2vareq/08-partitioning.c @@ -0,0 +1,39 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq --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/77-lin2vareq/09-loop_relational.c b/tests/regression/77-lin2vareq/09-loop_relational.c new file mode 100644 index 0000000000..0254d00dc9 --- /dev/null +++ b/tests/regression/77-lin2vareq/09-loop_relational.c @@ -0,0 +1,22 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq --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/77-lin2vareq/10-linear_loop.c b/tests/regression/77-lin2vareq/10-linear_loop.c new file mode 100644 index 0000000000..96f46217c6 --- /dev/null +++ b/tests/regression/77-lin2vareq/10-linear_loop.c @@ -0,0 +1,21 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq --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/77-lin2vareq/11-overflow_ignored.c b/tests/regression/77-lin2vareq/11-overflow_ignored.c new file mode 100644 index 0000000000..d3e6ebf069 --- /dev/null +++ b/tests/regression/77-lin2vareq/11-overflow_ignored.c @@ -0,0 +1,27 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq --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/77-lin2vareq/12-bounds_guards_ov.c b/tests/regression/77-lin2vareq/12-bounds_guards_ov.c new file mode 100644 index 0000000000..c66d4f3b06 --- /dev/null +++ b/tests/regression/77-lin2vareq/12-bounds_guards_ov.c @@ -0,0 +1,19 @@ +//SKIP PARAM: --set ana.activated[+] lin2vareq +// 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/77-lin2vareq/13-meet-tcons.c b/tests/regression/77-lin2vareq/13-meet-tcons.c new file mode 100644 index 0000000000..79cbf2ed81 --- /dev/null +++ b/tests/regression/77-lin2vareq/13-meet-tcons.c @@ -0,0 +1,15 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq --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/77-lin2vareq/14-function-call.c b/tests/regression/77-lin2vareq/14-function-call.c new file mode 100644 index 0000000000..12815e4626 --- /dev/null +++ b/tests/regression/77-lin2vareq/14-function-call.c @@ -0,0 +1,19 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq --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/77-lin2vareq/15-join_all_cases.c b/tests/regression/77-lin2vareq/15-join_all_cases.c new file mode 100644 index 0000000000..69ba5d9aa3 --- /dev/null +++ b/tests/regression/77-lin2vareq/15-join_all_cases.c @@ -0,0 +1,31 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq --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/77-lin2vareq/16-sum-of-two-vars.c b/tests/regression/77-lin2vareq/16-sum-of-two-vars.c new file mode 100644 index 0000000000..1bcc6ed446 --- /dev/null +++ b/tests/regression/77-lin2vareq/16-sum-of-two-vars.c @@ -0,0 +1,24 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq --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/77-lin2vareq/17-svcomp-signextension.c b/tests/regression/77-lin2vareq/17-svcomp-signextension.c new file mode 100644 index 0000000000..cf2f0bdabc --- /dev/null +++ b/tests/regression/77-lin2vareq/17-svcomp-signextension.c @@ -0,0 +1,28 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq --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/77-lin2vareq/18-forget_var.c b/tests/regression/77-lin2vareq/18-forget_var.c new file mode 100644 index 0000000000..7fd40e5c61 --- /dev/null +++ b/tests/regression/77-lin2vareq/18-forget_var.c @@ -0,0 +1,16 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq --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/77-lin2vareq/19-cast-to-short.c b/tests/regression/77-lin2vareq/19-cast-to-short.c new file mode 100644 index 0000000000..d1e3f857d7 --- /dev/null +++ b/tests/regression/77-lin2vareq/19-cast-to-short.c @@ -0,0 +1,29 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq --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/77-lin2vareq/20-function_call2.c b/tests/regression/77-lin2vareq/20-function_call2.c new file mode 100644 index 0000000000..f406862b74 --- /dev/null +++ b/tests/regression/77-lin2vareq/20-function_call2.c @@ -0,0 +1,21 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq --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/77-lin2vareq/21-global-variables.c b/tests/regression/77-lin2vareq/21-global-variables.c new file mode 100644 index 0000000000..a8cf6ba6a3 --- /dev/null +++ b/tests/regression/77-lin2vareq/21-global-variables.c @@ -0,0 +1,21 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq --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/77-lin2vareq/22-cast-to-short2.c b/tests/regression/77-lin2vareq/22-cast-to-short2.c new file mode 100644 index 0000000000..d33098712a --- /dev/null +++ b/tests/regression/77-lin2vareq/22-cast-to-short2.c @@ -0,0 +1,29 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq --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/77-lin2vareq/23-function-return-value.c b/tests/regression/77-lin2vareq/23-function-return-value.c new file mode 100644 index 0000000000..5efae1873d --- /dev/null +++ b/tests/regression/77-lin2vareq/23-function-return-value.c @@ -0,0 +1,18 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq --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/77-lin2vareq/24-narrowing-on-steroids.c b/tests/regression/77-lin2vareq/24-narrowing-on-steroids.c new file mode 100644 index 0000000000..3d4bfb0234 --- /dev/null +++ b/tests/regression/77-lin2vareq/24-narrowing-on-steroids.c @@ -0,0 +1,29 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq --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/77-lin2vareq/25-different_types.c b/tests/regression/77-lin2vareq/25-different_types.c new file mode 100644 index 0000000000..3439b406cd --- /dev/null +++ b/tests/regression/77-lin2vareq/25-different_types.c @@ -0,0 +1,31 @@ +// PARAM: --set ana.activated[+] lin2vareq +#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/77-lin2vareq/26-termination-overflow.c b/tests/regression/77-lin2vareq/26-termination-overflow.c new file mode 100644 index 0000000000..81c6d90828 --- /dev/null +++ b/tests/regression/77-lin2vareq/26-termination-overflow.c @@ -0,0 +1,13 @@ +// SKIP TERM PARAM: --set "ana.activated[+]" lin2vareq + +#include + +int main() { + int i = 2147483647; + i++; + while (i <= 10) { + printf("%d\n", i); + } + + return 0; +} diff --git a/tests/regression/77-lin2vareq/27-overflow-unknown.c b/tests/regression/77-lin2vareq/27-overflow-unknown.c new file mode 100644 index 0000000000..40e073d9fb --- /dev/null +++ b/tests/regression/77-lin2vareq/27-overflow-unknown.c @@ -0,0 +1,19 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq +#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/77-lin2vareq/28-overflow-on-steroids.c b/tests/regression/77-lin2vareq/28-overflow-on-steroids.c new file mode 100644 index 0000000000..b8275bac2f --- /dev/null +++ b/tests/regression/77-lin2vareq/28-overflow-on-steroids.c @@ -0,0 +1,43 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq --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/77-lin2vareq/29-meet-tcons-on-steroids.c b/tests/regression/77-lin2vareq/29-meet-tcons-on-steroids.c new file mode 100644 index 0000000000..501db8ee25 --- /dev/null +++ b/tests/regression/77-lin2vareq/29-meet-tcons-on-steroids.c @@ -0,0 +1,19 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq --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/77-lin2vareq/30-cast-non-int.c b/tests/regression/77-lin2vareq/30-cast-non-int.c new file mode 100644 index 0000000000..0c7f100f81 --- /dev/null +++ b/tests/regression/77-lin2vareq/30-cast-non-int.c @@ -0,0 +1,11 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq --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/77-lin2vareq/31-careful.c b/tests/regression/77-lin2vareq/31-careful.c new file mode 100644 index 0000000000..dec0525cf0 --- /dev/null +++ b/tests/regression/77-lin2vareq/31-careful.c @@ -0,0 +1,22 @@ +// SKIP PARAM: --set ana.activated[+] lin2vareq --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 + __goblint_check(j == i-1); //UNKNOWN + __goblint_check(j == i + UINT_MAX); //UNKNOWN +} diff --git a/tests/regression/77-lin2vareq/dune b/tests/regression/77-lin2vareq/dune new file mode 100644 index 0000000000..b4cede7223 --- /dev/null +++ b/tests/regression/77-lin2vareq/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)))) \ No newline at end of file