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  call.lhs().make_nil();
64  call.function()=
65  symbol_exprt(s_it->second.name, s_it->second.type);
66  call.arguments().resize(1);
67  call.arguments()[0]=
71  function_id_string, from_integer(0, index_type()))),
72  to_code_type(s_it->second.type).parameters()[0].type());
73 
74  return call;
75 }
76 
78  goto_modelt &goto_model,
79  const irep_idt &id)
80 {
81  Forall_goto_functions(f_it, goto_model.goto_functions)
82  {
83  // don't instrument our internal functions
84  if(has_prefix(id2string(f_it->first), CPROVER_PREFIX))
85  continue;
86 
87  // don't instrument the function to be called,
88  // or otherwise this will be recursive
89  if(f_it->first==id)
90  continue;
91 
92  // patch in a call to `id' at the entry point
93  goto_programt &body=f_it->second.body;
94 
96  body.insert_before(body.instructions.begin());
97  t->make_function_call(
98  function_to_call(goto_model.symbol_table, id, f_it->first));
99  t->function=f_it->first;
100  }
101 }
102 
104  goto_modelt &goto_model,
105  const irep_idt &id)
106 {
107  Forall_goto_functions(f_it, goto_model.goto_functions)
108  {
109  // don't instrument our internal functions
110  if(has_prefix(id2string(f_it->first), CPROVER_PREFIX))
111  continue;
112 
113  // don't instrument the function to be called,
114  // or otherwise this will be recursive
115  if(f_it->first==id)
116  continue;
117 
118  // patch in a call to `id' at the exit points
119  goto_programt &body=f_it->second.body;
120 
121  // make sure we have END_OF_FUNCTION
122  if(body.instructions.empty() ||
123  !body.instructions.back().is_end_function())
125 
127  {
128  if(i_it->is_return())
129  {
131  call.function=f_it->first;
132  call.make_function_call(
133  function_to_call(goto_model.symbol_table, id, f_it->first));
134  body.insert_before_swap(i_it, call);
135 
136  // move on
137  i_it++;
138  }
139  }
140 
141  // exiting without return
142  goto_programt::targett last=body.instructions.end();
143  last--;
144  assert(last->is_end_function());
145 
146  // is there already a return?
147  bool has_return=false;
148 
149  if(last!=body.instructions.begin())
150  {
151  goto_programt::targett before_last=last;
152  --before_last;
153  if(before_last->is_return())
154  has_return=true;
155  }
156 
157  if(!has_return)
158  {
160  call.make_function_call(
161  function_to_call(goto_model.symbol_table, id, f_it->first));
162  call.function=f_it->first;
163  body.insert_before_swap(last, call);
164  }
165  }
166 }
irep_idt function
The function this instruction belongs to.
Definition: goto_program.h:179
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
semantic type conversion
Definition: std_expr.h:2111
Function Entering and Exiting.
Base type of functions.
Definition: std_types.h:764
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:441
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
targett insert_before(const_targett target)
Insertion before the given target.
Definition: goto_program.h:473
#define CPROVER_PREFIX
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:993
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
void make_function_call(const codet &_code)
Definition: goto_program.h:294
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
argumentst & arguments()
Definition: std_code.h:890
instructionst::iterator targett
Definition: goto_program.h:397
The empty type.
Definition: std_types.h:54
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
API to expression classes.
void function_enter(goto_modelt &goto_model, const irep_idt &id)
Definition: function.cpp:77
The symbol table.
Definition: symbol_table.h:19
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
A function call.
Definition: std_code.h:858
bitvector_typet index_type()
Definition: c_types.cpp:16
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Operator to return the address of an object.
Definition: std_expr.h:3168
const symbolst & symbols
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
exprt & function()
Definition: std_code.h:878
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
const parameterst & parameters() const
Definition: std_types.h:905
#define Forall_goto_functions(it, functions)
void make_nil()
Definition: irep.h:315
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
Expression to hold a symbol (variable)
Definition: std_expr.h:90
const typet & subtype() const
Definition: type.h:33
void function_exit(goto_modelt &goto_model, const irep_idt &id)
Definition: function.cpp:103
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
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.
array index operator
Definition: std_expr.h:1462