47 id.starts_with(
"value_set::dynamic_object") ||
48 id ==
"value_set::return_value" ||
id ==
"value_set::memory")
52 return type.
id() == ID_struct || type.
id() == ID_struct_tag;
57 auto found =
values.find(
id);
58 return !found.has_value() ? nullptr : &(found->get());
74 auto existing_entry =
values.find(index);
75 if(existing_entry.has_value())
81 values.update(index, [&new_values,
this](
entryt &entry) {
96 values.insert(index, std::move(new_entry));
105 auto entry=dest.
read().find(n);
107 if(entry==dest.
read().end())
112 else if(!entry->second)
114 else if(offset && *entry->second == *offset)
129 auto &new_offset = dest.
write()[n];
148 else if(e.
identifier ==
"value_set::return_value")
150 display_name =
"RETURN_VALUE" + e.
suffix;
158 identifier=symbol.
name;
165 out << indent << display_name <<
" = { ";
169 std::size_t width = 0;
171 for(object_map_dt::const_iterator o_it = object_map.begin();
172 o_it != object_map.end();
177 std::ostringstream stream;
179 if(o.
id() == ID_invalid || o.
id() == ID_unknown)
183 stream <<
"<" <<
format(o) <<
", ";
186 stream <<
format(*o_it->second);
198 const std::string result = stream.str();
200 width += result.size();
202 object_map_dt::const_iterator next(o_it);
205 if(next != object_map.end())
209 out <<
"\n" << std::string(indent.size(),
' ') <<
" ";
222 this->
values.get_view(view);
224 for(
const auto &values_entry : view)
230 const value_sett::expr_sett &expr_set=
231 value_entries.expr_set();
233 for(value_sett::expr_sett::const_iterator
234 e_it=expr_set.begin();
235 e_it!=expr_set.end();
238 std::string value_str=
254 if(
object.
id()==ID_invalid ||
255 object.
id()==ID_unknown)
267 return std::move(od);
278 for(
const auto &delta_entry : delta_view)
280 if(delta_entry.is_in_both_maps())
283 delta_entry.get_other_map_value().object_map,
284 delta_entry.m.object_map))
286 values.update(delta_entry.k, [&](
entryt &existing_entry) {
287 make_union(existing_entry.object_map, delta_entry.m.object_map);
294 values.insert(delta_entry.k, delta_entry.m);
306 for(
const auto &number_and_offset : src.
read())
310 dest, number_and_offset.first, number_and_offset.second) !=
324 for(object_map_dt::const_iterator it=src.
read().begin();
325 it!=src.
read().end();
341 if(expr.
id()==ID_pointer_offset)
350 for(object_map_dt::const_iterator
351 it=object_map.begin();
352 it!=object_map.end();
355 if(!it->second || !it->second->is_constant())
362 if(!ptr_offset.has_value())
368 if(mod && *ptr_offset != previous_offset)
372 previous_offset = *ptr_offset;
394 .map([&](
const object_map_dt::value_type &pair) {
return to_expr(pair); });
400 bool is_simplified)
const
406 bool includes_nondet_pointer =
false;
409 if(includes_nondet_pointer && expr.
type().
id() == ID_pointer)
431 const std::string &suffix,
const std::string &field)
436 suffix.compare(1, field.length(), field) == 0 &&
437 (suffix.length() == field.length() + 1 ||
438 suffix[field.length() + 1] ==
'.' ||
439 suffix[field.length() + 1] ==
'[');
443 const std::string &suffix,
const std::string &field)
447 "suffix should start with " + field);
448 return suffix.substr(field.length() + 1);
454 const std::string &suffix,
458 type.
id() != ID_pointer && type.
id() != ID_signedbv &&
459 type.
id() != ID_unsignedbv && type.
id() != ID_array &&
460 type.
id() != ID_struct && type.
id() != ID_struct_tag &&
461 type.
id() != ID_union && type.
id() != ID_union_tag)
470 return std::move(index);
472 const typet &followed_type = type.
id() == ID_struct_tag
474 : type.
id() == ID_union_tag
479 if(followed_type.
id() == ID_struct || followed_type.
id() == ID_union)
486 const irep_idt &first_component_name =
487 struct_union_type.
components().front().get_name();
493 return std::move(index);
500 return std::move(identifier);
508 bool &includes_nondet_pointer,
509 const std::string &suffix,
510 const typet &original_type,
514 std::cout <<
"GET_VALUE_SET_REC EXPR: " <<
format(expr) <<
"\n";
515 std::cout <<
"GET_VALUE_SET_REC SUFFIX: " << suffix <<
'\n';
518 if(expr.
id()==ID_unknown || expr.
id()==ID_invalid)
522 else if(expr.
id()==ID_index)
527 type.
id() == ID_array,
"operand 0 of index expression must be an array");
532 includes_nondet_pointer,
537 else if(expr.
id()==ID_member)
542 compound.
type().
id() == ID_struct ||
543 compound.
type().
id() == ID_struct_tag ||
544 compound.
type().
id() == ID_union ||
545 compound.
type().
id() == ID_union_tag,
546 "compound of member expression must be struct or union");
548 const std::string &component_name=
554 includes_nondet_pointer,
555 "." + component_name + suffix,
559 else if(expr.
id()==ID_symbol)
567 if(entry_index.has_value())
572 else if(expr.
id() == ID_nondet_symbol)
574 if(expr.
type().
id() == ID_pointer)
575 includes_nondet_pointer =
true;
579 else if(expr.
id()==ID_if)
584 includes_nondet_pointer,
591 includes_nondet_pointer,
596 else if(expr.
id()==ID_address_of)
600 else if(expr.
id()==ID_dereference)
606 if(object_map.begin()==object_map.end())
610 for(object_map_dt::const_iterator
611 it1=object_map.begin();
612 it1!=object_map.end();
619 object, dest, includes_nondet_pointer, suffix, original_type, ns);
634 expr.
type().
id() == ID_unsignedbv || expr.
type().
id() == ID_signedbv)
642 else if(expr.
id()==ID_typecast)
647 const typet &op_type = op.type();
649 if(op_type.
id()==ID_pointer)
653 op, dest, includes_nondet_pointer, suffix, original_type, ns);
656 op_type.
id() == ID_unsignedbv || op_type.
id() == ID_signedbv ||
657 op_type.
id() == ID_bv)
674 op, tmp, includes_nondet_pointer, suffix, original_type, ns);
676 if(tmp.
read().empty())
681 else if(tmp.
read().size()==1 &&
698 expr.
id() == ID_plus || expr.
id() == ID_minus || expr.
id() == ID_bitor ||
699 expr.
id() == ID_bitand || expr.
id() == ID_bitxor ||
700 expr.
id() == ID_bitnand || expr.
id() == ID_bitnor ||
701 expr.
id() == ID_bitxnor)
705 expr.
id_string() +
" expected to have at least two operands");
708 std::optional<exprt> additional_offset;
711 std::optional<exprt> ptr_operand;
713 expr.
type().
id() == ID_pointer &&
714 (expr.
id() == ID_plus || expr.
id() == ID_minus))
716 for(
const auto &op : expr.
operands())
718 if(op.type().id() == ID_pointer)
720 if(ptr_operand.has_value())
730 if(!additional_offset.has_value())
731 additional_offset = op;
741 if(ptr_operand.has_value() && additional_offset.has_value())
743 typet pointer_base_type =
745 if(pointer_base_type.
id() == ID_empty)
750 if(!size.has_value() || (*size) == 0)
752 additional_offset.reset();
757 *additional_offset,
from_integer(*size, additional_offset->type())};
759 if(expr.
id()==ID_minus)
763 "unexpected subtraction of pointer from integer");
765 additional_offset->type().id() != ID_unsignedbv,
766 "offset type must support negation");
773 if(ptr_operand.has_value())
778 includes_nondet_pointer,
786 for(
const auto &op : expr.
operands())
789 op, pointer_expr_set, includes_nondet_pointer,
"", op.type(), ns);
793 for(object_map_dt::const_iterator
794 it=pointer_expr_set.
read().begin();
795 it!=pointer_expr_set.
read().end();
801 if(offset && additional_offset.has_value())
807 *additional_offset, offset->type())},
813 insert(dest, it->first, offset);
816 else if(expr.
id()==ID_mult)
823 expr.
id_string() +
" expected to have at least two operands");
828 for(
const auto &op : expr.
operands())
831 op, pointer_expr_set, includes_nondet_pointer,
"", op.type(), ns);
834 for(object_map_dt::const_iterator
835 it=pointer_expr_set.
read().begin();
836 it!=pointer_expr_set.
read().end();
844 insert(dest, it->first, offset);
847 else if(expr.
id() == ID_lshr || expr.
id() == ID_ashr || expr.
id() == ID_shl)
855 includes_nondet_pointer,
860 for(
const auto &object_map_entry : pointer_expr_set.
read())
862 offsett offset = object_map_entry.second;
867 insert(dest, object_map_entry.first, offset);
870 else if(expr.
id()==ID_side_effect)
874 if(statement==ID_function_call)
879 else if(statement==ID_allocate)
883 const typet &dynamic_type=
884 static_cast<const typet &
>(expr.
find(ID_C_cxx_alloc_type));
892 else if(statement==ID_cpp_new ||
893 statement==ID_cpp_new_array)
910 else if(expr.
id()==ID_struct)
912 const auto &struct_components =
913 expr.
type().
id() == ID_struct_tag
917 struct_components.size() == expr.
operands().size(),
918 "struct expression should have an operand per component");
919 auto component_iter = struct_components.begin();
920 bool found_component =
false;
924 for(
const auto &op : expr.
operands())
926 const std::string &component_name =
930 std::string remaining_suffix =
935 includes_nondet_pointer,
939 found_component =
true;
949 for(
const auto &op : expr.
operands())
952 op, dest, includes_nondet_pointer, suffix, original_type, ns);
956 else if(expr.
id() == ID_union)
961 includes_nondet_pointer,
966 else if(expr.
id()==ID_with)
973 (expr.
type().
id() == ID_struct_tag || expr.
type().
id() == ID_struct) &&
980 std::string remaining_suffix =
985 includes_nondet_pointer,
991 (expr.
type().
id() == ID_struct &&
993 (expr.
type().
id() == ID_struct_tag &&
1001 includes_nondet_pointer,
1014 includes_nondet_pointer,
1021 includes_nondet_pointer,
1027 else if(expr.
type().
id() == ID_array && !suffix.empty())
1029 std::string new_value_suffix;
1031 new_value_suffix = suffix.substr(2);
1039 includes_nondet_pointer,
1046 includes_nondet_pointer,
1058 includes_nondet_pointer,
1065 includes_nondet_pointer,
1071 else if(expr.
id()==ID_array)
1074 std::string new_suffix = suffix;
1076 new_suffix = suffix.substr(2);
1080 for(
const auto &op : expr.
operands())
1083 op, dest, includes_nondet_pointer, new_suffix, original_type, ns);
1086 else if(expr.
id()==ID_array_of)
1089 std::string new_suffix = suffix;
1091 new_suffix = suffix.substr(2);
1098 includes_nondet_pointer,
1103 else if(expr.
id()==ID_dynamic_object)
1108 const std::string prefix=
1109 "value_set::dynamic_object"+
1113 const std::string full_name=prefix+suffix;
1127 else if(expr.
id()==ID_byte_extract_little_endian ||
1128 expr.
id()==ID_byte_extract_big_endian)
1135 byte_extract_expr.op().type().id() == ID_struct ||
1136 byte_extract_expr.op().type().id() == ID_struct_tag)
1138 exprt offset = byte_extract_expr.offset();
1146 byte_extract_expr.op().type().
id() == ID_struct_tag
1150 for(
const auto &c : struct_type.
components())
1152 const irep_idt &name = c.get_name();
1154 if(offset_int.has_value())
1157 if(comp_offset.has_value())
1160 type_size.has_value() && *offset_int + *type_size <= *comp_offset)
1167 member_size.has_value() &&
1168 *offset_int >= *comp_offset + *member_size)
1179 member, dest, includes_nondet_pointer, suffix, original_type, ns);
1184 byte_extract_expr.op().type().id() == ID_union ||
1185 byte_extract_expr.op().type().id() == ID_union_tag)
1188 const auto &components =
1189 byte_extract_expr.op().type().id() == ID_union_tag
1193 for(
const auto &c : components)
1195 const irep_idt &name = c.get_name();
1196 member_exprt member(byte_extract_expr.op(), name, c.type());
1198 member, dest, includes_nondet_pointer, suffix, original_type, ns);
1205 byte_extract_expr.op(),
1207 includes_nondet_pointer,
1212 else if(expr.
id()==ID_byte_update_little_endian ||
1213 expr.
id()==ID_byte_update_big_endian)
1219 byte_update_expr.op(),
1221 includes_nondet_pointer,
1226 byte_update_expr.value(),
1228 includes_nondet_pointer,
1235 else if(expr.
id() == ID_let)
1240 value_sett value_set_with_local_definition = *
this;
1241 value_set_with_local_definition.
assign(
1242 let_expr.symbol(), let_expr.value(), ns,
false,
false);
1247 includes_nondet_pointer,
1258 includes_nondet_pointer,
1263 for(
const auto &object_map_entry : pointer_expr_set.
read())
1265 offsett offset = object_map_entry.second;
1270 insert(dest, object_map_entry.first, offset);
1276 for(
const auto &op : expr.
operands())
1279 op, pointer_expr_set, includes_nondet_pointer,
"", original_type, ns);
1282 for(
const auto &object_map_entry : pointer_expr_set.
read())
1284 offsett offset = object_map_entry.second;
1289 insert(dest, object_map_entry.first, offset);
1292 if(pointer_expr_set.
read().empty())
1297 std::cout <<
"GET_VALUE_SET_REC RESULT:\n";
1298 for(
const auto &obj : dest.
read())
1301 std::cout <<
" " <<
format(e) <<
"\n";
1312 if(src.
id()==ID_typecast)
1330 for(object_map_dt::const_iterator
1331 it=object_map.
read().begin();
1332 it!=object_map.
read().end();
1343 std::cout <<
"GET_REFERENCE_SET_REC EXPR: " <<
format(expr)
1347 if(expr.
id()==ID_symbol ||
1348 expr.
id()==ID_dynamic_object ||
1349 expr.
id()==ID_string_constant ||
1350 expr.
id()==ID_array)
1356 expr.
type().
id() == ID_array &&
1366 else if(expr.
id()==ID_dereference)
1370 bool includes_nondet_pointer =
false;
1372 pointer, dest, includes_nondet_pointer,
"", pointer.type(), ns);
1375 for(
const auto &map_entry : dest.
read())
1384 else if(expr.
id()==ID_index)
1391 array.
type().
id() == ID_array,
"index takes array-typed operand");
1400 for(object_map_dt::const_iterator
1401 a_it=object_map.begin();
1402 a_it!=object_map.end();
1407 if(
object.
id()==ID_unknown)
1417 if(!index.
is_zero() && o.has_value())
1421 if(!size.has_value() || *size == 0)
1435 insert(dest, deref_index_expr, o);
1441 else if(expr.
id()==ID_member)
1443 const irep_idt &component_name=expr.
get(ID_component_name);
1452 for(object_map_dt::const_iterator
1453 it=object_map.begin();
1454 it!=object_map.end();
1459 if(
object.
id()==ID_unknown)
1462 object.type().
id() == ID_struct ||
1463 object.type().
id() == ID_struct_tag ||
object.type().
id() == ID_union ||
1464 object.type().
id() == ID_union_tag)
1474 object.type().
id() == ID_struct ||
1475 object.type().
id() == ID_struct_tag ||
1476 object.type().
id() == ID_union ||
object.type().
id() == ID_union_tag)
1479 if(struct_op.
type() !=
object.type())
1485 insert(dest, member_expr, o);
1496 else if(expr.
id()==ID_if)
1514 std::cout <<
"ASSIGN LHS: " <<
format(lhs) <<
" : "
1516 std::cout <<
"ASSIGN RHS: " <<
format(rhs) <<
" : "
1518 std::cout <<
"--------------------------------------------\n";
1522 if(lhs.
type().
id() == ID_struct || lhs.
type().
id() == ID_struct_tag)
1524 const auto &components =
1525 lhs.
type().
id() == ID_struct_tag
1529 for(
const auto &c : components)
1531 const typet &subtype = c.type();
1532 const irep_idt &name = c.get_name();
1536 subtype.
id() != ID_code,
"struct member must not be of code type");
1537 if(c.get_is_padding())
1544 if(rhs.
id()==ID_unknown ||
1545 rhs.
id()==ID_invalid)
1550 rhs_member=
exprt(rhs.
id(), subtype);
1556 "value_sett::assign types should match, got: "
1560 if(rhs.
type().
id() == ID_struct_tag || rhs.
type().
id() == ID_union_tag)
1568 assign(lhs_member, rhs_member, ns,
true, add_to_sets);
1570 else if(rhs.
type().
id() == ID_struct || rhs.
type().
id() == ID_union)
1578 assign(lhs_member, rhs_member, ns,
true, add_to_sets);
1583 else if(lhs.
type().
id() == ID_array)
1590 if(rhs.
id()==ID_unknown ||
1591 rhs.
id()==ID_invalid)
1604 "value_sett::assign types should match, got: "
1608 if(rhs.
id()==ID_array_of)
1619 for(
const auto &op : rhs.
operands())
1621 assign(lhs_index, op, ns, is_simplified, add_to_sets);
1625 else if(rhs.
id()==ID_with)
1632 assign(lhs_index, op0_index, ns, is_simplified, add_to_sets);
1634 lhs_index,
to_with_expr(rhs).new_value(), ns, is_simplified,
true);
1642 assign(lhs_index, rhs_index, ns, is_simplified,
true);
1657 assign_rec(lhs, values_rhs,
"", ns, add_to_sets);
1664 const std::string &suffix,
1669 std::cout <<
"ASSIGN_REC LHS: " <<
format(lhs) <<
'\n';
1670 std::cout <<
"ASSIGN_REC LHS ID: " << lhs.
id() <<
'\n';
1671 std::cout <<
"ASSIGN_REC SUFFIX: " << suffix <<
'\n';
1673 for(object_map_dt::const_iterator it=values_rhs.
read().begin();
1674 it!=values_rhs.
read().end();
1676 std::cout <<
"ASSIGN_REC RHS: " <<
1681 if(lhs.
id()==ID_symbol)
1688 entryt{identifier, suffix}, lhs.
type(), values_rhs, add_to_sets);
1690 else if(lhs.
id()==ID_dynamic_object)
1695 const std::string name=
1696 "value_set::dynamic_object"+
1701 else if(lhs.
id()==ID_dereference)
1705 lhs.
id_string() +
" expected to have one operand");
1710 if(reference_set.
read().size()!=1)
1713 for(object_map_dt::const_iterator
1714 it=reference_set.
read().begin();
1715 it!=reference_set.
read().end();
1722 if(
object.
id()!=ID_unknown)
1723 assign_rec(
object, values_rhs, suffix, ns, add_to_sets);
1726 else if(lhs.
id()==ID_index)
1730 const typet &type = array.type();
1733 type.
id() == ID_array,
"operand 0 of index expression must be an array");
1735 assign_rec(array, values_rhs,
"[]" + suffix, ns,
true);
1737 else if(lhs.
id()==ID_member)
1740 const auto &component_name = lhs_member_expr.get_component_name();
1741 const exprt &compound = lhs_member_expr.compound();
1744 compound.
type().
id() == ID_struct ||
1745 compound.
type().
id() == ID_struct_tag ||
1746 compound.
type().
id() == ID_union ||
1747 compound.
type().
id() == ID_union_tag,
1748 "operand 0 of member expression must be struct or union");
1753 "." +
id2string(component_name) + suffix,
1757 else if(lhs.
id()==
"valid_object" ||
1758 lhs.
id()==
"dynamic_type" ||
1759 lhs.
id()==
"is_zero_string" ||
1760 lhs.
id()==
"zero_string" ||
1761 lhs.
id()==
"zero_string_length")
1765 else if(lhs.
id()==ID_string_constant)
1770 else if(lhs.
id() == ID_null_object)
1774 else if(lhs.
id()==ID_typecast)
1778 assign_rec(typecast_expr.
op(), values_rhs, suffix, ns, add_to_sets);
1780 else if(lhs.
id()==ID_byte_extract_little_endian ||
1781 lhs.
id()==ID_byte_extract_big_endian)
1785 else if(lhs.
id()==ID_integer_address)
1809 for(std::size_t i=0; i<arguments.size(); i++)
1811 const std::string identifier=
"value_set::dummy_arg_"+std::to_string(i);
1812 const symbol_exprt dummy_lhs(identifier, arguments[i].type());
1813 assign(dummy_lhs, arguments[i], ns,
false,
false);
1820 for(code_typet::parameterst::const_iterator
1821 it=parameter_types.begin();
1822 it!=parameter_types.end();
1825 const irep_idt &identifier=it->get_identifier();
1826 if(identifier.
empty())
1830 symbol_exprt(
"value_set::dummy_arg_"+std::to_string(i), it->type());
1833 assign(actual_lhs, v_expr, ns,
true,
true);
1849 assign(lhs, rhs, ns,
false,
false);
1858 if(statement==ID_block)
1860 for(
const auto &op : code.
operands())
1863 else if(statement==ID_function_call)
1868 else if(statement==ID_assign)
1873 else if(statement==ID_decl)
1877 const typet &symbol_type = symbol.
type();
1880 symbol_type.
id() == ID_pointer ||
1881 (symbol_type.
id() == ID_array &&
1882 to_array_type(symbol_type).element_type().
id() == ID_pointer))
1891 assign(symbol, address_of_expr, ns,
false,
false);
1894 assign(symbol,
exprt(ID_invalid), ns,
false,
false);
1897 else if(statement==ID_expression)
1901 else if(statement == ID_cpp_delete || statement == ID_cpp_delete_array)
1905 else if(statement==
"lock" || statement==
"unlock")
1909 else if(statement==ID_asm)
1913 else if(statement==ID_nondet)
1917 else if(statement==ID_printf)
1921 else if(statement==ID_return)
1929 else if(statement==ID_array_set)
1932 else if(statement==ID_array_copy)
1935 else if(statement==ID_array_replace)
1938 else if(statement == ID_array_equal)
1941 else if(statement==ID_assume)
1945 else if(statement==ID_user_specified_predicate ||
1946 statement==ID_user_specified_parameter_predicates ||
1947 statement==ID_user_specified_return_predicates)
1951 else if(statement==ID_fence)
1958 else if(statement==ID_dead)
1962 else if(statement == ID_havoc_object)
1968 "value_sett: unexpected statement: " +
id2string(statement));
1976 if(expr.
id()==ID_and)
1978 for(
const auto &op : expr.
operands())
1981 else if(expr.
id()==ID_equal)
1984 else if(expr.
id()==ID_notequal)
1987 else if(expr.
id()==ID_not)
1990 else if(expr.
id()==ID_dynamic_object)
2006 const std::unordered_set<exprt, irep_hash> &values_to_erase)
2008 if(values_to_erase.empty())
2015 std::vector<object_map_dt::key_type> keys_to_erase;
2017 for(
auto &key_value : entry->object_map.read())
2019 const auto &rhs_object =
to_expr(key_value);
2020 if(values_to_erase.count(rhs_object))
2022 keys_to_erase.emplace_back(key_value.first);
2027 keys_to_erase.size() == values_to_erase.size(),
2028 "value_sett::erase_value_from_entry() should erase exactly one value for "
2029 "each element in the set it is given");
2031 entryt replacement = *entry;
2032 for(
const auto &key_to_erase : keys_to_erase)
2036 values.replace(index, std::move(replacement));
2041 const std::string &erase_prefix,
2044 for(
const auto &c : struct_union_type.
components())
2046 const typet &subtype = c.type();
2047 const irep_idt &name = c.get_name();
2051 subtype.
id() != ID_code,
"struct/union member must not be of code type");
2052 if(c.get_is_padding())
2061 const std::string &erase_prefix,
2064 if(type.
id() == ID_struct_tag)
2067 else if(type.
id() == ID_union_tag)
2070 else if(type.
id() == ID_array)
2072 to_array_type(type).element_type(), erase_prefix +
"[]", ns);
2073 else if(
values.has_key(erase_prefix))
2074 values.erase(erase_prefix);
std::optional< symbol_exprt > get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
Get the failed-dereference symbol for the given symbol.
API to expression classes for bitvectors.
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
unsignedbv_typet unsigned_char_type()
bitvector_typet char_type()
bitvector_typet c_index_type()
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Operator to return the address of an object.
const typet & element_type() const
The type of the elements of the array.
A base class for binary expressions.
A goto_instruction_codet representing an assignment in the program.
A goto_instruction_codet representing the declaration of a local variable.
goto_instruction_codet representation of a "return from afunction" statement.
const exprt & return_value() const
std::vector< parametert > parameterst
const parameterst & parameters() const
Data structure for representing an arbitrary statement in a program.
const irep_idt & get_statement() const
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Representation of heap-allocated objects.
unsigned int get_instance() const
void set_instance(unsigned int instance)
Base class for all expressions.
std::vector< exprt > operandst
bool is_zero() const
Return whether the expression is a constant representing 0.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irept & find(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
const std::string & id_string() const
const irep_idt & id() const
const std::string & get_string(const irep_idt &name) const
Extract member of struct or union.
const exprt & compound() const
Binary multiplication Associativity is not specified.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Split an expression into a base object and a (byte) offset.
The plus expression Associativity is not specified.
const typet & base_type() const
The type of the data what we point to.
std::vector< view_itemt > viewt
std::vector< delta_view_itemt > delta_viewt
void get_delta_view(const sharing_mapt &other, delta_viewt &delta_view, const bool only_common=true) const
Get a delta view of the elements in the map.
const irep_idt & get_statement() const
Structure type, corresponds to C style structs.
Base type for structs and unions.
const typet & component_type(const irep_idt &component_name) const
const componentst & components() const
bool has_component(const irep_idt &component_name) const
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
typet type
Type of symbol.
irep_idt name
The unique identifier.
const irep_idt & display_name() const
Return language specific display name if present.
The Boolean constant true.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
The unary minus expression.
std::list< exprt > valuest
virtual void apply_code_rec(const codet &code, const namespacet &ns)
Subclass customisation point for applying code to this domain:
sharing_mapt< irep_idt, entryt > valuest
Map representing the entire value set, mapping from string LHS IDs to RHS expression sets.
bool eval_pointer_offset(exprt &expr, const namespacet &ns) const
Tries to resolve any pointer_offset_exprt expressions in expr to constant integers using this value-s...
const entryt * find_entry(const irep_idt &id) const
Finds an entry in this value-set.
std::vector< exprt > get_value_set(exprt expr, const namespacet &ns) const
Gets values pointed to by expr, including following dereference operators (i.e.
std::optional< exprt > offsett
Represents the offset into an object: either some (possibly constant) expression, or an unknown value...
virtual void get_value_set_rec(const exprt &expr, object_mapt &dest, bool &includes_nondet_pointer, const std::string &suffix, const typet &original_type, const namespacet &ns) const
Subclass customisation point for recursion over RHS expression.
xmlt output_xml(void) const
Output the value set formatted as XML.
void output(std::ostream &out, const std::string &indent="") const
Pretty-print this value-set.
void dereference_rec(const exprt &src, exprt &dest) const
Sets dest to src with any wrapping typecasts removed.
void erase_symbol(const symbol_exprt &symbol_expr, const namespacet &ns)
valuest values
Stores the LHS ID -> RHS expression set map.
unsigned location_number
Matches the location_number field of the instruction that corresponds to this value_sett instance in ...
static object_numberingt object_numbering
Global shared object numbering, used to abbreviate expressions stored in value sets.
bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
Merges an existing element into an object map.
void erase_struct_union_symbol(const struct_union_typet &struct_union_type, const std::string &erase_prefix, const namespacet &ns)
void get_reference_set_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
See get_reference_set.
exprt to_expr(const object_map_dt::value_type &it) const
Converts an object_map_dt element object_number -> offset into an object_descriptor_exprt with ....
void erase_values_from_entry(const irep_idt &index, const std::unordered_set< exprt, irep_hash > &values_to_erase)
Update the entry stored at index by erasing any values listed in values_to_erase.
void update_entry(const entryt &e, const typet &type, const object_mapt &new_values, bool add_to_sets)
Adds or replaces an entry in this value-set.
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool is_simplified, bool add_to_sets)
Transforms this value-set by executing executing the assignment lhs := rhs against it.
reference_counting< object_map_dt, empty_object_map > object_mapt
Reference-counts instances of object_map_dt, such that multiple instructions' value_sett instances ca...
virtual void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, bool add_to_sets)
Subclass customisation point for recursion over LHS expression:
insert_actiont get_insert_action(const object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const
Determines what would happen if object number n was inserted into map dest with offset offset – the p...
bool make_union(object_mapt &dest, const object_mapt &src) const
Merges two RHS expression sets.
virtual bool field_sensitive(const irep_idt &id, const typet &type)
Determines whether an identifier of a given type should have its fields distinguished.
void guard(const exprt &expr, const namespacet &ns)
Transforms this value-set by assuming an expression holds.
bool make_union_would_change(const object_mapt &dest, const object_mapt &src) const
Determines whether merging two RHS expression sets would cause any change.
void do_end_function(const exprt &lhs, const namespacet &ns)
Transforms this value-set by assigning this function's return value to a given LHS expression.
static const object_map_dt empty_object_map
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
Transforms this value-set by executing the actual -> formal parameter assignments for a particular ca...
void get_reference_set(const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
Gets the set of expressions that expr may refer to, according to this value set.
virtual void apply_assign_side_effects(const exprt &lhs, const exprt &rhs, const namespacet &)
Subclass customisation point to apply global side-effects to this domain, after RHS values are read b...
std::map< object_numberingt::number_type, offsett > object_map_dt
Represents a set of expressions (exprt instances) with corresponding offsets (offsett instances).
virtual void adjust_assign_rhs_values(const exprt &rhs, const namespacet &, object_mapt &rhs_values) const
Subclass customisation point to filter or otherwise alter the value-set returned from get_value_set b...
std::optional< irep_idt > get_index_of_symbol(irep_idt identifier, const typet &type, const std::string &suffix, const namespacet &ns) const
Get the index of the symbol and suffix.
void erase_symbol_rec(const typet &type, const std::string &erase_prefix, const namespacet &ns)
Operator to update elements in structs and arrays.
xmlt & new_element(const std::string &key)
static void escape(const std::string &s, std::ostream &out)
escaping for XML elements
bool has_prefix(const std::string &s, const std::string &prefix)
#define Forall_operands(it, expr)
bool can_cast_expr(const exprt &base)
Check whether a reference to a generic exprt is of a specific derived class.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
const code_assignt & to_code_assign(const goto_instruction_codet &code)
const code_declt & to_code_decl(const goto_instruction_codet &code)
const code_returnt & to_code_return(const goto_instruction_codet &code)
const std::string & id2string(const irep_idt &d)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
numberingt< exprt, irep_hash > object_numberingt
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)
Cast an exprt to a pointer_offset_exprt.
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
std::optional< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
std::optional< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNIMPLEMENTED_FEATURE(FEATURE)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
ssa_exprt remove_level_2(ssa_exprt ssa)
bool is_ssa_expr(const exprt &expr)
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
side_effect_exprt & to_side_effect_expr(exprt &expr)
const code_assumet & to_code_assume(const codet &code)
const codet & to_code(const exprt &expr)
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const struct_or_union_tag_typet & to_struct_or_union_tag_type(const typet &type)
Cast a typet to a struct_or_union_tag_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Represents a row of a value_sett.
static bool failed(bool error_indicator)
static std::string strip_first_field_from_suffix(const std::string &suffix, const std::string &field)
static bool suffix_starts_with_field(const std::string &suffix, const std::string &field)
Check if 'suffix' starts with 'field'.