Merge branch 'issue_1140' into issue-1374-3

.github/workflows/docs.yml

@@ -41,7 +41,7 @@ jobs:
 
       - name: Setup Pages
         id: pages
-        uses: actions/configure-pages@v4
+        uses: actions/configure-pages@v5
 
       - name: Install dependencies
         run: opam install . --deps-only --locked --with-doc

.github/workflows/locked.yml

@@ -18,7 +18,7 @@ jobs:
       matrix:
         os:
           - ubuntu-latest
-          - macos-latest
+          - macos-13
         ocaml-compiler:
           - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
           # don't add any other because they won't be used
@@ -62,7 +62,7 @@ jobs:
         if: always()
         with:
           name: suite_result-${{ matrix.os }}
-          path: tests/suite_result/
+          path: _build/default/tests/suite_result/
 
   extraction:
     if: ${{ github.event_name == 'workflow_dispatch' || github.event_name == 'schedule' }}

.github/workflows/unlocked.yml

@@ -16,7 +16,7 @@ jobs:
       matrix:
         os:
           - ubuntu-latest
-          - macos-latest
+          - macos-13
         ocaml-compiler:
           - 5.0.x
           - ocaml-variants.4.14.0+options,ocaml-option-flambda
@@ -91,7 +91,7 @@ jobs:
       matrix:
         os:
           - ubuntu-latest
-          - macos-latest
+          - macos-13
         ocaml-compiler:
           - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file, downgrade deps step
 
@@ -134,7 +134,7 @@ jobs:
       - name: Downgrade dependencies
         # must specify ocaml-base-compiler again to prevent it from being downgraded
         # prevent num downgrade to avoid dune/jbuilder error: https://github.com/ocaml/dune/issues/5280
-        run: opam install $(opam exec -- opam-0install --prefer-oldest goblint ocaml-variants.4.14.0+options ocaml-option-flambda num.1.4)
+        run: opam install $(opam exec -- opam-0install --prefer-oldest goblint ocaml-variants.4.14.0+options ocaml-option-flambda num.1.5)
 
       - name: Build
         run: ./make.sh nat
@@ -189,7 +189,7 @@ jobs:
       matrix:
         os:
           - ubuntu-latest
-          - macos-latest
+          - macos-13
         ocaml-compiler:
           - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
 

.mailmap

@@ -17,6 +17,9 @@ Stefan Marcik <[email protected]> <stefan@stefan-ubuntu.(none)>
 Ralf Vogler <[email protected]>
 <[email protected]> <[email protected]>
 <[email protected]> <[email protected]>
+Michael Petter <[email protected]>
+<[email protected]> <[email protected]>
+<[email protected]> <[email protected]>
 
 Ivana Zuzic <[email protected]> <[email protected]>
 Kerem Çakırer <[email protected]> <[email protected]>

README.md

