From 99e69959c4cfbc9113811008c201d13d55ef1755 Mon Sep 17 00:00:00 2001 From: Fabian Stemmler Date: Sun, 21 Apr 2024 13:02:45 +0200 Subject: [PATCH 01/36] feature: divide and narrow --- src/analyses/basePriv.ml | 109 ++++++--- src/config/options.schema.json | 57 +++++ src/constraint/constrSys.ml | 8 + src/framework/constraints.ml | 5 + src/maingoblint.ml | 7 + src/solver/td3.ml | 210 +++++++++++++++++- .../95-dividedsides/01-modulo-guard.c | 27 +++ .../95-dividedsides/02-state-machine.c | 49 ++++ .../95-dividedsides/03-guarded_inc.c | 25 +++ .../regression/95-dividedsides/04-semaphore.c | 67 ++++++ .../95-dividedsides/05-nested_loop.c | 40 ++++ .../95-dividedsides/06-cyclic-dependency.c | 30 +++ .../95-dividedsides/07-ctxt-widen.c | 53 +++++ .../95-dividedsides/08-ctxt-insensitive.c | 15 ++ .../09-longjmp-counting-local.c | 22 ++ .../10-longjmp-heap-counting-return.c | 18 ++ .../11-longjmp-counting-return.c | 23 ++ .../12-multiple-growing-updates.c | 31 +++ .../95-dividedsides/13-threaded-ctxt-widen.c | 45 ++++ .../95-dividedsides/14-widening-thresholds.c | 28 +++ .../15-intertwined_increment.c | 33 +++ .../16-cyclic-dependency-guarded.c | 35 +++ .../95-dividedsides/17-dead-side-effect.c | 26 +++ .../95-dividedsides/18-dead-side-effect2.c | 32 +++ .../95-dividedsides/19-dead-side-effect3.c | 29 +++ .../95-dividedsides/20-dead-side-effect4.c | 31 +++ .../95-dividedsides/21-dead-escape.c | 39 ++++ .../95-dividedsides/22-dead-escape-indirect.c | 37 +++ tests/unit/solver/solverTest.ml | 1 + 29 files changed, 1096 insertions(+), 36 deletions(-) create mode 100644 tests/regression/95-dividedsides/01-modulo-guard.c create mode 100644 tests/regression/95-dividedsides/02-state-machine.c create mode 100644 tests/regression/95-dividedsides/03-guarded_inc.c create mode 100644 tests/regression/95-dividedsides/04-semaphore.c create mode 100644 tests/regression/95-dividedsides/05-nested_loop.c create mode 100644 tests/regression/95-dividedsides/06-cyclic-dependency.c create mode 100644 tests/regression/95-dividedsides/07-ctxt-widen.c create mode 100644 tests/regression/95-dividedsides/08-ctxt-insensitive.c create mode 100644 tests/regression/95-dividedsides/09-longjmp-counting-local.c create mode 100644 tests/regression/95-dividedsides/10-longjmp-heap-counting-return.c create mode 100644 tests/regression/95-dividedsides/11-longjmp-counting-return.c create mode 100644 tests/regression/95-dividedsides/12-multiple-growing-updates.c create mode 100644 tests/regression/95-dividedsides/13-threaded-ctxt-widen.c create mode 100644 tests/regression/95-dividedsides/14-widening-thresholds.c create mode 100644 tests/regression/95-dividedsides/15-intertwined_increment.c create mode 100644 tests/regression/95-dividedsides/16-cyclic-dependency-guarded.c create mode 100644 tests/regression/95-dividedsides/17-dead-side-effect.c create mode 100644 tests/regression/95-dividedsides/18-dead-side-effect2.c create mode 100644 tests/regression/95-dividedsides/19-dead-side-effect3.c create mode 100644 tests/regression/95-dividedsides/20-dead-side-effect4.c create mode 100644 tests/regression/95-dividedsides/21-dead-escape.c create mode 100644 tests/regression/95-dividedsides/22-dead-escape-indirect.c diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 3afd758daa..4a48e41899 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -719,6 +719,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 = @@ -740,30 +781,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. *) @@ -774,6 +809,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. *) @@ -782,11 +818,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 @@ -796,16 +832,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 ) @@ -821,7 +863,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 @@ -860,7 +902,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 @@ -1969,18 +2011,25 @@ end let priv_module: (module S) Lazy.t = lazy ( + let changes_only = get_bool "ana.base.priv.protection.changes-only" in let module Priv: S = (val match get_string "ana.base.privatization" with | "none" -> (module NonePriv: S) | "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" when changes_only -> (module ProtectionBasedPriv (ProtectionChangesOnlySide) (struct let check_read_unprotected = false let handle_atomic = false end)(NoWrapper)) + | "protection" -> (module ProtectionBasedPriv (ProtectionCPASide) (struct let check_read_unprotected = false let handle_atomic = false end)(NoWrapper)) + | "protection-tid" when changes_only -> (module ProtectionBasedPriv (ProtectionChangesOnlySide) (struct let check_read_unprotected = false let handle_atomic = false end)(DigestWrapper(ThreadNotStartedDigest))) + | "protection-tid" -> (module ProtectionBasedPriv (ProtectionCPASide) (struct let check_read_unprotected = false let handle_atomic = false end)(DigestWrapper(ThreadNotStartedDigest))) + | "protection-atomic" when changes_only -> (module ProtectionBasedPriv (ProtectionChangesOnlySide) (struct let check_read_unprotected = false let handle_atomic = true end)(NoWrapper)) (* experimental *) + | "protection-atomic" -> (module ProtectionBasedPriv (ProtectionCPASide) (struct let check_read_unprotected = false let handle_atomic = true end)(NoWrapper)) (* experimental *) + | "protection-read" when changes_only -> (module ProtectionBasedPriv (ProtectionChangesOnlySide) (struct let check_read_unprotected = true let handle_atomic = false end)(NoWrapper)) + | "protection-read" -> (module ProtectionBasedPriv (ProtectionCPASide) (struct let check_read_unprotected = true let handle_atomic = false end)(NoWrapper)) + | "protection-read-tid" when changes_only -> (module ProtectionBasedPriv (ProtectionChangesOnlySide) (struct let check_read_unprotected = true let handle_atomic = false end)(DigestWrapper(ThreadNotStartedDigest))) + | "protection-read-tid" -> (module ProtectionBasedPriv (ProtectionCPASide) (struct let check_read_unprotected = true let handle_atomic = false end)(DigestWrapper(ThreadNotStartedDigest))) + | "protection-read-atomic" when changes_only -> (module ProtectionBasedPriv (ProtectionChangesOnlySide) (struct let check_read_unprotected = true let handle_atomic = true end)(NoWrapper)) (* experimental *) + | "protection-read-atomic" -> (module ProtectionBasedPriv (ProtectionCPASide) (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 43e2ad1d59..a1717dfacd 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -770,6 +770,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": @@ -2421,6 +2435,49 @@ "type": "boolean", "default": true }, + "narrow-sides": { + "title": "solvers.td3.narrow-sides", + "type": "object", + "properties": { + "enabled": { + "title": "solvers.td3.narrow-sides.enabled", + "description": "Individually track side-effects from different unknowns to enable narrowing of globals.", + "type": "boolean", + "default": false + }, + "stable": { + "title": "solvers.td3.narrow-sides.stable", + "description": "Controls when to narrow. true: If unknown remains stable after evaluating its rhs, apply all sides with narrowing. false: Apply sides that did not increase with narrowing.", + "type": "boolean", + "default": false + }, + "conservative-widen": { + "title": "solvers.td3.narrow-sides.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-sides.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-sides.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": -1 + }, + "eliminate-dead": { + "title": "solvers.td3.narrow-sides.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..49d7797cc5 100644 --- a/src/constraint/constrSys.ml +++ b/src/constraint/constrSys.ml @@ -48,6 +48,8 @@ sig val sys_change: (v -> d) -> v sys_change_info (** Compute incremental constraint system change from old solution. *) + + val postmortem: v -> v list end (** Any system of side-effecting equations over lattices. *) @@ -64,6 +66,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 +208,11 @@ struct let sys_change get = S.sys_change (getL % get % l) (getG % get % g) + + let postmortem leaf = + match leaf with + | `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 fb4b5081e8..a98cd2193c 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -539,4 +539,9 @@ struct in {obsolete; delete; reluctant; restart} + + let postmortem leaf = + match leaf with + | FunctionEntry fd, c -> [(Function fd, c)] + | _ -> [] end diff --git a/src/maingoblint.ml b/src/maingoblint.ml index cb81ea0b86..b74dfdd0cd 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -142,6 +142,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" && Option.is_none (List.find_opt (String.equal @@ 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"); @@ -165,6 +167,11 @@ 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-sides.enabled" then fail "solvers.td3.space is incompatible with solvers.td3.narrow-sides"; + if (get_bool "incremental.load" || get_bool "incremental.save") && get_bool "solvers.td3.narrow-sides.enabled" then ( + set_bool "solvers.td3.narrow-sides.enabled" false; + warn "solvers.td3.narrow-sides implicitly disabled by incremental analysis"; + ); 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/td3.ml b/src/solver/td3.ml index 3cab3cf7f7..a7a4ca25e3 100644 --- a/src/solver/td3.ml +++ b/src/solver/td3.ml @@ -51,10 +51,15 @@ module Base = module VS = Set.Make (S.Var) let exists_key f hm = HM.exists (fun k _ -> f k) hm + type divided_side_phase = D_Widen | D_Narrow | D_Box [@@deriving show] + 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; + prev_sides: VS.t HM.t; + divided_side_effects: ((S.Dom.t * (int * divided_side_phase) option) HM.t) HM.t; + orphan_side_effects: S.Dom.t HM.t; rho: S.Dom.t HM.t; wpoint: unit HM.t; stable: unit HM.t; @@ -67,10 +72,15 @@ module Base = type marshal = solver_data - let create_empty_data () = { + let create_empty_data () = + let narrow_sides = GobConfig.get_bool "solvers.td3.narrow-sides.enabled" in + { st = []; infl = HM.create 10; sides = HM.create 10; + prev_sides = HM.create 10; + divided_side_effects = HM.create (if narrow_sides then 10 else 0); + orphan_side_effects = HM.create (if narrow_sides then 10 else 0); rho = HM.create 10; wpoint = HM.create 10; stable = HM.create 10; @@ -119,6 +129,9 @@ module Base = wpoint = HM.copy data.wpoint; infl = HM.copy data.infl; sides = HM.copy data.sides; + prev_sides = HM.copy data.prev_sides; + divided_side_effects = HM.map (fun k v -> HM.copy v) data.divided_side_effects; + orphan_side_effects = HM.copy data.orphan_side_effects; side_infl = HM.copy data.side_infl; side_dep = HM.copy data.side_dep; st = data.st; (* data.st is immutable *) @@ -164,6 +177,20 @@ module Base = HM.iter (fun k v -> HM.replace sides (S.Var.relift k) (VS.map S.Var.relift v) ) data.sides; + 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 orphan_side_effects = HM.create (HM.length data.orphan_side_effects) in + HM.iter (fun k v -> + HM.replace orphan_side_effects (S.Var.relift k) (S.Dom.relift v) + ) data.orphan_side_effects; 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 +216,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; stable; side_dep; side_infl; var_messages; rho_write; dep} + {st; infl; sides; prev_sides; divided_side_effects; orphan_side_effects; rho; wpoint; stable; side_dep; side_infl; var_messages; rho_write; dep} type phase = Widen | Narrow [@@deriving show] (* used in inner solve *) @@ -224,6 +251,9 @@ module Base = let infl = data.infl in let sides = data.sides in + let prev_sides = data.prev_sides in + let divided_side_effects = data.divided_side_effects in + let orphan_side_effects = data.orphan_side_effects in let rho = data.rho in let wpoint = data.wpoint in let stable = data.stable in @@ -246,6 +276,14 @@ module Base = These don't have to be re-verified and warnings can be reused. *) let superstable = HM.copy stable in + let narrow_sides = GobConfig.get_bool "solvers.td3.narrow-sides.enabled" in + let narrow_sides_stable = GobConfig.get_bool "solvers.td3.narrow-sides.stable" in + let narrow_sides_conservative_widen = GobConfig.get_bool "solvers.td3.narrow-sides.conservative-widen" in + let narrow_sides_immediate_growth = GobConfig.get_bool "solvers.td3.narrow-sides.immediate-growth" in + let narrow_sides_gas_default = GobConfig.get_int "solvers.td3.narrow-sides.narrow-gas" in + let narrow_sides_gas_default = if narrow_sides_gas_default < 0 then None else Some (narrow_sides_gas_default, D_Widen) in + let narrow_sides_eliminate_dead = GobConfig.get_bool "solvers.td3.narrow-sides.eliminate-dead" in + let reluctant = GobConfig.get_bool "incremental.reluctant.enabled" in let var_messages = data.var_messages in @@ -315,7 +353,42 @@ 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) + if narrow_sides then + let acc = HM.create 0 in + let changed = HM.create 0 in + Fun.protect ~finally:(fun () -> ( + if narrow_sides_eliminate_dead then begin + let prev_sides_x = HM.find_option prev_sides x in + begin match prev_sides_x with + | Some prev_sides_x -> VS.iter (fun y -> + if Option.is_none @@ HM.find_option 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 (fun x -> solve x Widen) casualties + end; + ) prev_sides_x + | None -> () end; + let new_sides = ref VS.empty in + HM.iter (fun y _ -> new_sides := VS.add y !new_sides) acc; + if VS.is_empty !new_sides then + HM.remove prev_sides x + else + HM.replace prev_sides x !new_sides; + end; + if narrow_sides_immediate_growth && not narrow_sides_stable then + HM.iter (fun y acc -> if not @@ HM.mem changed y then ignore @@ divided_side D_Narrow ~x y acc) acc + else ( + begin if not narrow_sides_immediate_growth then + let op = if narrow_sides_stable then D_Widen else D_Box in + HM.iter (fun y acc -> ignore @@ divided_side op ~x y acc) acc + end; + if narrow_sides_stable && HM.mem stable x then + HM.iter (fun y acc -> ignore @@ divided_side D_Narrow ~x y acc) acc + ) + )) (fun () -> eq x (eval l x) (side_acc acc changed x)) + else + eq x (eval l x) (side ~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 *) @@ -364,6 +437,122 @@ module Base = ) ) ) + and combined_side y = + let combined = match HM.find_option divided_side_effects y with + | Some map -> HM.fold (fun _ (value, _) acc -> S.Dom.join acc value) map (S.Dom.bot ()) + | None -> S.Dom.bot () in + let orphaned = HM.find_default orphan_side_effects y (S.Dom.bot()) in + S.Dom.join combined orphaned + and side_acc acc changed x y d = + 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 + match new_acc with + | Some new_acc -> ( + HM.replace acc y new_acc; + if narrow_sides_immediate_growth then ( + let y_changed = divided_side D_Widen ~x y new_acc in + if y_changed && not @@ narrow_sides_stable then + HM.replace changed y (); + ) + ) + | _ -> () + and reduce_side_narrow_gas (gas, phase) = + if phase = D_Widen then gas - 1, D_Narrow else (gas, phase) + and divided_side (phase:divided_side_phase) ?(do_destabilize=true) ?x y d : bool = + if tracing then trace "side" "divided side to %a from %a ## value: %a" S.Var.pretty_trace y (Pretty.docOpt (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 (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); + init y; + if tracing then trace "sol2" "stable add %a" S.Var.pretty_trace y; + HM.replace stable y (); + + match x with + | Some x -> ( + let sided = match HM.find_option sides y with + | Some sides -> VS.mem x sides + | None -> false in + if not sided then add_sides y x; + let init_divided_side_effects y = if not (HM.mem divided_side_effects y) then HM.replace divided_side_effects y (HM.create 10) in + init_divided_side_effects y; + + let y_sides = HM.find divided_side_effects y in + let (old_side, narrow_gas) = HM.find_default y_sides x (S.Dom.bot (), narrow_sides_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 + (* Potential optimization: don't widen locally if joining does not affect the combined value *) + 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 + (if narrow_sides_conservative_widen && (S.Dom.leq tmp (HM.find rho y)) then + tmp + else + S.Dom.widen old_side tmp), Option.map (fun (x, _) -> (x, D_Widen)) narrow_gas + else old_side, narrow_gas) + | D_Narrow -> + (* TODO: This manual "narrowing" to bot is not nice! + Also, it could break analyses that rely on non-identity addons to values, + like wideningThresholds. Remove this, once domains are fixed so narrowing + with bottom produces bottom. *) + let result = if S.Dom.is_bot d then d else S.Dom.narrow old_side d in + let narrow_gas = if not @@ S.Dom.equal result old_side then + Option.map reduce_side_narrow_gas narrow_gas + else + narrow_gas + in + result, narrow_gas + | _ -> failwith "unreachable" + 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_phase 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 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, grew: %b, shrank: %b) Old value: %a ## New value: %a" + S.Var.pretty_trace y S.Var.pretty_trace x (show_divided_side_phase phase) (S.Dom.leq y_oldval y_newval) (S.Dom.leq y_newval y_oldval) S.Dom.pretty y_oldval S.Dom.pretty y_newval; + HM.replace rho y y_newval; + if do_destabilize then + destabilize y; + ); + true + ) else + false + ) else + false + ) + | None -> ( + let orphaned = HM.find_default orphan_side_effects y (S.Dom.bot ()) in + let wd = S.Dom.widen orphaned (S.Dom.join orphaned d) in + HM.replace orphan_side_effects y wd; + if tracing then trace "side" "orphaned side to %a" S.Var.pretty_trace y; + let y_oldval = HM.find rho y in + if not (S.Dom.leq wd y_oldval) then ( + if tracing then trace "side" "orphaned side changed %a (phase: %s)" S.Var.pretty_trace y (show_divided_side_phase phase); + HM.replace rho y (S.Dom.join wd y_oldval); + if do_destabilize then + destabilize y; + true + ) else + false + ) and eq x get set = if tracing then trace "sol2" "eq %a" S.Var.pretty_trace x; match Hooks.system x with @@ -378,7 +567,12 @@ 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 = + if narrow_sides then + failwith "narrow-sides not yet implemented for simple solve" + else + eq y (eval l x) (side ~x) + in HM.remove called y; if HM.mem wpoint y then (HM.remove l y; solve y Widen; HM.find rho y) else (if cache then HM.replace l y eqd; eqd) @@ -495,7 +689,11 @@ 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; - HM.replace rho x d; + (* TODO: SIDE make this change-proof *) + if narrow_sides then + ignore @@ divided_side ~do_destabilize:false D_Widen x d + else + HM.replace rho x d; HM.replace stable x (); (* solve x Widen *) in @@ -1047,7 +1245,7 @@ module Base = print_data_verbose data "Data after postsolve"; verify_data data; - (rho, {st; infl; sides; rho; wpoint; stable; side_dep; side_infl; var_messages; rho_write; dep}) + (rho, {st; infl; sides; prev_sides; divided_side_effects; orphan_side_effects; rho; wpoint; stable; side_dep; side_infl; var_messages; rho_write; dep}) end (** TD3 with no hooks. *) diff --git a/tests/regression/95-dividedsides/01-modulo-guard.c b/tests/regression/95-dividedsides/01-modulo-guard.c new file mode 100644 index 0000000000..d08b6716e6 --- /dev/null +++ b/tests/regression/95-dividedsides/01-modulo-guard.c @@ -0,0 +1,27 @@ +// PARAM: --enable solvers.td3.narrow-sides.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/95-dividedsides/02-state-machine.c b/tests/regression/95-dividedsides/02-state-machine.c new file mode 100644 index 0000000000..21e3062db8 --- /dev/null +++ b/tests/regression/95-dividedsides/02-state-machine.c @@ -0,0 +1,49 @@ +// PARAM: --enable ana.int.interval --enable solvers.td3.narrow-sides.enabled +#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/95-dividedsides/03-guarded_inc.c b/tests/regression/95-dividedsides/03-guarded_inc.c new file mode 100644 index 0000000000..557f7508a7 --- /dev/null +++ b/tests/regression/95-dividedsides/03-guarded_inc.c @@ -0,0 +1,25 @@ +// PARAM: --enable solvers.td3.narrow-sides.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/95-dividedsides/04-semaphore.c b/tests/regression/95-dividedsides/04-semaphore.c new file mode 100644 index 0000000000..a99c48bd4c --- /dev/null +++ b/tests/regression/95-dividedsides/04-semaphore.c @@ -0,0 +1,67 @@ +// PARAM: --enable solvers.td3.narrow-sides.enabled --enable solvers.td3.narrow-sides.stable --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/95-dividedsides/05-nested_loop.c b/tests/regression/95-dividedsides/05-nested_loop.c new file mode 100644 index 0000000000..3d7c147192 --- /dev/null +++ b/tests/regression/95-dividedsides/05-nested_loop.c @@ -0,0 +1,40 @@ +// PARAM: --enable solvers.td3.narrow-sides.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/95-dividedsides/06-cyclic-dependency.c b/tests/regression/95-dividedsides/06-cyclic-dependency.c new file mode 100644 index 0000000000..fd68e518cf --- /dev/null +++ b/tests/regression/95-dividedsides/06-cyclic-dependency.c @@ -0,0 +1,30 @@ +// PARAM: --enable solvers.td3.narrow-sides.enabled --enable ana.int.interval + +// This is supposed to check if the solver terminates +#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/95-dividedsides/07-ctxt-widen.c b/tests/regression/95-dividedsides/07-ctxt-widen.c new file mode 100644 index 0000000000..78f14cd293 --- /dev/null +++ b/tests/regression/95-dividedsides/07-ctxt-widen.c @@ -0,0 +1,53 @@ +// PARAM: --enable ana.int.interval_set --set ana.context.gas_value 0 --enable solvers.td3.narrow-sides.enabled --enable solvers.td3.narrow-sides.stable +// 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/95-dividedsides/08-ctxt-insensitive.c b/tests/regression/95-dividedsides/08-ctxt-insensitive.c new file mode 100644 index 0000000000..b0e1651e64 --- /dev/null +++ b/tests/regression/95-dividedsides/08-ctxt-insensitive.c @@ -0,0 +1,15 @@ +// 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-sides.enabled --disable solvers.td3.narrow-sides.stable + +int fac(int i) { + if (i > 0) { + return fac(i - 1) * i; + } + assert(i == 0); + return 1; +} + +int main(void) +{ + fac(10); + return 0; +} diff --git a/tests/regression/95-dividedsides/09-longjmp-counting-local.c b/tests/regression/95-dividedsides/09-longjmp-counting-local.c new file mode 100644 index 0000000000..f25c447495 --- /dev/null +++ b/tests/regression/95-dividedsides/09-longjmp-counting-local.c @@ -0,0 +1,22 @@ +// PARAM: --enable solvers.td3.narrow-sides.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/95-dividedsides/10-longjmp-heap-counting-return.c b/tests/regression/95-dividedsides/10-longjmp-heap-counting-return.c new file mode 100644 index 0000000000..e34a388d29 --- /dev/null +++ b/tests/regression/95-dividedsides/10-longjmp-heap-counting-return.c @@ -0,0 +1,18 @@ +// PARAM: --enable ana.int.interval --enable ana.int.enums --enable solvers.td3.narrow-sides.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/95-dividedsides/11-longjmp-counting-return.c b/tests/regression/95-dividedsides/11-longjmp-counting-return.c new file mode 100644 index 0000000000..f9de739691 --- /dev/null +++ b/tests/regression/95-dividedsides/11-longjmp-counting-return.c @@ -0,0 +1,23 @@ +// PARAM: --enable ana.int.interval --enable ana.int.enums --enable solvers.td3.narrow-sides.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/95-dividedsides/12-multiple-growing-updates.c b/tests/regression/95-dividedsides/12-multiple-growing-updates.c new file mode 100644 index 0000000000..ee58e99074 --- /dev/null +++ b/tests/regression/95-dividedsides/12-multiple-growing-updates.c @@ -0,0 +1,31 @@ +// PARAM: --enable ana.int.interval_set --enable solvers.td3.narrow-sides.enabled --enable solvers.td3.narrow-sides.stable +#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/95-dividedsides/13-threaded-ctxt-widen.c b/tests/regression/95-dividedsides/13-threaded-ctxt-widen.c new file mode 100644 index 0000000000..d4f6632cf2 --- /dev/null +++ b/tests/regression/95-dividedsides/13-threaded-ctxt-widen.c @@ -0,0 +1,45 @@ +// PARAM: --enable ana.int.interval_set --set ana.context.gas_value 0 --enable solvers.td3.narrow-sides.enabled --enable solvers.td3.narrow-sides.stable +#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/95-dividedsides/14-widening-thresholds.c b/tests/regression/95-dividedsides/14-widening-thresholds.c new file mode 100644 index 0000000000..43123bccae --- /dev/null +++ b/tests/regression/95-dividedsides/14-widening-thresholds.c @@ -0,0 +1,28 @@ +// PARAM: --enable ana.int.interval --enable ana.int.interval_threshold_widening --set ana.int.interval_threshold_widening_constants comparisons --enable solvers.td3.narrow-sides.enabled --enable solvers.td3.narrow-sides.stable +#include + +//TODO: this tests that threshold widening also narrows correctly. This should not be in this folder +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; +int glob = 0; + +void *thread(void *data) { + int ub = *(int*)data; + for(int i = 0; i < ub; i++) { + pthread_mutex_lock(&mutex); + glob = i + 2; + 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/95-dividedsides/15-intertwined_increment.c b/tests/regression/95-dividedsides/15-intertwined_increment.c new file mode 100644 index 0000000000..9ed177f716 --- /dev/null +++ b/tests/regression/95-dividedsides/15-intertwined_increment.c @@ -0,0 +1,33 @@ +// PARAM: --enable ana.int.interval --enable solvers.td3.narrow-sides.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/95-dividedsides/16-cyclic-dependency-guarded.c b/tests/regression/95-dividedsides/16-cyclic-dependency-guarded.c new file mode 100644 index 0000000000..11a5613a47 --- /dev/null +++ b/tests/regression/95-dividedsides/16-cyclic-dependency-guarded.c @@ -0,0 +1,35 @@ +// PARAM: --enable solvers.td3.narrow-sides.enabled --enable solvers.td3.narrow-sides.stable --set solvers.td3.narrow-sides.narrow-gas 9 --enable ana.int.interval + +// This is supposed to check if the solver terminates +#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; +} \ No newline at end of file diff --git a/tests/regression/95-dividedsides/17-dead-side-effect.c b/tests/regression/95-dividedsides/17-dead-side-effect.c new file mode 100644 index 0000000000..e3b39c53f0 --- /dev/null +++ b/tests/regression/95-dividedsides/17-dead-side-effect.c @@ -0,0 +1,26 @@ +// PARAM: --enable solvers.td3.narrow-sides.enabled --enable ana.int.interval --enable solvers.td3.narrow-sides.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/95-dividedsides/18-dead-side-effect2.c b/tests/regression/95-dividedsides/18-dead-side-effect2.c new file mode 100644 index 0000000000..ffbb337494 --- /dev/null +++ b/tests/regression/95-dividedsides/18-dead-side-effect2.c @@ -0,0 +1,32 @@ +// PARAM: --enable solvers.td3.narrow-sides.enabled --enable ana.int.interval --enable solvers.td3.narrow-sides.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/95-dividedsides/19-dead-side-effect3.c b/tests/regression/95-dividedsides/19-dead-side-effect3.c new file mode 100644 index 0000000000..b143cad9a3 --- /dev/null +++ b/tests/regression/95-dividedsides/19-dead-side-effect3.c @@ -0,0 +1,29 @@ +// PARAM: --enable ana.int.interval --enable solvers.td3.narrow-sides.enabled --enable solvers.td3.narrow-sides.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/95-dividedsides/20-dead-side-effect4.c b/tests/regression/95-dividedsides/20-dead-side-effect4.c new file mode 100644 index 0000000000..24db427997 --- /dev/null +++ b/tests/regression/95-dividedsides/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-sides.enabled --enable solvers.td3.narrow-sides.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/95-dividedsides/21-dead-escape.c b/tests/regression/95-dividedsides/21-dead-escape.c new file mode 100644 index 0000000000..61480a1346 --- /dev/null +++ b/tests/regression/95-dividedsides/21-dead-escape.c @@ -0,0 +1,39 @@ +// PARAM: --enable solvers.td3.narrow-sides.enabled --enable ana.int.interval --enable solvers.td3.narrow-sides.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); + // Paradoxically, a != &i is not known without eliminate-dead. + __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/regression/95-dividedsides/22-dead-escape-indirect.c b/tests/regression/95-dividedsides/22-dead-escape-indirect.c new file mode 100644 index 0000000000..6b26288431 --- /dev/null +++ b/tests/regression/95-dividedsides/22-dead-escape-indirect.c @@ -0,0 +1,37 @@ +// PARAM: --enable solvers.td3.narrow-sides.enabled --enable ana.int.interval --enable solvers.td3.narrow-sides.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) From 0153efaf716687dadaa1be91b53425be1e56a827 Mon Sep 17 00:00:00 2001 From: Fabian Stemmler Date: Thu, 28 Nov 2024 12:11:13 +0100 Subject: [PATCH 02/36] rename narrow-sides to narrow-globs for consistency with paper --- src/config/options.schema.json | 16 +++---- src/maingoblint.ml | 8 ++-- src/solver/td3.ml | 46 +++++++++---------- .../95-dividedsides/01-modulo-guard.c | 2 +- .../95-dividedsides/02-state-machine.c | 2 +- .../95-dividedsides/03-guarded_inc.c | 2 +- .../regression/95-dividedsides/04-semaphore.c | 2 +- .../95-dividedsides/05-nested_loop.c | 2 +- .../95-dividedsides/06-cyclic-dependency.c | 2 +- .../95-dividedsides/07-ctxt-widen.c | 2 +- .../95-dividedsides/08-ctxt-insensitive.c | 2 +- .../09-longjmp-counting-local.c | 2 +- .../10-longjmp-heap-counting-return.c | 2 +- .../11-longjmp-counting-return.c | 2 +- .../12-multiple-growing-updates.c | 2 +- .../95-dividedsides/13-threaded-ctxt-widen.c | 2 +- .../95-dividedsides/14-widening-thresholds.c | 2 +- .../15-intertwined_increment.c | 2 +- .../16-cyclic-dependency-guarded.c | 2 +- .../95-dividedsides/17-dead-side-effect.c | 2 +- .../95-dividedsides/18-dead-side-effect2.c | 2 +- .../95-dividedsides/19-dead-side-effect3.c | 2 +- .../95-dividedsides/20-dead-side-effect4.c | 2 +- .../95-dividedsides/21-dead-escape.c | 2 +- .../95-dividedsides/22-dead-escape-indirect.c | 2 +- 25 files changed, 57 insertions(+), 57 deletions(-) diff --git a/src/config/options.schema.json b/src/config/options.schema.json index a1717dfacd..355f3bff55 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -2435,42 +2435,42 @@ "type": "boolean", "default": true }, - "narrow-sides": { - "title": "solvers.td3.narrow-sides", + "narrow-globs": { + "title": "solvers.td3.narrow-globs", "type": "object", "properties": { "enabled": { - "title": "solvers.td3.narrow-sides.enabled", + "title": "solvers.td3.narrow-globs.enabled", "description": "Individually track side-effects from different unknowns to enable narrowing of globals.", "type": "boolean", "default": false }, "stable": { - "title": "solvers.td3.narrow-sides.stable", + "title": "solvers.td3.narrow-globs.stable", "description": "Controls when to narrow. true: If unknown remains stable after evaluating its rhs, apply all sides with narrowing. false: Apply sides that did not increase with narrowing.", "type": "boolean", "default": false }, "conservative-widen": { - "title": "solvers.td3.narrow-sides.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-sides.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-sides.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": -1 }, "eliminate-dead": { - "title": "solvers.td3.narrow-sides.eliminate-dead", + "title": "solvers.td3.narrow-globs.eliminate-dead", "description": "side-effects that no longer occur are narrowed with bot.", "type": "boolean", "default": false diff --git a/src/maingoblint.ml b/src/maingoblint.ml index b74dfdd0cd..2d4b6b9ebe 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -167,10 +167,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-sides.enabled" then fail "solvers.td3.space is incompatible with solvers.td3.narrow-sides"; - if (get_bool "incremental.load" || get_bool "incremental.save") && get_bool "solvers.td3.narrow-sides.enabled" then ( - set_bool "solvers.td3.narrow-sides.enabled" false; - warn "solvers.td3.narrow-sides implicitly disabled by incremental analysis"; + 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 ( + set_bool "solvers.td3.narrow-globs.enabled" false; + warn "solvers.td3.narrow-globs.enabled implicitly disabled by incremental analysis"; ); 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"; diff --git a/src/solver/td3.ml b/src/solver/td3.ml index a7a4ca25e3..44d3b28716 100644 --- a/src/solver/td3.ml +++ b/src/solver/td3.ml @@ -73,14 +73,14 @@ module Base = type marshal = solver_data let create_empty_data () = - let narrow_sides = GobConfig.get_bool "solvers.td3.narrow-sides.enabled" in + let narrow_globs = GobConfig.get_bool "solvers.td3.narrow-globs.enabled" in { st = []; infl = HM.create 10; sides = HM.create 10; prev_sides = HM.create 10; - divided_side_effects = HM.create (if narrow_sides then 10 else 0); - orphan_side_effects = HM.create (if narrow_sides then 10 else 0); + divided_side_effects = HM.create (if narrow_globs then 10 else 0); + orphan_side_effects = HM.create (if narrow_globs then 10 else 0); rho = HM.create 10; wpoint = HM.create 10; stable = HM.create 10; @@ -276,13 +276,13 @@ module Base = These don't have to be re-verified and warnings can be reused. *) let superstable = HM.copy stable in - let narrow_sides = GobConfig.get_bool "solvers.td3.narrow-sides.enabled" in - let narrow_sides_stable = GobConfig.get_bool "solvers.td3.narrow-sides.stable" in - let narrow_sides_conservative_widen = GobConfig.get_bool "solvers.td3.narrow-sides.conservative-widen" in - let narrow_sides_immediate_growth = GobConfig.get_bool "solvers.td3.narrow-sides.immediate-growth" in - let narrow_sides_gas_default = GobConfig.get_int "solvers.td3.narrow-sides.narrow-gas" in - let narrow_sides_gas_default = if narrow_sides_gas_default < 0 then None else Some (narrow_sides_gas_default, D_Widen) in - let narrow_sides_eliminate_dead = GobConfig.get_bool "solvers.td3.narrow-sides.eliminate-dead" in + let narrow_globs = GobConfig.get_bool "solvers.td3.narrow-globs.enabled" in + let narrow_globs_stable = GobConfig.get_bool "solvers.td3.narrow-globs.stable" in + let narrow_globs_conservative_widen = GobConfig.get_bool "solvers.td3.narrow-globs.conservative-widen" in + let narrow_globs_immediate_growth = GobConfig.get_bool "solvers.td3.narrow-globs.immediate-growth" in + let narrow_globs_gas_default = GobConfig.get_int "solvers.td3.narrow-globs.narrow-gas" in + let narrow_globs_gas_default = if narrow_globs_gas_default < 0 then None else Some (narrow_globs_gas_default, D_Widen) in + let narrow_globs_eliminate_dead = GobConfig.get_bool "solvers.td3.narrow-globs.eliminate-dead" in let reluctant = GobConfig.get_bool "incremental.reluctant.enabled" in @@ -353,11 +353,11 @@ module Base = | _ -> (* The RHS is re-evaluated, all deps are re-trigerred *) HM.replace dep x VS.empty; - if narrow_sides then + if narrow_globs then let acc = HM.create 0 in let changed = HM.create 0 in Fun.protect ~finally:(fun () -> ( - if narrow_sides_eliminate_dead then begin + if narrow_globs_eliminate_dead then begin let prev_sides_x = HM.find_option prev_sides x in begin match prev_sides_x with | Some prev_sides_x -> VS.iter (fun y -> @@ -376,14 +376,14 @@ module Base = else HM.replace prev_sides x !new_sides; end; - if narrow_sides_immediate_growth && not narrow_sides_stable then + if narrow_globs_immediate_growth && not narrow_globs_stable then HM.iter (fun y acc -> if not @@ HM.mem changed y then ignore @@ divided_side D_Narrow ~x y acc) acc else ( - begin if not narrow_sides_immediate_growth then - let op = if narrow_sides_stable then D_Widen else D_Box in + begin if not narrow_globs_immediate_growth then + let op = if narrow_globs_stable then D_Widen else D_Box in HM.iter (fun y acc -> ignore @@ divided_side op ~x y acc) acc end; - if narrow_sides_stable && HM.mem stable x then + if narrow_globs_stable && HM.mem stable x then HM.iter (fun y acc -> ignore @@ divided_side D_Narrow ~x y acc) acc ) )) (fun () -> eq x (eval l x) (side_acc acc changed x)) @@ -450,9 +450,9 @@ module Base = match new_acc with | Some new_acc -> ( HM.replace acc y new_acc; - if narrow_sides_immediate_growth then ( + if narrow_globs_immediate_growth then ( let y_changed = divided_side D_Widen ~x y new_acc in - if y_changed && not @@ narrow_sides_stable then + if y_changed && not @@ narrow_globs_stable then HM.replace changed y (); ) ) @@ -480,7 +480,7 @@ module Base = init_divided_side_effects y; let y_sides = HM.find divided_side_effects y in - let (old_side, narrow_gas) = HM.find_default y_sides x (S.Dom.bot (), narrow_sides_gas_default) 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 @@ -492,7 +492,7 @@ module Base = | D_Widen -> ( let tmp = S.Dom.join old_side d in if not @@ S.Dom.equal tmp old_side then - (if narrow_sides_conservative_widen && (S.Dom.leq tmp (HM.find rho y)) then + (if narrow_globs_conservative_widen && (S.Dom.leq tmp (HM.find rho y)) then tmp else S.Dom.widen old_side tmp), Option.map (fun (x, _) -> (x, D_Widen)) narrow_gas @@ -568,8 +568,8 @@ module Base = else ( HM.replace called y (); let eqd = - if narrow_sides then - failwith "narrow-sides not yet implemented for simple solve" + if narrow_globs then + failwith "narrow-globs not yet implemented for simple solve" else eq y (eval l x) (side ~x) in @@ -690,7 +690,7 @@ module Base = if tracing then trace "sol2" "set_start %a ## %a" S.Var.pretty_trace x S.Dom.pretty d; init x; (* TODO: SIDE make this change-proof *) - if narrow_sides then + if narrow_globs then ignore @@ divided_side ~do_destabilize:false D_Widen x d else HM.replace rho x d; diff --git a/tests/regression/95-dividedsides/01-modulo-guard.c b/tests/regression/95-dividedsides/01-modulo-guard.c index d08b6716e6..14cbc7a692 100644 --- a/tests/regression/95-dividedsides/01-modulo-guard.c +++ b/tests/regression/95-dividedsides/01-modulo-guard.c @@ -1,4 +1,4 @@ -// PARAM: --enable solvers.td3.narrow-sides.enabled --enable ana.int.interval +// PARAM: --enable solvers.td3.narrow-globs.enabled --enable ana.int.interval #include #include diff --git a/tests/regression/95-dividedsides/02-state-machine.c b/tests/regression/95-dividedsides/02-state-machine.c index 21e3062db8..f144768793 100644 --- a/tests/regression/95-dividedsides/02-state-machine.c +++ b/tests/regression/95-dividedsides/02-state-machine.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.int.interval --enable solvers.td3.narrow-sides.enabled +// PARAM: --enable ana.int.interval --enable solvers.td3.narrow-globs.enabled #include int state = 0; diff --git a/tests/regression/95-dividedsides/03-guarded_inc.c b/tests/regression/95-dividedsides/03-guarded_inc.c index 557f7508a7..9245750b1a 100644 --- a/tests/regression/95-dividedsides/03-guarded_inc.c +++ b/tests/regression/95-dividedsides/03-guarded_inc.c @@ -1,4 +1,4 @@ -// PARAM: --enable solvers.td3.narrow-sides.enabled --enable ana.int.interval --enable ana.base.priv.protection.changes-only +// PARAM: --enable solvers.td3.narrow-globs.enabled --enable ana.int.interval --enable ana.base.priv.protection.changes-only #include #include #include diff --git a/tests/regression/95-dividedsides/04-semaphore.c b/tests/regression/95-dividedsides/04-semaphore.c index a99c48bd4c..a4296b4423 100644 --- a/tests/regression/95-dividedsides/04-semaphore.c +++ b/tests/regression/95-dividedsides/04-semaphore.c @@ -1,4 +1,4 @@ -// PARAM: --enable solvers.td3.narrow-sides.enabled --enable solvers.td3.narrow-sides.stable --enable ana.int.interval --enable ana.base.priv.protection.changes-only +// PARAM: --enable solvers.td3.narrow-globs.enabled --enable solvers.td3.narrow-globs.stable --enable ana.int.interval --enable ana.base.priv.protection.changes-only #include #include #include diff --git a/tests/regression/95-dividedsides/05-nested_loop.c b/tests/regression/95-dividedsides/05-nested_loop.c index 3d7c147192..4047a6c92b 100644 --- a/tests/regression/95-dividedsides/05-nested_loop.c +++ b/tests/regression/95-dividedsides/05-nested_loop.c @@ -1,4 +1,4 @@ -// PARAM: --enable solvers.td3.narrow-sides.enabled --enable ana.int.interval +// PARAM: --enable solvers.td3.narrow-globs.enabled --enable ana.int.interval #include #include #include diff --git a/tests/regression/95-dividedsides/06-cyclic-dependency.c b/tests/regression/95-dividedsides/06-cyclic-dependency.c index fd68e518cf..e7640bbc62 100644 --- a/tests/regression/95-dividedsides/06-cyclic-dependency.c +++ b/tests/regression/95-dividedsides/06-cyclic-dependency.c @@ -1,4 +1,4 @@ -// PARAM: --enable solvers.td3.narrow-sides.enabled --enable ana.int.interval +// PARAM: --enable solvers.td3.narrow-globs.enabled --enable ana.int.interval // This is supposed to check if the solver terminates #include diff --git a/tests/regression/95-dividedsides/07-ctxt-widen.c b/tests/regression/95-dividedsides/07-ctxt-widen.c index 78f14cd293..1819f2b842 100644 --- a/tests/regression/95-dividedsides/07-ctxt-widen.c +++ b/tests/regression/95-dividedsides/07-ctxt-widen.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.int.interval_set --set ana.context.gas_value 0 --enable solvers.td3.narrow-sides.enabled --enable solvers.td3.narrow-sides.stable +// PARAM: --enable ana.int.interval_set --set ana.context.gas_value 0 --enable solvers.td3.narrow-globs.enabled --enable solvers.td3.narrow-globs.stable // Taken from context gas tests, where the assertions were unknown. #include diff --git a/tests/regression/95-dividedsides/08-ctxt-insensitive.c b/tests/regression/95-dividedsides/08-ctxt-insensitive.c index b0e1651e64..78297700ad 100644 --- a/tests/regression/95-dividedsides/08-ctxt-insensitive.c +++ b/tests/regression/95-dividedsides/08-ctxt-insensitive.c @@ -1,4 +1,4 @@ -// 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-sides.enabled --disable solvers.td3.narrow-sides.stable +// 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 --disable solvers.td3.narrow-globs.stable int fac(int i) { if (i > 0) { diff --git a/tests/regression/95-dividedsides/09-longjmp-counting-local.c b/tests/regression/95-dividedsides/09-longjmp-counting-local.c index f25c447495..20d2ae4e9c 100644 --- a/tests/regression/95-dividedsides/09-longjmp-counting-local.c +++ b/tests/regression/95-dividedsides/09-longjmp-counting-local.c @@ -1,4 +1,4 @@ -// PARAM: --enable solvers.td3.narrow-sides.enabled --enable ana.int.interval --disable exp.volatiles_are_top +// PARAM: --enable solvers.td3.narrow-globs.enabled --enable ana.int.interval --disable exp.volatiles_are_top #include #include #include diff --git a/tests/regression/95-dividedsides/10-longjmp-heap-counting-return.c b/tests/regression/95-dividedsides/10-longjmp-heap-counting-return.c index e34a388d29..08ba46bd05 100644 --- a/tests/regression/95-dividedsides/10-longjmp-heap-counting-return.c +++ b/tests/regression/95-dividedsides/10-longjmp-heap-counting-return.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.int.interval --enable ana.int.enums --enable solvers.td3.narrow-sides.enabled --enable exp.earlyglobs --set ana.setjmp.split none --disable exp.volatiles_are_top +// 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 diff --git a/tests/regression/95-dividedsides/11-longjmp-counting-return.c b/tests/regression/95-dividedsides/11-longjmp-counting-return.c index f9de739691..193f604acc 100644 --- a/tests/regression/95-dividedsides/11-longjmp-counting-return.c +++ b/tests/regression/95-dividedsides/11-longjmp-counting-return.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.int.interval --enable ana.int.enums --enable solvers.td3.narrow-sides.enabled --set ana.setjmp.split none +// PARAM: --enable ana.int.interval --enable ana.int.enums --enable solvers.td3.narrow-globs.enabled --set ana.setjmp.split none #include #include diff --git a/tests/regression/95-dividedsides/12-multiple-growing-updates.c b/tests/regression/95-dividedsides/12-multiple-growing-updates.c index ee58e99074..cd831349a6 100644 --- a/tests/regression/95-dividedsides/12-multiple-growing-updates.c +++ b/tests/regression/95-dividedsides/12-multiple-growing-updates.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.int.interval_set --enable solvers.td3.narrow-sides.enabled --enable solvers.td3.narrow-sides.stable +// PARAM: --enable ana.int.interval_set --enable solvers.td3.narrow-globs.enabled --enable solvers.td3.narrow-globs.stable #include pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; diff --git a/tests/regression/95-dividedsides/13-threaded-ctxt-widen.c b/tests/regression/95-dividedsides/13-threaded-ctxt-widen.c index d4f6632cf2..aa10fc0a70 100644 --- a/tests/regression/95-dividedsides/13-threaded-ctxt-widen.c +++ b/tests/regression/95-dividedsides/13-threaded-ctxt-widen.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.int.interval_set --set ana.context.gas_value 0 --enable solvers.td3.narrow-sides.enabled --enable solvers.td3.narrow-sides.stable +// PARAM: --enable ana.int.interval_set --set ana.context.gas_value 0 --enable solvers.td3.narrow-globs.enabled --enable solvers.td3.narrow-globs.stable #include pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; diff --git a/tests/regression/95-dividedsides/14-widening-thresholds.c b/tests/regression/95-dividedsides/14-widening-thresholds.c index 43123bccae..9ce4acc6ee 100644 --- a/tests/regression/95-dividedsides/14-widening-thresholds.c +++ b/tests/regression/95-dividedsides/14-widening-thresholds.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.int.interval --enable ana.int.interval_threshold_widening --set ana.int.interval_threshold_widening_constants comparisons --enable solvers.td3.narrow-sides.enabled --enable solvers.td3.narrow-sides.stable +// 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 --enable solvers.td3.narrow-globs.stable #include //TODO: this tests that threshold widening also narrows correctly. This should not be in this folder diff --git a/tests/regression/95-dividedsides/15-intertwined_increment.c b/tests/regression/95-dividedsides/15-intertwined_increment.c index 9ed177f716..0d5e1f5aae 100644 --- a/tests/regression/95-dividedsides/15-intertwined_increment.c +++ b/tests/regression/95-dividedsides/15-intertwined_increment.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.int.interval --enable solvers.td3.narrow-sides.enabled +// PARAM: --enable ana.int.interval --enable solvers.td3.narrow-globs.enabled #include #include diff --git a/tests/regression/95-dividedsides/16-cyclic-dependency-guarded.c b/tests/regression/95-dividedsides/16-cyclic-dependency-guarded.c index 11a5613a47..f4e40a6447 100644 --- a/tests/regression/95-dividedsides/16-cyclic-dependency-guarded.c +++ b/tests/regression/95-dividedsides/16-cyclic-dependency-guarded.c @@ -1,4 +1,4 @@ -// PARAM: --enable solvers.td3.narrow-sides.enabled --enable solvers.td3.narrow-sides.stable --set solvers.td3.narrow-sides.narrow-gas 9 --enable ana.int.interval +// PARAM: --enable solvers.td3.narrow-globs.enabled --enable solvers.td3.narrow-globs.stable --set solvers.td3.narrow-globs.narrow-gas 9 --enable ana.int.interval // This is supposed to check if the solver terminates #include diff --git a/tests/regression/95-dividedsides/17-dead-side-effect.c b/tests/regression/95-dividedsides/17-dead-side-effect.c index e3b39c53f0..6bf2864ec0 100644 --- a/tests/regression/95-dividedsides/17-dead-side-effect.c +++ b/tests/regression/95-dividedsides/17-dead-side-effect.c @@ -1,4 +1,4 @@ -// PARAM: --enable solvers.td3.narrow-sides.enabled --enable ana.int.interval --enable solvers.td3.narrow-sides.eliminate-dead --enable ana.base.priv.protection.changes-only +// 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 diff --git a/tests/regression/95-dividedsides/18-dead-side-effect2.c b/tests/regression/95-dividedsides/18-dead-side-effect2.c index ffbb337494..81e1e09706 100644 --- a/tests/regression/95-dividedsides/18-dead-side-effect2.c +++ b/tests/regression/95-dividedsides/18-dead-side-effect2.c @@ -1,4 +1,4 @@ -// PARAM: --enable solvers.td3.narrow-sides.enabled --enable ana.int.interval --enable solvers.td3.narrow-sides.eliminate-dead --enable ana.base.priv.protection.changes-only +// 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 diff --git a/tests/regression/95-dividedsides/19-dead-side-effect3.c b/tests/regression/95-dividedsides/19-dead-side-effect3.c index b143cad9a3..bef3c7e001 100644 --- a/tests/regression/95-dividedsides/19-dead-side-effect3.c +++ b/tests/regression/95-dividedsides/19-dead-side-effect3.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.int.interval --enable solvers.td3.narrow-sides.enabled --enable solvers.td3.narrow-sides.eliminate-dead --enable ana.base.priv.protection.changes-only +// 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; diff --git a/tests/regression/95-dividedsides/20-dead-side-effect4.c b/tests/regression/95-dividedsides/20-dead-side-effect4.c index 24db427997..c437321f4c 100644 --- a/tests/regression/95-dividedsides/20-dead-side-effect4.c +++ b/tests/regression/95-dividedsides/20-dead-side-effect4.c @@ -1,4 +1,4 @@ -// PARAM: --disable ana.int.def_exc --enable ana.int.interval --set ana.context.gas_value 0 --enable solvers.td3.narrow-sides.enabled --enable solvers.td3.narrow-sides.eliminate-dead --enable ana.base.priv.protection.changes-only +// 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; diff --git a/tests/regression/95-dividedsides/21-dead-escape.c b/tests/regression/95-dividedsides/21-dead-escape.c index 61480a1346..401db937bc 100644 --- a/tests/regression/95-dividedsides/21-dead-escape.c +++ b/tests/regression/95-dividedsides/21-dead-escape.c @@ -1,4 +1,4 @@ -// PARAM: --enable solvers.td3.narrow-sides.enabled --enable ana.int.interval --enable solvers.td3.narrow-sides.eliminate-dead --enable ana.base.priv.protection.changes-only +// 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 diff --git a/tests/regression/95-dividedsides/22-dead-escape-indirect.c b/tests/regression/95-dividedsides/22-dead-escape-indirect.c index 6b26288431..cab62e7403 100644 --- a/tests/regression/95-dividedsides/22-dead-escape-indirect.c +++ b/tests/regression/95-dividedsides/22-dead-escape-indirect.c @@ -1,4 +1,4 @@ -// PARAM: --enable solvers.td3.narrow-sides.enabled --enable ana.int.interval --enable solvers.td3.narrow-sides.eliminate-dead --enable ana.base.priv.protection.changes-only +// 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 From 56302fcc8e8662d2402c6b4c204e6809f817ef68 Mon Sep 17 00:00:00 2001 From: Fabian Stemmler Date: Sun, 1 Dec 2024 17:59:55 +0100 Subject: [PATCH 03/36] remove outdated comment --- src/solver/td3.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/solver/td3.ml b/src/solver/td3.ml index 44d3b28716..232459ee20 100644 --- a/src/solver/td3.ml +++ b/src/solver/td3.ml @@ -486,7 +486,6 @@ module Base = else phase in - (* Potential optimization: don't widen locally if joining does not affect the combined value *) if not (phase = D_Narrow && narrow_gas = Some (0, D_Widen)) then ( let (new_side, narrow_gas) = match phase with | D_Widen -> ( From adc1070942ad0870e2e607b0cc0d18ae1bc45d76 Mon Sep 17 00:00:00 2001 From: Fabian Stemmler Date: Sun, 1 Dec 2024 18:00:38 +0100 Subject: [PATCH 04/36] account for fixed narrowing with bot in the upstream --- src/solver/td3.ml | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/solver/td3.ml b/src/solver/td3.ml index 232459ee20..d90ababd66 100644 --- a/src/solver/td3.ml +++ b/src/solver/td3.ml @@ -497,11 +497,7 @@ module Base = S.Dom.widen old_side tmp), Option.map (fun (x, _) -> (x, D_Widen)) narrow_gas else old_side, narrow_gas) | D_Narrow -> - (* TODO: This manual "narrowing" to bot is not nice! - Also, it could break analyses that rely on non-identity addons to values, - like wideningThresholds. Remove this, once domains are fixed so narrowing - with bottom produces bottom. *) - let result = if S.Dom.is_bot d then d else S.Dom.narrow old_side d in + let result = S.Dom.narrow old_side d in let narrow_gas = if not @@ S.Dom.equal result old_side then Option.map reduce_side_narrow_gas narrow_gas else From 17bb74f7ac486938ea4d8030213746973281f36b Mon Sep 17 00:00:00 2001 From: Fabian Stemmler Date: Mon, 2 Dec 2024 12:30:04 +0100 Subject: [PATCH 05/36] remove superfluous feature (narrow-globs.stable) and adjust tests --- src/config/options.schema.json | 6 ----- src/solver/td3.ml | 26 +++++++------------ .../regression/95-dividedsides/04-semaphore.c | 2 +- .../95-dividedsides/06-cyclic-dependency.c | 2 +- .../95-dividedsides/07-ctxt-widen.c | 2 +- .../95-dividedsides/08-ctxt-insensitive.c | 2 +- .../12-multiple-growing-updates.c | 2 +- .../95-dividedsides/13-threaded-ctxt-widen.c | 2 +- .../95-dividedsides/14-widening-thresholds.c | 7 ++--- .../16-cyclic-dependency-guarded.c | 2 +- 10 files changed, 21 insertions(+), 32 deletions(-) diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 355f3bff55..fb0a203f0c 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -2445,12 +2445,6 @@ "type": "boolean", "default": false }, - "stable": { - "title": "solvers.td3.narrow-globs.stable", - "description": "Controls when to narrow. true: If unknown remains stable after evaluating its rhs, apply all sides with narrowing. false: Apply sides that did not increase with narrowing.", - "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", diff --git a/src/solver/td3.ml b/src/solver/td3.ml index d90ababd66..326f2c4df0 100644 --- a/src/solver/td3.ml +++ b/src/solver/td3.ml @@ -51,14 +51,14 @@ module Base = module VS = Set.Make (S.Var) let exists_key f hm = HM.exists (fun k _ -> f k) hm - type divided_side_phase = D_Widen | D_Narrow | D_Box [@@deriving show] + type divided_side_mode = D_Widen | D_Narrow | D_Box [@@deriving show] 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; prev_sides: VS.t HM.t; - divided_side_effects: ((S.Dom.t * (int * divided_side_phase) option) HM.t) HM.t; + divided_side_effects: ((S.Dom.t * (int * divided_side_mode) option) HM.t) HM.t; orphan_side_effects: S.Dom.t HM.t; rho: S.Dom.t HM.t; wpoint: unit HM.t; @@ -277,7 +277,6 @@ module Base = let superstable = HM.copy stable in let narrow_globs = GobConfig.get_bool "solvers.td3.narrow-globs.enabled" in - let narrow_globs_stable = GobConfig.get_bool "solvers.td3.narrow-globs.stable" in let narrow_globs_conservative_widen = GobConfig.get_bool "solvers.td3.narrow-globs.conservative-widen" in let narrow_globs_immediate_growth = GobConfig.get_bool "solvers.td3.narrow-globs.immediate-growth" in let narrow_globs_gas_default = GobConfig.get_int "solvers.td3.narrow-globs.narrow-gas" in @@ -376,15 +375,10 @@ module Base = else HM.replace prev_sides x !new_sides; end; - if narrow_globs_immediate_growth && not narrow_globs_stable then + 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 ( - begin if not narrow_globs_immediate_growth then - let op = if narrow_globs_stable then D_Widen else D_Box in - HM.iter (fun y acc -> ignore @@ divided_side op ~x y acc) acc - end; - if narrow_globs_stable && HM.mem stable x then - HM.iter (fun y acc -> ignore @@ divided_side D_Narrow ~x y acc) acc + HM.iter (fun y acc -> ignore @@ divided_side D_Box ~x y acc) acc ) )) (fun () -> eq x (eval l x) (side_acc acc changed x)) else @@ -452,14 +446,14 @@ module Base = 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 && not @@ narrow_globs_stable then + if y_changed then HM.replace changed y (); ) ) | _ -> () and reduce_side_narrow_gas (gas, phase) = if phase = D_Widen then gas - 1, D_Narrow else (gas, phase) - and divided_side (phase:divided_side_phase) ?(do_destabilize=true) ?x y d : bool = + and divided_side (phase:divided_side_mode) ?(do_destabilize=true) ?x y d : bool = if tracing then trace "side" "divided side to %a from %a ## value: %a" S.Var.pretty_trace y (Pretty.docOpt (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 (Pretty.docOpt (S.Var.pretty_trace ())) x S.Dom.pretty d; if Hooks.system y <> None then ( @@ -508,7 +502,7 @@ module Base = 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_phase phase) S.Dom.pretty old_side S.Dom.pretty new_side; + 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 @@ -521,8 +515,8 @@ module Base = 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, grew: %b, shrank: %b) Old value: %a ## New value: %a" - S.Var.pretty_trace y S.Var.pretty_trace x (show_divided_side_phase phase) (S.Dom.leq y_oldval y_newval) (S.Dom.leq y_newval y_oldval) S.Dom.pretty y_oldval S.Dom.pretty y_newval; + 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; if do_destabilize then destabilize y; @@ -540,7 +534,7 @@ module Base = if tracing then trace "side" "orphaned side to %a" S.Var.pretty_trace y; let y_oldval = HM.find rho y in if not (S.Dom.leq wd y_oldval) then ( - if tracing then trace "side" "orphaned side changed %a (phase: %s)" S.Var.pretty_trace y (show_divided_side_phase phase); + if tracing then trace "side" "orphaned side changed %a (phase: %s)" S.Var.pretty_trace y (show_divided_side_mode phase); HM.replace rho y (S.Dom.join wd y_oldval); if do_destabilize then destabilize y; diff --git a/tests/regression/95-dividedsides/04-semaphore.c b/tests/regression/95-dividedsides/04-semaphore.c index a4296b4423..7450ce8bf5 100644 --- a/tests/regression/95-dividedsides/04-semaphore.c +++ b/tests/regression/95-dividedsides/04-semaphore.c @@ -1,4 +1,4 @@ -// PARAM: --enable solvers.td3.narrow-globs.enabled --enable solvers.td3.narrow-globs.stable --enable ana.int.interval --enable ana.base.priv.protection.changes-only +// PARAM: --enable solvers.td3.narrow-globs.enabled --enable ana.int.interval --enable ana.base.priv.protection.changes-only #include #include #include diff --git a/tests/regression/95-dividedsides/06-cyclic-dependency.c b/tests/regression/95-dividedsides/06-cyclic-dependency.c index e7640bbc62..8dd45db86b 100644 --- a/tests/regression/95-dividedsides/06-cyclic-dependency.c +++ b/tests/regression/95-dividedsides/06-cyclic-dependency.c @@ -1,6 +1,6 @@ // PARAM: --enable solvers.td3.narrow-globs.enabled --enable ana.int.interval +// NOTIMEOUT -// This is supposed to check if the solver terminates #include #include diff --git a/tests/regression/95-dividedsides/07-ctxt-widen.c b/tests/regression/95-dividedsides/07-ctxt-widen.c index 1819f2b842..92fe3371e8 100644 --- a/tests/regression/95-dividedsides/07-ctxt-widen.c +++ b/tests/regression/95-dividedsides/07-ctxt-widen.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.int.interval_set --set ana.context.gas_value 0 --enable solvers.td3.narrow-globs.enabled --enable solvers.td3.narrow-globs.stable +// 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 diff --git a/tests/regression/95-dividedsides/08-ctxt-insensitive.c b/tests/regression/95-dividedsides/08-ctxt-insensitive.c index 78297700ad..6ded214460 100644 --- a/tests/regression/95-dividedsides/08-ctxt-insensitive.c +++ b/tests/regression/95-dividedsides/08-ctxt-insensitive.c @@ -1,4 +1,4 @@ -// 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 --disable solvers.td3.narrow-globs.stable +// 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 int fac(int i) { if (i > 0) { diff --git a/tests/regression/95-dividedsides/12-multiple-growing-updates.c b/tests/regression/95-dividedsides/12-multiple-growing-updates.c index cd831349a6..52952c752e 100644 --- a/tests/regression/95-dividedsides/12-multiple-growing-updates.c +++ b/tests/regression/95-dividedsides/12-multiple-growing-updates.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.int.interval_set --enable solvers.td3.narrow-globs.enabled --enable solvers.td3.narrow-globs.stable +// PARAM: --enable ana.int.interval_set --enable solvers.td3.narrow-globs.enabled #include pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; diff --git a/tests/regression/95-dividedsides/13-threaded-ctxt-widen.c b/tests/regression/95-dividedsides/13-threaded-ctxt-widen.c index aa10fc0a70..9cad9d63a8 100644 --- a/tests/regression/95-dividedsides/13-threaded-ctxt-widen.c +++ b/tests/regression/95-dividedsides/13-threaded-ctxt-widen.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.int.interval_set --set ana.context.gas_value 0 --enable solvers.td3.narrow-globs.enabled --enable solvers.td3.narrow-globs.stable +// PARAM: --enable ana.int.interval_set --set ana.context.gas_value 0 --enable solvers.td3.narrow-globs.enabled #include pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; diff --git a/tests/regression/95-dividedsides/14-widening-thresholds.c b/tests/regression/95-dividedsides/14-widening-thresholds.c index 9ce4acc6ee..170c7a9537 100644 --- a/tests/regression/95-dividedsides/14-widening-thresholds.c +++ b/tests/regression/95-dividedsides/14-widening-thresholds.c @@ -1,4 +1,4 @@ -// 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 --enable solvers.td3.narrow-globs.stable +// 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 //TODO: this tests that threshold widening also narrows correctly. This should not be in this folder @@ -7,9 +7,10 @@ int glob = 0; void *thread(void *data) { int ub = *(int*)data; - for(int i = 0; i < ub; i++) { + for(int i = 0; i < 256;) { + i += 2; pthread_mutex_lock(&mutex); - glob = i + 2; + glob = i; pthread_mutex_unlock(&mutex); } return NULL; diff --git a/tests/regression/95-dividedsides/16-cyclic-dependency-guarded.c b/tests/regression/95-dividedsides/16-cyclic-dependency-guarded.c index f4e40a6447..a555823c9d 100644 --- a/tests/regression/95-dividedsides/16-cyclic-dependency-guarded.c +++ b/tests/regression/95-dividedsides/16-cyclic-dependency-guarded.c @@ -1,4 +1,4 @@ -// PARAM: --enable solvers.td3.narrow-globs.enabled --enable solvers.td3.narrow-globs.stable --set solvers.td3.narrow-globs.narrow-gas 9 --enable ana.int.interval +// 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 // This is supposed to check if the solver terminates #include From d85ad23fa2d94277b015f11ac99dc298d6ba7d48 Mon Sep 17 00:00:00 2001 From: Fabian Stemmler Date: Mon, 2 Dec 2024 12:31:12 +0100 Subject: [PATCH 06/36] rename test directory --- .../{95-dividedsides => 82-dividedsides}/01-modulo-guard.c | 0 .../{95-dividedsides => 82-dividedsides}/02-state-machine.c | 0 .../{95-dividedsides => 82-dividedsides}/03-guarded_inc.c | 0 .../{95-dividedsides => 82-dividedsides}/04-semaphore.c | 0 .../{95-dividedsides => 82-dividedsides}/05-nested_loop.c | 0 .../{95-dividedsides => 82-dividedsides}/06-cyclic-dependency.c | 0 .../{95-dividedsides => 82-dividedsides}/07-ctxt-widen.c | 0 .../{95-dividedsides => 82-dividedsides}/08-ctxt-insensitive.c | 0 .../09-longjmp-counting-local.c | 0 .../10-longjmp-heap-counting-return.c | 0 .../11-longjmp-counting-return.c | 0 .../12-multiple-growing-updates.c | 0 .../{95-dividedsides => 82-dividedsides}/13-threaded-ctxt-widen.c | 0 .../{95-dividedsides => 82-dividedsides}/14-widening-thresholds.c | 0 .../15-intertwined_increment.c | 0 .../16-cyclic-dependency-guarded.c | 0 .../{95-dividedsides => 82-dividedsides}/17-dead-side-effect.c | 0 .../{95-dividedsides => 82-dividedsides}/18-dead-side-effect2.c | 0 .../{95-dividedsides => 82-dividedsides}/19-dead-side-effect3.c | 0 .../{95-dividedsides => 82-dividedsides}/20-dead-side-effect4.c | 0 .../{95-dividedsides => 82-dividedsides}/21-dead-escape.c | 0 .../22-dead-escape-indirect.c | 0 22 files changed, 0 insertions(+), 0 deletions(-) rename tests/regression/{95-dividedsides => 82-dividedsides}/01-modulo-guard.c (100%) rename tests/regression/{95-dividedsides => 82-dividedsides}/02-state-machine.c (100%) rename tests/regression/{95-dividedsides => 82-dividedsides}/03-guarded_inc.c (100%) rename tests/regression/{95-dividedsides => 82-dividedsides}/04-semaphore.c (100%) rename tests/regression/{95-dividedsides => 82-dividedsides}/05-nested_loop.c (100%) rename tests/regression/{95-dividedsides => 82-dividedsides}/06-cyclic-dependency.c (100%) rename tests/regression/{95-dividedsides => 82-dividedsides}/07-ctxt-widen.c (100%) rename tests/regression/{95-dividedsides => 82-dividedsides}/08-ctxt-insensitive.c (100%) rename tests/regression/{95-dividedsides => 82-dividedsides}/09-longjmp-counting-local.c (100%) rename tests/regression/{95-dividedsides => 82-dividedsides}/10-longjmp-heap-counting-return.c (100%) rename tests/regression/{95-dividedsides => 82-dividedsides}/11-longjmp-counting-return.c (100%) rename tests/regression/{95-dividedsides => 82-dividedsides}/12-multiple-growing-updates.c (100%) rename tests/regression/{95-dividedsides => 82-dividedsides}/13-threaded-ctxt-widen.c (100%) rename tests/regression/{95-dividedsides => 82-dividedsides}/14-widening-thresholds.c (100%) rename tests/regression/{95-dividedsides => 82-dividedsides}/15-intertwined_increment.c (100%) rename tests/regression/{95-dividedsides => 82-dividedsides}/16-cyclic-dependency-guarded.c (100%) rename tests/regression/{95-dividedsides => 82-dividedsides}/17-dead-side-effect.c (100%) rename tests/regression/{95-dividedsides => 82-dividedsides}/18-dead-side-effect2.c (100%) rename tests/regression/{95-dividedsides => 82-dividedsides}/19-dead-side-effect3.c (100%) rename tests/regression/{95-dividedsides => 82-dividedsides}/20-dead-side-effect4.c (100%) rename tests/regression/{95-dividedsides => 82-dividedsides}/21-dead-escape.c (100%) rename tests/regression/{95-dividedsides => 82-dividedsides}/22-dead-escape-indirect.c (100%) diff --git a/tests/regression/95-dividedsides/01-modulo-guard.c b/tests/regression/82-dividedsides/01-modulo-guard.c similarity index 100% rename from tests/regression/95-dividedsides/01-modulo-guard.c rename to tests/regression/82-dividedsides/01-modulo-guard.c diff --git a/tests/regression/95-dividedsides/02-state-machine.c b/tests/regression/82-dividedsides/02-state-machine.c similarity index 100% rename from tests/regression/95-dividedsides/02-state-machine.c rename to tests/regression/82-dividedsides/02-state-machine.c diff --git a/tests/regression/95-dividedsides/03-guarded_inc.c b/tests/regression/82-dividedsides/03-guarded_inc.c similarity index 100% rename from tests/regression/95-dividedsides/03-guarded_inc.c rename to tests/regression/82-dividedsides/03-guarded_inc.c diff --git a/tests/regression/95-dividedsides/04-semaphore.c b/tests/regression/82-dividedsides/04-semaphore.c similarity index 100% rename from tests/regression/95-dividedsides/04-semaphore.c rename to tests/regression/82-dividedsides/04-semaphore.c diff --git a/tests/regression/95-dividedsides/05-nested_loop.c b/tests/regression/82-dividedsides/05-nested_loop.c similarity index 100% rename from tests/regression/95-dividedsides/05-nested_loop.c rename to tests/regression/82-dividedsides/05-nested_loop.c diff --git a/tests/regression/95-dividedsides/06-cyclic-dependency.c b/tests/regression/82-dividedsides/06-cyclic-dependency.c similarity index 100% rename from tests/regression/95-dividedsides/06-cyclic-dependency.c rename to tests/regression/82-dividedsides/06-cyclic-dependency.c diff --git a/tests/regression/95-dividedsides/07-ctxt-widen.c b/tests/regression/82-dividedsides/07-ctxt-widen.c similarity index 100% rename from tests/regression/95-dividedsides/07-ctxt-widen.c rename to tests/regression/82-dividedsides/07-ctxt-widen.c diff --git a/tests/regression/95-dividedsides/08-ctxt-insensitive.c b/tests/regression/82-dividedsides/08-ctxt-insensitive.c similarity index 100% rename from tests/regression/95-dividedsides/08-ctxt-insensitive.c rename to tests/regression/82-dividedsides/08-ctxt-insensitive.c diff --git a/tests/regression/95-dividedsides/09-longjmp-counting-local.c b/tests/regression/82-dividedsides/09-longjmp-counting-local.c similarity index 100% rename from tests/regression/95-dividedsides/09-longjmp-counting-local.c rename to tests/regression/82-dividedsides/09-longjmp-counting-local.c diff --git a/tests/regression/95-dividedsides/10-longjmp-heap-counting-return.c b/tests/regression/82-dividedsides/10-longjmp-heap-counting-return.c similarity index 100% rename from tests/regression/95-dividedsides/10-longjmp-heap-counting-return.c rename to tests/regression/82-dividedsides/10-longjmp-heap-counting-return.c diff --git a/tests/regression/95-dividedsides/11-longjmp-counting-return.c b/tests/regression/82-dividedsides/11-longjmp-counting-return.c similarity index 100% rename from tests/regression/95-dividedsides/11-longjmp-counting-return.c rename to tests/regression/82-dividedsides/11-longjmp-counting-return.c diff --git a/tests/regression/95-dividedsides/12-multiple-growing-updates.c b/tests/regression/82-dividedsides/12-multiple-growing-updates.c similarity index 100% rename from tests/regression/95-dividedsides/12-multiple-growing-updates.c rename to tests/regression/82-dividedsides/12-multiple-growing-updates.c diff --git a/tests/regression/95-dividedsides/13-threaded-ctxt-widen.c b/tests/regression/82-dividedsides/13-threaded-ctxt-widen.c similarity index 100% rename from tests/regression/95-dividedsides/13-threaded-ctxt-widen.c rename to tests/regression/82-dividedsides/13-threaded-ctxt-widen.c diff --git a/tests/regression/95-dividedsides/14-widening-thresholds.c b/tests/regression/82-dividedsides/14-widening-thresholds.c similarity index 100% rename from tests/regression/95-dividedsides/14-widening-thresholds.c rename to tests/regression/82-dividedsides/14-widening-thresholds.c diff --git a/tests/regression/95-dividedsides/15-intertwined_increment.c b/tests/regression/82-dividedsides/15-intertwined_increment.c similarity index 100% rename from tests/regression/95-dividedsides/15-intertwined_increment.c rename to tests/regression/82-dividedsides/15-intertwined_increment.c diff --git a/tests/regression/95-dividedsides/16-cyclic-dependency-guarded.c b/tests/regression/82-dividedsides/16-cyclic-dependency-guarded.c similarity index 100% rename from tests/regression/95-dividedsides/16-cyclic-dependency-guarded.c rename to tests/regression/82-dividedsides/16-cyclic-dependency-guarded.c diff --git a/tests/regression/95-dividedsides/17-dead-side-effect.c b/tests/regression/82-dividedsides/17-dead-side-effect.c similarity index 100% rename from tests/regression/95-dividedsides/17-dead-side-effect.c rename to tests/regression/82-dividedsides/17-dead-side-effect.c diff --git a/tests/regression/95-dividedsides/18-dead-side-effect2.c b/tests/regression/82-dividedsides/18-dead-side-effect2.c similarity index 100% rename from tests/regression/95-dividedsides/18-dead-side-effect2.c rename to tests/regression/82-dividedsides/18-dead-side-effect2.c diff --git a/tests/regression/95-dividedsides/19-dead-side-effect3.c b/tests/regression/82-dividedsides/19-dead-side-effect3.c similarity index 100% rename from tests/regression/95-dividedsides/19-dead-side-effect3.c rename to tests/regression/82-dividedsides/19-dead-side-effect3.c diff --git a/tests/regression/95-dividedsides/20-dead-side-effect4.c b/tests/regression/82-dividedsides/20-dead-side-effect4.c similarity index 100% rename from tests/regression/95-dividedsides/20-dead-side-effect4.c rename to tests/regression/82-dividedsides/20-dead-side-effect4.c diff --git a/tests/regression/95-dividedsides/21-dead-escape.c b/tests/regression/82-dividedsides/21-dead-escape.c similarity index 100% rename from tests/regression/95-dividedsides/21-dead-escape.c rename to tests/regression/82-dividedsides/21-dead-escape.c diff --git a/tests/regression/95-dividedsides/22-dead-escape-indirect.c b/tests/regression/82-dividedsides/22-dead-escape-indirect.c similarity index 100% rename from tests/regression/95-dividedsides/22-dead-escape-indirect.c rename to tests/regression/82-dividedsides/22-dead-escape-indirect.c From 30df0e8ee2fb43c4e61e6ddaa5848e7809d3b41e Mon Sep 17 00:00:00 2001 From: Fabian Stemmler Date: Mon, 2 Dec 2024 15:52:58 +0100 Subject: [PATCH 07/36] set meaningful default for narrow gas --- src/config/options.schema.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/config/options.schema.json b/src/config/options.schema.json index fb0a203f0c..762946e6e3 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -2461,7 +2461,7 @@ "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": -1 + "default": 5 }, "eliminate-dead": { "title": "solvers.td3.narrow-globs.eliminate-dead", From 59f4a2f409fea8aa95a1397e19cab477c2ec518e Mon Sep 17 00:00:00 2001 From: Fabian Stemmler Date: Tue, 3 Dec 2024 13:39:25 +0100 Subject: [PATCH 08/36] move some function definitions out of let rec --- src/solver/td3.ml | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/src/solver/td3.ml b/src/solver/td3.ml index 326f2c4df0..6b6deeb440 100644 --- a/src/solver/td3.ml +++ b/src/solver/td3.ml @@ -431,12 +431,6 @@ module Base = ) ) ) - and combined_side y = - let combined = match HM.find_option divided_side_effects y with - | Some map -> HM.fold (fun _ (value, _) acc -> S.Dom.join acc value) map (S.Dom.bot ()) - | None -> S.Dom.bot () in - let orphaned = HM.find_default orphan_side_effects y (S.Dom.bot()) in - S.Dom.join combined orphaned and side_acc acc changed x y d = 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 @@ -451,8 +445,6 @@ module Base = ) ) | _ -> () - and reduce_side_narrow_gas (gas, phase) = - if phase = D_Widen then gas - 1, D_Narrow else (gas, phase) and divided_side (phase:divided_side_mode) ?(do_destabilize=true) ?x y d : bool = if tracing then trace "side" "divided side to %a from %a ## value: %a" S.Var.pretty_trace y (Pretty.docOpt (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 (Pretty.docOpt (S.Var.pretty_trace ())) x S.Dom.pretty d; @@ -493,7 +485,7 @@ module Base = | 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 reduce_side_narrow_gas narrow_gas + Option.map (fun (gas, phase) -> if phase = D_Widen then gas - 1, D_Narrow else (gas, phase)) narrow_gas else narrow_gas in @@ -508,6 +500,13 @@ module Base = HM.remove y_sides x else HM.replace y_sides x (new_side, narrow_gas); + + let combined_side y = + let combined = match HM.find_option divided_side_effects y with + | Some map -> HM.fold (fun _ (value, _) acc -> S.Dom.join acc value) map (S.Dom.bot ()) + | None -> S.Dom.bot () in + let orphaned = HM.find_default orphan_side_effects y (S.Dom.bot()) in + S.Dom.join combined orphaned 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. *) From 58c107f76111d6a74ba813e074d4bc4c79363aec Mon Sep 17 00:00:00 2001 From: Fabian Stemmler Date: Tue, 3 Dec 2024 14:02:10 +0100 Subject: [PATCH 09/36] remove unnecessary orphan side effect handling it is not needed, as long as narrow-globs does work with incremental solving. --- src/solver/td3.ml | 181 ++++++++++++++++++++-------------------------- 1 file changed, 80 insertions(+), 101 deletions(-) diff --git a/src/solver/td3.ml b/src/solver/td3.ml index 6b6deeb440..4d69fc57fd 100644 --- a/src/solver/td3.ml +++ b/src/solver/td3.ml @@ -59,7 +59,7 @@ module Base = sides: VS.t HM.t; prev_sides: VS.t HM.t; divided_side_effects: ((S.Dom.t * (int * divided_side_mode) option) HM.t) HM.t; - orphan_side_effects: S.Dom.t HM.t; + narrow_globs_start_values: S.Dom.t HM.t; rho: S.Dom.t HM.t; wpoint: unit HM.t; stable: unit HM.t; @@ -80,7 +80,7 @@ module Base = sides = HM.create 10; prev_sides = HM.create 10; divided_side_effects = HM.create (if narrow_globs then 10 else 0); - orphan_side_effects = HM.create (if narrow_globs then 10 else 0); + narrow_globs_start_values = HM.create (if narrow_globs then 10 else 0); rho = HM.create 10; wpoint = HM.create 10; stable = HM.create 10; @@ -131,7 +131,7 @@ module Base = sides = HM.copy data.sides; prev_sides = HM.copy data.prev_sides; divided_side_effects = HM.map (fun k v -> HM.copy v) data.divided_side_effects; - orphan_side_effects = HM.copy data.orphan_side_effects; + narrow_globs_start_values = HM.copy data.narrow_globs_start_values; side_infl = HM.copy data.side_infl; side_dep = HM.copy data.side_dep; st = data.st; (* data.st is immutable *) @@ -187,10 +187,10 @@ module Base = 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 orphan_side_effects = HM.create (HM.length data.orphan_side_effects) in + let narrow_globs_start_values = HM.create (HM.length data.narrow_globs_start_values) in HM.iter (fun k v -> - HM.replace orphan_side_effects (S.Var.relift k) (S.Dom.relift v) - ) data.orphan_side_effects; + HM.replace narrow_globs_start_values (S.Var.relift k) (S.Dom.relift v) + ) data.narrow_globs_start_values; 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) @@ -216,7 +216,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; prev_sides; divided_side_effects; orphan_side_effects; rho; wpoint; stable; side_dep; side_infl; var_messages; rho_write; dep} + {st; infl; sides; prev_sides; divided_side_effects; narrow_globs_start_values; rho; wpoint; stable; side_dep; side_infl; var_messages; rho_write; dep} type phase = Widen | Narrow [@@deriving show] (* used in inner solve *) @@ -253,7 +253,7 @@ module Base = let sides = data.sides in let prev_sides = data.prev_sides in let divided_side_effects = data.divided_side_effects in - let orphan_side_effects = data.orphan_side_effects in + let narrow_globs_start_values = data.narrow_globs_start_values in let rho = data.rho in let wpoint = data.wpoint in let stable = data.stable in @@ -361,7 +361,7 @@ module Base = begin match prev_sides_x with | Some prev_sides_x -> VS.iter (fun y -> if Option.is_none @@ HM.find_option acc y then begin - ignore @@ divided_side D_Narrow ~x y (S.Dom.bot ()); + 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 (fun x -> solve x Widen) casualties @@ -376,9 +376,9 @@ module Base = HM.replace 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 + 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 + HM.iter (fun y acc -> ignore @@ divided_side D_Box x y acc) acc ) )) (fun () -> eq x (eval l x) (side_acc acc changed x)) else @@ -439,15 +439,15 @@ module Base = | Some 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 + let y_changed = divided_side D_Widen x y new_acc in if y_changed then HM.replace changed y (); ) ) | _ -> () - and divided_side (phase:divided_side_mode) ?(do_destabilize=true) ?x y d : bool = - if tracing then trace "side" "divided side to %a from %a ## value: %a" S.Var.pretty_trace y (Pretty.docOpt (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 (Pretty.docOpt (S.Var.pretty_trace ())) x S.Dom.pretty d; + 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; 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; ); @@ -456,91 +456,72 @@ module Base = if tracing then trace "sol2" "stable add %a" S.Var.pretty_trace y; HM.replace stable y (); - match x with - | Some x -> ( - let sided = match HM.find_option sides y with - | Some sides -> VS.mem x sides - | None -> false in - if not sided then add_sides y x; - let init_divided_side_effects y = if not (HM.mem divided_side_effects y) then HM.replace divided_side_effects y (HM.create 10) in - init_divided_side_effects y; - - let y_sides = HM.find 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 - (if narrow_globs_conservative_widen && (S.Dom.leq tmp (HM.find rho y)) then - tmp - else - S.Dom.widen old_side tmp), Option.map (fun (x, _) -> (x, D_Widen)) narrow_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" + let sided = match HM.find_option sides y with + | Some sides -> VS.mem x sides + | None -> false in + if not sided then add_sides y x; + let init_divided_side_effects y = if not (HM.mem divided_side_effects y) then HM.replace divided_side_effects y (HM.create 10) in + init_divided_side_effects y; + + let y_sides = HM.find 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 + (if narrow_globs_conservative_widen && (S.Dom.leq tmp (HM.find rho y)) then + tmp + else + S.Dom.widen old_side tmp), Option.map (fun (x, _) -> (x, D_Widen)) narrow_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" + 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 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 combined = match HM.find_option divided_side_effects y with - | Some map -> HM.fold (fun _ (value, _) acc -> S.Dom.join acc value) map (S.Dom.bot ()) - | None -> S.Dom.bot () in - let orphaned = HM.find_default orphan_side_effects y (S.Dom.bot()) in - S.Dom.join combined orphaned 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; - if do_destabilize then - destabilize y; - ); - true - ) else - false - ) else - false - ) - | None -> ( - let orphaned = HM.find_default orphan_side_effects y (S.Dom.bot ()) in - let wd = S.Dom.widen orphaned (S.Dom.join orphaned d) in - HM.replace orphan_side_effects y wd; - if tracing then trace "side" "orphaned side to %a" S.Var.pretty_trace y; + 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 combined = match HM.find_option divided_side_effects y with + | Some map -> HM.fold (fun _ (value, _) acc -> S.Dom.join acc value) map (S.Dom.bot ()) + | None -> S.Dom.bot () in + let start_value = HM.find_default narrow_globs_start_values y (S.Dom.bot()) in + S.Dom.join combined start_value in let y_oldval = HM.find rho y in - if not (S.Dom.leq wd y_oldval) then ( - if tracing then trace "side" "orphaned side changed %a (phase: %s)" S.Var.pretty_trace y (show_divided_side_mode phase); - HM.replace rho y (S.Dom.join wd y_oldval); - if do_destabilize then - destabilize y; - true - ) else - false - ) + 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 and eq x get set = if tracing then trace "sol2" "eq %a" S.Var.pretty_trace x; match Hooks.system x with @@ -677,11 +658,9 @@ 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; - (* TODO: SIDE make this change-proof *) if narrow_globs then - ignore @@ divided_side ~do_destabilize:false D_Widen x d - else - HM.replace rho x d; + HM.replace narrow_globs_start_values x d; + HM.replace rho x d; HM.replace stable x (); (* solve x Widen *) in @@ -1233,7 +1212,7 @@ module Base = print_data_verbose data "Data after postsolve"; verify_data data; - (rho, {st; infl; sides; prev_sides; divided_side_effects; orphan_side_effects; rho; wpoint; stable; side_dep; side_infl; var_messages; rho_write; dep}) + (rho, {st; infl; sides; prev_sides; divided_side_effects; narrow_globs_start_values; rho; wpoint; stable; side_dep; side_infl; var_messages; rho_write; dep}) end (** TD3 with no hooks. *) From 503757018930f1f9a636ecca12b30ae94e3a6361 Mon Sep 17 00:00:00 2001 From: Fabian Stemmler Date: Tue, 3 Dec 2024 15:43:49 +0100 Subject: [PATCH 10/36] mini refactor --- src/analyses/basePriv.ml | 19 +++++++------------ 1 file changed, 7 insertions(+), 12 deletions(-) diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 4a48e41899..dd77ef6456 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -2012,24 +2012,19 @@ 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) | "mutex-oplus" -> (module PerMutexOplusPriv) | "mutex-meet" -> (module PerMutexMeetPriv) | "mutex-meet-tid" -> (module PerMutexMeetTIDPriv (ThreadDigest)) - | "protection" when changes_only -> (module ProtectionBasedPriv (ProtectionChangesOnlySide) (struct let check_read_unprotected = false let handle_atomic = false end)(NoWrapper)) - | "protection" -> (module ProtectionBasedPriv (ProtectionCPASide) (struct let check_read_unprotected = false let handle_atomic = false end)(NoWrapper)) - | "protection-tid" when changes_only -> (module ProtectionBasedPriv (ProtectionChangesOnlySide) (struct let check_read_unprotected = false let handle_atomic = false end)(DigestWrapper(ThreadNotStartedDigest))) - | "protection-tid" -> (module ProtectionBasedPriv (ProtectionCPASide) (struct let check_read_unprotected = false let handle_atomic = false end)(DigestWrapper(ThreadNotStartedDigest))) - | "protection-atomic" when changes_only -> (module ProtectionBasedPriv (ProtectionChangesOnlySide) (struct let check_read_unprotected = false let handle_atomic = true end)(NoWrapper)) (* experimental *) - | "protection-atomic" -> (module ProtectionBasedPriv (ProtectionCPASide) (struct let check_read_unprotected = false let handle_atomic = true end)(NoWrapper)) (* experimental *) - | "protection-read" when changes_only -> (module ProtectionBasedPriv (ProtectionChangesOnlySide) (struct let check_read_unprotected = true let handle_atomic = false end)(NoWrapper)) - | "protection-read" -> (module ProtectionBasedPriv (ProtectionCPASide) (struct let check_read_unprotected = true let handle_atomic = false end)(NoWrapper)) - | "protection-read-tid" when changes_only -> (module ProtectionBasedPriv (ProtectionChangesOnlySide) (struct let check_read_unprotected = true let handle_atomic = false end)(DigestWrapper(ThreadNotStartedDigest))) - | "protection-read-tid" -> (module ProtectionBasedPriv (ProtectionCPASide) (struct let check_read_unprotected = true let handle_atomic = false end)(DigestWrapper(ThreadNotStartedDigest))) - | "protection-read-atomic" when changes_only -> (module ProtectionBasedPriv (ProtectionChangesOnlySide) (struct let check_read_unprotected = true let handle_atomic = true end)(NoWrapper)) (* experimental *) - | "protection-read-atomic" -> (module ProtectionBasedPriv (ProtectionCPASide) (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)) From bac638f42be04eb3374ada323f308de274168278 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 13 Feb 2025 14:00:40 +0100 Subject: [PATCH 11/36] Simplify --- src/constraint/constrSys.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/constraint/constrSys.ml b/src/constraint/constrSys.ml index 49d7797cc5..8e7e29448c 100644 --- a/src/constraint/constrSys.ml +++ b/src/constraint/constrSys.ml @@ -209,8 +209,7 @@ struct let sys_change get = S.sys_change (getL % get % l) (getG % get % g) - let postmortem leaf = - match leaf with + let postmortem = function | `L g -> List.map (fun x -> `L x) @@ S.postmortem g | _ -> [] end From 635ce324e42912d3d1146d90a42ac3a85907b3fb Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 13 Feb 2025 14:01:39 +0100 Subject: [PATCH 12/36] Simplify --- src/framework/constraints.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 9207777c4d..070f7c2a0a 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -550,8 +550,7 @@ struct {obsolete; delete; reluctant; restart} - let postmortem leaf = - match leaf with + let postmortem = function | FunctionEntry fd, c -> [(Function fd, c)] | _ -> [] end From 670a3bf455a01c06101a86090f7787b7b010c2d4 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 13 Feb 2025 14:05:00 +0100 Subject: [PATCH 13/36] Simplify `ana.base.priv.protection.changes-only` check --- src/maingoblint.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 1ee6d053c0..3d5da20910 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -141,7 +141,7 @@ 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" && Option.is_none (List.find_opt (String.equal @@ get_string "ana.base.privatization") ["protection"; "protection-tid"; "protection-atomic"; "protection-read"; "protection-read-tid"; "protection-read-atomic"]) then + 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."; From 1585943dc8aba4e551b46b6673e1e2980a4fd813 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 13 Feb 2025 15:01:40 +0100 Subject: [PATCH 14/36] Simplify --- src/solver/td3.ml | 25 +++++++++++-------------- 1 file changed, 11 insertions(+), 14 deletions(-) diff --git a/src/solver/td3.ml b/src/solver/td3.ml index d506aad0bb..60e9caecd0 100644 --- a/src/solver/td3.ml +++ b/src/solver/td3.ml @@ -383,22 +383,19 @@ module Base = Fun.protect ~finally:(fun () -> ( if narrow_globs_eliminate_dead then begin let prev_sides_x = HM.find_option prev_sides x in - begin match prev_sides_x with - | Some prev_sides_x -> VS.iter (fun y -> - if Option.is_none @@ HM.find_option 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 (fun x -> solve x Widen) casualties - end; - ) prev_sides_x - | None -> () end; - let new_sides = ref VS.empty in - HM.iter (fun y _ -> new_sides := VS.add y !new_sides) acc; - if VS.is_empty !new_sides then + 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 (fun x -> solve x 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 prev_sides x else - HM.replace prev_sides x !new_sides; + HM.replace 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 From efb4f4ce714ec1549c38a70a8d2163c20b65dfb0 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 13 Feb 2025 16:54:46 +0100 Subject: [PATCH 15/36] Indentation --- src/solver/td3.ml | 49 +++++++++++++++++++++++++---------------------- 1 file changed, 26 insertions(+), 23 deletions(-) diff --git a/src/solver/td3.ml b/src/solver/td3.ml index 60e9caecd0..85ad47139f 100644 --- a/src/solver/td3.ml +++ b/src/solver/td3.ml @@ -460,17 +460,16 @@ module Base = and side_acc acc changed x y d = 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 - match new_acc with - | Some new_acc -> ( + | 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; @@ -482,38 +481,40 @@ module Base = if tracing then trace "sol2" "stable add %a" S.Var.pretty_trace y; HM.replace stable y (); - let sided = match HM.find_option sides y with - | Some sides -> VS.mem x sides - | None -> false in + let sided = GobOption.exists (VS.mem x) (HM.find_option sides y) in if not sided then add_sides y x; - let init_divided_side_effects y = if not (HM.mem divided_side_effects y) then HM.replace divided_side_effects y (HM.create 10) in - init_divided_side_effects y; + if not (HM.mem divided_side_effects y) then HM.replace divided_side_effects y (HM.create 10); let y_sides = HM.find 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 + 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 - (if narrow_globs_conservative_widen && (S.Dom.leq tmp (HM.find rho y)) then - tmp - else - S.Dom.widen old_side tmp), Option.map (fun (x, _) -> (x, D_Widen)) narrow_gas - else old_side, narrow_gas) + | 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 + 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 + (result, narrow_gas) | _ -> failwith "unreachable" in @@ -530,13 +531,15 @@ module Base = | Some map -> HM.fold (fun _ (value, _) acc -> S.Dom.join acc value) map (S.Dom.bot ()) | None -> S.Dom.bot () in let start_value = HM.find_default narrow_globs_start_values y (S.Dom.bot()) in - S.Dom.join combined start_value 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 + 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; From c4fbf748d6c55f7b6b2c0ab1381a60e7a9d91e55 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 13 Feb 2025 16:59:59 +0100 Subject: [PATCH 16/36] Hopefully make intent a little clearer --- src/solver/td3.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/solver/td3.ml b/src/solver/td3.ml index 85ad47139f..3f10fd0366 100644 --- a/src/solver/td3.ml +++ b/src/solver/td3.ml @@ -527,9 +527,9 @@ module Base = HM.replace y_sides x (new_side, narrow_gas); let combined_side y = - let combined = match HM.find_option divided_side_effects y with - | Some map -> HM.fold (fun _ (value, _) acc -> S.Dom.join acc value) map (S.Dom.bot ()) - | None -> S.Dom.bot () in + let contribs = HM.find_option 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 narrow_globs_start_values y (S.Dom.bot()) in S.Dom.join combined start_value in From 35b3972fdc777a6d94112811c84f8c4064d9af36 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 24 Feb 2025 11:09:27 +0100 Subject: [PATCH 17/36] Do not move tests --- .../{84-widening_gas => 82-widening_gas}/01-side_parallel.c | 0 .../{84-widening_gas => 82-widening_gas}/02-loop_increment.c | 0 .../03-loop_conditional_side.c | 0 .../{84-widening_gas => 82-widening_gas}/04-side_simple_update.c | 0 .../{84-widening_gas => 82-widening_gas}/05-side_and_no_side.c | 0 .../{84-widening_gas => 82-widening_gas}/06-post_loop1.c | 0 .../{84-widening_gas => 82-widening_gas}/07-post_loop2.c | 0 .../{84-widening_gas => 82-widening_gas}/08-semaphore.c | 0 .../{82-dividedsides => 84-dividedsides}/01-modulo-guard.c | 0 .../{82-dividedsides => 84-dividedsides}/02-state-machine.c | 0 .../{82-dividedsides => 84-dividedsides}/03-guarded_inc.c | 0 .../{82-dividedsides => 84-dividedsides}/04-semaphore.c | 0 .../{82-dividedsides => 84-dividedsides}/05-nested_loop.c | 0 .../{82-dividedsides => 84-dividedsides}/06-cyclic-dependency.c | 0 .../{82-dividedsides => 84-dividedsides}/07-ctxt-widen.c | 0 .../{82-dividedsides => 84-dividedsides}/08-ctxt-insensitive.c | 0 .../09-longjmp-counting-local.c | 0 .../10-longjmp-heap-counting-return.c | 0 .../11-longjmp-counting-return.c | 0 .../12-multiple-growing-updates.c | 0 .../{82-dividedsides => 84-dividedsides}/13-threaded-ctxt-widen.c | 0 .../{82-dividedsides => 84-dividedsides}/14-widening-thresholds.c | 0 .../15-intertwined_increment.c | 0 .../16-cyclic-dependency-guarded.c | 0 .../{82-dividedsides => 84-dividedsides}/17-dead-side-effect.c | 0 .../{82-dividedsides => 84-dividedsides}/18-dead-side-effect2.c | 0 .../{82-dividedsides => 84-dividedsides}/19-dead-side-effect3.c | 0 .../{82-dividedsides => 84-dividedsides}/20-dead-side-effect4.c | 0 .../{82-dividedsides => 84-dividedsides}/21-dead-escape.c | 0 .../22-dead-escape-indirect.c | 0 30 files changed, 0 insertions(+), 0 deletions(-) rename tests/regression/{84-widening_gas => 82-widening_gas}/01-side_parallel.c (100%) rename tests/regression/{84-widening_gas => 82-widening_gas}/02-loop_increment.c (100%) rename tests/regression/{84-widening_gas => 82-widening_gas}/03-loop_conditional_side.c (100%) rename tests/regression/{84-widening_gas => 82-widening_gas}/04-side_simple_update.c (100%) rename tests/regression/{84-widening_gas => 82-widening_gas}/05-side_and_no_side.c (100%) rename tests/regression/{84-widening_gas => 82-widening_gas}/06-post_loop1.c (100%) rename tests/regression/{84-widening_gas => 82-widening_gas}/07-post_loop2.c (100%) rename tests/regression/{84-widening_gas => 82-widening_gas}/08-semaphore.c (100%) rename tests/regression/{82-dividedsides => 84-dividedsides}/01-modulo-guard.c (100%) rename tests/regression/{82-dividedsides => 84-dividedsides}/02-state-machine.c (100%) rename tests/regression/{82-dividedsides => 84-dividedsides}/03-guarded_inc.c (100%) rename tests/regression/{82-dividedsides => 84-dividedsides}/04-semaphore.c (100%) rename tests/regression/{82-dividedsides => 84-dividedsides}/05-nested_loop.c (100%) rename tests/regression/{82-dividedsides => 84-dividedsides}/06-cyclic-dependency.c (100%) rename tests/regression/{82-dividedsides => 84-dividedsides}/07-ctxt-widen.c (100%) rename tests/regression/{82-dividedsides => 84-dividedsides}/08-ctxt-insensitive.c (100%) rename tests/regression/{82-dividedsides => 84-dividedsides}/09-longjmp-counting-local.c (100%) rename tests/regression/{82-dividedsides => 84-dividedsides}/10-longjmp-heap-counting-return.c (100%) rename tests/regression/{82-dividedsides => 84-dividedsides}/11-longjmp-counting-return.c (100%) rename tests/regression/{82-dividedsides => 84-dividedsides}/12-multiple-growing-updates.c (100%) rename tests/regression/{82-dividedsides => 84-dividedsides}/13-threaded-ctxt-widen.c (100%) rename tests/regression/{82-dividedsides => 84-dividedsides}/14-widening-thresholds.c (100%) rename tests/regression/{82-dividedsides => 84-dividedsides}/15-intertwined_increment.c (100%) rename tests/regression/{82-dividedsides => 84-dividedsides}/16-cyclic-dependency-guarded.c (100%) rename tests/regression/{82-dividedsides => 84-dividedsides}/17-dead-side-effect.c (100%) rename tests/regression/{82-dividedsides => 84-dividedsides}/18-dead-side-effect2.c (100%) rename tests/regression/{82-dividedsides => 84-dividedsides}/19-dead-side-effect3.c (100%) rename tests/regression/{82-dividedsides => 84-dividedsides}/20-dead-side-effect4.c (100%) rename tests/regression/{82-dividedsides => 84-dividedsides}/21-dead-escape.c (100%) rename tests/regression/{82-dividedsides => 84-dividedsides}/22-dead-escape-indirect.c (100%) diff --git a/tests/regression/84-widening_gas/01-side_parallel.c b/tests/regression/82-widening_gas/01-side_parallel.c similarity index 100% rename from tests/regression/84-widening_gas/01-side_parallel.c rename to tests/regression/82-widening_gas/01-side_parallel.c diff --git a/tests/regression/84-widening_gas/02-loop_increment.c b/tests/regression/82-widening_gas/02-loop_increment.c similarity index 100% rename from tests/regression/84-widening_gas/02-loop_increment.c rename to tests/regression/82-widening_gas/02-loop_increment.c diff --git a/tests/regression/84-widening_gas/03-loop_conditional_side.c b/tests/regression/82-widening_gas/03-loop_conditional_side.c similarity index 100% rename from tests/regression/84-widening_gas/03-loop_conditional_side.c rename to tests/regression/82-widening_gas/03-loop_conditional_side.c diff --git a/tests/regression/84-widening_gas/04-side_simple_update.c b/tests/regression/82-widening_gas/04-side_simple_update.c similarity index 100% rename from tests/regression/84-widening_gas/04-side_simple_update.c rename to tests/regression/82-widening_gas/04-side_simple_update.c diff --git a/tests/regression/84-widening_gas/05-side_and_no_side.c b/tests/regression/82-widening_gas/05-side_and_no_side.c similarity index 100% rename from tests/regression/84-widening_gas/05-side_and_no_side.c rename to tests/regression/82-widening_gas/05-side_and_no_side.c diff --git a/tests/regression/84-widening_gas/06-post_loop1.c b/tests/regression/82-widening_gas/06-post_loop1.c similarity index 100% rename from tests/regression/84-widening_gas/06-post_loop1.c rename to tests/regression/82-widening_gas/06-post_loop1.c diff --git a/tests/regression/84-widening_gas/07-post_loop2.c b/tests/regression/82-widening_gas/07-post_loop2.c similarity index 100% rename from tests/regression/84-widening_gas/07-post_loop2.c rename to tests/regression/82-widening_gas/07-post_loop2.c diff --git a/tests/regression/84-widening_gas/08-semaphore.c b/tests/regression/82-widening_gas/08-semaphore.c similarity index 100% rename from tests/regression/84-widening_gas/08-semaphore.c rename to tests/regression/82-widening_gas/08-semaphore.c diff --git a/tests/regression/82-dividedsides/01-modulo-guard.c b/tests/regression/84-dividedsides/01-modulo-guard.c similarity index 100% rename from tests/regression/82-dividedsides/01-modulo-guard.c rename to tests/regression/84-dividedsides/01-modulo-guard.c diff --git a/tests/regression/82-dividedsides/02-state-machine.c b/tests/regression/84-dividedsides/02-state-machine.c similarity index 100% rename from tests/regression/82-dividedsides/02-state-machine.c rename to tests/regression/84-dividedsides/02-state-machine.c diff --git a/tests/regression/82-dividedsides/03-guarded_inc.c b/tests/regression/84-dividedsides/03-guarded_inc.c similarity index 100% rename from tests/regression/82-dividedsides/03-guarded_inc.c rename to tests/regression/84-dividedsides/03-guarded_inc.c diff --git a/tests/regression/82-dividedsides/04-semaphore.c b/tests/regression/84-dividedsides/04-semaphore.c similarity index 100% rename from tests/regression/82-dividedsides/04-semaphore.c rename to tests/regression/84-dividedsides/04-semaphore.c diff --git a/tests/regression/82-dividedsides/05-nested_loop.c b/tests/regression/84-dividedsides/05-nested_loop.c similarity index 100% rename from tests/regression/82-dividedsides/05-nested_loop.c rename to tests/regression/84-dividedsides/05-nested_loop.c diff --git a/tests/regression/82-dividedsides/06-cyclic-dependency.c b/tests/regression/84-dividedsides/06-cyclic-dependency.c similarity index 100% rename from tests/regression/82-dividedsides/06-cyclic-dependency.c rename to tests/regression/84-dividedsides/06-cyclic-dependency.c diff --git a/tests/regression/82-dividedsides/07-ctxt-widen.c b/tests/regression/84-dividedsides/07-ctxt-widen.c similarity index 100% rename from tests/regression/82-dividedsides/07-ctxt-widen.c rename to tests/regression/84-dividedsides/07-ctxt-widen.c diff --git a/tests/regression/82-dividedsides/08-ctxt-insensitive.c b/tests/regression/84-dividedsides/08-ctxt-insensitive.c similarity index 100% rename from tests/regression/82-dividedsides/08-ctxt-insensitive.c rename to tests/regression/84-dividedsides/08-ctxt-insensitive.c diff --git a/tests/regression/82-dividedsides/09-longjmp-counting-local.c b/tests/regression/84-dividedsides/09-longjmp-counting-local.c similarity index 100% rename from tests/regression/82-dividedsides/09-longjmp-counting-local.c rename to tests/regression/84-dividedsides/09-longjmp-counting-local.c diff --git a/tests/regression/82-dividedsides/10-longjmp-heap-counting-return.c b/tests/regression/84-dividedsides/10-longjmp-heap-counting-return.c similarity index 100% rename from tests/regression/82-dividedsides/10-longjmp-heap-counting-return.c rename to tests/regression/84-dividedsides/10-longjmp-heap-counting-return.c diff --git a/tests/regression/82-dividedsides/11-longjmp-counting-return.c b/tests/regression/84-dividedsides/11-longjmp-counting-return.c similarity index 100% rename from tests/regression/82-dividedsides/11-longjmp-counting-return.c rename to tests/regression/84-dividedsides/11-longjmp-counting-return.c diff --git a/tests/regression/82-dividedsides/12-multiple-growing-updates.c b/tests/regression/84-dividedsides/12-multiple-growing-updates.c similarity index 100% rename from tests/regression/82-dividedsides/12-multiple-growing-updates.c rename to tests/regression/84-dividedsides/12-multiple-growing-updates.c diff --git a/tests/regression/82-dividedsides/13-threaded-ctxt-widen.c b/tests/regression/84-dividedsides/13-threaded-ctxt-widen.c similarity index 100% rename from tests/regression/82-dividedsides/13-threaded-ctxt-widen.c rename to tests/regression/84-dividedsides/13-threaded-ctxt-widen.c diff --git a/tests/regression/82-dividedsides/14-widening-thresholds.c b/tests/regression/84-dividedsides/14-widening-thresholds.c similarity index 100% rename from tests/regression/82-dividedsides/14-widening-thresholds.c rename to tests/regression/84-dividedsides/14-widening-thresholds.c diff --git a/tests/regression/82-dividedsides/15-intertwined_increment.c b/tests/regression/84-dividedsides/15-intertwined_increment.c similarity index 100% rename from tests/regression/82-dividedsides/15-intertwined_increment.c rename to tests/regression/84-dividedsides/15-intertwined_increment.c diff --git a/tests/regression/82-dividedsides/16-cyclic-dependency-guarded.c b/tests/regression/84-dividedsides/16-cyclic-dependency-guarded.c similarity index 100% rename from tests/regression/82-dividedsides/16-cyclic-dependency-guarded.c rename to tests/regression/84-dividedsides/16-cyclic-dependency-guarded.c diff --git a/tests/regression/82-dividedsides/17-dead-side-effect.c b/tests/regression/84-dividedsides/17-dead-side-effect.c similarity index 100% rename from tests/regression/82-dividedsides/17-dead-side-effect.c rename to tests/regression/84-dividedsides/17-dead-side-effect.c diff --git a/tests/regression/82-dividedsides/18-dead-side-effect2.c b/tests/regression/84-dividedsides/18-dead-side-effect2.c similarity index 100% rename from tests/regression/82-dividedsides/18-dead-side-effect2.c rename to tests/regression/84-dividedsides/18-dead-side-effect2.c diff --git a/tests/regression/82-dividedsides/19-dead-side-effect3.c b/tests/regression/84-dividedsides/19-dead-side-effect3.c similarity index 100% rename from tests/regression/82-dividedsides/19-dead-side-effect3.c rename to tests/regression/84-dividedsides/19-dead-side-effect3.c diff --git a/tests/regression/82-dividedsides/20-dead-side-effect4.c b/tests/regression/84-dividedsides/20-dead-side-effect4.c similarity index 100% rename from tests/regression/82-dividedsides/20-dead-side-effect4.c rename to tests/regression/84-dividedsides/20-dead-side-effect4.c diff --git a/tests/regression/82-dividedsides/21-dead-escape.c b/tests/regression/84-dividedsides/21-dead-escape.c similarity index 100% rename from tests/regression/82-dividedsides/21-dead-escape.c rename to tests/regression/84-dividedsides/21-dead-escape.c diff --git a/tests/regression/82-dividedsides/22-dead-escape-indirect.c b/tests/regression/84-dividedsides/22-dead-escape-indirect.c similarity index 100% rename from tests/regression/82-dividedsides/22-dead-escape-indirect.c rename to tests/regression/84-dividedsides/22-dead-escape-indirect.c From f70615c1fa58d1d9a242dedbf53212f46b6bf00f Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 21 Mar 2025 13:00:06 +0100 Subject: [PATCH 18/36] ... --- src/solver/td3.ml | 24 +++- src/solver/td3UpdateRule.ml | 213 ++++++++++++++++++++++++++++++++++++ 2 files changed, 233 insertions(+), 4 deletions(-) create mode 100644 src/solver/td3UpdateRule.ml diff --git a/src/solver/td3.ml b/src/solver/td3.ml index 3f10fd0366..bead49281a 100644 --- a/src/solver/td3.ml +++ b/src/solver/td3.ml @@ -49,6 +49,9 @@ module Base = open SolverBox.Warrow (S.Dom) include Generic.SolverStats (S) (HM) module VS = Set.Make (S.Var) + + module UpdateRule = Td3UpdateRule.Ours(S) (HM) (VS) + let exists_key f hm = HM.exists (fun k _ -> f k) hm type divided_side_mode = D_Widen | D_Narrow | D_Box [@@deriving show] @@ -57,6 +60,7 @@ module Base = 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; 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; @@ -78,6 +82,7 @@ module Base = st = []; infl = HM.create 10; sides = HM.create 10; + update_rule_data = UpdateRule.create_empty_data (); 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); @@ -129,6 +134,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; 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; @@ -177,6 +183,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 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) @@ -216,7 +223,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; prev_sides; divided_side_effects; narrow_globs_start_values; rho; wpoint_gas; stable; side_dep; side_infl; var_messages; rho_write; dep} + {st; infl; sides; update_rule_data; prev_sides; divided_side_effects; narrow_globs_start_values; rho; wpoint_gas; stable; side_dep; side_infl; var_messages; rho_write; dep} type phase = Widen | Narrow [@@deriving show] (* used in inner solve *) @@ -252,9 +259,12 @@ module Base = let infl = data.infl in let sides = data.sides in + let update_rule_data = data.update_rule_data in let prev_sides = data.prev_sides in let divided_side_effects = data.divided_side_effects in let narrow_globs_start_values = data.narrow_globs_start_values in + + let rho = data.rho in let wpoint_gas = data.wpoint_gas in let stable = data.stable in @@ -377,7 +387,7 @@ module Base = | _ -> (* The RHS is re-evaluated, all deps are re-trigerred *) HM.replace dep x VS.empty; - if narrow_globs then + let alpha x eq eval solve = let acc = HM.create 0 in let changed = HM.create 0 in Fun.protect ~finally:(fun () -> ( @@ -403,6 +413,12 @@ module Base = HM.iter (fun y acc -> ignore @@ divided_side D_Box x y acc) acc ) )) (fun () -> eq x (eval l x) (side_acc acc changed x)) + in + if narrow_globs then + let eq_delayed = fun () -> eq x (eval l x) in + let solve_widen x = solve x Widen in + UpdateRule.narrow_globals x eq_delayed solve_widen rho init stable data.update_rule_data sides add_sides rho destabilize (Hooks.system) + (* alpha x eq eval solve *) else eq x (eval l x) (side ~x) in @@ -661,7 +677,7 @@ module Base = if tracing then trace "sol2" "set_start %a ## %a" S.Var.pretty_trace x S.Dom.pretty d; init x; if narrow_globs then - HM.replace narrow_globs_start_values x d; + UpdateRule.register_start update_rule_data x d; HM.replace rho x d; HM.replace stable x (); (* solve x Widen *) @@ -1214,7 +1230,7 @@ module Base = print_data_verbose data "Data after postsolve"; verify_data data; - (rho, {st; infl; sides; prev_sides; divided_side_effects; narrow_globs_start_values; rho; wpoint_gas; stable; side_dep; side_infl; var_messages; rho_write; dep}) + (rho, {st; infl; sides; update_rule_data; prev_sides; divided_side_effects; narrow_globs_start_values; rho; wpoint_gas; stable; side_dep; side_infl; var_messages; rho_write; dep}) end (** TD3 with no hooks. *) diff --git a/src/solver/td3UpdateRule.ml b/src/solver/td3UpdateRule.ml new file mode 100644 index 0000000000..c511714da2 --- /dev/null +++ b/src/solver/td3UpdateRule.ml @@ -0,0 +1,213 @@ +(** 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 + val active: bool + val create_empty_data : unit -> data + val copy_marshal: data -> data + val relift_marshal: data -> data +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 + let active = false + let create_empty_data () = () + let copy_marshal _ = () + let relift_marshal _ = () + + let register_start x d = () + end + +module Ours = +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; + } + let active = false + 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 narrow_globs = GobConfig.get_bool "solvers.td3.narrow-globs.enabled" + 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" + + type phase = Widen | Narrow [@@deriving show] (* used in inner solve *) + + let rec side_acc init stable data sides add_sides rho destabilize system 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 init stable data sides add_sides rho destabilize system in + if y_changed then + HM.replace changed y (); + ) + ) new_acc; + and divided_side (phase:divided_side_mode) x y d init stable data sides add_sides rho destabilize system: 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; + if 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 (system y = None); + 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" + 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 + + let narrow_globals x eq_delayed widen_solve rho init stable data sides add_sides rho destabilize system = + 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 ()) init stable data sides add_sides rho destabilize system; + if S.Dom.is_bot @@ HM.find rho y then + let casualties = S.postmortem y in + List.iter widen_solve 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 init stable data sides add_sides rho destabilize system) acc + else ( + HM.iter (fun y acc -> ignore @@ divided_side D_Box x y acc init stable data sides add_sides rho destabilize system) acc + ) + )) (fun () -> (eq_delayed ()) (side_acc init stable data sides add_sides rho destabilize system acc changed x)) + + + let register_start data x d = HM.replace data.narrow_globs_start_values x d +end From 25bb6f8fdd341140a85f4406a10a38d7fe4d072b Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 21 Mar 2025 13:29:41 +0100 Subject: [PATCH 19/36] ... --- src/solver/td3.ml | 170 ++------------------------------ src/solver/td3UpdateRule.ml | 187 ++++++++++++++++++------------------ 2 files changed, 100 insertions(+), 257 deletions(-) diff --git a/src/solver/td3.ml b/src/solver/td3.ml index bead49281a..2288d9f3c3 100644 --- a/src/solver/td3.ml +++ b/src/solver/td3.ml @@ -54,16 +54,11 @@ module Base = let exists_key f hm = HM.exists (fun k _ -> f k) hm - type divided_side_mode = D_Widen | D_Narrow | D_Box [@@deriving show] - 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; - 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; 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; @@ -76,16 +71,11 @@ module Base = type marshal = solver_data - let create_empty_data () = - let narrow_globs = GobConfig.get_bool "solvers.td3.narrow-globs.enabled" in - { + let create_empty_data () = { st = []; infl = HM.create 10; sides = HM.create 10; update_rule_data = UpdateRule.create_empty_data (); - 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); rho = HM.create 10; wpoint_gas = HM.create 10; stable = HM.create 10; @@ -135,9 +125,6 @@ module Base = infl = HM.copy data.infl; sides = HM.copy data.sides; update_rule_data = UpdateRule.copy_marshal data.update_rule_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; side_infl = HM.copy data.side_infl; side_dep = HM.copy data.side_dep; st = data.st; (* data.st is immutable *) @@ -184,20 +171,6 @@ module Base = 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 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; 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) @@ -223,7 +196,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; update_rule_data; prev_sides; divided_side_effects; narrow_globs_start_values; 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 *) @@ -260,10 +233,6 @@ module Base = let infl = data.infl in let sides = data.sides in let update_rule_data = data.update_rule_data in - let prev_sides = data.prev_sides in - let divided_side_effects = data.divided_side_effects in - let narrow_globs_start_values = data.narrow_globs_start_values in - let rho = data.rho in let wpoint_gas = data.wpoint_gas in @@ -288,11 +257,6 @@ module Base = let superstable = HM.copy stable in let narrow_globs = GobConfig.get_bool "solvers.td3.narrow-globs.enabled" in - let narrow_globs_conservative_widen = GobConfig.get_bool "solvers.td3.narrow-globs.conservative-widen" in - let narrow_globs_immediate_growth = GobConfig.get_bool "solvers.td3.narrow-globs.immediate-growth" in - let narrow_globs_gas_default = GobConfig.get_int "solvers.td3.narrow-globs.narrow-gas" in - let narrow_globs_gas_default = if narrow_globs_gas_default < 0 then None else Some (narrow_globs_gas_default, D_Widen) in - let narrow_globs_eliminate_dead = GobConfig.get_bool "solvers.td3.narrow-globs.eliminate-dead" in let reluctant = GobConfig.get_bool "incremental.reluctant.enabled" in @@ -387,40 +351,12 @@ module Base = | _ -> (* The RHS is re-evaluated, all deps are re-trigerred *) HM.replace dep x VS.empty; - let alpha x eq eval solve = - 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 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 (fun x -> solve x 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 prev_sides x - else - HM.replace 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 () -> eq x (eval l x) (side_acc acc changed x)) - in + let eqx = eq x (eval l x) in if narrow_globs then - let eq_delayed = fun () -> eq x (eval l x) in let solve_widen x = solve x Widen in - UpdateRule.narrow_globals x eq_delayed solve_widen rho init stable data.update_rule_data sides add_sides rho destabilize (Hooks.system) - (* alpha x eq eval solve *) + UpdateRule.eq_wrap x eqx solve_widen rho init stable data.update_rule_data sides add_sides rho destabilize (Hooks.system) else - eq x (eval l x) (side ~x) + eqx (side ~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 *) @@ -473,100 +409,6 @@ module Base = ) ) ) - and side_acc acc changed x y d = - 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; - 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); - 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 divided_side_effects y) then HM.replace divided_side_effects y (HM.create 10); - - let y_sides = HM.find 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" - 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 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 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 and eq x get set = if tracing then trace "sol2" "eq %a" S.Var.pretty_trace x; match Hooks.system x with @@ -1230,7 +1072,7 @@ module Base = print_data_verbose data "Data after postsolve"; verify_data data; - (rho, {st; infl; sides; update_rule_data; prev_sides; divided_side_effects; narrow_globs_start_values; 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. *) diff --git a/src/solver/td3UpdateRule.ml b/src/solver/td3UpdateRule.ml index c511714da2..05859f9f0c 100644 --- a/src/solver/td3UpdateRule.ml +++ b/src/solver/td3UpdateRule.ml @@ -86,102 +86,103 @@ functor (S:EqConstrSys) -> type phase = Widen | Narrow [@@deriving show] (* used in inner solve *) - let rec side_acc init stable data sides add_sides rho destabilize system 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 init stable data sides add_sides rho destabilize system in - if y_changed then - HM.replace changed y (); - ) - ) new_acc; - and divided_side (phase:divided_side_mode) x y d init stable data sides add_sides rho destabilize system: 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; - if 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 (system y = None); - 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 + + let eq_wrap x eqx widen_solve rho init stable data sides add_sides rho destabilize system = + let rec side_acc init stable data sides add_sides rho system 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 init stable data sides add_sides rho system in + if y_changed then + HM.replace changed y (); + ) + ) new_acc; + and divided_side (phase:divided_side_mode) x y d init stable data sides add_sides rho system: 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; + if 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 (system y = None); + 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 - S.Dom.widen old_side tmp + narrow_gas 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" - in + (result, narrow_gas) + | _ -> failwith "unreachable" + 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 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 + if S.Dom.is_bot new_side && narrow_gas = None then + HM.remove y_sides x 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 + 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 - ) else - false - - let narrow_globals x eq_delayed widen_solve rho init stable data sides add_sides rho destabilize system = + in let acc = HM.create 0 in let changed = HM.create 0 in Fun.protect ~finally:(fun () -> ( @@ -189,7 +190,7 @@ functor (S:EqConstrSys) -> 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 ()) init stable data sides add_sides rho destabilize system; + ignore @@ divided_side D_Narrow x y (S.Dom.bot ()) init stable data sides add_sides rho system; if S.Dom.is_bot @@ HM.find rho y then let casualties = S.postmortem y in List.iter widen_solve casualties @@ -202,11 +203,11 @@ functor (S:EqConstrSys) -> 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 init stable data sides add_sides rho destabilize system) acc + HM.iter (fun y acc -> if not @@ HM.mem changed y then ignore @@ divided_side D_Narrow x y acc init stable data sides add_sides rho system) acc else ( - HM.iter (fun y acc -> ignore @@ divided_side D_Box x y acc init stable data sides add_sides rho destabilize system) acc + HM.iter (fun y acc -> ignore @@ divided_side D_Box x y acc init stable data sides add_sides rho system) acc ) - )) (fun () -> (eq_delayed ()) (side_acc init stable data sides add_sides rho destabilize system acc changed x)) + )) (fun () -> eqx (side_acc init stable data sides add_sides rho system acc changed x)) let register_start data x d = HM.replace data.narrow_globs_start_values x d From 4de2b53830d1ba1088d6e4088fdf872bd42e5ad5 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 21 Mar 2025 13:36:52 +0100 Subject: [PATCH 20/36] ... --- src/solver/td3.ml | 2 +- src/solver/td3UpdateRule.ml | 17 ++++++++--------- 2 files changed, 9 insertions(+), 10 deletions(-) diff --git a/src/solver/td3.ml b/src/solver/td3.ml index 2288d9f3c3..54ceffc1b3 100644 --- a/src/solver/td3.ml +++ b/src/solver/td3.ml @@ -354,7 +354,7 @@ module Base = let eqx = eq x (eval l x) in if narrow_globs then let solve_widen x = solve x Widen in - UpdateRule.eq_wrap x eqx solve_widen rho init stable data.update_rule_data sides add_sides rho destabilize (Hooks.system) + UpdateRule.eq_wrap x eqx solve_widen init stable data.update_rule_data sides add_sides rho destabilize (Hooks.system) else eqx (side ~x) in diff --git a/src/solver/td3UpdateRule.ml b/src/solver/td3UpdateRule.ml index 05859f9f0c..4ac8477c97 100644 --- a/src/solver/td3UpdateRule.ml +++ b/src/solver/td3UpdateRule.ml @@ -86,9 +86,8 @@ functor (S:EqConstrSys) -> type phase = Widen | Narrow [@@deriving show] (* used in inner solve *) - - let eq_wrap x eqx widen_solve rho init stable data sides add_sides rho destabilize system = - let rec side_acc init stable data sides add_sides rho system acc changed x y d:unit = + let eq_wrap x eqx widen_solve init stable data sides add_sides rho destabilize system = + 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 @@ -96,12 +95,12 @@ functor (S:EqConstrSys) -> 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 init stable data sides add_sides rho system in + 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 init stable data sides add_sides rho system: bool = + 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; if system y <> None then ( @@ -190,7 +189,7 @@ functor (S:EqConstrSys) -> 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 ()) init stable data sides add_sides rho system; + 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 widen_solve casualties @@ -203,11 +202,11 @@ functor (S:EqConstrSys) -> 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 init stable data sides add_sides rho system) acc + 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 init stable data sides add_sides rho system) acc + HM.iter (fun y acc -> ignore @@ divided_side D_Box x y acc) acc ) - )) (fun () -> eqx (side_acc init stable data sides add_sides rho system acc changed x)) + )) (fun () -> eqx (side_acc acc changed x)) let register_start data x d = HM.replace data.narrow_globs_start_values x d From e324519e425b8bc7dfe2a9f5112af9874ad27aa0 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 21 Mar 2025 14:55:23 +0100 Subject: [PATCH 21/36] Progress --- src/solver/td3.ml | 39 +++++++++++++++++------------------ src/solver/td3UpdateRule.ml | 41 ++++++++++++++++++++++++++----------- 2 files changed, 48 insertions(+), 32 deletions(-) diff --git a/src/solver/td3.ml b/src/solver/td3.ml index 54ceffc1b3..4f27a00e7d 100644 --- a/src/solver/td3.ml +++ b/src/solver/td3.ml @@ -45,15 +45,21 @@ 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 = Td3UpdateRule.Ours(S) (HM) (VS) + 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; @@ -352,11 +358,7 @@ module Base = (* The RHS is re-evaluated, all deps are re-trigerred *) HM.replace dep x VS.empty; let eqx = eq x (eval l x) in - if narrow_globs then - let solve_widen x = solve x Widen in - UpdateRule.eq_wrap x eqx solve_widen init stable data.update_rule_data sides add_sides rho destabilize (Hooks.system) - else - eqx (side ~x) + UpdateRule.eq_wrap x eqx (fun x-> solve x Widen) init stable data.update_rule_data sides add_sides rho destabilize side assert_can_receive_side 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 *) @@ -458,10 +460,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; @@ -518,8 +517,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; - if narrow_globs then - UpdateRule.register_start update_rule_data x d; + UpdateRule.register_start update_rule_data x d; HM.replace rho x d; HM.replace stable x (); (* solve x Widen *) @@ -1076,10 +1074,10 @@ module Base = 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) @@ -1105,11 +1103,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) -> @@ -1184,7 +1182,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; @@ -1223,17 +1221,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 index 4ac8477c97..586fd64095 100644 --- a/src/solver/td3UpdateRule.ml +++ b/src/solver/td3UpdateRule.ml @@ -10,11 +10,24 @@ module type S = functor (S:EqConstrSys) -> functor (HM:Hashtbl.S with type key = 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 eq_wrap: + S.v -> + ((S.v -> S.d -> unit) -> S.d) -> + (S.v -> unit) -> + (S.v -> 'b) -> + unit HM.t -> + data -> + VS.t HM.t -> + (S.v -> S.v -> unit) -> + S.d HM.t -> (S.v -> unit) -> (?x:S.v -> S.v -> S.d -> unit) -> (S.v -> unit) -> S.d end (** Inactive *) -module Inactive: S = +module Inactive:S = functor (S:EqConstrSys) -> functor (HM:Hashtbl.S with type key = S.v) -> functor (VS:Set.S with type elt = S.v) -> @@ -25,10 +38,13 @@ module Inactive: S = let copy_marshal _ = () let relift_marshal _ = () - let register_start x d = () + let register_start _ _ _ = () + + let eq_wrap x eqx _ _ _ _ _ _ _ _ (side:?x:S.v -> S.v -> S.d -> unit) _ = + eqx (side ~x) end -module Ours = +module Ours:S = functor (S:EqConstrSys) -> functor (HM:Hashtbl.S with type key = S.v) -> functor (VS:Set.S with type elt = S.v) -> @@ -77,7 +93,8 @@ functor (S:EqConstrSys) -> narrow_globs_start_values; } - let narrow_globs = GobConfig.get_bool "solvers.td3.narrow-globs.enabled" + 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" @@ -86,7 +103,7 @@ functor (S:EqConstrSys) -> type phase = Widen | Narrow [@@deriving show] (* used in inner solve *) - let eq_wrap x eqx widen_solve init stable data sides add_sides rho destabilize system = + let eq_wrap x eqx widen_solve init stable data sides add_sides rho destabilize side assert_can_receive_side = 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 @@ -103,10 +120,7 @@ functor (S:EqConstrSys) -> 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; - if 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 (system y = None); + assert_can_receive_side y; init y; if tracing then trace "sol2" "stable add %a" S.Var.pretty_trace y; HM.replace stable y (); @@ -207,7 +221,10 @@ functor (S:EqConstrSys) -> HM.iter (fun y acc -> ignore @@ divided_side D_Box x y acc) acc ) )) (fun () -> eqx (side_acc acc changed x)) - - - let register_start data x d = HM.replace data.narrow_globs_start_values x d end + +let choose () = + if GobConfig.get_bool "solvers.td3.narrow-globs.enabled" then + (module Ours : S) + else + (module Inactive : S) From 8a39202623c7916e14b4fe381047b58d5f80309e Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 21 Mar 2025 14:56:39 +0100 Subject: [PATCH 22/36] Document TD3 update rule --- src/solver/goblint_solver.ml | 1 + 1 file changed, 1 insertion(+) 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 From b714bcdff0249dd6e81ceafa08971074ab6bccf2 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 21 Mar 2025 14:57:34 +0100 Subject: [PATCH 23/36] Rename to narrow --- src/solver/td3UpdateRule.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/solver/td3UpdateRule.ml b/src/solver/td3UpdateRule.ml index 586fd64095..75b23a1139 100644 --- a/src/solver/td3UpdateRule.ml +++ b/src/solver/td3UpdateRule.ml @@ -44,7 +44,7 @@ module Inactive:S = eqx (side ~x) end -module Ours:S = +module Narrow:S = functor (S:EqConstrSys) -> functor (HM:Hashtbl.S with type key = S.v) -> functor (VS:Set.S with type elt = S.v) -> @@ -225,6 +225,6 @@ end let choose () = if GobConfig.get_bool "solvers.td3.narrow-globs.enabled" then - (module Ours : S) + (module Narrow : S) else (module Inactive : S) From f42b689e09c456f60b6117e9326317e02cbc753a Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 21 Mar 2025 15:15:03 +0100 Subject: [PATCH 24/36] Document incompatibility --- src/maingoblint.ml | 1 + src/solver/td3.ml | 11 ++++------- 2 files changed, 5 insertions(+), 7 deletions(-) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 3d5da20910..471a011147 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -165,6 +165,7 @@ let check_arguments () = ^ String.concat " and " @@ List.map (fun s -> "'" ^ s ^ "'") imprecise_options) ); 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_bool "solvers.td3.narrow-globs.enabled" then fail "solvers.td3.space is incompatible with solvers.td3.narrow-globs.enabled"; 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 ( diff --git a/src/solver/td3.ml b/src/solver/td3.ml index 4f27a00e7d..93b0a696d1 100644 --- a/src/solver/td3.ml +++ b/src/solver/td3.ml @@ -262,8 +262,6 @@ module Base = These don't have to be re-verified and warnings can be reused. *) let superstable = HM.copy stable in - let narrow_globs = GobConfig.get_bool "solvers.td3.narrow-globs.enabled" in - let reluctant = GobConfig.get_bool "incremental.reluctant.enabled" in let var_messages = data.var_messages in @@ -427,11 +425,10 @@ module Base = else ( HM.replace called y (); let eqd = - if narrow_globs then - failwith "narrow-globs not yet implemented for simple solve" - else - eq y (eval l x) (side ~x) - in + (* 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) From 82d81df078f810670d43827add89c3f844a4de81 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 21 Mar 2025 15:16:21 +0100 Subject: [PATCH 25/36] Was already documented --- src/maingoblint.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 471a011147..73f2273fc1 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -164,7 +164,6 @@ let check_arguments () = "trans.activated: to increase the precision of 'remove_dead_code' transform, disable " ^ String.concat " and " @@ List.map (fun s -> "'" ^ s ^ "'") imprecise_options) ); - 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_bool "solvers.td3.narrow-globs.enabled" then fail "solvers.td3.space is incompatible with solvers.td3.narrow-globs.enabled"; 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"; From ff07b9b9e7981c50f4b3432c22d05e20f05c07e9 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 21 Mar 2025 15:26:20 +0100 Subject: [PATCH 26/36] Types --- src/solver/td3UpdateRule.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/solver/td3UpdateRule.ml b/src/solver/td3UpdateRule.ml index 75b23a1139..9d7f01907c 100644 --- a/src/solver/td3UpdateRule.ml +++ b/src/solver/td3UpdateRule.ml @@ -17,7 +17,7 @@ module type S = functor (S:EqConstrSys) -> functor (HM:Hashtbl.S with type key = S.v -> ((S.v -> S.d -> unit) -> S.d) -> (S.v -> unit) -> - (S.v -> 'b) -> + (S.v -> unit) -> unit HM.t -> data -> VS.t HM.t -> @@ -101,7 +101,6 @@ functor (S:EqConstrSys) -> 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" - type phase = Widen | Narrow [@@deriving show] (* used in inner solve *) let eq_wrap x eqx widen_solve init stable data sides add_sides rho destabilize side assert_can_receive_side = let rec side_acc acc changed x y d:unit = From 2770225035e9abc368823b8042a83fb4986506ce Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 21 Mar 2025 15:33:32 +0100 Subject: [PATCH 27/36] Indent --- src/solver/td3UpdateRule.ml | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/src/solver/td3UpdateRule.ml b/src/solver/td3UpdateRule.ml index 9d7f01907c..ddee260ae8 100644 --- a/src/solver/td3UpdateRule.ml +++ b/src/solver/td3UpdateRule.ml @@ -14,15 +14,15 @@ module type S = functor (S:EqConstrSys) -> functor (HM:Hashtbl.S with type key = val register_start: data -> S.v -> S.d -> unit val eq_wrap: - S.v -> - ((S.v -> S.d -> unit) -> S.d) -> - (S.v -> unit) -> - (S.v -> unit) -> - unit HM.t -> - data -> - VS.t HM.t -> - (S.v -> S.v -> unit) -> - S.d HM.t -> (S.v -> unit) -> (?x:S.v -> S.v -> S.d -> unit) -> (S.v -> unit) -> S.d + S.v -> + ((S.v -> S.d -> unit) -> S.d) -> + (S.v -> unit) -> + (S.v -> unit) -> + unit HM.t -> + data -> + VS.t HM.t -> + (S.v -> S.v -> unit) -> + S.d HM.t -> (S.v -> unit) -> (?x:S.v -> S.v -> S.d -> unit) -> (S.v -> unit) -> S.d end (** Inactive *) @@ -45,7 +45,7 @@ module Inactive:S = end module Narrow:S = -functor (S:EqConstrSys) -> + functor (S:EqConstrSys) -> functor (HM:Hashtbl.S with type key = S.v) -> functor (VS:Set.S with type elt = S.v) -> struct @@ -114,7 +114,7 @@ functor (S:EqConstrSys) -> 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; @@ -158,7 +158,7 @@ functor (S:EqConstrSys) -> narrow_gas in (result, narrow_gas) - | _ -> failwith "unreachable" + | _ -> failwith "unreachable" (* handled above *) in if not (S.Dom.equal old_side new_side) then ( @@ -219,8 +219,8 @@ functor (S:EqConstrSys) -> else ( HM.iter (fun y acc -> ignore @@ divided_side D_Box x y acc) acc ) - )) (fun () -> eqx (side_acc acc changed x)) -end + )) (fun () -> eqx (side_acc acc changed x)) + end let choose () = if GobConfig.get_bool "solvers.td3.narrow-globs.enabled" then From f5aae176647a62617d5d5bbfc7f37f72da9527b2 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 21 Mar 2025 16:47:57 +0100 Subject: [PATCH 28/36] Wrapper --- src/solver/td3.ml | 4 +- src/solver/td3UpdateRule.ml | 259 +++++++++++++++++++----------------- 2 files changed, 138 insertions(+), 125 deletions(-) diff --git a/src/solver/td3.ml b/src/solver/td3.ml index 93b0a696d1..d7db26e245 100644 --- a/src/solver/td3.ml +++ b/src/solver/td3.ml @@ -330,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_wrap) 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; @@ -355,8 +356,7 @@ module Base = | _ -> (* The RHS is re-evaluated, all deps are re-trigerred *) HM.replace dep x VS.empty; - let eqx = eq x (eval l x) in - UpdateRule.eq_wrap x eqx (fun x-> solve x Widen) init stable data.update_rule_data sides add_sides rho destabilize side assert_can_receive_side + 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 *) diff --git a/src/solver/td3UpdateRule.ml b/src/solver/td3UpdateRule.ml index ddee260ae8..5977dd2773 100644 --- a/src/solver/td3UpdateRule.ml +++ b/src/solver/td3UpdateRule.ml @@ -4,8 +4,11 @@ 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 active: bool val create_empty_data : unit -> data val copy_marshal: data -> data @@ -13,16 +16,19 @@ module type S = functor (S:EqConstrSys) -> functor (HM:Hashtbl.S with type key = val register_start: data -> S.v -> S.d -> unit - val eq_wrap: - S.v -> - ((S.v -> S.d -> unit) -> S.d) -> - (S.v -> unit) -> - (S.v -> unit) -> - unit HM.t -> - data -> - VS.t HM.t -> - (S.v -> S.v -> unit) -> - S.d HM.t -> (S.v -> unit) -> (?x:S.v -> S.v -> S.d -> unit) -> (S.v -> unit) -> S.d + 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 *) @@ -33,6 +39,7 @@ module Inactive:S = 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 active = false let create_empty_data () = () let copy_marshal _ = () @@ -40,8 +47,8 @@ module Inactive:S = let register_start _ _ _ = () - let eq_wrap x eqx _ _ _ _ _ _ _ _ (side:?x:S.v -> S.v -> S.d -> unit) _ = - eqx (side ~x) + 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 = @@ -56,6 +63,9 @@ module Narrow:S = 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 active = false let create_empty_data () = let narrow_globs = GobConfig.get_bool "solvers.td3.narrow-globs.enabled" in @@ -101,125 +111,128 @@ module Narrow:S = 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 eq_wrap x eqx widen_solve init stable data sides add_sides rho destabilize side assert_can_receive_side = - 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 + 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 - S.Dom.widen old_side tmp + narrow_gas 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 + (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 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 + if S.Dom.is_bot new_side && narrow_gas = None then + HM.remove y_sides x 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 + 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 - ) 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 - 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 widen_solve 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)) + (eq_wrapper: eq_wrapper) + end let choose () = From 4c7595f3e9ad36cce8127bb63d069bab472fa430 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 21 Mar 2025 16:55:25 +0100 Subject: [PATCH 29/36] Fix --- src/solver/td3.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solver/td3.ml b/src/solver/td3.ml index d7db26e245..e9d7156b15 100644 --- a/src/solver/td3.ml +++ b/src/solver/td3.ml @@ -330,7 +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_wrap) x eqx + 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; From 0e2522abc60c36a091a799264705b0e1f9b009e4 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 17 Apr 2025 14:00:19 +0200 Subject: [PATCH 30/36] Rename test folder --- .../{84-dividedsides => 85-narrow_globs}/01-modulo-guard.c | 0 .../{84-dividedsides => 85-narrow_globs}/02-state-machine.c | 0 .../{84-dividedsides => 85-narrow_globs}/03-guarded_inc.c | 0 .../{84-dividedsides => 85-narrow_globs}/04-semaphore.c | 0 .../{84-dividedsides => 85-narrow_globs}/05-nested_loop.c | 0 .../{84-dividedsides => 85-narrow_globs}/06-cyclic-dependency.c | 0 .../{84-dividedsides => 85-narrow_globs}/07-ctxt-widen.c | 0 .../{84-dividedsides => 85-narrow_globs}/08-ctxt-insensitive.c | 0 .../09-longjmp-counting-local.c | 0 .../10-longjmp-heap-counting-return.c | 0 .../11-longjmp-counting-return.c | 0 .../12-multiple-growing-updates.c | 0 .../{84-dividedsides => 85-narrow_globs}/13-threaded-ctxt-widen.c | 0 .../{84-dividedsides => 85-narrow_globs}/14-widening-thresholds.c | 0 .../15-intertwined_increment.c | 0 .../16-cyclic-dependency-guarded.c | 0 .../{84-dividedsides => 85-narrow_globs}/17-dead-side-effect.c | 0 .../{84-dividedsides => 85-narrow_globs}/18-dead-side-effect2.c | 0 .../{84-dividedsides => 85-narrow_globs}/19-dead-side-effect3.c | 0 .../{84-dividedsides => 85-narrow_globs}/20-dead-side-effect4.c | 0 .../{84-dividedsides => 85-narrow_globs}/21-dead-escape.c | 0 .../22-dead-escape-indirect.c | 0 22 files changed, 0 insertions(+), 0 deletions(-) rename tests/regression/{84-dividedsides => 85-narrow_globs}/01-modulo-guard.c (100%) rename tests/regression/{84-dividedsides => 85-narrow_globs}/02-state-machine.c (100%) rename tests/regression/{84-dividedsides => 85-narrow_globs}/03-guarded_inc.c (100%) rename tests/regression/{84-dividedsides => 85-narrow_globs}/04-semaphore.c (100%) rename tests/regression/{84-dividedsides => 85-narrow_globs}/05-nested_loop.c (100%) rename tests/regression/{84-dividedsides => 85-narrow_globs}/06-cyclic-dependency.c (100%) rename tests/regression/{84-dividedsides => 85-narrow_globs}/07-ctxt-widen.c (100%) rename tests/regression/{84-dividedsides => 85-narrow_globs}/08-ctxt-insensitive.c (100%) rename tests/regression/{84-dividedsides => 85-narrow_globs}/09-longjmp-counting-local.c (100%) rename tests/regression/{84-dividedsides => 85-narrow_globs}/10-longjmp-heap-counting-return.c (100%) rename tests/regression/{84-dividedsides => 85-narrow_globs}/11-longjmp-counting-return.c (100%) rename tests/regression/{84-dividedsides => 85-narrow_globs}/12-multiple-growing-updates.c (100%) rename tests/regression/{84-dividedsides => 85-narrow_globs}/13-threaded-ctxt-widen.c (100%) rename tests/regression/{84-dividedsides => 85-narrow_globs}/14-widening-thresholds.c (100%) rename tests/regression/{84-dividedsides => 85-narrow_globs}/15-intertwined_increment.c (100%) rename tests/regression/{84-dividedsides => 85-narrow_globs}/16-cyclic-dependency-guarded.c (100%) rename tests/regression/{84-dividedsides => 85-narrow_globs}/17-dead-side-effect.c (100%) rename tests/regression/{84-dividedsides => 85-narrow_globs}/18-dead-side-effect2.c (100%) rename tests/regression/{84-dividedsides => 85-narrow_globs}/19-dead-side-effect3.c (100%) rename tests/regression/{84-dividedsides => 85-narrow_globs}/20-dead-side-effect4.c (100%) rename tests/regression/{84-dividedsides => 85-narrow_globs}/21-dead-escape.c (100%) rename tests/regression/{84-dividedsides => 85-narrow_globs}/22-dead-escape-indirect.c (100%) diff --git a/tests/regression/84-dividedsides/01-modulo-guard.c b/tests/regression/85-narrow_globs/01-modulo-guard.c similarity index 100% rename from tests/regression/84-dividedsides/01-modulo-guard.c rename to tests/regression/85-narrow_globs/01-modulo-guard.c diff --git a/tests/regression/84-dividedsides/02-state-machine.c b/tests/regression/85-narrow_globs/02-state-machine.c similarity index 100% rename from tests/regression/84-dividedsides/02-state-machine.c rename to tests/regression/85-narrow_globs/02-state-machine.c diff --git a/tests/regression/84-dividedsides/03-guarded_inc.c b/tests/regression/85-narrow_globs/03-guarded_inc.c similarity index 100% rename from tests/regression/84-dividedsides/03-guarded_inc.c rename to tests/regression/85-narrow_globs/03-guarded_inc.c diff --git a/tests/regression/84-dividedsides/04-semaphore.c b/tests/regression/85-narrow_globs/04-semaphore.c similarity index 100% rename from tests/regression/84-dividedsides/04-semaphore.c rename to tests/regression/85-narrow_globs/04-semaphore.c diff --git a/tests/regression/84-dividedsides/05-nested_loop.c b/tests/regression/85-narrow_globs/05-nested_loop.c similarity index 100% rename from tests/regression/84-dividedsides/05-nested_loop.c rename to tests/regression/85-narrow_globs/05-nested_loop.c diff --git a/tests/regression/84-dividedsides/06-cyclic-dependency.c b/tests/regression/85-narrow_globs/06-cyclic-dependency.c similarity index 100% rename from tests/regression/84-dividedsides/06-cyclic-dependency.c rename to tests/regression/85-narrow_globs/06-cyclic-dependency.c diff --git a/tests/regression/84-dividedsides/07-ctxt-widen.c b/tests/regression/85-narrow_globs/07-ctxt-widen.c similarity index 100% rename from tests/regression/84-dividedsides/07-ctxt-widen.c rename to tests/regression/85-narrow_globs/07-ctxt-widen.c diff --git a/tests/regression/84-dividedsides/08-ctxt-insensitive.c b/tests/regression/85-narrow_globs/08-ctxt-insensitive.c similarity index 100% rename from tests/regression/84-dividedsides/08-ctxt-insensitive.c rename to tests/regression/85-narrow_globs/08-ctxt-insensitive.c diff --git a/tests/regression/84-dividedsides/09-longjmp-counting-local.c b/tests/regression/85-narrow_globs/09-longjmp-counting-local.c similarity index 100% rename from tests/regression/84-dividedsides/09-longjmp-counting-local.c rename to tests/regression/85-narrow_globs/09-longjmp-counting-local.c diff --git a/tests/regression/84-dividedsides/10-longjmp-heap-counting-return.c b/tests/regression/85-narrow_globs/10-longjmp-heap-counting-return.c similarity index 100% rename from tests/regression/84-dividedsides/10-longjmp-heap-counting-return.c rename to tests/regression/85-narrow_globs/10-longjmp-heap-counting-return.c diff --git a/tests/regression/84-dividedsides/11-longjmp-counting-return.c b/tests/regression/85-narrow_globs/11-longjmp-counting-return.c similarity index 100% rename from tests/regression/84-dividedsides/11-longjmp-counting-return.c rename to tests/regression/85-narrow_globs/11-longjmp-counting-return.c diff --git a/tests/regression/84-dividedsides/12-multiple-growing-updates.c b/tests/regression/85-narrow_globs/12-multiple-growing-updates.c similarity index 100% rename from tests/regression/84-dividedsides/12-multiple-growing-updates.c rename to tests/regression/85-narrow_globs/12-multiple-growing-updates.c diff --git a/tests/regression/84-dividedsides/13-threaded-ctxt-widen.c b/tests/regression/85-narrow_globs/13-threaded-ctxt-widen.c similarity index 100% rename from tests/regression/84-dividedsides/13-threaded-ctxt-widen.c rename to tests/regression/85-narrow_globs/13-threaded-ctxt-widen.c diff --git a/tests/regression/84-dividedsides/14-widening-thresholds.c b/tests/regression/85-narrow_globs/14-widening-thresholds.c similarity index 100% rename from tests/regression/84-dividedsides/14-widening-thresholds.c rename to tests/regression/85-narrow_globs/14-widening-thresholds.c diff --git a/tests/regression/84-dividedsides/15-intertwined_increment.c b/tests/regression/85-narrow_globs/15-intertwined_increment.c similarity index 100% rename from tests/regression/84-dividedsides/15-intertwined_increment.c rename to tests/regression/85-narrow_globs/15-intertwined_increment.c diff --git a/tests/regression/84-dividedsides/16-cyclic-dependency-guarded.c b/tests/regression/85-narrow_globs/16-cyclic-dependency-guarded.c similarity index 100% rename from tests/regression/84-dividedsides/16-cyclic-dependency-guarded.c rename to tests/regression/85-narrow_globs/16-cyclic-dependency-guarded.c diff --git a/tests/regression/84-dividedsides/17-dead-side-effect.c b/tests/regression/85-narrow_globs/17-dead-side-effect.c similarity index 100% rename from tests/regression/84-dividedsides/17-dead-side-effect.c rename to tests/regression/85-narrow_globs/17-dead-side-effect.c diff --git a/tests/regression/84-dividedsides/18-dead-side-effect2.c b/tests/regression/85-narrow_globs/18-dead-side-effect2.c similarity index 100% rename from tests/regression/84-dividedsides/18-dead-side-effect2.c rename to tests/regression/85-narrow_globs/18-dead-side-effect2.c diff --git a/tests/regression/84-dividedsides/19-dead-side-effect3.c b/tests/regression/85-narrow_globs/19-dead-side-effect3.c similarity index 100% rename from tests/regression/84-dividedsides/19-dead-side-effect3.c rename to tests/regression/85-narrow_globs/19-dead-side-effect3.c diff --git a/tests/regression/84-dividedsides/20-dead-side-effect4.c b/tests/regression/85-narrow_globs/20-dead-side-effect4.c similarity index 100% rename from tests/regression/84-dividedsides/20-dead-side-effect4.c rename to tests/regression/85-narrow_globs/20-dead-side-effect4.c diff --git a/tests/regression/84-dividedsides/21-dead-escape.c b/tests/regression/85-narrow_globs/21-dead-escape.c similarity index 100% rename from tests/regression/84-dividedsides/21-dead-escape.c rename to tests/regression/85-narrow_globs/21-dead-escape.c diff --git a/tests/regression/84-dividedsides/22-dead-escape-indirect.c b/tests/regression/85-narrow_globs/22-dead-escape-indirect.c similarity index 100% rename from tests/regression/84-dividedsides/22-dead-escape-indirect.c rename to tests/regression/85-narrow_globs/22-dead-escape-indirect.c From b6ceb8ced6dbdd9cde8bd097f58bd2bcfc7a9d1d Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 17 Apr 2025 14:04:25 +0200 Subject: [PATCH 31/36] Changes to tests Co-authored-by: Simmo Saan --- tests/regression/85-narrow_globs/02-state-machine.c | 3 ++- tests/regression/85-narrow_globs/07-ctxt-widen.c | 2 +- tests/regression/85-narrow_globs/08-ctxt-insensitive.c | 3 ++- .../regression/85-narrow_globs/12-multiple-growing-updates.c | 3 ++- tests/regression/85-narrow_globs/13-threaded-ctxt-widen.c | 3 ++- tests/regression/85-narrow_globs/14-widening-thresholds.c | 2 +- tests/regression/85-narrow_globs/15-intertwined_increment.c | 4 ++-- .../85-narrow_globs/16-cyclic-dependency-guarded.c | 5 ++--- 8 files changed, 14 insertions(+), 11 deletions(-) diff --git a/tests/regression/85-narrow_globs/02-state-machine.c b/tests/regression/85-narrow_globs/02-state-machine.c index f144768793..43e6f23d84 100644 --- a/tests/regression/85-narrow_globs/02-state-machine.c +++ b/tests/regression/85-narrow_globs/02-state-machine.c @@ -1,5 +1,6 @@ // PARAM: --enable ana.int.interval --enable solvers.td3.narrow-globs.enabled -#include +#include +#include int state = 0; diff --git a/tests/regression/85-narrow_globs/07-ctxt-widen.c b/tests/regression/85-narrow_globs/07-ctxt-widen.c index 92fe3371e8..12cfdfdaea 100644 --- a/tests/regression/85-narrow_globs/07-ctxt-widen.c +++ b/tests/regression/85-narrow_globs/07-ctxt-widen.c @@ -1,6 +1,6 @@ // 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 +#include int h(int i) { diff --git a/tests/regression/85-narrow_globs/08-ctxt-insensitive.c b/tests/regression/85-narrow_globs/08-ctxt-insensitive.c index 6ded214460..b3ed58bfe4 100644 --- a/tests/regression/85-narrow_globs/08-ctxt-insensitive.c +++ b/tests/regression/85-narrow_globs/08-ctxt-insensitive.c @@ -1,10 +1,11 @@ // 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; } - assert(i == 0); + __goblint_check(i == 0); return 1; } diff --git a/tests/regression/85-narrow_globs/12-multiple-growing-updates.c b/tests/regression/85-narrow_globs/12-multiple-growing-updates.c index 52952c752e..77be309d99 100644 --- a/tests/regression/85-narrow_globs/12-multiple-growing-updates.c +++ b/tests/regression/85-narrow_globs/12-multiple-growing-updates.c @@ -1,11 +1,12 @@ // 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) { +void *thread(void *d) { for(int i = 0; i < 10; i++) { pthread_mutex_lock(&mutex); glob = i; diff --git a/tests/regression/85-narrow_globs/13-threaded-ctxt-widen.c b/tests/regression/85-narrow_globs/13-threaded-ctxt-widen.c index 9cad9d63a8..74cb400ae6 100644 --- a/tests/regression/85-narrow_globs/13-threaded-ctxt-widen.c +++ b/tests/regression/85-narrow_globs/13-threaded-ctxt-widen.c @@ -1,11 +1,12 @@ // 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) { +void *thread(void *d) { f(10); return NULL; } diff --git a/tests/regression/85-narrow_globs/14-widening-thresholds.c b/tests/regression/85-narrow_globs/14-widening-thresholds.c index 170c7a9537..8ddd060f57 100644 --- a/tests/regression/85-narrow_globs/14-widening-thresholds.c +++ b/tests/regression/85-narrow_globs/14-widening-thresholds.c @@ -1,7 +1,7 @@ // 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 -//TODO: this tests that threshold widening also narrows correctly. This should not be in this folder pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; int glob = 0; diff --git a/tests/regression/85-narrow_globs/15-intertwined_increment.c b/tests/regression/85-narrow_globs/15-intertwined_increment.c index 0d5e1f5aae..04af57e547 100644 --- a/tests/regression/85-narrow_globs/15-intertwined_increment.c +++ b/tests/regression/85-narrow_globs/15-intertwined_increment.c @@ -1,6 +1,6 @@ -// PARAM: --enable ana.int.interval --enable solvers.td3.narrow-globs.enabled +// PARAM: --enable ana.int.interval --enable solvers.td3.narrow-globs.enabled #include -#include +#include int a, b; pthread_mutex_t m = PTHREAD_MUTEX_INITIALIZER; diff --git a/tests/regression/85-narrow_globs/16-cyclic-dependency-guarded.c b/tests/regression/85-narrow_globs/16-cyclic-dependency-guarded.c index a555823c9d..7407049aac 100644 --- a/tests/regression/85-narrow_globs/16-cyclic-dependency-guarded.c +++ b/tests/regression/85-narrow_globs/16-cyclic-dependency-guarded.c @@ -1,6 +1,5 @@ // 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 - -// This is supposed to check if the solver terminates +// NOTIMEOUT #include #include @@ -32,4 +31,4 @@ int main(void) { __goblint_check(b <= 10); pthread_mutex_unlock(&mutex); return 0; -} \ No newline at end of file +} From f85eea0f8ef48da4dcb62dfa55a535878984016d Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 17 Apr 2025 14:07:14 +0200 Subject: [PATCH 32/36] Fail when interactive & narrowing on globals are active. --- src/maingoblint.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 73f2273fc1..bd65ab4eb8 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -168,8 +168,7 @@ let check_arguments () = 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 ( - set_bool "solvers.td3.narrow-globs.enabled" false; - warn "solvers.td3.narrow-globs.enabled implicitly disabled by incremental analysis"; + 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"; From e250672bf9970f43d479c50810aa67b08dba645d Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 17 Apr 2025 14:08:21 +0200 Subject: [PATCH 33/36] Fix merge artifact with option check --- src/maingoblint.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index bd65ab4eb8..ad04fbf3aa 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -164,7 +164,7 @@ let check_arguments () = "trans.activated: to increase the precision of 'remove_dead_code' transform, disable " ^ String.concat " and " @@ List.map (fun s -> "'" ^ s ^ "'") imprecise_options) ); - 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 "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 ( From 21d4c8d548af1ae3020e03cbd751e544c10a0dc4 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 17 Apr 2025 14:14:48 +0200 Subject: [PATCH 34/36] Test 85/21: Comment on perhaps surprising lack of precision --- tests/regression/85-narrow_globs/21-dead-escape.c | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/tests/regression/85-narrow_globs/21-dead-escape.c b/tests/regression/85-narrow_globs/21-dead-escape.c index 401db937bc..45f60fffea 100644 --- a/tests/regression/85-narrow_globs/21-dead-escape.c +++ b/tests/regression/85-narrow_globs/21-dead-escape.c @@ -22,7 +22,10 @@ void* f(void *d) { // so none of these unknowns are queried and this check // succeeds whether eliminate-dead is on or not. __goblint_check(i == 1); - // Paradoxically, a != &i is not known without eliminate-dead. + // 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; } @@ -34,6 +37,6 @@ int main(void) { // 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 +} From 058b23dd03216fbd36855841f56067c6b7160185 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 17 Apr 2025 14:16:31 +0200 Subject: [PATCH 35/36] UpdateRules: remove unused `active` bool --- src/solver/td3UpdateRule.ml | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/solver/td3UpdateRule.ml b/src/solver/td3UpdateRule.ml index 5977dd2773..48972a54d1 100644 --- a/src/solver/td3UpdateRule.ml +++ b/src/solver/td3UpdateRule.ml @@ -9,7 +9,6 @@ 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 active: bool val create_empty_data : unit -> data val copy_marshal: data -> data val relift_marshal: data -> data @@ -40,7 +39,6 @@ module Inactive:S = struct type data = unit type eq_wrapper = S.v -> ((S.v -> S.d -> unit) -> S.d) -> S.d - let active = false let create_empty_data () = () let copy_marshal _ = () let relift_marshal _ = () @@ -66,7 +64,6 @@ module Narrow:S = type eq_wrapper = S.v -> ((S.v -> S.d -> unit) -> S.d) -> S.d - let active = false let create_empty_data () = let narrow_globs = GobConfig.get_bool "solvers.td3.narrow-globs.enabled" in { From fa3125d925757f74046cdeafaeaefe1ad5972571 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 17 Apr 2025 14:43:29 +0200 Subject: [PATCH 36/36] Document `postmortem` --- src/constraint/constrSys.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/constraint/constrSys.ml b/src/constraint/constrSys.ml index 8e7e29448c..9800c5c015 100644 --- a/src/constraint/constrSys.ml +++ b/src/constraint/constrSys.ml @@ -46,9 +46,11 @@ 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