Go to the documentation of this file.
31 for(std::size_t i=0; i<
entries.size(); i++)
32 out <<
"STORE " << i <<
": " <<
to_string(i,
"") <<
'\n';
97 if(expr.
id()==ID_typecast)
102 typecast_expr.type().id() == ID_signedbv ||
103 typecast_expr.type().id() == ID_unsignedbv)
105 const typet &op_type = typecast_expr.op().type();
107 if(op_type.
id() == ID_signedbv || op_type.
id() == ID_unsignedbv)
116 else if(op_type.
id() == ID_bool)
128 if(expr.
type().
id()==ID_pointer)
129 if(expr.
get(ID_value)==ID_NULL)
132 const auto i = numeric_cast<mp_integer>(expr);
144 if(expr.
id()==ID_member)
150 if(expr.
id()==ID_symbol)
166 if(expr.
id()==ID_address_of)
174 if(expr.
id()==ID_symbol)
176 else if(expr.
id()==ID_member)
178 else if(expr.
id()==ID_index)
181 if(index_expr.index().is_constant())
189 const std::pair<unsigned, unsigned> &p,
205 dest.insert(std::pair<unsigned, unsigned>(f, s));
217 bool constant_seen=
false;
240 for(
const auto &le :
le_set)
243 for(
const auto &ne :
ne_set)
249 const std::pair<unsigned, unsigned> &eq,
250 const std::pair<unsigned, unsigned> &ineq)
252 std::pair<unsigned, unsigned> n;
256 if(eq.first==ineq.first)
263 if(eq.first==ineq.second)
270 if(eq.second==ineq.first)
277 if(eq.second==ineq.second)
287 std::pair<unsigned, unsigned> s=p;
288 std::swap(s.first, s.second);
301 std::pair<unsigned, unsigned> s=p;
302 std::swap(s.first, s.second);
319 std::ostream &out)
const
351 out <<
to_string(bounds.first, identifier)
352 <<
" in " << bounds.second
356 for(
const auto &le :
le_set)
359 <<
" <= " <<
to_string(le.second, identifier)
363 for(
const auto &ne :
ne_set)
366 <<
" != " <<
to_string(ne.second, identifier)
373 if(expr.
type()==type)
376 if(type.
id()==ID_unsignedbv)
400 if(expr.
type().
id()!=ID_bool)
401 throw "non-Boolean argument to strengthen()";
404 std::cout <<
"S: " <<
from_expr(*
ns,
"", expr) <<
'\n';
422 else if(expr.
id()==ID_not)
426 else if(expr.
id()==ID_and)
431 else if(expr.
id()==ID_le ||
439 if(rel.op1().id() == ID_bitand)
453 std::pair<unsigned, unsigned> p;
458 const auto i0 = numeric_cast<mp_integer>(rel.op0());
459 const auto i1 = numeric_cast<mp_integer>(rel.op1());
465 else if(i1.has_value())
470 else if(expr.
id()==ID_lt)
474 else if(i1.has_value())
485 else if(expr.
id()==ID_equal)
491 if(op_type.
id()==ID_struct)
496 for(
const auto &comp : struct_type.
components())
499 equal_expr.op0(), comp.get_name(), comp.type());
501 equal_expr.op1(), comp.get_name(), comp.type());
503 const equal_exprt equality(lhs_member_expr, rhs_member_expr);
515 if(equal_expr.op1().id() == ID_bitand)
517 const exprt &bitand_op = equal_expr.
op1();
521 exprt tmp(equal_expr);
529 else if(equal_expr.op0().id() == ID_bitand)
531 exprt tmp(equal_expr);
532 std::swap(tmp.
op0(), tmp.
op1());
538 if(equal_expr.op1().id() == ID_typecast)
543 else if(equal_expr.op0().id() == ID_typecast)
549 std::pair<unsigned, unsigned> p, s;
558 const auto i0 = numeric_cast<mp_integer>(equal_expr.op0());
559 const auto i1 = numeric_cast<mp_integer>(equal_expr.op1());
562 else if(i1.has_value())
566 std::swap(s.first, s.second);
574 else if(expr.
id()==ID_notequal)
578 std::pair<unsigned, unsigned> p;
604 if(expr.
type().
id()!=ID_bool)
605 throw "implies: non-Boolean expression";
608 std::cout <<
"I: " <<
from_expr(*
ns,
"", expr) <<
'\n';
616 else if(expr.
id()==ID_not)
620 else if(expr.
id()==ID_and)
628 else if(expr.
id()==ID_or)
634 else if(expr.
id()==ID_le ||
636 expr.
id()==ID_equal ||
637 expr.
id()==ID_notequal)
641 std::pair<unsigned, unsigned> p;
651 if(rel.id() == ID_le)
663 else if(rel.id() == ID_lt)
675 else if(rel.id() == ID_equal)
677 else if(rel.id() == ID_notequal)
693 const auto tmp = numeric_cast<mp_integer>(e_a);
700 if(e_a.
type().
id()==ID_unsignedbv)
704 bounds_mapt::const_iterator it=
bounds_map.find(a);
712 if(expr.
type().
id()!=ID_bool)
713 throw "nnf: non-Boolean expression";
725 else if(expr.
id()==ID_not)
732 else if(expr.
id()==ID_and)
740 else if(expr.
id()==ID_or)
748 else if(expr.
id()==ID_typecast)
753 typecast_expr.op().type().id() == ID_unsignedbv ||
754 typecast_expr.op().type().id() == ID_signedbv)
757 tmp.
lhs() = typecast_expr.op();
767 else if(expr.
id()==ID_le)
773 std::swap(expr.
op0(), expr.
op1());
776 else if(expr.
id()==ID_lt)
782 std::swap(expr.
op0(), expr.
op1());
785 else if(expr.
id()==ID_ge)
792 std::swap(expr.
op0(), expr.
op1());
795 else if(expr.
id()==ID_gt)
802 std::swap(expr.
op0(), expr.
op1());
805 else if(expr.
id()==ID_equal)
808 expr.
id(ID_notequal);
810 else if(expr.
id()==ID_notequal)
824 if(expr.
id()==ID_address_of)
830 if(expr.
id()==ID_symbol ||
831 expr.
id()==ID_member)
846 bounds_mapt::const_iterator it=
bounds_map.find(a);
850 if(it->second.singleton())
864 const mp_integer value = numeric_cast_v<mp_integer>(e);
866 if(expr.
type().
id()==ID_pointer)
935 std::size_t old_ne_set=
ne_set.size();
936 std::size_t old_le_set=
le_set.size();
946 old_ne_set!=
ne_set.size() ||
947 old_le_set!=
le_set.size())
957 for(bounds_mapt::iterator
962 bounds_mapt::const_iterator o_it=other.find(it->first);
964 if(o_it==other.end())
966 bounds_mapt::iterator next(it);
975 it->second.approx_union_with(o_it->second);
995 if(lhs.
id()==ID_symbol ||
1002 else if(lhs.
id()==ID_index)
1006 else if(lhs.
id()==ID_dereference)
1011 else if(lhs.
id()==
"object_value")
1016 else if(lhs.
id()==ID_if)
1023 else if(lhs.
id()==ID_typecast)
1029 else if(lhs.
id()==
"valid_object")
1032 else if(lhs.
id()==
"dynamic_size")
1035 else if(lhs.
id()==ID_byte_extract_little_endian ||
1036 lhs.
id()==ID_byte_extract_big_endian)
1042 else if(lhs.
id() == ID_null_object ||
1043 lhs.
id() ==
"is_zero_string" ||
1044 lhs.
id() ==
"zero_string" ||
1045 lhs.
id() ==
"zero_string_length")
1050 throw "modifies: unexpected lhs: "+lhs.
id_string();
1076 if(statement==ID_block)
1081 else if(statement==ID_assign)
1084 throw "assignment expected to have two operands";
1088 else if(statement==ID_decl)
1095 else if(statement==ID_expression)
1099 else if(statement==ID_function_call)
1104 else if(statement==ID_cpp_delete ||
1105 statement==ID_cpp_delete_array)
1109 else if(statement==ID_printf)
1113 else if(statement==
"lock" ||
1114 statement==
"unlock" ||
1121 std::cerr << code.
pretty() <<
'\n';
1122 throw "invariant_sett: unexpected statement: "+
id2string(statement);
const componentst & components() const
void strengthen(const exprt &expr)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
#define PRECONDITION(CONDITION)
interval_templatet< mp_integer > boundst
size_type find(size_type a) const
#define Forall_operands(it, expr)
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
tvt implies(const exprt &expr) const
std::set< std::pair< unsigned, unsigned > > ineq_sett
void get_bounds(unsigned a, boundst &dest) const
void check_index(size_type a)
The type of an expression, extends irept.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
void add_type_bounds(const exprt &expr, const typet &type)
tvt is_lt(std::pair< unsigned, unsigned > p) const
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Base class for all expressions.
void intersection(const unsigned_union_find &other)
tvt is_le(std::pair< unsigned, unsigned > p) const
optionalt< number_type > get_number(const key_type &a) const
bool make_union_bounds_map(const bounds_mapt &other)
bool is_true() const
Return whether the expression is a constant representing true.
std::string to_string(unsigned n, const irep_idt &identifier) const
#define UNREACHABLE
This should be used to mark dead code.
static void nnf(exprt &expr, bool negate=false)
std::vector< entryt > entries
bool is_false() const
Return whether the expression is a constant representing false.
number_type number(const key_type &a)
void apply_code(const codet &code)
const codet & to_code(const exprt &expr)
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
typet & type()
Return the type of the expression.
unsigned add(const exprt &expr)
size_type count(size_type a) const
static void intersection(ineq_sett &dest, const ineq_sett &other)
unsigned_union_find eq_set
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
void add_le(const std::pair< unsigned, unsigned > &p)
The null pointer constant.
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)
void make_union(size_type a, size_type b)
#define forall_operands(it, expr)
void add_eq(const std::pair< unsigned, unsigned > &eq)
void output(const irep_idt &identifier, std::ostream &out) const
const exprt & get_expr(unsigned n) const
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
bool get(const exprt &expr, unsigned &n)
const std::string & id_string() const
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
void modifies(const exprt &lhs)
bool is_constant(unsigned n) const
The Boolean constant false.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
static void remove(ineq_sett &dest, unsigned a)
tvt implies_rec(const exprt &expr) const
void add_ne(const std::pair< unsigned, unsigned > &p)
bool has_le(const std::pair< unsigned, unsigned > &p) const
inv_object_storet * object_store
void output(std::ostream &out) const
std::size_t get_width() const
void add(const std::pair< unsigned, unsigned > &p, ineq_sett &dest)
typename Map::mapped_type number_type
interval_templatet< T > lower_interval(const T &l)
std::map< unsigned, boundst > bounds_mapt
Extract member of struct or union.
Deprecated expression utility functions.
const std::string & get_string(const irep_namet &name) const
Structure type, corresponds to C style structs.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const irep_idt & get(const irep_namet &name) const
void assignment(const exprt &lhs, const exprt &rhs)
std::string build_string(const exprt &expr) const
size_type count_roots() const
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
bool is_constant() const
Return whether the expression is a constant.
void simplify(exprt &expr) const
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
bool get_object(const exprt &expr, unsigned &n) const
bool make_union(const invariant_sett &other_invariants)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const irept & get_nil_irep()
tvt is_ne(std::pair< unsigned, unsigned > p) const
bool is_root(size_type a) const
exprt get_constant(const exprt &expr) const
static bool is_constant_address_rec(const exprt &expr)
Semantic type conversion.
std::string to_string(unsigned a, const irep_idt &identifier) const
The Boolean constant true.
void isolate(size_type a)
void strengthen_rec(const exprt &expr)
tvt is_eq(std::pair< unsigned, unsigned > p) const
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
static bool is_constant_address(const exprt &expr)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
void add_bounds(unsigned a, const boundst &bound)
bool has_ne(const std::pair< unsigned, unsigned > &p) const
bool has_eq(const std::pair< unsigned, unsigned > &p) const
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
interval_templatet< T > upper_interval(const T &u)
Data structure for representing an arbitrary statement in a program.
const std::string integer2string(const mp_integer &n, unsigned base)