cprover
Loading...
Searching...
No Matches
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:

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_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)
 
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_idtfunction_id
 Name of the instrumented function.
 
const goto_functionstfunctions
 Other functions of the model.
 
symbol_tabletst
 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.
 

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 142 of file instrument_spec_assigns.h.

Member Typedef Documentation

◆ cond_target_exprt_to_car_mapt

◆ 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 333 of file instrument_spec_assigns.h.

◆ symbol_exprt_to_car_mapt

Definition at line 325 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,
symbol_tablet _st,
message_handlert _message_handler 
)
inline

Class constructor.

Parameters
_function_idname of the instrumented function
_functionsother functions of the model
_stsymbol table of the goto_model
_message_handlerused to output warning/error messages

Definition at line 151 of file instrument_spec_assigns.h.

Member Function Documentation

◆ check_inclusion_assignment()

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.

Parameters
lhsthe assignment lhs or argument to havoc/havoc_object
cfg_info_optallows target set pruning if available
destdestination program to append instructions to
Remarks
if provided, the internal instruction pointer of cfg_info_opt::target() must point to the instruction containing the lhs in question.

Definition at line 81 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,
optionalt< cfg_infot > &  cfg_info_opt,
goto_programt dest 
)

Generates inclusion check instructions for an argument passed to free.

Parameters
exprthe argument to the free operator
cfg_info_optallows target set pruning if available
destdestination program to append instructions to
Remarks
If provided, the internal instruction pointer of cfg_info_opt::target() must point to the instruction containing the lhs in question.

Definition at line 121 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 189 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 472 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 432 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 453 of file instrument_spec_assigns.cpp.

◆ create_fresh_symbol()

const symbolt instrument_spec_assignst::create_fresh_symbol ( const std::string &  suffix,
const typet type,
const source_locationt location 
) const
protected

Creates a fresh symbolt with given suffix, scoped to function_id.

Definition at line 180 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 241 of file instrument_spec_assigns.cpp.

◆ inclusion_check_assertion()

void instrument_spec_assignst::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
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.
cfg_info_optallows target set pruning if available
destdestination program to append instructions to
Remarks
If available, cfg_info_opt must point to the lhs in question.

Definition at line 323 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,
optionalt< cfg_infot > &  cfg_info_opt 
) 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.
cfg_info_optallows target set pruning if available
Remarks
If available, cfg_info_opt must point to the lhs in question.

Definition at line 381 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 362 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 489 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 506 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 55 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 49 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 292 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 273 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 74 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 166 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 32 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 142 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 42 of file instrument_spec_assigns.cpp.

◆ track_static_locals()

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.

Parameters
desta snaphot program for the identified static locals.

Definition at line 92 of file instrument_spec_assigns.cpp.

Member Data Documentation

◆ from_heap_alloc

exprt_to_car_mapt instrument_spec_assignst::from_heap_alloc
protected

Map to from malloc'd symbols to corresponding conditional address ranges.

Definition at line 337 of file instrument_spec_assigns.h.

◆ from_spec_assigns

cond_target_exprt_to_car_mapt instrument_spec_assignst::from_spec_assigns
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.

◆ from_stack_alloc

symbol_exprt_to_car_mapt instrument_spec_assignst::from_stack_alloc
protected

Map to from DECL symbols to corresponding conditional address ranges.

Definition at line 329 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 221 of file instrument_spec_assigns.h.

◆ functions

const goto_functionst& instrument_spec_assignst::functions
protected

Other functions of the model.

Definition at line 224 of file instrument_spec_assigns.h.

◆ log

messaget instrument_spec_assignst::log
protected

Logger.

Definition at line 233 of file instrument_spec_assigns.h.

◆ ns

const namespacet instrument_spec_assignst::ns
protected

Program namespace.

Definition at line 230 of file instrument_spec_assigns.h.

◆ st

symbol_tablet& instrument_spec_assignst::st
protected

Program symbol table.

Definition at line 227 of file instrument_spec_assigns.h.


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