Go to the documentation of this file.
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 &&
531 if(potential_array_expr.id()==ID_array)
538 const exprt &func_expr =
539 potential_array_expr.
operands()[numeric_cast_v<std::size_t>(value)];
540 bool value_const=
false;
546 out_expressions.insert(
547 out_expressions.end(),
548 array_out_functions.begin(),
549 array_out_functions.end());
553 LOG(
"Failed to resolve array value", func_expr);
561 for(
const exprt &array_entry : potential_array_expr.
operands())
567 array_entry, array_contents, is_entry_const);
571 LOG(
"Failed to resolve array value", array_entry);
575 for(
const exprt &resolved_array_entry : array_contents)
577 out_expressions.push_back(resolved_array_entry);
585 "Squashing index of did not result in an array",
586 potential_array_expr);
591 out_is_const=all_possible_const || array_const;
596 LOG(
"Failed to squash index of to array expression", index_expr);
615 bool is_struct_const;
618 bool resolved_struct=
620 member_expr.
compound(), potential_structs, is_struct_const);
623 for(
const exprt &potential_struct : potential_structs)
625 if(potential_struct.id()==ID_struct)
628 const exprt &component_value=
631 bool component_const=
false;
634 component_value, resolved_expressions, component_const);
637 out_expressions.insert(
638 out_expressions.end(),
639 resolved_expressions.begin(),
640 resolved_expressions.end());
644 LOG(
"Could not resolve component value", component_value);
651 "Squashing member access did not resolve in a struct",
656 out_is_const=is_struct_const;
661 LOG(
"Failed to squash struct access", member_expr);
688 if(resolved && pointer_const)
690 bool all_objects_const=
true;
691 for(
const exprt &pointer_val : pointer_values)
693 if(pointer_val.id()==ID_address_of)
696 bool object_const=
false;
699 address_expr.
object(), out_object_values, object_const);
703 out_expressions.insert(
704 out_expressions.end(),
705 out_object_values.begin(),
706 out_object_values.end());
708 all_objects_const&=object_const;
712 LOG(
"Failed to resolve value of a dereference", address_expr);
718 "Squashing dereference did not result in an address", pointer_val);
722 out_is_const=all_objects_const;
729 LOG(
"Failed to resolve pointer of dereference", deref_expr);
731 else if(!pointer_const)
733 LOG(
"Pointer value not const so can't squash", deref_expr);
755 typecast_expr.
op(), typecast_values, typecast_const);
759 out_expressions.insert(
760 out_expressions.end(),
761 typecast_values.begin(),
762 typecast_values.end());
763 out_is_const=typecast_const;
768 LOG(
"Could not resolve typecast value", typecast_expr);
777 const exprt &expression)
const
788 if(type.
id() == ID_array)
791 return type.
get_bool(ID_C_constant);
803 size_t component_number=
806 return struct_expr.
operands()[component_number];
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 try_resolve_typecast(const typecast_exprt &typecast_expr, expressionst &out_expressions, bool &out_is_const)
To squash a typecast access.
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 symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only 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 is_const_expression(const exprt &expression) const
To evaluate the const-ness of the expression type.
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.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
The type of an expression, extends irept.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
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.
typet type
Type of symbol.
Operator to dereference a pointer.
exprt replace_const_symbols(const exprt &expression) const
To collapse the symbols down to their values where possible This takes a very general approach,...
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_expression(const exprt &expr, expressionst &out_resolved_expression, bool &out_is_const)
To squash various expr types to simplify the expression.
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.
Base class for all expressions.
const symbol_tablet & symbol_table
bool is_const_type(const typet &type) const
To evaluate the const-ness of the type.
Expression to hold a symbol (variable)
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
std::unordered_set< symbol_exprt, irep_hash > functionst
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.
Struct constructor from list of elements.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
const exprt & compound() const
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)
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...
#define PRECONDITION(CONDITION)
const irep_idt & get_identifier() const
exprt simplify_expr(exprt src, const namespacet &ns)
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.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
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.
std::list< exprt > expressionst
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 is_zero() const
Return whether the expression is a constant representing 0.
Extract member of struct or union.
exprt value
Initial value of symbol.
Structure type, corresponds to C style structs.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
irep_idt get_component_name() const
exprt resolve_symbol(const symbol_exprt &symbol_expr) const
Look up a symbol in the symbol table and return its value.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
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...
Operator to return the address of an object.
Semantic type conversion.
A constant literal expression.
bool get_bool(const irep_idt &name) const
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.
#define LOG(message, irep)
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
const typet & element_type() const
The type of the elements of the array.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.