KLEE

https://klee-se.org/docs
Admin
KLEE is a symbolic execution engine that automatically generates test cases for C and C++ programs...
Tokens:13,831
Snippets:202
Trust Score:7.3
Update:5 months ago
Show doc for...
Tokens:
Raw
### Initialize Environment from File

Source: https://klee-se.org/docs/options

Start KLEE execution by loading the environment from a specified file in "env" format.

```bash
--env-file=<file_name>
```

--------------------------------

### KQuery Syntax Example

Source: https://klee-se.org/docs/kquery

Illustrates the basic syntax for equality checks in KQuery.

```kquery
"(" "Eq" [ type ] LHS RHS ")"
```

--------------------------------

### KQuery Array Declaration and Read Example

Source: https://klee-se.org/docs/kquery

Illustrates array declaration, version labeling, and reading elements from an array.

```kquery
array const_array[] : w32 -> w8 = [5,6]
(Read w8 0 U0:[0=255] @ const_array) # U0 now refers to an array [255,6]
(Read w8 1 U0) # Read from byte offset 1 of [255,6]
```

--------------------------------

### KQuery Identifier Examples

Source: https://klee-se.org/docs/kquery

Provides examples of valid identifiers in KQuery.

```kquery
_foo
arr10_20
```

--------------------------------

### KQuery Equality Example

Source: https://klee-se.org/docs/kquery

A concrete example of an equality check in KQuery.

```kquery
(Eq w32 a b)
```

--------------------------------

### Change Working Directory at Startup

Source: https://klee-se.org/docs/options

Instruct KLEE to change to a specified directory before starting execution. Defaults to the location of the tested file.

```bash
--run-in-dir=<dir_name>
```

--------------------------------

### KQuery Expression Label Example

Source: https://klee-se.org/docs/kquery

An example demonstrating the use of expression labels for repeated expressions.

```kquery
(Add w32 N0:(Add w32 1 1) N0) # Four
```

--------------------------------

### Get Help for Klee-Stats Options

Source: https://klee-se.org/docs/tools

Run `klee-stats --help` to display all available command-line options and their descriptions. This is essential for understanding how to customize the output and analysis.

```bash
$ klee-stats --help

```

--------------------------------

### Execution Tree Compression Example

Source: https://klee-se.org/docs/options

Illustrates how `--compress-exec-tree` simplifies deep execution trees by reducing chains of unary edges to a single edge.

```text
 /\            /\
A  \          A  E
    \    =>
     \
      E

```

--------------------------------

### Example KLEE Info File Content

Source: https://klee-se.org/docs/files

The 'info' file contains KLEE run details, including the command-line arguments, execution time, and summary statistics.

```text
$ cat info
klee --write-kqueries demo.o
PID: 12460
Started: 2009-05-20 22:31:41
BEGIN searcher description
DFSSearcher
END searcher description
Finished: 2009-05-20 22:31:41
Elapsed: 00:00:00
KLEE: done: explored paths = 3
KLEE: done: avg. constructs per query = 6
KLEE: done: total queries = 3
KLEE: done: valid queries = 0
KLEE: done: invalid queries = 3
KLEE: done: query cex = 3
KLEE: done: total instructions = 67
KLEE: done: completed paths = 3
KLEE: done: generated tests = 3


```

--------------------------------

### KQuery Comment Example

Source: https://klee-se.org/docs/kquery

Demonstrates how to add comments in KQuery using the '#' symbol.

```kquery
(Add w32 1 1) # Two, hopefully
```

--------------------------------

### KQuery Type Example

Source: https://klee-se.org/docs/kquery

An example of a type declaration in KQuery, specifying a 32-bit width.

```kquery
w32
```

--------------------------------

### Select KLEE Search Heuristic

Source: https://klee-se.org/docs/options

Choose the state exploration strategy for KLEE. Examples show how to select Depth-First Search (DFS) and Random Path Selection.

```bash
$ klee --search=dfs demo.o
```

```bash
$ klee --search=random-path demo.o
```

--------------------------------

### KQuery Query Command Examples

Source: https://klee-se.org/docs/kquery

Define queries for constraint solvers, optionally specifying expressions and arrays for counterexamples. Constraints must be consistent.

```kquery
(query [] false)
```

```kquery
(query [(Eq w8 (Read w8 0 mem) 10)] false [] [ mem ])
```

--------------------------------

### KQuery Number Examples

Source: https://klee-se.org/docs/kquery

Examples of numeric literals in KQuery, including boolean, signed decimal, and binary with separators.

```kquery
false
-10
0b1000_0001 # 129
```

--------------------------------

### Start klee-stats for Grafana Live Monitoring

Source: https://klee-se.org/docs/tools

Run klee-stats with the --grafana flag to enable it to serve data for live monitoring in Grafana. It defaults to port 5000.

```bash
$ klee-stats --grafana <klee-out-dir>

```

--------------------------------

### Grafana Startup Log Message

Source: https://klee-se.org/docs/tools

