cprover
|
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, const source_locationt &_source_location, symbol_tablet &_st, message_handlert &_message_handler) | |
void | get_instructions (goto_programt &dest) |
Generates the assigns clause replacement instructions in dest. More... | |
![]() | |
instrument_spec_assignst (const irep_idt &_function_id, const goto_functionst &_functions, symbol_tablet &_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) |
Search the call graph reachable from the instrumented function to identify local static variables used directly or indirectly, add them to the stack-allocated tracked locations, and generate corresponding snapshot instructions in dest. More... | |
void | check_inclusion_assignment (const exprt &lhs, optionalt< cfg_infot > &cfg_info_opt, goto_programt &dest) |
Generates inclusion check instructions for an assignment, havoc or havoc_object instruction. More... | |
void | check_inclusion_heap_allocated_and_invalidate_aliases (const exprt &expr, optionalt< cfg_infot > &cfg_info_opt, goto_programt &dest) |
Generates inclusion check instructions for an argument passed to free. 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... | |
Private Attributes | |
const std::vector< exprt > & | targets |
const source_locationt & | source_location |
Additional Inherited Members | |
![]() | |
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 > |
![]() | |
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... | |
const symbolt | create_fresh_symbol (const std::string &suffix, const typet &type, const source_locationt &location) const |
Creates a fresh symbolt with given suffix, scoped to function_id. 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, optionalt< cfg_infot > &cfg_info_opt) 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, optionalt< cfg_infot > &cfg_info_opt, 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... | |
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) |
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... | |
![]() | |
const irep_idt & | function_id |
Name of the instrumented function. More... | |
const goto_functionst & | functions |
Other functions of the model. More... | |
symbol_tablet & | st |
Program symbol table. More... | |
const namespacet | ns |
Program namespace. More... | |
messaget | log |
Logger. More... | |
cond_target_exprt_to_car_mapt | from_spec_assigns |
Map to from conditional target expressions of assigns clauses to corresponding conditional address ranges. More... | |
symbol_exprt_to_car_mapt | from_stack_alloc |
Map to from DECL symbols to corresponding conditional address ranges. More... | |
exprt_to_car_mapt | from_heap_alloc |
Map to from malloc'd symbols to corresponding conditional address ranges. More... | |
Class to generate havocking instructions for target expressions of a function contract's assign clause (replacement).
replaced_function_id | Name of the replaced function |
goto_functions | Other functions forming the GOTO model |
targets | Assigns clause targets for the replaced function |
source_location | Source location of the replaced function call (added to all generated instructions) |
mode | Language mode to use for newly generated symbols |
ns | Namespace of the model |
st | Symbol table of the model (new symbols will be added) |
message_handler | handler used to log translation warnings/errors |
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 54 of file havoc_assigns_clause_targets.h.
|
inline |
Definition at line 57 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 31 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:
And generate these instructions otherwise:
Where target_type
is the type of the target expression.
Definition at line 59 of file havoc_assigns_clause_targets.cpp.
|
private |
Definition at line 105 of file havoc_assigns_clause_targets.h.
|
private |
Definition at line 104 of file havoc_assigns_clause_targets.h.