Merge branch 'master' into dune-runtest

.github/workflows/coverage.yml

@@ -38,6 +38,11 @@ jobs:
         uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
+          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
+
+      - name: Install graph-easy # TODO: remove if depext --with-test works
+        if: ${{ matrix.os == 'ubuntu-latest' }}
+        run: sudo apt install -y libgraph-easy-perl
 
       - name: Install dependencies
         run: opam install . --deps-only --locked --with-test

.github/workflows/docs.yml

@@ -2,8 +2,7 @@ name: docs
 
 on:
   push:
-    branches:
-      - master
+  pull_request:
 
   workflow_dispatch:
 
@@ -55,7 +54,7 @@ jobs:
         run: opam exec -- dune build @doc
 
       - name: Upload artifact
-        uses: actions/upload-pages-artifact@v2
+        uses: actions/upload-pages-artifact@v3
         with:
           path: _build/default/_doc/_html/
 
@@ -65,7 +64,8 @@ jobs:
       url: ${{ steps.deployment.outputs.page_url }}
     runs-on: ubuntu-latest
     needs: api-build
+    if: ${{ github.event_name == 'push' && github.ref == 'refs/heads/master' }}
     steps:
       - name: Deploy to GitHub Pages
         id: deployment
-        uses: actions/deploy-pages@v3
+        uses: actions/deploy-pages@v4

.github/workflows/locked.yml

@@ -40,6 +40,11 @@ jobs:
         uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
+          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
+
+      - name: Install graph-easy # TODO: remove if depext --with-test works
+        if: ${{ matrix.os == 'ubuntu-latest' }}
+        run: sudo apt install -y libgraph-easy-perl
 
       - name: Install dependencies
         run: opam install . --deps-only --locked --with-test
@@ -85,6 +90,11 @@ jobs:
         uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
+          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
+
+      - name: Install graph-easy # TODO: remove if depext --with-test works
+        if: ${{ matrix.os == 'ubuntu-latest' }}
+        run: sudo apt install -y libgraph-easy-perl
 
       - name: Install spin
         run: sudo apt-get -y install spin
@@ -141,7 +151,7 @@ jobs:
         run: ./make.sh nat
 
       - name: Build Gobview
-        run: opam exec -- dune build gobview
+        run: ./make.sh view
 
       - name: Install selenium
         run: pip3 install selenium webdriver-manager

.github/workflows/unlocked.yml

@@ -49,6 +49,11 @@ jobs:
         uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
+          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
+
+      - name: Install graph-easy # TODO: remove if depext --with-test works
+        if: ${{ matrix.os == 'ubuntu-latest' }}
+        run: sudo apt install -y libgraph-easy-perl
 
       - name: Install dependencies
         run: opam install . --deps-only --with-test
@@ -57,7 +62,7 @@ jobs:
         if: ${{ matrix.apron }}
         run: |
           opam depext apron
-          opam install apron
+          opam install apron mlgmpidl.1.2.15
 
       - name: Install Z3 dependencies
         if: ${{ matrix.z3 }}
@@ -105,14 +110,19 @@ jobs:
         uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
+          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
+
+      - name: Install graph-easy # TODO: remove if depext --with-test works
+        if: ${{ matrix.os == 'ubuntu-latest' }}
+        run: sudo apt install -y libgraph-easy-perl
 
       - name: Install dependencies
         run: opam install . --deps-only --with-test
 
       - name: Install Apron dependencies
         run: |
           opam depext apron
-          opam install apron
+          opam install apron mlgmpidl.1.2.15
 
       - name: Build
         if: ${{ false }}
@@ -193,14 +203,19 @@ jobs:
         uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
+          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
+
+      - name: Install graph-easy # TODO: remove if depext --with-test works
+        if: ${{ matrix.os == 'ubuntu-latest' }}
+        run: sudo apt install -y libgraph-easy-perl
 
       - name: Install Goblint with test
         run: opam install goblint --with-test
 
       - name: Install Apron dependencies
         run: |
           opam depext apron
-          opam install apron
+          opam install apron mlgmpidl.1.2.15
 
       - name: Symlink installed goblint to repository # because tests want to use locally built one
         run: ln -s $(opam exec -- which goblint) goblint

.gitignore

@@ -10,6 +10,7 @@ goblint
 goblint.byte
 goblint.json
 goblint.domaintest
+goblint_http.exe
 src/config*.ml
 tests/bench.txt
 .DS_Store

docs/user-guide/inspecting.md

@@ -18,11 +18,10 @@ For the initial setup:
 
 To build GobView (also for development):
 
