cprover
require_goto_statements.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: Unit test utilities
4 
5  Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
10 
11 #include <testing-utils/catch.hpp>
12 
13 #include <algorithm>
14 #include <util/expr_iterator.h>
17 #include <util/suffix.h>
18 
23 std::vector<codet>
25 {
26  std::vector<codet> statements;
27  for(auto sub_expression_it = function_value.depth_begin();
28  sub_expression_it != function_value.depth_end();
29  ++sub_expression_it)
30  {
31  if(sub_expression_it->id() == ID_code)
32  {
33  statements.push_back(to_code(*sub_expression_it));
34  }
35  }
36 
37  return statements;
38 }
39 
42 const std::vector<codet>
44  const symbol_tablet &symbol_table)
45 {
46  // Retrieve __CPROVER_start
47  const symbolt *entry_point_function =
48  symbol_table.lookup(goto_functionst::entry_point());
49  REQUIRE(entry_point_function != nullptr);
50  return get_all_statements(entry_point_function->value);
51 }
52 
67  const std::vector<codet> &statements,
68  const irep_idt &structure_name,
69  const optionalt<irep_idt> &superclass_name,
70  const irep_idt &component_name,
71  const symbol_tablet &symbol_table)
72 {
74 
75  for(const auto &assignment : statements)
76  {
77  if(assignment.get_statement() == ID_assign)
78  {
79  const code_assignt &code_assign = to_code_assign(assignment);
80 
81  if(code_assign.lhs().id() == ID_member)
82  {
83  const member_exprt &member_expr = to_member_expr(code_assign.lhs());
84 
85  if(superclass_name.has_value())
86  {
87  // Structure of the expression:
88  // member_exprt member_expr:
89  // - component name: \p component_name
90  // - operand (component of): member_exprt superclass_expr:
91  // - component name: @\p superclass_name
92  // - operand (component of): symbol for \p structure_name
93  if(
94  member_expr.get_component_name() == component_name &&
95  member_expr.compound().id() == ID_member)
96  {
97  const member_exprt &superclass_expr =
98  to_member_expr(member_expr.op0());
99  const irep_idt supercomponent_name =
100  "@" + id2string(superclass_name.value());
101 
103  const namespacet ns(symbol_table);
104  ode.build(superclass_expr, ns);
105  if(
106  superclass_expr.get_component_name() == supercomponent_name &&
108  structure_name)
109  {
110  if(
111  code_assign.rhs() ==
112  null_pointer_exprt(to_pointer_type(code_assign.lhs().type())))
113  {
114  locations.null_assignment = code_assign;
115  }
116  else
117  {
118  locations.non_null_assignments.push_back(code_assign);
119  }
120  }
121  }
122  }
123  else
124  {
125  // Structure of the expression:
126  // member_exprt member_expr:
127  // - component name: \p component_name
128  // - operand (component of): symbol for \p structure_name
129  if(
130  member_expr.op().id() == ID_symbol &&
131  to_symbol_expr(member_expr.op()).get_identifier() == structure_name &&
132  member_expr.get_component_name() == component_name)
133  {
134  if(
135  code_assign.rhs() ==
136  null_pointer_exprt(to_pointer_type(code_assign.lhs().type())))
137  {
138  locations.null_assignment = code_assign;
139  }
140  else
141  {
142  locations.non_null_assignments.push_back(code_assign);
143  }
144  }
145  }
146  }
147  }
148  }
149  return locations;
150 }
151 
160  const std::vector<codet> &statements,
161  const irep_idt &component_name)
162 {
164 
165  for(const auto &assignment : statements)
166  {
167  if(assignment.get_statement() == ID_assign)
168  {
169  const code_assignt &code_assign = to_code_assign(assignment);
170 
171  if(code_assign.lhs().id() == ID_member)
172  {
173  const member_exprt &member_expr = to_member_expr(code_assign.lhs());
174  if(
175  member_expr.get_component_name() == component_name &&
176  member_expr.op().id() == ID_dereference &&
177  member_expr.op().op0().id() == ID_symbol &&
178  has_suffix(
179  id2string(to_symbol_expr(member_expr.op().op0()).get_identifier()),
180  "this"))
181  {
182  if(
183  code_assign.rhs() ==
184  null_pointer_exprt(to_pointer_type(code_assign.lhs().type())))
185  {
186  locations.null_assignment = code_assign;
187  }
188  else
189  {
190  locations.non_null_assignments.push_back(code_assign);
191  }
192  }
193  }
194  }
195  }
196  return locations;
197 }
198 
207  const irep_idt &pointer_name,
208  const std::vector<codet> &instructions)
209 {
210  INFO("Looking for symbol: " << pointer_name);
211  std::regex special_chars{R"([-[\]{}()*+?.,\^$|#\s])"};
212  std::string sanitized =
213  std::regex_replace(id2string(pointer_name), special_chars, R"(\$&)");
215  std::regex("^" + sanitized + "$"), instructions);
216 }
217 
220  const std::regex &pointer_name_match,
221  const std::vector<codet> &instructions)
222 {
224  bool found_assignment = false;
225  std::vector<irep_idt> all_symbols;
226  for(const codet &statement : instructions)
227  {
228  if(statement.get_statement() == ID_assign)
229  {
230  const code_assignt &code_assign = to_code_assign(statement);
231  if(code_assign.lhs().id() == ID_symbol)
232  {
233  const symbol_exprt &symbol_expr = to_symbol_expr(code_assign.lhs());
234  all_symbols.push_back(symbol_expr.get_identifier());
235  if(
236  std::regex_search(
237  id2string(symbol_expr.get_identifier()), pointer_name_match))
238  {
239  if(
240  code_assign.rhs() ==
241  null_pointer_exprt(to_pointer_type(code_assign.lhs().type())))
242  {
243  locations.null_assignment = code_assign;
244  }
245  else
246  {
247  locations.non_null_assignments.push_back(code_assign);
248  }
249  found_assignment = true;
250  }
251  }
252  }
253  }
254 
255  std::ostringstream found_symbols;
256  for(const auto entry : all_symbols)
257  {
258  found_symbols << entry << std::endl;
259  }
260  INFO("Symbols: " << found_symbols.str());
261  REQUIRE(found_assignment);
262 
263  return locations;
264 }
265 
273  const irep_idt &variable_name,
274  const std::vector<codet> &entry_point_instructions)
275 {
276  for(const auto &statement : entry_point_instructions)
277  {
278  if(statement.get_statement() == ID_decl)
279  {
280  const auto &decl_statement = to_code_decl(statement);
281 
282  if(decl_statement.get_identifier() == variable_name)
283  {
284  return decl_statement;
285  }
286  }
287  }
288  throw no_decl_found_exceptiont(variable_name.c_str());
289 }
290 
303  const irep_idt &structure_name,
304  const optionalt<irep_idt> &superclass_name,
305  const irep_idt &component_name,
306  const irep_idt &component_type_name,
307  const optionalt<irep_idt> &typecast_name,
308  const std::vector<codet> &entry_point_instructions,
309  const symbol_tablet &symbol_table)
310 {
311  // First we need to find the assignments to the component belonging to
312  // the structure_name object
313  const auto &component_assignments =
315  entry_point_instructions,
316  structure_name,
317  superclass_name,
318  component_name,
319  symbol_table);
320  REQUIRE(component_assignments.non_null_assignments.size() == 1);
321 
322  // We are expecting that the resulting statement can be of two forms:
323  // 1. structure_name.(@superclass_name if given).component =
324  // (struct cast_type_name *) tmp_object_factory$1;
325  // followed by a direct assignment like this:
326  // tmp_object_factory$1 = &tmp_object_factory$2;
327  // 2. structure_name.component = &tmp_object_factory$1;
328  exprt component_assignment_rhs_expr =
329  component_assignments.non_null_assignments[0].rhs();
330 
331  // If the rhs is a typecast (case 1 above), deconstruct it to get the name of
332  // the variable and find the assignment to it
333  if(component_assignment_rhs_expr.id() == ID_typecast)
334  {
335  const auto &component_assignment_rhs =
336  to_typecast_expr(component_assignment_rhs_expr);
337 
338  // Check the type we are casting to
339  if(typecast_name.has_value())
340  {
341  REQUIRE(component_assignment_rhs.type().id() == ID_pointer);
342  REQUIRE(
344  to_pointer_type(component_assignment_rhs.type()).subtype())
345  .get(ID_identifier) == typecast_name.value());
346  }
347 
348  const auto &component_reference_tmp_name =
349  to_symbol_expr(component_assignment_rhs.op()).get_identifier();
350  const auto &component_reference_assignments =
352  component_reference_tmp_name, entry_point_instructions)
354  REQUIRE(component_reference_assignments.size() == 1);
355  component_assignment_rhs_expr = component_reference_assignments[0].rhs();
356  }
357 
358  // The rhs assigns an address of a variable, get its name
359  const auto &component_reference_assignment_rhs =
360  to_address_of_expr(component_assignment_rhs_expr);
361  const auto &component_tmp_name =
362  to_symbol_expr(component_reference_assignment_rhs.op()).get_identifier();
363 
364  // After we have found the declaration of the final assignment's
365  // right hand side, then we want to identify that the type
366  // is the one we expect, e.g.:
367  // struct java.lang.Integer { __CPROVER_string @class_identifier; }
368  // tmp_object_factory$2;
369  const auto &component_declaration =
371  component_tmp_name, entry_point_instructions);
372  REQUIRE(component_declaration.symbol().type().id() == ID_struct);
373  const auto &component_struct =
374  to_struct_type(component_declaration.symbol().type());
375  REQUIRE(component_struct.get(ID_name) == component_type_name);
376 
377  return component_tmp_name;
378 }
379 
389 const irep_idt &
391  const irep_idt &structure_name,
392  const optionalt<irep_idt> &superclass_name,
393  const irep_idt &array_component_name,
394  const irep_idt &array_type_name,
395  const std::vector<codet> &entry_point_instructions,
396  const symbol_tablet &symbol_table)
397 {
398  // First we need to find the assignments to the component belonging to
399  // the structure_name object
400  const auto &component_assignments =
402  entry_point_instructions,
403  structure_name,
404  superclass_name,
405  array_component_name,
406  symbol_table);
407  REQUIRE(component_assignments.non_null_assignments.size() == 1);
408 
409  // We are expecting that the resulting statement is of form:
410  // structure_name.array_component_name = (struct array_type_name *)
411  // tmp_object_factory$1;
412  const exprt &component_assignment_rhs_expr =
413  component_assignments.non_null_assignments[0].rhs();
414 
415  // The rhs is a typecast, deconstruct it to get the name of the variable
416  // and find the assignment to it
417  PRECONDITION(component_assignment_rhs_expr.id() == ID_typecast);
418  const auto &component_assignment_rhs =
419  to_typecast_expr(component_assignment_rhs_expr);
420  const auto &component_reference_tmp_name =
421  to_symbol_expr(component_assignment_rhs.op()).get_identifier();
422 
423  // Check the type we are casting to matches the array type
424  REQUIRE(component_assignment_rhs.type().id() == ID_pointer);
425  REQUIRE(
427  to_pointer_type(component_assignment_rhs.type()).subtype())
428  .get(ID_identifier) == array_type_name);
429 
430  // Get the tmp_object name and find assignments to it, there should be only
431  // one that assigns the correct array through side effect
432  const auto &component_reference_assignments =
434  component_reference_tmp_name, entry_point_instructions);
435  REQUIRE(component_reference_assignments.non_null_assignments.size() == 1);
436  const exprt &component_reference_assignment_rhs_expr =
437  component_reference_assignments.non_null_assignments[0].rhs();
438 
439  // The rhs is side effect
440  PRECONDITION(component_reference_assignment_rhs_expr.id() == ID_side_effect);
441  const auto &array_component_reference_assignment_rhs =
442  to_side_effect_expr(component_reference_assignment_rhs_expr);
443 
444  // The type of the side effect is an array with the correct element type
445  PRECONDITION(
446  array_component_reference_assignment_rhs.type().id() == ID_pointer);
447  const typet &array =
448  to_pointer_type(array_component_reference_assignment_rhs.type()).subtype();
449  PRECONDITION(is_java_array_tag(array.get(ID_identifier)));
450  REQUIRE(array.get(ID_identifier) == array_type_name);
451 
452  return component_reference_tmp_name;
453 }
454 
460 const irep_idt &
462  const irep_idt &argument_name,
463  const std::vector<codet> &entry_point_statements)
464 {
465  // Trace the creation of the object that is being supplied as the input
466  // argument to the function under test
467  const pointer_assignment_locationt &argument_assignments =
470  id2string(argument_name),
471  entry_point_statements);
472 
473  // There should be at most one assignment to it
474  REQUIRE(argument_assignments.non_null_assignments.size() == 1);
475 
476  // The following finds the name of the tmp object that gets assigned
477  // to the input argument. There must be one such assignment only,
478  // and usually looks like this:
479  // argument_name = &tmp_object_factory$1;
480  const auto &argument_assignment =
481  argument_assignments.non_null_assignments[0];
482  const auto &argument_tmp_name =
483  to_symbol_expr(to_address_of_expr(argument_assignment.rhs()).object())
484  .get_identifier();
485  return argument_tmp_name;
486 }
487 
494 std::vector<code_function_callt> require_goto_statements::find_function_calls(
495  const std::vector<codet> &statements,
496  const irep_idt &function_call_identifier)
497 {
498  std::vector<code_function_callt> function_calls;
499  for(const codet &statement : statements)
500  {
501  if(statement.get_statement() == ID_function_call)
502  {
503  const code_function_callt &function_call =
504  to_code_function_call(statement);
505 
506  if(function_call.function().id() == ID_symbol)
507  {
508  if(
509  to_symbol_expr(function_call.function()).get_identifier() ==
510  function_call_identifier)
511  {
512  function_calls.push_back(function_call);
513  }
514  }
515  }
516  }
517  return function_calls;
518 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
dstringt::c_str
const char * c_str() const
Definition: dstring.h:86
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
typet::subtype
const typet & subtype() const
Definition: type.h:38
exprt::depth_end
depth_iteratort depth_end()
Definition: expr.cpp:284
object_descriptor_exprt::build
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
Definition: std_expr.cpp:123
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
to_code_decl
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:399
address_of_exprt::object
exprt & object()
Definition: std_expr.h:3265
require_goto_statements::require_entry_point_statements
const std::vector< codet > require_entry_point_statements(const symbol_tablet &symbol_table)
Definition: require_goto_statements.cpp:43
require_goto_statements::find_this_component_assignment
pointer_assignment_locationt find_this_component_assignment(const std::vector< codet > &statements, const irep_idt &component_name)
Find assignment statements that set this->{component_name}.
Definition: require_goto_statements.cpp:159
typet
The type of an expression, extends irept.
Definition: type.h:27
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:274
object_descriptor_exprt
Split an expression into a base object and a (byte) offset.
Definition: std_expr.h:2136
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:352
require_goto_statements::pointer_assignment_locationt::non_null_assignments
std::vector< code_assignt > non_null_assignments
Definition: require_goto_statements.h:30
exprt
Base class for all expressions.
Definition: expr.h:54
is_java_array_tag
bool is_java_array_tag(const irep_idt &tag)
See above.
Definition: java_types.cpp:173
exprt::op0
exprt & op0()
Definition: expr.h:84
require_goto_statements::require_declaration_of_name
const code_declt & require_declaration_of_name(const irep_idt &variable_name, const std::vector< codet > &entry_point_instructions)
Find the declaration of the specific variable.
Definition: require_goto_statements.cpp:272
to_side_effect_expr
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1620
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
has_suffix
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:15
require_goto_statements::get_all_statements
std::vector< codet > get_all_statements(const exprt &function_value)
Expand value of a function to include all child codets.
Definition: require_goto_statements.cpp:24
require_goto_statements::require_entry_point_argument_assignment
const irep_idt & require_entry_point_argument_assignment(const irep_idt &argument_name, const std::vector< codet > &entry_point_statements)
Checks that the input argument (of method under test) with given name is assigned a single non-null o...
Definition: require_goto_statements.cpp:461
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:136
require_goto_statements::find_function_calls
std::vector< code_function_callt > find_function_calls(const std::vector< codet > &statements, const irep_idt &function_call_identifier)
Verify that a collection of statements contains a function call to a function whose symbol identifier...
Definition: require_goto_statements.cpp:494
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1036
require_goto_statements::pointer_assignment_locationt
Definition: require_goto_statements.h:27
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:4471
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:3282
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
member_exprt::compound
const exprt & compound() const
Definition: std_expr.h:3942
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:269
require_goto_statements.h
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
irept::id
const irep_idt & id() const
Definition: irep.h:259
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:543
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:371
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
object_descriptor_exprt::root_object
const exprt & root_object() const
Definition: std_expr.cpp:199
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
require_goto_statements::pointer_assignment_locationt::null_assignment
optionalt< code_assignt > null_assignment
Definition: require_goto_statements.h:29
require_goto_statements::find_pointer_assignments
pointer_assignment_locationt find_pointer_assignments(const irep_idt &pointer_name, const std::vector< codet > &instructions)
For a given variable name, gets the assignments to it in the provided instructions.
Definition: require_goto_statements.cpp:206
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3890
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
require_goto_statements::require_struct_component_assignment
const irep_idt & require_struct_component_assignment(const irep_idt &structure_name, const optionalt< irep_idt > &superclass_name, const irep_idt &component_name, const irep_idt &component_type_name, const optionalt< irep_idt > &typecast_name, const std::vector< codet > &entry_point_instructions, const symbol_tablet &symbol_table)
Checks that the component of the structure (possibly inherited from the superclass) is assigned an ob...
Definition: require_goto_statements.cpp:302
expr_iterator.h
suffix.h
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
exprt::depth_begin
depth_iteratort depth_begin()
Definition: expr.cpp:282
require_goto_statements::no_decl_found_exceptiont
Definition: require_goto_statements.h:33
symbolt
Symbol table entry.
Definition: symbol.h:27
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2306
goto_functions.h
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:86
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:3915
require_goto_statements::require_struct_array_component_assignment
const irep_idt & require_struct_array_component_assignment(const irep_idt &structure_name, const optionalt< irep_idt > &superclass_name, const irep_idt &array_component_name, const irep_idt &array_type_name, const std::vector< codet > &entry_point_instructions, const symbol_tablet &symbol_table)
Checks that the array component of the structure (possibly inherited from the superclass) is assigned...
Definition: require_goto_statements.cpp:390
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:101
require_goto_statements::find_struct_component_assignments
pointer_assignment_locationt find_struct_component_assignments(const std::vector< codet > &statements, const irep_idt &structure_name, const optionalt< irep_idt > &superclass_name, const irep_idt &component_name, const symbol_tablet &symbol_table)
Find assignment statements of the form:
Definition: require_goto_statements.cpp:66
java_types.h
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:256
code_function_callt::function
exprt & function()
Definition: std_code.h:1099
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34