Documentation: Overview of SSA

src/goto-symex/README.md

@@ -10,12 +10,21 @@ This takes a goto-program and translates it to an equation system by
 traversing the program, branching and merging and unwinding loops and recursion
 as needed.
 
-The output of the symbolic execution is a system of equations; an object
-containing a list of \ref symex_target_equationt::SSA_stept structures, each of
-which are equalities between \ref exprt expressions.
-The output is in static, single assignment (SSA) form, which is *not*
-the case for goto-programs.
+The output of symbolic execution is a system of equations, asserations and
+assumptions; an object of type `symex_target_equationt`, containing a list of
+`symex_target_equationt::SSA_stept`, each of which are equalities between
+`exprt` expressions. This list is constructed incrementally as the symbolic
+execution engine walks through the goto-program using the `symex_targett`
+interface. This interface (implemented by `symex_target_equationt`) exposes
+functions that append SSA steps into the aforementioned list while transforming
+expressions into Static Single Assignment (SSA) form. For more details on this
+process see `symex_target_equation.h`, for an overview of SSA see \ref
+static-single-assignment.
+
+At a later stage, BMC will convert the generated SSA steps into an
+equation that can be passed to the solver.
 
+---
 \section symbolic-execution Symbolic Execution
 
 In the \ref goto-symex directory.
@@ -135,47 +144,80 @@ execution run does not add any paths to the workqueue but rather merges
 all the paths together, so the additional path-exploration loop is
 skipped over.
 
-\subsection ssa-renaming SSA renaming levels
-
-In goto-programs, variable names get a prefix to indicate their scope
-(like `main::1::%foo` or whatever). At symbolic execution level, variables
-also get a _suffix_ because we’re doing single-static assignment. There
-are three “levels” of renaming. At Level 2, variables are renamed every
-time they are encountered in a function. At Level 1, variables are
-renamed every time the functions that contain those variables are
-called. At Level 0, variables are renamed every time a new thread
-containing those variables are spawned. We can inspect the renamed
-variable names with the –show-vcc flag, which prints a string with the
-following format: `%%s!%%d@%%d#%%d`. The string field is the variable name,
-and the numbers after the !, @, and # are the L0, L1, and L2 suffixes
-respectively. The following examples illustrate Level 1 and 2 renaming:
+---
+\section static-single-assignment Static Single Assignment (SSA) Form
+
+**Key classes:**
+* \ref symex_targett
+* \ref symex_target_equationt
+
+*Static Single Assignment (SSA)* form is an intermediate
+representation that satisfies the following properties:
+
+1. Every variable is *assigned exactly once*.
+2. Every variable must be *defined* before use.
+
+In-order to convert a goto-program to SSA form all variables are
+indexed (renamed) through the addition of a _suffix_.
+
+There are three “levels” of indexing:
+
+**Level 2 (L2):** variables are indexed every time they are
+encountered in a function.
+
+**Level 1 (L1):** variables are indexed every time the functions that
+contain those variables are called.
+
+**Level 0 (L0):** variables are indexed every time a new thread
+containing those variables are spawned.
+
+We can inspect the indexed variable names with the **--show-vcc** or
+**--program-only** flags. Variables in SSA form are printed in the
+following format: `%%s!%%d@%%d#%%d`. Where the string field is the
+variable name, and the numbers after the !, @, and # are the L0, L1,
+and L2 suffixes respectively.
+
+> Note: **--program-only** prints all the SSA steps in-order. In
+> contrast, **--show-vcc** will for each assertion print the SSA steps
+> (assumes, assignments and constraints only) that synthetically
+> precede the assertion. In the presence of multiple threads it will
+> also print SSA steps that succeed the assertion.
+
+\subsection L1-L2 Level 1 and level 2 indexing
+
+The following examples illustrate Level 1 and 2 indexing.
 
     $ cat l1.c
-    int main() {
+    int main()
+    {
       int x=7;
       x=8;
       assert(0);
     }
+
     $ cbmc --show-vcc l1.c
     ...
     {-12} x!0@1#2 == 7
     {-13} x!0@1#3 == 8
 
-That is, the L0 names for both xs are 0; the L1 names for both xs are 1;
-but each occurrence of x within main() gets a fresh L2 suffix (2 and 3,
-respectively).
+That is, the L0 names for both x's are 0; the L1 names for both x's
+are 1; but each occurrence of x within main() gets a fresh L2 suffix
+(2 and 3, respectively).
 
     $ cat l2.c
-    void foo(){
+    void foo()
+    {
       int x=7;
       x=8;
       x=9;
     }
-    int main(){
+    int main()
+    {
       foo();
       foo();
       assert(0);
     }
+
     $ cbmc --show-vcc l2.c
     ...
     {-12} x!0@1#2 == 7
@@ -186,23 +228,42 @@ respectively).
     {-17} x!0@2#4 == 9
 
 That is, every time we enter function foo, the L1 counter of x is
-incremented (from 1 to 2) and the L0 counter is reset (back to 2, after
-having been incremented up to 4). The L0 counter then increases every
-time we access x as we walk through the function.
+incremented (from 1 to 2) and the L2 counter is reset (back to 2,
+after having been incremented up to 4). The L2 counter then increases
+every time we access x as we walk through the function.
+
+\subsection L0 Level 0 indexing (threads only)
+
+TODO: describe and give a concrete example
+
+\subsection PL Relevant Primary Literature
+
+Thread indexing is based on the following paper:
+
+> Lee, J., Midkiff, S.P. and Padua, D.A., 1997, August. Concurrent
+> static single assignment form and constant propagation for
+> explicitly parallel programs. In International Workshop on Languages
+> and Compilers for Parallel Computing (pp. 114-130). Springer,
+> Berlin, Heidelberg.
+
+Seminal paper on SSA:
+
+> Rosen, B.K., Wegman, M.N. and Zadeck, F.K., 1988, January. Global
+> value numbers and redundant computations. In Proceedings of the 15th
+> ACM SIGPLAN-SIGACT symposium on Principles of programming languages
+> (pp. 12-27). ACM.
 
 ---
 \section counter-example-production Counter Example Production
 
 In the \ref goto-symex directory.
 
-
-
 **Key classes:**
-* symex_target_equationt
-* prop_convt
+* \ref symex_target_equationt
+* \ref prop_convt
 * \ref bmct
-* fault_localizationt
-* counterexample_beautificationt
+* \ref fault_localizationt
+* \ref counterexample_beautificationt
 
 \dot
 digraph G {