cprover
function.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Function Entering and Exiting
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "function.h"
13 
14 #include <util/arith_tools.h>
15 #include <util/c_types.h>
16 #include <util/cprover_prefix.h>
17 #include <util/pointer_expr.h>
18 #include <util/prefix.h>
19 #include <util/std_expr.h>
20 #include <util/string_constant.h>
21 
23  symbol_tablet &symbol_table,
24  const irep_idt &id,
25  const irep_idt &argument)
26 {
27  // already there?
28 
29  symbol_tablet::symbolst::const_iterator s_it=
30  symbol_table.symbols.find(id);
31 
32  if(s_it==symbol_table.symbols.end())
33  {
34  // not there
36  p.subtype().set(ID_C_constant, true);
37 
38  const code_typet function_type({code_typet::parametert(p)}, empty_typet());
39 
40  symbolt new_symbol;
41  new_symbol.name=id;
42  new_symbol.base_name=id;
43  new_symbol.type=function_type;
44 
45  symbol_table.insert(std::move(new_symbol));
46 
47  s_it=symbol_table.symbols.find(id);
48  assert(s_it!=symbol_table.symbols.end());
49  }
50 
51  // signature is expected to be
52  // (type *) -> ...
53  if(s_it->second.type.id()!=ID_code ||
54  to_code_type(s_it->second.type).parameters().size()!=1 ||
55  to_code_type(s_it->second.type).parameters()[0].type().id()!=ID_pointer)
56  {
57  std::string error = "function '" + id2string(id) + "' has wrong signature";
58  throw error;
59  }
60 
61  string_constantt function_id_string(argument);
62 
64  symbol_exprt(s_it->second.name, s_it->second.type),
65  {typecast_exprt(
66  address_of_exprt(
67  index_exprt(function_id_string, from_integer(0, index_type()))),
68  to_code_type(s_it->second.type).parameters()[0].type())});
69 
70  return call;
71 }
72 
74  goto_modelt &goto_model,
75  const irep_idt &id)
76 {
77  for(auto &gf_entry : goto_model.goto_functions.function_map)
78  {
79  // don't instrument our internal functions
80  if(has_prefix(id2string(gf_entry.first), CPROVER_PREFIX))
81  continue;
82 
83  // don't instrument the function to be called,
84  // or otherwise this will be recursive
85  if(gf_entry.first == id)
86  continue;
87 
88  // patch in a call to `id' at the entry point
89  goto_programt &body = gf_entry.second.body;
90 
91  body.insert_before(
92  body.instructions.begin(),
94  function_to_call(goto_model.symbol_table, id, gf_entry.first)));
95  }
96 }
97 
99  goto_modelt &goto_model,
100  const irep_idt &id)
101 {
102  for(auto &gf_entry : goto_model.goto_functions.function_map)
103  {
104  // don't instrument our internal functions
105  if(has_prefix(id2string(gf_entry.first), CPROVER_PREFIX))
106  continue;
107 
108  // don't instrument the function to be called,
109  // or otherwise this will be recursive
110  if(gf_entry.first == id)
111  continue;
112 
113  // patch in a call to `id' at the exit points
114  goto_programt &body = gf_entry.second.body;
115 
116  // make sure we have END_OF_FUNCTION
117  if(body.instructions.empty() ||
118  !body.instructions.back().is_end_function())
119  {
121  }
122 
124  {
125  if(i_it->is_return())
126  {
128  function_to_call(goto_model.symbol_table, id, gf_entry.first));
129  body.insert_before_swap(i_it, call);
130 
131  // move on
132  i_it++;
133  }
134  }
135 
136  // exiting without return
137  goto_programt::targett last=body.instructions.end();
138  last--;
139  assert(last->is_end_function());
140 
141  // is there already a return?
142  bool has_return=false;
143 
144  if(last!=body.instructions.begin())
145  {
146  goto_programt::targett before_last=last;
147  --before_last;
148  if(before_last->is_return())
149  has_return=true;
150  }
151 
152  if(!has_return)
153  {
155  function_to_call(goto_model.symbol_table, id, gf_entry.first));
156  body.insert_before_swap(last, call);
157  }
158  }
159 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1185
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
typet::subtype
const typet & subtype() const
Definition: type.h:47
arith_tools.h
typet
The type of an expression, extends irept.
Definition: type.h:28
prefix.h
goto_programt::make_end_function
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:941
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:670
string_constant.h
goto_modelt
Definition: goto_model.h:26
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
string_constantt
Definition: string_constant.h:16
goto_programt::make_function_call
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
Definition: goto_program.h:1033
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
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
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:738
empty_typet
The empty type.
Definition: std_types.h:45
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
function_to_call
code_function_callt function_to_call(symbol_tablet &symbol_table, const irep_idt &id, const irep_idt &argument)
Definition: function.cpp:22
pointer_expr.h
API to expression classes for Pointers.
symbol_tablet::insert
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Definition: symbol_table.cpp:19
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
code_typet
Base type of functions.
Definition: std_types.h:533
function_enter
void function_enter(goto_modelt &goto_model, const irep_idt &id)
Definition: function.cpp:73
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:649
cprover_prefix.h
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:569
function.h
Function Entering and Exiting.
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
code_typet::parametert
Definition: std_types.h:550
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
function_exit
void function_exit(goto_modelt &goto_model, const irep_idt &id)
Definition: function.cpp:98
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:590
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
std_expr.h
API to expression classes.
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
c_types.h
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:563