45 id==
"value_set::return_value" ||
46 id==
"value_set::memory")
50 return type.
id() == ID_struct || type.
id() == ID_struct_tag;
56 return !found.has_value() ? nullptr : &(found->get());
73 if(existing_entry.has_value())
103 auto entry=dest.
read().find(n);
105 if(entry==dest.
read().end())
110 else if(!entry->second)
112 else if(offset && *entry->second == *offset)
127 auto &new_offset = dest.
write()[n];
139 const std::string &indent)
const
151 display_name = id2string(e.identifier) + e.suffix;
154 else if(e.
identifier ==
"value_set::return_value")
156 display_name =
"RETURN_VALUE" + e.suffix;
162 const symbolt &symbol=ns.lookup(e.identifier);
163 display_name=id2string(symbol.display_name())+e.suffix;
164 identifier=symbol.name;
166 identifier = id2string(e.identifier);
167 display_name = id2string(identifier) + e.suffix;
171 out << indent << display_name <<
" = { ";
175 std::size_t width = 0;
177 for(object_map_dt::const_iterator o_it = object_map.begin();
178 o_it != object_map.end();
181 const exprt &o = object_numbering[o_it->first];
183 std::ostringstream stream;
185 if(o.id() == ID_invalid || o.id() == ID_unknown)
189 stream <<
"<" << format(o) <<
", ";
192 stream << *o_it->second;
196 if(o.type().is_nil())
199 stream <<
", " << format(o.type());
204 const std::string result = stream.str();
206 width += result.size();
208 object_map_dt::const_iterator next(o_it);
211 if(next != object_map.end())
215 out <<
"\n" << std::string(indent.size(),
' ') <<
" ";
227 if(
object.
id()==ID_invalid ||
228 object.
id()==ID_unknown)
240 return std::move(od);
251 for(
const auto &delta_entry : delta_view)
253 if(delta_entry.is_in_both_maps())
256 delta_entry.get_other_map_value().object_map,
257 delta_entry.m.object_map))
260 make_union(existing_entry.object_map, delta_entry.m.object_map);
279 for(
const auto &number_and_offset : src.
read())
283 dest, number_and_offset.first, number_and_offset.second) !=
297 for(object_map_dt::const_iterator it=src.
read().begin();
298 it!=src.
read().end();
314 if(expr.
id()==ID_pointer_offset)
323 for(object_map_dt::const_iterator
324 it=object_map.begin();
325 it!=object_map.end();
334 if(!ptr_offset.has_value())
337 *ptr_offset += *it->second;
339 if(mod && *ptr_offset != previous_offset)
343 previous_offset = *ptr_offset;
366 for(object_map_dt::const_iterator
367 it=object_map.
read().begin();
368 it!=object_map.
read().end();
373 for(value_setst::valuest::const_iterator it=dest.begin();
374 it!=dest.end(); it++)
375 std::cout <<
"GET_VALUE_SET: " <<
format(*it) <<
'\n';
384 .map([&](
const object_map_dt::value_type &pair) {
return to_expr(pair); });
391 bool is_simplified)
const
402 bool is_simplified)
const
416 const std::string &suffix,
const std::string &field)
421 suffix.compare(1, field.length(), field) == 0 &&
422 (suffix.length() == field.length() + 1 ||
423 suffix[field.length() + 1] ==
'.' ||
424 suffix[field.length() + 1] ==
'[');
428 const std::string &suffix,
const std::string &field)
432 "suffix should start with " + field);
433 return suffix.substr(field.length() + 1);
439 const std::string &suffix,
443 type.
id() != ID_pointer && type.
id() != ID_signedbv &&
444 type.
id() != ID_unsignedbv && type.
id() != ID_array &&
445 type.
id() != ID_struct && type.
id() != ID_struct_tag &&
446 type.
id() != ID_union && type.
id() != ID_union_tag)
455 return std::move(index);
457 const typet &followed_type = type.
id() == ID_struct_tag
459 : type.
id() == ID_union_tag
464 if(followed_type.
id() == ID_struct || followed_type.
id() == ID_union)
469 const irep_idt &first_component_name =
470 struct_union_type.
components().front().get_name();
476 return std::move(index);
482 return std::move(identifier);
490 const std::string &suffix,
491 const typet &original_type,
495 std::cout <<
"GET_VALUE_SET_REC EXPR: " <<
format(expr) <<
"\n";
496 std::cout <<
"GET_VALUE_SET_REC SUFFIX: " << suffix <<
'\n';
501 if(expr.
id()==ID_unknown || expr.
id()==ID_invalid)
505 else if(expr.
id()==ID_index)
510 type.
id() == ID_array,
"operand 0 of index expression must be an array");
513 to_index_expr(expr).array(), dest,
"[]" + suffix, original_type, ns);
515 else if(expr.
id()==ID_member)
520 type.
id() == ID_struct || type.
id() == ID_union,
521 "compound of member expression must be struct or union");
523 const std::string &component_name=
529 "." + component_name + suffix,
533 else if(expr.
id()==ID_symbol)
538 if(entry_index.has_value())
543 else if(expr.
id()==ID_if)
546 to_if_expr(expr).true_case(), dest, suffix, original_type, ns);
548 to_if_expr(expr).false_case(), dest, suffix, original_type, ns);
550 else if(expr.
id()==ID_address_of)
554 else if(expr.
id()==ID_dereference)
560 if(object_map.begin()==object_map.end())
564 for(object_map_dt::const_iterator
565 it1=object_map.begin();
566 it1!=object_map.end();
579 if(expr.
get(ID_value)==ID_NULL &&
580 expr_type.
id()==ID_pointer)
584 else if(expr_type.
id()==ID_unsignedbv ||
585 expr_type.
id()==ID_signedbv)
593 else if(expr.
id()==ID_typecast)
598 const typet &op_type = op.type();
600 if(op_type.
id()==ID_pointer)
605 else if(op_type.
id()==ID_unsignedbv ||
606 op_type.
id()==ID_signedbv)
619 if(tmp.
read().empty())
624 else if(tmp.
read().size()==1 &&
641 expr.
id() == ID_plus || expr.
id() == ID_minus || expr.
id() == ID_bitor ||
642 expr.
id() == ID_bitand || expr.
id() == ID_bitxor ||
643 expr.
id() == ID_bitnand || expr.
id() == ID_bitnor ||
644 expr.
id() == ID_bitxnor)
647 throw expr.
id_string()+
" expected to have at least two operands";
655 expr.
operands().size() == 2 && expr_type.
id() == ID_pointer &&
656 (expr.
id() == ID_plus || expr.
id() == ID_minus))
676 if(pointer_sub_type.
id()==ID_empty)
681 if(!size.has_value() || (*size) == 0)
689 if(expr.
id()==ID_minus)
695 ptr_operand, pointer_expr_set,
"", ptr_operand.
type(), ns);
703 *it, pointer_expr_set,
"", it->type(), ns);
707 for(object_map_dt::const_iterator
708 it=pointer_expr_set.
read().begin();
709 it!=pointer_expr_set.
read().end();
715 if(offset && i.has_value())
720 insert(dest, it->first, offset);
723 else if(expr.
id()==ID_mult)
729 throw expr.
id_string()+
" expected to have at least two operands";
737 *it, pointer_expr_set,
"", it->type(), ns);
740 for(object_map_dt::const_iterator
741 it=pointer_expr_set.
read().begin();
742 it!=pointer_expr_set.
read().end();
750 insert(dest, it->first, offset);
753 else if(expr.
id()==ID_side_effect)
757 if(statement==ID_function_call)
760 throw "unexpected function_call sideeffect";
762 else if(statement==ID_allocate)
766 const typet &dynamic_type=
767 static_cast<const typet &
>(expr.
find(ID_C_cxx_alloc_type));
775 else if(statement==ID_cpp_new ||
776 statement==ID_cpp_new_array)
779 assert(expr_type.
id()==ID_pointer);
790 else if(expr.
id()==ID_struct)
794 struct_components.size() == expr.
operands().size(),
795 "struct expression should have an operand per component");
796 auto component_iter = struct_components.begin();
797 bool found_component =
false;
803 const std::string &component_name =
807 std::string remaining_suffix =
810 found_component =
true;
824 else if(expr.
id()==ID_with)
830 if(expr_type.
id() == ID_struct && !suffix.
empty())
836 std::string remaining_suffix =
839 with_expr.
new_value(), dest, remaining_suffix, original_type, ns);
855 else if(expr_type.
id() == ID_array && !suffix.
empty())
857 std::string new_value_suffix;
859 new_value_suffix = suffix.substr(2);
866 with_expr.
new_value(), dest, new_value_suffix, original_type, ns);
876 else if(expr.
id()==ID_array)
879 std::string new_suffix = suffix;
881 new_suffix = suffix.substr(2);
888 else if(expr.
id()==ID_array_of)
891 std::string new_suffix = suffix;
893 new_suffix = suffix.substr(2);
900 else if(expr.
id()==ID_dynamic_object)
905 const std::string prefix=
906 "value_set::dynamic_object"+
910 const std::string full_name=prefix+suffix;
924 else if(expr.
id()==ID_byte_extract_little_endian ||
925 expr.
id()==ID_byte_extract_big_endian)
931 exprt op1 = byte_extract_expr.
op1();
935 const auto op1_offset = numeric_cast<mp_integer>(op1);
936 const typet &op_type = ns.
follow(byte_extract_expr.op().type());
937 if(op1_offset.has_value() && op_type.
id() == ID_struct)
943 const irep_idt &name = c.get_name();
947 if(!comp_offset.has_value())
949 else if(*comp_offset > *op1_offset)
951 else if(*comp_offset != *op1_offset)
962 if(op_type.
id() == ID_union)
967 const irep_idt &name = c.get_name();
968 member_exprt member(byte_extract_expr.op(), name, c.type());
976 byte_extract_expr.op(), dest, suffix, original_type, ns);
978 else if(expr.
id()==ID_byte_update_little_endian ||
979 expr.
id()==ID_byte_update_big_endian)
986 byte_update_expr.value(), dest, suffix, original_type, ns);
990 else if(expr.
id() == ID_let)
995 value_sett value_set_with_local_definition = *
this;
996 value_set_with_local_definition.
assign(
997 let_expr.symbol(), let_expr.value(), ns,
false,
false);
1000 let_expr.where(), dest, suffix, original_type, ns);
1009 std::cout <<
"GET_VALUE_SET_REC RESULT:\n";
1010 for(
const auto &obj : dest.
read())
1013 std::cout <<
" " <<
format(e) <<
"\n";
1024 if(src.
id()==ID_typecast)
1026 assert(src.
type().
id()==ID_pointer);
1042 for(object_map_dt::const_iterator
1043 it=object_map.
read().begin();
1044 it!=object_map.
read().end();
1055 std::cout <<
"GET_REFERENCE_SET_REC EXPR: " <<
format(expr)
1059 if(expr.
id()==ID_symbol ||
1060 expr.
id()==ID_dynamic_object ||
1061 expr.
id()==ID_string_constant ||
1062 expr.
id()==ID_array)
1064 if(expr.
type().
id()==ID_array &&
1072 else if(expr.
id()==ID_dereference)
1079 for(expr_sett::const_iterator it=value_set.begin();
1080 it!=value_set.end(); it++)
1081 std::cout <<
"VALUE_SET: " <<
format(*it) <<
'\n';
1086 else if(expr.
id()==ID_index)
1089 throw "index expected to have two operands";
1097 array_type.
id() == ID_array,
"index takes array-typed operand");
1104 for(object_map_dt::const_iterator
1105 a_it=object_map.begin();
1106 a_it!=object_map.end();
1111 if(
object.
id()==ID_unknown)
1120 const auto i = numeric_cast<mp_integer>(offset);
1125 else if(i.has_value() && o)
1129 if(!size.has_value() || *size == 0)
1137 insert(dest, deref_index_expr, o);
1143 else if(expr.
id()==ID_member)
1145 const irep_idt &component_name=expr.
get(ID_component_name);
1154 for(object_map_dt::const_iterator
1155 it=object_map.begin();
1156 it!=object_map.end();
1161 if(
object.
id()==ID_unknown)
1172 const typet &final_object_type = ns.
follow(
object.type());
1174 if(final_object_type.
id()==ID_struct ||
1175 final_object_type.
id()==ID_union)
1178 if(ns.
follow(struct_op.
type())!=final_object_type)
1184 insert(dest, member_expr, o);
1193 else if(expr.
id()==ID_if)
1211 std::cout <<
"ASSIGN LHS: " <<
format(lhs) <<
" : "
1213 std::cout <<
"ASSIGN RHS: " <<
format(rhs) <<
" : "
1215 std::cout <<
"--------------------------------------------\n";
1221 if(type.
id()==ID_struct ||
1222 type.
id()==ID_union)
1226 const typet &subtype = c.type();
1227 const irep_idt &name = c.get_name();
1230 if(subtype.
id() == ID_code || c.get_is_padding())
1237 if(rhs.
id()==ID_unknown ||
1238 rhs.
id()==ID_invalid)
1243 rhs_member=
exprt(rhs.
id(), subtype);
1249 "value_sett::assign types should match, got: "
1259 assign(lhs_member, rhs_member, ns,
true, add_to_sets);
1263 else if(type.
id()==ID_array)
1268 if(rhs.
id()==ID_unknown ||
1269 rhs.
id()==ID_invalid)
1282 "value_sett::assign types should match, got: "
1286 if(rhs.
id()==ID_array_of)
1295 else if(rhs.
id()==ID_array ||
1296 rhs.
id()==ID_constant)
1300 assign(lhs_index, *o_it, ns, is_simplified, add_to_sets);
1304 else if(rhs.
id()==ID_with)
1311 assign(lhs_index, op0_index, ns, is_simplified, add_to_sets);
1313 lhs_index,
to_with_expr(rhs).new_value(), ns, is_simplified,
true);
1319 assign(lhs_index, rhs_index, ns, is_simplified,
true);
1334 assign_rec(lhs, values_rhs,
"", ns, add_to_sets);
1341 const std::string &suffix,
1346 std::cout <<
"ASSIGN_REC LHS: " <<
format(lhs) <<
'\n';
1347 std::cout <<
"ASSIGN_REC LHS ID: " << lhs.
id() <<
'\n';
1348 std::cout <<
"ASSIGN_REC SUFFIX: " << suffix <<
'\n';
1350 for(object_map_dt::const_iterator it=values_rhs.
read().begin();
1351 it!=values_rhs.
read().end();
1353 std::cout <<
"ASSIGN_REC RHS: " <<
1358 if(lhs.
id()==ID_symbol)
1363 entryt{identifier, suffix}, lhs.
type(), values_rhs, add_to_sets);
1365 else if(lhs.
id()==ID_dynamic_object)
1370 const std::string name=
1371 "value_set::dynamic_object"+
1376 else if(lhs.
id()==ID_dereference)
1379 throw lhs.
id_string()+
" expected to have one operand";
1384 if(reference_set.
read().size()!=1)
1387 for(object_map_dt::const_iterator
1388 it=reference_set.
read().begin();
1389 it!=reference_set.
read().end();
1396 if(
object.
id()!=ID_unknown)
1397 assign_rec(
object, values_rhs, suffix, ns, add_to_sets);
1400 else if(lhs.
id()==ID_index)
1404 const typet &type = array.type();
1407 type.
id() == ID_array,
"operand 0 of index expression must be an array");
1409 assign_rec(array, values_rhs,
"[]" + suffix, ns,
true);
1411 else if(lhs.
id()==ID_member)
1414 const auto &component_name = lhs_member_expr.get_component_name();
1416 const typet &type = ns.
follow(lhs_member_expr.compound().type());
1419 type.
id() == ID_struct || type.
id() == ID_union,
1420 "operand 0 of member expression must be struct or union");
1423 lhs_member_expr.compound(),
1425 "." +
id2string(component_name) + suffix,
1429 else if(lhs.
id()==
"valid_object" ||
1430 lhs.
id()==
"dynamic_size" ||
1431 lhs.
id()==
"dynamic_type" ||
1432 lhs.
id()==
"is_zero_string" ||
1433 lhs.
id()==
"zero_string" ||
1434 lhs.
id()==
"zero_string_length")
1438 else if(lhs.
id()==ID_string_constant)
1443 else if(lhs.
id() == ID_null_object)
1447 else if(lhs.
id()==ID_typecast)
1451 assign_rec(typecast_expr.
op(), values_rhs, suffix, ns, add_to_sets);
1453 else if(lhs.
id()==ID_byte_extract_little_endian ||
1454 lhs.
id()==ID_byte_extract_big_endian)
1458 else if(lhs.
id()==ID_integer_address)
1464 throw "assign NYI: '" + lhs.
id_string() +
"'";
1482 for(std::size_t i=0; i<arguments.size(); i++)
1484 const std::string identifier=
"value_set::dummy_arg_"+
std::to_string(i);
1485 const symbol_exprt dummy_lhs(identifier, arguments[i].type());
1486 assign(dummy_lhs, arguments[i], ns,
false,
false);
1493 for(code_typet::parameterst::const_iterator
1494 it=parameter_types.begin();
1495 it!=parameter_types.end();
1498 const irep_idt &identifier=it->get_identifier();
1499 if(identifier.
empty())
1506 assign(actual_lhs, v_expr, ns,
true,
true);
1522 assign(lhs, rhs, ns,
false,
false);
1531 if(statement==ID_block)
1536 else if(statement==ID_function_call)
1541 else if(statement==ID_assign)
1544 throw "assignment expected to have two operands";
1548 else if(statement==ID_decl)
1551 throw "decl expected to have one operand";
1555 if(lhs.
id()!=ID_symbol)
1556 throw "decl expected to have symbol on lhs";
1561 lhs_type.
id() == ID_pointer ||
1562 (lhs_type.
id() == ID_array && lhs_type.
subtype().
id() == ID_pointer))
1568 assign(lhs, address_of_expr, ns,
false,
false);
1574 else if(statement==ID_expression)
1578 else if(statement==
"cpp_delete" ||
1579 statement==
"cpp_delete[]")
1583 else if(statement==
"lock" || statement==
"unlock")
1587 else if(statement==ID_asm)
1591 else if(statement==ID_nondet)
1595 else if(statement==ID_printf)
1599 else if(statement==ID_return)
1610 else if(statement==ID_array_set)
1613 else if(statement==ID_array_copy)
1616 else if(statement==ID_array_replace)
1619 else if(statement==ID_assume)
1623 else if(statement==ID_user_specified_predicate ||
1624 statement==ID_user_specified_parameter_predicates ||
1625 statement==ID_user_specified_return_predicates)
1629 else if(statement==ID_fence)
1636 else if(statement==ID_dead)
1643 throw "value_sett: unexpected statement: "+
id2string(statement);
1651 if(expr.
id()==ID_and)
1656 else if(expr.
id()==ID_equal)
1659 else if(expr.
id()==ID_notequal)
1662 else if(expr.
id()==ID_not)
1665 else if(expr.
id()==ID_dynamic_object)
1681 const std::unordered_set<exprt, irep_hash> &values_to_erase)
1683 if(values_to_erase.empty())
1690 std::vector<object_map_dt::key_type> keys_to_erase;
1692 for(
auto &key_value : entry->object_map.read())
1694 const auto &rhs_object =
to_expr(key_value);
1695 if(values_to_erase.count(rhs_object))
1697 keys_to_erase.emplace_back(key_value.first);
1702 keys_to_erase.size() == values_to_erase.size(),
1703 "value_sett::erase_value_from_entry() should erase exactly one value for "
1704 "each element in the set it is given");
1706 entryt replacement = *entry;
1707 for(
const auto &key_to_erase : keys_to_erase)
1716 const std::string &erase_prefix,
1719 for(
const auto &c : struct_union_type.
components())
1721 const typet &subtype = c.type();
1722 const irep_idt &name = c.get_name();
1725 if(subtype.
id() == ID_code || c.get_is_padding())
1734 const std::string &erase_prefix,
1737 if(type.
id() == ID_struct_tag)
1740 else if(type.
id() == ID_union_tag)
1743 else if(type.
id() == ID_array)