From 4f37035b679b41881c12369197a643ddd42dabd6 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 29 Nov 2017 11:07:36 +0000 Subject: [PATCH 1/3] Introduce bswap_exprt ID_bswap was previously used without a dedicated class. --- src/ansi-c/c_typecheck_expr.cpp | 3 +- src/util/simplify_expr.cpp | 4 +-- src/util/simplify_expr_class.h | 3 +- src/util/simplify_expr_int.cpp | 12 +++---- src/util/std_expr.h | 62 +++++++++++++++++++++++++++++++++ 5 files changed, 72 insertions(+), 12 deletions(-) diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 6fe03a3cfa0..57a55a27c89 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/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; diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index ab747030d60..71a3140d99a 100644 --- a/src/util/simplify_expr.cpp +++ b/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) diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index 3aa34492cb5..05b963934d3 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com #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); diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 4d065f6d49b..f296e02d81f 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -23,16 +23,13 @@ Author: Daniel Kroening, kroening@kroening.com #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 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; } diff --git a/src/util/std_expr.h b/src/util/std_expr.h index f148723f3b5..dd132f38faf 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -505,6 +505,68 @@ inline void validate_expr(const unary_minus_exprt &value) validate_operands(value, 1, "Unary minus must have one operand"); } +/*! \brief The byte swap expression +*/ +class bswap_exprt: public unary_exprt +{ +public: + bswap_exprt(): unary_exprt(ID_bswap) + { + } + + bswap_exprt(const exprt &_op, const typet &_type) + : unary_exprt(ID_bswap, _op, _type) + { + } + + explicit bswap_exprt(const exprt &_op) + : unary_exprt(ID_bswap, _op, _op.type()) + { + } +}; + +/*! \brief Cast a generic exprt to a \ref bswap_exprt + * + * This is an unchecked conversion. \a expr must be known to be \ref + * bswap_exprt. + * + * \param expr Source expression + * \return Object of type \ref bswap_exprt + * + * \ingroup gr_std_expr +*/ +inline const bswap_exprt &to_bswap_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_bswap); + DATA_INVARIANT(expr.operands().size() == 1, "bswap must have one operand"); + DATA_INVARIANT( + expr.op0().type() == expr.type(), "bswap type must match operand type"); + return static_cast(expr); +} + +/*! \copydoc to_bswap_expr(const exprt &) + * \ingroup gr_std_expr +*/ +inline bswap_exprt &to_bswap_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_bswap); + DATA_INVARIANT(expr.operands().size() == 1, "bswap must have one operand"); + DATA_INVARIANT( + expr.op0().type() == expr.type(), "bswap type must match operand type"); + return static_cast(expr); +} + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return base.id() == ID_bswap; +} +inline void validate_expr(const bswap_exprt &value) +{ + validate_operands(value, 1, "bswap must have one operand"); + DATA_INVARIANT( + value.op().type() == value.type(), "bswap type must match operand type"); +} /*! \brief A generic base class for expressions that are predicates, i.e., boolean-typed. From 05bc9ed9f0ea32043605fb115abc92073ef0dd88 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 28 Nov 2017 19:09:33 +0000 Subject: [PATCH 2/3] Implement bswap in SAT back-end Previously only constants were supported via expression simplification. --- regression/cbmc/gcc_bswap1/main.c | 41 +++++++++++++++++++++++++ regression/cbmc/gcc_bswap1/test.desc | 11 +++++++ src/solvers/Makefile | 1 + src/solvers/flattening/boolbv.cpp | 2 ++ src/solvers/flattening/boolbv.h | 1 + src/solvers/flattening/boolbv_bswap.cpp | 41 +++++++++++++++++++++++++ 6 files changed, 97 insertions(+) create mode 100644 regression/cbmc/gcc_bswap1/main.c create mode 100644 regression/cbmc/gcc_bswap1/test.desc create mode 100644 src/solvers/flattening/boolbv_bswap.cpp diff --git a/regression/cbmc/gcc_bswap1/main.c b/regression/cbmc/gcc_bswap1/main.c new file mode 100644 index 00000000000..a016604d2d2 --- /dev/null +++ b/regression/cbmc/gcc_bswap1/main.c @@ -0,0 +1,41 @@ +#include +#include + +#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; +} diff --git a/regression/cbmc/gcc_bswap1/test.desc b/regression/cbmc/gcc_bswap1/test.desc new file mode 100644 index 00000000000..816eb3a838b --- /dev/null +++ b/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$ diff --git a/src/solvers/Makefile b/src/solvers/Makefile index c8cbebee1a6..f1484b6b695 100644 --- a/src/solvers/Makefile +++ b/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 \ diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 238ff04ddfa..1f67010402d 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/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)); diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index f015e96097b..585bbdfeca6 100644 --- a/src/solvers/flattening/boolbv.h +++ b/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); diff --git a/src/solvers/flattening/boolbv_bswap.cpp b/src/solvers/flattening/boolbv_bswap.cpp new file mode 100644 index 00000000000..db3444a089d --- /dev/null +++ b/src/solvers/flattening/boolbv_bswap.cpp @@ -0,0 +1,41 @@ +/*******************************************************************\ + +Module: Bit-blasting of bswap + +Author: Michael Tautschnig + +\*******************************************************************/ + +#include "boolbv.h" + +#include +#include + +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; +} From d16a91821dc529f78689c5d1e45bbcf1779de27d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 10 Jan 2018 08:37:06 +0000 Subject: [PATCH 3/3] C library: network byteorder functions On some systems htonl etc. are just macros (always true for big-endian systems, where they are null macros; and also true on Mac OS). For others we to provide the implementation. In all cases the full support for bswap* is necessary, and that is now available as of the preceding commit. Also fixes arpa/inet.h being unavailable on Windows/Visual Studio. --- regression/cbmc/inet_endian1/main.c | 23 ++++++ regression/cbmc/inet_endian1/test.desc | 8 ++ src/ansi-c/library/inet.c | 107 +++++++++++++++++++++++++ 3 files changed, 138 insertions(+) create mode 100644 regression/cbmc/inet_endian1/main.c create mode 100644 regression/cbmc/inet_endian1/test.desc diff --git a/regression/cbmc/inet_endian1/main.c b/regression/cbmc/inet_endian1/main.c new file mode 100644 index 00000000000..4178ecff4a8 --- /dev/null +++ b/regression/cbmc/inet_endian1/main.c @@ -0,0 +1,23 @@ +#ifndef _WIN32 +#include +#include + +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 diff --git a/regression/cbmc/inet_endian1/test.desc b/regression/cbmc/inet_endian1/test.desc new file mode 100644 index 00000000000..9efefbc7362 --- /dev/null +++ b/regression/cbmc/inet_endian1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/ansi-c/library/inet.c b/src/ansi-c/library/inet.c index 88a508cc47f..9a208babb88 100644 --- a/src/ansi-c/library/inet.c +++ b/src/ansi-c/library/inet.c @@ -1,6 +1,11 @@ /* FUNCTION: inet_addr */ +#ifndef _WIN32 + +#ifndef __CPROVER_INET_H_INCLUDED #include +#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 +#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 +#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 +#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 +#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 +#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 +#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 +}