diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml index d4fc872620..7f6d5a1cfb 100644 --- a/.github/workflows/coverage.yml +++ b/.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 }} @@ -35,10 +35,9 @@ jobs: # otherwise setup-ocaml pins non-locked dependencies # https://github.com/ocaml/setup-ocaml/issues/166 OPAMLOCKED: locked - uses: ocaml/setup-ocaml@v2 + uses: ocaml/setup-ocaml@v3 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' }} diff --git a/.github/workflows/docker.yml b/.github/workflows/docker.yml index 36568e6cb2..daa7f224b8 100644 --- a/.github/workflows/docker.yml +++ b/.github/workflows/docker.yml @@ -59,7 +59,7 @@ jobs: - name: Build Docker image id: build - uses: docker/build-push-action@v5 + uses: docker/build-push-action@v6 with: context: . load: true # load into docker instead of immediately pushing @@ -72,7 +72,7 @@ jobs: run: docker run --rm -v $(pwd):/data ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:${{ steps.meta.outputs.version }} /data/tests/regression/04-mutex/01-simple_rc.c # run image by version in case multiple tags - name: Push Docker image - uses: docker/build-push-action@v5 + uses: docker/build-push-action@v6 with: context: . push: true diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 242acef3de..c5b414a741 100644 --- a/.github/workflows/docs.yml +++ b/.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 }} @@ -35,7 +35,7 @@ jobs: # otherwise setup-ocaml pins non-locked dependencies # https://github.com/ocaml/setup-ocaml/issues/166 OPAMLOCKED: locked - uses: ocaml/setup-ocaml@v2 + uses: ocaml/setup-ocaml@v3 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} diff --git a/.github/workflows/indentation.yml b/.github/workflows/indentation.yml index e22e674301..96ef5ee56a 100644 --- a/.github/workflows/indentation.yml +++ b/.github/workflows/indentation.yml @@ -25,7 +25,7 @@ jobs: fetch-depth: 0 - name: Set up OCaml ${{ matrix.ocaml-compiler }} - uses: ocaml/setup-ocaml@v2 + uses: ocaml/setup-ocaml@v3 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml index 18935725ca..4f892ea419 100644 --- a/.github/workflows/locked.yml +++ b/.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 }} @@ -37,10 +37,9 @@ jobs: # otherwise setup-ocaml pins non-locked dependencies # https://github.com/ocaml/setup-ocaml/issues/166 OPAMLOCKED: locked - uses: ocaml/setup-ocaml@v2 + uses: ocaml/setup-ocaml@v3 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' }} @@ -73,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 }} @@ -87,10 +86,9 @@ jobs: # otherwise setup-ocaml pins non-locked dependencies # https://github.com/ocaml/setup-ocaml/issues/166 OPAMLOCKED: locked - uses: ocaml/setup-ocaml@v2 + uses: ocaml/setup-ocaml@v3 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' }} @@ -116,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 @@ -132,7 +130,7 @@ jobs: # otherwise setup-ocaml pins non-locked dependencies # https://github.com/ocaml/setup-ocaml/issues/166 OPAMLOCKED: locked - uses: ocaml/setup-ocaml@v2 + uses: ocaml/setup-ocaml@v3 with: ocaml-compiler: ${{ matrix.ocaml-compiler }} diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml index db41ad3007..6a9eced42c 100644 --- a/.github/workflows/unlocked.yml +++ b/.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 @@ -45,10 +45,9 @@ jobs: uses: actions/checkout@v4 - name: Set up OCaml ${{ matrix.ocaml-compiler }} - uses: ocaml/setup-ocaml@v2 + uses: ocaml/setup-ocaml@v3 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' }} @@ -92,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) @@ -109,7 +108,6 @@ 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' }} @@ -133,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 @@ -165,7 +163,7 @@ jobs: - name: Build dev Docker image id: build - uses: docker/build-push-action@v5 + uses: docker/build-push-action@v6 with: context: . target: dev @@ -190,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 }} @@ -199,10 +197,9 @@ jobs: uses: actions/checkout@v4 - name: Set up OCaml ${{ matrix.ocaml-compiler }} - uses: ocaml/setup-ocaml@v2 + uses: ocaml/setup-ocaml@v3 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' }} diff --git a/.zenodo.json b/.zenodo.json index 22705c2d9c..1e71573948 100644 --- a/.zenodo.json +++ b/.zenodo.json @@ -23,6 +23,11 @@ "affiliation": "Technische Universität München", "orcid": "0009-0009-9644-7475" }, + { + "name": "Holter, Karoliine", + "affiliation": "University of Tartu", + "orcid": "0009-0008-3725-4131" + }, { "name": "Vogler, Ralf", "affiliation": "Technische Universität München" diff --git a/CITATION.cff b/CITATION.cff index 25d46cf762..7a93859c54 100644 --- a/CITATION.cff +++ b/CITATION.cff @@ -21,6 +21,10 @@ authors: # same authors as in .zenodo.json and dune-project family-names: Tilscher affiliation: "Technische Universität München" orcid: "https://orcid.org/0009-0009-9644-7475" + - given-names: Karoliine + family-names: Holter + affiliation: "University of Tartu" + orcid: "https://orcid.org/0009-0008-3725-4131" - given-names: Ralf family-names: Vogler affiliation: "Technische Universität München" diff --git a/conf/examples/medium-program.json b/conf/examples/medium-program.json index 2c1e7c7346..5afc1aa2f8 100644 --- a/conf/examples/medium-program.json +++ b/conf/examples/medium-program.json @@ -9,6 +9,7 @@ "base", "threadid", "threadflag", + "threadreturn", "mallocWrapper", "mutexEvents", "mutex", @@ -18,6 +19,7 @@ "expRelation", "mhp", "assert", + "pthreadMutexType", "var_eq", "symb_locks", "region", diff --git a/conf/examples/very-precise.json b/conf/examples/very-precise.json index 2197335eaf..074d448a85 100644 --- a/conf/examples/very-precise.json +++ b/conf/examples/very-precise.json @@ -22,6 +22,7 @@ "base", "threadid", "threadflag", + "threadreturn", "mallocWrapper", "mutexEvents", "mutex", @@ -31,6 +32,7 @@ "expRelation", "mhp", "assert", + "pthreadMutexType", "var_eq", "symb_locks", "region", diff --git a/docs/developer-guide/firstanalysis.md b/docs/developer-guide/firstanalysis.md index 4eb35e7f5d..bd4dfb3c11 100644 --- a/docs/developer-guide/firstanalysis.md +++ b/docs/developer-guide/firstanalysis.md @@ -35,7 +35,7 @@ This program is in the Goblint repository: `tests/regression/99-tutorials/01-fir But if you run Goblint out of the box on this example, it will not work: ```console -./goblint --enable warn.debug tests/regression/99-tutorials/01-first.c +./goblint tests/regression/99-tutorials/01-first.c ``` This will claim that the assertion in unknown. @@ -74,10 +74,10 @@ For more information on the signature of the individual transfer functions, plea ## Extending the domain You could now enrich the lattice to also have a representation for non-negative (i.e., zero or positive) values. -Then the join of `Zero` and `Pos` would be "non-negative" instead of `Top`, allowing you to prove that such join is greated than `Neg`. +Then the join of `Zero` and `Pos` would be "non-negative" instead of `Top`, allowing you to prove that such join is greater than `Neg`. For example, have a look at the following program: `tests/regression/99-tutorials/02-first-extend.c`. _Hint:_ The easiest way to do this is to use the powerset lattice of `{-, 0, +}`. For example, "non-negative" is represented by `{0, +}`, while negative is represented by `{-}`. -To do this, modify `SL` by using `SetDomain.FiniteSet` (takes a `struct` with a list of finite elements as second parameter) instead of `Lattice.Flat` and reimplementing the two functions using `singleton` and `for_all`. +To do this, modify `SL` by using `SetDomain.FiniteSet` (which needs a finite list of elements to be added to `Signs`) instead of `Lattice.Flat` and reimplementing the two functions using `singleton` and `for_all`. diff --git a/docs/user-guide/assumptions.md b/docs/user-guide/assumptions.md index f77e3b5097..33284ccc00 100644 --- a/docs/user-guide/assumptions.md +++ b/docs/user-guide/assumptions.md @@ -17,3 +17,22 @@ _NB! This list is likely incomplete._ See [PR #1414](https://github.com/goblint/analyzer/pull/1414). +2. Pointer arithmetic does not overflow. + + [C11's N1570][n1570] at 6.5.6.8 states that + + > When an expression that has integer type is added to or subtracted from a pointer, the result has the type of the pointer operand. + > [...] + > the evaluation shall not produce an overflow; otherwise, the behavior is undefined. + + after a long list of defined behaviors. + + Goblint does not report overflow and out-of-bounds pointer arithmetic (when the pointer _is not dereferenced_). + This affects the overflow analysis (SV-COMP no-overflow property) in the `base` analysis. + + This _does not_ affect the `memOutOfBounds` analysis (SV-COMP valid-memsafety property), which is for undefined behavior from _dereferencing_ such out-of-bounds pointers. + + See [PR #1511](https://github.com/goblint/analyzer/pull/1511). + + +[n1570]: https://www.open-std.org/jtc1/sc22/wg14/www/docs/n1570.pdf diff --git a/dune-project b/dune-project index 878abd3b4f..3927e77bdd 100644 --- a/dune-project +++ b/dune-project @@ -15,13 +15,26 @@ (source (github goblint/analyzer)) (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 +(authors "Simmo Saan" "Michael Schwarz" "Julian Erhard" "Sarah Tilscher" "Karoliine Holter" "Ralf Vogler" "Kalmer Apinis" "Vesal Vojdani" ) ; same authors as in .zenodo.json and CITATION.cff (maintainers "Simmo Saan " "Michael Schwarz " "Karoliine Holter") (license MIT) (package (name goblint) (synopsis "Static analysis framework for C") + (description "\ +Goblint is a sound static analysis framework for C programs using abstract interpretation. +It specializes in thread-modular verification of multi-threaded programs, especially regarding data races. +Goblint includes analyses for assertions, overflows, deadlocks, etc and can be extended with new analyses. +") + (tags ( + "program analysis" + "program verification" + "static analysis" + "abstract interpretation" + "C" + "data race analysis" + "concurrency")) (depends (ocaml (>= 4.14)) (goblint-cil (>= 2.0.3)) ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint. @@ -29,7 +42,7 @@ (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) @@ -54,7 +67,7 @@ conf-gcc ; ensures opam-repository CI installs real gcc from homebrew on MacOS ) (depopts - apron + (apron (>= v0.9.15)) z3 ) (conflicts diff --git a/goblint.opam b/goblint.opam index 9a26d2596f..7fe108f682 100644 --- a/goblint.opam +++ b/goblint.opam @@ -1,6 +1,11 @@ # This file is generated by dune, edit dune-project instead opam-version: "2.0" synopsis: "Static analysis framework for C" +description: """ +Goblint is a sound static analysis framework for C programs using abstract interpretation. +It specializes in thread-modular verification of multi-threaded programs, especially regarding data races. +Goblint includes analyses for assertions, overflows, deadlocks, etc and can be extended with new analyses. +""" maintainer: [ "Simmo Saan " "Michael Schwarz " @@ -11,11 +16,21 @@ authors: [ "Michael Schwarz" "Julian Erhard" "Sarah Tilscher" + "Karoliine Holter" "Ralf Vogler" "Kalmer Apinis" "Vesal Vojdani" ] license: "MIT" +tags: [ + "program analysis" + "program verification" + "static analysis" + "abstract interpretation" + "C" + "data race analysis" + "concurrency" +] homepage: "https://goblint.in.tum.de" doc: "https://goblint.readthedocs.io/en/latest/" bug-reports: "https://github.com/goblint/analyzer/issues" @@ -27,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} @@ -51,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"} @@ -78,9 +96,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#079b426b5cf6ebeade55f11de0b33d6e63ab50b6" ] - # 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-cil.2.0.3" "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f" ] ] depexts: [ ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test} diff --git a/goblint.opam.locked b/goblint.opam.locked index 5526a26b56..2973619808 100644 --- a/goblint.opam.locked +++ b/goblint.opam.locked @@ -12,6 +12,7 @@ authors: [ "Michael Schwarz" "Julian Erhard" "Sarah Tilscher" + "Karoliine Holter" "Ralf Vogler" "Kalmer Apinis" "Vesal Vojdani" @@ -21,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} @@ -136,9 +142,18 @@ pin-depends: [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#079b426b5cf6ebeade55f11de0b33d6e63ab50b6" ] - [ - "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 is a sound static analysis framework for C programs using abstract interpretation. +It specializes in thread-modular verification of multi-threaded programs, especially regarding data races. +Goblint includes analyses for assertions, overflows, deadlocks, etc and can be extended with new analyses.""" +tags: [ + "program analysis" + "program verification" + "static analysis" + "abstract interpretation" + "C" + "data race analysis" + "concurrency" +] diff --git a/goblint.opam.template b/goblint.opam.template index abd21204c9..a730d5c064 100644 --- a/goblint.opam.template +++ b/goblint.opam.template @@ -3,9 +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#079b426b5cf6ebeade55f11de0b33d6e63ab50b6" ] - # 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-cil.2.0.3" "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f" ] ] depexts: [ ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test} diff --git a/gobview b/gobview index 72abbb576b..03b0682f97 160000 --- a/gobview +++ b/gobview @@ -1 +1 @@ -Subproject commit 72abbb576b8ffc8759dcfa31501738f6b561b05a +Subproject commit 03b0682f973eab0d26cf8aea74c63a9e869c9716 diff --git a/make.sh b/make.sh index 5b55e51beb..0f76759065 100755 --- a/make.sh +++ b/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() { diff --git a/scripts/creduce/privPrecCompare.sh b/scripts/creduce/privPrecCompare.sh index fdc5f9219d..2165112924 100755 --- a/scripts/creduce/privPrecCompare.sh +++ b/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 diff --git a/scripts/privPrecCompare.sh b/scripts/privPrecCompare.sh index c5b9f2c01e..2b09fb80b5 100755 --- a/scripts/privPrecCompare.sh +++ b/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? diff --git a/scripts/test-gobview.py b/scripts/test-gobview.py index f5961108d7..10808a9b62 100644 --- a/scripts/test-gobview.py +++ b/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() diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index 5935627148..71340be583 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/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 @@ -388,11 +388,11 @@ struct let st = ctx.local in let reachable_from_args = reachable_from_args ctx args in let fundec = Node.find_fundec ctx.node in - if M.tracing then M.tracel "combine" "relation f: %a" CilType.Varinfo.pretty f.svar; - if M.tracing then M.tracel "combine" "relation formals: %a" (d_list "," CilType.Varinfo.pretty) f.sformals; - if M.tracing then M.tracel "combine" "relation args: %a" (d_list "," d_exp) args; - if M.tracing then M.tracel "combine" "relation st: %a" D.pretty st; - if M.tracing then M.tracel "combine" "relation fun_st: %a" D.pretty fun_st; + if M.tracing then M.tracel "combine-rel" "relation f: %a" CilType.Varinfo.pretty f.svar; + if M.tracing then M.tracel "combine-rel" "relation formals: %a" (d_list "," CilType.Varinfo.pretty) f.sformals; + if M.tracing then M.tracel "combine-rel" "relation args: %a" (d_list "," d_exp) args; + if M.tracing then M.tracel "combine-rel" "relation st: %a" D.pretty st; + if M.tracing then M.tracel "combine-rel" "relation fun_st: %a" D.pretty fun_st; let new_fun_rel = RD.add_vars fun_st.rel (RD.vars st.rel) in let arg_substitutes = let filter_actuals (x,e) = @@ -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" "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 @@ -432,7 +432,7 @@ struct ) in let unify_rel = RD.unify new_rel new_fun_rel in (* TODO: unify_with *) - if M.tracing then M.tracel "combine" "relation unifying %a %a = %a" RD.pretty new_rel RD.pretty new_fun_rel RD.pretty unify_rel; + if M.tracing then M.tracel "combine-rel" "relation unifying %a %a = %a" RD.pretty new_rel RD.pretty new_fun_rel RD.pretty unify_rel; {fun_st with rel = unify_rel} let combine_assign ctx r fe f args fc fun_st (f_ask : Queries.ask) = @@ -694,15 +694,18 @@ struct ctx.local let event ctx e octx = + let ask = Analyses.ask_of_ctx ctx in let st = ctx.local in match e with - | Events.Lock (addr, _) when ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) - Priv.lock (Analyses.ask_of_ctx ctx) ctx.global st addr - | Events.Unlock addr when ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) - if addr = UnknownPtr then - M.info ~category:Unsound "Unknown mutex unlocked, relation privatization unsound"; (* TODO: something more sound *) + | Events.Lock (addr, _) when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *) + CommonPriv.lift_lock ask (fun st m -> + Priv.lock ask ctx.global st m + ) st addr + | Events.Unlock addr when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *) WideningTokens.with_local_side_tokens (fun () -> - Priv.unlock (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st addr + CommonPriv.lift_unlock ask (fun st m -> + Priv.unlock ask ctx.global ctx.sideg st m + ) st addr ) | Events.EnterMultiThreaded -> Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st @@ -765,7 +768,7 @@ struct let sync ctx reason = (* After the solver is finished, store the results (for later comparison) *) - if !AnalysisState.postsolving then begin + if !AnalysisState.postsolving && GobConfig.get_string "exp.relation.prec-dump" <> "" then begin let keep_local = GobConfig.get_bool "ana.relation.invariant.local" in let keep_global = GobConfig.get_bool "ana.relation.invariant.global" in @@ -781,7 +784,7 @@ struct PCU.RH.replace results ctx.node new_value; end; WideningTokens.with_local_side_tokens (fun () -> - Priv.sync (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg ctx.local (reason :> [`Normal | `Join | `Return | `Init | `Thread]) + Priv.sync (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg ctx.local (reason :> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread]) ) let init marshal = diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index b8a439fc59..9b25abb371 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -33,10 +33,10 @@ module type S = the state when following conditional guards. *) val write_global: ?invariant:bool -> Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> varinfo -> varinfo -> relation_components_t - val lock: Q.ask -> (V.t -> G.t) -> relation_components_t -> LockDomain.Addr.t -> relation_components_t - val unlock: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> LockDomain.Addr.t -> relation_components_t + val lock: Q.ask -> (V.t -> G.t) -> relation_components_t -> LockDomain.MustLock.t -> relation_components_t + val unlock: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> LockDomain.MustLock.t -> relation_components_t - val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> [`Normal | `Join | `Return | `Init | `Thread] -> relation_components_t + val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread] -> relation_components_t val escape: Node.t -> Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> EscapeDomain.EscapedVars.t -> relation_components_t val enter_multithreaded: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> relation_components_t @@ -99,8 +99,7 @@ struct { st with rel = rel_local } let sync (ask: Q.ask) getg sideg (st: relation_components_t) reason = - match reason with - | `Join when ConfCheck.branched_thread_creation () -> + let branched_sync () = if ask.f (Q.MustBeSingleThreaded {since_start = true}) then st else @@ -113,7 +112,14 @@ struct ) in {st with rel = rel_local} + in + match reason with + | `Join when ConfCheck.branched_thread_creation () -> + branched_sync () + | `JoinCall when ConfCheck.branched_thread_creation () -> + branched_sync () | `Join + | `JoinCall | `Normal | `Init | `Thread @@ -341,17 +347,8 @@ struct let thread_join ?(force=false) ask getg exp st = st let thread_return ask getg sideg tid st = st - let sync ask getg sideg (st: relation_components_t) reason = - match reason with - | `Return -> (* required for thread return *) - (* TODO: implement? *) - begin match ThreadId.get_current ask with - | `Lifted x (* when CPA.mem x st.cpa *) -> - st - | _ -> - st - end - | `Join when ConfCheck.branched_thread_creation () -> + let sync (ask:Q.ask) getg sideg (st: relation_components_t) reason = + let branched_sync () = if ask.f (Q.MustBeSingleThreaded { since_start= true }) then st else @@ -380,7 +377,22 @@ struct let rel_local' = RD.meet rel_local (getg ()) in {st with rel = rel_local'} *) st + in + match reason with + | `Return -> (* required for thread return *) + (* TODO: implement? *) + begin match ThreadId.get_current ask with + | `Lifted x (* when CPA.mem x st.cpa *) -> + st + | _ -> + st + end + | `Join when ConfCheck.branched_thread_creation () -> + branched_sync () + | `JoinCall when ConfCheck.branched_thread_creation_at_call ask -> + branched_sync () | `Join + | `JoinCall | `Normal | `Init | `Thread -> @@ -476,7 +488,7 @@ struct let startstate () = () - let atomic_mutex = LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var + let atomic_mutex = LockDomain.MustLock.of_var LibraryFunctions.verifier_atomic_var let get_m_with_mutex_inits ask getg m = let get_m = getg (V.mutex m) in @@ -496,7 +508,7 @@ struct in let get_mutex_inits = getg V.mutex_inits in let get_mutex_inits' = RD.keep_vars get_mutex_inits [g_var] in - if not (RD.mem_var get_mutex_inits' g_var) then (* TODO: is this just a workaround for an escape bug? https://github.com/goblint/analyzer/pull/1354/files#r1498882657 *) + if RD.mem_var get_mutex_global_g g_var && not (RD.mem_var get_mutex_inits' g_var) then (* TODO: is this just a workaround for an escape bug? https://github.com/goblint/analyzer/pull/1354/files#r1498882657 *) (* This is an escaped variable whose value was never side-effected to get_mutex_inits' *) get_mutex_global_g else @@ -582,9 +594,9 @@ struct let write_escape = write_global_internal ~skip_meet:true let lock ask getg (st: relation_components_t) m = - let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in + let atomic = Param.handle_atomic && LockDomain.MustLock.equal m atomic_mutex in (* TODO: somehow actually unneeded here? *) - if not atomic && Locksets.(not (Lockset.mem m (current_lockset ask))) then ( + if not atomic && Locksets.(not (MustLockset.mem m (current_lockset ask))) then ( let rel = st.rel in let get_m = get_m_with_mutex_inits ask getg m in (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *) @@ -597,7 +609,7 @@ struct st (* sound w.r.t. recursive lock *) let unlock ask getg sideg (st: relation_components_t) m: relation_components_t = - let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in + let atomic = Param.handle_atomic && LockDomain.MustLock.equal m atomic_mutex in let rel = st.rel in if not atomic then ( let rel_side = keep_only_protected_globals ask m rel in @@ -631,17 +643,8 @@ struct let thread_join ?(force=false) ask getg exp st = st let thread_return ask getg sideg tid st = st - let sync ask getg sideg (st: relation_components_t) reason = - match reason with - | `Return -> (* required for thread return *) - (* TODO: implement? *) - begin match ThreadId.get_current ask with - | `Lifted x (* when CPA.mem x st.cpa *) -> - st - | _ -> - st - end - | `Join when ConfCheck.branched_thread_creation () -> + let sync (ask:Q.ask) getg sideg (st: relation_components_t) reason = + let branched_sync () = if ask.f (Q.MustBeSingleThreaded {since_start = true}) then st else @@ -664,7 +667,22 @@ struct ) in {st with rel = rel_local} + in + match reason with + | `Return -> (* required for thread return *) + (* TODO: implement? *) + begin match ThreadId.get_current ask with + | `Lifted x (* when CPA.mem x st.cpa *) -> + st + | _ -> + st + end + | `Join when ConfCheck.branched_thread_creation () -> + branched_sync () + | `JoinCall when ConfCheck.branched_thread_creation_at_call ask -> + branched_sync () | `Join + | `JoinCall | `Normal | `Init | `Thread -> @@ -698,7 +716,7 @@ struct let invariant_global (ask: Q.ask) (getg: V.t -> G.t): V.t -> Invariant.t = function | `Left m' -> (* mutex *) - let atomic = LockDomain.Addr.equal m' (LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var) in + 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 @@ -743,7 +761,7 @@ module type ClusterArg = functor (RD: RelationDomain.RD) -> sig module LRD: Lattice.S - val keep_only_protected_globals: Q.ask -> LockDomain.Addr.t -> LRD.t -> LRD.t + val keep_only_protected_globals: Q.ask -> LockDomain.MustLock.t -> LRD.t -> LRD.t val keep_global: varinfo -> LRD.t -> LRD.t val lock: RD.t -> LRD.t -> LRD.t -> RD.t @@ -1002,7 +1020,7 @@ struct let get_m_with_mutex_inits inits ask getg m = let get_m = get_relevant_writes ask m (G.mutex @@ getg (V.mutex m)) in - if M.tracing then M.traceli "relationpriv" "get_m_with_mutex_inits %a\n get=%a" LockDomain.Addr.pretty m LRD.pretty get_m; + if M.tracing then M.traceli "relationpriv" "get_m_with_mutex_inits %a\n get=%a" LockDomain.MustLock.pretty m LRD.pretty get_m; let r = if not inits then get_m @@ -1015,7 +1033,7 @@ struct if M.tracing then M.traceu "relationpriv" "-> %a" LRD.pretty r; r - let atomic_mutex = LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var + let atomic_mutex = LockDomain.MustLock.of_var LibraryFunctions.verifier_atomic_var let get_mutex_global_g_with_mutex_inits inits ask getg g = let get_mutex_global_g = @@ -1128,8 +1146,8 @@ struct {rel = rel_local; priv = (W.add g w,lmust,l)} (* Keep write local as if it were protected by the atomic section. *) let lock ask getg (st: relation_components_t) m = - let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in - if not atomic && Locksets.(not (Lockset.mem m (current_lockset ask))) then ( + let atomic = Param.handle_atomic && LockDomain.MustLock.equal m atomic_mutex in + if not atomic && Locksets.(not (MustLockset.mem m (current_lockset ask))) then ( let rel = st.rel in let _,lmust,l = st.priv in let lm = LLock.mutex m in @@ -1152,7 +1170,7 @@ struct RD.keep_filter oct protected let unlock ask getg sideg (st: relation_components_t) m: relation_components_t = - let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in + let atomic = Param.handle_atomic && LockDomain.MustLock.equal m atomic_mutex in let rel = st.rel in let w,lmust,l = st.priv in if not atomic then ( @@ -1232,9 +1250,7 @@ struct st let sync (ask:Q.ask) getg sideg (st: relation_components_t) reason = - match reason with - | `Return -> st (* TODO: implement? *) - | `Join when ConfCheck.branched_thread_creation () -> + let branched_sync () = if ask.f (Q.MustBeSingleThreaded {since_start = true}) then st else @@ -1249,7 +1265,15 @@ struct ) in {st with rel = rel_local} + in + match reason with + | `Return -> st (* TODO: implement? *) + | `Join when ConfCheck.branched_thread_creation () -> + branched_sync () + | `JoinCall when ConfCheck.branched_thread_creation_at_call ask -> + branched_sync () | `Join + | `JoinCall | `Normal | `Init | `Thread -> @@ -1332,7 +1356,7 @@ struct r let lock ask getg st m = - if M.tracing then M.traceli "relationpriv" "lock %a" LockDomain.Addr.pretty m; + if M.tracing then M.traceli "relationpriv" "lock %a" LockDomain.MustLock.pretty m; if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st; let getg x = let r = getg x in @@ -1344,7 +1368,7 @@ struct r let unlock ask getg sideg st m = - if M.tracing then M.traceli "relationpriv" "unlock %a" LockDomain.Addr.pretty m; + if M.tracing then M.traceli "relationpriv" "unlock %a" LockDomain.MustLock.pretty m; if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st; let getg x = let r = getg x in diff --git a/src/analyses/base.ml b/src/analyses/base.ml index ce42ad75bc..4ae2fc711c 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -17,6 +17,7 @@ module IdxDom = ValueDomain.IndexDomain module AD = ValueDomain.AD module Addr = ValueDomain.Addr module Offs = ValueDomain.Offs +module ZeroInit = ValueDomain.ZeroInit module LF = LibraryFunctions module CArrays = ValueDomain.CArrays module PU = PrecisionUtil @@ -260,6 +261,8 @@ struct (* adds n to the last offset *) let rec addToOffset n (t:typ option) = function | `Index (i, `NoOffset) -> + (* Binary operations on pointer types should not generate warnings in SV-COMP *) + GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> (* If we have arrived at the last Offset and it is an Index, we add our integer to it *) `Index(IdxDom.add i (iDtoIdx n), `NoOffset) | `Field (f, `NoOffset) -> @@ -450,7 +453,7 @@ struct else ctx.local - let sync ctx reason = sync' (reason :> [`Normal | `Join | `Return | `Init | `Thread]) ctx + let sync ctx reason = sync' (reason :> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread]) ctx let publish_all ctx reason = ignore (sync' reason ctx) @@ -2662,7 +2665,7 @@ struct | Some lv -> let heap_var = AD.of_var (heap_var true ctx) in (* ignore @@ printf "alloca will allocate %a bytes\n" ID.pretty (eval_int ~ctx size); *) - set_many ~ctx st [(heap_var, TVoid [], Blob (VD.bot (), eval_int ~ctx st size, true)); + set_many ~ctx st [(heap_var, TVoid [], Blob (VD.bot (), eval_int ~ctx st size, ZeroInit.malloc)); (eval_lv ~ctx st lv, (Cilfacade.typeOfLval lv), Address heap_var)] | _ -> st end @@ -2675,7 +2678,7 @@ struct else AD.of_var (heap_var false ctx) in (* ignore @@ printf "malloc will allocate %a bytes\n" ID.pretty (eval_int ~ctx size); *) - set_many ~ctx st [(heap_var, TVoid [], Blob (VD.bot (), eval_int ~ctx st size, true)); + set_many ~ctx st [(heap_var, TVoid [], Blob (VD.bot (), eval_int ~ctx st size, ZeroInit.malloc)); (eval_lv ~ctx st lv, (Cilfacade.typeOfLval lv), Address heap_var)] | _ -> st end @@ -2692,7 +2695,7 @@ struct let countval = eval_int ~ctx st n in if ID.to_int countval = Some Z.one then ( set_many ~ctx st [ - (add_null (AD.of_var heap_var), TVoid [], Blob (VD.bot (), sizeval, false)); + (add_null (AD.of_var heap_var), TVoid [], Blob (VD.bot (), sizeval, ZeroInit.calloc)); (eval_lv ~ctx st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_var heap_var))) ] ) @@ -2700,7 +2703,7 @@ struct let blobsize = ID.mul (ID.cast_to ik @@ sizeval) (ID.cast_to ik @@ countval) in (* the memory that was allocated by calloc is set to bottom, but we keep track that it originated from calloc, so when bottom is read from memory allocated by calloc it is turned to zero *) set_many ~ctx st [ - (add_null (AD.of_var heap_var), TVoid [], Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.one) (Blob (VD.bot (), blobsize, false)))); + (add_null (AD.of_var heap_var), TVoid [], Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.one) (Blob (VD.bot (), blobsize, ZeroInit.calloc)))); (eval_lv ~ctx st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_mval (heap_var, `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero, `NoOffset))))) ] ) @@ -2723,7 +2726,7 @@ struct let p_addr' = AD.remove NullPtr p_addr in (* realloc with NULL is same as malloc, remove to avoid unknown value from NullPtr access *) let p_addr_get = get ~ctx st p_addr' None in (* implicitly includes join of malloc value (VD.bot) *) let size_int = eval_int ~ctx st size in - let heap_val:value = Blob (p_addr_get, size_int, true) in (* copy old contents with new size *) + let heap_val:value = Blob (p_addr_get, size_int, ZeroInit.malloc) in (* copy old contents with new size *) let heap_addr = AD.of_var (heap_var false ctx) in let heap_addr' = if get_bool "sem.malloc.fail" then @@ -3072,12 +3075,14 @@ struct match e with | Events.Lock (addr, _) when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *) if M.tracing then M.tracel "priv" "LOCK EVENT %a" LockDomain.Addr.pretty addr; - Priv.lock ask (priv_getg ctx.global) st addr + CommonPriv.lift_lock ask (fun st m -> + Priv.lock ask (priv_getg ctx.global) st m + ) st addr | Events.Unlock addr when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *) - if addr = UnknownPtr then - M.info ~category:Unsound "Unknown mutex unlocked, base privatization unsound"; (* TODO: something more sound *) WideningTokens.with_local_side_tokens (fun () -> - Priv.unlock ask (priv_getg ctx.global) (priv_sideg ctx.sideg) st addr + CommonPriv.lift_unlock ask (fun st m -> + Priv.unlock ask (priv_getg ctx.global) (priv_sideg ctx.sideg) st m + ) st addr ) | Events.Escape escaped -> Priv.escape ask (priv_getg ctx.global) (priv_sideg ctx.sideg) st escaped diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 241d8d3826..347a365778 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -28,10 +28,10 @@ sig * the state when following conditional guards. *) val write_global: ?invariant:bool -> Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> varinfo -> VD.t -> BaseComponents (D).t - val lock: Q.ask -> (V.t -> G.t) -> BaseComponents (D).t -> LockDomain.Addr.t -> BaseComponents (D).t - val unlock: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> LockDomain.Addr.t -> BaseComponents (D).t + val lock: Q.ask -> (V.t -> G.t) -> BaseComponents (D).t -> LockDomain.MustLock.t -> BaseComponents (D).t + val unlock: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> LockDomain.MustLock.t -> BaseComponents (D).t - val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> [`Normal | `Join | `Return | `Init | `Thread] -> BaseComponents (D).t + val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread] -> BaseComponents (D).t val escape: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> EscapeDomain.EscapedVars.t -> BaseComponents (D).t val enter_multithreaded: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> BaseComponents (D).t @@ -191,7 +191,7 @@ struct let get_mutex_inits = getg V.mutex_inits in let is_in_Gm x _ = is_protected_by ask m x in let get_mutex_inits' = CPA.filter is_in_Gm get_mutex_inits in - if M.tracing then M.tracel "priv" "get_m_with_mutex_inits %a:\n get_m: %a\n get_mutex_inits: %a\n get_mutex_inits': %a" LockDomain.Addr.pretty m CPA.pretty get_m CPA.pretty get_mutex_inits CPA.pretty get_mutex_inits'; + if M.tracing then M.tracel "priv" "get_m_with_mutex_inits %a:\n get_m: %a\n get_mutex_inits: %a\n get_mutex_inits': %a" LockDomain.MustLock.pretty m CPA.pretty get_m CPA.pretty get_mutex_inits CPA.pretty get_mutex_inits'; CPA.join get_m get_mutex_inits' (** [get_m_with_mutex_inits] optimized for implementation-specialized [read_global]. *) @@ -281,7 +281,7 @@ struct cpa' *) let lock ask getg (st: BaseComponents (D).t) m = - if Locksets.(not (Lockset.mem m (current_lockset ask))) then ( + if Locksets.(not (MustLockset.mem m (current_lockset ask))) then ( let get_m = get_m_with_mutex_inits ask getg m in (* Really we want is_unprotected, but pthread_cond_wait emits unlock-lock events, where our (necessary) original context still has the mutex, @@ -292,7 +292,7 @@ struct No other privatization uses is_unprotected, so this hack is only needed here. *) let is_in_V x _ = is_protected_by ask m x && is_unprotected_without ask x m in let cpa' = CPA.filter is_in_V get_m in - if M.tracing then M.tracel "priv" "PerMutexOplusPriv.lock m=%a cpa'=%a" LockDomain.Addr.pretty m CPA.pretty cpa'; + if M.tracing then M.tracel "priv" "PerMutexOplusPriv.lock m=%a cpa'=%a" LockDomain.MustLock.pretty m CPA.pretty cpa'; {st with cpa = CPA.fold CPA.add cpa' st.cpa} ) else @@ -301,13 +301,13 @@ struct let unlock ask getg sideg (st: BaseComponents (D).t) m = let is_in_Gm x _ = is_protected_by ask m x in let side_m_cpa = CPA.filter is_in_Gm st.cpa in - if M.tracing then M.tracel "priv" "PerMutexOplusPriv.unlock m=%a side_m_cpa=%a" LockDomain.Addr.pretty m CPA.pretty side_m_cpa; + if M.tracing then M.tracel "priv" "PerMutexOplusPriv.unlock m=%a side_m_cpa=%a" LockDomain.MustLock.pretty m CPA.pretty side_m_cpa; sideg (V.mutex m) side_m_cpa; st let sync ask getg sideg (st: BaseComponents (D).t) reason = - match reason with - | `Join when ConfCheck.branched_thread_creation () -> (* required for branched thread creation *) + let branched_sync () = + (* required for branched thread creation *) let global_cpa = CPA.filter (fun x _ -> is_global ask x && is_unprotected ask x) st.cpa in sideg V.mutex_inits global_cpa; (* must be like enter_multithreaded *) (* TODO: this makes mutex-oplus less precise in 28-race_reach/10-ptrmunge_racefree and 28-race_reach/trylock2_racefree, why? *) @@ -318,7 +318,14 @@ struct sideg (V.global x) (CPA.singleton x v) ) st.cpa; st + in + match reason with + | `Join when ConfCheck.branched_thread_creation () -> + branched_sync () + | `JoinCall when ConfCheck.branched_thread_creation_at_call ask -> + branched_sync () | `Join + | `JoinCall | `Return | `Normal | `Init @@ -334,7 +341,7 @@ struct let invariant_global (ask: Q.ask) getg = function | `Left m' -> (* mutex *) - let atomic = LockDomain.Addr.equal m' (LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var) in + let atomic = LockDomain.MustLock.equal m' (LockDomain.MustLock.of_var LibraryFunctions.verifier_atomic_var) in if atomic || ask.f (GhostVarAvailable (Locked m')) then ( let cpa = get_m_with_mutex_inits ask getg m' in (* TODO: disjunct with mutex_inits instead of join? *) let inv = CPA.fold (fun v _ acc -> @@ -405,14 +412,14 @@ struct cpa' *) let lock (ask: Queries.ask) getg (st: BaseComponents (D).t) m = - if Locksets.(not (Lockset.mem m (current_lockset ask))) then ( + if Locksets.(not (MustLockset.mem m (current_lockset ask))) then ( let get_m = get_m_with_mutex_inits ask getg m in (* Additionally filter get_m in case it contains variables it no longer protects. *) let is_in_Gm x _ = is_protected_by ask m x in let get_m = CPA.filter is_in_Gm get_m in let long_meet m1 m2 = CPA.long_map2 VD.meet m1 m2 in let meet = long_meet st.cpa get_m in - if M.tracing then M.tracel "priv" "LOCK %a:\n get_m: %a\n meet: %a" LockDomain.Addr.pretty m CPA.pretty get_m CPA.pretty meet; + if M.tracing then M.tracel "priv" "LOCK %a:\n get_m: %a\n meet: %a" LockDomain.MustLock.pretty m CPA.pretty get_m CPA.pretty meet; {st with cpa = meet} ) else @@ -432,8 +439,8 @@ struct {st with cpa = cpa'} let sync ask getg sideg (st: BaseComponents (D).t) reason = - match reason with - | `Join when ConfCheck.branched_thread_creation () -> (* required for branched thread creation *) + let branched_sync () = + (* required for branched thread creation *) let global_cpa = CPA.filter (fun x _ -> is_global ask x && is_unprotected ask x) st.cpa in sideg V.mutex_inits global_cpa; (* must be like enter_multithreaded *) @@ -450,7 +457,14 @@ struct ) st.cpa st.cpa in {st with cpa = cpa'} + in + match reason with + | `Join when ConfCheck.branched_thread_creation () -> + branched_sync () + | `JoinCall when ConfCheck.branched_thread_creation_at_call ask -> + branched_sync () | `Join + | `JoinCall | `Return | `Normal | `Init @@ -551,7 +565,7 @@ struct {st with cpa = cpa'; priv = (W.add x w,LMust.add lm lmust,l')} let lock (ask: Queries.ask) getg (st: BaseComponents (D).t) m = - if Locksets.(not (Lockset.mem m (current_lockset ask))) then ( + if Locksets.(not (MustLockset.mem m (current_lockset ask))) then ( let _,lmust,l = st.priv in let lm = LLock.mutex m in let get_m = get_m_with_mutex_inits (not (LMust.mem lm lmust)) ask getg m in @@ -778,7 +792,7 @@ struct let unlock ask getg sideg (st: BaseComponents (D).t) m = let sideg = Wrapper.sideg ask sideg in - let atomic = Param.handle_atomic && LockDomain.Addr.equal m (LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var) in + let atomic = Param.handle_atomic && LockDomain.MustLock.equal m (LockDomain.MustLock.of_var LibraryFunctions.verifier_atomic_var) in (* TODO: what about G_m globals in cpa that weren't actually written? *) CPA.fold (fun x v (st: BaseComponents (D).t) -> if is_protected_by ask m x then ( (* is_in_Gm *) @@ -800,9 +814,9 @@ struct ) st.cpa st let sync ask getg sideg (st: BaseComponents (D).t) reason = - let sideg = Wrapper.sideg ask sideg in - match reason with - | `Join when ConfCheck.branched_thread_creation () -> (* required for branched thread creation *) + let branched_sync () = + (* required for branched thread creation *) + let sideg = Wrapper.sideg ask sideg in CPA.fold (fun x v (st: BaseComponents (D).t) -> if is_global ask x && is_unprotected ask x then ( sideg (V.unprotected x) v; @@ -812,7 +826,14 @@ struct else st ) st.cpa st + in + match reason with + | `Join when ConfCheck.branched_thread_creation () -> + branched_sync () + | `JoinCall when ConfCheck.branched_thread_creation_at_call ask -> + branched_sync () | `Join + | `JoinCall | `Return | `Normal | `Init @@ -876,8 +897,7 @@ struct but conjunction is unsound when one of the mutexes is temporarily unlocked. Hypothetical read-protection is also somehow relevant. *) LockDomain.MustLockset.fold (fun m acc -> - let m: LockDomain.Addr.t = Addr (LockDomain.MustLock.to_mval m) in (* TODO: don't convert *) - if LockDomain.Addr.equal m (LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var) then + if LockDomain.MustLock.equal m (LockDomain.MustLock.of_var LibraryFunctions.verifier_atomic_var) then acc else if ask.f (GhostVarAvailable (Locked m)) then ( let var = WitnessGhost.to_varinfo (Locked m) in @@ -897,12 +917,12 @@ struct module GWeak = struct - include MapDomain.MapBot (Lockset) (WeakRange) + include MapDomain.MapBot (MustLockset) (WeakRange) let name () = "weak" end module GSync = struct - include MapDomain.MapBot (Lockset) (SyncRange) + include MapDomain.MapBot (MustLockset) (SyncRange) let name () = "synchronized" end module G = @@ -958,7 +978,7 @@ struct let invariant_vars ask getg st = let module VS = Set.Make (CilType.Varinfo) in let s = current_lockset ask in - Lockset.fold (fun m acc -> + MustLockset.fold (fun m acc -> GSync.fold (fun s' cpa' acc -> SyncRange.fold_sync_vars VS.add cpa' acc ) (G.sync (getg (V.mutex m))) acc @@ -1037,7 +1057,7 @@ struct let read_global ask getg (st: BaseComponents (D).t) x = let s = current_lockset ask in GWeak.fold (fun s' tm acc -> - if Lockset.disjoint s s' then + if MustLockset.disjoint s s' then ThreadMap.fold (fun t' v acc -> VD.join v acc ) tm acc @@ -1057,7 +1077,7 @@ struct let lock ask getg (st: BaseComponents (D).t) m = let s = current_lockset ask in let cpa' = GSync.fold (fun s' cpa' acc -> - if Lockset.disjoint s s' then + if MustLockset.disjoint s s' then CPA.join cpa' acc else acc @@ -1066,13 +1086,13 @@ struct {st with cpa = cpa'} let unlock ask getg sideg (st: BaseComponents (D).t) m = - let s = Lockset.remove m (current_lockset ask) in + let s = MustLockset.remove m (current_lockset ask) in let t = current_thread ask in let side_cpa = CPA.filter (fun x _ -> GWeak.fold (fun s' tm acc -> (* TODO: swap 2^M and T partitioning for lookup by t here first? *) let v = ThreadMap.find t tm in - (Lockset.mem m s' && not (VD.is_bot v)) || acc + (MustLockset.mem m s' && not (VD.is_bot v)) || acc ) (G.weak (getg (V.global x))) false ) st.cpa in @@ -1084,6 +1104,7 @@ struct | `Return | `Normal | `Join (* TODO: no problem with branched thread creation here? *) + | `JoinCall | `Init | `Thread -> st @@ -1098,7 +1119,7 @@ struct let read_global ask getg (st: BaseComponents (D).t) x = let s = current_lockset ask in GWeak.fold (fun s' v acc -> - if Lockset.disjoint s s' then + if MustLockset.disjoint s s' then VD.join v acc else acc @@ -1115,7 +1136,7 @@ struct let lock ask getg (st: BaseComponents (D).t) m = let s = current_lockset ask in let cpa' = GSync.fold (fun s' cpa' acc -> - if Lockset.disjoint s s' then + if MustLockset.disjoint s s' then CPA.join cpa' acc else acc @@ -1124,10 +1145,10 @@ struct {st with cpa = cpa'} let unlock ask getg sideg (st: BaseComponents (D).t) m = - let s = Lockset.remove m (current_lockset ask) in + let s = MustLockset.remove m (current_lockset ask) in let side_cpa = CPA.filter (fun x _ -> GWeak.fold (fun s' v acc -> - (Lockset.mem m s' && not (VD.is_bot v)) || acc + (MustLockset.mem m s' && not (VD.is_bot v)) || acc ) (G.weak (getg (V.global x))) false ) st.cpa in @@ -1139,6 +1160,7 @@ struct | `Return | `Normal | `Join (* TODO: no problem with branched thread creation here? *) + | `JoinCall | `Init | `Thread -> st @@ -1169,7 +1191,7 @@ struct let read_global ask getg (st: BaseComponents (D).t) x = let s = current_lockset ask in GWeak.fold (fun s' v acc -> - if Lockset.disjoint s s' then + if MustLockset.disjoint s s' then VD.join v acc else acc @@ -1190,7 +1212,7 @@ struct let lock ask getg (st: BaseComponents (D).t) m = let s = current_lockset ask in let cpa' = GSync.fold (fun s' cpa' acc -> - if Lockset.disjoint s s' then + if MustLockset.disjoint s s' then CPA.join cpa' acc else acc @@ -1199,7 +1221,7 @@ struct {st with cpa = cpa'} let unlock ask getg sideg (st: BaseComponents (D).t) m = - let s = Lockset.remove m (current_lockset ask) in + let s = MustLockset.remove m (current_lockset ask) in let is_in_W x _ = W.mem x st.priv in let side_cpa = CPA.filter is_in_W st.cpa in sideg (V.mutex m) (G.create_sync (GSync.singleton s side_cpa)); @@ -1210,6 +1232,7 @@ struct | `Return | `Normal | `Join (* TODO: no problem with branched thread creation here? *) + | `JoinCall | `Init | `Thread -> st @@ -1219,7 +1242,7 @@ struct if Param.side_effect_global_init then ( CPA.fold (fun x v (st: BaseComponents (D).t) -> if is_global ask x then ( - sideg (V.global x) (G.create_weak (GWeak.singleton (Lockset.empty ()) v)); + sideg (V.global x) (G.create_weak (GWeak.singleton (MustLockset.empty ()) v)); {st with priv = W.add x st.priv} (* TODO: is this add necessary? *) ) else @@ -1242,13 +1265,13 @@ struct module DV = struct - include MapDomain.MapBot_LiftTop (Lock) (MustVars) + include MapDomain.MapBot_LiftTop (LockDomain.MustLock) (MustVars) let name () = "V" end module L = struct - include MapDomain.MapBot_LiftTop (Lock) (MinLocksets) + include MapDomain.MapBot_LiftTop (LockDomain.MustLock) (MinLocksets) let name () = "L" end end @@ -1272,7 +1295,7 @@ struct let startstate () = (DV.bot (), L.bot ()) - let lockset_init = Lockset.top () + let lockset_init = MustLockset.all () let distr_init getg x v = if get_bool "exp.priv-distr-init" then @@ -1291,7 +1314,7 @@ struct let syncs = UnwrappedG.sync (getg (V.mutex m)) in MinLocksets.fold (fun b acc -> GSync.fold (fun s' cpa' acc -> - if Lockset.disjoint b s' then + if MustLockset.disjoint b s' then let v = CPA.find x cpa' in VD.join v acc else @@ -1304,7 +1327,7 @@ struct in let weaks = UnwrappedG.weak (getg (V.global x)) in let d_weak = GWeak.fold (fun s' v acc -> - if Lockset.disjoint s s' then + if MustLockset.disjoint s s' then VD.join v acc else acc @@ -1351,7 +1374,7 @@ struct let unlock ask getg sideg (st: BaseComponents (D).t) m = let sideg = Wrapper.sideg ask sideg in let getg = Wrapper.getg ask getg in - let s = Lockset.remove m (current_lockset ask) in + let s = MustLockset.remove m (current_lockset ask) in let is_in_G x _ = is_global ask x in let side_cpa = CPA.filter is_in_G st.cpa in let side_cpa = CPA.mapi (fun x v -> @@ -1368,6 +1391,7 @@ struct | `Return | `Normal | `Join (* TODO: no problem with branched thread creation here? *) + | `JoinCall | `Init | `Thread -> st @@ -1405,13 +1429,13 @@ struct module GWeakW = struct - include MapDomain.MapBot (Lockset) (VD) + include MapDomain.MapBot (MustLockset) (VD) let fold_weak f m a = fold (fun _ v a -> f v a) m a end module GSyncW = struct - include MapDomain.MapBot (Lockset) (LockCenteredBase.CPA) + include MapDomain.MapBot (MustLockset) (LockCenteredBase.CPA) let fold_sync_vars f m a = fold (fun _ cpa a -> @@ -1443,11 +1467,11 @@ struct let startstate () = (W.bot (), P.top ()) - let lockset_init = Lockset.top () + let lockset_init = MustLockset.all () let distr_init getg x v = if get_bool "exp.priv-distr-init" then - let v_init = GWeakW.find lockset_init (GWeak.find (Lockset.empty ()) (UnwrappedG.weak (getg (V.global x)))) in + let v_init = GWeakW.find lockset_init (GWeak.find (MustLockset.empty ()) (UnwrappedG.weak (getg (V.global x)))) in VD.join v v_init else v @@ -1458,13 +1482,13 @@ struct let (w, p) = st.priv in let p_x = P.find x p in let d_cpa = CPA.find x st.cpa in - let d_sync = Lockset.fold (fun m acc -> - if MinLocksets.exists (fun s''' -> not (Lockset.mem m s''')) p_x then + let d_sync = MustLockset.fold (fun m acc -> + if MinLocksets.exists (fun s''' -> not (MustLockset.mem m s''')) p_x then let syncs = UnwrappedG.sync (getg (V.mutex m)) in GSync.fold (fun s' gsyncw' acc -> - if Lockset.disjoint s s' then + if MustLockset.disjoint s s' then GSyncW.fold (fun w' cpa' acc -> - if MinLocksets.exists (fun s'' -> Lockset.disjoint s'' w') p_x then + if MinLocksets.exists (fun s'' -> MustLockset.disjoint s'' w') p_x then let v = CPA.find x cpa' in VD.join v acc else @@ -1479,9 +1503,9 @@ struct in let weaks = UnwrappedG.weak (getg (V.global x)) in let d_weak = GWeak.fold (fun s' gweakw' acc -> - if Lockset.disjoint s s' then + if MustLockset.disjoint s s' then GWeakW.fold (fun w' v acc -> - if MinLocksets.exists (fun s'' -> Lockset.disjoint s'' w') p_x then + if MinLocksets.exists (fun s'' -> MustLockset.disjoint s'' w') p_x then VD.join v acc else acc @@ -1521,10 +1545,10 @@ struct let unlock ask getg sideg (st: BaseComponents (D).t) m = let getg = Wrapper.getg ask getg in let sideg = Wrapper.sideg ask sideg in - let s = Lockset.remove m (current_lockset ask) in + let s = MustLockset.remove m (current_lockset ask) in let (w, p) = st.priv in let p' = P.map (fun s' -> MinLocksets.add s s') p in - if M.tracing then M.traceli "priv" "unlock %a %a" Lock.pretty m CPA.pretty st.cpa; + if M.tracing then M.traceli "priv" "unlock %a %a" LockDomain.MustLock.pretty m CPA.pretty st.cpa; let side_gsyncw = CPA.fold (fun x v acc -> if is_global ask x then ( let w_x = W.find x w in @@ -1537,7 +1561,7 @@ struct acc ) st.cpa (GSyncW.bot ()) in - if M.tracing then M.traceu "priv" "unlock %a %a" Lock.pretty m GSyncW.pretty side_gsyncw; + if M.tracing then M.traceu "priv" "unlock %a %a" LockDomain.MustLock.pretty m GSyncW.pretty side_gsyncw; sideg (V.mutex m) (UnwrappedG.create_sync (GSync.singleton s side_gsyncw)); {st with priv = (w, p')} @@ -1546,6 +1570,7 @@ struct | `Return | `Normal | `Join (* TODO: no problem with branched thread creation here? *) + | `JoinCall | `Init | `Thread -> st @@ -1557,7 +1582,7 @@ struct if EscapeDomain.EscapedVars.mem x escaped then ( let (w, p) = st.priv in let p' = P.add x (MinLocksets.singleton s) p in - sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (Lockset.empty ()) (GWeakW.singleton lockset_init v))); + sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (MustLockset.empty ()) (GWeakW.singleton lockset_init v))); {st with cpa = CPA.remove x st.cpa; priv = (w, p')} ) else @@ -1568,7 +1593,7 @@ struct let sideg = Wrapper.sideg ask sideg in CPA.fold (fun x v (st: BaseComponents (D).t) -> if is_global ask x then ( - sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (Lockset.empty ()) (GWeakW.singleton lockset_init v))); + sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (MustLockset.empty ()) (GWeakW.singleton lockset_init v))); {st with cpa = CPA.remove x st.cpa} ) else @@ -1598,11 +1623,11 @@ struct let startstate () = ((W.bot (), P.top ()), (DV.bot (), L.bot ())) - let lockset_init = Lockset.top () + let lockset_init = MustLockset.all () let distr_init getg x v = if get_bool "exp.priv-distr-init" then - let v_init = GWeakW.find lockset_init (GWeak.find (Lockset.empty ()) (UnwrappedG.weak (getg (V.global x)))) in + let v_init = GWeakW.find lockset_init (GWeak.find (MustLockset.empty ()) (UnwrappedG.weak (getg (V.global x)))) in VD.join v v_init else v @@ -1618,9 +1643,9 @@ struct let syncs = UnwrappedG.sync (getg (V.mutex m)) in MinLocksets.fold (fun b acc -> GSync.fold (fun s' gsyncw' acc -> - if Lockset.disjoint b s' then + if MustLockset.disjoint b s' then GSyncW.fold (fun w' cpa' acc -> - if MinLocksets.exists (fun s'' -> Lockset.disjoint s'' w') p_x then + if MinLocksets.exists (fun s'' -> MustLockset.disjoint s'' w') p_x then let v = CPA.find x cpa' in VD.join v acc else @@ -1636,9 +1661,9 @@ struct in let weaks = UnwrappedG.weak (getg (V.global x)) in let d_m_weak = GWeak.fold (fun s' gweakw' acc -> - if Lockset.disjoint s s' then + if MustLockset.disjoint s s' then GWeakW.fold (fun w' v acc -> - if MinLocksets.exists (fun s'' -> Lockset.disjoint s'' w') p_x then + if MinLocksets.exists (fun s'' -> MustLockset.disjoint s'' w') p_x then VD.join v acc else acc @@ -1648,13 +1673,13 @@ struct ) weaks (VD.bot ()) in let d_m = VD.join d_m_sync d_m_weak in - let d_g_sync = Lockset.fold (fun m acc -> - if MinLocksets.exists (fun s''' -> not (Lockset.mem m s''')) p_x then + let d_g_sync = MustLockset.fold (fun m acc -> + if MinLocksets.exists (fun s''' -> not (MustLockset.mem m s''')) p_x then let syncs = UnwrappedG.sync (getg (V.mutex m)) in GSync.fold (fun s' gsyncw' acc -> - if Lockset.disjoint s s' then + if MustLockset.disjoint s s' then GSyncW.fold (fun w' cpa' acc -> - if MinLocksets.exists (fun s'' -> Lockset.disjoint s'' w') p_x then + if MinLocksets.exists (fun s'' -> MustLockset.disjoint s'' w') p_x then let v = CPA.find x cpa' in VD.join v acc else @@ -1706,7 +1731,7 @@ struct let unlock ask getg sideg (st: BaseComponents (D).t) m = let getg = Wrapper.getg ask getg in let sideg = Wrapper.sideg ask sideg in - let s = Lockset.remove m (current_lockset ask) in + let s = MustLockset.remove m (current_lockset ask) in let ((w, p), vl) = st.priv in let p' = P.map (fun s' -> MinLocksets.add s s') p in let side_gsyncw = CPA.fold (fun x v acc -> @@ -1728,6 +1753,7 @@ struct | `Return | `Normal | `Join (* TODO: no problem with branched thread creation here? *) + | `JoinCall | `Init | `Thread -> st @@ -1739,7 +1765,7 @@ struct if EscapeDomain.EscapedVars.mem x escaped then ( let ((w, p), (vv, l)) = st.priv in let p' = P.add x (MinLocksets.singleton s) p in - sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (Lockset.empty ()) (GWeakW.singleton lockset_init v))); + sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (MustLockset.empty ()) (GWeakW.singleton lockset_init v))); {st with cpa = CPA.remove x st.cpa; priv = ((w, p'), (vv, l))} ) else @@ -1750,7 +1776,7 @@ struct let sideg = Wrapper.sideg ask sideg in CPA.fold (fun x v (st: BaseComponents (D).t) -> if is_global ask x then ( - sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (Lockset.empty ()) (GWeakW.singleton lockset_init v))); + sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (MustLockset.empty ()) (GWeakW.singleton lockset_init v))); {st with cpa = CPA.remove x st.cpa} ) else @@ -1859,7 +1885,7 @@ struct r let lock ask getg st m = - if M.tracing then M.traceli "priv" "lock %a" LockDomain.Addr.pretty m; + if M.tracing then M.traceli "priv" "lock %a" LockDomain.MustLock.pretty m; if M.tracing then M.trace "priv" "st: %a" BaseComponents.pretty st; let getg x = let r = getg x in @@ -1871,7 +1897,7 @@ struct r let unlock ask getg sideg st m = - if M.tracing then M.traceli "priv" "unlock %a" LockDomain.Addr.pretty m; + if M.tracing then M.traceli "priv" "unlock %a" LockDomain.MustLock.pretty m; if M.tracing then M.trace "priv" "st: %a" BaseComponents.pretty st; let getg x = let r = getg x in diff --git a/src/analyses/basePriv.mli b/src/analyses/basePriv.mli index e176a450fa..40e50c2a69 100644 --- a/src/analyses/basePriv.mli +++ b/src/analyses/basePriv.mli @@ -17,10 +17,10 @@ sig val read_global: Queries.ask -> (V.t -> G.t) -> BaseDomain.BaseComponents (D).t -> varinfo -> BaseDomain.VD.t val write_global: ?invariant:bool -> Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> varinfo -> BaseDomain.VD.t -> BaseDomain.BaseComponents (D).t - val lock: Queries.ask -> (V.t -> G.t) -> BaseDomain.BaseComponents (D).t -> LockDomain.Addr.t -> BaseDomain.BaseComponents (D).t - val unlock: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> LockDomain.Addr.t -> BaseDomain.BaseComponents (D).t + val lock: Queries.ask -> (V.t -> G.t) -> BaseDomain.BaseComponents (D).t -> LockDomain.MustLock.t -> BaseDomain.BaseComponents (D).t + val unlock: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> LockDomain.MustLock.t -> BaseDomain.BaseComponents (D).t - val sync: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> [`Normal | `Join | `Return | `Init | `Thread] -> BaseDomain.BaseComponents (D).t + val sync: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread] -> BaseDomain.BaseComponents (D).t val escape: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> EscapeDomain.EscapedVars.t -> BaseDomain.BaseComponents (D).t val enter_multithreaded: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> BaseDomain.BaseComponents (D).t diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index aa829c4606..003cdfa96c 100644 --- a/src/analyses/commonPriv.ml +++ b/src/analyses/commonPriv.ml @@ -59,6 +59,24 @@ struct not threadflag_path_sens else true + + (** Whether branched thread creation at start nodes of procedures needs to be handled by [sync `JoinCall] of privatization. *) + let branched_thread_creation_at_call (ask:Queries.ask) = + let threadflag_active = List.mem "threadflag" (GobConfig.get_string_list "ana.activated") in + if threadflag_active then + let sens = GobConfig.get_string_list "ana.ctx_sens" in + let threadflag_ctx_sens = match sens with + | [] -> (* use values of "ana.ctx_insens" (blacklist) *) + not (List.mem "threadflag" @@ GobConfig.get_string_list "ana.ctx_insens") + | sens -> (* use values of "ana.ctx_sens" (whitelist) *) + List.mem "threadflag" sens + in + if not threadflag_ctx_sens then + true + else + ask.f (Queries.GasExhausted) + else + true end module Protection = @@ -92,7 +110,7 @@ module MutexGlobals = struct module VMutex = struct - include LockDomain.Addr + include LockDomain.MustLock let name () = "mutex" end module VMutexInits = Printable.UnitConf (struct let name = "MUTEX_INITS" end) @@ -130,23 +148,14 @@ end module Locksets = struct - module Lock = - struct - include LockDomain.Addr - let name () = "lock" - end - - module Lockset = SetDomain.ToppedSet (Lock) (struct let topname = "All locks" end) - - module MustLockset = SetDomain.Reverse (Lockset) + module MustLockset = LockDomain.MustLockset - let current_lockset (ask: Q.ask): Lockset.t = + let current_lockset (ask: Q.ask): MustLockset.t = (* TODO: remove this global_init workaround *) if !AnalysisState.global_initialization then - Lockset.empty () + MustLockset.empty () else - let mls = ask.f Queries.MustLockset in - LockDomain.MustLockset.fold (fun ml acc -> Lockset.add (Addr (LockDomain.MustLock.to_mval ml)) acc) mls (Lockset.empty ()) (* TODO: use MustLockset as Lockset *) + ask.f Queries.MustLockset (* TODO: reversed SetDomain.Hoare *) module MinLocksets = HoareDomain.Set_LiftTop (MustLockset) (struct let topname = "All locksets" end) (* reverse Lockset because Hoare keeps maximal, but we need minimal *) @@ -171,7 +180,7 @@ struct let name () = "P" (* TODO: change MinLocksets.exists/top instead? *) - let find x p = find_opt x p |? MinLocksets.singleton (Lockset.empty ()) (* ensure exists has something to check for thread returns *) + let find x p = find_opt x p |? MinLocksets.singleton (MustLockset.empty ()) (* ensure exists has something to check for thread returns *) end end @@ -252,7 +261,7 @@ struct module LLock = struct - include Printable.Either (Locksets.Lock) (struct include CilType.Varinfo let name () = "global" end) + include Printable.Either (LockDomain.MustLock) (struct include CilType.Varinfo let name () = "global" end) let mutex m = `Left m let global x = `Right x end @@ -305,3 +314,41 @@ struct let startstate () = W.bot (), LMust.top (), L.bot () end + + +let lift_lock (ask: Q.ask) f st (addr: LockDomain.Addr.t) = + (* Should be in sync with: + 1. LocksetAnalysis.MakeMust.event + 2. MutexAnalysis.Spec.Arg.add + 3. LockDomain.MustLocksetRW.add_mval_rw *) + match addr with + | UnknownPtr -> st + | Addr (v, _) when ask.f (IsMultiple v) -> st + | Addr mv when LockDomain.Mval.is_definite mv -> f st (LockDomain.MustLock.of_mval mv) + | Addr _ + | NullPtr + | StrPtr _ -> st + +let lift_unlock (ask: Q.ask) f st (addr: LockDomain.Addr.t) = + (* Should be in sync with: + 1. LocksetAnalysis.MakeMust.event + 2. MutexAnalysis.Spec.Arg.remove + 3. MutexAnalysis.Spec.Arg.remove_all + 4. LockDomain.MustLocksetRW.remove_mval_rw *) + match addr with + | UnknownPtr -> + LockDomain.MustLockset.fold (fun ml st -> + (* call privatization's unlock only with definite lock *) + f st ml + ) (ask.f MustLockset) st + | StrPtr _ + | NullPtr -> st + | Addr mv when LockDomain.Mval.is_definite mv -> f st (LockDomain.MustLock.of_mval mv) + | Addr mv -> + LockDomain.MustLockset.fold (fun ml st -> + if LockDomain.MustLock.semantic_equal_mval ml mv = Some false then + st + else + (* call privatization's unlock only with definite lock *) + f st ml + ) (ask.f MustLockset) st diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml index 22b9db1cd4..448e3a79e5 100644 --- a/src/analyses/condVars.ml +++ b/src/analyses/condVars.ml @@ -116,7 +116,7 @@ struct match rval with | BinOp (op, _, _, _) when is_cmp op -> (* logical expression *) save_expr lval rval - | Lval k when Option.is_some (mustPointTo ctx (AddrOf k) >? flip D.get d) -> (* var-eq for transitive closure *) + | Lval k -> (* var-eq for transitive closure *) mustPointTo ctx (AddrOf k) >? flip D.get_elt d |> Option.map (save_expr lval) |? d | _ -> d diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml index 2727de9d04..95a22578cb 100644 --- a/src/analyses/mCP.ml +++ b/src/analyses/mCP.ml @@ -322,6 +322,13 @@ struct f (Result.top ()) (!base_id, spec !base_id, assoc !base_id ctx.local) *) | Queries.DYojson -> `Lifted (D.to_yojson ctx.local) + | Queries.GasExhausted -> + if (get_int "ana.context.gas_value" >= 0) then + (* There is a lifter above this that will answer it, save to ask *) + ctx.ask (Queries.GasExhausted) + else + (* Abort to avoid infinite recursion *) + false | _ -> let r = fold_left (f ~q) (Result.top ()) @@ spec_list ctx.local in do_sideg ctx !sides; diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 65373b2f0c..bb50c96432 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -209,15 +209,14 @@ struct MustLockset.disjoint held_locks protecting | Queries.MayBePublicWithout _ when MustLocksetRW.is_all ls -> false | Queries.MayBePublicWithout {global=v; write; without_mutex; protection} -> - let held_locks = MustLocksetRW.to_must_lockset @@ fst @@ Arg.remove' ctx ~warn:false without_mutex in + let held_locks = MustLockset.remove without_mutex (MustLocksetRW.to_must_lockset ls) in let protecting = protecting ~write protection v in (* TODO: unsound in 29/24, why did we do this before? *) (* if Mutexes.mem verifier_atomic (Lockset.export_locks (Lockset.remove (without_mutex, true) ctx.local)) then false else *) MustLockset.disjoint held_locks protecting - | Queries.MustBeProtectedBy {mutex = Addr mutex_mv; global=v; write; protection} when Mval.is_definite mutex_mv -> (* only definite Addrs can be in must-locksets to begin with, anything else cannot protect anything *) - let ml = LockDomain.MustLock.of_mval mutex_mv in + | Queries.MustBeProtectedBy {mutex = ml; global=v; write; protection} -> let protecting = protecting ~write protection v in (* TODO: unsound in 29/24, why did we do this before? *) (* if LockDomain.Addr.equal mutex (LockDomain.Addr.of_var LF.verifier_atomic_var) then diff --git a/src/analyses/mutexGhosts.ml b/src/analyses/mutexGhosts.ml index 6e95504731..7bc4423f04 100644 --- a/src/analyses/mutexGhosts.ml +++ b/src/analyses/mutexGhosts.ml @@ -13,7 +13,7 @@ struct module ThreadCreate = Printable.UnitConf (struct let name = "threadcreate" end) module V = struct - include Printable.Either3 (Node) (LockDomain.Addr) (ThreadCreate) + include Printable.Either3 (Node) (LockDomain.MustLock) (ThreadCreate) let node x = `Left x let lock x = `Middle x let threadcreate = `Right () @@ -58,6 +58,11 @@ struct let create_threadcreate threadcreate = `Lifted2 (`Lifted2 threadcreate) end + let mustlock_of_addr (addr: LockDomain.Addr.t): LockDomain.MustLock.t option = + match addr with + | Addr mv when LockDomain.Mval.is_definite mv -> Some (LockDomain.MustLock.of_mval mv) + | _ -> None + let event ctx e octx = let verifier_atomic_addr = LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var in begin match e with @@ -67,7 +72,9 @@ struct let (locked, _, _) = G.node (ctx.global (V.node ctx.prev_node)) in if Locked.cardinal locked > 1 then ( Locked.iter (fun lock -> - ctx.sideg (V.lock lock) (G.create_lock true) + Option.iter (fun lock -> + ctx.sideg (V.lock lock) (G.create_lock true) + ) (mustlock_of_addr lock) ) locked ); ) @@ -77,7 +84,9 @@ struct let (_, unlocked, _) = G.node (ctx.global (V.node ctx.prev_node)) in if Locked.cardinal unlocked > 1 then ( Locked.iter (fun lock -> - ctx.sideg (V.lock lock) (G.create_lock true) + Option.iter (fun lock -> + ctx.sideg (V.lock lock) (G.create_lock true) + ) (mustlock_of_addr lock) ) unlocked ); ) @@ -92,8 +101,7 @@ struct ctx.local let ghost_var_available ctx = function - | WitnessGhost.Var.Locked (Addr (v, o) as lock) -> not (LockDomain.Addr.Offs.contains_index o) && not (G.lock (ctx.global (V.lock lock))) - | Locked _ -> false + | WitnessGhost.Var.Locked ((v, o) as lock) -> not (Offset.Z.contains_index o) && not (G.lock (ctx.global (V.lock lock))) | Multithreaded -> true let ghost_var_available ctx v = @@ -111,31 +119,31 @@ struct let entries = (* TODO: do variable_entry-s only once *) Locked.fold (fun l acc -> - if ghost_var_available ctx (Locked l) then ( + match mustlock_of_addr l with + | Some l when ghost_var_available ctx (Locked l) -> let entry = WitnessGhost.variable_entry ~task (Locked l) in Queries.YS.add entry acc - ) - else + | _ -> acc ) (Locked.union locked unlocked) (Queries.YS.empty ()) in let entries = Locked.fold (fun l acc -> - if ghost_var_available ctx (Locked l) then ( + match mustlock_of_addr l with + | Some l when ghost_var_available ctx (Locked l) -> let entry = WitnessGhost.update_entry ~task ~node:g (Locked l) GoblintCil.one in Queries.YS.add entry acc - ) - else + | _ -> acc ) locked entries in let entries = Unlocked.fold (fun l acc -> - if ghost_var_available ctx (Locked l) then ( + match mustlock_of_addr l with + | Some l when ghost_var_available ctx (Locked l) -> let entry = WitnessGhost.update_entry ~task ~node:g (Locked l) GoblintCil.zero in Queries.YS.add entry acc - ) - else + | _ -> acc ) unlocked entries in diff --git a/src/analyses/mutexTypeAnalysis.ml b/src/analyses/mutexTypeAnalysis.ml index 441f2e9953..4a993bbd7d 100644 --- a/src/analyses/mutexTypeAnalysis.ml +++ b/src/analyses/mutexTypeAnalysis.ml @@ -12,16 +12,17 @@ struct let name () = "pthreadMutexType" - (* Removing indexes here avoids complicated lookups and allows to have the LVals as vars here, at the price that different types of mutexes in arrays are not dinstinguished *) - module O = Offset.Unit - - module V = struct - include Printable.Prod(CilType.Varinfo)(O) (* TODO: use Mval.Unit *) + module V = + struct + (* Removing indexes here avoids complicated lookups and allows to have the LVals as vars here, at the price that different types of mutexes in arrays are not dinstinguished *) + include Mval.Unit let is_write_only _ = false end module G = MAttr + module O = Offset.Unit + (* transfer functions *) let assign ctx (lval:lval) (rval:exp) : D.t = match lval with diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml index d76cd06190..66d8e3a357 100644 --- a/src/analyses/unassumeAnalysis.ml +++ b/src/analyses/unassumeAnalysis.ml @@ -85,7 +85,9 @@ struct let yaml = match Yaml_unix.of_file (Fpath.v (GobConfig.get_string "witness.yaml.unassume")) with | Ok yaml -> yaml - | Error (`Msg m) -> failwith ("Yaml_unix.of_file: " ^ m) + | Error (`Msg m) -> + Logs.error "Yaml_unix.of_file: %s" m; + Svcomp.errorwith "witness missing" in let yaml_entries = yaml |> GobYaml.list |> BatResult.get_ok in diff --git a/src/autoTune.ml b/src/autoTune.ml index 434b4fb0b2..8ec77739e7 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -186,7 +186,7 @@ let enableAnalyses anas = (*escape is also still enabled, because otherwise we get a warning*) (*does not consider dynamic calls!*) -let notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadid"; "threadJoins"; "threadreturn"; "mhp"; "region"] +let notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadid"; "threadJoins"; "threadreturn"; "mhp"; "region"; "pthreadMutexType"] let reduceThreadAnalyses () = let isThreadCreate = function | LibraryDesc.ThreadCreate _ -> true diff --git a/src/build-info/dune b/src/build-info/dune index 5a64b399a4..e1a45ef8fc 100644 --- a/src/build-info/dune +++ b/src/build-info/dune @@ -15,7 +15,7 @@ (target configVersion.ml) (mode (promote (until-clean) (only configVersion.ml))) ; replace existing file in source tree, even if releasing (only overrides) (deps (universe)) ; do not cache, always regenerate - (action (pipe-stdout (bash "git describe --all --long --dirty || echo \"n/a\"") (with-stdout-to %{target} (bash "xargs printf '(* Automatically regenerated, changes do not persist! *)\nlet version = \"%s\"'"))))) + (action (pipe-stdout (bash "git describe --all --long --dirty || echo \"n/a\"") (with-stdout-to %{target} (bash "xargs printf '(* Automatically regenerated, changes do not persist! *)\nlet version = Sys.opaque_identity \"%s\"'"))))) (rule (target configProfile.ml) @@ -31,7 +31,7 @@ (target configDatetime.ml) (mode (promote (until-clean) (only configDatetime.ml))) ; replace existing file in source tree, even if releasing (only overrides) (deps (universe)) ; do not cache, always regenerate - (action (pipe-stdout (bash "date +\"%Y-%m-%dT%H:%M:%S\" || echo \"n/a\"") (with-stdout-to %{target} (bash "xargs printf '(* Automatically regenerated, changes do not persist! *)\nlet datetime = \"%s\"'"))))) + (action (pipe-stdout (bash "date +\"%Y-%m-%dT%H:%M:%S\" || echo \"n/a\"") (with-stdout-to %{target} (bash "xargs printf '(* Automatically regenerated, changes do not persist! *)\nlet datetime = Sys.opaque_identity \"%s\"'"))))) (env (_ diff --git a/src/cdomain/value/cdomains/addressDomain.ml b/src/cdomain/value/cdomains/addressDomain.ml index dc1ebfff7d..da684cc4f4 100644 --- a/src/cdomain/value/cdomains/addressDomain.ml +++ b/src/cdomain/value/cdomains/addressDomain.ml @@ -320,7 +320,7 @@ struct let string_writing_defined dest = (* if the destination address set contains a StrPtr, writing to such a string literal is undefined behavior *) - if List.exists Option.is_some (List.map Addr.to_c_string (elements dest)) then + if exists (fun a -> Option.is_some (Addr.to_c_string a)) dest then (M.warn ~category:M.Category.Behavior.Undefined.other "May write to a string literal, which leads to a segmentation fault in most cases"; false) else diff --git a/src/cdomain/value/cdomains/floatDomain.ml b/src/cdomain/value/cdomains/floatDomain.ml index c86770826c..0977c68890 100644 --- a/src/cdomain/value/cdomains/floatDomain.ml +++ b/src/cdomain/value/cdomains/floatDomain.ml @@ -241,12 +241,12 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct let minimal = function | Bot -> raise (ArithmeticOnFloatBot (Printf.sprintf "minimal %s" (show Bot))) - | Interval (l, _) -> Float_t.to_float l + | Interval (l, _) -> Some (Float_t.to_float l) | _ -> None let maximal = function | Bot -> raise (ArithmeticOnFloatBot (Printf.sprintf "maximal %s" (show Bot))) - | Interval (_, h) -> Float_t.to_float h + | Interval (_, h) -> Some (Float_t.to_float h) | _ -> None let is_exact = function diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 3bf81b1ba1..c525732d3b 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -572,6 +572,14 @@ module IntervalArith (Ints_t : IntOps.IntOps) = struct let min_ik' = Ints_t.to_bigint min_ik in let t = List.find_opt (fun x -> Z.compare l x >= 0 && Z.compare x min_ik' >= 0) ts in BatOption.map_default Ints_t.of_bigint min_ik t + let is_upper_threshold u = + let ts = if get_interval_threshold_widening_constants () = "comparisons" then WideningThresholds.upper_thresholds () else ResettableLazy.force widening_thresholds in + let u = Ints_t.to_bigint u in + List.exists (Z.equal u) ts + let is_lower_threshold l = + let ts = if get_interval_threshold_widening_constants () = "comparisons" then WideningThresholds.lower_thresholds () else ResettableLazy.force widening_thresholds_desc in + let l = Ints_t.to_bigint l in + List.exists (Z.equal l) ts end module IntervalFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) option = @@ -702,9 +710,10 @@ struct match x, y with | _,None | None, _ -> None | Some (x1,x2), Some (y1,y2) -> + let threshold = get_interval_threshold_widening () in let (min_ik, max_ik) = range ik in - let lr = if Ints_t.compare min_ik x1 = 0 then y1 else x1 in - let ur = if Ints_t.compare max_ik x2 = 0 then y2 else x2 in + let lr = if Ints_t.compare min_ik x1 = 0 || threshold && Ints_t.compare y1 x1 > 0 && IArith.is_lower_threshold x1 then y1 else x1 in + let ur = if Ints_t.compare max_ik x2 = 0 || threshold && Ints_t.compare y2 x2 < 0 && IArith.is_upper_threshold x2 then y2 else x2 in norm ik @@ Some (lr,ur) |> fst @@ -1382,8 +1391,9 @@ struct let min_ys = minimal ys |> Option.get in let max_ys = maximal ys |> Option.get in let min_range,max_range = range ik in - let min = if min_xs =. min_range then min_ys else min_xs in - let max = if max_xs =. max_range then max_ys else max_xs in + let threshold = get_interval_threshold_widening () in + let min = if min_xs =. min_range || threshold && min_ys >. min_xs && IArith.is_lower_threshold min_xs then min_ys else min_xs in + let max = if max_xs =. max_range || threshold && max_ys <. max_xs && IArith.is_upper_threshold max_xs then max_ys else max_xs in xs |> (function (_, y)::z -> (min, y)::z | _ -> []) |> List.rev @@ -2256,9 +2266,8 @@ struct shift_op a b in (* If one of the parameters of the shift is negative, the result is undefined *) - let x_min = minimal x in - let y_min = minimal y in - if x_min = None || y_min = None || Z.compare (Option.get x_min) Z.zero < 0 || Z.compare (Option.get y_min) Z.zero < 0 then + let is_negative = GobOption.for_all (fun x -> Z.lt x Z.zero) in + if is_negative (minimal x) || is_negative (minimal y) then top_of ik else norm ik @@ lift2 shift_op_big_int ik x y @@ -2404,7 +2413,6 @@ module Booleans = MakeBooleans ( (* Inclusion/Exclusion sets. Go to top on arithmetic operations (except for some easy cases, e.g. multiplication with 0). Joins on widen, i.e. precise integers as long as not derived from arithmetic expressions. *) module Enums : S with type int_t = Z.t = struct - open Batteries module R = Interval32 (* range for exclusion *) let range_ikind = Cil.IInt @@ -2514,7 +2522,8 @@ module Enums : S with type int_t = Z.t = struct let ex = if Z.gt x Z.zero || Z.lt y Z.zero then BISet.singleton Z.zero else BISet.empty () in norm ik @@ (Exc (ex, r)) - let join ik = curry @@ function + let join _ x y = + match x, y with | Inc x, Inc y -> Inc (BISet.union x y) | Exc (x,r1), Exc (y,r2) -> Exc (BISet.inter x y, R.join r1 r2) | Exc (x,r), Inc y @@ -2522,13 +2531,14 @@ module Enums : S with type int_t = Z.t = struct let r = if BISet.is_empty y then r else - let (min_el_range, max_el_range) = Tuple2.mapn (fun x -> R.of_interval range_ikind (Size.min_range_sign_agnostic x)) (BISet.min_elt y, BISet.max_elt y) in + let (min_el_range, max_el_range) = Batteries.Tuple2.mapn (fun x -> R.of_interval range_ikind (Size.min_range_sign_agnostic x)) (BISet.min_elt y, BISet.max_elt y) in let range = R.join min_el_range max_el_range in R.join r range in Exc (BISet.diff x y, r) - let meet ikind = curry @@ function + let meet _ x y = + match x, y with | Inc x, Inc y -> Inc (BISet.inter x y) | Exc (x,r1), Exc (y,r2) -> let r = R.meet r1 r2 in @@ -2582,7 +2592,8 @@ module Enums : S with type int_t = Z.t = struct try lift2 f ikind a b with Division_by_zero -> top_of ikind let neg ?no_ov = lift1 Z.neg - let add ?no_ov ikind = curry @@ function + let add ?no_ov ikind a b = + match a, b with | Inc z,x when BISet.is_singleton z && BISet.choose z = Z.zero -> x | x,Inc z when BISet.is_singleton z && BISet.choose z = Z.zero -> x | x,y -> lift2 Z.add ikind x y @@ -2616,9 +2627,8 @@ module Enums : S with type int_t = Z.t = struct shift_op a b in (* If one of the parameters of the shift is negative, the result is undefined *) - let x_min = minimal x in - let y_min = minimal y in - if x_min = None || y_min = None || Z.compare (Option.get x_min) Z.zero < 0 || Z.compare (Option.get y_min) Z.zero < 0 then + let is_negative = GobOption.for_all (fun x -> Z.lt x Z.zero) in + if is_negative (minimal x) || is_negative (minimal y) then top_of ik else lift2 shift_op_big_int ik x y) diff --git a/src/cdomain/value/cdomains/offset.ml b/src/cdomain/value/cdomains/offset.ml index 9c9c5c3333..e8cba0afc5 100644 --- a/src/cdomain/value/cdomains/offset.ml +++ b/src/cdomain/value/cdomains/offset.ml @@ -213,7 +213,7 @@ struct let bits_offset, _size = GoblintCil.bitsOffset (TComp (field.fcomp, [])) field_as_offset in let bits_offset = idx_of_int bits_offset in let remaining_offset = offset_to_index_offset ~typ:field.ftype o in - Idx.add bits_offset remaining_offset + GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> Idx.add bits_offset remaining_offset | `Index (x, o) -> let (item_typ, item_size_in_bits) = match Option.map unrollType typ with @@ -223,9 +223,10 @@ struct | _ -> (None, Idx.top ()) in - let bits_offset = Idx.mul item_size_in_bits x in + (* Binary operations on offsets should not generate overflow warnings in SV-COMP *) + let bits_offset = GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> Idx.mul item_size_in_bits x in let remaining_offset = offset_to_index_offset ?typ:item_typ o in - Idx.add bits_offset remaining_offset + GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> Idx.add bits_offset remaining_offset in offset_to_index_offset ?typ offs diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml index 09593fb614..c6dd8e004e 100644 --- a/src/cdomain/value/cdomains/valueDomain.ml +++ b/src/cdomain/value/cdomains/valueDomain.ml @@ -49,19 +49,32 @@ module type Blob = sig type value type size - type origin - include Lattice.S with type t = value * size * origin + type zeroinit + include Lattice.S with type t = value * size * zeroinit val map: (value -> value) -> t -> t val value: t -> value val invalidate_value: VDQ.t -> typ -> t -> t end -(* ZeroInit is true if malloc was used to allocate memory and it's false if calloc was used *) -module ZeroInit = +module type ZeroInit = +sig + include Lattice.S + + val is_malloc : t -> bool + val malloc : t + val calloc : t +end + +(* ZeroInit is false if malloc was used to allocate memory and true if calloc was used *) +module ZeroInit : ZeroInit = struct include Lattice.Fake(Basetype.RawBools) - let name () = "no zeroinit" + let name () = "zeroinit" + + let is_malloc x = not x + let malloc = false + let calloc = true end module Blob (Value: S) (Size: IntDomain.Z)= @@ -70,7 +83,7 @@ struct let name () = "blob" type value = Value.t type size = Size.t - type origin = ZeroInit.t + type zeroinit = ZeroInit.t let map f (v, s, o) = f v, s, o let value (a, b, c) = a @@ -862,8 +875,8 @@ struct end | _, _ -> None - let zero_init_calloced_memory orig x t = - if orig then + let zero_init_calloced_memory zeroinit x t = + if ZeroInit.is_malloc zeroinit then (* This Blob came from malloc *) x else if x = Bot then @@ -878,23 +891,23 @@ struct if M.tracing then M.traceli "eval_offset" "do_eval_offset %a %a (%a)" pretty x Offs.pretty offs (Pretty.docOpt (CilType.Exp.pretty ())) exp; let r = match x, offs with - | Blob((va, _, orig) as c), `Index (_, ox) -> + | Blob((va, _, zeroinit) as c), `Index (_, ox) -> begin let l', o' = shift_one_over l o in let ev = do_eval_offset ask f (Blobs.value c) ox exp l' o' v t in - zero_init_calloced_memory orig ev t + zero_init_calloced_memory zeroinit ev t end - | Blob((va, _, orig) as c), `Field _ -> + | Blob((va, _, zeroinit) as c), `Field _ -> begin let l', o' = shift_one_over l o in let ev = do_eval_offset ask f (Blobs.value c) offs exp l' o' v t in - zero_init_calloced_memory orig ev t + zero_init_calloced_memory zeroinit ev t end - | Blob((va, _, orig) as c), `NoOffset -> + | Blob((va, _, zeroinit) as c), `NoOffset -> begin let l', o' = shift_one_over l o in let ev = do_eval_offset ask f (Blobs.value c) offs exp l' o' v t in - zero_init_calloced_memory orig ev t + zero_init_calloced_memory zeroinit ev t end | Bot, _ -> Bot | _ -> @@ -952,24 +965,24 @@ struct let update_offset ?(blob_destructive=false) (ask: VDQ.t) (x:t) (offs:offs) (value:t) (exp:exp option) (v:lval) (t:typ): t = let rec do_update_offset (ask:VDQ.t) (x:t) (offs:offs) (value:t) (exp:exp option) (l:lval option) (o:offset option) (v:lval) (t:typ):t = if M.tracing then M.traceli "update_offset" "do_update_offset %a %a (%a) %a" pretty x Offs.pretty offs (Pretty.docOpt (CilType.Exp.pretty ())) exp pretty value; - let mu = function Blob (Blob (y, s', orig), s, orig2) -> Blob (y, ID.join s s',orig) | x -> x in + let mu = function Blob (Blob (y, s', zeroinit), s, _) -> Blob (y, ID.join s s', zeroinit) | x -> x in let r = match x, offs with | Mutex, _ -> (* hide mutex structure contents, not updated anyway *) Mutex - | Blob (x,s,orig), `Index (_,ofs) -> + | Blob (x,s,zeroinit), `Index (_,ofs) -> begin let l', o' = shift_one_over l o in - let x = zero_init_calloced_memory orig x t in - mu (Blob (join x (do_update_offset ask x ofs value exp l' o' v t), s, orig)) + let x = zero_init_calloced_memory zeroinit x t in + mu (Blob (join x (do_update_offset ask x ofs value exp l' o' v t), s, zeroinit)) end - | Blob (x,s,orig), `Field(f, _) -> + | Blob (x,s,zeroinit), `Field(f, _) -> begin (* We only have Blob for dynamically allocated memory. In these cases t is the type of the lval used to access it, i.e. for a struct s {int x; int y;} a; accessed via a->x *) (* will be int. Here, we need a zero_init of the entire contents of the blob though, which we get by taking the associated f.fcomp. Putting [] for attributes is ok, as we don't *) (* consider them in VD *) let l', o' = shift_one_over l o in - let x = zero_init_calloced_memory orig x (TComp (f.fcomp, [])) in + let x = zero_init_calloced_memory zeroinit x (TComp (f.fcomp, [])) in (* Strong update of scalar variable is possible if the variable is unique and size of written value matches size of blob being written to. *) let do_strong_update = match v with @@ -978,37 +991,38 @@ struct let blob_size_opt = ID.to_int s in not @@ ask.is_multiple var && not @@ Cil.isVoidType t (* Size of value is known *) - && Option.is_some blob_size_opt (* Size of blob is known *) - && Z.equal (Option.get blob_size_opt) (Z.of_int @@ Cil.bitsSizeOf (TComp (toptype, []))/8) + && GobOption.exists (fun blob_size -> (* Size of blob is known *) + Z.equal blob_size (Z.of_int @@ Cil.bitsSizeOf (TComp (toptype, []))/8) + ) blob_size_opt | _ -> false in if do_strong_update then - Blob ((do_update_offset ask x offs value exp l' o' v t), s, orig) + Blob ((do_update_offset ask x offs value exp l' o' v t), s, zeroinit) else - mu (Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, orig)) + mu (Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, zeroinit)) end - | Blob (x,s,orig), _ -> + | Blob (x,s,zeroinit), _ -> begin let l', o' = shift_one_over l o in - let x = zero_init_calloced_memory orig x t in + let x = zero_init_calloced_memory zeroinit x t in (* Strong update of scalar variable is possible if the variable is unique and size of written value matches size of blob being written to. *) let do_strong_update = begin match v with | (Var var, _) -> let blob_size_opt = ID.to_int s in not @@ ask.is_multiple var - && Option.is_some blob_size_opt (* Size of blob is known *) - && (( - not @@ Cil.isVoidType t (* Size of value is known *) - && Z.equal (Option.get blob_size_opt) (Z.of_int @@ Cil.alignOf_int t) - ) || blob_destructive) + && GobOption.exists (fun blob_size -> (* Size of blob is known *) + (not @@ Cil.isVoidType t (* Size of value is known *) + && Z.equal blob_size (Z.of_int @@ Cil.alignOf_int t)) + || blob_destructive + ) blob_size_opt | _ -> false end in if do_strong_update then - Blob ((do_update_offset ask x offs value exp l' o' v t), s, orig) + Blob ((do_update_offset ask x offs value exp l' o' v t), s, zeroinit) else - mu (Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, orig)) + mu (Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, zeroinit)) end | Thread _, _ -> (* hack for pthread_t variables *) @@ -1036,7 +1050,7 @@ struct match offs with | `NoOffset -> begin match value with - | Blob (y, s, orig) -> mu (Blob (join x y, s, orig)) + | Blob (y, s, zeroinit) -> mu (Blob (join x y, s, zeroinit)) | Int _ -> cast t value | _ -> value end @@ -1289,7 +1303,7 @@ and Unions: UnionDomain.S with type t = UnionDomain.Field.t * Compound.t and typ and CArrays: ArrayDomain.StrWithDomain with type value = Compound.t and type idx = ArrIdxDomain.t = ArrayDomain.AttributeConfiguredAndNullByteArrayDomain(Compound)(ArrIdxDomain) -and Blobs: Blob with type size = ID.t and type value = Compound.t and type origin = ZeroInit.t = Blob (Compound) (ID) +and Blobs: Blob with type size = ID.t and type value = Compound.t and type zeroinit = ZeroInit.t = Blob (Compound) (ID) module type InvariantArg = diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index 7e60cce74b..5500ad8c3b 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -181,7 +181,7 @@ struct else if Z.lt coeff Z.minus_one then Z.to_string coeff else Format.asprintf "+%s" (Z.to_string coeff) in - coeff_str ^ Var.to_string var + coeff_str ^ Var.show var in let const_to_str vl = if Z.equal vl Z.zero then @@ -203,11 +203,10 @@ struct | Some m when Matrix.is_empty m -> "⊤" | Some m -> let constraint_list = List.init (Matrix.num_rows m) (fun i -> vec_to_constraint (conv_to_ints @@ Matrix.get_row m i) t.env) in - Format.asprintf "%s" ("[|"^ (String.concat "; " constraint_list) ^"|]") + "[|"^ (String.concat "; " constraint_list) ^"|]" let pretty () (x:t) = text (show x) - let printXml f x = BatPrintf.fprintf f "\n\n\nmatrix\n\n\n%s\n\nenv\n\n\n%s\n\n\n" (XmlUtil.escape (Format.asprintf "%s" (show x) )) (XmlUtil.escape (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (x.env))) - + let printXml f x = BatPrintf.fprintf f "\n\n\nmatrix\n\n\n%s\n\nenv\n\n\n%a\n\n\n" (XmlUtil.escape (show x)) Environment.printXml x.env let eval_interval ask = Bounds.bound_texpr let name () = "affeq" @@ -257,7 +256,7 @@ struct let meet t1 t2 = timing_wrap "meet" (meet t1) t2 let leq t1 t2 = - let env_comp = Environment.compare t1.env t2.env in (* Apron's Environment.compare has defined return values. *) + let env_comp = Environment.cmp t1.env t2.env in (* Apron's Environment.cmp has defined return values. *) if env_comp = -2 || env_comp > 0 then (* -2: environments are not compatible (a variable has different types in the 2 environements *) (* -1: if env1 is a subset of env2, (OK) *) @@ -334,7 +333,7 @@ struct else match Option.get a.d, Option.get b.d with | x, y when is_top_env a || is_top_env b -> {d = Some (Matrix.empty ()); env = Environment.lce a.env b.env} - | x, y when (Environment.compare a.env b.env <> 0) -> + | x, y when (Environment.cmp a.env b.env <> 0) -> let sup_env = Environment.lce a.env b.env in let mod_x = dim_add (Environment.dimchange a.env sup_env) x in let mod_y = dim_add (Environment.dimchange b.env sup_env) y in @@ -430,8 +429,8 @@ struct let assign_exp ask t var exp no_ov = let res = assign_exp ask t var exp no_ov in - if M.tracing then M.tracel "ops" "assign_exp t:\n %s \n var: %s \n exp: %a\n no_ov: %b -> \n %s" - (show t) (Var.to_string var) d_exp exp (Lazy.force no_ov) (show res) ; + if M.tracing then M.tracel "ops" "assign_exp t:\n %s \n var: %a \n exp: %a\n no_ov: %b -> \n %s" + (show t) Var.pretty var d_exp exp (Lazy.force no_ov) (show res); res let assign_var (t: VarManagement(Vc)(Mx).t) v v' = @@ -441,7 +440,7 @@ struct let assign_var t v v' = let res = assign_var t v v' in - if M.tracing then M.tracel "ops" "assign_var t:\n %s \n v: %s \n v': %s\n -> %s" (show t) (Var.to_string v) (Var.to_string v') (show res) ; + if M.tracing then M.tracel "ops" "assign_var t:\n %s \n v: %a \n v': %a\n -> %s" (show t) Var.pretty v Var.pretty v' (show res); res let assign_var_parallel t vv's = @@ -499,7 +498,7 @@ struct let substitute_exp ask t var exp no_ov = let res = substitute_exp ask t var exp no_ov in - if M.tracing then M.tracel "ops" "Substitute_expr t: \n %s \n var: %s \n exp: %a \n -> \n %s" (show t) (Var.to_string var) d_exp exp (show res); + if M.tracing then M.tracel "ops" "Substitute_expr t: \n %s \n var: %a \n exp: %a \n -> \n %s" (show t) Var.pretty var d_exp exp (show res); res let substitute_exp ask t var exp no_ov = timing_wrap "substitution" (substitute_exp ask t var exp) no_ov diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml index d0ef268ca6..03ac3ed3f0 100644 --- a/src/cdomains/apron/apronDomain.apron.ml +++ b/src/cdomains/apron/apronDomain.apron.ml @@ -283,7 +283,7 @@ struct let assign_exp_with ask nd v e no_ov = match Convert.texpr1_of_cil_exp ask nd (A.env nd) e no_ov with | texpr1 -> - if M.tracing then M.trace "apron" "assign_exp converted: %s" (Format.asprintf "%a" Texpr1.print texpr1); + if M.tracing then M.trace "apron" "assign_exp converted: %a" Texpr1.pretty texpr1; A.assign_texpr_with Man.mgr nd v texpr1 None | exception Convert.Unsupported_CilExp _ -> if M.tracing then M.trace "apron" "assign_exp unsupported"; @@ -442,7 +442,7 @@ struct let invariant _ = [] let show (x:t) = - Format.asprintf "%a (env: %a)" A.print x (Environment.print: Format.formatter -> Environment.t -> unit) (A.env x) + GobFormat.asprintf "%a (env: %a)" A.print x Environment.pp (A.env x) let pretty () (x:t) = text (show x) let equal x y = @@ -451,10 +451,10 @@ struct let hash (x:t) = A.hash Man.mgr x - let compare (x:t) y: int = - (* there is no A.compare, but polymorphic compare should delegate to Abstract0 and Environment compare's implemented in Apron's C *) - Stdlib.compare x y - let printXml f x = BatPrintf.fprintf f "\n\n\nconstraints\n\n\n%s\n\nenv\n\n\n%s\n\n\n" (XmlUtil.escape (Format.asprintf "%a" A.print x)) (XmlUtil.escape (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (A.env x))) + let compare (x: t) (y: t): int = + failwith "Apron.Abstract1 doesn't have total order" (* https://github.com/antoinemine/apron/issues/99 *) + + let printXml f x = BatPrintf.fprintf f "\n\n\nconstraints\n\n\n%s\n\nenv\n\n\n%a\n\n\n" (XmlUtil.escape (GobFormat.asprint A.print x)) Environment.printXml (A.env x) let to_yojson (x: t) = let constraints = @@ -463,11 +463,9 @@ struct |> Lincons1Set.elements |> List.map (fun lincons1 -> `String (Lincons1.show lincons1)) in - let env = `String (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (A.env x)) - in `Assoc [ ("constraints", `List constraints); - ("env", env); + ("env", Environment.to_yojson (A.env x)); ] let unify x y = @@ -533,9 +531,9 @@ struct | _ -> begin match Convert.tcons1_of_cil_exp ask d (A.env d) e negate no_ov with | tcons1 -> - if M.tracing then M.trace "apron" "assert_constraint %a %s" d_exp e (Format.asprintf "%a" Tcons1.print tcons1); + if M.tracing then M.trace "apron" "assert_constraint %a %a" d_exp e Tcons1.pretty tcons1; if M.tracing then M.trace "apron" "assert_constraint st: %a" D.pretty d; - if M.tracing then M.trace "apron" "assert_constraint tcons1: %s" (Format.asprintf "%a" Tcons1.print tcons1); + if M.tracing then M.trace "apron" "assert_constraint tcons1: %a" Tcons1.pretty tcons1; let r = meet_tcons ask d tcons1 e in if M.tracing then M.trace "apron" "assert_constraint r: %a" D.pretty r; r @@ -598,7 +596,7 @@ struct let x_cons = A.to_lincons_array Man.mgr x_j in let y_cons = A.to_lincons_array Man.mgr y_j in let try_add_con j con1 = - if M.tracing then M.tracei "apron" "try_add_con %s" (Format.asprintf "%a" (Lincons1.print: Format.formatter -> Lincons1.t -> unit) con1); + if M.tracing then M.tracei "apron" "try_add_con %a" Lincons1.pretty con1; let t = meet_lincons j con1 in let t_x = A.change_environment Man.mgr t x_env false in let t_y = A.change_environment Man.mgr t y_env false in @@ -637,7 +635,7 @@ struct in let env_exists_mem_con1 env con1 = let r = env_exists_mem_con1 env con1 in - if M.tracing then M.trace "apron" "env_exists_mem_con1 %s %s -> %B" (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) env) (Lincons1.show con1) r; + if M.tracing then M.trace "apron" "env_exists_mem_con1 %a %a -> %B" Environment.pretty env Lincons1.pretty con1 r; r in (* Heuristically reorder constraints to pass 36/12 with singlethreaded->multithreaded mode switching. *) diff --git a/src/cdomains/apron/gobApron.apron.ml b/src/cdomains/apron/gobApron.apron.ml index c39a3e42db..fbb1fe9ec5 100644 --- a/src/cdomains/apron/gobApron.apron.ml +++ b/src/cdomains/apron/gobApron.apron.ml @@ -1,9 +1,38 @@ open Batteries include Apron +module Scalar = +struct + include Scalar + + let pp = print + include Printable.SimpleFormat ( + struct + type nonrec t = t + let pp = pp + end + ) +end + +module Coeff = +struct + include Coeff + + let s_of_z z = Coeff.s_of_mpqf (Mpqf.of_mpz (Z_mlgmpidl.mpz_of_z z)) +end + module Var = struct include Var + + let pp = print + include Printable.SimpleFormat ( + struct + type nonrec t = t + let pp = pp + end + ) + let equal x y = Var.compare x y = 0 end @@ -11,8 +40,17 @@ module Lincons1 = struct include Lincons1 - let show = Format.asprintf "%a" print - let compare x y = String.compare (show x) (show y) (* HACK *) + let pp = print + include Printable.SimpleFormat ( + struct + type nonrec t = t + let pp = pp + end + ) + + let compare x y = + (* TODO: implement proper total Lincons1 order *) + String.compare (show x) (show y) (* HACK *) let num_vars x = (* Apron.Linexpr0.get_size returns some internal nonsense, so we count ourselves. *) @@ -36,12 +74,63 @@ struct |> of_enum end +module Texpr1 = +struct + include Texpr1 + + let pp = print + include Printable.SimpleFormat ( + struct + type nonrec t = t + let pp = pp + end + ) + + module Expr = + struct + type t = expr + + let pp = print_expr + include Printable.SimpleFormat ( + struct + type nonrec t = t + let pp = pp + end + ) + end +end + +module Tcons1 = +struct + include Tcons1 + + let pp = print + include Printable.SimpleFormat ( + struct + type nonrec t = t + let pp = pp + end + ) +end + (** A few code elements for environment changes from functions as remove_vars etc. have been moved to sharedFunctions as they are needed in a similar way inside affineEqualityDomain. A module that includes various methods used by variable handling operations such as add_vars, remove_vars etc. in apronDomain and affineEqualityDomain. *) module Environment = struct include Environment + let pp: Format.formatter -> Environment.t -> unit = Environment.print + include Printable.SimpleFormat ( + struct + type nonrec t = t + let pp = pp + end + ) + + let compare (x: t) (y: t): int = + (* TODO: implement total Environment order in OCaml *) + failwith "Apron.Environment doesn't have total order" (* https://github.com/antoinemine/apron/issues/99 *) + let ivars_only env = let ivs, fvs = Environment.vars env in assert (Array.length fvs = 0); (* shouldn't ever contain floats *) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index 67bd67f4e5..c1ca3661a5 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -11,21 +11,44 @@ open Batteries open GoblintCil open Pretty module M = Messages -open Apron +open GobApron open VectorMatrix module Mpqf = SharedFunctions.Mpqf module Rhs = struct - (* (Some i, k) represents a sum of a variable with index i and the number k. - (None, k) represents the number k. *) - type t = (int option * GobZ.t) [@@deriving eq, ord, hash] - let var_zero i = (Some i, Z.zero) - let show_formatted formatter = function - | (Some v, o) when Z.equal o Z.zero -> formatter v - | (Some v, o) -> Printf.sprintf "%s%+Ld" (formatter v) (Z.to_int64 o) - | (None, o) -> Printf.sprintf "%Ld" (Z.to_int64 o) - let show rhs = show_formatted (Printf.sprintf "var_%d") rhs + (* Rhs represents coefficient*var_i + offset / divisor + depending on whether coefficient is 0, the monomial term may disappear completely, not refering to any var_i, thus: + (Some (coefficient, i), offset, divisor ) with coefficient != 0 , or + (None , offset, divisor ) *) + type t = ((GobZ.t * int) option * GobZ.t * GobZ.t) [@@deriving eq, ord, hash] + let var_zero i = (Some (Z.one,i), Z.zero, Z.one) + let show_coeff c = + if Z.equal c Z.one then "" + else if Z.equal c Z.minus_one then "-" + else (Z.to_string c) ^"·" + let show_rhs_formatted formatter = let ztostring n = (if Z.(geq n zero) then "+" else "") ^ Z.to_string n in + function + | (Some (coeff,v), o,_) when Z.equal o Z.zero -> Printf.sprintf "%s%s" (show_coeff coeff) (formatter v) + | (Some (coeff,v), o,_) -> Printf.sprintf "%s%s %s" (show_coeff coeff) (formatter v) (ztostring o) + | (None, o,_) -> Printf.sprintf "%s" (Z.to_string o) + let show (v,o,d) = + let rhs=show_rhs_formatted (Printf.sprintf "var_%d") (v,o,d) in + if not (Z.equal d Z.one) then "(" ^ rhs ^ ")/" ^ (Z.to_string d) else rhs + + (** factor out gcd from all terms, i.e. ax=by+c with a positive is the canonical form for adx+bdy+cd *) + let canonicalize (v,o,d) = + let gcd = Z.gcd o d in (* gcd of coefficients *) + let gcd = Option.map_default (fun (c,_) -> Z.gcd c gcd) gcd v in (* include monomial in gcd computation *) + let commondivisor = if Z.(lt d zero) then Z.neg gcd else gcd in (* canonical form dictates d being positive *) + (BatOption.map (fun (coeff,i) -> (Z.div coeff commondivisor,i)) v, Z.div o commondivisor, Z.div d commondivisor) + + (** Substitute rhs for varx in rhs' *) + let subst rhs varx rhs' = + match rhs,rhs' with + | (monom, o, d), (Some (c', x'), o', d') when x'=varx -> canonicalize (Option.map (fun (c,x) -> (Z.mul c c',x)) monom, Z.((o*c')+(d*o')), Z.mul d d') + | _ -> rhs' + end module EqualitiesConjunction = struct @@ -36,7 +59,7 @@ module EqualitiesConjunction = struct let show_formatted formatter econ = if IntMap.is_empty econ then "{}" else - let str = IntMap.fold (fun i (refvar,off) acc -> Printf.sprintf "%s=%s ∧ %s" (formatter i) (Rhs.show_formatted formatter (refvar,off)) acc) econ "" in + let str = IntMap.fold (fun i (refmonom,off,divi) acc -> Printf.sprintf "%s%s=%s ∧ %s" (Rhs.show_coeff divi) (formatter i) (Rhs.show_rhs_formatted formatter (refmonom,off,divi)) acc) econ "" in "{" ^ String.sub str 0 (String.length str - 4) ^ "}" let show econ = show_formatted (Printf.sprintf "var_%d") econ @@ -52,16 +75,23 @@ module EqualitiesConjunction = struct (** trivial equalities are of the form var_i = var_i and are not kept explicitely in the sparse representation of EquanlitiesConjunction *) let nontrivial (_,econmap) lhs = IntMap.mem lhs econmap + (** turn x = (cy+o)/d into y = (dx-o)/c*) + let inverse x (c,y,o,d) = (y, (Some (d, x), Z.neg o, c)) + (** sparse implementation of get rhs for lhs, but will default to no mapping for sparse entries *) let get_rhs (_,econmap) lhs = IntMap.find_default (Rhs.var_zero lhs) lhs econmap - (** set_rhs, staying loyal to immutable, sparse map underneath *) + (** set_rhs, staying loyal to immutable, sparse map underneath; do not attempt any normalization *) let set_rhs (dim,map) lhs rhs = (dim, if Rhs.equal rhs Rhs.(var_zero lhs) then IntMap.remove lhs map else IntMap.add lhs rhs map ) + + (** canonicalize equation, and set_rhs, staying loyal to immutable, sparse map underneath *) + let canonicalize_and_set (dim,map) lhs rhs = set_rhs (dim,map) lhs (Rhs.canonicalize rhs) + let copy = identity @@ -86,9 +116,10 @@ module EqualitiesConjunction = struct IntHashtbl.add h x r; r) in - let rec bumpentry k (refvar,offset) = function (* directly bumps lhs-variable during a run through indexes, bumping refvar explicitely with a new lookup in indexes *) - | (tbl,delta,head::rest) when k>=head -> bumpentry k (refvar,offset) (tbl,delta+1,rest) (* rec call even when =, in order to correctly interpret double bumps *) - | (tbl,delta,lyst) (* k (IntMap.add (op k delta) (BatOption.map (memobumpvar) refvar, offset) tbl, delta, lyst) + let rec bumpentry k (refvar,offset,divi) = function (* directly bumps lhs-variable during a run through indexes, bumping refvar explicitly with a new lookup in indexes *) + + | (tbl,delta,head::rest) when k>=head -> bumpentry k (refvar,offset,divi) (tbl,delta+1,rest) (* rec call even when =, in order to correctly interpret double bumps *) + | (tbl,delta,lyst) (* k (IntMap.add (op k delta) (BatOption.map (fun (c,v) -> (c,memobumpvar v)) refvar,offset,divi) tbl, delta, lyst) in let (a,_,_) = IntMap.fold bumpentry map (IntMap.empty,0,offsetlist) in (* Build new map during fold with bumped key/vals *) (op dim (Array.length indexes), a) @@ -111,17 +142,28 @@ module EqualitiesConjunction = struct (* Forget information about variable i *) let forget_variable d var = let res = - (let ref_var_opt = fst (get_rhs d var) in + (let ref_var_opt = Tuple3.first (get_rhs d var) in match ref_var_opt with - | Some ref_var when ref_var = var -> + | Some (_,ref_var) when ref_var = var -> + if M.tracing then M.trace "forget" "headvar var_%d" var; (* var is the reference variable of its connected component *) - (let cluster = IntMap.fold - (fun i (ref, offset) l -> if ref = ref_var_opt then i::l else l) (snd d) [] in + (let cluster = List.sort (Int.compare) @@ IntMap.fold + (fun i (refe,_,_) l -> BatOption.map_default (fun (coeff,refe) -> if (refe=ref_var) then i::l else l) l refe) (snd d) [] in + if M.tracing then M.trace "forget" "cluster varindices: [%s]" (String.concat ", " (List.map (string_of_int) cluster)); (* obtain cluster with common reference variable ref_var*) match cluster with (* new ref_var is taken from head of the cluster *) - | head :: tail -> - let headconst = snd (get_rhs d head) in (* take offset between old and new reference variable *) - List.fold (fun map i -> set_rhs map i Z.(Some head, snd (get_rhs d i) - headconst)) d cluster (* shift offset to match new reference variable *) + | head :: clusterrest -> + (* head: divi*x = coeff*y + offs *) + (* divi*x = coeff*y + offs =inverse=> y =( divi*x - offs)/coeff *) + let (newref,offs,divi) = (get_rhs d head) in + let (coeff,y) = BatOption.get newref in + let (y,yrhs) = inverse head (coeff,y,offs,divi) in (* reassemble yrhs out of components *) + let shifted_cluster = (List.fold (fun map i -> + let irhs = (get_rhs d i) in (* old entry is i = irhs *) + Rhs.subst yrhs y irhs |> (* new entry for i is irhs [yrhs/y] *) + set_rhs map i + ) d clusterrest) in + set_rhs shifted_cluster head (Rhs.var_zero head) (* finally make sure that head is now trivial *) | [] -> d) (* empty cluster means no work for us *) | _ -> d) (* variable is either a constant or expressed by another refvar *) in let res = (fst res, IntMap.remove var (snd res)) in (* set d(var) to unknown, finally *) @@ -153,31 +195,68 @@ module EqualitiesConjunction = struct exception Contradiction - let meet_with_one_conj ts i (var, b) = + let meet_with_one_conj ts i (var, offs, divi) = + let (var,offs,divi) = Rhs.canonicalize (var,offs,divi) in (* make sure that the one new conj is properly canonicalized *) let res = - let subst_var tsi x (vart, bt) = + let subst_var (dim,econj) x (vary, o, d) = + (* [[x substby (cy+o)/d ]] ((c'x+o')/d') *) + (* =====> (c'cy + c'o+o'd)/(dd') *) let adjust = function - | (Some vare, b') when vare = x -> (vart, Z.(b' + bt)) + | (Some (c',varx), o',d') when varx = x -> + let open Z in Rhs.canonicalize (BatOption.map (fun (c, y)-> (c * c', y)) vary, c'*o + o'*d, d'*d) | e -> e in - (fst tsi, IntMap.add x (vart, bt) @@ IntMap.map adjust (snd tsi)) (* in case of sparse representation, make sure that the equality is now included in the conjunction *) + (dim, IntMap.add x (vary, o, d) @@ IntMap.map adjust econj) (* in case of sparse representation, make sure that the equality is now included in the conjunction *) in - let (var1, b1) = get_rhs ts i in - (match var, var1 with - | None , None -> if not @@ Z.equal b b1 then raise Contradiction else ts - | None , Some h1 -> subst_var ts h1 (None, Z.(b - b1)) - | Some j, None -> subst_var ts j (None, Z.(b1 - b)) - | Some j, Some h1 -> + (match var, (get_rhs ts i) with + (*| new conj , old conj *) + | None , (None , o1, divi1) -> if not @@ (Z.equal offs o1 && Z.equal divi divi1) then raise Contradiction else ts + (* o/d = x_i = (c1*x_h1+o1)/d1 *) + (* ======> x_h1 = (o*d1-o1*d)/(d*c1) /\ x_i = o/d *) + | None , (Some (coeff1,h1), o1, divi1) -> subst_var ts h1 (None, Z.(offs*divi1 - o1*divi),Z.(divi*coeff1)) + (* (c*x_j+o)/d = x_i = o1/d1 *) + (* ======> x_j = (o1*d-o*d1)/(d1*c) /\ x_i = o1/d1 *) + | Some (coeff,j), (None , o1, divi1) -> subst_var ts j (None, Z.(o1*divi - offs*divi1),Z.(divi1*coeff)) + (* (c*x_j+o)/d = x_i = (c1*x_h1+o1)/d1 *) + (* ======> x_j needs normalization wrt. ts *) + | Some (coeff,j), ((Some (coeff1,h1), o1, divi1) as oldi)-> (match get_rhs ts j with - | (None, b2) -> subst_var ts i (None, Z.(b2 + b)) - | (Some h2, b2) -> - if h1 = h2 then - (if not @@ Z.equal b1 Z.(b2 + b) then raise Contradiction else ts) - else if h1 < h2 then subst_var ts h2 (Some h1, Z.(b1 - (b + b2))) - else subst_var ts h1 (Some h2, Z.(b + (b2 - b1))))) in - if M.tracing then M.trace "meet" "meet_with_one_conj conj: { %s } eq: var_%d=%s -> { %s } " (show (snd ts)) i (Rhs.show (var,b)) (show (snd ts)) + (* ts[x_j]=o2/d2 ========> ... *) + | (None , o2, divi2) -> + let newxi = Rhs.subst (None,o2,divi2) j (Some (coeff,j),offs,divi) in + let newxh1 = snd @@ inverse i (coeff1,h1,o1,divi1) in + let newxh1 = Rhs.subst newxi i newxh1 in + subst_var ts h1 newxh1 + (* ts[x_j]=(c2*x_h2+o2)/d2 ========> ... *) + | (Some (coeff2,h2), o2, divi2) as normalizedj -> + if h1 = h2 then (* this is the case where x_i and x_j already where in the same equivalence class; let's see whether the new equality contradicts the old one *) + let normalizedi= Rhs.subst normalizedj j (Some(coeff,j),offs,divi) in + if not @@ Rhs.equal normalizedi oldi then raise Contradiction else ts + else if h1 < h2 (* good, we now unite the two equvalence classes; let's decide upon the representative *) + then (* express h2 in terms of h1: *) + let (_,newh2)= inverse j (coeff2,h2,o2,divi2) in + let newh2 = Rhs.subst oldi i (Rhs.subst (snd @@ inverse i (coeff,j,offs,divi)) j newh2) in + subst_var ts h2 newh2 + else (* express h1 in terms of h2: *) + let (_,newh1)= inverse i (coeff1,h1,o1,divi1) in + let newh1 = Rhs.subst normalizedj j (Rhs.subst (Some(coeff,j),offs,divi) i newh1) in + subst_var ts h1 newh1)) in + if M.tracing then M.tracel "meet_with_one_conj" "meet_with_one_conj conj: %s eq: var_%d=%s -> %s " (show (snd ts)) i (Rhs.show (var,offs,divi)) (show (snd res)) ; res + (** affine transform variable i allover conj with transformer (Some (coeff,i)+offs)/divi *) + let affine_transform econ i (coeff, j, offs, divi) = + if nontrivial econ i then (* i cannot occur on any other rhs apart from itself *) + set_rhs econ i (Rhs.subst (get_rhs econ i) i (Some (coeff,j), offs, divi)) + else (* var_i = var_i, i.e. it may occur on the rhs of other equalities *) + (* so now, we transform with the inverse of the transformer: *) + let inv = snd (inverse i (coeff,j,offs,divi)) in + IntMap.fold (fun k v acc -> + match v with + | (Some (c,x),o,d) when x=i-> set_rhs acc k (Rhs.subst inv i v) + | _ -> acc + ) (snd econ) econ + end (** [VarManagement] defines the type t of the affine equality domain (a record that contains an optional matrix and an apron environment) and provides the functions needed for handling variables (which are defined by [RelationDomain.D2]) such as [add_vars], [remove_vars]. @@ -195,32 +274,32 @@ struct let open Apron.Texpr1 in let exception NotLinearExpr in let exception ScalarIsInfinity in - let negate coeff_var_list = List.map (fun (coeff, var) -> (Z.(-coeff), var)) coeff_var_list in - let multiply_with_Z number coeff_var_list = - List.map (fun (coeff, var) -> (Z.(number * coeff, var))) coeff_var_list in + let negate coeff_var_list = + List.map (fun (monom, offs, divi) -> Z.(BatOption.map (fun (coeff,i) -> (neg coeff, i)) monom, neg offs, divi)) coeff_var_list in + let multiply_with_Q dividend divisor coeff_var_list = + List.map (fun (monom, offs, divi) -> Rhs.canonicalize Z.(BatOption.map (fun (coeff,i) -> (dividend*coeff,i)) monom, dividend*offs, divi*divisor) ) coeff_var_list in let multiply a b = (* if one of them is a constant, then multiply. Otherwise, the expression is not linear *) match a, b with - | [(a_coeff, None)], b -> multiply_with_Z a_coeff b - | a, [(b_coeff, None)] -> multiply_with_Z b_coeff a + | [(None,coeff, divi)], c + | c, [(None,coeff, divi)] -> multiply_with_Q coeff divi c | _ -> raise NotLinearExpr in let rec convert_texpr texp = begin match texp with - (* If x is a constant, replace it with its const. val. immediately *) | Cst (Interval _) -> failwith "constant was an interval; this is not supported" | Cst (Scalar x) -> begin match SharedFunctions.int_of_scalar ?round:None x with - | Some x -> [(x, None)] + | Some x -> [(None,x,Z.one)] | None -> raise ScalarIsInfinity end | Var x -> let var_dim = Environment.dim_of_var t.env x in begin match t.d with - | None -> [(Z.one, Some var_dim)] + | None -> [(Some (Z.one,var_dim),Z.zero,Z.one)] | Some d -> (match (EConj.get_rhs d var_dim) with - | (Some i, k) -> [(Z.one, Some i); (k, None)] - | (None, k) -> [(k, None)]) + | (Some (coeff,i), k,divi) -> [(Some (coeff,i),Z.zero,divi); (None,k,divi)] + | (None, k,divi) -> [ (None,k,divi)]) end | Unop (Neg, e, _, _) -> negate (convert_texpr e) | Unop (Cast, e, _, _) -> convert_texpr e (* Ignore since casts in apron are used for floating point nums and rounding in contrast to CIL casts *) @@ -234,59 +313,41 @@ struct | exception ScalarIsInfinity -> None | x -> Some(x) - (** convert and simplify (wrt. reference variables) a texpr into a tuple of a list of monomials and a constant *) + (** convert and simplify (wrt. reference variables) a texpr into a tuple of a list of monomials (coeff,varidx,divi) and a (constant/divi) *) let simplified_monomials_from_texp (t: t) texp = BatOption.bind (monomials_from_texp t texp) (fun monomiallist -> let d = Option.get t.d in - let expr = Array.make (Environment.size t.env) Z.zero in - let accumulate_constants a (c, v) = match v with - | None -> Z.(a + c) - | Some idx -> let (term,con) = (EConj.get_rhs d idx) in - (Option.may (fun ter -> expr.(ter) <- Z.(expr.(ter) + c)) term; - Z.(a + c * con)) + let module IMap = EConj.IntMap in + let accumulate_constants (exprcache,(aconst,adiv)) (v,offs,divi) = match v with + | None -> let gcdee = Z.gcd adiv divi in exprcache,(Z.(aconst*divi/gcdee + offs*adiv/gcdee),Z.lcm adiv divi) + | Some (coeff,idx) -> let (somevar,someoffs,somedivi)=Rhs.subst (EConj.get_rhs d idx) idx (v,offs,divi) in (* normalize! *) + let newcache = Option.map_default (fun (coef,ter) -> IMap.add ter Q.((IMap.find_default zero ter exprcache) + make coef somedivi) exprcache) exprcache somevar in + let gcdee = Z.gcd adiv divi in + (newcache,(Z.(aconst*divi/gcdee + offs*adiv/gcdee),Z.lcm adiv divi)) in - let constant = List.fold_left accumulate_constants Z.zero monomiallist in (* abstract simplification of the guard wrt. reference variables *) - Some (Array.fold_lefti (fun list v (c) -> if Z.equal c Z.zero then list else (c,v)::list) [] expr, constant) ) + let (expr,constant) = List.fold_left accumulate_constants (IMap.empty,(Z.zero,Z.one)) monomiallist in (* abstract simplification of the guard wrt. reference variables *) + Some (IMap.fold (fun v c acc -> if Q.equal c Q.zero then acc else (Q.num c,v,Q.den c)::acc) expr [], constant) ) + + let simplified_monomials_from_texp (t: t) texp = + let res = simplified_monomials_from_texp t texp in + if M.tracing then M.tracel "from_texp" "%s %a -> %s" (EConj.show @@ snd @@ BatOption.get t.d) Texpr1.Expr.pretty texp + (BatOption.map_default (fun (l,(o,d)) -> List.fold_right (fun (a,x,b) acc -> Printf.sprintf "%s*var_%d/%s + %s" (Z.to_string a) x (Z.to_string b) acc) l ((Z.to_string o)^"/"^(Z.to_string d))) "" res); + res let simplify_to_ref_and_offset (t: t) texp = BatOption.bind (simplified_monomials_from_texp t texp ) - (fun (sum_of_terms, constant) -> + (fun (sum_of_terms, (constant,divisor)) -> (match sum_of_terms with - | [] -> Some (None, constant) - | [(coeff,var)] when Z.equal coeff Z.one -> Some (Some var, constant) + | [] -> Some (None, constant,divisor) + | [(coeff,var,divi)] -> Some (Rhs.canonicalize (Some (Z.mul divisor coeff,var), Z.mul constant divi,Z.mul divisor divi)) |_ -> None)) let simplify_to_ref_and_offset t texp = timing_wrap "coeff_vec" (simplify_to_ref_and_offset t) texp - (* Copy because function is not "with" so should not mutate inputs *) - let assign_const t var const = match t.d with + let assign_const t var const divi = match t.d with | None -> t - | Some t_d -> {d = Some (EConj.set_rhs t_d var (None, const)); env = t.env} - - let subtract_const_from_var t var const = - match t.d with - | None -> t - | Some t_d -> - let subtract_const_from_var_for_single_equality index (eq_var_opt, off2) econ = - if index <> var then - begin match eq_var_opt with - | Some eq_var when eq_var = var -> - EConj.set_rhs econ index (eq_var_opt, Z.(off2 - const)) - | _ -> econ - end - else econ - in - let d = - if not @@ EConj.nontrivial t_d var - (* var is a reference variable -> it can appear on the right-hand side of an equality *) - then - (EConj.IntMap.fold (subtract_const_from_var_for_single_equality) (snd t_d) t_d) - else - (* var never appears on the right hand side-> we only need to modify the array entry at index var *) - EConj.set_rhs t_d var (Tuple2.map2 (Z.add const) (EConj.get_rhs t_d var)) - in - {d = Some d; env = t.env} + | Some t_d -> {d = Some (EConj.set_rhs t_d var (None, const, divi)); env = t.env} end @@ -299,9 +360,9 @@ struct if t.d = None then None, None else match simplify_to_ref_and_offset t (Texpr1.to_expr texpr) with - | Some (None, offset) -> - (if M.tracing then M.tracel "bounds" "min: %s max: %s" (IntOps.BigIntOps.to_string offset) (IntOps.BigIntOps.to_string offset); - Some offset, Some offset) + | Some (None, offset, divisor) when Z.equal (Z.rem offset divisor) Z.zero -> let res = Z.div offset divisor in + (if M.tracing then M.tracel "bounds" "min: %a max: %a" GobZ.pretty res GobZ.pretty res; + Some res, Some res) | _ -> None, None let bound_texpr d texpr1 = timing_wrap "bounds calculation" (bound_texpr d) texpr1 @@ -336,11 +397,23 @@ struct let top () = {d = Some (EConj.empty()); env = empty_env} (** is_top returns true for top_of array and empty array; precondition: t.env and t.d are of same size *) - let is_top t = Environment.equal empty_env t.env && GobOption.exists EConj.is_top_con t.d + let is_top t = GobOption.exists EConj.is_top_con t.d + + let to_subscript i = + let transl = [|"₀";"₁";"₂";"₃";"₄";"₅";"₆";"₇";"₈";"₉"|] in + let rec subscr i = + if i = 0 then "" + else (subscr (i/10)) ^ transl.(i mod 10) in + subscr i + + let show_var env i = + let res = Var.to_string (Environment.var_of_dim env i) in + match String.split_on_char '#' res with + | varname::rest::[] -> varname ^ (try to_subscript @@ int_of_string rest with _ -> "#" ^ rest) + | _ -> res (** prints the current variable equalities with resolved variable names *) let show varM = - let lookup i = Var.to_string (Environment.var_of_dim varM.env i) in match varM.d with | None -> "⊥\n" | Some arr when EConj.is_top_con arr -> "⊤\n" @@ -348,25 +421,25 @@ struct if is_bot varM then "Bot \n" else - EConj.show_formatted lookup (snd arr) ^ (" with dimension " ^ (string_of_int @@ fst arr)) + EConj.show_formatted (show_var varM.env) (snd arr) ^ (to_subscript @@ fst arr) let pretty () (x:t) = text (show x) - let printXml f x = BatPrintf.fprintf f "\n\n\nequalities\n\n\n%s\n\nenv\n\n\n%s\n\n\n" (XmlUtil.escape (Format.asprintf "%s" (show x) )) (XmlUtil.escape (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (x.env))) + let printXml f x = BatPrintf.fprintf f "\n\n\nequalities\n\n\n%s\n\nenv\n\n\n%a\n\n\n" (XmlUtil.escape (show x)) Environment.printXml x.env let eval_interval ask = Bounds.bound_texpr - let meet_with_one_conj t i (var, b) = + let meet_with_one_conj t i (var, o, divi) = match t.d with | None -> t | Some d -> try - { d = Some (EConj.meet_with_one_conj d i (var, b)); env = t.env} + { d = Some (EConj.meet_with_one_conj d i (var, o, divi)); env = t.env} with EConj.Contradiction -> if M.tracing then M.trace "meet" " -> Contradiction\n"; { d = None; env = t.env} let meet_with_one_conj t i e = let res = meet_with_one_conj t i e in - if M.tracing then M.trace "meet" "meet_with_one_conj %s with var_%d=%s -> %s" (show t) i (Rhs.show e) (show res); + if M.tracing then M.tracel "meet" "%s with single eq %s=%s -> %s" (show t) (Z.(to_string @@ Tuple3.third e)^ show_var t.env i) (Rhs.show_rhs_formatted (show_var t.env) e) (show res); res let meet t1 t2 = @@ -374,7 +447,7 @@ struct let t1 = change_d t1 sup_env ~add:true ~del:false in let t2 = change_d t2 sup_env ~add:true ~del:false in match t1.d, t2.d with - | Some d1', Some d2' -> + | Some d1', Some d2' -> EConj.IntMap.fold (fun lhs rhs map -> meet_with_one_conj map lhs rhs) (snd d2') t1 (* even on sparse d2, this will chose the relevant conjs to meet with*) | _ -> {d = None; env = sup_env} @@ -386,16 +459,18 @@ struct let meet t1 t2 = timing_wrap "meet" (meet t1) t2 let leq t1 t2 = - let env_comp = Environment.compare t1.env t2.env in (* Apron's Environment.compare has defined return values. *) - let implies ts i (var, b) = - let tuple_cmp = Tuple2.eq (Option.eq ~eq:Int.equal) (Z.equal) in + let env_comp = Environment.cmp t1.env t2.env in (* Apron's Environment.cmp has defined return values. *) + let implies ts i (var, offs, divi) = + let tuple_cmp = Tuple3.eq (Option.eq ~eq:(Tuple2.eq (Z.equal) (Int.equal))) (Z.equal) (Z.equal) in match var with - | None -> tuple_cmp (var, b) (EConj.get_rhs ts i) - | Some j -> tuple_cmp (EConj.get_rhs ts i) @@ Tuple2.map2 (Z.add b) (EConj.get_rhs ts j) + (* directly compare in case of constant value *) + | None -> tuple_cmp (var, offs, divi) (EConj.get_rhs ts i) + (* normalize in case of a full blown equality *) + | Some (coeffj,j) -> tuple_cmp (EConj.get_rhs ts i) @@ Rhs.subst (EConj.get_rhs ts j) j (var, offs, divi) in if env_comp = -2 || env_comp > 0 then false else - if is_bot_env t1 || is_top t2 then true else - if is_bot_env t2 || is_top t1 then false else + if is_bot_env t1 || is_top t2 then true + else if is_bot_env t2 || is_top t1 then false else let m1, m2 = Option.get t1.d, Option.get t2.d in let m1' = if env_comp = 0 then m1 else VarManagement.dim_add (Environment.dimchange t1.env t2.env) m1 in EConj.IntMap.for_all (implies m1') (snd m2) (* even on sparse m2, it suffices to check the non-trivial equalities, still present in sparse m2 *) @@ -412,32 +487,50 @@ struct (* joinfunction handles the dirty details of performing an "inner join" on the lhs of both bindings; in the resulting binding, the lhs is then mapped to values that are later relevant for sorting/grouping, i.e. - lhs itself - - the difference of both offsets + - criteria A and B that characterize equivalence class, depending on the reference variable and the affine expression parameters wrt. each EConj - rhs1 - - rhs2 + - rhs2 however, we have to account for the sparseity of EConj maps by manually patching holes with default values *) - let joinfunction lhs rhs1 rhs2 = match rhs1, rhs2 with - | Some (ai,aj),Some (bi,bj) -> Some (lhs,Z.(aj - bj),(ai,aj),(bi,bj)) (* this is explicitely what we want *) - | None, Some (bi,bj) -> Some (lhs,Z.neg bj ,Rhs.var_zero lhs,(bi,bj)) (* account for the sparseity of binding 1 *) - | Some (ai,aj), None -> Some (lhs,aj ,(ai,aj),Rhs.var_zero lhs) (* account for the sparseity of binding 2 *) - | _,_ -> None (* no binding for lhs in both maps is replicated implicitely in a sparse result map *) + let joinfunction lhs rhs1 rhs2 = + ( + let e = Option.default (Rhs.var_zero lhs) in + match rhs1,rhs2 with (* first of all re-instantiate implicit sparse elements *) + | None, None -> None + | a, b -> Some (e a, e b)) + |> + BatOption.map (fun (r1,r2) -> match (r1,r2) with (* criterion A , criterion B *) + | (Some (c1,_),o1,d1), (Some (c2,_),o2,d2)-> lhs, Q.make Z.((o1*d2)-(o2*d1)) Z.(c1*d2), Q.make Z.(c2*d2) Z.(c1*d1), r1, r2 + | (None, oc,dc), (Some (cv,_),ov,dv) + | (Some (cv,_),ov,dv), (None ,oc,dc)-> lhs, Q.make Z.((oc*dv)-(ov*dc)) Z.(dc*cv), Q.one , r1, r2 (* equivalence class defined by (oc/dc-ov/dv)/(cv/dv) *) + | (None, o1,d1), (None ,o2,d2)-> lhs, (if Z.(zero = ((o1*d2)-(o2*d1))) then Q.one else Q.zero), Q.zero, r1, r2 (* only two equivalence classes: constants with matching values or constants with different values *) + ) in let table = List.of_enum @@ EConj.IntMap.values @@ EConj.IntMap.merge joinfunction (snd ad) (snd bd) in - (*compare two variables for grouping depending on delta function and reference index*) - let cmp_z (_, t0i, t1i, t2i) (_, t0j, t1j, t2j) = - let cmp_ref = Option.compare ~cmp:Int.compare in - Tuple3.compare ~cmp1:cmp_ref ~cmp2:cmp_ref ~cmp3:Z.compare (fst t1i, fst t2i, t0i) (fst t1j, fst t2j, t0j) + (* compare two variables for grouping depending on affine function parameters a, b and reference variable indices *) + let cmp_z (_, ai, bi, t1i, t2i) (_, aj, bj, t1j, t2j) = + let cmp_ref = Option.compare ~cmp:(fun x y -> Int.compare (snd x) (snd y)) in + Tuple4.compare ~cmp1:cmp_ref ~cmp2:cmp_ref ~cmp3:Q.compare ~cmp4:Q.compare (Tuple3.first t1i, Tuple3.first t2i, ai, bi) (Tuple3.first t1j, Tuple3.first t2j, aj, bj) in - (*Calculate new components as groups*) + (* Calculate new components as groups *) let new_components = BatList.group cmp_z table in - (*Adjust the domain array to represent the new components*) - let modify map idx_h b_h (idx, _, (opt1, z1), (opt2, z2)) = EConj.set_rhs map (idx) - (if opt1 = opt2 && Z.equal z1 z2 then (opt1, z1) - else (Some idx_h, Z.(z1 - b_h))) + let varentry ci offi ch offh xh = + let (coeff,off,d) = Q.(ci,(offi*ch)-(ci*offh),ch) in (* compute new rhs in Q *) + let (coeff,off,d) = Z.(coeff.num*d.den*off.den,off.num*d.den*coeff.den,d. num*coeff.den*off.den) in (* convert that back into Z *) + Rhs.canonicalize (Some(coeff,xh),off,d) in + (* ci1 = a*ch1+b /\ ci2 = a*ch2+b *) + (* ===> a = (ci1-ci2)/(ch1-ch2) b = ci2-a*ch2 *) + let constentry ci1 ci2 ch1 ch2 xh = + let a = Q.((ci1-ci2) / (ch1-ch2)) in + let b = Q.(ci2 - a*ch2) in + Rhs.canonicalize (Some (Z.(a.num*b.den),xh),Z.(b.num*a.den) ,Z.(a.den*b.den) ) in let iterate map l = match l with - | (idx_h, _, (_, b_h), _) :: t -> List.fold (fun map' e -> modify map' idx_h b_h e) map l + | (_, _, _, rhs , rhs' ) :: t when Rhs.equal rhs rhs' -> List.fold (fun acc (x,_,_,rh,_) -> EConj.set_rhs acc x rh) map l + | (h, _, _, ((Some (ch,_),oh,dh)), ((Some _,_,_) )) :: t -> List.fold (fun acc (i,_,_,(monom,oi,di),_) -> EConj.set_rhs acc i (varentry Q.(make (fst@@Option.get monom) di) Q.(make oi di) Q.(make ch dh) Q.(make oh dh) h)) map t + | (h, _, _, ((Some (ch,_),oh,dh)), ((None,_,_) )) :: t -> List.fold (fun acc (i,_,_,(monom,oi,di),_) -> EConj.set_rhs acc i (varentry Q.(make (fst@@Option.get monom) di) Q.(make oi di) Q.(make ch dh) Q.(make oh dh) h)) map t + | (h, _, _, ((None,_,_) ), ((Some (ch,_),oh,dh))) :: t -> List.fold (fun acc (i,_,_,_,(monom,oi,di)) -> EConj.set_rhs acc i (varentry Q.(make (fst@@Option.get monom) di) Q.(make oi di) Q.(make ch dh) Q.(make oh dh) h)) map t + | (h, _, _, ((None,oh1,dh1) ), ((None),oh2,dh2) ) :: t -> List.fold (fun acc (i,_,_,(_,oi1,di1),(_,oi2,di2)) -> EConj.set_rhs acc i (constentry Q.(make oi1 di1) Q.(make oi2 di2) Q.(make oh1 dh1) Q.(make oh2 dh2) h)) map t | [] -> let exception EmptyComponent in raise EmptyComponent in Some (List.fold iterate (EConj.make_empty_conj @@ fst ad) new_components) @@ -450,7 +543,7 @@ struct | Some x, Some y when is_top a || is_top b -> let new_env = Environment.lce a.env b.env in top_of new_env - | Some x, Some y when (Environment.compare a.env b.env <> 0) -> + | Some x, Some y when (Environment.cmp a.env b.env <> 0) -> let sup_env = Environment.lce a.env b.env in let mod_x = dim_add (Environment.dimchange a.env sup_env) x in let mod_y = dim_add (Environment.dimchange b.env sup_env) y in @@ -512,15 +605,15 @@ struct | None -> (* Statement "assigned_var = ?" (non-linear assignment) *) forget_var t var - | Some (None, off) -> + | Some (None, off, divi) -> (* Statement "assigned_var = off" (constant assignment) *) - assign_const (forget_var t var) var_i off - | Some (Some exp_var, off) when var_i = exp_var -> - (* Statement "assigned_var = assigned_var + off" *) - subtract_const_from_var t var_i off - | Some (Some exp_var, off) -> - (* Statement "assigned_var = exp_var + off" (assigned_var is not the same as exp_var) *) - meet_with_one_conj (forget_var t var) var_i (Some exp_var, off) + assign_const (forget_var t var) var_i off divi + | Some (Some (coeff_var,exp_var), off, divi) when var_i = exp_var -> + (* Statement "assigned_var = (coeff_var*assigned_var + off) / divi" *) + {d=Some (EConj.affine_transform d var_i (coeff_var, var_i, off, divi)); env=t.env } + | Some (Some monomial, off, divi) -> + (* Statement "assigned_var = (monomial) + off / divi" (assigned_var is not the same as exp_var) *) + meet_with_one_conj (forget_var t var) var_i (Some (monomial), off, divi) end | None -> bot_env @@ -537,8 +630,8 @@ struct let assign_exp ask t var exp no_ov = let res = assign_exp ask t var exp no_ov in - if M.tracing then M.tracel "ops" "assign_exp t:\n %s \n var: %s \n exp: %a\n no_ov: %b -> \n %s" - (show t) (Var.to_string var) d_exp exp (Lazy.force no_ov) (show res) ; + if M.tracing then M.tracel "ops" "assign_exp t:\n %s \n var: %a \n exp: %a\n no_ov: %b -> \n %s" + (show t) Var.pretty var d_exp exp (Lazy.force no_ov) (show res); res let assign_var (t: VarManagement.t) v v' = @@ -547,7 +640,7 @@ struct let assign_var t v v' = let res = assign_var t v v' in - if M.tracing then M.tracel "ops" "assign_var t:\n %s \n v: %s \n v': %s\n -> %s" (show t) (Var.to_string v) (Var.to_string v') (show res) ; + if M.tracing then M.tracel "ops" "assign_var t:\n %s \n v: %a \n v': %a\n -> %s" (show t) Var.pretty v Var.pretty v' (show res); res (** Parallel assignment of variables. @@ -600,7 +693,7 @@ struct let substitute_exp ask t var exp no_ov = let res = substitute_exp ask t var exp no_ov in - if M.tracing then M.tracel "ops" "Substitute_expr t: \n %s \n var: %s \n exp: %a \n -> \n %s" (show t) (Var.to_string var) d_exp exp (show res); + if M.tracing then M.tracel "ops" "Substitute_expr t: \n %s \n var: %a \n exp: %a \n -> \n %s" (show t) Var.pretty var d_exp exp (show res); res let substitute_exp ask t var exp no_ov = timing_wrap "substitution" (substitute_exp ask t var exp) no_ov @@ -624,9 +717,9 @@ struct | Some d -> match simplified_monomials_from_texp t (Texpr1.to_expr @@ Tcons1.get_texpr1 tcons) with | None -> t - | Some (sum_of_terms, constant) ->( + | Some (sum_of_terms, (constant,divisor)) ->( match sum_of_terms with - | [] -> (* no reference variables in the guard *) + | [] -> (* no reference variables in the guard, so check constant for zero *) begin match Tcons1.get_typ tcons with | EQ when Z.equal constant Z.zero -> t | SUPEQ when Z.geq constant Z.zero -> t @@ -635,15 +728,21 @@ struct | EQMOD _ -> t | _ -> bot_env (* all other results are violating the guard *) end - | [(varexpr, index)] -> (* guard has a single reference variable only *) - if Tcons1.get_typ tcons = EQ && Z.divisible constant varexpr then - meet_with_one_conj t index (None, (Z.(-(constant) / varexpr))) + | [(coeff, index, divi)] -> (* guard has a single reference variable only *) + if Tcons1.get_typ tcons = EQ then + meet_with_one_conj t index (Rhs.canonicalize (None, Z.neg @@ Z.(divi*constant),Z.(coeff*divisor))) else t (* only EQ is supported in equality based domains *) - | [(a1,var1); (a2,var2)] -> (* two variables in relation needs a little sorting out *) + | [(c1,var1,d1); (c2,var2,d2)] -> (* two variables in relation needs a little sorting out *) begin match Tcons1.get_typ tcons with - | EQ when Z.(a1 * a2 = -one) -> (* var1-var1 or var2-var1 *) - meet_with_one_conj t var2 (Some var1, Z.mul a1 constant) + | EQ -> (* c1*var1/d1 + c2*var2/d2 +constant/divisor = 0*) + (* ======> c1*divisor*d2 * var1 = -c2*divisor*d1 * var2 +constant*-d1*d2*) + (* \/ c2*divisor*d1 * var2 = -c1*divisor*d2 * var1 +constant*-d1*d2*) + let open Z in + if var1 < var2 then + meet_with_one_conj t var2 (Rhs.canonicalize (Some (neg @@ c1*divisor,var1),neg @@ constant*d2*d1,c2*divisor*d1)) + else + meet_with_one_conj t var1 (Rhs.canonicalize (Some (neg @@ c2*divisor,var2),neg @@ constant*d2*d1,c1*divisor*d2)) | _-> t (* Not supported in equality based 2vars without coeffiients *) end | _ -> t (* For equalities of more then 2 vars we just return t *)) @@ -697,14 +796,14 @@ struct lincons in let get_const acc i = function - | (None, o) -> + | (None, o, d) -> let xi = Environment.var_of_dim t.env i in - of_coeff xi [(Coeff.s_of_int (-1), xi)] o :: acc - | (Some r, _) when r = i -> acc - | (Some r, o) -> + of_coeff xi [(GobApron.Coeff.s_of_z @@ Z.neg d, xi)] o :: acc + | (Some (c,r), _,_) when r = i -> acc + | (Some (c,r), o, d) -> let xi = Environment.var_of_dim t.env i in let ri = Environment.var_of_dim t.env r in - of_coeff xi [(Coeff.s_of_int (-1), xi); (Coeff.s_of_int 1, ri)] o :: acc + of_coeff xi [(GobApron.Coeff.s_of_z @@ Z.neg d, xi); (GobApron.Coeff.s_of_z c, ri)] o :: acc in BatOption.get t.d |> fun (_,map) -> EConj.IntMap.fold (fun lhs rhs list -> get_const list lhs rhs) map [] diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index 827dc252fc..86b5f2770f 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -6,7 +6,8 @@ open GobApron module M = Messages -let int_of_scalar ?round (scalar: Scalar.t) = + +let int_of_scalar ?(scalewith=Z.one) ?round (scalar: Scalar.t) = if Scalar.is_infty scalar <> 0 then (* infinity means unbounded *) None else @@ -20,23 +21,26 @@ let int_of_scalar ?round (scalar: Scalar.t) = | None when Stdlib.Float.is_integer f -> Some f | None -> None in - Z.of_float f + Z.(of_float f * scalewith) | Mpqf scalar -> (* octMPQ, boxMPQ, polkaMPQ *) let n = Mpqf.get_num scalar in let d = Mpqf.get_den scalar in + let scale = Z_mlgmpidl.mpz_of_z scalewith in let+ z = if Mpzf.cmp_int d 1 = 0 then (* exact integer (denominator 1) *) - Some n + Some (Mpzf.mul scale n) else begin match round with - | Some `Floor -> Some (Mpzf.fdiv_q n d) (* floor division *) - | Some `Ceil -> Some (Mpzf.cdiv_q n d) (* ceiling division *) - | None -> None + | Some `Floor -> Some (Mpzf.mul scale (Mpzf.fdiv_q n d)) (* floor division *) + | Some `Ceil -> Some (Mpzf.mul scale (Mpzf.cdiv_q n d)) (* ceiling division *) + | None -> let product = Mpzf.mul scale n in if Mpz.divisible_p product d then + Some (Mpzf.divexact product d) (* scale, preferably with common denominator *) + else None end in Z_mlgmpidl.z_of_mpzf z | _ -> - failwith ("int_of_scalar: unsupported: " ^ Scalar.to_string scalar) + failwith ("int_of_scalar: unsupported: " ^ Scalar.show scalar) module type ConvertArg = @@ -109,7 +113,7 @@ struct | `Bot -> raise (Unsupported_CilExp Exp_not_supported) (* This should never happen according to Michael Schwarz *) | `Top -> IntDomain.IntDomTuple.top_of ik | `Lifted x -> x (* Cast should be unnecessary because it should be taken care of by EvalInt. *) in - if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp/query: %a -> %a" d_plainexp e IntDomain.IntDomTuple.pretty res; + if M.tracing then M.trace "relation-query" "texpr1_expr_of_cil_exp/query: %a -> %a" d_plainexp e IntDomain.IntDomTuple.pretty res; res in (* recurse without env and ask arguments *) @@ -136,8 +140,15 @@ struct let expr = (** simplify asks for a constant value of some subexpression e, similar to a constant fold. In particular but not exclusively this query is answered by the 2 var equalities domain itself. This normalizes arbitrary expressions to a point where they - might be able to be represented by means of 2 var equalities *) + might be able to be represented by means of 2 var equalities + + This simplification happens during a time, when there are temporary variables a#in and a#out part of the expression, + but are not represented in the ctx, thus queries may result in top for these variables. Wrapping this in speculative + mode is a stop-gap measure to avoid flagging overflows. We however should address simplification in a more generally useful way. + outside of the apron-related expression conversion. + *) let simplify e = + GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> let ikind = try (Cilfacade.get_ikind_exp e) with Invalid_argument _ -> raise (Unsupported_CilExp Exp_not_supported) in let simp = query e ikind in let const = IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to ikind simp in @@ -189,7 +200,7 @@ struct in let exp = Cil.constFold false exp in let res = conv exp in - if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp: %a -> %s (%b)" d_plainexp exp (Format.asprintf "%a" Texpr1.print_expr res) (Lazy.force no_ov); + if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp: %a -> %a (%b)" d_plainexp exp Texpr1.Expr.pretty res (Lazy.force no_ov); res let texpr1_of_cil_exp ask d env e no_ov = @@ -238,11 +249,11 @@ module CilOfApron (V: SV) = struct exception Unsupported_Linexpr1 - let cil_exp_of_linexpr1 (linexpr1:Linexpr1.t) = + let cil_exp_of_linexpr1 ?scalewith (linexpr1:Linexpr1.t) = let longlong = TInt(ILongLong,[]) in let coeff_to_const consider_flip (c:Coeff.union_5) = match c with | Scalar c -> - (match int_of_scalar c with + (match int_of_scalar ?scalewith c with | Some i -> let ci,truncation = truncateCilint ILongLong i in if truncation = NoTruncation then @@ -256,15 +267,14 @@ struct else Const (CInt(i,ILongLong,None)), false else - (M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %s" (Scalar.to_string c); raise Unsupported_Linexpr1) + (M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %a" Scalar.pretty c; raise Unsupported_Linexpr1) | None -> raise Unsupported_Linexpr1) | _ -> raise Unsupported_Linexpr1 in let expr = ref (fst @@ coeff_to_const false (Linexpr1.get_cst linexpr1)) in let append_summand (c:Coeff.union_5) v = match V.to_cil_varinfo v with - | Some vinfo -> - (* TODO: What to do with variables that have a type that cannot be stored into ILongLong to avoid overflows? *) + | Some vinfo when IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:(TInt(ILongLong,[])) -> let var = Cilfacade.mkCast ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in let coeff, flip = coeff_to_const true c in let prod = BinOp(Mult, coeff, var, longlong) in @@ -272,17 +282,45 @@ struct expr := BinOp(MinusA,!expr,prod,longlong) else expr := BinOp(PlusA,!expr,prod,longlong) - | None -> M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var: %s" (Var.to_string v); raise Unsupported_Linexpr1 + | None -> M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var: %a" Var.pretty v; raise Unsupported_Linexpr1 + | _ -> M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var in overflow preserving manner: %a" Var.pretty v; raise Unsupported_Linexpr1 in Linexpr1.iter append_summand linexpr1; !expr + let lcm_den linexpr1 = + let exception UnsupportedScalar + in + let frac_of_scalar scalar = + if Scalar.is_infty scalar <> 0 then (* infinity means unbounded *) + None + else match scalar with + | Float f -> if Stdlib.Float.is_integer f then Some (Q.of_float f) else None + | Mpqf f -> Some (Z_mlgmpidl.q_of_mpqf f) + | _ -> raise UnsupportedScalar + in + let extract_den (c:Coeff.union_5) = + match c with + | Scalar c -> BatOption.map Q.den (frac_of_scalar c) + | _ -> None + in + let lcm_denom = ref (BatOption.default Z.one (extract_den (Linexpr1.get_cst linexpr1))) in + let lcm_coeff (c:Coeff.union_5) _ = + match (extract_den c) with + | Some z -> lcm_denom := Z.lcm z !lcm_denom + | _ -> () + in + try + Linexpr1.iter lcm_coeff linexpr1; !lcm_denom + with UnsupportedScalar -> Z.one + let cil_exp_of_lincons1 (lincons1:Lincons1.t) = let zero = Cil.kinteger ILongLong 0 in try let linexpr1 = Lincons1.get_linexpr1 lincons1 in - let cilexp = cil_exp_of_linexpr1 linexpr1 in + let common_denominator = lcm_den linexpr1 in + let cilexp = cil_exp_of_linexpr1 ~scalewith:common_denominator linexpr1 in match Lincons1.get_typ lincons1 with | EQ -> Some (Cil.constFold false @@ BinOp(Eq, cilexp, zero, TInt(IInt,[]))) | SUPEQ -> Some (Cil.constFold false @@ BinOp(Ge, cilexp, zero, TInt(IInt,[]))) diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml index 35d73e5f28..08353f4795 100644 --- a/src/cdomains/lockDomain.ml +++ b/src/cdomains/lockDomain.ml @@ -24,6 +24,8 @@ struct else Some false + let of_var v: t = (v, `NoOffset) + let of_mval ((v, o): Mval.t): t = (v, Offset.Poly.map_indices (fun i -> IndexDomain.to_int i |> Option.get) o) diff --git a/src/common/cdomains/floatOps/floatOps.ml b/src/common/cdomains/floatOps/floatOps.ml index 80946b1749..eced6af248 100644 --- a/src/common/cdomains/floatOps/floatOps.ml +++ b/src/common/cdomains/floatOps/floatOps.ml @@ -16,7 +16,7 @@ module type CFloatType = sig val pi : t val of_float: round_mode -> float -> t - val to_float: t -> float option + val to_float: t -> float val to_big_int: t -> Z.t val is_finite: t -> bool @@ -68,7 +68,7 @@ module CDouble = struct let pi = Float.pi let of_float _ x = x - let to_float x = Some x + let to_float x = x let to_big_int = big_int_of_float let is_finite = Float.is_finite @@ -112,7 +112,7 @@ module CFloat = struct let smallest = smallest' () let pi = pi' () - let to_float x = Some x + let to_float x = x let to_big_int = big_int_of_float let is_finite x = Float.is_finite x && x >= lower_bound && x <= upper_bound diff --git a/src/common/cdomains/floatOps/floatOps.mli b/src/common/cdomains/floatOps/floatOps.mli index 7cd74f7e7d..a07582f442 100644 --- a/src/common/cdomains/floatOps/floatOps.mli +++ b/src/common/cdomains/floatOps/floatOps.mli @@ -17,7 +17,7 @@ module type CFloatType = sig val pi : t val of_float: round_mode -> float -> t - val to_float: t -> float option + val to_float: t -> float val to_big_int: t -> Z.t val is_finite: t -> bool diff --git a/src/common/domains/printable.ml b/src/common/domains/printable.ml index 1a642c932a..e001a2b557 100644 --- a/src/common/domains/printable.ml +++ b/src/common/domains/printable.ml @@ -88,6 +88,20 @@ struct let to_yojson x = `String (show x) end +module type Formatable = +sig + type t + val pp: Format.formatter -> t -> unit +end + +module SimpleFormat (P: Formatable) = +struct + let show x = GobFormat.asprint P.pp x + let pretty () x = text (show x) + let printXml f x = BatPrintf.fprintf f "\n\n%s\n\n\n" (XmlUtil.escape (show x)) + let to_yojson x = `String (show x) +end + module type Name = sig val name: string end module UnitConf (N: Name) = @@ -588,7 +602,7 @@ module Prod4 (Base1: S) (Base2: S) (Base3: S) (Base4: S) = struct let arbitrary () = QCheck.quad (Base1.arbitrary ()) (Base2.arbitrary ()) (Base3.arbitrary ()) (Base4.arbitrary ()) end -module PQueue (Base: S) = +module PQueue (Base: S) = struct type t = Base.t BatDeque.dq include Std @@ -604,22 +618,22 @@ struct let rec loop n q = match BatDeque.front q with | None -> () - | Some (x, xs) -> (BatPrintf.fprintf f "%d\n%a\n" n Base.printXml x; + | Some (x, xs) -> (BatPrintf.fprintf f "%d\n%a\n" n Base.printXml x; loop (n+1) (xs)) in BatPrintf.fprintf f "\n\n"; - loop 0 xs; + loop 0 xs; BatPrintf.fprintf f "\n\n" let to_yojson q = `List (BatDeque.to_list @@ BatDeque.map (Base.to_yojson) q) let hash q = BatDeque.fold_left (fun acc x -> (acc + 71) * (Base.hash x)) 11 q let equal q1 q2 = BatDeque.eq ~eq:Base.equal q1 q2 - let compare q1 q2 = + let compare q1 q2 = match BatDeque.front q1, BatDeque.front q2 with | None, None -> 0 | None, Some(_, _) -> -1 | Some(_, _), None -> 1 - | Some(a1, q1'), Some(a2, q2') -> + | Some(a1, q1'), Some(a2, q2') -> let c = Base.compare a1 a2 in if c <> 0 then c else compare q1' q2' diff --git a/src/common/util/gobFormat.ml b/src/common/util/gobFormat.ml index 3cda0a4758..8f26ff0087 100644 --- a/src/common/util/gobFormat.ml +++ b/src/common/util/gobFormat.ml @@ -19,3 +19,12 @@ let pp_set_ansi_color_tags ppf = Format.pp_set_mark_tags ppf true let pp_print_nothing (ppf: Format.formatter) () = () + +let pp_infinity = 1000000001 (* Exact value not exposed before OCaml 5.2, but use the smallest value permitted by documentation. *) + +let pp_set_infinite_geometry = Format.pp_set_geometry ~max_indent:(pp_infinity - 2) ~margin:(pp_infinity - 1) + +let asprintf (fmt: ('a, Format.formatter, unit, string) format4): 'a = + Format.asprintf ("%t" ^^ fmt) pp_set_infinite_geometry + +let asprint pp x = asprintf "%a" pp x (* eta-expanded to bypass value restriction *) diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 779b9bbf65..16c9d7e8ef 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -344,7 +344,7 @@ "default": [ "expRelation", "base", "threadid", "threadflag", "threadreturn", "escape", "mutexEvents", "mutex", "access", "race", "mallocWrapper", "mhp", - "assert" + "assert", "pthreadMutexType" ] }, "path_sens": { @@ -980,7 +980,7 @@ }, "gas_value": { "title": "ana.context.gas_value", - "description": "Denotes the gas value x for the ContextGasLifter. Negative values deactivate the context gas, zero yields a context-insensitve analysis. If enabled, the first x recursive calls of the call stack are analyzed context-sensitively. Any calls deeper in the call stack are analyzed with the same (empty) context.", + "description": "Denotes the gas value x for the ContextGasLifter. Negative values deactivate the context gas, zero yields a context-insensitive analysis. If enabled, the first x recursive calls of the call stack are analyzed context-sensitively. Any calls deeper in the call stack are analyzed with the same (empty) context.", "type": "integer", "default": -1 }, @@ -1561,6 +1561,26 @@ "description": "Output filename for transformations that output a transformed file.", "type":"string", "default": "transformed.c" + }, + "assert" : { + "title": "trans.assert", + "type": "object", + "properties": { + "function": { + "title": "trans.assert.function", + "description": "Function to use for assertions in output.", + "type": "string", + "enum": ["assert", "__goblint_check", "__VERIFIER_assert"], + "default": "__VERIFIER_assert" + }, + "wrap-atomic": { + "title": "trans.assert.wrap-atomic", + "description": "Wrap assertions in __VERIFIER_atomic_begin and __VERIFIER_atomic_end.", + "type": "boolean", + "default": true + } + }, + "additionalProperties": false } }, "additionalProperties": false diff --git a/src/domain/lattice.ml b/src/domain/lattice.ml index 99322c09d8..d45ddcbfc2 100644 --- a/src/domain/lattice.ml +++ b/src/domain/lattice.ml @@ -277,6 +277,8 @@ struct let narrow x y = match (x,y) with | (`Lifted x, `Lifted y) -> `Lifted (Base.narrow x y) + | (_, `Bot) -> `Bot + | (`Top, y) -> y | _ -> x end @@ -337,6 +339,8 @@ struct | (`Lifted x, `Lifted y) -> (try `Lifted (Base.narrow x y) with Uncomparable -> `Bot) + | (_, `Bot) -> `Bot + | (`Top, y) -> y | _ -> x end @@ -408,6 +412,8 @@ struct match (x,y) with | (`Lifted1 x, `Lifted1 y) -> `Lifted1 (Base1.narrow x y) | (`Lifted2 x, `Lifted2 y) -> `Lifted2 (Base2.narrow x y) + | (_, `Bot) -> `Bot + | (`Top, y) -> y | _ -> x end @@ -539,6 +545,7 @@ struct let narrow x y = match (x,y) with | (`Lifted x, `Lifted y) -> `Lifted (Base.narrow x y) + | (_, `Bot) -> `Bot | _ -> x end @@ -580,6 +587,7 @@ struct let narrow x y = match (x,y) with | (`Lifted x, `Lifted y) -> `Lifted (Base.narrow x y) + | (`Top, y) -> y | _ -> x let pretty_diff () (x,y) = diff --git a/src/domain/setDomain.ml b/src/domain/setDomain.ml index 1b5239de80..c552363f3d 100644 --- a/src/domain/setDomain.ml +++ b/src/domain/setDomain.ml @@ -184,7 +184,7 @@ struct end ) - let hash x = fold (fun x y -> y + Base.hash x) x 0 + let hash x = fold (fun x y -> 13 * y + Base.hash x) x 0 let relift x = map Base.relift x @@ -436,23 +436,23 @@ struct include Lattice.Reverse (Base) end -module type FiniteSetElems = +module type FiniteSetElem = sig - type t + include Printable.S val elems: t list + (** List of all possible elements. *) end -(* TODO: put elems into E *) -module FiniteSet (E:Printable.S) (Elems:FiniteSetElems with type t = E.t) = +module FiniteSet (E: FiniteSetElem) = struct module E = struct include E - let arbitrary () = QCheck.oneofl Elems.elems + let arbitrary () = QCheck.oneofl E.elems end include Make (E) - let top () = of_list Elems.elems + let top () = of_list E.elems let is_top x = equal x (top ()) end diff --git a/src/domains/queries.ml b/src/domains/queries.ml index cfeb251523..5436e5f7e0 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -50,8 +50,8 @@ end (* Helper definitions for deriving complex parts of Any.compare below. *) type maybepublic = {global: CilType.Varinfo.t; write: bool; protection: Protection.t} [@@deriving ord, hash] -type maybepublicwithout = {global: CilType.Varinfo.t; write: bool; without_mutex: PreValueDomain.Addr.t; protection: Protection.t} [@@deriving ord, hash] -type mustbeprotectedby = {mutex: PreValueDomain.Addr.t; global: CilType.Varinfo.t; write: bool; protection: Protection.t} [@@deriving ord, hash] +type maybepublicwithout = {global: CilType.Varinfo.t; write: bool; without_mutex: LockDomain.MustLock.t; protection: Protection.t} [@@deriving ord, hash] +type mustbeprotectedby = {mutex: LockDomain.MustLock.t; global: CilType.Varinfo.t; write: bool; protection: Protection.t} [@@deriving ord, hash] type mustprotectedvars = {mutex: LockDomain.MustLock.t; write: bool} [@@deriving ord, hash] type access = | Memory of {exp: CilType.Exp.t; var_opt: CilType.Varinfo.t option; kind: AccessKind.t} (** Memory location access (race). *) @@ -130,6 +130,7 @@ type _ t = | IsEverMultiThreaded: MayBool.t t | TmpSpecial: Mval.Exp.t -> ML.t t | MaySignedOverflow: exp -> MayBool.t t + | GasExhausted: MustBool.t t | YamlEntryGlobal: Obj.t * YamlWitnessType.Task.t -> YS.t t | GhostVarAvailable: WitnessGhostVar.t -> MayBool.t t | InvariantGlobalNodes: NS.t t (* TODO: V.t argument? *) @@ -204,6 +205,7 @@ struct | IsEverMultiThreaded -> (module MayBool) | TmpSpecial _ -> (module ML) | MaySignedOverflow _ -> (module MayBool) + | GasExhausted -> (module MustBool) | YamlEntryGlobal _ -> (module YS) | GhostVarAvailable _ -> (module MayBool) | InvariantGlobalNodes -> (module NS) @@ -277,6 +279,7 @@ struct | IsEverMultiThreaded -> MayBool.top () | TmpSpecial _ -> ML.top () | MaySignedOverflow _ -> MayBool.top () + | GasExhausted -> MustBool.top () | YamlEntryGlobal _ -> YS.top () | GhostVarAvailable _ -> MayBool.top () | InvariantGlobalNodes -> NS.top () @@ -346,10 +349,11 @@ struct | Any (TmpSpecial _) -> 56 | Any (IsAllocVar _) -> 57 | Any (MaySignedOverflow _) -> 58 - | Any (YamlEntryGlobal _) -> 59 - | Any (MustProtectingLocks _) -> 60 - | Any (GhostVarAvailable _) -> 61 - | Any InvariantGlobalNodes -> 62 + | Any GasExhausted -> 59 + | Any (YamlEntryGlobal _) -> 60 + | Any (MustProtectingLocks _) -> 61 + | Any (GhostVarAvailable _) -> 62 + | Any InvariantGlobalNodes -> 63 let rec compare a b = let r = Stdlib.compare (order a) (order b) in @@ -517,6 +521,7 @@ struct | Any IsEverMultiThreaded -> Pretty.dprintf "IsEverMultiThreaded" | Any (TmpSpecial lv) -> Pretty.dprintf "TmpSpecial %a" Mval.Exp.pretty lv | Any (MaySignedOverflow e) -> Pretty.dprintf "MaySignedOverflow %a" CilType.Exp.pretty e + | Any GasExhausted -> Pretty.dprintf "GasExhausted" | Any (GhostVarAvailable v) -> Pretty.dprintf "GhostVarAvailable %a" WitnessGhostVar.pretty v | Any InvariantGlobalNodes -> Pretty.dprintf "InvariantGlobalNodes" end diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index 4ef98358f4..1ea01c99fb 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -209,7 +209,7 @@ sig val context: (D.t, G.t, C.t, V.t) ctx -> fundec -> D.t -> C.t val startcontext: unit -> C.t - val sync : (D.t, G.t, C.t, V.t) ctx -> [`Normal | `Join | `Return] -> D.t + val sync : (D.t, G.t, C.t, V.t) ctx -> [`Normal | `Join | `JoinCall | `Return] -> D.t val query : (D.t, G.t, C.t, V.t) ctx -> 'a Queries.t -> 'a Queries.result (** A transfer function which handles the assignment of a rval to a lval, i.e., diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index f803250b0a..c638f0c273 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -575,8 +575,14 @@ struct let liftmap f = List.map (fun (x) -> (x, max 0 (cg_val ctx - 1))) f in liftmap (S.threadenter (conv ctx) ~multiple lval f args) + let query ctx (type a) (q: a Queries.t):a Queries.result = + match q with + | Queries.GasExhausted -> + let (d,i) = ctx.local in + (i <= 0) + | _ -> S.query (conv ctx) q + let sync ctx reason = S.sync (conv ctx) reason, cg_val ctx - let query ctx q = S.query (conv ctx) q let assign ctx lval expr = S.assign (conv ctx) lval expr, cg_val ctx let vdecl ctx v = S.vdecl (conv ctx) v, cg_val ctx let body ctx fundec = S.body (conv ctx) fundec, cg_val ctx @@ -624,9 +630,10 @@ struct let sync ctx = match ctx.prev_node, Cfg.prev ctx.prev_node with - | _, _ :: _ :: _ (* Join in CFG. *) - | FunctionEntry _, _ -> (* Function entry, also needs sync because partial contexts joined by solver, see 00-sanity/35-join-contexts. *) + | _, _ :: _ :: _ -> (* Join in CFG. *) S.sync ctx `Join + | FunctionEntry _, _ -> (* Function entry, also needs sync because partial contexts joined by solver, see 00-sanity/35-join-contexts. *) + S.sync ctx `JoinCall | _, _ -> S.sync ctx `Normal let side_context sideg f c = @@ -706,11 +713,13 @@ struct let tf_assign var edge prev_node lv e getl sidel getg sideg d = let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in - common_join ctx (S.assign ctx lv e) !r !spawns + let d = S.assign ctx lv e in (* Force transfer function to be evaluated before dereferencing in common_join argument. *) + common_join ctx d !r !spawns let tf_vdecl var edge prev_node v getl sidel getg sideg d = let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in - common_join ctx (S.vdecl ctx v) !r !spawns + let d = S.vdecl ctx v in (* Force transfer function to be evaluated before dereferencing in common_join argument. *) + common_join ctx d !r !spawns let normal_return r fd ctx sideg = let spawning_return = S.return ctx r fd in @@ -725,7 +734,7 @@ struct let tf_ret var edge prev_node ret fd getl sidel getg sideg d = let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in - let d = + let d = (* Force transfer function to be evaluated before dereferencing in common_join argument. *) if (CilType.Fundec.equal fd MyCFG.dummy_func || List.mem fd.svar.vname (get_string_list "mainfun")) && get_bool "kernel" @@ -740,11 +749,13 @@ struct let c: unit -> S.C.t = snd var |> Obj.obj in side_context sideg fd (c ()); let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in - common_join ctx (S.body ctx fd) !r !spawns + let d = S.body ctx fd in (* Force transfer function to be evaluated before dereferencing in common_join argument. *) + common_join ctx d !r !spawns let tf_test var edge prev_node e tv getl sidel getg sideg d = let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in - common_join ctx (S.branch ctx e tv) !r !spawns + let d = S.branch ctx e tv in (* Force transfer function to be evaluated before dereferencing in common_join argument. *) + common_join ctx d !r !spawns let tf_normal_call ctx lv e (f:fundec) args getl sidel getg sideg = let combine (cd, fc, fd) = @@ -863,11 +874,13 @@ struct let tf_asm var edge prev_node getl sidel getg sideg d = let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in - common_join ctx (S.asm ctx) !r !spawns + let d = S.asm ctx in (* Force transfer function to be evaluated before dereferencing in common_join argument. *) + common_join ctx d !r !spawns let tf_skip var edge prev_node getl sidel getg sideg d = let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in - common_join ctx (S.skip ctx) !r !spawns + let d = S.skip ctx in (* Force transfer function to be evaluated before dereferencing in common_join argument. *) + common_join ctx d !r !spawns let tf var getl sidel getg sideg prev_node edge d = begin match edge with diff --git a/src/framework/control.ml b/src/framework/control.ml index 05fad90caf..5e92282210 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -357,6 +357,7 @@ struct (* real beginning of the [analyze] function *) if get_bool "ana.sv-comp.enabled" then Witness.init (module FileCfg); (* TODO: move this out of analyze_loop *) + YamlWitness.init (); AnalysisState.global_initialization := true; GobConfig.earlyglobs := get_bool "exp.earlyglobs"; @@ -789,15 +790,19 @@ struct ); (* Before SV-COMP, so result can depend on YAML witness validation. *) - if get_string "witness.yaml.validate" <> "" then ( - let module YWitness = YamlWitness.Validator (R) in - YWitness.validate () - ); + let yaml_validate_result = + if get_string "witness.yaml.validate" <> "" then ( + let module YWitness = YamlWitness.Validator (R) in + Some (YWitness.validate ()) + ) + else + None + in if get_bool "ana.sv-comp.enabled" then ( (* SV-COMP and witness generation *) let module WResult = Witness.Result (R) in - WResult.write entrystates + WResult.write yaml_validate_result entrystates ); if get_bool "witness.yaml.enabled" then ( diff --git a/src/goblint.ml b/src/goblint.ml index a687badb8e..52b9bbdfc0 100644 --- a/src/goblint.ml +++ b/src/goblint.ml @@ -83,6 +83,11 @@ let main () = Logs.error "%s" (MessageUtil.colorize ~fd:Unix.stderr ("{RED}Analysis was aborted because it reached the set timeout of " ^ get_string "dbg.timeout" ^ " or was signalled SIGPROF!")); Goblint_timing.teardown_tef (); exit 124 + | Svcomp.Error msg -> + do_stats (); + Witness.print_svcomp_result ("ERROR (" ^ msg ^ ")"); + Goblint_timing.teardown_tef (); + exit 1 (* We do this since the evaluation order of top-level bindings is not defined, but we want `main` to run after all the other side-effects (e.g. registering analyses/solvers) have happened. *) let () = at_exit main diff --git a/src/solver/generic.ml b/src/solver/generic.ml index 1f0df57843..737aba6762 100644 --- a/src/solver/generic.ml +++ b/src/solver/generic.ml @@ -44,7 +44,7 @@ struct let histo = HM.create 1024 let increase (v:Var.t) = let set v c = - if not full_trace && (c > start_c && c > !max_c && (Option.is_none !max_var || not (Var.equal (Option.get !max_var) v))) then begin + if not full_trace && (c > start_c && c > !max_c && not (GobOption.exists (Var.equal v) !max_var)) then begin if tracing then trace "sol" "Switched tracing to %a" Var.pretty_trace v; max_c := c; max_var := Some v @@ -75,7 +75,7 @@ struct let update_var_event x o n = if tracing then increase x; - if full_trace || ((not (Dom.is_bot o)) && Option.is_some !max_var && Var.equal (Option.get !max_var) x) then begin + if full_trace || (not (Dom.is_bot o) && GobOption.exists (Var.equal x) !max_var) then begin if tracing then tracei "sol_max" "(%d) Update to %a" !max_c Var.pretty_trace x; if tracing then traceu "sol_max" "%a" Dom.pretty_diff (n, o) end diff --git a/src/transform/evalAssert.ml b/src/transform/evalAssert.ml index eab06222ef..0fee26355b 100644 --- a/src/transform/evalAssert.ml +++ b/src/transform/evalAssert.ml @@ -22,12 +22,8 @@ open Formatcil will be removed and they will fail on the next iteration *) -module EvalAssert = struct - (* should asserts be surrounded by __VERIFIER_atomic_{begin,end}? *) - let surroundByAtomic = true - - (* Cannot use Cilfacade.name_fundecs as assert() is external and has no fundec *) - let ass = makeVarinfo true "__VERIFIER_assert" (TVoid []) +module EvalAssert = +struct let atomicBegin = makeVarinfo true "__VERIFIER_atomic_begin" (TVoid []) let atomicEnd = makeVarinfo true "__VERIFIER_atomic_end" (TVoid []) @@ -39,6 +35,11 @@ module EvalAssert = struct val emit_after_lock = GobConfig.get_bool "witness.invariant.after-lock" val emit_other = GobConfig.get_bool "witness.invariant.other" + (* Cannot use Cilfacade.name_fundecs as assert() is external and has no fundec *) + val assert_function = makeVarinfo true (GobConfig.get_string "trans.assert.function") (TVoid []) + (* should asserts be surrounded by __VERIFIER_atomic_{begin,end}? *) + val surroundByAtomic = GobConfig.get_bool "trans.assert.wrap-atomic" + method! vstmt s = let is_lock exp args = match exp with @@ -59,7 +60,7 @@ module EvalAssert = struct match (ask ~node loc).f (Queries.Invariant context) with | `Lifted e -> let es = WitnessUtil.InvariantExp.process_exp e in - let asserts = List.map (fun e -> cInstr ("%v:assert (%e:exp);") loc [("assert", Fv ass); ("exp", Fe e)]) es in + let asserts = List.map (fun e -> cInstr ("%v:assert (%e:exp);") loc [("assert", Fv assert_function); ("exp", Fe e)]) es in if surroundByAtomic then let abegin = (cInstr ("%v:__VERIFIER_atomic_begin();") loc [("__VERIFIER_atomic_begin", Fv atomicBegin)]) in let aend = (cInstr ("%v:__VERIFIER_atomic_end();") loc [("__VERIFIER_atomic_end", Fv atomicEnd)]) in diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml index 452bd9cccd..48ce84b276 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -1247,7 +1247,7 @@ let libraries = descs_tbl ) libraries -let all_library_descs: (string, LibraryDesc.t) Hashtbl.t = +let _all_library_descs: (string, LibraryDesc.t) Hashtbl.t = Hashtbl.fold (fun _ descs_tbl acc -> Hashtbl.merge (fun name desc1 desc2 -> match desc1, desc2 with diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml index bb887e6cb1..59a8f01b40 100644 --- a/src/witness/svcomp.ml +++ b/src/witness/svcomp.ml @@ -60,6 +60,11 @@ struct | Unknown -> "unknown" end +exception Error of string + +let errorwith s = raise (Error s) + + module type TaskResult = sig module Arg: MyARG.S diff --git a/src/witness/witness.ml b/src/witness/witness.ml index fb88c2ce7b..7b0213b601 100644 --- a/src/witness/witness.ml +++ b/src/witness/witness.ml @@ -690,25 +690,16 @@ struct Timing.wrap "graphml witness" (write_file witness_path (module Task)) (module TaskResult) ) - let write entrystates = + let write yaml_validate_result entrystates = match !AnalysisState.verified with | Some false -> print_svcomp_result "ERROR (verify)" | _ -> - if get_string "witness.yaml.validate" <> "" then ( - match get_bool "witness.yaml.strict" with - | true when !YamlWitness.cnt_error > 0 -> - print_svcomp_result "ERROR (witness error)" - | true when !YamlWitness.cnt_unsupported > 0 -> - print_svcomp_result "ERROR (witness unsupported)" - | true when !YamlWitness.cnt_disabled > 0 -> - print_svcomp_result "ERROR (witness disabled)" - | _ when !YamlWitness.cnt_refuted > 0 -> - print_svcomp_result (Result.to_string (False None)) - | _ when !YamlWitness.cnt_unconfirmed > 0 -> - print_svcomp_result (Result.to_string Unknown) - | _ -> - write entrystates - ) - else + match yaml_validate_result with + | Some (Stdlib.Error msg) -> + print_svcomp_result ("ERROR (" ^ msg ^ ")") + | Some (Ok (Svcomp.Result.False _ | Unknown as result)) -> + print_svcomp_result (Result.to_string result) + | Some (Ok True) + | None -> write entrystates end diff --git a/src/witness/witnessGhostVar.ml b/src/witness/witnessGhostVar.ml index c6f780c8ae..82813b4a65 100644 --- a/src/witness/witnessGhostVar.ml +++ b/src/witness/witnessGhostVar.ml @@ -1,12 +1,12 @@ (** Ghost variables for YAML witnesses. *) type t = - | Locked of LockDomain.Addr.t (* TODO: change *) + | Locked of LockDomain.MustLock.t | Multithreaded [@@deriving eq, ord, hash] let name_varinfo = function - | Locked (Addr (v, os)) -> + | Locked (v, os) -> let name = if CilType.Varinfo.equal v LibraryFunctions.verifier_atomic_var then invalid_arg "__VERIFIER_atomic" @@ -16,16 +16,13 @@ let name_varinfo = function else Basetype.Variables.show v in - let rec offs: LockDomain.Addr.Offs.t -> string = function + let rec offs: Offset.Z.t -> string = function | `NoOffset -> "" | `Field (f, os') -> "_" ^ f.fname ^ offs os' | `Index (i, os') -> - match ValueDomain.ID.to_int i with - | Some i -> assert Z.Compare.(i >= Z.zero); "_" ^ Z.to_string i - | _ -> assert false (* must locksets cannot have ambiguous indices *) + assert Z.Compare.(i >= Z.zero); "_" ^ Z.to_string i in name ^ offs os ^ "_locked" - | Locked _ -> assert false | Multithreaded -> "multithreaded" let show = name_varinfo diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 596a35f631..d3988f8edb 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -575,6 +575,15 @@ struct Timing.wrap "yaml witness" write () end +let init () = + match GobConfig.get_string "witness.yaml.validate" with + | "" -> () + | path -> + (* Check witness existence before doing the analysis. *) + if not (Sys.file_exists path) then ( + Logs.error "witness.yaml.validate: %s not found" path; + Svcomp.errorwith "witness missing" + ) module ValidationResult = struct @@ -642,7 +651,9 @@ struct let yaml = match Yaml_unix.of_file (Fpath.v (GobConfig.get_string "witness.yaml.validate")) with | Ok yaml -> yaml - | Error (`Msg m) -> failwith ("Yaml_unix.of_file: " ^ m) + | Error (`Msg m) -> + Logs.error "Yaml_unix.of_file: %s" m; + Svcomp.errorwith "witness missing" in let yaml_entries = yaml |> GobYaml.list |> BatResult.get_ok in @@ -901,5 +912,19 @@ struct let certificate_path = GobConfig.get_string "witness.yaml.certificate" in if certificate_path <> "" then - yaml_entries_to_file (List.rev yaml_entries') (Fpath.v certificate_path) + yaml_entries_to_file (List.rev yaml_entries') (Fpath.v certificate_path); + + match GobConfig.get_bool "witness.yaml.strict" with + | true when !cnt_error > 0 -> + Error "witness error" + | true when !cnt_unsupported > 0 -> + Error "witness unsupported" + | true when !cnt_disabled > 0 -> + Error "witness disabled" + | _ when !cnt_refuted > 0 -> + Ok (Svcomp.Result.False None) + | _ when !cnt_unconfirmed > 0 -> + Ok Unknown + | _ -> + Ok True end diff --git a/tests/regression/01-cpa/71-widen-sides.c b/tests/regression/01-cpa/71-widen-sides.c index 522f6fae44..a93124c6e5 100644 --- a/tests/regression/01-cpa/71-widen-sides.c +++ b/tests/regression/01-cpa/71-widen-sides.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.ctx_insens "['base', 'mallocWrapper']" --enable ana.int.interval --sets solvers.td3.side_widen sides-local +// PARAM: --set ana.ctx_insens "['base', 'mallocWrapper']" --enable ana.int.interval --set solvers.td3.side_widen sides-local #include int further(int n) { diff --git a/tests/regression/03-practical/33-threshold-narrowing-intervals.c b/tests/regression/03-practical/33-threshold-narrowing-intervals.c new file mode 100644 index 0000000000..ef38c151da --- /dev/null +++ b/tests/regression/03-practical/33-threshold-narrowing-intervals.c @@ -0,0 +1,13 @@ +// PARAM: --enable ana.int.interval --enable ana.int.interval_threshold_widening --set ana.int.interval_threshold_widening_constants comparisons +#include + +int main() { + int i; + for(i = 0; i < 10 && i < 20; i += 3); + __goblint_check(i <= 12); + + int j; + for(j = 0; j > -10 && j > -20; j-= 3); + __goblint_check(j >= -12); + +} diff --git a/tests/regression/03-practical/34-threshold-narrowing-interval-sets.c b/tests/regression/03-practical/34-threshold-narrowing-interval-sets.c new file mode 100644 index 0000000000..c1f11c091e --- /dev/null +++ b/tests/regression/03-practical/34-threshold-narrowing-interval-sets.c @@ -0,0 +1,13 @@ +// PARAM: --enable ana.int.interval_set --enable ana.int.interval_threshold_widening --set ana.int.interval_threshold_widening_constants comparisons +#include + +int main() { + int i; + for(i = 0; i < 10 && i < 20; i += 3); + __goblint_check(i <= 12); + + int j; + for(j = 0; j > -10 && j > -20; j-= 3); + __goblint_check(j >= -12); + +} diff --git a/tests/regression/13-privatized/93-unlock-idx-ambiguous.c b/tests/regression/13-privatized/93-unlock-idx-ambiguous.c new file mode 100644 index 0000000000..081302514b --- /dev/null +++ b/tests/regression/13-privatized/93-unlock-idx-ambiguous.c @@ -0,0 +1,27 @@ +// PARAM: --set ana.base.privatization protection --enable ana.sv-comp.functions +#include +#include +extern _Bool __VERIFIER_nondet_bool(); + +int g; +pthread_mutex_t m[2] = {PTHREAD_MUTEX_INITIALIZER, PTHREAD_MUTEX_INITIALIZER}; + +void *t_fun(void *arg) { + pthread_mutex_lock(&m[0]); + pthread_mutex_lock(&m[1]); // so we're unlocking a mutex we definitely hold + g++; + int r = __VERIFIER_nondet_bool(); + pthread_mutex_unlock(&m[r]); // TODO NOWARN (definitely held either way) + // could have unlocked m[0], so should have published g there + return NULL; +} + +int main() { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + + pthread_mutex_lock(&m[0]); + __goblint_check(g == 0); // UNKNOWN! + pthread_mutex_unlock(&m[0]); + return 0; +} diff --git a/tests/regression/13-privatized/93-unlock-idx-ambiguous.t b/tests/regression/13-privatized/93-unlock-idx-ambiguous.t new file mode 100644 index 0000000000..8f24d728bf --- /dev/null +++ b/tests/regression/13-privatized/93-unlock-idx-ambiguous.t @@ -0,0 +1,65 @@ + $ goblint --set ana.base.privatization protection --enable ana.sv-comp.functions 93-unlock-idx-ambiguous.c + [Warning][Unknown] unlocking mutex (m[def_exc:Unknown int([0,1])]) which may not be held (93-unlock-idx-ambiguous.c:14:3-14:30) + [Warning][Assert] Assertion "g == 0" is unknown. (93-unlock-idx-ambiguous.c:24:3-24:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 14 + dead: 0 + total lines: 14 + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 0 + total memory locations: 1 + + $ goblint --set ana.base.privatization mutex-meet --enable ana.sv-comp.functions 93-unlock-idx-ambiguous.c + [Warning][Unknown] unlocking mutex (m[def_exc:Unknown int([0,1])]) which may not be held (93-unlock-idx-ambiguous.c:14:3-14:30) + [Warning][Assert] Assertion "g == 0" is unknown. (93-unlock-idx-ambiguous.c:24:3-24:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 14 + dead: 0 + total lines: 14 + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 0 + total memory locations: 1 + + $ goblint --set ana.base.privatization lock --enable ana.sv-comp.functions 93-unlock-idx-ambiguous.c + [Warning][Unknown] unlocking mutex (m[def_exc:Unknown int([0,1])]) which may not be held (93-unlock-idx-ambiguous.c:14:3-14:30) + [Warning][Assert] Assertion "g == 0" is unknown. (93-unlock-idx-ambiguous.c:24:3-24:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 14 + dead: 0 + total lines: 14 + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 0 + total memory locations: 1 + + $ goblint --set ana.base.privatization write --enable ana.sv-comp.functions 93-unlock-idx-ambiguous.c + [Warning][Unknown] unlocking mutex (m[def_exc:Unknown int([0,1])]) which may not be held (93-unlock-idx-ambiguous.c:14:3-14:30) + [Warning][Assert] Assertion "g == 0" is unknown. (93-unlock-idx-ambiguous.c:24:3-24:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 14 + dead: 0 + total lines: 14 + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 0 + total memory locations: 1 + + $ goblint --set ana.base.privatization mine-nothread --enable ana.sv-comp.functions 93-unlock-idx-ambiguous.c + [Warning][Unknown] unlocking mutex (m[def_exc:Unknown int([0,1])]) which may not be held (93-unlock-idx-ambiguous.c:14:3-14:30) + [Warning][Assert] Assertion "g == 0" is unknown. (93-unlock-idx-ambiguous.c:24:3-24:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 14 + dead: 0 + total lines: 14 + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 0 + total memory locations: 1 + diff --git a/tests/regression/13-privatized/94-unlock-unknown.c b/tests/regression/13-privatized/94-unlock-unknown.c new file mode 100644 index 0000000000..0897c38de8 --- /dev/null +++ b/tests/regression/13-privatized/94-unlock-unknown.c @@ -0,0 +1,25 @@ +// PARAM: --set ana.base.privatization protection --enable ana.sv-comp.functions +#include +#include + +int g; +pthread_mutex_t m[2] = {PTHREAD_MUTEX_INITIALIZER, PTHREAD_MUTEX_INITIALIZER}; + +void *t_fun(void *arg) { + pthread_mutex_lock(&m[0]); + g++; + pthread_mutex_t *r; // rand + pthread_mutex_unlock(r); + // could have unlocked m[0], so should have published g there + return NULL; +} + +int main() { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + + pthread_mutex_lock(&m[0]); + __goblint_check(g == 0); // UNKNOWN! + pthread_mutex_unlock(&m[0]); + return 0; +} diff --git a/tests/regression/13-privatized/94-unlock-unknown.t b/tests/regression/13-privatized/94-unlock-unknown.t new file mode 100644 index 0000000000..cc0aa921fe --- /dev/null +++ b/tests/regression/13-privatized/94-unlock-unknown.t @@ -0,0 +1,70 @@ + $ goblint --set ana.base.privatization protection --enable ana.sv-comp.functions 94-unlock-unknown.c + [Warning][Unknown] unlocking unknown mutex which may not be held (94-unlock-unknown.c:12:3-12:26) + [Warning][Unknown] unlocking NULL mutex (94-unlock-unknown.c:12:3-12:26) + [Warning][Assert] Assertion "g == 0" is unknown. (94-unlock-unknown.c:22:3-22:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 11 + dead: 0 + total lines: 11 + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 0 + total memory locations: 1 + + $ goblint --set ana.base.privatization mutex-meet --enable ana.sv-comp.functions 94-unlock-unknown.c + [Warning][Unknown] unlocking unknown mutex which may not be held (94-unlock-unknown.c:12:3-12:26) + [Warning][Unknown] unlocking NULL mutex (94-unlock-unknown.c:12:3-12:26) + [Warning][Assert] Assertion "g == 0" is unknown. (94-unlock-unknown.c:22:3-22:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 11 + dead: 0 + total lines: 11 + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 0 + total memory locations: 1 + + $ goblint --set ana.base.privatization lock --enable ana.sv-comp.functions 94-unlock-unknown.c + [Warning][Unknown] unlocking unknown mutex which may not be held (94-unlock-unknown.c:12:3-12:26) + [Warning][Unknown] unlocking NULL mutex (94-unlock-unknown.c:12:3-12:26) + [Warning][Assert] Assertion "g == 0" is unknown. (94-unlock-unknown.c:22:3-22:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 11 + dead: 0 + total lines: 11 + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 0 + total memory locations: 1 + + $ goblint --set ana.base.privatization write --enable ana.sv-comp.functions 94-unlock-unknown.c + [Warning][Unknown] unlocking unknown mutex which may not be held (94-unlock-unknown.c:12:3-12:26) + [Warning][Unknown] unlocking NULL mutex (94-unlock-unknown.c:12:3-12:26) + [Warning][Assert] Assertion "g == 0" is unknown. (94-unlock-unknown.c:22:3-22:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 11 + dead: 0 + total lines: 11 + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 0 + total memory locations: 1 + + $ goblint --set ana.base.privatization mine-nothread --enable ana.sv-comp.functions 94-unlock-unknown.c + [Warning][Unknown] unlocking unknown mutex which may not be held (94-unlock-unknown.c:12:3-12:26) + [Warning][Unknown] unlocking NULL mutex (94-unlock-unknown.c:12:3-12:26) + [Warning][Assert] Assertion "g == 0" is unknown. (94-unlock-unknown.c:22:3-22:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 11 + dead: 0 + total lines: 11 + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 0 + total memory locations: 1 + diff --git a/tests/regression/36-apron/45-context.c b/tests/regression/36-apron/45-context.c index 94328af97f..eda945abd5 100644 --- a/tests/regression/36-apron/45-context.c +++ b/tests/regression/36-apron/45-context.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.int.interval --enable ana.relation.context +// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.int.interval --enable ana.relation.context extern int __VERIFIER_nondet_int(); #include diff --git a/tests/regression/36-apron/46-no-context.c b/tests/regression/36-apron/46-no-context.c index bf115cee24..640784b913 100644 --- a/tests/regression/36-apron/46-no-context.c +++ b/tests/regression/36-apron/46-no-context.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.int.interval --disable ana.relation.context +// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.int.interval --disable ana.relation.context extern int __VERIFIER_nondet_int(); #include diff --git a/tests/regression/36-apron/47-no-context-attribute.c b/tests/regression/36-apron/47-no-context-attribute.c index 90b58cdc28..cf111f5ffc 100644 --- a/tests/regression/36-apron/47-no-context-attribute.c +++ b/tests/regression/36-apron/47-no-context-attribute.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.int.interval --enable ana.relation.context +// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.int.interval --enable ana.relation.context extern int __VERIFIER_nondet_int(); #include diff --git a/tests/regression/36-apron/48-context-attribute.c b/tests/regression/36-apron/48-context-attribute.c index 5e5ecf01fe..3304c20388 100644 --- a/tests/regression/36-apron/48-context-attribute.c +++ b/tests/regression/36-apron/48-context-attribute.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.int.interval --disable ana.relation.context +// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.int.interval --disable ana.relation.context extern int __VERIFIER_nondet_int(); #include diff --git a/tests/regression/36-apron/86-branched-thread-creation.c b/tests/regression/36-apron/86-branched-thread-creation.c index cac0a881a6..91a5411e8f 100644 --- a/tests/regression/36-apron/86-branched-thread-creation.c +++ b/tests/regression/36-apron/86-branched-thread-creation.c @@ -40,7 +40,7 @@ int main(void) { if(!mt) { pthread_mutex_lock(&mutex); - __goblint_check(g==h); //MAYFAIL + __goblint_check(g==h); //FAIL pthread_mutex_unlock(&mutex); } diff --git a/tests/regression/46-apron2/03-other-assume.c b/tests/regression/46-apron2/03-other-assume.c index 635911a197..c136d1bde3 100644 --- a/tests/regression/46-apron2/03-other-assume.c +++ b/tests/regression/46-apron2/03-other-assume.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --sets ana.relation.privatization mutex-meet-tid +// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --set ana.relation.privatization mutex-meet-tid #include #include diff --git a/tests/regression/46-apron2/04-other-assume-inprec.c b/tests/regression/46-apron2/04-other-assume-inprec.c index 09b8d150a8..ccf8ecefa1 100644 --- a/tests/regression/46-apron2/04-other-assume-inprec.c +++ b/tests/regression/46-apron2/04-other-assume-inprec.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --sets ana.relation.privatization mutex-meet-tid +// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --set ana.relation.privatization mutex-meet-tid #include #include diff --git a/tests/regression/46-apron2/26-autotune.c b/tests/regression/46-apron2/26-autotune.c index 96c5c85278..ec8f55fe19 100644 --- a/tests/regression/46-apron2/26-autotune.c +++ b/tests/regression/46-apron2/26-autotune.c @@ -1,4 +1,4 @@ -//SKIP PARAM: --enable ana.int.interval --sets sem.int.signed_overflow assume_none --set ana.activated[+] apron --enable ana.autotune.enabled +//SKIP PARAM: --enable ana.int.interval --set sem.int.signed_overflow assume_none --set ana.activated[+] apron --enable ana.autotune.enabled // Check that autotuner disables context for apron as well for recursive calls #include diff --git a/tests/regression/46-apron2/30-autotune-stub.c b/tests/regression/46-apron2/30-autotune-stub.c index e1b7603c3b..02c80e7d21 100644 --- a/tests/regression/46-apron2/30-autotune-stub.c +++ b/tests/regression/46-apron2/30-autotune-stub.c @@ -1,4 +1,4 @@ -//SKIP PARAM: --enable ana.int.interval --sets sem.int.signed_overflow assume_none --set ana.activated[+] apron --enable ana.autotune.enabled +//SKIP PARAM: --enable ana.int.interval --set sem.int.signed_overflow assume_none --set ana.activated[+] apron --enable ana.autotune.enabled // Check that autotuner respect goblint_stub attributes as hints to not track variables. #include diff --git a/tests/regression/46-apron2/87-unlock-idx-ambiguous.c b/tests/regression/46-apron2/87-unlock-idx-ambiguous.c new file mode 100644 index 0000000000..ff6461217e --- /dev/null +++ b/tests/regression/46-apron2/87-unlock-idx-ambiguous.c @@ -0,0 +1,28 @@ +// SKIP PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --enable ana.sv-comp.functions --set ana.path_sens[+] threadflag +// TODO: why nonterm without threadflag path-sens? +#include +#include +extern _Bool __VERIFIER_nondet_bool(); + +int g; +pthread_mutex_t m[2] = {PTHREAD_MUTEX_INITIALIZER, PTHREAD_MUTEX_INITIALIZER}; + +void *t_fun(void *arg) { + pthread_mutex_lock(&m[0]); + pthread_mutex_lock(&m[1]); // so we're unlocking a mutex we definitely hold + g++; + int r = __VERIFIER_nondet_bool(); + pthread_mutex_unlock(&m[r]); // TODO NOWARN (definitely held either way) + // could have unlocked m[0], so should have published g there + return NULL; +} + +int main() { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + + pthread_mutex_lock(&m[0]); + __goblint_check(g == 0); // UNKNOWN! + pthread_mutex_unlock(&m[0]); + return 0; +} diff --git a/tests/regression/46-apron2/87-unlock-idx-ambiguous.t b/tests/regression/46-apron2/87-unlock-idx-ambiguous.t new file mode 100644 index 0000000000..abbdd74f00 --- /dev/null +++ b/tests/regression/46-apron2/87-unlock-idx-ambiguous.t @@ -0,0 +1,39 @@ + $ goblint --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --enable ana.sv-comp.functions --set ana.path_sens[+] threadflag 87-unlock-idx-ambiguous.c + [Warning][Unknown] unlocking mutex (m[def_exc:Unknown int([0,1])]) which may not be held (87-unlock-idx-ambiguous.c:15:3-15:30) + [Warning][Assert] Assertion "g == 0" is unknown. (87-unlock-idx-ambiguous.c:25:3-25:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 14 + dead: 0 + total lines: 14 + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 0 + total memory locations: 1 + + $ goblint --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid --enable ana.sv-comp.functions --set ana.path_sens[+] threadflag 87-unlock-idx-ambiguous.c + [Warning][Unknown] unlocking mutex (m[def_exc:Unknown int([0,1])]) which may not be held (87-unlock-idx-ambiguous.c:15:3-15:30) + [Warning][Assert] Assertion "g == 0" is unknown. (87-unlock-idx-ambiguous.c:25:3-25:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 14 + dead: 0 + total lines: 14 + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 0 + total memory locations: 1 + + $ goblint --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid-cluster12 --enable ana.sv-comp.functions --set ana.path_sens[+] threadflag 87-unlock-idx-ambiguous.c + [Warning][Unknown] unlocking mutex (m[def_exc:Unknown int([0,1])]) which may not be held (87-unlock-idx-ambiguous.c:15:3-15:30) + [Warning][Assert] Assertion "g == 0" is unknown. (87-unlock-idx-ambiguous.c:25:3-25:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 14 + dead: 0 + total lines: 14 + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 0 + total memory locations: 1 + diff --git a/tests/regression/46-apron2/88-unlock-unknown.c b/tests/regression/46-apron2/88-unlock-unknown.c new file mode 100644 index 0000000000..dbdc4b9f77 --- /dev/null +++ b/tests/regression/46-apron2/88-unlock-unknown.c @@ -0,0 +1,25 @@ +// SKIP PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --enable ana.sv-comp.functions +#include +#include + +int g; +pthread_mutex_t m[2] = {PTHREAD_MUTEX_INITIALIZER, PTHREAD_MUTEX_INITIALIZER}; + +void *t_fun(void *arg) { + pthread_mutex_lock(&m[0]); + g++; + pthread_mutex_t *r; // rand + pthread_mutex_unlock(r); + // could have unlocked m[0], so should have published g there + return NULL; +} + +int main() { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + + pthread_mutex_lock(&m[0]); + __goblint_check(g == 0); // UNKNOWN! + pthread_mutex_unlock(&m[0]); + return 0; +} diff --git a/tests/regression/46-apron2/88-unlock-unknown.t b/tests/regression/46-apron2/88-unlock-unknown.t new file mode 100644 index 0000000000..35e4ec4503 --- /dev/null +++ b/tests/regression/46-apron2/88-unlock-unknown.t @@ -0,0 +1,42 @@ + $ goblint --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --enable ana.sv-comp.functions 88-unlock-unknown.c + [Warning][Unknown] unlocking unknown mutex which may not be held (88-unlock-unknown.c:12:3-12:26) + [Warning][Unknown] unlocking NULL mutex (88-unlock-unknown.c:12:3-12:26) + [Warning][Assert] Assertion "g == 0" is unknown. (88-unlock-unknown.c:22:3-22:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 11 + dead: 0 + total lines: 11 + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 0 + total memory locations: 1 + + $ goblint --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid --enable ana.sv-comp.functions --set ana.path_sens[+] threadflag 88-unlock-unknown.c + [Warning][Unknown] unlocking unknown mutex which may not be held (88-unlock-unknown.c:12:3-12:26) + [Warning][Unknown] unlocking NULL mutex (88-unlock-unknown.c:12:3-12:26) + [Warning][Assert] Assertion "g == 0" is unknown. (88-unlock-unknown.c:22:3-22:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 11 + dead: 0 + total lines: 11 + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 0 + total memory locations: 1 + + $ goblint --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid-cluster12 --enable ana.sv-comp.functions --set ana.path_sens[+] threadflag 88-unlock-unknown.c + [Warning][Unknown] unlocking unknown mutex which may not be held (88-unlock-unknown.c:12:3-12:26) + [Warning][Unknown] unlocking NULL mutex (88-unlock-unknown.c:12:3-12:26) + [Warning][Assert] Assertion "g == 0" is unknown. (88-unlock-unknown.c:22:3-22:26) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 11 + dead: 0 + total lines: 11 + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 0 + total memory locations: 1 + diff --git a/tests/regression/46-apron2/89-flag-ctx-sens.c b/tests/regression/46-apron2/89-flag-ctx-sens.c new file mode 100644 index 0000000000..41e4f02520 --- /dev/null +++ b/tests/regression/46-apron2/89-flag-ctx-sens.c @@ -0,0 +1,28 @@ +// SKIP PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet +// NOTIMEOUT +// See https://github.com/goblint/analyzer/pull/1508 +#include +#include + +int g; +pthread_mutex_t m = PTHREAD_MUTEX_INITIALIZER; + +void fn() { + // Just do nothing + return; +} + +void *t_fun(void *arg) { + pthread_mutex_lock(&m); + g = g+1; + fn(); + pthread_mutex_unlock(&m); + return NULL; +} + +int main() { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + + return 0; +} diff --git a/tests/regression/46-apron2/90-malloc.c b/tests/regression/46-apron2/90-malloc.c new file mode 100644 index 0000000000..8780568748 --- /dev/null +++ b/tests/regression/46-apron2/90-malloc.c @@ -0,0 +1,21 @@ +// SKIP PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set ana.apron.domain interval --set sem.int.signed_overflow assume_none +// Checks that assinging to malloc'ed memory does not cause both branches to be dead +#include +#include +void nop(void* arg) { +} + +void main() { + pthread_t thread; + pthread_create(&thread, 0, &nop, 0); + + long *k = malloc(sizeof(long)); + *k = 5; + if (1) + ; + + __goblint_check(*k >= 5); // Reachable and true + + *k = *k+1; + __goblint_check(*k >= 5); // Reachable and true +} diff --git a/tests/regression/46-apron2/91-malloc-tid.c b/tests/regression/46-apron2/91-malloc-tid.c new file mode 100644 index 0000000000..36696956e7 --- /dev/null +++ b/tests/regression/46-apron2/91-malloc-tid.c @@ -0,0 +1,21 @@ +// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid --set ana.apron.domain interval --set sem.int.signed_overflow assume_none +// Checks that assinging to malloc'ed memory does not cause both branches to be dead +#include +#include +void nop(void* arg) { +} + +void main() { + pthread_t thread; + pthread_create(&thread, 0, &nop, 0); + + long *k = malloc(sizeof(long)); + *k = 5; + if (1) + ; + + __goblint_check(*k >= 5); // Reachable and true + + *k = *k+1; + __goblint_check(*k >= 5); // Reachable and true +} diff --git a/tests/regression/46-apron2/92-malloc-atomic.c b/tests/regression/46-apron2/92-malloc-atomic.c new file mode 100644 index 0000000000..b2f057f6a4 --- /dev/null +++ b/tests/regression/46-apron2/92-malloc-atomic.c @@ -0,0 +1,21 @@ +// SKIP PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set ana.apron.domain interval --set sem.int.signed_overflow assume_none +// Checks that assinging to malloc'ed memory does not cause both branches to be dead +#include +#include +void nop(void* arg) { +} + +void main() { + pthread_t thread; + pthread_create(&thread, 0, &nop, 0); + + long *k = malloc(sizeof(long)); + *k = 5; + if (1) + ; + + __goblint_check(*k >= 5); // Reachable and true + + *k = *k+1; + __goblint_check(*k >= 5); // Reachable and true +} diff --git a/tests/regression/46-apron2/dune b/tests/regression/46-apron2/dune index cc0c04185c..89efde3083 100644 --- a/tests/regression/46-apron2/dune +++ b/tests/regression/46-apron2/dune @@ -8,3 +8,8 @@ (glob_files ??-*.c)) (locks /update_suite) (action (chdir ../../.. (run %{update_suite} group apron2 -q)))) + +(cram + (alias runaprontest) + (enabled_if %{lib-available:apron}) + (deps (glob_files *.c))) diff --git a/tests/regression/55-loop-unrolling/12-loop-no-overflows.c b/tests/regression/55-loop-unrolling/12-loop-no-overflows.c new file mode 100644 index 0000000000..03554e06c5 --- /dev/null +++ b/tests/regression/55-loop-unrolling/12-loop-no-overflows.c @@ -0,0 +1,37 @@ +// PARAM: --enable ana.int.interval_set +// extracted from SV-COMP task ldv-memsafety/memleaks_test12-2.i + +typedef unsigned int size_t; +struct ldv_list_head { + struct ldv_list_head *next, *prev; +}; +struct ldv_list_head ldv_global_msg_list = {&(ldv_global_msg_list), &(ldv_global_msg_list)}; +struct ldv_msg { + void *data; + struct ldv_list_head list; +}; + +static inline void __ldv_list_del(struct ldv_list_head *prev, struct ldv_list_head *next) { + next->prev = prev; + prev->next = next; +} + +static inline void ldv_list_del(struct ldv_list_head *entry) { + __ldv_list_del(entry->prev, entry->next); +} + +void ldv_msg_free(struct ldv_msg *msg) { + free(msg->data); + free(msg); +} + +// ldv_destroy_msgs +void main(void) { + struct ldv_msg *msg; + struct ldv_msg *n; + for (msg = ({ const typeof( ((typeof(*msg) *)0)->list ) *__mptr = ((&ldv_global_msg_list)->next); (typeof(*msg) *)( (char *)__mptr - ((size_t) &((typeof(*msg) *)0)->list) ); }), n = ({ const typeof( ((typeof(*(msg)) *)0)->list ) *__mptr = ((msg)->list.next); (typeof(*(msg)) *)( (char *)__mptr - ((size_t) &((typeof(*(msg)) *)0)->list) ); }); &msg->list != (&ldv_global_msg_list); msg = n, n = ({ const typeof( ((typeof(*(n)) *)0)->list ) *__mptr = ((n)->list.next); (typeof(*(n)) *)( (char *)__mptr - ((size_t) &((typeof(*(n)) *)0)->list) ); })) // NOWARN + { + ldv_list_del(&msg->list); + ldv_msg_free(msg); + } +} \ No newline at end of file diff --git a/tests/regression/55-loop-unrolling/13-unrolled-loop-no-overflows.c b/tests/regression/55-loop-unrolling/13-unrolled-loop-no-overflows.c new file mode 100644 index 0000000000..84700ac9da --- /dev/null +++ b/tests/regression/55-loop-unrolling/13-unrolled-loop-no-overflows.c @@ -0,0 +1,72 @@ +// PARAM: --enable ana.int.interval_set +// extracted from SV-COMP task ldv-memsafety/memleaks_test12-2.i with --set exp.unrolling-factor 1 + +typedef unsigned int size_t; +struct ldv_list_head { + struct ldv_list_head *next, *prev; +}; +struct ldv_list_head ldv_global_msg_list = {&(ldv_global_msg_list), &(ldv_global_msg_list)}; +struct ldv_msg { + void *data; + struct ldv_list_head list; +}; + +__inline static void __ldv_list_del(struct ldv_list_head *prev, struct ldv_list_head *next) { + next->prev = prev; + prev->next = next; + return; +} + +__inline static void ldv_list_del(struct ldv_list_head *entry) { + __ldv_list_del(entry->prev, entry->next); + return; +} + +void ldv_msg_free(struct ldv_msg *msg) { + free(msg->data); + free((void *)msg); + return; +} + +// ldv_destroy_msgs +void main(void) { + struct ldv_msg *msg; + struct ldv_msg *n; + struct ldv_list_head const *__mptr; + struct ldv_list_head const *__mptr___0; + struct ldv_list_head const *__mptr___1; + + __mptr = (struct ldv_list_head const *)ldv_global_msg_list.next; + msg = (struct ldv_msg *)((char *)__mptr - (size_t)(&((struct ldv_msg *)0)->list)); + __mptr___0 = (struct ldv_list_head const *)msg->list.next; + n = (struct ldv_msg *)((char *)__mptr___0 - (size_t)(&((struct ldv_msg *)0)->list)); + + if (!((unsigned long)(&msg->list) != (unsigned long)(&ldv_global_msg_list))) { // NOWARN + goto loop_end; + } + + ldv_list_del(&msg->list); + ldv_msg_free(msg); + msg = n; + __mptr___1 = (struct ldv_list_head const *)n->list.next; + n = (struct ldv_msg *)((char *)__mptr___1 - (size_t)(&((struct ldv_msg *)0)->list)); + + loop_continue_0: /* CIL Label */; + { + while (1) { + while_continue: /* CIL Label */; + if (!((unsigned long)(&msg->list) != (unsigned long)(&ldv_global_msg_list))) { + goto while_break; + } + + ldv_list_del(&msg->list); + ldv_msg_free(msg); + msg = n; + __mptr___1 = (struct ldv_list_head const *)n->list.next; + n = (struct ldv_msg *)((char *)__mptr___1 - (size_t)(&((struct ldv_msg *)0)->list)); + } + while_break: /* CIL Label */; + } + loop_end: /* CIL Label */; + return; +} \ No newline at end of file diff --git a/tests/regression/58-base-mm-tid/01-tid-toy1.c b/tests/regression/58-base-mm-tid/01-tid-toy1.c index bc3cd18efa..49e96881d1 100644 --- a/tests/regression/58-base-mm-tid/01-tid-toy1.c +++ b/tests/regression/58-base-mm-tid/01-tid-toy1.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.path_sens[+] threadflag --sets ana.base.privatization mutex-meet-tid +// PARAM: --set ana.path_sens[+] threadflag --set ana.base.privatization mutex-meet-tid // Inspired by 36/71 #include #include diff --git a/tests/regression/58-base-mm-tid/15-branched-thread-creation.c b/tests/regression/58-base-mm-tid/15-branched-thread-creation.c index 3292182adc..c7bb43519f 100644 --- a/tests/regression/58-base-mm-tid/15-branched-thread-creation.c +++ b/tests/regression/58-base-mm-tid/15-branched-thread-creation.c @@ -41,7 +41,7 @@ int main(void) { if(!mt) { pthread_mutex_lock(&mutex); - __goblint_check(g==h); //MAYFAIL + __goblint_check(g==h); //FAIL pthread_mutex_unlock(&mutex); } diff --git a/tests/regression/58-base-mm-tid/22-other-assume.c b/tests/regression/58-base-mm-tid/22-other-assume.c index 4f5c73b038..301195ac1f 100644 --- a/tests/regression/58-base-mm-tid/22-other-assume.c +++ b/tests/regression/58-base-mm-tid/22-other-assume.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.path_sens[+] threadflag --sets ana.base.privatization mutex-meet-tid +// PARAM: --set ana.path_sens[+] threadflag --set ana.base.privatization mutex-meet-tid // Copy of 46/03 for base #include #include diff --git a/tests/regression/58-base-mm-tid/23-other-assume-inprec.c b/tests/regression/58-base-mm-tid/23-other-assume-inprec.c index 37e59d3edf..a4bac04c59 100644 --- a/tests/regression/58-base-mm-tid/23-other-assume-inprec.c +++ b/tests/regression/58-base-mm-tid/23-other-assume-inprec.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.path_sens[+] threadflag --sets ana.base.privatization mutex-meet-tid --set ana.activated[+] threadJoins +// PARAM: --set ana.path_sens[+] threadflag --set ana.base.privatization mutex-meet-tid --set ana.activated[+] threadJoins // Copy of 46/04 for base #include #include diff --git a/tests/regression/66-interval-set-one/51-widen-sides.c b/tests/regression/66-interval-set-one/51-widen-sides.c index b086baf026..53fe749704 100644 --- a/tests/regression/66-interval-set-one/51-widen-sides.c +++ b/tests/regression/66-interval-set-one/51-widen-sides.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.ctx_insens "['base', 'mallocWrapper']" --enable ana.int.interval_set --sets solvers.td3.side_widen sides-local +// PARAM: --set ana.ctx_insens "['base', 'mallocWrapper']" --enable ana.int.interval_set --set solvers.td3.side_widen sides-local #include int further(int n) { diff --git a/tests/regression/67-interval-sets-two/16-branched-thread-creation.c b/tests/regression/67-interval-sets-two/16-branched-thread-creation.c index c309ec8ffd..d97f800621 100644 --- a/tests/regression/67-interval-sets-two/16-branched-thread-creation.c +++ b/tests/regression/67-interval-sets-two/16-branched-thread-creation.c @@ -41,7 +41,7 @@ int main(void) { if(!mt) { pthread_mutex_lock(&mutex); - __goblint_check(g==h); //MAYFAIL + __goblint_check(g==h); //FAIL pthread_mutex_unlock(&mutex); } diff --git a/tests/regression/77-lin2vareq/34-coefficient-features.c b/tests/regression/77-lin2vareq/34-coefficient-features.c new file mode 100644 index 0000000000..561eccf0af --- /dev/null +++ b/tests/regression/77-lin2vareq/34-coefficient-features.c @@ -0,0 +1,62 @@ +//SKIP PARAM: --set ana.activated[+] lin2vareq --set sem.int.signed_overflow assume_none +// this test checks basic coefficient handing in main and join capabilities in loop + +#include + +void loop() { + int random; + int i = 0; + int x = 0; + int y = 0; + + x=x+4; + y=y+8; + i=i+1; + + if (random) { + x=x+4; + y=y+8; + i=i+1; + } + + __goblint_check(x == 4*i); //SUCCESS + + x=0; + y=0; + + for(i = 1; i < 100; i++) { + x=x+4; + y=y+8; + + __goblint_check(y == 2*x); //SUCCESS + __goblint_check(x == 4*i); //SUCCESS + } +} + +void main() { + int a; + int b; + int c; + int unknown; + a = 4; + + b = 4*c; + + __goblint_check(b == 4*c); //SUCCESS + + b = a*c; + + __goblint_check(b == 4*c); //SUCCESS + + if (7*b == 20*unknown + a){ + + __goblint_check(7*b == 20*unknown + a); //SUCCESS + } + + b = unknown ? a*c : 4*c; + + __goblint_check(b == 4*c); //SUCCESS + + loop(); + +} \ No newline at end of file diff --git a/tests/regression/80-context_gas/21-sync.c b/tests/regression/80-context_gas/21-sync.c new file mode 100644 index 0000000000..33edf254e5 --- /dev/null +++ b/tests/regression/80-context_gas/21-sync.c @@ -0,0 +1,35 @@ +// PARAM: --set ana.context.gas_value 1 +// Like 00/35 but with gas this time! +// Misbehaves for gas <= 3 +#include +#include + +int g = 1; + +void foo() { + // Single-threaded: g = 1 in local state + // Multi-threaded: g = 2 in global unprotected invariant + // Joined contexts: g is unprotected, so read g = 2 from global unprotected invariant (only) + // Was soundly claiming that check will succeed! + int x = g; + __goblint_check(x == 2); // UNKNOWN! +} + +void *t_fun(void *arg) { + foo(); +} + +int do_stuff() { + foo(); + g = 2; + + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + + return 0; +} + +int main() { + do_stuff(); + return 0; +} diff --git a/tests/regression/80-context_gas/22-sync-precision.c b/tests/regression/80-context_gas/22-sync-precision.c new file mode 100644 index 0000000000..8fc1dd7779 --- /dev/null +++ b/tests/regression/80-context_gas/22-sync-precision.c @@ -0,0 +1,36 @@ +// PARAM: --set ana.context.gas_value 4 +// Like 00/35 but with gas this time! +// Misbehaves for gas <= 3 +#include +#include + +int g = 1; + +void foo() { + // Check that we don't lose precision due to JoinCall + int x = g; + int x2 = g; + // A hack: In both contexts g has a single possible value, so we check that x = x2 + // to verify there is no precision loss + + __goblint_check(x == x2); +} + +void *t_fun(void *arg) { + foo(); +} + +int do_stuff() { + foo(); + g = 2; + + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + + return 0; +} + +int main() { + do_stuff(); + return 0; +} diff --git a/tests/unit/cdomains/floatDomainTest.ml b/tests/unit/cdomains/floatDomainTest.ml index 5f3cd4db47..c6cb18500a 100644 --- a/tests/unit/cdomains/floatDomainTest.ml +++ b/tests/unit/cdomains/floatDomainTest.ml @@ -14,12 +14,12 @@ struct let mul = Float_t.mul let div = Float_t.div - let pred x = Option.get (to_float (Float_t.pred (of_float Nearest x))) - let succ x = Option.get (to_float (Float_t.succ (of_float Nearest x))) + let pred x = to_float (Float_t.pred (of_float Nearest x)) + let succ x = to_float (Float_t.succ (of_float Nearest x)) - let fmax = Option.get (to_float Float_t.upper_bound) - let fmin = Option.get (to_float Float_t.lower_bound) - let fsmall = Option.get (to_float Float_t.smallest) + let fmax = to_float Float_t.upper_bound + let fmin = to_float Float_t.lower_bound + let fsmall = to_float Float_t.smallest let fi_zero = FI.of_const 0. let fi_one = FI.of_const 1. @@ -53,7 +53,7 @@ struct FI.top () + FI.top () = FI.top (); (FI.of_const fmin) + (FI.of_const fmax) = fi_zero; (FI.of_const fsmall) + (FI.of_const fsmall) = FI.of_const (fsmall +. fsmall); - let one_plus_fsmall = Option.get (to_float (Float_t.add Up (Float_t.of_float Up 1.) Float_t.smallest)) in + let one_plus_fsmall = to_float (Float_t.add Up (Float_t.of_float Up 1.) Float_t.smallest) in (FI.of_const fsmall) + (FI.of_const 1.) = FI.of_interval (1., one_plus_fsmall); (FI.of_interval (1., 2.)) + (FI.of_interval (2., 3.)) = FI.of_interval (3., 5.); (FI.of_interval (-. 2., 3.)) + (FI.of_interval (-. 100., 20.)) = FI.of_interval (-. 102., 23.); @@ -286,27 +286,27 @@ struct let test_FI_add = QCheck.Test.make ~name:"test_FI_add" (QCheck.pair QCheck.float QCheck.float) (fun (arg1, arg2) -> let result = FI.add (FI.of_const arg1) (FI.of_const arg2) in - (FI.leq (FI.of_const (Option.get (to_float (add Up (of_float Nearest arg1) (of_float Nearest arg2))))) result) && - (FI.leq (FI.of_const (Option.get (to_float (add Down (of_float Nearest arg1) (of_float Nearest arg2))))) result)) + (FI.leq (FI.of_const (to_float (add Up (of_float Nearest arg1) (of_float Nearest arg2)))) result) && + (FI.leq (FI.of_const (to_float (add Down (of_float Nearest arg1) (of_float Nearest arg2)))) result)) let test_FI_sub = QCheck.Test.make ~name:"test_FI_sub" (QCheck.pair QCheck.float QCheck.float) (fun (arg1, arg2) -> let result = FI.sub (FI.of_const arg1) (FI.of_const arg2) in - (FI.leq (FI.of_const (Option.get (to_float (sub Up (of_float Nearest arg1) (of_float Nearest arg2))))) result) && - (FI.leq (FI.of_const (Option.get (to_float (sub Down (of_float Nearest arg1) (of_float Nearest arg2))))) result)) + (FI.leq (FI.of_const (to_float (sub Up (of_float Nearest arg1) (of_float Nearest arg2)))) result) && + (FI.leq (FI.of_const (to_float (sub Down (of_float Nearest arg1) (of_float Nearest arg2))))) result) let test_FI_mul = QCheck.Test.make ~name:"test_FI_mul" (QCheck.pair QCheck.float QCheck.float) (fun (arg1, arg2) -> let result = FI.mul (FI.of_const arg1) (FI.of_const arg2) in - (FI.leq (FI.of_const (Option.get (to_float (mul Up (of_float Nearest arg1) (of_float Nearest arg2))))) result) && - (FI.leq (FI.of_const (Option.get (to_float (mul Down (of_float Nearest arg1) (of_float Nearest arg2))))) result)) + (FI.leq (FI.of_const (to_float (mul Up (of_float Nearest arg1) (of_float Nearest arg2)))) result) && + (FI.leq (FI.of_const (to_float (mul Down (of_float Nearest arg1) (of_float Nearest arg2)))) result)) let test_FI_div = QCheck.Test.make ~name:"test_FI_div" (QCheck.pair QCheck.float QCheck.float) (fun (arg1, arg2) -> let result = FI.div (FI.of_const arg1) (FI.of_const arg2) in - (FI.leq (FI.of_const (Option.get (to_float (div Up (of_float Nearest arg1) (of_float Nearest arg2))))) result) && - (FI.leq (FI.of_const (Option.get (to_float (div Down (of_float Nearest arg1) (of_float Nearest arg2))))) result)) + (FI.leq (FI.of_const (to_float (div Up (of_float Nearest arg1) (of_float Nearest arg2)))) result) && + (FI.leq (FI.of_const (to_float (div Down (of_float Nearest arg1) (of_float Nearest arg2)))) result)) let test () = [ diff --git a/tests/unit/cdomains/intDomainTest.ml b/tests/unit/cdomains/intDomainTest.ml index e697b022eb..a60b7a6cb1 100644 --- a/tests/unit/cdomains/intDomainTest.ml +++ b/tests/unit/cdomains/intDomainTest.ml @@ -205,6 +205,7 @@ struct let i65536 = I.of_interval ik (Z.zero, of_int 65536) let i65537 = I.of_interval ik (Z.zero, of_int 65537) let imax = I.of_interval ik (Z.zero, of_int 2147483647) + let imin = I.of_interval ik (of_int (-2147483648), Z.zero) let assert_equal x y = assert_equal ~cmp:I.equal ~printer:I.show x y @@ -218,9 +219,34 @@ struct assert_equal imax (I.widen ik i65536 i65537); assert_equal imax (I.widen ik i65536 imax) + let test_interval_narrow _ = + GobConfig.set_bool "ana.int.interval_threshold_widening" true; + GobConfig.set_string "ana.int.interval_threshold_widening_constants" "comparisons"; + let i_zero_one = I.of_interval ik (Z.zero, Z.one) in + let i_zero_five = I.of_interval ik (Z.zero, of_int 5) in + let to_widen = I.of_interval ik (Z.zero, Z.zero) in + (* this should widen to [0, x], where x is the next largest threshold above 5 or the maximal int*) + let widened = I.widen ik to_widen i_zero_five in + (* either way, narrowing from [0, x] to [0, 1] should be possible *) + let narrowed = I.narrow ik widened i_zero_one in + (* however, narrowing should not allow [0, x] to grow *) + let narrowed2 = I.narrow ik widened imax in + assert_equal i_zero_one narrowed; + assert_equal widened narrowed2; + + (* the same tests, but for lower bounds *) + let i_minus_one_zero = I.of_interval ik (Z.minus_one, Z.zero) in + let i_minus_five_zero = I.of_interval ik (of_int (-5), Z.zero) in + let widened = I.widen ik to_widen i_minus_five_zero in + let narrowed = I.narrow ik widened i_minus_one_zero in + let narrowed2 = I.narrow ik widened imin in + assert_equal i_minus_one_zero narrowed; + assert_equal widened narrowed2 + let test () = [ "test_interval_rem" >:: test_interval_rem; "test_interval_widen" >:: test_interval_widen; + "test_interval_narrow" >:: test_interval_narrow; ] end diff --git a/tests/unit/maindomaintest.ml b/tests/unit/maindomaintest.ml index 8e6a7f5a3a..8e1db76b83 100644 --- a/tests/unit/maindomaintest.ml +++ b/tests/unit/maindomaintest.ml @@ -15,14 +15,11 @@ struct let show = show end include Printable.SimpleShow (P) + + let elems = ['a'; 'b'; 'c'; 'd'] end -module ArbitraryLattice = SetDomain.FiniteSet (PrintableChar) ( - struct - type t = char - let elems = ['a'; 'b'; 'c'; 'd'] - end - ) +module ArbitraryLattice = SetDomain.FiniteSet (PrintableChar) module HoareArbitrary = HoareDomain.Set_LiftTop (ArbitraryLattice) (struct let topname = "Top" end) module HoareArbitrary_NoTop = HoareDomain.Set (ArbitraryLattice)