Merge pull request #157 from ftsrg/svcomp22

Merging the SV-COMP'22-related features

build.gradle.kts

@@ -11,7 +11,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.inf.theta"
-    version = "3.0.2"
+    version = "4.0.0"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

doc/CEGAR-algorithms.md

@@ -149,4 +149,13 @@ Available for CFA. The SMT-solver to use during verification. The `--abstraction
 * `Z3`: The native integration of Microsoft's Z3 solver. (See subproject [solver-z3](../subprojects/solver/solver-z3) for more details.)
 * `<solver_name>:<solver_version>`: An installed SMT-LIB solver. (See subprojects [solver-smtlib](../subprojects/solver/solver-smtlib) and [solver-smtlib-cli](../subprojects/solver/solver-smtlib-cli) for more details.)
 
-It is recommended to stick with the default `Z3` option at first, and only use the SMT-LIB based solvers, if some required features are not supported by `Z3` (e.g. interpolating with bitvectors, floating points).
+It is recommended to stick with the default `Z3` option at first, and only use the SMT-LIB based solvers, if some required features are not supported by `Z3` (e.g. interpolating with bitvectors, floating points).
+
+### `--lbe`
+LBE (Large Block Encoding) can be configured the following ways (see further details in the [LBE documentation](LBE.md)):
+
+- `NO_LBE`: Turns off LBE completely
+- `LBE_SEQ`: Only applies sequential collapsing to edges
+- `LBE_FULL`: Applies sequential and parallel collapsing, too.
+
+`LBE_FULL` configuration performs better with predicate abstraction (both boolean and cartesian). `LBE_SEQ` gives better results in almost every case than `NO_LBE`.

doc/LBE.md

@@ -0,0 +1,176 @@
+# **Large Block Encoding**
+
+Authors: Márk Somorjai, Csanád Telbisz
+December 2021
+
+## **Table of contents**
+
+**[Configurations](#Configurations)**
+
+**[Transformation](#Transformation)**
+
+_[Definitions](#Definitions)_
+
+_[Steps](#Steps)_
+
+_[Algorithm](#Algorithm)_
+
+_[Example](#Example)_
+
+**[Implementation](#Implementation)**
+
+
+<a name="Configurations"></a>
+# Configurations
+
+We implemented the algorithm in Java, as a procedural pass in the Theta model checking framework. Passes transform the CFA in different ways, before the verification algorithm can begin. We have opened a pull request, to have our pass be integrated in the framework.
+
+The following configurations can be applied to LBE by setting the `--lbe` flag when running Theta (see the definitions below for further details):
+
+- `NO_LBE`: Turns off LBE completely
+- `LBE_SEQ`: Only collapses snakes and removes middle locations (_see 1st image below_)
+- `LBE_FULL`: Collapses snakes and parallel edges, removes middle locations (_see 2nd image below_)
+
+<p align="center">
+<img src="LBE-images/config_seq.jpg" style="margin-bottom: 15px; max-width: 400px" alt="snake">
+</p>
+
+<p align="center">
+<img src="LBE-images/config_full.jpg" style="margin-bottom: 15px; max-width: 400px" alt="snake">
+</p>
+
+`LBE_FULL` configuration performs better with predicate abstraction (both boolean and cartesian). `LBE_SEQ` gives better results in almost every case than `NO_LBE`. The diagram below illustrates the results of 133 benchmark tests:
+
+<p align="center">
+<img src="LBE-images/results.jpg" style="margin-bottom: 15px; max-width: 400px" alt="snake">
+</p>
+
+A more detailed representation of the test results can be seen on [this quantile plot](LBE-images/quantile_plot.png).
+
+<a name="Transformation"></a>
+## Transformation
+
+The transformation turns a single block encoded CFA into a large block encoded CFA. During the transformation, each loop-free subgraph of the CFA is replaced by a single edge with a larger formula representing the removed subgraph.
+
+<a name="Definitions"></a>
+## Definitions
+
+In order to make the algorithm more understandable, the following definitions were introduced:
+
+**snake:** A graph component, where the incoming and outgoing degree of every location is 1, apart from the two ends of the subgraph.
+
+_Example: nodes {L<sub>1</sub>, L<sub>2</sub>, L<sub>3</sub>, L<sub>4</sub>} and the edges between them form a snake._
+
+<p align="center">
+<img src="LBE-images/LBE-snake.jpg" style="margin-bottom: 15px" alt="snake">
+</p>
+
+**parallel edges:** Edges with the same source and target location.
+
+_Example: edges {e<sub>1</sub>, e<sub>2</sub>, e<sub>3</sub>} are parallel edges._
+
+<p align="center">
+<img src="LBE-images/LBE-parallel%20edges.jpg" style="margin-bottom: 15px" height="150" alt="parallel">
+</p>
+
+**middle location:** A location with an incoming degree of 1 and an outgoing degree that's at least 1.
+
+_Example: L<sub>2</sub> and L<sub>3</sub> are middle locations, while L<sub>1</sub>, L<sub>4</sub> and L<sub>5</sub> are not._
+
+<p align="center">
+<img src="LBE-images/LBE-middle%20location.jpg" style="margin-bottom: 15px; height: 150px;" alt="middle location">
+</p>
+
+<a name="Steps"></a>
+## Steps
+
+Using the definitions above, the algorithm can be divided into 3 main steps:
+
+### 1. Error locations to sinks
+
+To prepare the CFA for transformation, precautionary steps need to be taken to avoid giving wrong results. In this step, all outgoing edges are removed from error locations. This is to make sure they don't disappear later on in the transformation, because locations with in- and outgoing edges could be removed. From a software verification standpoint this step has no effect, since the goal is to determine whether error locations are reachable or not, and outgoing edges do not affect reachability.
+
+### 2. Remove parallel edges and snakes
+
+In this step, all parallel edges and snakes are removed from the CFA. This is done by doing the following 2 operations on all locations where they are applicable, until there is none:
+
+#### a) Collapse outgoing parallel edges into a single edge
+
+The visited location is checked for outgoing edges that go the same target. If found, the parallel edges are removed from the graph. The labels that were on them are combined by the _or_ operator (||), and put on a single edge going from the visited location to the original target location. Example of this can be seen below, with the visited location being L.
+
+<p align="center">
+<img src="LBE-images/collapse%20parallel.jpg" style="margin-bottom: 15px; height: 150px;" alt="collapse parallel">
+</p>
+
+Before the operation, going from the visited location to the target was only possible, if any of the parallel edges&#39; labels were satisfied. This stays true after the transformation thanks to the _or_ operator, thus the original semantics are kept.
+
+#### b) Collapse part of snake into a single edge
+
+If the visited location has a single incoming and outgoing edge, it is part of a snake. In this case, the location is removed. The labels that were on the incoming and outgoing edge are combined by the _and_ operator (, or &&), and put on a single edge going from the incoming edge's source location to the outgoing edge's target location. An example of this can be seen below, with the visited location being L.
+
+<p align="center">
+<img src="LBE-images/collapse%20snake.jpg" style="margin-bottom: 15px; height: 200px;" alt="collapse snake">
+</p>
+
+Before the operation, going from the source of the incoming edge to the target of the outgoing edge was only possible, if both of the incoming and outgoing edges' labels were satisfied. This still is the case after the operation thanks to the semantics of the _and_ operator, therefore the original semantics are kept.
+
+### 3. Remove middle locations
+
+In this step, middle locations are removed from the CFA. If a middle location is found, it is removed. For each outgoing edge from the middle location a new one is created, between the source of the incoming edge of the middle location and the target of the outgoing edge. The labels on incoming and outgoing edges are combined by the _and_ operator (, or &&), and are put on the new edge. An example of this can be seen below, with L being the middle location.
+
+<p align="center">
+<img src="LBE-images/remove%20middle.jpg" style="margin-bottom: 15px; height: 200px;" alt="remove middle location">
+</p>
+
+This step is similar to 2.b), the difference being that here all middle locations are removed, not just parts of snakes. By the same reasoning, going from the source of the incoming edge to the target of the outgoing edge before the operation was only possible, if both of the incoming and outgoing edges' labels were satisfied. This still is the case after the operation thanks to the semantics of the _and_ operator, therefore the original semantics are kept.
+
+<a name="Algorithm"></a>
+## Algorithm
+
+With the steps now defined, the algorithm consists of the following:
+
+- Do step 1 once. This makes sure the error location will not be removed.
+- Do step 2 and 3 repeatedly, as long as any of them can be applied. That is, until there are no more snakes, parallel edges and middle locations in the CFA.
+
+At first glance, the complexity of the algorithm seems exponential due to the fact that doing almost any of steps 2.a), 2.b) and 3. can create new snakes, parallel edges and middle locations, because of which all locations need to be checked again and again. However, all steps remove at least a location or an edge, meaning the number of locations to check decreases. Combined with storing what locations could&#39;ve been affected by the executed steps (further discussed in the implementation section), the algorithmic complexity can be reduced O((N + M) \* M), where N is the number of nodes, M is the number of edges in the CFA.
+
+<a name="Example"></a>
+## Example
+
+```cpp
+void reach_error();
+    int main() {
+    int rand;
+    if (rand) {
+        rand = 1;
+    }
+    if (rand) {
+        reach_error();
+    }
+    return 0;
+}
+```
+
+
+The steps of the transformation are illustrated on an example below. The program and its representative single block encoded CFA are given in the beginning:
+
+<p align="center">
+<img src="LBE-images/LBE_example.jpg" style="margin-bottom: 15px; max-height: 700px;" alt="remove middle location">
+</p>
+
+<a name="Implementation"></a>
+# Implementation
+
+The implementation follows the steps described above closely, the steps are implemented as functions:
+
+- _collapseParallelsAndSnakes_ implements step 2.
+- _collapseParallelEdges_ implements step 2.a)
+- _collapsePartOfSnake_ implements step 2.b)
+- _removeAllMiddleLocation_ implements step 3.
+
+The repeated checking and collapsing happens in functions _removeAllMiddleLocations_ and _collapseParallelsAndSnakes._ To reduce complexity, a list of locations to check for snakes, parallel edges and middle locations is kept and passed around between the functions. By default, all locations are in the list. As the steps get executed repeatedly, only locations that had a parent or a child change get added back to the list, while all visited locations are removed. More specifically, locations that had one of the following happen to them are added to the list and are checked again:
+
+- Parallel edges coming into a location have been collapsed.
+- A location had a part of a snake outgoing from it, which has been collapsed.
+
+This reduces the amount of unnecessary checking done on parts of the CFA that didn't change.

doc/Portfolio.md

@@ -0,0 +1,74 @@
+# Portfolio in Theta
+As Theta is a configurable framework, there is a large amount of possible parameters, mostly configuring the CEGAR analysis. Changing the default values of these parameters requires experience with the analysis and the algorithms, but finding a proper configuration often means the difference between solving or not solving the input.
+
+The main goal of the portfolio is to provide a simple, general way of checking input tasks without the need to care about the configurations by integrating this experience into a complex portfolio with algorithm selection.
+
+For a more advanced user, it also provides the ability to create further portfolios of different configurations based on different decisions and/or a sequential order.
+
+## Usage
+Usage of the portfolio simply happens by using the `--portfolio` flag with a parameter (see below). It overrides other flags, so further configuration is not possible, except the flags controlling the verbosity of the output (e.g. `--loglevel`, `--output-results`).
+
+### Complex (dynamic) portfolio
+*Use `--portfolio COMPLEX` as a parameter to use this portfolio.*
+
+![complex-portfolio-process](portfolio-images/complex-portfolio.png)
+
+The complex portfolio has a global timeout of approximately 900 seconds.
+
+"Based on preliminary experiments and domain knowledge, we manually constructed a dynamic algorithm selection portfolio for SV-COMP'22, illustrated by Figure.
+Rounded white boxes correspond to decision points.
+We start by branching on the arithmetic (floats, bitvectors, integers).
+Under integers, there are further decision points based on the cyclomatic complexity and the number of havocs and variables.
+Grey boxes represent configurations, defining the *solver\domain\refinement* in this order.
+Lighter and darker grey represents explicit and predicate domains respectively.
+Internal timeouts are written below the boxes.
+An unspecified timeout means that the configuration can use all the remaining time.
+The solver can be CVC4 (C), MathSAT (M), MathSAT with floats (Mf) or Z3 (Z).
+Abstract domains are explicit values (E), explicit values with all variables tracked (EA), Cartesian predicate abstraction (PC) or Boolean predicate abstraction (PB).
+Finally, refinement can be Newton with weakest preconditions (N), sequence interpolation (S) or backward binary interpolation (B).
+Arrows marked with a question mark (?) indicate an inconclusive result, that can happen due to timeouts or unknown results.
+Furthermore, this year's portfolio also includes a novel dynamic (run-time) check for refinement progress between iterations that can shut down potential infinite loops (by treating them as unknown result).
+Note also that for solver issues (e.g., exceptions from the solver) we have different paths in some cases."
+
+(figure and description from the [SV-COMP 2022 tool paper](http://ftsrg.mit.bme.hu/paper-tacas2022-theta/paper.pdf))
+
+### Sequential (simple) portfolio
+*Use `--portfolio SIMPLE` as a parameter to use this portfolio.*
+
+The simple sequential portfolio is simply a configuration of three different configurations in a sequential order. Each of the three has a 300 second local timeout.
+The configurations are:
+1. An explicit analysis (mainly for the simpler tasks to finish these as early as possible)
+2. A predicate analysis (mainly for more complex tasks, where explicit analysis fials/gets stuck)
+3. A Newtonian analysis (mainly to handle bitvector arithmetics as well)
+
+The precise parameters of these configurations:
+1. `–domain EXPL –initprec EMPTY –search ERR –encodingLBE –refinement SEQ_ITP –maxenum 1 –precgranularityGLOBAL –prunestrategy LAZY`
+2. `–domain PRED_CART –initprec EMPTY –search ERR–encoding  LBE  –refinement  BW_BIN_ITP  –predsplitWHOLE –precgranularity GLOBAL –prunestrategy LAZY`
+3. `–domain  EXPL  –initprec  EMPTY  –search  ERR  –encoding  LBE  –refinement  NWT_IT_WP  –maxenum1 –precgranularity GLOBAL –prunestrategy LAZY`
+
+### Adding further portfolios
+To create a new concrete portfolio, create a subclass of the `hu.bme.mit.theta.xcfa.analysis.portfolio.common.AbstractPortfolio` class and implement its abstract method `executeAnalysis`. The `AbstractPortfolio` class serves as a utility, in which the execution of any given configuration with a time limit on a separate thread is already implemented in the method `executeConfiguration`.
+
+For further information, see the javadoc and/or the already implemented `ComplexPortfolio` and `SequentialPortfolio` classes.
+
+To enable your portfolio as a parameter, add a new value to `hu.bme.mit.theta.xcfa.analysis.portfolio.Portfolio` and extend `hu.bme.mit.theta.xcfa.cli.XcfaCli` with this value (the corresponding switch statement is around line 422).
+
+## Limitations
+### Limited to XCFA
+The current version of the portfolio was created specifically to verify C programs transformed to the XCFA formalism. In the future it will be available for further formalisms.
+
+### Limitations/Errors due to Threads
+The portfolio executes the analysis on a separate thread as it needs to be able to interrupt in case a time limit is reached. On the other hand, Theta often spends a large amount of time executing and waiting for SMT solvers or on other longer tasks (e.g. building the ARG), which cannot be interrupted quickly. Thus the portfolio is required to use `Thread.stop()`, when an interrupt seems insufficient, while also handling several possible states of the tool (SMT solver process running/in background, etc.). There are possible corner cases, where this might not work properly (the thread or a solver is not stopped properly, gets stuck, etc.). Solving these issues requires a completely new, process-based solution, which is currently under progress - until then, some bugs remain.
+
+### Limited to Linux
+To set and handle time limits, the portfolio has to measure the uptime of different processes (as most solvers are executed as different processes). To achieve that, the utility `ps` is used, which is only available on linux. Thus the portfolio is currently not available on Windows.
+
+## Further Details
+The portfolio was implemented as part of the bachelor's thesis work of Zsófia Ádám, available [here](https://zenodo.org/record/5907927).
+
+The complex portfolio was used on SV-COMP 2022, the resulting tool paper can be found [here](http://ftsrg.mit.bme.hu/paper-tacas2022-theta/paper.pdf).
+
+## Future Plans
+* We are planning on refactoring the portfolio to work with all formalisms and configuraitons of Theta
+* We also plan to introduce configuration files to make the creation of further portfolios easier
+* Theta might go through an architectural refactoring process to create a more modular, portfolio-centric architecture

settings.gradle.kts

@@ -5,6 +5,8 @@ include(
         "common/common",
         "common/core",
 
+        "frontends/c-frontend",
+
         "cfa/cfa",
         "cfa/cfa-analysis",
         "cfa/cfa-cli",
@@ -13,6 +15,11 @@ include(
         "sts/sts-analysis",
         "sts/sts-cli",
 
+        "xcfa/xcfa",
+        "xcfa/xcfa-analysis",
+        "xcfa/xcfa-cli",
+        "xcfa/cat",
+
         "xta/xta",
         "xta/xta-analysis",
         "xta/xta-cli",

subprojects/cfa/cfa-analysis/src/main/java/hu/bme/mit/theta/cfa/analysis/CfaAction.java

@@ -1,5 +1,5 @@
 /*
- *  Copyright 2017 Budapest University of Technology and Economics
+ *  Copyright 2022 Budapest University of Technology and Economics
  *
  *  Licensed under the Apache License, Version 2.0 (the "License");
  *  you may not use this file except in compliance with the License.
@@ -15,19 +15,19 @@
  */
 package hu.bme.mit.theta.cfa.analysis;
 
-import static com.google.common.base.Preconditions.checkArgument;
-import static com.google.common.base.Preconditions.checkNotNull;
-
-import java.util.Collections;
-import java.util.List;
-import java.util.stream.Collectors;
-
 import hu.bme.mit.theta.analysis.expr.StmtAction;
 import hu.bme.mit.theta.cfa.CFA.Edge;
 import hu.bme.mit.theta.cfa.CFA.Loc;
 import hu.bme.mit.theta.common.Utils;
 import hu.bme.mit.theta.core.stmt.Stmt;
 
+import java.util.Collections;
+import java.util.List;
+import java.util.stream.Collectors;
+
+import static com.google.common.base.Preconditions.checkArgument;
+import static com.google.common.base.Preconditions.checkNotNull;
+
 public final class CfaAction extends StmtAction {
 
 	private final List<Edge> edges;