Merge branch 'master' into affineeq-refine

Author: DrMichaelPetter

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
+  }
+}

docs/artifact-descriptions/vmcai25.md

@@ -96,14 +96,14 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
-# pin-depends: [
-  # published goblint-cil 2.0.5 is currently up-to-date, so no pin needed
-  # [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd" ]
+pin-depends: [
+  # published goblint-cil 2.0.5 is currently up-to-date, but pinned for reproducibility
+  [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new camlidl release
-  # [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ]
+  [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
-  # [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
-# ]
+  [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
+]
 depexts: [
   ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
 ]

goblint.opam

@@ -137,6 +137,20 @@ conflicts: [
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]
+pin-depends: [
+  [
+    "goblint-cil.2.0.5"
+    "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd"
+  ]
+  [
+    "camlidl.1.12"
+    "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0"
+  ]
+  [
+    "apron.v0.9.15"
+    "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a"
+  ]
+]
 depexts: ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
 description: """\
 Goblint is a sound static analysis framework for C programs using abstract interpretation.

goblint.opam.locked

@@ -1,14 +1,14 @@
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
-# pin-depends: [
-  # published goblint-cil 2.0.5 is currently up-to-date, so no pin needed
-  # [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd" ]
+pin-depends: [
+  # published goblint-cil 2.0.5 is currently up-to-date, but pinned for reproducibility
+  [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new camlidl release
-  # [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ]
+  [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
-  # [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
-# ]
+  [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
+]
 depexts: [
   ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
 ]

goblint.opam.template

@@ -41,3 +41,4 @@ nav:
     - "🇸 SAS '21": artifact-descriptions/sas21.md
     - "🇪 ESOP '23": artifact-descriptions/esop23.md
     - "🇻 VMCAI '24": artifact-descriptions/vmcai24.md
+    - "🇻 VMCAI '25": artifact-descriptions/vmcai25.md

gobview

@@ -48,6 +48,13 @@
 
     "MessageCategory", # included in Messages
     "PreValueDomain", # included in ValueDomain
+    "IntervalDomain", # included in IntDomain
+    "IntervalSetDomain", # included in IntDomain
+    "DefExcDomain", # included in IntDomain
+    "EnumsDomain", # included in IntDomain
+    "CongruenceDomain", # included in IntDomain
+    "IntDomTuple", # included in IntDomain
+    "WitnessGhostVar", # included in WitnessGhost
 
     "ConfigVersion",
     "ConfigProfile",

mkdocs.yml

@@ -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
 
 

scripts/goblint-lib-modules.py

@@ -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) ->