Verification back ends such as SMT solvers are typically highly complex pieces of software with performance, correctness and robustness as key requirements. Full verification of SMT solvers, however, is difficult due to their complex nature and still an open question. Grammar-based black-box input fuzzing proved to be effective to uncover bugs in SMT solvers but is entirely input-based and restricted to a certain input language. State-of-theart SMT solvers, however, usually provide a rich API, which often introduces additional functionality not supported by the input language. Previous work showed that applying model-based API fuzzing to SAT solvers is more effective than input fuzzing. In this paper, we introduce a model-based API testing framework for our SMT solver Boolector. Our experimental results show that model-based API fuzzing in combination with delta debugging techniques is effective for testing SMT solvers.
of the error in a time efficient manner. Applying this approach to the SAT solver Lingeling [
In this paper, based on the results in [
The core test case generation engine in our model-based testing framework is our model-based
API testing tool BtorMBT, which implements a model of Boolector’s API and generates valid
sequences of API calls. In case that one of these sequences causes an error, Boolector
generates an API error trace, which allows to replay and reproduce faulty behaviour with our trace
execution tool BtorUntrace. Our delta debugging tool ddMBT then minimizes such an API
error trace while preserving its fault-inducing characteristics when replayed with BtorUntrace.
Figure 1 describes the general workflow of our framework and its components as follows.
Data Model Boolector, our system under test, is an SMT solver for the quantifier-free
theory of fixed-size bit-vectors, arrays, and uninterpreted functions as defined in the SMT-LIB
v2 [
API Model Boolector provides a rich public API with full access to the complete feature set of the solver. It is available in C and Python, but since both BtorMBT and BtorUntrace, which tightly integrate Boolector via its API, are written in C, we will in the following focus on Option Model
Data Model API Model
API
Error Trace BtorMBT
API
Boolector
API
BtorUntrace ddMBT
Minimized API
Error Trace its C API, which consists of more than 150 API functions. Figure 2 illustrates the API model of Boolector as implemented in BtorMBT. It incorporates Boolector’s option model and the data model as above, and will be described in more detail in Section 3.
BtorMBT Our model-based API testing tool BtorMBT generates test cases as valid sequences of calls to Boolector’s API and implements the API model illustrated in Fig. 2. It aims to exploit the full feature set of Boolector as available via its API. In case of an error, Boolector generates an API error trace, which can then be replayed with our trace execution tool BtorUntrace. Note that delegating API tracing to the solver assumes that it traces API sequences correctly. Within our model-based API testing workflow it would therefore be more reliable to let BtorMBT do the tracing, which we leave to future work. However, API tracing as provided by the solver itself is still a valuable feature since it allows to reproduce erroneous behavior outside of our test framework without the need for the original setup of the tool chain that triggered the error. We will describe BtorMBT in more detail in Section 3. API Error Trace Boolector provides the possibility to trace all API calls with their arguments into a dedicated trace file. Given such an API trace, the trace execution tool BtorUntrace then replays the sequence of API calls listed in the trace file and reproduces undesired behavior in case of an error. An example of an API trace generated by Boolector is given in Fig. 3. We will describe API tracing and the trace in Fig. 3 in Section 4 in more detail. BtorUntrace The trace execution tool BtorUntrace allows to replay a sequence of API calls given an API trace file as above. We will describe BtorUntrace in Section 4 in more detail. ddMBT Given an API Error trace file which logs a sequence of API calls leading to undesired behavior of Boolector, the delta debugger ddMBT minimizes the API trace while preserving this behavior reproduced via BtorUntrace. We will describe ddMBT in more detail in Section 5. 3
Our model-based API tester BtorMBT is a dedicated tool for testing random configurations
of Boolector. It is explicitly tailored to Boolector and supports the quantifier-free theories of
fixed-size bit-vectors, arrays and uninterpreted functions, extended with non-recursive
firstorder lambda terms. BtorMBT serves as the test case generation engine in our model-based
testing workflow and fully supports all functionality provided by Boolector via its API. In
contrast to input fuzzers such as FuzzSMT [
Note that Boolector makes heavy use of runtime assertions and provides means to internally
check key features of the solver. This includes model validation for satisfiable instances, checking
the inconsistency of the set of inconsistent assumptions (also called failed assumptions [
The general architecture of BtorMBT is defined by a state machine implementing the data, options and API Model of Boolector as illustrated in Fig. 2. Test case generation with BtorMBT is performed in rounds, each with a different configuration of Boolector. One round corresponds to a sequence of states from state New to state Delete and the states are defined as follows. New In each round, a fresh instance of Boolector is generated. Further, all parameters that influence formula size and structure such as probability distributions and maximum numbers for generating and releasing expressions are (re)initialized with random values (within certain ranges).
Set Options Boolector provides multiple solver engines, with some of them relying on an
underlying SAT solver. As back-end SAT solver, Boolector supports the solvers Lingeling [
Generate Initial Expressions After a new Boolector configuration and all parameters that influence the formula size and structure have been set up, an initial set of inputs and non-input expressions is generated. The set of inputs is divided into randomly sized shares of uninterpreted functions, array variables, and Boolean and bit-vector constants and variables. Non-input expressions are randomly generated by combining inputs and already existing noninput expressions until the maximum number of non-input expressions is reached. Note that in case that the chosen solver engine only supports the quantifier-free theory of fixed-size bitvectors, only bit-vector expressions are generated.
Main After generating an initial set of expressions, in state Main a random number of operations that influence the structure of the input formula is performed in random order: (1) new expressions are generated, (2) existing expressions are released, (3) and existing Boolean expressions are added to the input formula as assertions and, in the incremental case, assumptions. Note that when selecting expressions to generate new non-input expressions, in order New
Set Options Delete
Dump Formula Query Model sat Assignments incremental
Generate Initial
Expressions
Main Sat incremental Reset for Incremental Usage to increase expression depth, expressions from the initial set are chosen with lower probability. After finalizing the current input formula, BtorMBT randomly performs various operations that operate on the current state of the input formula and possibly manipulate the current state of the Boolector instance e.g., simplifying the input formula by means of rewriting and other techniques, or generating a clone of the current Boolector instance. Next, BtorMBT randomly picks between dumping the input formula (state Dump Formula) or determining its satisfiability (state Sat). Note that the latter is chosen with higher probability.
Dump Formula Boolector allows to dump the current state of the input formula (without
assumptions) anytime during the solving process and supports BTOR [
Sat After setting up the current input, a call to determine its satisfiability is issued.
Boolector supports incremental solving under assumptions and, in case of unsatisfiability, allows to
determine the set of failed assumptions [
Query Model Assignments If the input formula is satisfiable and model generation is
enabled, calls to query the model assignments of all generated expressions are issued. Further,
if model printing is enabled, the model of the input formula is printed to stdout. Boolector
supports model output formats based on BTOR [
Reset for Incremental Usage Prior to performing an incremental step, parameters such as maximum numbers and probability distributions are reinitialized with random values (within certain ranges). Note that the value ranges for these parameters may differ from the ranges employed in state New.
Delete State Delete concludes one round (one test case) with releasing all generated
expressions and deleting the current Boolector instance.
28 return true
29 sat b1
30 return 10
31 release b1 e2@b1
32 release b1 e3@b1
33 release b1 e4@b1
34 release b1 e6@b1
35 release b1 e8@b1
36 release b1 e9@b1
37 release b1 e-10@b1
38 release_sort b1 s1@b1
39 release_sort b1 s3@b1
40 delete b1
As of version 2.0, Boolector provides a cloning feature which allows to generate a disjunct
copy of a Boolector instance [
In order to test and guarantee that a full clone behaves exactly the same as the instance it has been cloned from, BtorMBT provides a dedicated shadow clone test setting similar to shadow clone testing as implemented for Lingeling. Shadow clone testing is randomly enabled and when enabled, BtorMBT initially generates a full clone (the shadow clone) of the current Boolector instance, which then mirrors every API call to the original instance and cross-checks return values for equivalence. Additionally, Boolector implements extensive checks for freshly generated clones and internally checks the state of the shadow clone after each API call. A shadow clone may be initialized anytime prior to the first SAT call and is usually randomly released and regenerated multiple times after being initialized, at different stages during one test round, to prevent that clones are only generated and checked prior to (incremental) API calls. 4
Our SMT solver Boolector allows to record all API calls with their arguments to a trace file, which then serves as input for our trace execution tool BtorUntrace. An example of an API trace generated by Boolector is given in Fig. 3, with each line of the trace either listing an API call or the return value of an API call in chronological order. A line representing an API call consists of an identifier, the Boolector instance to issue the call to, and the arguments to the call. A line representing the return value of an API call must immediately follow the line of the call and consists of the keyword return and the return value, which can either be an identifier or a numerical value. As an example, consider the API call in line 7 and its return value in line 8. Identifier array_sort in line 7 refers to the API call to create an array sort with bit-vector sort s1 as its first (index sort) and second (element sort) argument, issued to Boolector instance b1. Line 8 identifies the return value of this call as array sort s3.
BtorUntrace is a dedicated tool for replaying traces generated by Boolector and tightly integrates Boolector via its C API. In our model-based API testing workflow, BtorUntrace is used in combination with BtorMBT to reproduce faulty behavior when a test case generated by BtorMBT fails. However, BtorUntrace is also useful outside of our testing workflow when debugging undesired behavior triggered by any (real world) application of Boolector. Since BtorUntrace only requires the API trace to replay a faulty run of Boolector, it is, e.g., not necessary to have the original (possibly complex) setup of the tool chain available for debugging purposes. Further, some errors triggered via the API may not be triggered with a dump of the corresponding input formula since some (sequences of) Boolector API calls can not be expressed in the input file formats it supports. 5
Our delta debugger ddMBT minimizes a given API error trace while preserving its
failureinducing characteristics based on the exit code and error message produced by Boolector when
replaying the (minimized) trace with BtorUntrace. Trace minimization with ddMBT works in
rounds until fixpoint, with each round divided into three phases. In the first phase, lines of the
trace file are eliminated in a divide-and-conquer manner similar to the original delta debugging
algorithm proposed in [
In the following, similarly as in [
Since we aim to evaluate BtorMBT and FuzzSMT on as even terms as possible, we provide a script for FuzzSMT that simulates option fuzzing and the round-based behavior as implemented in BtorMBT. In the following, we refer to this script as FuzzSMT, and compare against the version of BtorMBT released together with the current version 2.4 of Boolector.
We optionally switch off option fuzzing (while still randomly choosing solver engines and SAT
solvers) and refer to BtorMBT and FuzzSMT without option fuzzing as BtorMBTno and
FuzzSMTno. Note that we compiled Boolector with all three supported SAT solvers Lingeling [
We evaluated BtorMBT and FuzzSMT on runs of 100k rounds and chose a time limit of 2 seconds per round. Note that since increasing this time limit did not increase code coverage for 100k rounds for configuration BtorMBT, we chose this limit as a good compromise between throughput and test coverage.
In order to be able to determine if either of the tools is able to identify faulty mutations of Boolector (see Section 6.4), we thoroughly tested our base version 2.4 of Boolector prior to our experimental evaluation and run 10M rounds with each BtorMBT and FuzzSMT, all of which did not result in a single error.
We performed all our experiments on a cluster with 30 nodes of 2.83 GHz Intel Core 2 Quad machines running Ubuntu 14.04.5 LTS. 6.2
We used the tool gcov of the GNU Compiler Collection (GCC) suite to determine the code coverage over 100k non-faulty rounds of BtorMBT and FuzzMBT with and without option fuzzing. The evolution of line coverage for configurations BtorMBT, BtorMBTno, FuzzSMT and FuzzSMTno as measured by gcov over 100k rounds is illustrated in Fig. 4.
After 10k runs, BtorMBT already aocphtiioevnesfu7z5zi%ng,linaendco8v7er%agewhweinthooupt- 100.0 BBttoorrMMBBTTno toinonthfeuzoztinhger ishaennda,blreeda.chesFuazzcSoMveTr-, 90.0 FFuuzzzzSSMMTTno 90.0 ] age of 64% and 72%. After 100k [% trFouunz7sz8,S%MBt(To+r3Ma%cBh)iTeavniedms9pa0ro%cvoev(s+erc1ao2gv%eer)oa,fgwe6h5ui%lpe rveoageC 80.0 7783..14 (+1%) and 73% (+1%). ieLn 766076...046
Unsurprisingly, BtorMBT covers 65.0 more than 98% of Boolector’s API, 6601..08 with error handling code as the un- 57.5 covered rest that is not triggered due 0 20000 40000 60000 80000 100000 to the fact that all test cases were error free. FuzzSMT, on the other hand, Figure 4: Code coverage evolution over 100k rounds. only achieves a coverage of 52%, which is likely to be improved by introducing full SMT-LIB v2 support, however, not up to the coverage rate BtorMBT achieved. Note that for both tools, a coverage rate of 100% for error free test cases is in general impossible due to the fact that error handling code is not triggered. Further, since FuzzSMT only generates input in SMT-LIB v2 format, all code related to parsing BTOR format (3%) remains unused. 6.3
When fuzz testing an SMT solver, no matter if it is input fuzzing or API fuzzing, the number of tests completed within a certain time frame (the throughput) is an important measure of efficiency and effectiveness of the test method. A high number may indicate that the generated test cases are too trivial and therefore less likely to trigger errors. A low number, on the other hand, may be caused by too difficult and therefore too time consuming test cases, which may considerably slow down progress when testing. We aim to perform as many good test cases, i.e., test cases with a high code coverage rate, in as little time as possible, which is a balancing act between the two extremes above.
For 100k rounds, BtorMBT achieves a throughput of on average 45 rounds per second, which increases by 20% when shadow clone testing is disabled. FuzzSMT, on the other hand, achieves a far lower throughput of 7 test cases per second since it first generates an input file that is then handed to the SMT solver. Further, FuzzSMT is written in Java, and (re)starting the Java VM in each round introduces additional overhead which further decreases throughput.
Note that in 100k rounds with BtorMBT, 20% of all calls to determine satisfiability are incremental. Further, one in four solved instances is satisfiable, which corresponds to a rather unbalanced ratio of 1:3 of satisfiable to unsatisfiable instances. We leave improving this ratio to future work. 6.4
In our final experiment, we evaluated the success rate of BtorMBT and FuzzSMT in identifying faulty configurations of Boolector. We compiled a set of test configurations TC (4626 in total), which consists of two subsets TCA and TCD and contains configurations where we introduced artificial defects into the source code of Boolector. Set TCA contains 2305 configurations with a randomly inserted abort statement, and set TCD consists of 2321 configurations where we deleted a random statement from the code. All 4626 configurations in set TC are faulty configurations. However, some defects, e.g., modifications of heuristics due to a missing statement, may result in performance bugs rather than producing incorrect results or any other erroneous behavior and are therefore impossible to detect with either test method.
For each faulty test configuration, we set a limit of 100k rounds for BtorMBT. However, since the low throughput of FuzzSMT (7 rounds per second) would require too much runtime for our experiment with 100k rounds even on a cluster with 30 nodes (26 days in the worst case), we limited the number of rounds for FuzzSMT to 10k and compare its results to the number of faulty configurations identified by BtorMBT within 10k rounds.
Table 1 shows the number of faulty configurations identified by BtorMBT and FuzzSMT with and without option fuzzing within 100k and 10k rounds. Overall, within 10k rounds BtorMBT has a 11% higher success rate than FuzzSMT, which is increased by 14% to 80.4% when the limit is extended to 100k rounds. Disabling option fuzzing, on the other hand, decreases the number of configurations identified as faulty for both tools by 12%.
Not surprisingly, for both tools the success rates for configuration set TCA correspond to their code coverage as determined in Section 6.2. The number of successfully identified faulty configurations in set TCD, on the other hand, is significantly lower due to the fact that set TCD contains test cases with defects that concern error handling code or decrease performance rather than introducing erroneous behavior. Further, in case of BtorMBT, since dumps in AIGER format are not tested for correctness it is not possible to detect configurations that produce incorrect AIGER output. The same applies in case of FuzzSMT for configurations that produce incorrect dump output in any format since it is not checked for correctness. 100k 10k
TCA (2305) TCD (2321) TC (4626) TCA (2305) TCD (2321) TC (4626) In this paper, we presented a model-based API testing tool set for our SMT solver Boolector. It consists of several dedicated tools, the model-based API tester BtorMBT, the API trace exection tool BtorUntrace and the API trace minimizing tool ddMBT.
Our API fuzzer BtorMBT generates random but valid sequences of calls to Boolector’s API and allows to test random configurations of Boolector on random input formulas. With a success rate of 80% on our artificial set of faulty configurations of Boolector and a line coverage of 90% over 100k rounds, our experiments suggest that BtorMBT is an effective method for testing Boolector. Our extremely positive practical experience confirms this claim. Based on our results, we believe that applying our techniques to other SMT solvers is effective in general. An interesting direction for future work would be introducing symbolic execution techniques into BtorMBT in order to be able to direct trace generation towards maximal code coverage.
Our model-based API testing framework is the core component of the testing workflow in
the development process of Boolector. However, it still needs to be complemented by several
other tools to cover cases that can not be tested with BtorMBT alone. The solver front end, for
example, can only be tested by using the solver as standalone tool with files in BTOR or
SMTLIB format as input. For that purpose, we use a suite of regression tests and FuzzSMT, even
though its support for the SMT-LIB v2 format is incomplete. Another example is parser testing,
which is incomplete with BtorMBT since Boolector is currently not able to dump incremental
input and in general does not use the full feature set of the SMT-LIB language when dumping.
Further, dumping with Boolector only produces valid input files. However, a parser must be
tested for correct parse error handling on invalid input, too. We test Boolector’s parsers by
means of the tool fzsexpr of the ddsexpr tool set [
Currently, BtorMBT produces a rather unbalanced ratio of 1:3 of satisfiable to unsatisfiable instances. Further, AIGER dump output is not checked for correctness since Boolector does not allow to parse AIGER input files. We leave improving the ratio of satisfiable to unsatisfiable instances and checking the correctness of AIGER dumps to future work.