Documentation: this commit updates the README file in the

goto-symex directory. Specifically, it details the roles played by
symex_target_equationt and symex_targett in symex.

Author: Degiorgio

src/goto-symex/README.md

@@ -15,12 +15,22 @@ when analysis is incomplete.  The symbolic execution includes constant
 folding so loops that have a constant number of iterations will be
 handled completely (assuming the unwinding limit is sufficient).
 
-The output of the symbolic execution is a system of equations; an object
-containing a list of `symex_target_elements`, each of which are
-equalities between `expr` expressions. See `symex_target_equation.h`.
-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; 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.
@@ -95,47 +105,73 @@ 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:**
+* symex_targett
+* 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
+versioned (renamed) through the addition of a _suffix_.
+
+There are three “levels” of versioning:
+
+**Level 2 (L2):** variables are versioned every time they are encountered
+in a function.
+
+**Level 1 (L1):** variables are versioned every time the functions that
+contain those variables are called.
+
+**Level 0 (L0):** variables are versioned every time a new thread
+containing those variables are spawned.
+
+We can inspect the versioned variable names with the **–show-vcc** flag,
+this prints a string with 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.
+
+\subsection L1-L2 Level 1 and level 2 versioning
+
+The following examples illustrate Level 1 and 2 versioning.
 
     $ 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
@@ -150,6 +186,10 @@ 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.
 
+\subsection L0 Level 0 versioning
+
+TODO
+
 ---
 \section counter-example-production Counter Example Production