CBMC
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/pointer_expr.h>
18 #include <util/string_constant.h>
19 
21 
23  symbol_table_baset &symbol_table,
24  const irep_idt &id,
25  const irep_idt &argument)
26 {
27  // already there?
28 
29  symbol_table_baset::symbolst::const_iterator s_it =
30  symbol_table.symbols.find(id);
31 
32  if(s_it==symbol_table.symbols.end())
33  {
34  // This has to be dead code: a symbol table must contain all functions that
35  // appear in goto_functions.
37 #if 0
38 
39  // not there
40  auto p = pointer_type(char_type());
41  p.base_type().set(ID_C_constant, true);
42 
43  const code_typet function_type({code_typet::parametert(p)}, empty_typet());
44 
45  symbolt new_symbol{id, function_type, irep_idt{}};
46  new_symbol.base_name=id;
47 
48  symbol_table.insert(std::move(new_symbol));
49 
50  s_it=symbol_table.symbols.find(id);
51  DATA_INVARIANT(s_it != symbol_table.symbols.end(), "symbol not found");
52 #endif
53  }
54 
55  // signature is expected to be
56  // (type *) -> ...
57  if(s_it->second.type.id()!=ID_code ||
58  to_code_type(s_it->second.type).parameters().size()!=1 ||
59  to_code_type(s_it->second.type).parameters()[0].type().id()!=ID_pointer)
60  {
61  std::string error = "function '" + id2string(id) + "' has wrong signature";
62  throw error;
63  }
64 
65  string_constantt function_id_string(argument);
66 
68  symbol_exprt(s_it->second.name, s_it->second.type),
69  {typecast_exprt(
70  address_of_exprt(
71  index_exprt(function_id_string, from_integer(0, c_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  for(auto &gf_entry : goto_model.goto_functions.function_map)
82  {
83  // don't instrument our internal functions
84  if(gf_entry.first.starts_with(CPROVER_PREFIX))
85  continue;
86 
87  // don't instrument the function to be called,
88  // or otherwise this will be recursive
89  if(gf_entry.first == id)
90  continue;
91 
92  // patch in a call to `id' at the entry point
93  goto_programt &body = gf_entry.second.body;
94 
95  body.insert_before(
96  body.instructions.begin(),
98  function_to_call(goto_model.symbol_table, id, gf_entry.first)));
99  }
100 }
101 
103  goto_modelt &goto_model,
104  const irep_idt &id)
105 {
106  for(auto &gf_entry : goto_model.goto_functions.function_map)
107  {
108  // don't instrument our internal functions
109  if(gf_entry.first.starts_with(CPROVER_PREFIX))
110  continue;
111 
112  // don't instrument the function to be called,
113  // or otherwise this will be recursive
114  if(gf_entry.first == id)
115  continue;
116 
117  // patch in a call to `id' at the exit points
118  goto_programt &body = gf_entry.second.body;
119 
120  // make sure we have END_OF_FUNCTION
121  if(body.instructions.empty() ||
122  !body.instructions.back().is_end_function())
123  {
125  }
126 
128  {
129  if(i_it->is_set_return_value())
130  {
132  function_to_call(goto_model.symbol_table, id, gf_entry.first));
133  body.insert_before_swap(i_it, call);
134 
135  // move on
136  i_it++;
137  }
138  }
139 
140  // exiting without return
141  goto_programt::targett last=body.instructions.end();
142  last--;
143  DATA_INVARIANT(last->is_end_function(), "must be end of function");
144 
145  // is there already a return?
146  bool has_set_return_value = false;
147 
148  if(last!=body.instructions.begin())
149  {
150  goto_programt::targett before_last=last;
151  --before_last;
152  if(before_last->is_set_return_value())
153  has_set_return_value = true;
154  }
155 
156  if(!has_set_return_value)
157  {
159  function_to_call(goto_model.symbol_table, id, gf_entry.first));
160  body.insert_before_swap(last, call);
161  }
162  }
163 }
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:235
bitvector_typet char_type()
Definition: c_types.cpp:106
goto_instruction_codet representation of a function call statement.
Base type of functions.
Definition: std_types.h:583
const parameterst & parameters() const
Definition: std_types.h:699
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
The empty type.
Definition: std_types.h:51
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:181
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:643
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
instructionst::iterator targett
Definition: goto_program.h:614
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:739
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:692
Expression to hold a symbol (variable)
Definition: std_expr.h:131
The symbol table base class interface.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
Symbol table entry.
Definition: symbol.h:28
#define CPROVER_PREFIX
void function_exit(goto_modelt &goto_model, const irep_idt &id)
Definition: function.cpp:102
void function_enter(goto_modelt &goto_model, const irep_idt &id)
Definition: function.cpp:77
code_function_callt function_to_call(symbol_table_baset &symbol_table, const irep_idt &id, const irep_idt &argument)
Definition: function.cpp:22
Function Entering and Exiting.
Symbol Table + CFG.
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:40
API to expression classes for Pointers.
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:788