30 for(
unsigned i=0; i<
entries.size(); i++)
31 out <<
"STORE " << i <<
": " <<
to_string(i,
"") <<
'\n';
91 if(expr.
id()==ID_typecast)
95 if(expr.
type().
id()==ID_signedbv ||
96 expr.
type().
id()==ID_unsignedbv)
117 if(expr.
type().
id()==ID_pointer)
118 if(expr.
get(ID_value)==ID_NULL)
132 if(expr.
id()==ID_member)
138 if(expr.
id()==ID_symbol)
149 return object_store->get(expr, n);
154 if(expr.
id()==ID_address_of)
163 if(expr.
id()==ID_symbol)
165 else if(expr.
id()==ID_member)
170 else if(expr.
id()==ID_index)
181 const std::pair<unsigned, unsigned> &p,
184 eq_set.check_index(p.first);
185 eq_set.check_index(p.second);
188 unsigned f_r=eq_set.find(p.first);
189 unsigned s_r=eq_set.find(p.second);
191 for(
unsigned f=0; f<eq_set.size(); f++)
193 if(eq_set.find(f)==f_r)
195 for(
unsigned s=0; s<eq_set.size(); s++)
196 if(eq_set.find(s)==s_r)
197 dest.insert(std::pair<unsigned, unsigned>(f, s));
204 eq_set.make_union(p.first, p.second);
207 unsigned r=eq_set.find(p.first);
209 bool constant_seen=
false;
212 for(
unsigned i=0; i<eq_set.size(); i++)
214 if(eq_set.find(i)==
r)
216 if(object_store->is_constant(i))
232 for(
const auto &le : le_set)
233 add_eq(le_set, p, le);
235 for(
const auto &ne : ne_set)
236 add_eq(ne_set, p, ne);
241 const std::pair<unsigned, unsigned> &eq,
242 const std::pair<unsigned, unsigned> &ineq)
244 std::pair<unsigned, unsigned> n;
248 if(eq.first==ineq.first)
255 if(eq.first==ineq.second)
262 if(eq.second==ineq.first)
269 if(eq.second==ineq.second)
279 std::pair<unsigned, unsigned> s=p;
280 std::swap(s.first, s.second);
285 if(has_ne(p) || has_ne(s))
293 std::pair<unsigned, unsigned> s=p;
294 std::swap(s.first, s.second);
303 if(has_ne(s) || has_ne(p))
311 std::ostream &out)
const 322 for(
unsigned i=0; i<eq_set.size(); i++)
323 if(eq_set.is_root(i) &&
327 for(
unsigned j=0; j<eq_set.size(); j++)
328 if(eq_set.find(j)==i)
341 for(
const auto &bounds : bounds_map)
343 out <<
to_string(bounds.first, identifier)
344 <<
" in " << bounds.second
348 for(
const auto &le : le_set)
351 <<
" <= " <<
to_string(le.second, identifier)
355 for(
const auto &ne : ne_set)
358 <<
" != " <<
to_string(ne.second, identifier)
365 if(expr.
type()==type)
368 if(type.
id()==ID_unsignedbv)
375 if(get_object(expr, a))
392 if(expr.
type().
id()!=ID_bool)
393 throw "non-Boolean argument to strengthen()";
396 std::cout <<
"S: " <<
from_expr(*
ns,
"", expr) <<
'\n';
414 else if(expr.
id()==ID_not)
418 else if(expr.
id()==ID_and)
423 else if(expr.
id()==ID_le ||
431 if(expr.
op1().
id()==ID_bitand)
445 std::pair<unsigned, unsigned> p;
447 if(get_object(expr.
op0(), p.first) ||
448 get_object(expr.
op1(), p.second))
464 else if(expr.
id()==ID_lt)
479 else if(expr.
id()==ID_equal)
485 if(op_type.id()==ID_struct)
489 exprt lhs_member_expr(ID_member);
490 exprt rhs_member_expr(ID_member);
494 for(
const auto &comp : struct_type.
components())
496 const irep_idt &component_name=comp.get(ID_name);
498 lhs_member_expr.
set(ID_component_name, component_name);
499 rhs_member_expr.
set(ID_component_name, component_name);
500 lhs_member_expr.
type()=comp.type();
501 rhs_member_expr.
type()=comp.type();
504 equality.
lhs()=lhs_member_expr;
505 equality.
rhs()=rhs_member_expr;
508 strengthen_rec(equality);
517 if(expr.
op1().
id()==ID_bitand)
531 else if(expr.
op0().
id()==ID_bitand)
534 std::swap(tmp.
op0(), tmp.
op1());
540 if(expr.
op1().
id()==ID_typecast)
545 else if(expr.
op0().
id()==ID_typecast)
551 std::pair<unsigned, unsigned> p, s;
553 if(get_object(expr.
op0(), p.first) ||
554 get_object(expr.
op1(), p.second))
560 add_bounds(p.second,
boundst(i));
562 add_bounds(p.first,
boundst(i));
565 std::swap(s.first, s.second);
568 if(has_ne(p) || has_ne(s))
573 else if(expr.
id()==ID_notequal)
577 std::pair<unsigned, unsigned> p;
579 if(get_object(expr.
op0(), p.first) ||
580 get_object(expr.
op1(), p.second))
595 return implies_rec(tmp);
600 if(expr.
type().
id()!=ID_bool)
601 throw "implies: non-Boolean expression";
604 std::cout <<
"I: " <<
from_expr(*
ns,
"", expr) <<
'\n';
612 else if(expr.
id()==ID_not)
616 else if(expr.
id()==ID_and)
619 if(implies_rec(*it)!=
tvt(
true))
624 else if(expr.
id()==ID_or)
627 if(implies_rec(*it)==
tvt(
true))
630 else if(expr.
id()==ID_le ||
632 expr.
id()==ID_equal ||
633 expr.
id()==ID_notequal)
637 std::pair<unsigned, unsigned> p;
639 bool ob0=get_object(expr.
op0(), p.first);
640 bool ob1=get_object(expr.
op1(), p.second);
654 get_bounds(p.first, b0);
655 get_bounds(p.second, b1);
659 else if(expr.
id()==ID_lt)
666 get_bounds(p.first, b0);
667 get_bounds(p.second, b1);
671 else if(expr.
id()==ID_equal)
673 else if(expr.
id()==ID_notequal)
688 const exprt &e_a=object_store->get_expr(a);
696 if(e_a.
type().
id()==ID_unsignedbv)
700 bounds_mapt::const_iterator it=bounds_map.find(a);
702 if(it!=bounds_map.end())
708 if(expr.
type().
id()!=ID_bool)
709 throw "nnf: non-Boolean expression";
721 else if(expr.
id()==ID_not)
724 nnf(expr.
op0(), !negate);
729 else if(expr.
id()==ID_and)
737 else if(expr.
id()==ID_or)
745 else if(expr.
id()==ID_typecast)
749 if(expr.
op0().
type().
id()==ID_unsignedbv ||
764 else if(expr.
id()==ID_le)
770 std::swap(expr.
op0(), expr.
op1());
773 else if(expr.
id()==ID_lt)
779 std::swap(expr.
op0(), expr.
op1());
782 else if(expr.
id()==ID_ge)
789 std::swap(expr.
op0(), expr.
op1());
792 else if(expr.
id()==ID_gt)
799 std::swap(expr.
op0(), expr.
op1());
802 else if(expr.
id()==ID_equal)
805 expr.
id(ID_notequal);
807 else if(expr.
id()==ID_notequal)
822 if(expr.
id()==ID_address_of)
828 if(expr.
id()==ID_symbol ||
829 expr.
id()==ID_member)
831 exprt tmp=get_constant(expr);
841 if(!get_object(expr, a))
844 bounds_mapt::const_iterator it=bounds_map.
find(a);
846 if(it!=bounds_map.end())
848 if(it->second.singleton())
852 unsigned r=eq_set.find(a);
855 for(
unsigned i=0; i<eq_set.size(); i++)
856 if(eq_set.find(i)==
r)
858 const exprt &e=object_store->get_expr(i);
865 if(expr.
type().
id()==ID_pointer)
870 tmp.
set(ID_value, ID_NULL);
877 else if(object_store->is_constant_address(e))
905 return object_store->to_string(a, identifier);
936 unsigned old_eq_roots=eq_set.count_roots();
938 eq_set.intersection(other.
eq_set);
941 unsigned old_ne_set=ne_set.size();
942 unsigned old_le_set=le_set.size();
951 if(old_eq_roots!=eq_set.count_roots() ||
952 old_ne_set!=ne_set.size() ||
953 old_le_set!=le_set.size())
963 for(bounds_mapt::iterator
964 it=bounds_map.begin();
965 it!=bounds_map.end();
968 bounds_mapt::const_iterator o_it=other.find(it->first);
970 if(o_it==other.end())
972 bounds_mapt::iterator next(it);
974 bounds_map.erase(it);
981 it->second.approx_union_with(o_it->second);
1001 if(lhs.
id()==ID_symbol ||
1002 lhs.
id()==ID_member)
1005 if(!get_object(lhs, a))
1008 else if(lhs.
id()==ID_index)
1012 else if(lhs.
id()==ID_dereference)
1017 else if(lhs.
id()==
"object_value")
1022 else if(lhs.
id()==ID_if)
1026 modifies(lhs.
op1());
1027 modifies(lhs.
op2());
1029 else if(lhs.
id()==ID_typecast)
1033 modifies(lhs.
op0());
1035 else if(lhs.
id()==
"valid_object")
1038 else if(lhs.
id()==
"dynamic_size")
1041 else if(lhs.
id()==ID_byte_extract_little_endian ||
1042 lhs.
id()==ID_byte_extract_big_endian)
1046 modifies(lhs.
op0());
1048 else if(lhs.
id()==
"NULL-object" ||
1049 lhs.
id()==
"is_zero_string" ||
1050 lhs.
id()==
"zero_string" ||
1051 lhs.
id()==
"zero_string_length")
1056 throw "modifies: unexpected lhs: "+lhs.
id_string();
1075 strengthen(equality);
1082 if(statement==ID_block)
1087 else if(statement==ID_assign ||
1091 throw "assignment expected to have two operands";
1093 assignment(code.
op0(), code.
op1());
1095 else if(statement==ID_decl)
1098 assignment(code.
op0(), code.
op1());
1100 modifies(code.
op0());
1102 else if(statement==ID_expression)
1106 else if(statement==ID_function_call)
1111 else if(statement==ID_cpp_delete ||
1112 statement==ID_cpp_delete_array)
1116 else if(statement==ID_free)
1120 else if(statement==ID_printf)
1124 else if(statement==
"lock" ||
1125 statement==
"unlock" ||
1132 std::cerr << code.
pretty() <<
'\n';
1133 throw "invariant_sett: unexpected statement: "+
id2string(statement);
const irept & get_nil_irep()
void get_bounds(unsigned a, boundst &dest) const
The type of an expression.
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
const typet & follow(const typet &src) const
void strengthen_rec(const exprt &expr)
const std::string & id2string(const irep_idt &d)
static bool is_constant_address(const exprt &expr)
static void nnf(exprt &expr, bool negate=false)
const std::string integer2string(const mp_integer &n, unsigned base)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
void strengthen(const exprt &expr)
bool make_union(const invariant_sett &other_invariants)
void copy_to_operands(const exprt &expr)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
bool get(const exprt &expr, unsigned &n)
const componentst & components() const
void add(const std::pair< unsigned, unsigned > &p, ineq_sett &dest)
tvt is_eq(std::pair< unsigned, unsigned > p) const
std::string build_string(const exprt &expr) const
void add_type_bounds(const exprt &expr, const typet &type)
bool get_number(const T &a, number_type &n) const
void assignment(const exprt &lhs, const exprt &rhs)
exprt get_constant(const exprt &expr) const
interval_templatet< T > upper_interval(const T &u)
void output(std::ostream &out) const
tvt implies(const exprt &expr) const
const irep_idt & id() const
The boolean constant true.
void apply_code(const codet &code)
API to expression classes.
const irep_idt & get(const irep_namet &name) const
#define PRECONDITION(CONDITION)
unsigned add(const exprt &expr)
bool is_constant(unsigned n) const
#define forall_operands(it, expr)
unsigned_union_find eq_set
std::map< unsigned, boundst > bounds_mapt
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
std::string to_string(unsigned n, const irep_idt &identifier) const
The boolean constant false.
std::size_t get_width() const
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
void simplify(exprt &expr) const
Base class for all expressions.
std::string to_string(unsigned a, const irep_idt &identifier) const
void add_eq(const std::pair< unsigned, unsigned > &eq)
const std::string & get_string(const irep_namet &name) const
static bool is_constant_address_rec(const exprt &expr)
std::vector< entryt > entries
const std::string & id_string() const
#define Forall_operands(it, expr)
bool make_union_bounds_map(const bounds_mapt &other)
void intersection(const typename graph_nodet< E >::edgest &a, const typename graph_nodet< E >::edgest &b, typename graph_nodet< E >::edgest &dest)
Compute intersection of two edge sets, in linear time.
const codet & to_code(const exprt &expr)
std::set< std::pair< unsigned, unsigned > > ineq_sett
tvt implies_rec(const exprt &expr) const
A statement in a programming language.
void modifies(const exprt &lhs)
number_type number(const T &a)
Generic exception types primarily designed for use with invariants.
bool get_object(const exprt &expr, unsigned &n) const
void output(const irep_idt &identifier, std::ostream &out) const
const irept & find(const irep_namet &name) const
interval_templatet< T > lower_interval(const T &l)
void set(const irep_namet &name, const irep_idt &value)
tvt is_le(std::pair< unsigned, unsigned > p) const
bool simplify(exprt &expr, const namespacet &ns)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.