cprover
Loading...
Searching...
No Matches
function.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Function Entering and Exiting
4
5Author: 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/prefix.h>
20
22
24 symbol_table_baset &symbol_table,
25 const irep_idt &id,
26 const irep_idt &argument)
27{
28 // already there?
29
30 symbol_table_baset::symbolst::const_iterator s_it =
31 symbol_table.symbols.find(id);
32
33 if(s_it==symbol_table.symbols.end())
34 {
35 // This has to be dead code: a symbol table must contain all functions that
36 // appear in goto_functions.
38#if 0
39
40 // not there
41 auto p = pointer_type(char_type());
42 p.base_type().set(ID_C_constant, true);
43
44 const code_typet function_type({code_typet::parametert(p)}, empty_typet());
45
46 symbolt new_symbol{id, function_type, irep_idt{}};
47 new_symbol.base_name=id;
48
49 symbol_table.insert(std::move(new_symbol));
50
51 s_it=symbol_table.symbols.find(id);
52 DATA_INVARIANT(s_it != symbol_table.symbols.end(), "symbol not found");
53#endif
54 }
55
56 // signature is expected to be
57 // (type *) -> ...
58 if(s_it->second.type.id()!=ID_code ||
59 to_code_type(s_it->second.type).parameters().size()!=1 ||
60 to_code_type(s_it->second.type).parameters()[0].type().id()!=ID_pointer)
61 {
62 std::string error = "function '" + id2string(id) + "' has wrong signature";
63 throw error;
64 }
65
66 string_constantt function_id_string(argument);
67
69 symbol_exprt(s_it->second.name, s_it->second.type),
70 {typecast_exprt(
71 address_of_exprt(
72 index_exprt(function_id_string, from_integer(0, c_index_type()))),
73 to_code_type(s_it->second.type).parameters()[0].type())});
74
75 return call;
76}
77
79 goto_modelt &goto_model,
80 const irep_idt &id)
81{
82 for(auto &gf_entry : goto_model.goto_functions.function_map)
83 {
84 // don't instrument our internal functions
85 if(has_prefix(id2string(gf_entry.first), CPROVER_PREFIX))
86 continue;
87
88 // don't instrument the function to be called,
89 // or otherwise this will be recursive
90 if(gf_entry.first == id)
91 continue;
92
93 // patch in a call to `id' at the entry point
94 goto_programt &body = gf_entry.second.body;
95
96 body.insert_before(
97 body.instructions.begin(),
99 function_to_call(goto_model.symbol_table, id, gf_entry.first)));
100 }
101}
102
104 goto_modelt &goto_model,
105 const irep_idt &id)
106{
107 for(auto &gf_entry : goto_model.goto_functions.function_map)
108 {
109 // don't instrument our internal functions
110 if(has_prefix(id2string(gf_entry.first), CPROVER_PREFIX))
111 continue;
112
113 // don't instrument the function to be called,
114 // or otherwise this will be recursive
115 if(gf_entry.first == id)
116 continue;
117
118 // patch in a call to `id' at the exit points
119 goto_programt &body = gf_entry.second.body;
120
121 // make sure we have END_OF_FUNCTION
122 if(body.instructions.empty() ||
123 !body.instructions.back().is_end_function())
124 {
126 }
127
129 {
130 if(i_it->is_set_return_value())
131 {
133 function_to_call(goto_model.symbol_table, id, gf_entry.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 DATA_INVARIANT(last->is_end_function(), "must be end of function");
145
146 // is there already a return?
147 bool has_set_return_value = false;
148
149 if(last!=body.instructions.begin())
150 {
151 goto_programt::targett before_last=last;
152 --before_last;
153 if(before_last->is_set_return_value())
154 has_set_return_value = true;
155 }
156
157 if(!has_set_return_value)
158 {
160 function_to_call(goto_model.symbol_table, id, gf_entry.first));
161 body.insert_before_swap(last, call);
162 }
163 }
164}
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:240
bitvector_typet char_type()
Definition c_types.cpp:111
goto_instruction_codet representation of a function call statement.
Base type of functions.
Definition std_types.h:539
const parameterst & parameters() const
Definition std_types.h:655
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
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.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
instructionst::iterator targett
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.
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Expression to hold a symbol (variable)
Definition std_expr.h:113
The symbol table base class interface.
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Symbol table entry.
Definition symbol.h:28
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
#define CPROVER_PREFIX
void function_exit(goto_modelt &goto_model, const irep_idt &id)
Definition function.cpp:103
void function_enter(goto_modelt &goto_model, const irep_idt &id)
Definition function.cpp:78
code_function_callt function_to_call(symbol_table_baset &symbol_table, const irep_idt &id, const irep_idt &argument)
Definition function.cpp:23
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:47
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:744