Merge branch 'master' into thesis-weakly-relational-pointer

.github/workflows/coverage.yml

@@ -18,7 +18,7 @@ jobs:
         os:
           - ubuntu-latest
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
           # don't add any other because they won't be used
 
     runs-on: ${{ matrix.os }}

.github/workflows/docs.yml

@@ -18,7 +18,7 @@ jobs:
         os:
           - ubuntu-latest
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
           # don't add any other because they won't be used
 
     runs-on: ${{ matrix.os }}

.github/workflows/locked.yml

@@ -20,7 +20,7 @@ jobs:
           - ubuntu-latest
           - macos-13
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
           # don't add any other because they won't be used
 
     runs-on: ${{ matrix.os }}
@@ -72,7 +72,7 @@ jobs:
         os:
           - ubuntu-latest
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
           # don't add any other because they won't be used
 
     runs-on: ${{ matrix.os }}
@@ -114,7 +114,7 @@ jobs:
         os:
           - ubuntu-latest
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
           # don't add any other because they won't be used
         node-version:
           - 14

.github/workflows/unlocked.yml

@@ -21,7 +21,7 @@ jobs:
           - 5.2.x
           - 5.1.x
           - 5.0.x
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda
           - 4.14.x
         apron:
           - false
@@ -91,7 +91,7 @@ jobs:
           - ubuntu-latest
           - macos-13
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file, downgrade deps step
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file, downgrade deps step
 
     name: lower-bounds (${{ matrix.os }}, ${{ matrix.ocaml-compiler }}, downgrade)
 
@@ -131,7 +131,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.5)
+        run: opam install $(opam exec -- opam-0install --prefer-oldest goblint ocaml-variants.4.14.2+options ocaml-option-flambda num.1.5)
 
       - name: Build
         run: ./make.sh nat
@@ -188,7 +188,7 @@ jobs:
           - ubuntu-latest
           - macos-13
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
 
     runs-on: ${{ matrix.os }}
 

dune-project

@@ -42,7 +42,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e
     (zarith (>= 1.10))
     (yojson (>= 2.0.0))
     (qcheck-core (>= 0.19))
-    ppx_deriving
+    (ppx_deriving (>= 6.0.2))
     (ppx_deriving_hash (>= 0.1.2))
     (ppx_deriving_yojson (>= 3.7.0))
     (ounit2 :with-test)
