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/symbol_table.h>
17 #include <util/std_expr.h>
18 #include <util/std_types.h>
19 #include <util/arith_tools.h>
20 #include <util/cprover_prefix.h>
21 
23 
25 {
26  const irep_idt identifier="$stack_depth";
27  signedbv_typet type(sizeof(int)*8);
28 
29  symbolt new_symbol;
30  new_symbol.name=identifier;
31  new_symbol.base_name=identifier;
32  new_symbol.pretty_name=identifier;
33  new_symbol.type=type;
34  new_symbol.is_static_lifetime=true;
35  new_symbol.value=from_integer(0, type);
36  new_symbol.mode=ID_C;
37  new_symbol.is_thread_local=true;
38  new_symbol.is_lvalue=true;
39 
40  symbol_table.move(new_symbol);
41 
42  return symbol_exprt(identifier, type);
43 }
44 
46  goto_programt &goto_program,
47  const symbol_exprt &symbol,
48  const int i_depth,
49  const exprt &max_depth)
50 {
51  assert(!goto_program.instructions.empty());
52 
53  goto_programt::targett first=goto_program.instructions.begin();
54 
55  binary_relation_exprt guard(symbol, ID_le, max_depth);
56  goto_programt::targett assert_ins=goto_program.insert_before(first);
57  assert_ins->make_assertion(guard);
58  assert_ins->source_location=first->source_location;
59  assert_ins->function=first->function;
60 
61  assert_ins->source_location.set_comment(
62  "Stack depth exceeds "+std::to_string(i_depth));
63  assert_ins->source_location.set_property_class("stack-depth");
64 
65  goto_programt::targett plus_ins=goto_program.insert_before(first);
66  plus_ins->make_assignment();
67  plus_ins->code=code_assignt(symbol,
68  plus_exprt(symbol, from_integer(1, symbol.type())));
69  plus_ins->source_location=first->source_location;
70  plus_ins->function=first->function;
71 
72  goto_programt::targett last=--goto_program.instructions.end();
73  assert(last->is_end_function());
74 
75  goto_programt::instructiont minus_ins;
76  minus_ins.make_assignment();
77  minus_ins.code=code_assignt(symbol,
78  minus_exprt(symbol, from_integer(1, symbol.type())));
79  minus_ins.source_location=last->source_location;
80  minus_ins.function=last->function;
81 
82  goto_program.insert_before_swap(last, minus_ins);
83 }
84 
86  symbol_tablet &symbol_table,
87  goto_functionst &goto_functions,
88  const int depth)
89 {
90  const symbol_exprt sym=add_stack_depth_symbol(symbol_table);
91  const exprt depth_expr(from_integer(depth, sym.type()));
92 
93  Forall_goto_functions(f_it, goto_functions)
94  if(f_it->second.body_available() &&
95  f_it->first!=CPROVER_PREFIX "initialize" &&
96  f_it->first!=goto_functionst::entry_point())
97  stack_depth(f_it->second.body, sym, depth, depth_expr);
98 
99  // initialize depth to 0
100  goto_functionst::function_mapt::iterator
101  i_it=goto_functions.function_map.find(CPROVER_PREFIX "initialize");
102  assert(i_it!=goto_functions.function_map.end());
103 
104  goto_programt &init=i_it->second.body;
105  goto_programt::targett first=init.instructions.begin();
106  goto_programt::targett it=init.insert_before(first);
107  it->make_assignment();
108  it->code=code_assignt(sym, from_integer(0, sym.type()));
109  it->source_location=first->source_location;
110  it->function=first->function;
111 
112  // update counters etc.
113  goto_functions.update();
114 }
irep_idt name
The unique identifier.
Definition: symbol.h:46
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:568
bool is_thread_local
Definition: symbol.h:70
#define CPROVER_PREFIX
irep_idt mode
Language mode.
Definition: symbol.h:55
instructionst instructions
The list of instructions in the goto program.
Goto Programs with Functions.
exprt value
Initial value of symbol.
Definition: symbol.h:40
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:58
typet & type()
Definition: expr.h:60
Stack depth checks.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
bool is_static_lifetime
Definition: symbol.h:70
Fixed-width bit-vector with two&#39;s complement interpretation.
Definition: std_types.h:1171
API to expression classes.
The symbol table.
Definition: symbol_table.h:52
The plus expression.
Definition: std_expr.h:702
symbol_exprt add_stack_depth_symbol(symbol_tablet &symbol_table)
Definition: stack_depth.cpp:24
Symbol table.
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
targett insert_before(const_targett target)
Insertion before the given target.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
typet type
Type of symbol.
Definition: symbol.h:37
API to type classes.
Base class for all expressions.
Definition: expr.h:46
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
Definition: expr.h:142
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
binary minus
Definition: std_expr.h:758
Expression to hold a symbol (variable)
Definition: std_expr.h:82
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Assignment.
Definition: std_code.h:144
bool is_lvalue
Definition: symbol.h:71
void stack_depth(goto_programt &goto_program, const symbol_exprt &symbol, const int i_depth, const exprt &max_depth)
Definition: stack_depth.cpp:45