CBMC
instrument_spec_assignst Class Reference

A class that generates instrumentation for assigns clause checking. More...

#include <instrument_spec_assigns.h>

+ Inheritance diagram for instrument_spec_assignst:
+ Collaboration diagram for instrument_spec_assignst:

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_intervaltcovered_locationst
 Map type from function identifiers to covered locations. More...
 
typedef std::unordered_set< symbol_exprt, irep_hashpropagated_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_exprtcreate_car_from_spec_assigns (const exprt &condition, const exprt &target)
 
const car_exprtcreate_car_from_stack_alloc (const symbol_exprt &target)
 
const car_exprtcreate_car_from_heap_alloc (const exprt &target)
 
const car_exprtcreate_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_idtfunction_id
 Name of the instrumented function. More...
 
const goto_functionstfunctions
 Other functions of the model. More...
 
cfg_infotcfg_info
 CFG information for simplification. More...
 
symbol_table_basetst
 Program symbol table. More...
 
const namespacet ns
 Program namespace. More...
 
messaget log
 Logger. More...
 
const irep_idtmode
 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...
 

Detailed Description

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.

Member Typedef Documentation

◆ car_expr_listt

List of malloc'd conditional address ranges.

Definition at line 619 of file instrument_spec_assigns.h.

◆ cond_target_exprt_to_car_mapt

Definition at line 597 of file instrument_spec_assigns.h.

◆ covered_locationst

Map type from function identifiers to covered locations.

Definition at line 405 of file instrument_spec_assigns.h.

◆ exprt_to_car_mapt

using instrument_spec_assignst::exprt_to_car_mapt = std::unordered_map<const exprt, const car_exprt, irep_hash>
protected

Definition at line 615 of file instrument_spec_assigns.h.

◆ propagated_static_localst

Definition at line 406 of file instrument_spec_assigns.h.

◆ symbol_exprt_to_car_mapt

using instrument_spec_assignst::symbol_exprt_to_car_mapt = std::unordered_map<const symbol_exprt, const car_exprt, irep_hash>
protected

Definition at line 607 of file instrument_spec_assigns.h.

Constructor & Destructor Documentation

◆ instrument_spec_assignst()

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 
)
inline

Class constructor.

Parameters
_function_idname of the instrumented function
_functionsother functions of the model
_cfg_infocontrol flow graph info about the function
_stsymbol table of the goto_model
_message_handlerused to output warning/error messages

Definition at line 196 of file instrument_spec_assigns.h.

Member Function Documentation

◆ check_inclusion_assignment()

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.

Parameters
lhsthe assignment lhs or argument to havoc/havoc_object
destdestination program to append instructions to

Definition at line 148 of file instrument_spec_assigns.cpp.

◆ check_inclusion_heap_allocated_and_invalidate_aliases()

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.

Parameters
exprthe argument to the free operator
destdestination program to append instructions to

Definition at line 313 of file instrument_spec_assigns.cpp.

◆ collect_static_symbols()

void instrument_spec_assignst::collect_static_symbols ( covered_locationst covered_locations,
std::unordered_set< symbol_exprt, irep_hash > &  dest 
)
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.

◆ create_car_expr()

car_exprt instrument_spec_assignst::create_car_expr ( const exprt condition,
const exprt target 
) const
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.

◆ create_car_from_heap_alloc()

const car_exprt & instrument_spec_assignst::create_car_from_heap_alloc ( const exprt target)
protected

Definition at line 877 of file instrument_spec_assigns.cpp.

◆ create_car_from_spec_assigns()

const car_exprt & instrument_spec_assignst::create_car_from_spec_assigns ( const exprt condition,
const exprt target 
)
protected

Definition at line 833 of file instrument_spec_assigns.cpp.

◆ create_car_from_stack_alloc()

const car_exprt & instrument_spec_assignst::create_car_from_stack_alloc ( const symbol_exprt target)
protected

Definition at line 856 of file instrument_spec_assigns.cpp.

◆ create_car_from_static_local()

const car_exprt & instrument_spec_assignst::create_car_from_static_local ( const symbol_exprt target)
protected

Definition at line 885 of file instrument_spec_assigns.cpp.

◆ create_snapshot()

void instrument_spec_assignst::create_snapshot ( const car_exprt car,
goto_programt dest 
) const
protected

Returns snapshot instructions for a car_exprt.

Definition at line 618 of file instrument_spec_assigns.cpp.

◆ get_static_locals()

template<typename C >
void instrument_spec_assignst::get_static_locals ( std::insert_iterator< C >  inserter) const
inline

Inserts the detected static local symbols into a target container.

Template Parameters
CThe type of the target container
Parameters
inserterAn insert_iterator on the target container

Definition at line 462 of file instrument_spec_assigns.h.

◆ inclusion_check_assertion()

void instrument_spec_assignst::inclusion_check_assertion ( const car_exprt lhs,
bool  allow_null_lhs,
bool  include_stack_allocated,
goto_programt dest 
) const
protected

Returns an inclusion check assertion of lhs over all tracked cars.

Parameters
lhsthe lhs expression to check for inclusion
allow_null_lhsif true, allow the lhs to be NULL
include_stack_allocatedif true, include stack allocated targets in the inclusion check.
destdestination program to append instructions to

Definition at line 700 of file instrument_spec_assigns.cpp.

◆ inclusion_check_full()

exprt instrument_spec_assignst::inclusion_check_full ( const car_exprt lhs,
bool  allow_null_lhs,
bool  include_stack_allocated 
) const
protected

Returns an inclusion check expression of lhs over all tracked cars.

Parameters
lhsthe lhs expression to check for inclusion
allow_null_lhsif true, allow the lhs to be NULL
include_stack_allocatedif true, include stack allocated targets in the inclusion check.

