Benchexec

- One tool-info module improved.

- BenchExec is now available in a PPA for easy installation on Ubuntu.
Just run the following commands

sudo add-apt-repository ppa:sosy-lab/benchmarking
sudo apt install benchexec

- Column filters are now reflected in the URL of HTML tables.
This makes it possible to open a table, configure some filters,
and share a link with others that will apply these filters on load.
Furthermore, using the back and forward buttons of the browser
will now also update the applied filters.
- Add parameter `--initial-table-state` to `table-generator`,
which allows to define the default state of HTML tables
(e.g., filters, opened tab, etc.).
- Category-specific statistics are shown more often again on first table tab.
Since BenchExec 3.0 these were removed in some cases where we cannot compute
them, but this accidentally removed them from more than the desired cases.
- Improved rounding in table-generator.
- SV-COMP scoring schema updated according to rules of SV-COMP'21.
- Many tool-info modules updated to use the new API from BenchExec 3.3
and improvements for SV-COMP'21 and Test-Comp'21.
- Improved warnings in certain cases where a benchmark definition
does not make sense (e.g., `<exclude>` tags that do not match anything).
- HTML tables now show a proper error message if the browser is not supported
and also a loading message.
- Several smaller bug fixes like avoiding crashes in corner cases.

- New API for tool-info modules (needed by `benchexec` for getting information
about the benchmarked tool). The new API is defined by class
[`benchexec.tools.template.BaseTool2`](https://github.com/sosy-lab/benchexec/blob/master/benchexec/tools/template.py)
and is similar to the old API, but more convenient to use and provides more
useful information to the tool-info module.
The old API is still supported
and will be removed no sooner than in BenchExec 4.0. We also provide a
[migration guide](https://github.com/sosy-lab/benchexec/blob/master/doc/tool-integration.md#migrating-tool-info-modules-to-new-api).
- A new parameter `--tool-directory` for `benchexec` allows to specify
the installation directory of the benchmarked tool easily
without having to modify `PATH` or change into the tool's directory.
Note that this only works if the respective tool-info module
makes use of the new `BaseTool2` API.
- New version 2.0 of the
[task-definition format](https://github.com/sosy-lab/benchexec/blob/master/doc/benchexec.md#task-definition-files)
for `benchexec`.
This format allows to specify arbitrary additional information in a key
named `options` and `benchexec` will pass everything in this key
to the tool-info module, but note that this only works
if the respective tool-info module makes use of the new `BaseTool2` API.
This is useful to add domain-specific information about tasks, for example
in the [SV-Benchmarks](https://github.com/sosy-lab/sv-benchmarks#task-definitions)
repository it is used to declare the program language.
BenchExec also still supports version 1.0 of the format.

- `table-generator` is now defined to work on Windows
and we test this in continuous integration.
Previously, it probably was working on Windows most of the time
but we did not systematically test this.
- Fix a crash in `benchexec` for task with property
but without task-definition file.

- The HTML tables produced by `table-generator` now provide a score-based
quantile plot in addition to the regular quantile plot if scores are used.
If available, it is shown by default on the tab for quantile plots.
Score-based quantile plots are for example used by SV-COMP to visualize results.
- Better axis labels in scatter plot of HTML tables.
- More auxiliary lines available in scatter plot of HTML tables.
- New tool-info module added.

Bug fixes:

- Fix crash in `benchexec` if a non-SV-COMP property was used.
- Fix for empty property files being treated as SV-COMP properties.
- Fix unnecessarily large I/O for text file with results of `benchexec`
during benchmarking. The `.results.txt` file is now written incrementally.
- Fix incorrect handling of `<withoutfile>` tasks if the tool-info module
declared a non-standard working directory.
- Small fix for the new filter overlay in the HTML tables
when the first run set has no filter.

- Fix our `benchexec.check_cgroups` installation check,
which showed invalid warnings since BenchExec 2.7.
- Improve handling of inaccessible mountpoints in containers.
This should make it possible to use nested containers on most systems
using the default arguments (e.g., no need for `--hidden-dir /sys`).
- Improved row filters of HTML tables (thanks to [DennisSimon](https://github.com/DennisSimon)).
In addition to filtering via drop-down fields in the table header,
it is now also possible to define filters on a separate overlay,
which can be opened from all tabs via a button in the top-right corner
(e.g., also while looking at plots).
The filters for status and category in the filter overlay are more flexible
because several values can be selected for status and category.
This allows to define filters like
`category = "correct" AND (status = "false" OR status = "false(unreach-call)")`.
Furthermore, the filter overlay allows to filter the parts of the task id
(left-most column) individually and makes it easier to define filters
with numeric ranges.
- Redesigned UI for changing the plot settings of quantile and scatter plots
in the HTML tables (thanks to [lachnerm](https://github.com/lachnerm)).
- Hiding columns in HTML tables is now reflected in the URL.
This makes it possible to create links to tables that hide columns.

This release contains only one new feature compared to BenchExec 2.7:

- Tables produced by `table-generator` now show the expected verdict of each task,
if it is known and it is not the same for all rows.

However, there are several deprecated features removed
and other backwards-incompatible changes
to make BenchExec more consistent and user-friendly:

- Support for Python 2.7 and 3.4 is removed,
the minimal Python version is now 3.5 for all components of BenchExec.
We plan to remove support for Python 3.5
after Ubuntu 16.04 goes out of support in 2021.
- If a tool-info module returns `UNKNOWN` for a run result,
BenchExec will no longer overwrite that if it thinks the tool terminated
abnormally. It will continue to do so if `ERROR` is returned.
- Result values named `cpuenergy-pkg[0-9]+` are renamed to `cpuenergy-pkg[0-9]+-package`
because these are not a sum of all the other CPU-energy measurements.
- Names of result files produced by `benchexec` now contain timestamps
with seconds in order to avoid problems when starting `benchexec`
in quick succession.
- Support for generating the old-style static HTML tables
(with `table-generator --static-table`) is removed.
Only the modern tables that are available since BenchExec 2.3
and CSV tables can be generated.
- More metadata are stored in result files of `benchexec`,
so `table-generator` no longer needs access to the task-definition files,
and changes to the expected verdict that are made after benchmarking
will not be reflected in tables.
- The Python library Tempita is no longer a dependency of BenchExec.
- We do not create and distribute `.egg` packages for BenchExec releases anymore,
only the more modern `.whl` packages,
as well as Debian/Ubuntu packages and Tar archives.

Furthermore, BenchExec no longer contains hard-coded knowledge about any specific property,
all properties are treated in the same way.
(The only exception is that score computation is enabled for SV-COMP properties.)
This simplification implies several more changes:

- For checking expected verdicts and computing scores it is now required that
task-definition files are used.
Expected verdicts encoded in the task name are no longer supported.
- Tool-info modules need to return results `true` or `false`,
the results `sat` and `unsat` are no longer supported
(these were allowed only for the property `SATISFIABLE`).
- There is no special handling for composite properties like SV-COMP's property
for memory safety anymore. Previously this property would be represented as
a collection of its subproperties, now it is treated as one property.
Task-definition files can still contain a violated subproperty,
and `benchexec` will continue to use this information for checking the tool result,
but this does not depend on which property is used.
- Score computation is fixed for tables where property files have uncommon names.
The name of property files is now no longer relevant (as it should have been).
Because of this, `table-generator` needs to have access to
the property files that were used during benchmarking.