KLEEF: Symbolic Execution Engine (Competition Contribution)

As a symbolic interpreter [1], KLEE runs a program on a symbolic memory, which maps program locations to symbolic values, representing sets of concrete values. When it meets a branching instruction, it adds target instructions to a queue and after each executed instruction it decides which instruction execute next. Symbolic interpreter collects all conditions from branching instructions in a path constraint. It is a formula, which may be either unsatisfiable (if the path is infeasible) or satisfiable, and have multiple solutions. Each solution gives a concrete test, which would visit the corresponding path. A symbolic interpreter usually relies on an SMT solver (like Z3 [8]) to get solutions of path constraints.

The KLEE engine is split into two logical parts. The first part is a symbolic interpreter, which takes a symbolic state, executes one instruction, and produces new states. The second part is a searcher, which chooses the next symbolic state to execute according to a strategy, specified by input options, e.g., BFS or DFS.

We enhanced KLEE with support for arbitrary data structures such as trees and linked lists by implementing lazy initialization [7]. If KLEE dereferences a symbolic pointer, it forks the symbolic state into many: each one assumes that the pointer refers to one of the existing locations in the memory. In KLEEF we also fork one extra state, where the pointer refers to a fresh, lazy initialized symbolic object, which is distinct from all other object of the current symbolic memory. If there are not enough objects in the memory, KLEEF will create a new one and continue execution while KLEE will not. In the configuration used at the competition we only create lazy initialized symbolic objects for symbolic pointers without forking the state into existing locations beforehand.

We improve KLEE with symcretes [10], which help to support dynamically allocated arrays (with symbolic sizes) and external calls. KLEEF thus supports detecting buffer overflows. A symcrete is a pair of symbolic value and its concrete instance valid in the current context. The concrete part of symcrete values is derived from the model of a path constraint. It stays the same if the solver can find a model for concretized constraints. Having failed, the concretization will be updated by values from the model for the original constraints. When a logical solver receives a query with a symcrete, an equality between the symbolic and concrete parts of the symcrete are added to the query. This helps the solver to solve the query, as a part of the model is already specified in the symcrete. KLEEF thus handles dynamically allocated arrays by making array size and address symcretes. KLEEF uses the solver to minimize possible array size and sparse storage for arrays, so that the entire process does not blow up.

We have implemented searchers optimized specifically for maximizing coverage and reaching the error target. That is, KLEEF has targeted searcher and guided searcher which maximize coverage and error reachability, similar to [3]. The targeted searcher uses the shortest path based algorithm to choose the nearest execution state to the target location. Each execution state carries a set of targets. A guided searcher manages a bunch of targeted searchers with different targets and chooses states from every targeted searcher in interleaved manner.

KLEEF improves over KLEE in constraint solving by caching unsatisfiability cores, interning symbolic expressions, tracking constraints during simplification to detect conflicts and using an SMT solver incrementally. In KLEEF we added support for Bitwuzla [9] SMT solver, which performs significantly better on Test-Comp benchmarks. For example, KLEEF with Z3 achieves 2430 points running for 30 seconds on Test-Comp 2023 benchmarks, while KLEEF with Bitwuzla achieves 2560 points within the same time limit.

In order to run the competition version from the command line, one should get the archive with binaries from Zenodo¹ and follow the README inside.

In order to generate a test coverage for a project without configuring KLEEF manually, one should use a user-friendly wrapper UnitTestBot C/C++ [6, 12]. It allows KLEEF to be run in VS Code and JetBrains CLion.

In order to build KLEEF from sources, one should install LLVM, clone KLEEF from GitHub² and run build.sh script in the repository root.

Common Parameters. Parameters --strip-unwanted-calls, --delete-dead-loops=false, --mock-all-externals are used to (de)activate necessary LLVM passes to simplify bitcode for a symbolic execution. A parameter --external-calls=all allows function calls with symbolic arguments. An option --libc=klee makes KLEEF support an extended number of external functions.

Parameters --cex-cache-validity-cores, --use-forked-solver=false, --solver-backend=bitwuzla-tree, --max-solvers-approx-tree-inc=16 are used to cache unsatisfiability cores and call a Bitwuzla solver incrementally.

A parameter --fp-runtime adds a floating point support. Parameters starting with --allocate-determ activate X86 support. An option --x86FP-as-x87FP80 adds emulation of X86 floating points as extended 80 bit floating points.

Finally, --max-memory and --max-time fix memory and time limit.

Parameters for Cover-Error. An option --optimize=true simplifies code before execution, e.g., it joins some branches to multiple blocks into selection instructions. Options --search=dfs --search=bfs make KLEEF interleave between DFS and BFS. Options --function-call-reproduce=reach_error, --exit-on-error-type=Assert make KLEEF run towards reach_error function and fail only there. An option --dump-states-on-halt=unreached permits KLEEF to generate tests for unfinished paths.

Parameters for Cover-Branches. A parameter --track-coverage=all makes KLEEF track coverage by both branches and instructions. Options --optimize=false and --optimize-aggressive=false disable optimizations which decrease coverage. Options --use-iterative-deepening-search=max-cycles, --max-cycles-before-stuck=15 activate an iterative-deepening mode of execution on a number of executed loop cycles. A parameter --max-solver-time=10s fixes a time limit for an SMT solver. An option --only-output-states-covering-new makes KLEEF only generate tests which increase coverage. Options --search=dfs, --search=random-state make KLEEF interleave between DFS and taking a random state. A parameter --dump-states-on-halt=all makes KLEEF generate tests for the symbolic states remaining in the end. Options --cover-on-the-fly, --delay-cover-on-the-fly, --mem-trigger-cof start on the fly test generation after approaching memory cap.