46 id==
"value_set::return_value" ||
47 id==
"value_set::memory")
51 return type.
id() == ID_struct || type.
id() == ID_struct_tag;
57 return !found.has_value() ? nullptr : &(found->get());
74 if(existing_entry.has_value())
104 auto entry=dest.
read().find(n);
106 if(entry==dest.
read().end())
111 else if(!entry->second)
113 else if(offset && *entry->second == *offset)
128 auto &new_offset = dest.
write()[n];
144 display_name = id2string(e.identifier) + e.suffix;
147 else if(e.
identifier ==
"value_set::return_value")
149 display_name =
"RETURN_VALUE" + e.suffix;
155 const symbolt &symbol=ns.lookup(e.identifier);
156 display_name=id2string(symbol.display_name())+e.suffix;
157 identifier=symbol.name;
159 identifier = id2string(e.identifier);
160 display_name = id2string(identifier) + e.suffix;
164 out << indent << display_name <<
" = { ";
168 std::size_t width = 0;
170 for(object_map_dt::const_iterator o_it = object_map.begin();
171 o_it != object_map.end();
174 const exprt &o = object_numbering[o_it->first];
176 std::ostringstream stream;
178 if(o.id() == ID_invalid || o.id() == ID_unknown)
182 stream <<
"<" << format(o) <<
", ";
185 stream << *o_it->second;
189 if(o.type().is_nil())
192 stream <<
", " << format(o.type());
197 const std::string result = stream.str();
199 width += result.size();
201 object_map_dt::const_iterator next(o_it);
204 if(next != object_map.end())
208 out <<
"\n" << std::string(indent.size(),
' ') <<
" ";
220 if(
object.
id()==ID_invalid ||
221 object.
id()==ID_unknown)
233 return std::move(od);
244 for(
const auto &delta_entry : delta_view)
246 if(delta_entry.is_in_both_maps())
249 delta_entry.get_other_map_value().object_map,
250 delta_entry.m.object_map))
253 make_union(existing_entry.object_map, delta_entry.m.object_map);
272 for(
const auto &number_and_offset : src.
read())
276 dest, number_and_offset.first, number_and_offset.second) !=
290 for(object_map_dt::const_iterator it=src.
read().begin();
291 it!=src.
read().end();
307 if(expr.
id()==ID_pointer_offset)
316 for(object_map_dt::const_iterator
317 it=object_map.begin();
318 it!=object_map.end();
327 if(!ptr_offset.has_value())
330 *ptr_offset += *it->second;
332 if(mod && *ptr_offset != previous_offset)
336 previous_offset = *ptr_offset;
357 .map([&](
const object_map_dt::value_type &pair) {
return to_expr(pair); });
363 bool is_simplified)
const
377 const std::string &suffix,
const std::string &field)
382 suffix.compare(1, field.length(), field) == 0 &&
383 (suffix.length() == field.length() + 1 ||
384 suffix[field.length() + 1] ==
'.' ||
385 suffix[field.length() + 1] ==
'[');
389 const std::string &suffix,
const std::string &field)
393 "suffix should start with " + field);
394 return suffix.substr(field.length() + 1);
400 const std::string &suffix,
404 type.
id() != ID_pointer && type.
id() != ID_signedbv &&
405 type.
id() != ID_unsignedbv && type.
id() != ID_array &&
406 type.
id() != ID_struct && type.
id() != ID_struct_tag &&
407 type.
id() != ID_union && type.
id() != ID_union_tag)
416 return std::move(index);
418 const typet &followed_type = type.
id() == ID_struct_tag
420 : type.
id() == ID_union_tag
425 if(followed_type.
id() == ID_struct || followed_type.
id() == ID_union)
432 const irep_idt &first_component_name =
433 struct_union_type.
components().front().get_name();
439 return std::move(index);
446 return std::move(identifier);
454 const std::string &suffix,
455 const typet &original_type,
459 std::cout <<
"GET_VALUE_SET_REC EXPR: " <<
format(expr) <<
"\n";
460 std::cout <<
"GET_VALUE_SET_REC SUFFIX: " << suffix <<
'\n';
465 if(expr.
id()==ID_unknown || expr.
id()==ID_invalid)
469 else if(expr.
id()==ID_index)
474 type.
id() == ID_array,
"operand 0 of index expression must be an array");
477 to_index_expr(expr).array(), dest,
"[]" + suffix, original_type, ns);
479 else if(expr.
id()==ID_member)
484 type.
id() == ID_struct || type.
id() == ID_union,
485 "compound of member expression must be struct or union");
487 const std::string &component_name=
493 "." + component_name + suffix,
497 else if(expr.
id()==ID_symbol)
502 if(entry_index.has_value())
507 else if(expr.
id()==ID_if)
510 to_if_expr(expr).true_case(), dest, suffix, original_type, ns);
512 to_if_expr(expr).false_case(), dest, suffix, original_type, ns);
514 else if(expr.
id()==ID_address_of)
518 else if(expr.
id()==ID_dereference)
524 if(object_map.begin()==object_map.end())
528 for(object_map_dt::const_iterator
529 it1=object_map.begin();
530 it1!=object_map.end();
543 if(expr.
get(ID_value)==ID_NULL &&
544 expr_type.
id()==ID_pointer)
548 else if(expr_type.
id()==ID_unsignedbv ||
549 expr_type.
id()==ID_signedbv)
557 else if(expr.
id()==ID_typecast)
562 const typet &op_type = op.type();
564 if(op_type.
id()==ID_pointer)
569 else if(op_type.
id()==ID_unsignedbv ||
570 op_type.
id()==ID_signedbv)
583 if(tmp.
read().empty())
588 else if(tmp.
read().size()==1 &&
605 expr.
id() == ID_plus || expr.
id() == ID_minus || expr.
id() == ID_bitor ||
606 expr.
id() == ID_bitand || expr.
id() == ID_bitxor ||
607 expr.
id() == ID_bitnand || expr.
id() == ID_bitnor ||
608 expr.
id() == ID_bitxnor)
611 throw expr.
id_string()+
" expected to have at least two operands";
619 expr.
operands().size() == 2 && expr_type.
id() == ID_pointer &&
620 (expr.
id() == ID_plus || expr.
id() == ID_minus))
640 if(pointer_sub_type.
id()==ID_empty)
645 if(!size.has_value() || (*size) == 0)
653 if(expr.
id()==ID_minus)
659 ptr_operand, pointer_expr_set,
"", ptr_operand.
type(), ns);
667 *it, pointer_expr_set,
"", it->type(), ns);
671 for(object_map_dt::const_iterator
672 it=pointer_expr_set.
read().begin();
673 it!=pointer_expr_set.
read().end();
679 if(offset && i.has_value())
684 insert(dest, it->first, offset);
687 else if(expr.
id()==ID_mult)
693 throw expr.
id_string()+
" expected to have at least two operands";
701 *it, pointer_expr_set,
"", it->type(), ns);
704 for(object_map_dt::const_iterator
705 it=pointer_expr_set.
read().begin();
706 it!=pointer_expr_set.
read().end();
714 insert(dest, it->first, offset);
717 else if(expr.
id()==ID_side_effect)
721 if(statement==ID_function_call)
724 throw "unexpected function_call sideeffect";
726 else if(statement==ID_allocate)
730 const typet &dynamic_type=
731 static_cast<const typet &
>(expr.
find(ID_C_cxx_alloc_type));
739 else if(statement==ID_cpp_new ||
740 statement==ID_cpp_new_array)
743 assert(expr_type.
id()==ID_pointer);
754 else if(expr.
id()==ID_struct)
758 struct_components.size() == expr.
operands().size(),
759 "struct expression should have an operand per component");
760 auto component_iter = struct_components.begin();
761 bool found_component =
false;
767 const std::string &component_name =
771 std::string remaining_suffix =
774 found_component =
true;
788 else if(expr.
id() == ID_union)
793 else if(expr.
id()==ID_with)
799 if(expr_type.
id() == ID_struct && !suffix.
empty())
805 std::string remaining_suffix =
808 with_expr.
new_value(), dest, remaining_suffix, original_type, ns);
824 else if(expr_type.
id() == ID_array && !suffix.
empty())
826 std::string new_value_suffix;
828 new_value_suffix = suffix.substr(2);
835 with_expr.
new_value(), dest, new_value_suffix, original_type, ns);
845 else if(expr.
id()==ID_array)
848 std::string new_suffix = suffix;
850 new_suffix = suffix.substr(2);
857 else if(expr.
id()==ID_array_of)
860 std::string new_suffix = suffix;
862 new_suffix = suffix.substr(2);
869 else if(expr.
id()==ID_dynamic_object)
874 const std::string prefix=
875 "value_set::dynamic_object"+
879 const std::string full_name=prefix+suffix;
893 else if(expr.
id()==ID_byte_extract_little_endian ||
894 expr.
id()==ID_byte_extract_big_endian)
900 const typet &op_type = ns.
follow(byte_extract_expr.op().type());
901 if(op_type.
id() == ID_struct)
903 exprt offset = byte_extract_expr.offset();
907 const auto offset_int = numeric_cast<mp_integer>(offset);
914 const irep_idt &name = c.get_name();
916 if(offset_int.has_value())
919 if(comp_offset.has_value())
922 type_size.has_value() && *offset_int + *type_size <= *comp_offset)
929 member_size.has_value() &&
930 *offset_int >= *comp_offset + *member_size)
944 if(op_type.
id() == ID_union)
949 const irep_idt &name = c.get_name();
950 member_exprt member(byte_extract_expr.op(), name, c.type());
958 byte_extract_expr.op(), dest, suffix, original_type, ns);
960 else if(expr.
id()==ID_byte_update_little_endian ||
961 expr.
id()==ID_byte_update_big_endian)
968 byte_update_expr.value(), dest, suffix, original_type, ns);
972 else if(expr.
id() == ID_let)
977 value_sett value_set_with_local_definition = *
this;
978 value_set_with_local_definition.
assign(
979 let_expr.symbol(), let_expr.value(), ns,
false,
false);
982 let_expr.where(), dest, suffix, original_type, ns);
991 std::cout <<
"GET_VALUE_SET_REC RESULT:\n";
992 for(
const auto &obj : dest.
read())
995 std::cout <<
" " <<
format(e) <<
"\n";
1006 if(src.
id()==ID_typecast)
1008 assert(src.
type().
id()==ID_pointer);
1024 for(object_map_dt::const_iterator
1025 it=object_map.
read().begin();
1026 it!=object_map.
read().end();
1037 std::cout <<
"GET_REFERENCE_SET_REC EXPR: " <<
format(expr)
1041 if(expr.
id()==ID_symbol ||
1042 expr.
id()==ID_dynamic_object ||
1043 expr.
id()==ID_string_constant ||
1044 expr.
id()==ID_array)
1046 if(expr.
type().
id()==ID_array &&
1054 else if(expr.
id()==ID_dereference)
1061 for(
const auto &map_entry : dest.
read())
1070 else if(expr.
id()==ID_index)
1073 throw "index expected to have two operands";
1081 array_type.
id() == ID_array,
"index takes array-typed operand");
1088 for(object_map_dt::const_iterator
1089 a_it=object_map.begin();
1090 a_it!=object_map.end();
1095 if(
object.
id()==ID_unknown)
1104 const auto i = numeric_cast<mp_integer>(offset);
1109 else if(i.has_value() && o)
1113 if(!size.has_value() || *size == 0)
1121 insert(dest, deref_index_expr, o);
1127 else if(expr.
id()==ID_member)
1129 const irep_idt &component_name=expr.
get(ID_component_name);
1138 for(object_map_dt::const_iterator
1139 it=object_map.begin();
1140 it!=object_map.end();
1145 if(
object.
id()==ID_unknown)
1156 const typet &final_object_type = ns.
follow(
object.type());
1158 if(final_object_type.
id()==ID_struct ||
1159 final_object_type.
id()==ID_union)
1162 if(ns.
follow(struct_op.
type())!=final_object_type)
1168 insert(dest, member_expr, o);
1177 else if(expr.
id()==ID_if)
1195 std::cout <<
"ASSIGN LHS: " <<
format(lhs) <<
" : "
1197 std::cout <<
"ASSIGN RHS: " <<
format(rhs) <<
" : "
1199 std::cout <<
"--------------------------------------------\n";
1205 if(type.
id() == ID_struct)
1209 const typet &subtype = c.type();
1210 const irep_idt &name = c.get_name();
1213 if(subtype.
id() == ID_code || c.get_is_padding())
1220 if(rhs.
id()==ID_unknown ||
1221 rhs.
id()==ID_invalid)
1226 rhs_member=
exprt(rhs.
id(), subtype);
1232 "value_sett::assign types should match, got: "
1242 assign(lhs_member, rhs_member, ns,
true, add_to_sets);
1246 else if(type.
id()==ID_array)
1251 if(rhs.
id()==ID_unknown ||
1252 rhs.
id()==ID_invalid)
1265 "value_sett::assign types should match, got: "
1269 if(rhs.
id()==ID_array_of)
1278 else if(rhs.
id()==ID_array ||
1279 rhs.
id()==ID_constant)
1283 assign(lhs_index, *o_it, ns, is_simplified, add_to_sets);
1287 else if(rhs.
id()==ID_with)
1294 assign(lhs_index, op0_index, ns, is_simplified, add_to_sets);
1296 lhs_index,
to_with_expr(rhs).new_value(), ns, is_simplified,
true);
1302 assign(lhs_index, rhs_index, ns, is_simplified,
true);
1317 assign_rec(lhs, values_rhs,
"", ns, add_to_sets);
1324 const std::string &suffix,
1329 std::cout <<
"ASSIGN_REC LHS: " <<
format(lhs) <<
'\n';
1330 std::cout <<
"ASSIGN_REC LHS ID: " << lhs.
id() <<
'\n';
1331 std::cout <<
"ASSIGN_REC SUFFIX: " << suffix <<
'\n';
1333 for(object_map_dt::const_iterator it=values_rhs.
read().begin();
1334 it!=values_rhs.
read().end();
1336 std::cout <<
"ASSIGN_REC RHS: " <<
1341 if(lhs.
id()==ID_symbol)
1346 entryt{identifier, suffix}, lhs.
type(), values_rhs, add_to_sets);
1348 else if(lhs.
id()==ID_dynamic_object)
1353 const std::string name=
1354 "value_set::dynamic_object"+
1359 else if(lhs.
id()==ID_dereference)
1362 throw lhs.
id_string()+
" expected to have one operand";
1367 if(reference_set.
read().size()!=1)
1370 for(object_map_dt::const_iterator
1371 it=reference_set.
read().begin();
1372 it!=reference_set.
read().end();
1379 if(
object.
id()!=ID_unknown)
1380 assign_rec(
object, values_rhs, suffix, ns, add_to_sets);
1383 else if(lhs.
id()==ID_index)
1387 const typet &type = array.type();
1390 type.
id() == ID_array,
"operand 0 of index expression must be an array");
1392 assign_rec(array, values_rhs,
"[]" + suffix, ns,
true);
1394 else if(lhs.
id()==ID_member)
1397 const auto &component_name = lhs_member_expr.get_component_name();
1399 const typet &type = ns.
follow(lhs_member_expr.compound().type());
1402 type.
id() == ID_struct || type.
id() == ID_union,
1403 "operand 0 of member expression must be struct or union");
1406 lhs_member_expr.compound(),
1408 "." +
id2string(component_name) + suffix,
1412 else if(lhs.
id()==
"valid_object" ||
1413 lhs.
id()==
"dynamic_type" ||
1414 lhs.
id()==
"is_zero_string" ||
1415 lhs.
id()==
"zero_string" ||
1416 lhs.
id()==
"zero_string_length")
1420 else if(lhs.
id()==ID_string_constant)
1425 else if(lhs.
id() == ID_null_object)
1429 else if(lhs.
id()==ID_typecast)
1433 assign_rec(typecast_expr.
op(), values_rhs, suffix, ns, add_to_sets);
1435 else if(lhs.
id()==ID_byte_extract_little_endian ||
1436 lhs.
id()==ID_byte_extract_big_endian)
1440 else if(lhs.
id()==ID_integer_address)
1446 throw "assign NYI: '" + lhs.
id_string() +
"'";
1464 for(std::size_t i=0; i<arguments.size(); i++)
1466 const std::string identifier=
"value_set::dummy_arg_"+
std::to_string(i);
1467 const symbol_exprt dummy_lhs(identifier, arguments[i].type());
1468 assign(dummy_lhs, arguments[i], ns,
false,
false);
1475 for(code_typet::parameterst::const_iterator
1476 it=parameter_types.begin();
1477 it!=parameter_types.end();
1480 const irep_idt &identifier=it->get_identifier();
1481 if(identifier.
empty())
1488 assign(actual_lhs, v_expr, ns,
true,
true);
1504 assign(lhs, rhs, ns,
false,
false);
1513 if(statement==ID_block)
1518 else if(statement==ID_function_call)
1523 else if(statement==ID_assign)
1526 throw "assignment expected to have two operands";
1530 else if(statement==ID_decl)
1533 throw "decl expected to have one operand";
1537 if(lhs.
id()!=ID_symbol)
1538 throw "decl expected to have symbol on lhs";
1543 lhs_type.
id() == ID_pointer ||
1544 (lhs_type.
id() == ID_array && lhs_type.
subtype().
id() == ID_pointer))
1550 assign(lhs, address_of_expr, ns,
false,
false);
1556 else if(statement==ID_expression)
1560 else if(statement==
"cpp_delete" ||
1561 statement==
"cpp_delete[]")
1565 else if(statement==
"lock" || statement==
"unlock")
1569 else if(statement==ID_asm)
1573 else if(statement==ID_nondet)
1577 else if(statement==ID_printf)
1581 else if(statement==ID_return)
1592 else if(statement==ID_array_set)
1595 else if(statement==ID_array_copy)
1598 else if(statement==ID_array_replace)
1601 else if(statement==ID_assume)
1605 else if(statement==ID_user_specified_predicate ||
1606 statement==ID_user_specified_parameter_predicates ||
1607 statement==ID_user_specified_return_predicates)
1611 else if(statement==ID_fence)
1618 else if(statement==ID_dead)
1625 throw "value_sett: unexpected statement: "+
id2string(statement);
1633 if(expr.
id()==ID_and)
1638 else if(expr.
id()==ID_equal)
1641 else if(expr.
id()==ID_notequal)
1644 else if(expr.
id()==ID_not)
1647 else if(expr.
id()==ID_dynamic_object)
1663 const std::unordered_set<exprt, irep_hash> &values_to_erase)
1665 if(values_to_erase.empty())
1672 std::vector<object_map_dt::key_type> keys_to_erase;
1674 for(
auto &key_value : entry->object_map.read())
1676 const auto &rhs_object =
to_expr(key_value);
1677 if(values_to_erase.count(rhs_object))
1679 keys_to_erase.emplace_back(key_value.first);
1684 keys_to_erase.size() == values_to_erase.size(),
1685 "value_sett::erase_value_from_entry() should erase exactly one value for "
1686 "each element in the set it is given");
1688 entryt replacement = *entry;
1689 for(
const auto &key_to_erase : keys_to_erase)
1698 const std::string &erase_prefix,
1701 for(
const auto &c : struct_union_type.
components())
1703 const typet &subtype = c.type();
1704 const irep_idt &name = c.get_name();
1707 if(subtype.
id() == ID_code || c.get_is_padding())
1716 const std::string &erase_prefix,
1719 if(type.
id() == ID_struct_tag)
1722 else if(type.
id() == ID_union_tag)
1725 else if(type.
id() == ID_array)