CBMC
|
A class that generates instrumentation for assigns clause checking. More...
#include <instrument_spec_assigns.h>
Classes | |
class | location_intervalt |
Represents an interval of source locations covered by the static local variable search. More... | |
Public Member Functions | |
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... | |
Protected Types | |
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 | |
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 | |
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... | |
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 186 of file instrument_spec_assigns.h.
|
protected |
List of malloc'd conditional address ranges.
Definition at line 619 of file instrument_spec_assigns.h.
|
protected |
Definition at line 597 of file instrument_spec_assigns.h.
|
protected |
Map type from function identifiers to covered locations.
Definition at line 405 of file instrument_spec_assigns.h.
|
protected |
Definition at line 615 of file instrument_spec_assigns.h.
|
protected |
Definition at line 406 of file instrument_spec_assigns.h.
|
protected |
Definition at line 607 of file instrument_spec_assigns.h.
|
inline |
Class constructor.
_function_id | name of the instrumented function |
_functions | other functions of the model |
_cfg_info | control flow graph info about the function |
_st | symbol table of the goto_model |
_message_handler | used to output warning/error messages |
Definition at line 196 of file instrument_spec_assigns.h.
void instrument_spec_assignst::check_inclusion_assignment | ( | const exprt & | lhs, |
goto_programt & | dest | ||
) | const |
Generates inclusion check instructions for an assignment, havoc or havoc_object instruction.
lhs | the assignment lhs or argument to havoc/havoc_object |
dest | destination program to append instructions to |
Definition at line 148 of file instrument_spec_assigns.cpp.
void instrument_spec_assignst::check_inclusion_heap_allocated_and_invalidate_aliases | ( | const exprt & | expr, |
goto_programt & | dest | ||
) |
Generates inclusion check instructions for an argument passed to free.
expr | the argument to the free operator |
dest | destination program to append instructions to |
Definition at line 313 of file instrument_spec_assigns.cpp.
|
protected |
Collects static symbols from the symbol table that have a source location included in one of the covered_locations
and writes them into dest.
Definition at line 293 of file instrument_spec_assigns.cpp.
|
protected |
Creates a conditional address range expression from a cleaned-up condition and target expression.
Definition at line 476 of file instrument_spec_assigns.cpp.
|
protected |
Definition at line 877 of file instrument_spec_assigns.cpp.
|
protected |
Definition at line 833 of file instrument_spec_assigns.cpp.
|
protected |
Definition at line 856 of file instrument_spec_assigns.cpp.
|
protected |
Definition at line 885 of file instrument_spec_assigns.cpp.
|
protected |
Returns snapshot instructions for a car_exprt.
Definition at line 618 of file instrument_spec_assigns.cpp.
|
inline |
Inserts the detected static local symbols into a target container.
C | The type of the target container |
inserter | An insert_iterator on the target container |
Definition at line 462 of file instrument_spec_assigns.h.
|
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. |
dest | destination program to append instructions to |
Definition at line 700 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. |
Definition at line 761 of file instrument_spec_assigns.cpp.
|
protected |
Returns inclusion check expression for a single candidate location.
Definition at line 742 of file instrument_spec_assigns.cpp.
|
protected |
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.
Definition at line 1030 of file instrument_spec_assigns.cpp.
|
protected |
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.
Definition at line 1041 of file instrument_spec_assigns.cpp.
void instrument_spec_assignst::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.
If pred
is not provided, then all instructions are instrumented. If pred
is provided, then only the instructions that satisfy pred are instrumented.
body | goto program containing the instructions |
instruction_it | target to the first instruction of the sequence |
instruction_end | target to the last instruction of the sequence |
pred | a predicate on targets to check if they should be instrumented |
Definition at line 332 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 905 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 922 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 115 of file instrument_spec_assigns.cpp.
|
protected |
Returns true iff an ASSIGN lhs := rhs
instruction must be instrumented.
Definition at line 934 of file instrument_spec_assigns.cpp.
|
protected |
Returns true iff a DEAD x
must be processed to update the write set.
Returns true iff a DEAD x
must be processed to upate the local write set.
The conditions are the same than for tracking a DECL x
instruction.
Definition at line 1024 of file instrument_spec_assigns.cpp.
|
protected |
Returns true iff a DECL x
must be explicitly added to the write set.
Returns true iff a DECL x
must be explicitly tracked in the write set.
Definition at line 1002 of file instrument_spec_assigns.cpp.
|
protected |
Returns true iff a function-local symbol must be tracked.
Track the symbol is not a local or is a dirty local.
A local is called 'dirty' if its address gets taken at some point in the program.
Assuming the goto program is obtained from a structured C program that passed C compiler checks, non-dirty locals can only be assigned to directly by name, cannot escape their lexical scope, and are always safe to assign. Hence, we only track dirty locals in the write set.
Definition at line 995 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 109 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 669 of file instrument_spec_assigns.cpp.
|
protected |
Returns the target validity expression for a car_exprt.
Definition at line 650 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 134 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 443 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 92 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 416 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 102 of file instrument_spec_assigns.cpp.
void instrument_spec_assignst::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.
dest | a snaphot program for the identified static locals. |
Definition at line 165 of file instrument_spec_assigns.cpp.
void instrument_spec_assignst::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.
it | start instruction (inclusive) |
end | end instruction (exclusive) |
dest | a snaphot program for the identified static locals. |
Definition at line 193 of file instrument_spec_assigns.cpp.
|
protected |
Traverses the given list of instructions, updating the given coverage map, recursing into function calls only once.
When the traversal terminates, the map will contain one entry per visited function, with the associated range of locations covered by the traversal. Function names and line numbers are collected from source locations attached to the instructions.
Definition at line 212 of file instrument_spec_assigns.cpp.
|
protected |
CFG information for simplification.
Definition at line 480 of file instrument_spec_assigns.h.
|
protected |
Definition at line 620 of file instrument_spec_assigns.h.
|
protected |
Map from conditional target expressions of assigns clauses to corresponding conditional address ranges.
Definition at line 602 of file instrument_spec_assigns.h.
|
protected |
Map from DECL symbols to corresponding conditional address ranges.
Definition at line 611 of file instrument_spec_assigns.h.
|
protected |
Map to from detected or propagated static local symbols to corresponding conditional address ranges.
Definition at line 626 of file instrument_spec_assigns.h.
|
protected |
Name of the instrumented function.
Definition at line 474 of file instrument_spec_assigns.h.
|
protected |
Other functions of the model.
Definition at line 477 of file instrument_spec_assigns.h.
|
protected |
Logger.
Definition at line 489 of file instrument_spec_assigns.h.
|
protected |
Language mode.
Definition at line 492 of file instrument_spec_assigns.h.
|
protected |
Program namespace.
Definition at line 486 of file instrument_spec_assigns.h.
|
protected |
Program symbol table.
Definition at line 483 of file instrument_spec_assigns.h.