Merge pull request #3383 from smowton/smowton/docs/goto-model-creation

Improve GOTO programs high-level documentation

Author: smowton

src/goto-programs/README.md

@@ -30,6 +30,15 @@ used depends on whether it is internal or being presented to the user.
 The comment lines are generated from the `source_location` field
 of the `instructiont` structure.
 
+GOTO programs are commonly produced using the `initialize_goto_model` function,
+which combines the complete process from command-line arguments specifying
+source code files, through parsing and generating a symbol table, to finally
+producing GOTO functions.
+
+Alternatively `lazy_goto_modelt` can be used, which facilitates producing GOTO
+functions on demand. See \ref section-lazy-conversion for more details on this
+method.
+
 \section goto_data_structures Data Structures
 
 A \ref goto_functionst object contains a set of GOTO programs. Note the
@@ -86,23 +95,19 @@ digraph G {
 At this stage, CBMC constructs a goto-program from a symbol table.
 Each symbol in the symbol table with function type (that is, the symbol's `type`
 field contains a \ref code_typet) will be converted to a corresponding GOTO
-program.
-
-It does not use the parse tree or the source file at all for this step. This
-may seem surprising, because the symbols are stored in a hash table and
-therefore have no intrinsic order; nevertheless, every \ref symbolt is
-associated with a \ref source_locationt, allowing CBMC to figure out the
-lexical order.
-
-The structure of what is informally called a goto-program follows.  The
-entire target program is converted to a single \ref goto_functionst
-object. The goto functions contains a set of \ref goto_programt objects;
-each of these correspond to a "function" or "method" in the target
-program. Each goto_program contains a list of
-\ref goto_programt::instructiont "instructions"; each
-instruction contains an associated statement---these are subtypes of
-\ref codet. Each instruction also contains a "target", which will be
-empty for now.
+program. The parse tree and source file are not used at all for this step.
+
+The conversion happens in two phases:
+
+1. Function `goto_convertt::convert` turns each `codet` in the symbol table
+   into corresponding GOTO instructions.
+2. `goto_convertt::finish_gotos` and others populate the `GOTO` and `CATCH`
+   instructions' `targets` members, pointing to their possible successors.
+   `DEAD` instructions are also added when GOTO instructions branch out of one
+   or more lexical blocks.
+
+Here is an example of a simple C program being converted into GOTO code (note
+the `targets` member of each instruction isn't populated yet):
 
 \dot
 digraph G{
@@ -241,39 +246,10 @@ void foo(){}"];
 }
 \enddot
 
-This is not the final form of the goto-functions, since the lists of
-instructions will be 'normalized' in the next step (Instrumentation),
-which removes some instructions and adds targets to others.
-
----
-\section instrumentation Instrumentation
-
-In the \ref goto-programs directory.
-
-**Key classes:**
-* goto_programt
-* goto_functionst
-* \ref goto_programt::instructiont
-
-\dot
-digraph G {
-  node [shape=box];
-  rankdir="LR";
-  1 [shape=none, label=""];
-  2 [label="goto conversion"];
-  3 [shape=none, label=""];
-  1 -> 2 [label="goto-programs, goto-functions, symbol table"];
-  2 -> 3 [label="transformed goto-programs"];
-}
-\enddot
-
-This stage applies several transformations to the goto-programs from the
-previous stage:
-
-* The diagram in the previous stage showed a goto_programt with four
-  instructions, but real programs usually yield instruction lists that
-  are littered with \ref code_skipt "skip" statements. The
-  instrumentation stage removes the majority of these.
+The `codet` representation of method bodies that is stored in the symbol table
+resembles C code quite strongly: it uses lexical variable scoping and has
+complex control-flow constructs such as `code_whilet` and `code_ifthenelset`.
+In converting to a GOTO program this structure is changed in several ways:
 
 * Variable lifespan implied by \ref code_declt instructions and lexical scopes
   described by \ref code_blockt nodes is replaced by `DECL` and corresponding
@@ -322,14 +298,63 @@ previous stage:
   instruction. Each goto_programt should have precisely one such
   instruction.
 
-This stage concludes the *analysis-independent* program transformations.
-
-\subsection goto-program-example-section Example:
-
-\subsubsection goto-program-example-1-section Unsigned mult (unsigned a, unsigned b) { int acc, i; for (i = 0; i < b; i++) acc += a; return acc; }
-
-To be documented.
-
+\section section-goto-transforms Subsequent Transformation
+
+It is normal for a program that calls `goto_convert` to immediately pass the
+GOTO functions through one or more transformations. For example, the ubiquitous
+`remove_returns` transformation turns the method return sequence generated by
+`goto_convert` (something like `RETURN x; GOTO end;`) into
+`function_name#return_value = x; GOTO end;`, and a callsite
+`y = function_name();` into `function_name(); y = function_name#return_value;`.
+
+Some subsequent parts of the CBMC pipeline assume that one or more of these
+transforms has been applied, making them effectively mandatory in that case.
+
+Common transformations include:
+
+* Removing superfluous SKIP instructions (`remove_skip`)
+* Converting indirect function calls into dispatch tables over direct calls
+  (`remove_virtual_functions` and `remove_function_pointers`)
+* Adding checks for null-pointer dereferences, arithmetic overflow and other
+  undefined behaviour (`goto_check`)
+* Adding code coverage assertions (`instrument_cover_goals`).
+
+By convention these post-convert transformations are applied by a driver program
+in a function named `process_goto_program` or `process_goto_functions`; examples
+of these can be found in `cbmc_parse_optionst`, `goto_analyzer_parse_optionst`
+and `goto_instrument_parse_optionst` among others.
+
+\section section-lazy-conversion Lazy GOTO Conversion
+
+The conventional source-code-to-GOTO-program pipeline is horizontally
+structured: all source-file information is converted into a symbol table, then
+each symbol-table method is converted into a GOTO program, then each transform
+is run over the whole GOTO-model in turn. This is fine when the GOTO model
+consumer will use most or all of the results of conversion, but if not then
+lazy conversion may be beneficial.
+
+Lazy conversion is coordinated by `lazy_goto_modelt`. Early source code parsing
+proceeds as usual, but while the same symbol table symbols are created as using
+`initialize_goto_model`, method bodies in the symbol table are not populated.
+`lazy_goto_modelt::get_goto_function` then allows each function to be converted
+on demand, passing individually through symbol-table `codet` production, GOTO
+conversion and driver-program transformation.
+
+`goto_symext` is able to use such a lazy GOTO model in place of the usual
+`goto_modelt`, enabling it to create GOTO programs on demand, and thus avoid
+spending time and memory generating GOTO programs that symex determines cannot
+in fact be reached. This is particularly useful when the source program contains
+many indirect calls (virtual function calls, or calls via function pointer), as
+the `remove_virtual_functions` and `remove_function_pointers` passes treat these
+very conservatively, producing large dispatch tables of possible callees which
+symex often finds to be largely unreachable.
+
+JBMC exhibits typical usage of `lazy_goto_modelt` when it is called with
+`--symex-driven-lazy-loading`. It defines a function
+`jbmc_parse_optionst::process_goto_function` which performs driver-program-
+specific post-GOTO-convert transformation. The lazy GOTO model is then passed to
+`goto_symext`, which will trigger symbol-table population, GOTO conversion
+and post-processing as needed.
 
 \section section-goto-binary Binary Representation