cprover
Loading...
Searching...
No Matches
remove_const_function_pointers.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto Programs
4
5Author: 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>
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=to_struct_type(ns.follow(struct_expr.type()));
804 size_t component_number=
805 struct_type.component_number(member_expr.get_component_name());
806
807 return struct_expr.operands()[component_number];
808}
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Target numeric_cast_v(const mp_integer &arg)
Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possibl...
Operator to return the address of an object.
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:783
A constant literal expression.
Definition std_expr.h:2942
Operator to dereference a pointer.
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
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:204
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
Array index operator.
Definition std_expr.h:1410
exprt & index()
Definition std_expr.h:1450
exprt & array()
Definition std_expr.h:1440
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
bool is_not_nil() const
Definition irep.h:380
const irep_idt & id() const
Definition irep.h:396
Extract member of struct or union.
Definition std_expr.h:2794
const exprt & compound() const
Definition std_expr.h:2843
irep_idt get_component_name() const
Definition std_expr.h:2816
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
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:1819
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:46
Expression to hold a symbol (variable)
Definition std_expr.h:113
const irep_idt & get_identifier() const
Definition std_expr.h:142
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:2017
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:326
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
#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:18
#define PRECONDITION(CONDITION)
Definition invariant.h:463
API to expression classes.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition std_expr.h:1842
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1478
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2051
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2886
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2992
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:844
Author: Diffblue Ltd.