KLEE

master branch

Solver Chain

Overview of solver chain and related command-line options

Contents

The solver chain

KLEE has a number of command line options that control the solver chain that is shared both by the klee and kleaver tools.

The solver chain is implemented internally using the decorator design pattern. Thus when a solver query is issued it travels through a nested stack of solvers and may eventually call the underlying SMT solver (core solver).

The reasons for this architecture are:

  1. Allows transforming the solver query into another form that is hopefully faster for the core solver to solve (e.g. the independence solver).
  2. Allows querying the core solver to be avoided in some cases (e.g. the counterexample caching solver).
  3. Allows logging of queries at different stages in the solver chain.

The constructSolverChain() function is used to create the solver chain.

Core solver

This is the underlying SMT solver. Several solvers are currently supported. The default is dependent on what solvers were available when KLEE was built. The solver can be selected using the -solver-backend= option.

  1. STP: Simple Theorem Prover SMT solver link. Use -solver-backend=stp.
  2. Z3: The Z3 Theorem Prover link. Use -solver-backend=z3.
  3. metaSMT: An Embedded Domain Specific Language for SMT link. Use -solver-backend=metasmt.

When using metaSMT as the core solver, its backend can be specified using the -metasmt-backend= option.

Caching Solvers

These solvers cache previous queries to avoid calling the underlying solver when possible.

Caching solver

This solver caches previous queries and their result to avoid calling the underlying solver in certain situations. The queries are canonicalized to increase the cache hit rate.

This solver can be enabled with the -use-cache option.

Counterexample caching solver

This solver caches satisfying assignments to queries (i.e. “counterexamples” to validity) which can be used to avoid calling the underlying solver in certain situations.

This solver can be enabled with the -use-cex-cache option.

Independence solver

This solver splits a query into disjoint sets of independent constraints and then calls the underlying solver on each set to solve them independently.

This solver can be enabled with the -use-independent-solver option.

Debugging solvers

The remaining solvers are used for debugging.

Assignment validating solver

This solver checks that assignments to satisfiable queries are satisfiable when substituted into the expressions in the query.

This is useful for checking the consistency of KLEE’s constraint language and that of the core solver.

This option can be enabled using the -debug-assignment-validating-solver option.

Debug validating solver

This solver is meant for debugging and currently is only useful if building with assertions is enabled. The solver can be enabled with the -debug-validate-solver option.

This solver invokes the underlying solver and a separate solver for every query and then checks that the solvers agree. The separate solver can be set with the -debug-crosscheck-core-solver= option which takes the same arguments as -solver-backend=.

This is useful for comparing two completly independent solvers (e.g. STP and Z3) and for checking that invoking the solver chain and a solver directly obtains the same results.

Query logging solver

The query logging solver logs queries at different positions in the chain.

The option to enable this is the --use-query-log= option. The format of the option is --use-query-log=TYPE:FORMAT, where:

In addition there are several options that change how these queries are logged.