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/format_expr.h>
16 #include <util/pointer_expr.h>
17 #include <util/simplify_expr.h>
18 #include <util/std_expr.h>
19 #include <util/symbol_table.h>
20 
21 #include "goto_functions.h"
22 
23 #define LOG(message, irep) \
24  do \
25  { \
26  log.debug().source_location = irep.source_location(); \
27  log.debug() << message << ": " << format(irep) << messaget::eom; \
28  } while(0)
29 
36  message_handlert &message_handler,
37  const namespacet &ns,
38  const symbol_tablet &symbol_table)
39  : log(message_handler), ns(ns), symbol_table(symbol_table)
40 {}
41 
54  const exprt &base_expression,
55  functionst &out_functions)
56 {
57  // Replace all const symbols with their values
58  exprt non_symbol_expression=replace_const_symbols(base_expression);
59  return try_resolve_function_call(non_symbol_expression, out_functions);
60 }
61 
70  const exprt &expression) const
71 {
72  if(expression.id()==ID_symbol)
73  {
74  if(is_const_expression(expression))
75  {
76  const symbolt &symbol =
77  symbol_table.lookup_ref(to_symbol_expr(expression).get_identifier());
78  if(symbol.type.id()!=ID_code)
79  {
80  const exprt &symbol_value=symbol.value;
81  return replace_const_symbols(symbol_value);
82  }
83  else
84  {
85  return expression;
86  }
87  }
88  else
89  {
90  return expression;
91  }
92  }
93  else
94  {
95  exprt const_symbol_cleared_expr=expression;
96  const_symbol_cleared_expr.operands().clear();
97  for(const exprt &op : expression.operands())
98  {
99  exprt const_symbol_cleared_op=replace_const_symbols(op);
100  const_symbol_cleared_expr.operands().push_back(const_symbol_cleared_op);
101  }
102 
103  return const_symbol_cleared_expr;
104  }
105 }
106 
111  const symbol_exprt &symbol_expr) const
112 {
113  const symbolt &symbol = symbol_table.lookup_ref(symbol_expr.get_identifier());
114  return symbol.value;
115 }
116 
126  const exprt &expr, functionst &out_functions)
127 {
128  PRECONDITION(out_functions.empty());
129  const exprt &simplified_expr=simplify_expr(expr, ns);
130  bool resolved=false;
131  functionst resolved_functions;
132  if(simplified_expr.id()==ID_index)
133  {
134  const index_exprt &index_expr=to_index_expr(simplified_expr);
135  resolved=try_resolve_index_of_function_call(index_expr, resolved_functions);
136  }
137  else if(simplified_expr.id()==ID_member)
138  {
139  const member_exprt &member_expr=to_member_expr(simplified_expr);
140  resolved=try_resolve_member_function_call(member_expr, resolved_functions);
141  }
142  else if(simplified_expr.id()==ID_address_of)
143  {
144  address_of_exprt address_expr=to_address_of_expr(simplified_expr);
146  address_expr, resolved_functions);
147  }
148  else if(simplified_expr.id()==ID_dereference)
149  {
150  const dereference_exprt &deref=to_dereference_expr(simplified_expr);
151  resolved=try_resolve_dereference_function_call(deref, resolved_functions);
152  }
153  else if(simplified_expr.id()==ID_typecast)
154  {
155  typecast_exprt typecast_expr=to_typecast_expr(simplified_expr);
156  resolved=
157  try_resolve_typecast_function_call(typecast_expr, resolved_functions);
158  }
159  else if(simplified_expr.id()==ID_symbol)
160  {
161  if(simplified_expr.type().id()==ID_code)
162  {
163  resolved_functions.insert(to_symbol_expr(simplified_expr));
164  resolved=true;
165  }
166  else
167  {
168  LOG("Non const symbol wasn't squashed", simplified_expr);
169  resolved=false;
170  }
171  }
172  else if(simplified_expr.id()==ID_constant)
173  {
174  if(simplified_expr.is_zero())
175  {
176  // We have the null pointer - no need to throw everything away
177  // but we don't add any functions either
178  resolved=true;
179  }
180  else
181  {
182  LOG("Non-zero constant value found", simplified_expr);
183  resolved=false;
184  }
185  }
186  else
187  {
188  LOG("Unrecognised expression", simplified_expr);
189  resolved=false;
190  }
191 
192  if(resolved)
193  {
194  out_functions.insert(resolved_functions.begin(), resolved_functions.end());
195  return true;
196  }
197  else
198  {
199  return false;
200  }
201 }
202 
210  const expressionst &exprs, functionst &out_functions)
211 {
212  for(const exprt &value : exprs)
213  {
214  functionst potential_out_functions;
215  bool resolved_value=
216  try_resolve_function_call(value, potential_out_functions);
217 
218  if(resolved_value)
219  {
220  out_functions.insert(
221  potential_out_functions.begin(),
222  potential_out_functions.end());
223  }
224  else
225  {
226  LOG("Could not resolve expression in array", value);
227  return false;
228  }
229  }
230  return true;
231 }
232 
245  const index_exprt &index_expr, functionst &out_functions)
246 {
247  expressionst potential_array_values;
248  bool array_const;
249  bool resolved=
250  try_resolve_index_of(index_expr, potential_array_values, array_const);
251 
252  if(!resolved)
253  {
254  LOG("Could not resolve array", index_expr);
255  return false;
256  }
257 
258  if(!array_const)
259  {
260  LOG("Array not const", index_expr);
261  return false;
262  }
263 
264  return try_resolve_function_calls(potential_array_values, out_functions);
265 }
266 
277  const member_exprt &member_expr, functionst &out_functions)
278 {
279  expressionst potential_component_values;
280  bool struct_const;
281  bool resolved=
282  try_resolve_member(member_expr, potential_component_values, struct_const);
283 
284  if(!resolved)
285  {
286  LOG("Could not resolve struct", member_expr);
287  return false;
288  }
289 
290  if(!struct_const)
291  {
292  LOG("Struct was not const so can't resolve values on it", member_expr);
293  return false;
294  }
295 
296  return try_resolve_function_calls(potential_component_values, out_functions);
297 }
298 
308  const address_of_exprt &address_expr, functionst &out_functions)
309 {
310  bool resolved=
311  try_resolve_function_call(address_expr.object(), out_functions);
312  if(!resolved)
313  {
314  LOG("Failed to resolve address of", address_expr);
315  }
316  return resolved;
317 }
318 
329  const dereference_exprt &deref_expr, functionst &out_functions)
330 {
331  expressionst potential_deref_values;
332  bool deref_const;
333  bool resolved=
334  try_resolve_dereference(deref_expr, potential_deref_values, deref_const);
335 
336  if(!resolved)
337  {
338  LOG("Failed to squash dereference", deref_expr);
339  return false;
340  }
341 
342  if(!deref_const)
343  {
344  LOG("Dereferenced value was not const so can't dereference", deref_expr);
345  return false;
346  }
347 
348  return try_resolve_function_calls(potential_deref_values, out_functions);
349 }
350 
361  const typecast_exprt &typecast_expr, functionst &out_functions)
362 {
363  // We simply ignore typecasts and assume they are valid
364  // I thought simplify_expr would deal with this, but for example
365  // a cast from a 32 bit width int to a 64bit width int it doesn't seem
366  // to allow
367  functionst typecast_values;
368  bool resolved=
369  try_resolve_function_call(typecast_expr.op(), typecast_values);
370 
371  if(resolved)
372  {
373  out_functions.insert(typecast_values.begin(), typecast_values.end());
374  return true;
375  }
376  else
377  {
378  LOG("Failed to squash typecast", typecast_expr);
379  return false;
380  }
381 }
382 
398  const exprt &expr, expressionst &out_resolved_expression, bool &out_is_const)
399 {
400  exprt simplified_expr=simplify_expr(expr, ns);
401  bool resolved;
402  expressionst resolved_expressions;
403  bool is_resolved_expression_const = false;
404  if(simplified_expr.id()==ID_index)
405  {
406  const index_exprt &index_expr=to_index_expr(simplified_expr);
407  resolved=
409  index_expr, resolved_expressions, is_resolved_expression_const);
410  }
411  else if(simplified_expr.id()==ID_member)
412  {
413  const member_exprt &member_expr=to_member_expr(simplified_expr);
414  resolved=try_resolve_member(
415  member_expr, resolved_expressions, is_resolved_expression_const);
416  }
417  else if(simplified_expr.id()==ID_dereference)
418  {
419  const dereference_exprt &deref=to_dereference_expr(simplified_expr);
420  resolved=
422  deref, resolved_expressions, is_resolved_expression_const);
423  }
424  else if(simplified_expr.id()==ID_typecast)
425  {
426  typecast_exprt typecast_expr=to_typecast_expr(simplified_expr);
427  resolved=
429  typecast_expr, resolved_expressions, is_resolved_expression_const);
430  }
431  else if(simplified_expr.id()==ID_symbol)
432  {
433  LOG("Non const symbol will not be squashed", simplified_expr);
434  resolved=false;
435  }
436  else
437  {
438  resolved_expressions.push_back(simplified_expr);
439  is_resolved_expression_const=is_const_expression(simplified_expr);
440  resolved=true;
441  }
442 
443  if(resolved)
444  {
445  out_resolved_expression.insert(
446  out_resolved_expression.end(),
447  resolved_expressions.begin(),
448  resolved_expressions.end());
449  out_is_const=is_resolved_expression_const;
450  return true;
451  }
452  else
453  {
454  return false;
455  }
456 }
457 
467  const exprt &expr, mp_integer &out_array_index)
468 {
469  expressionst index_value_expressions;
470  bool is_const=false;
471  bool resolved=try_resolve_expression(expr, index_value_expressions, is_const);
472  if(resolved)
473  {
474  if(index_value_expressions.size()==1 &&
475  index_value_expressions.front().id()==ID_constant)
476  {
477  const constant_exprt &constant_expr=
478  to_constant_expr(index_value_expressions.front());
479  mp_integer array_index;
480  bool errors=to_integer(constant_expr, array_index);
481  if(!errors)
482  {
483  out_array_index=array_index;
484  }
485  return !errors;
486  }
487  else
488  {
489  return false;
490  }
491  }
492  else
493  {
494  return false;
495  }
496 }
497 
509  const index_exprt &index_expr,
510  expressionst &out_expressions,
511  bool &out_is_const)
512 {
513  // Get the array(s) it belongs to
514  expressionst potential_array_exprs;
515  bool array_const=false;
516  bool resolved_array=
518  index_expr.array(),
519  potential_array_exprs,
520  array_const);
521 
522  if(resolved_array)
523  {
524  bool all_possible_const=true;
525  for(const exprt &potential_array_expr : potential_array_exprs)
526  {
527  all_possible_const=
528  all_possible_const &&
529  is_const_type(potential_array_expr.type().subtype());
530 
531  if(potential_array_expr.id()==ID_array)
532  {
533  // Get the index if we can
534  mp_integer value;
535  if(try_resolve_index_value(index_expr.index(), value))
536  {
537  expressionst array_out_functions;
538  const exprt &func_expr =
539  potential_array_expr.operands()[numeric_cast_v<std::size_t>(value)];
540  bool value_const=false;
541  bool resolved_value=
542  try_resolve_expression(func_expr, array_out_functions, value_const);
543 
544  if(resolved_value)
545  {
546  out_expressions.insert(
547  out_expressions.end(),
548  array_out_functions.begin(),
549  array_out_functions.end());
550  }
551  else
552  {
553  LOG("Failed to resolve array value", func_expr);
554  return false;
555  }
556  }
557  else
558  {
559  // We don't know what index it is,
560  // but we know the value is from the array
561  for(const exprt &array_entry : potential_array_expr.operands())
562  {
563  expressionst array_contents;
564  bool is_entry_const;
565  bool resolved_value=
567  array_entry, array_contents, is_entry_const);
568 
569  if(!resolved_value)
570  {
571  LOG("Failed to resolve array value", array_entry);
572  return false;
573  }
574 
575  for(const exprt &resolved_array_entry : array_contents)
576  {
577  out_expressions.push_back(resolved_array_entry);
578  }
579  }
580  }
581  }
582  else
583  {
584  LOG(
585  "Squashing index of did not result in an array",
586  potential_array_expr);
587  return false;
588  }
589  }
590 
591  out_is_const=all_possible_const || array_const;
592  return true;
593  }
594  else
595  {
596  LOG("Failed to squash index of to array expression", index_expr);
597  return false;
598  }
599 }
600 
610  const member_exprt &member_expr,
611  expressionst &out_expressions,
612  bool &out_is_const)
613 {
614  expressionst potential_structs;
615  bool is_struct_const;
616 
617  // Get the struct it belongs to
618  bool resolved_struct=
620  member_expr.compound(), potential_structs, is_struct_const);
621  if(resolved_struct)
622  {
623  for(const exprt &potential_struct : potential_structs)
624  {
625  if(potential_struct.id()==ID_struct)
626  {
627  struct_exprt struct_expr=to_struct_expr(potential_struct);
628  const exprt &component_value=
629  get_component_value(struct_expr, member_expr);
630  expressionst resolved_expressions;
631  bool component_const=false;
632  bool resolved=
634  component_value, resolved_expressions, component_const);
635  if(resolved)
636  {
637  out_expressions.insert(
638  out_expressions.end(),
639  resolved_expressions.begin(),
640  resolved_expressions.end());
641  }
642  else
643  {
644  LOG("Could not resolve component value", component_value);
645  return false;
646  }
647  }
648  else
649  {
650  LOG(
651  "Squashing member access did not resolve in a struct",
652  potential_struct);
653  return false;
654  }
655  }
656  out_is_const=is_struct_const;
657  return true;
658  }
659  else
660  {
661  LOG("Failed to squash struct access", member_expr);
662  return false;
663  }
664 }
665 
677  const dereference_exprt &deref_expr,
678  expressionst &out_expressions,
679  bool &out_is_const)
680 {
681  // We had a pointer, we need to check both the pointer
682  // type can't be changed, and what it what pointing to
683  // can't be changed
684  expressionst pointer_values;
685  bool pointer_const;
686  bool resolved=
687  try_resolve_expression(deref_expr.pointer(), pointer_values, pointer_const);
688  if(resolved && pointer_const)
689  {
690  bool all_objects_const=true;
691  for(const exprt &pointer_val : pointer_values)
692  {
693  if(pointer_val.id()==ID_address_of)
694  {
695  address_of_exprt address_expr=to_address_of_expr(pointer_val);
696  bool object_const=false;
697  expressionst out_object_values;
698  const bool resolved_address = try_resolve_expression(
699  address_expr.object(), out_object_values, object_const);
700 
701  if(resolved_address)
702  {
703  out_expressions.insert(
704  out_expressions.end(),
705  out_object_values.begin(),
706  out_object_values.end());
707 
708  all_objects_const&=object_const;
709  }
710  else
711  {
712  LOG("Failed to resolve value of a dereference", address_expr);
713  }
714  }
715  else
716  {
717  LOG(
718  "Squashing dereference did not result in an address", pointer_val);
719  return false;
720  }
721  }
722  out_is_const=all_objects_const;
723  return true;
724  }
725  else
726  {
727  if(!resolved)
728  {
729  LOG("Failed to resolve pointer of dereference", deref_expr);
730  }
731  else if(!pointer_const)
732  {
733  LOG("Pointer value not const so can't squash", deref_expr);
734  }
735  return false;
736  }
737 }
738 
747  const typecast_exprt &typecast_expr,
748  expressionst &out_expressions,
749  bool &out_is_const)
750 {
751  expressionst typecast_values;
752  bool typecast_const;
753  bool resolved=
755  typecast_expr.op(), typecast_values, typecast_const);
756 
757  if(resolved)
758  {
759  out_expressions.insert(
760  out_expressions.end(),
761  typecast_values.begin(),
762  typecast_values.end());
763  out_is_const=typecast_const;
764  return true;
765  }
766  else
767  {
768  LOG("Could not resolve typecast value", typecast_expr);
769  return false;
770  }
771 }
772 
777  const exprt &expression) const
778 {
779  return is_const_type(expression.type());
780 }
781 
787 {
788  if(type.id() == ID_array && type.subtype().get_bool(ID_C_constant))
789  return true;
790 
791  return type.get_bool(ID_C_constant);
792 }
793 
800  const struct_exprt &struct_expr, const member_exprt &member_expr)
801 {
802  const struct_typet &struct_type=to_struct_type(ns.follow(struct_expr.type()));
803  size_t component_number=
804  struct_type.component_number(member_expr.get_component_name());
805 
806  return struct_expr.operands()[component_number];
807 }
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:19
Operator to return the address of an object.
Definition: pointer_expr.h:200
exprt & object()
Definition: pointer_expr.h:209
A constant literal expression.
Definition: std_expr.h:2668
Operator to dereference a pointer.
Definition: pointer_expr.h:256
Base class for all expressions.
Definition: expr.h:54
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:78
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:96
Array index operator.
Definition: std_expr.h:1243
exprt & array()
Definition: std_expr.h:1259
exprt & index()
Definition: std_expr.h:1269
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
const irep_idt & id() const
Definition: irep.h:407
Extract member of struct or union.
Definition: std_expr.h:2528
const exprt & compound() const
Definition: std_expr.h:2569
irep_idt get_component_name() const
Definition: std_expr.h:2542
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
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...
bool try_resolve_function_call(const exprt &expr, functionst &out_functions)
To resolve an expression to the specific function calls it can be.
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.
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 get_component_value(const struct_exprt &struct_expr, const member_exprt &member_expr)
To extract the value of the specific component within a struct.
bool try_resolve_typecast(const typecast_exprt &typecast_expr, expressionst &out_expressions, bool &out_is_const)
To squash a typecast access.
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_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 is_const_type(const typet &type) const
To evaluate the const-ness of the type.
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.
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.
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...
bool is_const_expression(const exprt &expression) const
To evaluate the const-ness of the expression type.
std::unordered_set< symbol_exprt, irep_hash > functionst
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.
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.
exprt resolve_symbol(const symbol_exprt &symbol_expr) const
Look up a symbol in the symbol table and return its value.
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...
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.
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 replace_const_symbols(const exprt &expression) const
To collapse the symbols down to their values where possible This takes a very general approach,...
Struct constructor from list of elements.
Definition: std_expr.h:1583
Structure type, corresponds to C style structs.
Definition: std_types.h:226
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
Definition: std_types.cpp:50
Expression to hold a symbol (variable)
Definition: std_expr.h:81
const irep_idt & get_identifier() const
Definition: std_expr.h:110
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
Definition: symbol_table.h:20
Symbol table entry.
Definition: symbol.h:28
typet type
Type of symbol.
Definition: symbol.h:31
exprt value
Initial value of symbol.
Definition: symbol.h:34
Semantic type conversion.
Definition: std_expr.h:1781
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:294
Goto Programs with Functions.
BigInt mp_integer
Definition: mp_arith.h:19
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:312
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:237
#define LOG(message, irep)
exprt simplify_expr(exprt src, const namespacet &ns)
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2701
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1815
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1606
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
Author: Diffblue Ltd.