cprover
Loading...
Searching...
No Matches
stack_depth.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Stack depth checks
4
5Author: Daniel Kroening, Michael Tautschnig
6
7Date: November 2011
8
9\*******************************************************************/
10
13
14#include "stack_depth.h"
15
16#include <util/arith_tools.h>
18
21
23
25 goto_modelt &goto_model,
26 message_handlert &message_handler)
27{
28 const irep_idt identifier="$stack_depth";
29 unsignedbv_typet type(sizeof(std::size_t)*8);
30
31 symbolt new_symbol;
32 new_symbol.name=identifier;
33 new_symbol.base_name=identifier;
34 new_symbol.pretty_name=identifier;
35 new_symbol.type=type;
36 new_symbol.is_static_lifetime=true;
37 new_symbol.value=from_integer(0, type);
38 new_symbol.mode=ID_C;
39 new_symbol.is_thread_local=true;
40 new_symbol.is_lvalue=true;
41
42 bool failed = goto_model.symbol_table.add(new_symbol);
44
45 if(goto_model.goto_functions.function_map.erase(INITIALIZE_FUNCTION) != 0)
46 {
48 goto_model.symbol_table,
52 goto_model.symbol_table,
53 goto_model.goto_functions,
54 message_handler);
55 goto_model.goto_functions.update();
56 }
57
58 return new_symbol.symbol_expr();
59}
60
61static void stack_depth(
62 goto_programt &goto_program,
63 const symbol_exprt &symbol,
64 const std::size_t i_depth,
65 const exprt &max_depth)
66{
67 assert(!goto_program.instructions.empty());
68
69 goto_programt::targett first=goto_program.instructions.begin();
70
71 binary_relation_exprt guard(symbol, ID_le, max_depth);
73 first, goto_programt::make_assertion(guard, first->source_location()));
74
75 assert_ins->source_location_nonconst().set_comment(
76 "Stack depth exceeds " + std::to_string(i_depth));
77 assert_ins->source_location_nonconst().set_property_class("stack-depth");
78
79 goto_program.insert_before(
80 first,
82 code_assignt(symbol, plus_exprt(symbol, from_integer(1, symbol.type()))),
83 first->source_location()));
84
85 goto_programt::targett last=--goto_program.instructions.end();
86 assert(last->is_end_function());
87
89 code_assignt(symbol, minus_exprt(symbol, from_integer(1, symbol.type()))),
90 last->source_location());
91
92 goto_program.insert_before_swap(last, minus_ins);
93}
94
96 goto_modelt &goto_model,
97 const std::size_t depth,
98 message_handlert &message_handler)
99{
100 const symbol_exprt sym = add_stack_depth_symbol(goto_model, message_handler);
101
102 const exprt depth_expr(from_integer(depth, sym.type()));
103
104 for(auto &gf_entry : goto_model.goto_functions.function_map)
105 {
106 if(
107 gf_entry.second.body_available() &&
108 gf_entry.first != INITIALIZE_FUNCTION &&
110 {
111 stack_depth(gf_entry.second.body, sym, depth, depth_expr);
112 }
113 }
114
115 // update counters etc.
116 goto_model.goto_functions.update();
117}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Pre-defined bitvector types.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:674
A codet representing an assignment in the program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
typet & type()
Return the type of the expression.
Definition expr.h:82
const source_locationt & source_location() const
Definition expr.h:230
function_mapt function_map
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:33
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
instructionst::iterator targett
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Binary minus.
Definition std_expr.h:973
The plus expression Associativity is not specified.
Definition std_expr.h:914
Expression to hold a symbol (variable)
Definition std_expr.h:80
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Symbol table entry.
Definition symbol.h:28
bool is_static_lifetime
Definition symbol.h:65
bool is_thread_local
Definition symbol.h:65
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
irep_idt pretty_name
Language-specific display name.
Definition symbol.h:52
irep_idt irep_idt base_name
Name of module the symbol belongs to.
Definition symbol.h:46
bool is_lvalue
Definition symbol.h:66
exprt value
Initial value of symbol.
Definition symbol.h:34
irep_idt mode
Language mode.
Definition symbol.h:49
Fixed-width bit-vector with unsigned binary interpretation.
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Goto Programs with Functions.
Symbol Table + CFG.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
static void stack_depth(goto_programt &goto_program, const symbol_exprt &symbol, const std::size_t i_depth, const exprt &max_depth)
static symbol_exprt add_stack_depth_symbol(goto_modelt &goto_model, message_handlert &message_handler)
Stack depth checks.
static optionalt< codet > static_lifetime_init(const irep_idt &identifier, symbol_tablet &symbol_table)
#define INITIALIZE_FUNCTION
static bool failed(bool error_indicator)