CBMC
|
Class to generate havocking instructions for target expressions of a function contract's assign clause (replacement). More...
#include <havoc_assigns_clause_targets.h>
Public Member Functions | |
havoc_assigns_clause_targetst (const irep_idt &_function_id, const std::vector< exprt > &_targets, const goto_functionst &_functions, cfg_infot &_cfg_info, const source_locationt &_source_location, symbol_table_baset &_st, message_handlert &_message_handler) | |
void | get_instructions (goto_programt &dest) |
Generates the assigns clause replacement instructions in dest. More... | |
Public Member Functions inherited from instrument_spec_assignst | |
instrument_spec_assignst (const irep_idt &_function_id, const goto_functionst &_functions, cfg_infot &_cfg_info, symbol_table_baset &_st, message_handlert &_message_handler) | |
Class constructor. More... | |
void | track_spec_target (const exprt &expr, goto_programt &dest) |
Track an assigns clause target and generate snaphsot instructions and well-definedness assertions in dest. More... | |
void | track_stack_allocated (const symbol_exprt &symbol_expr, goto_programt &dest) |
Track a stack-allocated object and generate snaphsot instructions in dest. More... | |
bool | stack_allocated_is_tracked (const symbol_exprt &symbol_expr) const |
Returns true if the expression is tracked. More... | |
void | invalidate_stack_allocated (const symbol_exprt &symbol_expr, goto_programt &dest) |
Generate instructions to invalidate a stack-allocated object that goes DEAD in dest. More... | |
void | track_heap_allocated (const exprt &expr, goto_programt &dest) |
Track a whole heap-alloc object and generate snaphsot instructions in dest. More... | |
void | track_static_locals (goto_programt &dest) |
Searches the goto instructions reachable from the start to the end of the instrumented function's instruction to identify local static variables, declared directly in the function or indirectly in the functions it calls, add them to the stack-allocated set of tracked locations, and generates corresponding snapshot instructions in dest. More... | |
void | track_static_locals_between (goto_programt::const_targett it, const goto_programt::const_targett end, goto_programt &dest) |
Searches the goto instructions reachable between the given it and end target instructions to identify local static variables, declared directly in the function or indirectly in the functions it calls, add them to the stack-allocated set of tracked locations, and generates corresponding snapshot instructions in dest. More... | |
void | check_inclusion_assignment (const exprt &lhs, goto_programt &dest) const |
Generates inclusion check instructions for an assignment, havoc or havoc_object instruction. More... | |
void | check_inclusion_heap_allocated_and_invalidate_aliases (const exprt &expr, goto_programt &dest) |
Generates inclusion check instructions for an argument passed to free. More... | |
void | instrument_instructions (goto_programt &body, goto_programt::targett instruction_it, const goto_programt::targett &instruction_end, const std::function< bool(const goto_programt::targett &)> &pred={}) |
Instruments a sequence of instructions with inclusion checks. More... | |
template<typename C > | |
void | get_static_locals (std::insert_iterator< C > inserter) const |
Inserts the detected static local symbols into a target container. More... | |
Private Member Functions | |
void | havoc_if_valid (car_exprt car, goto_programt &dest) |
Generates instructions to conditionally havoc the given conditional address range expression car , adding results to dest . More... | |
void | havoc_static_local (car_exprt car, goto_programt &dest) |
Havoc a static local expression. More... | |
Private Attributes | |
const std::vector< exprt > & | targets |
const source_locationt & | source_location |
Additional Inherited Members | |
Protected Types inherited from instrument_spec_assignst | |
typedef std::unordered_map< irep_idt, location_intervalt > | covered_locationst |
Map type from function identifiers to covered locations. More... | |
typedef std::unordered_set< symbol_exprt, irep_hash > | propagated_static_localst |
using | cond_target_exprt_to_car_mapt = std::unordered_map< const conditional_target_exprt, const car_exprt, irep_hash > |
using | symbol_exprt_to_car_mapt = std::unordered_map< const symbol_exprt, const car_exprt, irep_hash > |
using | exprt_to_car_mapt = std::unordered_map< const exprt, const car_exprt, irep_hash > |
using | car_expr_listt = std::list< car_exprt > |
List of malloc'd conditional address ranges. More... | |
Protected Member Functions inherited from instrument_spec_assignst | |
void | traverse_instructions (const irep_idt ambient_function_id, goto_programt::const_targett it, const goto_programt::const_targett end, covered_locationst &covered_locations, propagated_static_localst &propagated) const |
Traverses the given list of instructions, updating the given coverage map, recursing into function calls only once. More... | |
void | collect_static_symbols (covered_locationst &covered_locations, std::unordered_set< symbol_exprt, irep_hash > &dest) |
Collects static symbols from the symbol table that have a source location included in one of the covered_locations and writes them into dest. More... | |
void | track_spec_target_group (const conditional_target_group_exprt &group, goto_programt &dest) |
Track and generate snaphsot instructions and target validity checking assertions for a conditional target group from an assigns clause. More... | |
void | track_plain_spec_target (const exprt &expr, goto_programt &dest) |
Track and generate snaphsot instructions and target validity checking assertions for a conditional target group from an assigns clause. More... | |
void | create_snapshot (const car_exprt &car, goto_programt &dest) const |
Returns snapshot instructions for a car_exprt. More... | |
exprt | target_validity_expr (const car_exprt &car, bool allow_null_target) const |
Returns the target validity expression for a car_exprt. More... | |
void | target_validity_assertion (const car_exprt &car, bool allow_null_target, goto_programt &dest) const |
Generates the target validity assertion for the given car and adds it to dest . More... | |
exprt | inclusion_check_single (const car_exprt &lhs, const car_exprt &candidate_car) const |
Returns inclusion check expression for a single candidate location. More... | |
exprt | inclusion_check_full (const car_exprt &lhs, bool allow_null_lhs, bool include_stack_allocated) const |
Returns an inclusion check expression of lhs over all tracked cars. More... | |
void | inclusion_check_assertion (const car_exprt &lhs, bool allow_null_lhs, bool include_stack_allocated, goto_programt &dest) const |
Returns an inclusion check assertion of lhs over all tracked cars. More... | |
void | invalidate_car (const car_exprt &tracked_car, const car_exprt &freed_car, goto_programt &result) const |
Adds an assignment in dest to invalidate the tracked car if was valid before and was pointing to the same object as the freed car. More... | |
void | invalidate_heap_and_spec_aliases (const car_exprt &freed_car, goto_programt &dest) const |
Generates instructions to invalidate all targets aliased with a car that was passed to free , assuming the inclusion check passes, ie. More... | |
bool | must_track_decl (const goto_programt::const_targett &target) const |
Returns true iff a DECL x must be explicitly added to the write set. More... | |
bool | must_track_dead (const goto_programt::const_targett &target) const |
Returns true iff a DEAD x must be processed to update the write set. More... | |
bool | must_track_decl_or_dead (const irep_idt &ident) const |
Returns true iff a function-local symbol must be tracked. More... | |
bool | must_check_assign (const goto_programt::const_targett &target) |
Returns true iff an ASSIGN lhs := rhs instruction must be instrumented. More... | |
void | instrument_assign_statement (goto_programt::targett &instruction_it, goto_programt &body) const |
Inserts an assertion in body immediately before the assignment at instruction_it , to ensure that the LHS of the assignment is included in the set of currently tracked CARs. More... | |
void | instrument_call_statement (goto_programt::targett &instruction_it, goto_programt &body) |
Inserts an assertion in body immediately before the function call at instruction_it , to ensure that all memory locations written to by the called function are included in the set of currently tracked CARs. More... | |
const car_exprt & | create_car_from_spec_assigns (const exprt &condition, const exprt &target) |
const car_exprt & | create_car_from_stack_alloc (const symbol_exprt &target) |
const car_exprt & | create_car_from_heap_alloc (const exprt &target) |
const car_exprt & | create_car_from_static_local (const symbol_exprt &target) |
car_exprt | create_car_expr (const exprt &condition, const exprt &target) const |
Creates a conditional address range expression from a cleaned-up condition and target expression. More... | |
Protected Attributes inherited from instrument_spec_assignst | |
const irep_idt & | function_id |
Name of the instrumented function. More... | |
const goto_functionst & | functions |
Other functions of the model. More... | |
cfg_infot & | cfg_info |
CFG information for simplification. More... | |
symbol_table_baset & | st |
Program symbol table. More... | |
const namespacet | ns |
Program namespace. More... | |
messaget | log |
Logger. More... | |
const irep_idt & | mode |
Language mode. More... | |
cond_target_exprt_to_car_mapt | from_spec_assigns |
Map from conditional target expressions of assigns clauses to corresponding conditional address ranges. More... | |
symbol_exprt_to_car_mapt | from_stack_alloc |
Map from DECL symbols to corresponding conditional address ranges. More... | |
car_expr_listt | from_heap_alloc |
symbol_exprt_to_car_mapt | from_static_local |
Map to from detected or propagated static local symbols to corresponding conditional address ranges. More... | |
Class to generate havocking instructions for target expressions of a function contract's assign clause (replacement).
Assigns clause targets can be interdependent as shown in this example:
To havoc these dependent targets simultaneously, we first take snapshots of their addresses, and havoc them in a second time. Snapshotting and havocking are both guarded by the validity of the target.
Definition at line 42 of file havoc_assigns_clause_targets.h.
|
inline |
_function_id | Name of the replaced function |
_targets | Assigns clause targets of the replaced function |
_functions | Other functions forming the GOTO model |
_cfg_info | CFG-based information on function symbols (not used) |
_source_location | Source location of the replaced function call (added to all generated instructions) |
_st | Symbol table of the model (new symbols will be added) |
_message_handler | handler used to log translation warnings/errors |
Definition at line 54 of file havoc_assigns_clause_targets.h.
void havoc_assigns_clause_targetst::get_instructions | ( | goto_programt & | dest | ) |
Generates the assigns clause replacement instructions in dest.
Definition at line 22 of file havoc_assigns_clause_targets.cpp.
|
private |
Generates instructions to conditionally havoc the given conditional address range expression car
, adding results to dest
.
Adds a special comment on the havoc instructions in order to trace back the origin of the havoc expressions to the function being replaced.
Generates these instructions for a __CPROVER_POINTER_OBJECT(...)
target:
Generates these instructions for an object slice target:
And generate these instructions otherwise:
Where target_type
is the type of the target expression.
Definition at line 55 of file havoc_assigns_clause_targets.cpp.
|
private |
Havoc a static local expression.
Definition at line 125 of file havoc_assigns_clause_targets.cpp.
|
private |
Definition at line 121 of file havoc_assigns_clause_targets.h.
|
private |
Definition at line 120 of file havoc_assigns_clause_targets.h.