Skip to content

SMT2: disambiguate element-address functions by index type #9064

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
tautschnig wants to merge 1 commit into
base: develop
Choose a base branch
from
+33 −7
Open

SMT2: disambiguate element-address functions by index type #9064

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
40 changes: 33 additions & 7 deletions src/solvers/smt2/smt2_conv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1923,15 +1923,30 @@ void smt2_convt::convert_expr(const exprt &expr)

auto element_size_expr_opt =
::size_of_expr(element_address_expr.element_type(), ns);
CHECK_RETURN(element_size_expr_opt.has_value());

out << "(element-address-" << type2id(expr.type()) << ' ';
// The size/offset arithmetic requires an integer index type. Heap arrays
// keyed by a non-integer type (Strata `Map Ref _`) or with mathematical
// element types have neither a sensible byte size nor an integer index;
// fall back to an integer index type and unit size to avoid building a
// constant of a struct type.
const typet &idx_t = element_address_expr.index().type();
const bool int_index =
idx_t.id() == ID_unsignedbv || idx_t.id() == ID_signedbv ||
idx_t.id() == ID_bv || idx_t.id() == ID_integer ||
idx_t.id() == ID_c_enum || idx_t.id() == ID_c_enum_tag;
const typet size_target = int_index ? idx_t : c_index_type();
Comment on lines +1931 to +1936
const exprt element_size_expr =
element_size_expr_opt.has_value()
? *element_size_expr_opt
: static_cast<exprt>(from_integer(1, size_target));
Comment on lines +1926 to +1940

out << "(element-address-" << type2id(expr.type()) << '_' << type2id(idx_t)
<< ' ';
convert_expr(element_address_expr.base());
out << ' ';
convert_expr(element_address_expr.index());
out << ' ';
convert_expr(typecast_exprt::conditional_cast(
*element_size_expr_opt, element_address_expr.index().type()));
convert_expr(
typecast_exprt::conditional_cast(element_size_expr, size_target));
out << ')';
}
else if(expr.id() == ID_field_address)
Expand Down Expand Up @@ -5974,7 +5989,8 @@ void smt2_convt::find_symbols(const exprt &expr)
}
else if(expr.id() == ID_element_address)
{
irep_idt function = "element-address-" + type2id(expr.type());
irep_idt function = "element-address-" + type2id(expr.type()) + "_" +
type2id(to_element_address_expr(expr).index().type());
Comment on lines +5992 to +5993

if(state_fkt_declared.insert(function).second)
{
Expand All @@ -5983,7 +5999,17 @@ void smt2_convt::find_symbols(const exprt &expr)
out << ' ';
convert_type(to_element_address_expr(expr).index().type());
out << ' '; // repeat, for the element size
convert_type(to_element_address_expr(expr).index().type());
// The size argument is built as an integer (see convert_expr for
// ID_element_address); for non-integer (e.g. struct-keyed) index types
// we fall back to c_index_type rather than the index type itself.
{
const typet &idx_t = to_element_address_expr(expr).index().type();
const bool int_index =
idx_t.id() == ID_unsignedbv || idx_t.id() == ID_signedbv ||
idx_t.id() == ID_bv || idx_t.id() == ID_integer ||
idx_t.id() == ID_c_enum || idx_t.id() == ID_c_enum_tag;
convert_type(int_index ? idx_t : c_index_type());
}
out << ") ";
convert_type(expr.type()); // return type
out << ")\n"; // declare-fun
Expand Down
Loading