[cfe-dev] Questions about symbolic execution in the static analyzer.

Kriso, Achim via cfe-dev cfe-dev at lists.llvm.org
Fri Jun 4 12:09:06 PDT 2021


Hello,

I am researching various static analyzers and want to get a better understanding of how the symbolic execution in the clang static analyzer works.

Every implementation of symbolic execution has to make certain tradeoffs to be feasible.

I'm interested in the following issues:

How does the static analyzer approach the path explosion problem?
In this [1] presentation it is mentioned that there are budgets which limit the exploration after visiting the same node multiple times.
Are there any additional techniques to alleviate path explosion?

Secondly, I'm am wondering how it deals with symbolic values as indices for arrays (or symbolic pointer arithmetic).
I have read the paper about its memory model [2], but it doesn't seem to address this question.
All the approaches to the problem I know rely either on address concretization, creating a new path for every possible index or using a more powerful constraint solver (for example using theory of arrays).

I hope you can answer my questions.

Sincerely,
Achim Kriso

[1] https://www.youtube.com/watch?v=4n3l-ZcDJNY
[2] http://lcs.ios.ac.cn/~xzx/memmodel.pdf


More information about the cfe-dev mailing list