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 <util/fresh_symbol.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 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 
78  const typet &expected_type,
79  const exprt &ptr,
80  const source_locationt &loc,
81  const irep_idt &function_id,
82  code_blockt &parent_block,
83  const unsigned insert_before_index,
84  const bool is_constructor,
85  const bool update_in_place)
86 {
87  // At this point we know 'ptr' points to an opaque-typed object.
88  // We should nondet-initialize it and insert the instructions *after*
89  // the offending call at (*parent_block)[insert_before_index].
90 
92  expected_type.id() == ID_pointer,
93  "Nondet initializer result type: expected a pointer",
94  expected_type);
95 
97 
98  const auto &expected_base = ns.follow(expected_type.subtype());
99  if(expected_base.id() != ID_struct)
100  return;
101 
102  const exprt cast_ptr =
103  make_clean_pointer_cast(ptr, to_pointer_type(expected_type), ns);
104 
105  exprt to_init = cast_ptr;
106  // If it's a constructor the thing we're constructing has already
107  // been allocated by this point.
108  if(is_constructor)
109  to_init = dereference_exprt(to_init, expected_base);
110 
112  if(assume_non_null)
113  parameters.max_nonnull_tree_depth = 1;
114 
115  // Generate new instructions.
116  code_blockt new_instructions;
117  parameters.function_id = function_id;
119  to_init,
120  new_instructions,
121  symbol_table,
122  loc,
125  parameters,
128 
129  // Insert new_instructions into parent block.
130  if(!new_instructions.operands().empty())
131  {
132  auto insert_position = parent_block.operands().begin();
133  std::advance(insert_position, insert_before_index);
134  parent_block.operands().insert(
135  insert_position,
136  new_instructions.operands().begin(),
137  new_instructions.operands().end());
138  }
139 }
140 
146 {
147  code_blockt new_instructions;
148  const java_method_typet &required_type = to_java_method_type(symbol.type);
149 
150  // synthetic source location that contains the opaque function name only
151  source_locationt synthesized_source_location;
152  synthesized_source_location.set_function(symbol.name);
153 
154  // Initialize the return value or `this` parameter under construction.
155  // Note symbol.type is required_type, but with write access
156  // Probably required_type should not be const
157  const bool is_constructor = required_type.get_is_constructor();
158  if(is_constructor)
159  {
160  const auto &this_argument = required_type.parameters()[0];
161  const typet &this_type = this_argument.type();
162  symbolt &init_symbol = get_fresh_aux_symbol(
163  this_type,
164  id2string(symbol.name),
165  "to_construct",
166  synthesized_source_location,
167  ID_java,
168  symbol_table);
169  const symbol_exprt &init_symbol_expression = init_symbol.symbol_expr();
170  code_assignt get_argument(
171  init_symbol_expression, symbol_exprt(this_argument.get_identifier()));
172  get_argument.add_source_location() = synthesized_source_location;
173  new_instructions.copy_to_operands(get_argument);
175  this_type,
176  init_symbol_expression,
177  synthesized_source_location,
178  symbol.name,
179  new_instructions,
180  1,
181  true,
182  false);
183  }
184  else
185  {
186  const typet &required_return_type = required_type.return_type();
187  if(required_return_type != empty_typet())
188  {
189  symbolt &to_return_symbol = get_fresh_aux_symbol(
190  required_return_type,
191  id2string(symbol.name),
192  "to_return",
193  synthesized_source_location,
194  ID_java,
195  symbol_table);
196  const exprt &to_return = to_return_symbol.symbol_expr();
197  if(to_return_symbol.type.id() != ID_pointer)
198  {
200  if(assume_non_null)
201  parameters.max_nonnull_tree_depth = 1;
202 
204  to_return,
205  new_instructions,
206  symbol_table,
208  false,
209  allocation_typet::LOCAL, // Irrelevant as type is primitive
210  parameters,
212  }
213  else
215  required_return_type,
216  to_return,
217  synthesized_source_location,
218  symbol.name,
219  new_instructions,
220  0,
221  false,
222  false);
223  new_instructions.copy_to_operands(code_returnt(to_return));
224  }
225  }
226 
227  symbol.value = new_instructions;
228 }
229 
234 {
235  const symbolt &sym = *symbol_table.lookup(symname);
236  if(!sym.is_type && sym.value.id() == ID_nil &&
237  sym.type.id() == ID_code &&
238  // do not stub internal locking calls as 'create_method_stub' does not
239  // automatically create the appropriate symbols for the formal parameters.
240  // This means that symex will (rightfully) crash when it encounters the
241  // function call as it will not be able to find symbols for the fromal
242  // parameters.
243  sym.name !=
244  "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" &&
245  sym.name !=
246  "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V")
247  {
249  }
250 }
251 
253  const irep_idt &function_name,
254  symbol_table_baset &symbol_table,
255  bool assume_non_null,
256  const object_factory_parameterst &object_factory_parameters,
258 {
259  java_simple_method_stubst stub_generator(
260  symbol_table, assume_non_null, object_factory_parameters, message_handler);
261 
262  stub_generator.check_method_stub(function_name);
263 }
264 
275  symbol_table_baset &symbol_table,
276  bool assume_non_null,
277  const object_factory_parameterst &object_factory_parameters,
279 {
280  // The intent here is to apply stub_generator.check_method_stub() to
281  // all the identifiers in the symbol table. However this method may alter the
282  // symbol table and iterating over a container which is being modified has
283  // undefined behaviour. Therefore in order for this to work reliably, we must
284  // take a copy of the identifiers in the symbol table and iterate over that,
285  // instead of iterating over the symbol table itself.
286  std::vector<irep_idt> identifiers;
287  identifiers.reserve(symbol_table.symbols.size());
288  for(const auto &symbol : symbol_table)
289  identifiers.push_back(symbol.first);
290 
291  java_simple_method_stubst stub_generator(
292  symbol_table, assume_non_null, object_factory_parameters, message_handler);
293 
294  for(const auto &identifier : identifiers)
295  {
296  stub_generator.check_method_stub(identifier);
297  }
298 }
#define loc()
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
void set_function(const irep_idt &function)
void create_method_stub(symbolt &symbol)
Replaces sym&#39;s value with an opaque method stub.
static bool is_constructor(const irep_idt &method_name)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
java_simple_method_stubst(symbol_table_baset &_symbol_table, bool _assume_non_null, const object_factory_parameterst &_object_factory_parameters, message_handlert &_message_handler)
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
Fresh auxiliary symbol creation.
Allocate local stacked objects.
Java simple opaque stub generation.
exprt value
Initial value of symbol.
Definition: symbol.h:37
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 java_generate_simple_method_stub(const irep_idt &function_name, symbol_table_baset &symbol_table, bool assume_non_null, const object_factory_parameterst &object_factory_parameters, message_handlert &message_handler)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
bool get_is_constructor() const
Definition: std_types.h:935
#define INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP)
Equivalent to INVARIANT_STRUCTURED(CONDITION, invariant_failedt, pretty_print_invariant_with_irep(IRE...
const irep_idt & id() const
Definition: irep.h:259
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
The empty type.
Definition: std_types.h:54
Operator to dereference a pointer.
Definition: std_expr.h:3282
API to expression classes.
TO_BE_DOCUMENTED.
Definition: namespace.h:74
const object_factory_parameterst & object_factory_parameters
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
const symbolst & symbols
typet type
Type of symbol.
Definition: symbol.h:34
Allocate dynamic objects (using MALLOC)
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:289
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
Base class for all expressions.
Definition: expr.h:42
const parameterst & parameters() const
Definition: std_types.h:905
The symbol table base class interface.
void java_generate_simple_method_stubs(symbol_table_baset &symbol_table, bool assume_non_null, const 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...
void gen_nondet_init(const exprt &expr, code_blockt &init_code, symbol_table_baset &symbol_table, const source_locationt &loc, bool skip_classid, allocation_typet alloc_type, const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place)
Initializes a primitive-typed or reference-typed object tree rooted at expr, allocating child objects...
JAVA Pointer Casts.
source_locationt & add_source_location()
Definition: expr.h:130
Sequential composition.
Definition: std_code.h:89
Expression to hold a symbol (variable)
Definition: std_expr.h:90
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1459
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
Return from a function.
Definition: std_code.h:923
bool is_type
Definition: symbol.h:63
const typet & subtype() const
Definition: type.h:33
operandst & operands()
Definition: expr.h:66
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const typet & return_type() const
Definition: std_types.h:895
Assignment.
Definition: std_code.h:196
void check_method_stub(const irep_idt &)
Replaces sym with a function stub per the function above if it is of suitable type.
exprt make_clean_pointer_cast(const exprt &rawptr, const pointer_typet &target_type, const namespacet &ns)
size_t max_nonnull_tree_depth
To force a certain depth of non-null objects.