\ingroup module_hidden \page goto-program-transformations Goto Program Transformations \section required-transforms Core Transformation Passes This section lists the transformation passes that must have been applied for the goto model to be in symex ready goto format. Note that the passes are listed below in the order they are currently called in CBMC. While all dependencies on the ordering are not fully documented, the following order should be used. \subsection assembly-transform Removal/Lowering of Assembly This pass goes through the goto model and removes or lowers instances of assembly intructions. Assembly instructions are stored in instances of the `other` instruction. The implementation of this pass is called via the \ref remove_asm(goto_modelt &, message_handlert &) function. For full documentation of this pass see \ref remove_asm.h This pass has no predecessor. \subsection linking-transform Linking of Standard Libraries This pass links the function definitions from the Cprover standard library models to the current goto model. The implementation of this pass is called via the \ref link_to_library(goto_modelt &, message_handlert &, const std::function &, const symbol_tablet &, symbol_tablet &, message_handlert &)> &) "link_to_library function." Predecessor pass is \ref assembly-transform . \subsection function-pointer-transform Removal/Lowering of Function Pointers This pass finds all the instructions which are function calls to the value of a function pointer. Each instruction is then replaced with a switch block. The switch block contains a case for each of the potential targets of the function pointer. The targets are found by looking for all functions in the goto program that approximately match the type of the function pointer. Note that for this pass to work as intended, all potential targets of calls to function pointers must be in the model. Otherwise they will not be added to the relevant switch blocks. This may cause the assertion that the switch blocks' fallthrough is unreachable to be shown to be violated via an invalid counter example. The implementation of this pass is called via the \ref remove_function_pointers(message_handlert &, goto_modelt &, bool) "remove_function_pointers" function. Detailed documentation of this pass belongs in \ref remove_function_pointers.h Predecessor pass is the \ref linking-transform or the optional \ref string-instrument-transform if it is being used. \subsection mmio-transform Memory Mapped IO Instrumentation This pass finds pointer dereferences and adds corresponding calls to the `__CPROVER_mm_io_r` and `__CPROVER_mm_io_w` modelling functions if they exist. See the device behaviour section of `modeling-mmio.md` for details of modeling memory-mapped I/O regions of device interfaces. This pass is always carried out but will only make changes if one of the modelling functions exist. The implementation of this pass is called via the \ref mm_io(goto_modelt &, message_handlert &) "mm_io" function. Further documentation of this pass can be found in \ref mm_io.h Predecessor pass is \ref function-pointer-transform . \subsection precondition-transform Instrument/Remove Preconditions This pass moves preconditions associated with functions to call sites rather than at the head of the function. Note that functions may have multiple call sites and in this case the instrumentation is copied to these multiple call sites. The implementation of this is called via \ref instrument_preconditions(goto_modelt &goto_model) . Documentation of this pass belongs in \ref instrument_preconditions.h Predecessor pass is \ref mmio-transform. \subsection returns-transform Removal/Lowering of Return Statements This pass replaces returns of values with writes and reads to global variables. The implementation of this is called via \ref remove_returns(goto_modelt &) . Detailed documentation of this pass can be found in \ref remove_returns.h The predecessor passes is the \ref precondition-transform or the optional \ref inlining-transform if is being used. \subsection vector-transform Remove/Lower Vector Typed Expressions This pass removes/lowers expressions corresponding to CPU instruction sets such as MMX, SSE and AVX. For more details on how this is done see vector_typet and remove_vector.cpp. The implementation of this is called via \ref remove_vector(goto_modelt &goto_model) Predecessor pass is \ref returns-transform. \subsection complex-transform Remove/Lower Complex Typed Expressions This pass is for the handling of complex numbers in the mathematical sense of a number consisting of paired real and imaginary parts. These are removed/lowered in this pass. The implementation of this is called via \ref remove_complex(goto_modelt &) . Documentation for this pass belongs in \ref remove_complex.h Predecessor pass is \ref vector-transform. \subsection unions-transform Rewrite Unions This pass converts union member access into byte extract and byte update operations. The implementation of this pass is called via \ref rewrite_union(goto_modelt &) Predecessor pass is \ref complex-transform. \subsection check-c-transform goto_check_c This is a pass that can add many checks and instrumentation largely related to the definition of the C language. Note that this transformation pass is mandatory in the current implementation, however it may have no effect depending on the command line options specified. The implementation of this pass is called via \ref goto_check_c(const optionst &, goto_modelt &, message_handlert &) Predecessor pass is \ref unions-transform. \subsection floats-transform Adjust Float Expressions This is a transform from general mathematical operations over floating point types into floating point specific operator variations which include a rounding mode. The implementation of this pass is called via \ref adjust_float_expressions(goto_modelt &) . Documentation of this pass can be found in \ref adjust_float_expressions.h Predecessor pass is \ref check-c-transform or the optional \ref assertions-transform if it is being used. \subsection update-transform Goto Functions Update This transformation updates in memory data goto program fields which may have been invalidated by previous passes. Note that the following are performed by this pass: - Incoming edges - Target numbers - location numbers - loop numbers The implementation of this pass is called via \ref goto_functionst::update() Predecessor pass is \ref floats-transform or the optional \ref string-abstraction-transform if it is being used. \subsection failed-symbols-transform Add Failed Symbols This pass adds failed symbols to the symbol table. See `src/pointer-analysis/add_failed_symbols.h` for details. The implementation of this pass is called via \ref add_failed_symbols(symbol_table_baset &) . The purpose of failed symbols is explained in the documentation of the function \ref goto_symext::dereference(exprt &, goto_symex_statet &, bool) Predecessor pass is \ref update-transform or the optional \ref nondet-transform if it is being used. \subsection remove-skip-transform Remove Skip Instructions This transformation removes skip instructions. Note that this transformation is called in many places and may be called as part of other transformations. This instance here is part of the mandatory transformation to reach symex ready goto format. If there is a use case where it is desirable to preserve a "no operation" instruction, a `LOCATION` type instruction may be used in place of a `SKIP` instruction. The `LOCATION` instruction has the same semantics as the `SKIP` instruction, but is not removed by the remove skip instructions pass. The implementation of this pass is called via \ref remove_skip(goto_modelt &) Predecessor pass is \ref failed-symbols-transform or the optional \ref unused-functions-transform if it is being used. \subsection properties-transform Label Properties This transformation adds newly generated unique property identifiers to assert instructions. The property identifiers are stored in the location data structure associated with each instruction. The implementation of this pass is called via \ref label_properties(goto_modelt &) Predecessor pass is \ref remove-skip-transform or the optional \ref coverage-transform if it is being used. \section optional-transforms Optional Transformation Passes The sections lists the optional transformation passes that are optional and will modify a goto model. Note that these are documented here for consistency, but not required for symex ready goto format. Note for each optional pass there is a listed predeceesor pass. This is the pass currently called before the listed pass in CBMC. While the ordering may not be fully documented, this should be followed. \subsection string-instrument-transform String Instrumentation This (optional) pass adds checks on calls to some of the C standard library string functions. It uses the tracking information added by the \ref string-abstraction-transform pass. It is switched on by the `--string-abstraction` command line option. The implementation of this pass is called via the \ref string_instrumentation(goto_modelt &goto_model) function. Detailed documentation of this pass belongs in \ref string_instrumentation.h The predecessor pass is \ref linking-transform . \subsection inlining-transform Partial Inlining This pass does partial inlining when this option is switched on. Partal inlining is inlining of functions either: marked as inline, or smaller than a specified limit. For further detail see the implementation function \ref goto_partial_inline(goto_modelt &, message_handlert &, unsigned, bool) Predecessor pass is \ref precondition-transform. \subsection assertions-transform Transform Assertions Assumptions This pass removes user provided assertions and assumptions when user has opted to do so. Note that this pass removes skip instructions if any other changes are made. The implementation of this pass is called via the \ref transform_assertions_assumptions(const optionst &, goto_modelt &) function. Predecessor pass is \ref check-c-transform. \subsection string-abstraction-transform String Abstraction This (optional) transformation pass adds tracking of length of C strings. It is switched on by the `--string-abstraction` command line option. This changes made by this pass are documented as part of the documentation for the \ref string_abstractiont class. The implementation of this pass is called via the \ref string_abstraction(goto_modelt &, message_handlert &) function. Predecessor pass is \ref floats-transform. \subsection nondet-transform Add Non-Deterministic Initialisation of Global Scoped Variables This transformation adds non-deterministic initialisation of global scoped variables including static variables. For details see `src/goto-instrument/nondet_static.h`. The initialisation code is added to the `CPROVER_initialize` function in the goto model. The implementation of this pass is called via the \ref nondet_static(goto_modelt &) function. Predecessor pass is \ref update-transform. \subsection unused-functions-transform Remove Unused Functions This pass removes unused functions from the goto model. In practice this builds a collection of all the functions that are potentially called, and then removes any function not in this collection. This pass cannot handle function calls via function pointers. Attempting to run this pass against a goto model which contains such a function call will result in an invariant violation. Therefore the function pointer removal pass must always be applied to the goto model before the remove unused functions pass. The implementation of this pass is called via the \ref remove_unused_functions(goto_modelt &, message_handlert &) function. Predecessor pass is \ref failed-symbols-transform. \subsection coverage-transform Add Coverage Goals This transformation adds coverage goals instrumentation and is only applied if the `--cover` option has been specified. The implementation of this pass is called via the \ref instrument_cover_goals(const cover_configt &, goto_modelt &, message_handlert &) function. Predecessor pass is \ref remove-skip-transform . \subsection slicing-transforms Slicing This includes several slicing passes as specified by various slicing command line options. The reachability slicer is enabled by the `--reachability-slice` command line option. The implementation of this pass is called via the \ref reachability_slicer(goto_modelt &, message_handlert &) function. The full slicer is enabled by the `--full-slice` command line option. The implementation of this pass is called via the \ref full_slicer(goto_modelt &, message_handlert &) function. Predecessor pass is \ref properties-transform .