Skip to content

Commit 22ae7aa

Browse files
author
Daniel Kroening
authored
Merge pull request diffblue#1637 from tautschnig/bswap
Implement bswap in SAT back-end
2 parents a1a972f + d16a918 commit 22ae7aa

File tree

14 files changed

+307
-12
lines changed

14 files changed

+307
-12
lines changed

‎regression/cbmc/gcc_bswap1/main.c

+41
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
#include <assert.h>
2+
#include <stdint.h>
3+
4+
#ifndef __GNUC__
5+
uint16_t __builtin_bswap16(uint16_t);
6+
uint32_t __builtin_bswap32(uint32_t);
7+
uint64_t __builtin_bswap64(uint64_t);
8+
#endif
9+
10+
uint16_t __VERIFIER_nondet_u16();
11+
uint32_t __VERIFIER_nondet_u32();
12+
uint64_t __VERIFIER_nondet_u64();
13+
14+
int main()
15+
{
16+
uint16_t sa = 0xabcd;
17+
assert(__builtin_bswap16(sa) == 0xcdab);
18+
uint16_t sb = __VERIFIER_nondet_u16();
19+
sb &= 0xff00;
20+
// expected to fail, only MSB guaranteed to be 0
21+
assert(__builtin_bswap16(sb) == 0);
22+
assert((__builtin_bswap16(sb) & 0xff00) == 0);
23+
24+
uint32_t a = 0xabcdef00;
25+
assert(__builtin_bswap32(a) == 0x00efcdab);
26+
uint32_t b = __VERIFIER_nondet_u32();
27+
b &= 0xffffff00;
28+
// expected to fail, only MSB guaranteed to be 0
29+
assert(__builtin_bswap32(b) == 0);
30+
assert((__builtin_bswap32(b) & 0xff000000) == 0);
31+
32+
uint64_t al = 0xabcdef0001020304LL;
33+
assert(__builtin_bswap64(al) == 0x0403020100efcdabLL);
34+
uint64_t bl = __VERIFIER_nondet_u64();
35+
bl &= 0xffffffffffffff00LL;
36+
// expected to fail, only MSB guaranteed to be 0
37+
assert(__builtin_bswap64(bl) == 0);
38+
assert((__builtin_bswap64(bl) & 0xff00000000000000) == 0);
39+
40+
return 0;
41+
}

‎regression/cbmc/gcc_bswap1/test.desc

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

‎regression/cbmc/inet_endian1/main.c

+23
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
#ifndef _WIN32
2+
#include <arpa/inet.h>
3+
#include <assert.h>
4+
5+
int main()
6+
{
7+
uint32_t l;
8+
assert(l == ntohl(htonl(l)));
9+
10+
uint16_t s;
11+
assert(s == ntohs(htons(s)));
12+
13+
return 0;
14+
}
15+
16+
#else
17+
18+
int main()
19+
{
20+
return 0;
21+
}
22+
23+
#endif

‎regression/cbmc/inet_endian1/test.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎src/ansi-c/c_typecheck_expr.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -2182,8 +2182,7 @@ exprt c_typecheck_baset::do_special_functions(
21822182
throw 0;
21832183
}
21842184

2185-
exprt bswap_expr(ID_bswap, expr.type());
2186-
bswap_expr.operands()=expr.arguments();
2185+
bswap_exprt bswap_expr(expr.arguments().front(), expr.type());
21872186
bswap_expr.add_source_location()=source_location;
21882187

21892188
return bswap_expr;

‎src/ansi-c/library/inet.c

+107
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,11 @@
11
/* FUNCTION: inet_addr */
22

3+
#ifndef _WIN32
4+
5+
#ifndef __CPROVER_INET_H_INCLUDED
36
#include <arpa/inet.h>
7+
#define __CPROVER_INET_H_INCLUDED
8+
#endif
49

510
in_addr_t __VERIFIER_nondet_in_addr_t();
611

@@ -16,8 +21,17 @@ in_addr_t inet_addr(const char *cp)
1621
return result;
1722
}
1823

24+
#endif
25+
1926
/* FUNCTION: inet_aton */
2027

28+
#ifndef _WIN32
29+
30+
#ifndef __CPROVER_INET_H_INCLUDED
31+
#include <arpa/inet.h>
32+
#define __CPROVER_INET_H_INCLUDED
33+
#endif
34+
2135
int __VERIFIER_nondet_int();
2236