-1. Run `dune build gobview` in the analyzer directory to build the web UI
-2. The executable for the http-server can then be found in the directory `./_build/default/gobview/goblint-http-server`. It takes the analyzer directory and additional Goblint configurations such as the files to be analyzed as parameters. Run it e.g. with the following command:\
-`./_build/default/gobview/goblint-http-server/goblint_http.exe -with-goblint ../analyzer/goblint -goblint --set files[+] "../analyzer/tests/regression/00-sanity/01-assert.c"`
-
-4. Visit <http://localhost:8080>
+1. Run `make view` in the analyzer directory to build the web UI
+2. The executable `goblint_http.exe` takes the analyzer directory and additional Goblint configurations such as the files to be analyzed as parameters. Run it e.g. with the following command:\
+`./goblint_http.exe tests/regression/00-sanity/01-assert.c`
+3. Visit <http://localhost:8080>
 
 ## Witnesses
 

dune-project

@@ -59,6 +59,7 @@
   )
   (conflicts
     (result (< 1.5)) ; transitive dependency, overrides standard Result module and doesn't have map_error, bind
+    (ez-conf-lib (= 1)) ; https://github.com/nberth/ez-conf-lib/issues/3
   )
   (sites
     (share lib)

goblint.opam

@@ -54,6 +54,7 @@ depends: [
 depopts: ["apron" "z3"]
 conflicts: [
   "result" {< "1.5"}
+  "ez-conf-lib" {= "1"}
 ]
 build: [
   ["dune" "subst"] {dev}
@@ -77,10 +78,13 @@ 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#3cb720fe333289aca998d67bd210c57a87248c51" ]
+  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#833378d9102578bab7b62174cb029d385db417a5" ]
   # 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}
+]
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]

goblint.opam.locked

@@ -125,6 +125,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 available: os-distribution != "alpine" & arch != "arm64"
 conflicts: [
   "result" {< "1.5"}
+  "ez-conf-lib" {= "1"}
 ]
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
@@ -133,10 +134,11 @@ post-messages: [
 pin-depends: [
   [
     "goblint-cil.2.0.3"
-    "git+https://github.com/goblint/cil.git#3cb720fe333289aca998d67bd210c57a87248c51"
+    "git+https://github.com/goblint/cil.git#833378d9102578bab7b62174cb029d385db417a5"
   ]
   [
     "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.template

@@ -3,10 +3,13 @@
 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#3cb720fe333289aca998d67bd210c57a87248c51" ]
+  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#833378d9102578bab7b62174cb029d385db417a5" ]
   # 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}
+]
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]

make.sh

@@ -17,7 +17,6 @@ rule() {
     clean)
       git clean -X -f
       dune clean
-    ;; gen) gen
     ;; nat*)
       eval $(opam config env)
       dune build $TARGET.exe &&
@@ -33,10 +32,9 @@ rule() {
       dune build --profile=release $TARGET.exe &&
       rm -f goblint &&
       cp _build/default/$TARGET.exe goblint
-    # alternatives to .exe: .bc (bytecode), .bc.js (js_of_ocaml), see https://dune.readthedocs.io/en/stable/dune-files.html#executable
-    ;; js) # https://dune.readthedocs.io/en/stable/jsoo.html
-      dune build $TARGET.bc.js &&
-      node _build/default/$TARGET.bc.js
+    ;; view)
+      eval $(opam config env)
+      dune build gobview
     ;; watch)
       eval $(opam config env)
       # dune build -w $TARGET.exe
@@ -61,8 +59,6 @@ rule() {
       dune build goblint.byte &&
       rm -f goblint.byte &&
       cp _build/default/goblint.byte goblint.byte
-    # ;; tag*)
-    #   otags -vi `find src/ -iregex [^.]*\.mli?`
 
     # setup, dependencies
     ;; deps)
@@ -98,8 +94,6 @@ rule() {
       tar xf master.tar.gz && rm master.tar.gz
       rm -rf linux-headers && mv linux-headers-master linux-headers
       for n in $(compgen -c gcc- | sed 's/gcc-//'); do if [ $n != 5 ]; then cp -n linux-headers/include/linux/compiler-gcc{5,$n}.h; fi; done
-    ;; lock)
-      opam lock
     ;; npm)
       if test ! -e "webapp/package.json"; then
         git submodule update --init --recursive webapp
@@ -115,8 +109,6 @@ rule() {
     ;; setup_gobview )
       [[ -f gobview/gobview.opam ]] || git submodule update --init gobview
       opam install --deps-only --locked gobview/
-    # ;; watch)
-    #   fswatch --event Updated -e $TARGET.ml src/ | xargs -n1 -I{} make
     ;; install)
       eval $(opam config env)
       dune build @install
@@ -141,20 +133,10 @@ rule() {
       cp _opam/share/apron/lib/libboxD.so $PREFIX/share/apron/lib/
       cp _opam/share/apron/lib/libpolkaMPQ.so $PREFIX/share/apron/lib/
 
-    # tests, CI
+    # tests
     ;; test)
       eval $(opam env)
       dune runtest
