Reproduction Package for fm-weck

NOTE This is the README for the fm-weck 1.2.1 Artifact. If you are interested in the tutorial for the latest version of fm-weck, please refer to the Tutorial.md.

This tutorial shows some of the features of fm-weck and how to use them. We show how to run fm-weck via the docker container.

The paper describes fm-weck’s three modes of operation: expert, automatic, and shell. This tutorial will show how to use these modes with several tools from the fm-tools repository.

The claims made in the paper are supported by the following examples:

1. fm-weck can verifiers “for experts” in expert mode.

2. fm-weck can verifiers in automatic mode, i.e., execute a software verification tool without needing to know it command line arguments.

3. fm-weck can start an interactive shell inside the recommended container for a given verifier.

Running fm-weck with Docker

This artifact contains the docker image as fm-weck.tar.gz. Load the image fm-weck.tar.gz into Docker:

docker load -i fm-weck.tar.gz

Navigate to the root directory fm-weck-artifact of the artifact. Now enter an interactive shell inside the container:

docker run --privileged --rm --entrypoint /bin/bash -it fm-weck

Explanation:

• --privileged allows the container to run other container instances inside of it (needed for fm-weck to run other tools in containers)

• --rm removes the container after it is stopped.

• --entrypoint /bin/bash sets the entrypoint to /bin/bash instead of the default entrypoint, which is fm-weck.

Your first fm-weck run

To get an overview of the available commands run:

$ fm-weck --help
usage: fm-weck [-h] [--version] [--config CONFIG]
               [--loglevel {debug,info,warning,error,critical}] [--list]
               {run,r,expert,e,m,shell,install,i} ...

fm-weck

positional arguments:
  {run,r,expert,e,m,shell,install,i}
    run (r)             Run a verifier inside a container.
    expert (e, m)       Manually run a verifier inside a container.Arguments are passed verbatim
                        to the tool, so expert-ise about it's command line is required.
    shell               Start an interactive shell inside the container.
    install (i)         Download and unpack a TOOL for later use.
    server (s)          Run fm-weck remotely on a server.

options:
  -h, --help            show this help message and exit
  --version             show program's version number and exit
  --config CONFIG       Path to the configuration file.
  --loglevel {debug,info,warning,error,critical}
                        Set the log level.
  --list                List all fm-tools that can be called by name.

To get an overview of the available tools run:

$ fm-weck --list
List of fm-tools callable by name:
  - 2ls
  - aise
  - aprove
  - brick
  - bubaak
[!snip]
  - cpachecker
[!snip]

List of properties callable by name:
  - coverage-branches
  - coverage-conditions
  - coverage-error-call
  - coverage-statements
  - def-behavior
  - no-data-race
  - no-overflow
  - termination
  - unreach-call
  - valid-memcleanup
  - valid-memsafety

Running a tool in expert mode

fm-weck run has two modes: the expert mode and the automatic mode. The expert mode allows you to run a tool and control all arguments passed to it.

Let’s look at an example: to get the version of CPAchecker, CPAchecker accepts the -version flag. To pass that flag directly to CPAchecker, you can run:

$ fm-weck expert cpachecker -version
INFO:httpx:HTTP Request: GET https://zenodo.org/api/records/11074229 "HTTP/1.1 200 OK"
tool_module:  benchexec.tools.cpachecker
INFO:fm_weck.engine:Running: ['podman', 'run', '--entrypoint', '[""]', '--cap-add', 'SYS_ADMIN', '-v', '/app:/home/cwd', '-v', '/root/.cache/weck_cache:/home/weck_cache', '-v', '/tmp/tmp32kjo54cfm_weck_output:/home/output', '--workdir', '/home/cwd', '--rm', 'registry.gitlab.com/sosy-lab/software/cpachecker:2.3.1', PosixPath('/home/weck_cache/CPAchecker-2.3.1/scripts/cpa.sh'), '-version']
Running CPAchecker with default heap size (1200M). Specify a larger value with -heap if you have more RAM.
Running CPAchecker with default stack size (1024k). Specify a larger value with -stack if needed.

