<!--
This file is part of fm-weck: executing fm-tools in containerized environments.
https://gitlab.com/sosy-lab/software/fm-weck

SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>

SPDX-License-Identifier: Apache-2.0
-->

# Tutorial

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 and via local installation.


## Installing fm-weck with pip (recommended)

To install fm-weck, you need to have Python 3.10 or higher installed on your system.
You can install fm-weck via pip:

```bash
pip install fm-weck
```

You can then run fm-weck via the command line:

```bash
fm-weck --help
```

### Installing podman

fm-weck uses [podman](https://podman.io/) to run tools inside a container. 
On Ubuntu you can install podman via the following command:

```bash
sudo apt install podman
```

## Running fm-weck with Docker

We also provide a Docker image for fm-weck. This image already contains podman and fm-weck installed. It's working directory is `/app`.

### Pulling the Docker image from Gitlab

You can pull the fm-weck docker image from the Gitlab registry:

```bash
docker pull registry.gitlab.com/sosy-lab/software/fm-weck:latest
```

To make the tutorial easier to read we will tag this image with a shorter name:

```bash
docker tag registry.gitlab.com/sosy-lab/software/fm-weck:latest fm-weck
```

### Convenience Setup (Optional)

fm-weck downloads tools and caches them. However, every time you run fm-weck via the container, the cache is lost,
and the tools are downloaded again. To avoid this, you can mount a volume to the container. By default fm-weck caches
tools in `/root/.cache/weck_cache` inside of the container. You can mount a volume to this directory to persist the cache.
Mounting a volume works with the `-v` flag. For example, to mount the cache to `/path/to/cache` on your host system, you can run:

```bash
docker run -v /path/to/cache:/root/.cache/weck_cache fm-weck --help
```
The cache is mounted to `/root/.cache/weck_cache` in the container. This is where the
installed fm-weck expects the cache to be. The `--help` command is just an example command to show that the container is working.
It prints the help message of fm-weck.


We provide a convenience script to run fm-weck with the caches mounted.
To use it, just source the `doc/convenient_docker.sh` script:

```bash
source doc/convenient_docker.sh
```

> **NOTE**    
> This still does not cache the images used by podman. Caching these images may
> lead to problems on some system configurations, such as using zfs or btrfs. 
> We recommend entering the container with an interactive shell instead.

#### Caching the podman images between runs

If you wish to run multiple commands that potentially share the same container image,
we recommend entering the container with an interactive shell:

```bash
docker run --privileged -it --rm -v $PWD:/home --workdir /home --entrypoint /bin/bash fm-weck
```
This command starts an interactive shell in the container. 
Your current directory is mounted to `/home` in the container.
You will start in the `/home` directory in the container.
You can then run fm-weck commands inside the container.

#### Alternative: start / stop weck container

The `convenient_docker.sh` also comes with the `start_weck_container` and `stop_weck_container` functions.
These functions start and stop the container in the background.
The current directory at the time of starting the container is mounted once to the container at the moment of starting it.
You will see output similar to the following:

```bash
$ start_weck_container
10f4736c43943e3b94b3ec4285838713d43bd9e360747ce89a001e9edddd7657
$ fm-weck --help
usage: fm-weck [-h] [--version] [--config CONFIG] [--loglevel LEVEL] [--logfile LOGFILE] [--list] [--dry-run]
               {run,r,expert,e,m,shell,install,i,runexec} ...

fm-weck

positional arguments:
  {run,r,expert,e,m,shell,install,i,runexec}
    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.
    runexec             Run runexec on a command inside a container.

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 LEVEL      Set the log level. Valid values are: debug, info, warning, error, critical
  --logfile LOGFILE     Path to the log file.
  --list                List all fm-tools that can be called by name.
  --dry-run             Just print the command that would be executed.
$ stop_weck_container
fm_weck
```


## Your first fm-weck run

> **NOTE**  
> From now on we will refer to fm-weck as `fm-weck` for brevity.
> If you are using the convenience script, are inside the container, or installed fm-weck via pip these commands will work as is.
> If you are using the docker image directly, you need to prepend `--privileged` to the docker commands, such that podman works inside the container.

To get an overview of the available commands run:

```bash
$ fm-weck --help
usage: fm-weck [-h] [--version] [--config CONFIG] [--loglevel LEVEL] [--logfile LOGFILE] [--list] [--dry-run]
               {run,r,expert,e,m,shell,install,i,runexec} ...

fm-weck

positional arguments:
  {run,r,expert,e,m,shell,install,i,runexec}
    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.
    runexec             Run runexec on a command inside a container.

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 LEVEL      Set the log level. Valid values are: debug, info, warning, error, critical
  --logfile LOGFILE     Path to the log file.
  --list                List all fm-tools that can be called by name.
  --dry-run             Just print the command that would be executed.
```

To get an overview of the available tools run:

```bash
$ 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 has three modes of operation: the automatic (run) mode, the manual (expert) mode and interactive (shell) 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:

```bash
$ fm-weck m cpachecker -version
INFO:httpx:HTTP Request: GET https://zenodo.org/api/records/11074229 "HTTP/1.1 200 OK"
tool_module:  benchexec.tools.cpachecker
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/software/cpachecker:2.3.1', PosixPath('/home/weck_cache/CPAchecker-2.3.1/scripts/cpa.sh'), PosixPath('-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)
```
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**  
> Depending on your system podman might print an error message similar to
> ```shell
> 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.


