46 id==
"value_set::return_value" ||
47 id==
"value_set::memory")
66 std::pair<valuest::iterator, bool>
r=
67 values.insert(std::pair<idt, entryt>(index, e));
69 return r.first->second;
77 object_map_dt::const_iterator entry=dest.
read().find(n);
79 if(entry==dest.
read().end())
82 dest.
write()[n]=object;
85 else if(!entry->second.offset_is_set)
87 else if(
object.offset_is_set &&
88 entry->second.offset==
object.offset)
92 dest.
write()[n].offset_is_set=
false;
99 std::ostream &out)
const 101 for(valuest::const_iterator
108 const entryt &e=v_it->second;
115 else if(e.
identifier==
"value_set::return_value")
117 display_name=
"RETURN_VALUE"+e.
suffix;
125 identifier=symbol.
name;
140 for(object_map_dt::const_iterator
141 o_it=object_map.begin();
142 o_it!=object_map.end();
149 if(o.
id()==ID_invalid || o.
id()==ID_unknown)
155 if(o_it->second.offset_is_set)
170 width+=result.size();
172 object_map_dt::const_iterator next(o_it);
175 if(next!=object_map.end())
191 if(
object.
id()==ID_invalid ||
192 object.
id()==ID_unknown)
199 if(it->second.offset_is_set)
211 valuest::iterator v_it=
values.begin();
213 for(valuest::const_iterator
214 it=new_values.begin();
215 it!=new_values.end();
218 if(v_it==
values.end() || it->first<v_it->first)
225 else if(v_it->first<it->first)
231 assert(v_it->first==it->first);
234 const entryt &new_e=it->second;
250 for(object_map_dt::const_iterator it=src.
read().begin();
251 it!=src.
read().end();
267 if(expr.
id()==ID_pointer_offset)
278 for(object_map_dt::const_iterator
279 it=object_map.begin();
280 it!=object_map.end();
282 if(!it->second.offset_is_set)
292 ptr_offset+=it->second.offset;
294 if(mod && ptr_offset!=previous_offset)
298 previous_offset=ptr_offset;
322 for(object_map_dt::const_iterator
323 it=object_map.
read().begin();
324 it!=object_map.
read().end();
329 for(value_setst::valuest::const_iterator it=dest.begin();
330 it!=dest.end(); it++)
331 std::cout <<
"GET_VALUE_SET: " <<
from_expr(
ns,
"", *it) <<
'\n';
339 bool is_simplified)
const 351 const std::string &suffix,
352 const typet &original_type,
356 std::cout <<
"GET_VALUE_SET_REC EXPR: " <<
from_expr(
ns,
"", expr) <<
"\n";
357 std::cout <<
"GET_VALUE_SET_REC SUFFIX: " << suffix <<
'\n';
362 if(expr.
id()==ID_unknown || expr.
id()==ID_invalid)
366 else if(expr.
id()==ID_index)
372 assert(type.id()==ID_array ||
373 type.id()==ID_incomplete_array);
377 else if(expr.
id()==ID_member)
383 assert(type.id()==ID_struct ||
384 type.id()==ID_union ||
385 type.id()==ID_incomplete_struct ||
386 type.id()==ID_incomplete_union);
388 const std::string &component_name=
392 "."+component_name+suffix, original_type,
ns);
394 else if(expr.
id()==ID_symbol)
399 if(expr_type.
id()==ID_pointer ||
400 expr_type.
id()==ID_signedbv ||
401 expr_type.
id()==ID_unsignedbv ||
402 expr_type.
id()==ID_struct ||
403 expr_type.
id()==ID_union ||
404 expr_type.
id()==ID_array)
407 valuest::const_iterator v_it=
412 (expr_type.
id()==ID_struct ||
413 expr_type.
id()==ID_union))
418 const std::string first_component_name=
419 struct_union_type.
components().front().get_string(ID_name);
422 id2string(identifier)+
"."+first_component_name+suffix);
427 v_it=
values.find(identifier);
437 else if(expr.
id()==ID_if)
440 throw "if takes three operands";
445 else if(expr.
id()==ID_address_of)
448 throw expr.
id_string()+
" expected to have one operand";
452 else if(expr.
id()==ID_dereference)
458 if(object_map.begin()==object_map.end())
462 for(object_map_dt::const_iterator
463 it1=object_map.begin();
464 it1!=object_map.end();
472 else if(expr.
id()==
"reference_to")
481 if(object_map.begin()==object_map.end())
485 for(object_map_dt::const_iterator
486 it=object_map.begin();
487 it!=object_map.end();
498 if(expr.
get(ID_value)==ID_NULL &&
499 expr_type.
id()==ID_pointer)
503 else if(expr_type.
id()==ID_unsignedbv ||
504 expr_type.
id()==ID_signedbv)
512 else if(expr.
id()==ID_typecast)
515 throw "typecast takes one operand";
521 if(op_type.
id()==ID_pointer)
526 else if(op_type.
id()==ID_unsignedbv ||
527 op_type.
id()==ID_signedbv)
540 if(tmp.
read().empty())
545 else if(tmp.
read().size()==1 &&
561 else if(expr.
id()==ID_plus ||
565 throw expr.
id_string()+
" expected to have at least two operands";
574 expr_type.
id()==ID_pointer)
582 ptr_operand=expr.
op1();
587 ptr_operand=expr.
op0();
593 if(pointer_sub_type.
id()==ID_empty)
606 if(expr.
id()==ID_minus)
612 ptr_operand, pointer_expr_set,
"", ptr_operand.
type(),
ns);
620 *it, pointer_expr_set,
"", it->type(),
ns);
624 for(object_map_dt::const_iterator
625 it=pointer_expr_set.
read().begin();
626 it!=pointer_expr_set.
read().end();
632 if(
object.offset_is_zero() && i_is_set)
637 insert(dest, it->first,
object);
640 else if(expr.
id()==ID_mult)
646 throw expr.
id_string()+
" expected to have at least two operands";
654 *it, pointer_expr_set,
"", it->type(),
ns);
657 for(object_map_dt::const_iterator
658 it=pointer_expr_set.
read().begin();
659 it!=pointer_expr_set.
read().end();
667 insert(dest, it->first,
object);
670 else if(expr.
id()==ID_side_effect)
674 if(statement==ID_function_call)
677 throw "unexpected function_call sideeffect";
679 else if(statement==ID_malloc)
683 const typet &dynamic_type=
684 static_cast<const typet &
>(expr.
find(ID_C_cxx_alloc_type));
692 else if(statement==ID_cpp_new ||
693 statement==ID_cpp_new_array)
696 assert(expr_type.
id()==ID_pointer);
707 else if(expr.
id()==ID_struct)
713 else if(expr.
id()==ID_with)
725 if(expr_type.
id()==ID_struct)
733 for(object_map_dt::const_iterator
734 it=object_map0.begin();
735 it!=object_map0.end();
740 if(e.
id()==ID_member &&
741 e.
get(ID_component_name)==component_name)
745 dest.
write().insert(tmp_map2.read().begin(), tmp_map2.read().end());
750 dest.
write().insert(*it);
764 else if(expr.
id()==ID_array)
770 else if(expr.
id()==ID_array_of)
776 else if(expr.
id()==ID_dynamic_object)
781 const std::string prefix=
782 "value_set::dynamic_object"+
786 const std::string full_name=prefix+suffix;
789 valuest::const_iterator v_it=
values.find(full_name);
800 else if(expr.
id()==ID_byte_extract_little_endian ||
801 expr.
id()==ID_byte_extract_big_endian)
804 throw "byte_extract takes two operands";
814 if(!
to_integer(op1, op1_offset) && op0_type.
id()==ID_struct)
818 for(struct_union_typet::componentst::const_iterator
820 !found && c_it!=struct_type.
components().end();
823 const irep_idt &name=c_it->get_name();
827 if(comp_offset>op1_offset)
829 else if(comp_offset!=op1_offset)
839 if(op0_type.
id()==ID_union)
844 for(union_typet::componentst::const_iterator
848 const irep_idt &name=c_it->get_name();
858 else if(expr.
id()==ID_byte_update_little_endian ||
859 expr.
id()==ID_byte_update_big_endian)
862 throw "byte_update takes three operands";
873 std::cout <<
"WARNING: not doing " << expr.
id() <<
'\n';
878 std::cout <<
"GET_VALUE_SET_REC RESULT:\n";
879 for(object_map_dt::const_iterator
880 it=dest.
read().begin();
881 it!=dest.
read().end();
896 if(src.
id()==ID_typecast)
898 assert(src.
type().
id()==ID_pointer);
901 throw "typecast expects one operand";
917 for(object_map_dt::const_iterator
918 it=object_map.
read().begin();
919 it!=object_map.
read().end();
930 std::cout <<
"GET_REFERENCE_SET_REC EXPR: " <<
from_expr(
ns,
"", expr)
934 if(expr.
id()==ID_symbol ||
935 expr.
id()==ID_dynamic_object ||
936 expr.
id()==ID_string_constant ||
939 if(expr.
type().
id()==ID_array &&
947 else if(expr.
id()==ID_dereference)
950 throw expr.
id_string()+
" expected to have one operand";
955 for(expr_sett::const_iterator it=value_set.begin();
956 it!=value_set.end(); it++)
957 std::cout <<
"VALUE_SET: " <<
from_expr(
ns,
"", *it) <<
'\n';
962 else if(expr.
id()==ID_index)
965 throw "index expected to have two operands";
972 assert(array_type.
id()==ID_array ||
973 array_type.
id()==ID_incomplete_array);
980 for(object_map_dt::const_iterator
981 a_it=object_map.begin();
982 a_it!=object_map.end();
987 if(
object.
id()==ID_unknown)
992 index_expr.
array()=object;
996 if(
ns.
follow(
object.type())!=array_type)
1018 insert(dest, index_expr, o);
1024 else if(expr.
id()==ID_member)
1026 const irep_idt &component_name=expr.
get(ID_component_name);
1029 throw "member expected to have one operand";
1038 for(object_map_dt::const_iterator
1039 it=object_map.begin();
1040 it!=object_map.end();
1045 if(
object.
id()==ID_unknown)
1052 member_expr.
op0()=object;
1053 member_expr.set_component_name(component_name);
1060 if(final_object_type.
id()==ID_struct ||
1061 final_object_type.
id()==ID_union)
1065 member_expr.op0().make_typecast(struct_op.
type());
1067 insert(dest, member_expr, o);
1076 else if(expr.
id()==ID_if)
1079 throw "if takes three operands";
1097 std::cout <<
"ASSIGN LHS: " <<
from_expr(
ns,
"", lhs) <<
'\n';
1098 std::cout <<
"ASSIGN RHS: " <<
from_expr(
ns,
"", rhs) <<
'\n';
1104 if(type.
id()==ID_struct ||
1105 type.
id()==ID_union)
1110 for(struct_union_typet::componentst::const_iterator
1115 const typet &subtype=c_it->type();
1116 const irep_idt &name=c_it->get(ID_name);
1119 if(subtype.
id()==ID_code ||
1120 c_it->get_is_padding())
continue;
1124 lhs_member.
op0()=lhs;
1128 if(rhs.
id()==ID_unknown ||
1129 rhs.
id()==ID_invalid)
1131 rhs_member=
exprt(rhs.
id(), subtype);
1136 throw "value_sett::assign type mismatch: " 1142 assign(lhs_member, rhs_member,
ns, is_simplified, add_to_sets);
1146 else if(type.
id()==ID_array)
1151 if(rhs.
id()==ID_unknown ||
1152 rhs.
id()==ID_invalid)
1164 throw "value_sett::assign type mismatch: " 1168 if(rhs.
id()==ID_array_of)
1171 assign(lhs_index, rhs.
op0(),
ns, is_simplified, add_to_sets);
1173 else if(rhs.
id()==ID_array ||
1174 rhs.
id()==ID_constant)
1178 assign(lhs_index, *o_it,
ns, is_simplified, add_to_sets);
1182 else if(rhs.
id()==ID_with)
1189 assign(lhs_index, op0_index,
ns, is_simplified, add_to_sets);
1190 assign(lhs_index, rhs.
op2(),
ns, is_simplified,
true);
1196 assign(lhs_index, rhs_index,
ns, is_simplified,
true);
1215 if(op.
type().
id()!=ID_pointer)
1216 throw "free expected to have pointer-type operand";
1227 for(object_map_dt::const_iterator
1228 it=object_map.begin();
1229 it!=object_map.end();
1234 if(
object.
id()==ID_dynamic_object)
1246 for(valuest::iterator v_it=
values.begin();
1253 v_it->second.object_map.read();
1257 for(object_map_dt::const_iterator
1258 o_it=old_object_map.begin();
1259 o_it!=old_object_map.end();
1264 if(
object.
id()==ID_dynamic_object)
1270 set(new_object_map, o_it);
1277 insert(new_object_map, tmp, o);
1282 set(new_object_map, o_it);
1286 v_it->second.object_map=new_object_map;
1293 const std::string &suffix,
1298 std::cout <<
"ASSIGN_REC LHS: " <<
from_expr(
ns,
"", lhs) <<
'\n';
1299 std::cout <<
"ASSIGN_REC LHS ID: " << lhs.
id() <<
'\n';
1300 std::cout <<
"ASSIGN_REC SUFFIX: " << suffix <<
'\n';
1302 for(object_map_dt::const_iterator it=values_rhs.
read().begin();
1303 it!=values_rhs.
read().end();
1305 std::cout <<
"ASSIGN_REC RHS: " <<
1310 if(lhs.
id()==ID_symbol)
1321 else if(lhs.
id()==ID_dynamic_object)
1326 const std::string name=
1327 "value_set::dynamic_object"+
1334 else if(lhs.
id()==ID_dereference)
1337 throw lhs.
id_string()+
" expected to have one operand";
1342 if(reference_set.
read().size()!=1)
1345 for(object_map_dt::const_iterator
1346 it=reference_set.
read().begin();
1347 it!=reference_set.
read().end();
1352 if(
object.
id()!=ID_unknown)
1353 assign_rec(
object, values_rhs, suffix,
ns, add_to_sets);
1356 else if(lhs.
id()==ID_index)
1359 throw "index expected to have two operands";
1363 assert(type.
id()==ID_array || type.
id()==ID_incomplete_array);
1367 else if(lhs.
id()==ID_member)
1370 throw "member expected to have one operand";
1372 const std::string &component_name=lhs.
get_string(ID_component_name);
1376 assert(type.
id()==ID_struct ||
1377 type.
id()==ID_union ||
1378 type.
id()==ID_incomplete_struct ||
1379 type.
id()==ID_incomplete_union);
1382 lhs.
op0(), values_rhs,
"."+component_name+suffix,
ns, add_to_sets);
1384 else if(lhs.
id()==
"valid_object" ||
1385 lhs.
id()==
"dynamic_size" ||
1386 lhs.
id()==
"dynamic_type" ||
1387 lhs.
id()==
"is_zero_string" ||
1388 lhs.
id()==
"zero_string" ||
1389 lhs.
id()==
"zero_string_length")
1393 else if(lhs.
id()==ID_string_constant)
1398 else if(lhs.
id()==
"NULL-object")
1402 else if(lhs.
id()==ID_typecast)
1406 assign_rec(typecast_expr.
op(), values_rhs, suffix,
ns, add_to_sets);
1408 else if(lhs.
id()==ID_byte_extract_little_endian ||
1409 lhs.
id()==ID_byte_extract_big_endian)
1414 else if(lhs.
id()==ID_integer_address)
1420 throw "assign NYI: `"+lhs.
id_string()+
"'";
1438 for(
unsigned i=0; i<arguments.size(); i++)
1440 const std::string identifier=
"value_set::dummy_arg_"+std::to_string(i);
1442 assign(dummy_lhs, arguments[i],
ns,
false,
false);
1449 for(code_typet::parameterst::const_iterator
1450 it=parameter_types.begin();
1451 it!=parameter_types.end();
1454 const irep_idt &identifier=it->get_identifier();
1459 symbol_exprt(
"value_set::dummy_arg_"+std::to_string(i), it->type());
1462 assign(actual_lhs, v_expr,
ns,
true,
true);
1478 assign(lhs, rhs,
ns,
false,
false);
1487 if(statement==ID_block)
1492 else if(statement==ID_function_call)
1497 else if(statement==ID_assign ||
1501 throw "assignment expected to have two operands";
1505 else if(statement==ID_decl)
1508 throw "decl expected to have one operand";
1512 if(lhs.
id()!=ID_symbol)
1513 throw "decl expected to have symbol on lhs";
1517 if(lhs_type.
id()==ID_pointer ||
1518 (lhs_type.
id()==ID_array &&
1527 address_of_expr.
object()=failed;
1529 assign(lhs, address_of_expr,
ns,
false,
false);
1535 else if(statement==
"specc_notify" ||
1536 statement==
"specc_wait")
1540 else if(statement==ID_expression)
1544 else if(statement==
"cpp_delete" ||
1545 statement==
"cpp_delete[]")
1549 else if(statement==ID_free)
1554 throw "free expected to have one operand";
1558 else if(statement==
"lock" || statement==
"unlock")
1562 else if(statement==ID_asm)
1566 else if(statement==ID_nondet)
1570 else if(statement==ID_printf)
1574 else if(statement==ID_return)
1583 else if(statement==ID_array_set)
1586 else if(statement==ID_array_copy)
1589 else if(statement==ID_array_replace)
1592 else if(statement==ID_assume)
1596 else if(statement==ID_user_specified_predicate ||
1597 statement==ID_user_specified_parameter_predicates ||
1598 statement==ID_user_specified_return_predicates)
1602 else if(statement==ID_fence)
1605 else if(statement==ID_input || statement==ID_output)
1612 throw "value_sett: unexpected statement: "+
id2string(statement);
1620 if(expr.
id()==ID_and)
1625 else if(expr.
id()==ID_equal)
1628 else if(expr.
id()==ID_notequal)
1631 else if(expr.
id()==ID_not)
1634 else if(expr.
id()==ID_dynamic_object)
1658 if(src.
id()==ID_struct ||
1659 src.
id()==ID_constant)
1665 else if(src.
id()==ID_with)
1670 const exprt &member_operand=src.
op1();
1672 if(component_name==member_operand.get(ID_component_name))
1679 else if(src.
id()==ID_typecast)
1689 member_expr.
op0()=src;
const irep_idt & get_statement() const
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
bool insert(object_mapt &dest, object_map_dt::const_iterator it) const
const std::string & id2string(const irep_idt &d)
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
const code_assumet & to_code_assume(const codet &code)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
void copy_to_operands(const exprt &expr)
const irep_idt & get_identifier() const
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool is_simplified, bool add_to_sets)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
bool make_union(object_mapt &dest, const object_mapt &src) const
std::vector< parametert > parameterst
void get_reference_set_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
bool offset_is_zero() const
void get_value_set(const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
const componentst & components() const
static const object_map_dt blank
static object_numberingt object_numbering
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
void dereference_rec(const exprt &src, exprt &dest) const
void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, bool add_to_sets)
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
exprt to_expr(object_map_dt::const_iterator it) const
Extract member of struct or union.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
void set_component_name(const irep_idt &component_name)
static bool field_sensitive(const irep_idt &id, const typet &type, const namespacet &)
const irep_idt & id() const
The boolean constant true.
bool eval_pointer_offset(exprt &expr, const namespacet &ns) const
exprt get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
API to expression classes.
const irep_idt & get(const irep_namet &name) const
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
split an expression into a base object and a (byte) offset
void get_value_set_rec(const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns) const
#define forall_operands(it, expr)
bitvector_typet index_type()
typet component_type(const irep_idt &component_name) const
Operator to return the address of an object.
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
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.
const irep_idt & display_name() const
mp_integer compute_pointer_offset(const exprt &expr, const namespacet &ns)
std::unordered_map< idt, entryt, string_hash > valuest
entryt & get_entry(const entryt &e, const typet &type, const namespacet &)
typet type
Type of symbol.
void do_end_function(const exprt &lhs, const namespacet &ns)
Base type of C structs and unions, and C++ classes.
void get_reference_set(const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
Base class for all expressions.
const parameterst & parameters() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
std::size_t component_number(const irep_idt &component_name) const
std::set< unsigned int > dynamic_object_id_sett
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
#define Forall_operands(it, expr)
const codet & to_code(const exprt &expr)
Expression to hold a symbol (variable)
void output(const namespacet &ns, std::ostream &out) const
exprt dynamic_object(const exprt &pointer)
A statement in a programming language.
unsignedbv_typet unsigned_char_type()
const typet & subtype() const
void guard(const exprt &expr, const namespacet &ns)
void do_free(const exprt &op, const namespacet &ns)
std::list< exprt > valuest
void make_typecast(const typet &_type)
const irept & find(const irep_namet &name) const
bitvector_typet char_type()
void apply_code(const codet &code, const namespacet &ns)
bool simplify(exprt &expr, const namespacet &ns)
exprt make_member(const exprt &src, const irep_idt &component_name, const namespacet &ns)