CPAchecker 2.3.1 (OpenJDK 64-Bit Server VM 17.0.11)

NOTE
Depending on your system podman might print an error message similar to

WARN[0020] Failed to add conmon to cgroupfs sandbox cgroup: creating cgroup path /libpod_parent/conmon: write /sys/fs/cgroup/cgroup.subtree_control: device or resource busy

This does not affect the execution of fm-weck. You may ignore this message.

You see some INFO output from fm-weck followed by the output of CPAchecker.
We can also run CPAchecker as “experts”, i.e., someone who knows how set CPAcheckers commandline.

NOTE
All commands in this section assume that you are in the /app directory of the container.

$ fm-weck expert cpachecker -default examples/example-safe.c
INFO:httpx:HTTP Request: GET https://zenodo.org/api/records/11074229 "HTTP/1.1 200 OK"
tool_module:  benchexec.tools.cpachecker
INFO:fm_weck.engine:Running: ['podman', 'run', '--entrypoint', '[""]', '--cap-add', 'SYS_ADMIN', '-v', '/app:/home/cwd', '-v', '/root/.cache/weck_cache:/home/weck_cache', '-v', '/tmp/tmpbbupwew7fm_weck_output:/home/output', '--workdir', '/home/cwd', '--rm', 'registry.gitlab.com/sosy-lab/software/cpachecker:2.3.1', PosixPath('/home/weck_cache/CPAchecker-2.3.1/scripts/cpa.sh'), '-default', 'examples/example-safe.c']
Running CPAchecker with default heap size (1200M). Specify a larger value with -heap if you have more RAM.
Running CPAchecker with default stack size (1024k). Specify a larger value with -stack if needed.
Language C detected and set for analysis (CPAMain.detectFrontendLanguageIfNecessary, INFO)

[!snip]

Stopping analysis ... (CPAchecker.runAlgorithm, INFO)

Verification result: TRUE. No property violation found by chosen configuration.
More details about the verification run can be found in the directory "./output".
Graphical representation included in the file "./output/Report.html".

CPAchecker produced the verification result TRUE, meaning it could prove the property (here: the default that was set by the CPAchecker developers) valid.

Peeking into the output directory, we see that it contains the output that CPAchecker produced.

$ ls output
abstractions.txt  ARGSimplified.dot  cfa      cfaPixel.svg   CPALog.txt      functionCalls.dot      Report.html     UsedConfiguration.properties  VariableTypeMapping.txt
ARG.dot           ARG.svg            cfa.dot  coverage.info  CPALog.txt.lck  functionCallsUsed.dot  Statistics.txt  VariableClassification.log    witness-2.0.yml

Peeking into the output directory, we see that it contains the output that CPAchecker produced.

We can also use the expert mode to run other tools from the fm-tools repository. The following command prints the version of UAutomizer:

$ fm-weck expert uautomizer:svcomp24 --version
INFO:httpx:HTTP Request: GET https://zenodo.org/api/records/10203545 "HTTP/1.1 200 OK"
INFO:httpx:HTTP Request: GET https://zenodo.org/api/records/10203545/files/uautomizer.zip/content "HTTP/1.1 200 OK"
129860KiB [00:45, 2883.07KiB/s]
INFO:httpx:HTTP Request: GET https://zenodo.org/api/records/10203545 "HTTP/1.1 200 OK"
tool_module:  benchexec.tools.ultimateautomizer
INFO:fm_weck.engine:Running: ['podman', 'run', '--entrypoint', '[""]', '--cap-add', 'SYS_ADMIN', '-v', '/app:/home/cwd', '-v', '/root/.cache/weck_cache:/home/weck_cache', '-v', '/tmp/tmpuvpyf_mofm_weck_output:/home/output', '--workdir', '/home/cwd', '--rm', 'registry.gitlab.com/sosy-lab/benchmarking/competition-scripts/user:2024', PosixPath('/home/weck_cache/UAutomizer-svcomp24/Ultimate.py'), '--version']
Trying to pull registry.gitlab.com/sosy-lab/benchmarking/competition-scripts/user:2024...
Getting image source signatures
Copying blob a35478ff8ddd done
Copying blob 857cc8cb19c0 done
Copying blob 06e2cd0cf31c done
Copying blob 4deaf16c24cd done
Copying blob 9a2d232d75f0 done
Copying blob 8c82958e4083 done
Copying config f149b84532 done
Writing manifest to image destination
Storing signatures
0e0057cc

