bv_typet is also sensitive to endianness

The bits within an object of bv_typet are ordered depending on
endianness. This is consistent with typecasts to/from bv_typet of some
other bitvector type, which do not alter the sequence of bits.

Author: tautschnig

src/solvers/lowering/byte_operators.cpp

@@ -50,10 +50,7 @@ static boundst map_bounds(
 
     // big-endian bounds need swapping
     if(result.ub < result.lb)
-    {
-      result.lb = endianness_map.number_of_bits() - result.lb - 1;
-      result.ub = endianness_map.number_of_bits() - result.ub - 1;
-    }
+      std::swap(result.lb, result.ub);
   }
 
   return result;
@@ -1295,7 +1292,7 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
     concatenation_exprt concatenation(
       std::move(op), bitvector_typet(subtype->id(), width_bytes * 8));
 
-    endianness_mapt map(src.type(), little_endian, ns);
+    endianness_mapt map(concatenation.type(), little_endian, ns);
     return bv_to_expr(concatenation, src.type(), map, ns);
   }
 }
@@ -2226,22 +2223,16 @@ static exprt lower_byte_update(
     // original_bits |= newvalue
     bitor_exprt bitor_expr{bitand_expr, value_shifted};
 
-    if(!is_little_endian && bit_width > type_bits)
-    {
-      return simplify_expr(
-        typecast_exprt::conditional_cast(
-          extractbits_exprt{bitor_expr,
-                            bit_width - 1,
-                            bit_width - type_bits,
-                            bv_typet{type_bits}},
-          src.type()),
-        ns);
-    }
-    else if(bit_width > type_bits)
+    if(bit_width > type_bits)
     {
+      endianness_mapt endianness_map(
+        bitor_expr.type(), src.id() == ID_byte_update_little_endian, ns);
+      const auto bounds = map_bounds(endianness_map, 0, type_bits - 1);
+
       return simplify_expr(
         typecast_exprt::conditional_cast(
-          extractbits_exprt{bitor_expr, type_bits - 1, 0, bv_typet{type_bits}},
+          extractbits_exprt{
+            bitor_expr, bounds.ub, bounds.lb, bv_typet{type_bits}},
           src.type()),
         ns);
     }

src/util/endianness_map.cpp

@@ -53,12 +53,10 @@ void endianness_mapt::build_big_endian(const typet &src)
 {
   if(src.id() == ID_c_enum_tag)
     build_big_endian(ns.follow_tag(to_c_enum_tag_type(src)));
-  else if(src.id()==ID_unsignedbv ||
-          src.id()==ID_signedbv ||
-          src.id()==ID_fixedbv ||
-          src.id()==ID_floatbv ||
-          src.id()==ID_c_enum ||
-          src.id()==ID_c_bit_field)
+  else if(
+    src.id() == ID_unsignedbv || src.id() == ID_signedbv ||
+    src.id() == ID_fixedbv || src.id() == ID_floatbv || src.id() == ID_c_enum ||
+    src.id() == ID_c_bit_field || src.id() == ID_bv)
   {
     // these do get re-ordered!
     auto bits = pointer_offset_bits(src, ns); // error is -1