Merge pull request #2246 from diffblue/z3-fpa

smt2: bswap and popcount

Author: Daniel Kroening

src/ansi-c/c_typecheck_expr.cpp

@@ -2186,7 +2186,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/solvers/smt2/smt2_conv.cpp

@@ -29,9 +29,10 @@ Author: Daniel Kroening, [email protected]
 #include <util/string_constant.h>
 
 #include <solvers/flattening/boolbv_width.h>
-#include <solvers/flattening/flatten_byte_operators.h>
 #include <solvers/flattening/c_bit_field_replacement_type.h>
+#include <solvers/flattening/flatten_byte_operators.h>
 #include <solvers/floatbv/float_bv.h>
+#include <solvers/lowering/expr_lowering.h>
 
 // Mark different kinds of error condition
 // General
@@ -1809,6 +1810,68 @@ void smt2_convt::convert_expr(const exprt &expr)
       "smt2_convt::convert_expr: `"+expr.id_string()+
       "' is not yet supported");
   }
+  else if(expr.id() == ID_bswap)
+  {
+    if(expr.operands().size() != 1)
+      INVALIDEXPR("bswap gets one operand");
+
+    if(expr.op0().type() != expr.type())
+      INVALIDEXPR("bswap gets one operand with same type");
+
+    // first 'let' the operand
+    out << "(let ((bswap_op ";
+    convert_expr(expr.op0());
+    out << ")) ";
+
+    if(expr.type().id() == ID_signedbv || expr.type().id() == ID_unsignedbv)
+    {
+      const std::size_t width = to_bitvector_type(expr.type()).get_width();
+
+      // width must be multiple of bytes
+      if(width % 8 != 0)
+        INVALIDEXPR("bswap must get bytes");
+
+      const std::size_t bytes = width / 8;
+
+      if(bytes <= 1)
+        out << "bswap_op";
+      else
+      {
+        // do a parallel 'let' for each byte
+        out << "(let (";
+
+        for(std::size_t byte = 0; byte < bytes; byte++)
+        {
+          if(byte != 0)
+            out << ' ';
+          out << "(bswap_byte_" << byte << ' ';
+          out << "((_ extract " << (byte * 8 + 7) << " " << (byte * 8)
+              << ") bswap_op)";
+          out << ')';
+        }
+
+        out << ") ";
+
+        // now stitch back together with 'concat'
+        out << "(concat";
+
+        for(std::size_t byte = 0; byte < bytes; byte++)
+          out << " bswap_byte_" << byte;
+
+        out << ')'; // concat
+        out << ')'; // let bswap_byte_*
+      }
+    }
+    else
+      UNEXPECTEDCASE("bswap must get bitvector operand");
+
+    out << ')'; // let bswap_op
+  }
+  else if(expr.id() == ID_popcount)
+  {
+    exprt lowered = lower_popcount(to_popcount_expr(expr), ns);
+    convert_expr(lowered);
+  }
   else
     UNEXPECTEDCASE(
       "smt2_convt::convert_expr: `"+expr.id_string()+"' is unsupported");

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