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/cprover_prefix.h>
16 #include <util/prefix.h>
17 #include <util/std_expr.h>
18 
19 #include <util/c_types.h>
20 #include <ansi-c/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  code_typet function_type;
39  function_type.return_type()=empty_typet();
40  function_type.parameters().push_back(
42 
43  symbolt new_symbol;
44  new_symbol.name=id;
45  new_symbol.base_name=id;
46  new_symbol.type=function_type;
47 
48  symbol_table.move(new_symbol);
49 
50  s_it=symbol_table.symbols.find(id);
51  assert(s_it!=symbol_table.symbols.end());
52  }
53 
54  // signature is expected to be
55  // (type *) -> ...
56  if(s_it->second.type.id()!=ID_code ||
57  to_code_type(s_it->second.type).parameters().size()!=1 ||
58  to_code_type(s_it->second.type).parameters()[0].type().id()!=ID_pointer)
59  {
60  std::string error="function `"+id2string(id)+"' has wrong signature";
61  throw error;
62  }
63 
64  string_constantt function_id_string(argument);
65 
67  call.lhs().make_nil();
68  call.function()=
69  symbol_exprt(s_it->second.name, s_it->second.type);
70  call.arguments().resize(1);
71  call.arguments()[0]=
75  function_id_string, from_integer(0, index_type()))),
76  to_code_type(s_it->second.type).parameters()[0].type());
77 
78  return call;
79 }
80 
82  symbol_tablet &symbol_table,
83  goto_functionst &goto_functions,
84  const irep_idt &id)
85 {
86  Forall_goto_functions(f_it, goto_functions)
87  {
88  // don't instrument our internal functions
89  if(has_prefix(id2string(f_it->first), CPROVER_PREFIX))
90  continue;
91 
92  // don't instrument the function to be called,
93  // or otherwise this will be recursive
94  if(f_it->first==id)
95  continue;
96 
97  // patch in a call to `id' at the entry point
98  goto_programt &body=f_it->second.body;
99 
101  body.insert_before(body.instructions.begin());
102  t->make_function_call(
103  function_to_call(symbol_table, id, f_it->first));
104  t->function=f_it->first;
105  }
106 }
107 
109  symbol_tablet &symbol_table,
110  goto_functionst &goto_functions,
111  const irep_idt &id)
112 {
113  Forall_goto_functions(f_it, goto_functions)
114  {
115  // don't instrument our internal functions
116  if(has_prefix(id2string(f_it->first), CPROVER_PREFIX))
117  continue;
118 
119  // don't instrument the function to be called,
120  // or otherwise this will be recursive
121  if(f_it->first==id)
122  continue;
123 
124  // patch in a call to `id' at the exit points
125  goto_programt &body=f_it->second.body;
126 
127  // make sure we have END_OF_FUNCTION
128  if(body.instructions.empty() ||
129  !body.instructions.back().is_end_function())
131 
133  {
134  if(i_it->is_return())
135  {
136  goto_programt::instructiont call;
137  call.function=f_it->first;
138  call.make_function_call(
139  function_to_call(symbol_table, id, f_it->first));
140  body.insert_before_swap(i_it, call);
141 
142  // move on
143  i_it++;
144  }
145  }
146 
147  // exiting without return
148  goto_programt::targett last=body.instructions.end();
149  last--;
150  assert(last->is_end_function());
151 
152  // is there already a return?
153  bool has_return=false;
154 
155  if(last!=body.instructions.begin())
156  {
157  goto_programt::targett before_last=last;
158  --before_last;
159  if(before_last->is_return())
160  has_return=true;
161  }
162 
163  if(!has_return)
164  {
165  goto_programt::instructiont call;
166  call.make_function_call(
167  function_to_call(symbol_table, id, f_it->first));
168  call.function=f_it->first;
169  body.insert_before_swap(last, call);
170  }
171  }
172 }
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
semantic type conversion
Definition: std_expr.h:1725
Function Entering and Exiting.
targett add_instruction()
Adds an instruction at the end.
Base type of functions.
Definition: std_types.h:734
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
#define CPROVER_PREFIX
instructionst instructions
The list of instructions in the goto program.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
void function_exit(symbol_tablet &symbol_table, goto_functionst &goto_functions, const irep_idt &id)
Definition: function.cpp:108
argumentst & arguments()
Definition: std_code.h:689
symbolst symbols
Definition: symbol_table.h:57
The empty type.
Definition: std_types.h:53
API to expression classes.
The symbol table.
Definition: symbol_table.h:52
A function call.
Definition: std_code.h:657
bitvector_typet index_type()
Definition: c_types.cpp:15
Operator to return the address of an object.
Definition: std_expr.h:2593
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
targett insert_before(const_targett target)
Insertion before the given target.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
typet type
Type of symbol.
Definition: symbol.h:37
exprt & function()
Definition: std_code.h:677
const parameterst & parameters() const
Definition: std_types.h:841
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
#define Forall_goto_functions(it, functions)
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
void make_nil()
Definition: irep.h:243
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
void function_enter(symbol_tablet &symbol_table, goto_functionst &goto_functions, const irep_idt &id)
Definition: function.cpp:81
Expression to hold a symbol (variable)
Definition: std_expr.h:82
const typet & subtype() const
Definition: type.h:31
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:22
bitvector_typet char_type()
Definition: c_types.cpp:113
const typet & return_type() const
Definition: std_types.h:831
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
array index operator
Definition: std_expr.h:1170