diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml index fd2c55b84e..3f924869fc 100644 --- a/.github/workflows/coverage.yml +++ b/.github/workflows/coverage.yml @@ -46,6 +46,9 @@ jobs: - name: Install dependencies run: opam install . --deps-only --locked --with-test + - name: Install os gem for operating system detection + run: sudo gem install os + - name: Install coverage dependencies run: opam install bisect_ppx diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 0ada04e369..1a6d17fab4 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -46,6 +46,9 @@ jobs: - name: Install dependencies run: opam install . --deps-only --locked --with-doc + - name: Install os gem for operating system detection + run: sudo gem install os + - name: Build API docs run: opam exec -- dune build @doc diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml index 16655bfdc7..8205d4ef34 100644 --- a/.github/workflows/locked.yml +++ b/.github/workflows/locked.yml @@ -48,6 +48,9 @@ jobs: - name: Install dependencies run: opam install . --deps-only --locked --with-test + - name: Install os gem for operating system detection + run: sudo gem install os + - name: Build run: ./make.sh nat @@ -100,6 +103,9 @@ jobs: - name: Install dependencies run: opam install . --deps-only --locked --with-test + - name: Install os gem for operating system detection + run: sudo gem install os + - name: Build run: ./make.sh nat @@ -142,6 +148,9 @@ jobs: - name: Install dependencies run: opam install . --deps-only --locked + - name: Install os gem for operating system detection + run: sudo gem install os + - name: Setup Gobview run: ./make.sh setup_gobview diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml index f3fe6cc558..81d1d3dc1c 100644 --- a/.github/workflows/unlocked.yml +++ b/.github/workflows/unlocked.yml @@ -57,6 +57,9 @@ jobs: - name: Install dependencies run: opam install . --deps-only --with-test + + - name: Install os gem for operating system detection + run: sudo gem install os - name: Install Apron dependencies if: ${{ matrix.apron }} @@ -118,6 +121,9 @@ jobs: - name: Install dependencies run: opam install . --deps-only --with-test + - name: Install os gem for operating system detection + run: sudo gem install os + - name: Install Apron dependencies run: | opam depext apron diff --git a/.gitignore b/.gitignore index 7038e51f8f..d13f6fbc01 100644 --- a/.gitignore +++ b/.gitignore @@ -23,6 +23,7 @@ doclist.odocl autom4te.cache mytests result/* +results/* pml-result/* tests/regression/*/goblint_temp linux-headers diff --git a/GOBLINT_README.md b/GOBLINT_README.md new file mode 100644 index 0000000000..45ae104f7f --- /dev/null +++ b/GOBLINT_README.md @@ -0,0 +1,67 @@ +**This is the README for the entire Goblint system, when getting started with the artifact, it is best to look at README.md** + +# Goblint +[![GitHub release status](https://img.shields.io/github/v/release/goblint/analyzer)](https://github.com/goblint/analyzer/releases) +[![opam package status](https://badgen.net/opam/v/goblint)](https://opam.ocaml.org/packages/goblint) +[![Zenodo DOI](https://zenodo.org/badge/2066905.svg)](https://zenodo.org/badge/latestdoi/2066905) + +[![locked workflow status](https://github.com/goblint/analyzer/actions/workflows/locked.yml/badge.svg)](https://github.com/goblint/analyzer/actions/workflows/locked.yml) +[![unlocked workflow status](https://github.com/goblint/analyzer/actions/workflows/unlocked.yml/badge.svg)](https://github.com/goblint/analyzer/actions/workflows/unlocked.yml) +[![Coverage Status](https://coveralls.io/repos/github/goblint/analyzer/badge.svg?branch=master)](https://coveralls.io/github/goblint/analyzer?branch=master) +[![docker workflow status](https://github.com/goblint/analyzer/actions/workflows/docker.yml/badge.svg)](https://github.com/goblint/analyzer/actions/workflows/docker.yml) +[![Documentation Status](https://readthedocs.org/projects/goblint/badge/?version=latest)](https://goblint.readthedocs.io/en/latest/?badge=latest) +[![project chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://goblint.zulipchat.com) + +Documentation can be browsed on [Read the Docs](https://goblint.readthedocs.io/en/latest/) or [GitHub](./docs/). + +## Installing +Both for using an up-to-date version of Goblint or developing it, the best way is to install from source by cloning this repository. +For benchmarking Goblint, please follow the [Benchmarking guide on Read the Docs](https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/). + +### Linux +1. Install [opam](https://opam.ocaml.org/doc/Install.html). +2. Make sure the following are installed: `git`, `patch`, `m4`, `autoconf`, `libgmp-dev`, `libmpfr-dev` and `pkg-config`. +3. Run `make setup` to install OCaml and dependencies via opam. +4. Run `make` to build Goblint itself. +5. Run `make install` to install Goblint into the opam switch for usage via switch's `PATH`. +6. _Optional:_ See [`scripts/bash-completion.sh`](./scripts/bash-completion.sh) for setting up bash completion for Goblint arguments. + +### MacOS +1. Install GCC with `brew install gcc grep` (first run `xcode-select --install` if you don't want to build it from source). Goblint requires GCC while macOS's default `cpp` is Clang, which will not work. +2. ONLY for M1 (ARM64) processor: homebrew changed its install location from `/usr/local/` to `/opt/homebrew/`. For packages to find their dependecies execute `sudo ln -s /opt/homebrew/{include,lib} /usr/local/`. +3. Continue using Linux instructions (the formulae in brew for `patch`, `libgmp-dev`, `libmpfr-dev` are `gpatch`, `gmp`, `mpfr`, respectively). + +### Windows +1. Install [WSL2](https://docs.microsoft.com/en-us/windows/wsl/install-win10). Goblint is not compatible with WSL1. +2. Continue using Linux instructions in WSL. + +### Other +* **[opam](https://opam.ocaml.org/packages/goblint/)**. Install [opam](https://opam.ocaml.org/doc/Install.html) and run `opam install goblint`. +* **[devcontainer](./.devcontainer/).** Select "Reopen in Container" in VS Code and continue with `make` using Linux instructions in devcontainer. +* **[Docker (GitHub Container Registry)](https://github.com/goblint/analyzer/pkgs/container/analyzer)**. Run `docker pull ghcr.io/goblint/analyzer:latest` (or `:nightly`). +* **Docker (repository).** Clone and run `docker build -t goblint .`. +* **Vagrant.** Clone and run `vagrant up && vagrant ssh`. + + +## Running +To confirm that building worked, you can try running Goblint as follows: +``` +./goblint tests/regression/04-mutex/01-simple_rc.c +``` +To confirm that installation into the opam switch worked, you can try running Goblint as follows: +``` +goblint tests/regression/04-mutex/01-simple_rc.c +``` +To confirm that the Docker container worked, you can try running Goblint as follows: +``` +docker run -it --rm -v $(pwd):/data goblint /data/tests/regression/04-mutex/01-simple_rc.c +``` +If pulled from GitHub Container Registry, use the container name `ghcr.io/goblint/analyzer:latest` (or `:nightly`) instead. + +For further information, see [documentation](https://goblint.readthedocs.io/en/latest/user-guide/running/). + +## Acknowledgements + +Work on Goblint was supported in part by Deutsche Forschungsgemeinschaft (DFG) (47140942/1480 [PUMA](https://gepris.dfg.de/gepris/projekt/4714094), 378803395/2428 [ConVeY](http://convey.in.tum.de)), ARTEMIS Joint Undertaking (269335 [MBAT](http://www.mbat-artemis.eu/home/)), ITEA3 project 14014 [ASSUME](http://assume-project.eu/), the Shota Rustaveli National Science Foundation of Georgia [FR-21-7973](https://viam.science.tsu.ge/new/index.php?lang=eng&page=projects&subpage=111), the Estonian Research Council ([IUT2-1](https://www.etis.ee/Portal/Projects/Display/561b7b1d-d1dd-43a2-90e5-0661de823823?lang=ENG), [PSG61](https://www.etis.ee/Portal/Projects/Display/743243bb-15c2-47b3-9c10-e7d86a9a276d?lang=ENG)), and the Estonian Centre of Excellence in IT (EXCITE), funded by the European Regional Development Fund. + +We also thank [Zulip](https://zulip.com) for providing free Zulip Cloud Standard hosting for the Goblint project. Zulip is an open-source modern team chat app designed to keep both live and asynchronous conversations organized. \ No newline at end of file diff --git a/README.md b/README.md index 6aee964826..a730fb07e3 100644 --- a/README.md +++ b/README.md @@ -1,65 +1,211 @@ -# Goblint -[![GitHub release status](https://img.shields.io/github/v/release/goblint/analyzer)](https://github.com/goblint/analyzer/releases) -[![opam package status](https://badgen.net/opam/v/goblint)](https://opam.ocaml.org/packages/goblint) -[![Zenodo DOI](https://zenodo.org/badge/2066905.svg)](https://zenodo.org/badge/latestdoi/2066905) - -[![locked workflow status](https://github.com/goblint/analyzer/actions/workflows/locked.yml/badge.svg)](https://github.com/goblint/analyzer/actions/workflows/locked.yml) -[![unlocked workflow status](https://github.com/goblint/analyzer/actions/workflows/unlocked.yml/badge.svg)](https://github.com/goblint/analyzer/actions/workflows/unlocked.yml) -[![Coverage Status](https://coveralls.io/repos/github/goblint/analyzer/badge.svg?branch=master)](https://coveralls.io/github/goblint/analyzer?branch=master) -[![docker workflow status](https://github.com/goblint/analyzer/actions/workflows/docker.yml/badge.svg)](https://github.com/goblint/analyzer/actions/workflows/docker.yml) -[![Documentation Status](https://readthedocs.org/projects/goblint/badge/?version=latest)](https://goblint.readthedocs.io/en/latest/?badge=latest) -[![project chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://goblint.zulipchat.com) - -Documentation can be browsed on [Read the Docs](https://goblint.readthedocs.io/en/latest/) or [GitHub](./docs/). - -## Installing -Both for using an up-to-date version of Goblint or developing it, the best way is to install from source by cloning this repository. -For benchmarking Goblint, please follow the [Benchmarking guide on Read the Docs](https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/). - -### Linux -1. Install [opam](https://opam.ocaml.org/doc/Install.html). -2. Make sure the following are installed: `git`, `patch`, `m4`, `autoconf`, `libgmp-dev`, `libmpfr-dev` and `pkg-config`. -3. Run `make setup` to install OCaml and dependencies via opam. -4. Run `make` to build Goblint itself. -5. Run `make install` to install Goblint into the opam switch for usage via switch's `PATH`. -6. _Optional:_ See [`scripts/bash-completion.sh`](./scripts/bash-completion.sh) for setting up bash completion for Goblint arguments. - -### MacOS -1. Install GCC with `brew install gcc grep` (first run `xcode-select --install` if you don't want to build it from source). Goblint requires GCC while macOS's default `cpp` is Clang, which will not work. -2. ONLY for M1 (ARM64) processor: homebrew changed its install location from `/usr/local/` to `/opt/homebrew/`. For packages to find their dependecies execute `sudo ln -s /opt/homebrew/{include,lib} /usr/local/`. -3. Continue using Linux instructions (the formulae in brew for `patch`, `libgmp-dev`, `libmpfr-dev` are `gpatch`, `gmp`, `mpfr`, respectively). - -### Windows -1. Install [WSL2](https://docs.microsoft.com/en-us/windows/wsl/install-win10). Goblint is not compatible with WSL1. -2. Continue using Linux instructions in WSL. - -### Other -* **[opam](https://opam.ocaml.org/packages/goblint/)**. Install [opam](https://opam.ocaml.org/doc/Install.html) and run `opam install goblint`. -* **[devcontainer](./.devcontainer/).** Select "Reopen in Container" in VS Code and continue with `make` using Linux instructions in devcontainer. -* **[Docker (GitHub Container Registry)](https://github.com/goblint/analyzer/pkgs/container/analyzer)**. Run `docker pull ghcr.io/goblint/analyzer:latest` (or `:nightly`). -* **Docker (repository).** Clone and run `docker build -t goblint .`. -* **Vagrant.** Clone and run `vagrant up && vagrant ssh`. - - -## Running -To confirm that building worked, you can try running Goblint as follows: -``` -./goblint tests/regression/04-mutex/01-simple_rc.c -``` -To confirm that installation into the opam switch worked, you can try running Goblint as follows: -``` -goblint tests/regression/04-mutex/01-simple_rc.c -``` -To confirm that the Docker container worked, you can try running Goblint as follows: -``` -docker run -it --rm -v $(pwd):/data goblint /data/tests/regression/04-mutex/01-simple_rc.c -``` -If pulled from GitHub Container Registry, use the container name `ghcr.io/goblint/analyzer:latest` (or `:nightly`) instead. - -For further information, see [documentation](https://goblint.readthedocs.io/en/latest/user-guide/running/). - -## Acknowledgements - -Work on Goblint was supported in part by Deutsche Forschungsgemeinschaft (DFG) (47140942/1480 [PUMA](https://gepris.dfg.de/gepris/projekt/4714094), 378803395/2428 [ConVeY](http://convey.in.tum.de)), ARTEMIS Joint Undertaking (269335 [MBAT](http://www.mbat-artemis.eu/home/)), ITEA3 project 14014 [ASSUME](http://assume-project.eu/), the Shota Rustaveli National Science Foundation of Georgia [FR-21-7973](https://viam.science.tsu.ge/new/index.php?lang=eng&page=projects&subpage=111), the Estonian Research Council ([IUT2-1](https://www.etis.ee/Portal/Projects/Display/561b7b1d-d1dd-43a2-90e5-0661de823823?lang=ENG), [PSG61](https://www.etis.ee/Portal/Projects/Display/743243bb-15c2-47b3-9c10-e7d86a9a276d?lang=ENG)), and the Estonian Centre of Excellence in IT (EXCITE), funded by the European Regional Development Fund. - -We also thank [Zulip](https://zulip.com) for providing free Zulip Cloud Standard hosting for the Goblint project. Zulip is an open-source modern team chat app designed to keep both live and asynchronous conversations organized. \ No newline at end of file +# Artifact Description +## Data Race Detection by Digest-Driven Abstract Intepretation + +This is the artifact description for our manuscript **Data Race Detection by Digest-Driven Abstract Intepretation**. + +The artifact contains [Goblint at `race_digest_staging` branch](https://github.com/goblint/analyzer/tree/race_digest_staging). + +## Overview + +This artifact contains the following components: + + Evaluation Results :: The evaluation results, and overview tables (HTML) + generated from the raw data. + Source Code :: Source code for Goblint. + Verifier Binary :: Binary for Goblint. + Benchmark Programs :: Benchmarks used for evaluation (SV-COMP 2025). + BenchExec Tool :: The BenchExec benchmarking tool can be used + to replicate our results on these benchmarks. + +The next section gives instructions on how to setup and quickly get an overview of the artifact. +The subsequent sections then describe each of these components in detail. +The final section gives information on how to reuse this artifact. + +Remark on license: + - `~/analyzer/LICENSE`: Is the MIT license governing the Goblint system as well as ancillary files such as this README + - The benchmarks from SV-COMP come with their individual licenses (all allowing for redistribution), where a `LICENSE` file is located in each folder of tasks or the license is otherwise directly recorded in the file header. + + +## Getting Started + +### 1. Setup + +The artifact is a virtual machine (VM), as the Benchexec system used for reliable benchmarking cannot be installed in docker images. The machine is intended for an x86 machine, behavior on M1 chips is untested. +Follow these steps to set it up: + +* If you have not done so already, install VirtualBox. + () +* Download the artifact. +* Import the artifact via the VirtualBox UI (`File > Import Appliance`). + +You can then start the VM from the VirtualBox UI. +Login with user `goblint` and password `goblint`. + +The machine is configured for `QWERTY` keyboards by default. If you use a different layout, you can click the small `en` button on the top right of the screen to select you keyboard layout. + +### 2. Quick Test of the Benchmark Setup + +To check Goblint is properly installed, run + + cd ~/analyzer + make sanitytest + +on a console in the VM. +The run should take no longer than 2-4 minutes, the expected output is + + Excellent: ignored check on tests/regression/03-practical/21-pfscan_combine_minimal.c:21 is now passing! + Excellent: ignored check on tests/regression/03-practical/21-pfscan_combine_minimal.c:29 is now passing! + No errors :) + +You can also run the analysis for a subset of tasks and configurations by executing from the analyzer directory: + + benchexec ../benchexec/minimal.xml -o minimal_results + +- This runs three configurations on 62 tasks and should run for anywhere between 2 and 7 minutes (depending on your hardware). +- Then, run the command output at the end (will look like `table-generator minimal_results/....`). +- Navigate to `minimal_results/results.*.table.html` (where `*` will be the timestamp when the command was run) and open the HTML file. +- The table will show `none` succeeding (`correct true`) for `1` task, `mutex-only` for `14`, and +`full` for `41`. + + +### 3. Running the Full Experiments + +The full run of the experiments takes somewhere between 5 and 10 hours. If desired, this can be reduced by not evaluating all of the configurations, but only some of them (runtime is proportional to number of configurations). To disable configurations, you can remove them from +`~/benchexec/races.xml`, ideally after making a backup copy in case you decide to run some configuration after all. + +To run the experiments, from `~/analyzer` run + + benchexec ../benchexec/races.xml + +- Then, run the command output at the end (will look like `table-generator results/....`). + + +## Evaluation Results + +This evaluation supports all _experimental_ claims made in Section 7. Please note that Table 1 is not based on our experiments, but cited from the report on SV-COMP 2025. + +- All claims can be verified by opening the tables generated by the steps outlined in (3. Running the Full Experiments) which are located in `~/analyzer/results/results.*.table.html`. +- If results were only generated for some configs in that step, the remaining results can be verified using the tables located in `~/analyzer/results-our-artifact-run/results.*.table.html` where `*` is replaced with the date from our run inside the artifact. + +These are HTML overviews as generated by the BenchExec benchmarking tool, and can be opened by a browser. + +The table contains one configuration for every column of the table in Fig. 8 which are named by the activated digests. + +- The row `correct true` indicates tasks where race-freedom was correctly established. +- The row `correct false` indicates tasks that were correctly identified as racy. (Goblint can't do this, always 0) +- The row `incorrect true` indicates false negatives, i.e., cases where race-freedom was claimed, even though the program is racy. +- The row `incorrect false` indicates false positives, i.e., cases where the definite presence of a race was claimed, but there is none. (Goblint never claims that a program must be racy, always 0) + + +### How the claims are supported by this table: + +> Fig. 8 + +The numbers in Fig. 8 can be directly read off from this table. + + +> None of the approaches produced any false negatives for the other 235 tasks in the benchmark set, which are racy. + +Can be verified by checking that the `incorrect true` number for all configurations is zero. + + +> Discussion in ln. 546ff + +Refers only to numbers in Fig. 8. + + +> With these settings, the system ran out of memory for 4 tasks, 3 tasks timed out, and the analyzer crashed for 7 tasks. + +The numbers in the VM are essentially the same as those on the server as Goblint is inherently single-threaded, and each of the cores of the server is not too powerful. Our run inside the VM matched exactly these numbers, however, some wiggle between machines is to be expected. + +The numbers can be inspected by clicking on the `Table` tab on top of the document. +Then, change the dropdown for one of the configs from `Show all` to: + +- Select `OUT OF MEMORY` to see how often Goblint ran out of memory +- Select `TIMEOUT` to see how often Goblint ran into a timeout +- Select `EXCEPTION(*)` to see the cases where Goblint crashed. + +> Where execution terminated, it did so within at most 20s, where for all but 6 tasks the runtime was below 10s. + +The same caveat as above applies here too. +The numbers can be inspected by clicking on the `Table` tab on top of the document. +Then, sort the runtime in a column by wall time by clicking on `walltime` twice. +In our run inside the artifact, there in fact were no tasks which ran more than `9s`, as each core in our machine for the VM is a bit more powerful than the cores in the server. Your run likely will not yield identical numbers, but they will be in the same ballpark. + + + +The *Table* tab also gives access to detailed evaluation results for each file. +For this to work, first unpack the `*.logfiles.zip` folder located in the `results` folder. +Clicking on a status then shows the complete log for the benchmark run. + +> **Note:** If you are trying to view logs for individual runs through the HTML table (by clicking on the evaluation result `true` or `false`), you may encounter a warning because browsers block access to local files. Follow the instructions in the message to enable log viewing. + + +## Source Code + +The Goblint analyzer () is developed by Technical University of Munich and University of Tartu with one of the authors recently having moved from TUM to National University of Singapore. The source code for Goblint at the time of evaluation can be found in this artifact in the `~/analyzer` directory. + +For an explanation of the general structure of the system, please refer to the online documentation of the system: https://goblint.readthedocs.io/en/latest/ + +The type of code particularly relevant for this paper is best illustrated along an example: + - A digest (lightweight thread ids in Fig. 4) + - Consider the file `~/analyzer/src/analyses/threadFlag.ml` which implements a slightly more powerful version of the lightweight thread ids in Fig. 4 + - $\cal A$ is defined in `~/analyzer/src/cdomains/threadFlagDomain.ml` (Simple) + - The functions `threadenter` and `threadspawn` take care of computing appropriate successors + - ||^? is implemented in the function `may_race` + ~~~ocaml + let may_race (m1,b1) (m2,b2) = + let use_threadflag = GobConfig.get_bool "ana.race.digests.threadflag" in + let both_mt = Flag.is_multi m1 && Flag.is_multi m2 in + let one_not_main = Flag.is_not_main m1 || Flag.is_not_main m2 in + ((not use_threadflag) || (both_mt && one_not_main)) && b1 && b2 + ~~~ + - The `b` components concern interaction with other analysis and can be ignored for now + - After checking whether the digest should be used to exclude races `GobConfig.get_bool "ana.race.digests.threadflag"`, the predicate returns $\top$ (mapped to `true` here) if both accesses happen in multi-threaded mode, and at least one of the threads is not the unique main thread. + - The code in all the other digests is conceptually similar to the code provided here. + - Product of ||^? + - Consider `~/analyzer/src/analyses/mCPAccess.ml`, here the product construction happens + ~~~ocaml + let may_race x y = binop_for_all (fun n (module S: Analyses.MCPA) x y -> + S.may_race (Obj.obj x) (Obj.obj y) + ) x y + ~~~ + - Here a fold over two lists of digests (each corresponding to one activated digest) is performed to get the effect of the definition in Section 5.3) + + +More recent versions of Goblint can be found at . + + +## Verifier Binaries + +A pre-built binary of Goblint is available as `~/analzyer/goblint`. +See `~/analyzer/GOBLINT_README.md` for information on how to run Goblint. +To build Goblint from scratch, run `make release`. + + +## Benchmark Programs + +This artifact includes the benchmark programs on which we evaluated the verifiers. +These benchmarks are taken from the publicly available sv-benchmarks set () +and correspond to the _NoData-Race_ category of SV-COMP'25 (). +The benchmarks are written in C and use POSIX threads (`pthreads`) to model concurrency. + + +## Extending & Reusing This Artifact + +* **Adding benchmarks:** You can easily add your own benchmarks programs written in C by following + the SV-COMP format and adding a task and corresponding *.yml file, e.g., to the folder `~/sv-benchmarks/c/pthread`. The easiest way to go about this is to copy the files `bigshot_p.*` and rename them to `yourtest.*`. + - The `*.c` file is provided for convenience only and contains the unpreprocessed program + - The `*.i` file contains the preprocessed (by GCC) program + - the `*.yml` file specifies: + - The input file (change to `yourtest.i`) + - The properties (of relevance here is only the `no-data-race.prp` property, change expected verdict according to your program) + - The memory model (change if you preprocessed for a 64bit machine) + + The framework automatically picks up new tasks placed in an existing directory. + +* **Adding your own analysis:** The easiest way to do this is to start with a simple analysis such as the thread-flag analysis described above and then gradually modifying it to obtain the desired analysis. + +## Acknowledgment + +This description is based, in part, on earlier artifact descriptions involving the Goblint system, in particular of our VMCAI'24, VMCAI'25 and ESOP'23 papers. diff --git a/conf/bench-yaml-validate.json b/conf/bench-yaml-validate.json index 7b18371bd1..2fcdb418da 100644 --- a/conf/bench-yaml-validate.json +++ b/conf/bench-yaml-validate.json @@ -71,7 +71,6 @@ }, "pre": { "cppflags": [ - "-DGOBLINT_NO_PTHREAD_ONCE", "-DGOBLINT_NO_QSORT", "-DGOBLINT_NO_BSEARCH" ] diff --git a/conf/bench-yaml.json b/conf/bench-yaml.json index fd97b2c08c..52f0b33347 100644 --- a/conf/bench-yaml.json +++ b/conf/bench-yaml.json @@ -67,7 +67,6 @@ }, "pre": { "cppflags": [ - "-DGOBLINT_NO_PTHREAD_ONCE", "-DGOBLINT_NO_QSORT", "-DGOBLINT_NO_BSEARCH" ] diff --git a/conf/ldv-races.json b/conf/ldv-races.json index a06a6da610..da8355c7e8 100644 --- a/conf/ldv-races.json +++ b/conf/ldv-races.json @@ -1,7 +1,6 @@ { "pre": { "cppflags": [ - "-DGOBLINT_NO_PTHREAD_ONCE", "-DGOBLINT_NO_QSORT", "-DGOBLINT_NO_BSEARCH" ] diff --git a/conf/race-digests/fresh-only.json b/conf/race-digests/fresh-only.json new file mode 100644 index 0000000000..9f2cafd408 --- /dev/null +++ b/conf/race-digests/fresh-only.json @@ -0,0 +1,127 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": false, + "interval": true + }, + "float": { + "interval": true, + "evaluate_math_functions": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "partitioned" + } + }, + "race": { + "free": false, + "call": false, + "digests": { + "lockset": false, + "fresh": true, + "region": false, + "symb_locks": false, + "threadflag": false, + "tid": false, + "join" : false + } + }, + "autotune": { + "enabled": true, + "activated": [ + "singleThreaded", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "noOverflows", + "termination", + "tmpSpecialAnalysis" + ] + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "graphml": { + "enabled": true, + "id": "enumerate", + "unknown": false + }, + "yaml": { + "enabled": true, + "format-version": "2.0", + "entry-types": [ + "invariant_set" + ], + "invariant-types": [ + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": false, + "other": false, + "accessed": false, + "exact": true + } + }, + "pre": { + "enabled": false + } +} diff --git a/conf/race-digests/full+once+barrier.json b/conf/race-digests/full+once+barrier.json new file mode 100644 index 0000000000..70ca39b92b --- /dev/null +++ b/conf/race-digests/full+once+barrier.json @@ -0,0 +1,120 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": false, + "interval": true + }, + "float": { + "interval": true, + "evaluate_math_functions": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless", + "pthreadBarriers", + "pthreadOnce" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "partitioned" + } + }, + "race": { + "free": false, + "call": false + }, + "autotune": { + "enabled": true, + "activated": [ + "singleThreaded", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "noOverflows", + "termination", + "tmpSpecialAnalysis" + ] + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "graphml": { + "enabled": true, + "id": "enumerate", + "unknown": false + }, + "yaml": { + "enabled": true, + "format-version": "2.0", + "entry-types": [ + "invariant_set" + ], + "invariant-types": [ + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": false, + "other": false, + "accessed": false, + "exact": true + } + }, + "pre": { + "enabled": false + } +} diff --git a/conf/race-digests/full-minus-region+symblocks.json b/conf/race-digests/full-minus-region+symblocks.json new file mode 100644 index 0000000000..0f7093a867 --- /dev/null +++ b/conf/race-digests/full-minus-region+symblocks.json @@ -0,0 +1,127 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": false, + "interval": true + }, + "float": { + "interval": true, + "evaluate_math_functions": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "partitioned" + } + }, + "race": { + "free": false, + "call": false, + "digests": { + "lockset": true, + "fresh": true, + "region": false, + "symb_locks": false, + "threadflag": true, + "tid": true, + "join" : true + } + }, + "autotune": { + "enabled": true, + "activated": [ + "singleThreaded", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "noOverflows", + "termination", + "tmpSpecialAnalysis" + ] + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "graphml": { + "enabled": true, + "id": "enumerate", + "unknown": false + }, + "yaml": { + "enabled": true, + "format-version": "2.0", + "entry-types": [ + "invariant_set" + ], + "invariant-types": [ + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": false, + "other": false, + "accessed": false, + "exact": true + } + }, + "pre": { + "enabled": false + } +} diff --git a/conf/race-digests/full-minus-region.json b/conf/race-digests/full-minus-region.json new file mode 100644 index 0000000000..afb1b4048c --- /dev/null +++ b/conf/race-digests/full-minus-region.json @@ -0,0 +1,127 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": false, + "interval": true + }, + "float": { + "interval": true, + "evaluate_math_functions": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "partitioned" + } + }, + "race": { + "free": false, + "call": false, + "digests": { + "lockset": true, + "fresh": true, + "region": false, + "symb_locks": true, + "threadflag": true, + "tid": true, + "join" : true + } + }, + "autotune": { + "enabled": true, + "activated": [ + "singleThreaded", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "noOverflows", + "termination", + "tmpSpecialAnalysis" + ] + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "graphml": { + "enabled": true, + "id": "enumerate", + "unknown": false + }, + "yaml": { + "enabled": true, + "format-version": "2.0", + "entry-types": [ + "invariant_set" + ], + "invariant-types": [ + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": false, + "other": false, + "accessed": false, + "exact": true + } + }, + "pre": { + "enabled": false + } +} diff --git a/conf/race-digests/full.json b/conf/race-digests/full.json new file mode 100644 index 0000000000..dedc393ba1 --- /dev/null +++ b/conf/race-digests/full.json @@ -0,0 +1,118 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": false, + "interval": true + }, + "float": { + "interval": true, + "evaluate_math_functions": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "partitioned" + } + }, + "race": { + "free": false, + "call": false + }, + "autotune": { + "enabled": true, + "activated": [ + "singleThreaded", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "noOverflows", + "termination", + "tmpSpecialAnalysis" + ] + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "graphml": { + "enabled": true, + "id": "enumerate", + "unknown": false + }, + "yaml": { + "enabled": true, + "format-version": "2.0", + "entry-types": [ + "invariant_set" + ], + "invariant-types": [ + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": false, + "other": false, + "accessed": false, + "exact": true + } + }, + "pre": { + "enabled": false + } +} diff --git a/conf/race-digests/mutex+threadflag.json b/conf/race-digests/mutex+threadflag.json new file mode 100644 index 0000000000..9bed592781 --- /dev/null +++ b/conf/race-digests/mutex+threadflag.json @@ -0,0 +1,127 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": false, + "interval": true + }, + "float": { + "interval": true, + "evaluate_math_functions": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "partitioned" + } + }, + "race": { + "free": false, + "call": false, + "digests": { + "lockset": true, + + "region": false, + "symb_locks": false, + "threadflag": true, + "tid": false, + "join" : false + } + }, + "autotune": { + "enabled": true, + "activated": [ + "singleThreaded", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "noOverflows", + "termination", + "tmpSpecialAnalysis" + ] + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "graphml": { + "enabled": true, + "id": "enumerate", + "unknown": false + }, + "yaml": { + "enabled": true, + "format-version": "2.0", + "entry-types": [ + "invariant_set" + ], + "invariant-types": [ + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": false, + "other": false, + "accessed": false, + "exact": true + } + }, + "pre": { + "enabled": false + } +} diff --git a/conf/race-digests/mutex-only.json b/conf/race-digests/mutex-only.json new file mode 100644 index 0000000000..a23e3bf546 --- /dev/null +++ b/conf/race-digests/mutex-only.json @@ -0,0 +1,127 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": false, + "interval": true + }, + "float": { + "interval": true, + "evaluate_math_functions": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "partitioned" + } + }, + "race": { + "free": false, + "call": false, + "digests": { + "lockset": true, + "fresh": false, + "region": false, + "symb_locks": false, + "threadflag": false, + "tid": false, + "join" : false + } + }, + "autotune": { + "enabled": true, + "activated": [ + "singleThreaded", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "noOverflows", + "termination", + "tmpSpecialAnalysis" + ] + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "graphml": { + "enabled": true, + "id": "enumerate", + "unknown": false + }, + "yaml": { + "enabled": true, + "format-version": "2.0", + "entry-types": [ + "invariant_set" + ], + "invariant-types": [ + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": false, + "other": false, + "accessed": false, + "exact": true + } + }, + "pre": { + "enabled": false + } +} diff --git a/conf/race-digests/none.json b/conf/race-digests/none.json new file mode 100644 index 0000000000..93b82cc39a --- /dev/null +++ b/conf/race-digests/none.json @@ -0,0 +1,127 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": false, + "interval": true + }, + "float": { + "interval": true, + "evaluate_math_functions": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "partitioned" + } + }, + "race": { + "free": false, + "call": false, + "digests": { + "lockset": false, + "fresh": false, + "region": false, + "symb_locks": false, + "threadflag": false, + "tid": false, + "join" : false + } + }, + "autotune": { + "enabled": true, + "activated": [ + "singleThreaded", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "noOverflows", + "termination", + "tmpSpecialAnalysis" + ] + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "graphml": { + "enabled": true, + "id": "enumerate", + "unknown": false + }, + "yaml": { + "enabled": true, + "format-version": "2.0", + "entry-types": [ + "invariant_set" + ], + "invariant-types": [ + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": false, + "other": false, + "accessed": false, + "exact": true + } + }, + "pre": { + "enabled": false + } +} diff --git a/conf/race-digests/region-only.json b/conf/race-digests/region-only.json new file mode 100644 index 0000000000..e202197269 --- /dev/null +++ b/conf/race-digests/region-only.json @@ -0,0 +1,128 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": false, + "interval": true + }, + "float": { + "interval": true, + "evaluate_math_functions": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "partitioned" + } + }, + "race": { + "free": false, + "call": false, + "digests": { + "lockset": false, + + "fresh": false, + "region": true, + "symb_locks": false, + "threadflag": false, + "tid": false, + "join" : false + } + }, + "autotune": { + "enabled": true, + "activated": [ + "singleThreaded", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "noOverflows", + "termination", + "tmpSpecialAnalysis" + ] + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "graphml": { + "enabled": true, + "id": "enumerate", + "unknown": false + }, + "yaml": { + "enabled": true, + "format-version": "2.0", + "entry-types": [ + "invariant_set" + ], + "invariant-types": [ + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": false, + "other": false, + "accessed": false, + "exact": true + } + }, + "pre": { + "enabled": false + } +} diff --git a/conf/race-digests/symblocks-only.json b/conf/race-digests/symblocks-only.json new file mode 100644 index 0000000000..e3a3ce6a06 --- /dev/null +++ b/conf/race-digests/symblocks-only.json @@ -0,0 +1,128 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": false, + "interval": true + }, + "float": { + "interval": true, + "evaluate_math_functions": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "partitioned" + } + }, + "race": { + "free": false, + "call": false, + "digests": { + "lockset": false, + + "fresh": false, + "region": false, + "symb_locks": true, + "threadflag": false, + "tid": false, + "join" : false + } + }, + "autotune": { + "enabled": true, + "activated": [ + "singleThreaded", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "noOverflows", + "termination", + "tmpSpecialAnalysis" + ] + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "graphml": { + "enabled": true, + "id": "enumerate", + "unknown": false + }, + "yaml": { + "enabled": true, + "format-version": "2.0", + "entry-types": [ + "invariant_set" + ], + "invariant-types": [ + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": false, + "other": false, + "accessed": false, + "exact": true + } + }, + "pre": { + "enabled": false + } +} diff --git a/conf/race-digests/tf-only.json b/conf/race-digests/tf-only.json new file mode 100644 index 0000000000..f87f076c03 --- /dev/null +++ b/conf/race-digests/tf-only.json @@ -0,0 +1,128 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": false, + "interval": true + }, + "float": { + "interval": true, + "evaluate_math_functions": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "partitioned" + } + }, + "race": { + "free": false, + "call": false, + "digests": { + "lockset": false, + + "fresh": false, + "region": false, + "symb_locks": false, + "threadflag": true, + "tid": false, + "join" : false + } + }, + "autotune": { + "enabled": true, + "activated": [ + "singleThreaded", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "noOverflows", + "termination", + "tmpSpecialAnalysis" + ] + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "graphml": { + "enabled": true, + "id": "enumerate", + "unknown": false + }, + "yaml": { + "enabled": true, + "format-version": "2.0", + "entry-types": [ + "invariant_set" + ], + "invariant-types": [ + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": false, + "other": false, + "accessed": false, + "exact": true + } + }, + "pre": { + "enabled": false + } +} diff --git a/conf/race-digests/tid+join.json b/conf/race-digests/tid+join.json new file mode 100644 index 0000000000..55382576e0 --- /dev/null +++ b/conf/race-digests/tid+join.json @@ -0,0 +1,128 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": false, + "interval": true + }, + "float": { + "interval": true, + "evaluate_math_functions": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "partitioned" + } + }, + "race": { + "free": false, + "call": false, + "digests": { + "lockset": false, + + "fresh": false, + "region": false, + "symb_locks": false, + "threadflag": false, + "tid": true, + "join" : true + } + }, + "autotune": { + "enabled": true, + "activated": [ + "singleThreaded", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "noOverflows", + "termination", + "tmpSpecialAnalysis" + ] + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "graphml": { + "enabled": true, + "id": "enumerate", + "unknown": false + }, + "yaml": { + "enabled": true, + "format-version": "2.0", + "entry-types": [ + "invariant_set" + ], + "invariant-types": [ + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": false, + "other": false, + "accessed": false, + "exact": true + } + }, + "pre": { + "enabled": false + } +} diff --git a/conf/race-digests/tid+mutex+join.json b/conf/race-digests/tid+mutex+join.json new file mode 100644 index 0000000000..e32d35f73c --- /dev/null +++ b/conf/race-digests/tid+mutex+join.json @@ -0,0 +1,128 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": false, + "interval": true + }, + "float": { + "interval": true, + "evaluate_math_functions": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "partitioned" + } + }, + "race": { + "free": false, + "call": false, + "digests": { + "lockset": true, + + "fresh": false, + "region": false, + "symb_locks": false, + "threadflag": false, + "tid": true, + "join" : true + } + }, + "autotune": { + "enabled": true, + "activated": [ + "singleThreaded", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "noOverflows", + "termination", + "tmpSpecialAnalysis" + ] + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "graphml": { + "enabled": true, + "id": "enumerate", + "unknown": false + }, + "yaml": { + "enabled": true, + "format-version": "2.0", + "entry-types": [ + "invariant_set" + ], + "invariant-types": [ + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": false, + "other": false, + "accessed": false, + "exact": true + } + }, + "pre": { + "enabled": false + } +} diff --git a/conf/race-digests/tid+mutex.json b/conf/race-digests/tid+mutex.json new file mode 100644 index 0000000000..f5baca160c --- /dev/null +++ b/conf/race-digests/tid+mutex.json @@ -0,0 +1,128 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": false, + "interval": true + }, + "float": { + "interval": true, + "evaluate_math_functions": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "partitioned" + } + }, + "race": { + "free": false, + "call": false, + "digests": { + "lockset": true, + + "fresh": false, + "region": false, + "symb_locks": false, + "threadflag": false, + "tid": true, + "join" : false + } + }, + "autotune": { + "enabled": true, + "activated": [ + "singleThreaded", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "noOverflows", + "termination", + "tmpSpecialAnalysis" + ] + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "graphml": { + "enabled": true, + "id": "enumerate", + "unknown": false + }, + "yaml": { + "enabled": true, + "format-version": "2.0", + "entry-types": [ + "invariant_set" + ], + "invariant-types": [ + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": false, + "other": false, + "accessed": false, + "exact": true + } + }, + "pre": { + "enabled": false + } +} diff --git a/conf/race-digests/tid-only.json b/conf/race-digests/tid-only.json new file mode 100644 index 0000000000..c97b857073 --- /dev/null +++ b/conf/race-digests/tid-only.json @@ -0,0 +1,128 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": false, + "interval": true + }, + "float": { + "interval": true, + "evaluate_math_functions": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "partitioned" + } + }, + "race": { + "free": false, + "call": false, + "digests": { + "lockset": false, + + "fresh": false, + "region": false, + "symb_locks": false, + "threadflag": false, + "tid": true, + "join" : false + } + }, + "autotune": { + "enabled": true, + "activated": [ + "singleThreaded", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "noOverflows", + "termination", + "tmpSpecialAnalysis" + ] + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "graphml": { + "enabled": true, + "id": "enumerate", + "unknown": false + }, + "yaml": { + "enabled": true, + "format-version": "2.0", + "entry-types": [ + "invariant_set" + ], + "invariant-types": [ + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": false, + "other": false, + "accessed": false, + "exact": true + } + }, + "pre": { + "enabled": false + } +} diff --git a/conf/traces-rel.json b/conf/traces-rel.json index 2b82a57554..fafb397a7f 100644 --- a/conf/traces-rel.json +++ b/conf/traces-rel.json @@ -83,7 +83,6 @@ }, "pre": { "cppflags": [ - "-DGOBLINT_NO_PTHREAD_ONCE", "-DGOBLINT_NO_QSORT", "-DGOBLINT_NO_BSEARCH" ] diff --git a/lib/libc/stub/src/pthread.c b/lib/libc/stub/src/pthread.c deleted file mode 100644 index 1de6202b4b..0000000000 --- a/lib/libc/stub/src/pthread.c +++ /dev/null @@ -1,11 +0,0 @@ -#ifndef GOBLINT_NO_PTHREAD_ONCE -#include - -int pthread_once(pthread_once_t *once_control,void (*init_routine)(void)) __attribute__((goblint_stub)); -int pthread_once(pthread_once_t *once_control,void (*init_routine)(void)) { - // Not actually once, just call it - int top; - init_routine(); - return top; -} -#endif diff --git a/make.sh b/make.sh index 0f76759065..a5d1691fd8 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.2+options,ocaml-option-flambda --locked + opam switch -y create . --deps-only --packages=ocaml-variants.4.14.2+options,ocaml-option-flambda } rule() { @@ -75,13 +75,13 @@ rule() { ;; setup) echo "Make sure you have the following installed: opam >= 2.0.0, git, patch, m4, autoconf, libgmp-dev, libmpfr-dev, pkg-config" echo "For the --html output you also need: javac, ant, dot (graphviz)" - echo "For running the regression tests you also need: ruby, gem, curl" + echo "For running the regression tests you also need: ruby, gem, curl, and the `os` gem" echo "For reference see ./Dockerfile or ./scripts/travis-ci.sh" opam_setup ;; dev) eval $(opam env) echo "Installing opam packages for test and doc..." - opam install -y . --deps-only --locked --with-test --with-doc + opam install -y . --deps-only --with-test --with-doc echo "Installing opam packages for development..." opam install -y ocaml-lsp-server ocp-indent # ocaml-lsp-server is needed for https://github.com/ocamllabs/vscode-ocaml-platform @@ -90,6 +90,7 @@ rule() { # Use `git commit -n` to temporarily bypass the hook if necessary. echo "Installing gem parallel (not needed for ./scripts/update_suite.rb -s)" sudo gem install parallel + sudo gem install os ;; headers) curl -L -O https://github.com/goblint/linux-headers/archive/master.tar.gz tar xf master.tar.gz && rm master.tar.gz diff --git a/scripts/sv-comp/archive.sh b/scripts/sv-comp/archive.sh index aefac8f769..33ea1b4368 100755 --- a/scripts/sv-comp/archive.sh +++ b/scripts/sv-comp/archive.sh @@ -37,7 +37,6 @@ zip goblint/scripts/sv-comp/goblint.zip \ goblint/lib/libc/stub/include/assert.h \ goblint/lib/goblint/runtime/include/goblint.h \ goblint/lib/libc/stub/src/stdlib.c \ - goblint/lib/libc/stub/src/pthread.c \ goblint/lib/sv-comp/stub/src/sv-comp.c \ goblint/README.md \ goblint/LICENSE diff --git a/scripts/update_suite.rb b/scripts/update_suite.rb index b21fb4b532..74fddc7b04 100755 --- a/scripts/update_suite.rb +++ b/scripts/update_suite.rb @@ -2,6 +2,7 @@ # gobopt environment variable can be used to override goblint defaults and PARAMs +require 'os' require 'find' require 'fileutils' require 'timeout' @@ -575,6 +576,8 @@ def run () end end +mac = OS.mac? + #processing the file information projects = [] project_ids = Set.new @@ -603,6 +606,7 @@ def run () lines = IO.readlines(path, :encoding => "UTF-8") next if not future and only.nil? and lines[0] =~ /SKIP/ + next if mac and lines[0] =~ /NOMAC/ next if marshal and lines[0] =~ /NOMARSHAL/ next if not has_linux_headers and lines[0] =~ /kernel/ if incremental then diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml index 55d79a1131..4c2741ac4a 100644 --- a/src/analyses/accessAnalysis.ml +++ b/src/analyses/accessAnalysis.ml @@ -28,8 +28,7 @@ struct let init _ = collect_local := get_bool "witness.yaml.enabled" && get_bool "witness.invariant.accessed"; - let activated = get_string_list "ana.activated" in - emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated + emit_single_threaded := true let do_access (man: (D.t, G.t, C.t, V.t) man) (kind:AccessKind.t) (reach:bool) (e:exp) = if M.tracing then M.trace "access" "do_access %a %a %B" d_exp e AccessKind.pretty kind reach; diff --git a/src/analyses/mallocFresh.ml b/src/analyses/mallocFresh.ml index c226d7e6ce..4e7bd84571 100644 --- a/src/analyses/mallocFresh.ml +++ b/src/analyses/mallocFresh.ml @@ -64,7 +64,9 @@ struct struct include BoolDomain.Bool let name () = "fresh" - let may_race f1 f2 = not (f1 || f2) + let may_race f1 f2 = + let use_fresh = GobConfig.get_bool "ana.race.digests.fresh" in + (not use_fresh) || not (f1 || f2) let should_print f = f end let access man (a: Queries.access) = diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index c712ca9644..996eca9954 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -267,6 +267,8 @@ struct include MustLocksetRW let name () = "lock" let may_race ls1 ls2 = + let use_lockset = GobConfig.get_bool "ana.race.digests.lockset" in + (not use_lockset) || (* not mutually exclusive *) not @@ exists (fun ((m1, w1) as l1) -> if w1 then diff --git a/src/analyses/pthreadBarriers.ml b/src/analyses/pthreadBarriers.ml new file mode 100644 index 0000000000..cc51c163c6 --- /dev/null +++ b/src/analyses/pthreadBarriers.ml @@ -0,0 +1,167 @@ +(** Must have waited barriers for Pthread barriers ([pthreadBarriers]). *) + +open GoblintCil +open Analyses +module LF = LibraryFunctions + +module Spec = +struct + module Barriers = struct + include SetDomain.ToppedSet (ValueDomain.Addr) (struct let topname = "All barriers" end) + let name () = "mayBarriers" + end + + module MustBarriers = struct + include Lattice.Reverse (Barriers) + let name () = "mustBarriers" + end + + module Capacity = Queries.ID + + include Analyses.IdentitySpec + module V = VarinfoV + + module TID = ThreadIdDomain.ThreadLifted + + module MHPplusLock = struct + module Locks = LockDomain.MustLockset + + include Printable.Prod (MHP) (Locks) + let name () = "MHPplusLock" + + let mhp (mhp1, l1) (mhp2, l2) = + MHP.may_happen_in_parallel mhp1 mhp2 && Locks.is_empty (Locks.inter l1 l2) + + let tid ((mhp:MHP.t), _) = mhp.tid + + let may_be_non_unique_thread (mhp, _) = MHP.may_be_non_unique_thread mhp + end + + module Waiters = SetDomain.ToppedSet (MHPplusLock) (struct let topname = "All MHP" end) + module Multiprocess = BoolDomain.MayBool + module G = Lattice.Prod3 (Multiprocess) (Capacity) (Waiters) + + let name () = "pthreadBarriers" + + module MustObserved = MapDomain.MapTop_LiftBot (TID) (MustBarriers) + module D = Lattice.Prod (Barriers) (MustObserved) + + include Analyses.ValueContexts(D) + + let possible_vinfos (a: Queries.ask) barrier = + Queries.AD.to_var_may (a.f (Queries.MayPointTo barrier)) + + let special man (lval: lval option) (f:varinfo) (arglist:exp list) : D.t = + let exists_k pred k waiters = + let k_product elems = + let rec doit k = + if k = 1 then + Seq.map (Seq.return) elems + else + let arg = doit (k-1) in + Seq.map_product (Seq.cons) elems arg + in + doit k + in + Seq.exists pred (k_product (Waiters.to_seq waiters)) + in + let desc = LF.find f in + match desc.special arglist with + | BarrierWait barrier -> + let ask = Analyses.ask_of_man man in + let may, must = man.local in + let barriers = possible_vinfos ask barrier in + let mhp = MHP.current ask in + let handle_one b = + try + let locks = man.ask (Queries.MustLockset) in + man.sideg b (Multiprocess.bot (), Capacity.bot (), Waiters.singleton (mhp, locks)); + let addr = ValueDomain.Addr.of_var b in + let (multiprocess, capacity, waiters) = man.global b in + let may = Barriers.add addr may in + if multiprocess then + (may, must) + else + let relevant_waiters = Waiters.filter (fun other -> MHPplusLock.mhp (mhp, locks) other) waiters in + if Waiters.exists MHPplusLock.may_be_non_unique_thread relevant_waiters then + (may, must) + else + match capacity with + | `Top | `Bot -> (may, must) + | `Lifted c -> + let count = Waiters.cardinal relevant_waiters in + (* Add 1 as the thread calling wait at the moment will not be MHP with itself *) + let min_cap = (BatOption.default Z.zero (Capacity.I.minimal c)) in + if Z.leq min_cap Z.one then + (may, must) + else if Z.geq (Z.of_int (count + 1)) min_cap then + (* This is quite a cute problem: Do (min_cap-1) elements exist in the set such that + MHP is pairwise true? This solution is a sledgehammer, there should be something much + better algorithmically (beyond just laziness) *) + let must = + let waiters = Waiters.elements relevant_waiters in + let min_cap = Z.to_int min_cap in + let can_proceed_pred seq = + let rec doit seq = match Seq.uncons seq with + | None -> true + | Some (h, t) -> Seq.for_all (MHPplusLock.mhp h) t && doit t + in + doit seq + in + let can_proceed = exists_k can_proceed_pred (min_cap - 1) relevant_waiters in + if not can_proceed then raise Analyses.Deadcode; + (* limit to this case to avoid having to construct all permutations above *) + if BatList.compare_length_with waiters (min_cap - 1) = 0 then + List.fold_left (fun acc elem -> + let tid = MHPplusLock.tid elem in + let curr = MustObserved.find tid acc in + let must' = MustObserved.add tid (Barriers.add addr curr) acc in + must' + ) must waiters + else + must + in + (may, must) + else + raise Analyses.Deadcode; + with Analyses.Deadcode -> D.bot () + in + let (may, must) = List.fold_left (fun acc b-> D.join acc (handle_one b)) (D.bot ()) barriers in + if Barriers.is_empty may then raise Analyses.Deadcode; + (may, must) + | BarrierInit { barrier; attr; count } -> + let multitprocess = not @@ Queries.AD.is_null @@ man.ask (Queries.MayPointTo attr) in + if multitprocess then M.warn "Barrier initialized with a non-NULL attr argument. Handled as if PTHREAD_PROCESS_SHARED potentially set."; + let count = man.ask (Queries.EvalInt count) in + let publish_one b = man.sideg b (multitprocess, count, Waiters.bot ()) in + let barriers = possible_vinfos (Analyses.ask_of_man man) barrier in + List.iter publish_one barriers; + man.local + | _ -> man.local + + let startstate v = (Barriers.empty (), MustObserved.empty ()) + let threadenter man ~multiple lval f args = [man.local] + let exitstate v = (Barriers.empty (), MustObserved.empty ()) + + module A = + struct + include Lattice.Prod3 (Barriers) (MustObserved) (TID) + let name () = "barriers" + let may_race (may_await_t1, must_observed_by_t1, t1) (may_await_t2, must_observed_by_t2, t2) = + let observed_from_t2 = MustObserved.find t2 must_observed_by_t1 in + if not (Barriers.subset observed_from_t2 may_await_t2) then + false + else + let observed_from_t1 = MustObserved.find t1 must_observed_by_t2 in + Barriers.subset observed_from_t1 may_await_t1 + let should_print f = true + end + + let access man (a: Queries.access) = + let (may,must) = man.local in + let mhp = MHP.current (Analyses.ask_of_man man) in + (may, must, mhp.tid) +end + +let _ = + MCP.register_analysis (module Spec : MCPSpec) diff --git a/src/analyses/pthreadOnce.ml b/src/analyses/pthreadOnce.ml new file mode 100644 index 0000000000..cc7dc3e611 --- /dev/null +++ b/src/analyses/pthreadOnce.ml @@ -0,0 +1,109 @@ +(** Must active and have passed pthreadOnce calls ([pthreadOnce]). *) + +open GoblintCil +open Analyses +module LF = LibraryFunctions + +module Spec = +struct + module Onces = struct + include SetDomain.ToppedSet (CilType.Varinfo) (struct let topname = "All onces" end) + let name () = "mayOnces" + end + + module ActiveOnces = struct + include Lattice.Reverse (Onces) + let name () = "active" + end + + module SeenOnces = struct + include Lattice.Reverse (Onces) + let name () = "seen" + end + + include Analyses.DefaultSpec + + let name () = "pthreadOnce" + module D = Lattice.Prod (ActiveOnces) (SeenOnces) + include Analyses.ValueContexts(D) + + (* transfer functions *) + let assign man (lval:lval) (rval:exp) : D.t = + man.local + + let branch man (exp:exp) (tv:bool) : D.t = + man.local + + let body man (f:fundec) : D.t = + man.local + + let return man (exp:exp option) (f:fundec) : D.t = + man.local + + let enter man (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = + [man.local, man.local] + + let combine_env man lval fexp f args fc au f_ask = + au + + let combine_assign man (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t = + man.local + + let special man (lval: lval option) (f:varinfo) (arglist:exp list) : D.t = + man.local + + let startstate v = (Onces.empty (), Onces.empty ()) + + let possible_vinfos (a: Queries.ask) barrier = + Queries.AD.to_var_may (a.f (Queries.MayPointTo barrier)) + + let event man (e: Events.t) oman : D.t = + match e with + | Events.EnterOnce { once_control; tf } when tf -> + (let (active, seen) = man.local in + let ask = Analyses.ask_of_man man in + let possible_vinfos = possible_vinfos ask once_control in + let unseen = List.filter (fun v -> not (Onces.mem v seen) && not (Onces.mem v active)) possible_vinfos in + match unseen with + | [] -> raise Deadcode + | [v] -> (Onces.add v active, seen) + | _ :: _ -> man.local) + | Events.EnterOnce { once_control; tf } -> + (let (active, seen) = man.local in + let ask = Analyses.ask_of_man man in + match possible_vinfos ask once_control with + | [v] -> (Onces.add v active, seen) + | _ -> man.local) + | Events.LeaveOnce { once_control } -> + (let (active, seen) = man.local in + let ask = Analyses.ask_of_man man in + let active' = Onces.diff active (Onces.of_list (possible_vinfos ask once_control)) in + let seen' = match possible_vinfos ask once_control with + | [v] -> Onces.add v seen + | _ -> seen + in + (active', seen')) + | _ -> man.local + + let access man _ = man.local + + module A = + struct + include D + let name () = "onces" + let may_race (a1, s1) (a2, s2) = + (Onces.is_empty (Onces.inter a1 (Onces.union a2 s2))) && (Onces.is_empty (Onces.inter a2 (Onces.union a1 s1))) + let should_print (a1, s1) = not (Onces.is_empty a1) || not (Onces.is_empty s1) + end + + + let threadenter man ~multiple lval f args = + let (_, seen) = man.local in + [Onces.empty (), seen] + + let threadspawn man ~multiple lval f args fman = man.local + let exitstate v = D.top () +end + +let _ = + MCP.register_analysis (module Spec : MCPSpec) diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index 263506b4fb..c1ca2e97b9 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -304,7 +304,7 @@ struct let event man e oman = match e with - | Events.Access {exp; ad; kind; reach} when ThreadFlag.is_currently_multi (Analyses.ask_of_man man) -> (* threadflag query in post-threadspawn man *) + | Events.Access {exp; ad; kind; reach} when true (* ThreadFlag.is_currently_multi (Analyses.ask_of_man man) *) -> (* threadflag query in post-threadspawn man *) (* must use original (pre-assign, etc) man queries *) let conf = 110 in let module AD = Queries.AD in diff --git a/src/analyses/region.ml b/src/analyses/region.ml index 0fb61059e2..d02df20d0d 100644 --- a/src/analyses/region.ml +++ b/src/analyses/region.ml @@ -64,7 +64,10 @@ struct struct include Printable.Option (Lvals) (struct let name = "no region" end) let name () = "region" - let may_race r1 r2 = match r1, r2 with + let may_race r1 r2 = + let use_region = GobConfig.get_bool "ana.race.digests.region" in + (not use_region) || + match r1, r2 with | None, _ | _, None -> false (* TODO: Should it happen in the first place that RegMap has empty value? Happens in 09-regions/34-escape_rc *) diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml index 0850fac317..9cf212b6b9 100644 --- a/src/analyses/symbLocks.ml +++ b/src/analyses/symbLocks.ml @@ -121,7 +121,9 @@ struct include SetDomain.Make (E) let name () = "symblock" - let may_race lp lp2 = disjoint lp lp2 + let may_race lp lp2 = + let use_symblocks = GobConfig.get_bool "ana.race.digests.symb_locks" in + (not use_symblocks) || disjoint lp lp2 let should_print lp = not (is_empty lp) end diff --git a/src/analyses/threadFlag.ml b/src/analyses/threadFlag.ml index 1e0ff7db9f..1e362fa104 100644 --- a/src/analyses/threadFlag.ml +++ b/src/analyses/threadFlag.ml @@ -54,13 +54,30 @@ struct module A = struct - include BoolDomain.Bool - let name () = "multi" - let may_race m1 m2 = m1 && m2 (* kill access when single threaded *) - let should_print m = not m + include Lattice.Prod(Flag)(BoolDomain.MayBool) + let name () = "threadflag" + + let may_race (m1,b1) (m2,b2) = + let use_threadflag = GobConfig.get_bool "ana.race.digests.threadflag" in + let both_mt = Flag.is_multi m1 && Flag.is_multi m2 in + let one_not_main = Flag.is_not_main m1 || Flag.is_not_main m2 in + ((not use_threadflag) || (both_mt && one_not_main)) && b1 && b2 + + (* kill access when single threaded *) + + let should_print m = true end + let access man _ = - is_currently_multi (Analyses.ask_of_man man) + let st = + if GobConfig.get_bool "ana.race.digests.join" then + is_currently_multi (Analyses.ask_of_man man) + else if GobConfig.get_bool "ana.race.digests.tid" then + has_ever_been_multi (Analyses.ask_of_man man) + else + true + in + ((man.local,st):A.t) let threadenter man ~multiple lval f args = if not (has_ever_been_multi (Analyses.ask_of_man man)) then diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml index 53d070a056..c6e521b1d5 100644 --- a/src/analyses/threadId.ml +++ b/src/analyses/threadId.ml @@ -132,7 +132,10 @@ struct struct include Printable.Option (ThreadLifted) (struct let name = "nonunique" end) let name () = "thread" - let may_race (t1: t) (t2: t) = match t1, t2 with + let may_race (t1: t) (t2: t) = + let use_tid = GobConfig.get_bool "ana.race.digests.tid" in + (not use_tid) || + match t1, t2 with | Some t1, Some t2 when ThreadLifted.equal t1 t2 -> false (* only unique threads *) | _, _ -> true let should_print = Option.is_some diff --git a/src/cdomains/mHP.ml b/src/cdomains/mHP.ml index afaf6d67e3..dc6d49a529 100644 --- a/src/cdomains/mHP.ml +++ b/src/cdomains/mHP.ml @@ -77,18 +77,25 @@ let must_be_joined other joined = (** May two program points with respective MHP information happen in parallel *) let may_happen_in_parallel one two = - let {tid=tid; created=created; must_joined=must_joined} = one in + let use_tid = GobConfig.get_bool "ana.race.digests.tid" in + let use_join = GobConfig.get_bool "ana.race.digests.join" in + let {tid; created; must_joined} = one in let {tid=tid2; created=created2; must_joined=must_joined2} = two in match tid,tid2 with | `Lifted tid, `Lifted tid2 -> - if (TID.is_unique tid) && (TID.equal tid tid2) then + if use_tid && (TID.is_unique tid) && (TID.equal tid tid2) then false - else if definitely_not_started (tid,created) tid2 || definitely_not_started (tid2,created2) tid then + else if use_tid && (definitely_not_started (tid,created) tid2 || definitely_not_started (tid2,created2) tid) then false - else if must_be_joined tid2 must_joined || must_be_joined tid must_joined2 then + else if use_tid && use_join && (must_be_joined tid2 must_joined || must_be_joined tid must_joined2) then false - else if exists_definitely_not_started_in_joined (tid,created) must_joined2 || exists_definitely_not_started_in_joined (tid2,created2) must_joined then + else if use_tid && use_join && (exists_definitely_not_started_in_joined (tid,created) must_joined2 || exists_definitely_not_started_in_joined (tid2,created2) must_joined) then false else true | _ -> true + +let may_be_non_unique_thread mhp = + match mhp.tid with + | `Lifted tid -> not (TID.is_unique tid) + | _ -> true \ No newline at end of file diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 39c863ad49..8a11ed88de 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -1105,6 +1105,55 @@ "description": "Report races for volatile variables.", "type": "boolean", "default": true + }, + "digests": { + "title": "ana.race.digests", + "type" : "object", + "properties" : { + "lockset" : { + "title": "ana.race.digests.lockset", + "description": "Use lockset digest for excluding data races.", + "type" : "boolean", + "default" : true + }, + "fresh" : { + "title": "ana.race.digests.fresh", + "description": "Use freshness analysis for excluding data races.", + "type" : "boolean", + "default" : true + }, + "region" : { + "title": "ana.race.digests.region", + "description": "Use region analysis for excluding data races.", + "type" : "boolean", + "default" : true + }, + "symb_locks" : { + "title": "ana.race.digests.symb_locks", + "description": "Use symb_locks analysis for excluding data races.", + "type" : "boolean", + "default" : true + }, + "threadflag" : { + "title": "ana.race.digests.threadflag", + "description": "Use threadflag analysis for excluding data races.", + "type" : "boolean", + "default" : true + }, + "tid" : { + "title": "ana.race.digests.tid", + "description": "Use tid analysis for excluding data races.", + "type" : "boolean", + "default" : true + }, + "join" : { + "title": "ana.race.digests.join", + "description": "Use join analysis for excluding data races.", + "type" : "boolean", + "default" : true + } + }, + "additionalProperties": false } }, "additionalProperties": false diff --git a/src/domain/disjointDomain.ml b/src/domain/disjointDomain.ml index 3e02c1d3a0..35a730a4d5 100644 --- a/src/domain/disjointDomain.ml +++ b/src/domain/disjointDomain.ml @@ -117,6 +117,7 @@ struct add e acc ) (empty ()) es let elements m = fold List.cons m [] (* no intermediate per-bucket lists *) + let to_seq m = fold Seq.cons m Seq.empty let map f m = fold (fun e acc -> add (f e) acc ) m (empty ()) (* no intermediate lists *) @@ -323,6 +324,7 @@ struct add e acc ) (empty ()) es let elements m = fold List.cons m [] (* no intermediate per-bucket lists *) + let to_seq m = fold Seq.cons m Seq.empty let map f s = fold (fun e acc -> add (f e) acc ) s (empty ()) (* no intermediate lists *) diff --git a/src/domain/setDomain.ml b/src/domain/setDomain.ml index c552363f3d..e11c8182de 100644 --- a/src/domain/setDomain.ml +++ b/src/domain/setDomain.ml @@ -95,6 +95,12 @@ sig On set abstractions this lists only canonical elements, not all subsumed elements. *) + val to_seq: t -> elt Seq.t + (** See {!Set.S.to_seq}. + + On set abstractions this lists only canonical elements, + not all subsumed elements. *) + val of_list: elt list -> t val min_elt: t -> elt @@ -332,6 +338,7 @@ struct let exists f = schema_default true (S.exists f) let filter f = schema (fun t -> `Lifted (S.filter f t)) "filter on `Top" let elements = schema S.elements "elements on `Top" + let to_seq = schema S.to_seq "to_seq on `Top" let of_list xs = `Lifted (S.of_list xs) let cardinal = schema S.cardinal "cardinal on `Top" let min_elt = schema S.min_elt "min_elt on `Top" @@ -471,6 +478,7 @@ struct let mem e e' = E.leq e e' let choose e = e let elements e = [e] + let to_seq e = Seq.return e let remove e e' = if E.leq e' e then E.bot () (* NB! strong removal *) diff --git a/src/domains/events.ml b/src/domains/events.ml index cc4af83819..205b81e443 100644 --- a/src/domains/events.ml +++ b/src/domains/events.ml @@ -16,6 +16,8 @@ type t = | Assert of exp | Unassume of {exp: CilType.Exp.t; tokens: WideningToken.t list} | Longjmped of {lval: CilType.Lval.t option} + | EnterOnce of {once_control: CilType.Exp.t; tf:bool} + | LeaveOnce of {once_control: CilType.Exp.t} (** Should event be emitted after transfer function raises [Deadcode]? *) let emit_on_deadcode = function @@ -31,7 +33,9 @@ let emit_on_deadcode = function | UpdateExpSplit _ (* Pointless to split on dead. *) | Unassume _ (* Avoid spurious writes. *) | Assert _ (* Pointless to refine dead. *) - | Longjmped _ -> + | Longjmped _ + | EnterOnce _ + | LeaveOnce _ -> false let pretty () = function @@ -47,3 +51,5 @@ let pretty () = function | Assert exp -> dprintf "Assert %a" d_exp exp | Unassume {exp; tokens} -> dprintf "Unassume {exp=%a; tokens=%a}" d_exp exp (d_list ", " WideningToken.pretty) tokens | Longjmped {lval} -> dprintf "Longjmped {lval=%a}" (docOpt (CilType.Lval.pretty ())) lval + | EnterOnce {once_control; tf} -> dprintf "todo" + | LeaveOnce {once_control} -> dprintf "todo" diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index c7cfce95d2..93755e668c 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -245,7 +245,7 @@ struct let tf_special_call man lv f args = S.special man lv f args - let tf_proc var edge prev_node lv e args getl sidel getg sideg d = + let rec tf_proc var edge prev_node lv e args getl sidel getg sideg d = let man, r, spawns = common_man var edge prev_node d getl sidel getg sideg in let functions = match e with @@ -258,6 +258,34 @@ struct let ad = man.ask (Queries.EvalFunvar e) in Queries.AD.to_var_may ad (* TODO: don't convert, handle UnknownPtr below *) in + let once once_control init_routine = + let enter = + let d' = S.event man (Events.EnterOnce { once_control; tf = true }) man in + let proc = tf_proc var edge prev_node None init_routine [] getl sidel getg sideg d' in + if not (S.D.is_bot proc) then + let rec proc_man = + { man with + ask = (fun (type a) (q: a Queries.t) -> S.query proc_man q); + local = proc; + } + in + S.event proc_man (Events.LeaveOnce { once_control }) proc_man + else + S.D.bot () + in + let not_enter = + (* Always possible, will never yield `Bot *) + let d' = S.event man (Events.EnterOnce { once_control; tf = false }) man in + let rec d'_man = + { man with + ask = (fun (type a) (q: a Queries.t) -> S.query d'_man q); + local = d'; + } + in + S.event d'_man (Events.LeaveOnce { once_control }) d'_man + in + D.join enter not_enter + in let one_function f = match f.vtype with | TFun (_, params, var_arg, _) -> @@ -266,14 +294,21 @@ struct (* Check whether number of arguments fits. *) (* If params is None, the function or its parameters are not declared, so we still analyze the unknown function call. *) if Option.is_none params || p_length = arg_length || (var_arg && arg_length >= p_length) then - begin Some (match Cilfacade.find_varinfo_fundec f with - | fd when LibraryFunctions.use_special f.vname -> - M.info ~category:Analyzer "Using special for defined function %s" f.vname; - tf_special_call man lv f args - | fd -> - tf_normal_call man lv e fd args getl sidel getg sideg - | exception Not_found -> - tf_special_call man lv f args) + begin + let is_once = LibraryFunctions.find ~nowarn:true f in + match is_once.special args with + | Once { once_control; init_routine } -> + Some (once once_control init_routine) + | _ + | exception LibraryDsl.Expected _-> (* propagate weirdness inside *) + Some (match Cilfacade.find_varinfo_fundec f with + | fd when LibraryFunctions.use_special f.vname -> + M.info ~category:Analyzer "Using special for defined function %s" f.vname; + tf_special_call man lv f args + | fd -> + tf_normal_call man lv e fd args getl sidel getg sideg + | exception Not_found -> + tf_special_call man lv f args) end else begin let geq = if var_arg then ">=" else "" in diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml index 415fb21605..96e816b32c 100644 --- a/src/goblint_lib.ml +++ b/src/goblint_lib.ml @@ -129,7 +129,9 @@ module BasePriv = BasePriv module RelationPriv = RelationPriv module ThreadEscape = ThreadEscape module PthreadSignals = PthreadSignals +module PthreadBarriers = PthreadBarriers module ExtractPthread = ExtractPthread +module PthreadOnce = PthreadOnce (** {2 Longjmp} diff --git a/src/maingoblint.ml b/src/maingoblint.ml index cb81ea0b86..c3f1d0f9ea 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -418,9 +418,6 @@ let preprocess_files () = if List.mem "c" (get_string_list "lib.activated") then extra_files := find_custom_include (Fpath.v "stdlib.c") :: !extra_files; - if List.mem "pthread" (get_string_list "lib.activated") then - extra_files := find_custom_include (Fpath.v "pthread.c") :: !extra_files; - if List.mem "sv-comp" (get_string_list "lib.activated") then extra_files := find_custom_include (Fpath.v "sv-comp.c") :: !extra_files; diff --git a/src/util/library/libraryDesc.ml b/src/util/library/libraryDesc.ml index 6f34de1864..862205aad1 100644 --- a/src/util/library/libraryDesc.ml +++ b/src/util/library/libraryDesc.ml @@ -69,6 +69,8 @@ type special = | SemDestroy of Cil.exp | Wait of { cond: Cil.exp; mutex: Cil.exp; } | TimedWait of { cond: Cil.exp; mutex: Cil.exp; abstime: Cil.exp; (** Unused *) } + | BarrierWait of Cil.exp + | BarrierInit of { barrier: Cil.exp; attr:Cil.exp; count: Cil.exp; } | Math of { fun_args: math; } | Memset of { dest: Cil.exp; ch: Cil.exp; count: Cil.exp; } | Bzero of { dest: Cil.exp; count: Cil.exp; } @@ -84,6 +86,7 @@ type special = | Longjmp of { env: Cil.exp; value: Cil.exp; } | Bounded of { exp: Cil.exp} (** Used to check for bounds for termination analysis. *) | Rand + | Once of { once_control: Cil.exp; init_routine: Cil.exp; } | Unknown (** Anything not belonging to other types. *) (* TODO: rename to Other? *) diff --git a/src/util/library/libraryDsl.ml b/src/util/library/libraryDsl.ml index a380714dc0..240c318579 100644 --- a/src/util/library/libraryDsl.ml +++ b/src/util/library/libraryDsl.ml @@ -30,6 +30,8 @@ struct | [] -> fail "^::" end +exception Expected = Pattern.Expected + type access = | Access of LibraryDesc.Access.t | If of (unit -> bool) * access diff --git a/src/util/library/libraryDsl.mli b/src/util/library/libraryDsl.mli index 42c300af8e..2eed55666d 100644 --- a/src/util/library/libraryDsl.mli +++ b/src/util/library/libraryDsl.mli @@ -82,3 +82,5 @@ val c_deep: access (** Conditional access, e.g. on an option. *) val if_: (unit -> bool) -> access -> access + +exception Expected of string diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml index 6643b58eef..326637654e 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -464,6 +464,7 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("pthread_create", special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [s]; __ "arg" []] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg; multiple = false }); (* For precision purposes arg is not considered accessed here. Instead all accesses (if any) come from actually analyzing start_routine. *) ("pthread_exit", special [__ "retval" []] @@ fun retval -> ThreadExit { ret_val = retval }); (* Doesn't dereference the void* itself, but just passes to pthread_join. *) ("pthread_join", special [__ "thread" []; __ "retval" [w]] @@ fun thread retval -> ThreadJoin {thread; ret_var = retval}); + ("pthread_once", special [__ "once_control" []; __ "init_routine" []] @@ fun once_control init_routine -> Once {once_control; init_routine}); ("pthread_kill", unknown [drop "thread" []; drop "sig" []]); ("pthread_equal", unknown [drop "t1" []; drop "t2" []]); ("pthread_cond_init", unknown [drop "cond" [w]; drop "attr" [r]]); @@ -520,6 +521,8 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("pthread_getspecific", unknown ~attrs:[InvalidateGlobals] [drop "key" []]); ("pthread_key_create", unknown [drop "key" [w]; drop "destructor" [s]]); ("pthread_key_delete", unknown [drop "key" [f]]); + ("pthread_barrier_init", special [__ "barrier" []; __ "attr" []; __ "count" []] @@ fun barrier attr count -> BarrierInit {barrier; attr; count}); + ("pthread_barrier_wait", special [__ "barrier" []] @@ fun barrier -> BarrierWait barrier); ("pthread_cancel", unknown [drop "thread" []]); ("pthread_testcancel", unknown []); ("pthread_setcancelstate", unknown [drop "state" []; drop "oldstate" [w]]); @@ -1298,7 +1301,7 @@ let is_safe_uncalled fn_name = List.exists (fun r -> Str.string_match r fn_name 0) kernel_safe_uncalled_regex -let unknown_desc f : LibraryDesc.t = +let unknown_desc f ~nowarn : LibraryDesc.t = let accs args : (LibraryDesc.Access.t * 'a list) list = [ ({ kind = Read; deep = true; }, if GobConfig.get_bool "sem.unknown_function.read.args" then args else []); ({ kind = Write; deep = true; }, if GobConfig.get_bool "sem.unknown_function.invalidate.args" then args else []); @@ -1314,7 +1317,7 @@ let unknown_desc f : LibraryDesc.t = [] in (* TODO: remove hack when all classify are migrated *) - if not (CilType.Varinfo.equal f dummyFunDec.svar) && not (use_special f.vname) then ( + if not nowarn && not (CilType.Varinfo.equal f dummyFunDec.svar) && not (use_special f.vname) then ( M.msg_final Error ~category:Imprecise ~tags:[Category Unsound] "Function definition missing"; M.error ~category:Imprecise ~tags:[Category Unsound] "Function definition missing for %s" f.vname ); @@ -1324,12 +1327,11 @@ let unknown_desc f : LibraryDesc.t = special = fun _ -> Unknown; } -let find f = +let find ?(nowarn=false) f = let name = f.vname in match Hashtbl.find_option (ResettableLazy.force activated_library_descs) name with | Some desc -> desc - | None -> unknown_desc f - + | None -> unknown_desc ~nowarn f let is_special fv = if use_special fv.vname then diff --git a/src/util/library/libraryFunctions.mli b/src/util/library/libraryFunctions.mli index 9a8e55a48a..7eb9c531fe 100644 --- a/src/util/library/libraryFunctions.mli +++ b/src/util/library/libraryFunctions.mli @@ -11,7 +11,7 @@ val use_special : string -> bool val is_safe_uncalled : string -> bool (** Find library function descriptor for {e special} function (as per {!is_special}). *) -val find: Cil.varinfo -> LibraryDesc.t +val find: ?nowarn:bool -> Cil.varinfo -> LibraryDesc.t val is_special: Cil.varinfo -> bool (** Check if function is treated specially. *) diff --git a/tests/regression/03-practical/35-base-mutex-macos.t b/tests/regression/03-practical/35-base-mutex-macos.t index 1d8a184d4c..929d03eb5b 100644 --- a/tests/regression/03-practical/35-base-mutex-macos.t +++ b/tests/regression/03-practical/35-base-mutex-macos.t @@ -1,4 +1,4 @@ - $ goblint --enable witness.yaml.enabled --disable witness.invariant.accessed --set pre.cppflags[+] -DGOBLINT_NO_PTHREAD_ONCE 35-base-mutex-macos.c + $ goblint --enable witness.yaml.enabled --disable witness.invariant.accessed 35-base-mutex-macos.c [Info][Deadcode] Logical lines of code (LLoC) summary: live: 2 dead: 0 diff --git a/tests/regression/04-mutex/01-simple_rc.t b/tests/regression/04-mutex/01-simple_rc.t index bd0bc0e161..f7b1131840 100644 --- a/tests/regression/04-mutex/01-simple_rc.t +++ b/tests/regression/04-mutex/01-simple_rc.t @@ -1,9 +1,9 @@ $ goblint --enable warn.deterministic 01-simple_rc.c 2>&1 | tee default-output.txt [Warning][Race] Memory location myglobal (race with conf. 110): (01-simple_rc.c:4:5-4:13) - write with [lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22) - write with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22) - read with [lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22) - read with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22) + write with [lock:{mutex1}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22) + write with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22) + read with [lock:{mutex1}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22) + read with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22) [Info][Race] Memory locations race summary: safe: 0 vulnerable: 0 @@ -18,13 +18,13 @@ $ diff default-output.txt full-output.txt 2,5c2,5 - < write with [lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22) - < write with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22) - < read with [lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22) - < read with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22) + < write with [lock:{mutex1}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22) + < write with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22) + < read with [lock:{mutex1}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22) + < read with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22) --- - > write with [mhp:{tid=[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]}, lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22) - > write with [mhp:{tid=[main]; created={[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]}}, lock:{mutex2}, thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22) - > read with [mhp:{tid=[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]}, lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22) - > read with [mhp:{tid=[main]; created={[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]}}, lock:{mutex2}, thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22) + > write with [mhp:{tid=[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]}, lock:{mutex1}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22) + > write with [mhp:{tid=[main]; created={[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]}}, lock:{mutex2}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22) + > read with [mhp:{tid=[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]}, lock:{mutex1}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:10:3-10:22) + > read with [mhp:{tid=[main]; created={[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]}}, lock:{mutex2}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & myglobal) (01-simple_rc.c:19:3-19:22) [1] diff --git a/tests/regression/04-mutex/49-type-invariants.t b/tests/regression/04-mutex/49-type-invariants.t index d757519b29..cd12bbd170 100644 --- a/tests/regression/04-mutex/49-type-invariants.t +++ b/tests/regression/04-mutex/49-type-invariants.t @@ -1,15 +1,15 @@ $ goblint --enable warn.deterministic --enable ana.race.direct-arithmetic --enable allglobs 49-type-invariants.c 2>&1 | tee default-output-1.txt [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (49-type-invariants.c:21:3-21:21) [Warning][Race] Memory location s.field (race with conf. 110): (49-type-invariants.c:8:10-8:11) - write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) - read with thread:[main, t_fun@49-type-invariants.c:20:3-20:40] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23) + write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) + read with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@49-type-invariants.c:20:3-20:40]] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 unsafe: 1 total memory locations: 2 [Success][Race] Memory location (struct S).field (safe): - write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) + write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 @@ -24,15 +24,15 @@ $ goblint --enable warn.deterministic --disable ana.race.direct-arithmetic --enable allglobs 49-type-invariants.c 2>&1 | tee default-output-2.txt [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (49-type-invariants.c:21:3-21:21) [Warning][Race] Memory location s.field (race with conf. 110): (49-type-invariants.c:8:10-8:11) - write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) - read with thread:[main, t_fun@49-type-invariants.c:20:3-20:40] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23) + write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) + read with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@49-type-invariants.c:20:3-20:40]] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 unsafe: 1 total memory locations: 2 [Success][Race] Memory location (struct S).field (safe): - write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) + write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 @@ -48,28 +48,28 @@ $ diff default-output-1.txt full-output-1.txt 3,4c3,4 - < write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) - < read with thread:[main, t_fun@49-type-invariants.c:20:3-20:40] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23) + < write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) + < read with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@49-type-invariants.c:20:3-20:40]] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23) --- - > write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) - > read with [mhp:{tid=[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}, thread:[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23) + > write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) + > read with [mhp:{tid=[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23) 11c11 - < write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) + < write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) --- - > write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) + > write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) [1] $ goblint --enable warn.deterministic --disable ana.race.direct-arithmetic --enable allglobs --enable dbg.full-output 49-type-invariants.c > full-output-2.txt 2>&1 $ diff default-output-2.txt full-output-2.txt 3,4c3,4 - < write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) - < read with thread:[main, t_fun@49-type-invariants.c:20:3-20:40] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23) + < write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) + < read with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@49-type-invariants.c:20:3-20:40]] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23) --- - > write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) - > read with [mhp:{tid=[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}, thread:[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23) + > write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) + > read with [mhp:{tid=[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23) 11c11 - < write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) + < write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) --- - > write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) + > write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) [1] diff --git a/tests/regression/04-mutex/77-type-nested-fields.t b/tests/regression/04-mutex/77-type-nested-fields.t index 15559cefec..7041b8e19c 100644 --- a/tests/regression/04-mutex/77-type-nested-fields.t +++ b/tests/regression/04-mutex/77-type-nested-fields.t @@ -2,15 +2,15 @@ [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (77-type-nested-fields.c:31:3-31:20) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (77-type-nested-fields.c:38:3-38:22) [Warning][Race] Memory location (struct T).s.field (race with conf. 100): - write with thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20) - write with [mhp:{created={[main, t_fun@77-type-nested-fields.c:37:3-37:40]}}, thread:[main]] (conf. 100) (exp: & tmp->s.field) (77-type-nested-fields.c:38:3-38:22) + write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20) + write with [mhp:{created={[main, t_fun@77-type-nested-fields.c:37:3-37:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->s.field) (77-type-nested-fields.c:38:3-38:22) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 unsafe: 1 total memory locations: 2 [Success][Race] Memory location (struct S).field (safe): - write with thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20) + write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 @@ -29,13 +29,13 @@ $ diff default-output.txt full-output.txt 4,5c4,5 - < write with thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20) - < write with [mhp:{created={[main, t_fun@77-type-nested-fields.c:37:3-37:40]}}, thread:[main]] (conf. 100) (exp: & tmp->s.field) (77-type-nested-fields.c:38:3-38:22) + < write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20) + < write with [mhp:{created={[main, t_fun@77-type-nested-fields.c:37:3-37:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->s.field) (77-type-nested-fields.c:38:3-38:22) --- - > write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]}, thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20) - > write with [mhp:{tid=[main]; created={[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]}}, thread:[main]] (conf. 100) (exp: & tmp->s.field) (77-type-nested-fields.c:38:3-38:22) + > write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20) + > write with [mhp:{tid=[main]; created={[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->s.field) (77-type-nested-fields.c:38:3-38:22) 12c12 - < write with thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20) + < write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20) --- - > write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]}, thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20) + > write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20) [1] diff --git a/tests/regression/04-mutex/79-type-nested-fields-deep1.t b/tests/regression/04-mutex/79-type-nested-fields-deep1.t index 680200aecd..857fa3aaf1 100644 --- a/tests/regression/04-mutex/79-type-nested-fields-deep1.t +++ b/tests/regression/04-mutex/79-type-nested-fields-deep1.t @@ -2,15 +2,15 @@ [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (79-type-nested-fields-deep1.c:36:3-36:20) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (79-type-nested-fields-deep1.c:43:3-43:24) [Warning][Race] Memory location (struct U).t.s.field (race with conf. 100): - write with thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20) - write with [mhp:{created={[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (79-type-nested-fields-deep1.c:43:3-43:24) + write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20) + write with [mhp:{created={[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (79-type-nested-fields-deep1.c:43:3-43:24) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 unsafe: 1 total memory locations: 2 [Success][Race] Memory location (struct S).field (safe): - write with thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20) + write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 @@ -29,13 +29,13 @@ $ diff default-output.txt full-output.txt 4,5c4,5 - < write with thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20) - < write with [mhp:{created={[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (79-type-nested-fields-deep1.c:43:3-43:24) + < write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20) + < write with [mhp:{created={[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (79-type-nested-fields-deep1.c:43:3-43:24) --- - > write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#⊤]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#⊤]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20) - > write with [mhp:{tid=[main]; created={[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#⊤]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (79-type-nested-fields-deep1.c:43:3-43:24) + > write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#⊤]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20) + > write with [mhp:{tid=[main]; created={[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (79-type-nested-fields-deep1.c:43:3-43:24) 12c12 - < write with thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20) + < write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20) --- - > write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#⊤]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#⊤]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20) + > write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#⊤]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20) [1] diff --git a/tests/regression/04-mutex/80-type-nested-fields-deep2.t b/tests/regression/04-mutex/80-type-nested-fields-deep2.t index 4a2811ccbd..dd4d6e90a8 100644 --- a/tests/regression/04-mutex/80-type-nested-fields-deep2.t +++ b/tests/regression/04-mutex/80-type-nested-fields-deep2.t @@ -2,15 +2,15 @@ [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (80-type-nested-fields-deep2.c:36:3-36:22) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (80-type-nested-fields-deep2.c:43:3-43:24) [Warning][Race] Memory location (struct U).t.s.field (race with conf. 100): - write with thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22) - write with [mhp:{created={[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (80-type-nested-fields-deep2.c:43:3-43:24) + write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40]] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22) + write with [mhp:{created={[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (80-type-nested-fields-deep2.c:43:3-43:24) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 unsafe: 1 total memory locations: 2 [Success][Race] Memory location (struct T).s.field (safe): - write with thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22) + write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40]] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 @@ -29,13 +29,13 @@ $ diff default-output.txt full-output.txt 4,5c4,5 - < write with thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22) - < write with [mhp:{created={[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (80-type-nested-fields-deep2.c:43:3-43:24) + < write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40]] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22) + < write with [mhp:{created={[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (80-type-nested-fields-deep2.c:43:3-43:24) --- - > write with [mhp:{tid=[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#⊤]}, thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#⊤]] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22) - > write with [mhp:{tid=[main]; created={[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#⊤]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (80-type-nested-fields-deep2.c:43:3-43:24) + > write with [mhp:{tid=[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#⊤]] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22) + > write with [mhp:{tid=[main]; created={[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (80-type-nested-fields-deep2.c:43:3-43:24) 12c12 - < write with thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22) + < write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40]] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22) --- - > write with [mhp:{tid=[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#⊤]}, thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#⊤]] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22) + > write with [mhp:{tid=[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#⊤]] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22) [1] diff --git a/tests/regression/04-mutex/84-distribute-fields-1.t b/tests/regression/04-mutex/84-distribute-fields-1.t index 0fd55dcb53..cf30127d7d 100644 --- a/tests/regression/04-mutex/84-distribute-fields-1.t +++ b/tests/regression/04-mutex/84-distribute-fields-1.t @@ -1,14 +1,14 @@ $ goblint --enable warn.deterministic --enable allglobs 84-distribute-fields-1.c 2>&1 | tee default-output.txt [Warning][Race] Memory location s.data (race with conf. 110): (84-distribute-fields-1.c:9:10-9:11) - write with thread:[main, t_fun@84-distribute-fields-1.c:18:3-18:40] (conf. 110) (exp: & s.data) (84-distribute-fields-1.c:12:3-12:13) - write with [mhp:{created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40]}}, thread:[main]] (conf. 110) (exp: & s) (84-distribute-fields-1.c:20:3-20:9) + write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@84-distribute-fields-1.c:18:3-18:40]] (conf. 110) (exp: & s.data) (84-distribute-fields-1.c:12:3-12:13) + write with [mhp:{created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & s) (84-distribute-fields-1.c:20:3-20:9) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 unsafe: 1 total memory locations: 2 [Success][Race] Memory location s (safe): (84-distribute-fields-1.c:9:10-9:11) - write with [mhp:{created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40]}}, thread:[main]] (conf. 110) (exp: & s) (84-distribute-fields-1.c:20:3-20:9) + write with [mhp:{created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & s) (84-distribute-fields-1.c:20:3-20:9) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 8 dead: 0 @@ -18,13 +18,13 @@ $ diff default-output.txt full-output.txt 2,3c2,3 - < write with thread:[main, t_fun@84-distribute-fields-1.c:18:3-18:40] (conf. 110) (exp: & s.data) (84-distribute-fields-1.c:12:3-12:13) - < write with [mhp:{created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40]}}, thread:[main]] (conf. 110) (exp: & s) (84-distribute-fields-1.c:20:3-20:9) + < write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@84-distribute-fields-1.c:18:3-18:40]] (conf. 110) (exp: & s.data) (84-distribute-fields-1.c:12:3-12:13) + < write with [mhp:{created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & s) (84-distribute-fields-1.c:20:3-20:9) --- - > write with [mhp:{tid=[main, t_fun@84-distribute-fields-1.c:18:3-18:40#⊤]}, thread:[main, t_fun@84-distribute-fields-1.c:18:3-18:40#⊤]] (conf. 110) (exp: & s.data) (84-distribute-fields-1.c:12:3-12:13) - > write with [mhp:{tid=[main]; created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40#⊤]}}, thread:[main]] (conf. 110) (exp: & s) (84-distribute-fields-1.c:20:3-20:9) + > write with [mhp:{tid=[main, t_fun@84-distribute-fields-1.c:18:3-18:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@84-distribute-fields-1.c:18:3-18:40#⊤]] (conf. 110) (exp: & s.data) (84-distribute-fields-1.c:12:3-12:13) + > write with [mhp:{tid=[main]; created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & s) (84-distribute-fields-1.c:20:3-20:9) 10c10 - < write with [mhp:{created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40]}}, thread:[main]] (conf. 110) (exp: & s) (84-distribute-fields-1.c:20:3-20:9) + < write with [mhp:{created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & s) (84-distribute-fields-1.c:20:3-20:9) --- - > write with [mhp:{tid=[main]; created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40#⊤]}}, thread:[main]] (conf. 110) (exp: & s) (84-distribute-fields-1.c:20:3-20:9) + > write with [mhp:{tid=[main]; created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & s) (84-distribute-fields-1.c:20:3-20:9) [1] diff --git a/tests/regression/04-mutex/85-distribute-fields-2.t b/tests/regression/04-mutex/85-distribute-fields-2.t index 7f8fb7c942..76ba6c759c 100644 --- a/tests/regression/04-mutex/85-distribute-fields-2.t +++ b/tests/regression/04-mutex/85-distribute-fields-2.t @@ -1,14 +1,14 @@ $ goblint --enable warn.deterministic --enable allglobs 85-distribute-fields-2.c 2>&1 | tee default-output.txt [Warning][Race] Memory location t.s.data (race with conf. 110): (85-distribute-fields-2.c:15:10-15:11) - write with thread:[main, t_fun@85-distribute-fields-2.c:24:3-24:40] (conf. 110) (exp: & t.s.data) (85-distribute-fields-2.c:18:3-18:15) - write with [mhp:{created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40]}}, thread:[main]] (conf. 110) (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11) + write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@85-distribute-fields-2.c:24:3-24:40]] (conf. 110) (exp: & t.s.data) (85-distribute-fields-2.c:18:3-18:15) + write with [mhp:{created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 unsafe: 1 total memory locations: 2 [Success][Race] Memory location t.s (safe): (85-distribute-fields-2.c:15:10-15:11) - write with [mhp:{created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40]}}, thread:[main]] (conf. 110) (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11) + write with [mhp:{created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 8 dead: 0 @@ -18,13 +18,13 @@ $ diff default-output.txt full-output.txt 2,3c2,3 - < write with thread:[main, t_fun@85-distribute-fields-2.c:24:3-24:40] (conf. 110) (exp: & t.s.data) (85-distribute-fields-2.c:18:3-18:15) - < write with [mhp:{created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40]}}, thread:[main]] (conf. 110) (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11) + < write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@85-distribute-fields-2.c:24:3-24:40]] (conf. 110) (exp: & t.s.data) (85-distribute-fields-2.c:18:3-18:15) + < write with [mhp:{created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11) --- - > write with [mhp:{tid=[main, t_fun@85-distribute-fields-2.c:24:3-24:40#⊤]}, thread:[main, t_fun@85-distribute-fields-2.c:24:3-24:40#⊤]] (conf. 110) (exp: & t.s.data) (85-distribute-fields-2.c:18:3-18:15) - > write with [mhp:{tid=[main]; created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40#⊤]}}, thread:[main]] (conf. 110) (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11) + > write with [mhp:{tid=[main, t_fun@85-distribute-fields-2.c:24:3-24:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@85-distribute-fields-2.c:24:3-24:40#⊤]] (conf. 110) (exp: & t.s.data) (85-distribute-fields-2.c:18:3-18:15) + > write with [mhp:{tid=[main]; created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11) 10c10 - < write with [mhp:{created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40]}}, thread:[main]] (conf. 110) (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11) + < write with [mhp:{created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11) --- - > write with [mhp:{tid=[main]; created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40#⊤]}}, thread:[main]] (conf. 110) (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11) + > write with [mhp:{tid=[main]; created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11) [1] diff --git a/tests/regression/04-mutex/86-distribute-fields-3.t b/tests/regression/04-mutex/86-distribute-fields-3.t index c5ebd6d28a..6819a98396 100644 --- a/tests/regression/04-mutex/86-distribute-fields-3.t +++ b/tests/regression/04-mutex/86-distribute-fields-3.t @@ -1,14 +1,14 @@ $ goblint --enable warn.deterministic --enable allglobs 86-distribute-fields-3.c 2>&1 | tee default-output.txt [Warning][Race] Memory location t.s.data (race with conf. 110): (86-distribute-fields-3.c:15:10-15:11) - write with thread:[main, t_fun@86-distribute-fields-3.c:24:3-24:40] (conf. 110) (exp: & t.s.data) (86-distribute-fields-3.c:18:3-18:15) - write with [mhp:{created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40]}}, thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) + write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@86-distribute-fields-3.c:24:3-24:40]] (conf. 110) (exp: & t.s.data) (86-distribute-fields-3.c:18:3-18:15) + write with [mhp:{created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 unsafe: 1 total memory locations: 2 [Success][Race] Memory location t (safe): (86-distribute-fields-3.c:15:10-15:11) - write with [mhp:{created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40]}}, thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) + write with [mhp:{created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 8 dead: 0 @@ -18,13 +18,13 @@ $ diff default-output.txt full-output.txt 2,3c2,3 - < write with thread:[main, t_fun@86-distribute-fields-3.c:24:3-24:40] (conf. 110) (exp: & t.s.data) (86-distribute-fields-3.c:18:3-18:15) - < write with [mhp:{created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40]}}, thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) + < write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@86-distribute-fields-3.c:24:3-24:40]] (conf. 110) (exp: & t.s.data) (86-distribute-fields-3.c:18:3-18:15) + < write with [mhp:{created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) --- - > write with [mhp:{tid=[main, t_fun@86-distribute-fields-3.c:24:3-24:40#⊤]}, thread:[main, t_fun@86-distribute-fields-3.c:24:3-24:40#⊤]] (conf. 110) (exp: & t.s.data) (86-distribute-fields-3.c:18:3-18:15) - > write with [mhp:{tid=[main]; created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40#⊤]}}, thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) + > write with [mhp:{tid=[main, t_fun@86-distribute-fields-3.c:24:3-24:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@86-distribute-fields-3.c:24:3-24:40#⊤]] (conf. 110) (exp: & t.s.data) (86-distribute-fields-3.c:18:3-18:15) + > write with [mhp:{tid=[main]; created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) 10c10 - < write with [mhp:{created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40]}}, thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) + < write with [mhp:{created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) --- - > write with [mhp:{tid=[main]; created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40#⊤]}}, thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) + > write with [mhp:{tid=[main]; created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) [1] diff --git a/tests/regression/04-mutex/87-distribute-fields-4.t b/tests/regression/04-mutex/87-distribute-fields-4.t index 2d3dfb6b7c..713bc79679 100644 --- a/tests/regression/04-mutex/87-distribute-fields-4.t +++ b/tests/regression/04-mutex/87-distribute-fields-4.t @@ -1,7 +1,7 @@ $ goblint --enable warn.deterministic --enable allglobs 87-distribute-fields-4.c 2>&1 | tee default-output.txt [Warning][Race] Memory location s (race with conf. 110): (87-distribute-fields-4.c:9:10-9:11) - write with thread:[main, t_fun@87-distribute-fields-4.c:19:3-19:40] (conf. 110) (exp: & s) (87-distribute-fields-4.c:13:3-13:9) - write with [mhp:{created={[main, t_fun@87-distribute-fields-4.c:19:3-19:40]}}, thread:[main]] (conf. 110) (exp: & s) (87-distribute-fields-4.c:21:3-21:9) + write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@87-distribute-fields-4.c:19:3-19:40]] (conf. 110) (exp: & s) (87-distribute-fields-4.c:13:3-13:9) + write with [mhp:{created={[main, t_fun@87-distribute-fields-4.c:19:3-19:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & s) (87-distribute-fields-4.c:21:3-21:9) [Info][Race] Memory locations race summary: safe: 0 vulnerable: 0 @@ -16,9 +16,9 @@ $ diff default-output.txt full-output.txt 2,3c2,3 - < write with thread:[main, t_fun@87-distribute-fields-4.c:19:3-19:40] (conf. 110) (exp: & s) (87-distribute-fields-4.c:13:3-13:9) - < write with [mhp:{created={[main, t_fun@87-distribute-fields-4.c:19:3-19:40]}}, thread:[main]] (conf. 110) (exp: & s) (87-distribute-fields-4.c:21:3-21:9) + < write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@87-distribute-fields-4.c:19:3-19:40]] (conf. 110) (exp: & s) (87-distribute-fields-4.c:13:3-13:9) + < write with [mhp:{created={[main, t_fun@87-distribute-fields-4.c:19:3-19:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & s) (87-distribute-fields-4.c:21:3-21:9) --- - > write with [mhp:{tid=[main, t_fun@87-distribute-fields-4.c:19:3-19:40#⊤]}, thread:[main, t_fun@87-distribute-fields-4.c:19:3-19:40#⊤]] (conf. 110) (exp: & s) (87-distribute-fields-4.c:13:3-13:9) - > write with [mhp:{tid=[main]; created={[main, t_fun@87-distribute-fields-4.c:19:3-19:40#⊤]}}, thread:[main]] (conf. 110) (exp: & s) (87-distribute-fields-4.c:21:3-21:9) + > write with [mhp:{tid=[main, t_fun@87-distribute-fields-4.c:19:3-19:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@87-distribute-fields-4.c:19:3-19:40#⊤]] (conf. 110) (exp: & s) (87-distribute-fields-4.c:13:3-13:9) + > write with [mhp:{tid=[main]; created={[main, t_fun@87-distribute-fields-4.c:19:3-19:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & s) (87-distribute-fields-4.c:21:3-21:9) [1] diff --git a/tests/regression/04-mutex/88-distribute-fields-5.t b/tests/regression/04-mutex/88-distribute-fields-5.t index 0afdc729ef..eba8db4d5a 100644 --- a/tests/regression/04-mutex/88-distribute-fields-5.t +++ b/tests/regression/04-mutex/88-distribute-fields-5.t @@ -1,7 +1,7 @@ $ goblint --enable warn.deterministic --enable allglobs 88-distribute-fields-5.c 2>&1 | tee default-output.txt [Warning][Race] Memory location t.s (race with conf. 110): (88-distribute-fields-5.c:15:10-15:11) - write with thread:[main, t_fun@88-distribute-fields-5.c:25:3-25:40] (conf. 110) (exp: & t.s) (88-distribute-fields-5.c:19:3-19:11) - write with [mhp:{created={[main, t_fun@88-distribute-fields-5.c:25:3-25:40]}}, thread:[main]] (conf. 110) (exp: & t.s) (88-distribute-fields-5.c:27:3-27:11) + write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@88-distribute-fields-5.c:25:3-25:40]] (conf. 110) (exp: & t.s) (88-distribute-fields-5.c:19:3-19:11) + write with [mhp:{created={[main, t_fun@88-distribute-fields-5.c:25:3-25:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & t.s) (88-distribute-fields-5.c:27:3-27:11) [Info][Race] Memory locations race summary: safe: 0 vulnerable: 0 @@ -16,9 +16,9 @@ $ diff default-output.txt full-output.txt 2,3c2,3 - < write with thread:[main, t_fun@88-distribute-fields-5.c:25:3-25:40] (conf. 110) (exp: & t.s) (88-distribute-fields-5.c:19:3-19:11) - < write with [mhp:{created={[main, t_fun@88-distribute-fields-5.c:25:3-25:40]}}, thread:[main]] (conf. 110) (exp: & t.s) (88-distribute-fields-5.c:27:3-27:11) + < write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@88-distribute-fields-5.c:25:3-25:40]] (conf. 110) (exp: & t.s) (88-distribute-fields-5.c:19:3-19:11) + < write with [mhp:{created={[main, t_fun@88-distribute-fields-5.c:25:3-25:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & t.s) (88-distribute-fields-5.c:27:3-27:11) --- - > write with [mhp:{tid=[main, t_fun@88-distribute-fields-5.c:25:3-25:40#⊤]}, thread:[main, t_fun@88-distribute-fields-5.c:25:3-25:40#⊤]] (conf. 110) (exp: & t.s) (88-distribute-fields-5.c:19:3-19:11) - > write with [mhp:{tid=[main]; created={[main, t_fun@88-distribute-fields-5.c:25:3-25:40#⊤]}}, thread:[main]] (conf. 110) (exp: & t.s) (88-distribute-fields-5.c:27:3-27:11) + > write with [mhp:{tid=[main, t_fun@88-distribute-fields-5.c:25:3-25:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@88-distribute-fields-5.c:25:3-25:40#⊤]] (conf. 110) (exp: & t.s) (88-distribute-fields-5.c:19:3-19:11) + > write with [mhp:{tid=[main]; created={[main, t_fun@88-distribute-fields-5.c:25:3-25:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & t.s) (88-distribute-fields-5.c:27:3-27:11) [1] diff --git a/tests/regression/04-mutex/89-distribute-fields-6.t b/tests/regression/04-mutex/89-distribute-fields-6.t index 20533099de..0bad7aba3f 100644 --- a/tests/regression/04-mutex/89-distribute-fields-6.t +++ b/tests/regression/04-mutex/89-distribute-fields-6.t @@ -1,7 +1,7 @@ $ goblint --enable warn.deterministic --enable allglobs 89-distribute-fields-6.c 2>&1 | tee default-output.txt [Warning][Race] Memory location t (race with conf. 110): (89-distribute-fields-6.c:15:10-15:11) - write with thread:[main, t_fun@89-distribute-fields-6.c:25:3-25:40] (conf. 110) (exp: & t) (89-distribute-fields-6.c:19:3-19:9) - write with [mhp:{created={[main, t_fun@89-distribute-fields-6.c:25:3-25:40]}}, thread:[main]] (conf. 110) (exp: & t) (89-distribute-fields-6.c:27:3-27:9) + write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@89-distribute-fields-6.c:25:3-25:40]] (conf. 110) (exp: & t) (89-distribute-fields-6.c:19:3-19:9) + write with [mhp:{created={[main, t_fun@89-distribute-fields-6.c:25:3-25:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & t) (89-distribute-fields-6.c:27:3-27:9) [Info][Race] Memory locations race summary: safe: 0 vulnerable: 0 @@ -16,9 +16,9 @@ $ diff default-output.txt full-output.txt 2,3c2,3 - < write with thread:[main, t_fun@89-distribute-fields-6.c:25:3-25:40] (conf. 110) (exp: & t) (89-distribute-fields-6.c:19:3-19:9) - < write with [mhp:{created={[main, t_fun@89-distribute-fields-6.c:25:3-25:40]}}, thread:[main]] (conf. 110) (exp: & t) (89-distribute-fields-6.c:27:3-27:9) + < write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@89-distribute-fields-6.c:25:3-25:40]] (conf. 110) (exp: & t) (89-distribute-fields-6.c:19:3-19:9) + < write with [mhp:{created={[main, t_fun@89-distribute-fields-6.c:25:3-25:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & t) (89-distribute-fields-6.c:27:3-27:9) --- - > write with [mhp:{tid=[main, t_fun@89-distribute-fields-6.c:25:3-25:40#⊤]}, thread:[main, t_fun@89-distribute-fields-6.c:25:3-25:40#⊤]] (conf. 110) (exp: & t) (89-distribute-fields-6.c:19:3-19:9) - > write with [mhp:{tid=[main]; created={[main, t_fun@89-distribute-fields-6.c:25:3-25:40#⊤]}}, thread:[main]] (conf. 110) (exp: & t) (89-distribute-fields-6.c:27:3-27:9) + > write with [mhp:{tid=[main, t_fun@89-distribute-fields-6.c:25:3-25:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@89-distribute-fields-6.c:25:3-25:40#⊤]] (conf. 110) (exp: & t) (89-distribute-fields-6.c:19:3-19:9) + > write with [mhp:{tid=[main]; created={[main, t_fun@89-distribute-fields-6.c:25:3-25:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & t) (89-distribute-fields-6.c:27:3-27:9) [1] diff --git a/tests/regression/04-mutex/90-distribute-fields-type-1.t b/tests/regression/04-mutex/90-distribute-fields-type-1.t index 1a5c739e9c..cc40a3cf4c 100644 --- a/tests/regression/04-mutex/90-distribute-fields-type-1.t +++ b/tests/regression/04-mutex/90-distribute-fields-type-1.t @@ -2,17 +2,17 @@ [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (90-distribute-fields-type-1.c:31:3-31:20) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (90-distribute-fields-type-1.c:39:3-39:17) [Warning][Race] Memory location (struct T).s.field (race with conf. 100): - write with thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20) - write with [mhp:{created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17) + write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40]] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20) + write with [mhp:{created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17) [Info][Race] Memory locations race summary: safe: 2 vulnerable: 0 unsafe: 1 total memory locations: 3 [Success][Race] Memory location (struct S).field (safe): - write with thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20) + write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40]] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20) [Success][Race] Memory location (struct T).s (safe): - write with [mhp:{created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17) + write with [mhp:{created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 @@ -31,17 +31,17 @@ $ diff default-output.txt full-output.txt 4,5c4,5 - < write with thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20) - < write with [mhp:{created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17) + < write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40]] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20) + < write with [mhp:{created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17) --- - > write with [mhp:{tid=[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]}, thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20) - > write with [mhp:{tid=[main]; created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17) + > write with [mhp:{tid=[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20) + > write with [mhp:{tid=[main]; created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17) 12c12 - < write with thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20) + < write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40]] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20) --- - > write with [mhp:{tid=[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]}, thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20) + > write with [mhp:{tid=[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20) 14c14 - < write with [mhp:{created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17) + < write with [mhp:{created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17) --- - > write with [mhp:{tid=[main]; created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17) + > write with [mhp:{tid=[main]; created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17) [1] diff --git a/tests/regression/04-mutex/91-distribute-fields-type-2.t b/tests/regression/04-mutex/91-distribute-fields-type-2.t index e22b21d2bd..e3a861adc0 100644 --- a/tests/regression/04-mutex/91-distribute-fields-type-2.t +++ b/tests/regression/04-mutex/91-distribute-fields-type-2.t @@ -2,17 +2,17 @@ [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (91-distribute-fields-type-2.c:32:3-32:17) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (91-distribute-fields-type-2.c:40:3-40:17) [Warning][Race] Memory location (struct T).s (race with conf. 100): - write with thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17) - write with [mhp:{created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17) + write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17) + write with [mhp:{created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17) [Info][Race] Memory locations race summary: safe: 2 vulnerable: 0 unsafe: 1 total memory locations: 3 [Success][Race] Memory location (struct S) (safe): - write with thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17) + write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17) [Success][Race] Memory location (struct T) (safe): - write with [mhp:{created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17) + write with [mhp:{created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 @@ -31,17 +31,17 @@ $ diff default-output.txt full-output.txt 4,5c4,5 - < write with thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17) - < write with [mhp:{created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17) + < write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17) + < write with [mhp:{created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17) --- - > write with [mhp:{tid=[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]}, thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17) - > write with [mhp:{tid=[main]; created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17) + > write with [mhp:{tid=[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17) + > write with [mhp:{tid=[main]; created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17) 12c12 - < write with thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17) + < write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17) --- - > write with [mhp:{tid=[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]}, thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17) + > write with [mhp:{tid=[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17) 14c14 - < write with [mhp:{created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17) + < write with [mhp:{created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17) --- - > write with [mhp:{tid=[main]; created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17) + > write with [mhp:{tid=[main]; created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17) [1] diff --git a/tests/regression/04-mutex/92-distribute-fields-type-deep.t b/tests/regression/04-mutex/92-distribute-fields-type-deep.t index d754ded21b..a0663678dd 100644 --- a/tests/regression/04-mutex/92-distribute-fields-type-deep.t +++ b/tests/regression/04-mutex/92-distribute-fields-type-deep.t @@ -2,17 +2,17 @@ [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (92-distribute-fields-type-deep.c:36:3-36:20) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (92-distribute-fields-type-deep.c:44:3-44:17) [Warning][Race] Memory location (struct U).t.s.field (race with conf. 100): - write with thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20) - write with [mhp:{created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17) + write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20) + write with [mhp:{created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17) [Info][Race] Memory locations race summary: safe: 2 vulnerable: 0 unsafe: 1 total memory locations: 3 [Success][Race] Memory location (struct S).field (safe): - write with thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20) + write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20) [Success][Race] Memory location (struct U).t (safe): - write with [mhp:{created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17) + write with [mhp:{created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 @@ -31,17 +31,17 @@ $ diff default-output.txt full-output.txt 4,5c4,5 - < write with thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20) - < write with [mhp:{created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17) + < write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20) + < write with [mhp:{created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17) --- - > write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]}, thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20) - > write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17) + > write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20) + > write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17) 12c12 - < write with thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20) + < write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20) --- - > write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]}, thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20) + > write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20) 14c14 - < write with [mhp:{created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17) + < write with [mhp:{created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17) --- - > write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17) + > write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17) [1] diff --git a/tests/regression/04-mutex/93-distribute-fields-type-global.t b/tests/regression/04-mutex/93-distribute-fields-type-global.t index 7e0dc61a3c..c5ca112278 100644 --- a/tests/regression/04-mutex/93-distribute-fields-type-global.t +++ b/tests/regression/04-mutex/93-distribute-fields-type-global.t @@ -1,17 +1,17 @@ $ goblint --enable warn.deterministic --enable allglobs 93-distribute-fields-type-global.c 2>&1 | tee default-output.txt [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (93-distribute-fields-type-global.c:13:3-13:29) [Warning][Race] Memory location s.field (race with conf. 110): (93-distribute-fields-type-global.c:8:10-8:11) - read with thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29) - write with [mhp:{created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9) + read with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40]] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29) + write with [mhp:{created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9) [Info][Race] Memory locations race summary: safe: 2 vulnerable: 0 unsafe: 1 total memory locations: 3 [Success][Race] Memory location (struct S).field (safe): - read with thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29) + read with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40]] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29) [Success][Race] Memory location s (safe): (93-distribute-fields-type-global.c:8:10-8:11) - write with [mhp:{created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9) + write with [mhp:{created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 @@ -27,17 +27,17 @@ $ diff default-output.txt full-output.txt 3,4c3,4 - < read with thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29) - < write with [mhp:{created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9) + < read with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40]] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29) + < write with [mhp:{created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9) --- - > read with [mhp:{tid=[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]}, thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29) - > write with [mhp:{tid=[main]; created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9) + > read with [mhp:{tid=[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29) + > write with [mhp:{tid=[main]; created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9) 11c11 - < read with thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29) + < read with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40]] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29) --- - > read with [mhp:{tid=[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]}, thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29) + > read with [mhp:{tid=[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29) 13c13 - < write with [mhp:{created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9) + < write with [mhp:{created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9) --- - > write with [mhp:{tid=[main]; created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9) + > write with [mhp:{tid=[main]; created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9) [1] diff --git a/tests/regression/06-symbeq/14-list_entry_rc.t b/tests/regression/06-symbeq/14-list_entry_rc.t index 0e5ec3ce9f..a94e910a9d 100644 --- a/tests/regression/06-symbeq/14-list_entry_rc.t +++ b/tests/regression/06-symbeq/14-list_entry_rc.t @@ -6,15 +6,15 @@ dead: 0 total lines: 23 [Warning][Race] Memory location (alloc@sid:$SID@tid:[main])[?].datum (race with conf. 110): (14-list_entry_rc.c:41:3-41:35) - write with thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) - write with [mhp:{created={[main, t_fun@14-list_entry_rc.c:45:3-45:40]}}, thread:[main]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) - read with thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) - read with [mhp:{created={[main, t_fun@14-list_entry_rc.c:45:3-45:40]}}, thread:[main]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) + write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) + write with [mhp:{created={[main, t_fun@14-list_entry_rc.c:45:3-45:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) + read with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) + read with [mhp:{created={[main, t_fun@14-list_entry_rc.c:45:3-45:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) [Info][Race] Memory locations race summary: - safe: 1 + safe: 2 vulnerable: 0 unsafe: 1 - total memory locations: 2 + total memory locations: 3 $ goblint --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --enable dbg.full-output 14-list_entry_rc.c 2>&1 | sed -r 's/sid:[0-9]+/sid:$SID/' > full-output.txt @@ -25,14 +25,14 @@ > [Warning][Unknown] unlocking mutex ((alloc@sid:$SID@tid:[main](#top))[def_exc:1].mutex) which may not be held (14-list_entry_rc.c:28:3-28:34) 7,11c7,11 < [Warning][Race] Memory location (alloc@sid:$SID@tid:[main])[?].datum (race with conf. 110): (14-list_entry_rc.c:41:3-41:35) - < write with thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) - < write with [mhp:{created={[main, t_fun@14-list_entry_rc.c:45:3-45:40]}}, thread:[main]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) - < read with thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) - < read with [mhp:{created={[main, t_fun@14-list_entry_rc.c:45:3-45:40]}}, thread:[main]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) + < write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) + < write with [mhp:{created={[main, t_fun@14-list_entry_rc.c:45:3-45:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) + < read with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) + < read with [mhp:{created={[main, t_fun@14-list_entry_rc.c:45:3-45:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) --- > [Warning][Race] Memory location (alloc@sid:$SID@tid:[main](#top))[?].datum (race with conf. 110): (14-list_entry_rc.c:41:3-41:35) - > write with [mhp:{tid=[main, t_fun@14-list_entry_rc.c:45:3-45:40#⊤]}, thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40#⊤]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) - > write with [mhp:{tid=[main]; created={[main, t_fun@14-list_entry_rc.c:45:3-45:40#⊤]}}, thread:[main]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) - > read with [mhp:{tid=[main, t_fun@14-list_entry_rc.c:45:3-45:40#⊤]}, thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40#⊤]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) - > read with [mhp:{tid=[main]; created={[main, t_fun@14-list_entry_rc.c:45:3-45:40#⊤]}}, thread:[main]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) + > write with [mhp:{tid=[main, t_fun@14-list_entry_rc.c:45:3-45:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40#⊤]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) + > write with [mhp:{tid=[main]; created={[main, t_fun@14-list_entry_rc.c:45:3-45:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) + > read with [mhp:{tid=[main, t_fun@14-list_entry_rc.c:45:3-45:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40#⊤]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) + > read with [mhp:{tid=[main]; created={[main, t_fun@14-list_entry_rc.c:45:3-45:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13) [1] diff --git a/tests/regression/06-symbeq/16-type_rc.t b/tests/regression/06-symbeq/16-type_rc.t index a5f977008d..703b73e0d0 100644 --- a/tests/regression/06-symbeq/16-type_rc.t +++ b/tests/regression/06-symbeq/16-type_rc.t @@ -6,8 +6,8 @@ Disable info messages because race summary contains (safe) memory location count [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:33:3-33:16) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:36:3-36:9) [Warning][Race] Memory location (struct s).datum (race with conf. 100): - write with thread:[main, t_fun@16-type_rc.c:35:3-35:37] (conf. 100) (exp: & s->datum) (16-type_rc.c:21:3-21:15) - write with [mhp:{created={[main, t_fun@16-type_rc.c:35:3-35:37]}}, thread:[main]] (conf. 100) (exp: & *d) (16-type_rc.c:36:3-36:9) + write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@16-type_rc.c:35:3-35:37]] (conf. 100) (exp: & s->datum) (16-type_rc.c:21:3-21:15) + write with [mhp:{created={[main, t_fun@16-type_rc.c:35:3-35:37]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & *d) (16-type_rc.c:36:3-36:9) [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:20:12-20:24) [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:31:3-31:14) [Error][Imprecise][Unsound] Function definition missing @@ -18,7 +18,7 @@ Disable info messages because race summary contains (safe) memory location count [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:33:3-33:16) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:36:3-36:9) [Success][Race] Memory location (struct s).datum (safe): - write with thread:[main, t_fun@16-type_rc.c:35:3-35:37] (conf. 100) (exp: & s->datum) (16-type_rc.c:21:3-21:15) + write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@16-type_rc.c:35:3-35:37]] (conf. 100) (exp: & s->datum) (16-type_rc.c:21:3-21:15) [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:20:12-20:24) [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:31:3-31:14) [Error][Imprecise][Unsound] Function definition missing @@ -27,18 +27,18 @@ Disable info messages because race summary contains (safe) memory location count $ diff default-output-1.txt full-output-1.txt 6,7c6,7 - < write with thread:[main, t_fun@16-type_rc.c:35:3-35:37] (conf. 100) (exp: & s->datum) (16-type_rc.c:21:3-21:15) - < write with [mhp:{created={[main, t_fun@16-type_rc.c:35:3-35:37]}}, thread:[main]] (conf. 100) (exp: & *d) (16-type_rc.c:36:3-36:9) + < write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@16-type_rc.c:35:3-35:37]] (conf. 100) (exp: & s->datum) (16-type_rc.c:21:3-21:15) + < write with [mhp:{created={[main, t_fun@16-type_rc.c:35:3-35:37]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & *d) (16-type_rc.c:36:3-36:9) --- - > write with [mhp:{tid=[main, t_fun@16-type_rc.c:35:3-35:37#⊤]}, thread:[main, t_fun@16-type_rc.c:35:3-35:37#⊤]] (conf. 100) (exp: & s->datum) (16-type_rc.c:21:3-21:15) - > write with [mhp:{tid=[main]; created={[main, t_fun@16-type_rc.c:35:3-35:37#⊤]}}, thread:[main]] (conf. 100) (exp: & *d) (16-type_rc.c:36:3-36:9) + > write with [mhp:{tid=[main, t_fun@16-type_rc.c:35:3-35:37#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@16-type_rc.c:35:3-35:37#⊤]] (conf. 100) (exp: & s->datum) (16-type_rc.c:21:3-21:15) + > write with [mhp:{tid=[main]; created={[main, t_fun@16-type_rc.c:35:3-35:37#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & *d) (16-type_rc.c:36:3-36:9) [1] $ goblint --enable warn.deterministic --disable warn.info --disable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --enable allglobs --enable dbg.full-output 16-type_rc.c > full-output-2.txt 2>&1 $ diff default-output-2.txt full-output-2.txt 6c6 - < write with thread:[main, t_fun@16-type_rc.c:35:3-35:37] (conf. 100) (exp: & s->datum) (16-type_rc.c:21:3-21:15) + < write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@16-type_rc.c:35:3-35:37]] (conf. 100) (exp: & s->datum) (16-type_rc.c:21:3-21:15) --- - > write with [mhp:{tid=[main, t_fun@16-type_rc.c:35:3-35:37#⊤]}, thread:[main, t_fun@16-type_rc.c:35:3-35:37#⊤]] (conf. 100) (exp: & s->datum) (16-type_rc.c:21:3-21:15) + > write with [mhp:{tid=[main, t_fun@16-type_rc.c:35:3-35:37#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@16-type_rc.c:35:3-35:37#⊤]] (conf. 100) (exp: & s->datum) (16-type_rc.c:21:3-21:15) [1] diff --git a/tests/regression/06-symbeq/21-mult_accs_rc.t b/tests/regression/06-symbeq/21-mult_accs_rc.t index 2eacd0382e..3b1c54990e 100644 --- a/tests/regression/06-symbeq/21-mult_accs_rc.t +++ b/tests/regression/06-symbeq/21-mult_accs_rc.t @@ -8,8 +8,8 @@ Disable info messages because race summary contains (safe) memory location count [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:29:3-29:15) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:34:3-34:9) [Warning][Race] Memory location (struct s).data (race with conf. 100): - write with thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37] (conf. 100) (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14) - write with [symblock:{p-lock:*.mutex}, mhp:{created={[main, t_fun@21-mult_accs_rc.c:31:3-31:37]}}, thread:[main]] (conf. 100) (exp: & *d) (21-mult_accs_rc.c:34:3-34:9) + write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37]] (conf. 100) (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14) + write with [symblock:{p-lock:*.mutex}, mhp:{created={[main, t_fun@21-mult_accs_rc.c:31:3-31:37]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & *d) (21-mult_accs_rc.c:34:3-34:9) [Warning][Unknown] locking NULL mutex (21-mult_accs_rc.c:14:3-14:32) [Warning][Unknown] unlocking NULL mutex (21-mult_accs_rc.c:17:3-17:34) [Warning][Unknown] unlocking unknown mutex which may not be held (21-mult_accs_rc.c:17:3-17:34) @@ -29,7 +29,7 @@ Disable info messages because race summary contains (safe) memory location count [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:29:3-29:15) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:34:3-34:9) [Success][Race] Memory location (struct s).data (safe): - write with thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37] (conf. 100) (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14) + write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37]] (conf. 100) (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14) [Warning][Unknown] locking NULL mutex (21-mult_accs_rc.c:14:3-14:32) [Warning][Unknown] unlocking NULL mutex (21-mult_accs_rc.c:17:3-17:34) [Warning][Unknown] unlocking unknown mutex which may not be held (21-mult_accs_rc.c:17:3-17:34) @@ -45,18 +45,18 @@ Disable info messages because race summary contains (safe) memory location count $ diff default-output-1.txt full-output-1.txt 8,9c8,9 - < write with thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37] (conf. 100) (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14) - < write with [symblock:{p-lock:*.mutex}, mhp:{created={[main, t_fun@21-mult_accs_rc.c:31:3-31:37]}}, thread:[main]] (conf. 100) (exp: & *d) (21-mult_accs_rc.c:34:3-34:9) + < write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37]] (conf. 100) (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14) + < write with [symblock:{p-lock:*.mutex}, mhp:{created={[main, t_fun@21-mult_accs_rc.c:31:3-31:37]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & *d) (21-mult_accs_rc.c:34:3-34:9) --- - > write with [mhp:{tid=[main, t_fun@21-mult_accs_rc.c:31:3-31:37#⊤]}, thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37#⊤]] (conf. 100) (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14) - > write with [symblock:{p-lock:*.mutex}, mhp:{tid=[main]; created={[main, t_fun@21-mult_accs_rc.c:31:3-31:37#⊤]}}, thread:[main]] (conf. 100) (exp: & *d) (21-mult_accs_rc.c:34:3-34:9) + > write with [mhp:{tid=[main, t_fun@21-mult_accs_rc.c:31:3-31:37#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37#⊤]] (conf. 100) (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14) + > write with [symblock:{p-lock:*.mutex}, mhp:{tid=[main]; created={[main, t_fun@21-mult_accs_rc.c:31:3-31:37#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100) (exp: & *d) (21-mult_accs_rc.c:34:3-34:9) [1] $ goblint --enable warn.deterministic --disable warn.info --disable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --enable allglobs --enable dbg.full-output 21-mult_accs_rc.c > full-output-2.txt 2>&1 $ diff default-output-2.txt full-output-2.txt 8c8 - < write with thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37] (conf. 100) (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14) + < write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37]] (conf. 100) (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14) --- - > write with [mhp:{tid=[main, t_fun@21-mult_accs_rc.c:31:3-31:37#⊤]}, thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37#⊤]] (conf. 100) (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14) + > write with [mhp:{tid=[main, t_fun@21-mult_accs_rc.c:31:3-31:37#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37#⊤]] (conf. 100) (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14) [1] diff --git a/tests/regression/13-privatized/63-access-threadspawn-lval.t b/tests/regression/13-privatized/63-access-threadspawn-lval.t index 313459637c..d0d7f90bee 100644 --- a/tests/regression/13-privatized/63-access-threadspawn-lval.t +++ b/tests/regression/13-privatized/63-access-threadspawn-lval.t @@ -12,10 +12,11 @@ Should have (safe) write accesses to id1 and id2: dead: 0 total lines: 13 [Success][Race] Memory location id1 (safe): (63-access-threadspawn-lval.c:4:11-4:14) - write with [multi:false, thread:[main]] (conf. 110) (exp: & *((pthread_t * __restrict )(& id1))) (63-access-threadspawn-lval.c:27:3-27:37) + write with [threadflag:(MT mode:Singlethreaded, bool:false), thread:[main]] (conf. 110) (exp: (pthread_t * __restrict )(& id1)) (63-access-threadspawn-lval.c:27:3-27:37) + write with [threadflag:(MT mode:Singlethreaded, bool:false), thread:[main]] (conf. 110) (exp: & *((pthread_t * __restrict )(& id1))) (63-access-threadspawn-lval.c:27:3-27:37) [Success][Race] Memory location id2 (safe): (63-access-threadspawn-lval.c:5:11-5:14) - write with [mhp:{created={[main, f@63-access-threadspawn-lval.c:27:3-27:37]}}, thread:[main]] (conf. 110) (exp: (pthread_t * __restrict )(& id2)) (63-access-threadspawn-lval.c:28:3-28:37) - write with [mhp:{created={[main, f@63-access-threadspawn-lval.c:27:3-27:37]}}, thread:[main]] (conf. 110) (exp: & *((pthread_t * __restrict )(& id2))) (63-access-threadspawn-lval.c:28:3-28:37) + write with [mhp:{created={[main, f@63-access-threadspawn-lval.c:27:3-27:37]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: (pthread_t * __restrict )(& id2)) (63-access-threadspawn-lval.c:28:3-28:37) + write with [mhp:{created={[main, f@63-access-threadspawn-lval.c:27:3-27:37]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & *((pthread_t * __restrict )(& id2))) (63-access-threadspawn-lval.c:28:3-28:37) [Info][Race] Memory locations race summary: safe: 2 vulnerable: 0 diff --git a/tests/regression/13-privatized/64-access-invalidate.t b/tests/regression/13-privatized/64-access-invalidate.t index 28227ec475..165fbe9aea 100644 --- a/tests/regression/13-privatized/64-access-invalidate.t +++ b/tests/regression/13-privatized/64-access-invalidate.t @@ -12,7 +12,8 @@ Should have (safe) write access to id1 and magic2 invalidate to A: dead: 0 total lines: 10 [Success][Race] Memory location id (safe): (64-access-invalidate.c:4:11-4:13) - write with [multi:false, thread:[main]] (conf. 110) (exp: & *((pthread_t * __restrict )(& id))) (64-access-invalidate.c:21:3-21:36) + write with [threadflag:(MT mode:Singlethreaded, bool:false), thread:[main]] (conf. 110) (exp: (pthread_t * __restrict )(& id)) (64-access-invalidate.c:21:3-21:36) + write with [threadflag:(MT mode:Singlethreaded, bool:false), thread:[main]] (conf. 110) (exp: & *((pthread_t * __restrict )(& id))) (64-access-invalidate.c:21:3-21:36) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 diff --git a/tests/regression/29-svcomp/16-atomic_priv.t b/tests/regression/29-svcomp/16-atomic_priv.t index 1662f881b7..04fb1994a6 100644 --- a/tests/regression/29-svcomp/16-atomic_priv.t +++ b/tests/regression/29-svcomp/16-atomic_priv.t @@ -9,9 +9,9 @@ dead: 0 total lines: 17 [Warning][Race] Memory location myglobal (race with conf. 110): (16-atomic_priv.c:8:5-8:17) - write with [lock:{[__VERIFIER_atomic]}, thread:[main, t_fun@16-atomic_priv.c:23:3-23:40]] (conf. 110) (exp: & myglobal) (16-atomic_priv.c:13:3-13:13) - write with [lock:{[__VERIFIER_atomic]}, thread:[main, t_fun@16-atomic_priv.c:23:3-23:40]] (conf. 110) (exp: & myglobal) (16-atomic_priv.c:15:3-15:13) - read with [mhp:{created={[main, t_fun@16-atomic_priv.c:23:3-23:40]}}, thread:[main]] (conf. 110) (exp: & myglobal) (16-atomic_priv.c:24:3-24:33) + write with [lock:{[__VERIFIER_atomic]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@16-atomic_priv.c:23:3-23:40]] (conf. 110) (exp: & myglobal) (16-atomic_priv.c:13:3-13:13) + write with [lock:{[__VERIFIER_atomic]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@16-atomic_priv.c:23:3-23:40]] (conf. 110) (exp: & myglobal) (16-atomic_priv.c:15:3-15:13) + read with [mhp:{created={[main, t_fun@16-atomic_priv.c:23:3-23:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & myglobal) (16-atomic_priv.c:24:3-24:33) [Info][Witness] witness generation summary: location invariants: 0 loop invariants: 0 @@ -63,9 +63,9 @@ Non-atomic privatization: dead: 0 total lines: 17 [Warning][Race] Memory location myglobal (race with conf. 110): (16-atomic_priv.c:8:5-8:17) - write with [lock:{[__VERIFIER_atomic]}, thread:[main, t_fun@16-atomic_priv.c:23:3-23:40]] (conf. 110) (exp: & myglobal) (16-atomic_priv.c:13:3-13:13) - write with [lock:{[__VERIFIER_atomic]}, thread:[main, t_fun@16-atomic_priv.c:23:3-23:40]] (conf. 110) (exp: & myglobal) (16-atomic_priv.c:15:3-15:13) - read with [mhp:{created={[main, t_fun@16-atomic_priv.c:23:3-23:40]}}, thread:[main]] (conf. 110) (exp: & myglobal) (16-atomic_priv.c:24:3-24:33) + write with [lock:{[__VERIFIER_atomic]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@16-atomic_priv.c:23:3-23:40]] (conf. 110) (exp: & myglobal) (16-atomic_priv.c:13:3-13:13) + write with [lock:{[__VERIFIER_atomic]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@16-atomic_priv.c:23:3-23:40]] (conf. 110) (exp: & myglobal) (16-atomic_priv.c:15:3-15:13) + read with [mhp:{created={[main, t_fun@16-atomic_priv.c:23:3-23:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & myglobal) (16-atomic_priv.c:24:3-24:33) [Info][Witness] witness generation summary: location invariants: 0 loop invariants: 0 diff --git a/tests/regression/36-apron/12-traces-min-rpb1.t b/tests/regression/36-apron/12-traces-min-rpb1.t index 2a760c0dcb..d6ce4301ee 100644 --- a/tests/regression/36-apron/12-traces-min-rpb1.t +++ b/tests/regression/36-apron/12-traces-min-rpb1.t @@ -7,11 +7,11 @@ dead: 0 total lines: 18 [Warning][Race] Memory location h (race with conf. 110): (12-traces-min-rpb1.c:8:5-8:10) - write with [lock:{A}, thread:[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]] (conf. 110) (exp: & h) (12-traces-min-rpb1.c:15:3-15:8) - read with [mhp:{created={[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]}}, thread:[main]] (conf. 110) (exp: & h) (12-traces-min-rpb1.c:27:3-27:26) + write with [lock:{A}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]] (conf. 110) (exp: & h) (12-traces-min-rpb1.c:15:3-15:8) + read with [mhp:{created={[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & h) (12-traces-min-rpb1.c:27:3-27:26) [Warning][Race] Memory location g (race with conf. 110): (12-traces-min-rpb1.c:7:5-7:10) - write with [lock:{A}, thread:[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]] (conf. 110) (exp: & g) (12-traces-min-rpb1.c:14:3-14:8) - read with [mhp:{created={[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]}}, thread:[main]] (conf. 110) (exp: & g) (12-traces-min-rpb1.c:27:3-27:26) + write with [lock:{A}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]] (conf. 110) (exp: & g) (12-traces-min-rpb1.c:14:3-14:8) + read with [mhp:{created={[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & g) (12-traces-min-rpb1.c:27:3-27:26) [Info][Witness] witness generation summary: location invariants: 3 loop invariants: 0 @@ -64,11 +64,11 @@ [Success][Assert] Assertion "g == h" will succeed (12-traces-min-rpb1.c:16:3-16:26) [Success][Assert] Assertion "g == h" will succeed (12-traces-min-rpb1.c:29:3-29:26) [Warning][Race] Memory location g (race with conf. 110): (12-traces-min-rpb1.c:7:5-7:10) - write with [lock:{A}, thread:[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]] (conf. 110) (exp: & g) (12-traces-min-rpb1.c:14:3-14:8) - read with [mhp:{created={[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]}}, thread:[main]] (conf. 110) (exp: & g) (12-traces-min-rpb1.c:27:3-27:26) + write with [lock:{A}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]] (conf. 110) (exp: & g) (12-traces-min-rpb1.c:14:3-14:8) + read with [mhp:{created={[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & g) (12-traces-min-rpb1.c:27:3-27:26) [Warning][Race] Memory location h (race with conf. 110): (12-traces-min-rpb1.c:8:5-8:10) - write with [lock:{A}, thread:[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]] (conf. 110) (exp: & h) (12-traces-min-rpb1.c:15:3-15:8) - read with [mhp:{created={[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]}}, thread:[main]] (conf. 110) (exp: & h) (12-traces-min-rpb1.c:27:3-27:26) + write with [lock:{A}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]] (conf. 110) (exp: & h) (12-traces-min-rpb1.c:15:3-15:8) + read with [mhp:{created={[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & h) (12-traces-min-rpb1.c:27:3-27:26) [Info][Race] Memory locations race summary: safe: 0 vulnerable: 0 diff --git a/tests/regression/45-escape/51-fresh-global.t b/tests/regression/45-escape/51-fresh-global.t index ceb21425e8..aa6e06e153 100644 --- a/tests/regression/45-escape/51-fresh-global.t +++ b/tests/regression/45-escape/51-fresh-global.t @@ -4,8 +4,8 @@ dead: 0 total lines: 15 [Warning][Race] Memory location (alloc@sid:$SID@tid:main) (race with conf. 110): (51-fresh-global.c:25:7-25:31) - write with lock:{A} (conf. 110) (exp: & *i) (51-fresh-global.c:10:3-10:10) - write with thread:main (conf. 110) (exp: & *i) (51-fresh-global.c:27:3-27:9) + write with [lock:{A}, threadflag:(MT mode:Multithreaded (other), bool:true)] (conf. 110) (exp: & *i) (51-fresh-global.c:10:3-10:10) + write with [threadflag:(MT mode:Multithreaded (main), bool:true), thread:main] (conf. 110) (exp: & *i) (51-fresh-global.c:27:3-27:9) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 diff --git a/tests/regression/46-apron2/95-witness-mm-escape.t b/tests/regression/46-apron2/95-witness-mm-escape.t index 11cd3691c5..9724c1a9a9 100644 --- a/tests/regression/46-apron2/95-witness-mm-escape.t +++ b/tests/regression/46-apron2/95-witness-mm-escape.t @@ -27,3 +27,8 @@ unsupported: 0 disabled: 0 total validation entries: 15 + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 0 + total memory locations: 1 diff --git a/tests/regression/56-witness/68-ghost-ambiguous-idx.t b/tests/regression/56-witness/68-ghost-ambiguous-idx.t index 40025acf17..03fd9bd708 100644 --- a/tests/regression/56-witness/68-ghost-ambiguous-idx.t +++ b/tests/regression/56-witness/68-ghost-ambiguous-idx.t @@ -6,9 +6,9 @@ dead: 0 total lines: 15 [Warning][Race] Memory location data (race with conf. 110): (68-ghost-ambiguous-idx.c:4:5-4:9) - write with [lock:{m[4]}, thread:[main, t_fun@68-ghost-ambiguous-idx.c:20:3-20:40]] (conf. 110) (exp: & data) (68-ghost-ambiguous-idx.c:9:3-9:9) - write with [lock:{m[4]}, thread:[main, t_fun@68-ghost-ambiguous-idx.c:20:3-20:40]] (conf. 110) (exp: & data) (68-ghost-ambiguous-idx.c:10:3-10:9) - read with [mhp:{created={[main, t_fun@68-ghost-ambiguous-idx.c:20:3-20:40]}}, thread:[main]] (conf. 110) (exp: & data) (68-ghost-ambiguous-idx.c:24:3-24:29) + write with [lock:{m[4]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@68-ghost-ambiguous-idx.c:20:3-20:40]] (conf. 110) (exp: & data) (68-ghost-ambiguous-idx.c:9:3-9:9) + write with [lock:{m[4]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@68-ghost-ambiguous-idx.c:20:3-20:40]] (conf. 110) (exp: & data) (68-ghost-ambiguous-idx.c:10:3-10:9) + read with [mhp:{created={[main, t_fun@68-ghost-ambiguous-idx.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & data) (68-ghost-ambiguous-idx.c:24:3-24:29) [Info][Witness] witness generation summary: location invariants: 0 loop invariants: 0 diff --git a/tests/regression/56-witness/69-ghost-ptr-protection.t b/tests/regression/56-witness/69-ghost-ptr-protection.t index 0c5fb0201c..c4c1f7519e 100644 --- a/tests/regression/56-witness/69-ghost-ptr-protection.t +++ b/tests/regression/56-witness/69-ghost-ptr-protection.t @@ -5,9 +5,9 @@ dead: 0 total lines: 15 [Warning][Race] Memory location p (race with conf. 110): (69-ghost-ptr-protection.c:7:5-7:12) - write with [lock:{m2}, thread:[main, t_fun@69-ghost-ptr-protection.c:22:3-22:40]] (conf. 110) (exp: & p) (69-ghost-ptr-protection.c:14:3-14:9) - write with [lock:{m2}, thread:[main, t_fun@69-ghost-ptr-protection.c:22:3-22:40]] (conf. 110) (exp: & p) (69-ghost-ptr-protection.c:15:3-15:9) - read with [mhp:{created={[main, t_fun@69-ghost-ptr-protection.c:22:3-22:40]}}, lock:{m1}, thread:[main]] (conf. 110) (exp: & p) (69-ghost-ptr-protection.c:26:3-26:27) + write with [lock:{m2}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@69-ghost-ptr-protection.c:22:3-22:40]] (conf. 110) (exp: & p) (69-ghost-ptr-protection.c:14:3-14:9) + write with [lock:{m2}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@69-ghost-ptr-protection.c:22:3-22:40]] (conf. 110) (exp: & p) (69-ghost-ptr-protection.c:15:3-15:9) + read with [mhp:{created={[main, t_fun@69-ghost-ptr-protection.c:22:3-22:40]}}, lock:{m1}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & p) (69-ghost-ptr-protection.c:26:3-26:27) [Info][Witness] witness generation summary: location invariants: 0 loop invariants: 0 @@ -124,9 +124,9 @@ Same with vojdani. dead: 0 total lines: 15 [Warning][Race] Memory location p (race with conf. 110): (69-ghost-ptr-protection.c:7:5-7:12) - write with [lock:{m2}, thread:[main, t_fun@69-ghost-ptr-protection.c:22:3-22:40]] (conf. 110) (exp: & p) (69-ghost-ptr-protection.c:14:3-14:9) - write with [lock:{m2}, thread:[main, t_fun@69-ghost-ptr-protection.c:22:3-22:40]] (conf. 110) (exp: & p) (69-ghost-ptr-protection.c:15:3-15:9) - read with [mhp:{created={[main, t_fun@69-ghost-ptr-protection.c:22:3-22:40]}}, lock:{m1}, thread:[main]] (conf. 110) (exp: & p) (69-ghost-ptr-protection.c:26:3-26:27) + write with [lock:{m2}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@69-ghost-ptr-protection.c:22:3-22:40]] (conf. 110) (exp: & p) (69-ghost-ptr-protection.c:14:3-14:9) + write with [lock:{m2}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@69-ghost-ptr-protection.c:22:3-22:40]] (conf. 110) (exp: & p) (69-ghost-ptr-protection.c:15:3-15:9) + read with [mhp:{created={[main, t_fun@69-ghost-ptr-protection.c:22:3-22:40]}}, lock:{m1}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110) (exp: & p) (69-ghost-ptr-protection.c:26:3-26:27) [Info][Witness] witness generation summary: location invariants: 0 loop invariants: 0 diff --git a/tests/regression/71-doublelocking/07-rec-dyn-osx.c b/tests/regression/71-doublelocking/07-rec-dyn-osx.c index bb3cf65657..4059356371 100644 --- a/tests/regression/71-doublelocking/07-rec-dyn-osx.c +++ b/tests/regression/71-doublelocking/07-rec-dyn-osx.c @@ -1,6 +1,5 @@ -// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType' --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE" +// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType' // Here, we do not include pthread.h, so MutexAttr.recursive_int remains at `2`, emulating the behavior of OS X. -#define GOBLINT_NO_PTHREAD_ONCE 1 typedef signed char __int8_t; typedef unsigned char __uint8_t; typedef short __int16_t; diff --git a/tests/regression/71-doublelocking/20-default-init-osx.c b/tests/regression/71-doublelocking/20-default-init-osx.c index 4d3ec1f8d7..eaa6ec58be 100644 --- a/tests/regression/71-doublelocking/20-default-init-osx.c +++ b/tests/regression/71-doublelocking/20-default-init-osx.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType' --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE" +// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType' // Here, we do not include pthread.h, to emulate the behavior of OS X. #define NULL ((void *)0) typedef signed char __int8_t; diff --git a/tests/regression/74-invalid_deref/01-oob-heap-simple.t b/tests/regression/74-invalid_deref/01-oob-heap-simple.t index ac3ec99fa8..0f241692cd 100644 --- a/tests/regression/74-invalid_deref/01-oob-heap-simple.t +++ b/tests/regression/74-invalid_deref/01-oob-heap-simple.t @@ -6,6 +6,11 @@ live: 8 dead: 0 total lines: 8 + [Info][Race] Memory locations race summary: + safe: 2 + vulnerable: 0 + unsafe: 0 + total memory locations: 2 $ goblint --set ana.activated[+] memOutOfBounds --enable ana.int.interval --enable dbg.full-output 01-oob-heap-simple.c > full-output.txt 2>&1 diff --git a/tests/regression/82-barrier/01-simple.c b/tests/regression/82-barrier/01-simple.c new file mode 100644 index 0000000000..285da1a6fb --- /dev/null +++ b/tests/regression/82-barrier/01-simple.c @@ -0,0 +1,26 @@ +// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers' +#include +#include +#include + +int g; + +pthread_barrier_t barrier; + + +int main(int argc, char const *argv[]) +{ + int top; + int i = 0; + + pthread_barrier_init(&barrier, NULL, 2); + + if(top) { + pthread_barrier_wait(&barrier); + // Unreachable + i = 1; + } + + __goblint_check(i == 0); + return 0; +} diff --git a/tests/regression/82-barrier/02-more.c b/tests/regression/82-barrier/02-more.c new file mode 100644 index 0000000000..53b4e99de2 --- /dev/null +++ b/tests/regression/82-barrier/02-more.c @@ -0,0 +1,45 @@ +// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers' +#include +#include +#include + +int g; + +pthread_barrier_t barrier; + +void* f2(void* ptr) { + pthread_barrier_wait(&barrier); + return NULL; +} + +void* f1(void* ptr) { + pthread_barrier_wait(&barrier); + + // This is past the barrier, so it will not be reached + pthread_t t2; + pthread_create(&t2,NULL,f2,NULL); + + return NULL; +} + +int main(int argc, char const *argv[]) +{ + int top; + int i = 0; + + pthread_barrier_init(&barrier, NULL, 3); + + pthread_t t1; + pthread_create(&t1,NULL,f1,NULL); + + if(top) { + pthread_barrier_wait(&barrier); + // Unreachable + i = 1; + } + + __goblint_check(i == 0); + + + return 0; +} diff --git a/tests/regression/82-barrier/03-problem.c b/tests/regression/82-barrier/03-problem.c new file mode 100644 index 0000000000..2d80706b92 --- /dev/null +++ b/tests/regression/82-barrier/03-problem.c @@ -0,0 +1,36 @@ +// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers' +#include +#include +#include + +int g; + +pthread_barrier_t barrier; + + +void* f1(void* ptr) { + pthread_barrier_wait(&barrier); + return NULL; +} + +int main(int argc, char const *argv[]) +{ + int top; + int i = 0; + + pthread_barrier_init(&barrier, NULL, 2); + + pthread_t t1; + pthread_create(&t1,NULL,f1,NULL); + + if(top) { + pthread_barrier_wait(&barrier); + // Live! + i = 1; + } + + __goblint_check(i == 0); //UNKNOWN! + + + return 0; +} diff --git a/tests/regression/82-barrier/04-challenge.c b/tests/regression/82-barrier/04-challenge.c new file mode 100644 index 0000000000..73d66e5c51 --- /dev/null +++ b/tests/regression/82-barrier/04-challenge.c @@ -0,0 +1,49 @@ +// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers' +#include +#include +#include + +int g; + +pthread_barrier_t barrier; + +void* f2(void* ptr) { + pthread_barrier_wait(&barrier); + return NULL; +} + +void* f1(void* ptr) { + pthread_barrier_wait(&barrier); + + // This is past the barrier, so it will not be reached + pthread_t t2; + pthread_create(&t2,NULL,f2,NULL); + + return NULL; +} + +int main(int argc, char const *argv[]) +{ + int top; + int i = 0; + + pthread_barrier_init(&barrier, NULL, 3); + + pthread_t t1; + pthread_create(&t1,NULL,f1,NULL); + + if(top) { + pthread_barrier_wait(&barrier); + // Unreachable + i = 1; + } + + // Created too late to have any effect + pthread_t t2; + pthread_create(&t2,NULL,f1,NULL); + + __goblint_check(i == 0); + + + return 0; +} diff --git a/tests/regression/82-barrier/05-mhp-not-enough.c b/tests/regression/82-barrier/05-mhp-not-enough.c new file mode 100644 index 0000000000..b289f3b0c0 --- /dev/null +++ b/tests/regression/82-barrier/05-mhp-not-enough.c @@ -0,0 +1,44 @@ +// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers' +#include +#include +#include + +int g; + +pthread_barrier_t barrier; + + +void* f1(void* ptr) { + pthread_barrier_wait(&barrier); + + // This should not be reached as either main calls wait or the other thread is created + // -> In the concrete, there never are three threads calling wait + + return NULL; +} + +int main(int argc, char const *argv[]) +{ + int top; + int i = 0; + + pthread_barrier_init(&barrier, NULL, 3); + + pthread_t t1; + pthread_create(&t1,NULL,f1,NULL); + + if(top) { + pthread_barrier_wait(&barrier); + // Unreachable + i = 1; + } else { + pthread_t t2; + pthread_create(&t2,NULL,f1,NULL); + } + + + __goblint_check(i == 0); + + + return 0; +} diff --git a/tests/regression/82-barrier/06-multiprocess.c b/tests/regression/82-barrier/06-multiprocess.c new file mode 100644 index 0000000000..f55790cfab --- /dev/null +++ b/tests/regression/82-barrier/06-multiprocess.c @@ -0,0 +1,35 @@ +// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers' +#include +#include +#include + +int g; + +pthread_barrier_t barrier; + + +int main(int argc, char const *argv[]) +{ + int top; + int i = 0; + + pthread_barrierattr_t barattr; + pthread_barrierattr_setpshared(&barattr, PTHREAD_PROCESS_SHARED); + + pthread_barrier_init(&barrier, &barattr, 2); + + fork(); + pthread_t t1; + + if(top) { + pthread_barrier_wait(&barrier); + // Reachable if both processes go into this branch + i = 1; + } + + + __goblint_check(i == 0); //UNKNOWN! + + + return 0; +} diff --git a/tests/regression/82-barrier/07-lockset.c b/tests/regression/82-barrier/07-lockset.c new file mode 100644 index 0000000000..d1c68f3d7f --- /dev/null +++ b/tests/regression/82-barrier/07-lockset.c @@ -0,0 +1,39 @@ +// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers' +#include +#include +#include + +int g; + +pthread_barrier_t barrier; +pthread_mutex_t mutex; + +void* f1(void* ptr) { + pthread_mutex_lock(&mutex); + pthread_barrier_wait(&barrier); + pthread_mutex_unlock(&mutex); + return NULL; +} + +int main(int argc, char const *argv[]) +{ + int top; + int i = 0; + + pthread_barrier_init(&barrier, NULL, 2); + + pthread_t t1; + pthread_create(&t1,NULL,f1,NULL); + + if(top) { + pthread_mutex_lock(&mutex); + pthread_barrier_wait(&barrier); + // Deadlocks + pthread_mutex_unlock(&mutex); + i = 1; + } + + __goblint_check(i == 0); + + return 0; +} diff --git a/tests/regression/82-barrier/08-lockset-more.c b/tests/regression/82-barrier/08-lockset-more.c new file mode 100644 index 0000000000..a33ecc1a78 --- /dev/null +++ b/tests/regression/82-barrier/08-lockset-more.c @@ -0,0 +1,47 @@ +// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers' +#include +#include +#include + +int g; + +pthread_barrier_t barrier; +pthread_mutex_t mutex; + +void* f1(void* ptr) { + pthread_mutex_lock(&mutex); + pthread_barrier_wait(&barrier); + pthread_mutex_unlock(&mutex); + return NULL; +} + +void* f2(void* ptr) { + pthread_mutex_lock(&mutex); + pthread_barrier_wait(&barrier); + pthread_mutex_unlock(&mutex); + return NULL; +} + +int main(int argc, char const *argv[]) +{ + int top; + int i = 0; + + pthread_barrier_init(&barrier, NULL, 2); + + pthread_t t1; + pthread_create(&t1,NULL,f1,NULL); + + pthread_t t2; + pthread_create(&t2,NULL,f2,NULL); + + + if(top) { + pthread_barrier_wait(&barrier); + i = 1; + } + + __goblint_check(i == 0); //UNKNOWN! + + return 0; +} diff --git a/tests/regression/82-barrier/09-race.c b/tests/regression/82-barrier/09-race.c new file mode 100644 index 0000000000..fad6ad6243 --- /dev/null +++ b/tests/regression/82-barrier/09-race.c @@ -0,0 +1,36 @@ +// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers' +#include +#include +#include + +int g; +int h; + +pthread_barrier_t barrier; +pthread_mutex_t mutex; + +void* f1(void* ptr) { + g = 2; //NORACE + h = 3; //RACE + pthread_barrier_wait(&barrier); + + return NULL; +} + +int main(int argc, char const *argv[]) +{ + int top; + int i = 0; + + pthread_barrier_init(&barrier, NULL, 2); + + pthread_t t1; + pthread_create(&t1,NULL,f1,NULL); + + h = 5; //RACE + + pthread_barrier_wait(&barrier); + g = 3; //NORACE + + return 0; +} diff --git a/tests/regression/82-barrier/10-several.c b/tests/regression/82-barrier/10-several.c new file mode 100644 index 0000000000..6fc9f57681 --- /dev/null +++ b/tests/regression/82-barrier/10-several.c @@ -0,0 +1,36 @@ +// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers' +#include +#include +#include + +int g; + +pthread_barrier_t barrier; + +void* f1(void* ptr) { + pthread_barrier_wait(&barrier); + + return NULL; +} + +int main(int argc, char const *argv[]) +{ + int top; + int i = 0; + + pthread_barrier_init(&barrier, NULL, 4); + + pthread_t t1, t2, t3; + pthread_create(&t1,NULL,f1,NULL); + pthread_create(&t2,NULL,f1,NULL); + pthread_create(&t3,NULL,f1,NULL); + + if(top) { + pthread_barrier_wait(&barrier); + i = 1; + } + + __goblint_check(i == 0); //UNKNOWN! + + return 0; +} diff --git a/tests/regression/82-barrier/11-race-more.c b/tests/regression/82-barrier/11-race-more.c new file mode 100644 index 0000000000..ed6c7ef29d --- /dev/null +++ b/tests/regression/82-barrier/11-race-more.c @@ -0,0 +1,37 @@ +// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers' +#include +#include +#include + +int g; + +pthread_barrier_t barrier; +pthread_mutex_t mutex; + +void* f1(void* ptr) { + pthread_mutex_lock(&mutex); + g = 4711; //NORACE + pthread_mutex_unlock(&mutex); + pthread_barrier_wait(&barrier); + + return NULL; +} + +int main(int argc, char const *argv[]) +{ + int top; + int i = 0; + + pthread_barrier_init(&barrier, NULL, 4); + + pthread_t t1, t2, t3; + pthread_create(&t1,NULL,f1,NULL); + pthread_create(&t2,NULL,f1,NULL); + pthread_create(&t3,NULL,f1,NULL); + + pthread_barrier_wait(&barrier); + + g = 3; //NORACE + + return 0; +} diff --git a/tests/regression/83-once/01-sanity.c b/tests/regression/83-once/01-sanity.c new file mode 100644 index 0000000000..8a26012571 --- /dev/null +++ b/tests/regression/83-once/01-sanity.c @@ -0,0 +1,27 @@ +// PARAM: --set ana.activated[+] pthreadOnce +#include +#include + +int g; +pthread_once_t once = PTHREAD_ONCE_INIT; +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; + +void fun() { + g++; +} + + +int main(void) { + pthread_t id; + + pthread_once(&once, fun); + pthread_once(&once, fun); + + __goblint_check(g < 2); + + if(g = 1) { + __goblint_check(1); //Reachable + } + + return 0; +} diff --git a/tests/regression/83-once/02-normal.c b/tests/regression/83-once/02-normal.c new file mode 100644 index 0000000000..ee10a7d6b4 --- /dev/null +++ b/tests/regression/83-once/02-normal.c @@ -0,0 +1,34 @@ +// PARAM: --set ana.activated[+] pthreadOnce +#include +#include + +int g; +pthread_once_t once = PTHREAD_ONCE_INIT; +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; + +void fun() { + g = 42; //NORACE +} + + +void *t_fun(void *arg) { + pthread_once(&once, fun); + + pthread_mutex_lock(&mutex1); + g = 10; //NORACE + pthread_mutex_unlock(&mutex1); + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + + pthread_once(&once, fun); + + pthread_mutex_lock(&mutex1); + g = 11; //NORACE + pthread_mutex_unlock(&mutex1); + pthread_join (id, NULL); + return 0; +} diff --git a/tests/regression/83-once/03-unknown.c b/tests/regression/83-once/03-unknown.c new file mode 100644 index 0000000000..16cb2c5a12 --- /dev/null +++ b/tests/regression/83-once/03-unknown.c @@ -0,0 +1,44 @@ +// PARAM: --set ana.activated[+] pthreadOnce +#include +#include + +int g; +pthread_once_t once1 = PTHREAD_ONCE_INIT; +pthread_once_t once2; // PTHREAD_ONCE_INIT is `0` +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; + +pthread_once_t *ptr; + +void fun() { + g = 42; //RACE +} + + +void *t_fun(void *arg) { + pthread_once(ptr, fun); + + pthread_mutex_lock(&mutex1); + g = 10; //RACE + pthread_mutex_unlock(&mutex1); + return NULL; +} + +int main(void) { + pthread_t id; + int top; + pthread_create(&id, NULL, t_fun, NULL); + + ptr = &once1; + + if(top) { + ptr = &once2; + } + + pthread_once(ptr, fun); + + pthread_mutex_lock(&mutex1); + g = 11; //RACE + pthread_mutex_unlock(&mutex1); + pthread_join (id, NULL); + return 0; +} diff --git a/tests/regression/83-once/04-thread.c b/tests/regression/83-once/04-thread.c new file mode 100644 index 0000000000..c467bacc22 --- /dev/null +++ b/tests/regression/83-once/04-thread.c @@ -0,0 +1,58 @@ +// PARAM: --set ana.activated[+] pthreadOnce +#include +#include + +int g; +int h; +int i; +pthread_once_t once = PTHREAD_ONCE_INIT; +pthread_once_t i_once = PTHREAD_ONCE_INIT; +pthread_mutex_t mut; + +void *t_other(void* arg) { + g = 17; //RACE + + pthread_mutex_lock(&mut); + i = 7; //NORACE + pthread_mutex_unlock(&mut); +} + +void nesting() { + h = 5; //NORACE +} + +void fun() { + // Even though this is only called inside the once, the accesses in the new thread and the accesses here can happen in parallel + // Checks that active is not passed to the created thread, but seen is passed + pthread_t tid = pthread_create(&tid, NULL, t_other, NULL); + g = 42; //RACE + + h = 8; //NORACE + // Active onces get passed to the callee and back to the caller + nesting(); + h = 12; //NORACE +} + +void ifun() { + i = 11; //NORACE +} + +void *t_fun(void *arg) { + pthread_once(&i_once, ifun); + pthread_once(&once, fun); + return NULL; +} + +int main(void) { + pthread_t id; + int top; + + pthread_create(&id, NULL, t_fun, NULL); + + pthread_once(&i_once, ifun); + pthread_once(&once, fun); + + h = 5; //NORACE + + return 0; +} diff --git a/tests/regression/83-once/05-unknown-tid.c b/tests/regression/83-once/05-unknown-tid.c new file mode 100644 index 0000000000..f6aa7956ba --- /dev/null +++ b/tests/regression/83-once/05-unknown-tid.c @@ -0,0 +1,28 @@ +// PARAM: --set ana.activated[+] pthreadOnce +#include +#include + +int g; +pthread_once_t once = PTHREAD_ONCE_INIT; +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; + +void fun() { + g++; //NORACE +} + + +void* thread(void* arg) { + pthread_once(&once, fun); + return NULL; +} + +int main(void) { + pthread_t id; + + for(int i=0; i < 100; i++) { + // Will receive unknown TID + pthread_create(&id, NULL, thread, NULL); + } + + return 0; +} diff --git a/tests/regression/83-once/06-multiple-inside-once.c b/tests/regression/83-once/06-multiple-inside-once.c new file mode 100644 index 0000000000..b388c85963 --- /dev/null +++ b/tests/regression/83-once/06-multiple-inside-once.c @@ -0,0 +1,27 @@ +// PARAM: --set ana.activated[+] pthreadOnce +#include +#include + +int g; +pthread_once_t once = PTHREAD_ONCE_INIT; +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; + +void fun() { + g++; //NORACE + g++; //NORACE +} + + +void* thread(void* arg) { + pthread_once(&once, fun); + return NULL; +} + +int main(void) { + pthread_t id; + + pthread_create(&id, NULL, thread, NULL); + pthread_once(&once, fun); + + return 0; +} diff --git a/tests/regression/83-once/07-different-onces.c b/tests/regression/83-once/07-different-onces.c new file mode 100644 index 0000000000..7e9bf83968 --- /dev/null +++ b/tests/regression/83-once/07-different-onces.c @@ -0,0 +1,29 @@ +// PARAM: --set ana.activated[+] pthreadOnce +// Developer used tow different pthread_once_t variables by mistake +#include +#include + +int g; +pthread_once_t once = PTHREAD_ONCE_INIT; +pthread_once_t once1 = PTHREAD_ONCE_INIT; +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; + +void fun() { + g++; //RACE! + g++; //RACE! +} + + +void* thread(void* arg) { + pthread_once(&once, fun); + return NULL; +} + +int main(void) { + pthread_t id; + + pthread_create(&id, NULL, thread, NULL); + pthread_once(&once1, fun); + + return 0; +} diff --git a/tests/regression/83-once/08-pointers.c b/tests/regression/83-once/08-pointers.c new file mode 100644 index 0000000000..b2df8c6c05 --- /dev/null +++ b/tests/regression/83-once/08-pointers.c @@ -0,0 +1,39 @@ +// PARAM: --set ana.activated[+] pthreadOnce +// Function to be called by once is passed as a pointer +#include +#include + +int g; +void init0(); + +void* initp = &init0; +pthread_once_t once = PTHREAD_ONCE_INIT; +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; + +void init0() { + g++; //NORACE +} + + +void init1() { + g++; //NORACE +} + + +void* thread(void* arg) { + pthread_once(&once, initp); + return NULL; +} + +int main(void) { + pthread_t id; + int top; + + if(top) { initp = &init1; } + + pthread_create(&id, NULL, thread, NULL); + + pthread_once(&once, initp); + + return 0; +} diff --git a/tests/regression/83-once/09-pointers2.c b/tests/regression/83-once/09-pointers2.c new file mode 100644 index 0000000000..3cf93c19a1 --- /dev/null +++ b/tests/regression/83-once/09-pointers2.c @@ -0,0 +1,38 @@ +// PARAM: --set ana.activated[+] pthreadOnce +// Function to be called by once is passed as a pointer +#include +#include + +int g; +void init0(); + +void* initp = &init0; +pthread_once_t once = PTHREAD_ONCE_INIT; +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; + +void init0() { + g++; //NORACE +} + + +void init1() { + g++; //NORACE +} + + +void* thread(void* arg) { + pthread_once(&once, initp); + return NULL; +} + +int main(void) { + pthread_t id; + int top; + + pthread_create(&id, NULL, thread, NULL); + if(top) { initp = &init1; } + pthread_once(&once, initp); + + + return 0; +} diff --git a/tests/regression/83-once/10-pointer-once.c b/tests/regression/83-once/10-pointer-once.c new file mode 100644 index 0000000000..c074c55994 --- /dev/null +++ b/tests/regression/83-once/10-pointer-once.c @@ -0,0 +1,33 @@ +// PARAM: --set ana.activated[+] pthreadOnce +// pthread_once object is passed as a pointer (and it may change) +#include +#include + +int g; +void init0(); + +pthread_once_t* optr; +pthread_once_t once = PTHREAD_ONCE_INIT; +pthread_once_t once1 = PTHREAD_ONCE_INIT; +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; + +void init0() { + g++; //RACE +} + + +void* thread(void* arg) { + pthread_once(&once, init0); + return NULL; +} + +int main(void) { + pthread_t id; + int top; + + pthread_create(&id, NULL, thread, NULL); + if(top) { optr = &once1; } + pthread_once(optr, init0); + + return 0; +}