Definition at line 761 of file instrument_spec_assigns.cpp.

◆ inclusion_check_single()

exprt instrument_spec_assignst::inclusion_check_single ( const car_exprt lhs,
const car_exprt candidate_car 
) const
protected

Returns inclusion check expression for a single candidate location.

Definition at line 742 of file instrument_spec_assigns.cpp.

◆ instrument_assign_statement()

void instrument_spec_assignst::instrument_assign_statement ( goto_programt::targett instruction_it,
goto_programt body 
) const
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.

◆ instrument_call_statement()

void instrument_spec_assignst::instrument_call_statement ( goto_programt::targett instruction_it,
goto_programt body 
)
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.

◆ instrument_instructions()

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.

Parameters
bodygoto program containing the instructions
instruction_ittarget to the first instruction of the sequence
instruction_endtarget to the last instruction of the sequence
preda predicate on targets to check if they should be instrumented

Definition at line 332 of file instrument_spec_assigns.cpp.

◆ invalidate_car()

void instrument_spec_assignst::invalidate_car ( const car_exprt tracked_car,
const car_exprt freed_car,
goto_programt result 
) const
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.

◆ invalidate_heap_and_spec_aliases()

void instrument_spec_assignst::invalidate_heap_and_spec_aliases ( const car_exprt freed_car,
goto_programt dest 
) const
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.

◆ invalidate_stack_allocated()

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.

◆ must_check_assign()

bool instrument_spec_assignst::must_check_assign ( const goto_programt::const_targett target)
protected

Returns true iff an ASSIGN lhs := rhs instruction must be instrumented.

Definition at line 934 of file instrument_spec_assigns.cpp.

◆ must_track_dead()

bool instrument_spec_assignst::must_track_dead ( const goto_programt::const_targett target) const
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.

See also
must_track_decl_or_dead.

The conditions are the same than for tracking a DECL x instruction.

Definition at line 1024 of file instrument_spec_assigns.cpp.

◆ must_track_decl()

bool instrument_spec_assignst::must_track_decl ( const goto_programt::const_targett target) const
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.

See also
must_track_decl_or_dead.

Definition at line 1002 of file instrument_spec_assigns.cpp.

◆ must_track_decl_or_dead()

bool instrument_spec_assignst::must_track_decl_or_dead ( const irep_idt ident) const
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.

◆ stack_allocated_is_tracked()

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.

◆ target_validity_assertion()

void instrument_spec_assignst::target_validity_assertion ( const car_exprt car,
bool  allow_null_target,
goto_programt dest 
) const
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.

◆ target_validity_expr()

exprt instrument_spec_assignst::target_validity_expr ( const car_exprt car,
bool  allow_null_target 
) const
protected

Returns the target validity expression for a car_exprt.

Definition at line 650 of file instrument_spec_assigns.cpp.

◆ track_heap_allocated()

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.

◆ track_plain_spec_target()

void instrument_spec_assignst::track_plain_spec_target ( const exprt expr,
goto_programt dest 
)
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.

◆ track_spec_target()

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.

◆ track_spec_target_group()

void instrument_spec_assignst::track_spec_target_group ( const conditional_target_group_exprt group,
goto_programt dest 
)
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.

◆ track_stack_allocated()

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.

◆ track_static_locals()

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.

Parameters
desta snaphot program for the identified static locals.

Definition at line 165 of file instrument_spec_assigns.cpp.

◆ track_static_locals_between()

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.

Parameters
itstart instruction (inclusive)
endend instruction (exclusive)
desta snaphot program for the identified static locals.

Definition at line 193 of file instrument_spec_assigns.cpp.

◆ traverse_instructions()

void instrument_spec_assignst::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
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.

Member Data Documentation

◆ cfg_info

cfg_infot& instrument_spec_assignst::cfg_info
protected

CFG information for simplification.

Definition at line 480 of file instrument_spec_assigns.h.

◆ from_heap_alloc

car_expr_listt instrument_spec_assignst::from_heap_alloc
protected

Definition at line 620 of file instrument_spec_assigns.h.

◆ from_spec_assigns

cond_target_exprt_to_car_mapt instrument_spec_assignst::from_spec_assigns
protected

Map from conditional target expressions of assigns clauses to corresponding conditional address ranges.

Definition at line 602 of file instrument_spec_assigns.h.

◆ from_stack_alloc

symbol_exprt_to_car_mapt instrument_spec_assignst::from_stack_alloc
protected

Map from DECL symbols to corresponding conditional address ranges.

Definition at line 611 of file instrument_spec_assigns.h.

◆ from_static_local

symbol_exprt_to_car_mapt instrument_spec_assignst::from_static_local
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.

◆ function_id

const irep_idt& instrument_spec_assignst::function_id
protected

Name of the instrumented function.

Definition at line 474 of file instrument_spec_assigns.h.

◆ functions

const goto_functionst& instrument_spec_assignst::functions
protected

Other functions of the model.

Definition at line 477 of file instrument_spec_assigns.h.

◆ log

messaget instrument_spec_assignst::log
protected

Logger.

Definition at line 489 of file instrument_spec_assigns.h.

◆ mode

const irep_idt& instrument_spec_assignst::mode
protected

Language mode.

Definition at line 492 of file instrument_spec_assigns.h.

◆ ns

const namespacet instrument_spec_assignst::ns
protected

Program namespace.

Definition at line 486 of file instrument_spec_assigns.h.

◆ st

symbol_table_baset& instrument_spec_assignst::st
protected

Program symbol table.

Definition at line 483 of file instrument_spec_assigns.h.


The documentation for this class was generated from the following files: