cprover
stack_depth.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Stack depth checks
4 
5 Author: Daniel Kroening, Michael Tautschnig
6 
7 Date: November 2011
8 
9 \*******************************************************************/
10 
13 
14 #include "stack_depth.h"
15 
16 #include <util/arith_tools.h>
17 #include <util/bitvector_types.h>
18 
20 
22 
24 {
25  const irep_idt identifier="$stack_depth";
26  unsignedbv_typet type(sizeof(std::size_t)*8);
27 
28  symbolt new_symbol;
29  new_symbol.name=identifier;
30  new_symbol.base_name=identifier;
31  new_symbol.pretty_name=identifier;
32  new_symbol.type=type;
33  new_symbol.is_static_lifetime=true;
34  new_symbol.value=from_integer(0, type);
35  new_symbol.mode=ID_C;
36  new_symbol.is_thread_local=true;
37  new_symbol.is_lvalue=true;
38 
39  symbol_table.insert(std::move(new_symbol));
40 
41  return symbol_exprt(identifier, type);
42 }
43 
45  goto_programt &goto_program,
46  const symbol_exprt &symbol,
47  const std::size_t i_depth,
48  const exprt &max_depth)
49 {
50  assert(!goto_program.instructions.empty());
51 
52  goto_programt::targett first=goto_program.instructions.begin();
53 
54  binary_relation_exprt guard(symbol, ID_le, max_depth);
55  goto_programt::targett assert_ins = goto_program.insert_before(
56  first, goto_programt::make_assertion(guard, first->source_location));
57 
58  assert_ins->source_location.set_comment(
59  "Stack depth exceeds "+std::to_string(i_depth));
60  assert_ins->source_location.set_property_class("stack-depth");
61 
62  goto_program.insert_before(
63  first,
65  code_assignt(symbol, plus_exprt(symbol, from_integer(1, symbol.type()))),
66  first->source_location));
67 
68  goto_programt::targett last=--goto_program.instructions.end();
69  assert(last->is_end_function());
70 
72  code_assignt(symbol, minus_exprt(symbol, from_integer(1, symbol.type()))),
73  last->source_location);
74 
75  goto_program.insert_before_swap(last, minus_ins);
76 }
77 
79  goto_modelt &goto_model,
80  const std::size_t depth)
81 {
82  const symbol_exprt sym=
84 
85  const exprt depth_expr(from_integer(depth, sym.type()));
86 
87  for(auto &gf_entry : goto_model.goto_functions.function_map)
88  {
89  if(
90  gf_entry.second.body_available() &&
91  gf_entry.first != INITIALIZE_FUNCTION &&
92  gf_entry.first != goto_functionst::entry_point())
93  {
94  stack_depth(gf_entry.second.body, sym, depth, depth_expr);
95  }
96  }
97 
98  // initialize depth to 0
99  goto_functionst::function_mapt::iterator i_it =
102  i_it!=goto_model.goto_functions.function_map.end(),
103  INITIALIZE_FUNCTION " must exist");
104 
105  goto_programt &init=i_it->second.body;
106  goto_programt::targett first=init.instructions.begin();
107  init.insert_before(
108  first,
110  code_assignt(sym, from_integer(0, sym.type()))));
111  // no suitable value for source location -- omitted
112 
113  // update counters etc.
114  goto_model.goto_functions.update();
115 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
arith_tools.h
stack_depth
void stack_depth(goto_programt &goto_program, const symbol_exprt &symbol, const std::size_t i_depth, const exprt &max_depth)
Definition: stack_depth.cpp:44
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
goto_model.h
Symbol Table + CFG.
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:830
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:26
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:1008
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: bitvector_types.h:159
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
symbolt::is_thread_local
bool is_thread_local
Definition: symbol.h:65
goto_programt::insert_before
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:623
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:877
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
bitvector_types.h
Pre-defined bitvector types.
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:23
symbol_tablet::insert
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Definition: symbol_table.cpp:19
minus_exprt
Binary minus.
Definition: std_expr.h:889
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:569
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
stack_depth.h
Stack depth checks.
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
symbolt
Symbol table entry.
Definition: symbol.h:28
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:100
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
goto_functionst::update
void update()
Definition: goto_functions.h:81
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:90
static_lifetime_init.h
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:590
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
add_stack_depth_symbol
symbol_exprt add_stack_depth_symbol(symbol_tablet &symbol_table)
Definition: stack_depth.cpp:23
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:238
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:563