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 
12 
14 
16 
17 #include <util/expr_iterator.h>
18 #include <util/expr_util.h>
19 #include <util/pointer_expr.h>
20 #include <util/suffix.h>
21 #include <util/symbol_table.h>
22 
27 std::vector<codet>
29 {
30  std::vector<codet> statements;
31  for(auto sub_expression_it = function_value.depth_begin();
32  sub_expression_it != function_value.depth_end();
33  ++sub_expression_it)
34  {
35  if(sub_expression_it->id() == ID_code)
36  {
37  statements.push_back(to_code(*sub_expression_it));
38  }
39  }
40 
41  return statements;
42 }
43 
46 const std::vector<codet>
48  const symbol_tablet &symbol_table)
49 {
50  // Retrieve __CPROVER_start
51  const symbolt *entry_point_function =
52  symbol_table.lookup(goto_functionst::entry_point());
53  REQUIRE(entry_point_function != nullptr);
54  return get_all_statements(entry_point_function->value);
55 }
56 
71  const std::vector<codet> &statements,
72  const irep_idt &structure_name,
73  const optionalt<irep_idt> &superclass_name,
74  const irep_idt &component_name,
75  const symbol_tablet &symbol_table)
76 {
77  pointer_assignment_locationt locations{};
78 
79  for(const auto &assignment : statements)
80  {
81  if(assignment.get_statement() == ID_assign)
82  {
83  const code_assignt &code_assign = to_code_assign(assignment);
84 
85  if(code_assign.lhs().id() == ID_member)
86  {
87  const member_exprt &member_expr = to_member_expr(code_assign.lhs());
88 
89  if(superclass_name.has_value())
90  {
91  // Structure of the expression:
92  // member_exprt member_expr:
93  // - component name: \p component_name
94  // - operand (component of): member_exprt superclass_expr:
95  // - component name: @\p superclass_name
96  // - operand (component of): symbol for \p structure_name
97  if(
98  member_expr.get_component_name() == component_name &&
99  member_expr.compound().id() == ID_member)
100  {
101  const member_exprt &superclass_expr =
102  to_member_expr(member_expr.compound());
103  const irep_idt supercomponent_name =
104  "@" + id2string(superclass_name.value());
105 
107  const namespacet ns(symbol_table);
108  ode.build(superclass_expr, ns);
109  if(
110  superclass_expr.get_component_name() == supercomponent_name &&
112  .get_identifier() == structure_name)
113  {
114  if(
115  code_assign.rhs() ==
116  null_pointer_exprt(to_pointer_type(code_assign.lhs().type())))
117  {
118  locations.null_assignment = code_assign;
119  }
120  else
121  {
122  locations.non_null_assignments.push_back(code_assign);
123  }
124  }
125  }
126  }
127  else
128  {
129  // Structure of the expression:
130  // member_exprt member_expr:
131  // - component name: \p component_name
132  // - operand (component of): symbol for \p structure_name
133 
135  const namespacet ns(symbol_table);
136  ode.build(member_expr, ns);
137  if(
138  member_expr.get_component_name() == component_name &&
140  .get_identifier() == structure_name)
141  {
142  if(
143  code_assign.rhs() ==
144  null_pointer_exprt(to_pointer_type(code_assign.lhs().type())))
145  {
146  locations.null_assignment = code_assign;
147  }
148  else
149  {
150  locations.non_null_assignments.push_back(code_assign);
151  }
152  }
153  }
154  }
155  }
156  }
157  return locations;
158 }
159 
168  const std::vector<codet> &statements,
169  const irep_idt &component_name)
170 {
172 
173  for(const auto &assignment : statements)
174  {
175  if(assignment.get_statement() == ID_assign)
176  {
177  const code_assignt &code_assign = to_code_assign(assignment);
178 
179  if(code_assign.lhs().id() == ID_member)
180  {
181  const member_exprt &member_expr = to_member_expr(code_assign.lhs());
182  if(
183  member_expr.get_component_name() == component_name &&
184  member_expr.op().id() == ID_dereference)
185  {
186  const auto &pointer = to_dereference_expr(member_expr.op()).pointer();
187  if(
188  pointer.id() == ID_symbol &&
189  has_suffix(
190  id2string(to_symbol_expr(pointer).get_identifier()),
191  id2string(ID_this)))
192  {
193  if(
194  code_assign.rhs() ==
195  null_pointer_exprt(to_pointer_type(code_assign.lhs().type())))
196  {
197  locations.null_assignment = code_assign;
198  }
199  else
200  {
201  locations.non_null_assignments.push_back(code_assign);
202  }
203  }
204  }
205  }
206  }
207  }
208  return locations;
209 }
210 
219  const irep_idt &pointer_name,
220  const std::vector<codet> &instructions)
221 {
222  INFO("Looking for symbol: " << pointer_name);
223  std::regex special_chars{R"([-[\]{}()*+?.,\^$|#\s])"};
224  std::string sanitized =
225  std::regex_replace(id2string(pointer_name), special_chars, R"(\$&)");
227  std::regex("^" + sanitized + "$"), instructions);
228 }
229 
232  const std::regex &pointer_name_match,
233  const std::vector<codet> &instructions)
234 {
236  bool found_assignment = false;
237  std::vector<irep_idt> all_symbols;
238  for(const codet &statement : instructions)
239  {
240  if(statement.get_statement() == ID_assign)
241  {
242  const code_assignt &code_assign = to_code_assign(statement);
243  if(code_assign.lhs().id() == ID_symbol)
244  {
245  const symbol_exprt &symbol_expr = to_symbol_expr(code_assign.lhs());
246  all_symbols.push_back(symbol_expr.get_identifier());
247  if(
248  std::regex_search(
249  id2string(symbol_expr.get_identifier()), pointer_name_match))
250  {
251  if(
252  code_assign.rhs() ==
253  null_pointer_exprt(to_pointer_type(code_assign.lhs().type())))
254  {
255  locations.null_assignment = code_assign;
256  }
257  else
258  {
259  locations.non_null_assignments.push_back(code_assign);
260  }
261  found_assignment = true;
262  }
263  }
264  }
265  }
266 
267  std::ostringstream found_symbols;
268  for(const auto &entry : all_symbols)
269  {
270  found_symbols << entry << std::endl;
271  }
272  INFO("Symbols: " << found_symbols.str());
273  REQUIRE(found_assignment);
274 
275  return locations;
276 }
277 
285  const irep_idt &variable_name,
286  const std::vector<codet> &entry_point_instructions)
287 {
288  for(const auto &statement : entry_point_instructions)
289  {
290  if(statement.get_statement() == ID_decl)
291  {
292  const auto &decl_statement = to_code_decl(statement);
293 
294  if(decl_statement.get_identifier() == variable_name)
295  {
296  return decl_statement;
297  }
298  }
299  }
300  throw no_decl_found_exceptiont(variable_name.c_str());
301 }
302 
309  const std::vector<codet> &entry_point_instructions,
310  const irep_idt &symbol_identifier)
311 {
312  const auto &assignments = require_goto_statements::find_pointer_assignments(
313  symbol_identifier, entry_point_instructions)
315  REQUIRE(assignments.size() == 1);
316  return assignments[0].rhs();
317 }
318 
328  const std::vector<codet> &entry_point_instructions,
329  const irep_idt &symbol_identifier)
330 {
332  entry_point_instructions, symbol_identifier);
333 
334  return expr_try_dynamic_cast<symbol_exprt>(skip_typecast(expr));
335 }
336 
351 static const irep_idt &
353  const std::vector<codet> &entry_point_instructions,
354  const irep_idt &input_symbol_identifier)
355 {
356  const symbol_exprt *symbol_assigned_to_input_symbol =
358  entry_point_instructions, input_symbol_identifier);
359 
360  if(symbol_assigned_to_input_symbol)
361  {
363  entry_point_instructions,
364  symbol_assigned_to_input_symbol->get_identifier());
365  }
366 
367  return input_symbol_identifier;
368 }
369 
384  const irep_idt &structure_name,
385  const optionalt<irep_idt> &superclass_name,
386  const irep_idt &component_name,
387  const irep_idt &component_type_name,
388  const optionalt<irep_idt> &typecast_name,
389  const std::vector<codet> &entry_point_instructions,
390  const symbol_tablet &symbol_table)
391 {
392  namespacet ns(symbol_table);
393 
394  // First we need to find the assignments to the component belonging to
395  // the structure_name object
396  const auto &component_assignments =
398  entry_point_instructions,
399  structure_name,
400  superclass_name,
401  component_name,
402  symbol_table);
403  INFO(
404  "looking for component assignment " << component_name << " in "
405  << structure_name);
406  REQUIRE(component_assignments.non_null_assignments.size() == 1);
407 
408  // We are expecting the non-null assignment to be of the form:
409  // malloc_site->(@superclass_name if given.)field =
410  // (possible typecast) malloc_site$0;
411  const symbol_exprt *rhs_symbol_expr = expr_try_dynamic_cast<symbol_exprt>(
412  skip_typecast(component_assignments.non_null_assignments[0].rhs()));
413  REQUIRE(rhs_symbol_expr);
414 
415  const irep_idt &symbol_identifier = get_ultimate_source_symbol(
416  entry_point_instructions, rhs_symbol_expr->get_identifier());
417 
418  // After we have found the declaration of the final assignment's
419  // right hand side, then we want to identify that the type
420  // is the one we expect, e.g.:
421  // struct java.lang.Integer *malloc_site$0;
422  const auto &component_declaration =
424  symbol_identifier, entry_point_instructions);
425  const typet &component_type =
426  to_pointer_type(component_declaration.symbol().type()).subtype();
427  REQUIRE(component_type.id() == ID_struct_tag);
428  const auto &component_struct =
429  ns.follow_tag(to_struct_tag_type(component_type));
430  REQUIRE(component_struct.get(ID_name) == component_type_name);
431 
432  return symbol_identifier;
433 }
434 
444 const irep_idt &
446  const irep_idt &structure_name,
447  const optionalt<irep_idt> &superclass_name,
448  const irep_idt &array_component_name,
449  const irep_idt &array_type_name,
450  const std::vector<codet> &entry_point_instructions,
451  const symbol_tablet &symbol_table)
452 {
453  // First we need to find the assignments to the component belonging to
454  // the structure_name object
455  const auto &component_assignments =
457  entry_point_instructions,
458  structure_name,
459  superclass_name,
460  array_component_name,
461  symbol_table);
462  REQUIRE(component_assignments.non_null_assignments.size() == 1);
463 
464  // We are expecting that the resulting statement is of form:
465  // structure_name.array_component_name = (struct array_type_name *)
466  // tmp_object_factory$1;
467  const exprt &component_assignment_rhs_expr =
468  component_assignments.non_null_assignments[0].rhs();
469 
470  // The rhs is a typecast, deconstruct it to get the name of the variable
471  // and find the assignment to it
472  PRECONDITION(component_assignment_rhs_expr.id() == ID_typecast);
473  const auto &component_assignment_rhs =
474  to_typecast_expr(component_assignment_rhs_expr);
475  const auto &component_reference_tmp_name =
476  to_symbol_expr(component_assignment_rhs.op()).get_identifier();
477 
478  // Check the type we are casting to matches the array type
479  REQUIRE(component_assignment_rhs.type().id() == ID_pointer);
480  REQUIRE(
482  to_pointer_type(component_assignment_rhs.type()).subtype())
483  .get(ID_identifier) == array_type_name);
484 
485  // Get the tmp_object name and find assignments to it, there should be only
486  // one that assigns the correct array through side effect
487  const auto &component_reference_assignments =
489  component_reference_tmp_name, entry_point_instructions);
490  REQUIRE(component_reference_assignments.non_null_assignments.size() == 1);
491  const exprt &component_reference_assignment_rhs_expr =
492  component_reference_assignments.non_null_assignments[0].rhs();
493 
494  // The rhs is side effect
495  PRECONDITION(component_reference_assignment_rhs_expr.id() == ID_side_effect);
496  const auto &array_component_reference_assignment_rhs =
497  to_side_effect_expr(component_reference_assignment_rhs_expr);
498 
499  // The type of the side effect is an array with the correct element type
500  PRECONDITION(
501  array_component_reference_assignment_rhs.type().id() == ID_pointer);
502  const typet &array =
503  to_pointer_type(array_component_reference_assignment_rhs.type()).subtype();
504  PRECONDITION(is_java_array_tag(array.get(ID_identifier)));
505  REQUIRE(array.get(ID_identifier) == array_type_name);
506 
507  return component_reference_tmp_name;
508 }
509 
515 const irep_idt &
517  const irep_idt &argument_name,
518  const std::vector<codet> &entry_point_statements)
519 {
520  // Trace the creation of the object that is being supplied as the input
521  // argument to the function under test
522  const pointer_assignment_locationt argument_assignments =
525  "::" + id2string(argument_name),
526  entry_point_statements);
527 
528  // There should be at most one assignment to it
529  REQUIRE(argument_assignments.non_null_assignments.size() == 1);
530 
531  // The following finds the name of the tmp object that gets assigned
532  // to the input argument. There must be one such assignment only,
533  // and it usually looks like this:
534  // argument_name = tmp_object_factory$1;
535  const auto &argument_assignment =
536  argument_assignments.non_null_assignments[0];
537  const symbol_exprt &argument_symbol =
538  to_symbol_expr(skip_typecast(argument_assignment.rhs()));
539  return argument_symbol.get_identifier();
540 }
541 
548 std::vector<code_function_callt> require_goto_statements::find_function_calls(
549  const std::vector<codet> &statements,
550  const irep_idt &function_call_identifier)
551 {
552  std::vector<code_function_callt> function_calls;
553  for(const codet &statement : statements)
554  {
555  if(statement.get_statement() == ID_function_call)
556  {
557  const code_function_callt &function_call =
558  to_code_function_call(statement);
559 
560  if(function_call.function().id() == ID_symbol)
561  {
562  if(
563  to_symbol_expr(function_call.function()).get_identifier() ==
564  function_call_identifier)
565  {
566  function_calls.push_back(function_call);
567  }
568  }
569  }
570  }
571  return function_calls;
572 }
A codet representing an assignment in the program.
Definition: std_code.h:293
exprt & rhs()
Definition: std_code.h:315
exprt & lhs()
Definition: std_code.h:310
A codet representing the declaration of a local variable.
Definition: std_code.h:400
codet representation of a function call statement.
Definition: std_code.h:1213
exprt & function()
Definition: std_code.h:1248
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
const char * c_str() const
Definition: dstring.h:99
Base class for all expressions.
Definition: expr.h:54
depth_iteratort depth_end()
Definition: expr.cpp:267
depth_iteratort depth_begin()
Definition: expr.cpp:265
typet & type()
Return the type of the expression.
Definition: expr.h:82
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
const irep_idt & id() const
Definition: irep.h:407
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
Extract member of struct or union.
Definition: std_expr.h:2613
const exprt & compound() const
Definition: std_expr.h:2654
irep_idt get_component_name() const
Definition: std_expr.h:2627
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The null pointer constant.
Definition: pointer_expr.h:703
Split an expression into a base object and a (byte) offset.
Definition: pointer_expr.h:147
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
static const exprt & root_object(const exprt &expr)
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
exprt value
Initial value of symbol.
Definition: symbol.h:34
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
const exprt & op() const
Definition: std_expr.h:293
Forward depth-first search iterators These iterators' copy operations are expensive,...
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:215
Deprecated expression utility functions.
Goto Programs with Functions.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
bool is_java_array_tag(const irep_idt &tag)
See above.
Definition: java_types.cpp:231
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...
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...
std::vector< codet > get_all_statements(const exprt &function_value)
Expand value of a function to include all child codets.
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...
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...
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.
const std::vector< codet > require_entry_point_statements(const symbol_tablet &symbol_table)
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}.
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:
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.
nonstd::optional< T > optionalt
Definition: optional.h:35
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:684
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
const symbol_exprt * try_get_unique_symbol_assigned_to_symbol(const std::vector< codet > &entry_point_instructions, const irep_idt &symbol_identifier)
Get the unique symbol assigned to a symbol, if one exists.
static const irep_idt & get_ultimate_source_symbol(const std::vector< codet > &entry_point_instructions, const irep_idt &input_symbol_identifier)
Follow the chain of non-null assignments until we find a symbol that hasn't ever had another symbol a...
const exprt & get_unique_non_null_expression_assigned_to_symbol(const std::vector< codet > &entry_point_instructions, const irep_idt &symbol_identifier)
Get the unique non-null expression assigned to a symbol.
Utilties for inspecting goto functions.
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1952
const codet & to_code(const exprt &expr)
Definition: std_code.h:153
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:480
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1324
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:381
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1900
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:17
Author: Diffblue Ltd.