**Assuming you are in the `doc` directory** of the fm-weck repository, you can run:

```bash
$ fm-weck m 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: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/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.
JVM property file.encoding is set to non-standard value 'ANSI_X3.4-1968'. This is not recommended and output files might be written in unexpected encodings. (CPAMain.main, WARNING)
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".

$ 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
```
CPAchecker produced the verification result TRUE, meaning it could prove the property 
(here: the default that was set by the CPAchecker developers) valid.

Let's clean up the output directory:

```bash
rm -r output
```


## Running a tool in automatic mode

> **NOTE**  
> All commands in this section assume that you are in the `/app` directory of the container or the `/doc` directory of the fm-weck repository if running locally.

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:
```shell
$ rm -r output
```

```bash
$ 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:

```bash
$ 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 mode vs. the automatic mode, we see that in 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](https://gitlab.com/sosy-lab/benchmarking/fm-tools/-/blob/main/data/cpachecker.yml) configuration file, we see that
version 2.3.1 of CPAchecker recommends the arguments `-svcomp24`, `-heap 10000M`, `-benchmark`, and `-timelimit 900 s`.

```yaml
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:

```bash
# 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](https://gitlab.com/sosy-lab/benchmarking/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:

```shell
$ rm -r output
```

```bash
$ 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"
INFO:httpx:HTTP Request: GET https://zenodo.org/api/records/10203545/files/uautomizer.zip/content "HTTP/1.1 200 OK"
129860KiB [00:04, 31412.89KiB/s]                                                                                                                                              
INFO:httpx:HTTP Request: GET https://zenodo.org/api/records/10203545 "HTTP/1.1 200 OK"
tool_module:  benchexec.tools.ultimateautomizer
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/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:

```bash
$ ls output
data  Ultimate.log  witness.graphml  witness.yml
```

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

```bash
$ 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
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:

```bash
$ ls output
data  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:

```bash
$ 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://zenodo.org/api/records/10202867/files/goblint.zip/content "HTTP/1.1 200 OK"
22908KiB [00:11, 1927.71KiB/s]
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"
ERROR:fm_weck.cli:
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
.fm-weck
/home/<your home>/.fm-weck
/home/<your home>/.config/fm-weck
/home/<your home>/.config/fm-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>"' > .fm-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`.


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

Now we can rerun the command:

```bash
$ fm-weck run goblint:svcomp24 --property no-overflow examples/AdditionIntMax.i
tool_module:  .goblint
[!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.
The automatic mode uses the svcomp24 configuration for Goblint, which will not produce errors 
and instead returns unknown whenever it cannot prove the property.

## Running an interactive shell

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

```bash
$ fm-weck shell cpachecker:2.3.1
root@62e2a8fcca5a:/home/cwd# ls
convenient_docker.sh  examples  output  README-Artifact.md  shell-completion-setup.md  Tutorial.md
root@62e2a8fcca5a:/home/cwd# exit
exit
```
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:

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

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

## Installing tools for later use

fm-weck can download and cache tools for later use.
If you want to install goblint, cpachecker and cbmc for later use, you can run:

```bash
$ fm-weck install goblint cpachecker cbmc
```