This log message indicates that the Grafana server has started successfully and is listening on port 3000.

```log
t=... lvl=info msg="HTTP Server Listen" logger=http.server address=0.0.0.0:3000 protocol=http subUrl= socket=

```

--------------------------------

### Current KLEE Options for Coreutils Experiments (paste)

Source: https://klee-se.org/docs/coreutils-experiments

A set of KLEE options that are closer to the original experimental setup but compatible with current KLEE versions. Note the changes in libc, runtime, external calls, and search strategies.

```bash
$ klee --simplify-sym-indices --write-cvcs --write-cov --output-module \
--max-memory=1000 --disable-inlining --optimize --use-forked-solver \
--use-cex-cache --libc=uclibc --posix-runtime \
--external-calls=all --only-output-states-covering-new \
--env-file=test.env --run-in-dir=/tmp/sandbox \
--max-sym-array-size=4096 --max-solver-time=30s --max-time=60min \
--watchdog --max-memory-inhibit=false --max-static-fork-pct=1 \
--max-static-solve-pct=1 --max-static-cpfork-pct=1 --switch-type=internal \
--search=random-path --search=nurs:covnew \
--use-batching-search --batch-instructions=10000 \
./paste.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdin 8 --sym-stdout

```

--------------------------------

### KQuery Primitive Expression Examples

Source: https://klee-se.org/docs/kquery

Use identifiers to refer to labeled expressions or constants specified by numeric tokens or type-numeric token pairs.

```kquery
true
```

```kquery
(w32 0)
```

```kquery
(Add w32 10 20) # The type for 10 and 20 is inferred to be w32.
```

--------------------------------

### Interleave KLEE Search Heuristics

Source: https://klee-se.org/docs/options

Combine multiple search heuristics in a round-robin fashion for state exploration. This example interleaves Random State and NURS:MD2U.

```bash
$ klee --search=random-state --search=nurs:md2u demo.o
```

--------------------------------

### Run Grafana Docker Container

Source: https://klee-se.org/docs/tools

Start the preconfigured Grafana Docker image to visualize KLEE statistics. This command runs Grafana in detached mode on the host network.

```bash
$ docker run -d --net=host --name=grafana klee/grafana

```

--------------------------------

### KQuery Arithmetic Operation Example

Source: https://klee-se.org/docs/kquery

Perform binary arithmetic operations like Add, Sub, Mul, UDiv, SDiv, URem, SRem. Ensure left- and right-hand side expressions match the expression type.

```kquery
(Add w32 10 20)
```

--------------------------------

### KQuery Extract Operation

Source: https://klee-se.org/docs/kquery

Extracts a specified number of bits (`type`) from a `child-expression` starting at a given `offset-number`.

```kquery
expression = ") "Extract" type offset-number child-expression )"
```

--------------------------------

### Prefer Printable Characters with klee_prefer_cex

Source: https://klee-se.org/docs/intrinsics

Use klee_prefer_cex after klee_make_symbolic to guide KLEE towards generating test cases with printable characters. This is useful for making failing test cases more readable. It is disabled by default and can be expensive.

```c
char input[4];
klee_make_symbolic(input, sizeof(input), "input");
assert(input[0] == 'Q');
```

```c
for (int i = 0; i < 4; i++)
  klee_prefer_cex(input, 32 <= input[i] && input[i] <= 126); // assume ASCII
```

--------------------------------

### Basic KLEE Command Structure

Source: https://klee-se.org/docs/options

Illustrates the general format for invoking KLEE. Specify KLEE options, the LLVM bitcode program, and then program-specific options.

```bash
$ klee [klee-options] <program.bc> [program-options]
```

--------------------------------

### Kleaver Basic Usage

Source: https://klee-se.org/docs/kleaver-options

Illustrates the fundamental command-line structure for invoking Kleaver with an input query log.

```bash
$ kleaver [options] <input query log>
```

--------------------------------

### Specify Entry Point for Execution

Source: https://klee-se.org/docs/options

Set a specific function as the entry point for KLEE execution instead of the default `main` function.

```bash
--entry-point=<function_name>
```

--------------------------------

### klee_assume with Short-Circuit Operators

Source: https://klee-se.org/docs/intrinsics

Demonstrates how short-circuit operators in `klee_assume` can lead to unexpected path counts due to compiler transformations. Using bitwise operators can sometimes mitigate this.

```c
#include "klee/klee.h"

int main() {
  int c,d;
  klee_make_symbolic(&c, sizeof(c), "c");
  klee_make_symbolic(&d, sizeof(d), "d");
  
  int tmp;
  if (c == 2) 
    tmp = d == 3;
  else
    tmp = 0;

  klee_assume(tmp);

  return 0;
}
```

--------------------------------

### Define Symbolic Files with KLEE

Source: https://klee-se.org/docs/options

Instruct KLEE to create symbolic files with specified names and sizes. Useful for testing file I/O operations symbolically.

```bash
-sym-files <NUM> <N>
```

--------------------------------

### Write Execution Tree to Database

