42 if(src.
id() == ID_array)
45 array_type.element_type() =
replace(array_type.element_type());
46 array_type.size() =
replace(array_type.size());
49 else if(src.
id() == ID_pointer)
64 for(
auto b_it = std::next(a_it); b_it !=
evaluate_exprs.end(); b_it++)
66 if(a_it->state() != b_it->state())
69 auto a_op = a_it->address();
71 b_it->address(), a_it->address().type());
94 if(a_it->state() != b_it->state())
96 auto a_op = a_it->address();
98 b_it->address(), a_it->address().type());
118 auto pointers_equal =
same_object(a_it->address(), *b_it);
135 if(a_it->state() != b_it->state())
137 auto operands_equal =
same_object(a_it->address(), b_it->address());
157 auto pointers_equal =
same_object(a_it->address(), *b_it);
170 if(a_it->object_identifier() ==
"return_value")
181 auto &symbol =
ns.
lookup(a_it->object_expr());
182 bool is_const = symbol.type.get_bool(ID_C_constant);
187 auto pointers_equal =
same_object(*a_it, b_it->address());
189 :
static_cast<exprt>(*b_it);
208 if(a_it->state() != b_it->state())
210 auto operands_equal =
same_object(a_it->address(), b_it->address());
230 if(a_it->state() != b_it->state())
232 auto operands_equal =
same_object(a_it->address(), b_it->address());
247 if(src_simplified != src)
251 std::cout <<
"OBJECT_SIZE1: " <<
format(equal) <<
'\n';
263 if(b_it->object().id() == ID_string_constant)
266 auto pointers_equal =
same_object(a_it->address(), *b_it);
269 from_integer(string_constant.get_value().size() + 1, a_it->type()));
287 if(a_it->state() != b_it->state())
289 auto operands_equal =
same_object(a_it->address(), b_it->address());
304 for(
auto b_it = std::next(a_it); b_it !=
ok_exprs.end(); b_it++)
306 if(a_it->id() != b_it->id())
308 if(a_it->state() != b_it->state())
310 if(a_it->size() != b_it->size())
312 auto a_op = a_it->address();
314 b_it->address(), a_it->address().type());
333 if(
ns.
lookup(
object.get_identifier(), symbol))
365 src.
id() == ID_initial_state || src.
id() == ID_evaluate ||
366 src.
id() == ID_state_is_cstring || src.
id() == ID_state_cstrlen ||
367 src.
id() == ID_state_is_sentinel_dll ||
368 src.
id() == ID_state_is_dynamic_object ||
369 src.
id() == ID_state_object_size || src.
id() == ID_state_live_object ||
370 src.
id() == ID_state_writeable_object || src.
id() == ID_state_r_ok ||
371 src.
id() == ID_state_w_ok || src.
id() == ID_state_rw_ok ||
372 src.
id() == ID_allocate || src.
id() == ID_reallocate)
382 if(src.
id() == ID_state_is_cstring)
385 std::cout <<
"R " <<
format(s) <<
" --> " <<
format(src) <<
'\n';
402 if(src.
id() == ID_state_is_cstring)
406 else if(src.
id() == ID_state_is_sentinel_dll)
416 is_sentinel_dll_expr.state(),
417 is_sentinel_dll_expr.head(),
418 *ok_expr_h_size_opt);
425 is_sentinel_dll_expr.state(),
426 is_sentinel_dll_expr.tail(),
427 *ok_expr_t_size_opt);
434 std::cout <<
"AXIOM-is-sentinel-dll-1: " <<
format(instance1) <<
"\n";
441 is_sentinel_dll_expr.state(), is_sentinel_dll_expr.head(),
ns);
444 is_sentinel_dll_expr.state(), is_sentinel_dll_expr.tail(),
ns);
446 if(head_next.has_value() && tail_prev.has_value())
448 auto head_next_is_tail =
449 equal_exprt(*head_next, is_sentinel_dll_expr.tail());
451 auto tail_prev_is_head =
452 equal_exprt(*tail_prev, is_sentinel_dll_expr.head());
456 ok_expr_h, ok_expr_t ),
460 std::cout <<
"AXIOM-is-sentinel-dll-2: " <<
format(instance2) <<
"\n";
465 else if(src.
id() == ID_evaluate)
470 else if(src.
id() == ID_state_live_object)
480 std::cout <<
"AXIOMc: " <<
format(instance) <<
"\n";
484 else if(src.
id() == ID_state_writeable_object)
489 else if(src.
id() == ID_state_is_dynamic_object)
494 else if(src.
id() == ID_allocate)
500 auto live_object_expr =
503 auto instance1 =
replace(live_object_expr);
505 std::cout <<
"ALLOCATE1: " <<
format(instance1) <<
"\n";
509 auto writeable_object_expr =
512 auto instance2 =
replace(writeable_object_expr);
514 std::cout <<
"ALLOCATE2: " <<
format(instance2) <<
"\n";
519 allocate_expr.state(), allocate_expr, allocate_expr.size().type());
524 std::cout <<
"ALLOCATE3: " <<
format(instance3) <<
"\n";
531 pointer_offset_expr,
from_integer(0, pointer_offset_expr.type())));
533 std::cout <<
"ALLOCATE4: " <<
format(instance4) <<
"\n";
537 auto is_dynamic_object_expr =
540 auto instance5 =
replace(is_dynamic_object_expr);
542 std::cout <<
"ALLOCATE5: " <<
format(instance5) <<
"\n";
545 else if(src.
id() == ID_reallocate)
551 auto live_object_expr =
554 auto instance1 =
replace(live_object_expr);
556 std::cout <<
"REALLOCATE1: " <<
format(instance1) <<
"\n";
561 reallocate_expr.state(), reallocate_expr, reallocate_expr.size().type());
566 std::cout <<
"REALLOCATE2: " <<
format(instance2) <<
"\n";
573 pointer_offset_expr,
from_integer(0, pointer_offset_expr.type())));
575 std::cout <<
"REALLOCATE3: " <<
format(instance3) <<
"\n";
579 auto is_dynamic_object_expr =
582 auto instance4 =
replace(is_dynamic_object_expr);
584 std::cout <<
"REALLOCATE4: " <<
format(instance4) <<
"\n";
587 else if(src.
id() == ID_deallocate_state)
596 deallocate_state_expr, deallocate_state_expr.address());
600 std::cout <<
"DEALLOCATE1: " <<
format(instance1) <<
"\n";
604 else if(src.
id() == ID_address_of)
608 else if(src.
id() == ID_object_address)
612 else if(src.
id() == ID_state_object_size)
617 else if(src.
id() == ID_initial_state)
622 src.
id() == ID_state_r_ok || src.
id() == ID_state_w_ok ||
623 src.
id() == ID_state_rw_ok)
631 if(!
ok_exprs.insert(ok_expr).second)
634 const auto &state = ok_expr.
state();
635 const auto &pointer = ok_expr.
address();
636 const auto &size = ok_expr.
size();
645 auto live_object_simplified =
651 auto writeable_object_simplified =
656 auto offset_simplified =
671 auto offset_casted_to_unsigned =
674 offset_casted_to_unsigned, size_type_ext);
677 plus_exprt(offset_extended, size_casted), ID_le, object_size_casted);
681 if(ok_expr.
id() == ID_state_w_ok || ok_expr.
id() == ID_state_rw_ok)
687 std::cout <<
"AXIOMd: " <<
format(instance) <<
"\n";
696 std::cout <<
"AXIOMe: " <<
format(instance) <<
"\n";
710 is_cstring_expr.
state(),
717 std::cout <<
"AXIOMa1: " <<
format(instance1) <<
"\n";
721 ok_simplified.visit_pre([
this](
const exprt &src) {
node(src); });
724 std::cout <<
"AXIOMa2: " <<
format(instance2) <<
"\n";
731 auto state = is_cstring_expr.
state();
732 auto p = is_cstring_expr.
address();
743 std::cout <<
"AXIOMb: " <<
format(instance) <<
"\n";
746 add(is_cstring_plus_one,
true);
754 constraint.visit_pre([
this](
const exprt &src) {
node(src); });
756 auto constraint_replaced =
replace(constraint);
760 std::cout <<
"CONSTRAINT1: " <<
format(constraint) <<
"\n";
761 std::cout <<
"CONSTRAINT2: " <<
format(constraint_replaced) <<
"\n";
764 dest << constraint_replaced;
unsignedbv_typet size_type()
signedbv_typet signed_size_type()
bitvector_typet char_type()
void is_dynamic_object_fc()
std::set< address_of_exprt > address_of_exprs
std::set< state_ok_exprt > ok_exprs
std::unordered_map< exprt, symbol_exprt, irep_hash > replacement_map
std::set< object_address_exprt > object_address_exprs
std::set< state_live_object_exprt > live_object_exprs
std::set< evaluate_exprt > evaluate_exprs
std::set< state_is_dynamic_object_exprt > is_dynamic_object_exprs
std::set< state_is_sentinel_dll_exprt > is_sentinel_dll_exprs
std::set< initial_state_exprt > initial_state_exprs
std::set< state_writeable_object_exprt > writeable_object_exprs
std::map< irep_idt, std::size_t > counters
exprt translate(exprt) const
std::set< state_is_cstring_exprt > is_cstring_exprs
const std::unordered_set< symbol_exprt, irep_hash > & address_taken
decision_proceduret & dest
std::set< state_object_size_exprt > object_size_exprs
std::vector< exprt > constraints
void add(const state_ok_exprt &)
void writeable_object_fc()
A base class for relations, i.e., binary predicates whose two operands have the same type.
std::size_t get_width() const
Base class for all expressions.
typet & type()
Return the type of the expression.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
const std::string & id_string() const
const irep_idt & id() const
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.
The plus expression Associativity is not specified.
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 & address() const
const exprt & state() const
const exprt & size() const
const exprt & address() const
const exprt & state() const
Expression to hold a symbol (variable)
An expression with three operands.
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.
bool has_prefix(const std::string &s, const std::string &prefix)
Decision Procedure Interface.
static exprt implication(exprt lhs, exprt rhs)
const std::string & id2string(const irep_idt &d)
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.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
exprt pointer_offset(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
exprt null_object(const exprt &pointer)
Various predicates over pointers in programs.
exprt simplify_state_expr_node(exprt, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &)
exprt simplify_state_expr(exprt, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &)
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.
Simplify State Expression.
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 reallocate_exprt & to_reallocate_expr(const exprt &expr)
Cast an exprt to a reallocate_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 deallocate_state_exprt & to_deallocate_state_expr(const exprt &expr)
Cast an exprt to a deallocate_state_exprt.
const initial_state_exprt & to_initial_state_expr(const exprt &expr)
Cast an exprt to a initial_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.
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const string_constantt & to_string_constant(const exprt &expr)