from Hacker News

A gentle introduction to symbolic execution

by joelburget on 4/8/19, 2:57 PM with 27 comments

  • by triska on 4/8/19, 4:27 PM

    Very nice, thank you for sharing this!

    Symbolic execution is also known as abstract interpretation. The program is being interpreted, with concrete values abstracted away, generalized to symbolic elements that often denote several or even infinitely many concrete values.

    Logic programming languages like Prolog are especially amenable to abstract interpretation, since we can absorb the Prolog system's built-in binding environment for variables, and simply plug in different values for the existing variables. We only have to reify unification, i.e., implement it within the language with suitable semantics.

    An impressive application of this idea is contained in the paper Meta-circular Abstract Interpretation in Prolog by Michael Codish and Harald Søndergaard:

    http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.137....

    As one of the examples, the authors show how abstract interpretation over the abstract parity domain {zero, one, even, odd} can be used to derive non-trivial facts about the Ackermann function.

    In particular, they deduce that Ackermann(i,j) is odd and greater than 1 for all i greater than 1, by taking a Prolog implementation of the Ackermann function, and interpreting it with these abstract domain elements instead of all concrete values (which would not terminate, since there are infinitely many concrete values). This is computed by fixpoint computation, determining the deductive closure of the relation.

  • by joelburget on 4/8/19, 4:33 PM

    Co-author here. We're planning to turn this into a series, with additional posts on how symbolic execution works at a lower level, how to present counterexamples to users, and ideas for future programming tools built on symbolic execution.

  • by souprock on 4/8/19, 9:05 PM

    There are actual jobs, in industry, making use of this stuff. For example, here is one that I put in the "Who is hiring?" item this month:

    https://news.ycombinator.com/item?id=19543995

    Typically one would convert a binary executable into some other form, then analyze it to find all possible bugs. Of course one quickly slams into troubles like the halting problem, but it is still usually possible to gain useful understanding of the binary executable.

  • by kazinator on 4/8/19, 10:47 PM

    When a program has a free variable, we can consider an entire space of possible execution paths, one for each possible value the variable could take.

    Or we could put on a greasy old pragmatic ball cap and issue an "unbound variable in line 42" error.

    A free free variable has no "possible value". If a variable has a value, it has a binding; if it has a binding, it is not a free variable.

    If we suspect that the variable is not actually free, but rather its definition has not yet appeared, we can defer the processing. Perhaps capture a continuation of the symbolic execution machine, and dispatch it later.

    If the expression which refers to the free variable is not actually evaluated (as our symbolic execution shows), we can squelch the warning, or change its wording.

    The idea that a free variable is implicitly universally quantified works in logic, but it doesn't transfer to an ordinary programming language (i.e. not Prolog, and its ilk) very well.

  • by llamathrowaway on 4/8/19, 9:27 PM

    Thank you for this. However the labels 'syntax Haskell' and 'syntax LLVM' do not seem to display properly on Firefox. Wish you could find a way to fix them.

  • by bediger4000 on 4/8/19, 5:04 PM

    I visited this expecting a tutorial about burning someone in effigy. Imagine my surprise!

  • by fwip on 4/9/19, 12:47 AM

    When you say “what is the result when x is 3 and y is 100?” - shouldn't the answer be 113, not 103?