cprover
simple_method_stubbing.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Simple Java method stubbing
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
11 
12 #include "simple_method_stubbing.h"
13 
16 
17 #include "java_utils.h"
18 #include <util/invariant_utils.h>
19 #include <util/namespace.h>
20 #include <util/std_code.h>
21 #include <util/std_expr.h>
22 
24 {
25 public:
27  symbol_table_baset &_symbol_table,
28  bool _assume_non_null,
29  const java_object_factory_parameterst &_object_factory_parameters,
30  message_handlert &_message_handler)
31  : symbol_table(_symbol_table),
32  assume_non_null(_assume_non_null),
33  object_factory_parameters(_object_factory_parameters),
34  message_handler(_message_handler)
35  {
36  }
37 
39  const typet &expected_type,
40  const exprt &ptr,
41  const source_locationt &loc,
42  const irep_idt &function_id,
43  code_blockt &parent_block,
44  unsigned insert_before_index,
45  bool is_constructor,
46  bool update_in_place);
47 
48  void create_method_stub(symbolt &symbol);
49 
50  void check_method_stub(const irep_idt &);
51 
52 protected:
57 };
58 
80  const typet &expected_type,
81  const exprt &ptr,
82  const source_locationt &loc,
83  const irep_idt &function_id,
84  code_blockt &parent_block,
85  const unsigned insert_before_index,
86  const bool is_constructor,
87  const bool update_in_place)
88 {
89  // At this point we know 'ptr' points to an opaque-typed object.
90  // We should nondet-initialize it and insert the instructions *after*
91  // the offending call at (*parent_block)[insert_before_index].
92 
94  expected_type.id() == ID_pointer,
95  "Nondet initializer result type: expected a pointer",
96  expected_type);
97 
99 
100  const auto &expected_base = ns.follow(expected_type.subtype());
101  if(expected_base.id() != ID_struct)
102  return;
103 
104  const exprt cast_ptr =
105  make_clean_pointer_cast(ptr, to_pointer_type(expected_type), ns);
106 
107  exprt to_init = cast_ptr;
108  // If it's a constructor the thing we're constructing has already
109  // been allocated by this point.
110  if(is_constructor)
111  to_init = dereference_exprt(to_init);
112 
114  if(assume_non_null)
115  parameters.min_null_tree_depth = 1;
116 
117  // Generate new instructions.
118  code_blockt new_instructions;
119  parameters.function_id = function_id;
121  to_init,
122  new_instructions,
123  symbol_table,
124  loc,
127  parameters,
131 
132  // Insert new_instructions into parent block.
133  if(!new_instructions.statements().empty())
134  {
135  auto insert_position = parent_block.statements().begin();
136  std::advance(insert_position, insert_before_index);
137  parent_block.statements().insert(
138  insert_position,
139  new_instructions.statements().begin(),
140  new_instructions.statements().end());
141  }
142 }
143 
149 {
150  code_blockt new_instructions;
151  java_method_typet &required_type = to_java_method_type(symbol.type);
152 
153  // synthetic source location that contains the opaque function name only
154  source_locationt synthesized_source_location;
155  synthesized_source_location.set_function(symbol.name);
156 
157  // make sure all parameters are named
158  for(auto &parameter : required_type.parameters())
159  {
160  if(parameter.get_identifier().empty())
161  {
162  symbolt &parameter_symbol = fresh_java_symbol(
163  parameter.type(),
164  "#anon",
165  synthesized_source_location,
166  symbol.name,
167  symbol_table);
168  parameter_symbol.is_parameter = true;
169  parameter.set_base_name(parameter_symbol.base_name);
170  parameter.set_identifier(parameter_symbol.name);
171  }
172  }
173 
174  // Initialize the return value or `this` parameter under construction.
175  // Note symbol.type is required_type, but with write access
176  // Probably required_type should not be const
177  const bool is_constructor = required_type.get_is_constructor();
178  if(is_constructor)
179  {
180  const auto &this_argument = required_type.parameters()[0];
181  const typet &this_type = this_argument.type();
182  symbolt &init_symbol = fresh_java_symbol(
183  this_type,
184  "to_construct",
185  synthesized_source_location,
186  symbol.name,
187  symbol_table);
188  const symbol_exprt &init_symbol_expression = init_symbol.symbol_expr();
189  code_assignt get_argument(
190  init_symbol_expression,
191  symbol_exprt(this_argument.get_identifier(), this_type));
192  get_argument.add_source_location() = synthesized_source_location;
193  new_instructions.add(get_argument);
195  this_type,
196  init_symbol_expression,
197  synthesized_source_location,
198  symbol.name,
199  new_instructions,
200  1,
201  true,
202  false);
203  }
204  else
205  {
206  const typet &required_return_type = required_type.return_type();
207  if(required_return_type != java_void_type())
208  {
209  symbolt &to_return_symbol = fresh_java_symbol(
210  required_return_type,
211  "to_return",
212  synthesized_source_location,
213  symbol.name,
214  symbol_table);
215  const exprt &to_return = to_return_symbol.symbol_expr();
216  if(to_return_symbol.type.id() != ID_pointer)
217  {
219  if(assume_non_null)
220  parameters.min_null_tree_depth = 1;
221 
223  to_return,
224  new_instructions,
225  symbol_table,
227  false,
228  lifetimet::AUTOMATIC_LOCAL, // Irrelevant as type is primitive
229  parameters,
232  }
233  else
235  required_return_type,
236  to_return,
237  synthesized_source_location,
238  symbol.name,
239  new_instructions,
240  0,
241  false,
242  false);
243  new_instructions.add(code_returnt(to_return));
244  }
245  }
246 
247  symbol.value = new_instructions;
248 }
249 
254 {
255  const symbolt &sym = symbol_table.lookup_ref(symname);
256  if(!sym.is_type && sym.value.id() == ID_nil &&
257  sym.type.id() == ID_code &&
258  // do not stub internal locking calls as 'create_method_stub' does not
259  // automatically create the appropriate symbols for the formal parameters.
260  // This means that symex will (rightfully) crash when it encounters the
261  // function call as it will not be able to find symbols for the fromal
262  // parameters.
263  sym.name !=
264  "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" &&
265  sym.name !=
266  "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V")
267  {
269  }
270 }
271 
273  const irep_idt &function_name,
274  symbol_table_baset &symbol_table,
275  bool assume_non_null,
276  const java_object_factory_parameterst &object_factory_parameters,
277  message_handlert &message_handler)
278 {
279  java_simple_method_stubst stub_generator(
280  symbol_table, assume_non_null, object_factory_parameters, message_handler);
281 
282  stub_generator.check_method_stub(function_name);
283 }
284 
295  symbol_table_baset &symbol_table,
296  bool assume_non_null,
297  const java_object_factory_parameterst &object_factory_parameters,
298  message_handlert &message_handler)
299 {
300  // The intent here is to apply stub_generator.check_method_stub() to
301  // all the identifiers in the symbol table. However this method may alter the
302  // symbol table and iterating over a container which is being modified has
303  // undefined behaviour. Therefore in order for this to work reliably, we must
304  // take a copy of the identifiers in the symbol table and iterate over that,
305  // instead of iterating over the symbol table itself.
306  std::vector<irep_idt> identifiers;
307  identifiers.reserve(symbol_table.symbols.size());
308  for(const auto &symbol : symbol_table)
309  identifiers.push_back(symbol.first);
310 
311  java_simple_method_stubst stub_generator(
312  symbol_table, assume_non_null, object_factory_parameters, message_handler);
313 
314  for(const auto &identifier : identifiers)
315  {
316  stub_generator.check_method_stub(identifier);
317  }
318 }
java_simple_method_stubst::assume_non_null
bool assume_non_null
Definition: simple_method_stubbing.cpp:54
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
java_simple_method_stubst
Definition: simple_method_stubbing.cpp:24
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
typet::subtype
const typet & subtype() const
Definition: type.h:47
java_simple_method_stubst::message_handler
message_handlert & message_handler
Definition: simple_method_stubbing.cpp:56
source_locationt::set_function
void set_function(const irep_idt &function)
Definition: source_location.h:126
lifetimet::AUTOMATIC_LOCAL
@ AUTOMATIC_LOCAL
Allocate local objects with automatic lifetime.
typet
The type of an expression, extends irept.
Definition: type.h:29
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
object_factory_parameterst::function_id
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
Definition: object_factory_parameters.h:82
java_generate_simple_method_stubs
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...
Definition: simple_method_stubbing.cpp:294
java_simple_method_stubst::check_method_stub
void check_method_stub(const irep_idt &)
Replaces sym with a function stub per the function above if it is of suitable type.
Definition: simple_method_stubbing.cpp:253
exprt
Base class for all expressions.
Definition: expr.h:53
make_clean_pointer_cast
exprt make_clean_pointer_cast(const exprt &rawptr, const pointer_typet &target_type, const namespacet &ns)
Definition: java_pointer_casts.cpp:86
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
namespace.h
simple_method_stubbing.h
Java simple opaque stub generation.
code_typet::get_is_constructor
bool get_is_constructor() const
Definition: std_types.h:887
java_simple_method_stubst::java_simple_method_stubst
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)
Definition: simple_method_stubbing.cpp:26
update_in_placet::MUST_UPDATE_IN_PLACE
@ MUST_UPDATE_IN_PLACE
code_blockt::statements
code_operandst & statements()
Definition: std_code.h:178
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
java_pointer_casts.h
JAVA Pointer Casts.
java_simple_method_stubst::create_method_stub_at
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...
Definition: simple_method_stubbing.cpp:79
java_object_factory.h
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
symbol_table_baset::get_writeable_ref
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
Definition: symbol_table_base.h:121
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
java_simple_method_stubst::create_method_stub
void create_method_stub(symbolt &symbol)
Replaces sym's value with an opaque method stub.
Definition: simple_method_stubbing.cpp:148
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
gen_nondet_init
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...
Definition: java_object_factory.cpp:1624
symbolt::is_parameter
bool is_parameter
Definition: symbol.h:67
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:28
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
std_code.h
fresh_java_symbol
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)
Definition: java_utils.cpp:566
object_factory_parameterst::min_null_tree_depth
size_t min_null_tree_depth
To force a certain depth of non-null objects.
Definition: object_factory_parameters.h:73
source_locationt
Definition: source_location.h:20
invariant_utils.h
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
java_generate_simple_method_stub
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)
Definition: simple_method_stubbing.cpp:272
java_simple_method_stubst::symbol_table
symbol_table_baset & symbol_table
Definition: simple_method_stubbing.cpp:53
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1310
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
symbolt
Symbol table entry.
Definition: symbol.h:28
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
symbolt::is_type
bool is_type
Definition: symbol.h:61
update_in_placet::NO_UPDATE_IN_PLACE
@ NO_UPDATE_IN_PLACE
lifetimet::DYNAMIC
@ DYNAMIC
Allocate dynamic objects (using ALLOCATE)
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
to_java_method_type
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:186
java_void_type
empty_typet java_void_type()
Definition: java_types.cpp:38
is_constructor
static bool is_constructor(const irep_idt &method_name)
Definition: java_bytecode_convert_method.cpp:128
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
java_utils.h
std_expr.h
API to expression classes.
java_method_typet
Definition: java_types.h:103
java_object_factory_parameterst
Definition: java_object_factory_parameters.h:16
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
java_simple_method_stubst::object_factory_parameters
const java_object_factory_parameterst & object_factory_parameters
Definition: simple_method_stubbing.cpp:55
INVARIANT_WITH_IREP
#define INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP)
Equivalent to INVARIANT_STRUCTURED(CONDITION, invariant_failedt, pretty_print_invariant_with_irep(IRE...
Definition: invariant_utils.h:29