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 
15 
17 
18 #include <util/expr_iterator.h>
19 #include <util/expr_util.h>
20 #include <util/pointer_expr.h>
21 #include <util/suffix.h>
22 
23 #include <algorithm>
24 
29 std::vector<codet>
31 {
32  std::vector<codet> statements;
33  for(auto sub_expression_it = function_value.depth_begin();
34  sub_expression_it != function_value.depth_end();
35  ++sub_expression_it)
36  {
37  if(sub_expression_it->id() == ID_code)
38  {
39  statements.push_back(to_code(*sub_expression_it));
40  }
41  }
42 
43  return statements;
44 }
45 
48 const std::vector<codet>
50  const symbol_tablet &symbol_table)
51 {
52  // Retrieve __CPROVER_start
53  const symbolt *entry_point_function =
54  symbol_table.lookup(goto_functionst::entry_point());
55  REQUIRE(entry_point_function != nullptr);
56  return get_all_statements(entry_point_function->value);
57 }
58 
73  const std::vector<codet> &statements,
74  const irep_idt &structure_name,
75  const optionalt<irep_idt> &superclass_name,
76  const irep_idt &component_name,
77  const symbol_tablet &symbol_table)
78 {
79  pointer_assignment_locationt locations{};
80 
81  for(const auto &assignment : statements)
82  {
83  if(assignment.get_statement() == ID_assign)
84  {
85  const code_assignt &code_assign = to_code_assign(assignment);
86 
87  if(code_assign.lhs().id() == ID_member)
88  {
89  const member_exprt &member_expr = to_member_expr(code_assign.lhs());
90 
91  if(superclass_name.has_value())
92  {
93  // Structure of the expression:
94  // member_exprt member_expr:
95  // - component name: \p component_name
96  // - operand (component of): member_exprt superclass_expr:
97  // - component name: @\p superclass_name
98  // - operand (component of): symbol for \p structure_name
99  if(
100  member_expr.get_component_name() == component_name &&
101  member_expr.compound().id() == ID_member)
102  {
103  const member_exprt &superclass_expr =
104  to_member_expr(member_expr.compound());
105  const irep_idt supercomponent_name =
106  "@" + id2string(superclass_name.value());
107 
109  const namespacet ns(symbol_table);
110  ode.build(superclass_expr, ns);
111  if(
112  superclass_expr.get_component_name() == supercomponent_name &&
114  .get_identifier() == structure_name)
115  {
116  if(
117  code_assign.rhs() ==
118  null_pointer_exprt(to_pointer_type(code_assign.lhs().type())))
119  {
120  locations.null_assignment = code_assign;
121  }
122  else
123  {
124  locations.non_null_assignments.push_back(code_assign);
125  }
126  }
127  }
128  }
129  else
130  {
131  // Structure of the expression:
132  // member_exprt member_expr:
133  // - component name: \p component_name
134  // - operand (component of): symbol for \p structure_name
135 
137  const namespacet ns(symbol_table);
138  ode.build(member_expr, ns);
139  if(
140  member_expr.get_component_name() == component_name &&
142  .get_identifier() == structure_name)
143  {
144  if(
145  code_assign.rhs() ==
146  null_pointer_exprt(to_pointer_type(code_assign.lhs().type())))
147  {
148  locations.null_assignment = code_assign;
149  }
150  else
151  {
152  locations.non_null_assignments.push_back(code_assign);
153  }
154  }
155  }
156  }
157  }
158  }
159  return locations;
160 }
161 
170  const std::vector<codet> &statements,
171  const irep_idt &component_name)
172 {
174 
175  for(const auto &assignment : statements)
176  {
177  if(assignment.get_statement() == ID_assign)
178  {
179  const code_assignt &code_assign = to_code_assign(assignment);
180 
181  if(code_assign.lhs().id() == ID_member)
182  {
183  const member_exprt &member_expr = to_member_expr(code_assign.lhs());
184  if(
185  member_expr.get_component_name() == component_name &&
186  member_expr.op().id() == ID_dereference)
187  {
188  const auto &pointer = to_dereference_expr(member_expr.op()).pointer();
189  if(
190  pointer.id() == ID_symbol &&
191  has_suffix(
192  id2string(to_symbol_expr(pointer).get_identifier()),
193  id2string(ID_this)))
194  {
195  if(
196  code_assign.rhs() ==
197  null_pointer_exprt(to_pointer_type(code_assign.lhs().type())))
198  {
199  locations.null_assignment = code_assign;
200  }
201  else
202  {
203  locations.non_null_assignments.push_back(code_assign);
204  }
205  }
206  }
207  }
208  }
209  }
210  return locations;
211 }
212 
221  const irep_idt &pointer_name,
222  const std::vector<codet> &instructions)
223 {
224  INFO("Looking for symbol: " << pointer_name);
225  std::regex special_chars{R"([-[\]{}()*+?.,\^$|#\s])"};
226  std::string sanitized =
227  std::regex_replace(id2string(pointer_name), special_chars, R"(\$&)");
229  std::regex("^" + sanitized + "$"), instructions);
230 }
231 
234  const std::regex &pointer_name_match,
235  const std::vector<codet> &instructions)
236 {
238  bool found_assignment = false;
239  std::vector<irep_idt> all_symbols;
240  for(const codet &statement : instructions)
241  {
242  if(statement.get_statement() == ID_assign)
243  {
244  const code_assignt &code_assign = to_code_assign(statement);
245  if(code_assign.lhs().id() == ID_symbol)
246  {
247  const symbol_exprt &symbol_expr = to_symbol_expr(code_assign.lhs());
248  all_symbols.push_back(symbol_expr.get_identifier());
249  if(
250  std::regex_search(
251  id2string(symbol_expr.get_identifier()), pointer_name_match))
252  {
253  if(
254  code_assign.rhs() ==
255  null_pointer_exprt(to_pointer_type(code_assign.lhs().type())))
256  {
257  locations.null_assignment = code_assign;
258  }
259  else
260  {
261  locations.non_null_assignments.push_back(code_assign);
262  }
263  found_assignment = true;
264  }
265  }
266  }
267  }
268 
269  std::ostringstream found_symbols;
270  for(const auto &entry : all_symbols)
271  {
272  found_symbols << entry << std::endl;
273  }
274  INFO("Symbols: " << found_symbols.str());
275  REQUIRE(found_assignment);
276 
277  return locations;
278 }
279 
287  const irep_idt &variable_name,
288  const std::vector<codet> &entry_point_instructions)
289 {
290  for(const auto &statement : entry_point_instructions)
291  {
292  if(statement.get_statement() == ID_decl)
293  {
294  const auto &decl_statement = to_code_decl(statement);
295 
296  if(decl_statement.get_identifier() == variable_name)
297  {
298  return decl_statement;
299  }
300  }
301  }
302  throw no_decl_found_exceptiont(variable_name.c_str());
303 }
304 
311  const std::vector<codet> &entry_point_instructions,
312  const irep_idt &symbol_identifier)
313 {
314  const auto &assignments = require_goto_statements::find_pointer_assignments(
315  symbol_identifier, entry_point_instructions)
317  REQUIRE(assignments.size() == 1);
318  return assignments[0].rhs();
319 }
320 
330  const std::vector<codet> &entry_point_instructions,
331  const irep_idt &symbol_identifier)
332 {
334  entry_point_instructions, symbol_identifier);
335 
336  return expr_try_dynamic_cast<symbol_exprt>(skip_typecast(expr));
337 }
338 
353 static const irep_idt &
355  const std::vector<codet> &entry_point_instructions,
356  const irep_idt &input_symbol_identifier)
357 {
358  const symbol_exprt *symbol_assigned_to_input_symbol =
360  entry_point_instructions, input_symbol_identifier);
361 
362  if(symbol_assigned_to_input_symbol)
363  {
365  entry_point_instructions,
366  symbol_assigned_to_input_symbol->get_identifier());
367  }
368 
369  return input_symbol_identifier;
370 }
371 
386  const irep_idt &structure_name,
387  const optionalt<irep_idt> &superclass_name,
388  const irep_idt &component_name,
389  const irep_idt &component_type_name,
390  const optionalt<irep_idt> &typecast_name,
391  const std::vector<codet> &entry_point_instructions,
392  const symbol_tablet &symbol_table)
393 {
394  namespacet ns(symbol_table);
395 
396  // First we need to find the assignments to the component belonging to
397  // the structure_name object
398  const auto &component_assignments =
400  entry_point_instructions,
401  structure_name,
402  superclass_name,
403  component_name,
404  symbol_table);
405  INFO(
406  "looking for component assignment " << component_name << " in "
407  << structure_name);
408  REQUIRE(component_assignments.non_null_assignments.size() == 1);
409 
410  // We are expecting the non-null assignment to be of the form:
411  // malloc_site->(@superclass_name if given.)field =
412  // (possible typecast) malloc_site$0;
413  const symbol_exprt *rhs_symbol_expr = expr_try_dynamic_cast<symbol_exprt>(
414  skip_typecast(component_assignments.non_null_assignments[0].rhs()));
415  REQUIRE(rhs_symbol_expr);
416 
417  const irep_idt &symbol_identifier = get_ultimate_source_symbol(
418  entry_point_instructions, rhs_symbol_expr->get_identifier());
419 
420  // After we have found the declaration of the final assignment's
421  // right hand side, then we want to identify that the type
422  // is the one we expect, e.g.:
423  // struct java.lang.Integer *malloc_site$0;
424  const auto &component_declaration =
426  symbol_identifier, entry_point_instructions);
427  const typet &component_type =
428  to_pointer_type(component_declaration.symbol().type()).subtype();
429  REQUIRE(component_type.id() == ID_struct_tag);
430  const auto &component_struct =
431  ns.follow_tag(to_struct_tag_type(component_type));
432  REQUIRE(component_struct.get(ID_name) == component_type_name);
433 
434  return symbol_identifier;
435 }
436 
446 const irep_idt &
448  const irep_idt &structure_name,
449  const optionalt<irep_idt> &superclass_name,
450  const irep_idt &array_component_name,
451  const irep_idt &array_type_name,
452  const std::vector<codet> &entry_point_instructions,
453  const symbol_tablet &symbol_table)
454 {
455  // First we need to find the assignments to the component belonging to
456  // the structure_name object
457  const auto &component_assignments =
459  entry_point_instructions,
460  structure_name,
461  superclass_name,
462  array_component_name,
463  symbol_table);
464  REQUIRE(component_assignments.non_null_assignments.size() == 1);
465 
466  // We are expecting that the resulting statement is of form:
467  // structure_name.array_component_name = (struct array_type_name *)
468  // tmp_object_factory$1;
469  const exprt &component_assignment_rhs_expr =
470  component_assignments.non_null_assignments[0].rhs();
471 
472  // The rhs is a typecast, deconstruct it to get the name of the variable
473  // and find the assignment to it
474  PRECONDITION(component_assignment_rhs_expr.id() == ID_typecast);
475  const auto &component_assignment_rhs =
476  to_typecast_expr(component_assignment_rhs_expr);
477  const auto &component_reference_tmp_name =
478  to_symbol_expr(component_assignment_rhs.op()).get_identifier();
479 
480  // Check the type we are casting to matches the array type
481  REQUIRE(component_assignment_rhs.type().id() == ID_pointer);
482  REQUIRE(
484  to_pointer_type(component_assignment_rhs.type()).subtype())
485  .get(ID_identifier) == array_type_name);
486 
487  // Get the tmp_object name and find assignments to it, there should be only
488  // one that assigns the correct array through side effect
489  const auto &component_reference_assignments =
491  component_reference_tmp_name, entry_point_instructions);
492  REQUIRE(component_reference_assignments.non_null_assignments.size() == 1);
493  const exprt &component_reference_assignment_rhs_expr =
494  component_reference_assignments.non_null_assignments[0].rhs();
495 
496  // The rhs is side effect
497  PRECONDITION(component_reference_assignment_rhs_expr.id() == ID_side_effect);
498  const auto &array_component_reference_assignment_rhs =
499  to_side_effect_expr(component_reference_assignment_rhs_expr);
500 
501  // The type of the side effect is an array with the correct element type
502  PRECONDITION(
503  array_component_reference_assignment_rhs.type().id() == ID_pointer);
504  const typet &array =
505  to_pointer_type(array_component_reference_assignment_rhs.type()).subtype();
506  PRECONDITION(is_java_array_tag(array.get(ID_identifier)));
507  REQUIRE(array.get(ID_identifier) == array_type_name);
508 
509  return component_reference_tmp_name;
510 }
511 
517 const irep_idt &
519  const irep_idt &argument_name,
520  const std::vector<codet> &entry_point_statements)
521 {
522  // Trace the creation of the object that is being supplied as the input
523  // argument to the function under test
524  const pointer_assignment_locationt argument_assignments =
527  "::" + id2string(argument_name),
528  entry_point_statements);
529 
530  // There should be at most one assignment to it
531  REQUIRE(argument_assignments.non_null_assignments.size() == 1);
532 
533  // The following finds the name of the tmp object that gets assigned
534  // to the input argument. There must be one such assignment only,
535  // and it usually looks like this:
536  // argument_name = tmp_object_factory$1;
537  const auto &argument_assignment =
538  argument_assignments.non_null_assignments[0];
539  const symbol_exprt &argument_symbol =
540  to_symbol_expr(skip_typecast(argument_assignment.rhs()));
541  return argument_symbol.get_identifier();
542 }
543 
550 std::vector<code_function_callt> require_goto_statements::find_function_calls(
551  const std::vector<codet> &statements,
552  const irep_idt &function_call_identifier)
553 {
554  std::vector<code_function_callt> function_calls;
555  for(const codet &statement : statements)
556  {
557  if(statement.get_statement() == ID_function_call)
558  {
559  const code_function_callt &function_call =
560  to_code_function_call(statement);
561 
562  if(function_call.function().id() == ID_symbol)
563  {
564  if(
565  to_symbol_expr(function_call.function()).get_identifier() ==
566  function_call_identifier)
567  {
568  function_calls.push_back(function_call);
569  }
570  }
571  }
572  }
573  return function_calls;
574 }
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:219
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: pointer_expr.cpp:108
to_code_decl
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:482
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:49
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:169
exprt::depth_begin
depth_iteratort depth_begin()
Definition: expr.cpp:292
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:442
typet
The type of an expression, extends irept.
Definition: type.h:28
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: pointer_expr.h:147
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:54
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:66
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:286
to_side_effect_expr
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1954
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
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:30
object_descriptor_exprt::root_object
static const exprt & root_object(const exprt &expr)
Definition: pointer_expr.cpp:125
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:518
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:550
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:82
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
require_goto_statements::pointer_assignment_locationt
Definition: require_goto_statements.h:28
null_pointer_exprt
The null pointer constant.
Definition: pointer_expr.h:461
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
member_exprt::compound
const exprt & compound() const
Definition: std_expr.h:2568
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:329
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
dereference_exprt::pointer
exprt & pointer()
Definition: pointer_expr.h:399
pointer_expr.h
API to expression classes for Pointers.
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
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:189
irept::id
const irep_idt & id() const
Definition: irep.h:407
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:468
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1326
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:293
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:310
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:220
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2527
expr_util.h
Deprecated expression utility functions.
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:385
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:1814
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:2611
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:2541
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:447
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:72
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:294
code_function_callt::function
exprt & function()
Definition: std_code.h:1250
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:354
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35