Source: https://klee-se.org/docs/options

Enable writing the execution tree into an SQLite database file named `exec_tree.db`.

```bash
--write-exec-tree
```

--------------------------------

### Original KLEE Options for Coreutils Experiments (paste)

Source: https://klee-se.org/docs/coreutils-experiments

The command-line options used with KLEE for the 'paste' utility during the OSDI'08 experiments. Some options may be renamed or removed in current KLEE versions.

```bash
$ klee --simplify-sym-indices --write-cvcs --write-cov --output-module \
--max-memory=1000 --disable-inlining --optimize --use-forked-solver \
--use-cex-cache --with-libc --with-file-model=release \
--allow-external-sym-calls --only-output-states-covering-new \
--exclude-libc-cov --exclude-cov-file=./../lib/functions.txt \
--env-file=test.env --run-in-dir=/tmp/sandbox --output-dir=paste-data-1h \
--max-sym-array-size=4096 --max-instruction-time=10. --max-time=3600. \
--watchdog --max-memory-inhibit=false --max-static-fork-pct=1 \
--max-static-solve-pct=1 --max-static-cpfork-pct=1 --switch-type=internal \
--randomize-fork --use-random-path --use-interleaved-covnew-NURS \
--use-batching-search --batch-instructions 10000 --init-env \
./paste.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdout

```

--------------------------------

### Specify Output Directory

Source: https://klee-se.org/docs/options

Define the directory where KLEE will write its results. Defaults to `klee-out-`.

```bash
--output-dir=<dir_name>
```

--------------------------------

### Run klee-stats on multiple directories

Source: https://klee-se.org/docs/tools

Execute klee-stats on the current directory to aggregate statistics from multiple KLEE output directories. This provides a combined view of performance and coverage across different runs.

```bash
$ klee-stats .
-------------------------------------------------------------------------
|   Path   |  Instrs|  Time(s)|  ICov(%)|  BCov(%)|  ICount|  TSolver(%)|
-------------------------------------------------------------------------
|klee-last |     499|     0.13|    45.69|    39.13|     394|        0.04|
|klee-out-3|     499|     0.03|    45.69|    39.13|     394|        0.12|
|klee-out-2|     499|     0.09|    45.69|    39.13|     394|        0.03|
|klee-out-8|     499|     0.13|    45.69|    39.13|     394|        0.04|
|klee-out-4|     499|     0.02|    45.69|    39.13|     394|        0.14|
-------------------------------------------------------------------------
|Total (5) |    2495|     0.40|    45.69|    39.13|    1970|        0.07|
-------------------------------------------------------------------------

```

--------------------------------

### Enable Batching Search in KLEE

Source: https://klee-se.org/docs/options

Execute multiple instructions before selecting a new state, improving performance. Options allow specifying batch size by instruction count or execution time.

```bash
-use-batching-search
```

```bash
-batch-instructions=1000
```

```bash
-batch-time=5s
```

--------------------------------

### Configure KLEE Instruction Logging

Source: https://klee-se.org/docs/options

Control the format and destination of LLVM instruction logging. Use 'stderr' for immediate output or 'file' to log to instructions.txt.

```bash
klee -debug-print-instructions=all:stderr input.bc
```

```bash
klee -debug-print-instructions=src:stderr input.bc
```

```bash
klee -debug-print-instructions=compact:stderr input.bc
```

```bash
klee -debug-print-instructions=all:file input.bc
```

```bash
klee -debug-print-instructions=src:file input.bc
```

```bash
klee -debug-print-instructions=compact:file input.bc
```

--------------------------------

### Display ktest file contents with ktest-tool

Source: https://klee-se.org/docs/tools

Use ktest-tool to convert the contents of a .ktest file into a human-readable format. This is useful for understanding the concrete input values that correspond to specific execution paths.

```bash
$ ktest-tool klee-last/test000003.ktest
ktest file : 'klee-last/test000003.ktest'
args       : ['get_sign.bc']
num objects: 1
object 0: name: 'a'
object 0: size: 4
object 0: data: b'\x00\x00\x00\x80'
object 0: hex : 0x00000080
object 0: int : -2147483648
object 0: uint: 2147483648
object 0: text: ....

```

--------------------------------

### Make Standard Input Symbolic

Source: https://klee-se.org/docs/options

Configure KLEE to treat standard input as symbolic data with a specified maximum size. This allows for symbolic testing of programs that read from stdin.

```bash
-sym-stdin <N>
```

--------------------------------

### KQuery Expression Labeling

Source: https://klee-se.org/docs/kquery

Shows how to define and use expression labels for lexical binding in KQuery.

```kquery
expression = identifier ":" expression
```

--------------------------------

### Generate test.env using testing-env.sh

Source: https://klee-se.org/docs/coreutils-experiments

Command to create the 'test.env' file by sourcing a provided 'testing-env.sh' script and capturing the resulting environment variables.

```bash
$ env -i /bin/bash -c '(source testing-env.sh; env >test.env)'

```

--------------------------------

