Skip to content

Construct array_exprt in a non-deprecated way [blocks: #3768] #3771

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

Merged
merged 1 commit into from
Jan 21, 2019
+44 −42
Merged

Construct array_exprt in a non-deprecated way [blocks: #3768] #3771

Show file tree
Hide file tree
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
12 changes: 6 additions & 6 deletions jbmc/src/java_bytecode/character_refine_preprocess.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1187,13 +1187,13 @@ exprt character_refine_preprocesst::expr_of_to_chars(
{
array_typet array_type=to_array_type(type);
const typet &char_type=array_type.subtype();
array_exprt case1(array_type);
array_exprt case2(array_type);
exprt low_surrogate=expr_of_low_surrogate(chr, char_type);
case1.copy_to_operands(low_surrogate);
case2.add_to_operands(
std::move(low_surrogate), expr_of_high_surrogate(chr, char_type));
return if_exprt(expr_of_is_bmp_code_point(chr, type), case1, case2);
array_exprt case1({low_surrogate}, array_type);
exprt high_surrogate = expr_of_high_surrogate(chr, char_type);
array_exprt case2(
{std::move(low_surrogate), std::move(high_surrogate)}, array_type);
return if_exprt(
expr_of_is_bmp_code_point(chr, type), std::move(case1), std::move(case2));
}

/// Converts function call to an assignment of an expression corresponding to
Expand Down
7 changes: 4 additions & 3 deletions jbmc/src/java_bytecode/java_bytecode_parser.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1614,13 +1614,14 @@ exprt java_bytecode_parsert::get_relement_value()

case '[':
{
array_exprt values;
u2 num_values=read_u2();
exprt::operandst values;
values.reserve(num_values);
for(std::size_t i=0; i<num_values; i++)
{
values.operands().push_back(get_relement_value());
values.push_back(get_relement_value());
}
return std::move(values);
return array_exprt(std::move(values), array_typet(typet(), exprt()));
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not sure about this one -- somehow an empty array with a correct type (seen many times below) seems considerably safer than this partially-constructed thing. If we're going to partially construct something, we should probably use a constructor with that express purpose, rather than pretending we're doing it safely?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The language front-ends will always remain a bit weird. I'm not sure what the best option is - we could also do exprt values(ID_array); to make very clear we are not building anything like a complete expression here.

}

case 's':
Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/java_string_literals.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ static array_exprt utf16_to_array(const std::wstring &in)
{
const auto jchar=java_char_type();
array_exprt ret(
array_typet(jchar, from_integer(in.length(), java_int_type())));
{}, array_typet(jchar, from_integer(in.length(), java_int_type())));
for(const auto c : in)
ret.copy_to_operands(from_integer(c, jchar));
return ret;
Expand Down
2 changes: 1 addition & 1 deletion jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ constant_exprt from_integer(const mp_integer &i)
array_string_exprt make_string_exprt(const std::string &str)
{
const constant_exprt length=from_integer(str.length(), t.length_type());
array_exprt content(array_typet(t.char_type(), length));
array_exprt content({}, array_typet(t.char_type(), length));

for(const char c : str)
content.copy_to_operands(from_integer(c, t.char_type()));
Expand Down
4 changes: 2 additions & 2 deletions src/goto-programs/interpreter.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -487,7 +487,7 @@ exprt interpretert::get_value(
else if(real_type.id()==ID_array)
{
// Get size of array
array_exprt result(to_array_type(real_type));
array_exprt result({}, to_array_type(real_type));
const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
mp_integer subtype_size=get_size(type.subtype());
mp_integer count;
Expand Down Expand Up @@ -551,7 +551,7 @@ exprt interpretert::get_value(
}
else if(real_type.id()==ID_array)
{
array_exprt result(to_array_type(real_type));
array_exprt result({}, to_array_type(real_type));
const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));

// Get size of array
Expand Down
8 changes: 3 additions & 5 deletions src/goto-programs/remove_vector.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,7 +97,7 @@ static void remove_vector(exprt &expr)
const typet subtype=array_type.subtype();
// do component-wise:
// x+y -> vector(x[0]+y[0],x[1]+y[1],...)
array_exprt array_expr(array_type);
array_exprt array_expr({}, array_type);
array_expr.operands().resize(numeric_cast_v<std::size_t>(dimension));

for(std::size_t i=0; i<array_expr.operands().size(); i++)
Expand All @@ -124,7 +124,7 @@ static void remove_vector(exprt &expr)
const typet subtype=array_type.subtype();
// do component-wise:
// -x -> vector(-x[0],-x[1],...)
array_exprt array_expr(array_type);
array_exprt array_expr({}, array_type);
array_expr.operands().resize(numeric_cast_v<std::size_t>(dimension));

for(std::size_t i=0; i<array_expr.operands().size(); i++)
Expand Down Expand Up @@ -153,9 +153,7 @@ static void remove_vector(exprt &expr)
const auto dimension = numeric_cast_v<std::size_t>(array_type.size());
exprt casted_op =
typecast_exprt::conditional_cast(op, array_type.subtype());
array_exprt array_expr(array_type);
array_expr.operands().resize(dimension, op);
expr = array_expr;
expr = array_exprt(exprt::operandst(dimension, casted_op), array_type);
}
}
}
Expand Down
4 changes: 2 additions & 2 deletions src/solvers/lowering/byte_operators.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ static exprt unpack_rec(
const namespacet &ns,
bool unpack_byte_array=false)
{
array_exprt array(
array_exprt array({},
array_typet(unsignedbv_typet(8), from_integer(0, size_type())));

// endianness_mapt should be the point of reference for mapping out
Expand Down Expand Up @@ -240,7 +240,7 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
element_width.has_value() && *element_width >= 1 &&
*element_width % 8 == 0 && to_integer(array_type.size(), num_elements))
{
array_exprt array(array_type);
array_exprt array({}, array_type);

for(mp_integer i=0; i<num_elements; ++i)
{
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/refinement/string_builtin_function.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -102,7 +102,7 @@ static array_string_exprt
make_string(Iter begin, Iter end, const array_typet &array_type)
{
const typet &char_type = array_type.subtype();
array_exprt array_expr(array_type);
array_exprt array_expr({}, array_type);
const auto &insert = std::back_inserter(array_expr.operands());
std::transform(begin, end, insert, [&](const mp_integer &i) {
return from_integer(i, char_type);
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/refinement/string_constraint_generator_float.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -422,7 +422,7 @@ std::pair<exprt, string_constraintst> add_axioms_from_float_scientific_notation(
two_power_e_over_ten_power_d_table.size(),
int_type);
array_exprt conversion_factor_table(
array_typet(float_type, conversion_factor_table_size));
{}, array_typet(float_type, conversion_factor_table_size));
for(const auto &negative : two_power_e_over_ten_power_d_table_negatives)
conversion_factor_table.copy_to_operands(
constant_float(negative, float_spec));
Expand Down
2 changes: 1 addition & 1 deletion src/solvers/refinement/string_refinement_util.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -171,7 +171,7 @@ array_exprt interval_sparse_arrayt::concretize(
{
const array_typet array_type(
default_value.type(), from_integer(size, index_type));
array_exprt array(array_type);
array_exprt array({}, array_type);
array.operands().reserve(size);

auto it = entries.begin();
Expand Down
4 changes: 2 additions & 2 deletions src/util/expr_initializer.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -122,7 +122,7 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
{
// we initialize this with an empty array

array_exprt value(array_type);
array_exprt value({}, array_type);
value.type().id(ID_array);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't see why this is necessary

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We could arguably make the no-operands-constructor non-deprecated. Would that seem better?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So I'm still in two minds about this. I see the following options:

  1. De-deprecate the no-operands-constructor so that such a change isn't necessary. Reduces the amount of noise in this PR.
  2. Require the above syntax. Adds some noise, but has the following advantages: a) smaller API as fewer constructors are provided and b) encouraging efficient bottom-up construction.

Comments would be appreciated.

value.type().set(ID_size, from_integer(0, size_type()));
value.add_source_location()=source_location;
Expand Down Expand Up @@ -157,7 +157,7 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
if(*array_size < 0)
return nil_exprt();

array_exprt value(array_type);
array_exprt value({}, array_type);
value.operands().resize(numeric_cast_v<std::size_t>(*array_size), tmpval);
value.add_source_location()=source_location;
return std::move(value);
Expand Down
2 changes: 1 addition & 1 deletion src/util/simplify_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1540,7 +1540,7 @@ exprt simplify_exprt::bits2expr(

const std::size_t el_size = numeric_cast_v<std::size_t>(*el_size_opt);

array_exprt result(array_type);
array_exprt result({}, array_type);
result.reserve_operands(n_el);

for(std::size_t i=0; i<n_el; ++i)
Expand Down
5 changes: 5 additions & 0 deletions src/util/std_expr.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1765,6 +1765,11 @@ class array_exprt : public multi_ary_exprt
: multi_ary_exprt(ID_array, _type)
{
}

array_exprt(operandst &&_operands, const array_typet &_type)
: multi_ary_exprt(ID_array, std::move(_operands), _type)
{
}
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This could have been a separate first commit

};

/// \brief Cast an exprt to an \ref array_exprt
Expand Down
3 changes: 1 addition & 2 deletions src/util/string_constant.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,8 +35,7 @@ array_exprt string_constantt::to_array_expr() const

exprt size=from_integer(string_size, index_type());

array_exprt dest;
dest.type()=array_typet(char_type, size);
array_exprt dest({}, array_typet(char_type, size));

dest.operands().resize(string_size);

Expand Down
7 changes: 4 additions & 3 deletions unit/pointer-analysis/value_set.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -263,9 +263,10 @@ SCENARIO(

WHEN("We query { &i1, &i2 }[i3]")
{
array_exprt arr(array_typet(int32_ptr, from_integer(2, int32_type)));
arr.copy_to_operands(address_of_exprt(i1.symbol_expr()));
arr.copy_to_operands(address_of_exprt(i2.symbol_expr()));
array_exprt arr(
{address_of_exprt(i1.symbol_expr()),
address_of_exprt(i2.symbol_expr())},
array_typet(int32_ptr, from_integer(2, int32_type)));

index_exprt index_of_arr(arr, i3.symbol_expr());

Expand Down
16 changes: 7 additions & 9 deletions unit/solvers/refinement/array_pool/array_pool.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,15 +43,13 @@ SCENARIO(
WHEN("Looking for the address of the first element of a constant array")
{
const array_typet array_type(char_type, from_integer(3, length_type));
const exprt array = [array_type, char_type]{
array_exprt a(array_type);
a.operands().push_back(from_integer('f', char_type));
a.operands().push_back(from_integer('o', char_type));
a.operands().push_back(from_integer('o', char_type));
return a;
}();
const exprt first_element =
index_exprt(array, from_integer(0, length_type));
const array_exprt array(
{from_integer('f', char_type),
from_integer('o', char_type),
from_integer('o', char_type)},
array_type);
const exprt first_element =
index_exprt(array, from_integer(0, length_type));
const exprt pointer = address_of_exprt(first_element, pointer_type);
const array_string_exprt associated_array =
pool.find(pointer, array_type.size());
Expand Down
4 changes: 2 additions & 2 deletions unit/solvers/refinement/string_refinement/concretize_array.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,9 +48,9 @@ SCENARIO("concretize_array_expression",
const exprt concrete = sparse_array.concretize(7, int_type);

// Assert
array_exprt expected(array_type);
// The expected result is `{ 'x', 'x', 'y', 'y', 'y', 'z', 'z' }`
expected.operands() = {charx, charx, chary, chary, chary, charz, charz};
array_exprt expected(
{charx, charx, chary, chary, chary, charz, charz}, array_type);
to_array_type(expected.type()).size() = from_integer(7, int_type);
REQUIRE(concrete==expected);
}