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 
66  const std::vector<codet> &statements,
67  const irep_idt &structure_name,
68  const optionalt<irep_idt> &superclass_name,
69  const irep_idt &component_name)
70 {
72 
73  for(const auto &assignment : statements)
74  {
75  if(assignment.get_statement() == ID_assign)
76  {
77  const code_assignt &code_assign = to_code_assign(assignment);
78 
79  if(code_assign.lhs().id() == ID_member)
80  {
81  const member_exprt &member_expr = to_member_expr(code_assign.lhs());
82 
83  if(superclass_name.has_value())
84  {
85  // Structure of the expression:
86  // member_exprt member_expr:
87  // - component name: \p component_name
88  // - operand (component of): member_exprt superclass_expr:
89  // - component name: @\p superclass_name
90  // - operand (component of): symbol for \p structure_name
91  if(
92  member_expr.get_component_name() == component_name &&
93  member_expr.compound().id() == ID_member)
94  {
95  const member_exprt &superclass_expr =
96  to_member_expr(member_expr.op0());
97  const irep_idt supercomponent_name =
98  "@" + id2string(superclass_name.value());
99 
100  if(
101  superclass_expr.get_component_name() == supercomponent_name &&
102  superclass_expr.symbol().get_identifier() == structure_name)
103  {
104  if(
105  code_assign.rhs() ==
106  null_pointer_exprt(to_pointer_type(code_assign.lhs().type())))
107  {
108  locations.null_assignment = code_assign;
109  }
110  else
111  {
112  locations.non_null_assignments.push_back(code_assign);
113  }
114  }
115  }
116  }
117  else
118  {
119  // Structure of the expression:
120  // member_exprt member_expr:
121  // - component name: \p component_name
122  // - operand (component of): symbol for \p structure_name
123  if(
124  member_expr.op().id() == ID_symbol &&
125  member_expr.symbol().get_identifier() == structure_name &&
126  member_expr.get_component_name() == component_name)
127  {
128  if(
129  code_assign.rhs() ==
130  null_pointer_exprt(to_pointer_type(code_assign.lhs().type())))
131  {
132  locations.null_assignment = code_assign;
133  }
134  else
135  {
136  locations.non_null_assignments.push_back(code_assign);
137  }
138  }
139  }
140  }
141  }
142  }
143  return locations;
144 }
145 
154  const std::vector<codet> &statements,
155  const irep_idt &component_name)
156 {
158 
159  for(const auto &assignment : statements)
160  {
161  if(assignment.get_statement() == ID_assign)
162  {
163  const code_assignt &code_assign = to_code_assign(assignment);
164 
165  if(code_assign.lhs().id() == ID_member)
166  {
167  const member_exprt &member_expr = to_member_expr(code_assign.lhs());
168  if(
169  member_expr.get_component_name() == component_name &&
170  member_expr.op().id() == ID_dereference &&
171  member_expr.op().op0().id() == ID_symbol &&
172  has_suffix(
173  id2string(to_symbol_expr(member_expr.op().op0()).get_identifier()),
174  "this"))
175  {
176  if(
177  code_assign.rhs() ==
178  null_pointer_exprt(to_pointer_type(code_assign.lhs().type())))
179  {
180  locations.null_assignment = code_assign;
181  }
182  else
183  {
184  locations.non_null_assignments.push_back(code_assign);
185  }
186  }
187  }
188  }
189  }
190  return locations;
191 }
192 
201  const irep_idt &pointer_name,
202  const std::vector<codet> &instructions)
203 {
204  INFO("Looking for symbol: " << pointer_name);
205  std::regex special_chars{R"([-[\]{}()*+?.,\^$|#\s])"};
206  std::string sanitized =
207  std::regex_replace(id2string(pointer_name), special_chars, R"(\$&)");
209  std::regex("^" + sanitized + "$"), instructions);
210 }
211 
214  const std::regex &pointer_name_match,
215  const std::vector<codet> &instructions)
216 {
218  bool found_assignment = false;
219  std::vector<irep_idt> all_symbols;
220  for(const codet &statement : instructions)
221  {
222  if(statement.get_statement() == ID_assign)
223  {
224  const code_assignt &code_assign = to_code_assign(statement);
225  if(code_assign.lhs().id() == ID_symbol)
226  {
227  const symbol_exprt &symbol_expr = to_symbol_expr(code_assign.lhs());
228  all_symbols.push_back(symbol_expr.get_identifier());
229  if(
230  std::regex_search(
231  id2string(symbol_expr.get_identifier()), pointer_name_match))
232  {
233  if(
234  code_assign.rhs() ==
235  null_pointer_exprt(to_pointer_type(code_assign.lhs().type())))
236  {
237  locations.null_assignment = code_assign;
238  }
239  else
240  {
241  locations.non_null_assignments.push_back(code_assign);
242  }
243  found_assignment = true;
244  }
245  }
246  }
247  }
248 
249  std::ostringstream found_symbols;
250  for(const auto entry : all_symbols)
251  {
252  found_symbols << entry << std::endl;
253  }
254  INFO("Symbols: " << found_symbols.str());
255  REQUIRE(found_assignment);
256 
257  return locations;
258 }
259 
267  const irep_idt &variable_name,
268  const std::vector<codet> &entry_point_instructions)
269 {
270  for(const auto &statement : entry_point_instructions)
271  {
272  if(statement.get_statement() == ID_decl)
273  {
274  const auto &decl_statement = to_code_decl(statement);
275 
276  if(decl_statement.get_identifier() == variable_name)
277  {
278  return decl_statement;
279  }
280  }
281  }
282  throw no_decl_found_exceptiont(variable_name.c_str());
283 }
284 
296  const irep_idt &structure_name,
297  const optionalt<irep_idt> &superclass_name,
298  const irep_idt &component_name,
299  const irep_idt &component_type_name,
300  const optionalt<irep_idt> &typecast_name,
301  const std::vector<codet> &entry_point_instructions)
302 {
303  // First we need to find the assignments to the component belonging to
304  // the structure_name object
305  const auto &component_assignments =
307  entry_point_instructions,
308  structure_name,
309  superclass_name,
310  component_name);
311  REQUIRE(component_assignments.non_null_assignments.size() == 1);
312 
313  // We are expecting that the resulting statement can be of two forms:
314  // 1. structure_name.(@superclass_name if given).component =
315  // (struct cast_type_name *) tmp_object_factory$1;
316  // followed by a direct assignment like this:
317  // tmp_object_factory$1 = &tmp_object_factory$2;
318  // 2. structure_name.component = &tmp_object_factory$1;
319  exprt component_assignment_rhs_expr =
320  component_assignments.non_null_assignments[0].rhs();
321 
322  // If the rhs is a typecast (case 1 above), deconstruct it to get the name of
323  // the variable and find the assignment to it
324  if(component_assignment_rhs_expr.id() == ID_typecast)
325  {
326  const auto &component_assignment_rhs =
327  to_typecast_expr(component_assignment_rhs_expr);
328 
329  // Check the type we are casting to
330  if(typecast_name.has_value())
331  {
332  REQUIRE(component_assignment_rhs.type().id() == ID_pointer);
333  REQUIRE(
335  to_pointer_type(component_assignment_rhs.type()).subtype())
336  .get(ID_identifier) == typecast_name.value());
337  }
338 
339  const auto &component_reference_tmp_name =
340  to_symbol_expr(component_assignment_rhs.op()).get_identifier();
341  const auto &component_reference_assignments =
343  component_reference_tmp_name, entry_point_instructions)
345  REQUIRE(component_reference_assignments.size() == 1);
346  component_assignment_rhs_expr = component_reference_assignments[0].rhs();
347  }
348 
349  // The rhs assigns an address of a variable, get its name
350  const auto &component_reference_assignment_rhs =
351  to_address_of_expr(component_assignment_rhs_expr);
352  const auto &component_tmp_name =
353  to_symbol_expr(component_reference_assignment_rhs.op()).get_identifier();
354 
355  // After we have found the declaration of the final assignment's
356  // right hand side, then we want to identify that the type
357  // is the one we expect, e.g.:
358  // struct java.lang.Integer { __CPROVER_string @class_identifier; }
359  // tmp_object_factory$2;
360  const auto &component_declaration =
362  component_tmp_name, entry_point_instructions);
363  REQUIRE(component_declaration.symbol().type().id() == ID_struct);
364  const auto &component_struct =
365  to_struct_type(component_declaration.symbol().type());
366  REQUIRE(component_struct.get(ID_name) == component_type_name);
367 
368  return component_tmp_name;
369 }
370 
380 const irep_idt &
382  const irep_idt &structure_name,
383  const optionalt<irep_idt> &superclass_name,
384  const irep_idt &array_component_name,
385  const irep_idt &array_type_name,
386  const irep_idt &array_component_element_type_name,
387  const std::vector<codet> &entry_point_instructions)
388 {
389  // First we need to find the assignments to the component belonging to
390  // the structure_name object
391  const auto &component_assignments =
393  entry_point_instructions,
394  structure_name,
395  superclass_name,
396  array_component_name);
397  REQUIRE(component_assignments.non_null_assignments.size() == 1);
398 
399  // We are expecting that the resulting statement is of form:
400  // structure_name.array_component_name = (struct array_type_name *)
401  // tmp_object_factory$1;
402  const exprt &component_assignment_rhs_expr =
403  component_assignments.non_null_assignments[0].rhs();
404 
405  // The rhs is a typecast, deconstruct it to get the name of the variable
406  // and find the assignment to it
407  PRECONDITION(component_assignment_rhs_expr.id() == ID_typecast);
408  const auto &component_assignment_rhs =
409  to_typecast_expr(component_assignment_rhs_expr);
410  const auto &component_reference_tmp_name =
411  to_symbol_expr(component_assignment_rhs.op()).get_identifier();
412 
413  // Check the type we are casting to matches the array type
414  REQUIRE(component_assignment_rhs.type().id() == ID_pointer);
415  REQUIRE(
416  to_symbol_type(to_pointer_type(component_assignment_rhs.type()).subtype())
417  .get(ID_identifier) == array_type_name);
418 
419  // Get the tmp_object name and find assignments to it, there should be only
420  // one that assigns the correct array through side effect
421  const auto &component_reference_assignments =
423  component_reference_tmp_name, entry_point_instructions);
424  REQUIRE(component_reference_assignments.non_null_assignments.size() == 1);
425  const exprt &component_reference_assignment_rhs_expr =
426  component_reference_assignments.non_null_assignments[0].rhs();
427 
428  // The rhs is side effect
429  PRECONDITION(component_reference_assignment_rhs_expr.id() == ID_side_effect);
430  const auto &array_component_reference_assignment_rhs =
431  to_side_effect_expr(component_reference_assignment_rhs_expr);
432 
433  // The type of the side effect is an array with the correct element type
434  PRECONDITION(
435  array_component_reference_assignment_rhs.type().id() == ID_pointer);
436  const typet &array =
437  to_pointer_type(array_component_reference_assignment_rhs.type()).subtype();
438  PRECONDITION(is_java_array_tag(array.get(ID_identifier)));
439  REQUIRE(array.get(ID_identifier) == array_type_name);
440 
441  return component_reference_tmp_name;
442 }
443 
449 const irep_idt &
451  const irep_idt &argument_name,
452  const std::vector<codet> &entry_point_statements)
453 {
454  // Trace the creation of the object that is being supplied as the input
455  // argument to the function under test
456  const pointer_assignment_locationt &argument_assignments =
459  id2string(argument_name),
460  entry_point_statements);
461 
462  // There should be at most one assignment to it
463  REQUIRE(argument_assignments.non_null_assignments.size() == 1);
464 
465  // The following finds the name of the tmp object that gets assigned
466  // to the input argument. There must be one such assignment only,
467  // and usually looks like this:
468  // argument_name = &tmp_object_factory$1;
469  const auto &argument_assignment =
470  argument_assignments.non_null_assignments[0];
471  const auto &argument_tmp_name =
472  to_symbol_expr(to_address_of_expr(argument_assignment.rhs()).object())
473  .get_identifier();
474  return argument_tmp_name;
475 }
476 
483 std::vector<code_function_callt> require_goto_statements::find_function_calls(
484  const std::vector<codet> &statements,
485  const irep_idt &function_call_identifier)
486 {
487  std::vector<code_function_callt> function_calls;
488  for(const codet &statement : statements)
489  {
490  if(statement.get_statement() == ID_function_call)
491  {
492  const code_function_callt &function_call =
493  to_code_function_call(statement);
494 
495  if(function_call.function().id() == ID_symbol)
496  {
497  if(
498  to_symbol_expr(function_call.function()).get_identifier() ==
499  function_call_identifier)
500  {
501  function_calls.push_back(function_call);
502  }
503  }
504  }
505  }
506  return function_calls;
507 }
The type of an expression.
Definition: type.h:22
const symbol_exprt & symbol() const
Definition: std_expr.h:3931
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:291
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
std::vector< codet > get_all_statements(const exprt &function_value)
Expand value of a function to include all child codets.
exprt & op0()
Definition: expr.h:72
const exprt & op() const
Definition: std_expr.h:340
const irep_idt & get_identifier() const
Definition: std_expr.h:128
Goto Programs with Functions.
const std::vector< codet > require_entry_point_statements(const symbol_tablet &symbol_table)
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
The null pointer constant.
Definition: std_expr.h:4518
exprt value
Initial value of symbol.
Definition: symbol.h:37
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)
Checks that the component of the structure (possibly inherited from the superclass) is assigned an ob...
typet & type()
Definition: expr.h:56
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Definition: std_expr.h:3199
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
depth_iteratort depth_begin()
Definition: expr.cpp:299
bool is_java_array_tag(const irep_idt &tag)
See above.
Definition: java_types.cpp:174
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}.
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1326
Extract member of struct or union.
Definition: std_expr.h:3869
const exprt & compound() const
Definition: std_expr.h:3920
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:240
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)
Find assignment statements of the form:
const irep_idt & id() const
Definition: irep.h:259
exprt & lhs()
Definition: std_code.h:209
A declaration of a local variable.
Definition: std_code.h:254
exprt & rhs()
Definition: std_code.h:214
nonstd::optional< T > optionalt
Definition: optional.h:35
The symbol table.
Definition: symbol_table.h:19
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3953
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...
A function call.
Definition: std_code.h:858
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
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.
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
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 irep_idt &array_component_element_type_name, const std::vector< codet > &entry_point_instructions)
Checks that the array component of the structure (possibly inherited from the superclass) is assigned...
static irep_idt entry_point()
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.
exprt & function()
Definition: std_code.h:878
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...
Base class for all expressions.
Definition: expr.h:42
irep_idt get_component_name() const
Definition: std_expr.h:3893
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:2143
const codet & to_code(const exprt &expr)
Definition: std_code.h:75
Expression to hold a symbol (variable)
Definition: std_expr.h:90
depth_iteratort depth_end()
Definition: expr.cpp:301
const char * c_str() const
Definition: dstring.h:84
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:15
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1459
Utilties for inspecting goto functions.
A statement in a programming language.
Definition: std_code.h:21
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Assignment.
Definition: std_code.h:196
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:909