Skip to content

Commit 69f5f2d

Browse files
belous-dpbelous-dp
authored
bit fields support added (#383)
* refactored klee constraints printing * changed all types sizes from bytes to bits * bit fields basic support added * fixed link to utbot * bit fields examples added * fixed unnamed bit fields klee wrapper generation & tests generation * unit tests added
1 parent 14e599c commit 69f5f2d

27 files changed

+1606
-397
lines changed

‎integration-tests/c-example/lib/structures/bitfields.c

+148
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,148 @@
1+
#include "bitfields.h"
2+
#include <assert.h>
3+
#include <limits.h>
4+
#include <stddef.h>
5+
#include <stdio.h>
6+
#include <stdlib.h>
7+
8+
static int ALIGN = -30;
9+
10+
#define print_sizeof(S) printf("size of %*s : %zu bytes\n", ALIGN, #S, sizeof((S){}))
11+
12+
void print_sizeof_structs() {
13+
print_sizeof(SimpleSignedStr);
14+
print_sizeof(SimpleUnsignedStr);
15+
print_sizeof(ImplementationDefinedStr);
16+
print_sizeof(PossiblySmallStr);
17+
print_sizeof(SimpleUnsignedUnion);
18+
print_sizeof(ComplexStr);
19+
print_sizeof(StrWithBool);
20+
print_sizeof(StrWithUnnamedBitfields);
21+
print_sizeof(StrWithUnnamedZeroBitfield);
22+
print_sizeof(StrWithBreak);
23+
}
24+
25+
int check_simple_signed_str(SimpleSignedStr s) {
26+
if (s.a == 1024 && s.b == -1 && s.d == -16) {
27+
return 1;
28+
} else if (s.b == 0) {
29+
return -1;
30+
}
31+
return 0;
32+
}
33+
34+
int is_sum_greater_10(SimpleUnsignedStr s) {
35+
return (s.a + s.b + s.c + s.d > 10 && s.d > 5);
36+
}
37+
38+
int is_all_greater_2(PossiblySmallStr s) {
39+
if (s.a > 2 && s.b > 2) {
40+
return 1;
41+
}
42+
return 0;
43+
}
44+
45+
int union_greater_2(SimpleUnsignedUnion u) {
46+
if (u.c > 2) {
47+
return 1;
48+
}
49+
return 0;
50+
}
51+
52+
int union_greater_2_short(SimpleUnsignedUnion u) {
53+
return u.c > 2;
54+
}
55+
56+
int sum_of_fields(ComplexStr s) {
57+
if (!s.a) {
58+
return -1;
59+
}
60+
return s.a + s.b + s.c + s.d + s.e;
61+
}
62+
63+
int decode_from_bool(StrWithBool s) {
64+
if (!s.a && !s.b && !s.c) {
65+
return 0;
66+
} else if (s.a && !s.b && !s.c) {
67+
return 1;
68+
} else if (!s.a && s.b && !s.c) {
69+
return 2;
70+
} else if (s.a && s.b && !s.c) {
71+
return 3;
72+
} else if (!s.a && !s.b && s.c) {
73+
return 4;
74+
} else if (s.a && !s.b && s.c) {
75+
return 5;
76+
} else if (!s.a && s.b && s.c) {
77+
return 6;
78+
}
79+
return 7;
80+
}
81+
82+
int decode_from_bool_simple(StrWithBool s) {
83+
if (!s.a && !s.b && !s.c) {
84+
return 0;
85+
} else if (s.a && !s.b && s.c) {
86+
return 5;
87+
}
88+
return 7;
89+
}
90+
91+
StrWithUnnamedBitfields mult_by_two(StrWithUnnamedBitfields s) {
92+
s.b1 *= 2;
93+
s.b2 *= 2;
94+
s.b3 *= 2;
95+
return s;
96+
}
97+
98+
int is_nice(StrWithUnnamedZeroBitfield s) {
99+
if (s.b1 == 69 && s.b2 == 42 && s.b3 == 1488) {
100+
return 13;
101+
}
102+
return 0;
103+
}
104+
105+
int check_fields_bounds(StrWithBreak s) {
106+
assert(s.b1 >= 0 && s.b1 <= 127);
107+
assert(s.breaking >= LLONG_MIN && s.breaking <= LLONG_MAX);
108+
assert(s.b2 >= -65536 && s.b2 <= 65535);
109+
assert(s.b3 == true || s.b3 == false);
110+
assert(s.b4 >= -2097152 && s.b4 <= 2097151);
111+
if (s.b1 >= 123 && s.b3) {
112+
return 1;
113+
} else if (s.b1 >= 123 && s.b4 < 0) {
114+
return 2;
115+
} else if (s.breaking > 42) {
116+
return 3;
117+
}
118+
return 4;
119+
}
120+
121+
void simple_modify(SimpleSignedStr* s) {
122+
s->a++;
123+
s->b = ~s->b;
124+
if (s->c >= 0) {
125+
s->c *= 2;
126+
}
127+
s->d /= 2;
128+
}
129+
130+
SimpleSignedStr* create_on_heap(int a, int b, int c, int d) {
131+
SimpleSignedStr* s = malloc(sizeof(SimpleSignedStr));
132+
if (s) {
133+
s->a = s->b = s->c = s->d = -1;
134+
if (a >= -8388608 && a <= 8388607) {
135+
s->a = a;
136+
}
137+
if (b >= -1 && b <= 0) {
138+
s->b = b;
139+
}
140+
if (c >= -2 && c <= 1) {
141+
s->c = c;
142+
}
143+
if (d >= -16 && d <= 15) {
144+
s->d = d;
145+
}
146+
}
147+
return s;
148+
}

‎integration-tests/c-example/lib/structures/bitfields.h

+103
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,103 @@
1+
#ifndef C_EXAMPLE_BITFIELDS_H
2+
#define C_EXAMPLE_BITFIELDS_H
3+
4+
#include <stdbool.h>
5+
6+
typedef struct {
7+
signed a : 24;
8+
signed b : 1;
9+
signed int c : 2;
10+
signed int d : 5;
11+
} SimpleSignedStr;
12+
13+
typedef struct {
14+
unsigned a : 2;
15+
unsigned b : 5;
16+
unsigned int c : 1;
17+
unsigned int d : 24;
18+
} SimpleUnsignedStr;
19+
20+
typedef struct {
21+
int a : 24;
22+
int b : 2;
23+
int c : 1;
24+
int d : 5;
25+
} ImplementationDefinedStr;
26+
27+
typedef struct {
28+
signed a : 3;
29+
signed b : 3;
30+
} PossiblySmallStr;
31+
32+
typedef union {
33+
unsigned a : 2;
34+
unsigned b : 1;
35+
unsigned c : 6;
36+
unsigned d : 23;
37+
} SimpleUnsignedUnion;
38+
39+
typedef struct {
40+
// will **usually** occupy 8 bytes:
41+
bool a : 1;
42+
unsigned b : 2;
43+
signed c : 1;
44+
unsigned d : 3;
45+
// 25 bits: unused
46+
int e;
47+
} ComplexStr;
48+
49+
typedef struct {
50+
// will **usually** occupy 1 byte
51+
bool a : 1, b : 1, c : 1;
52+
} StrWithBool;
53+
54+
// struct InvalidNumberOfBits { // should produce an error in C
55+
// bool a : 2;
56+
// unsigned b : 50;
57+
// signed c : 1;
58+
// unsigned d : 3;
59+
// };
60+
61+
typedef struct {
62+
// will **usually** occupy 4 bytes:
63+
// 5 bits: value of b1
64+
// 11 bits: unused -- explicitly specified padding
65+
// 6 bits: value of b2
66+
// 2 bits: value of b3
67+
// 3 bits: unused -- explicitly specified padding
68+
// 5 bits: unused -- implicitly
69+
unsigned b1 : 5, : 11, b2 : 6, b3 : 2;
70+
signed : 3;
71+
} StrWithUnnamedBitfields;
72+
73+
typedef struct {
74+
// will **usually** occupy 8 bytes:
75+
// 7 bits: value of b1
76+
// 25 bits: unused
77+
// 6 bits: value of b2
78+
// 15 bits: value of b3
79+
// 11 bits: unused
80+
unsigned b1 : 7;
81+
unsigned : 0; // start a new allocation unit
82+
unsigned b2 : 6;
83+
unsigned b3 : 15;
84+
} StrWithUnnamedZeroBitfield;
85+
86+
typedef struct {
87+
// will **usually** occupy 24 bytes:
88+
// 7 bits: value of b1
89+
// 57 bits: unused
90+
// 64 bits: value of breaking
91+
// 17 bits: value of b2
92+
// 1 bit: value of b3
93+
// 22 bits: value of b4
94+
// 24 bits: unused
95+
unsigned b1 : 7; // from 0 to 127
96+
long long breaking; // from LLONG_MIN to LLONG_MAX
97+
signed b2 : 17; // from -65536 to 65535
98+
bool b3 : 1; // from 0 to 1
99+
int b4 : 22; // usually from -2097152 to 2097151
100+
} StrWithBreak;
101+
102+
103+
#endif //C_EXAMPLE_BITFIELDS_H

‎integration-tests/cpp-example/cxx_lib/structs/bitfields.cpp

+36
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
#include "bitfields.hpp"
2+
#include <cassert>
3+
#include <limits>
4+
#include <cstdio>
5+
6+
static int ALIGN = -30;
7+
8+
#define print_sizeof(S) printf("size of %*s : %zu bytes\n", ALIGN, #S, sizeof((S){}))
9+
10+
void print_sizeof_structs() {
11+
print_sizeof(CppSpecificStruct);
12+
}
13+
14+
CppSpecificStruct modify_and_return_copy(CppSpecificStruct& s) {
15+
assert(s.b1 >= 0 && s.b1 <= 127);
16+
assert(s.breaking >= std::numeric_limits<long long>::min());
17+
assert(s.breaking <= std::numeric_limits<long long>::max());
18+
assert(s.b2 >= -65536 && s.b2 <= 65535);
19+
assert(s.b4 >= -2097152 && s.b4 <= 2097151);
20+
assert(s.b5 >= std::numeric_limits<int>::min());
21+
assert(s.b5 <= std::numeric_limits<int>::max());
22+
assert(s.b6 >= -8 && s.b6 <= 7);
23+
s.b1 = s.b1 * 2 + 1;
24+
s.breaking = std::numeric_limits<long long>::max();
25+
if (s.b2 != -65536) {
26+
s.b2 = -s.b2;
27+
}
28+
s.b3 ^= 1;
29+
if (s.b5 > 0) {
30+
s.b5 = 10;
31+
} else {
32+
s.b5 = -10;
33+
}
34+
s.b6 = (s.b1 > 0) + (s.b2 > 0) + (s.b3 > 0) + (s.b4 > 0) + (s.b5 > 0) + (s.b6 > 0);
35+
return CppSpecificStruct(s);
36+
}

‎integration-tests/cpp-example/cxx_lib/structs/bitfields.hpp

+29
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
#ifndef CPP_EXAMPLE_BITFIELDS_H
2+
#define CPP_EXAMPLE_BITFIELDS_H
3+
4+
struct CppSpecificStruct {
5+
// will **usually** occupy 40 bytes:
6+
// 7 bits: value of b1
7+
// 57 bits: unused
8+
// 64 bits: value of breaking
9+
// 17 bits: value of b2
10+
// 1 bit: value of b3
11+
// 22 bits: value of b4
12+
// 24 bits: unused
13+
// 32 bits: value of b5
14+
// 34 bits: unused
15+
// 4 bits: value of b6
16+
// 58 bits: unused
17+
unsigned b1 : 7; // from 0 to 127
18+
long long breaking; // from LLONG_MIN to LLONG_MAX
19+
signed b2 : 17; // from -65536 to 65535
20+
bool b3 : 1; // from 0 to 1
21+
int b4 : 22; // from -2097152 to 2097151
22+
unsigned : 0; // starts a new allocation unit
23+
signed b5 : 66; // from INT_MIN to INT_MAX
24+
signed b6 : 4; // from -8 to 7
25+
};
26+
27+
CppSpecificStruct modify_and_return_copy(CppSpecificStruct& s);
28+
29+
#endif //CPP_EXAMPLE_BITFIELDS_H

‎server/CMakeLists.txt

+1-1
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ if (NOT DEFINED RUN_INFO)
1717
endif ()
1818

1919
project(UTBotCpp DESCRIPTION "Tool that generates unit test by C/C++ source code, trying to reach all branches and maximize code coverage"
20-
HOMEPAGE_URL "https://unittestbot.org" VERSION ${VERSION})
20+
HOMEPAGE_URL "https://www.utbot.org" VERSION ${VERSION})
2121
set(PROJECT_ORG "UnitTestBot")
2222

2323
message("Project: ${PROJECT_NAME}")

0 commit comments

Comments
 (0)