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 
18 
19 #include "java_utils.h"
20 #include <util/invariant_utils.h>
21 #include <util/namespace.h>
22 #include <util/std_code.h>
23 #include <util/symbol_table_base.h>
24 
26 {
27 public:
29  symbol_table_baset &_symbol_table,
30  bool _assume_non_null,
31  const java_object_factory_parameterst &_object_factory_parameters,
32  message_handlert &_message_handler)
33  : symbol_table(_symbol_table),
34  assume_non_null(_assume_non_null),
35  object_factory_parameters(_object_factory_parameters),
36  message_handler(_message_handler)
37  {
38  }
39 
41  const typet &expected_type,
42  const exprt &ptr,
43  const source_locationt &loc,
44  const irep_idt &function_id,
45  code_blockt &parent_block,
46  unsigned insert_before_index,
47  bool is_constructor,
48  bool update_in_place);
49 
50  void create_method_stub(symbolt &symbol);
51 
52  void check_method_stub(const irep_idt &);
53 
54 protected:
59 };
60 
82  const typet &expected_type,
83  const exprt &ptr,
84  const source_locationt &loc,
85  const irep_idt &function_id,
86  code_blockt &parent_block,
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 
96  expected_type.id() == ID_pointer,
97  "Nondet initializer result type: expected a pointer",
98  expected_type);
99 
101 
102  const auto &expected_base = ns.follow(expected_type.subtype());
103  if(expected_base.id() != ID_struct)
104  return;
105 
106  const exprt cast_ptr =
107  make_clean_pointer_cast(ptr, to_pointer_type(expected_type), ns);
108 
109  exprt to_init = cast_ptr;
110  // If it's a constructor the thing we're constructing has already
111  // been allocated by this point.
112  if(is_constructor)
113  to_init = dereference_exprt(to_init);
114 
116  if(assume_non_null)
117  parameters.min_null_tree_depth = 1;
118 
119  // Generate new instructions.
120  code_blockt new_instructions;
121  parameters.function_id = function_id;
123  to_init,
124  new_instructions,
125  symbol_table,
126  loc,
129  parameters,
133 
134  // Insert new_instructions into parent block.
135  if(!new_instructions.statements().empty())
136  {
137  auto insert_position = parent_block.statements().begin();
138  std::advance(insert_position, insert_before_index);
139  parent_block.statements().insert(
140  insert_position,
141  new_instructions.statements().begin(),
142  new_instructions.statements().end());
143  }
144 }
145 
151 {
152  code_blockt new_instructions;
153  java_method_typet &required_type = to_java_method_type(symbol.type);
154 
155  // synthetic source location that contains the opaque function name only
156  source_locationt synthesized_source_location;
157  synthesized_source_location.set_function(symbol.name);
158 
159  // make sure all parameters are named
160  for(auto &parameter : required_type.parameters())
161  {
162  if(parameter.get_identifier().empty())
163  {
164  symbolt &parameter_symbol = fresh_java_symbol(
165  parameter.type(),
166  "#anon",
167  synthesized_source_location,
168  symbol.name,
169  symbol_table);
170  parameter_symbol.is_parameter = true;
171  parameter.set_base_name(parameter_symbol.base_name);
172  parameter.set_identifier(parameter_symbol.name);
173  }
174  }
175 
176  // Initialize the return value or `this` parameter under construction.
177  // Note symbol.type is required_type, but with write access
178  // Probably required_type should not be const
179  const bool is_constructor = required_type.get_is_constructor();
180  if(is_constructor)
181  {
182  const auto &this_argument = required_type.parameters()[0];
183  const typet &this_type = this_argument.type();
185  this_type,
186  "to_construct",
187  synthesized_source_location,
188  symbol.name,
189  symbol_table);
190  const symbol_exprt &init_symbol_expression = init_symbol.symbol_expr();
191  code_assignt get_argument(
192  init_symbol_expression,
193  symbol_exprt(this_argument.get_identifier(), this_type));
194  get_argument.add_source_location() = synthesized_source_location;
195  new_instructions.add(get_argument);
197  this_type,
198  init_symbol_expression,
199  synthesized_source_location,
200  symbol.name,
201  new_instructions,
202  1,
203  true,
204  false);
205  }
206  else
207  {
208  const typet &required_return_type = required_type.return_type();
209  if(required_return_type != java_void_type())
210  {
211  symbolt &to_return_symbol = fresh_java_symbol(
212  required_return_type,
213  "to_return",
214  synthesized_source_location,
215  symbol.name,
216  symbol_table);
217  const exprt &to_return = to_return_symbol.symbol_expr();
218  if(to_return_symbol.type.id() != ID_pointer)
219  {
221  if(assume_non_null)
222  parameters.min_null_tree_depth = 1;
223 
225  to_return,
226  new_instructions,
227  symbol_table,
229  false,
230  lifetimet::AUTOMATIC_LOCAL, // Irrelevant as type is primitive
231  parameters,
234  }
235  else
237  required_return_type,
238  to_return,
239  synthesized_source_location,
240  symbol.name,
241  new_instructions,
242  0,
243  false,
244  false);
245  new_instructions.add(code_returnt(to_return));
246  }
247  }
248 
249  symbol.value = new_instructions;
250 }
251 
256 {
257  const symbolt &sym = symbol_table.lookup_ref(symname);
258  if(!sym.is_type && sym.value.id() == ID_nil &&
259  sym.type.id() == ID_code &&
260  // do not stub internal locking calls as 'create_method_stub' does not
261  // automatically create the appropriate symbols for the formal parameters.
262  // This means that symex will (rightfully) crash when it encounters the
263  // function call as it will not be able to find symbols for the fromal
264  // parameters.
265  sym.name !=
266  "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" &&
267  sym.name !=
268  "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V")
269  {
271  }
272 }
273 
275  const irep_idt &function_name,
276  symbol_table_baset &symbol_table,
277  bool assume_non_null,
278  const java_object_factory_parameterst &object_factory_parameters,
279  message_handlert &message_handler)
280 {
281  java_simple_method_stubst stub_generator(
282  symbol_table, assume_non_null, object_factory_parameters, message_handler);
283 
284  stub_generator.check_method_stub(function_name);
285 }
286 
297  symbol_table_baset &symbol_table,
298  bool assume_non_null,
299  const java_object_factory_parameterst &object_factory_parameters,
300  message_handlert &message_handler)
301 {
302  // The intent here is to apply stub_generator.check_method_stub() to
303  // all the identifiers in the symbol table. However this method may alter the
304  // symbol table and iterating over a container which is being modified has
305  // undefined behaviour. Therefore in order for this to work reliably, we must
306  // take a copy of the identifiers in the symbol table and iterate over that,
307  // instead of iterating over the symbol table itself.
308  std::vector<irep_idt> identifiers;
309  identifiers.reserve(symbol_table.symbols.size());
310  for(const auto &symbol : symbol_table)
311  identifiers.push_back(symbol.first);
312 
313  java_simple_method_stubst stub_generator(
314  symbol_table, assume_non_null, object_factory_parameters, message_handler);
315 
316  for(const auto &identifier : identifiers)
317  {
318  stub_generator.check_method_stub(identifier);
319  }
320 }
@ DYNAMIC
Allocate dynamic objects (using ALLOCATE)
@ AUTOMATIC_LOCAL
Allocate local objects with automatic lifetime.
A codet representing an assignment in the program.
A codet representing sequential composition of program statements.
Definition: std_code.h:130
void add(const codet &code)
Definition: std_code.h:168
code_operandst & statements()
Definition: std_code.h:138
codet representation of a "return from a function" statement.
const typet & return_type() const
Definition: std_types.h:645
bool get_is_constructor() const
Definition: std_types.h:685
const parameterst & parameters() const
Definition: std_types.h:655
Operator to dereference a pointer.
Definition: pointer_expr.h:648
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
source_locationt & add_source_location()
Definition: expr.h:235
const irep_idt & id() const
Definition: irep.h:396
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
void set_function(const irep_idt &function)
Expression to hold a symbol (variable)
Definition: std_expr.h:80
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
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_parameter
Definition: symbol.h:67
bool is_type
Definition: symbol.h:61
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
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
const typet & subtype() const
Definition: type.h:48
#define INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP)
Equivalent to INVARIANT_STRUCTURED(CONDITION, invariant_failedt, pretty_print_invariant_with_irep(IRE...
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()
Definition: java_types.cpp:37
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)
Definition: java_utils.cpp:558
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
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.