### Generate KLEE Execution Tree in DOT format

Source: https://klee-se.org/docs/tools

Convert the KLEE execution tree into the Graphviz DOT format for visualization. This allows generating image files like SVG or PNG.

```bash
$ klee-exec-tree tree-dot klee-out-1 | dot -Tsvg > tree.svg

```

--------------------------------

### Link a single external LLVM IR library

Source: https://klee-se.org/docs/options

Use this option to link a single external LLVM IR file or archive when running KLEE. Ensure the library file is accessible.

```bash
$ klee -link-llvm-lib=libhelper.so.bc test.bc
```

--------------------------------

### Generate .ktest file from AFL testcase

Source: https://klee-se.org/docs/tools

Convert AFL-generated testcases into .ktest files using ktest-gen. This allows KLEE to use these testcases as seeds for further exploration.

```bash
# Assumes that you are in the AFL output directory (specified via the -o option when fuzzing.
# Ignores hidden directories.
# AFL-generated testcases always begin with 'id:'

find ./queue -not -path '*/\.*' -type f -name 'id:*'    \
    -exec ktest-gen --bout-file {}.ktest --sym-file {} \;

```

--------------------------------

### Run klee-stats on a single directory

Source: https://klee-se.org/docs/tools

Invoke klee-stats on a specific KLEE output directory to view a summary of execution statistics. The output includes path, instructions, time, coverage, and solver information.

```bash
$ klee-stats klee-out-2
-------------------------------------------------------------------------
|   Path   |  Instrs|  Time(s)|  ICov(%)|  BCov(%)|  ICount|  TSolver(%)|
-------------------------------------------------------------------------
|klee-out-2|     499|     0.09|    45.69|    39.13|     394|        0.03|
-------------------------------------------------------------------------

```

--------------------------------

### Specify Query Log Directory

Source: https://klee-se.org/docs/kleaver-options

Sets the directory where Kleaver will store logs of queries issued to the underlying solver. Defaults to the current working directory.

```bash
$ kleaver --query-log-dir=kleaver-log query.kquery
```

--------------------------------

### Exit KLEE on First Error

Source: https://klee-se.org/docs/options

Instruct KLEE to terminate immediately upon encountering any arbitrary error during analysis.

```bash
klee -exit-on-error input.bc
```

--------------------------------

### Write Instruction Stats After Instructions

Source: https://klee-se.org/docs/options

Write instruction-level statistics after a specified number of instructions. Set to 0 to disable.

```bash
-istats-write-after-instructions=N
```

--------------------------------

### Make Standard Output Symbolic

Source: https://klee-se.org/docs/options

Enable KLEE to treat standard output as symbolic. This is useful for testing programs where the output content is critical and needs to be explored symbolically.

```bash
-sym-stdout
```

--------------------------------

### Write Statistics After Instructions

Source: https://klee-se.org/docs/options

Write statistics after a specified number of instructions. Set to 0 to disable.

```bash
-stats-write-after-instructions=N
```

--------------------------------

### Handle Zero-Size Malloc Calls

Source: https://klee-se.org/docs/options

Configure KLEE to return NULL when malloc(0) is called. This can help identify potential issues related to zero-sized allocations.

```bash
klee --return-null-on-zero-malloc input.bc
```

--------------------------------

### Write Running Stats Trace File

Source: https://klee-se.org/docs/options

Enable writing of a running stats trace file. This is enabled by default.

```bash
-output-stats
```

--------------------------------

### Coreutils Applications Tested

Source: https://klee-se.org/docs/coreutils-experiments

Lists the 89 Coreutils applications that were part of the OSDI'08 experiments.

```text
base64 basename cat chcon chgrp chmod chown chroot cksum comm cp csplit cut
date dd df dircolors dirname du echo env expand expr factor false fmt fold
head hostid hostname id ginstall join kill link ln logname ls md5sum mkdir
mkfifo mknod mktemp mv nice nl nohup od paste pathchk pinky pr printenv printf
ptx pwd readlink rm rmdir runcon seq setuidgid shred shuf sleep sort split
stat stty sum sync tac tail tee touch tr tsort tty uname unexpand uniq unlink
uptime users wc whoami who yes

```

--------------------------------

### Modification in Coreutils 'sort.c'

Source: https://klee-se.org/docs/coreutils-experiments

Shows the specific change made to the `INPUT_FILE_SIZE_GUESS` macro in the `sort.c` file for the experiments.

```c
#define INPUT_FILE_SIZE_GUESS (1024 * 1024)
to #define INPUT_FILE_SIZE_GUESS 1024 in file sort.c
```

--------------------------------

### Enhanced Arguments for Specific Coreutils

Source: https://klee-se.org/docs/coreutils-experiments

Arguments adjusted for tools with unsatisfactory coverage, increasing the number and size of symbolic arguments and files. Consult man pages for specific tool options.

```bash
--sym-args 0 3 10 --sym-files 1 8 --sym-stdin 8 --sym-stdout
```

