Skip to content

Update echidna configuration.md to include symbolic execution documentation #404

New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Merged
merged 7 commits into from
Sep 5, 2025
Merged

Update echidna configuration.md to include symbolic execution documentation #404

Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
602d13b
Update echidna configuration.md to include symbolic execution documen…
gustavo-grieco Aug 21, 2025
cbd0403
Apply suggestions from code review
gustavo-grieco Aug 21, 2025
c5107d4
Update configuration.md
gustavo-grieco Aug 21, 2025
7c04b86
Update configuration.md
gustavo-grieco Aug 21, 2025
f1ea943
Update program-analysis/echidna/configuration.md
gustavo-grieco Aug 21, 2025
726f177
Update configuration.md
gustavo-grieco Aug 21, 2025
f35035e
lint
gustavo-grieco Sep 5, 2025
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
70 changes: 46 additions & 24 deletions program-analysis/echidna/configuration.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -375,49 +375,54 @@ Run events server on the given port.

### `symExec`

| Type | Default | Available in |
| ---- | ------- | ------------ |
| Bool | `false` | 2.2.4+ |
| Type | Default | Available in | CLI equivalent |
| ---- | ------- | ------------ | -------------- |
| Bool | `false` | 2.2.4+ | `--sym-exec` |

Whether to add an additional symbolic execution worker.

### `symExecConcolic`

| Type | Default | Available in |
| ---- | ------- | ------------ |
| Bool | `true` | 2.2.4+ |

Whether symbolic execution will be concolic (vs full symbolic execution). Only
relevant if `symExec` is true.

### `symExecNSolvers`

| Type | Default | Available in |
| ---- | ------- | ------------ |
| Int | `1` | 2.2.4+ |
| Type | Default | Available in | CLI equivalent |
| ---- | ------- | ------------ | ---------------------- |
| Int | `1` | 2.2.4+ | `--sym-exec-n-solvers` |

Number of SMT solvers used in symbolic execution. While there is a single
symExec worker, N threads may be used to solve SMT queries. Only relevant if
`symExec` is true.

### `symExecTimeout`

| Type | Default | Available in | CLI equivalent |
| ---- | ------- | ------------ | -------------------- |
| Int | `30` | 2.2.4+ | `--sym-exec-timeout` |

Timeout for symbolic execution SMT solver per formula to solve. Only relevant if `symExec` is true.

### `symExecSMTSolver`

| Type | Default | Available in |
| ------ | ---------- | ------------ |
| String | `bitwuzla` | 2.2.8+ |

The SMT solver used when doing symbolic execution. Valid values are: "cvc5", "z3" and "bitwuzla". Only relevant if `symExec` is true.

### `symExecMaxExplore`

| Type | Default | Available in |
| ---- | ------- | ------------ |
| Int | `30` | 2.2.4+ |
| Int | `10` | 2.2.8+ |

Timeout for symbolic execution SMT solver. Only relevant if `symExec` is true.
When the SMT solver used is Z3, this timeout applies per query, and is not
global.
Number of states in exponents of 2 (i.e. 2^10 states) that we may explore using symbolic execution. Only relevant if
`symExec` is true.

### `symExecMaxIters`

| Type | Default | Available in |
| ---- | ------- | ------------ |
| Int | `10` | 2.2.4+ |
| Int | `5` | 2.2.4+ |

Number of times we may revisit a particular branching point. Only relevant if
`symExec` is true and `symExecConcolic` is false.
Number of times we may revisit a particular branching point. Only relevant if `symExec` is true.

### `symExecAskSMTIters`

Expand All @@ -426,8 +431,17 @@ Number of times we may revisit a particular branching point. Only relevant if
| Int | `1` | 2.2.4+ |

Number of times we may revisit a particular branching point before we consult
the smt solver to check reachability. Only relevant if `symExec` is true and
`symExecConcolic` is false.
the smt solver to check reachability. Only relevant if `symExec` is true.

### `symExecTargets`

| Type | Default | Available in | CLI Equivalent |
| -------- | ------- | ------------ | ------------------- |
| [String] | `null` | 2.2.4+ | `--sym-exec-target` |

List of whitelisted functions for using symbolic exploration. When set to null,
all functions are eligible. If used in the CLI, it will only allow a single target.
Only relevant if `symExec` is true.

### `disableSlither`

Expand Down Expand Up @@ -497,3 +511,11 @@ introduction of on-chain fuzzing in Echidna, it had become deprecated, and was l

Enabled the collection of worst-case gas usage. The information was stored as
part of the corpus on the `gas_info` field. This functionality was experimental.

### `symExecConcolic`

| Type | Default | Available in |
| ---- | ------- | -------------- |
| Bool | `true` | \* until 2.2.7 |

This option controlled whether symbolic execution will be concolic (vs full symbolic execution). It has been removed from the current version of Echidna.