Running a tool in automatic mode

NOTE
All commands in this section assume that you are in the /app directory of the container.

The automatic mode allows you to run a tool without knowing all the command line arguments. You can specify the tool by name:version and the property by name.

Let us again run CPAchecker on the example-safe.c file. This time we know that we want to check for a the unreach-call property. The unreach-call property instructs the verifier to check if a special function, called reach_error(), is reachable in the supplied program file.

To get rid of leftover files from the previous run, clean up the output directory:

$ rm -r output

$ fm-weck run cpachecker:2.3.1 --property unreach-call examples/example-safe.c
INFO:httpx:HTTP Request: GET https://zenodo.org/api/records/11074229 "HTTP/1.1 200 OK"
tool_module:  benchexec.tools.cpachecker
INFO:fm_weck.engine:Running: ['podman', 'run', '--entrypoint', '[""]', '--cap-add', 'SYS_ADMIN', '-v', '/app:/home/cwd', '-v', '/root/.cache/weck_cache:/home/weck_cache', '-v', '/tmp/tmp1soytyaofm_weck_output:/home/output', '--workdir', '/home/cwd', '--rm', 'registry.gitlab.com/sosy-lab/software/cpachecker:2.3.1', '/home/weck_cache/.scripts/run_with_overlay.sh', 'CPAchecker-2.3.1', './scripts/cpa.sh', '-svcomp24', '-heap', '10000M', '-benchmark', '-timelimit', '900 s', '-stats', '-spec', PosixPath('/home/weck_cache/.properties/unreach-call.prp'), '-64', 'examples/example-safe.c']
Running CPAchecker with Java heap of size 10000M.
Running CPAchecker with default stack size (1024k). Specify a larger value with -stack if needed.
Language C detected and set for analysis (CPAMain.detectFrontendLanguageIfNecessary, INFO)

Using the following resource limits: CPU-time limit of 900s (ResourceLimitChecker.fromConfiguration, INFO)

CPAchecker 2.3.1 / svcomp24 (OpenJDK 64-Bit Server VM 17.0.11) started (CPAchecker.run, INFO)

[!snip]

Time for Garbage Collector:       0.016s (in 4 runs)
Garbage Collector(s) used:    G1 Old Generation, G1 Young Generation

Verification result: TRUE. No property violation found by chosen configuration.
More details about the verification run can be found in the directory "./output".

CPAchecker again produced the verification result TRUE, meaning it could prove the property. If we take a look at the output directory, we see that it now contains the output of the automatic run:

$ ls output
witness.graphml  witness.yml

A closer inspection of the automatic run

NOTE
This section does a little detour into the inner workings of fm-weck. If you just want to use fm-weck, or test the artifact, this section can be skipped.

Comparing how CPAchecker was called in the expert and automatic mode vs. the automatic mode, we see that the automatic mode there are more arguments passed to CPAchecker. This is because the automatic mode adds the arguments recommended by the tool developers to the command line.

Peeking at the cpachecker.yml configuration file, we see that version 2.3.1 of CPAchecker recommends the arguments -svcomp24, -heap 10000M, -benchmark, and -timelimit 900 s.

versions:
  - version: "2.3.1"
    doi: 10.5281/zenodo.11074229
    benchexec_toolinfo_options: ["-svcomp24", "-heap", "10000M", "-benchmark", "-timelimit", "900 s"]
    required_ubuntu_packages:
      - openjdk-17-jdk-headless
    base_container_images:
      - docker.io/ubuntu:22.04
    full_container_images:
      - registry.gitlab.com/sosy-lab/software/cpachecker:2.3.1

