bswap_exprt now knows how many bits a byte has

Author: kroening

src/ansi-c/c_typecheck_expr.cpp

@@ -2190,7 +2190,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
-    bswap_exprt bswap_expr(expr.arguments().front(), expr.type());
+    // these are hard-wired to 8 bits according to the gcc manual
+    bswap_exprt bswap_expr(expr.arguments().front(), 8, expr.type());
     bswap_expr.add_source_location()=source_location;
 
     return bswap_expr;

src/solvers/flattening/boolbv_bswap.cpp

@@ -8,15 +8,14 @@ Author: Michael Tautschnig
 
 #include "boolbv.h"
 
-#include <util/config.h>
 #include <util/invariant.h>
 
 bvt boolbvt::convert_bswap(const bswap_exprt &expr)
 {
   const std::size_t width = boolbv_width(expr.type());
 
   // width must be multiple of bytes
-  const std::size_t byte_bits = config.ansi_c.char_width;
+  const std::size_t byte_bits = expr.get_bits_per_byte();
   if(width % byte_bits != 0)
     return conversion_failed(expr);
 

src/util/irep_ids.def

@@ -664,6 +664,7 @@ IREP_ID_TWO(overlay_class, java::com.diffblue.OverlayClassImplementation)
 IREP_ID_TWO(overlay_method, java::com.diffblue.OverlayMethodImplementation)
 IREP_ID_TWO(C_annotations, #annotations)
 IREP_ID_ONE(final)
+IREP_ID_ONE(bits_per_byte)
 
 // Projects depending on this code base that wish to extend the list of
 // available ids should provide a file local_irep_ids.h in their source tree and

src/util/simplify_expr_int.cpp

@@ -28,18 +28,19 @@ bool simplify_exprt::simplify_bswap(bswap_exprt &expr)
 {
   if(expr.type().id() == ID_unsignedbv && expr.op().is_constant())
   {
+    auto bits_per_byte = expr.get_bits_per_byte();
     std::size_t width=to_bitvector_type(expr.type()).get_width();
     mp_integer value;
     to_integer(expr.op(), value);
     std::vector<mp_integer> bytes;
 
     // take apart
-    for(std::size_t bit=0; bit<width; bit+=8)
-      bytes.push_back((value >> bit)%256);
+    for(std::size_t bit = 0; bit < width; bit += bits_per_byte)
+      bytes.push_back((value >> bit)%power(2, bits_per_byte));
 
     // put back together, but backwards
     mp_integer new_value=0;
-    for(std::size_t bit=0; bit<width; bit+=8)
+    for(std::size_t bit = 0; bit < width; bit += bits_per_byte)
     {
       assert(!bytes.empty());
       new_value+=bytes.back()<<bit;

src/util/std_expr.h

@@ -506,18 +506,25 @@ inline void validate_expr(const unary_minus_exprt &value)
 class bswap_exprt: public unary_exprt
 {
 public:
-  bswap_exprt(): unary_exprt(ID_bswap)
+  bswap_exprt(const exprt &_op, std::size_t bits_per_byte, const typet &_type)
+    : unary_exprt(ID_bswap, _op, _type)
   {
+    set_bits_per_byte(bits_per_byte);
   }
 
-  bswap_exprt(const exprt &_op, const typet &_type)
-    : unary_exprt(ID_bswap, _op, _type)
+  explicit bswap_exprt(const exprt &_op, std::size_t &_bits_per_byte)
+    : unary_exprt(ID_bswap, _op, _op.type())
   {
   }
 
-  explicit bswap_exprt(const exprt &_op)
-    : unary_exprt(ID_bswap, _op, _op.type())
+  std::size_t get_bits_per_byte() const
+  {
+    return get_size_t(ID_bits_per_byte);
+  }
+
+  void set_bits_per_byte(std::size_t bits_per_byte)
   {
+    set(ID_bits_per_byte, bits_per_byte);
   }
 };