Optimise byte_update lowering

In the case of updates to a byte array do just a single translation of the
update value to an array of bytes.

Author: tautschnig

src/solvers/lowering/byte_operators.cpp

@@ -628,7 +628,13 @@ static exprt lower_byte_update(
   const namespacet &ns,
   bool negative_offset)
 {
-  assert(src.operands().size()==3);
+  DATA_INVARIANT(
+    src.id() == ID_byte_update_little_endian ||
+    src.id() == ID_byte_update_big_endian,
+    "byte_update with unknown id " + src.id_string());
+
+  const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
+    ? ID_byte_extract_little_endian : ID_byte_extract_big_endian;
 
   mp_integer element_size=
     pointer_offset_size(src.op2().type(), ns);
@@ -657,49 +663,36 @@ static exprt lower_byte_update(
       // byte array?
       if(sub_size==1)
       {
+        byte_extract_exprt byte_extract_expr(
+          extract_opcode,
+          src.op2(),
+          from_integer(0, src.op1().type()),
+          array_typet(subtype, from_integer(element_size, size_type())));
+
+        array_exprt new_value =
+          to_array_expr(lower_byte_extract(byte_extract_expr, ns));
+        CHECK_RETURN(new_value.operands().size() == element_size);
+
         // apply 'array-update-with' element_size times
         exprt result=src.op0();
 
-        for(mp_integer i=0; i<element_size; ++i)
+        std::size_t i = 0;
+        for(const auto &element : new_value.operands())
         {
           exprt i_expr=from_integer(i, ns.follow(src.op1().type()));
-
-          exprt new_value;
-
-          if(i==0 && element_size==1) // bytes?
-          {
-            new_value=src.op2();
-            if(new_value.type()!=subtype)
-              new_value.make_typecast(subtype);
-          }
-          else
-          {
-            byte_extract_exprt byte_extract_expr(
-              src.id()==ID_byte_update_little_endian?
-                ID_byte_extract_little_endian:
-                src.id()==ID_byte_update_big_endian?
-                  ID_byte_extract_big_endian:
-                    throw "unexpected src.id() in lower_byte_update",
-              subtype);
-
-            byte_extract_expr.op()=src.op2();
-            byte_extract_expr.offset()=i_expr;
-
-            new_value=lower_byte_extract(byte_extract_expr, ns);
-          }
+          ++i;
 
           const exprt where = simplify_expr(plus_exprt(src.op1(), i_expr), ns);
 
           // skip elements that wouldn't change
-          if(new_value.id() == ID_index)
+          if(element.id() == ID_index)
           {
-            const index_exprt &index_expr = to_index_expr(new_value);
+            const index_exprt &index_expr = to_index_expr(element);
             if(index_expr.array() == src.op0() && index_expr.index() == where)
               continue;
           }
 
-          with_exprt with_expr(result, where, new_value);
-          with_expr.type()=src.type();
+          with_exprt with_expr(result, where, element);
 
           result.swap(with_expr);
         }
@@ -751,12 +744,6 @@ static exprt lower_byte_update(
             else
               stored_value_offset=minus_exprt(cell_offset, src.op1());
 
-            auto extract_opcode=
-              src.id()==ID_byte_update_little_endian ?
-              ID_byte_extract_little_endian :
-              src.id()==ID_byte_update_big_endian ?
-              ID_byte_extract_big_endian :
-              throw "unexpected src.id() in lower_byte_update";
             byte_extract_exprt byte_extract_expr(
               extract_opcode,
               element_size<sub_size ? src.op2().type() : subtype);