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>
19#include <util/std_code.h>
21#include <util/symbol_table.h>
22
24
26 symbol_tablet &symbol_table,
27 const irep_idt &id,
28 const irep_idt &argument)
29{
30 // already there?
31
32 symbol_tablet::symbolst::const_iterator s_it=
33 symbol_table.symbols.find(id);
34
35 if(s_it==symbol_table.symbols.end())
36 {
37 // not there
39 p.subtype().set(ID_C_constant, true);
40
41 const code_typet function_type({code_typet::parametert(p)}, empty_typet());
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.insert(std::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
65
67 symbol_exprt(s_it->second.name, s_it->second.type),
68 {typecast_exprt(
69 address_of_exprt(
70 index_exprt(function_id_string, from_integer(0, c_index_type()))),
71 to_code_type(s_it->second.type).parameters()[0].type())});
72
73 return call;
74}
75
77 goto_modelt &goto_model,
78 const irep_idt &id)
79{
80 for(auto &gf_entry : goto_model.goto_functions.function_map)
81 {
82 // don't instrument our internal functions
84 continue;
85
86 // don't instrument the function to be called,
87 // or otherwise this will be recursive
88 if(gf_entry.first == id)
89 continue;
90
91 // patch in a call to `id' at the entry point
92 goto_programt &body = gf_entry.second.body;
93
94 body.insert_before(
95 body.instructions.begin(),
97 function_to_call(goto_model.symbol_table, id, gf_entry.first)));
98 }
99}
100
102 goto_modelt &goto_model,
103 const irep_idt &id)
104{
105 for(auto &gf_entry : goto_model.goto_functions.function_map)
106 {
107 // don't instrument our internal functions
109 continue;
110
111 // don't instrument the function to be called,
112 // or otherwise this will be recursive
113 if(gf_entry.first == id)
114 continue;
115
116 // patch in a call to `id' at the exit points
117 goto_programt &body = gf_entry.second.body;
118
119 // make sure we have END_OF_FUNCTION
120 if(body.instructions.empty() ||
121 !body.instructions.back().is_end_function())
122 {
124 }
125
127 {
128 if(i_it->is_set_return_value())
129 {
131 function_to_call(goto_model.symbol_table, id, gf_entry.first));
133
134 // move on
135 i_it++;
136 }
137 }
138
139 // exiting without return
141 last--;
142 assert(last->is_end_function());
143
144 // is there already a return?
145 bool has_set_return_value = false;
146
147 if(last!=body.instructions.begin())
148 {
150 --before_last;
151 if(before_last->is_set_return_value())
153 }
154
156 {
158 function_to_call(goto_model.symbol_table, id, gf_entry.first));
160 }
161 }
162}
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:253
bitvector_typet char_type()
Definition c_types.cpp:124
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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:37
The empty type.
Definition std_types.h:51
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:33
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.
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
Expression to hold a symbol (variable)
Definition std_expr.h:80
const symbolst & symbols
Read-only field, used to look up symbols given their names.
The symbol table.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Symbol table entry.
Definition symbol.h:28
The type of an expression, extends irept.
Definition type.h:29
const typet & subtype() const
Definition type.h:48
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:101
code_function_callt function_to_call(symbol_tablet &symbol_table, const irep_idt &id, const irep_idt &argument)
Definition function.cpp:25
void function_enter(goto_modelt &goto_model, const irep_idt &id)
Definition function.cpp:76
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.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
Author: Diffblue Ltd.