const namespacet &ns,

std::ostream &out) const

{

for(valuest::const_iterator

v_it=values.begin();

v_it!=values.end();

v_it++)

{

irep_idt identifier, display_name;

const entryt &e=v_it->second;

if(e.identifier.starts_with("value_set::dynamic_object"))

{

display_name=id2string(e.identifier)+e.suffix;

identifier.clear();

}

else

{

#if 0

const symbolt &symbol=ns.lookup(id2string(e.identifier));

display_name=symbol.display_name()+e.suffix;

identifier=symbol.name;

#else

identifier=id2string(e.identifier);

display_name=id2string(identifier)+e.suffix;

#endif

}

out << display_name;

out << " = { ";

object_mapt object_map;

flatten(e, object_map);

std::size_t width=0;

const auto &entries = object_map.read();

for(object_map_dt::const_iterator o_it = entries.begin();

o_it != entries.end();

++o_it)

{

const exprt &o=object_numbering[o_it->first];

std::string result;

if(o.id()==ID_invalid || o.id()==ID_unknown)

{

result="<";

result+=from_expr(ns, identifier, o);

result+=", *, "; // offset unknown

if(o.type().id()==ID_unknown)

result+='*';

else

result+=from_type(ns, identifier, o.type());

result+='>';

}

else

{

result="<"+from_expr(ns, identifier, o)+", ";

if(o_it->second)

result += integer2string(*o_it->second);

else

result+='*';

result+=", ";

if(o.type().id()==ID_unknown)

result+='*';

else

result+=from_type(ns, identifier, o.type());

result+='>';

}

out << result;

width+=result.size();

object_map_dt::const_iterator next(o_it);

next++;

if(next != entries.end())

{

out << ", ";

if(width>=40)

out << "\n ";

}

}

out << " } \n";

}

const entryt &e,

object_mapt &dest) const

{

#if 0

std::cout << "FLATTEN: " << e.identifier << e.suffix << '\n';

#endif

flatten_seent seen;

flatten_rec(e, dest, seen);

#if 0

std::cout << "FLATTEN: Done.\n";

#endif

const entryt &e,

object_mapt &dest,

flatten_seent &seen) const