This is reflected in the command line arguments passed to CPAchecker in the automatic mode:

# Expert mode
INFO:root:Running: [ !snip ..., '/home/weck_cache/CPAchecker-2.3.1/scripts/cpa.sh', '-default', 'examples/example-safe.c']
# Automatic mode
INFO:root:Running: [ !snip ..., './scripts/cpa.sh', '-svcomp24', '-heap', '10000M', '-benchmark', '-timelimit', '900 s', '-stats', '-spec', PosixPath('/home/weck_cache/.properties/unreach-call.prp'), '-64', 'examples/example-safe.c']

We can see another difference in the output of the two runs:

• the expert run just calls the executable of the tool, in this case cpa.sh, with an absolute path to the the executable.

• while the automatic run calls the executable relative to the root of the tool directory (/home/weck_cache/CPAchecker-2.3.1), in this case ./scripts/cpa.sh.

In fact the automatic mode uses a script run_with_overlay.sh to overlay the tool directory over the current working directory inside the container. This allows fm-weck to also run the many tools that rely on being called from their root directory. One of those – UAutomizer – will be executed in the next section.

Running a different tool

So far we have only run CPAchecker. We now demonstrate, that it is super simple to run other tools from the fm-tools repository.

1. We run UAutomizer on the example-safe.c file:

If you want to compare the output of your run with the expected output further down, you can run:

$ rm -r output

$ fm-weck run uautomizer:svcomp24 --property unreach-call examples/example-safe.c
INFO:httpx:HTTP Request: GET https://zenodo.org/api/records/10203545 "HTTP/1.1 200 OK"
tool_module:  benchexec.tools.ultimateautomizer
WARNING:root:Cannot determine ./Ultimate.py version, error output: /root/.cache/weck_cache/UAutomizer-svcomp24/./Ultimate.py:61: SyntaxWarning: invalid escape sequence '\s'
  "^\s*CHECK\s*\(\s*init\s*\((.*)\)\s*,\s*LTL\((.*)\)\s*\)\s*$", re.MULTILINE
/root/.cache/weck_cache/UAutomizer-svcomp24/./Ultimate.py:63: SyntaxWarning: invalid escape sequence '\s'
  funid_regex = re.compile("\s*(\S*)\s*\(.*\)")
/root/.cache/weck_cache/UAutomizer-svcomp24/./Ultimate.py:64: SyntaxWarning: invalid escape sequence '\W'
  word_regex = re.compile("\b[^\W\d_]+\b")

INFO:fm_weck.engine:Running: ['podman', 'run', '--entrypoint', '[""]', '--cap-add', 'SYS_ADMIN', '-v', '/app:/home/cwd', '-v', '/root/.cache/weck_cache:/home/weck_cache', '-v', '/tmp/tmp3x1mcm2xfm_weck_output:/home/output', '--workdir', '/home/cwd', '--rm', 'registry.gitlab.com/sosy-lab/benchmarking/competition-scripts/user:2024', '/home/weck_cache/.scripts/run_with_overlay.sh', 'UAutomizer-svcomp24', './Ultimate.py', '--spec', PosixPath('/home/weck_cache/.properties/unreach-call.prp'), '--file', 'examples/example-safe.c', '--full-output', '--architecture', '64bit']
Checking for ERROR reachability
Using default analysis
Version 0e0057cc
Calling Ultimate with: /usr/lib/jvm/java-1.11.0-openjdk-amd64/bin/java -Dosgi.configuration.area=/home/_cwd/data/config -Xmx15G -Xms4m -jar /home/_cwd/plugins/org.eclipse.equinox.launcher_1.5.800.v20200727-1323.jar -data @noDefault -ultimatedata /home/_cwd/data -tc /home/_cwd/config/AutomizerReach.xml -i examples/example-safe.c -s /home/_cwd/config/svcomp-Reach-64bit-Automizer_Default.epf --cacsl2boogietranslator.entry.function main --witnessprinter.witness.directory /home/_cwd --witnessprinter.witness.filename witness --witnessprinter.write.witness.besides.input.file false --witnessprinter.graph.data.specification CHECK( init(main()), LTL(G ! call(reach_error())) )

 --witnessprinter.graph.data.producer Automizer --witnessprinter.graph.data.architecture 64bit --witnessprinter.graph.data.programhash 63b4a5254a86dd212025f3e9aec65d99d090a4eb0087d6a42e6ba5c8a1987f15
