diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index eb4c6f48c7..e676f3878f 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -866,6 +866,47 @@ sig include AtomicParam end +module P = +struct + include MustVars + let name () = "P" +end + +module Sigma' = +struct + include CPA + let name () = "Protected Changes" +end + +module type ProtectionDom = +sig + include Lattice.S + val add: bool -> varinfo -> VD.t -> t -> t + val remove: varinfo -> t -> t + val precise_side: varinfo -> VD.t -> t -> VD.t option + val empty: unit -> t + val getP: t -> P.t +end + +module ProtectionCPASide: ProtectionDom = +struct + include P + + let add _ x _ t = P.add x t + let precise_side x v t = Some v + let getP t = t +end + +module ProtectionChangesOnlySide: ProtectionDom = +struct + include Lattice.Prod (P) (Sigma') + let add invariant x v t = P.add x @@ fst t, if not invariant then Sigma'.add x v @@ snd t else snd t + let remove x t = P.remove x @@ fst t, Sigma'.remove x @@ snd t + let precise_side x v t = Sigma'.find_opt x @@ snd t + let empty () = P.empty (), Sigma'.empty () + let getP t = fst t +end + (** Protection-Based Reading. *) module ProtectionBasedV = struct module VUnprot = @@ -887,30 +928,24 @@ module ProtectionBasedV = struct end (** Protection-Based Reading. *) -module ProtectionBasedPriv (Param: PerGlobalPrivParam)(Wrapper:PrivatizationWrapper): S = +module ProtectionBasedPriv (D: ProtectionDom) (Param: PerGlobalPrivParam)(Wrapper:PrivatizationWrapper): S = struct include NoFinalize include ConfCheck.RequireMutexActivatedInit open Protection - module P = - struct - include MustVars - let name () = "P" - end - (* W is implicitly represented by CPA domain *) - module D = P + module D = D module Wrapper = Wrapper (VD) module G = Wrapper.G module V = ProtectionBasedV.V - let startstate () = P.empty () + let startstate () = D.empty () let read_global (ask: Queries.ask) getg (st: BaseComponents (D).t) x = let getg = Wrapper.getg ask getg in - if P.mem x st.priv then + if P.mem x @@ D.getP st.priv then CPA.find x st.cpa else if Param.handle_atomic && ask.f MustBeAtomic then VD.join (CPA.find x st.cpa) (getg (V.unprotected x)) (* Account for previous unpublished unprotected writes in current atomic section. *) @@ -921,6 +956,7 @@ struct let write_global ?(invariant=false) (ask: Queries.ask) getg sideg (st: BaseComponents (D).t) x v = let sideg = Wrapper.sideg ask sideg in + let unprotected = is_unprotected ask x in if not invariant then ( if not (Param.handle_atomic && ask.f MustBeAtomic) then sideg (V.unprotected x) v; (* Delay publishing unprotected write in the atomic section. *) @@ -929,11 +965,11 @@ struct (* Unlock after invariant will still side effect refined value (if protected) from CPA, because cannot distinguish from non-invariant write since W is implicit. *) ); if Param.handle_atomic && ask.f MustBeAtomic then - {st with cpa = CPA.add x v st.cpa; priv = P.add x st.priv} (* Keep write local as if it were protected by the atomic section. *) - else if is_unprotected ask x then + {st with cpa = CPA.add x v st.cpa; priv = D.add invariant x v st.priv} (* Keep write local as if it were protected by the atomic section. *) + else if unprotected then st else - {st with cpa = CPA.add x v st.cpa; priv = P.add x st.priv} + {st with cpa = CPA.add x v st.cpa; priv = D.add invariant x v st.priv} let lock ask getg st m = st @@ -943,16 +979,22 @@ struct (* TODO: what about G_m globals in cpa that weren't actually written? *) CPA.fold (fun x v (st: BaseComponents (D).t) -> if is_protected_by ask m x then ( (* is_in_Gm *) - (* Extra precision in implementation to pass tests: - If global is read-protected by multiple locks, - then inner unlock shouldn't yet publish. *) - if not Param.check_read_unprotected || is_unprotected_without ask ~write:false x m then - sideg (V.protected x) v; - if atomic then - sideg (V.unprotected x) v; (* Publish delayed unprotected write as if it were protected by the atomic section. *) - + (* Only apply sides for values that were actually written to globals! + This excludes invariants inferred through guards. *) + begin match D.precise_side x v st.priv with + | Some v -> begin + (* Extra precision in implementation to pass tests: + If global is read-protected by multiple locks, + then inner unlock shouldn't yet publish. *) + if not Param.check_read_unprotected || is_unprotected_without ask ~write:false x m then + sideg (V.protected x) v; + if atomic then + sideg (V.unprotected x) v; (* Publish delayed unprotected write as if it were protected by the atomic section. *) + end + | None -> () + end; if is_unprotected_without ask x m then (* is_in_V' *) - {st with cpa = CPA.remove x st.cpa; priv = P.remove x st.priv} + {st with cpa = CPA.remove x st.cpa; priv = D.remove x st.priv} else st ) @@ -968,7 +1010,7 @@ struct if is_global ask x && is_unprotected ask x then ( sideg (V.unprotected x) v; sideg (V.protected x) v; (* must be like enter_multithreaded *) - {st with cpa = CPA.remove x st.cpa; priv = P.remove x st.priv} + {st with cpa = CPA.remove x st.cpa; priv = D.remove x st.priv} ) else st @@ -1007,7 +1049,7 @@ struct if is_global ask x then ( sideg (V.unprotected x) v; sideg (V.protected x) v; - {st with cpa = CPA.remove x st.cpa; priv = P.remove x st.priv} + {st with cpa = CPA.remove x st.cpa; priv = D.remove x st.priv} ) else st @@ -2116,6 +2158,8 @@ end let priv_module: (module S) Lazy.t = lazy ( + let changes_only = get_bool "ana.base.priv.protection.changes-only" in + let module ProtDom: ProtectionDom = (val if changes_only then (module ProtectionChangesOnlySide : ProtectionDom) else (module ProtectionCPASide)) in let module Priv: S = (val match get_string "ana.base.privatization" with | "none" -> (module NonePriv: S) @@ -2123,12 +2167,12 @@ let priv_module: (module S) Lazy.t = | "mutex-oplus" -> (module PerMutexOplusPriv) | "mutex-meet" -> (module PerMutexMeetPriv) | "mutex-meet-tid" -> (module PerMutexMeetTIDPriv (ThreadDigest)) - | "protection" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false let handle_atomic = false end)(NoWrapper)) - | "protection-tid" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false let handle_atomic = false end)(DigestWrapper(ThreadNotStartedDigest))) - | "protection-atomic" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false let handle_atomic = true end)(NoWrapper)) (* experimental *) - | "protection-read" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true let handle_atomic = false end)(NoWrapper)) - | "protection-read-tid" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true let handle_atomic = false end)(DigestWrapper(ThreadNotStartedDigest))) - | "protection-read-atomic" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true let handle_atomic = true end)(NoWrapper)) (* experimental *) + | "protection" -> (module ProtectionBasedPriv (ProtDom) (struct let check_read_unprotected = false let handle_atomic = false end)(NoWrapper)) + | "protection-tid" -> (module ProtectionBasedPriv (ProtDom) (struct let check_read_unprotected = false let handle_atomic = false end)(DigestWrapper(ThreadNotStartedDigest))) + | "protection-atomic" -> (module ProtectionBasedPriv (ProtDom) (struct let check_read_unprotected = false let handle_atomic = true end)(NoWrapper)) (* experimental *) + | "protection-read" -> (module ProtectionBasedPriv (ProtDom) (struct let check_read_unprotected = true let handle_atomic = false end)(NoWrapper)) + | "protection-read-tid" -> (module ProtectionBasedPriv (ProtDom) (struct let check_read_unprotected = true let handle_atomic = false end)(DigestWrapper(ThreadNotStartedDigest))) + | "protection-read-atomic" -> (module ProtectionBasedPriv (ProtDom) (struct let check_read_unprotected = true let handle_atomic = true end)(NoWrapper)) (* experimental *) | "mine" -> (module MinePriv) | "mine-nothread" -> (module MineNoThreadPriv) | "mine-W" -> (module MineWPriv (struct let side_effect_global_init = true end)) diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 8d4ba6c472..1c02d51deb 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -790,6 +790,20 @@ "title": "ana.base.priv", "type": "object", "properties": { + "protection": { + "title": "ana.base.priv.protection", + "description": "Options for protection based privatization schemes.", + "type": "object", + "properties": { + "changes-only": { + "title": "ana.base.priv.protection.changes-only", + "description": "Only propagate changes to globals on unlock, don't side the full value of the privatized global.", + "type": "boolean", + "default": false + } + }, + "additionalProperties": false + }, "not-started": { "title": "ana.base.priv.not-started", "description": @@ -2474,6 +2488,43 @@ "type": "boolean", "default": true }, + "narrow-globs": { + "title": "solvers.td3.narrow-globs", + "type": "object", + "properties": { + "enabled": { + "title": "solvers.td3.narrow-globs.enabled", + "description": "Individually track side-effects from different unknowns to enable narrowing of globals.", + "type": "boolean", + "default": false + }, + "conservative-widen": { + "title": "solvers.td3.narrow-globs.conservative-widen", + "description": "Controls when to widen divided sides. true: Only widen on a side-effect, if joining would affect the overall value of the global. false: Always widen increasing/incomparable side-effects", + "type": "boolean", + "default": true + }, + "immediate-growth": { + "title": "solvers.td3.narrow-globs.immediate-growth", + "description": "Controls when growing side-effects are applied. true: immediately when they are triggered. false: after the source unknown has been fully evaluated", + "type": "boolean", + "default": true + }, + "narrow-gas": { + "title": "solvers.td3.narrow-globs.narrow-gas", + "description": "Limits the number of times a side-effect can switch from widening to narrowing to enforce termination. 0 disables narrowing, -1 allows narrowing infinitely often.", + "type": "integer", + "default": 5 + }, + "eliminate-dead": { + "title": "solvers.td3.narrow-globs.eliminate-dead", + "description": "side-effects that no longer occur are narrowed with bot.", + "type": "boolean", + "default": false + } + }, + "additionalProperties": false + }, "remove-wpoint": { "title": "solvers.td3.remove-wpoint", "description": "Remove widening points after narrowing phase. Enables a form of local restarting which increases precision of nested loops.", diff --git a/src/constraint/constrSys.ml b/src/constraint/constrSys.ml index 60859f1ccb..9800c5c015 100644 --- a/src/constraint/constrSys.ml +++ b/src/constraint/constrSys.ml @@ -46,8 +46,12 @@ sig (** The system in functional form. *) val system : v -> ((v -> d) -> (v -> d -> unit) -> d) m - val sys_change: (v -> d) -> v sys_change_info (** Compute incremental constraint system change from old solution. *) + val sys_change: (v -> d) -> v sys_change_info + + (** List of unknowns that should be queried again when the argument unknown has shrunk to bot, to eagerly trigger (analysis-time!) abstract garbage collection idependently of reach-based pruning at the end. + @see Stemmler, F., Schwarz, M., Erhard, J., Tilscher, S., Seidl, H. Taking out the Toxic Trash: Recovering Precision in Mixed Flow-Sensitive Static Analyses *) + val postmortem: v -> v list end (** Any system of side-effecting equations over lattices. *) @@ -64,6 +68,7 @@ sig val system : LVar.t -> ((LVar.t -> D.t) -> (LVar.t -> D.t -> unit) -> (GVar.t -> G.t) -> (GVar.t -> G.t -> unit) -> D.t) option val iter_vars: (LVar.t -> D.t) -> (GVar.t -> G.t) -> VarQuery.t -> LVar.t VarQuery.f -> GVar.t VarQuery.f -> unit val sys_change: (LVar.t -> D.t) -> (GVar.t -> G.t) -> [`L of LVar.t | `G of GVar.t] sys_change_info + val postmortem: LVar.t -> LVar.t list end (** A solver is something that can translate a system into a solution (hash-table). @@ -205,6 +210,10 @@ struct let sys_change get = S.sys_change (getL % get % l) (getG % get % g) + + let postmortem = function + | `L g -> List.map (fun x -> `L x) @@ S.postmortem g + | _ -> [] end (** Splits a [EqConstrSys] solution into a [GlobConstrSys] solution with given [Hashtbl.S] for the [EqConstrSys]. *) diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 4c32b286c8..968c2acdba 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -549,4 +549,8 @@ struct in {obsolete; delete; reluctant; restart} + + let postmortem = function + | FunctionEntry fd, c -> [(Function fd, c)] + | _ -> [] end diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 70b7f04f4f..ad04fbf3aa 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -141,6 +141,8 @@ let check_arguments () = if get_bool "ana.base.context.int" && not (get_bool "ana.base.context.non-ptr") then (set_bool "ana.base.context.int" false; warn "ana.base.context.int implicitly disabled by ana.base.context.non-ptr"); (* order matters: non-ptr=false, int=true -> int=false cascades to interval=false with warning *) if get_bool "ana.base.context.interval" && not (get_bool "ana.base.context.int") then (set_bool "ana.base.context.interval" false; warn "ana.base.context.interval implicitly disabled by ana.base.context.int"); + if get_bool "ana.base.priv.protection.changes-only" && not @@ List.mem (get_string "ana.base.privatization") ["protection"; "protection-tid"; "protection-atomic"; "protection-read"; "protection-read-tid"; "protection-read-atomic"] then + warn "ana.base.priv.protection.changes-only requires ana.base.privatization to be protection based"; if get_bool "incremental.only-rename" then (set_bool "incremental.load" true; warn "incremental.only-rename implicitly activates incremental.load. Previous AST is loaded for diff and rename, but analyis results are not reused."); if get_bool "incremental.restart.sided.enabled" && get_string_list "incremental.restart.list" <> [] then warn "Passing a non-empty list to incremental.restart.list (manual restarting) while incremental.restart.sided.enabled (automatic restarting) is activated."; if get_bool "ana.autotune.enabled" && get_bool "incremental.load" then (set_bool "ana.autotune.enabled" false; warn "ana.autotune.enabled implicitly disabled by incremental.load"); @@ -164,6 +166,10 @@ let check_arguments () = ); if get_bool "solvers.td3.space" && get_bool "solvers.td3.remove-wpoint" then fail "solvers.td3.space is incompatible with solvers.td3.remove-wpoint"; if get_bool "solvers.td3.space" && get_string "solvers.td3.side_widen" = "sides-local" then fail "solvers.td3.space is incompatible with solvers.td3.side_widen = 'sides-local'"; + if get_bool "solvers.td3.space" && get_bool "solvers.td3.narrow-globs.enabled" then fail "solvers.td3.space is incompatible with solvers.td3.narrow-globs.enabled"; + if (get_bool "incremental.load" || get_bool "incremental.save") && get_bool "solvers.td3.narrow-globs.enabled" then ( + fail "solvers.td3.space is incompatible with incremental analsyis."; + ); if List.mem "termination" @@ get_string_list "ana.activated" then ( if GobConfig.get_bool "incremental.load" || GobConfig.get_bool "incremental.save" then fail "termination analysis is not compatible with incremental analysis"; set_list "ana.activated" (GobConfig.get_list "ana.activated" @ [`String ("threadflag")]); diff --git a/src/solver/goblint_solver.ml b/src/solver/goblint_solver.ml index a98e71cbc3..ebbe4f5f4e 100644 --- a/src/solver/goblint_solver.ml +++ b/src/solver/goblint_solver.ml @@ -32,3 +32,4 @@ module SolverStats = SolverStats module SolverBox = SolverBox module SideWPointSelect = SideWPointSelect +module Td3UpdateRule = Td3UpdateRule diff --git a/src/solver/td3.ml b/src/solver/td3.ml index d18755e27a..e9d7156b15 100644 --- a/src/solver/td3.ml +++ b/src/solver/td3.ml @@ -45,16 +45,26 @@ module Base = functor (S:EqConstrSys) -> functor (HM:Hashtbl.S with type key = S.v) -> functor (Hooks: Hooks with module S = S and module HM = HM) -> + functor (UpdateRule: Td3UpdateRule.S) -> struct open SolverBox.Warrow (S.Dom) include Generic.SolverStats (S) (HM) module VS = Set.Make (S.Var) + + module UpdateRule = UpdateRule(S) (HM) (VS) + let exists_key f hm = HM.exists (fun k _ -> f k) hm + let assert_can_receive_side x = + if Hooks.system x <> None then ( + failwith ("side-effect to unknown w/ rhs: " ^ GobPretty.sprint S.Var.pretty_trace x); + ) + type solver_data = { st: (S.Var.t * S.Dom.t) list; (* needed to destabilize start functions if their start state changed because of some changed global initializer *) infl: VS.t HM.t; sides: VS.t HM.t; + update_rule_data: UpdateRule.data; rho: S.Dom.t HM.t; wpoint_gas: int HM.t; (** Tracks the widening gas of both side-effected and non-side-effected variables. Although they may have different gas budgets, they can be in the same map since no side-effected variable may ever have a rhs.*) stable: unit HM.t; @@ -71,6 +81,7 @@ module Base = st = []; infl = HM.create 10; sides = HM.create 10; + update_rule_data = UpdateRule.create_empty_data (); rho = HM.create 10; wpoint_gas = HM.create 10; stable = HM.create 10; @@ -119,6 +130,7 @@ module Base = wpoint_gas = HM.copy data.wpoint_gas; infl = HM.copy data.infl; sides = HM.copy data.sides; + update_rule_data = UpdateRule.copy_marshal data.update_rule_data; side_infl = HM.copy data.side_infl; side_dep = HM.copy data.side_dep; st = data.st; (* data.st is immutable *) @@ -164,6 +176,7 @@ module Base = HM.iter (fun k v -> HM.replace sides (S.Var.relift k) (VS.map S.Var.relift v) ) data.sides; + let update_rule_data = UpdateRule.relift_marshal data.update_rule_data in let side_infl = HM.create (HM.length data.side_infl) in HM.iter (fun k v -> HM.replace side_infl (S.Var.relift k) (VS.map S.Var.relift v) @@ -189,7 +202,7 @@ module Base = HM.iter (fun k v -> HM.replace dep (S.Var.relift k) (VS.map S.Var.relift v) ) data.dep; - {st; infl; sides; rho; wpoint_gas; stable; side_dep; side_infl; var_messages; rho_write; dep} + {st; infl; sides; update_rule_data; rho; wpoint_gas; stable; side_dep; side_infl; var_messages; rho_write; dep} type phase = Widen | Narrow [@@deriving show] (* used in inner solve *) @@ -225,6 +238,8 @@ module Base = let infl = data.infl in let sides = data.sides in + let update_rule_data = data.update_rule_data in + let rho = data.rho in let wpoint_gas = data.wpoint_gas in let stable = data.stable in @@ -315,6 +330,7 @@ module Base = else true ) w false (* nosemgrep: fold-exists *) (* does side effects *) + and eq_wrapper x eqx = ((UpdateRule.get_wrapper ~solve_widen:(fun x-> solve x Widen) ~init ~stable ~data:update_rule_data ~sides ~add_sides ~rho ~destabilize ~side ~assert_can_receive_side):UpdateRule.eq_wrapper) x eqx and solve ?reuse_eq x phase = if tracing then trace "sol2" "solve %a, phase: %s, called: %b, stable: %b, wpoint: %a" S.Var.pretty_trace x (show_phase phase) (HM.mem called x) (HM.mem stable x) pretty_wpoint x; init x; @@ -340,7 +356,7 @@ module Base = | _ -> (* The RHS is re-evaluated, all deps are re-trigerred *) HM.replace dep x VS.empty; - eq x (eval l x) (side ~x) + eq_wrapper x (eq x (eval l x)) in HM.remove called x; let old = HM.find rho x in (* d from older solve *) (* find old value after eq since wpoint restarting in eq/eval might have changed it meanwhile *) @@ -408,7 +424,11 @@ module Base = if cache && HM.mem l y then HM.find l y else ( HM.replace called y (); - let eqd = eq y (eval l x) (side ~x) in + let eqd = + (* We check in maingoblint that `solvers.td3.space` and `solvers.td3.narrow-globs.enabled` are not on at the same time *) + (* Narrowing on for globals ('solvers.td3.narrow-globs.enabled') would require enhancing this to work withe Narrow update rule *) + eq y (eval l x) (side ~x) + in HM.remove called y; if HM.mem wpoint_gas y then (HM.remove l y; solve y Widen; HM.find rho y) else (if cache then HM.replace l y eqd; eqd) @@ -437,10 +457,7 @@ module Base = tmp and side ?x y d = (* side from x to y; only to variables y w/o rhs; x only used for trace *) if tracing then trace "sol2" "side to %a (wpx: %a) from %a ## value: %a" S.Var.pretty_trace y pretty_wpoint y (Pretty.docOpt (S.Var.pretty_trace ())) x S.Dom.pretty d; - if Hooks.system y <> None then ( - Logs.warn "side-effect to unknown w/ rhs: %a, contrib: %a" S.Var.pretty_trace y S.Dom.pretty d; - ); - assert (Hooks.system y = None); + assert_can_receive_side y; init y; WPS.notify_side wps_data x y; @@ -497,6 +514,7 @@ module Base = let set_start (x,d) = if tracing then trace "sol2" "set_start %a ## %a" S.Var.pretty_trace x S.Dom.pretty d; init x; + UpdateRule.register_start update_rule_data x d; HM.replace rho x d; HM.replace stable x (); (* solve x Widen *) @@ -1049,14 +1067,14 @@ module Base = print_data_verbose data "Data after postsolve"; verify_data data; - (rho, {st; infl; sides; rho; wpoint_gas; stable; side_dep; side_infl; var_messages; rho_write; dep}) + (rho, {st; infl; sides; update_rule_data; rho; wpoint_gas; stable; side_dep; side_infl; var_messages; rho_write; dep}) end (** TD3 with no hooks. *) -module Basic: GenericEqIncrSolver = +module Basic(UpdateRule: Td3UpdateRule.S): GenericEqIncrSolver = functor (Arg: IncrSolverArg) -> functor (S:EqConstrSys) -> - functor (HM:Hashtbl.S with type key = S.v) -> + functor (HM:Hashtbl.S with type key = S.v)-> struct include Generic.SolverStats (S) (HM) @@ -1082,11 +1100,11 @@ module Basic: GenericEqIncrSolver = let prune ~reachable = () end - include Base (Arg) (S) (HM) (Hooks) + include Base (Arg) (S) (HM) (Hooks) (UpdateRule) end (** TD3 with eval skipping using [dep_vals]. *) -module DepVals: GenericEqIncrSolver = +module DepVals(UpdateRule: Td3UpdateRule.S): GenericEqIncrSolver = functor (Arg: IncrSolverArg) -> functor (S:EqConstrSys) -> functor (HM:Hashtbl.S with type key = S.v) -> @@ -1161,7 +1179,7 @@ module DepVals: GenericEqIncrSolver = ) !current_dep_vals end - module Base = Base (Arg) (S) (HM) (Hooks) + module Base = Base (Arg) (S) (HM) (Hooks) (UpdateRule) type marshal = { base: Base.marshal; @@ -1200,17 +1218,18 @@ let after_config () = let restart_wpoint = GobConfig.get_bool "solvers.td3.restart.wpoint.enabled" in let restart_once = GobConfig.get_bool "solvers.td3.restart.wpoint.once" in let skip_unchanged_rhs = GobConfig.get_bool "solvers.td3.skip-unchanged-rhs" in + let module UpdateRule = (val Td3UpdateRule.choose ()) in if skip_unchanged_rhs then ( if restart_sided || restart_wpoint || restart_once then ( M.warn "restarting active, ignoring solvers.td3.skip-unchanged-rhs"; (* TODO: fix DepVals with restarting, https://github.com/goblint/analyzer/pull/738#discussion_r876005821 *) - Selector.add_solver ("td3", (module Basic: GenericEqIncrSolver)) + Selector.add_solver ("td3", (module Basic(UpdateRule): GenericEqIncrSolver)) ) else - Selector.add_solver ("td3", (module DepVals: GenericEqIncrSolver)) + Selector.add_solver ("td3", (module DepVals(UpdateRule): GenericEqIncrSolver)) ) else - Selector.add_solver ("td3", (module Basic: GenericEqIncrSolver)) + Selector.add_solver ("td3", (module Basic(UpdateRule): GenericEqIncrSolver)) let () = AfterConfig.register after_config diff --git a/src/solver/td3UpdateRule.ml b/src/solver/td3UpdateRule.ml new file mode 100644 index 0000000000..48972a54d1 --- /dev/null +++ b/src/solver/td3UpdateRule.ml @@ -0,0 +1,239 @@ +(** Narrowing strategies for side-effects *) + +open Batteries +open ConstrSys +open Messages + + + +module type S = functor (S:EqConstrSys) -> functor (HM:Hashtbl.S with type key = S.v) -> functor (VS:Set.S with type elt = S.v) -> sig + type data + type eq_wrapper = S.v -> ((S.v -> S.d -> unit) -> S.d) -> S.d + val create_empty_data : unit -> data + val copy_marshal: data -> data + val relift_marshal: data -> data + + val register_start: data -> S.v -> S.d -> unit + + val get_wrapper: + solve_widen:(S.v -> unit) -> + init:(S.v -> unit) -> + stable:unit HM.t -> + data:data -> + sides:VS.t HM.t -> + add_sides: (S.v -> S.v -> unit) -> + rho: S.d HM.t -> + destabilize: (S.v -> unit) -> + side: (?x:S.v -> S.v -> S.d -> unit) -> + assert_can_receive_side: (S.v -> unit) + -> eq_wrapper + +end + +(** Inactive *) + +module Inactive:S = + functor (S:EqConstrSys) -> + functor (HM:Hashtbl.S with type key = S.v) -> + functor (VS:Set.S with type elt = S.v) -> + struct + type data = unit + type eq_wrapper = S.v -> ((S.v -> S.d -> unit) -> S.d) -> S.d + let create_empty_data () = () + let copy_marshal _ = () + let relift_marshal _ = () + + let register_start _ _ _ = () + + let get_wrapper ~solve_widen ~init ~stable ~data ~sides ~add_sides ~rho ~destabilize ~(side:?x:S.v -> S.v -> S.d -> unit) ~assert_can_receive_side = + (fun x eqx -> eqx (side ~x)) + end + +module Narrow:S = + functor (S:EqConstrSys) -> + functor (HM:Hashtbl.S with type key = S.v) -> + functor (VS:Set.S with type elt = S.v) -> + struct + type divided_side_mode = D_Widen | D_Narrow | D_Box [@@deriving show] + + type data = { + prev_sides: VS.t HM.t; + divided_side_effects: ((S.Dom.t * (int * divided_side_mode) option) HM.t) HM.t; + narrow_globs_start_values: S.Dom.t HM.t; + } + + type eq_wrapper = S.v -> ((S.v -> S.d -> unit) -> S.d) -> S.d + + let create_empty_data () = + let narrow_globs = GobConfig.get_bool "solvers.td3.narrow-globs.enabled" in + { + prev_sides = HM.create 10; + divided_side_effects = HM.create (if narrow_globs then 10 else 0); + narrow_globs_start_values = HM.create (if narrow_globs then 10 else 0); + } + + let copy_marshal data = + { + prev_sides = HM.copy data.prev_sides; + divided_side_effects = HM.map (fun k v -> HM.copy v) data.divided_side_effects; + narrow_globs_start_values = HM.copy data.narrow_globs_start_values; + } + + let relift_marshal data = + let prev_sides = HM.create (HM.length data.prev_sides) in + HM.iter (fun k v -> + HM.replace prev_sides (S.Var.relift k) (VS.map S.Var.relift v) + ) data.prev_sides; + let divided_side_effects = HM.create (HM.length data.divided_side_effects) in + HM.iter (fun k v -> + let inner_copy = HM.create (HM.length v) in + HM.iter (fun k (v, gas) -> HM.replace inner_copy (S.Var.relift k) ((S.Dom.relift v), gas)) v; + HM.replace divided_side_effects (S.Var.relift k) inner_copy + ) data.divided_side_effects; + let narrow_globs_start_values = HM.create (HM.length data.narrow_globs_start_values) in + HM.iter (fun k v -> + HM.replace narrow_globs_start_values (S.Var.relift k) (S.Dom.relift v) + ) data.narrow_globs_start_values; + { + prev_sides; + divided_side_effects; + narrow_globs_start_values; + } + + let register_start data x d = HM.replace data.narrow_globs_start_values x d + + let narrow_globs_conservative_widen = GobConfig.get_bool "solvers.td3.narrow-globs.conservative-widen" + let narrow_globs_immediate_growth = GobConfig.get_bool "solvers.td3.narrow-globs.immediate-growth" + let narrow_globs_gas_default = GobConfig.get_int "solvers.td3.narrow-globs.narrow-gas" + let narrow_globs_gas_default = if narrow_globs_gas_default < 0 then None else Some (narrow_globs_gas_default, D_Widen) + let narrow_globs_eliminate_dead = GobConfig.get_bool "solvers.td3.narrow-globs.eliminate-dead" + + let get_wrapper ~solve_widen ~init ~stable ~data ~sides ~add_sides ~rho ~destabilize ~(side:?x:S.v -> S.v -> S.d -> unit) ~assert_can_receive_side = + let eq_wrapper x eqx = + let rec side_acc acc changed x y d:unit = + let new_acc = match HM.find_option acc y with + | Some acc -> if not @@ S.Dom.leq d acc then Some (S.Dom.join acc d) else None + | None -> Some d + in + Option.may (fun new_acc -> + HM.replace acc y new_acc; + if narrow_globs_immediate_growth then ( + let y_changed = divided_side D_Widen x y new_acc in + if y_changed then + HM.replace changed y (); + ) + ) new_acc; + and divided_side (phase:divided_side_mode) x y d: bool = + if tracing then trace "side" "divided side to %a from %a ## value: %a" S.Var.pretty_trace y S.Var.pretty_trace x S.Dom.pretty d; + if tracing then trace "sol2" "divided side to %a from %a ## value: %a" S.Var.pretty_trace y S.Var.pretty_trace x S.Dom.pretty d; + assert_can_receive_side y; + init y; + if tracing then trace "sol2" "stable add %a" S.Var.pretty_trace y; + HM.replace stable y (); + + let sided = GobOption.exists (VS.mem x) (HM.find_option sides y) in + if not sided then add_sides y x; + if not (HM.mem data.divided_side_effects y) then HM.replace data.divided_side_effects y (HM.create 10); + + let y_sides = HM.find data.divided_side_effects y in + let (old_side, narrow_gas) = HM.find_default y_sides x (S.Dom.bot (), narrow_globs_gas_default) in + let phase = if phase = D_Box then + if S.Dom.leq d old_side then D_Narrow else D_Widen + else + phase + in + if not (phase = D_Narrow && narrow_gas = Some (0, D_Widen)) then ( + let (new_side, narrow_gas) = match phase with + | D_Widen -> + let tmp = S.Dom.join old_side d in + if not @@ S.Dom.equal tmp old_side then + let new_side = + if narrow_globs_conservative_widen && S.Dom.leq tmp (HM.find rho y) then + tmp + else + S.Dom.widen old_side tmp + in + let new_gas = Option.map (fun (x, _) -> (x, D_Widen)) narrow_gas in + (new_side, new_gas) + else + (old_side, narrow_gas) + | D_Narrow -> + let result = S.Dom.narrow old_side d in + let narrow_gas = if not @@ S.Dom.equal result old_side then + Option.map (fun (gas, phase) -> if phase = D_Widen then (gas - 1, D_Narrow) else (gas, phase)) narrow_gas + else + narrow_gas + in + (result, narrow_gas) + | _ -> failwith "unreachable" (* handled above *) + in + + if not (S.Dom.equal old_side new_side) then ( + if tracing then trace "side" "divided side to %a from %a changed (phase: %s) Old value: %a ## New value: %a" S.Var.pretty_trace y S.Var.pretty_trace x (show_divided_side_mode phase) S.Dom.pretty old_side S.Dom.pretty new_side; + + if S.Dom.is_bot new_side && narrow_gas = None then + HM.remove y_sides x + else + HM.replace y_sides x (new_side, narrow_gas); + + let combined_side y = + let contribs = HM.find_option data.divided_side_effects y in + let join map = HM.fold (fun _ (value, _) acc -> S.Dom.join acc value) map (S.Dom.bot ()) in + let combined = Option.map_default join (S.Dom.bot ()) contribs in + let start_value = HM.find_default data.narrow_globs_start_values y (S.Dom.bot()) in + S.Dom.join combined start_value + in + let y_oldval = HM.find rho y in + let y_newval = if S.Dom.leq old_side new_side then + (* If new side is strictly greater than the old one, the value of y can only increase. *) + S.Dom.join y_oldval new_side + else + combined_side y + in + if not (S.Dom.equal y_newval y_oldval) then ( + if tracing then trace "side" "value of %a changed by side from %a (phase: %s) Old value: %a ## New value: %a" + S.Var.pretty_trace y S.Var.pretty_trace x (show_divided_side_mode phase) S.Dom.pretty y_oldval S.Dom.pretty y_newval; + HM.replace rho y y_newval; + destabilize y; + ); + true + ) else + false + ) else + false + in + let acc = HM.create 0 in + let changed = HM.create 0 in + Fun.protect ~finally:(fun () -> ( + if narrow_globs_eliminate_dead then begin + let prev_sides_x = HM.find_option data.prev_sides x in + Option.may (VS.iter (fun y -> + if not @@ HM.mem acc y then begin + ignore @@ divided_side D_Narrow x y (S.Dom.bot ()); + if S.Dom.is_bot @@ HM.find rho y then + let casualties = S.postmortem y in + List.iter solve_widen casualties + end; + )) prev_sides_x; + let new_sides = HM.fold (fun k _ acc -> VS.add k acc) acc VS.empty in + if VS.is_empty new_sides then + HM.remove data.prev_sides x + else + HM.replace data.prev_sides x new_sides; + end; + if narrow_globs_immediate_growth then + HM.iter (fun y acc -> if not @@ HM.mem changed y then ignore @@ divided_side D_Narrow x y acc) acc + else ( + HM.iter (fun y acc -> ignore @@ divided_side D_Box x y acc) acc + ) + )) (fun () -> eqx (side_acc acc changed x)) + in + (eq_wrapper: eq_wrapper) + + end + +let choose () = + if GobConfig.get_bool "solvers.td3.narrow-globs.enabled" then + (module Narrow : S) + else + (module Inactive : S) diff --git a/tests/regression/85-narrow_globs/01-modulo-guard.c b/tests/regression/85-narrow_globs/01-modulo-guard.c new file mode 100644 index 0000000000..14cbc7a692 --- /dev/null +++ b/tests/regression/85-narrow_globs/01-modulo-guard.c @@ -0,0 +1,27 @@ +// PARAM: --enable solvers.td3.narrow-globs.enabled --enable ana.int.interval +#include +#include + +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +int a = 17; + +void f() { + pthread_mutex_lock(&mutex); + if (a % 2) { + a = 3 * a + 1; + } else { + a = a / 2; + } + a = a % 0xbeef; + pthread_mutex_unlock(&mutex); +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, f, NULL); + pthread_mutex_lock(&mutex); + __goblint_check(a >= 0); // UNKNOWN cannot narrow lower bound to 0, only -0xbeef + 1 + __goblint_check(a < 0xbeef); + pthread_mutex_unlock(&mutex); + return 0; +} diff --git a/tests/regression/85-narrow_globs/02-state-machine.c b/tests/regression/85-narrow_globs/02-state-machine.c new file mode 100644 index 0000000000..43e6f23d84 --- /dev/null +++ b/tests/regression/85-narrow_globs/02-state-machine.c @@ -0,0 +1,50 @@ +// PARAM: --enable ana.int.interval --enable solvers.td3.narrow-globs.enabled +#include +#include + +int state = 0; + +void *thread(void *d) { + while (1) { + int input; + int next_state; + int current_state = state; + switch (current_state) { + case 0: + if(input) + next_state = current_state + 1; + else + next_state = current_state; + break; + case 1: + if(input) + next_state = current_state + 1; + else + next_state = current_state + 2; + break; + case 2: + next_state = 0; + break; + case 3: + next_state = 4; + break; + case 4: + next_state = 5; + break; + case 5: + next_state = 5; + break; + default: + next_state = -1; + } + state = next_state; + } +} + +int main(void) { + int id; + pthread_create(&id, NULL, thread, NULL); + __goblint_check(state >= -1); + __goblint_check(state <= 5); + pthread_join(&id, NULL); +} diff --git a/tests/regression/85-narrow_globs/03-guarded_inc.c b/tests/regression/85-narrow_globs/03-guarded_inc.c new file mode 100644 index 0000000000..9245750b1a --- /dev/null +++ b/tests/regression/85-narrow_globs/03-guarded_inc.c @@ -0,0 +1,25 @@ +// PARAM: --enable solvers.td3.narrow-globs.enabled --enable ana.int.interval --enable ana.base.priv.protection.changes-only +#include +#include +#include + +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +int a = 0; + +void f(void *d) { + pthread_mutex_lock(&mutex); + if (a < 10) + a++; + pthread_mutex_unlock(&mutex); +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, f, NULL); + + __goblint_check(a <= 10); + pthread_mutex_lock(&mutex); + __goblint_check(a <= 10); + pthread_mutex_unlock(&mutex); + return 0; +} diff --git a/tests/regression/85-narrow_globs/04-semaphore.c b/tests/regression/85-narrow_globs/04-semaphore.c new file mode 100644 index 0000000000..7450ce8bf5 --- /dev/null +++ b/tests/regression/85-narrow_globs/04-semaphore.c @@ -0,0 +1,67 @@ +// PARAM: --enable solvers.td3.narrow-globs.enabled --enable ana.int.interval --enable ana.base.priv.protection.changes-only +#include +#include +#include + +typedef struct { + pthread_mutex_t mutex; + int count; +} semaphore_t; + +void semaphor_init(semaphore_t *sem, int count) { + sem->count = count; + pthread_mutex_init(&sem->mutex, NULL); +} + +void semaphor_up(semaphore_t *sem) { + pthread_mutex_lock(&sem->mutex); + if (sem->count < 1000) + sem->count++; + pthread_mutex_unlock(&sem->mutex); +} + +void semaphor_down(semaphore_t *sem) { + while(1) { + pthread_mutex_lock(&sem->mutex); + if(sem->count > 0) { + sem->count--; + pthread_mutex_unlock(&sem->mutex); + break; + } + pthread_mutex_unlock(&sem->mutex); + usleep(10); + } +} + +void worker(void *data) { + semaphore_t* sem = (semaphore_t*)data; + while(1) { + semaphor_down(sem); + // do work + semaphor_up(sem); + } +} + +int main(void) { + semaphore_t sem; + semaphor_init(&sem, 10); + + pthread_t id1; + pthread_create(&id1, NULL, worker, &sem); + pthread_t id2; + pthread_create(&id2, NULL, worker, &sem); + + __goblint_check(sem.count <= 1000); + pthread_mutex_lock(&sem.mutex); + __goblint_check(sem.count <= 1000); + pthread_mutex_unlock(&sem.mutex); + + __goblint_check(sem.count >= 0); + pthread_mutex_lock(&sem.mutex); + __goblint_check(sem.count >= 0); + pthread_mutex_unlock(&sem.mutex); + + pthread_join(&id1, NULL); + pthread_join(&id2, NULL); + return 0; +} diff --git a/tests/regression/85-narrow_globs/05-nested_loop.c b/tests/regression/85-narrow_globs/05-nested_loop.c new file mode 100644 index 0000000000..4047a6c92b --- /dev/null +++ b/tests/regression/85-narrow_globs/05-nested_loop.c @@ -0,0 +1,40 @@ +// PARAM: --enable solvers.td3.narrow-globs.enabled --enable ana.int.interval +#include +#include +#include + +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +int a = 0; +int b = 0; +int c = 0; + +void f(void *d) { + for(int i = 0; i < 15; i++) { + pthread_mutex_lock(&mutex); + c = i; + pthread_mutex_unlock(&mutex); + for(int j = 0; j < i; j++) { + pthread_mutex_lock(&mutex); + b = i + j; + pthread_mutex_unlock(&mutex); + for(int k = 0; k < j; k++) { + pthread_mutex_lock(&mutex); + a = i + j + k; + pthread_mutex_unlock(&mutex); + __goblint_check(i + j + k <= 100); + } + } + } +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, f, NULL); + + pthread_mutex_lock(&mutex); + __goblint_check(a <= 100); + __goblint_check(b <= 100); + __goblint_check(c <= 100); + pthread_mutex_unlock(&mutex); + return 0; +} diff --git a/tests/regression/85-narrow_globs/06-cyclic-dependency.c b/tests/regression/85-narrow_globs/06-cyclic-dependency.c new file mode 100644 index 0000000000..8dd45db86b --- /dev/null +++ b/tests/regression/85-narrow_globs/06-cyclic-dependency.c @@ -0,0 +1,30 @@ +// PARAM: --enable solvers.td3.narrow-globs.enabled --enable ana.int.interval +// NOTIMEOUT + +#include +#include + +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +int a = 0; +int b = 0; +void* g(void *d) { + pthread_mutex_lock(&mutex); + b = a + 1; + pthread_mutex_unlock(&mutex); + return NULL; +} + + +void* f(void *d) { + pthread_mutex_lock(&mutex); + a = b + 1; + pthread_mutex_unlock(&mutex); + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, f, NULL); + pthread_create(&id, NULL, g, NULL); + return 0; +} \ No newline at end of file diff --git a/tests/regression/85-narrow_globs/07-ctxt-widen.c b/tests/regression/85-narrow_globs/07-ctxt-widen.c new file mode 100644 index 0000000000..12cfdfdaea --- /dev/null +++ b/tests/regression/85-narrow_globs/07-ctxt-widen.c @@ -0,0 +1,53 @@ +// PARAM: --enable ana.int.interval_set --set ana.context.gas_value 0 --enable solvers.td3.narrow-globs.enabled +// Taken from context gas tests, where the assertions were unknown. +#include + +int h(int i) +{ + if (i == 0) + { + return 3; + } + if (i > 0) + { + return h(i - 1); + } + return 13; +} + +int g(int i) +{ + if (i == 0) + { + return 2; + } + if (i > 0) + { + return h(i - 1); + } + return 12; +} + +int f(int i) +{ + if (i == 0) + { + return 1; + } + if (i > 0) + { + return g(i - 1); + } + return 11; +} + +int main(void) +{ + __goblint_check(f(11) == 3); + __goblint_check(g(12) == 3); + __goblint_check(g(20) == 3); + __goblint_check(f(20) == 3); + __goblint_check(h(40) == 3); + __goblint_check(h(300) == 3); + __goblint_check(f(300) == 3); +} diff --git a/tests/regression/85-narrow_globs/08-ctxt-insensitive.c b/tests/regression/85-narrow_globs/08-ctxt-insensitive.c new file mode 100644 index 0000000000..b3ed58bfe4 --- /dev/null +++ b/tests/regression/85-narrow_globs/08-ctxt-insensitive.c @@ -0,0 +1,16 @@ +// PARAM: --set ana.context.callString_length 0 --set "ana.activated[+]" call_string --set ana.ctx_sens "['call_string']" --enable ana.int.interval_set --enable solvers.td3.narrow-globs.enabled +#include + +int fac(int i) { + if (i > 0) { + return fac(i - 1) * i; + } + __goblint_check(i == 0); + return 1; +} + +int main(void) +{ + fac(10); + return 0; +} diff --git a/tests/regression/85-narrow_globs/09-longjmp-counting-local.c b/tests/regression/85-narrow_globs/09-longjmp-counting-local.c new file mode 100644 index 0000000000..20d2ae4e9c --- /dev/null +++ b/tests/regression/85-narrow_globs/09-longjmp-counting-local.c @@ -0,0 +1,22 @@ +// PARAM: --enable solvers.td3.narrow-globs.enabled --enable ana.int.interval --disable exp.volatiles_are_top +#include +#include +#include + +jmp_buf my_jump_buffer; +void foo(int count) +{ + __goblint_check(count >= 0 && count <= 5); + longjmp(my_jump_buffer, 1); +} +int main(void) +{ + volatile int count = 0; + setjmp (my_jump_buffer); + if (count < 5) { + count++; + foo(count); + __goblint_check(0); //NOWARN + } + __goblint_check(count == 5); +} diff --git a/tests/regression/85-narrow_globs/10-longjmp-heap-counting-return.c b/tests/regression/85-narrow_globs/10-longjmp-heap-counting-return.c new file mode 100644 index 0000000000..08ba46bd05 --- /dev/null +++ b/tests/regression/85-narrow_globs/10-longjmp-heap-counting-return.c @@ -0,0 +1,18 @@ +// PARAM: --enable ana.int.interval --enable ana.int.enums --enable solvers.td3.narrow-globs.enabled --enable exp.earlyglobs --set ana.setjmp.split none --disable exp.volatiles_are_top +#include +#include +#include + +int main(void) +{ + jmp_buf* my_jump_buffer = malloc(sizeof(jmp_buf)); + + volatile int count = setjmp(*my_jump_buffer); + __goblint_check(count == 0); // UNKNOWN! + if (count < 5) { + __goblint_check(count >= 0 & count < 5); + longjmp(*my_jump_buffer, count + 1); + __goblint_check(0); // NOWARN + } + __goblint_check(count == 5); +} diff --git a/tests/regression/85-narrow_globs/11-longjmp-counting-return.c b/tests/regression/85-narrow_globs/11-longjmp-counting-return.c new file mode 100644 index 0000000000..193f604acc --- /dev/null +++ b/tests/regression/85-narrow_globs/11-longjmp-counting-return.c @@ -0,0 +1,23 @@ +// PARAM: --enable ana.int.interval --enable ana.int.enums --enable solvers.td3.narrow-globs.enabled --set ana.setjmp.split none +#include +#include + +jmp_buf my_jump_buffer; + +void foo(int count) +{ + __goblint_check(count >= 0 && count < 5); + longjmp(my_jump_buffer, count + 1); + __goblint_check(0); // NOWARN +} + +int main(void) +{ + int count = setjmp(my_jump_buffer); + __goblint_check(count == 0); // UNKNOWN! + if (count < 5) { + foo(count); + __goblint_check(0); // NOWARN + } + __goblint_check(count == 5); +} diff --git a/tests/regression/85-narrow_globs/12-multiple-growing-updates.c b/tests/regression/85-narrow_globs/12-multiple-growing-updates.c new file mode 100644 index 0000000000..77be309d99 --- /dev/null +++ b/tests/regression/85-narrow_globs/12-multiple-growing-updates.c @@ -0,0 +1,32 @@ +// PARAM: --enable ana.int.interval_set --enable solvers.td3.narrow-globs.enabled +#include +#include + +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +int glob = 0; +int glob2 = 0; + +void *thread(void *d) { + for(int i = 0; i < 10; i++) { + pthread_mutex_lock(&mutex); + glob = i; + pthread_mutex_unlock(&mutex); + } + + for(int i = -1; i > -10; i--) { + pthread_mutex_lock(&mutex); + glob = i; + pthread_mutex_unlock(&mutex); + } +} + +int main(void) +{ + int id; + pthread_create(&id, NULL, thread, NULL); + pthread_mutex_lock(&mutex); + __goblint_check(glob >= -10); + __goblint_check(glob <= 10); + pthread_mutex_unlock(&mutex); + pthread_join(&id, NULL); +} diff --git a/tests/regression/85-narrow_globs/13-threaded-ctxt-widen.c b/tests/regression/85-narrow_globs/13-threaded-ctxt-widen.c new file mode 100644 index 0000000000..74cb400ae6 --- /dev/null +++ b/tests/regression/85-narrow_globs/13-threaded-ctxt-widen.c @@ -0,0 +1,46 @@ +// PARAM: --enable ana.int.interval_set --set ana.context.gas_value 0 --enable solvers.td3.narrow-globs.enabled +#include +#include + +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +int glob = 0; +int glob2 = 0; + +void *thread(void *d) { + f(10); + return NULL; +} + +void f(int i) { + pthread_mutex_lock(&mutex); + glob = i; + pthread_mutex_unlock(&mutex); + if (i > 0) { + f(i - 1); + } +} + +void *thread2(void *d) { + g(10); + return NULL; +} + +void g(int i) { + pthread_mutex_lock(&mutex); + glob2 = i; + pthread_mutex_unlock(&mutex); + if (i != 0) { + g(i - 1); + } +} + +int main(void) +{ + int id; + pthread_create(&id, NULL, thread, NULL); + pthread_create(&id, NULL, thread2, NULL); + pthread_mutex_lock(&mutex); + __goblint_check(glob >= 0 && glob <= 10); + __goblint_check(glob2 >= 0 && glob2 <= 10); //UNKNOWN (operator != does not permit narrowing) + pthread_mutex_unlock(&mutex); +} diff --git a/tests/regression/85-narrow_globs/14-widening-thresholds.c b/tests/regression/85-narrow_globs/14-widening-thresholds.c new file mode 100644 index 0000000000..8ddd060f57 --- /dev/null +++ b/tests/regression/85-narrow_globs/14-widening-thresholds.c @@ -0,0 +1,29 @@ +// PARAM: --enable ana.int.interval --enable ana.int.interval_threshold_widening --set ana.int.interval_threshold_widening_constants comparisons --enable solvers.td3.narrow-globs.enabled +#include +#include + +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +int glob = 0; + +void *thread(void *data) { + int ub = *(int*)data; + for(int i = 0; i < 256;) { + i += 2; + pthread_mutex_lock(&mutex); + glob = i; + pthread_mutex_unlock(&mutex); + } + return NULL; +} + +int main(void) +{ + int id; + int ub = 256; + pthread_create(&id, NULL, thread, &ub); + pthread_mutex_lock(&mutex); + __goblint_check(glob >= 0); + __goblint_check(glob <= 258); + pthread_mutex_unlock(&mutex); + pthread_join(&id, NULL); +} diff --git a/tests/regression/85-narrow_globs/15-intertwined_increment.c b/tests/regression/85-narrow_globs/15-intertwined_increment.c new file mode 100644 index 0000000000..04af57e547 --- /dev/null +++ b/tests/regression/85-narrow_globs/15-intertwined_increment.c @@ -0,0 +1,33 @@ +// PARAM: --enable ana.int.interval --enable solvers.td3.narrow-globs.enabled +#include +#include + +int a, b; +pthread_mutex_t m = PTHREAD_MUTEX_INITIALIZER; + +void *t_fun1(void *arg) { + int i = a; + if (i < 1000) { + b = i + 1; + } +} + +void *t_fun2(void *arg) { + int i = b; + if (i < 1000) { + a = i + 1; + } +} + +int main(void) { + pthread_t id1, id2; + pthread_create(&id1, NULL, t_fun1, NULL); + pthread_create(&id2, NULL, t_fun2, NULL); + pthread_join (id1, NULL); + pthread_join (id2, NULL); + pthread_mutex_lock(&m); + __goblint_check(a <= 1000); + __goblint_check(b <= 1000); + pthread_mutex_unlock(&m); + return 0; +} diff --git a/tests/regression/85-narrow_globs/16-cyclic-dependency-guarded.c b/tests/regression/85-narrow_globs/16-cyclic-dependency-guarded.c new file mode 100644 index 0000000000..7407049aac --- /dev/null +++ b/tests/regression/85-narrow_globs/16-cyclic-dependency-guarded.c @@ -0,0 +1,34 @@ +// PARAM: --enable solvers.td3.narrow-globs.enabled --set solvers.td3.narrow-globs.narrow-gas 9 --enable ana.int.interval --set ana.base.privatization protection-read --enable ana.base.priv.protection.changes-only +// NOTIMEOUT +#include +#include + +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +int a = 0; +int b = 0; +void* g(void *d) { + pthread_mutex_lock(&mutex); + b = a + 1; + pthread_mutex_unlock(&mutex); + return NULL; +} + + +void* f(void *d) { + pthread_mutex_lock(&mutex); + if (b < 10) + a = b; + pthread_mutex_unlock(&mutex); + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, f, NULL); + pthread_create(&id, NULL, g, NULL); + pthread_mutex_lock(&mutex); + __goblint_check(a <= 10); + __goblint_check(b <= 10); + pthread_mutex_unlock(&mutex); + return 0; +} diff --git a/tests/regression/85-narrow_globs/17-dead-side-effect.c b/tests/regression/85-narrow_globs/17-dead-side-effect.c new file mode 100644 index 0000000000..6bf2864ec0 --- /dev/null +++ b/tests/regression/85-narrow_globs/17-dead-side-effect.c @@ -0,0 +1,26 @@ +// PARAM: --enable solvers.td3.narrow-globs.enabled --enable ana.int.interval --enable solvers.td3.narrow-globs.eliminate-dead --enable ana.base.priv.protection.changes-only +#include +#include + +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +int a = 0; +int b = 0; + +void* f(void *d) { + pthread_mutex_lock(&mutex); + if (a < 10) { + a++; + } + if (a > 20) { + b = 1; + } + pthread_mutex_unlock(&mutex); + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, f, NULL); + __goblint_check(!b); //NORACE + return 0; +} \ No newline at end of file diff --git a/tests/regression/85-narrow_globs/18-dead-side-effect2.c b/tests/regression/85-narrow_globs/18-dead-side-effect2.c new file mode 100644 index 0000000000..81e1e09706 --- /dev/null +++ b/tests/regression/85-narrow_globs/18-dead-side-effect2.c @@ -0,0 +1,32 @@ +// PARAM: --enable solvers.td3.narrow-globs.enabled --enable ana.int.interval --enable solvers.td3.narrow-globs.eliminate-dead --enable ana.base.priv.protection.changes-only +#include +#include + +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +int a = 0; +int b = 0; + +void g() { + b = 1; +} + +void* f(void *d) { + pthread_mutex_lock(&mutex); + if (a < 10) { + a++; + } + if (a > 20) { + g(); + } + pthread_mutex_unlock(&mutex); + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, f, NULL); + pthread_mutex_lock(&mutex); + __goblint_check(!b); + pthread_mutex_lock(&mutex); + return 0; +} \ No newline at end of file diff --git a/tests/regression/85-narrow_globs/19-dead-side-effect3.c b/tests/regression/85-narrow_globs/19-dead-side-effect3.c new file mode 100644 index 0000000000..bef3c7e001 --- /dev/null +++ b/tests/regression/85-narrow_globs/19-dead-side-effect3.c @@ -0,0 +1,29 @@ +// PARAM: --enable ana.int.interval --enable solvers.td3.narrow-globs.enabled --enable solvers.td3.narrow-globs.eliminate-dead --enable ana.base.priv.protection.changes-only +#include +#include +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +int a = 0; +int b = 0; + +void g(int i) { + __goblint_check(i <= 10); + pthread_mutex_lock(&mutex); + b = i; + pthread_mutex_unlock(&mutex); +} + +void* f(void *d) { + int j = 0; + for(int i = 0; i < 10; i++) { + g(j); + j = i; + } + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, f, NULL); + __goblint_check(b <= 10); + return 0; +} \ No newline at end of file diff --git a/tests/regression/85-narrow_globs/20-dead-side-effect4.c b/tests/regression/85-narrow_globs/20-dead-side-effect4.c new file mode 100644 index 0000000000..c437321f4c --- /dev/null +++ b/tests/regression/85-narrow_globs/20-dead-side-effect4.c @@ -0,0 +1,31 @@ +// PARAM: --disable ana.int.def_exc --enable ana.int.interval --set ana.context.gas_value 0 --enable solvers.td3.narrow-globs.enabled --enable solvers.td3.narrow-globs.eliminate-dead --enable ana.base.priv.protection.changes-only +#include +#include +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +int b = 0; + +void g() { + pthread_mutex_lock(&mutex); + b = 1; + pthread_mutex_unlock(&mutex); +} + +void f(int i) { + if (i < 0) { + g(); + } + if (i > 0) { + f(i - 1); + } +} + +void *thread(void * data) { + f(10000); +} + +int main(void) { + int id; + pthread_create(&id, NULL, thread, NULL); + __goblint_check(b == 0); + return 0; +} \ No newline at end of file diff --git a/tests/regression/85-narrow_globs/21-dead-escape.c b/tests/regression/85-narrow_globs/21-dead-escape.c new file mode 100644 index 0000000000..45f60fffea --- /dev/null +++ b/tests/regression/85-narrow_globs/21-dead-escape.c @@ -0,0 +1,42 @@ +// PARAM: --enable solvers.td3.narrow-globs.enabled --enable ana.int.interval --enable solvers.td3.narrow-globs.eliminate-dead --enable ana.base.priv.protection.changes-only +#include +#include + +int b = 0; +int *a = &b; + +void* f(void *d) { + int i = 0; + + for(int j = 0, k = 0; j < 10; j++) { + if (k > 20) { + a = &i; + } + k = j; + } + i++; + + // The unknowns for protected:i etc. exist. + // Also, i is in the global set of escapees. + // However, locally i is known not to have escaped, + // so none of these unknowns are queried and this check + // succeeds whether eliminate-dead is on or not. + __goblint_check(i == 1); + // a != &i is not known without eliminate-dead + // The pointer has escaped at some point and was recorded at the global a. + // We don't filter points-to-sets read from globals to exclude things which are locally known (by the ThreadEscape analysis) to not have escaped. + // I don't think this is particularly common, and iterating and querying for each lval is probably just expensive. + __goblint_check(a != &i); + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, f, NULL); + + // a is thought to (possibly) point to the *flow-insensitively* tracked i, + // which is widened by the i++. + __goblint_check(*a <= 1); + + return 0; +} diff --git a/tests/regression/85-narrow_globs/22-dead-escape-indirect.c b/tests/regression/85-narrow_globs/22-dead-escape-indirect.c new file mode 100644 index 0000000000..cab62e7403 --- /dev/null +++ b/tests/regression/85-narrow_globs/22-dead-escape-indirect.c @@ -0,0 +1,37 @@ +// PARAM: --enable solvers.td3.narrow-globs.enabled --enable ana.int.interval --enable solvers.td3.narrow-globs.eliminate-dead --enable ana.base.priv.protection.changes-only +#include +#include + +int b = 0; +int *a = &b; + +void g (int k, int *i) { + if (k > 20) { + a = &i; + } +} + +void* f(void *d) { + int i = 0; + + for(int j = 0, k = 0; j < 10; j++) { + g(k, &i); + k = j; + } + i++; + + __goblint_check(i == 1); + __goblint_check(a != &i); + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, f, NULL); + + // a is thought to (possibly) point to the *flow-insensitively* tracked i, + // which is widened by the i++. + __goblint_check(*a <= 1); + + return 0; +} \ No newline at end of file diff --git a/tests/unit/solver/solverTest.ml b/tests/unit/solver/solverTest.ml index 807755137b..67f18a7560 100644 --- a/tests/unit/solver/solverTest.ml +++ b/tests/unit/solver/solverTest.ml @@ -46,6 +46,7 @@ module ConstrSys = struct let iter_vars _ _ _ _ _ = () let sys_change _ _ = {obsolete = []; delete = []; reluctant = []; restart = []} + let postmortem _ = [] end module LH = BatHashtbl.Make (ConstrSys.LVar)