Implement bswap in SAT back-end

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$

regression/cbmc/inet_endian1/main.c

@@ -0,0 +1,23 @@
+#ifndef _WIN32
+#include <arpa/inet.h>
+#include <assert.h>
+
+int main()
+{
+  uint32_t l;
+  assert(l == ntohl(htonl(l)));
+
+  uint16_t s;
+  assert(s == ntohs(htons(s)));
+
+  return 0;
+}
+
+#else
+
+int main()
+{
+  return 0;
+}
+
+#endif

regression/cbmc/inet_endian1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/ansi-c/c_typecheck_expr.cpp

@@ -2182,8 +2182,7 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
-    exprt bswap_expr(ID_bswap, expr.type());
-    bswap_expr.operands()=expr.arguments();
+    bswap_exprt bswap_expr(expr.arguments().front(), expr.type());
     bswap_expr.add_source_location()=source_location;
 
     return bswap_expr;

src/ansi-c/library/inet.c

@@ -1,6 +1,11 @@
 /* FUNCTION: inet_addr */
 
+#ifndef _WIN32
+
+#ifndef __CPROVER_INET_H_INCLUDED
 #include <arpa/inet.h>
+#define __CPROVER_INET_H_INCLUDED
+#endif
 
 in_addr_t __VERIFIER_nondet_in_addr_t();
 
@@ -16,8 +21,17 @@ in_addr_t inet_addr(const char *cp)
   return result;
 }
 
+#endif
+
 /* FUNCTION: inet_aton */
 
+#ifndef _WIN32
+
+#ifndef __CPROVER_INET_H_INCLUDED
+#include <arpa/inet.h>
+#define __CPROVER_INET_H_INCLUDED
+#endif
+
 int __VERIFIER_nondet_int();
 
 int inet_aton(const char *cp, struct in_addr *pin)
@@ -33,8 +47,17 @@ int inet_aton(const char *cp, struct in_addr *pin)
   return result;
 }
 
+#endif
+
 /* FUNCTION: inet_network */
 
+#ifndef _WIN32
+
+#ifndef __CPROVER_INET_H_INCLUDED
+#include <arpa/inet.h>
+#define __CPROVER_INET_H_INCLUDED
+#endif
+
 in_addr_t __VERIFIER_nondet_in_addr_t();
 
 in_addr_t inet_network(const char *cp)
@@ -48,3 +71,87 @@ in_addr_t inet_network(const char *cp)
   in_addr_t result=__VERIFIER_nondet_in_addr_t();
   return result;
 }
+
+#endif
+
+/* FUNCTION: htonl */
+
+#ifndef __CPROVER_STDINT_H_INCLUDED
+#include <stdint.h>
+#define __CPROVER_STDINT_H_INCLUDED
+#endif
+
+#undef htonl
+
+uint32_t __builtin_bswap32(uint32_t);
+
+uint32_t htonl(uint32_t hostlong)
+{
+#if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
+  return __builtin_bswap32(hostlong);
+#else
+  return hostlong;
+#endif
+}
+
+/* FUNCTION: htons */
+
+#ifndef __CPROVER_STDINT_H_INCLUDED
+#include <stdint.h>
+#define __CPROVER_STDINT_H_INCLUDED
+#endif
+
+#undef htons
+
+uint16_t __builtin_bswap16(uint16_t);
+
+uint16_t htons(uint16_t hostshort)
+{
+#if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
+  return __builtin_bswap16(hostshort);
+#else
+  return hostlong;
+#endif
+}
+
+
+/* FUNCTION: ntohl */
+
+#ifndef __CPROVER_STDINT_H_INCLUDED
+#include <stdint.h>
+#define __CPROVER_STDINT_H_INCLUDED
+#endif
+
+#undef ntohl
+
+uint32_t __builtin_bswap32(uint32_t);
+
+uint32_t ntohl(uint32_t netlong)
+{
+#if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
+  return __builtin_bswap32(netlong);
+#else
+  return netlong;
+#endif
+}
+
+
+/* FUNCTION: ntohs */
+
+#ifndef __CPROVER_STDINT_H_INCLUDED
+#include <stdint.h>
+#define __CPROVER_STDINT_H_INCLUDED
+#endif
+
+#undef ntohs
+
+uint16_t __builtin_bswap16(uint16_t);
+
+uint16_t ntohs(uint16_t netshort)
+{
+#if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
+  return __builtin_bswap16(netshort);
+#else
+  return netshort;
+#endif
+}

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

src/util/simplify_expr.cpp

@@ -2322,8 +2322,8 @@ bool simplify_exprt::simplify_node(exprt &expr)
   else if(expr.id()==ID_ieee_float_equal ||
           expr.id()==ID_ieee_float_notequal)
     result=simplify_ieee_float_relation(expr) && result;
-  else if(expr.id()==ID_bswap)
-    result=simplify_bswap(expr) && result;
+  else if(expr.id() == ID_bswap)
+    result = simplify_bswap(to_bswap_expr(expr)) && result;
   else if(expr.id()==ID_isinf)
     result=simplify_isinf(expr) && result;
   else if(expr.id()==ID_isnan)

src/util/simplify_expr_class.h

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include "mp_arith.h"
 #include "replace_expr.h"
 
+class bswap_exprt;
 class byte_extract_exprt;
 class byte_update_exprt;
 class exprt;
@@ -100,7 +101,7 @@ class simplify_exprt
   bool simplify_dereference(exprt &expr);
   bool simplify_address_of(exprt &expr);
   bool simplify_pointer_offset(exprt &expr);
-  bool simplify_bswap(exprt &expr);
+  bool simplify_bswap(bswap_exprt &expr);
   bool simplify_isinf(exprt &expr);
   bool simplify_isnan(exprt &expr);
   bool simplify_isnormal(exprt &expr);

src/util/simplify_expr_int.cpp

@@ -23,16 +23,13 @@ Author: Daniel Kroening, [email protected]
 #include "rational_tools.h"
 #include "ieee_float.h"
 
-bool simplify_exprt::simplify_bswap(exprt &expr)
+bool simplify_exprt::simplify_bswap(bswap_exprt &expr)
 {
-  if(expr.type().id()==ID_unsignedbv &&
-     expr.operands().size()==1 &&
-     expr.op0().type()==expr.type() &&
-     expr.op0().is_constant())
+  if(expr.type().id() == ID_unsignedbv && expr.op().is_constant())
   {
     std::size_t width=to_bitvector_type(expr.type()).get_width();
     mp_integer value;
-    to_integer(expr.op0(), value);
+    to_integer(expr.op(), value);
     std::vector<mp_integer> bytes;
 
     // take apart
@@ -48,7 +45,8 @@ bool simplify_exprt::simplify_bswap(exprt &expr)
       bytes.pop_back();
     }
 
-    expr=from_integer(new_value, expr.type());
+    constant_exprt c = from_integer(new_value, expr.type());
+    expr.swap(c);
     return false;
   }