2337
int inet_aton(const char *cp, struct in_addr *pin)
@@ -33,8 +47,17 @@ int inet_aton(const char *cp, struct in_addr *pin)
3347
return result;
3448
}
3549

50+
#endif
51+
3652
/* FUNCTION: inet_network */
3753

54+
#ifndef _WIN32
55+
56+
#ifndef __CPROVER_INET_H_INCLUDED
57+
#include <arpa/inet.h>
58+
#define __CPROVER_INET_H_INCLUDED
59+
#endif
60+
3861
in_addr_t __VERIFIER_nondet_in_addr_t();
3962

4063
in_addr_t inet_network(const char *cp)
@@ -48,3 +71,87 @@ in_addr_t inet_network(const char *cp)
4871
in_addr_t result=__VERIFIER_nondet_in_addr_t();
4972
return result;
5073
}
74+
75+
#endif
76+
77+
/* FUNCTION: htonl */
78+
79+
#ifndef __CPROVER_STDINT_H_INCLUDED
80+
#include <stdint.h>
81+
#define __CPROVER_STDINT_H_INCLUDED
82+
#endif
83+
84+
#undef htonl
85+
86+
uint32_t __builtin_bswap32(uint32_t);
87+
88+
uint32_t htonl(uint32_t hostlong)
89+
{
90+
#if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
91+
return __builtin_bswap32(hostlong);
92+
#else
93+
return hostlong;
94+
#endif
95+
}
96+
97+
/* FUNCTION: htons */
98+
99+
#ifndef __CPROVER_STDINT_H_INCLUDED
100+
#include <stdint.h>
101+
#define __CPROVER_STDINT_H_INCLUDED
102+
#endif
103+
104+
#undef htons
105+
106+
uint16_t __builtin_bswap16(uint16_t);
107+
108+
uint16_t htons(uint16_t hostshort)
109+
{
110+
#if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
111+
return __builtin_bswap16(hostshort);
112+
#else
113+
return hostlong;
114+
#endif
115+
}
116+
117+
118+
/* FUNCTION: ntohl */
119+
120+
#ifndef __CPROVER_STDINT_H_INCLUDED
121+
#include <stdint.h>
122+
#define __CPROVER_STDINT_H_INCLUDED
123+
#endif
124+
125+
#undef ntohl
126+
127+
uint32_t __builtin_bswap32(uint32_t);
128+
129+
uint32_t ntohl(uint32_t netlong)
130+
{
131+
#if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
132+
return __builtin_bswap32(netlong);
133+
#else
134+
return netlong;
135+
#endif
136+
}
137+
138+
139+
/* FUNCTION: ntohs */
140+
141+
#ifndef __CPROVER_STDINT_H_INCLUDED
142+
#include <stdint.h>
143+
#define __CPROVER_STDINT_H_INCLUDED
144+
#endif
145+
146+
#undef ntohs
147+
148+
uint16_t __builtin_bswap16(uint16_t);
149+
150+
uint16_t ntohs(uint16_t netshort)
151+
{
152+
#if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
153+
return __builtin_bswap16(netshort);
154+
#else
155+
return netshort;
156+
#endif
157+
}

‎src/solvers/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -106,6 +106,7 @@ SRC = $(BOOLEFORCE_SRC) \
106106
flattening/boolbv_array.cpp \
107107
flattening/boolbv_array_of.cpp \
108108
flattening/boolbv_bitwise.cpp \
109+
flattening/boolbv_bswap.cpp \
109110
flattening/boolbv_bv_rel.cpp \
110111
flattening/boolbv_byte_extract.cpp \
111112
flattening/boolbv_byte_update.cpp \

‎src/solvers/flattening/boolbv.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -245,6 +245,8 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
245245
}
246246
else if(expr.id()==ID_abs)
247247
return convert_abs(expr);
248+
else if(expr.id() == ID_bswap)
249+
return convert_bswap(to_bswap_expr(expr));
248250
else if(expr.id()==ID_byte_extract_little_endian ||
249251
expr.id()==ID_byte_extract_big_endian)
250252
return convert_byte_extract(to_byte_extract_expr(expr));

‎src/solvers/flattening/boolbv.h

+1
Original file line numberDiff line numberDiff line change
@@ -133,6 +133,7 @@ class boolbvt:public arrayst
133133

