cprover
|
A class that generates instrumentation for assigns clause checking. More...
#include <instrument_spec_assigns.h>
Public Member Functions | |
instrument_spec_assignst (const irep_idt &_function_id, const goto_functionst &_functions, symbol_tablet &_st, message_handlert &_message_handler) | |
Class constructor. | |
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. | |
void | track_stack_allocated (const symbol_exprt &symbol_expr, goto_programt &dest) |
Track a stack-allocated object and generate snaphsot instructions in dest. | |
bool | stack_allocated_is_tracked (const symbol_exprt &symbol_expr) const |
Returns true if the expression is tracked. | |
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. | |
void | track_heap_allocated (const exprt &expr, goto_programt &dest) |
Track a whole heap-alloc object and generate snaphsot instructions in dest. | |
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. | |
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. | |
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. | |
Protected Types | |
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 > |
Protected Member Functions | |
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. | |
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. | |
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. | |
void | create_snapshot (const car_exprt &car, goto_programt &dest) const |
Returns snapshot instructions for a car_exprt. | |
exprt | target_validity_expr (const car_exprt &car, bool allow_null_target) const |
Returns the target validity expression for a car_exprt. | |
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 . | |
exprt | inclusion_check_single (const car_exprt &lhs, const car_exprt &candidate_car) const |
Returns inclusion check expression for a single candidate location. | |
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. | |
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. | |
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. | |
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. | |
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. | |
Protected Attributes | |
const irep_idt & | function_id |
Name of the instrumented function. | |
const goto_functionst & | functions |
Other functions of the model. | |
symbol_tablet & | st |
Program symbol table. | |
const namespacet | ns |
Program namespace. | |
messaget | log |
Logger. | |
cond_target_exprt_to_car_mapt | from_spec_assigns |
Map to from conditional target expressions of assigns clauses to corresponding conditional address ranges. | |
symbol_exprt_to_car_mapt | from_stack_alloc |
Map to from DECL symbols to corresponding conditional address ranges. | |
exprt_to_car_mapt | from_heap_alloc |
Map to from malloc'd symbols to corresponding conditional address ranges. | |
A class that generates instrumentation for assigns clause checking.
The track_*
methods add targets to the sets of tracked targets and append instructions to the given destination program.
The check_inclusion_*
methods generate assertions checking for inclusion of a designated target in one of the tracked targets, and append instructions to the given destination.
Definition at line 142 of file instrument_spec_assigns.h.
|
protected |
Definition at line 315 of file instrument_spec_assigns.h.
|
protected |
Definition at line 333 of file instrument_spec_assigns.h.
|
protected |
Definition at line 325 of file instrument_spec_assigns.h.
|
inline |
Class constructor.
_function_id | name of the instrumented function |
_functions | other functions of the model |
_st | symbol table of the goto_model |
_message_handler | used to output warning/error messages |
Definition at line 151 of file instrument_spec_assigns.h.
void instrument_spec_assignst::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.
lhs | the assignment lhs or argument to havoc/havoc_object |
cfg_info_opt | allows target set pruning if available |
dest | destination program to append instructions to |
cfg_info_opt::target()
must point to the instruction containing the lhs in question. Definition at line 81 of file instrument_spec_assigns.cpp.
void instrument_spec_assignst::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.
expr | the argument to the free operator |
cfg_info_opt | allows target set pruning if available |
dest | destination program to append instructions to |
cfg_info_opt::target()
must point to the instruction containing the lhs in question. Definition at line 121 of file instrument_spec_assigns.cpp.
|
protected |
Creates a conditional address range expression from a cleaned-up condition and target expression.
Definition at line 189 of file instrument_spec_assigns.cpp.
|
protected |
Definition at line 472 of file instrument_spec_assigns.cpp.
|
protected |
Definition at line 432 of file instrument_spec_assigns.cpp.
|
protected |
Definition at line 453 of file instrument_spec_assigns.cpp.
|
protected |
Creates a fresh symbolt with given suffix, scoped to function_id.
Definition at line 180 of file instrument_spec_assigns.cpp.
|
protected |
Returns snapshot instructions for a car_exprt.
Definition at line 241 of file instrument_spec_assigns.cpp.
|
protected |
Returns an inclusion check assertion of lhs over all tracked cars.
lhs | the lhs expression to check for inclusion |
allow_null_lhs | if true, allow the lhs to be NULL |
include_stack_allocated | if true, include stack allocated targets in the inclusion check. |
cfg_info_opt | allows target set pruning if available |
dest | destination program to append instructions to |
cfg_info_opt
must point to the lhs
in question. Definition at line 323 of file instrument_spec_assigns.cpp.
|
protected |
Returns an inclusion check expression of lhs over all tracked cars.
lhs | the lhs expression to check for inclusion |
allow_null_lhs | if true, allow the lhs to be NULL |
include_stack_allocated | if true, include stack allocated targets in the inclusion check. |
cfg_info_opt | allows target set pruning if available |
cfg_info_opt
must point to the lhs
in question. Definition at line 381 of file instrument_spec_assigns.cpp.
|
protected |
Returns inclusion check expression for a single candidate location.
Definition at line 362 of file instrument_spec_assigns.cpp.
|
protected |
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.
Definition at line 489 of file instrument_spec_assigns.cpp.
|
protected |
Generates instructions to invalidate all targets aliased with a car that was passed to free
, assuming the inclusion check passes, ie.
that the freed_car is fully included in one of the tracked targets.
Definition at line 506 of file instrument_spec_assigns.cpp.
void instrument_spec_assignst::invalidate_stack_allocated | ( | const symbol_exprt & | symbol_expr, |
goto_programt & | dest | ||
) |
Generate instructions to invalidate a stack-allocated object that goes DEAD in dest.
Definition at line 55 of file instrument_spec_assigns.cpp.
bool instrument_spec_assignst::stack_allocated_is_tracked | ( | const symbol_exprt & | symbol_expr | ) | const |
Returns true if the expression is tracked.
Definition at line 49 of file instrument_spec_assigns.cpp.
|
protected |
Generates the target validity assertion for the given car
and adds it to dest
.
The assertion checks that if the car's condition holds then the target is r_ok
(or NULL
if allow_null_targets
is true).
Definition at line 292 of file instrument_spec_assigns.cpp.
|
protected |
Returns the target validity expression for a car_exprt.
Definition at line 273 of file instrument_spec_assigns.cpp.
void instrument_spec_assignst::track_heap_allocated | ( | const exprt & | expr, |
goto_programt & | dest | ||
) |
Track a whole heap-alloc object and generate snaphsot instructions in dest.
Definition at line 74 of file instrument_spec_assigns.cpp.
|
protected |
Track and generate snaphsot instructions and target validity checking assertions for a conditional target group from an assigns clause.
Definition at line 166 of file instrument_spec_assigns.cpp.
void instrument_spec_assignst::track_spec_target | ( | const exprt & | expr, |
goto_programt & | dest | ||
) |
Track an assigns clause target and generate snaphsot instructions and well-definedness assertions in dest.
Definition at line 32 of file instrument_spec_assigns.cpp.
|
protected |
Track and generate snaphsot instructions and target validity checking assertions for a conditional target group from an assigns clause.
Definition at line 142 of file instrument_spec_assigns.cpp.
void instrument_spec_assignst::track_stack_allocated | ( | const symbol_exprt & | symbol_expr, |
goto_programt & | dest | ||
) |
Track a stack-allocated object and generate snaphsot instructions in dest.
Definition at line 42 of file instrument_spec_assigns.cpp.
void instrument_spec_assignst::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.
dest | a snaphot program for the identified static locals. |
Definition at line 92 of file instrument_spec_assigns.cpp.
|
protected |
Map to from malloc'd symbols to corresponding conditional address ranges.
Definition at line 337 of file instrument_spec_assigns.h.
|
protected |
Map to from conditional target expressions of assigns clauses to corresponding conditional address ranges.
Definition at line 320 of file instrument_spec_assigns.h.
|
protected |
Map to from DECL symbols to corresponding conditional address ranges.
Definition at line 329 of file instrument_spec_assigns.h.
|
protected |
Name of the instrumented function.
Definition at line 221 of file instrument_spec_assigns.h.
|
protected |
Other functions of the model.
Definition at line 224 of file instrument_spec_assigns.h.
|
protected |
Logger.
Definition at line 233 of file instrument_spec_assigns.h.
|
protected |
Program namespace.
Definition at line 230 of file instrument_spec_assigns.h.
|
protected |
Program symbol table.
Definition at line 227 of file instrument_spec_assigns.h.