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)
77 if(symbol.
type.
id()!=ID_code)
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);
171 else if(simplified_expr.
id()==ID_constant)
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);
337 LOG(
"Failed to squash dereference", deref_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;
473 if(index_value_expressions.size()==1 &&
474 index_value_expressions.front().id()==ID_constant)
479 bool errors=
to_integer(constant_expr, array_index);
482 out_array_index=array_index;
514 bool array_const=
false;
518 potential_array_exprs,
523 bool all_possible_const=
true;
524 for(
const exprt &potential_array_expr : potential_array_exprs)
527 all_possible_const &&
530 if(potential_array_expr.id()==ID_array)
537 const exprt &func_expr =
538 potential_array_expr.
operands()[numeric_cast_v<std::size_t>(value)];
539 bool value_const=
false;
545 out_expressions.insert(
546 out_expressions.end(),
547 array_out_functions.begin(),
548 array_out_functions.end());
552 LOG(
"Failed to resolve array value", func_expr);
560 for(
const exprt &array_entry : potential_array_expr.operands())
566 array_entry, array_contents, is_entry_const);
570 LOG(
"Failed to resolve array value", array_entry);
574 for(
const exprt &resolved_array_entry : array_contents)
576 out_expressions.push_back(resolved_array_entry);
584 "Squashing index of did not result in an array",
585 potential_array_expr);
590 out_is_const=all_possible_const || array_const;
595 LOG(
"Failed to squash index of to array expression", index_expr);
614 bool is_struct_const;
617 bool resolved_struct=
619 member_expr.
compound(), potential_structs, is_struct_const);
622 for(
const exprt &potential_struct : potential_structs)
624 if(potential_struct.id()==ID_struct)
627 const exprt &component_value=
630 bool component_const=
false;
633 component_value, resolved_expressions, component_const);
636 out_expressions.insert(
637 out_expressions.end(),
638 resolved_expressions.begin(),
639 resolved_expressions.end());
643 LOG(
"Could not resolve component value", component_value);
650 "Squashing member access did not resolve in a struct",
655 out_is_const=is_struct_const;
660 LOG(
"Failed to squash struct access", member_expr);
687 if(resolved && pointer_const)
689 bool all_objects_const=
true;
690 for(
const exprt &pointer_val : pointer_values)
692 if(pointer_val.id()==ID_address_of)
695 bool object_const=
false;
698 address_expr.
object(), out_object_values, object_const);
702 out_expressions.insert(
703 out_expressions.end(),
704 out_object_values.begin(),
705 out_object_values.end());
707 all_objects_const&=object_const;
711 LOG(
"Failed to resolve value of a dereference", address_expr);
717 "Squashing dereference did not result in an address", pointer_val);
721 out_is_const=all_objects_const;
728 LOG(
"Failed to resolve pointer of dereference", deref_expr);
730 else if(!pointer_const)
732 LOG(
"Pointer value not const so can't squash", deref_expr);
754 typecast_expr.
op(), typecast_values, typecast_const);
758 out_expressions.insert(
759 out_expressions.end(),
760 typecast_values.begin(),
761 typecast_values.end());
762 out_is_const=typecast_const;
767 LOG(
"Could not resolve typecast value", typecast_expr);
776 const exprt &expression)
const
787 if(type.
id() == ID_array)
790 return type.
get_bool(ID_C_constant);
802 size_t component_number=
805 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 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 typet & follow(const typet &) const
Resolve type symbol to the type it points to.
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_tablet &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.
const symbol_tablet & symbol_table
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
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 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 simplify_expr(exprt src, const namespacet &ns)
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define PRECONDITION(CONDITION)
API to expression classes.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
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 struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.