Generate flow-insensitive YAML witness invariants with ghosts for privatized variables

conf/svcomp-ghost.json

@@ -0,0 +1,139 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless",
+      "mutexGhosts",
+      "pthreadMutexType"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      },
+      "invariant": {
+        "local": false,
+        "global": true
+      }
+    },
+    "relation": {
+      "invariant": {
+        "local": false,
+        "global": true,
+        "one-var": false
+      }
+    },
+    "apron": {
+      "invariant": {
+        "diff-box": true
+      }
+    },
+    "var_eq": {
+      "invariant": {
+        "enabled": false
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.1",
+      "entry-types": [
+        "flow_insensitive_invariant",
+        "ghost_instrumentation"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": true,
+      "other": true,
+      "accessed": false,
+      "exact": true,
+      "all-locals": false,
+      "flow_insensitive-as": "invariant_set-location_invariant"
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}

scripts/goblint-lib-modules.py

@@ -48,6 +48,7 @@
 
     "MessageCategory", # included in Messages
     "PreValueDomain", # included in ValueDomain
+    "WitnessGhostVar", # included in WitnessGhost
 
     "ConfigVersion",
     "ConfigProfile",

src/analyses/apron/relationAnalysis.apron.ml

@@ -634,6 +634,15 @@ struct
       )
     |> Enum.fold (fun acc x -> Invariant.(acc && of_exp x)) Invariant.none
 
+  let query_invariant_global ctx g =
+    if GobConfig.get_bool "ana.relation.invariant.global" && ctx.ask (GhostVarAvailable Multithreaded) then (
+      let var = WitnessGhost.to_varinfo Multithreaded in
+      let inv = Priv.invariant_global (Analyses.ask_of_ctx ctx) ctx.global g in
+      Invariant.(of_exp (UnOp (LNot, Lval (GoblintCil.var var), GoblintCil.intType)) || inv) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
+    )
+    else
+      Invariant.none
+
   let query ctx (type a) (q: a Queries.t): a Queries.result =
     let open Queries in
     let st = ctx.local in
@@ -655,6 +664,9 @@ struct
       let vf' x = vf (Obj.repr x) in
       Priv.iter_sys_vars ctx.global vq vf'
     | Queries.Invariant context -> query_invariant ctx context
+    | Queries.InvariantGlobal g ->
+      let g: V.t = Obj.obj g in
+      query_invariant_global ctx g
     | _ -> Result.top q
 
 

src/analyses/apron/relationPriv.apron.ml

@@ -46,6 +46,9 @@ module type S =
     val thread_return: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> ThreadIdDomain.Thread.t -> relation_components_t -> relation_components_t
     val iter_sys_vars: (V.t -> G.t) -> VarQuery.t -> V.t VarQuery.f -> unit (** [Queries.IterSysVars] for apron. *)
 
+    val invariant_global: Q.ask -> (V.t -> G.t) -> V.t -> Invariant.t
+    (** Returns flow-insensitive invariant for global unknown. *)
+
     val invariant_vars: Q.ask -> (V.t -> G.t) -> relation_components_t -> varinfo list
     (** Returns global variables which are privatized. *)
 
@@ -137,6 +140,7 @@ struct
     {rel = RD.top (); priv = startstate ()}
 
   let iter_sys_vars getg vq vf = ()
+  let invariant_global ask getg g = Invariant.none
   let invariant_vars ask getg st = []
 
   let init () = ()
@@ -424,6 +428,7 @@ struct
     {rel = getg (); priv = startstate ()}
 
   let iter_sys_vars getg vq vf = () (* TODO: or report singleton global for any Global query? *)
+  let invariant_global ask getg g = Invariant.none
   let invariant_vars ask getg st = protected_vars ask (* TODO: is this right? *)
 
   let finalize () = ()
@@ -708,6 +713,41 @@ struct
 
   let init () = ()
   let finalize () = ()
+
+  let invariant_global (ask: Q.ask) (getg: V.t -> G.t): V.t -> Invariant.t = function
+    | `Left m' -> (* mutex *)
+      let atomic = LockDomain.MustLock.equal m' (LockDomain.MustLock.of_var LibraryFunctions.verifier_atomic_var) in
+      if atomic || ask.f (GhostVarAvailable (Locked m')) then (
+        (* filters like query_invariant *)
+        let one_var = GobConfig.get_bool "ana.relation.invariant.one-var" in
+        let exact = GobConfig.get_bool "witness.invariant.exact" in
+
+        let rel = keep_only_protected_globals ask m' (get_m_with_mutex_inits ask getg m') in (* Could be more precise if mutex_inits invariant is added by disjunction instead of joining abstract values. *)
+        let inv =
+          RD.invariant rel
+          |> List.enum
+          |> Enum.filter_map (fun (lincons1: Apron.Lincons1.t) ->
+              (* filter one-vars and exact *)
+              (* TODO: exact filtering doesn't really work with octagon because it returns two SUPEQ constraints instead *)
+              if (one_var || GobApron.Lincons1.num_vars lincons1 >= 2) && (exact || Apron.Lincons1.get_typ lincons1 <> EQ) then
+                RD.cil_exp_of_lincons1 lincons1
+                |> Option.filter (fun exp -> not (InvariantCil.exp_contains_tmp exp))
+              else
+                None
+            )
+          |> Enum.fold (fun acc x -> Invariant.(acc && of_exp x)) Invariant.none
+        in
+        if atomic then
+          inv
+        else (
+          let var = WitnessGhost.to_varinfo (Locked m') in
+          Invariant.(of_exp (Lval (GoblintCil.var var)) || inv) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
+        )
+      )
+      else
+        Invariant.none
+    | g -> (* global *)
+      Invariant.none (* Could output unprotected one-variable (so non-relational) invariants, but probably not very useful. [BasePriv] does those anyway. *)
 end
 
 (** May written variables. *)
@@ -1275,6 +1315,8 @@ struct
     | _ -> ()
 
   let finalize () = ()
+
+  let invariant_global ask getg g = Invariant.none
 end
 
 module TracingPriv = functor (Priv: S) -> functor (RD: RelationDomain.RD) ->

src/analyses/base.ml

@@ -1181,6 +1181,9 @@ struct
     not is_alloc || (is_alloc && not (ctx.ask (Queries.IsHeapVar v)))
 
   let query_invariant ctx context =
+    let keep_local = GobConfig.get_bool "ana.base.invariant.local" in
+    let keep_global = GobConfig.get_bool "ana.base.invariant.global" in
+
     let cpa = ctx.local.BaseDomain.cpa in
     let ask = Analyses.ask_of_ctx ctx in
 
@@ -1193,6 +1196,13 @@ struct
     in
     let module I = ValueDomain.ValueInvariant (Arg) in
 
+    let var_filter v =
+      if is_global ask v then
+        keep_global
+      else
+        keep_local
+    in
+
     let var_invariant ?offset v =
       if not (InvariantCil.var_is_heap v) then
         I.key_invariant v ?offset (Arg.find v)
@@ -1203,14 +1213,23 @@ struct
     if Lval.Set.is_top context.Invariant.lvals then (
       if !earlyglobs || ThreadFlag.has_ever_been_multi ask then (
         let cpa_invariant =
-          CPA.fold (fun k v a ->
-              if not (is_global ask k) then
-                Invariant.(a && var_invariant k)
-              else
-                a
-            ) cpa Invariant.none
+          if keep_local then (
+            CPA.fold (fun k v a ->
+                if not (is_global ask k) then
+                  Invariant.(a && var_invariant k)
+                else
+                  a
+              ) cpa Invariant.none
+          )
+          else
+            Invariant.none
+        in
+        let priv_vars =
+          if keep_global then
+            Priv.invariant_vars ask (priv_getg ctx.global) ctx.local
+          else
+            []
         in
-        let priv_vars = Priv.invariant_vars ask (priv_getg ctx.global) ctx.local in
         let priv_invariant =
           List.fold_left (fun acc v ->
               Invariant.(var_invariant v && acc)
@@ -1220,15 +1239,18 @@ struct
       )
       else (
         CPA.fold (fun k v a ->
-            Invariant.(a && var_invariant k)
+            if var_filter k then
+              Invariant.(a && var_invariant k)
+            else
+              a
           ) cpa Invariant.none
       )
     )
     else (
       Lval.Set.fold (fun k a ->
           let i =
             match k with
-            | (Var v, offset) when not (InvariantCil.var_is_heap v) ->
+            | (Var v, offset) when var_filter v && not (InvariantCil.var_is_heap v) ->
               (try I.key_invariant_lval v ~offset ~lval:k (Arg.find v) with Not_found -> Invariant.none)
             | _ -> Invariant.none
           in
@@ -1243,13 +1265,23 @@ struct
       Invariant.none
 
   let query_invariant_global ctx g =
-    if GobConfig.get_bool "ana.base.invariant.enabled" && get_bool "exp.earlyglobs" then (
+    if GobConfig.get_bool "ana.base.invariant.enabled" && GobConfig.get_bool "ana.base.invariant.global" then (
       (* Currently these global invariants are only sound with earlyglobs enabled for both single- and multi-threaded programs.
-         Otherwise, the values of globals in single-threaded mode are not accounted for. *)
-      (* TODO: account for single-threaded values without earlyglobs. *)
+         Otherwise, the values of globals in single-threaded mode are not accounted for.
+         They are also made sound without earlyglobs using the multithreaded mode ghost variable. *)
       match g with
       | `Left g' -> (* priv *)
-        Priv.invariant_global (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) g'
+        let inv = Priv.invariant_global (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) g' in
+        if get_bool "exp.earlyglobs" then
+          inv
+        else (
+          if ctx.ask (GhostVarAvailable Multithreaded) then (
+            let var = WitnessGhost.to_varinfo Multithreaded in
+            Invariant.(of_exp (UnOp (LNot, Lval (GoblintCil.var var), GoblintCil.intType)) || inv) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
+          )
+          else
+            Invariant.none
+        )
       | `Right _ -> (* thread return *)
         Invariant.none
     )