Skip to content

Commit 22ae7aa

Browse files
kroeningkroening
authored
Merge pull request #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‎

Lines changed: 41 additions & 0 deletions
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‎

Lines changed: 11 additions & 0 deletions
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‎

Lines changed: 23 additions & 0 deletions
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‎

Lines changed: 8 additions & 0 deletions
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‎

Lines changed: 1 addition & 2 deletions
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‎

Lines changed: 107 additions & 0 deletions
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‎

Lines changed: 1 addition & 0 deletions
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‎

Lines changed: 2 additions & 0 deletions
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‎

Lines changed: 1 addition & 0 deletions
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‎

Lines changed: 41 additions & 0 deletions
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+
}

0 commit comments

Comments
 (0)