```bash
--sym-args 0 3 10 --sym-files 2 12 --sym-stdin 12 --sym-stdout
```

```bash
--sym-args 0 4 300 --sym-files 2 30 --sym-stdin 30 --sym-stdout
```

```bash
--sym-args 0 1 10 --sym-args 0 3 2 --sym-stdout
```

```bash
--sym-args 0 1 10 --sym-args 0 3 2 --sym-files 1 8 --sym-stdin 8 --sym-stdout
```

```bash
--sym-args 0 3 10 --sym-files 2 12 --sym-stdin 12 --sym-stdout
```

```bash
--sym-args 0 1 2 --sym-args 0 1 300 --sym-files 1 8 --sym-stdin 8 --sym-stdout
```

```bash
--sym-args 0 3 10 --sym-files 2 12 --sym-stdin 12 --sym-stdout
```

--------------------------------

### Analyze KLEE Execution Tree Terminations

Source: https://klee-se.org/docs/tools

Use klee-exec-tree to display termination statistics from KLEE's execution tree. This provides insights into how different paths in the execution tree terminate.

```bash
$ klee-exec-tree terminations klee-out-1
termination type,count
Exit,2230
Interrupted,48352
OutOfMemory,31547
Ptr,4
External,14
...

```

--------------------------------

### Display Statistics in Readable CSV Format

Source: https://klee-se.org/docs/tools

Use the `--table-format=readable-csv` option to display KLEE statistics in a human-readable CSV format. This is useful for quick analysis and comparison of multiple KLEE runs.

```bash
$ klee-stats --table-format=readable-csv klee-out-2 klee-out-3
Path      ,  Instrs,  Time(s),  ICov(%),  BCov(%),  ICount,  TSolver(%)
klee-out-2,     499,     0.09,    45.69,    39.13,     394,        0.03
klee-out-3,     499,     0.03,    45.69,    39.13,     394,        0.12

```

--------------------------------

### Extract sandbox.tgz

Source: https://klee-se.org/docs/coreutils-experiments

Command to extract the 'sandbox.tgz' archive into the '/tmp' directory, used to set up the experimental sandbox environment.

```bash
$ cd /tmp $ tar xfv sandbox.tgz

```

--------------------------------

### Enable Statistics Output

Source: https://klee-se.org/docs/options

Enable the output of statistics generated by KLEE during execution. This is enabled by default.

```bash
-stats
```

--------------------------------

### Analyze KLEE Execution Tree Branches

Source: https://klee-se.org/docs/tools

Use klee-exec-tree to display branch statistics from KLEE's execution tree in CSV format. This helps in understanding branching behavior.

```bash
$ klee-exec-tree branches klee-out-1
branch type,count
Alloc,0
Br,55055
Call,0
Exact,0
Free,0
Getval,0
Memop,0
Realloc,0
Switch,27091
IndirectBr,0
...

```

--------------------------------

### Link multiple external LLVM IR libraries

Source: https://klee-se.org/docs/options

Provide the `-link-llvm-lib` option multiple times to link several external libraries. This allows your program to resolve symbols from multiple sources.

```bash
$ klee -link-llvm-lib=libhelper.so.bc -link-llvm-lib=libhelper2.so.bc test.bc
```

--------------------------------

### KQuery Format Declaration

Source: https://klee-se.org/docs/kleaver-options

Defines the basic structure of a KQuery source file, consisting of array declarations or query commands.

```kquery
kquery = { array-declaration | query-command }
```

--------------------------------

### Write Instruction Level Statistics

Source: https://klee-se.org/docs/options

Enable writing of instruction-level statistics in Callgrind format. This is enabled by default.

```bash
-output-istats
```

--------------------------------

### KLEE Search Heuristic Options

Source: https://klee-se.org/docs/options

Lists available search heuristics for KLEE, including various Non Uniform Random Search (NURS) variants. The default is 'random-path' interleaved with 'nurs:covnew'.

```bash
$ klee --help
-search - Specify the search heuristic (default=random-path interleaved with nurs:covnew)
  =dfs - use Depth First Search (DFS)
  =random-state - randomly select a state to explore
  =random-path - use Random Path Selection (see OSDI'08 paper)
  =nurs:covnew - use Non Uniform Random Search (NURS) with Coverage-New heuristic
  =nurs:md2u - use NURS with Min-Dist-to-Uncovered heuristic
  =nurs:depth - use NURS with 2^depth heuristic
  =nurs:icnt - use NURS with Instr-Count heuristic
  =nurs:cpicnt - use NURS with CallPath-Instr-Count heuristic
  =nurs:qc - use NURS with Query-Cost heuristic
```

--------------------------------

### Declare and Initialize KQuery Arrays

Source: https://klee-se.org/docs/kquery

Declare arrays as symbolic or with a list of constant values. For constant arrays, the initializer list must match the array size.

```kquery
array foo[10] : w32 -> w8 = symbolic # A ten element symbolic array
```

```kquery
array foo[] : w8 -> w1 = [ true, false, false, true ] # A constant array of
four booleans
```

