Merge branch 'master' into unboxed

conf/ldv-races.json

@@ -29,7 +29,9 @@
       "escape",
       "expRelation",
       "mhp",
-      "assert"
+      "assert",
+      "var_eq",
+      "symb_locks"
     ],
     "malloc": {
       "wrappers": [
@@ -52,6 +54,19 @@
       ]
     }
   },
+  "lib": {
+    "activated": [
+      "c",
+      "posix",
+      "pthread",
+      "gcc",
+      "glibc",
+      "linux-userspace",
+      "goblint",
+      "ncurses",
+      "klever"
+    ]
+  },
   "witness": {
     "graphml": {
       "enabled": true,

conf/min-unsound.json

@@ -0,0 +1,6 @@
+{
+    "ana": {
+        "activated": [
+        ]
+    }
+}

docs/developer-guide/debugging.md

@@ -60,14 +60,14 @@ This will create a file called `goblint.byte`.
 ### Debugging Goblint with VS Code
 
 To debug OCaml programs, you can use the command line interface of `ocamldebug` or make use of the Visual Studio Code
-integration provided by `hackwaly.ocamlearlybird`.
+integration provided by `ocamllabs.ocaml-platform`.
 In the following, we describe the steps necessary to set up this VS Code extension to
 debug Goblint.
 
 ### Setting-up Earlybird
 
-Install the [`hackwaly.ocamlearlybird` extension](https://marketplace.visualstudio.com/items?itemName=hackwaly.ocamlearlybird) in your installation of Visual Studio Code.
-To be able to use this extension, you additionally need to install `ocamlearlybird` on the opam switch you use for Goblint.
+Install the [`ocamllabs.ocaml-platform` extension](https://marketplace.visualstudio.com/items?itemName=ocamllabs.ocaml-platform) in your installation of Visual Studio Code.
+To be able to use this extension, you additionally need to install `earlybird` on the opam switch you use for Goblint.
 To do so, run the following command in the `analyzer` directory:
 
 ```console
@@ -76,7 +76,7 @@ opam install earlybird
 
 ### Providing a Launch Configuration
 
-To let the `hackwaly.ocamlearlybird` extension know which executable it should debug, and which arguments it should pass, we have to provide a configuration file.
+To let the `ocamllabs.ocaml-platform` extension know which executable it should debug, and which arguments it should pass, we have to provide a configuration file.
 The configuration file has to be named `launch.json` and must reside in the `./.vscode` directory. Here is an example `launch.json`:
 
 ```JSON
@@ -92,6 +92,9 @@ The configuration file has to be named `launch.json` and must reside in the `./.
           "tests/regression/00-sanity/01-assert.c",
           "--enable", "ana.int.interval",
         ],
+        "env": {
+          "LD_LIBRARY_PATH": "$LD_LIBRARY_PATH:_build/default/src/common"
+        },
         "stopOnEntry": false,
       }
     ]

docs/developer-guide/messaging.md

@@ -18,7 +18,8 @@ A message consists of the following:
         3. **Context.** Optional. Currently completely abstract, so not very useful.
     * **Group.** For messages related to numerous locations with different texts. Contains the following:
         1. **Group text.** An overall description of the group message.
-        2. **Pieces.** A list of single messages as described above.
+        2. **Group location.** Optional. An overall location of the group message.
+        3. **Pieces.** A list of single messages as described above.
 
 ## Creating
 

dune-project

@@ -16,7 +16,7 @@
 (homepage "https://goblint.in.tum.de")
 (documentation "https://goblint.readthedocs.io/en/latest/")
 (authors "Simmo Saan" "Michael Schwarz" "Julian Erhard" "Sarah Tilscher" "Ralf Vogler" "Kalmer Apinis" "Vesal Vojdani" ) ; same authors as in .zenodo.json and CITATION.cff
-(maintainers "Simmo Saan <[email protected]>" "Michael Schwarz <[email protected]>")
+(maintainers "Simmo Saan <[email protected]>" "Michael Schwarz <[email protected]>" "Karoliine Holter")
 (license MIT)
 
 (package

goblint.opam

@@ -4,6 +4,7 @@ synopsis: "Static analysis framework for C"
 maintainer: [
   "Simmo Saan <[email protected]>"
   "Michael Schwarz <[email protected]>"
+  "Karoliine Holter"
 ]
 authors: [
   "Simmo Saan"

goblint.opam.locked

@@ -5,6 +5,7 @@ synopsis: "Static analysis framework for C"
 maintainer: [
   "Simmo Saan <[email protected]>"
   "Michael Schwarz <[email protected]>"
+  "Karoliine Holter"
 ]
 authors: [
   "Simmo Saan"

scripts/goblint-lib-modules.py

@@ -8,6 +8,7 @@
 
 goblint_lib_paths = [
     src_root_path / "goblint_lib.ml",
+    src_root_path / "solver" / "goblint_solver.ml",
     src_root_path / "util" / "std" / "goblint_std.ml",
 ]
 goblint_lib_modules = set()
@@ -33,6 +34,7 @@
 
     # libraries
     "Goblint_std",
+    "Goblint_solver",
     "Goblint_timing",
     "Goblint_backtrace",
     "Goblint_tracing",
@@ -63,5 +65,5 @@
 
 missing_modules = src_modules - goblint_lib_modules
 if len(missing_modules) > 0:
-    print(f"Modules missing from {goblint_lib_path}: {missing_modules}")
+    print(f"Modules missing from {goblint_lib_paths[0]}: {missing_modules}")
     sys.exit(1)

src/analyses/apron/relationPriv.apron.ml

@@ -843,7 +843,7 @@ struct
 end
 
 (** Per-mutex meet with TIDs. *)
-module PerMutexMeetPrivTID (Cluster: ClusterArg): S  = functor (RD: RelationDomain.RD) ->
+module PerMutexMeetPrivTID (Digest: Digest) (Cluster: ClusterArg): S  = functor (RD: RelationDomain.RD) ->
 struct
   open CommonPerMutex(RD)
   include MutexGlobals
@@ -853,21 +853,17 @@ struct
   module Cluster = NC
   module LRD = NC.LRD
 
-  include PerMutexTidCommon(struct
-      let exclude_not_started () = GobConfig.get_bool "ana.relation.priv.not-started"
-      let exclude_must_joined () = GobConfig.get_bool "ana.relation.priv.must-joined"
-    end)(LRD)
+  include PerMutexTidCommon (Digest) (LRD)
 
   module AV = RD.V
   module P = UnitP
 
   let name () = "PerMutexMeetPrivTID(" ^ (Cluster.name ()) ^ (if GobConfig.get_bool "ana.relation.priv.must-joined" then  ",join"  else "") ^ ")"
 
   let get_relevant_writes (ask:Q.ask) m v =
-    let current = ThreadId.get_current ask in
-    let must_joined = ask.f Queries.MustJoinedThreads in
+    let current = Digest.current ask in
     GMutex.fold (fun k v acc ->
-        if compatible ask current must_joined k then
+        if not (Digest.accounted_for ask ~current ~other:k) then
           LRD.join acc (Cluster.keep_only_protected_globals ask m v)
         else
           acc
@@ -945,8 +941,8 @@ struct
     (* unlock *)
     let rel_side = RD.keep_vars rel_local [g_var] in
     let rel_side = Cluster.unlock (W.singleton g) rel_side in
-    let tid = ThreadId.get_current ask in
-    let sidev = GMutex.singleton tid rel_side in
+    let digest = Digest.current ask in
+    let sidev = GMutex.singleton digest rel_side in
     sideg (V.global g) (G.create_global sidev);
     let l' = L.add lm rel_side l in
     let rel_local' =
@@ -983,8 +979,8 @@ struct
     else
       let rel_side = keep_only_protected_globals ask m rel in
       let rel_side = Cluster.unlock w rel_side in
-      let tid = ThreadId.get_current ask in
-      let sidev = GMutex.singleton tid rel_side in
+      let digest = Digest.current ask in
+      let sidev = GMutex.singleton digest rel_side in
       sideg (V.mutex m) (G.create_mutex sidev);
       let lm = LLock.mutex m in
       let l' = L.add lm rel_side l in
@@ -1068,8 +1064,8 @@ struct
     in
     let rel_side = RD.keep_vars rel g_vars in
     let rel_side = Cluster.unlock (W.top ()) rel_side in (* top W to avoid any filtering *)
-    let tid = ThreadId.get_current ask in
-    let sidev = GMutex.singleton tid rel_side in
+    let digest = Digest.current ask in
+    let sidev = GMutex.singleton digest rel_side in
     sideg V.mutex_inits (G.create_mutex sidev);
     (* Introduction into local state not needed, will be read via initializer *)
     (* Also no side-effect to mutex globals needed, the value here will either by read via the initializer, *)
@@ -1207,11 +1203,11 @@ let priv_module: (module S) Lazy.t =
          | "protection" -> (module ProtectionBasedPriv (struct let path_sensitive = false end))
          | "protection-path" -> (module ProtectionBasedPriv (struct let path_sensitive = true end))
          | "mutex-meet" -> (module PerMutexMeetPriv)
-         | "mutex-meet-tid" -> (module PerMutexMeetPrivTID (NoCluster))
-         | "mutex-meet-tid-cluster12" -> (module PerMutexMeetPrivTID (DownwardClosedCluster (Clustering12)))
-         | "mutex-meet-tid-cluster2" -> (module PerMutexMeetPrivTID (ArbitraryCluster (Clustering2)))
-         | "mutex-meet-tid-cluster-max" -> (module PerMutexMeetPrivTID (ArbitraryCluster (ClusteringMax)))
-         | "mutex-meet-tid-cluster-power" -> (module PerMutexMeetPrivTID (DownwardClosedCluster (ClusteringPower)))
+         | "mutex-meet-tid" -> (module PerMutexMeetPrivTID (ThreadDigest) (NoCluster))
+         | "mutex-meet-tid-cluster12" -> (module PerMutexMeetPrivTID (ThreadDigest) (DownwardClosedCluster (Clustering12)))
+         | "mutex-meet-tid-cluster2" -> (module PerMutexMeetPrivTID (ThreadDigest) (ArbitraryCluster (Clustering2)))
+         | "mutex-meet-tid-cluster-max" -> (module PerMutexMeetPrivTID (ThreadDigest) (ArbitraryCluster (ClusteringMax)))
+         | "mutex-meet-tid-cluster-power" -> (module PerMutexMeetPrivTID (ThreadDigest) (DownwardClosedCluster (ClusteringPower)))
          | _ -> failwith "ana.relation.privatization: illegal value"
       )
     in

src/analyses/base.ml

@@ -6,6 +6,7 @@ open Pretty
 open Analyses
 open GobConfig
 open BaseUtil
+open ReturnUtil
 module A = Analyses
 module H = Hashtbl
 module Q = Queries
@@ -143,13 +144,6 @@ struct
    * Initializing my variables
    **************************************************************************)
 
-  let return_varstore = ref dummyFunDec.svar
-  let return_varinfo () = !return_varstore
-  let return_var () = AD.of_var (return_varinfo ())
-  let return_lval (): lval = (Var (return_varinfo ()), NoOffset)
-
-  let longjmp_return = ref dummyFunDec.svar
-
   let heap_var on_stack ctx =
     let info = match (ctx.ask (Q.AllocVar {on_stack})) with
       | `Lifted vinfo -> vinfo
@@ -1953,8 +1947,8 @@ struct
 
 
 
-  let forkfun (ctx:(D.t, G.t, C.t, V.t) Analyses.ctx) (lv: lval option) (f: varinfo) (args: exp list) : (lval option * varinfo * exp list) list * bool =
-    let create_thread lval arg v =
+  let forkfun (ctx:(D.t, G.t, C.t, V.t) Analyses.ctx) (lv: lval option) (f: varinfo) (args: exp list) : (lval option * varinfo * exp list * bool) list =
+    let create_thread ~multiple lval arg v =
       try
         (* try to get function declaration *)
         let fd = Cilfacade.find_varinfo_fundec v in
@@ -1963,7 +1957,7 @@ struct
           | Some x -> [x]
           | None -> List.map (fun x -> MyCFG.unknown_exp) fd.sformals
         in
-        Some (lval, v, args)
+        Some (lval, v, args, multiple)
       with Not_found ->
         if LF.use_special f.vname then None (* we handle this function *)
         else if isFunctionType v.vtype then
@@ -1973,7 +1967,7 @@ struct
             | Some x -> [x]
             | None -> List.map (fun x -> MyCFG.unknown_exp) (Cil.argsToList v_args)
           in
-          Some (lval, v, args)
+          Some (lval, v, args, multiple)
         else (
           M.debug ~category:Analyzer "Not creating a thread from %s because its type is %a" v.vname d_type v.vtype;
           None
@@ -1982,7 +1976,7 @@ struct
     let desc = LF.find f in
     match desc.special args, f.vname with
     (* handling thread creations *)
-    | ThreadCreate { thread = id; start_routine = start; arg = ptc_arg }, _ -> begin
+    | ThreadCreate { thread = id; start_routine = start; arg = ptc_arg; multiple }, _ -> begin
         (* extra sync so that we do not analyze new threads with bottom global invariant *)
         publish_all ctx `Thread;
         (* Collect the threads. *)
@@ -1994,7 +1988,7 @@ struct
           else
             start_funvars
         in
-        List.filter_map (create_thread (Some (Mem id, NoOffset)) (Some ptc_arg)) start_funvars_with_unknown, false
+        List.filter_map (create_thread ~multiple (Some (Mem id, NoOffset)) (Some ptc_arg)) start_funvars_with_unknown
       end
     | _, _ when get_bool "sem.unknown_function.spawn" ->
       (* TODO: Remove sem.unknown_function.spawn check because it is (and should be) really done in LibraryFunctions.
@@ -2008,8 +2002,8 @@ struct
       let flist = shallow_flist @ deep_flist in
       let addrs = List.concat_map AD.to_var_may flist in
       if addrs <> [] then M.debug ~category:Analyzer "Spawning non-unique functions from unknown function: %a" (d_list ", " CilType.Varinfo.pretty) addrs;
-      List.filter_map (create_thread None None) addrs, true
-    | _, _ -> [], false
+      List.filter_map (create_thread ~multiple:true None None) addrs
+    | _, _ -> []
 
   let assert_fn ctx e refine =
     (* make the state meet the assertion in the rest of the code *)
@@ -2140,9 +2134,9 @@ struct
       let addr = eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval in
       (addr, AD.type_of addr)
     in
-    let forks, multiple = forkfun ctx lv f args in
-    if M.tracing then if not (List.is_empty forks) then M.tracel "spawn" "Base.special %s: spawning functions %a\n" f.vname (d_list "," CilType.Varinfo.pretty) (List.map BatTuple.Tuple3.second forks);
-    List.iter (BatTuple.Tuple3.uncurry (ctx.spawn ~multiple)) forks;
+    let forks = forkfun ctx lv f args in
+    if M.tracing then if not (List.is_empty forks) then M.tracel "spawn" "Base.special %s: spawning functions %a\n" f.vname (d_list "," CilType.Varinfo.pretty) (List.map BatTuple.Tuple4.second forks);
+    List.iter (fun (lval, f, args, multiple) -> ctx.spawn ~multiple lval f args) forks;
     let st: store = ctx.local in
     let gs = ctx.global in
     let desc = LF.find f in
@@ -2871,7 +2865,7 @@ struct
         | "once" ->
           f (D.bot ())
         | "fixpoint" ->
-          let module DFP = LocalFixpoint.Make (D) in
+          let module DFP = Goblint_solver.LocalFixpoint.Make (D) in
           DFP.lfp f
         | _ ->
           assert false
@@ -2930,8 +2924,6 @@ end
 module type MainSpec = sig
   include MCPSpec
   include BaseDomain.ExpEvaluator
-  val return_lval: unit -> Cil.lval
-  val return_varinfo: unit -> Cil.varinfo
 end
 
 let main_module: (module MainSpec) Lazy.t =