Repository navigation
Idea : Simplify and improve the symbolic execution code in the symex tool #749
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.
Activity
martin-cs commentedon Apr 3, 2017
Sorry; wrong Daniel, I meant my thanks to @DanielNeville (who may have some relevant code / pointers / suggestions).
[-]Simplify and improve the symbolic execution code in the symex tool[/-][+]Idea : Simplify and improve the symbolic execution code in the symex tool[/+]Degiorgio commentedon Apr 3, 2017
My personal opinion is that we should go with option B) I don't think there are any advantages in having two modules that are essentially trying to do the same thing.
martin-cs commentedon Apr 3, 2017
@Degiorgio If you have a spare 15 minutes or so (ha ha), is there any chance you could have a look at the interfaces and give a rough guestimate of how long it might take to do B?
Shout out to @DanielNeville @johnfxgalea and @SeanHeelan who might have opinions on the subject.
DanielNeville commentedon May 4, 2017
Hi, With regards to this:
I agree with @Degiorgio that option B makes the most sense. Looking at symex/path_search.cpp, it feels like the "swap" point from path-symex code to existing CBMC bmc code should be around line 136.
https://github.com/diffblue/cbmc/blob/master/src/symex/path_search.cpp#L136
This is the main point where the code jumps from handling the queue, selecting a state, etc, to actually manipulating an object which contains a path constraint. It currently links into path_symex.cpp and other files within the path-symex folder, which are disjoint from the existing code.
martin-cs commentedon Aug 11, 2017
@theyoucheng may have made some progress on this...
tautschnig commentedon Aug 11, 2017
Is there any code to look at?
theyoucheng commentedon Aug 11, 2017