{

#if 0

std::cout << "FLATTEN_REC: " << e.identifier << e.suffix << '\n';

#endif

std::string identifier = id2string(e.identifier);

CHECK_RETURN(seen.find(identifier + e.suffix) == seen.end());

bool generalize_index = false;

seen.insert(identifier + e.suffix);

for(const auto &object_entry : e.object_map.read())

{

const exprt &o = object_numbering[object_entry.first];

if(o.type().id()=="#REF#")

{

if(seen.find(o.get(ID_identifier))!=seen.end())

{

generalize_index = true;

continue;

}

valuest::const_iterator fi = values.find(o.get(ID_identifier));

if(fi==values.end())

{

// this is some static object, keep it in.

const symbol_exprt se(

o.get(ID_identifier), to_type_with_subtype(o.type()).subtype());

insert(dest, se, mp_integer{0});

}

else

{

object_mapt temp;

flatten_rec(fi->second, temp, seen);

for(object_map_dt::iterator t_it=temp.write().begin();

t_it!=temp.write().end();

t_it++)

{

if(t_it->second && object_entry.second)

{

*t_it->second += *object_entry.second;

}

else

t_it->second.reset();

}

for(const auto &object_entry : temp.read())

insert(dest, object_entry);

}

}

else

insert(dest, object_entry);

}

if(generalize_index) // this means we had recursive symbols in there

{

for(auto &object_entry : dest.write())

object_entry.second.reset();

}

seen.erase(identifier + e.suffix);

{

const exprt &object=object_numbering[it.first];

if(object.id()==ID_invalid ||

object.id()==ID_unknown)

return object;

object_descriptor_exprt od;

od.object()=object;

if(it.second)

od.offset() = from_integer(*it.second, c_index_type());

od.type()=od.object().type();

return std::move(od);

{

UNREACHABLE;

bool result=false;

for(valuest::const_iterator

it=new_values.begin();

it!=new_values.end();

it++)

{

valuest::iterator it2=values.find(it->first);

if(it2==values.end())

{

// we always track these

if(

it->second.identifier.starts_with("value_set::dynamic_object") ||

it->second.identifier.starts_with("value_set::return_value"))

{

values.insert(*it);

result=true;

}

continue;

}

entryt &e=it2->second;

const entryt &new_e=it->second;

if(make_union(e.object_map, new_e.object_map))

result=true;

}

changed = result;

return result;

{

bool result=false;

for(const auto &object_entry : src.read())

{

if(insert(dest, object_entry))

result=true;

}

return result;

{

object_mapt object_map;

get_value_set(expr, object_map, ns);

object_mapt flat_map;

for(const auto &object_entry : object_map.read())

{

const exprt &object = object_numbering[object_entry.first];

if(object.type().id()=="#REF#")

{

DATA_INVARIANT(object.id() == ID_symbol, "reference to symbol required");

const irep_idt &ident = object.get(ID_identifier);

valuest::const_iterator v_it = values.find(ident);

if(v_it!=values.end())

{

object_mapt temp;

flatten(v_it->second, temp);

for(object_map_dt::iterator t_it=temp.write().begin();

t_it!=temp.write().end();

t_it++)

{

if(t_it->second && object_entry.second)

{

*t_it->second += *object_entry.second;

}

else

t_it->second.reset();

flat_map.write()[t_it->first]=t_it->second;

}

}

}

else

flat_map.write()[object_entry.first] = object_entry.second;

}

std::vector<exprt> result;

for(const auto &object_entry : flat_map.read())

result.push_back(to_expr(object_entry));

#if 0

// Sanity check!

for(std::list<exprt>::const_iterator it=value_set.begin();

it!=value_set.end();

it++)

assert(it->type().id()!="#REF");

#endif

#if 0

for(expr_sett::const_iterator it=value_set.begin(); it!=value_set.end(); it++)

std::cout << "GET_VALUE_SET: " << format(*it) << '\n';

#endif

return result;

const exprt &expr,

object_mapt &dest,

const namespacet &ns) const

{

exprt tmp(expr);

simplify(tmp, ns);

gvs_recursion_sett recset;

bool includes_nondet_pointer = false;

get_value_set_rec(

tmp, dest, includes_nondet_pointer, "", tmp.type(), ns, recset);

const exprt &expr,

object_mapt &dest,

bool &includes_nondet_pointer,

const std::string &suffix,

const typet &original_type,

const namespacet &ns,

gvs_recursion_sett &recursion_set) const

{

#if 0

std::cout << "GET_VALUE_SET_REC EXPR: " << format(expr)

<< '\n';

std::cout << "GET_VALUE_SET_REC SUFFIX: " << suffix << '\n';

std::cout << '\n';

#endif

if(expr.type().id()=="#REF#")

{

valuest::const_iterator fi = values.find(expr.get(ID_identifier));

if(fi!=values.end())

{

for(const auto &object_entry : fi->second.object_map.read())

{

get_value_set_rec(

object_numbering[object_entry.first],

dest,

includes_nondet_pointer,

suffix,

original_type,

ns,

recursion_set);

}

return;

}

else

{

insert(dest, exprt(ID_unknown, original_type));

return;

}

}

else if(expr.id()==ID_unknown || expr.id()==ID_invalid)

{

insert(dest, exprt(ID_unknown, original_type));

return;

}

else if(expr.id()==ID_index)

{

const typet &type = to_index_expr(expr).array().type();

if(type.id() == ID_array)

{

get_value_set_rec(

to_index_expr(expr).array(),

dest,

includes_nondet_pointer,

"[]" + suffix,

original_type,

ns,

recursion_set);

}

else

insert(dest, exprt(ID_unknown, original_type));

return;

}

else if(expr.id()==ID_member)

{

const auto &compound = to_member_expr(expr).compound();

if(compound.is_not_nil())

{

DATA_INVARIANT(

compound.type().id() == ID_struct ||

compound.type().id() == ID_struct_tag ||

compound.type().id() == ID_union ||

compound.type().id() == ID_union_tag,

"operand 0 of member expression must be struct or union");

const std::string &component_name =

id2string(to_member_expr(expr).get_component_name());

get_value_set_rec(

compound,

dest,

includes_nondet_pointer,

"." + component_name + suffix,

original_type,

ns,

recursion_set);

return;

}

}

else if(expr.id()==ID_symbol)

{

// just keep a reference to the ident in the set

// (if it exists)

irep_idt ident = id2string(to_symbol_expr(expr).get_identifier()) + suffix;

valuest::const_iterator v_it=values.find(ident);

if(ident.starts_with(alloc_adapter_prefix))

{

insert(dest, expr, mp_integer{0});

return;

}

else if(v_it!=values.end())

{

type_with_subtypet t("#REF#", expr.type());

symbol_exprt sym(ident, t);

insert(dest, sym, mp_integer{0});

return;

}

}

else if(expr.id()==ID_if)

{

get_value_set_rec(

to_if_expr(expr).true_case(),

dest,

includes_nondet_pointer,

suffix,

original_type,

ns,

recursion_set);

get_value_set_rec(

to_if_expr(expr).false_case(),

dest,

includes_nondet_pointer,

suffix,

original_type,

ns,

recursion_set);

return;

}

else if(expr.id()==ID_address_of)

{

get_reference_set_sharing(to_address_of_expr(expr).object(), dest, ns);

return;

}

else if(expr.id()==ID_dereference)

{

object_mapt reference_set;

get_reference_set_sharing(expr, reference_set, ns);

const object_map_dt &object_map=reference_set.read();

if(object_map.begin()!=object_map.end())

{

for(const auto &object_entry : object_map)

{

const exprt &object = object_numbering[object_entry.first];

get_value_set_rec(

object,

dest,

includes_nondet_pointer,

suffix,

original_type,

ns,

recursion_set);

}

return;

}

}

else if(expr.is_constant())

{

// check if NULL

if(to_constant_expr(expr).is_null_pointer())

{

insert(

dest,

exprt(ID_null_object, to_pointer_type(expr.type()).base_type()),

mp_integer{0});

return;

}

}

else if(expr.id()==ID_typecast)

{

get_value_set_rec(

to_typecast_expr(expr).op(),

dest,

includes_nondet_pointer,

suffix,

original_type,

ns,

recursion_set);

return;

}

else if(expr.id()==ID_plus || expr.id()==ID_minus)

{

if(expr.operands().size()<2)

throw expr.id_string()+" expected to have at least two operands";

if(expr.type().id()==ID_pointer)

{

// find the pointer operand

const exprt *ptr_operand=nullptr;

for(const auto &op : expr.operands())

{

if(op.type().id() == ID_pointer)

{

if(ptr_operand==nullptr)

ptr_operand = &op;

else

throw "more than one pointer operand in pointer arithmetic";

}

}

if(ptr_operand==nullptr)

throw "pointer type sum expected to have pointer operand";

object_mapt pointer_expr_set;

get_value_set_rec(

*ptr_operand,

pointer_expr_set,

includes_nondet_pointer,

"",

ptr_operand->type(),

ns,

recursion_set);

for(const auto &object_entry : pointer_expr_set.read())

{

offsett offset = object_entry.second;

if(offset_is_zero(offset) && expr.operands().size() == 2)

{

if(to_binary_expr(expr).op0().type().id() != ID_pointer)

{

const auto i = numeric_cast<mp_integer>(to_binary_expr(expr).op0());

if(!i.has_value())

offset.reset();

else

*offset = (expr.id() == ID_plus) ? *i : -*i;

}

else

{

const auto i = numeric_cast<mp_integer>(to_binary_expr(expr).op1());

if(!i.has_value())

offset.reset();

else

*offset = (expr.id() == ID_plus) ? *i : -*i;

}

}

else

offset.reset();

insert(dest, object_entry.first, offset);

}

return;

}

}

else if(expr.id()==ID_side_effect)

{

const irep_idt &statement = to_side_effect_expr(expr).get_statement();

if(statement==ID_function_call)

{

// these should be gone

throw "unexpected function_call sideeffect";

}

else if(statement==ID_allocate)

{

if(expr.type().id()!=ID_pointer)

throw "malloc expected to return pointer type";

PRECONDITION(suffix.empty());

const typet &dynamic_type=

static_cast<const typet &>(expr.find(ID_C_cxx_alloc_type));

dynamic_object_exprt dynamic_object(dynamic_type);

// let's make up a `unique' number for this object...

dynamic_object.set_instance(

(from_function << 16) | from_target_index);

dynamic_object.valid()=true_exprt();

insert(dest, dynamic_object, mp_integer{0});

return;

}

else if(statement==ID_cpp_new ||

statement==ID_cpp_new_array)

{

PRECONDITION(suffix.empty());

PRECONDITION(expr.type().id() == ID_pointer);

dynamic_object_exprt dynamic_object(

to_pointer_type(expr.type()).base_type());

dynamic_object.set_instance(

(from_function << 16) | from_target_index);

dynamic_object.valid()=true_exprt();

insert(dest, dynamic_object, mp_integer{0});

return;

}

}

else if(expr.id()==ID_struct)

{

// this is like a static struct object

insert(dest, address_of_exprt(expr), mp_integer{0});

return;

}

else if(expr.id()==ID_with)

{

// these are supposed to be done by assign()

throw "unexpected value in get_value_set: "+expr.id_string();

}

else if(expr.id()==ID_array_of ||

expr.id()==ID_array)

{

// an array constructor, possibly containing addresses

for(const auto &op : expr.operands())

{

get_value_set_rec(

op,

dest,

includes_nondet_pointer,

suffix,

original_type,

ns,

recursion_set);

}

}

else if(expr.id()==ID_dynamic_object)

{

const dynamic_object_exprt &dynamic_object=

to_dynamic_object_expr(expr);

const std::string name=

"value_set::dynamic_object"+

std::to_string(dynamic_object.get_instance())+

suffix;

// look it up

valuest::const_iterator v_it=values.find(name);

if(v_it!=values.end())

{

make_union(dest, v_it->second.object_map);

return;

}

}

insert(dest, exprt(ID_unknown, original_type));

const exprt &src,

exprt &dest) const

{

// remove pointer typecasts

if(src.id()==ID_typecast)

{

PRECONDITION(src.type().id() == ID_pointer);

dereference_rec(to_typecast_expr(src).op(), dest);

}

else

dest=src;

const exprt &expr,

expr_sett &dest,

const namespacet &ns) const

{

object_mapt object_map;

get_reference_set_sharing(expr, object_map, ns);

for(const auto &object_entry : object_map.read())

{

const exprt &object = object_numbering[object_entry.first];

if(object.type().id() == "#REF#")

{

const irep_idt &ident = object.get(ID_identifier);

valuest::const_iterator vit = values.find(ident);

if(vit==values.end())

{

// Assume the variable never was assigned,

// so assume it's reference set is unknown.

dest.insert(exprt(ID_unknown, object.type()));

}

else

{

object_mapt omt;

flatten(vit->second, omt);

for(object_map_dt::iterator t_it=omt.write().begin();

t_it!=omt.write().end();

t_it++)

{

if(t_it->second && object_entry.second)

{

*t_it->second += *object_entry.second;

}

else

t_it->second.reset();

}

for(const auto &o : omt.read())

dest.insert(to_expr(o));

}

}

else

dest.insert(to_expr(object_entry));

}

const exprt &expr,

expr_sett &dest,

const namespacet &ns) const

{

object_mapt object_map;

get_reference_set_sharing(expr, object_map, ns);

for(const auto &object_entry : object_map.read())

dest.insert(to_expr(object_entry));

const exprt &expr,

object_mapt &dest,

const namespacet &ns) const

{

#if 0

std::cout << "GET_REFERENCE_SET_REC EXPR: " << format(expr)

<< '\n';

#endif

if(expr.type().id()=="#REF#")

{

valuest::const_iterator fi = values.find(expr.get(ID_identifier));

if(fi!=values.end())

{

for(const auto &object_entry : fi->second.object_map.read())

{

get_reference_set_sharing_rec(

object_numbering[object_entry.first], dest, ns);

}

return;

}

}

else if(expr.id()==ID_symbol ||

expr.id()==ID_dynamic_object ||

expr.id()==ID_string_constant)

{

if(

expr.type().id() == ID_array &&

to_array_type(expr.type()).element_type().id() == ID_array)

{

insert(dest, expr);

}

else

insert(dest, expr, mp_integer{0});

return;

}

else if(expr.id()==ID_dereference)

{

gvs_recursion_sett recset;

object_mapt temp;

bool includes_nondet_pointer = false;

get_value_set_rec(

to_dereference_expr(expr).pointer(),

temp,

includes_nondet_pointer,

"",

to_dereference_expr(expr).pointer().type(),

ns,

recset);

// REF's need to be dereferenced manually!

for(const auto &object_entry : temp.read())

{

const exprt &obj = object_numbering[object_entry.first];

if(obj.type().id()=="#REF#")

{

const irep_idt &ident = obj.get(ID_identifier);

valuest::const_iterator v_it = values.find(ident);

if(v_it!=values.end())

{

object_mapt t2;

flatten(v_it->second, t2);

for(object_map_dt::iterator t_it=t2.write().begin();

t_it!=t2.write().end();

t_it++)

{

if(t_it->second && object_entry.second)

{

*t_it->second += *object_entry.second;

}

else

t_it->second.reset();

}

for(const auto &t2_object_entry : t2.read())

insert(dest, t2_object_entry);

}

else

insert(

dest,

exprt(ID_unknown, to_type_with_subtype(obj.type()).subtype()));

}

else

insert(dest, object_entry);

}

#if 0

for(expr_sett::const_iterator it=value_set.begin();

it!=value_set.end();

it++)

std::cout << "VALUE_SET: " << format(*it) << '\n';

#endif

return;

}

else if(expr.id()==ID_index)

{

const exprt &array = to_index_expr(expr).array();

const exprt &offset = to_index_expr(expr).index();

const typet &array_type = array.type();

DATA_INVARIANT(

array_type.id() == ID_array, "index takes array-typed operand");

object_mapt array_references;

get_reference_set_sharing(array, array_references, ns);

const object_map_dt &object_map=array_references.read();

for(const auto &object_entry : object_map)

{

const exprt &object = object_numbering[object_entry.first];

if(

object.id() == ID_unknown ||

(object.type().id() != ID_array && object.type().id() != ID_vector))

{

insert(dest, exprt(ID_unknown, expr.type()));

}

else

{

index_exprt index_expr(

object, from_integer(0, c_index_type()), expr.type());

exprt casted_index;

// adjust type?

if(object.type().id() != "#REF#" && object.type() != array_type)

casted_index = typecast_exprt(index_expr, array.type());

else

casted_index = index_expr;

offsett o = object_entry.second;

const auto i = numeric_cast<mp_integer>(offset);

if(offset == 0)

{

}

else if(i.has_value() && offset_is_zero(o))

*o = *i;

else

o.reset();

insert(dest, casted_index, o);

}

}

return;

}

else if(expr.id()==ID_member)

{

const irep_idt &component_name=expr.get(ID_component_name);

const exprt &struct_op = to_member_expr(expr).compound();

object_mapt struct_references;

get_reference_set_sharing(struct_op, struct_references, ns);

for(const auto &object_entry : struct_references.read())

{

const exprt &object = object_numbering[object_entry.first];

const typet &obj_type = object.type();

if(object.id()==ID_unknown)

insert(dest, exprt(ID_unknown, expr.type()));

else if(

obj_type.id() != ID_struct && obj_type.id() != ID_union &&

obj_type.id() != ID_struct_tag && obj_type.id() != ID_union_tag)

{

// we catch objects of the wrong type,

// to avoid non-integral typecasts.

insert(dest, exprt(ID_unknown, expr.type()));

}

else

{

offsett o = object_entry.second;

member_exprt member_expr(object, component_name, expr.type());

// adjust type?

if(struct_op.type() != object.type())

{

member_expr.compound() =

typecast_exprt(member_expr.compound(), struct_op.type());

}

insert(dest, member_expr, o);

}

}

return;

}

else if(expr.id()==ID_if)

{

get_reference_set_sharing_rec(to_if_expr(expr).true_case(), dest, ns);

get_reference_set_sharing_rec(to_if_expr(expr).false_case(), dest, ns);

return;

}

insert(dest, exprt(ID_unknown, expr.type()));

const exprt &lhs,

const exprt &rhs,

const namespacet &ns)