CBMC
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/namespace.h>
17 #include <util/pointer_expr.h>
18 #include <util/simplify_expr.h>
19 #include <util/std_expr.h>
20 #include <util/symbol_table_base.h>
21 
22 #define LOG(message, irep) \
23  do \
24  { \
25  log.debug().source_location = irep.source_location(); \
26  log.debug() << message << ": " << format(irep) << messaget::eom; \
27  } while(0)
28 
35  message_handlert &message_handler,
36  const namespacet &ns,
37  const symbol_table_baset &symbol_table)
38  : log(message_handler), ns(ns), symbol_table(symbol_table)
39 {}
40 
53  const exprt &base_expression,
54  functionst &out_functions)
55 {
56  // Replace all const symbols with their values
57  exprt non_symbol_expression=replace_const_symbols(base_expression);
58  return try_resolve_function_call(non_symbol_expression, out_functions);
59 }
60 
69  const exprt &expression) const
70 {
71  if(expression.id()==ID_symbol)
72  {
73  if(is_const_expression(expression))
74  {
75  const symbolt &symbol =
76  symbol_table.lookup_ref(to_symbol_expr(expression).get_identifier());
77  if(symbol.type.id() != ID_code && symbol.value.is_not_nil())
78  {
79  const exprt &symbol_value=symbol.value;
80  return replace_const_symbols(symbol_value);
81  }
82  else
83  {
84  return expression;
85  }
86  }
87  else
88  {
89  return expression;
90  }
91  }
92  else
93  {
94  exprt const_symbol_cleared_expr=expression;
95  const_symbol_cleared_expr.operands().clear();
96  for(const exprt &op : expression.operands())
97  {
98  exprt const_symbol_cleared_op=replace_const_symbols(op);
99  const_symbol_cleared_expr.operands().push_back(const_symbol_cleared_op);
100  }
101 
102  return const_symbol_cleared_expr;
103  }
104 }
105 
110  const symbol_exprt &symbol_expr) const
111 {
112  const symbolt &symbol = symbol_table.lookup_ref(symbol_expr.get_identifier());
113  return symbol.value;
114 }
115 
125  const exprt &expr, functionst &out_functions)
126 {
127  PRECONDITION(out_functions.empty());
128  const exprt &simplified_expr=simplify_expr(expr, ns);
129  bool resolved=false;
130  functionst resolved_functions;
131  if(simplified_expr.id()==ID_index)
132  {
133  const index_exprt &index_expr=to_index_expr(simplified_expr);
134  resolved=try_resolve_index_of_function_call(index_expr, resolved_functions);
135  }
136  else if(simplified_expr.id()==ID_member)
137  {
138  const member_exprt &member_expr=to_member_expr(simplified_expr);
139  resolved=try_resolve_member_function_call(member_expr, resolved_functions);
140  }
141  else if(simplified_expr.id()==ID_address_of)
142  {
143  address_of_exprt address_expr=to_address_of_expr(simplified_expr);
145  address_expr, resolved_functions);
146  }
147  else if(simplified_expr.id()==ID_dereference)
148  {
149  const dereference_exprt &deref=to_dereference_expr(simplified_expr);
150  resolved=try_resolve_dereference_function_call(deref, resolved_functions);
151  }
152  else if(simplified_expr.id()==ID_typecast)
153  {
154  typecast_exprt typecast_expr=to_typecast_expr(simplified_expr);
155  resolved=
156  try_resolve_typecast_function_call(typecast_expr, resolved_functions);
157  }
158  else if(simplified_expr.id()==ID_symbol)
159  {
160  if(simplified_expr.type().id()==ID_code)
161  {
162  resolved_functions.insert(to_symbol_expr(simplified_expr));
163  resolved=true;
164  }
165  else
166  {
167  LOG("Non const symbol wasn't squashed", simplified_expr);
168  resolved=false;
169  }
170  }
171  else if(simplified_expr.is_constant())
172  {
173  if(simplified_expr.is_zero())
174  {
175  // We have the null pointer - no need to throw everything away
176  // but we don't add any functions either
177  resolved=true;
178  }
179  else
180  {
181  LOG("Non-zero constant value found", simplified_expr);
182  resolved=false;
183  }
184  }
185  else
186  {
187  LOG("Unrecognised expression", simplified_expr);
188  resolved=false;
189  }
190 
191  if(resolved)
192  {
193  out_functions.insert(resolved_functions.begin(), resolved_functions.end());
194  return true;
195  }
196  else
197  {
198  return false;
199  }
200 }
201 
209  const expressionst &exprs, functionst &out_functions)
210 {
211  for(const exprt &value : exprs)
212  {
213  functionst potential_out_functions;
214  bool resolved_value=
215  try_resolve_function_call(value, potential_out_functions);
216 
217  if(resolved_value)
218  {
219  out_functions.insert(
220  potential_out_functions.begin(),
221  potential_out_functions.end());
222  }
223  else
224  {
225  LOG("Could not resolve expression in array", value);
226  return false;
227  }
228  }
229  return true;
230 }
231 
244  const index_exprt &index_expr, functionst &out_functions)
245 {
246  expressionst potential_array_values;
247  bool array_const;
248  bool resolved=
249  try_resolve_index_of(index_expr, potential_array_values, array_const);
250 
251  if(!resolved)
252  {
253  LOG("Could not resolve array", index_expr);
254  return false;
255  }
256 
257  if(!array_const)
258  {
259  LOG("Array not const", index_expr);
260  return false;
261  }
262 
263  return try_resolve_function_calls(potential_array_values, out_functions);
264 }
265 
276  const member_exprt &member_expr, functionst &out_functions)
277 {
278  expressionst potential_component_values;
279  bool struct_const;
280  bool resolved=
281  try_resolve_member(member_expr, potential_component_values, struct_const);
282 
283  if(!resolved)
284  {
285  LOG("Could not resolve struct", member_expr);
286  return false;
287  }
288 
289  if(!struct_const)
290  {
291  LOG("Struct was not const so can't resolve values on it", member_expr);
292  return false;
293  }
294 
295  return try_resolve_function_calls(potential_component_values, out_functions);
296 }
297 
307  const address_of_exprt &address_expr, functionst &out_functions)
308 {
309  bool resolved=
310  try_resolve_function_call(address_expr.object(), out_functions);
311  if(!resolved)
312  {
313  LOG("Failed to resolve address of", address_expr);
314  }
315  return resolved;
316 }
317 
328  const dereference_exprt &deref_expr, functionst &out_functions)
329 {
330  expressionst potential_deref_values;
331  bool deref_const;
332  bool resolved=
333  try_resolve_dereference(deref_expr, potential_deref_values, deref_const);
334 
335  if(!resolved)
336  {
337  LOG("Failed to squash dereference", deref_expr);
338  return false;
339  }
340 
341  if(!deref_const)
342  {
343  LOG("Dereferenced value was not const so can't dereference", deref_expr);
344  return false;
345  }
346 
347  return try_resolve_function_calls(potential_deref_values, out_functions);
348 }
349 
360  const typecast_exprt &typecast_expr, functionst &out_functions)
361 {
362  // We simply ignore typecasts and assume they are valid
363  // I thought simplify_expr would deal with this, but for example
364  // a cast from a 32 bit width int to a 64bit width int it doesn't seem
365  // to allow
366  functionst typecast_values;
367  bool resolved=
368  try_resolve_function_call(typecast_expr.op(), typecast_values);
369 
370  if(resolved)
371  {
372  out_functions.insert(typecast_values.begin(), typecast_values.end());
373  return true;
374  }
375  else
376  {
377  LOG("Failed to squash typecast", typecast_expr);
378  return false;
379  }
380 }
381 
397  const exprt &expr, expressionst &out_resolved_expression, bool &out_is_const)
398 {
399  exprt simplified_expr=simplify_expr(expr, ns);
400  bool resolved;
401  expressionst resolved_expressions;
402  bool is_resolved_expression_const = false;
403  if(simplified_expr.id()==ID_index)
404  {
405  const index_exprt &index_expr=to_index_expr(simplified_expr);
406  resolved=
408  index_expr, resolved_expressions, is_resolved_expression_const);
409  }
410  else if(simplified_expr.id()==ID_member)
411  {
412  const member_exprt &member_expr=to_member_expr(simplified_expr);
413  resolved=try_resolve_member(
414  member_expr, resolved_expressions, is_resolved_expression_const);
415  }
416  else if(simplified_expr.id()==ID_dereference)
417  {
418  const dereference_exprt &deref=to_dereference_expr(simplified_expr);
419  resolved=
421  deref, resolved_expressions, is_resolved_expression_const);
422  }
423  else if(simplified_expr.id()==ID_typecast)
424  {
425  typecast_exprt typecast_expr=to_typecast_expr(simplified_expr);
426  resolved=
428  typecast_expr, resolved_expressions, is_resolved_expression_const);
429  }
430  else if(simplified_expr.id()==ID_symbol)
431  {
432  LOG("Non const symbol will not be squashed", simplified_expr);
433  resolved=false;
434  }
435  else
436  {
437  resolved_expressions.push_back(simplified_expr);
438  is_resolved_expression_const=is_const_expression(simplified_expr);
439  resolved=true;
440  }
441 
442  if(resolved)
443  {
444  out_resolved_expression.insert(
445  out_resolved_expression.end(),
446  resolved_expressions.begin(),
447  resolved_expressions.end());
448  out_is_const=is_resolved_expression_const;
449  return true;
450  }
451  else
452  {
453  return false;
454  }
455 }
456 
466  const exprt &expr, mp_integer &out_array_index)
467 {
468  expressionst index_value_expressions;
469  bool is_const=false;
470  bool resolved=try_resolve_expression(expr, index_value_expressions, is_const);
471  if(resolved)
472  {
473  if(
474  index_value_expressions.size() == 1 &&
475  index_value_expressions.front().is_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 &&
530  to_array_type(potential_array_expr.type()).element_type());
531 
532  if(potential_array_expr.id()==ID_array)
533  {
534  // Get the index if we can
535  mp_integer value;
536  if(try_resolve_index_value(index_expr.index(), value))
537  {
538  expressionst array_out_functions;
539  const exprt &func_expr =
540  potential_array_expr.operands()[numeric_cast_v<std::size_t>(value)];
541  bool value_const=false;
542  bool resolved_value=
543  try_resolve_expression(func_expr, array_out_functions, value_const);
544 
545  if(resolved_value)
546  {
547  out_expressions.insert(
548  out_expressions.end(),
549  array_out_functions.begin(),
550  array_out_functions.end());
551  }
552  else
553  {
554  LOG("Failed to resolve array value", func_expr);
555  return false;
556  }
557  }
558  else
559  {
560  // We don't know what index it is,
561  // but we know the value is from the array
562  for(const exprt &array_entry : potential_array_expr.operands())
563  {
564  expressionst array_contents;
565  bool is_entry_const;
566  bool resolved_value=
568  array_entry, array_contents, is_entry_const);
569 
570  if(!resolved_value)
571  {
572  LOG("Failed to resolve array value", array_entry);
573  return false;
574  }
575 
576  for(const exprt &resolved_array_entry : array_contents)
577  {
578  out_expressions.push_back(resolved_array_entry);
579  }
580  }
581  }
582  }
583  else
584  {
585  LOG(
586  "Squashing index of did not result in an array",
587  potential_array_expr);
588  return false;
589  }
590  }
591 
592  out_is_const=all_possible_const || array_const;
593  return true;
594  }
595  else
596  {
597  LOG("Failed to squash index of to array expression", index_expr);
598  return false;
599  }
600 }
601 
611  const member_exprt &member_expr,
612  expressionst &out_expressions,
613  bool &out_is_const)
614 {
615  expressionst potential_structs;
616  bool is_struct_const;
617 
618  // Get the struct it belongs to
619  bool resolved_struct=
621  member_expr.compound(), potential_structs, is_struct_const);
622  if(resolved_struct)
623  {
624  for(const exprt &potential_struct : potential_structs)
625  {
626  if(potential_struct.id()==ID_struct)
627  {
628  struct_exprt struct_expr=to_struct_expr(potential_struct);
629  const exprt &component_value=
630  get_component_value(struct_expr, member_expr);
631  expressionst resolved_expressions;
632  bool component_const=false;
633  bool resolved=
635  component_value, resolved_expressions, component_const);
636  if(resolved)
637  {
638  out_expressions.insert(
639  out_expressions.end(),
640  resolved_expressions.begin(),
641  resolved_expressions.end());
642  }
643  else
644  {
645  LOG("Could not resolve component value", component_value);
646  return false;
647  }
648  }
649  else
650  {
651  LOG(
652  "Squashing member access did not resolve in a struct",
653  potential_struct);
654  return false;
655  }
656  }
657  out_is_const=is_struct_const;
658  return true;
659  }
660  else
661  {
662  LOG("Failed to squash struct access", member_expr);
663  return false;
664  }
665 }
666 
679  expressionst &out_expressions,
680  bool &out_is_const)
681 {
682  // We had a pointer, we need to check both the pointer
683  // type can't be changed, and what it what pointing to
684  // can't be changed
685  expressionst pointer_values;
686  bool pointer_const;
687  bool resolved=
688  try_resolve_expression(deref_expr.pointer(), pointer_values, pointer_const);
689  if(resolved && pointer_const)
690  {
691  bool all_objects_const=true;
692  for(const exprt &pointer_val : pointer_values)
693  {
694  if(pointer_val.id()==ID_address_of)
695  {
696  address_of_exprt address_expr=to_address_of_expr(pointer_val);
697  bool object_const=false;
698  expressionst out_object_values;
699  const bool resolved_address = try_resolve_expression(
700  address_expr.object(), out_object_values, object_const);
701 
702  if(resolved_address)
703  {
704  out_expressions.insert(
705  out_expressions.end(),
706  out_object_values.begin(),
707  out_object_values.end());
708 
709  all_objects_const&=object_const;
710  }
711  else
712  {
713  LOG("Failed to resolve value of a dereference", address_expr);
714  }
715  }
716  else
717  {
718  LOG(
719  "Squashing dereference did not result in an address", pointer_val);
720  return false;
721  }
722  }
723  out_is_const=all_objects_const;
724  return true;
725  }
726  else
727  {
728  if(!resolved)
729  {
730  LOG("Failed to resolve pointer of dereference", deref_expr);
731  }
732  else if(!pointer_const)
733  {
734  LOG("Pointer value not const so can't squash", deref_expr);
735  }
736  return false;
737  }
738 }
739 
748  const typecast_exprt &typecast_expr,
749  expressionst &out_expressions,
750  bool &out_is_const)
751 {
752  expressionst typecast_values;
753  bool typecast_const;
754  bool resolved=
756  typecast_expr.op(), typecast_values, typecast_const);
757 
758  if(resolved)
759  {
760  out_expressions.insert(
761  out_expressions.end(),
762  typecast_values.begin(),
763  typecast_values.end());
764  out_is_const=typecast_const;
765  return true;
766  }
767  else
768  {
769  LOG("Could not resolve typecast value", typecast_expr);
770  return false;
771  }
772 }
773 
778  const exprt &expression) const
779 {
780  return is_const_type(expression.type());
781 }
782 
788 {
789  if(type.id() == ID_array)
790  return to_array_type(type).element_type().get_bool(ID_C_constant);
791  else
792  return type.get_bool(ID_C_constant);
793 }
794 
801  const struct_exprt &struct_expr, const member_exprt &member_expr)
802 {
803  const struct_typet &struct_type =
804  ns.follow_tag(to_struct_tag_type(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 }
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:20
Operator to return the address of an object.
Definition: pointer_expr.h:540
exprt & object()
Definition: pointer_expr.h:549
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:827
A constant literal expression.
Definition: std_expr.h:3000
Operator to dereference a pointer.
Definition: pointer_expr.h:834
Base class for all expressions.
Definition: expr.h:56
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:47
typet & type()
Return the type of the expression.
Definition: expr.h:84
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.h:212
operandst & operands()
Definition: expr.h:94
Array index operator.
Definition: std_expr.h:1470
exprt & array()
Definition: std_expr.h:1500
exprt & index()
Definition: std_expr.h:1510
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:57
bool is_not_nil() const
Definition: irep.h:372
const irep_idt & id() const
Definition: irep.h:388
Extract member of struct or union.
Definition: std_expr.h:2854
const exprt & compound() const
Definition: std_expr.h:2903
irep_idt get_component_name() const
Definition: std_expr.h:2876
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
remove_const_function_pointerst(message_handlert &message_handler, const namespacet &ns, const symbol_table_baset &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:1877
Structure type, corresponds to C style structs.
Definition: std_types.h:231
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:47
Expression to hold a symbol (variable)
Definition: std_expr.h:131
const irep_idt & get_identifier() const
Definition: std_expr.h:160
The symbol table base class interface.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
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:2073
The type of an expression, extends irept.
Definition: type.h:29
const exprt & op() const
Definition: std_expr.h:391
double log(double x)
Definition: math.c:2776
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:890
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:577
#define LOG(message, irep)
exprt deref_expr(const exprt &expr)
Wraps a given expression into a dereference_exprt unless it is an address_of_exprt in which case it j...
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition: smt_terms.h:17
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3055
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2107
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1900
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2946
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1538
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:888
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:518
Author: Diffblue Ltd.