22 #define LOG(message, irep) \
25 log.debug().source_location = irep.source_location(); \
26 log.debug() << message << ": " << format(irep) << messaget::eom; \
38 :
log(message_handler), ns(ns), symbol_table(symbol_table)
53 const exprt &base_expression,
69 const exprt &expression)
const
71 if(expression.
id()==ID_symbol)
94 exprt const_symbol_cleared_expr=expression;
95 const_symbol_cleared_expr.
operands().clear();
99 const_symbol_cleared_expr.
operands().push_back(const_symbol_cleared_op);
102 return const_symbol_cleared_expr;
131 if(simplified_expr.
id()==ID_index)
136 else if(simplified_expr.
id()==ID_member)
141 else if(simplified_expr.
id()==ID_address_of)
145 address_expr, resolved_functions);
147 else if(simplified_expr.
id()==ID_dereference)
152 else if(simplified_expr.
id()==ID_typecast)
158 else if(simplified_expr.
id()==ID_symbol)
160 if(simplified_expr.
type().
id()==ID_code)
167 LOG(
"Non const symbol wasn't squashed", simplified_expr);
181 LOG(
"Non-zero constant value found", simplified_expr);
187 LOG(
"Unrecognised expression", simplified_expr);
193 out_functions.insert(resolved_functions.begin(), resolved_functions.end());
211 for(
const exprt &value : exprs)
219 out_functions.insert(
220 potential_out_functions.begin(),
221 potential_out_functions.end());
225 LOG(
"Could not resolve expression in array", value);
253 LOG(
"Could not resolve array", index_expr);
259 LOG(
"Array not const", index_expr);
285 LOG(
"Could not resolve struct", member_expr);
291 LOG(
"Struct was not const so can't resolve values on it", member_expr);
313 LOG(
"Failed to resolve address of", address_expr);
343 LOG(
"Dereferenced value was not const so can't dereference",
deref_expr);
372 out_functions.insert(typecast_values.begin(), typecast_values.end());
377 LOG(
"Failed to squash typecast", typecast_expr);
402 bool is_resolved_expression_const =
false;
403 if(simplified_expr.
id()==ID_index)
408 index_expr, resolved_expressions, is_resolved_expression_const);
410 else if(simplified_expr.
id()==ID_member)
414 member_expr, resolved_expressions, is_resolved_expression_const);
416 else if(simplified_expr.
id()==ID_dereference)
421 deref, resolved_expressions, is_resolved_expression_const);
423 else if(simplified_expr.
id()==ID_typecast)
428 typecast_expr, resolved_expressions, is_resolved_expression_const);
430 else if(simplified_expr.
id()==ID_symbol)
432 LOG(
"Non const symbol will not be squashed", simplified_expr);
437 resolved_expressions.push_back(simplified_expr);
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;
474 index_value_expressions.size() == 1 &&
475 index_value_expressions.front().is_constant())
480 bool errors=
to_integer(constant_expr, array_index);
483 out_array_index=array_index;
515 bool array_const=
false;
519 potential_array_exprs,
524 bool all_possible_const=
true;
525 for(
const exprt &potential_array_expr : potential_array_exprs)
528 all_possible_const &&
532 if(potential_array_expr.id()==ID_array)
539 const exprt &func_expr =
540 potential_array_expr.
operands()[numeric_cast_v<std::size_t>(value)];
541 bool value_const=
false;
547 out_expressions.insert(
548 out_expressions.end(),
549 array_out_functions.begin(),
550 array_out_functions.end());
554 LOG(
"Failed to resolve array value", func_expr);
562 for(
const exprt &array_entry : potential_array_expr.
operands())
568 array_entry, array_contents, is_entry_const);
572 LOG(
"Failed to resolve array value", array_entry);
576 for(
const exprt &resolved_array_entry : array_contents)
578 out_expressions.push_back(resolved_array_entry);
586 "Squashing index of did not result in an array",
587 potential_array_expr);
592 out_is_const=all_possible_const || array_const;
597 LOG(
"Failed to squash index of to array expression", index_expr);
616 bool is_struct_const;
619 bool resolved_struct=
621 member_expr.
compound(), potential_structs, is_struct_const);
624 for(
const exprt &potential_struct : potential_structs)
626 if(potential_struct.id()==ID_struct)
629 const exprt &component_value=
632 bool component_const=
false;
635 component_value, resolved_expressions, component_const);
638 out_expressions.insert(
639 out_expressions.end(),
640 resolved_expressions.begin(),
641 resolved_expressions.end());
645 LOG(
"Could not resolve component value", component_value);
652 "Squashing member access did not resolve in a struct",
657 out_is_const=is_struct_const;
662 LOG(
"Failed to squash struct access", member_expr);
689 if(resolved && pointer_const)
691 bool all_objects_const=
true;
692 for(
const exprt &pointer_val : pointer_values)
694 if(pointer_val.id()==ID_address_of)
697 bool object_const=
false;
700 address_expr.
object(), out_object_values, object_const);
704 out_expressions.insert(
705 out_expressions.end(),
706 out_object_values.begin(),
707 out_object_values.end());
709 all_objects_const&=object_const;
713 LOG(
"Failed to resolve value of a dereference", address_expr);
719 "Squashing dereference did not result in an address", pointer_val);
723 out_is_const=all_objects_const;
732 else if(!pointer_const)
756 typecast_expr.
op(), typecast_values, typecast_const);
760 out_expressions.insert(
761 out_expressions.end(),
762 typecast_values.begin(),
763 typecast_values.end());
764 out_is_const=typecast_const;
769 LOG(
"Could not resolve typecast value", typecast_expr);
778 const exprt &expression)
const
789 if(type.
id() == ID_array)
792 return type.
get_bool(ID_C_constant);
805 size_t component_number=
808 return struct_expr.
operands()[component_number];
Operator to return the address of an object.
const typet & element_type() const
The type of the elements of the array.
A constant literal expression.
Operator to dereference a pointer.
Base class for all expressions.
bool is_zero() const
Return whether the expression is a constant representing 0.
typet & type()
Return the type of the expression.
bool is_constant() const
Return whether the expression is a constant.
bool get_bool(const irep_idt &name) const
const irep_idt & id() const
Extract member of struct or union.
const exprt & compound() const
irep_idt get_component_name() const
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
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...
const symbol_table_baset & symbol_table
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.
std::list< exprt > expressionst
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.
Structure type, corresponds to C style structs.
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
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.
typet type
Type of symbol.
exprt value
Initial value of symbol.
Semantic type conversion.
The type of an expression, extends irept.
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_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)
#define PRECONDITION(CONDITION)
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.