Skip to content

Commit 90b91fe

Browse files
committed
Updated documentation for the execution tree options & tool, to be in sync with the code
1 parent 6542ad3 commit 90b91fe

File tree

3 files changed

+10
-10
lines changed

3 files changed

+10
-10
lines changed
File renamed without changes.

docs/options.md

+4-4
Original file line numberDiff line numberDiff line change
@@ -171,10 +171,10 @@ There are several options to modify how KLEE outputs statistics:
171171
* `--write-exec-tree` - Write execution tree into `exec_tree.db` (*default=false*)
172172

173173
Since symbolic execution aims to execute all feasible paths of a program, it creates an exploration tree instead of a single execution path.
174-
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`).
175-
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`).
176-
The batching interval can be modified with `--ptree-batch-size`.
177-
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.
174+
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`).
175+
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`).
176+
The batching interval can be modified with `--exec-tree-batch-size`.
177+
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.
178178

179179
Sometimes the traversal of deep execution trees with the `random-path` searcher can become quite costly.
180180
`--compress-exec-tree` can help in this case by reducing paths of long chains of unary edges to a single edge:

docs/tools.md

+6-6
Original file line numberDiff line numberDiff line change
@@ -240,9 +240,9 @@ KLEE can subsequently be run with the `-seed-dir` option to seed further explora
240240

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

243-
## klee-ptree
243+
## klee-exec-tree
244244

245-
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:
245+
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:
246246

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

256256
```
257-
$ klee-ptree branches klee-out-1
257+
$ klee-exec-tree branches klee-out-1
258258
branch type,count
259259
Alloc,0
260260
Br,55055
@@ -268,7 +268,7 @@ Switch,27091
268268
IndirectBr,0
269269
...
270270
271-
$ klee-ptree terminations klee-out-1
271+
$ klee-exec-tree terminations klee-out-1
272272
termination type,count
273273
Exit,2230
274274
Interrupted,48352
@@ -282,7 +282,7 @@ It also can be used to dump the tree in [Graphviz](https://graphviz.org/)' `.dot
282282
We recommend `.svg` as it shows tooltips with e.g. state id, asm line, branch type.
283283

284284
```
285-
$ klee-ptree tree-dot klee-out-1 | dot -Tsvg > tree.svg
285+
$ klee-exec-tree tree-dot klee-out-1 | dot -Tsvg > tree.svg
286286
```
287287

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

0 commit comments

Comments
 (0)