26 if(expr.
id() == ID_dereference)
31 pointer.id() == ID_typecast &&
38 if(pointer.is_constant())
59 const exprt &pointer = expr.
op();
62 if(pointer.
id() == ID_if)
70 if(r_it.has_changed())
84 if(expr.
id()==ID_index)
88 bool no_change =
true;
92 if(array_result.has_changed())
95 new_index_expr.array() = array_result.expr;
98 auto index_result =
simplify_rec(new_index_expr.index());
100 if(index_result.has_changed())
103 new_index_expr.index() = index_result.expr;
115 if(step_size.has_value())
117 const auto index = numeric_cast<mp_integer>(new_index_expr.index());
119 if(index.has_value())
135 return new_index_expr;
137 else if(expr.
id()==ID_member)
141 bool no_change =
true;
143 auto struct_op_result =
146 if(struct_op_result.has_changed())
148 new_member_expr.struct_op() = struct_op_result.expr;
152 const typet &op_type = new_member_expr.struct_op().type();
154 if(op_type.
id() == ID_struct || op_type.
id() == ID_struct_tag)
163 op_type.
id() == ID_struct_tag
168 if(offset.has_value())
181 return new_member_expr;
183 else if(expr.
id()==ID_dereference)
187 if(r_pointer.has_changed())
189 new_expr.pointer() = r_pointer.expr;
190 return std::move(new_expr);
193 else if(expr.
id()==ID_if)
197 bool no_change =
true;
200 if(r_cond.has_changed())
202 new_if_expr.cond() = r_cond.expr;
207 if(true_result.has_changed())
209 new_if_expr.true_case() = true_result.expr;
215 if(false_result.has_changed())
217 new_if_expr.false_case() = false_result.expr;
222 if(new_if_expr.cond().is_true())
224 return new_if_expr.true_case();
226 else if(new_if_expr.cond().is_false())
228 return new_if_expr.false_case();
241 if(expr.
type().
id() != ID_pointer)
246 if(new_object.expr.id() == ID_index)
250 if(!index_expr.index().is_zero())
255 auto new_address_of_expr = expr;
256 new_address_of_expr.
object() = std::move(index_expr);
257 return plus_exprt(std::move(new_address_of_expr), offset);
260 else if(new_object.expr.id() == ID_dereference)
266 if(new_object.has_changed())
268 auto new_expr = expr;
269 new_expr.
object() = new_object;
281 if(ptr.
type().
id()!=ID_pointer)
284 if(ptr.
id()==ID_address_of)
288 if(offset.has_value())
291 else if(ptr.
id()==ID_typecast)
294 const typet &op_type = op.type();
296 if(op_type.
id()==ID_pointer)
300 auto new_expr = expr;
305 else if(op_type.
id()==ID_signedbv ||
306 op_type.
id()==ID_unsignedbv)
322 if(tmp.
id()==ID_plus && tmp.
operands().size()==2)
327 plus_expr.op0().id() == ID_typecast &&
336 plus_expr.op1().id() == ID_typecast &&
348 else if(ptr.
id()==ID_plus)
353 for(
const auto &op : ptr.
operands())
355 if(op.type().id()==ID_pointer)
356 ptr_expr.push_back(op);
357 else if(!op.is_zero())
363 int_expr.push_back(tmp);
367 if(ptr_expr.size()!=1 || int_expr.empty())
370 typet pointer_base_type =
372 if(pointer_base_type.
id() == ID_empty)
377 if(!element_size.has_value())
385 if(int_expr.size()==1)
386 sum=int_expr.front();
394 auto new_expr =
plus_exprt(pointer_offset_expr, product);
419 number%=
power(2, offset_bits);
444 tmp0_address_of.object().id() == ID_index &&
458 tmp1_address_of.object().id() == ID_index &&
464 const auto &tmp0_object = tmp0_address_of.object();
465 const auto &tmp1_object = tmp1_address_of.object();
467 if(tmp0_object.id() == ID_symbol && tmp1_object.id() == ID_symbol)
475 tmp0_object.id() == ID_dynamic_object &&
476 tmp1_object.id() == ID_dynamic_object)
484 (tmp0_object.id() == ID_symbol && tmp1_object.id() == ID_dynamic_object) ||
485 (tmp0_object.id() == ID_dynamic_object && tmp1_object.id() == ID_symbol))
490 tmp0_object.id() == ID_string_constant &&
491 tmp1_object.id() == ID_string_constant && tmp0_object == tmp1_object)
506 for(
const auto &operand : expr.
operands())
511 if(op.
id()==ID_address_of)
515 if((op_object.id() != ID_symbol && op_object.id() != ID_dynamic_object &&
516 op_object.id() != ID_string_constant))
526 if(new_inequality_ops.empty())
527 new_inequality_ops.push_back(op);
530 new_inequality_ops.push_back(
532 op, new_inequality_ops.front().
type())));
536 auto new_expr = expr;
538 new_expr.
operands() = std::move(new_inequality_ops);
550 if(op_result.expr.id() == ID_if)
555 auto p_o_false = expr;
558 auto p_o_true = expr;
561 auto new_expr =
if_exprt(cond, p_o_true, p_o_false, expr.
type());
565 if(op_result.has_changed())
567 auto new_expr = expr;
568 new_expr.
op() = op_result;
569 return std::move(new_expr);
578 auto new_expr = expr;
579 exprt &op = new_expr.op();
581 bool no_change =
true;
585 if(op_result.has_changed())
596 if(op.
id() == ID_address_of)
600 if(op_object.id() == ID_symbol)
608 else if(op_object.id() == ID_string_constant)
612 else if(op_object.id() == ID_array)
621 return std::move(new_expr);
627 auto new_expr = expr;
628 exprt &op = new_expr.op();
629 bool no_change =
true;
633 if(op_result.has_changed())
646 if(op.
id()==ID_address_of)
654 return std::move(new_expr);
660 auto new_expr = expr;
661 bool no_change =
true;
662 exprt &op = new_expr.pointer();
665 if(op_result.has_changed())
671 if(op.
id() == ID_address_of)
675 if(op_object.id() == ID_symbol)
680 if(size_opt.has_value())
683 exprt size = size_opt.value();
685 if(size.
type() != expr_type)
691 else if(op_object.id() == ID_string_constant)
702 return std::move(new_expr);
712 return std::move(new_expr);
722 return std::move(new_expr);
pointer_typet pointer_type(const typet &subtype)
bitvector_typet char_type()
bitvector_typet c_index_type()
Operator to return the address of an object.
A base class for relations, i.e., binary predicates whose two operands have the same type.
std::size_t get_width() const
struct configt::bv_encodingt bv_encoding
A constant literal expression.
const irep_idt & get_value() const
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
unsigned int get_instance() const
Base class for all expressions.
std::vector< exprt > operandst
bool is_boolean() const
Return whether the expression represents a Boolean.
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.
The Boolean constant false.
The trinary if-then-else operator.
const irep_idt & id() const
irep_idt get_component_name() const
Binary multiplication Associativity is not specified.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Expression for finding the size (in bytes) of the object a pointer points to.
The plus expression Associativity is not specified.
A numerical identifier for the object a pointer points to.
The offset (in bytes) of a pointer relative to the object.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
pointer_in_range (see pointer_in_range_exprt) with prophecy expressions to encode whether a pointer r...
exprt lower(const namespacet &ns) const
A base class for a predicate that indicates that an address range is ok to read or write or both.
exprt lower(const namespacet &ns) const
Lower an r_or_w_ok_exprt to arithmetic and logic expressions.
resultt simplify_inequality_address_of(const binary_relation_exprt &)
resultt simplify_prophecy_r_or_w_ok(const prophecy_r_or_w_ok_exprt &)
Try to simplify prophecy_{r,w,rw}_ok to a constant expression.
static resultt changed(resultt<> result)
resultt simplify_unary_pointer_predicate_preorder(const unary_exprt &)
resultt simplify_address_of(const address_of_exprt &)
resultt simplify_node(const exprt &)
resultt simplify_prophecy_pointer_in_range(const prophecy_pointer_in_range_exprt &)
Try to simplify prophecy_pointer_in_range to a constant expression.
resultt simplify_rec(const exprt &)
resultt simplify_typecast(const typecast_exprt &)
resultt simplify_pointer_object(const pointer_object_exprt &)
resultt simplify_object(const exprt &)
resultt simplify_mult(const mult_exprt &)
resultt simplify_address_of_arg(const exprt &)
resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
resultt simplify_inequality_pointer_object(const binary_relation_exprt &)
static resultt unchanged(exprt expr)
resultt simplify_is_invalid_pointer(const unary_exprt &)
resultt simplify_pointer_offset(const pointer_offset_exprt &)
resultt simplify_plus(const plus_exprt &)
resultt simplify_if_preorder(const if_exprt &expr)
resultt simplify_is_dynamic_object(const unary_exprt &)
resultt simplify_object_size(const object_size_exprt &)
Structure type, corresponds to C style structs.
const irep_idt & get_identifier() const
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
Generic base class for unary expressions.
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Deprecated expression utility functions.
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
std::optional< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
std::optional< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
Various predicates over pointers in programs.
#define SYMEX_DYNAMIC_PREFIX
static bool is_dereference_integer_object(const exprt &expr, mp_integer &address)
#define PRECONDITION(CONDITION)
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_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 typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_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 struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const string_constantt & to_string_constant(const exprt &expr)