cprover
Loading...
Searching...
No Matches
simple_method_stubbing.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Simple Java method stubbing
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
11
13
18
19#include "java_utils.h"
21#include <util/namespace.h>
22#include <util/std_code.h>
24
60
82 const typet &expected_type,
83 const exprt &ptr,
84 const source_locationt &loc,
85 const irep_idt &function_id,
87 const unsigned insert_before_index,
88 const bool is_constructor,
89 const bool update_in_place)
90{
91 // At this point we know 'ptr' points to an opaque-typed object.
92 // We should nondet-initialize it and insert the instructions *after*
93 // the offending call at (*parent_block)[insert_before_index].
94
97 "Nondet initializer result type: expected a pointer",
99
101
102 const auto &expected_base =
103 ns.follow(to_pointer_type(expected_type).base_type());
104 if(expected_base.id() != ID_struct)
105 return;
106
107 const exprt cast_ptr =
109
111 // If it's a constructor the thing we're constructing has already
112 // been allocated by this point.
115
118 parameters.min_null_tree_depth = 1;
119
120 // Generate new instructions.
122 parameters.function_id = function_id;
124 to_init,
127 loc,
130 parameters,
134
135 // Insert new_instructions into parent block.
136 if(!new_instructions.statements().empty())
137 {
138 auto insert_position = parent_block.statements().begin();
140 parent_block.statements().insert(
142 new_instructions.statements().begin(),
143 new_instructions.statements().end());
144 }
145}
146
152{
155
156 // synthetic source location that contains the opaque function name only
158 synthesized_source_location.set_function(symbol.name);
159
160 // make sure all parameters are named
161 for(auto &parameter : required_type.parameters())
162 {
163 if(parameter.get_identifier().empty())
164 {
166 parameter.type(),
167 "#anon",
169 symbol.name,
171 parameter_symbol.is_parameter = true;
172 parameter.set_base_name(parameter_symbol.base_name);
173 parameter.set_identifier(parameter_symbol.name);
174 }
175 }
176
177 // Initialize the return value or `this` parameter under construction.
178 // Note symbol.type is required_type, but with write access
179 // Probably required_type should not be const
180 const bool is_constructor = required_type.get_is_constructor();
182 {
183 const auto &this_argument = required_type.parameters()[0];
184 const typet &this_type = this_argument.type();
186 this_type,
187 "to_construct",
189 symbol.name,
191 const symbol_exprt &init_symbol_expression = init_symbol.symbol_expr();
194 symbol_exprt(this_argument.get_identifier(), this_type));
195 get_argument.add_source_location() = synthesized_source_location;
198 this_type,
201 symbol.name,
203 1,
204 true,
205 false);
206 }
207 else
208 {
209 const typet &required_return_type = required_type.return_type();
211 {
214 "to_return",
216 symbol.name,
218 const exprt &to_return = to_return_symbol.symbol_expr();
219 if(to_return_symbol.type.id() != ID_pointer)
220 {
223 parameters.min_null_tree_depth = 1;
224
226 to_return,
230 false,
231 lifetimet::AUTOMATIC_LOCAL, // Irrelevant as type is primitive
232 parameters,
235 }
236 else
239 to_return,
241 symbol.name,
243 0,
244 false,
245 false);
247 }
248 }
249
250 symbol.value = new_instructions;
251}
252
257{
259 if(!sym.is_type && sym.value.id() == ID_nil &&
260 sym.type.id() == ID_code &&
261 // do not stub internal locking calls as 'create_method_stub' does not
262 // automatically create the appropriate symbols for the formal parameters.
263 // This means that symex will (rightfully) crash when it encounters the
264 // function call as it will not be able to find symbols for the fromal
265 // parameters.
266 sym.name !=
267 "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" &&
268 sym.name !=
269 "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V")
270 {
272 }
273}
274
276 const irep_idt &function_name,
277 symbol_table_baset &symbol_table,
278 bool assume_non_null,
279 const java_object_factory_parameterst &object_factory_parameters,
280 message_handlert &message_handler)
281{
283 symbol_table, assume_non_null, object_factory_parameters, message_handler);
284
285 stub_generator.check_method_stub(function_name);
286}
287
298 symbol_table_baset &symbol_table,
299 bool assume_non_null,
300 const java_object_factory_parameterst &object_factory_parameters,
301 message_handlert &message_handler)
302{
303 // The intent here is to apply stub_generator.check_method_stub() to
304 // all the identifiers in the symbol table. However this method may alter the
305 // symbol table and iterating over a container which is being modified has
306 // undefined behaviour. Therefore in order for this to work reliably, we must
307 // take a copy of the identifiers in the symbol table and iterate over that,
308 // instead of iterating over the symbol table itself.
309 std::vector<irep_idt> identifiers;
310 identifiers.reserve(symbol_table.symbols.size());
311 for(const auto &symbol : symbol_table)
312 identifiers.push_back(symbol.first);
313
315 symbol_table, assume_non_null, object_factory_parameters, message_handler);
316
317 for(const auto &identifier : identifiers)
318 {
319 stub_generator.check_method_stub(identifier);
320 }
321}
@ DYNAMIC
Allocate dynamic objects (using ALLOCATE)
@ AUTOMATIC_LOCAL
Allocate local objects with automatic lifetime.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
A codet representing sequential composition of program statements.
Definition std_code.h:130
A codet representing an assignment in the program.
Definition std_code.h:24
codet representation of a "return from a function" statement.
Definition std_code.h:893
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
void check_method_stub(const irep_idt &)
Replaces sym with a function stub per the function above if it is of suitable type.
const java_object_factory_parameterst & object_factory_parameters
java_simple_method_stubst(symbol_table_baset &_symbol_table, bool _assume_non_null, const java_object_factory_parameterst &_object_factory_parameters, message_handlert &_message_handler)
void create_method_stub_at(const typet &expected_type, const exprt &ptr, const source_locationt &loc, const irep_idt &function_id, code_blockt &parent_block, unsigned insert_before_index, bool is_constructor, bool update_in_place)
Nondet-initialize an object, including allocating referees for reference fields and nondet-initialisi...
void create_method_stub(symbolt &symbol)
Replaces sym's value with an opaque method stub.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Expression to hold a symbol (variable)
Definition std_expr.h:113
The symbol table base class interface.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Symbol table entry.
Definition symbol.h:28
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
exprt value
Initial value of symbol.
Definition symbol.h:34
The type of an expression, extends irept.
Definition type.h:29
#define INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP)
Equivalent to INVARIANT_STRUCTURED(CONDITION, invariant_failedt, pretty_print_invariant_with_irep(I...
static bool is_constructor(const irep_idt &method_name)
static std::unordered_set< irep_idt > init_symbol(const symbolt &sym, code_blockt &code_block, symbol_table_baset &symbol_table, const source_locationt &source_location, bool assume_init_pointers_not_null, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled, message_handlert &message_handler)
void gen_nondet_init(const exprt &expr, code_blockt &init_code, symbol_table_baset &symbol_table, const source_locationt &loc, bool skip_classid, lifetimet lifetime, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place, message_handlert &log)
Initializes a primitive-typed or reference-typed object tree rooted at expr, allocating child objects...
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
exprt make_clean_pointer_cast(const exprt &rawptr, const pointer_typet &target_type, const namespacet &ns)
JAVA Pointer Casts.
empty_typet java_void_type()
const java_method_typet & to_java_method_type(const typet &type)
Definition java_types.h:184
symbolt & fresh_java_symbol(const typet &type, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &function_name, symbol_table_baset &symbol_table)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
void java_generate_simple_method_stub(const irep_idt &function_name, symbol_table_baset &symbol_table, bool assume_non_null, const java_object_factory_parameterst &object_factory_parameters, message_handlert &message_handler)
void java_generate_simple_method_stubs(symbol_table_baset &symbol_table, bool assume_non_null, const java_object_factory_parameterst &object_factory_parameters, message_handlert &message_handler)
Generates function stubs for most undefined functions in the symbol table, except as forbidden in jav...
Java simple opaque stub generation.
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
size_t min_null_tree_depth
To force a certain depth of non-null objects.
Author: Diffblue Ltd.