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
64 string_constantt function_id_string(argument);
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
83 if(has_prefix(id2string(gf_entry.first), CPROVER_PREFIX))
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
108 if(has_prefix(id2string(gf_entry.first), CPROVER_PREFIX))
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));
132 body.insert_before_swap(i_it, call);
133
134 // move on
135 i_it++;
136 }
137 }
138
139 // exiting without return
140 goto_programt::targett last=body.instructions.end();
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 {
149 goto_programt::targett before_last=last;
150 --before_last;
151 if(before_last->is_set_return_value())
152 has_set_return_value = true;
153 }
154
155 if(!has_set_return_value)
156 {
158 function_to_call(goto_model.symbol_table, id, gf_entry.first));
159 body.insert_before_swap(last, call);
160 }
161 }
162}
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
bitvector_typet char_type()
Definition: c_types.cpp:124
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.
Definition: goto_program.h:180
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:598
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:619
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:986
instructionst::iterator targett
Definition: goto_program.h:592
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:715
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:668
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.
Definition: symbol_table.h:14
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Symbol table entry.
Definition: symbol.h:28
irep_idt name
The unique identifier.
Definition: symbol.h:40
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.