diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 43e2ad1d59..3e3378252a 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -2395,6 +2395,20 @@ "enum": ["never", "always", "sides", "cycle", "unstable_called", "unstable_self", "sides-pp","sides-local"], "default": "sides" }, + "side_widen_gas": { + "title": "solvers.td3.side_widen_gas", + "description": + "Delay widening globals through side-effects. With a widening gas of N, the solver will perform widening only once unknown has grown through side-effects N times and the widening condition according to the side_widen policy has been met. A value of 0 behaves as before the feature was introduced.", + "type": "integer", + "default": 0 + }, + "widen_gas": { + "title": "solvers.td3.widen_gas", + "description": + "Delay widening non-globals, i.e. unknowns with right hand sides. With a widening gas of N, the solver will perform widening only once unknown has grown N times. A value of 0 behaves as before the feature was introduced.", + "type": "integer", + "default": 0 + }, "space": { "title": "solvers.td3.space", "description": diff --git a/src/solver/goblint_solver.ml b/src/solver/goblint_solver.ml index 0a264d7dea..9a14c5b13e 100644 --- a/src/solver/goblint_solver.ml +++ b/src/solver/goblint_solver.ml @@ -29,3 +29,5 @@ module PostSolver = PostSolver module LocalFixpoint = LocalFixpoint module SolverStats = SolverStats module SolverBox = SolverBox + +module SideWPointSelect = SideWPointSelect diff --git a/src/solver/sideWPointSelect.ml b/src/solver/sideWPointSelect.ml new file mode 100644 index 0000000000..06eb2e9025 --- /dev/null +++ b/src/solver/sideWPointSelect.ml @@ -0,0 +1,222 @@ +(** Strategies for widening leaf unknowns *) + +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 + + (** Create data required by this widening point selection strategy. + The parameters are not necessarily used by all strategies. + @param is_stable This callback should return whether an unknown is stable. + @param add_infl Allows the strategy to record additional influences. + This is mainly intended for strategies like unstable-self, + which records the influence of a side-effecting unknown x to the leaf y. + *) + val create_data: (S.v -> bool) -> (S.v -> S.v -> unit) -> data + + (** Notifies this strategy that a side-effect has occured. + This allows the strategy to adapt its internal data structure. + @param data The internal state of this strategy + @param x The optional source of the side-effect + @param y The leaf receiving the side-effect + *) + val notify_side: data -> S.v option -> S.v -> unit + + (** Whether the destabilization of the side-effected var should record the destabilization + of called variables and start variables. This information should be passed to [should_mark_wpoint] + by the solver. + *) + val record_destabilized_vs: bool + + (** This strategy can decide to prevent widening. + Note that, if this strategy does not veto, this does not mean that widening + will necessarily be performed. Nor does a call to this function imply that + the value of the leaf has grown. + @param data The internal state of this strategy + @param called Set of called unknowns + @param old_sides Prior side-effects to leaf y + @param x Optional source of the side-effect + @param y Side-effected leaf y + @return [true]: widening will not be applied; [false]: widening might be applied + *) + val veto_widen: data -> unit HM.t -> VS.t -> S.v option -> S.v -> bool + + (** The value of the leaf has grown. Should it be marked a widening point? + Widening points are widened when their value grows, unless vetoed. + Even if this function is called, leaf y might already be a widening point + from an earlier side-effect. + @param data The internal state of this strategy + @param called Set of called unknowns + @param old_sides Prior side-effects to leaf y + @param x Optional source of the side-effect + @param y Side-effected leaf y + @param destabilized_vs Optional destabilization info, described in [record_destabilized_vs] + @return [true]: mark as widening point; [false]: do not mark as widening point + + *) + val should_mark_wpoint: data -> unit HM.t -> VS.t -> S.v option -> S.v -> bool option -> bool + end + +(** Any side-effect after the first one will be widened which will unnecessarily lose precision. *) +module Always : 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 create_data _ _ = () + let notify_side _ _ _ = () + let record_destabilized_vs = false + let veto_widen _ _ _ _ _ = false + let should_mark_wpoint _ _ _ _ _ _ = true + end + +(* On side-effect cycles, this should terminate via the outer `solver` loop. TODO check. *) +(** Never widen side-effects. *) +module Never : 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 create_data _ _ = () + let notify_side _ _ _ = () + let record_destabilized_vs = false + let veto_widen _ _ _ _ _ = false + let should_mark_wpoint _ _ _ _ _ _ = false + end + +(** Widening check happens by checking sides. + Only widen if value increases and there has already been a side-effect from the same source *) +module SidesLocal : 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 create_data _ _ = () + let notify_side _ _ _ = () + let record_destabilized_vs = false + let veto_widen state called old_sides x y = + match x with + | None -> false + | Some x when VS.mem x old_sides -> false + | _ -> true + let should_mark_wpoint _ _ _ _ _ _ = true + end + +(** If there was already a `side x y d` from the same program point and now again, make y a widening point. + Different from `Sides` in that it will not distinguish between side-effects from different contexts, + only the program point matters. *) +module SidesPP : 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 create_data _ _ = () + let notify_side _ _ _ = () + let record_destabilized_vs = false + let veto_widen state called old_sides x y = false + let should_mark_wpoint state called old_sides x y _ = match x with + | Some x -> + let n = S.Var.node x in + VS.exists (fun v -> Node.equal (S.Var.node v) n) old_sides + | None -> false + (* TODO: This is consistent with the previous implementation, but if multiple side-effects come in with x = None, + the leaf will never be widened. This is different from SidesLocal *) + end + +(** If there already was a `side x y d` that changed rho[y] and now again, we make y a wpoint. + x caused more than one update to y. >=3 partial context calls will be precise since sides come from different x. TODO this has 8 instead of 5 phases of `solver` for side_cycle.c *) +module Sides : 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 create_data _ _ = () + let notify_side _ _ _ = () + let record_destabilized_vs = false + let veto_widen state called old_sides x y = false + let should_mark_wpoint state called old_sides x y _ = match x with | Some(x) -> VS.mem x old_sides | None -> true + end + +(* TODO: The following two don't check if a vs got destabilized which may be a problem. *) + +(* TODO test/remove. Check for which examples this is problematic! *) +(** Side to y destabilized itself via some infl-cycle. Records influences from unknowns to globals *) +module UnstableSelf : 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 = { is_stable: S.v -> bool; add_infl: S.v -> S.v -> unit } + + let create_data is_stable add_infl = { is_stable; add_infl } + let notify_side data x y = (match x with None -> () | Some x -> data.add_infl x y) + let record_destabilized_vs = false + let veto_widen _ _ _ _ _ = false + let should_mark_wpoint state called old_sides x y _ = not (state.is_stable y) + end + +(* TODO test/remove. *) +(** Widen if any called var (not just y) is no longer stable. Expensive! *) +module UnstableCalled : 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 = { is_stable: S.v -> bool } + + let create_data is_stable _ = { is_stable } + let notify_side _ _ _ = () + let record_destabilized_vs = false + let veto_widen state called old_sides y x = false + let should_mark_wpoint state called old_sides y x _ = HM.exists (fun k _ -> not (state.is_stable k)) called (* this is very expensive since it iterates over called! see https://github.com/goblint/analyzer/issues/265#issuecomment-880748636 *) + end + +(** Destabilized a called or start var. Problem: two partial context calls will be precise, but third call will widen the state. + If this side destabilized some of the initial unknowns vs, there may be a side-cycle between vs and we should make y a wpoint *) +module Cycle : 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 create_data _ _ = () + let notify_side _ _ _ = () + let record_destabilized_vs = true + let veto_widen state called old_sides x y = false + let should_mark_wpoint state called old_sides x y cycle = + match cycle with + | Some cycle -> + if tracing && cycle then trace "side_widen" "cycle: should mark wpoint %a" S.Var.pretty_trace y; + cycle + | None -> + failwith "destabilize_vs information not provided to side_widen cycle strategy"; + end + +let choose_impl: unit -> (module S) = fun () -> + let conf = GobConfig.get_string "solvers.td3.side_widen" in + match conf with + | "always" -> (module Always) + | "never" -> (module Never) + | "sides-local" -> (module SidesLocal) + | "sides" -> (module Sides) + | "sides-pp" -> (module SidesPP) + | "unstable-self" -> (module UnstableSelf) + | "unstable-called" -> (module UnstableCalled) + | "cycle" -> (module Cycle) + | _ -> failwith ("Unknown value '" ^ conf ^ "' for option solvers.td3.side_widen!") diff --git a/src/solver/td3.ml b/src/solver/td3.ml index 3cab3cf7f7..c336e8ee5c 100644 --- a/src/solver/td3.ml +++ b/src/solver/td3.ml @@ -56,7 +56,7 @@ module Base = infl: VS.t HM.t; sides: VS.t HM.t; rho: S.Dom.t HM.t; - wpoint: unit 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; side_dep: VS.t HM.t; (** Dependencies of side-effected variables. Knowing these allows restarting them and re-triggering all side effects. *) side_infl: VS.t HM.t; (** Influences to side-effected variables. Not normally in [infl], but used for restarting them. *) @@ -72,7 +72,7 @@ module Base = infl = HM.create 10; sides = HM.create 10; rho = HM.create 10; - wpoint = HM.create 10; + wpoint_gas = HM.create 10; stable = HM.create 10; side_dep = HM.create 10; side_infl = HM.create 10; @@ -85,7 +85,7 @@ module Base = Logs.debug "|rho|=%d" (HM.length data.rho); Logs.debug "|stable|=%d" (HM.length data.stable); Logs.debug "|infl|=%d" (HM.length data.infl); - Logs.debug "|wpoint|=%d" (HM.length data.wpoint); + Logs.debug "|wpoint_gas|=%d" (HM.length data.wpoint_gas); Logs.debug "|sides|=%d" (HM.length data.sides); Logs.debug "|side_dep|=%d" (HM.length data.side_dep); Logs.debug "|side_infl|=%d" (HM.length data.side_infl); @@ -116,7 +116,7 @@ module Base = { rho = HM.copy data.rho; stable = HM.copy data.stable; - wpoint = HM.copy data.wpoint; + wpoint_gas = HM.copy data.wpoint_gas; infl = HM.copy data.infl; sides = HM.copy data.sides; side_infl = HM.copy data.side_infl; @@ -152,10 +152,10 @@ module Base = HM.iter (fun k v -> HM.replace stable (S.Var.relift k) v ) data.stable; - let wpoint = HM.create (HM.length data.wpoint) in + let wpoint_gas = HM.create (HM.length data.wpoint_gas) in HM.iter (fun k v -> - HM.replace wpoint (S.Var.relift k) v - ) data.wpoint; + HM.replace wpoint_gas (S.Var.relift k) v + ) data.wpoint_gas; let infl = HM.create (HM.length data.infl) in HM.iter (fun k v -> HM.replace infl (S.Var.relift k) (VS.map S.Var.relift v) @@ -189,7 +189,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; rho; wpoint_gas; stable; side_dep; side_infl; var_messages; rho_write; dep} type phase = Widen | Narrow [@@deriving show] (* used in inner solve *) @@ -208,7 +208,7 @@ module Base = HM.clear data.infl ); if not reuse_wpoint then ( - HM.clear data.wpoint; + HM.clear data.wpoint_gas; HM.clear data.sides ); data @@ -217,7 +217,8 @@ module Base = in let term = GobConfig.get_bool "solvers.td3.term" in - let side_widen = GobConfig.get_string "solvers.td3.side_widen" in + let default_side_widen_gas = GobConfig.get_int "solvers.td3.side_widen_gas" in + let default_widen_gas = GobConfig.get_int "solvers.td3.widen_gas" in let space = GobConfig.get_bool "solvers.td3.space" in let cache = GobConfig.get_bool "solvers.td3.space_cache" in let called = HM.create 10 in @@ -225,7 +226,7 @@ module Base = let infl = data.infl in let sides = data.sides in let rho = data.rho in - let wpoint = data.wpoint in + let wpoint_gas = data.wpoint_gas in let stable = data.stable in let narrow_reuse = GobConfig.get_bool "solvers.td3.narrow-reuse" in @@ -252,6 +253,11 @@ module Base = let rho_write = data.rho_write in let dep = data.dep in + let (module WPS) = SideWPointSelect.choose_impl () in + let module WPS = struct + include WPS (S) (HM) (VS) + end in + let () = print_solver_stats := fun () -> print_data data; Logs.info "|called|=%d" (HM.length called); @@ -275,6 +281,21 @@ module Base = let destabilize_ref: (S.v -> unit) ref = ref (fun _ -> failwith "no destabilize yet") in let destabilize x = !destabilize_ref x in (* must be eta-expanded to use changed destabilize_ref *) + let format_wpoint x = Option.map_default (fun x -> Printf.sprintf "true (gas: %d)" x) "false" (HM.find_option wpoint_gas x) in + let mark_wpoint x default_gas = + if not (HM.mem wpoint_gas x) then (HM.replace wpoint_gas x default_gas) in + let reduce_gas x = + match HM.find_option wpoint_gas x with + | Some old_gas -> + let decremented_gas = old_gas - 1 in + if decremented_gas >= 0 then ( + if tracing then trace "widengas" "reducing gas of %a: %d -> %d" S.Var.pretty_trace x old_gas decremented_gas; + HM.replace wpoint_gas x decremented_gas + ) + | None -> ((* Not a widening point *)) in + let should_widen x = HM.find_option wpoint_gas x = Some 0 in + let wps_data = WPS.create_data (fun x -> HM.mem stable x) add_infl in + (* Same as destabilize, but returns true if it destabilized a called var, or a var in vs which was stable. *) let rec destabilize_vs x = (* TODO remove? Only used for side_widen cycle. *) if tracing then trace "sol2" "destabilize_vs %a" S.Var.pretty_trace x; @@ -291,19 +312,19 @@ module Base = true ) w false (* nosemgrep: fold-exists *) (* does side effects *) and solve ?reuse_eq x phase = - if tracing then trace "sol2" "solve %a, phase: %s, called: %b, stable: %b, wpoint: %b" S.Var.pretty_trace x (show_phase phase) (HM.mem called x) (HM.mem stable x) (HM.mem wpoint x); + if tracing then trace "sol2" "solve %a, phase: %s, called: %b, stable: %b, wpoint: %s" S.Var.pretty_trace x (show_phase phase) (HM.mem called x) (HM.mem stable x) (format_wpoint x); init x; assert (Hooks.system x <> None); if not (HM.mem called x || HM.mem stable x) then ( if tracing then trace "sol2" "stable add %a" S.Var.pretty_trace x; HM.replace stable x (); HM.replace called x (); - (* Here we cache HM.mem wpoint x before eq. If during eq eval makes x wpoint, then be still don't apply widening the first time, but just overwrite. + (* Here we cache should_widen x before eq. If during eq eval makes x wpoint (with config widen_gas = 0), then be still don't apply widening the first time, but just overwrite. It means that the first iteration at wpoint is still precise. This doesn't matter during normal solving (?), because old would be bot. This matters during incremental loading, when wpoints have been removed (or not marshaled) and are redetected. Then the previous local wpoint value is discarded automagically and not joined/widened, providing limited restarting of local wpoints. (See eval for more complete restarting.) *) - let wp = HM.mem wpoint x in (* if x becomes a wpoint during eq, checking this will delay widening until next solve *) + let wp = should_widen x in (* if x becomes a wpoint (with gas = 0) during eq, checking this will delay widening until next solve *) let l = HM.create 10 in (* local cache *) let eqd = (* d from equation/rhs *) match reuse_eq with @@ -319,17 +340,24 @@ module Base = 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 *) + + (* if value has changed, reduce gas (only applies to marked widening points) *) + if not (term && phase = Narrow) && not (S.Dom.equal eqd old) then reduce_gas x; + let wpd = (* d after widen/narrow (if wp) *) if not wp then eqd - else if term then - match phase with - | Widen -> S.Dom.widen old (S.Dom.join old eqd) - | Narrow when GobConfig.get_bool "exp.no-narrow" -> old (* no narrow *) - | Narrow -> - (* assert S.Dom.(leq eqd old || not (leq old eqd)); (* https://github.com/goblint/analyzer/pull/490#discussion_r875554284 *) *) - S.Dom.narrow old eqd - else - box old eqd + else ( + if term then + match phase with + | Widen -> S.Dom.widen old (S.Dom.join old eqd) + | Narrow when GobConfig.get_bool "exp.no-narrow" -> old (* no narrow *) + | Narrow -> + (* assert S.Dom.(leq eqd old || not (leq old eqd)); (* https://github.com/goblint/analyzer/pull/490#discussion_r875554284 *) *) + S.Dom.narrow old eqd + else ( + box old eqd + ) + ) in if tracing then trace "sol" "Var: %a (wp: %b)\nOld value: %a\nEqd: %a\nNew value: %a" S.Var.pretty_trace x wp S.Dom.pretty old S.Dom.pretty eqd S.Dom.pretty wpd; if cache then ( @@ -339,7 +367,7 @@ module Base = if not (Timing.wrap "S.Dom.equal" (fun () -> S.Dom.equal old wpd) ()) then ( (* value changed *) if tracing then trace "sol" "Changed"; (* if tracing && not (S.Dom.is_bot old) && HM.mem wpoint x then trace "solchange" "%a (wpx: %b): %a -> %a" S.Var.pretty_trace x (HM.mem wpoint x) S.Dom.pretty old S.Dom.pretty wpd; *) - if tracing && not (S.Dom.is_bot old) && HM.mem wpoint x then trace "solchange" "%a (wpx: %b): %a" S.Var.pretty_trace x (HM.mem wpoint x) S.Dom.pretty_diff (wpd, old); + if tracing && not (S.Dom.is_bot old) && should_widen x then trace "solchange" "%a (wpx: %s): %a" S.Var.pretty_trace x (format_wpoint x) S.Dom.pretty_diff (wpd, old); update_var_event x old wpd; HM.replace rho x wpd; destabilize x; @@ -350,7 +378,7 @@ module Base = if tracing then trace "sol2" "solve still unstable %a" S.Var.pretty_trace x; (solve[@tailcall]) x Widen ) else ( - if term && phase = Widen && HM.mem wpoint x then ( (* TODO: or use wp? *) + if term && phase = Widen && HM.mem wpoint_gas x then ( (* TODO: or use wp? *) if tracing then trace "sol2" "solve switching to narrow %a" S.Var.pretty_trace x; if tracing then trace "sol2" "stable remove %a" S.Var.pretty_trace x; HM.remove stable x; @@ -358,8 +386,8 @@ module Base = Hooks.stable_remove x; (solve[@tailcall]) ~reuse_eq:eqd x Narrow ) else if remove_wpoint && not space && (not term || phase = Narrow) then ( (* this makes e.g. nested loops precise, ex. tests/regression/34-localization/01-nested.c - if we do not remove wpoint, the inner loop head will stay a wpoint and widen the outer loop variable. *) - if tracing then trace "sol2" "solve removing wpoint %a (%b)" S.Var.pretty_trace x (HM.mem wpoint x); - HM.remove wpoint x + if tracing then trace "sol2" "solve removing wpoint %a (%s)" S.Var.pretty_trace x (format_wpoint x); + HM.remove wpoint_gas x; ) ) ) @@ -372,22 +400,23 @@ module Base = and simple_solve l x y = if tracing then trace "sol2" "simple_solve %a (rhs: %b)" S.Var.pretty_trace y (Hooks.system y <> None); if Hooks.system y = None then (init y; HM.replace stable y (); HM.find rho y) else - if not space || HM.mem wpoint y then (solve y Widen; HM.find rho y) else + (* TODO: should td_space store information for widening points with remaining gas? *) + if not space || HM.mem wpoint_gas y then (solve y Widen; HM.find rho y) else if HM.mem called y then (init y; HM.remove l y; HM.find rho y) else (* TODO: [HM.mem called y] is not in the TD3 paper, what is it for? optimization? *) - (* if HM.mem called y then (init y; let y' = HM.find_default l y (S.Dom.bot ()) in HM.replace rho y y'; HM.remove l y; y') else *) + (* if HM.mem called y then (init y; let y' = HM.find_default l y (S.Dom.bot ()) in HM.replace rho y y'; HM.remove l y; y') else *) 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 HM.remove called y; - if HM.mem wpoint y then (HM.remove l y; solve y Widen; HM.find rho 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) ) and eval l x y = if tracing then trace "sol2" "eval %a ## %a" S.Var.pretty_trace x S.Var.pretty_trace y; get_var_event y; if HM.mem called y then ( - if restart_wpoint && not (HM.mem wpoint y) then ( + if restart_wpoint && not (HM.mem wpoint_gas y) then ( (* Even though solve cleverly restarts redetected wpoints during incremental load, the loop body would be calculated based on the old wpoint value. The loop body might then side effect the old value, see tests/incremental/06-local-wpoint-read. Here we avoid this, by setting it to bottom for the loop body eval. *) @@ -399,20 +428,22 @@ module Base = ) ); if tracing then trace "sol2" "eval adding wpoint %a from %a" S.Var.pretty_trace y S.Var.pretty_trace x; - HM.replace wpoint y (); + mark_wpoint y default_widen_gas; ); let tmp = simple_solve l x y in if HM.mem rho y then add_infl y x; if tracing then trace "sol2" "eval %a ## %a -> %a" S.Var.pretty_trace x S.Var.pretty_trace y S.Dom.pretty tmp; 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: %b) from %a ## value: %a" S.Var.pretty_trace y (HM.mem wpoint y) (Pretty.docOpt (S.Var.pretty_trace ())) x S.Dom.pretty d; + if tracing then trace "sol2" "side to %a (wpx: %s) from %a ## value: %a" S.Var.pretty_trace y (format_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); init y; - (match x with None -> () | Some x -> if side_widen = "unstable_self" then add_infl x y); + + WPS.notify_side wps_data x y; + let widen a b = if M.tracing then M.traceli "sol2" "side widen %a %a" S.Dom.pretty a S.Dom.pretty b; let r = S.Dom.widen a (S.Dom.join a b) in @@ -420,69 +451,39 @@ module Base = r in let old_sides = HM.find_default sides y VS.empty in - let op a b = match side_widen with - | "sides-local" when not (S.Dom.leq b a) -> ( - match x with - | None -> widen a b - | Some x when VS.mem x old_sides -> widen a b - | _ -> S.Dom.join a b - ) - | _ when HM.mem wpoint y -> widen a b - | _ -> S.Dom.join a b + let vetoed_widen = WPS.veto_widen wps_data called old_sides x y in + let op a b = (* If y still has widening gas, widening will not be performed. *) + if vetoed_widen || not (should_widen y) then S.Dom.join a b else widen a b in let old = HM.find rho y in let tmp = op old d in if tracing then trace "sol2" "stable add %a" S.Var.pretty_trace y; HM.replace stable y (); if not (S.Dom.leq tmp old) then ( - if tracing && not (S.Dom.is_bot old) then trace "solside" "side to %a (wpx: %b) from %a: %a -> %a" S.Var.pretty_trace y (HM.mem wpoint y) (Pretty.docOpt (S.Var.pretty_trace ())) x S.Dom.pretty old S.Dom.pretty tmp; - if tracing && not (S.Dom.is_bot old) then trace "solchange" "side to %a (wpx: %b) from %a: %a" S.Var.pretty_trace y (HM.mem wpoint y) (Pretty.docOpt (S.Var.pretty_trace ())) x S.Dom.pretty_diff (tmp, old); - let sided = match x with - | Some x -> - let sided = VS.mem x old_sides in - if not sided then add_sides y x; - sided - | None -> false - in + if tracing && not (S.Dom.is_bot old) then trace "solside" "side to %a (wpx: %s) from %a: %a -> %a" S.Var.pretty_trace y (format_wpoint y) (Pretty.docOpt (S.Var.pretty_trace ())) x S.Dom.pretty old S.Dom.pretty tmp; + if tracing && not (S.Dom.is_bot old) then trace "solchange" "side to %a (wpx: %s) from %a: %a" S.Var.pretty_trace y (format_wpoint y) (Pretty.docOpt (S.Var.pretty_trace ())) x S.Dom.pretty_diff (tmp, old); + + (match x with + | Some x -> + if not (VS.mem x old_sides) then add_sides y x; + | None -> ()); + (* HM.replace rho y ((if HM.mem wpoint y then S.Dom.widen old else identity) (S.Dom.join old d)); *) HM.replace rho y tmp; - if side_widen <> "cycle" then destabilize y; + let destabilized_vs: bool option = if WPS.record_destabilized_vs then ( + destabilize y; + None + ) else + Some (destabilize_vs y) in + (* make y a widening point if ... This will only matter for the next side _ y. *) - let wpoint_if e = - if e then ( - if tracing then trace "sol2" "side adding wpoint %a from %a" S.Var.pretty_trace y (Pretty.docOpt (S.Var.pretty_trace ())) x; - HM.replace wpoint y () - ) - in - match side_widen with - | "always" -> (* Any side-effect after the first one will be widened which will unnecessarily lose precision. *) - wpoint_if true - | "never" -> (* On side-effect cycles, this should terminate via the outer `solver` loop. TODO check. *) - () - | "sides-local" -> (* Never make globals widening points in this strategy, the widening check happens by checking sides *) - () - | "sides" -> - (* if there already was a `side x y d` that changed rho[y] and now again, we make y a wpoint *) - (* x caused more than one update to y. >=3 partial context calls will be precise since sides come from different x. TODO this has 8 instead of 5 phases of `solver` for side_cycle.c *) - wpoint_if sided - | "sides-pp" -> - begin match x with - | Some x -> - let n = S.Var.node x in - let sided = VS.exists (fun v -> Node.equal (S.Var.node v) n) old_sides in - wpoint_if sided - | None -> () - end - | "cycle" -> (* destabilized a called or start var. Problem: two partial context calls will be precise, but third call will widen the state. *) - (* if this side destabilized some of the initial unknowns vs, there may be a side-cycle between vs and we should make y a wpoint *) - let destabilized_vs = destabilize_vs y in - wpoint_if destabilized_vs - (* TODO: The following two don't check if a vs got destabilized which may be a problem. *) - | "unstable_self" -> (* TODO test/remove. Side to y destabilized itself via some infl-cycle. The above add_infl is only required for this option. Check for which examples this is problematic! *) - wpoint_if @@ not (HM.mem stable y) - | "unstable_called" -> (* TODO test/remove. Widen if any called var (not just y) is no longer stable. Expensive! *) - wpoint_if @@ exists_key (neg (HM.mem stable)) called (* this is very expensive since it folds over called! see https://github.com/goblint/analyzer/issues/265#issuecomment-880748636 *) - | x -> failwith ("Unknown value '" ^ x ^ "' for option solvers.td3.side_widen!") + if WPS.should_mark_wpoint wps_data called old_sides x y destabilized_vs then ( + if tracing then trace "sol2" "side adding wpoint %a from %a" S.Var.pretty_trace y (Pretty.docOpt (S.Var.pretty_trace ())) x; + mark_wpoint y default_side_widen_gas + ); + + (* y has grown. Reduce widening gas! *) + if not vetoed_widen then reduce_gas y; ) and init x = if tracing then trace "sol2" "init %a" S.Var.pretty_trace x; @@ -527,7 +528,7 @@ module Base = Logs.debug "Restarting to bot %a" S.Var.pretty_trace x; HM.replace rho x (S.Dom.bot ()); (* HM.remove rho x; *) - HM.remove wpoint x; (* otherwise gets immediately widened during resolve *) + HM.remove wpoint_gas x; (* otherwise gets immediately widened during resolve *) HM.remove sides x; (* just in case *) (* immediately redo "side effect" from st *) @@ -648,7 +649,7 @@ module Base = let delete_marked s = List.iter (fun k -> HM.remove s k) sys_change.delete in delete_marked rho; delete_marked infl; (* TODO: delete from inner sets? *) - delete_marked wpoint; + delete_marked wpoint_gas; delete_marked dep; Hooks.delete_marked sys_change.delete; @@ -860,7 +861,7 @@ module Base = if GobConfig.get_bool "dbg.print_wpoints" then ( Logs.newline (); Logs.debug "Widening points:"; - HM.iter (fun k () -> Logs.debug "%a" S.Var.pretty_trace k) wpoint; + HM.iter (fun k gas -> Logs.debug "%a (gas: %d)" S.Var.pretty_trace k gas) wpoint_gas; Logs.newline (); ); @@ -928,7 +929,7 @@ module Base = let reachable' = HM.create (HM.length rho) in let reachable_and_superstable = HM.create (HM.length rho) in let rec one_var' x = - if (not (HM.mem reachable' x)) then ( + if not (HM.mem reachable' x) then ( if HM.mem superstable x then HM.replace reachable_and_superstable x (); HM.replace reachable' x (); Option.may (VS.iter one_var') (HM.find_option dep x); @@ -1047,7 +1048,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; rho; wpoint_gas; stable; side_dep; side_infl; var_messages; rho_write; dep}) end (** TD3 with no hooks. *) diff --git a/tests/regression/56-witness/60-tm-inv-transfer-protection.c b/tests/regression/56-witness/60-tm-inv-transfer-protection.c index 07260adbdd..f6ff78e3ea 100644 --- a/tests/regression/56-witness/60-tm-inv-transfer-protection.c +++ b/tests/regression/56-witness/60-tm-inv-transfer-protection.c @@ -1,4 +1,4 @@ -// PARAM: --set solvers.td3.side_widen always --enable ana.int.interval --set ana.base.privatization protection +// PARAM: --set solvers.td3.side_widen always --set solvers.td3.side_widen_gas 0 --enable ana.int.interval --set ana.base.privatization protection #include #include diff --git a/tests/regression/82-widening_gas/01-side_parallel.c b/tests/regression/82-widening_gas/01-side_parallel.c new file mode 100644 index 0000000000..4053b09fec --- /dev/null +++ b/tests/regression/82-widening_gas/01-side_parallel.c @@ -0,0 +1,47 @@ +// PARAM: --set solvers.td3.side_widen always --set solvers.td3.side_widen_gas 4 --enable ana.int.interval +#include +#include + +int a = 0; +int b = 0; +int c = 0; + +pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER; + +void *increase_to_3(void *arg) { + for(int i = 0; i < 3; i++) { + pthread_mutex_lock(&A); + a = i; + b = i; + c = i; + pthread_mutex_unlock(&A); + } + return NULL; +} + +void *increase_to_4(void *arg) { + for(int i = 0; i < 4; i++) { + pthread_mutex_lock(&A); + b = i; + c = i; + pthread_mutex_unlock(&A); + } + return NULL; +} + +int main(void) { + // don't care about id + pthread_t id; + pthread_create(&id, NULL, increase_to_3, NULL); + pthread_create(&id, NULL, increase_to_4, NULL); + + pthread_mutex_lock(&A); + __goblint_check(a >= 0); + __goblint_check(a <= 3); + + __goblint_check(b >= 0); + __goblint_check(b <= 4); + pthread_mutex_unlock(&A); + + return 0; +} diff --git a/tests/regression/82-widening_gas/02-loop_increment.c b/tests/regression/82-widening_gas/02-loop_increment.c new file mode 100644 index 0000000000..e9149d5274 --- /dev/null +++ b/tests/regression/82-widening_gas/02-loop_increment.c @@ -0,0 +1,14 @@ +// PARAM: --set solvers.td3.widen_gas 5 --enable ana.int.interval +#include + +int main(void) { + int a; + int b; + + for(a = 0; a != 3; a ++) + __goblint_check(a < 3); + for(b = 0; b != 4; b ++) + __goblint_check(b < 4); + + return 0; +} diff --git a/tests/regression/82-widening_gas/03-loop_conditional_side.c b/tests/regression/82-widening_gas/03-loop_conditional_side.c new file mode 100644 index 0000000000..c01e326e2e --- /dev/null +++ b/tests/regression/82-widening_gas/03-loop_conditional_side.c @@ -0,0 +1,22 @@ +// PARAM: --set solvers.td3.widen_gas 11 --enable ana.int.interval --enable exp.earlyglobs +#include +int g = 0; + +int main () { + int i = 0; + // i is widened 11 times: + // [0, 0] -> [0, 1] -> ... -> [0, 10] + loop: + if(i > 11) { + g = 42; + } + + // Exit with '==' condition to prevent narrowing from + // regaining any meaningful information through the loop body. + if (i == 10) + goto end; + i++; + goto loop; + end: + __goblint_check(g != 42); +} diff --git a/tests/regression/82-widening_gas/04-side_simple_update.c b/tests/regression/82-widening_gas/04-side_simple_update.c new file mode 100644 index 0000000000..9ffe665d2f --- /dev/null +++ b/tests/regression/82-widening_gas/04-side_simple_update.c @@ -0,0 +1,34 @@ +// PARAM: --set solvers.td3.side_widen always --set solvers.td3.side_widen_gas 3 --enable ana.int.interval --enable exp.earlyglobs +#include +#include + +int a = 0; +int b = 0; +int c = 0; + +pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER; + +void *thread(void *arg) { + pthread_mutex_lock(&A); + a = 1; + b = 1; + b = 2; + c = 1; + c = 2; + c = 3; + pthread_mutex_unlock(&A); + return NULL; +} + +int main(void) { + // don't care about id + pthread_t id; + pthread_create(&id, NULL, thread, NULL); + + pthread_mutex_lock(&A); + __goblint_check(a <= 1); + __goblint_check(b <= 2); + __goblint_check(c <= 3); + pthread_mutex_unlock(&A); + return 0; +} diff --git a/tests/regression/82-widening_gas/05-side_and_no_side.c b/tests/regression/82-widening_gas/05-side_and_no_side.c new file mode 100644 index 0000000000..cad2ee0287 --- /dev/null +++ b/tests/regression/82-widening_gas/05-side_and_no_side.c @@ -0,0 +1,32 @@ +// PARAM: --set solvers.td3.side_widen always --set solvers.td3.side_widen_gas 3 --set solvers.td3.widen_gas 4 --enable ana.int.interval +#include +#include + +int a = 0; + +pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER; + +void *thread(void *arg) { + // i: [0, 0] -> [0, 1] -> [0, 2] -> [0, 3] + // a: [0, 0] -> [0, 1] -> [0, 2] + for(int i = 0; i != 3; i++) { + pthread_mutex_lock(&A); + a = i; + pthread_mutex_unlock(&A); + } + return NULL; +} + +int main(void) { + // don't care about id + pthread_t id; + pthread_create(&id, NULL, thread, NULL); + + pthread_mutex_lock(&A); + __goblint_check(a >= 0); + __goblint_check(a <= 2); + pthread_mutex_unlock(&A); + + return 0; +} + diff --git a/tests/regression/82-widening_gas/06-post_loop1.c b/tests/regression/82-widening_gas/06-post_loop1.c new file mode 100644 index 0000000000..19feae0c05 --- /dev/null +++ b/tests/regression/82-widening_gas/06-post_loop1.c @@ -0,0 +1,20 @@ +// PARAM: --set solvers.td3.widen_gas 6 --enable ana.int.interval +#include + +int main(void) { + int a; + int b = 0; + + for(a = 0; a < 5; a ++) { + b = b < a ? a : b; + // widening gas cannot help here: + // b += a; + // even though the interval of a eventually stabilizes at [0, 4], + // we are not tracking the number of possible iterations. + // Hence, the interval of b keeps growing, as it can be + // increased by 4 each iteration. + } + __goblint_check(b < 5); + + return 0; +} diff --git a/tests/regression/82-widening_gas/07-post_loop2.c b/tests/regression/82-widening_gas/07-post_loop2.c new file mode 100644 index 0000000000..946736dcd8 --- /dev/null +++ b/tests/regression/82-widening_gas/07-post_loop2.c @@ -0,0 +1,17 @@ +// PARAM: --set solvers.td3.widen_gas 5 --enable ana.int.interval --enable exp.no-narrow +#include + +int main(void) { + // represents non-deterministic value + int unknown; + int a = unknown > 9 ? 9 : (unknown < -9 ? -9 : unknown); + + while (-10 < a && a < 10) { + a = -2 * (a - 1); + } + + __goblint_check(-16 <= a); + __goblint_check(a <= 20); + + return 0; +} diff --git a/tests/regression/82-widening_gas/08-semaphore.c b/tests/regression/82-widening_gas/08-semaphore.c new file mode 100644 index 0000000000..4d0fa7c572 --- /dev/null +++ b/tests/regression/82-widening_gas/08-semaphore.c @@ -0,0 +1,60 @@ +// PARAM: --set solvers.td3.side_widen_gas 10 --enable ana.int.interval +#include +#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 < 0x1000) { + abort(); + } + 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) { + pthread_t id; + semaphore_t sem; + semaphor_init(&sem, 10); + + pthread_create(&id, NULL, worker, &sem); + pthread_create(&id, NULL, worker, &sem); + + pthread_mutex_lock(&sem.mutex); + __goblint_check(sem.count >= 0); + pthread_mutex_unlock(&sem.mutex); + return 0; +}