--------------------------------

### Redirect KLEE Warnings to File

Source: https://klee-se.org/docs/options

Configure KLEE to output warnings only to a file, suppressing them from the console. Useful for cleaner output during execution.

```bash
$ klee --warnings-only-to-file ...
```

--------------------------------

### Specify Symbolic Arguments with KLEE

Source: https://klee-se.org/docs/options

Options for defining symbolic command-line arguments for the program being executed by KLEE. Use '-sym-arg' for a single symbolic argument of a specific length.

```bash
-sym-arg <N>
```

```bash
-sym-args <MIN> <MAX> <N>
```

--------------------------------

### Sort Command for Non-Threaded KLEE

Source: https://klee-se.org/docs/coreutils-experiments

When using KLEE, which does not support threads, add `--parallel=1` as a command-line flag for the `sort` utility. This ensures compatibility with KLEE's execution environment.

```bash
--parallel=1
```

--------------------------------

### Control File Write Operations in KLEE

Source: https://klee-se.org/docs/options

Manage how KLEE handles write operations that exceed the initial file size. '-save-all-writes' allows these writes, while its default behavior discards them.

```bash
-save-all-writes
```

--------------------------------

### Configure KDAlloc Memory Reservation Sizes

Source: https://klee-se.org/docs/options

Set reserved memory sizes for KDAlloc segments. Note that these only reserve address space, not actual memory.

```bash
klee --kdalloc-globals-size=2 input.bc
```

```bash
klee --kdalloc-constants-size=2 input.bc
```

```bash
klee --kdalloc-heap-size=1024 input.bc
```

```bash
klee --kdalloc-stack-size=100 input.bc
```

--------------------------------

### KQuery Comparison Operations Syntax

Source: https://klee-se.org/docs/kquery

Defines the syntax for comparison operations like Eq, Ne, Ult, Ule, Ugt, Uge, Slt, Sle, Sgt, Sge. Types must match, and 'w1' is used if type is specified.

```kquery
comparison-expr-kind = ( "Eq" | "Ne" | "Ult" | "Ule" | "Ugt" | "Uge" | "Slt" |
"Sle" | "Sgt" | "Sge" )
expression = ") " comparison-expr-kind [ type ] expression expression )"
```

--------------------------------

### KQuery Sign-Extend (SExt)

Source: https://klee-se.org/docs/kquery

Sign-extends an `input-expression` to a specified `type` by replicating the most significant bit.

```kquery
expression = ") "SExt" type input-expression )"
```

--------------------------------

### Enable Deterministic Memory Allocation with KDAlloc

Source: https://klee-se.org/docs/options

Configure KDAlloc for deterministic memory allocation. This option enables features like cross-run determinism and improved memory error detection.

```bash
klee --kdalloc input.bc
```

--------------------------------

### Basic klee_assume Usage

Source: https://klee-se.org/docs/intrinsics

Use `klee_assume` to constrain symbolic variables. It adds the condition to path constraints, similar to an if statement but errors on unsatisfiable conditions.

```c
#include "klee/klee.h"

int main() {
  int c,d;
  klee_make_symbolic(&c, sizeof(c), "c");
  klee_make_symbolic(&d, sizeof(d), "d");

  klee_assume((c==2) && (d==3));

  return 0;
}
```

--------------------------------

### Configure KDAlloc Quarantine Size

Source: https://klee-se.org/docs/options

Adjust the size of KDAlloc's quarantine queues. A non-zero size helps detect use-after-free bugs by preventing immediate memory address reuse.

```bash
klee --kdalloc-quarantine=8 input.bc
```

```bash
klee --kdalloc-quarantine=0 input.bc
```

```bash
klee --kdalloc-quarantine=-1 input.bc
```

--------------------------------

### Convert KLEE Stats to CSV using sqlite3

Source: https://klee-se.org/docs/tools

Use the sqlite3 command-line tool to query KLEE statistics and output them in CSV format. This is useful for custom data analysis and filtering.

```bash
$ sqlite3 <klee-out-dir>/run.stats
> SELECT * FROM stats

```

```bash
$ sqlite3 -csv -header run.stats "select Instructions,printf(\"%.2f\",100.0*CoveredInstructions/(CoveredInstructions+UncoveredInstructions)) AS 'Icov(%)',printf(\"%.2f\",1.0*SolverTime/60000000) AS 'SolverTime(min)',NumQueries from stats ORDER BY WallTime DESC LIMIT 1"
Instructions,Icov(%),SolverTime(min),NumQueries
2376923,3.96,51.77,514

```

--------------------------------

### klee_prefer_cex(object, condition)

Source: https://klee-se.org/docs/intrinsics

This function tells KLEE to prefer certain values when generating test cases as output. It should be called immediately after a klee_make_symbolic call. When KLEE has a choice between many possible test cases, it will prefer to use values that satisfy the condition.

