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