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

@@ -657,49 +657,40 @@ static exprt lower_byte_update(
       // byte array?
       if(sub_size==1)
       {
+        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",
+          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);
         }