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 <ansi-c/c_qualifiers.h>
15 #include <util/simplify_expr.h>
16 #include <util/arith_tools.h>
17 
18 #define LOG(message, irep) \
19  debug() << "Case " << __LINE__ << " : " << message << "\n" \
20  << irep.pretty() << eom;
21 
28  message_handlert &message_handler,
29  const namespacet &ns,
30  const symbol_tablet &symbol_table):
31  messaget(message_handler),
32  ns(ns),
33  symbol_table(symbol_table)
34 {}
35 
48  const exprt &base_expression,
49  functionst &out_functions)
50 {
51  // Replace all const symbols with their values
52  exprt non_symbol_expression=replace_const_symbols(base_expression);
53  return try_resolve_function_call(non_symbol_expression, out_functions);
54 }
55 
64  const exprt &expression) const
65 {
66  if(expression.id()==ID_symbol)
67  {
68  if(is_const_expression(expression))
69  {
70  const symbolt &symbol=
71  symbol_table.lookup(expression.get(ID_identifier));
72  if(symbol.type.id()!=ID_code)
73  {
74  const exprt &symbol_value=symbol.value;
75  return replace_const_symbols(symbol_value);
76  }
77  else
78  {
79  return expression;
80  }
81  }
82  else
83  {
84  return expression;
85  }
86  }
87  else
88  {
89  exprt const_symbol_cleared_expr=expression;
90  const_symbol_cleared_expr.operands().clear();
91  for(const exprt &op : expression.operands())
92  {
93  exprt const_symbol_cleared_op=replace_const_symbols(op);
94  const_symbol_cleared_expr.operands().push_back(const_symbol_cleared_op);
95  }
96 
97  return const_symbol_cleared_expr;
98  }
99 }
100 
105  const symbol_exprt &symbol_expr) const
106 {
107  const symbolt &symbol=
108  symbol_table.lookup(symbol_expr.get_identifier());
109  return symbol.value;
110 }
111 
121  const exprt &expr, functionst &out_functions)
122 {
123  assert(out_functions.empty());
124  const exprt &simplified_expr=simplify_expr(expr, ns);
125  bool resolved=false;
126  functionst resolved_functions;
127  if(simplified_expr.id()==ID_index)
128  {
129  const index_exprt &index_expr=to_index_expr(simplified_expr);
130  resolved=try_resolve_index_of_function_call(index_expr, resolved_functions);
131  }
132  else if(simplified_expr.id()==ID_member)
133  {
134  const member_exprt &member_expr=to_member_expr(simplified_expr);
135  resolved=try_resolve_member_function_call(member_expr, resolved_functions);
136  }
137  else if(simplified_expr.id()==ID_address_of)
138  {
139  address_of_exprt address_expr=to_address_of_expr(simplified_expr);
141  address_expr, resolved_functions);
142  }
143  else if(simplified_expr.id()==ID_dereference)
144  {
145  const dereference_exprt &deref=to_dereference_expr(simplified_expr);
146  resolved=try_resolve_dereference_function_call(deref, resolved_functions);
147  }
148  else if(simplified_expr.id()==ID_typecast)
149  {
150  typecast_exprt typecast_expr=to_typecast_expr(simplified_expr);
151  resolved=
152  try_resolve_typecast_function_call(typecast_expr, resolved_functions);
153  }
154  else if(simplified_expr.id()==ID_symbol)
155  {
156  if(simplified_expr.type().id()==ID_code)
157  {
158  resolved_functions.insert(simplified_expr);
159  resolved=true;
160  }
161  else
162  {
163  LOG("Non const symbol wasn't squashed", simplified_expr);
164  resolved=false;
165  }
166  }
167  else if(simplified_expr.id()==ID_constant)
168  {
169  if(simplified_expr.is_zero())
170  {
171  // We have the null pointer - no need to throw everything away
172  // but we don't add any functions either
173  resolved=true;
174  }
175  else
176  {
177  LOG("Non-zero constant value found", simplified_expr);
178  resolved=false;
179  }
180  }
181  else
182  {
183  LOG("Unrecognised expression", simplified_expr);
184  resolved=false;
185  }
186 
187  if(resolved)
188  {
189  out_functions.insert(resolved_functions.begin(), resolved_functions.end());
190  return true;
191  }
192  else
193  {
194  return false;
195  }
196 }
197 
205  const expressionst &exprs, functionst &out_functions)
206 {
207  for(const exprt &value : exprs)
208  {
209  functionst potential_out_functions;
210  bool resolved_value=
211  try_resolve_function_call(value, potential_out_functions);
212 
213  if(resolved_value)
214  {
215  out_functions.insert(
216  potential_out_functions.begin(),
217  potential_out_functions.end());
218  }
219  else
220  {
221  LOG("Could not resolve expression in array", value);
222  return false;
223  }
224  }
225  return true;
226 }
227 
240  const index_exprt &index_expr, functionst &out_functions)
241 {
242  expressionst potential_array_values;
243  bool array_const;
244  bool resolved=
245  try_resolve_index_of(index_expr, potential_array_values, array_const);
246 
247  if(!resolved)
248  {
249  LOG("Could not resolve array", index_expr);
250  return false;
251  }
252 
253  if(!array_const)
254  {
255  LOG("Array not const", index_expr);
256  return false;
257  }
258 
259  return try_resolve_function_calls(potential_array_values, out_functions);
260 }
261 
272  const member_exprt &member_expr, functionst &out_functions)
273 {
274  expressionst potential_component_values;
275  bool struct_const;
276  bool resolved=
277  try_resolve_member(member_expr, potential_component_values, struct_const);
278 
279  if(!resolved)
280  {
281  LOG("Could not resolve struct", member_expr);
282  return false;
283  }
284 
285  if(!struct_const)
286  {
287  LOG("Struct was not const so can't resolve values on it", member_expr);
288  return false;
289  }
290 
291  return try_resolve_function_calls(potential_component_values, out_functions);
292 }
293 
303  const address_of_exprt &address_expr, functionst &out_functions)
304 {
305  bool resolved=
306  try_resolve_function_call(address_expr.object(), out_functions);
307  if(!resolved)
308  {
309  LOG("Failed to resolve address of", address_expr);
310  }
311  return resolved;
312 }
313 
324  const dereference_exprt &deref_expr, functionst &out_functions)
325 {
326  expressionst potential_deref_values;
327  bool deref_const;
328  bool resolved=
329  try_resolve_dereference(deref_expr, potential_deref_values, deref_const);
330 
331  if(!resolved)
332  {
333  LOG("Failed to squash dereference", deref_expr);
334  return false;
335  }
336 
337  if(!deref_const)
338  {
339  LOG("Dereferenced value was not const so can't dereference", deref_expr);
340  return false;
341  }
342 
343  return try_resolve_function_calls(potential_deref_values, out_functions);
344 }
345 
356  const typecast_exprt &typecast_expr, functionst &out_functions)
357 {
358  // We simply ignore typecasts and assume they are valid
359  // I thought simplify_expr would deal with this, but for example
360  // a cast from a 32 bit width int to a 64bit width int it doesn't seem
361  // to allow
362  functionst typecast_values;
363  bool resolved=
364  try_resolve_function_call(typecast_expr.op(), typecast_values);
365 
366  if(resolved)
367  {
368  out_functions.insert(typecast_values.begin(), typecast_values.end());
369  return true;
370  }
371  else
372  {
373  LOG("Failed to squash typecast", typecast_expr);
374  return false;
375  }
376 }
377 
393  const exprt &expr, expressionst &out_resolved_expression, bool &out_is_const)
394 {
395  exprt simplified_expr=simplify_expr(expr, ns);
396  bool resolved;
397  expressionst resolved_expressions;
398  bool is_resolved_expression_const;
399  if(simplified_expr.id()==ID_index)
400  {
401  const index_exprt &index_expr=to_index_expr(simplified_expr);
402  resolved=
404  index_expr, resolved_expressions, is_resolved_expression_const);
405  }
406  else if(simplified_expr.id()==ID_member)
407  {
408  const member_exprt &member_expr=to_member_expr(simplified_expr);
409  resolved=try_resolve_member(
410  member_expr, resolved_expressions, is_resolved_expression_const);
411  }
412  else if(simplified_expr.id()==ID_dereference)
413  {
414  const dereference_exprt &deref=to_dereference_expr(simplified_expr);
415  resolved=
417  deref, resolved_expressions, is_resolved_expression_const);
418  }
419  else if(simplified_expr.id()==ID_typecast)
420  {
421  typecast_exprt typecast_expr=to_typecast_expr(simplified_expr);
422  resolved=
424  typecast_expr, resolved_expressions, is_resolved_expression_const);
425  }
426  else if(simplified_expr.id()==ID_symbol)
427  {
428  LOG("Non const symbol will not be squashed", simplified_expr);
429  resolved=false;
430  }
431  else
432  {
433  resolved_expressions.push_back(simplified_expr);
434  is_resolved_expression_const=is_const_expression(simplified_expr);
435  resolved=true;
436  }
437 
438  if(resolved)
439  {
440  out_resolved_expression.insert(
441  out_resolved_expression.end(),
442  resolved_expressions.begin(),
443  resolved_expressions.end());
444  out_is_const=is_resolved_expression_const;
445  return true;
446  }
447  else
448  {
449  return false;
450  }
451 }
452 
462  const exprt &expr, mp_integer &out_array_index)
463 {
464  expressionst index_value_expressions;
465  bool is_const=false;
466  bool resolved=try_resolve_expression(expr, index_value_expressions, is_const);
467  if(resolved)
468  {
469  if(index_value_expressions.size()==1 &&
470  index_value_expressions.front().id()==ID_constant)
471  {
472  const constant_exprt &constant_expr=
473  to_constant_expr(index_value_expressions.front());
474  mp_integer array_index;
475  bool errors=to_integer(constant_expr, array_index);
476  if(!errors)
477  {
478  out_array_index=array_index;
479  }
480  return !errors;
481  }
482  else
483  {
484  return false;
485  }
486  }
487  else
488  {
489  return false;
490  }
491 }
492 
504  const index_exprt &index_expr,
505  expressionst &out_expressions,
506  bool &out_is_const)
507 {
508  // Get the array(s) it belongs to
509  expressionst potential_array_exprs;
510  bool array_const=false;
511  bool resolved_array=
513  index_expr.array(),
514  potential_array_exprs,
515  array_const);
516 
517  if(resolved_array)
518  {
519  bool all_possible_const=true;
520  for(const exprt &potential_array_expr : potential_array_exprs)
521  {
522  all_possible_const=
523  all_possible_const &&
524  is_const_type(potential_array_expr.type().subtype());
525 
526  if(potential_array_expr.id()==ID_array)
527  {
528  // Get the index if we can
529  mp_integer value;
530  if(try_resolve_index_value(index_expr.index(), value))
531  {
532  expressionst array_out_functions;
533  const exprt &func_expr=
534  potential_array_expr.operands()[integer2size_t(value)];
535  bool value_const=false;
536  bool resolved_value=
537  try_resolve_expression(func_expr, array_out_functions, value_const);
538 
539  if(resolved_value)
540  {
541  out_expressions.insert(
542  out_expressions.end(),
543  array_out_functions.begin(),
544  array_out_functions.end());
545  }
546  else
547  {
548  LOG("Failed to resolve array value", func_expr);
549  return false;
550  }
551  }
552  else
553  {
554  // We don't know what index it is,
555  // but we know the value is from the array
556  for(const exprt &array_entry : potential_array_expr.operands())
557  {
558  expressionst array_contents;
559  bool is_entry_const;
560  bool resolved_value=
562  array_entry, array_contents, is_entry_const);
563 
564  if(!resolved_value)
565  {
566  LOG("Failed to resolve array value", array_entry);
567  return false;
568  }
569 
570  for(const exprt &resolved_array_entry : array_contents)
571  {
572  out_expressions.push_back(resolved_array_entry);
573  }
574  }
575  }
576  }
577  else
578  {
579  LOG(
580  "Squashing index of did not result in an array",
581  potential_array_expr);
582  return false;
583  }
584  }
585 
586  out_is_const=all_possible_const || array_const;
587  return true;
588  }
589  else
590  {
591  LOG("Failed to squash index of to array expression", index_expr);
592  return false;
593  }
594 }
595 
605  const member_exprt &member_expr,
606  expressionst &out_expressions,
607  bool &out_is_const)
608 {
609  expressionst potential_structs;
610  bool is_struct_const;
611 
612  // Get the struct it belongs to
613  bool resolved_struct=
615  member_expr.compound(), potential_structs, is_struct_const);
616  if(resolved_struct)
617  {
618  for(const exprt &potential_struct : potential_structs)
619  {
620  if(potential_struct.id()==ID_struct)
621  {
622  struct_exprt struct_expr=to_struct_expr(potential_struct);
623  const exprt &component_value=
624  get_component_value(struct_expr, member_expr);
625  expressionst resolved_expressions;
626  bool component_const=false;
627  bool resolved=
629  component_value, resolved_expressions, component_const);
630  if(resolved)
631  {
632  out_expressions.insert(
633  out_expressions.end(),
634  resolved_expressions.begin(),
635  resolved_expressions.end());
636  }
637  else
638  {
639  LOG("Could not resolve component value", component_value);
640  return false;
641  }
642  }
643  else
644  {
645  LOG(
646  "Squashing member access did not resolve in a struct",
647  potential_struct);
648  return false;
649  }
650  }
651  out_is_const=is_struct_const;
652  return true;
653  }
654  else
655  {
656  LOG("Failed to squash struct access", member_expr);
657  return false;
658  }
659 }
660 
672  const dereference_exprt &deref_expr,
673  expressionst &out_expressions,
674  bool &out_is_const)
675 {
676  // We had a pointer, we need to check both the pointer
677  // type can't be changed, and what it what pointing to
678  // can't be changed
679  expressionst pointer_values;
680  bool pointer_const;
681  bool resolved=
682  try_resolve_expression(deref_expr.pointer(), pointer_values, pointer_const);
683  if(resolved && pointer_const)
684  {
685  bool all_objects_const=true;
686  for(const exprt &pointer_val : pointer_values)
687  {
688  if(pointer_val.id()==ID_address_of)
689  {
690  address_of_exprt address_expr=to_address_of_expr(pointer_val);
691  bool object_const=false;
692  expressionst out_object_values;
693  bool resolved=
695  address_expr.object(), out_object_values, object_const);
696 
697  if(resolved)
698  {
699  out_expressions.insert(
700  out_expressions.end(),
701  out_object_values.begin(),
702  out_object_values.end());
703 
704  all_objects_const&=object_const;
705  }
706  else
707  {
708  LOG("Failed to resolve value of a dereference", address_expr);
709  }
710  }
711  else
712  {
713  LOG(
714  "Squashing dereference did not result in an address", pointer_val);
715  return false;
716  }
717  }
718  out_is_const=all_objects_const;
719  return true;
720  }
721  else
722  {
723  if(!resolved)
724  {
725  LOG("Failed to resolve pointer of dereference", deref_expr);
726  }
727  else if(!pointer_const)
728  {
729  LOG("Pointer value not const so can't squash", deref_expr);
730  }
731  return false;
732  }
733 }
734 
743  const typecast_exprt &typecast_expr,
744  expressionst &out_expressions,
745  bool &out_is_const)
746 {
747  expressionst typecast_values;
748  bool typecast_const;
749  bool resolved=
751  typecast_expr.op(), typecast_values, typecast_const);
752 
753  if(resolved)
754  {
755  out_expressions.insert(
756  out_expressions.end(),
757  typecast_values.begin(),
758  typecast_values.end());
759  out_is_const=typecast_const;
760  return true;
761  }
762  else
763  {
764  LOG("Could not resolve typecast value", typecast_expr);
765  return false;
766  }
767 }
768 
773  const exprt &expression) const
774 {
775  return is_const_type(expression.type());
776 }
777 
783 {
784  c_qualifierst qualifers(type);
785  if(type.id()==ID_array)
786  {
787  c_qualifierst array_type_qualifers(type.subtype());
788  return qualifers.is_constant || array_type_qualifers.is_constant;
789  }
790  else
791  {
792  return qualifers.is_constant;
793  }
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.
Definition: type.h:20
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:1760
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
semantic type conversion
Definition: std_expr.h:1725
symbolt & lookup(const irep_idt &identifier)
Find a symbol in the symbol table.
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:19
exprt & object()
Definition: std_expr.h:2608
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 irep_idt & get_identifier() const
Definition: std_expr.h:120
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3302
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:40
const struct_exprt & to_struct_expr(const exprt &expr)
Cast a generic exprt to a struct_exprt.
Definition: std_expr.h:1487
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:60
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
A constant literal expression.
Definition: std_expr.h:3685
Structure type.
Definition: std_types.h:296
exprt & op()
Definition: std_expr.h:1739
std::unordered_set< exprt, irep_hash > functionst
Extract member of struct or union.
Definition: std_expr.h:3214
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 dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Definition: std_expr.h:2748
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1229
const exprt & compound() const
Definition: std_expr.h:3281
const irep_idt & id() const
Definition: irep.h:189
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Definition: std_expr.h:2629
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:2701
The symbol table.
Definition: symbol_table.h:52
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
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:62
#define LOG(message, irep)
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...
Operator to return the address of an object.
Definition: std_expr.h:2593
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
typet type
Type of symbol.
Definition: symbol.h:37
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:1208
Base class for all expressions.
Definition: expr.h:46
exprt & pointer()
Definition: std_expr.h:2727
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:3249
Expression to hold a symbol (variable)
Definition: std_expr.h:82
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:18
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:3725
const typet & subtype() const
Definition: type.h:31
operandst & operands()
Definition: expr.h:70
struct constructor from list of elements
Definition: std_expr.h:1464
exprt & array()
Definition: std_expr.h:1198
bool is_const_type(const typet &type) const
To evaluate the const-ness of the type.
array index operator
Definition: std_expr.h:1170