Skip to content

Updated documentation for the execution tree options & tool, to be in… #375

New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

#

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Merged
merged 1 commit into from
Feb 29, 2024
Merged

Updated documentation for the execution tree options & tool, to be in… #375

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
0 content/ptree.png → content/exec-tree.png
View file
Open in desktop
File renamed without changes
8 changes: 4 additions & 4 deletions docs/options.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -171,10 +171,10 @@ There are several options to modify how KLEE outputs statistics:
* `--write-exec-tree` - Write execution tree into `exec_tree.db` (*default=false*)

Since symbolic execution aims to execute all feasible paths of a program, it creates an exploration tree instead of a single execution path.
KLEE maintains this tree in memory when either a searcher (e.g. `random-path`) depends on it or the user explicitly requests a copy on disk (`-write-ptree`).
To decrease the overhead of constant disk writes in the latter case, KLEE batches a number of nodes until it eventually writes them into an SQLite database (`ptree.db`).
The batching interval can be modified with `--ptree-batch-size`.
Afterwards, [klee-ptree]({{site.baseurl}}/docs/tools/#klee-ptree) can be used to convert the tree into an `.svg` file or to print some useful statistics.
KLEE maintains this tree in memory when either a searcher (e.g. `random-path`) depends on it or the user explicitly requests a copy on disk (`-write-exec-tree`).
To decrease the overhead of constant disk writes in the latter case, KLEE batches a number of nodes until it eventually writes them into an SQLite database (`exec_tree.db`).
The batching interval can be modified with `--exec-tree-batch-size`.
Afterwards, [klee-exec-tree]({{site.baseurl}}/docs/tools/#klee-exec-tree) can be used to convert the tree into an `.svg` file or to print some useful statistics.

Sometimes the traversal of deep execution trees with the `random-path` searcher can become quite costly.
`--compress-exec-tree` can help in this case by reducing paths of long chains of unary edges to a single edge:
Expand Down
12 changes: 6 additions & 6 deletions docs/tools.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -240,9 +240,9 @@ KLEE can subsequently be run with the `-seed-dir` option to seed further explora

Similar to `ktest-gen`, except that it generates random data for the `.ktest` file.

## klee-ptree
## klee-exec-tree

When KLEE was used with `--write-ptree`, `klee-ptree` can be used to show various statistics of the execution tree, e.g. branch information and information about the termination types of paths:
When KLEE was used with `--write-exec-tree`, `klee-exec-tree` can be used to show various statistics of the execution tree, e.g. branch information and information about the termination types of paths:

* `branches` - print branch statistics in `.csv` format
* `depths` - print depths statistics in `.csv` format
Expand All @@ -254,7 +254,7 @@ When KLEE was used with `--write-ptree`, `klee-ptree` can be used to show variou
Example usage:

```
$ klee-ptree branches klee-out-1
$ klee-exec-tree branches klee-out-1
branch type,count
Alloc,0
Br,55055
Expand All @@ -268,7 +268,7 @@ Switch,27091
IndirectBr,0
...

$ klee-ptree terminations klee-out-1
$ klee-exec-tree terminations klee-out-1
termination type,count
Exit,2230
Interrupted,48352
Expand All @@ -282,7 +282,7 @@ It also can be used to dump the tree in [Graphviz](https://graphviz.org/)' `.dot
We recommend `.svg` as it shows tooltips with e.g. state id, asm line, branch type.

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

[![]({{site.url}}/content/ptree.png){:.wide}]({{site.url}}/content/ptree.png)
[![]({{site.url}}/content/exec-tree.png){:.wide}]({{site.url}}/content/exec-tree.png)