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 
91  body.insert_before(body.instructions.begin());
92  t->make_function_call(
93  function_to_call(goto_model.symbol_table, id, f_it->first));
94  t->function=f_it->first;
95  }
96 }
97 
99  goto_modelt &goto_model,
100  const irep_idt &id)
101 {
102  Forall_goto_functions(f_it, goto_model.goto_functions)
103  {
104  // don't instrument our internal functions
105  if(has_prefix(id2string(f_it->first), CPROVER_PREFIX))
106  continue;
107 
108  // don't instrument the function to be called,
109  // or otherwise this will be recursive
110  if(f_it->first==id)
111  continue;
112 
113  // patch in a call to `id' at the exit points
114  goto_programt &body=f_it->second.body;
115 
116  // make sure we have END_OF_FUNCTION
117  if(body.instructions.empty() ||
118  !body.instructions.back().is_end_function())
120 
122  {
123  if(i_it->is_return())
124  {
126  call.function=f_it->first;
127  call.make_function_call(
128  function_to_call(goto_model.symbol_table, id, f_it->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  call.make_function_call(
156  function_to_call(goto_model.symbol_table, id, f_it->first));
157  call.function=f_it->first;
158  body.insert_before_swap(last, call);
159  }
160  }
161 }
irep_idt function
The function this instruction belongs to.
Definition: goto_program.h:184
The type of an expression, extends irept.
Definition: type.h:27
irep_idt name
The unique identifier.
Definition: symbol.h:40
Function Entering and Exiting.
Base type of functions.
Definition: std_types.h:751
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:477
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:510
#define CPROVER_PREFIX
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.
Definition: symbol.h:27
void make_function_call(const codet &_code)
Definition: goto_program.h:299
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
instructionst::iterator targett
Definition: goto_program.h:414
The empty type.
Definition: std_types.h:48
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
API to expression classes.
void function_enter(goto_modelt &goto_model, const irep_idt &id)
Definition: function.cpp:72
The symbol table.
Definition: symbol_table.h:19
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
codet representation of a function call statement.
Definition: std_code.h:1036
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
const symbolst & symbols
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:541
const parameterst & parameters() const
Definition: std_types.h:893
#define Forall_goto_functions(it, functions)
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
Expression to hold a symbol (variable)
Definition: std_expr.h:143
const typet & subtype() const
Definition: type.h:38
void function_exit(goto_modelt &goto_model, const irep_idt &id)
Definition: function.cpp:98
code_function_callt function_to_call(symbol_tablet &symbol_table, const irep_idt &id, const irep_idt &argument)
Definition: function.cpp:21
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
bitvector_typet char_type()
Definition: c_types.cpp:114
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.