[Bug-Candidate]: Internal Error: TODO: implement copySlice with a symbolically sized region

[rappie]

Describe the issue:

Got this error while testing symbolic execution on one of my fuzzing suites.

Code example to reproduce the issue:

https://github.com/perimetersec/drips-fuzzing

symExec: true

<snip>

# whether symbolic execution will be concolic (vs full symbolic execution)
# only relevant if symExec is true
symExecConcolic: true
# number of SMT solvers used in symbolic execution
# only relevant if symExec is true
symExecNSolvers: 1
# timeout for symbolic execution SMT solver
# only relevant if symExec is true
symExecTimeout: 30
# Number of times we may revisit a particular branching point
# only relevant if symExec is true and symExecConcolic is false
symExecMaxIters: 10
# 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
symExecAskSMTIters: 1

Version:

Latest master with symbolic execution

[rappie]

@samalws-tob

[rappie]

Looks like it keeps running, but now my memory usage is stable. Maybe the symexec worker crashed?

[ggrieco-tob]

The symbolic worker crashes and it won't recover (that's an know issue, but we need to open a new report for that). We should investigate the error.

[ggrieco-tob]

This error is a missing implementation (e.g. TODO) from the HEVM code. I assume it's a known issue from hevm, but perhaps it is useful to let then know it is reachable (so please create a report in their issue tracker and link this one). A few debug capabilities are coming to the echidna's symexec feature that will allow users to report in which transactions are actually causing a crash. These are going to be very useful for reporting issues.