134134
virtual bvt convert_index(const exprt &array, const mp_integer &index);
135135
virtual bvt convert_index(const index_exprt &expr);
136+
virtual bvt convert_bswap(const bswap_exprt &expr);
136137
virtual bvt convert_byte_extract(const byte_extract_exprt &expr);
137138
virtual bvt convert_byte_update(const byte_update_exprt &expr);
138139
virtual bvt convert_constraint_select_one(const exprt &expr);

‎src/solvers/flattening/boolbv_bswap.cpp

+41
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
/*******************************************************************\
2+
3+
Module: Bit-blasting of bswap
4+
5+
Author: Michael Tautschnig
6+
7+
\*******************************************************************/
8+
9+
#include "boolbv.h"
10+
11+
#include <util/config.h>
12+
#include <util/invariant.h>
13+
14+
bvt boolbvt::convert_bswap(const bswap_exprt &expr)
15+
{
16+
const std::size_t width = boolbv_width(expr.type());
17+
18+
// width must be multiple of bytes
19+
const std::size_t byte_bits = config.ansi_c.char_width;
20+
if(width % byte_bits != 0)
21+
return conversion_failed(expr);
22+
23+
bvt result = convert_bv(expr.op());
24+
CHECK_RETURN(result.size() == width);
25+
26+
std::size_t dest_base = width;
27+
28+
for(std::size_t src = 0; src < width; ++src)
29+
{
30+
std::size_t bit_offset = src % byte_bits;
31+
if(bit_offset == 0)
32+
dest_base -= byte_bits;
33+
34+
if(src >= dest_base)
35+
break;
36+
37+
result[src].swap(result[dest_base + bit_offset]);
38+
}
39+
40+
return result;
41+
}

‎src/util/simplify_expr.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -2322,8 +2322,8 @@ bool simplify_exprt::simplify_node(exprt &expr)
23222322
else if(expr.id()==ID_ieee_float_equal ||
23232323
expr.id()==ID_ieee_float_notequal)
23242324
result=simplify_ieee_float_relation(expr) && result;
2325-
else if(expr.id()==ID_bswap)
2326-
result=simplify_bswap(expr) && result;
2325+
else if(expr.id() == ID_bswap)
2326+
result = simplify_bswap(to_bswap_expr(expr)) && result;
23272327
else if(expr.id()==ID_isinf)
23282328
result=simplify_isinf(expr) && result;
23292329
else if(expr.id()==ID_isnan)

‎src/util/simplify_expr_class.h

+2-1
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
2121
#include "mp_arith.h"
2222
#include "replace_expr.h"
2323

24+
class bswap_exprt;
2425
class byte_extract_exprt;
2526
class byte_update_exprt;
2627
class exprt;
@@ -100,7 +101,7 @@ class simplify_exprt
100101
bool simplify_dereference(exprt &expr);
101102
bool simplify_address_of(exprt &expr);
102103
bool simplify_pointer_offset(exprt &expr);
103-
bool simplify_bswap(exprt &expr);
104+
bool simplify_bswap(bswap_exprt &expr);
104105
bool simplify_isinf(exprt &expr);
105106
bool simplify_isnan(exprt &expr);
106107
bool simplify_isnormal(exprt &expr);

‎src/util/simplify_expr_int.cpp

+5-7
Original file line numberDiff line numberDiff line change
@@ -23,16 +23,13 @@ Author: Daniel Kroening, [email protected]
2323
#include "rational_tools.h"
2424
#include "ieee_float.h"
2525

26-
bool simplify_exprt::simplify_bswap(exprt &expr)
26+
bool simplify_exprt::simplify_bswap(bswap_exprt &expr)
2727
{
28-
if(expr.type().id()==ID_unsignedbv &&
29-
expr.operands().size()==1 &&
30-
expr.op0().type()==expr.type() &&
31-
expr.op0().is_constant())
28+
if(expr.type().id() == ID_unsignedbv && expr.op().is_constant())
3229
{
3330
std::size_t width=to_bitvector_type(expr.type()).get_width();
3431
mp_integer value;
35-
to_integer(expr.op0(), value);
32+
to_integer(expr.op(), value);
3633
std::vector<mp_integer> bytes;
3734

3835
// take apart
@@ -48,7 +45,8 @@ bool simplify_exprt::simplify_bswap(exprt &expr)
4845
bytes.pop_back();
4946
}
5047

51-
expr=from_integer(new_value, expr.type());
48+
constant_exprt c = from_integer(new_value, expr.type());
49+
expr.swap(c);
5250
return false;
5351
}
5452

0 commit comments

Comments
 (0)