- Generated by
1.9.1
|
CBMC
|
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.
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 remove_asm(goto_modelt &, message_handlert &) function. For full documentation of this pass see remove_asm.h
This pass has no predecessor.
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 link_to_library function.
Predecessor pass is Removal/Lowering of Assembly .
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 remove_function_pointers function. Detailed documentation of this pass belongs in remove_function_pointers.h
Predecessor pass is the Linking of Standard Libraries or the optional String Instrumentation if it is being used.
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 mm_io function. Further documentation of this pass can be found in mm_io.h
Predecessor pass is Removal/Lowering of Function Pointers .
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 instrument_preconditions(goto_modelt &goto_model) . Documentation of this pass belongs in instrument_preconditions.h
Predecessor pass is Memory Mapped IO Instrumentation.
This pass replaces returns of values with writes and reads to global variables.
The implementation of this is called via remove_returns(goto_modelt &) . Detailed documentation of this pass can be found in remove_returns.h
The predecessor passes is the Instrument/Remove Preconditions or the optional Partial Inlining if is being used.
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 remove_vector(goto_modelt &goto_model)
Predecessor pass is Removal/Lowering of Return Statements.
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 remove_complex(goto_modelt &) . Documentation for this pass belongs in remove_complex.h
Predecessor pass is Remove/Lower Vector Typed Expressions.
This pass converts union member access into byte extract and byte update operations.
The implementation of this pass is called via rewrite_union(goto_modelt &)
Predecessor pass is Remove/Lower Complex Typed Expressions.
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 goto_check_c(const optionst &, goto_modelt &, message_handlert &)
Predecessor pass is Rewrite Unions.
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 adjust_float_expressions(goto_modelt &) . Documentation of this pass can be found in adjust_float_expressions.h
Predecessor pass is goto_check_c or the optional Transform Assertions Assumptions if it is being used.
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:
The implementation of this pass is called via goto_functionst::update()
Predecessor pass is Adjust Float Expressions or the optional String Abstraction if it is being used.
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 add_failed_symbols(symbol_table_baset &) . The purpose of failed symbols is explained in the documentation of the function goto_symext::dereference(exprt &, statet &, bool)
Predecessor pass is Goto Functions Update or the optional Add Non-Deterministic Initialisation of Global Scoped Variables if it is being used.
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 remove_skip(goto_modelt &)
Predecessor pass is Add Failed Symbols or the optional Remove Unused Functions if it is being used.
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 label_properties(goto_modelt &)
Predecessor pass is Remove Skip Instructions or the optional Add Coverage Goals if it is being used.
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.
This (optional) pass adds checks on calls to some of the C standard library string functions. It uses the tracking information added by the String Abstraction pass. It is switched on by the --string-abstraction command line option.
The implementation of this pass is called via the string_instrumentation(goto_modelt &goto_model) function. Detailed documentation of this pass belongs in string_instrumentation.h
The predecessor pass is Linking of Standard Libraries .
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 goto_partial_inline(goto_modelt &, message_handlert &, unsigned, bool)
Predecessor pass is Instrument/Remove Preconditions.
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 transform_assertions_assumptions(const optionst &, goto_modelt &) function.
Predecessor pass is goto_check_c.
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 string_abstractiont class. The implementation of this pass is called via the string_abstraction(goto_modelt &, message_handlert &) function.
Predecessor pass is Adjust Float Expressions.
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 nondet_static(goto_modelt &) function.
Predecessor pass is Goto Functions Update.
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 remove_unused_functions(goto_modelt &, message_handlert &) function.
Predecessor pass is Add Failed Symbols.
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 instrument_cover_goals(const cover_configt &, goto_modelt &, message_handlert &) function.
Predecessor pass is Remove Skip Instructions .
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 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 full_slicer(goto_modelt &, message_handlert &) function.
Predecessor pass is Label Properties .
Last modified: 2024-05-06 15:55:43 +0200
1.9.1