Merge pull request #3771 from tautschnig/deprecation-array_exprt

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

Author: tautschnig

jbmc/src/java_bytecode/character_refine_preprocess.cpp

@@ -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

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -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()));
     }
 
   case 's':

jbmc/src/java_bytecode/java_string_literals.cpp

@@ -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;

jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -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()));

src/goto-programs/interpreter.cpp

@@ -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;
@@ -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

src/goto-programs/remove_vector.cpp

@@ -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++)
@@ -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++)
@@ -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);
       }
     }
   }

src/solvers/lowering/byte_operators.cpp

@@ -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
@@ -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)
       {

src/solvers/refinement/string_builtin_function.cpp

@@ -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);

src/solvers/refinement/string_constraint_generator_float.cpp

@@ -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));

src/solvers/refinement/string_refinement_util.cpp

@@ -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();

src/util/expr_initializer.cpp

@@ -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);
       value.type().set(ID_size, from_integer(0, size_type()));
       value.add_source_location()=source_location;
@@ -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);

src/util/simplify_expr.cpp

@@ -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)

src/util/std_expr.h

@@ -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)
+  {
+  }
 };
 
 /// \brief Cast an exprt to an \ref array_exprt

src/util/string_constant.cpp

@@ -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);
 

unit/pointer-analysis/value_set.cpp

@@ -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());
 

unit/solvers/refinement/array_pool/array_pool.cpp

@@ -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());

unit/solvers/refinement/string_refinement/concretize_array.cpp

@@ -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);
 }