cprover
remove_const_function_pointers.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Programs
4 
5 Author: Thomas Kiley, thomas.kiley@diffblue.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <util/arith_tools.h>
15 #include <util/simplify_expr.h>
16 #include <util/std_expr.h>
17 #include <util/symbol_table.h>
18 
19 #include "goto_functions.h"
20 
21 #define LOG(message, irep) \
22  debug() << "Case " << __LINE__ << " : " << message << "\n" \
23  << irep.pretty() << eom;
24 
32  const namespacet &ns,
33  const symbol_tablet &symbol_table):
35  ns(ns),
36  symbol_table(symbol_table)
37 {}
38 
51  const exprt &base_expression,
52  functionst &out_functions)
53 {
54  // Replace all const symbols with their values
55  exprt non_symbol_expression=replace_const_symbols(base_expression);
56  return try_resolve_function_call(non_symbol_expression, out_functions);
57 }
58 
67  const exprt &expression) const
68 {
69  if(expression.id()==ID_symbol)
70  {
71  if(is_const_expression(expression))
72  {
73  const symbolt &symbol =
74  *symbol_table.lookup(to_symbol_expr(expression).get_identifier());
75  if(symbol.type.id()!=ID_code)
76  {
77  const exprt &symbol_value=symbol.value;
78  return replace_const_symbols(symbol_value);
79  }
80  else
81  {
82  return expression;
83  }
84  }
85  else
86  {
87  return expression;
88  }
89  }
90  else
91  {
92  exprt const_symbol_cleared_expr=expression;
93  const_symbol_cleared_expr.operands().clear();
94  for(const exprt &op : expression.operands())
95  {
96  exprt const_symbol_cleared_op=replace_const_symbols(op);
97  const_symbol_cleared_expr.operands().push_back(const_symbol_cleared_op);
98  }
99 
100  return const_symbol_cleared_expr;
101  }
102 }
103 
108  const symbol_exprt &symbol_expr) const
109 {
110  const symbolt &symbol=
111  *symbol_table.lookup(symbol_expr.get_identifier());
112  return symbol.value;
113 }
114 
124  const exprt &expr, functionst &out_functions)
125 {
126  assert(out_functions.empty());
127  const exprt &simplified_expr=simplify_expr(expr, ns);
128  bool resolved=false;
129  functionst resolved_functions;
130  if(simplified_expr.id()==ID_index)
131  {
132  const index_exprt &index_expr=to_index_expr(simplified_expr);
133  resolved=try_resolve_index_of_function_call(index_expr, resolved_functions);
134  }
135  else if(simplified_expr.id()==ID_member)
136  {
137  const member_exprt &member_expr=to_member_expr(simplified_expr);
138  resolved=try_resolve_member_function_call(member_expr, resolved_functions);
139  }
140  else if(simplified_expr.id()==ID_address_of)
141  {
142  address_of_exprt address_expr=to_address_of_expr(simplified_expr);
144  address_expr, resolved_functions);
145  }
146  else if(simplified_expr.id()==ID_dereference)
147  {
148  const dereference_exprt &deref=to_dereference_expr(simplified_expr);
149  resolved=try_resolve_dereference_function_call(deref, resolved_functions);
150  }
151  else if(simplified_expr.id()==ID_typecast)
152  {
153  typecast_exprt typecast_expr=to_typecast_expr(simplified_expr);
154  resolved=
155  try_resolve_typecast_function_call(typecast_expr, resolved_functions);
156  }
157  else if(simplified_expr.id()==ID_symbol)
158  {
159  if(simplified_expr.type().id()==ID_code)
160  {
161  resolved_functions.insert(to_symbol_expr(simplified_expr));
162  resolved=true;
163  }
164  else
165  {
166  LOG("Non const symbol wasn't squashed", simplified_expr);
167  resolved=false;
168  }
169  }
170  else if(simplified_expr.id()==ID_constant)
171  {
172  if(simplified_expr.is_zero())
173  {
174  // We have the null pointer - no need to throw everything away
175  // but we don't add any functions either
176  resolved=true;
177  }
178  else
179  {
180  LOG("Non-zero constant value found", simplified_expr);
181  resolved=false;
182  }
183  }
184  else
185  {
186  LOG("Unrecognised expression", simplified_expr);
187  resolved=false;
188  }
189 
190  if(resolved)
191  {
192  out_functions.insert(resolved_functions.begin(), resolved_functions.end());
193  return true;
194  }
195  else
196  {
197  return false;
198  }
199 }
200 
208  const expressionst &exprs, functionst &out_functions)
209 {
210  for(const exprt &value : exprs)
211  {
212  functionst potential_out_functions;
213  bool resolved_value=
214  try_resolve_function_call(value, potential_out_functions);
215 
216  if(resolved_value)
217  {
218  out_functions.insert(
219  potential_out_functions.begin(),
220  potential_out_functions.end());
221  }
222  else
223  {
224  LOG("Could not resolve expression in array", value);
225  return false;
226  }
227  }
228  return true;
229 }
230 
243  const index_exprt &index_expr, functionst &out_functions)
244 {
245  expressionst potential_array_values;
246  bool array_const;
247  bool resolved=
248  try_resolve_index_of(index_expr, potential_array_values, array_const);
249 
250  if(!resolved)
251  {
252  LOG("Could not resolve array", index_expr);
253  return false;
254  }
255 
256  if(!array_const)
257  {
258  LOG("Array not const", index_expr);
259  return false;
260  }
261 
262  return try_resolve_function_calls(potential_array_values, out_functions);
263 }
264 
275  const member_exprt &member_expr, functionst &out_functions)
276 {
277  expressionst potential_component_values;
278  bool struct_const;
279  bool resolved=
280  try_resolve_member(member_expr, potential_component_values, struct_const);
281 
282  if(!resolved)
283  {
284  LOG("Could not resolve struct", member_expr);
285  return false;
286  }
287 
288  if(!struct_const)
289  {
290  LOG("Struct was not const so can't resolve values on it", member_expr);
291  return false;
292  }
293 
294  return try_resolve_function_calls(potential_component_values, out_functions);
295 }
296 
306  const address_of_exprt &address_expr, functionst &out_functions)
307 {
308  bool resolved=
309  try_resolve_function_call(address_expr.object(), out_functions);
310  if(!resolved)
311  {
312  LOG("Failed to resolve address of", address_expr);
313  }
314  return resolved;
315 }
316 
327  const dereference_exprt &deref_expr, functionst &out_functions)
328 {
329  expressionst potential_deref_values;
330  bool deref_const;
331  bool resolved=
332  try_resolve_dereference(deref_expr, potential_deref_values, deref_const);
333 
334  if(!resolved)
335  {
336  LOG("Failed to squash dereference", deref_expr);
337  return false;
338  }
339 
340  if(!deref_const)
341  {
342  LOG("Dereferenced value was not const so can't dereference", deref_expr);
343  return false;
344  }
345 
346  return try_resolve_function_calls(potential_deref_values, out_functions);
347 }
348 
359  const typecast_exprt &typecast_expr, functionst &out_functions)
360 {
361  // We simply ignore typecasts and assume they are valid
362  // I thought simplify_expr would deal with this, but for example
363  // a cast from a 32 bit width int to a 64bit width int it doesn't seem
364  // to allow
365  functionst typecast_values;
366  bool resolved=
367  try_resolve_function_call(typecast_expr.op(), typecast_values);
368 
369  if(resolved)
370  {
371  out_functions.insert(typecast_values.begin(), typecast_values.end());
372  return true;
373  }
374  else
375  {
376  LOG("Failed to squash typecast", typecast_expr);
377  return false;
378  }
379 }
380 
396  const exprt &expr, expressionst &out_resolved_expression, bool &out_is_const)
397 {
398  exprt simplified_expr=simplify_expr(expr, ns);
399  bool resolved;
400  expressionst resolved_expressions;
401  bool is_resolved_expression_const = false;
402  if(simplified_expr.id()==ID_index)
403  {
404  const index_exprt &index_expr=to_index_expr(simplified_expr);
405  resolved=
407  index_expr, resolved_expressions, is_resolved_expression_const);
408  }
409  else if(simplified_expr.id()==ID_member)
410  {
411  const member_exprt &member_expr=to_member_expr(simplified_expr);
412  resolved=try_resolve_member(
413  member_expr, resolved_expressions, is_resolved_expression_const);
414  }
415  else if(simplified_expr.id()==ID_dereference)
416  {
417  const dereference_exprt &deref=to_dereference_expr(simplified_expr);
418  resolved=
420  deref, resolved_expressions, is_resolved_expression_const);
421  }
422  else if(simplified_expr.id()==ID_typecast)
423  {
424  typecast_exprt typecast_expr=to_typecast_expr(simplified_expr);
425  resolved=
427  typecast_expr, resolved_expressions, is_resolved_expression_const);
428  }
429  else if(simplified_expr.id()==ID_symbol)
430  {
431  LOG("Non const symbol will not be squashed", simplified_expr);
432  resolved=false;
433  }
434  else
435  {
436  resolved_expressions.push_back(simplified_expr);
437  is_resolved_expression_const=is_const_expression(simplified_expr);
438  resolved=true;
439  }
440 
441  if(resolved)
442  {
443  out_resolved_expression.insert(
444  out_resolved_expression.end(),
445  resolved_expressions.begin(),
446  resolved_expressions.end());
447  out_is_const=is_resolved_expression_const;
448  return true;
449  }
450  else
451  {
452  return false;
453  }
454 }
455 
465  const exprt &expr, mp_integer &out_array_index)
466 {
467  expressionst index_value_expressions;
468  bool is_const=false;
469  bool resolved=try_resolve_expression(expr, index_value_expressions, is_const);
470  if(resolved)
471  {
472  if(index_value_expressions.size()==1 &&
473  index_value_expressions.front().id()==ID_constant)
474  {
475  const constant_exprt &constant_expr=
476  to_constant_expr(index_value_expressions.front());
477  mp_integer array_index;
478  bool errors=to_integer(constant_expr, array_index);
479  if(!errors)
480  {
481  out_array_index=array_index;
482  }
483  return !errors;
484  }
485  else
486  {
487  return false;
488  }
489  }
490  else
491  {
492  return false;
493  }
494 }
495 
507  const index_exprt &index_expr,
508  expressionst &out_expressions,
509  bool &out_is_const)
510 {
511  // Get the array(s) it belongs to
512  expressionst potential_array_exprs;
513  bool array_const=false;
514  bool resolved_array=
516  index_expr.array(),
517  potential_array_exprs,
518  array_const);
519 
520  if(resolved_array)
521  {
522  bool all_possible_const=true;
523  for(const exprt &potential_array_expr : potential_array_exprs)
524  {
525  all_possible_const=
526  all_possible_const &&
527  is_const_type(potential_array_expr.type().subtype());
528 
529  if(potential_array_expr.id()==ID_array)
530  {
531  // Get the index if we can
532  mp_integer value;
533  if(try_resolve_index_value(index_expr.index(), value))
534  {
535  expressionst array_out_functions;
536  const exprt &func_expr=
537  potential_array_expr.operands()[integer2size_t(value)];
538  bool value_const=false;
539  bool resolved_value=
540  try_resolve_expression(func_expr, array_out_functions, value_const);
541 
542  if(resolved_value)
543  {
544  out_expressions.insert(
545  out_expressions.end(),
546  array_out_functions.begin(),
547  array_out_functions.end());
548  }
549  else
550  {
551  LOG("Failed to resolve array value", func_expr);
552  return false;
553  }
554  }
555  else
556  {
557  // We don't know what index it is,
558  // but we know the value is from the array
559  for(const exprt &array_entry : potential_array_expr.operands())
560  {
561  expressionst array_contents;
562  bool is_entry_const;
563  bool resolved_value=
565  array_entry, array_contents, is_entry_const);
566 
567  if(!resolved_value)
568  {
569  LOG("Failed to resolve array value", array_entry);
570  return false;
571  }
572 
573  for(const exprt &resolved_array_entry : array_contents)
574  {
575  out_expressions.push_back(resolved_array_entry);
576  }
577  }
578  }
579  }
580  else
581  {
582  LOG(
583  "Squashing index of did not result in an array",
584  potential_array_expr);
585  return false;
586  }
587  }
588 
589  out_is_const=all_possible_const || array_const;
590  return true;
591  }
592  else
593  {
594  LOG("Failed to squash index of to array expression", index_expr);
595  return false;
596  }
597 }
598 
608  const member_exprt &member_expr,
609  expressionst &out_expressions,
610  bool &out_is_const)
611 {
612  expressionst potential_structs;
613  bool is_struct_const;
614 
615  // Get the struct it belongs to
616  bool resolved_struct=
618  member_expr.compound(), potential_structs, is_struct_const);
619  if(resolved_struct)
620  {
621  for(const exprt &potential_struct : potential_structs)
622  {
623  if(potential_struct.id()==ID_struct)
624  {
625  struct_exprt struct_expr=to_struct_expr(potential_struct);
626  const exprt &component_value=
627  get_component_value(struct_expr, member_expr);
628  expressionst resolved_expressions;
629  bool component_const=false;
630  bool resolved=
632  component_value, resolved_expressions, component_const);
633  if(resolved)
634  {
635  out_expressions.insert(
636  out_expressions.end(),
637  resolved_expressions.begin(),
638  resolved_expressions.end());
639  }
640  else
641  {
642  LOG("Could not resolve component value", component_value);
643  return false;
644  }
645  }
646  else
647  {
648  LOG(
649  "Squashing member access did not resolve in a struct",
650  potential_struct);
651  return false;
652  }
653  }
654  out_is_const=is_struct_const;
655  return true;
656  }
657  else
658  {
659  LOG("Failed to squash struct access", member_expr);
660  return false;
661  }
662 }
663 
675  const dereference_exprt &deref_expr,
676  expressionst &out_expressions,
677  bool &out_is_const)
678 {
679  // We had a pointer, we need to check both the pointer
680  // type can't be changed, and what it what pointing to
681  // can't be changed
682  expressionst pointer_values;
683  bool pointer_const;
684  bool resolved=
685  try_resolve_expression(deref_expr.pointer(), pointer_values, pointer_const);
686  if(resolved && pointer_const)
687  {
688  bool all_objects_const=true;
689  for(const exprt &pointer_val : pointer_values)
690  {
691  if(pointer_val.id()==ID_address_of)
692  {
693  address_of_exprt address_expr=to_address_of_expr(pointer_val);
694  bool object_const=false;
695  expressionst out_object_values;
696  bool resolved=
698  address_expr.object(), out_object_values, object_const);
699 
700  if(resolved)
701  {
702  out_expressions.insert(
703  out_expressions.end(),
704  out_object_values.begin(),
705  out_object_values.end());
706 
707  all_objects_const&=object_const;
708  }
709  else
710  {
711  LOG("Failed to resolve value of a dereference", address_expr);
712  }
713  }
714  else
715  {
716  LOG(
717  "Squashing dereference did not result in an address", pointer_val);
718  return false;
719  }
720  }
721  out_is_const=all_objects_const;
722  return true;
723  }
724  else
725  {
726  if(!resolved)
727  {
728  LOG("Failed to resolve pointer of dereference", deref_expr);
729  }
730  else if(!pointer_const)
731  {
732  LOG("Pointer value not const so can't squash", deref_expr);
733  }
734  return false;
735  }
736 }
737 
746  const typecast_exprt &typecast_expr,
747  expressionst &out_expressions,
748  bool &out_is_const)
749 {
750  expressionst typecast_values;
751  bool typecast_const;
752  bool resolved=
754  typecast_expr.op(), typecast_values, typecast_const);
755 
756  if(resolved)
757  {
758  out_expressions.insert(
759  out_expressions.end(),
760  typecast_values.begin(),
761  typecast_values.end());
762  out_is_const=typecast_const;
763  return true;
764  }
765  else
766  {
767  LOG("Could not resolve typecast value", typecast_expr);
768  return false;
769  }
770 }
771 
776  const exprt &expression) const
777 {
778  return is_const_type(expression.type());
779 }
780 
786 {
787  if(type.id() == ID_array && type.subtype().get_bool(ID_C_constant))
788  return true;
789 
790  return type.get_bool(ID_C_constant);
791 }
792 
799  const struct_exprt &struct_expr, const member_exprt &member_expr)
800 {
801  const struct_typet &struct_type=to_struct_type(ns.follow(struct_expr.type()));
802  size_t component_number=
803  struct_type.component_number(member_expr.get_component_name());
804 
805  return struct_expr.operands()[component_number];
806 }
exprt replace_const_symbols(const exprt &expression) const
To collapse the symbols down to their values where possible This takes a very general approach...
The type of an expression.
Definition: type.h:22
semantic type conversion
Definition: std_expr.h:2111
remove_const_function_pointerst(message_handlert &message_handler, const namespacet &ns, const symbol_tablet &symbol_table)
To take a function call on a function pointer, and if possible resolve it to a small collection of po...
BigInt mp_integer
Definition: mp_arith.h:22
exprt & object()
Definition: std_expr.h:3178
bool try_resolve_typecast_function_call(const typecast_exprt &typecast_expr, functionst &out_functions)
To resolve an expression to the specific function calls it can be.
exprt get_component_value(const struct_exprt &struct_expr, const member_exprt &member_expr)
To extract the value of the specific component within a struct.
exprt simplify_expr(const exprt &src, const namespacet &ns)
bool try_resolve_member_function_call(const member_exprt &member_expr, functionst &out_functions)
To resolve an expression to the specific function calls it can be.
bool try_resolve_index_of(const index_exprt &index_expr, expressionst &out_expressions, bool &out_is_const)
To squash an index access by first finding the array it is accessing Then if the index can be resolve...
const exprt & op() const
Definition: std_expr.h:340
const irep_idt & get_identifier() const
Definition: std_expr.h:128
Goto Programs with Functions.
bool try_resolve_typecast(const typecast_exprt &typecast_expr, expressionst &out_expressions, bool &out_is_const)
To squash a typecast access.
exprt value
Initial value of symbol.
Definition: symbol.h:37
bool try_resolve_dereference(const dereference_exprt &deref_expr, expressionst &out_expressions, bool &out_is_const)
To squash a dereference access by first finding the address_of the dereference is dereferencing...
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
A constant literal expression.
Definition: std_expr.h:4422
Structure type.
Definition: std_types.h:297
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Definition: std_expr.h:3326
Extract member of struct or union.
Definition: std_expr.h:3869
bool try_resolve_function_calls(const expressionst &exprs, functionst &out_functions)
To resolve a collection of expressions to the specific function calls they can be.
const exprt & compound() const
Definition: std_expr.h:3920
const irep_idt & id() const
Definition: irep.h:259
bool try_resolve_member(const member_exprt &member_expr, expressionst &out_expressions, bool &out_is_const)
To squash an member access by first finding the struct it is accessing Then return the squashed value...
bool try_resolve_expression(const exprt &expr, expressionst &out_resolved_expression, bool &out_is_const)
To squash various expr types to simplify the expression.
exprt resolve_symbol(const symbol_exprt &symbol_expr) const
Look up a symbol in the symbol table and return its value.
bool is_const_expression(const exprt &expression) const
To evaluate the const-ness of the expression type.
bool try_resolve_index_value(const exprt &index_value_expr, mp_integer &out_array_index)
Given an index into an array, resolve, if possible, the index that is being accessed.
Operator to dereference a pointer.
Definition: std_expr.h:3282
API to expression classes.
The symbol table.
Definition: symbol_table.h:19
bool try_resolve_index_of_function_call(const index_exprt &index_expr, functionst &out_functions)
To resolve an expression to the specific function calls it can be.
TO_BE_DOCUMENTED.
Definition: namespace.h:74
#define LOG(message, irep)
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3953
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
bool operator()(const exprt &base_expression, functionst &out_functions)
To take a function call on a function pointer, and if possible resolve it to a small collection of po...
const typet & follow(const typet &) const
Definition: namespace.cpp:55
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
Author: Diffblue Ltd.
Operator to return the address of an object.
Definition: std_expr.h:3168
const struct_exprt & to_struct_expr(const exprt &expr)
Cast a generic exprt to a struct_exprt.
Definition: std_expr.h:1838
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4463
typet type
Type of symbol.
Definition: symbol.h:34
bool try_resolve_dereference_function_call(const dereference_exprt &deref_expr, functionst &out_functions)
To resolve an expression to the specific function calls it can be.
bool try_resolve_address_of_function_call(const address_of_exprt &address_expr, functionst &out_functions)
To resolve an expression to the specific function calls it can be.
exprt & index()
Definition: std_expr.h:1496
Base class for all expressions.
Definition: expr.h:42
exprt & pointer()
Definition: std_expr.h:3305
std::size_t component_number(const irep_idt &component_name) const
Definition: std_types.cpp:29
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
std::unordered_set< symbol_exprt, irep_hash > functionst
Expression to hold a symbol (variable)
Definition: std_expr.h:90
bool try_resolve_function_call(const exprt &expr, functionst &out_functions)
To resolve an expression to the specific function calls it can be.
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
const typet & subtype() const
Definition: type.h:33
operandst & operands()
Definition: expr.h:66
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
struct constructor from list of elements
Definition: std_expr.h:1815
exprt & array()
Definition: std_expr.h:1486
bool is_const_type(const typet &type) const
To evaluate the const-ness of the type.
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
array index operator
Definition: std_expr.h:1462