@@ -67,7 +67,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e
     conf-gcc ; ensures opam-repository CI installs real gcc from homebrew on MacOS
   )
   (depopts
-    apron
+    (apron (>= v0.9.15))
     z3
   )
   (conflicts

goblint.opam

@@ -42,7 +42,7 @@ depends: [
   "zarith" {>= "1.10"}
   "yojson" {>= "2.0.0"}
   "qcheck-core" {>= "0.19"}
-  "ppx_deriving"
+  "ppx_deriving" {>= "6.0.2"}
   "ppx_deriving_hash" {>= "0.1.2"}
   "ppx_deriving_yojson" {>= "3.7.0"}
   "ounit2" {with-test}
@@ -66,7 +66,10 @@ depends: [
   "benchmark" {with-test}
   "conf-gcc"
 ]
-depopts: ["apron" "z3"]
+depopts: [
+  "apron" {>= "v0.9.15"}
+  "z3"
+]
 conflicts: [
   "result" {< "1.5"}
   "ez-conf-lib" {= "1"}
@@ -94,8 +97,6 @@ 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#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" ]
 ]
 depexts: [
   ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}

goblint.opam.locked

@@ -22,89 +22,94 @@ homepage: "https://goblint.in.tum.de"
 doc: "https://goblint.readthedocs.io/en/latest/"
 bug-reports: "https://github.com/goblint/analyzer/issues"
 depends: [
-  "angstrom" {= "0.15.0"}
-  "apron" {= "v0.9.14~beta.2"}
+  "angstrom" {= "0.16.0"}
+  "apron" {= "v0.9.15"}
   "arg-complete" {= "0.1.0"}
   "astring" {= "0.8.5"}
   "base-bigarray" {= "base"}
   "base-bytes" {= "base"}
   "base-threads" {= "base"}
   "base-unix" {= "base"}
-  "batteries" {= "3.6.0"}
+  "batteries" {= "3.8.0"}
   "benchmark" {= "1.6" & with-test}
   "bigarray-compat" {= "1.1.0"}
-  "bigstringaf" {= "0.9.0"}
+  "bigstringaf" {= "0.9.1"}
   "bos" {= "0.2.1"}
-  "camlidl" {= "1.11"}
+  "camlidl" {= "1.12"}
   "camlp-streams" {= "5.0.1"}
   "catapult" {= "0.2"}
   "catapult-file" {= "0.2"}
-  "cmdliner" {= "1.1.1" & with-doc}
-  "conf-autoconf" {= "0.1"}
+  "cmdliner" {= "1.3.0" & with-doc}
+  "conf-autoconf" {= "0.2"}
+  "conf-findutils" {= "1"}
   "conf-gcc" {= "1.0"}
   "conf-gmp" {= "4"}
-  "conf-mpfr" {= "3"}
+  "conf-gmp-paths" {= "1"}
+  "conf-mpfr-paths" {= "1"}
   "conf-perl" {= "2"}
-  "conf-pkg-config" {= "2"}
   "conf-ruby" {= "1.0.0" & with-test}
-  "conf-which" {= "1"}
   "cppo" {= "1.6.9"}
   "cpu" {= "2.0.0"}
-  "csexp" {= "1.5.1"}
-  "ctypes" {= "0.20.1"}
-  "dune" {= "3.7.1"}
-  "dune-build-info" {= "3.7.1"}
-  "dune-configurator" {= "3.7.1"}
-  "dune-private-libs" {= "3.7.1"}
-  "dune-site" {= "3.7.1"}
-  "dyn" {= "3.7.1"}
+  "crunch" {= "3.3.1" & with-doc}
+  "csexp" {= "1.5.2"}
+  "cstruct" {= "6.2.0"}
+  "ctypes" {= "0.22.0"}
+  "dune" {= "3.16.0"}
+  "dune-build-info" {= "3.16.0"}
+  "dune-configurator" {= "3.16.0"}
+  "dune-private-libs" {= "3.16.0"}
+  "dune-site" {= "3.16.0"}
+  "dyn" {= "3.16.0"}
+  "ez-conf-lib" {= "2"}
   "fileutils" {= "0.6.4"}
   "fmt" {= "0.9.0"}
   "fpath" {= "0.7.3"}
   "goblint-cil" {= "2.0.3"}
+  "hex" {= "1.5.0"}
   "integers" {= "0.7.0"}
-  "json-data-encoding" {= "0.12.1"}
-  "jsonrpc" {= "1.15.0~5.0preview1"}
+  "json-data-encoding" {= "1.0.1"}
+  "jsonrpc" {= "1.17.0"}
   "logs" {= "0.7.0"}
-  "mlgmpidl" {= "1.2.15"}
-  "num" {= "1.4"}
-  "ocaml" {= "4.14.0"}
+  "mlgmpidl" {= "1.3.0"}
+  "num" {= "1.5"}
+  "ocaml" {= "4.14.2"}
   "ocaml-compiler-libs" {= "v0.12.4"}
   "ocaml-config" {= "2"}
   "ocaml-option-flambda" {= "1"}
   "ocaml-syntax-shims" {= "1.0.0"}
-  "ocaml-variants" {= "4.14.0+options"}
-  "ocamlbuild" {= "0.14.2"}
-  "ocamlfind" {= "1.9.5"}
-  "odoc" {= "2.2.0" & with-doc}
-  "odoc-parser" {= "2.0.0" & with-doc}
-  "ordering" {= "3.7.1"}
-  "ounit2" {= "2.2.6" & with-test}
-  "pp" {= "1.1.2"}
+  "ocaml-variants" {= "4.14.2+options"}
+  "ocamlbuild" {= "0.14.3"}
+  "ocamlfind" {= "1.9.6"}
+  "odoc" {= "2.4.2" & with-doc}
+  "odoc-parser" {= "2.4.2" & with-doc}
+  "ordering" {= "3.16.0"}
+  "ounit2" {= "2.2.7" & with-test}
+  "pp" {= "1.2.0"}
   "ppx_derivers" {= "1.2.1"}
-  "ppx_deriving" {= "5.2.1"}
+  "ppx_deriving" {= "6.0.2"}
   "ppx_deriving_hash" {= "0.1.2"}
-  "ppx_deriving_yojson" {= "3.7.0"}
-  "ppxlib" {= "0.28.0"}
-  "qcheck-core" {= "0.20"}
-  "qcheck-ounit" {= "0.20" & with-test}
-  "re" {= "1.10.4" & with-doc}
-  "result" {= "1.5"}
+  "ppx_deriving_yojson" {= "3.8.0"}
+  "ppxlib" {= "0.32.1"}
+  "ptime" {= "1.1.0" & with-doc}
+  "qcheck-core" {= "0.21.3"}
+  "qcheck-ounit" {= "0.21.3" & with-test}
+  "re" {= "1.11.0" & with-doc}
+  "result" {= "1.5" & with-doc}
   "rresult" {= "0.7.0"}
   "seq" {= "base"}
-  "sexplib0" {= "v0.15.1"}
-  "sha" {= "1.15.2"}
+  "sexplib0" {= "v0.16.0"}
+  "sha" {= "1.15.4"}
   "stdlib-shims" {= "0.3.0"}
-  "stdune" {= "3.7.1"}
+  "stdune" {= "3.16.0"}
   "stringext" {= "1.6.0"}
-  "topkg" {= "1.0.6"}
-  "tyxml" {= "4.5.0" & with-doc}
-  "uri" {= "4.2.0"}
+  "topkg" {= "1.0.7"}
+  "tyxml" {= "4.6.0" & with-doc}
+  "uri" {= "4.4.0"}
   "uuidm" {= "0.9.8"}
   "uutf" {= "1.0.3" & with-doc}
-  "yaml" {= "3.1.0"}
-  "yojson" {= "2.0.2"}
-  "zarith" {= "1.12"}
+  "yaml" {= "3.2.0"}
+  "yojson" {= "2.2.1"}
+  "zarith" {= "1.13"}
 ]
 build: [
   ["dune" "subst"] {dev}
@@ -137,10 +142,6 @@ pin-depends: [
     "goblint-cil.2.0.3"
     "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f"
   ]
-  [
-    "ppx_deriving.5.2.1"
-    "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6"
-  ]
 ]
 depexts: ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
 description: """\

goblint.opam.template

@@ -4,8 +4,6 @@ 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#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" ]
 ]
 depexts: [
   ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}

make.sh

@@ -8,7 +8,7 @@ opam_setup() {
   set -x
   opam init -y -a --bare $SANDBOXING # sandboxing is disabled in travis and docker
   opam update
-  opam switch -y create . --deps-only --packages=ocaml-variants.4.14.0+options,ocaml-option-flambda --locked
+  opam switch -y create . --deps-only --packages=ocaml-variants.4.14.2+options,ocaml-option-flambda --locked
 }
 
 rule() {

scripts/creduce/privPrecCompare.sh

@@ -22,7 +22,7 @@ for PRIV in "${PRIVS[@]}"; do
     PRIVDUMP="$OUTDIR/$PRIV"
     LOG="$OUTDIR/$PRIV.log"
     rm -f $PRIVDUMP
-    $GOBLINTDIR/goblint --sets exp.privatization $PRIV --sets exp.priv-prec-dump $PRIVDUMP $OPTS -v --enable warn.debug &> $LOG
+    $GOBLINTDIR/goblint --set exp.privatization $PRIV --set exp.priv-prec-dump $PRIVDUMP $OPTS -v --enable warn.debug &> $LOG
     grep -F "Function definition missing" $LOG && exit 1
 done
 

scripts/privPrecCompare.sh

@@ -10,7 +10,7 @@ mkdir -p $OUTDIR
 for PRIV in "${PRIVS[@]}"; do
     echo $PRIV
     PRIVDUMP="$OUTDIR/$PRIV"
-    ./goblint --sets exp.privatization $PRIV --sets exp.priv-prec-dump $PRIVDUMP "$@"
+    ./goblint --set exp.privatization $PRIV --set exp.priv-prec-dump $PRIVDUMP "$@"
 done
 
 PRIVDUMPS=("${PRIVS[*]/#/$OUTDIR/}") # why [*] here?

scripts/test-gobview.py

@@ -6,6 +6,7 @@
 from webdriver_manager.chrome import ChromeDriverManager
 from selenium.webdriver.common.by import By
 from selenium.webdriver.chrome.options import Options
+from selenium.webdriver.common.desired_capabilities import DesiredCapabilities
 from threading import Thread
 import subprocess
 
@@ -17,6 +18,11 @@
 # cleanup
 def cleanup(browser, thread):
   print("cleanup")
+
+  # print messages
+  for entry in browser.get_log('browser'):
+    print(entry)
+
   browser.close()
   p.kill()
   thread.join()
@@ -35,6 +41,8 @@ def serve():
 print("starting installation of browser\n")
 options = Options()
 options.add_argument('headless')
+# options.set_capability("loggingPrefs", { 'browser':'ALL' })
+options.set_capability("goog:loggingPrefs", { 'browser':'ALL' })
 browser = webdriver.Chrome(service=Service(ChromeDriverManager().install()),options=options)
 print("finished webdriver installation \n")
 browser.maximize_window()

src/analyses/apron/relationAnalysis.apron.ml

@@ -295,7 +295,7 @@ struct
     (* there should be smarter ways to do this, e.g. by keeping track of which values are written etc. ... *)
     (* See, e.g, Beckschulze E, Kowalewski S, Brauer J (2012) Access-based localization for octagons. Electron Notes Theor Comput Sci 287:29–40 *)
     (* Also, a local *)
-    let vname = Apron.Var.to_string var in
+    let vname = GobApron.Var.show var in
     let locals = fundec.sformals @ fundec.slocals in
     match List.find_opt (fun v -> VM.var_name (Local v) = vname) locals with (* TODO: optimize *)
     | None -> true
@@ -418,7 +418,7 @@ struct
     in
     let any_local_reachable = any_local_reachable fundec reachable_from_args in
     let arg_vars = f.sformals |> List.filter (RD.Tracked.varinfo_tracked) |> List.map RV.arg in
-    if M.tracing then M.tracel "combine-rel" "relation remove vars: %a" (docList (fun v -> Pretty.text (Apron.Var.to_string v))) arg_vars;
+    if M.tracing then M.tracel "combine-rel" "relation remove vars: %a" (docList (GobApron.Var.pretty ())) arg_vars;
     RD.remove_vars_with new_fun_rel arg_vars; (* fine to remove arg vars that also exist in caller because unify from new_rel adds them back with proper constraints *)
     let tainted = f_ask.f Queries.MayBeTainted in
     let tainted_vars = TaintPartialContexts.conv_varset tainted in