34 const std::unordered_set<symbol_exprt, irep_hash> &
address_taken,
41 else if(a.
id() == ID_pointer && b.
id() == ID_pointer)
49 const std::unordered_set<symbol_exprt, irep_hash> &
address_taken,
57 std::cout <<
"U: " <<
format(update_state_expr) <<
"\n";
58 std::cout <<
"u: " <<
format(update_state_expr.address()) <<
"\n";
59 std::cout <<
"T: " <<
format(update_state_expr.address().type()) <<
"\n";
60 std::cout <<
"E: " <<
format(evaluate_expr.
address()) <<
"\n";
71 std::cout <<
"M: ?\n";
83 update_state_expr.new_value(), evaluate_expr.
type()),
100 auto new_evaluate_expr =
101 evaluate_expr.
with_state(update_state_expr.state());
105 std::move(simplified_cond),
108 update_state_expr.new_value(), evaluate_expr.
type()),
111 std::move(simplified_new_evaluate_expr));
116 auto new_evaluate_expr = evaluate_expr.
with_state(update_state_expr.state());
117 auto simplified_new_evaluate_expr =
122 update_state_expr.new_value().type(), evaluate_expr.
type()))
135 auto simplified_same_object =
144 auto same_offset =
equal_exprt(offset_w, offset_r);
146 auto same =
and_exprt(simplified_same_object, same_offset);
148 auto simplified_same =
152 update_state_expr.new_value(), evaluate_expr.
type());
155 if_exprt(simplified_same, new_value, simplified_new_evaluate_expr);
162 return simplified_new_evaluate_expr;
165 auto object = update_state_expr.new_value();
173 std::move(simplified_same_object),
174 std::move(byte_extract),
175 std::move(simplified_new_evaluate_expr));
184 if(src.
state().
id() == ID_update_state)
190 else if(src.
state().
id() == ID_enter_scope_state)
196 else if(src.
state().
id() == ID_exit_scope_state)
203 return std::move(src);
216 if(evaluate_expr.
address() == allocate_expr.address())
222 auto symbol_expr =
symbol_exprt(identifier, object_type);
225 return std::move(evaluate_expr);
229 auto new_evaluate_expr = evaluate_expr;
230 new_evaluate_expr.
state() = allocate_expr.state();
231 return std::move(new_evaluate_expr);
234 return std::move(evaluate_expr);
244 const auto &deallocate_state_expr =
246 auto new_evaluate_expr =
247 evaluate_expr.
with_state(deallocate_state_expr.state());
248 return std::move(new_evaluate_expr);
257 const auto &enter_scope_state_expr =
259 auto new_evaluate_expr =
260 evaluate_expr.
with_state(enter_scope_state_expr.state());
261 return std::move(new_evaluate_expr);
270 const auto &exit_scope_state_expr =
272 auto new_evaluate_expr =
273 evaluate_expr.
with_state(exit_scope_state_expr.state());
274 return std::move(new_evaluate_expr);
279 if(src.
id() == ID_object_address)
281 else if(src.
id() == ID_element_address)
283 else if(src.
id() == ID_field_address)
285 else if(src.
id() == ID_plus)
288 for(
auto &op : plus_expr.operands())
289 if(op.type().id() == ID_pointer)
293 else if(src.
id() == ID_typecast)
296 if(op.type().id() == ID_pointer)
312 const std::unordered_set<symbol_exprt, irep_hash> &
address_taken,
315 const auto &pointer = src.
address();
319 if(
object.
id() == ID_object_address)
326 else if(identifier ==
"return_value")
336 const auto &symbol = ns.
lookup(identifier);
337 if(symbol.is_static_lifetime)
346 if(src.
state().
id() == ID_update_state)
353 else if(src.
state().
id() == ID_deallocate_state)
359 auto simplified_same_object =
364 simplified_same_object,
false_exprt(), new_live_object_expr);
366 else if(src.
state().
id() == ID_enter_scope_state)
378 auto simplified_same_object =
381 src.
with_state(enter_scope_state_expr.state()),
385 simplified_same_object,
true_exprt(), new_live_object_expr);
390 src.
with_state(enter_scope_state_expr.state()),
395 else if(src.
state().
id() == ID_exit_scope_state)
405 auto simplified_same_object =
408 src.
with_state(exit_scope_state_expr.state()),
412 simplified_same_object,
false_exprt(), new_live_object_expr);
417 src.
with_state(exit_scope_state_expr.state()),
423 return std::move(src);
430 const auto &pointer = src.
address();
434 if(
object.
id() == ID_object_address)
447 const auto &symbol = ns.
lookup(identifier);
454 if(src.
state().
id() == ID_update_state)
457 return std::move(src);
460 return std::move(src);
465 const auto &pointer = src.
address();
469 if(
object.
id() == ID_object_address)
477 if(src.
state().
id() == ID_update_state)
483 else if(src.
state().
id() == ID_enter_scope_state)
488 else if(src.
state().
id() == ID_exit_scope_state)
494 return std::move(src);
501 const auto &pointer = src.
address();
505 if(
object.
id() == ID_object_address)
508 auto size_opt =
size_of_expr(object_address_expr.object_type(), ns);
509 if(size_opt.has_value())
512 return std::move(src);
517 if(src.
state().
id() == ID_update_state)
522 return std::move(src);
527 const std::unordered_set<symbol_exprt, irep_hash> &
address_taken,
530 auto &state = src.
state();
532 auto &size = src.
size();
534 if(state.id() == ID_update_state)
543 else if(state.id() == ID_enter_scope_state)
553 auto enter_scope_address =
554 enter_scope_state_expr.object_type().id() == ID_array ?
556 enter_scope_state_expr.address();
567 pointer, enter_scope_state_expr.address(),
address_taken, ns);
570 auto simplified_same_object =
579 auto object_size_opt =
581 if(!object_size_opt.has_value())
582 return std::move(src);
592 if_exprt(simplified_same_object, simplified_upper, rec_result);
596 else if(state.id() == ID_exit_scope_state)
607 auto simplified_same_object =
623 return std::move(src);
627static bool is_one(
const exprt &src)
629 if(src.
id() == ID_typecast)
634 return value_opt.has_value() && *value_opt == 1;
643 return (type.
id() == ID_signedbv || type.
id() == ID_unsignedbv) &&
656 return integer_opt.has_value() && *integer_opt == 0;
661 const std::unordered_set<symbol_exprt, irep_hash> &
address_taken,
665 const auto &state = src.
state();
666 const auto &pointer = src.
address();
668 if(state.id() == ID_update_state)
672 auto cstring_in_old_state = src;
673 cstring_in_old_state.
op0() = update_state_expr.state();
674 auto simplified_cstring_in_old_state =
684 return simplified_cstring_in_old_state;
690 if(update_state_expr.new_value().is_zero())
695 auto simplified_same_object =
699 simplified_same_object,
true_exprt(), simplified_cstring_in_old_state);
702 else if(state.id() == ID_enter_scope_state)
710 else if(state.id() == ID_exit_scope_state)
719 if(pointer.id() == ID_plus)
723 if(plus_expr.operands().size() == 2 && is_one(plus_expr.op1()))
726 auto new_is_cstring = src;
727 new_is_cstring.
op1() = plus_expr.
op0();
732 return or_exprt(new_is_cstring, is_zero);
737 pointer.id() == ID_address_of &&
744 pointer.id() == ID_element_address &&
754 return std::move(src);
759 const std::unordered_set<symbol_exprt, irep_hash> &
address_taken,
762 const auto &state = src.
state();
763 const auto &pointer = src.
address();
765 if(state.id() == ID_update_state)
769 auto cstrlen_in_old_state = src.
with_state(update_state_expr.state());
770 auto simplified_cstrlen_in_old_state =
780 return simplified_cstrlen_in_old_state;
789 if(pointer == update_state_expr.address())
794 if(pointer.id() == ID_plus)
798 if(plus_expr.operands().size() == 2 && is_one(plus_expr.op1()))
801 auto new_is_cstring = src;
802 new_is_cstring.
op1() = plus_expr.
op0();
807 return or_exprt(new_is_cstring, is_zero);
812 pointer.id() == ID_address_of &&
821 pointer.id() == ID_element_address &&
833 return std::move(src);
838 const std::unordered_set<symbol_exprt, irep_hash> &
address_taken,
842 const auto &state = src.
state();
843 const auto &head = src.
head();
844 const auto &tail = src.
tail();
851 if(head_next.has_value() && tail_prev.has_value())
854 auto head_next_simplified =
856 auto tail_prev_simplified =
858 if(head_next_simplified == tail && tail_prev_simplified == head)
863 if(state.id() == ID_update_state)
868 const auto &update_type = update_state_expr.new_value().type();
869 if(update_type != src.
head().
type())
872 auto without_update = src.
with_state(update_state_expr.state());
876 else if(state.id() == ID_enter_scope_state)
883 else if(state.id() == ID_exit_scope_state)
891 return std::move(src);
896 const std::unordered_set<symbol_exprt, irep_hash> &
address_taken,
899 if(src.
pointer().
id() == ID_object_address)
904 else if(src.
pointer().
id() == ID_element_address)
909 auto size_opt =
size_of_expr(element_address_expr.element_type(), ns);
910 if(size_opt.has_value())
914 element_address_expr.index(), src.
type()),
921 return std::move(sum);
924 else if(src.
pointer().
id() == ID_address_of)
927 if(address_of_expr.object().id() == ID_string_constant)
930 else if(src.
pointer().
id() == ID_typecast)
942 return std::move(src);
947 const std::unordered_set<symbol_exprt, irep_hash> &
address_taken,
952 if(src.
pointer() != simplified_pointer)
955 return std::move(src);
960 const std::unordered_set<symbol_exprt, irep_hash> &
address_taken,
963 if(src.
id() == ID_allocate)
967 else if(src.
id() == ID_evaluate)
971 if(evaluate_expr.state().id() == ID_update_state)
975 else if(evaluate_expr.state().id() == ID_allocate_state)
979 else if(evaluate_expr.state().id() == ID_deallocate_state)
983 else if(evaluate_expr.state().id() == ID_enter_scope_state)
987 else if(evaluate_expr.state().id() == ID_exit_scope_state)
993 src.
id() == ID_state_r_ok || src.
id() == ID_state_w_ok ||
994 src.
id() == ID_state_rw_ok)
998 else if(src.
id() == ID_state_live_object)
1003 else if(src.
id() == ID_state_writeable_object)
1008 else if(src.
id() == ID_state_is_cstring)
1013 else if(src.
id() == ID_state_cstrlen)
1017 else if(src.
id() == ID_state_is_sentinel_dll)
1022 else if(src.
id() == ID_state_is_dynamic_object)
1027 else if(src.
id() == ID_plus)
1031 src.
type().
id() == ID_pointer &&
1032 plus_expr.op0().id() == ID_element_address)
1036 new_element_address_expr.index() =
plus_exprt(
1037 new_element_address_expr.index(),
1039 plus_expr.op1(), new_element_address_expr.index().type()));
1040 new_element_address_expr.index() =
1046 else if(src.
id() == ID_pointer_offset)
1051 else if(src.
id() == ID_pointer_object)
1056 else if(src.
id() == ID_state_object_size)
1060 else if(src.
id() == ID_equal)
1064 equal_expr.lhs().id() == ID_pointer_object &&
1065 equal_expr.rhs().id() == ID_pointer_object)
1069 if(lhs_p.id() == ID_object_address && rhs_p.id() == ID_object_address)
1086 const std::unordered_set<symbol_exprt, irep_hash> &
address_taken,
std::unordered_set< symbol_exprt, irep_hash > address_taken(const std::vector< exprt > &src)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
byte_extract_exprt make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
Construct a byte_extract_exprt with endianness and byte width matching the current configuration.
unsignedbv_typet size_type()
bitvector_typet char_type()
allocate_exprt with_state(exprt state) const
const exprt & state() const
typet index_type() const
The type of the index expressions into any instance of this type.
A base class for relations, i.e., binary predicates whose two operands have the same type.
std::size_t get_width() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Operator to return the address of an array element relative to a base address.
const exprt & state() const
const exprt & address() const
const exprt & state() const
evaluate_exprt with_state(exprt state) const
const exprt & state() const
Base class for all expressions.
bool is_false() const
Return whether the expression is a constant representing false.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
The Boolean constant false.
The trinary if-then-else operator.
const irep_idt & id() const
Binary multiplication Associativity is not specified.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Operator to return the address of an object.
irep_idt object_identifier() const
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.
const typet & base_type() const
The type of the data what we point to.
const exprt & state() const
state_cstrlen_exprt with_state(exprt state) const
const exprt & address() const
const exprt & address() const
const exprt & state() const
state_is_cstring_exprt with_state(exprt state) const
const exprt & state() const
const exprt & address() const
state_is_dynamic_object_exprt with_state(exprt state) const
const exprt & head() const
const exprt & state() const
state_is_sentinel_dll_exprt with_state(exprt state) const
const exprt & tail() const
const exprt & address() const
const exprt & state() const
state_live_object_exprt with_state(exprt state) const
const exprt & state() const
state_object_size_exprt with_state(exprt state) const
const exprt & address() const
state_ok_exprt with_state(exprt state) const
const exprt & size() const
const exprt & address() const
const exprt & state() const
const exprt & address() const
const exprt & state() const
Expression to hold a symbol (variable)
The Boolean constant true.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
Fixed-width bit-vector with unsigned binary interpretation.
const exprt & state() const
bool has_prefix(const std::string &s, const std::string &prefix)
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Deprecated expression utility functions.
static exprt implication(exprt lhs, exprt rhs)
const std::string & id2string(const irep_idt &d)
optionalt< exprt > may_alias(const exprt &a, const exprt &b, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
exprt may_be_same_object(const exprt &a, const exprt &b, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
const element_address_exprt & to_element_address_expr(const exprt &expr)
Cast an exprt to an element_address_exprt.
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)
Cast an exprt to a pointer_offset_exprt.
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
const field_address_exprt & to_field_address_expr(const exprt &expr)
Cast an exprt to an field_address_exprt.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
exprt pointer_offset(const exprt &pointer)
exprt object_size(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
Various predicates over pointers in programs.
optionalt< exprt > sentinel_dll_prev(const exprt &state, const exprt &node, const namespacet &ns)
optionalt< exprt > sentinel_dll_next(const exprt &state, const exprt &node, const namespacet &ns)
const state_is_sentinel_dll_exprt & to_state_is_sentinel_dll_expr(const exprt &expr)
Cast an exprt to a state_is_sentinel_dll_exprt.
exprt simplify_expr(exprt src, const namespacet &ns)
exprt simplify_evaluate_enter_scope_state(evaluate_exprt evaluate_expr, const namespacet &ns)
exprt simplify_allocate(allocate_exprt src)
exprt simplify_is_dynamic_object_expr(state_is_dynamic_object_exprt src)
exprt simplify_object_expression_rec(exprt src)
static bool is_zero_char(const exprt &src, const namespacet &ns)
exprt simplify_live_object_expr(state_live_object_exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
exprt simplify_is_sentinel_dll_expr(state_is_sentinel_dll_exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
exprt simplify_evaluate_exit_scope_state(evaluate_exprt evaluate_expr, const namespacet &ns)
exprt simplify_ok_expr(state_ok_exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
exprt simplify_state_expr_node(exprt, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &)
exprt simplify_is_cstring_expr(state_is_cstring_exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
exprt simplify_evaluate_update(evaluate_exprt evaluate_expr, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
exprt simplify_cstrlen_expr(state_cstrlen_exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
std::size_t allocate_counter
exprt simplify_pointer_offset_expr(pointer_offset_exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
static bool is_a_char_type(const typet &type)
exprt simplify_evaluate_deallocate_state(evaluate_exprt evaluate_expr, const namespacet &ns)
exprt simplify_object_expression(exprt src)
exprt simplify_object_size_expr(state_object_size_exprt src, const namespacet &ns)
exprt simplify_state_expr(exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
exprt simplify_writeable_object_expr(state_writeable_object_exprt src, const namespacet &ns)
exprt simplify_pointer_object_expr(pointer_object_exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
exprt simplify_evaluate_allocate_state(evaluate_exprt evaluate_expr, const namespacet &ns)
static bool types_are_compatible(const typet &a, const typet &b)
Simplify State Expression.
#define PRECONDITION(CONDITION)
const state_ok_exprt & to_state_ok_expr(const exprt &expr)
Cast an exprt to a state_ok_exprt.
const state_is_cstring_exprt & to_state_is_cstring_expr(const exprt &expr)
Cast an exprt to a state_is_cstring_exprt.
const state_cstrlen_exprt & to_state_cstrlen_expr(const exprt &expr)
Cast an exprt to a state_cstrlen_exprt.
const exit_scope_state_exprt & to_exit_scope_state_expr(const exprt &expr)
Cast an exprt to a exit_scope_state_exprt.
const enter_scope_state_exprt & to_enter_scope_state_expr(const exprt &expr)
Cast an exprt to a enter_scope_state_exprt.
const state_writeable_object_exprt & to_state_writeable_object_expr(const exprt &expr)
Cast an exprt to a state_writeable_object_exprt.
const state_is_dynamic_object_exprt & to_state_is_dynamic_object_expr(const exprt &expr)
Cast an exprt to a state_is_dynamic_object_exprt.
const state_object_size_exprt & to_state_object_size_expr(const exprt &expr)
Cast an exprt to a state_object_size_exprt.
const update_state_exprt & to_update_state_expr(const exprt &expr)
Cast an exprt to a update_state_exprt.
const deallocate_state_exprt & to_deallocate_state_expr(const exprt &expr)
Cast an exprt to a deallocate_state_exprt.
const allocate_exprt & to_allocate_expr(const exprt &expr)
Cast an exprt to a allocate_exprt.
const evaluate_exprt & to_evaluate_expr(const exprt &expr)
Cast an exprt to a evaluate_exprt.
const state_live_object_exprt & to_state_live_object_expr(const exprt &expr)
Cast an exprt to a state_live_object_exprt.
API to expression classes.
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 equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.