Merge pull request #1636 from Red-Panda64/feature/divide-and-narrow

Narrowing of globals in TD

Author: michael-schwarz

src/analyses/basePriv.ml

@@ -866,6 +866,47 @@ sig
   include AtomicParam
 end
 
+module P =
+struct
+  include MustVars
+  let name () = "P"
+end
+
+module Sigma' =
+struct
+  include CPA
+  let name () = "Protected Changes"
+end
+
+module type ProtectionDom =
+sig
+  include Lattice.S
+  val add: bool -> varinfo -> VD.t -> t -> t
+  val remove: varinfo -> t -> t
+  val precise_side: varinfo -> VD.t -> t -> VD.t option
+  val empty: unit -> t
+  val getP: t -> P.t
+end
+
+module ProtectionCPASide: ProtectionDom =
+struct
+  include P
+
+  let add _ x _ t = P.add x t
+  let precise_side x v t = Some v
+  let getP t = t
+end
+
+module ProtectionChangesOnlySide: ProtectionDom =
+struct
+  include Lattice.Prod (P) (Sigma')
+  let add invariant x v t = P.add x @@ fst t, if not invariant then Sigma'.add x v @@ snd t else snd t
+  let remove x t = P.remove x @@ fst t, Sigma'.remove x @@ snd t
+  let precise_side x v t = Sigma'.find_opt x @@ snd t
+  let empty () = P.empty (), Sigma'.empty ()
+  let getP t = fst t
+end
+
 (** Protection-Based Reading. *)
 module ProtectionBasedV = struct
   module VUnprot =
@@ -887,30 +928,24 @@ module ProtectionBasedV = struct
 end
 
 (** Protection-Based Reading. *)
-module ProtectionBasedPriv (Param: PerGlobalPrivParam)(Wrapper:PrivatizationWrapper): S =
+module ProtectionBasedPriv (D: ProtectionDom) (Param: PerGlobalPrivParam)(Wrapper:PrivatizationWrapper): S =
 struct
   include NoFinalize
   include ConfCheck.RequireMutexActivatedInit
   open Protection
 
-  module P =
-  struct
-    include MustVars
-    let name () = "P"
-  end
-
   (* W is implicitly represented by CPA domain *)
-  module D = P
+  module D = D
 
   module Wrapper = Wrapper (VD)
   module G = Wrapper.G
   module V = ProtectionBasedV.V
 
-  let startstate () = P.empty ()
+  let startstate () = D.empty ()
 
   let read_global (ask: Queries.ask) getg (st: BaseComponents (D).t) x =
     let getg = Wrapper.getg ask getg in
-    if P.mem x st.priv then
+    if P.mem x @@ D.getP st.priv then
       CPA.find x st.cpa
     else if Param.handle_atomic && ask.f MustBeAtomic then
       VD.join (CPA.find x st.cpa) (getg (V.unprotected x)) (* Account for previous unpublished unprotected writes in current atomic section. *)
@@ -921,6 +956,7 @@ struct
 
   let write_global ?(invariant=false) (ask: Queries.ask) getg sideg (st: BaseComponents (D).t) x v =
     let sideg = Wrapper.sideg ask sideg in
+    let unprotected = is_unprotected ask x in
     if not invariant then (
       if not (Param.handle_atomic && ask.f MustBeAtomic) then
         sideg (V.unprotected x) v; (* Delay publishing unprotected write in the atomic section. *)
@@ -929,11 +965,11 @@ struct
         (* Unlock after invariant will still side effect refined value (if protected) from CPA, because cannot distinguish from non-invariant write since W is implicit. *)
     );
     if Param.handle_atomic && ask.f MustBeAtomic then
-      {st with cpa = CPA.add x v st.cpa; priv = P.add x st.priv} (* Keep write local as if it were protected by the atomic section. *)
-    else if is_unprotected ask x then
+      {st with cpa = CPA.add x v st.cpa; priv = D.add invariant x v st.priv} (* Keep write local as if it were protected by the atomic section. *)
+    else if unprotected then
       st
     else
-      {st with cpa = CPA.add x v st.cpa; priv = P.add x st.priv}
+      {st with cpa = CPA.add x v st.cpa; priv = D.add invariant x v st.priv}
 
   let lock ask getg st m = st
 
@@ -943,16 +979,22 @@ struct
     (* TODO: what about G_m globals in cpa that weren't actually written? *)
     CPA.fold (fun x v (st: BaseComponents (D).t) ->
         if is_protected_by ask m x then ( (* is_in_Gm *)
-          (* Extra precision in implementation to pass tests:
-             If global is read-protected by multiple locks,
-             then inner unlock shouldn't yet publish. *)
-          if not Param.check_read_unprotected || is_unprotected_without ask ~write:false x m then
-            sideg (V.protected x) v;
-          if atomic then
-            sideg (V.unprotected x) v; (* Publish delayed unprotected write as if it were protected by the atomic section. *)
-
+          (* Only apply sides for values that were actually written to globals!
+             This excludes invariants inferred through guards. *)
+          begin match D.precise_side x v st.priv with
+            | Some v -> begin
+                (* Extra precision in implementation to pass tests:
+                   If global is read-protected by multiple locks,
+                   then inner unlock shouldn't yet publish. *)
+                if not Param.check_read_unprotected || is_unprotected_without ask ~write:false x m then
+                  sideg (V.protected x) v;
+                if atomic then
+                  sideg (V.unprotected x) v; (* Publish delayed unprotected write as if it were protected by the atomic section. *)
+              end
+            | None -> ()
+          end;
           if is_unprotected_without ask x m then (* is_in_V' *)
-            {st with cpa = CPA.remove x st.cpa; priv = P.remove x st.priv}
+            {st with cpa = CPA.remove x st.cpa; priv = D.remove x st.priv}
           else
             st
         )
@@ -968,7 +1010,7 @@ struct
           if is_global ask x && is_unprotected ask x then (
             sideg (V.unprotected x) v;
             sideg (V.protected x) v; (* must be like enter_multithreaded *)
-            {st with cpa = CPA.remove x st.cpa; priv = P.remove x st.priv}
+            {st with cpa = CPA.remove x st.cpa; priv = D.remove x st.priv}
           )
           else
             st
@@ -1007,7 +1049,7 @@ struct
         if is_global ask x then (
           sideg (V.unprotected x) v;
           sideg (V.protected x) v;
-          {st with cpa = CPA.remove x st.cpa; priv = P.remove x st.priv}
+          {st with cpa = CPA.remove x st.cpa; priv = D.remove x st.priv}
         )
         else
           st
@@ -2116,19 +2158,21 @@ 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)
         | "vojdani" -> (module VojdaniPriv: 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" -> (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))

src/config/options.schema.json

@@ -790,6 +790,20 @@
               "title": "ana.base.priv",
               "type": "object",
               "properties": {
+                "protection": {
+                  "title": "ana.base.priv.protection",
+                  "description": "Options for protection based privatization schemes.",
+                  "type": "object",
+                  "properties": {
+                    "changes-only": {
+                      "title": "ana.base.priv.protection.changes-only",
+                      "description": "Only propagate changes to globals on unlock, don't side the full value of the privatized global.",
+                      "type": "boolean",
+                      "default": false
+                    }
+                  },
+                  "additionalProperties": false
+                },
                 "not-started": {
                   "title": "ana.base.priv.not-started",
                   "description":
@@ -2526,6 +2540,43 @@
               "type": "boolean",
               "default": true
             },
+            "narrow-globs": {
+              "title": "solvers.td3.narrow-globs",
+              "type": "object",
+              "properties": {
+                "enabled": {
+                  "title": "solvers.td3.narrow-globs.enabled",
+                  "description": "Individually track side-effects from different unknowns to enable narrowing of globals.",
+                  "type": "boolean",
+                  "default": false
+                },
+                "conservative-widen": {
+                  "title": "solvers.td3.narrow-globs.conservative-widen",
+                  "description": "Controls when to widen divided sides. true: Only widen on a side-effect, if joining would affect the overall value of the global. false: Always widen increasing/incomparable side-effects",
+                  "type": "boolean",
+                  "default": true
+                },
+                "immediate-growth": {
+                  "title": "solvers.td3.narrow-globs.immediate-growth",
+                  "description": "Controls when growing side-effects are applied. true: immediately when they are triggered. false: after the source unknown has been fully evaluated",
+                  "type": "boolean",
+                  "default": true
+                },
+                "narrow-gas": {
+                  "title": "solvers.td3.narrow-globs.narrow-gas",
+                  "description": "Limits the number of times a side-effect can switch from widening to narrowing to enforce termination. 0 disables narrowing, -1 allows narrowing infinitely often.",
+                  "type": "integer",
+                  "default": 5
+                },
+                "eliminate-dead": {
+                  "title": "solvers.td3.narrow-globs.eliminate-dead",
+                  "description": "side-effects that no longer occur are narrowed with bot.",
+                  "type": "boolean",
+                  "default": false
+                }
+              },
+              "additionalProperties": false
+            },
             "remove-wpoint": {
               "title": "solvers.td3.remove-wpoint",
               "description": "Remove widening points after narrowing phase. Enables a form of local restarting which increases precision of nested loops.",

src/constraint/constrSys.ml

@@ -46,8 +46,12 @@ sig
   (** The system in functional form. *)
   val system : v -> ((v -> d) -> (v -> d -> unit) -> d) m
 
-  val sys_change: (v -> d) -> v sys_change_info
   (** Compute incremental constraint system change from old solution. *)
+  val sys_change: (v -> d) -> v sys_change_info
+
+  (** List of unknowns that should be queried again when the argument unknown has shrunk to bot, to eagerly trigger (analysis-time!) abstract garbage collection idependently of reach-based pruning at the end.
+      @see <https://arxiv.org/abs/2504.06026> Stemmler, F., Schwarz, M., Erhard, J., Tilscher, S., Seidl, H. Taking out the Toxic Trash: Recovering Precision in Mixed Flow-Sensitive Static Analyses *)
+  val postmortem: v -> v list
 end
 
 (** Any system of side-effecting equations over lattices. *)
@@ -64,6 +68,7 @@ sig
   val system : LVar.t -> ((LVar.t -> D.t) -> (LVar.t -> D.t -> unit) -> (GVar.t -> G.t) -> (GVar.t -> G.t -> unit) -> D.t) option
   val iter_vars: (LVar.t -> D.t) -> (GVar.t -> G.t) -> VarQuery.t -> LVar.t VarQuery.f -> GVar.t VarQuery.f -> unit
   val sys_change: (LVar.t -> D.t) -> (GVar.t -> G.t) -> [`L of LVar.t | `G of GVar.t] sys_change_info
+  val postmortem: LVar.t -> LVar.t list
 end
 
 (** A solver is something that can translate a system into a solution (hash-table).
@@ -205,6 +210,10 @@ struct
 
   let sys_change get =
     S.sys_change (getL % get % l) (getG % get % g)
+
+  let postmortem = function
+    | `L g -> List.map (fun x -> `L x) @@ S.postmortem g
+    | _ -> []
 end
 
 (** Splits a [EqConstrSys] solution into a [GlobConstrSys] solution with given [Hashtbl.S] for the [EqConstrSys]. *)

src/framework/constraints.ml

@@ -549,4 +549,8 @@ struct
     in
 
     {obsolete; delete; reluctant; restart}
+
+  let postmortem = function
+    | FunctionEntry fd, c -> [(Function fd, c)]
+    | _ -> []
 end

src/maingoblint.ml

@@ -141,6 +141,8 @@ let check_arguments () =
   if get_bool "ana.base.context.int" && not (get_bool "ana.base.context.non-ptr") then (set_bool "ana.base.context.int" false; warn "ana.base.context.int implicitly disabled by ana.base.context.non-ptr");
   (* order matters: non-ptr=false, int=true -> int=false cascades to interval=false with warning *)
   if get_bool "ana.base.context.interval" && not (get_bool "ana.base.context.int") then (set_bool "ana.base.context.interval" false; warn "ana.base.context.interval implicitly disabled by ana.base.context.int");
+  if get_bool "ana.base.priv.protection.changes-only" && not @@ List.mem (get_string "ana.base.privatization") ["protection"; "protection-tid"; "protection-atomic"; "protection-read"; "protection-read-tid"; "protection-read-atomic"] then
+    warn "ana.base.priv.protection.changes-only requires ana.base.privatization to be protection based";
   if get_bool "incremental.only-rename" then (set_bool "incremental.load" true; warn "incremental.only-rename implicitly activates incremental.load. Previous AST is loaded for diff and rename, but analyis results are not reused.");
   if get_bool "incremental.restart.sided.enabled" && get_string_list "incremental.restart.list" <> [] then warn "Passing a non-empty list to incremental.restart.list (manual restarting) while incremental.restart.sided.enabled (automatic restarting) is activated.";
   if get_bool "ana.autotune.enabled" && get_bool "incremental.load" then (set_bool "ana.autotune.enabled" false; warn "ana.autotune.enabled implicitly disabled by incremental.load");
@@ -164,6 +166,10 @@ let check_arguments () =
   );
   if get_bool "solvers.td3.space" && get_bool "solvers.td3.remove-wpoint" then fail "solvers.td3.space is incompatible with solvers.td3.remove-wpoint";
   if get_bool "solvers.td3.space" && get_string "solvers.td3.side_widen" = "sides-local" then fail "solvers.td3.space is incompatible with solvers.td3.side_widen = 'sides-local'";
+  if get_bool "solvers.td3.space" && get_bool "solvers.td3.narrow-globs.enabled" then fail "solvers.td3.space is incompatible with solvers.td3.narrow-globs.enabled";
+  if (get_bool "incremental.load" || get_bool "incremental.save") && get_bool "solvers.td3.narrow-globs.enabled" then (
+    fail "solvers.td3.space is incompatible with incremental analsyis.";
+  );
   if List.mem "termination" @@ get_string_list "ana.activated" then (
     if GobConfig.get_bool "incremental.load" || GobConfig.get_bool "incremental.save" then fail "termination analysis is not compatible with incremental analysis";
     set_list "ana.activated" (GobConfig.get_list "ana.activated" @ [`String ("threadflag")]);

src/solver/goblint_solver.ml

@@ -32,3 +32,4 @@ module SolverStats = SolverStats
 module SolverBox = SolverBox
 
 module SideWPointSelect = SideWPointSelect
+module Td3UpdateRule = Td3UpdateRule