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 
19 
21 
23 {
24  const irep_idt identifier="$stack_depth";
25  signedbv_typet type(sizeof(int)*8);
26 
27  symbolt new_symbol;
28  new_symbol.name=identifier;
29  new_symbol.base_name=identifier;
30  new_symbol.pretty_name=identifier;
31  new_symbol.type=type;
32  new_symbol.is_static_lifetime=true;
33  new_symbol.value=from_integer(0, type);
34  new_symbol.mode=ID_C;
35  new_symbol.is_thread_local=true;
36  new_symbol.is_lvalue=true;
37 
38  symbol_table.insert(std::move(new_symbol));
39 
40  return symbol_exprt(identifier, type);
41 }
42 
45  const symbol_exprt &symbol,
46  const int i_depth,
47  const exprt &max_depth)
48 {
49  assert(!goto_program.instructions.empty());
50 
52 
53  binary_relation_exprt guard(symbol, ID_le, max_depth);
55  assert_ins->make_assertion(guard);
56  assert_ins->source_location=first->source_location;
57  assert_ins->function=first->function;
58 
59  assert_ins->source_location.set_comment(
60  "Stack depth exceeds "+std::to_string(i_depth));
61  assert_ins->source_location.set_property_class("stack-depth");
62 
64  plus_ins->make_assignment();
65  plus_ins->code=code_assignt(symbol,
66  plus_exprt(symbol, from_integer(1, symbol.type())));
67  plus_ins->source_location=first->source_location;
68  plus_ins->function=first->function;
69 
71  assert(last->is_end_function());
72 
74  minus_ins.make_assignment();
75  minus_ins.code=code_assignt(symbol,
76  minus_exprt(symbol, from_integer(1, symbol.type())));
77  minus_ins.source_location=last->source_location;
78  minus_ins.function=last->function;
79 
80  goto_program.insert_before_swap(last, minus_ins);
81 }
82 
84  goto_modelt &goto_model,
85  const int depth)
86 {
87  const symbol_exprt sym=
89 
90  const exprt depth_expr(from_integer(depth, sym.type()));
91 
92  Forall_goto_functions(f_it, goto_model.goto_functions)
93  if(f_it->second.body_available() &&
94  f_it->first != INITIALIZE_FUNCTION &&
95  f_it->first!=goto_functionst::entry_point())
96  stack_depth(f_it->second.body, sym, depth, depth_expr);
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  goto_programt::targett it=init.insert_before(first);
108  it->make_assignment();
109  it->code=code_assignt(sym, from_integer(0, sym.type()));
110  // no suitable value for source location -- omitted
111  it->function = INITIALIZE_FUNCTION;
112 
113  // update counters etc.
114  goto_model.goto_functions.update();
115 }
irep_idt name
The unique identifier.
Definition: symbol.h:43
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:441
bool is_thread_local
Definition: symbol.h:67
targett insert_before(const_targett target)
Insertion before the given target.
Definition: goto_program.h:473
irep_idt mode
Language mode.
Definition: symbol.h:52
exprt value
Initial value of symbol.
Definition: symbol.h:37
function_mapt function_map
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:55
typet & type()
Definition: expr.h:56
Stack depth checks.
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
bool is_static_lifetime
Definition: symbol.h:67
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
Symbol Table + CFG.
instructionst::iterator targett
Definition: goto_program.h:397
Fixed-width bit-vector with two&#39;s complement interpretation.
Definition: std_types.h:1262
#define INITIALIZE_FUNCTION
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
The symbol table.
Definition: symbol_table.h:19
The plus expression.
Definition: std_expr.h:893
symbol_exprt add_stack_depth_symbol(symbol_tablet &symbol_table)
Definition: stack_depth.cpp:22
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
typet type
Type of symbol.
Definition: symbol.h:34
static irep_idt entry_point()
Base class for all expressions.
Definition: expr.h:42
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
std::string to_string(const string_constraintt &expr)
Used for debug printing.
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
Definition: expr.h:125
goto_programt & goto_program
Definition: cover.cpp:63
binary minus
Definition: std_expr.h:959
Expression to hold a symbol (variable)
Definition: std_expr.h:90
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
Assignment.
Definition: std_code.h:195
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
bool is_lvalue
Definition: symbol.h:68
void stack_depth(goto_programt &goto_program, const symbol_exprt &symbol, const int i_depth, const exprt &max_depth)
Definition: stack_depth.cpp:43