```APIDOC
## `klee_prefer_cex(object, condition)`

### Description
This function tells KLEE to prefer certain values when generating test cases as output. A KLEE state can correspond to many different possible test cases. This function helps guide KLEE towards more readable or desirable test case outputs.

### Parameters
- **object**: The symbolic object for which to prefer certain values.
- **condition**: A boolean expression that specifies the preferred values. KLEE will attempt to generate test cases where this condition is true.

### Usage Notes
- **IMPORTANT:** Only use `klee_prefer_cex` immediately after a `klee_make_symbolic` call. It currently cannot be used after a `klee_range` call.
- When KLEE finds paths that conflict with the `klee_prefer_cex` condition, it will ignore the preference and generate (potentially unreadable) test cases anyway.
- The POSIX runtime uses `klee_prefer_cex` internally to prefer printable characters in symbolic command-line arguments. To enable this option, use `-readable-posix-inputs`. It is disabled by default, as `klee_prefer_cex` can be expensive when used extensively.

### Example
```c
char input[4];
klee_make_symbolic(input, sizeof(input), "input");
for (int i = 0; i < 4; i++)
  klee_prefer_cex(input, 32 <= input[i] && input[i] <= 126); // assume ASCII
assert(input[0] == 'Q');
```
```

--------------------------------

### KQuery Type Syntax

Source: https://klee-se.org/docs/kquery

Defines the syntax for type declarations in KQuery, specifying bit-width.

```kquery
type = "w[0-9]+"
```

--------------------------------

### Coreutils Symbolic Argument Generation

Source: https://klee-se.org/docs/coreutils-experiments

Default arguments used for symbolic execution of Coreutils applications. These arguments aim to trigger diverse behaviors with minimal options and input streams.

```bash
--sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdin 8 --sym-stdout
```

--------------------------------

### Control External Call Warnings

Source: https://klee-se.org/docs/options

Configure the frequency of warnings for external calls. Use `once-per-function` to limit warnings to a single instance per external function.

```bash
--external-call-warnings=once-per-function
```

--------------------------------

### KQuery Number Syntax

Source: https://klee-se.org/docs/kquery

Defines the syntax for numeric constants, including signed and various base formats.

```kquery
number = "true" | "false" | signed-constant
signed-constant = [ "+" | "-" ] ( dec-constant | bin-constant | oct-constant |
hex-constant )
dec-constant = "[0-9_]+"
bin-constant = "0b[01_]+"
oct-constant = "0o[0-7_]+"
hex-constant = "0x[0-9a-fA-F_]+"
```

--------------------------------

### Set Execution Tree Batch Size

Source: https://klee-se.org/docs/options

Specify the number of execution tree nodes to batch for writing. Defaults to 100.

```bash
--exec-tree-batch-size=<uint>
```

--------------------------------

### KQuery Bitwise Operations Syntax

Source: https://klee-se.org/docs/kquery

Defines the syntax for bitwise operations like And, Or, Xor, Shl, LShr, and AShr. These operations are binary and require matching types for operands.

```kquery
bitwise-expr-kind = ( "And" | "Or" | "Xor" | "Shl" | "LShr" | "AShr" )
expression = ") bitwise-expr-kind type expression expression )"
```

--------------------------------

### KQuery Array Versioning with Updates

Source: https://klee-se.org/docs/kquery

Refer to array versions by identifier or by specifying a list of writes. Most recent writes appear first.

```kquery
array small_array[2] : w32 -> w8 = symbolic # The array we will read from
```

```kquery
(Read w8 0 small_array) # No Updates to small_array
```

```kquery
(Read w8 1 [1=0xff] @ small_array) # Read from small_array at byte offset 1
with update where byte 1 set to decimal 255
```

--------------------------------

### Enable Code Optimization

Source: https://klee-se.org/docs/options

Optimize the code before execution using compiler optimization passes. This option is disabled by default.

```bash
--optimize
```

--------------------------------

### Set Instruction Stats Write Interval

Source: https://klee-se.org/docs/options

Specify the approximate time interval in seconds between writes of instruction-level statistics. Defaults to 10.0s.

```bash
-istats-write-interval=TIME
```

--------------------------------

### KQuery Zero-Extend (ZExt)

Source: https://klee-se.org/docs/kquery

Zero-extends a `child-expression` to a specified `type` by padding undefined bits with zeros.

```kquery
expression = ") "ZExt" type child-expression )"
```

--------------------------------

### Exit KLEE on Specific Error Types

Source: https://klee-se.org/docs/options

Configure KLEE to exit only when specific types of errors occur. Multiple error types can be specified.

```bash
klee -exit-on-error-type=Assert -exit-on-error-type=Ptr input.bc
```

--------------------------------

### Silently Terminate Infeasible Assumptions

Source: https://klee-se.org/docs/options

Use `-silent-klee-assume` to prevent KLEE from reporting an error when an assumed condition is infeasible, instead silently terminating the current path.

```bash
-silent-klee-assume
```

--------------------------------

### Set External Call Policy

Source: https://klee-se.org/docs/options

