35 #define forall_objects(it, map) \ 36 for(object_map_dt::const_iterator (it) = (map).begin(); \ 40 #define forall_valid_objects(it, map) \ 41 for(object_map_dt::const_iterator (it) = (map).begin(); \ 44 if((map).is_valid_at((it)->first, from_function, from_target_index)) 46 #define Forall_objects(it, map) \ 47 for(object_map_dt::iterator (it) = (map).begin(); \ 51 #define Forall_valid_objects(it, map) \ 52 for(object_map_dt::iterator (it) = (map).begin(); \ 55 if((map).is_valid_at((it)->first, from_function, from_target_index)) 59 std::ostream &out)
const 61 for(valuest::const_iterator
71 std::ostream &out)
const 89 identifier=symbol.
name;
97 out << display_name <<
" = { ";
107 std::string result=
"<";
109 if(o.
id()==ID_invalid)
113 if(o.
type().
id()==ID_unknown)
115 else if(o.
type().
id()==ID_invalid)
121 else if(o.
id()==ID_unknown)
125 if(o.
type().
id()==ID_unknown)
127 else if(o.
type().
id()==ID_invalid)
135 result+=
from_expr(ns, identifier, o)+
", ";
137 if(o_it->second.offset_is_set)
144 if(o.
type().
id()==ID_unknown)
155 out << result <<
'\n';
158 object_map_dt::validity_rangest::const_iterator vr =
163 if(vr->second.empty())
164 std::cout <<
" Empty validity record\n";
167 for(object_map_dt::vrange_listt::const_iterator vit =
169 vit!=vr->second.end();
173 " [" << vit->from <<
"," << vit->to <<
"]";
176 from_target_index<=vit->to)
184 out <<
" No validity information\n";
188 width+=result.size();
193 if(next!=object_map.
read().
end())
206 if(
object.
id()==ID_invalid ||
207 object.
id()==ID_unknown)
214 if(it->second.offset_is_set)
258 dest.
write()[it->first] = it->second;
268 std::list<exprt> &value_set,
275 value_set.push_back(
to_expr(it));
278 for(std::list<exprt>::const_iterator it=value_set.begin();
279 it!=value_set.end(); it++)
280 std::cout <<
"GET_VALUE_SET: " <<
from_expr(ns,
"", *it) <<
'\n';
298 const std::string &suffix,
299 const typet &original_type,
303 std::cout <<
"GET_VALUE_SET_REC EXPR: " << expr <<
'\n';
304 std::cout <<
"GET_VALUE_SET_REC SUFFIX: " << suffix <<
'\n';
308 if(expr.id()==ID_unknown || expr.id()==ID_invalid)
313 else if(expr.id()==ID_index)
315 assert(expr.operands().size()==2);
319 assert(type.id()==ID_array ||
320 type.id()==ID_incomplete_array);
326 else if(expr.id()==ID_member)
328 assert(expr.operands().size()==1);
330 if(expr.op0().is_not_nil())
334 assert(type.
id()==ID_struct ||
335 type.
id()==ID_union ||
336 type.
id()==ID_incomplete_struct ||
337 type.
id()==ID_incomplete_union);
339 const std::string &component_name=
348 else if(expr.id()==ID_symbol)
352 irep_idt ident = expr.get_string(ID_identifier)+suffix;
361 valuest::const_iterator v_it=
values.find(ident);
370 else if(expr.id()==ID_if)
372 if(expr.operands().size()!=3)
373 throw "if takes three operands";
382 else if(expr.id()==ID_address_of)
384 if(expr.operands().size()!=1)
385 throw expr.id_string()+
" expected to have one operand";
391 else if(expr.id()==ID_dereference)
397 if(object_map.
begin()!=object_map.
end())
409 else if(expr.id()==
"reference_to")
417 if(object_map.
begin()!=object_map.
end())
429 else if(expr.is_constant())
432 if(expr.get(ID_value)==ID_NULL &&
433 expr.type().id()==ID_pointer)
439 else if(expr.id()==ID_typecast)
441 if(expr.operands().size()!=1)
442 throw "typecast takes one operand";
449 else if(expr.id()==ID_plus || expr.id()==ID_minus)
451 if(expr.operands().size()<2)
452 throw expr.id_string()+
" expected to have at least two operands";
454 if(expr.type().id()==ID_pointer)
457 const exprt *ptr_operand=
nullptr;
460 if(it->type().id()==ID_pointer)
462 if(ptr_operand==
nullptr)
465 throw "more than one pointer operand in pointer arithmetic";
468 if(ptr_operand==
nullptr)
469 throw "pointer type sum expected to have pointer operand";
473 ptr_operand->
type(), ns);
479 if(
object.offset_is_zero() &&
480 expr.operands().size()==2)
482 if(expr.op0().type().id()!=ID_pointer)
488 object.offset=(expr.id()==ID_plus)? i : -i;
494 object.offset_is_set=
false;
496 object.offset=(expr.id()==ID_plus)? i : -i;
500 object.offset_is_set=
false;
508 else if(expr.id()==ID_side_effect)
510 const irep_idt &statement=expr.get(ID_statement);
512 if(statement==ID_function_call)
515 throw "unexpected function_call sideeffect";
517 else if(statement==ID_malloc)
519 if(expr.type().id()!=ID_pointer)
520 throw "malloc expected to return pointer type";
524 const typet &dynamic_type=
525 static_cast<const typet &
>(expr.find(ID_C_cxx_alloc_type));
536 else if(statement==ID_cpp_new ||
537 statement==ID_cpp_new_array)
540 assert(expr.type().id()==ID_pointer);
552 else if(expr.id()==ID_struct)
558 else if(expr.id()==ID_with ||
559 expr.id()==ID_array_of ||
563 throw "unexpected value in get_value_set: "+expr.id_string();
565 else if(expr.id()==ID_dynamic_object)
570 const std::string name=
571 "value_set::dynamic_object"+
576 valuest::const_iterator v_it=
values.find(name);
593 if(src.
id()==ID_typecast)
595 assert(src.
type().
id()==ID_pointer);
598 throw "typecast expects one operand";
624 std::cout <<
"GET_REFERENCE_SET_REC EXPR: " <<
from_expr(ns,
"", expr)
628 if(expr.
id()==ID_symbol ||
629 expr.
id()==ID_dynamic_object ||
630 expr.
id()==ID_string_constant)
632 if(expr.
type().
id()==ID_array &&
640 else if(expr.
id()==ID_dereference)
643 throw expr.
id_string()+
" expected to have one operand";
648 for(expr_sett::const_iterator it=value_set.begin();
649 it!=value_set.end(); it++)
650 std::cout <<
"VALUE_SET: " <<
from_expr(ns,
"", *it) <<
'\n';
655 else if(expr.
id()==ID_index)
658 throw "index expected to have two operands";
664 assert(array_type.
id()==ID_array ||
665 array_type.
id()==ID_incomplete_array);
677 if(
object.
id()==ID_unknown)
683 index_expr.op0()=object;
687 if(ns.
follow(
object.type())!=array_type)
688 index_expr.make_typecast(array.
type());
708 else if(expr.
id()==ID_member)
710 const irep_idt &component_name=expr.
get(ID_component_name);
713 throw "member expected to have one operand";
727 if(
object.
id()==ID_unknown)
729 else if(
object.
id()==ID_dynamic_object &&
730 obj_type.
id()!=ID_struct &&
731 obj_type.
id()!=ID_union)
741 exprt member_expr(ID_member, expr.
type());
743 member_expr.set(ID_component_name, component_name);
747 member_expr.op0().make_typecast(struct_op.
type());
755 else if(expr.
id()==ID_if)
758 throw "if takes three operands";
775 std::cout <<
"ASSIGN LHS: " << lhs <<
'\n';
776 std::cout <<
"ASSIGN LTYPE: " << ns.
follow(lhs.type()) <<
'\n';
777 std::cout <<
"ASSIGN RHS: " <<
from_expr(ns,
"", rhs) <<
'\n';
783 throw "if takes three operands";
792 if(type.
id()==ID_struct ||
799 for(struct_typet::componentst::const_iterator
804 const typet &subtype=c_it->type();
805 const irep_idt &name=c_it->get(ID_name);
808 if(subtype.
id()==ID_code)
811 exprt lhs_member(ID_member, subtype);
812 lhs_member.
set(ID_component_name, name);
817 if(rhs.
id()==ID_unknown ||
818 rhs.
id()==ID_invalid)
820 rhs_member=
exprt(rhs.
id(), subtype);
826 "type mismatch:\nRHS: "+rhs.
type().
pretty()+
"\n"+
829 if(rhs.
id()==ID_struct ||
830 rhs.
id()==ID_constant)
835 else if(rhs.
id()==ID_with)
840 const exprt &member_operand=rhs.
op1();
843 member_operand.get(ID_component_name);
845 if(component_name==name)
848 rhs_member=rhs.
op2();
853 rhs_member=
exprt(ID_member, subtype);
855 rhs_member.
set(ID_component_name, name);
860 rhs_member=
exprt(ID_member, subtype);
862 rhs_member.
set(ID_component_name, name);
865 assign(lhs_member, rhs_member, ns, add_to_sets);
869 else if(type.
id()==ID_array)
874 if(rhs.
id()==ID_unknown ||
875 rhs.
id()==ID_invalid)
883 if(rhs.
id()==ID_array_of)
887 assign(lhs_index, rhs.
op0(), ns, add_to_sets);
889 else if(rhs.
id()==ID_array ||
890 rhs.
id()==ID_constant)
894 assign(lhs_index, *o_it, ns, add_to_sets);
897 else if(rhs.
id()==ID_with)
904 assign(lhs_index, op0_index, ns, add_to_sets);
911 assign(lhs_index, rhs_index, ns,
true);
922 assign_rec(lhs, values_rhs,
"", ns, add_to_sets);
931 if(op.
type().
id()!=ID_pointer)
932 throw "free expected to have pointer-type operand";
947 if(
object.
id()==ID_dynamic_object)
959 for(valuest::iterator v_it=
values.begin();
966 v_it->second.object_map.read();
974 if(
object.
id()==ID_dynamic_object)
980 set(new_object_map, o_it);
992 set(new_object_map, o_it);
998 v_it->second.suffix);
1007 const std::string &suffix,
1012 std::cout <<
"ASSIGN_REC LHS: " << lhs <<
'\n';
1013 std::cout <<
"ASSIGN_REC SUFFIX: " << suffix <<
'\n';
1016 it!=values_rhs.
read().
end(); it++)
1017 std::cout <<
"ASSIGN_REC RHS: " <<
to_expr(it) <<
'\n';
1020 if(lhs.id()==ID_symbol)
1022 const irep_idt &identifier=lhs.get(ID_identifier);
1025 "value_set::dynamic_object") ||
1027 "value_set::return_value") ||
1042 else if(lhs.id()==ID_dynamic_object)
1047 const std::string name=
1048 "value_set::dynamic_object"+
1059 make_union(temp_entry.object_map, values_rhs);
1061 else if(lhs.id()==ID_dereference)
1063 if(lhs.operands().size()!=1)
1064 throw lhs.id_string()+
" expected to have one operand";
1073 if(
object.
id()!=ID_unknown)
1074 assign_rec(
object, values_rhs, suffix, ns, add_to_sets);
1077 else if(lhs.id()==ID_index)
1079 if(lhs.operands().size()!=2)
1080 throw "index expected to have two operands";
1084 assert(type.
id()==ID_array || type.
id()==ID_incomplete_array);
1086 assign_rec(lhs.op0(), values_rhs,
"[]"+suffix, ns, add_to_sets);
1088 else if(lhs.id()==ID_member)
1090 if(lhs.operands().size()!=1)
1091 throw "member expected to have one operand";
1093 if(lhs.op0().is_nil())
1096 const std::string &component_name=lhs.get_string(ID_component_name);
1100 assert(type.
id()==ID_struct ||
1101 type.
id()==ID_union ||
1102 type.
id()==ID_incomplete_struct ||
1103 type.
id()==ID_incomplete_union);
1105 assign_rec(lhs.op0(), values_rhs,
"."+component_name+suffix,
1108 else if(lhs.id()==
"valid_object" ||
1109 lhs.id()==
"dynamic_size" ||
1110 lhs.id()==
"dynamic_type")
1114 else if(lhs.id()==ID_string_constant)
1119 else if(lhs.id()==
"NULL-object")
1123 else if(lhs.id()==ID_typecast)
1130 else if(lhs.id()==
"zero_string" ||
1131 lhs.id()==
"is_zero_string" ||
1132 lhs.id()==
"zero_string_length")
1136 else if(lhs.id()==ID_byte_extract_little_endian ||
1137 lhs.id()==ID_byte_extract_big_endian)
1139 assert(lhs.operands().size()==2);
1140 assign_rec(lhs.op0(), values_rhs, suffix, ns,
true);
1143 throw "assign NYI: `"+lhs.id_string()+
"'";
1168 for(
unsigned i=0; i<arguments.size(); i++)
1170 const std::string identifier=
"value_set::" +
id2string(
function) +
"::" +
1171 "argument$"+std::to_string(i);
1176 assign(dummy_lhs, arguments[i], ns,
true);
1192 for(code_typet::parameterst::const_iterator
1193 it=parameter_types.begin();
1194 it!=parameter_types.end();
1197 const irep_idt &identifier=it->get_identifier();
1205 "argument$"+std::to_string(i), it->type());
1208 assign(actual_lhs, v_expr, ns,
true);
1220 irep_idt rvs = std::string(
"value_set::return_value") +
1234 if(statement==ID_block)
1239 else if(statement==ID_function_call)
1244 else if(statement==ID_assign ||
1248 throw "assignment expected to have two operands";
1252 else if(statement==ID_decl)
1255 throw "decl expected to have one operand";
1259 if(lhs.
id()!=ID_symbol)
1260 throw "decl expected to have symbol on lhs";
1264 else if(statement==ID_specc_notify ||
1265 statement==ID_specc_wait)
1269 else if(statement==ID_expression)
1273 else if(statement==ID_cpp_delete ||
1274 statement==ID_cpp_delete_array)
1278 else if(statement==ID_free)
1283 throw "free expected to have one operand";
1287 else if(statement==
"lock" || statement==
"unlock")
1291 else if(statement==ID_asm)
1295 else if(statement==ID_nondet)
1299 else if(statement==ID_printf)
1303 else if(statement==ID_return)
1308 irep_idt rvs = std::string(
"value_set::return_value") +
1315 else if(statement==ID_input || statement==ID_output)
1323 "value_set_fivrnst: unexpected statement: "+
id2string(statement);
1350 if(old.
offset==
object.offset)
1391 if(old.
offset==
object.offset)
1418 vrange_listt::iterator it=ranges.begin();
1420 while(it->function!=f && it!=ranges.end()) it++;
1423 it!=ranges.end() && it->function==f && it->from <= line;
1428 if( line == it->to+1)
1433 vrange_listt::iterator n_it = it; n_it++;
1434 if(n_it!=ranges.end() &&
1435 it->function == n_it->function &&
1436 it->to+1 == n_it->from)
1438 n_it->from = it->from;
1439 it = ranges.erase(it);
1449 if(it!=ranges.end())
1453 if( line == it->from - 1)
1458 if(it!=ranges.begin())
1460 vrange_listt::iterator p_it = it; p_it--;
1461 if(p_it->function == it->function &&
1462 p_it->to+1 == it->from)
1465 it = ranges.erase(it);
1475 ranges.insert(it, insr);
1483 unsigned line)
const 1486 std::cout <<
"IS_VALID_AT: " << inx <<
", " << f <<
", line " << line <<
1490 validity_rangest::const_iterator vrs = validity_ranges.find(inx);
1491 if(vrs!=validity_ranges.end())
1495 object_map_dt::vrange_listt::const_iterator it = ranges.begin();
1497 while(it->function!=f &&
1502 it!=ranges.end() && it->function==f && it->from<=line;
1504 if(it->contains(f, line))
1515 for(valuest::iterator it=
values.begin();
1539 if(
make_union(state_map, t_it->second.object_map))
The type of an expression.
irep_idt name
The unique identifier.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
const typet & follow(const typet &src) const
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
const std::string & id2string(const irep_idt &d)
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
const std::string integer2string(const mp_integer &n, unsigned base)
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast a generic exprt to a dynamic_object_exprt.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
static object_numberingt object_numbering
void output(const namespacet &ns, std::ostream &out) const
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
bool insert_from(object_mapt &dest, object_map_dt::const_iterator it) const
bool set_valid_at(unsigned inx, unsigned f, unsigned line)
void copy_to_operands(const exprt &expr)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::vector< parametert > parameterst
void apply_code(const exprt &code, const namespacet &ns)
const componentst & components() const
void copy_objects(object_mapt &dest, const object_mapt &src) const
static const object_map_dt blank
void dereference_rec(const exprt &src, exprt &dest) const
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
static const char * alloc_adapter_prefix
void do_free(const exprt &op, const namespacet &ns)
bool make_union(object_mapt &dest, const object_mapt &src) const
bool insert_to(object_mapt &dest, object_map_dt::const_iterator it) const
void get_value_set_rec(const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns) const
const irep_idt & id() const
void output_entry(const entryt &e, const namespacet &ns, std::ostream &out) const
The boolean constant true.
#define forall_valid_objects(it, map)
void do_end_function(const exprt &lhs, const namespacet &ns)
entryt & get_entry(const idt &id, const std::string &suffix)
API to expression classes.
const irep_idt & get(const irep_namet &name) const
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool add_to_sets=false)
split an expression into a base object and a (byte) offset
Value Set (Flow Insensitive, Validity Regions)
#define forall_operands(it, expr)
exprt to_expr(object_map_dt::const_iterator it) const
bitvector_typet index_type()
objmapt::const_iterator const_iterator
validity_rangest validity_ranges
Operator to return the address of an object.
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
#define forall_objects(it, map)
void add_var(const idt &id, const std::string &suffix)
std::vector< exprt > operandst
bool has_prefix(const std::string &s, const std::string &prefix)
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
std::list< validity_ranget > vrange_listt
const irep_idt & display_name() const
typet type
Type of symbol.
void get_reference_set_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
static hash_numbering< irep_idt, irep_id_hash > function_numbering
std::unordered_set< exprt, irep_hash > expr_sett
void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, bool add_to_sets)
Base class for all expressions.
const parameterst & parameters() const
bool offset_is_zero() const
bool is_valid_at(unsigned inx, unsigned f, unsigned line) const
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
const std::string & get_string(const irep_namet &name) const
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
const std::string & id_string() const
bool make_valid_union(object_mapt &dest, const object_mapt &src) const
std::unordered_set< unsigned int > dynamic_object_id_sett
Expression to hold a symbol (variable)
exprt dynamic_object(const exprt &pointer)
void get_value_set(const exprt &expr, std::list< exprt > &expr_set, const namespacet &ns) const
const typet & subtype() const
entryt & get_temporary_entry(const idt &id, const std::string &suffix)
const_iterator find(unsigned k)
unsigned from_target_index
void set(const irep_namet &name, const irep_idt &value)
#define Forall_valid_objects(it, map)
bool simplify(exprt &expr, const namespacet &ns)