36 const exprt &other_operand,
56 const std::vector<exprt> value_set_elements =
59 bool constant_found =
false;
61 for(
const auto &value_set_element : value_set_elements)
64 value_set_element.id() == ID_unknown ||
65 value_set_element.id() == ID_invalid ||
77 value_set_element,
false, language_mode))
84 value_set_element, symbol_expr, ns);
96 constant_found =
true;
115 else if(value_set_elements.size() == 1)
131 if(expr.
id() != ID_equal && expr.
id() != ID_notequal)
152 if(maybe_constant.has_value())
153 return changed(*maybe_constant);
165 auto collect_objects = [
this](
const exprt &pointer)
167 std::set<exprt> objects;
177 const std::vector<exprt> value_set_elements =
180 for(
const auto &value_set_element : value_set_elements)
183 value_set_element.id() == ID_unknown ||
184 value_set_element.id() == ID_invalid ||
204 if(lhs_objects.size() == 1 && lhs_objects == rhs_objects)
213 std::set_intersection(
219 if(!lhs_objects.empty() && !rhs_objects.empty() &&
intersection.empty())
236 if(ptr.
type().
id() != ID_pointer)
246 const std::vector<exprt> value_set_elements =
249 std::optional<exprt> offset;
251 for(
const auto &value_set_element : value_set_elements)
254 value_set_element.id() == ID_unknown ||
255 value_set_element.id() == ID_invalid ||
266 this_offset.
id() == ID_unknown ||
267 (offset.has_value() && this_offset != *offset))
272 else if(!offset.has_value())
274 offset = this_offset;
278 if(!offset.has_value())
bool is_failed_symbol(const exprt &expr)
Return true if, and only if, expr is the result of failed dereferencing.
A base class for relations, i.e., binary predicates whose two operands have the same type.
A constant literal expression.
bool is_null_pointer() const
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Base class for all expressions.
bool is_true() const
Return whether the expression is a constant representing true.
bool is_boolean() const
Return whether the expression represents a Boolean.
bool is_false() const
Return whether the expression is a constant representing false.
typet & type()
Return the type of the expression.
The Boolean constant false.
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
static const exprt & root_object(const exprt &expr)
The offset (in bytes) of a pointer relative to the object.
resultt simplify_pointer_offset(const pointer_offset_exprt &) override
const value_sett & value_set
resultt simplify_inequality(const binary_relation_exprt &) override
simplifies inequalities !=, <=, <, >=, >, and also ==
resultt simplify_inequality_pointer_object(const binary_relation_exprt &) override
When all candidates in the value set have the same offset we can replace a pointer_offset expression ...
const irep_idt language_mode
static resultt changed(resultt<> result)
resultt simplify_rec(const exprt &)
virtual resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
virtual resultt simplify_inequality_pointer_object(const binary_relation_exprt &)
static resultt unchanged(exprt expr)
virtual resultt simplify_pointer_offset(const pointer_offset_exprt &)
Expression providing an SSA-renamed symbol of expressions.
Expression to hold a symbol (variable)
The Boolean constant true.
static exprt conditional_cast(const exprt &expr, const typet &type)
Return value for build_reference_to; see that method for documentation.
static valuet build_reference_to(const exprt &what, const exprt &pointer, const namespacet &ns)
static bool should_ignore_value(const exprt &what, bool exclude_null_derefs, const irep_idt &language_mode)
Determine whether possible alias what should be ignored when replacing a pointer by its referees.
State type in value_set_domaint, used in value-set analysis and goto-symex.
std::vector< exprt > get_value_set(exprt expr, const namespacet &ns) const
Gets values pointed to by expr, including following dereference operators (i.e.
bool can_cast_expr(const exprt &base)
Check whether a reference to a generic exprt is of a specific derived class.
bool can_cast_type(const typet &base)
Check whether a reference to a generic typet is of a specific derived class.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
GOTO Symex constant propagation.
void intersection(const typename graph_nodet< E >::edgest &a, const typename graph_nodet< E >::edgest &b, typename graph_nodet< E >::edgest &dest)
Compute intersection of two edge sets, in linear time.
API to expression classes for Pointers.
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
exprt simplify_expr(exprt src, const namespacet &ns)
static std::optional< exprt > try_evaluate_pointer_comparison(const irep_idt &operation, const symbol_exprt &symbol_expr, const exprt &other_operand, const value_sett &value_set, const irep_idt language_mode, const namespacet &ns)
Try to evaluate a simple pointer comparison.
#define PRECONDITION(CONDITION)
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.