Description
[Documenting a TODO rather than an immediate issue.]
Short version : we have 1.75 symex engines, maybe we should have 1 or 2.
In conversation with @marek-trtik today I realised that the current set-up and issues with symbolic execution were not widely known (probably because they are not documented!), so I'm opening this to record this, to warn people and to have as a TODO. Marek said that @Degiorgio might care about this if he isn't already aware.
-
The code in goto-symex/ should work for any kind of symbolic execution. The really key method is symex_step which computes the symbolic execution / strongest-post of one instruction. (We also have weakest pre but that uses different infrastructure).
-
cbmc/symex_bmc inherits from this and adds the BMC specific behaviour (for example, unwinding limits).
-
It would be nice to think that path-symex/ inherits from it and adds all of the per-path symex things (work queue, branching heuristics, incremental checking, incremental solvers, etc.). Unfortunately (my thanks to @danpoe for pointing this out) this is not the case, it has it's own implementation of /some/ of the symbolic execution functionality. symex and impara ( calling @bjowac ) both use this code-base
-
The problem is that path-symex doesn't support everything that goto-symex does, so it will crash on a lot of "real world" programs. Possible solutions:
A. Port the functionality from goto-symex to path-symex. Advantage : relatively straight-forward and doesn't require architectural changes, disadvantage : duplicate code.
B. Rewrite path-symex to use goto-symex : Advantage : should be mostly reducing the code / throwing things away, disadvantage : bigger job.
C. Rewrite anything that uses path-symex to goto-symex and throw it away. Advantage : possibly an easier job, disadvantage : will likely require rewriting some of the functionality of path-symex.