--- Real Ultimate output ---
This is Ultimate 0.2.4-dev-0e0057c
[!snip]
--- End real Ultimate output ---

Execution finished normally
Writing output log to file Ultimate.log
Result:
TRUE

UAutomizer also produced the verification result TRUE, meaning it could prove the property. Additionally, the output directory contains the witness:

$ ls output
Ultimate.log  witness.graphml  witness.yml

2. We run UAutomizer on the AdditionIntMax.i file to check for the no-overflow property:

$ fm-weck run uautomizer:svcomp24 --property no-overflow examples/AdditionIntMax.i
INFO:httpx:HTTP Request: GET https://zenodo.org/api/records/10203545 "HTTP/1.1 200 OK"
tool_module:  benchexec.tools.ultimateautomizer
WARNING:root:Cannot determine ./Ultimate.py version, error output: /root/.cache/weck_cache/UAutomizer-svcomp24/./Ultimate.py:61: SyntaxWarning: invalid escape sequence '\s'
  "^\s*CHECK\s*\(\s*init\s*\((.*)\)\s*,\s*LTL\((.*)\)\s*\)\s*$", re.MULTILINE
/root/.cache/weck_cache/UAutomizer-svcomp24/./Ultimate.py:63: SyntaxWarning: invalid escape sequence '\s'
  funid_regex = re.compile("\s*(\S*)\s*\(.*\)")
/root/.cache/weck_cache/UAutomizer-svcomp24/./Ultimate.py:64: SyntaxWarning: invalid escape sequence '\W'
  word_regex = re.compile("\b[^\W\d_]+\b")

INFO:root:Running: ['podman', 'run', '--entrypoint', '[""]', '--cap-add', 'SYS_ADMIN', '-v', '/home/wachowitz/Projects/fm-weck/doc:/home/cwd', '-v', '/home/wachowitz/.cache/weck_cache:/home/weck_cache', '--workdir', '/home/cwd', '--rm', 'registry.gitlab.com/sosy-lab/benchmarking/competition-scripts/user:2024', '/home/weck_cache/.scripts/run_with_overlay.sh', 'UAutomizer-svcomp24', './Ultimate.py', '--spec', PosixPath('/home/weck_cache/.properties/no-overflow.prp'), '--file', 'examples/AdditionIntMax.i', '--full-output', '--architecture', '64bit']
Checking for overflows
Using default analysis
Version 0e0057cc
Calling Ultimate with: /usr/lib/jvm/java-1.11.0-openjdk-amd64/bin/java -Dosgi.configuration.area=/home/_cwd/data/config -Xmx15G -Xms4m -jar /home/_cwd/plugins/org.eclipse.equinox.launcher_1.5.800.v20200727-1323.jar -data @noDefault -ultimatedata /home/_cwd/data -tc /home/_cwd/config/AutomizerReach.xml -i examples/AdditionIntMax.i -s /home/_cwd/config/svcomp-Overflow-64bit-Automizer_Default.epf --cacsl2boogietranslator.entry.function main --witnessprinter.witness.directory /home/_cwd --witnessprinter.witness.filename witness --witnessprinter.write.witness.besides.input.file false --witnessprinter.graph.data.specification CHECK( init(main()), LTL(G ! overflow) )

 --witnessprinter.graph.data.producer Automizer --witnessprinter.graph.data.architecture 64bit --witnessprinter.graph.data.programhash 17515b65d583c44dcb7e235e0e9227ff5f3e328b2b111df737a68b768cd4ce6e