@@ -8,6 +8,7 @@
 [![Coverage Status](https://coveralls.io/repos/github/goblint/analyzer/badge.svg?branch=master)](https://coveralls.io/github/goblint/analyzer?branch=master)
 [![docker workflow status](https://github.com/goblint/analyzer/actions/workflows/docker.yml/badge.svg)](https://github.com/goblint/analyzer/actions/workflows/docker.yml)
 [![Documentation Status](https://readthedocs.org/projects/goblint/badge/?version=latest)](https://goblint.readthedocs.io/en/latest/?badge=latest)
+[![project chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://goblint.zulipchat.com)
 
 Documentation can be browsed on [Read the Docs](https://goblint.readthedocs.io/en/latest/) or [GitHub](./docs/).
 
@@ -56,3 +57,9 @@ docker run -it --rm -v $(pwd):/data goblint /data/tests/regression/04-mutex/01-s
 If pulled from GitHub Container Registry, use the container name `ghcr.io/goblint/analyzer:latest` (or `:nightly`) instead.
 
 For further information, see [documentation](https://goblint.readthedocs.io/en/latest/user-guide/running/).
+
+## Acknowledgements
+
+Work on Goblint was supported in part by Deutsche Forschungsgemeinschaft (DFG) (47140942/1480 [PUMA](https://gepris.dfg.de/gepris/projekt/4714094), 378803395/2428 [ConVeY](http://convey.in.tum.de)), ARTEMIS Joint Undertaking (269335 [MBAT](http://www.mbat-artemis.eu/home/)), ITEA3 project 14014 [ASSUME](http://assume-project.eu/), the Shota Rustaveli National Science Foundation of Georgia [FR-21-7973](https://viam.science.tsu.ge/new/index.php?lang=eng&page=projects&subpage=111), the Estonian Research Council ([IUT2-1](https://www.etis.ee/Portal/Projects/Display/561b7b1d-d1dd-43a2-90e5-0661de823823?lang=ENG), [PSG61](https://www.etis.ee/Portal/Projects/Display/743243bb-15c2-47b3-9c10-e7d86a9a276d?lang=ENG)), and the Estonian Centre of Excellence in IT (EXCITE), funded by the European Regional Development Fund.
+
+We also thank [Zulip](https://zulip.com) for providing free Zulip Cloud Standard hosting for the Goblint project. Zulip is an open-source modern team chat app designed to keep both live and asynchronous conversations organized.

conf/traces.json

@@ -3,7 +3,8 @@
     "int": {
       "def_exc": true,
       "interval": false,
-      "enums": true
+      "enums": true,
+      "def_exc_widen_by_join": true
     },
     "malloc": {
       "wrappers": [

docs/developer-guide/testing.md

@@ -153,7 +153,7 @@ The comparison input and the metadata in the patch headers are not necessary and
 ## Unit tests
 
 ### Running
-The unit tests can be run with `dune runtest unittest`.
+The unit tests can be run with `dune runtest tests/unit`.
 Use `--watch` for automatic rebuilding and retesting.
 
 ## Domain tests

docs/user-guide/assumptions.md

@@ -0,0 +1,19 @@
+# Assumptions
+
+Goblint makes the following (implicit) assumptions about the systems and programs it analyzes.
+
+_NB! This list is likely incomplete._
+
+1. `PTHREAD_MUTEX_DEFAULT` is a non-recursive mutex type.
+
+    Although the [POSIX Programmer's Manual](https://linux.die.net/man/3/pthread_mutexattr_settype) states that
+
+    > An implementation may map this mutex to one of the other mutex types.
+
+    including `PTHREAD_MUTEX_RECURSIVE`, on Linux and OSX it seems to be mapped to `PTHREAD_MUTEX_NORMAL`.
+    Goblint assumes this to be the case.
+
+    This affects the `maylocks` analysis.
+
+    See [PR #1414](https://github.com/goblint/analyzer/pull/1414).
+

goblint.opam

@@ -78,7 +78,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
   # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
-  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#833378d9102578bab7b62174cb029d385db417a5" ]
+  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
 ]

goblint.opam.locked

@@ -134,7 +134,7 @@ post-messages: [
 pin-depends: [
   [
     "goblint-cil.2.0.3"
-    "git+https://github.com/goblint/cil.git#833378d9102578bab7b62174cb029d385db417a5"
+    "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f"
   ]
   [
     "ppx_deriving.5.2.1"

goblint.opam.template

@@ -3,7 +3,7 @@
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
   # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
-  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#833378d9102578bab7b62174cb029d385db417a5" ]
+  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
 ]

mkdocs.yml

@@ -22,6 +22,7 @@ nav:
     - ▶️ Running: user-guide/running.md
     - 🔧 Configuring: user-guide/configuring.md
     - 🗂️ Options reference: jsfh/options.schema.html
+    - ⚠️ Assumptions: user-guide/assumptions.md
     - 🔍 Inspecting: user-guide/inspecting.md
     - 📝 Annotating: user-guide/annotating.md
     - 🐎 Benchmarking: user-guide/benchmarking.md

scripts/goblint-lib-modules.py

@@ -48,6 +48,7 @@
     "ConfigVersion",
     "ConfigProfile",
     "ConfigOcaml",
+    "ConfigDatetime",
 ])
 
 src_modules = set()

scripts/update_suite.rb

@@ -29,6 +29,7 @@ def pink; colorize(35) end
   def cyan; colorize(36) end
   def white; colorize(37) end
   def bg_black; colorize(40) end # gray for me
+  def bold; colorize(1) end
   def gray; colorize("38;5;240") end
 end
 class Array
@@ -63,6 +64,7 @@ def clearline
 #Command line parameters
 #Either only run a single test, or
 #"future" will also run tests we normally skip
+quiet = ARGV.last == "-q" && ARGV.pop
 $dump = ARGV.last == "-d" && ARGV.pop
 sequential = ARGV.last == "-s" && ARGV.pop
 marshal = ARGV.last == "-m" && ARGV.pop
@@ -85,10 +87,24 @@ def clearline
   future = thegroup.start_with?"-"
   future = !future # why does negation above fail?
   only = nil
+  descr = " group #{thegroup}"
 else
   future = false
+  if only.nil? then
+    descr = ""
+  else
+    descr = " #{only}"
+  end
 end
 
+if cfg then
+  descr = " incremental cfg"
+elsif incremental then
+  descr = " incremental ast"
+end
+
+print "update_suite#{descr}: ".bold
+
 $testresults = File.expand_path("tests/suite_result")
 begin
   Dir.mkdir($testresults)
@@ -608,9 +624,10 @@ def run ()
   dirname = File.dirname(filepath)
   filename = File.basename(filepath)
   Dir.chdir(dirname)
-  clearline
+  clearline unless quiet
   id = "#{p.id} #{p.group}/#{p.name}"
-  print "Testing #{id}"
+  print "Testing #{id}" unless quiet
+  print "." if quiet
   begin
     Dir.mkdir(File.join($testresults, p.group)) unless Dir.exist?(File.join($testresults, p.group))
   rescue
@@ -688,7 +705,7 @@ def run ()
   puts ("Results: " + theresultfile)
 end
 if $alliswell then
-  puts "No errors :)".green
+  puts "No errors :)".green unless quiet
 else
   puts "#{$failed.length} test(s) failed: #{$failed}".red
 end

src/analyses/apron/relationAnalysis.apron.ml

@@ -76,6 +76,7 @@ struct
               VH.find v_ins v
             else
               let v_in = Cilfacade.create_var @@ makeVarinfo false (v.vname ^ "#in") v.vtype in (* temporary local g#in for global g *)
+              v_in.vattr <- v.vattr; (* preserve goblint_relation_track attribute *)
               VH.replace v_ins v v_in;
               v_in
           in
@@ -97,6 +98,7 @@ struct
     let v_ins_inv = VH.create (List.length vs) in
     List.iter (fun v ->
         let v_in = Cilfacade.create_var @@ makeVarinfo false (v.vname ^ "#in") v.vtype in (* temporary local g#in for global g *)
+        v_in.vattr <- v.vattr; (* preserve goblint_relation_track attribute *)
         VH.replace v_ins_inv v_in v;
       ) vs;
     let rel = RD.add_vars st.rel (List.map RV.local (VH.keys v_ins_inv |> List.of_enum)) in (* add temporary g#in-s *)

src/analyses/apron/relationPriv.apron.ml

@@ -607,7 +607,10 @@ struct
         )
       in
       (* Unprotected invariant is one big relation. *)
-      sideg (V.mutex atomic_mutex) rel_side;
+      (* If no globals are contained here, none need to be published *)
+      (* https://github.com/goblint/analyzer/pull/1354 *)
+      if RD.vars rel_side <> [] then
+        sideg (V.mutex atomic_mutex) rel_side;
       let rel_local =
         let newly_unprot var = match AV.find_metadata var with
           | Some (Global g) -> is_unprotected_without ask g atomic_mutex

src/analyses/base.ml

@@ -755,7 +755,7 @@ struct
       let te1 = Cilfacade.typeOf e1 in
       let te2 = Cilfacade.typeOf e2 in
       let both_arith_type = isArithmeticType te1 && isArithmeticType te2 in
-      let is_safe = (extra_is_safe || VD.is_safe_cast t1 te1 && VD.is_safe_cast t2 te2) && not both_arith_type in
+      let is_safe = (extra_is_safe || VD.is_statically_safe_cast t1 te1 && VD.is_statically_safe_cast t2 te2) && not both_arith_type in
       if M.tracing then M.tracel "cast" "remove cast on both sides for %a? -> %b" d_exp exp is_safe;
       if is_safe then ( (* we can ignore the casts if the casts can't change the value *)
         let e1 = if isArithmeticType te1 then c1 else e1 in
@@ -1264,6 +1264,26 @@ struct
     let res = match Cilfacade.get_ikind_exp exp with
       | exception _ -> BoolDomain.MayBool.top ()
       | ik ->
+        let checkDiv e1 e2 =
+          let binop = (GobOption.map2 Z.div )in
+          match ctx.ask (EvalInt e1), ctx.ask (EvalInt e2) with
+          | `Bot, _ -> false
+          | _, `Bot -> false
+          | `Lifted i1, `Lifted i2 ->
+            ( let divisor_contains_zero = (ID.is_bot @@ ID.meet i2 (ID.of_int ik Z.zero))  in
+              if divisor_contains_zero then true else 
+                ( let (min_ik, max_ik) = IntDomain.Size.range ik in
+                  let (min_i1, max_i1) = (IntDomain.IntDomTuple.minimal i1, IntDomain.IntDomTuple.maximal i1) in
+                  let (min_i2, max_i2) = (IntDomain.IntDomTuple.minimal i2, IntDomain.IntDomTuple.maximal i2) in
+                  let (min_i2, max_i2) = (Option.map (fun x -> if (Z.zero=x) then Z.one else x) min_i2,
+                                          Option.map (fun x -> if (Z.zero=x) then Z.neg Z.one else x) max_i2) in
+                  let possible_combinations = [binop min_i1 min_i2; binop  min_i1 max_i2; binop max_i1 min_i2; binop max_i1 max_i2] in
+                  let min_exp = List.min possible_combinations in
+                  let max_exp = List.max possible_combinations in
+                  match min_exp, max_exp with
+                  | Some min, Some max when min >= min_ik && max <= max_ik -> false
+                  | _ -> true ))
+          | _   -> true in
         let checkBinop e1 e2 binop =
           match ctx.ask (EvalInt e1), ctx.ask (EvalInt e2) with
           | `Bot, _ -> false
@@ -1317,7 +1337,7 @@ struct
               | PlusA|PlusPI|IndexPI -> checkBinop e1 e2 (GobOption.map2 Z.(+))
               | MinusA|MinusPI|MinusPP -> checkBinop e1 e2 (GobOption.map2 Z.(-))
               | Mult -> checkBinop e1 e2 (GobOption.map2 Z.mul)
-              | Div -> checkBinop e1 e2 (GobOption.map2 Z.div)
+              | Div -> checkDiv e1 e2
               | Mod -> (* an overflow happens when the second operand is negative *)
                 checkPredicate e2 (fun interval_bound _ -> Z.gt interval_bound Z.zero)
               (* operations that do not result in overflow in C: *)
@@ -1375,10 +1395,15 @@ struct
     | Q.EvalInt e ->
       query_evalint ~ctx ctx.local e
     | Q.EvalMutexAttr e -> begin
-        let e:exp = Lval (Cil.mkMem ~addr:e ~off:NoOffset) in
-        match eval_rv ~ctx ctx.local e with
-        | MutexAttr a -> a
-        | v -> MutexAttrDomain.top ()
+        match eval_rv_address ~ctx ctx.local e with
+        | Address a ->
+          let default = `Lifted MutexAttrDomain.MutexKind.NonRec in (* Goblint assumption *)
+          begin match get ~ctx ~top:(MutexAttr default) ctx.local a None with (* ~top corresponds to default NULL with assume_top *)
+            | MutexAttr a -> a
+            | Bot -> default (* corresponds to default NULL with assume_none *)
+            | _ -> MutexAttrDomain.top ()
+          end
+        | _ -> MutexAttrDomain.top ()
       end
     | Q.EvalLength e -> begin
         match eval_rv_address ~ctx ctx.local e with