This is written in the wiki entry of Symbolic Execution, but I can't find any reference for it. Can anyone show me a pointer? Thank you.
$\begingroup$
$\endgroup$
Add a comment
|
3 Answers
$\begingroup$
$\endgroup$
0
I am not aware of a paper concerned with the comparison between symbolic execution and abstract interpretation. Nor do I think one is needed. Reading the original descriptions of these two techniques should be enough.
- King, Symbolic Execution and Program Testing, 1976
- Cousot, Cousot, Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction of Approximation of Fixpoints, 1977
(Conversely, if there would be some unexpected connection, then that would be worth describing. But I very much doubt this is the case.)
The main idea of symbolic execution is that, at an arbitrary point in execution, you can express the values of all variables as functions of the initial values. The main idea of abstract interpretation is that you can systematically explore all executions of a program by a series of over-approximations. (I can hear several AI enthusiasts groaning at the previous approximation.)
Thus, at least in the original formulation, symbolic execution was not concerned with exploring all possible executions. You can see this even in the title: it includes the word ‘testing’. But here's more from Section 8: "For programs with infinite execution trees, the symbolic testing cannot be exhaustive and no absolute proof of correctness can be established."
In contrast, abstract interpretation aims to explore all executions. To do so, it uses several ingredients, one of which is very similar to the main idea of symbolic execution. These ingredients are (1) abstract states, (2) joining and widening (hence, ‘lattice’ in the title).
Abstract states. The concrete state of a program at a particular point in time is basically a snapshot of the memory content (including the program code itself and the program counter). This has a lot of detail, which is hard to track. When you analyze a particular property, you may want to ignore large parts of the concrete state. Or you may want to care only whether a particular variable is negative, zero, or positive, but not care about its exact value. In general, you want to consider an abstract version of the concrete state. For this to work out, you must have a commutativity property: If you take a concrete state, execute a statement, and then abstract the resulting state, you should obtain the same result as if you abstract the initial state, and then execute the same statement but on the abstract state. This commutativity diagram appears in both papers. This is the common idea. Again, abstract interpretation is more general, for it does not dictate how to abstract a state -- it just says there should be a way to do it. In contrast, symbolic execution says that you use (symbolic) expressions that mention the initial values.
Joining and Widening. If program execution reaches a certain statement in two different ways, symbolic execution does not try to merge the two analyzes. That is why the quote above talks about execution trees, rather than dags. But, remember that abstract interpretation wants to cover all executions. Thus, it asks for a way to merge the analyses of two executions at the point where they have the same program counter. (The join could be very dumb ({a} join {b} = {a,b}) such that it amounts to what symbolic execution does.) In general, joining itself is not sufficient to guarantee that you'll eventually finish analyzing all executions. (In particular, the dumb join mentioned earlier won't work.) Consider a program with a loops: "n=input(); for i in range(n): dostuff()". How many times should you go around the loop and keep joining? No fixed answer works. Thus, something else is needed, and that is widening, which can be seen as a heuristic. Suppose you went around the loop 3 times and you learned that "i=0 or i=1 or i=2". Then you say: hmmm, ... let's widen, and you get "i>=0". Again abstract interpretation does not say how to do widening -- it just says what properties widening should have to work out.
(Sorry for this long answer: I really didn't have time to make it shorter.)
$\begingroup$
$\endgroup$
2
I think this is meant in a very shallow sense. The first step of abstract interpretation is to identify a concrete collecting semantics. Rather than describe the evolution of a single state, collecting semantics describes the evolution of sets of states. Since symbolic execution reasons about the representations of sets of states, one can argue that it represents the concrete semantics of the program. I am not aware of a more precise correspondence being worked out.
-
$\begingroup$ Thank you. But if SE represents the concrete semantics then what is the abstract semantics. Without the abstract semantics, one can't say it is a case of AI. Could you explain a little bit more? By the way, I read your paper, SAT solvers are AI, it is really interesting. $\endgroup$– seanCommented Nov 9, 2013 at 6:12
-
3$\begingroup$ First, abstraction is a reflexive notion, meaning that every structure is a trivial abstraction of itself via the identity function. Second, symbolic execution will not compute the entire concrete semantics because only some program paths are explored, so in this sense, there is an underapproximating abstraction. $\endgroup$– Vijay DCommented Nov 9, 2013 at 6:55
$\begingroup$
$\endgroup$
See Patrick Cousot. Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique des programmes (Iterative methods for construction and approximation of fixpoints of monotone operators on lattices, program static analysis). Thèse ès Sciences Mathématiques, Université Joseph Fourier, Grenoble, France, 21 March 1978. https://cs.nyu.edu/~pcousot/publications.www/CousotTheseEsSciences1978.pdf (unfortunately in french), page (3)-27 to (3)-29