-    ;; travis) # run a travis docker container with the files tracked by git - intended to debug setup problems on travis-ci.com
-      echo "run ./scripts/travis-ci.sh to setup ocaml"
-      # echo "bind-mount cwd: beware that cwd of host can be modified and IO is very slow!"
-      # docker run -it -u travis -v $(pwd):$(pwd):delegated -w $(pwd) travisci/ci-garnet:packer-1515445631-7dfb2e1 bash
-      echo "copy cwd w/o git-ignored files: changes in container won't affect host's cwd."
-      # cp cwd (with .git, _opam, _build): 1m51s, cp ls-files: 0.5s
-      docker run -it -u travis -v `pwd`:/analyzer:ro,delegated -w /home/travis travisci/ci-garnet:packer-1515445631-7dfb2e1 bash -c 'cd /analyzer; mkdir ~/a; cp --parents $(git ls-files) ~/a; cd ~/a; bash'
-    ;; server)
-      rsync -avz --delete --exclude='/.git' --exclude='server.sh' --exclude-from="$(git ls-files --exclude-standard -oi --directory > /tmp/excludes; echo /tmp/excludes)" . serverseidl6.informatik.tu-muenchen.de:~/analyzer2
-      ssh serverseidl6.informatik.tu-muenchen.de 'cd ~/analyzer2; make nat && make test'
 
     ;; *)
       echo "Unknown action '$1'. Try clean, native, byte, profile or doc.";;

scripts/test-gobview.py

@@ -24,10 +24,8 @@ def cleanup(browser, thread):
 # serve GobView in different thread so it does not block the testing
 def serve():
   global p
-  goblint_http_path = '_build/default/gobview/goblint-http-server/goblint_http.exe'
-  p = subprocess.Popen(['./' + goblint_http_path,
-                  '-with-goblint', '../analyzer/goblint',
-                  '-goblint', '--set', 'files[+]', '"../analyzer/tests/regression/00-sanity/01-assert.c"'])
+  goblint_http_path = './goblint_http.exe'
+  p = subprocess.Popen([goblint_http_path, 'tests/regression/00-sanity/01-assert.c'])
 
 print("serving at port", PORT)
 thread = Thread(target=serve, args=())

src/cdomain/value/domains/invariantCil.ml

@@ -21,7 +21,11 @@ let exp_replace_original_name e =
 let var_is_in_scope scope vi =
   match Cilfacade.find_scope_fundec vi with
   | None -> vi.vstorage <> Static (* CIL pulls static locals into globals, but they aren't syntactically in global scope *)
-  | Some fd -> CilType.Fundec.equal fd scope
+  | Some fd -> 
+    if CilType.Fundec.equal fd scope then
+      GobConfig.get_bool "witness.invariant.all-locals" || (not @@ hasAttribute "goblint_cil_nested" vi.vattr)
+    else
+      false
 
 class exp_is_in_scope_visitor (scope: fundec) (acc: bool ref) = object
   inherit nopCilVisitor

src/common/common.mld

@@ -54,6 +54,7 @@ XmlUtil
 {!modules:
 CilType
 Cilfacade
+CilLocation
 RichVarinfo
 }
 

src/common/framework/cfgTools.ml

@@ -619,6 +619,12 @@ let getCFG (file: file) : cfg * cfg * stmt list CfgEdgeH.t =
   if get_bool "justcfg" then fprint_hash_dot cfgB;
   (fun n -> H.find_default cfgF n []), (fun n -> H.find_default cfgB n []), skippedByEdge
 
+let compute_cfg_skips file =
+  let cfgF, cfgB, skippedByEdge = getCFG file in
+  (module struct let prev = cfgB let next = cfgF end : CfgBidir), skippedByEdge
+
+let compute_cfg file = fst (compute_cfg_skips file)
+
 
 let iter_fd_edges (module Cfg : CfgBackward) fd =
   let ready      = NH.create 113 in

src/common/util/cilCfg0.ml

@@ -0,0 +1,24 @@
+(** CIL CFG functions to avoid dependency problems. *)
+
+open GoblintCil
+
+class allBBVisitor = object (* puts every instruction into its own basic block *)
+  inherit nopCilVisitor
+  method! vstmt s =
+    match s.skind with
+    | Instr(il) ->
+      let list_of_stmts =
+        List.map (fun one_inst -> mkStmtOneInstr one_inst) il in
+      let block = mkBlock list_of_stmts in
+      ChangeDoChildrenPost(s, (fun _ -> s.skind <- Block(block); s))
+    | _ -> DoChildren
+
+  method! vvdec _ = SkipChildren
+  method! vexpr _ = SkipChildren
+  method! vlval _ = SkipChildren
+  method! vtype _ = SkipChildren
+end
+
+let end_basic_blocks f =
+  let thisVisitor = new allBBVisitor in
+  visitCilFileSameGlobals thisVisitor f