46 id==
"value_set::return_value" ||
47 id==
"value_set::memory")
51 return ns.
follow(type).
id()==ID_struct;
57 auto found =
values.find(
id);
58 return found ==
values.end() ? nullptr : &found->second;
73 std::pair<valuest::iterator, bool>
r=
74 values.insert(std::pair<idt, entryt>(index, e));
76 return r.first->second;
89 dest.
write()[n] = offset;
92 else if(!entry->second)
94 else if(offset && *entry->second == *offset)
98 dest.
write()[n].reset();
105 std::ostream &out)
const
107 for(valuest::const_iterator
114 const entryt &e=v_it->second;
121 else if(e.
identifier==
"value_set::return_value")
123 display_name=
"RETURN_VALUE"+e.
suffix;
131 identifier=symbol.
name;
147 o_it=object_map.
begin();
148 o_it!=object_map.
end();
155 if(o.
id()==ID_invalid || o.
id()==ID_unknown)
159 result=
"<"+
from_expr(ns, identifier, o)+
", ";
176 width+=result.size();
181 if(next!=object_map.
end())
197 if(
object.
id()==ID_invalid ||
198 object.
id()==ID_unknown)
210 return std::move(od);
217 valuest::iterator v_it=
values.begin();
219 for(valuest::const_iterator
220 it=new_values.begin();
221 it!=new_values.end();
224 if(v_it==
values.end() || it->first<v_it->first)
231 else if(v_it->first<it->first)
237 assert(v_it->first==it->first);
240 const entryt &new_e=it->second;
273 if(expr.
id()==ID_pointer_offset)
285 it=object_map.
begin();
286 it!=object_map.
end();
295 if(!ptr_offset.has_value())
298 *ptr_offset += *it->second;
300 if(mod && *ptr_offset != previous_offset)
304 previous_offset = *ptr_offset;
335 for(value_setst::valuest::const_iterator it=dest.begin();
336 it!=dest.end(); it++)
337 std::cout <<
"GET_VALUE_SET: " <<
format(*it) <<
'\n';
345 bool is_simplified)
const
358 const std::string &suffix,
const std::string &field)
363 suffix.compare(1, field.length(), field) == 0 &&
364 (suffix.length() == field.length() + 1 ||
365 suffix[field.length() + 1] ==
'.' ||
366 suffix[field.length() + 1] ==
'[');
370 const std::string &suffix,
const std::string &field)
374 "suffix should start with " + field);
375 return suffix.substr(field.length() + 1);
381 const std::string &suffix,
382 const typet &original_type,
386 std::cout <<
"GET_VALUE_SET_REC EXPR: " <<
format(expr) <<
"\n";
387 std::cout <<
"GET_VALUE_SET_REC SUFFIX: " << suffix <<
'\n';
392 if(expr.
id()==ID_unknown || expr.
id()==ID_invalid)
396 else if(expr.
id()==ID_index)
403 type.id()==ID_incomplete_array,
404 "operand 0 of index expression must be an array");
408 else if(expr.
id()==ID_member)
415 type.id()==ID_union ||
416 type.id()==ID_incomplete_struct ||
417 type.id()==ID_incomplete_union,
418 "operand 0 of member expression must be struct or union");
420 const std::string &component_name=
424 "."+component_name+suffix, original_type, ns);
426 else if(expr.
id()==ID_symbol)
431 if(expr_type.
id()==ID_pointer ||
432 expr_type.
id()==ID_signedbv ||
433 expr_type.
id()==ID_unsignedbv ||
434 expr_type.
id()==ID_struct ||
435 expr_type.
id()==ID_union ||
436 expr_type.
id()==ID_array)
443 if(!entry && (expr_type.
id() == ID_struct || expr_type.
id() == ID_union))
448 const irep_idt &first_component_name =
449 struct_union_type.
components().front().get_name();
468 else if(expr.
id()==ID_if)
471 throw "if takes three operands";
476 else if(expr.
id()==ID_address_of)
479 throw expr.
id_string()+
" expected to have one operand";
483 else if(expr.
id()==ID_dereference)
489 if(object_map.
begin()==object_map.
end())
494 it1=object_map.
begin();
495 it1!=object_map.
end();
505 else if(expr.
id()==
"reference_to")
514 if(object_map.
begin()==object_map.
end())
519 it=object_map.
begin();
520 it!=object_map.
end();
533 if(expr.
get(ID_value)==ID_NULL &&
534 expr_type.
id()==ID_pointer)
538 else if(expr_type.
id()==ID_unsignedbv ||
539 expr_type.
id()==ID_signedbv)
547 else if(expr.
id()==ID_typecast)
550 throw "typecast takes one operand";
556 if(op_type.
id()==ID_pointer)
561 else if(op_type.
id()==ID_unsignedbv ||
562 op_type.
id()==ID_signedbv)
596 else if(expr.
id()==ID_plus ||
600 throw expr.
id_string()+
" expected to have at least two operands";
609 expr_type.
id()==ID_pointer)
617 ptr_operand=expr.
op1();
622 ptr_operand=expr.
op0();
628 if(pointer_sub_type.
id()==ID_empty)
633 if(!size.has_value() || (*size) == 0)
641 if(expr.
id()==ID_minus)
647 ptr_operand, pointer_expr_set,
"", ptr_operand.
type(), ns);
655 *it, pointer_expr_set,
"", it->type(), ns);
661 it!=pointer_expr_set.
read().
end();
667 if(offset && i_is_set)
672 insert(dest, it->first, offset);
675 else if(expr.
id()==ID_mult)
681 throw expr.
id_string()+
" expected to have at least two operands";
689 *it, pointer_expr_set,
"", it->type(), ns);
694 it!=pointer_expr_set.
read().
end();
702 insert(dest, it->first, offset);
705 else if(expr.
id()==ID_side_effect)
709 if(statement==ID_function_call)
712 throw "unexpected function_call sideeffect";
714 else if(statement==ID_allocate)
718 const typet &dynamic_type=
719 static_cast<const typet &>(expr.
find(ID_C_cxx_alloc_type));
727 else if(statement==ID_cpp_new ||
728 statement==ID_cpp_new_array)
731 assert(expr_type.
id()==ID_pointer);
742 else if(expr.
id()==ID_struct)
746 struct_components.size() == expr.
operands().size(),
747 "struct expression should have an operand per component");
748 auto component_iter = struct_components.begin();
749 bool found_component =
false;
755 const std::string &component_name =
759 std::string remaining_suffix =
762 found_component =
true;
776 else if(expr.
id()==ID_with)
782 if(expr_type.
id() == ID_struct && !suffix.
empty())
788 std::string remaining_suffix =
791 with_expr.
new_value(), dest, remaining_suffix, original_type, ns);
807 else if(expr_type.
id() == ID_array && !suffix.
empty())
809 std::string new_value_suffix;
811 new_value_suffix = suffix.substr(2);
818 with_expr.
new_value(), dest, new_value_suffix, original_type, ns);
828 else if(expr.
id()==ID_array)
831 std::string new_suffix = suffix;
833 new_suffix = suffix.substr(2);
840 else if(expr.
id()==ID_array_of)
843 std::string new_suffix = suffix;
845 new_suffix = suffix.substr(2);
852 else if(expr.
id()==ID_dynamic_object)
857 const std::string prefix=
858 "value_set::dynamic_object"+
862 const std::string full_name=prefix+suffix;
876 else if(expr.
id()==ID_byte_extract_little_endian ||
877 expr.
id()==ID_byte_extract_big_endian)
880 throw "byte_extract takes two operands";
890 if(!
to_integer(op1, op1_offset) && op0_type.
id()==ID_struct)
896 const irep_idt &name = c.get_name();
900 if(!comp_offset.has_value())
902 else if(*comp_offset > op1_offset)
904 else if(*comp_offset != op1_offset)
915 if(op0_type.
id()==ID_union)
920 const irep_idt &name = c.get_name();
930 else if(expr.
id()==ID_byte_update_little_endian ||
931 expr.
id()==ID_byte_update_big_endian)
934 throw "byte_update takes three operands";
945 std::cout <<
"WARNING: not doing " << expr.
id() <<
'\n';
950 std::cout <<
"GET_VALUE_SET_REC RESULT:\n";
951 for(
const auto &obj : dest.
read())
954 std::cout <<
" " <<
format(e) <<
"\n";
965 if(src.
id()==ID_typecast)
967 assert(src.
type().
id()==ID_pointer);
970 throw "typecast expects one operand";
999 std::cout <<
"GET_REFERENCE_SET_REC EXPR: " <<
format(expr)
1003 if(expr.
id()==ID_symbol ||
1004 expr.
id()==ID_dynamic_object ||
1005 expr.
id()==ID_string_constant ||
1006 expr.
id()==ID_array)
1008 if(expr.
type().
id()==ID_array &&
1016 else if(expr.
id()==ID_dereference)
1019 throw expr.
id_string()+
" expected to have one operand";
1024 for(expr_sett::const_iterator it=value_set.begin();
1025 it!=value_set.end(); it++)
1026 std::cout <<
"VALUE_SET: " <<
format(*it) <<
'\n';
1031 else if(expr.
id()==ID_index)
1034 throw "index expected to have two operands";
1041 assert(array_type.
id()==ID_array ||
1042 array_type.
id()==ID_incomplete_array);
1050 a_it=object_map.
begin();
1051 a_it!=object_map.
end();
1056 if(
object.
id()==ID_unknown)
1074 if(!size.has_value() || *size == 0)
1082 insert(dest, deref_index_expr, o);
1088 else if(expr.
id()==ID_member)
1090 const irep_idt &component_name=expr.
get(ID_component_name);
1093 throw "member expected to have one operand";
1103 it=object_map.
begin();
1104 it!=object_map.
end();
1109 if(
object.
id()==ID_unknown)
1120 const typet &final_object_type = ns.
follow(
object.type());
1122 if(final_object_type.id()==ID_struct ||
1123 final_object_type.id()==ID_union)
1126 if(ns.
follow(struct_op.
type())!=final_object_type)
1127 member_expr.op0().make_typecast(struct_op.
type());
1129 insert(dest, member_expr, o);
1138 else if(expr.
id()==ID_if)
1141 throw "if takes three operands";
1159 std::cout <<
"ASSIGN LHS: " <<
format(lhs) <<
" : "
1161 std::cout <<
"ASSIGN RHS: " <<
format(rhs) <<
" : "
1163 std::cout <<
"--------------------------------------------\n";
1169 if(type.
id()==ID_struct ||
1170 type.
id()==ID_union)
1174 const typet &subtype = c.type();
1175 const irep_idt &name = c.get_name();
1178 if(subtype.
id() == ID_code || c.get_is_padding())
1185 if(rhs.
id()==ID_unknown ||
1186 rhs.
id()==ID_invalid)
1188 rhs_member=
exprt(rhs.
id(), subtype);
1193 throw "value_sett::assign type mismatch: "
1199 assign(lhs_member, rhs_member, ns,
false, add_to_sets);
1203 else if(type.
id()==ID_array)
1208 if(rhs.
id()==ID_unknown ||
1209 rhs.
id()==ID_invalid)
1221 throw "value_sett::assign type mismatch: "
1225 if(rhs.
id()==ID_array_of)
1228 assign(lhs_index, rhs.
op0(), ns, is_simplified, add_to_sets);
1230 else if(rhs.
id()==ID_array ||
1231 rhs.
id()==ID_constant)
1235 assign(lhs_index, *o_it, ns, is_simplified, add_to_sets);
1239 else if(rhs.
id()==ID_with)
1246 assign(lhs_index, op0_index, ns, is_simplified, add_to_sets);
1247 assign(lhs_index, rhs.
op2(), ns, is_simplified,
true);
1253 assign(lhs_index, rhs_index, ns, is_simplified,
true);
1269 assign_rec(lhs, values_rhs,
"", ns, add_to_sets);
1276 const std::string &suffix,
1281 std::cout <<
"ASSIGN_REC LHS: " <<
format(lhs) <<
'\n';
1282 std::cout <<
"ASSIGN_REC LHS ID: " << lhs.
id() <<
'\n';
1283 std::cout <<
"ASSIGN_REC SUFFIX: " << suffix <<
'\n';
1288 std::cout <<
"ASSIGN_REC RHS: " <<
1293 if(lhs.
id()==ID_symbol)
1304 else if(lhs.
id()==ID_dynamic_object)
1309 const std::string name=
1310 "value_set::dynamic_object"+
1317 else if(lhs.
id()==ID_dereference)
1320 throw lhs.
id_string()+
" expected to have one operand";
1330 it!=reference_set.
read().
end();
1337 if(
object.
id()!=ID_unknown)
1338 assign_rec(
object, values_rhs, suffix, ns, add_to_sets);
1341 else if(lhs.
id()==ID_index)
1344 throw "index expected to have two operands";
1349 "operand 0 of index expression must be an array");
1353 else if(lhs.
id()==ID_member)
1356 throw "member expected to have one operand";
1358 const std::string &component_name=lhs.
get_string(ID_component_name);
1363 type.
id()==ID_union ||
1364 type.
id()==ID_incomplete_struct ||
1365 type.
id()==ID_incomplete_union,
1366 "operand 0 of member expression must be struct or union");
1369 lhs.
op0(), values_rhs,
"."+component_name+suffix, ns, add_to_sets);
1371 else if(lhs.
id()==
"valid_object" ||
1372 lhs.
id()==
"dynamic_size" ||
1373 lhs.
id()==
"dynamic_type" ||
1374 lhs.
id()==
"is_zero_string" ||
1375 lhs.
id()==
"zero_string" ||
1376 lhs.
id()==
"zero_string_length")
1380 else if(lhs.
id()==ID_string_constant)
1385 else if(lhs.
id() == ID_null_object)
1389 else if(lhs.
id()==ID_typecast)
1393 assign_rec(typecast_expr.
op(), values_rhs, suffix, ns, add_to_sets);
1395 else if(lhs.
id()==ID_byte_extract_little_endian ||
1396 lhs.
id()==ID_byte_extract_big_endian)
1401 else if(lhs.
id()==ID_integer_address)
1407 throw "assign NYI: `"+lhs.
id_string()+
"'";
1425 for(std::size_t i=0; i<arguments.size(); i++)
1427 const std::string identifier=
"value_set::dummy_arg_"+
std::to_string(i);
1428 const symbol_exprt dummy_lhs(identifier, arguments[i].type());
1429 assign(dummy_lhs, arguments[i], ns,
false,
false);
1436 for(code_typet::parameterst::const_iterator
1437 it=parameter_types.begin();
1438 it!=parameter_types.end();
1441 const irep_idt &identifier=it->get_identifier();
1449 assign(actual_lhs, v_expr, ns,
true,
true);
1465 assign(lhs, rhs, ns,
false,
false);
1474 if(statement==ID_block)
1479 else if(statement==ID_function_call)
1484 else if(statement==ID_assign)
1487 throw "assignment expected to have two operands";
1491 else if(statement==ID_decl)
1494 throw "decl expected to have one operand";
1498 if(lhs.
id()!=ID_symbol)
1499 throw "decl expected to have symbol on lhs";
1503 if(lhs_type.
id()==ID_pointer ||
1504 (lhs_type.
id()==ID_array &&
1514 assign(lhs, address_of_expr, ns,
false,
false);
1520 else if(statement==ID_expression)
1524 else if(statement==
"cpp_delete" ||
1525 statement==
"cpp_delete[]")
1529 else if(statement==
"lock" || statement==
"unlock")
1533 else if(statement==ID_asm)
1537 else if(statement==ID_nondet)
1541 else if(statement==ID_printf)
1545 else if(statement==ID_return)
1551 assign(lhs, code.
op0(), ns,
false,
false);
1554 else if(statement==ID_array_set)
1557 else if(statement==ID_array_copy)
1560 else if(statement==ID_array_replace)
1563 else if(statement==ID_assume)
1567 else if(statement==ID_user_specified_predicate ||
1568 statement==ID_user_specified_parameter_predicates ||
1569 statement==ID_user_specified_return_predicates)
1573 else if(statement==ID_fence)
1576 else if(statement==ID_input || statement==ID_output)
1580 else if(statement==ID_dead)
1587 throw "value_sett: unexpected statement: "+
id2string(statement);
1595 if(expr.
id()==ID_and)
1600 else if(expr.
id()==ID_equal)
1603 else if(expr.
id()==ID_notequal)
1606 else if(expr.
id()==ID_not)
1609 else if(expr.
id()==ID_dynamic_object)
1621 assign(expr.
op0(), address_of, ns,
false,
false);