--- Real Ultimate output ---
This is Ultimate 0.2.4-dev-0e0057c
[!snip]
--- End real Ultimate output ---

Execution finished normally
Writing output log to file Ultimate.log
Writing human readable error path to file UltimateCounterExample.errorpath
Result:
FALSE(OVERFLOW)

UAutomizer produced the verification result FALSE(OVERFLOW), meaning it could not prove the property and there is and integer overflow in the program. The output directory contains the counter example:

$ ls output
UltimateCounterExample.errorpath  Ultimate.log  witness.graphml  witness.yml

Working with local configuration

We have seen automatic and expert runs of fm-weck with two analyzers that have all necessary information available in fm-data, CPAchecker and UAutomizer. It is also possible to execute analyzers that have an SV-COMP archive, but miss the fm-data information. We show this on the example of the static analysis tool ‘Goblint’ Goblint is a static analysis tool that can be used to check for integer overflows.

3. We run goblint on the AdditionIntMax.i file to check for the no-overflow property:

$ fm-weck run goblint:svcomp24 --property no-overflow examples/AdditionIntMax.i
INFO:httpx:HTTP Request: GET https://zenodo.org/api/records/10202867 "HTTP/1.1 200 OK"
INFO:httpx:HTTP Request: GET https://gitlab.com/sosy-lab/software/benchexec/-/raw/main/benchexec/tools/goblint.py "HTTP/1.1 200 OK"
tool_module:  .goblint
ERROR:root:
No image specified in the fm-tool yml file for goblint.
There is currently no configuration file found in the search path.
The search order was 
.weck
/root/.weck
/root/.config/weck
/root/.config/weck/config.toml
Please specify an image in the fm-tool yml file or add a configuration.

To add a configuration you can do the following (on POSIX Terminals):

printf "[defaults]\nimage = your_image" > .weck

Replace 'your_image' with the image you want to use.

OH NO! there is not yet an image specified for Goblint in the fm-tools repository. The error message also tells us how to fix this: we can specify an image in a configuration file.

Let’ create a configuration file for fm-weck. Goblint took part in SV-COMP 2024, so we can assume, that it runs in the SV-COMP 2024 environment. The SV-COMP 2024 image is registry.gitlab.com/sosy-lab/benchmarking/competition-scripts/user:2024.

$ printf '[defaults]\nengine="podman"\nimage = "registry.gitlab.com/sosy-lab/benchmarking/competition-scripts/user:2024"' > .weck

Now we can rerun the command:

$ fm-weck run goblint:svcomp24 --property no-overflow examples/AdditionIntMax.i
tool_module:  .goblint
--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
[!snip]
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1

Goblint produced the verification result unknown, meaning it could not prove the property. This is expected: The automatic mode uses the svcomp24 configuration for Goblint, which will not produce errors.

Running an interactive shell

To enter an interactive shell inside the container, you can run:

$ fm-weck shell cpachecker:2.3.1
INFO:root:Running: ['podman', 'run', '--entrypoint', '[""]', '--cap-add', 'SYS_ADMIN', '-v', '/home/wachowitz/Projects/fm-weck/doc:/home/cwd', '-v', '/home/wachowitz/.cache/weck_cache:/home/weck_cache', '--workdir', '/home/cwd', '--rm', '-it', 'registry.gitlab.com/sosy-lab/software/cpachecker:2.3.1', '/bin/bash']
root@62e2a8fcca5a:/home/cwd# ls
README.md  examples  fm-tools  output  pyproject.toml  src

This will start an interactive shell inside the container with the CPAchecker image. The current directory is mounted to /home/cwd in the container, which is also the working directory.

NOTE The next step will only work if you have completed Example 3 of ‘Runing a different tool’ (Goblint) and have created a configuration file.

You can also start an interactive shell just from the configuration file:

$ fm-weck shell
root@ba9a6acc5552:/home/cwd# 

This will start an interactive shell inside the container with the image specified in the configuration file.