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/prefix.h>
18 #include <util/std_expr.h>
19 #include <util/string_constant.h>
20 
22  symbol_tablet &symbol_table,
23  const irep_idt &id,
24  const irep_idt &argument)
25 {
26  // already there?
27 
28  symbol_tablet::symbolst::const_iterator s_it=
29  symbol_table.symbols.find(id);
30 
31  if(s_it==symbol_table.symbols.end())
32  {
33  // not there
35  p.subtype().set(ID_C_constant, true);
36 
37  const code_typet function_type({code_typet::parametert(p)}, empty_typet());
38 
39  symbolt new_symbol;
40  new_symbol.name=id;
41  new_symbol.base_name=id;
42  new_symbol.type=function_type;
43 
44  symbol_table.insert(std::move(new_symbol));
45 
46  s_it=symbol_table.symbols.find(id);
47  assert(s_it!=symbol_table.symbols.end());
48  }
49 
50  // signature is expected to be
51  // (type *) -> ...
52  if(s_it->second.type.id()!=ID_code ||
53  to_code_type(s_it->second.type).parameters().size()!=1 ||
54  to_code_type(s_it->second.type).parameters()[0].type().id()!=ID_pointer)
55  {
56  std::string error = "function '" + id2string(id) + "' has wrong signature";
57  throw error;
58  }
59 
60  string_constantt function_id_string(argument);
61 
63  symbol_exprt(s_it->second.name, s_it->second.type),
64  {typecast_exprt(
65  address_of_exprt(
66  index_exprt(function_id_string, from_integer(0, index_type()))),
67  to_code_type(s_it->second.type).parameters()[0].type())});
68 
69  return call;
70 }
71 
73  goto_modelt &goto_model,
74  const irep_idt &id)
75 {
76  Forall_goto_functions(f_it, goto_model.goto_functions)
77  {
78  // don't instrument our internal functions
79  if(has_prefix(id2string(f_it->first), CPROVER_PREFIX))
80  continue;
81 
82  // don't instrument the function to be called,
83  // or otherwise this will be recursive
84  if(f_it->first==id)
85  continue;
86 
87  // patch in a call to `id' at the entry point
88  goto_programt &body=f_it->second.body;
89 
90  body.insert_before(
91  body.instructions.begin(),
93  function_to_call(goto_model.symbol_table, id, f_it->first)));
94  }
95 }
96 
98  goto_modelt &goto_model,
99  const irep_idt &id)
100 {
101  Forall_goto_functions(f_it, goto_model.goto_functions)
102  {
103  // don't instrument our internal functions
104  if(has_prefix(id2string(f_it->first), CPROVER_PREFIX))
105  continue;
106 
107  // don't instrument the function to be called,
108  // or otherwise this will be recursive
109  if(f_it->first==id)
110  continue;
111 
112  // patch in a call to `id' at the exit points
113  goto_programt &body=f_it->second.body;
114 
115  // make sure we have END_OF_FUNCTION
116  if(body.instructions.empty() ||
117  !body.instructions.back().is_end_function())
118  {
120  }
121 
123  {
124  if(i_it->is_return())
125  {
127  function_to_call(goto_model.symbol_table, id, f_it->first));
128  body.insert_before_swap(i_it, call);
129 
130  // move on
131  i_it++;
132  }
133  }
134 
135  // exiting without return
136  goto_programt::targett last=body.instructions.end();
137  last--;
138  assert(last->is_end_function());
139 
140  // is there already a return?
141  bool has_return=false;
142 
143  if(last!=body.instructions.begin())
144  {
145  goto_programt::targett before_last=last;
146  --before_last;
147  if(before_last->is_return())
148  has_return=true;
149  }
150 
151  if(!has_return)
152  {
154  function_to_call(goto_model.symbol_table, id, f_it->first));
155  body.insert_before_swap(last, call);
156  }
157  }
158 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1201
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:29
prefix.h
goto_programt::make_end_function
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:957
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:686
string_constant.h
goto_modelt
Definition: goto_model.h:26
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
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:1049
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
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:639
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
empty_typet
The empty type.
Definition: std_types.h:46
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
function_to_call
code_function_callt function_to_call(symbol_tablet &symbol_table, const irep_idt &id, const irep_idt &argument)
Definition: function.cpp:21
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:736
function_enter
void function_enter(goto_modelt &goto_model, const irep_idt &id)
Definition: function.cpp:72
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
cprover_prefix.h
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
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:585
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:442
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:753
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
function_exit
void function_exit(goto_modelt &goto_model, const irep_idt &id)
Definition: function.cpp:97
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:606
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
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:579