Go to the documentation of this file.
29 if(expr.
id() == ID_dereference)
34 pointer.id() == ID_typecast &&
41 if(pointer.is_constant())
61 if(expr.
id()==ID_index)
65 bool no_change =
true;
69 if(array_result.has_changed())
72 new_index_expr.array() = array_result.expr;
75 auto index_result =
simplify_rec(new_index_expr.index());
77 if(index_result.has_changed())
80 new_index_expr.index() = index_result.expr;
92 if(step_size.has_value())
94 const auto index = numeric_cast<mp_integer>(new_index_expr.index());
112 return new_index_expr;
114 else if(expr.
id()==ID_member)
118 bool no_change =
true;
120 auto struct_op_result =
123 if(struct_op_result.has_changed())
125 new_member_expr.struct_op() = struct_op_result.expr;
129 const typet &op_type =
ns.
follow(new_member_expr.struct_op().type());
131 if(op_type.
id() == ID_struct)
141 if(offset.has_value())
154 return new_member_expr;
156 else if(expr.
id()==ID_dereference)
160 if(r_pointer.has_changed())
162 new_expr.pointer() = r_pointer.expr;
163 return std::move(new_expr);
166 else if(expr.
id()==ID_if)
170 bool no_change =
true;
173 if(r_cond.has_changed())
175 new_if_expr.cond() = r_cond.expr;
180 if(true_result.has_changed())
182 new_if_expr.true_case() = true_result.expr;
188 if(false_result.has_changed())
190 new_if_expr.false_case() = false_result.expr;
195 if(new_if_expr.cond().is_true())
197 return new_if_expr.true_case();
199 else if(new_if_expr.cond().is_false())
201 return new_if_expr.false_case();
214 if(expr.
type().
id() != ID_pointer)
219 if(new_object.expr.id() == ID_index)
223 if(!index_expr.index().is_zero())
228 auto new_address_of_expr = expr;
229 new_address_of_expr.
object() = std::move(index_expr);
230 return plus_exprt(std::move(new_address_of_expr), offset);
233 else if(new_object.expr.id() == ID_dereference)
239 if(new_object.has_changed())
241 auto new_expr = expr;
242 new_expr.
object() = new_object;
254 if(ptr.
id()==ID_if && ptr.
operands().size()==3)
264 if(ptr.
type().
id()!=ID_pointer)
267 if(ptr.
id()==ID_address_of)
271 if(offset.has_value())
274 else if(ptr.
id()==ID_typecast)
277 const typet &op_type = op.type();
279 if(op_type.
id()==ID_pointer)
283 auto new_expr = expr;
288 else if(op_type.
id()==ID_signedbv ||
289 op_type.
id()==ID_unsignedbv)
306 if(tmp.
id()==ID_plus && tmp.
operands().size()==2)
311 plus_expr.op0().id() == ID_typecast &&
320 plus_expr.op1().id() == ID_typecast &&
332 else if(ptr.
id()==ID_plus)
337 for(
const auto &op : ptr.
operands())
339 if(op.type().id()==ID_pointer)
340 ptr_expr.push_back(op);
341 else if(!op.is_zero())
347 int_expr.push_back(tmp);
351 if(ptr_expr.size()!=1 || int_expr.empty())
354 typet pointer_sub_type=ptr_expr.front().type().
subtype();
355 if(pointer_sub_type.
id()==ID_empty)
360 if(!element_size.has_value())
368 if(int_expr.size()==1)
369 sum=int_expr.front();
384 auto new_expr =
plus_exprt(pointer_offset_expr, product);
388 else if(ptr.
id()==ID_constant)
411 number%=
power(2, offset_bits);
434 if(tmp0.
id()==ID_typecast)
442 tmp0_address_of.object().id() == ID_index &&
452 if(tmp1.
id()==ID_typecast)
460 tmp1_address_of.object().id() == ID_index &&
466 const auto &tmp0_object = tmp0_address_of.object();
467 const auto &tmp1_object = tmp1_address_of.object();
469 if(tmp0_object.id() == ID_symbol && tmp1_object.id() == ID_symbol)
477 tmp0_object.id() == ID_dynamic_object &&
478 tmp1_object.id() == ID_dynamic_object)
486 (tmp0_object.id() == ID_symbol && tmp1_object.id() == ID_dynamic_object) ||
487 (tmp0_object.id() == ID_dynamic_object && tmp1_object.id() == ID_symbol))
507 if(op.
id()==ID_address_of)
511 if((op_object.id() != ID_symbol && op_object.id() != ID_dynamic_object &&
512 op_object.id() != ID_string_constant))
517 else if(op.
id() != ID_constant || !op.
is_zero())
522 if(new_inequality_ops.empty())
523 new_inequality_ops.push_back(op);
526 new_inequality_ops.push_back(
528 op, new_inequality_ops.front().
type())));
532 auto new_expr = expr;
534 new_expr.
operands() = std::move(new_inequality_ops);
546 if(op_result.expr.id() == ID_if)
551 auto p_o_false = expr;
554 auto p_o_true = expr;
557 auto new_expr =
if_exprt(cond, p_o_true, p_o_false, expr.
type());
561 if(op_result.has_changed())
563 auto new_expr = expr;
564 new_expr.
op() = op_result;
565 return std::move(new_expr);
574 auto new_expr = expr;
575 exprt &op = new_expr.op();
587 bool no_change =
true;
591 if(op_result.has_changed())
598 if(op.
id() == ID_constant && op.
get(ID_value) == ID_NULL)
602 if(op.
id() == ID_address_of)
606 if(op_object.id() == ID_symbol)
614 else if(op_object.id() == ID_string_constant)
618 else if(op_object.id() == ID_array)
627 return std::move(new_expr);
633 auto new_expr = expr;
634 exprt &op = new_expr.op();
635 bool no_change =
true;
639 if(op_result.has_changed())
646 if(op.
id()==ID_constant && op.
get(ID_value)==ID_NULL)
652 if(op.
id()==ID_address_of)
660 return std::move(new_expr);
668 if(a.
id() == ID_address_of && b.
id() == ID_address_of)
674 if(a.
id()==ID_constant && b.
id()==ID_constant &&
675 a.
get(ID_value)==ID_NULL && b.
get(ID_value)==ID_NULL)
678 if(a.
id()==ID_constant && b.
id()==ID_address_of &&
679 a.
get(ID_value)==ID_NULL)
682 if(b.
id()==ID_constant && a.
id()==ID_address_of &&
683 b.
get(ID_value)==ID_NULL)
694 if(a.
id()==ID_symbol && b.
id()==ID_symbol)
699 else if(a.
id()==ID_index && b.
id()==ID_index)
704 else if(a.
id()==ID_member && b.
id()==ID_member)
716 auto new_expr = expr;
717 bool no_change =
true;
718 exprt &op = new_expr.op();
721 if(op_result.has_changed())
727 if(op.
id() == ID_address_of)
731 if(op_object.id() == ID_symbol)
736 if(size_opt.has_value())
739 exprt size = size_opt.value();
741 if(size.
type() != expr_type)
750 else if(op_object.id() == ID_string_constant)
761 return std::move(new_expr);
resultt simplify_rec(const exprt &)
resultt simplify_is_invalid_pointer(const unary_exprt &)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
static exprt conditional_cast(const exprt &expr, const typet &type)
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const typet & subtype() const
struct configt::bv_encodingt bv_encoding
resultt simplify_address_of(const address_of_exprt &)
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
exprt good_pointer_def(const exprt &pointer, const namespacet &ns)
The type of an expression, extends irept.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Operator to dereference a pointer.
The trinary if-then-else operator.
Various predicates over pointers in programs.
resultt simplify_inequality_address_of(const binary_relation_exprt &)
resultt simplify_is_dynamic_object(const unary_exprt &)
const string_constantt & to_string_constant(const exprt &expr)
The plus expression Associativity is not specified.
Base class for all expressions.
Generic base class for unary expressions.
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
resultt simplify_pointer_offset(const unary_exprt &)
struct configt::ansi_ct ansi_c
bitvector_typet index_type()
static resultt unchanged(exprt expr)
resultt simplify_node(exprt)
static bool is_dereference_integer_object(const exprt &expr, mp_integer &address)
resultt simplify_if(const if_exprt &)
optionalt< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
typet & type()
Return the type of the expression.
unsigned int get_instance() const
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const std::string & id2string(const irep_idt &d)
#define forall_operands(it, expr)
#define SYMEX_DYNAMIC_PREFIX
#define PRECONDITION(CONDITION)
static resultt changed(resultt<> result)
const irep_idt & get_identifier() const
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Binary multiplication Associativity is not specified.
resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
pointer_typet pointer_type(const typet &subtype)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
resultt simplify_good_pointer(const unary_exprt &)
const irep_idt & id() const
std::vector< exprt > operandst
The Boolean constant false.
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
resultt simplify_pointer_object(const unary_exprt &)
exprt pointer_offset(const exprt &pointer)
bitvector_typet char_type()
std::size_t get_width() const
bool is_zero() const
Return whether the expression is a constant representing 0.
Deprecated expression utility functions.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
resultt simplify_object(const exprt &)
static tvt objects_equal(const exprt &a, const exprt &b)
static tvt objects_equal_address_of(const exprt &a, const exprt &b)
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
resultt simplify_inequality_pointer_object(const binary_relation_exprt &)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const irep_idt & get(const irep_namet &name) const
bool value_is_zero_string() const
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
A base class for relations, i.e., binary predicates whose two operands have the same type.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
bool has_prefix(const std::string &s, const std::string &prefix)
irep_idt get_component_name() const
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
resultt simplify_address_of_arg(const exprt &)
Operator to return the address of an object.
Semantic type conversion.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
A constant literal expression.
resultt simplify_object_size(const unary_exprt &)
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
API to expression classes.
const irep_idt & get_value() const
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.