Control how KLEE handles calls to external functions. Use `--external-calls=all` to allow all external calls, concretizing symbolic arguments. Default is `concrete`.

```bash
--external-calls=all
```

--------------------------------

### Replacing _exit with exit for gcov

Source: https://klee-se.org/docs/coreutils-experiments

To ensure coverage information is recorded by gcov, replace calls to `_exit` with `exit`. This allows gcov's handler to execute and dump coverage data before program termination.

```c
exit
```

--------------------------------

### KQuery Logical Shift Left (Shl)

Source: https://klee-se.org/docs/kquery

Implements a logical shift left operation. Bits are shifted left, with new zero bits filling the rightmost positions.

```kquery
expression = ") "Shl" type X Y )"
```

--------------------------------

### KQuery Neg Macro

Source: https://klee-se.org/docs/kquery

A macro form to generate a subtraction from zero. Optionally accepts a `type`.

```kquery
expression = ") "Neg" [ type ] expression )"
```

--------------------------------

### KQuery Read Operation

Source: https://klee-se.org/docs/kquery

Reads from a versioned array. Evaluates to the first write in `version` matching `index-expression`. Type constraints apply to the expression and index.

```kquery
expression = ") "Read" type index-expression version )"
```

--------------------------------

### KQuery Reserved Keywords

Source: https://klee-se.org/docs/kquery

Lists reserved keywords in KQuery related to floating-point and integer types.

```kquery
floating-point-type = "fp[0-9]+([.].*)?"
integer-type = "i[0-9]+"
```

--------------------------------

### Optimize Parsing with Independent Queries

Source: https://klee-se.org/docs/kleaver-options

Enables optimization to reduce memory footprint when processing independent queries by clearing array declarations after each query.

```bash
$ kleaver --clear-array-decls-after-query=true klee-queries.kquery
```

--------------------------------

### KQuery Identifier Syntax

Source: https://klee-se.org/docs/kquery

Defines the syntax for identifiers used in KQuery for array names and expression labels.

```kquery
identifier = "[a-zA-Z_][a-zA-Z0-9._]*"
```

--------------------------------

### Set Stats Write Interval

Source: https://klee-se.org/docs/options

Specify the approximate time interval in seconds between writes of statistics. Defaults to 1.0s.

```bash
-stats-write-interval=TIME
```

--------------------------------

### KQuery Logical Shift Right (LShr)

Source: https://klee-se.org/docs/kquery

Implements a logical shift right operation. Bits are shifted right, with new zero bits filling the leftmost positions.

```kquery
expression = ") "LShr" type X Y )"
```

--------------------------------

### Limit Injected Failures in KLEE

Source: https://klee-se.org/docs/options

Set a maximum number of injected failures that KLEE will allow during execution. '-fd-fail' is a shortcut for allowing a single failure.

```bash
-max-fail <N>
```

```bash
-fd-fail
```

--------------------------------

### KQuery ReadLSB Macro

Source: https://klee-se.org/docs/kquery

Simplifies contiguous array accesses by concatenating read operations. Reads from `index-expression` form the least significant bits.

```kquery
expression = ") "ReadLSB" type index-expression version )"
```

--------------------------------

### Compress Execution Tree

Source: https://klee-se.org/docs/options

Remove intermediate nodes in the execution tree when possible to reduce its size. Defaults to false.

```bash
--compress-exec-tree
```

--------------------------------

### Stop Grafana Docker Container

Source: https://klee-se.org/docs/tools

Use the docker stop command to terminate the running Grafana container.

```bash
$ docker stop grafana

```

--------------------------------

### KQuery Bitwise NOT Operation

Source: https://klee-se.org/docs/kquery

Perform bitwise negation using the 'Not' operation. The result is the one's complement of the input expression. Type specification is optional but must match the expression type if provided.

```kquery
(Not [type] expression)
```

--------------------------------

### KQuery Arithmetic Shift Right (AShr)

Source: https://klee-se.org/docs/kquery

Implements an arithmetic shift right operation. Bits are shifted right, preserving the sign bit by copying the leftmost bit into new positions.

```kquery
expression = ") "AShr" type X Y )"
```

--------------------------------

### KQuery ReadMSB Macro

Source: https://klee-se.org/docs/kquery

Simplifies contiguous array accesses by concatenating read operations. Reads from `index-expression` form the most significant bits.

```kquery
expression = ") "ReadMSB" type index-expression version )"
```

--------------------------------

### KQuery Select Operation

Source: https://klee-se.org/docs/kquery

Conditionally evaluates to `true-expression` or `false-expression` based on `cond-expression`. The condition must be `w1` type.

```kquery
expression = ") "Select" type cond-expression true-expression false-
expression )"
```

--------------------------------

### KQuery Concat Operation

Source: https://klee-se.org/docs/kquery

Concatenates two bitvector expressions, `msb-expression` and `lsb-expression`, to form a new bitvector of the specified `type`.

```kquery
expression = ") "Concat" [type] msb-expression lsb-expression )"
```
Tokens:
Raw