Implement bswap in SAT back-end

Previously only constants were supported via expression simplification.

Author: tautschnig

regression/cbmc/gcc_bswap1/main.c

@@ -0,0 +1,41 @@
+#include <assert.h>
+#include <stdint.h>
+
+#ifndef __GNUC__
+uint16_t __builtin_bswap16(uint16_t);
+uint32_t __builtin_bswap32(uint32_t);
+uint64_t __builtin_bswap64(uint64_t);
+#endif
+
+uint16_t __VERIFIER_nondet_u16();
+uint32_t __VERIFIER_nondet_u32();
+uint64_t __VERIFIER_nondet_u64();
+
+int main()
+{
+  uint16_t sa = 0xabcd;
+  assert(__builtin_bswap16(sa) == 0xcdab);
+  uint16_t sb = __VERIFIER_nondet_u16();
+  sb &= 0xff00;
+  // expected to fail, only MSB guaranteed to be 0
+  assert(__builtin_bswap16(sb) == 0);
+  assert((__builtin_bswap16(sb) & 0xff00) == 0);
+
+  uint32_t a = 0xabcdef00;
+  assert(__builtin_bswap32(a) == 0x00efcdab);
+  uint32_t b = __VERIFIER_nondet_u32();
+  b &= 0xffffff00;
+  // expected to fail, only MSB guaranteed to be 0
+  assert(__builtin_bswap32(b) == 0);
+  assert((__builtin_bswap32(b) & 0xff000000) == 0);
+
+  uint64_t al = 0xabcdef0001020304LL;
+  assert(__builtin_bswap64(al) == 0x0403020100efcdabLL);
+  uint64_t bl = __VERIFIER_nondet_u64();
+  bl &= 0xffffffffffffff00LL;
+  // expected to fail, only MSB guaranteed to be 0
+  assert(__builtin_bswap64(bl) == 0);
+  assert((__builtin_bswap64(bl) & 0xff00000000000000) == 0);
+
+  return 0;
+}

regression/cbmc/gcc_bswap1/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[main\.assertion\.[258]\] assertion __builtin_bswap(16|32|64)\((sb|b|bl)\) == 0: FAILURE$
+^\*\* 3 of 9 failed
+--
+^warning: ignoring
+\[main\.assertion\.[258]\] assertion __builtin_bswap(16|32|64)\((sb|b|bl)\) == 0: SUCCESS$

src/solvers/Makefile

@@ -106,6 +106,7 @@ SRC = $(BOOLEFORCE_SRC) \
       flattening/boolbv_array.cpp \
       flattening/boolbv_array_of.cpp \
       flattening/boolbv_bitwise.cpp \
+      flattening/boolbv_bswap.cpp \
       flattening/boolbv_bv_rel.cpp \
       flattening/boolbv_byte_extract.cpp \
       flattening/boolbv_byte_update.cpp \

src/solvers/flattening/boolbv.cpp

@@ -245,6 +245,8 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
   }
   else if(expr.id()==ID_abs)
     return convert_abs(expr);
+  else if(expr.id() == ID_bswap)
+    return convert_bswap(to_bswap_expr(expr));
   else if(expr.id()==ID_byte_extract_little_endian ||
           expr.id()==ID_byte_extract_big_endian)
     return convert_byte_extract(to_byte_extract_expr(expr));

src/solvers/flattening/boolbv.h

@@ -133,6 +133,7 @@ class boolbvt:public arrayst
 
   virtual bvt convert_index(const exprt &array, const mp_integer &index);
   virtual bvt convert_index(const index_exprt &expr);
+  virtual bvt convert_bswap(const bswap_exprt &expr);
   virtual bvt convert_byte_extract(const byte_extract_exprt &expr);
   virtual bvt convert_byte_update(const byte_update_exprt &expr);
   virtual bvt convert_constraint_select_one(const exprt &expr);

src/solvers/flattening/boolbv_bswap.cpp

@@ -0,0 +1,41 @@
+/*******************************************************************\
+
+Module: Bit-blasting of bswap
+
+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;
+  if(width % byte_bits != 0)
+    return conversion_failed(expr);
+
+  bvt result = convert_bv(expr.op());
+  CHECK_RETURN(result.size() == width);
+
+  std::size_t dest_base = width;
+
+  for(std::size_t src = 0; src < width; ++src)
+  {
+    std::size_t bit_offset = src % byte_bits;
+    if(bit_offset == 0)
+      dest_base -= byte_bits;
+
+    if(src >= dest_base)
+      break;
+
+    result[src].swap(result[dest_base + bit_offset]);
+  }
+
+  return result;
+}