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  code_typet function_type;
38  function_type.return_type()=empty_typet();
39  function_type.parameters().push_back(
41 
42  symbolt new_symbol;
43  new_symbol.name=id;
44  new_symbol.base_name=id;
45  new_symbol.type=function_type;
46 
47  symbol_table.insert(std::move(new_symbol));
48 
49  s_it=symbol_table.symbols.find(id);
50  assert(s_it!=symbol_table.symbols.end());
51  }
52 
53  // signature is expected to be
54  // (type *) -> ...
55  if(s_it->second.type.id()!=ID_code ||
56  to_code_type(s_it->second.type).parameters().size()!=1 ||
57  to_code_type(s_it->second.type).parameters()[0].type().id()!=ID_pointer)
58  {
59  std::string error="function `"+id2string(id)+"' has wrong signature";
60  throw error;
61  }
62 
63  string_constantt function_id_string(argument);
64 
66  call.lhs().make_nil();
67  call.function()=
68  symbol_exprt(s_it->second.name, s_it->second.type);
69  call.arguments().resize(1);
70  call.arguments()[0]=
74  function_id_string, from_integer(0, index_type()))),
75  to_code_type(s_it->second.type).parameters()[0].type());
76 
77  return call;
78 }
79 
81  goto_modelt &goto_model,
82  const irep_idt &id)
83 {
84  Forall_goto_functions(f_it, goto_model.goto_functions)
85  {
86  // don't instrument our internal functions
87  if(has_prefix(id2string(f_it->first), CPROVER_PREFIX))
88  continue;
89 
90  // don't instrument the function to be called,
91  // or otherwise this will be recursive
92  if(f_it->first==id)
93  continue;
94 
95  // patch in a call to `id' at the entry point
96  goto_programt &body=f_it->second.body;
97 
99  body.insert_before(body.instructions.begin());
100  t->make_function_call(
101  function_to_call(goto_model.symbol_table, id, f_it->first));
102  t->function=f_it->first;
103  }
104 }
105 
107  goto_modelt &goto_model,
108  const irep_idt &id)
109 {
110  Forall_goto_functions(f_it, goto_model.goto_functions)
111  {
112  // don't instrument our internal functions
113  if(has_prefix(id2string(f_it->first), CPROVER_PREFIX))
114  continue;
115 
116  // don't instrument the function to be called,
117  // or otherwise this will be recursive
118  if(f_it->first==id)
119  continue;
120 
121  // patch in a call to `id' at the exit points
122  goto_programt &body=f_it->second.body;
123 
124  // make sure we have END_OF_FUNCTION
125  if(body.instructions.empty() ||
126  !body.instructions.back().is_end_function())
128 
130  {
131  if(i_it->is_return())
132  {
134  call.function=f_it->first;
135  call.make_function_call(
136  function_to_call(goto_model.symbol_table, id, f_it->first));
137  body.insert_before_swap(i_it, call);
138 
139  // move on
140  i_it++;
141  }
142  }
143 
144  // exiting without return
145  goto_programt::targett last=body.instructions.end();
146  last--;
147  assert(last->is_end_function());
148 
149  // is there already a return?
150  bool has_return=false;
151 
152  if(last!=body.instructions.begin())
153  {
154  goto_programt::targett before_last=last;
155  --before_last;
156  if(before_last->is_return())
157  has_return=true;
158  }
159 
160  if(!has_return)
161  {
163  call.make_function_call(
164  function_to_call(goto_model.symbol_table, id, f_it->first));
165  call.function=f_it->first;
166  body.insert_before_swap(last, call);
167  }
168  }
169 }
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:43
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:987
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:860
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:80
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:828
bitvector_typet index_type()
Definition: c_types.cpp:16
Operator to return the address of an object.
Definition: std_expr.h:3170
const symbolst & symbols
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
exprt & function()
Definition: std_code.h:848
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
const parameterst & parameters() const
Definition: std_types.h:905
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
#define Forall_goto_functions(it, functions)
void make_nil()
Definition: irep.h:243
#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:106
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
const typet & return_type() const
Definition: std_types.h:895
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
array index operator
Definition: std_expr.h:1462