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