Skip to content

Commit

Permalink
bit fields support added (#383)
Browse files Browse the repository at this point in the history
* 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
  • Loading branch information
belous-dp authored Sep 2, 2022
1 parent 14e599c commit 69f5f2d
Show file tree
Hide file tree
Showing 27 changed files with 1,606 additions and 397 deletions.
148 changes: 148 additions & 0 deletions integration-tests/c-example/lib/structures/bitfields.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,148 @@
#include "bitfields.h"
#include <assert.h>
#include <limits.h>
#include <stddef.h>
#include <stdio.h>
#include <stdlib.h>

static int ALIGN = -30;

#define print_sizeof(S) printf("size of %*s : %zu bytes\n", ALIGN, #S, sizeof((S){}))

void print_sizeof_structs() {
print_sizeof(SimpleSignedStr);
print_sizeof(SimpleUnsignedStr);
print_sizeof(ImplementationDefinedStr);
print_sizeof(PossiblySmallStr);
print_sizeof(SimpleUnsignedUnion);
print_sizeof(ComplexStr);
print_sizeof(StrWithBool);
print_sizeof(StrWithUnnamedBitfields);
print_sizeof(StrWithUnnamedZeroBitfield);
print_sizeof(StrWithBreak);
}

int check_simple_signed_str(SimpleSignedStr s) {
if (s.a == 1024 && s.b == -1 && s.d == -16) {
return 1;
} else if (s.b == 0) {
return -1;
}
return 0;
}

int is_sum_greater_10(SimpleUnsignedStr s) {
return (s.a + s.b + s.c + s.d > 10 && s.d > 5);
}

int is_all_greater_2(PossiblySmallStr s) {
if (s.a > 2 && s.b > 2) {
return 1;
}
return 0;
}

int union_greater_2(SimpleUnsignedUnion u) {
if (u.c > 2) {
return 1;
}
return 0;
}

int union_greater_2_short(SimpleUnsignedUnion u) {
return u.c > 2;
}

int sum_of_fields(ComplexStr s) {
if (!s.a) {
return -1;
}
return s.a + s.b + s.c + s.d + s.e;
}

int decode_from_bool(StrWithBool s) {
if (!s.a && !s.b && !s.c) {
return 0;
} else if (s.a && !s.b && !s.c) {
return 1;
} else if (!s.a && s.b && !s.c) {
return 2;
} else if (s.a && s.b && !s.c) {
return 3;
} else if (!s.a && !s.b && s.c) {
return 4;
} else if (s.a && !s.b && s.c) {
return 5;
} else if (!s.a && s.b && s.c) {
return 6;
}
return 7;
}

int decode_from_bool_simple(StrWithBool s) {
if (!s.a && !s.b && !s.c) {
return 0;
} else if (s.a && !s.b && s.c) {
return 5;
}
return 7;
}

StrWithUnnamedBitfields mult_by_two(StrWithUnnamedBitfields s) {
s.b1 *= 2;
s.b2 *= 2;
s.b3 *= 2;
return s;
}

int is_nice(StrWithUnnamedZeroBitfield s) {
if (s.b1 == 69 && s.b2 == 42 && s.b3 == 1488) {
return 13;
}
return 0;
}

int check_fields_bounds(StrWithBreak s) {
assert(s.b1 >= 0 && s.b1 <= 127);
assert(s.breaking >= LLONG_MIN && s.breaking <= LLONG_MAX);
assert(s.b2 >= -65536 && s.b2 <= 65535);
assert(s.b3 == true || s.b3 == false);
assert(s.b4 >= -2097152 && s.b4 <= 2097151);
if (s.b1 >= 123 && s.b3) {
return 1;
} else if (s.b1 >= 123 && s.b4 < 0) {
return 2;
} else if (s.breaking > 42) {
return 3;
}
return 4;
}

void simple_modify(SimpleSignedStr* s) {
s->a++;
s->b = ~s->b;
if (s->c >= 0) {
s->c *= 2;
}
s->d /= 2;
}

SimpleSignedStr* create_on_heap(int a, int b, int c, int d) {
SimpleSignedStr* s = malloc(sizeof(SimpleSignedStr));
if (s) {
s->a = s->b = s->c = s->d = -1;
if (a >= -8388608 && a <= 8388607) {
s->a = a;
}
if (b >= -1 && b <= 0) {
s->b = b;
}
if (c >= -2 && c <= 1) {
s->c = c;
}
if (d >= -16 && d <= 15) {
s->d = d;
}
}
return s;
}
103 changes: 103 additions & 0 deletions integration-tests/c-example/lib/structures/bitfields.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,103 @@
#ifndef C_EXAMPLE_BITFIELDS_H
#define C_EXAMPLE_BITFIELDS_H

#include <stdbool.h>

typedef struct {
signed a : 24;
signed b : 1;
signed int c : 2;
signed int d : 5;
} SimpleSignedStr;

typedef struct {
unsigned a : 2;
unsigned b : 5;
unsigned int c : 1;
unsigned int d : 24;
} SimpleUnsignedStr;

typedef struct {
int a : 24;
int b : 2;
int c : 1;
int d : 5;
} ImplementationDefinedStr;

typedef struct {
signed a : 3;
signed b : 3;
} PossiblySmallStr;

typedef union {
unsigned a : 2;
unsigned b : 1;
unsigned c : 6;
unsigned d : 23;
} SimpleUnsignedUnion;

typedef struct {
// will **usually** occupy 8 bytes:
bool a : 1;
unsigned b : 2;
signed c : 1;
unsigned d : 3;
// 25 bits: unused
int e;
} ComplexStr;

typedef struct {
// will **usually** occupy 1 byte
bool a : 1, b : 1, c : 1;
} StrWithBool;

// struct InvalidNumberOfBits { // should produce an error in C
// bool a : 2;
// unsigned b : 50;
// signed c : 1;
// unsigned d : 3;
// };

typedef struct {
// will **usually** occupy 4 bytes:
// 5 bits: value of b1
// 11 bits: unused -- explicitly specified padding
// 6 bits: value of b2
// 2 bits: value of b3
// 3 bits: unused -- explicitly specified padding
// 5 bits: unused -- implicitly
unsigned b1 : 5, : 11, b2 : 6, b3 : 2;
signed : 3;
} StrWithUnnamedBitfields;

typedef struct {
// will **usually** occupy 8 bytes:
// 7 bits: value of b1
// 25 bits: unused
// 6 bits: value of b2
// 15 bits: value of b3
// 11 bits: unused
unsigned b1 : 7;
unsigned : 0; // start a new allocation unit
unsigned b2 : 6;
unsigned b3 : 15;
} StrWithUnnamedZeroBitfield;

typedef struct {
// will **usually** occupy 24 bytes:
// 7 bits: value of b1
// 57 bits: unused
// 64 bits: value of breaking
// 17 bits: value of b2
// 1 bit: value of b3
// 22 bits: value of b4
// 24 bits: unused
unsigned b1 : 7; // from 0 to 127
long long breaking; // from LLONG_MIN to LLONG_MAX
signed b2 : 17; // from -65536 to 65535
bool b3 : 1; // from 0 to 1
int b4 : 22; // usually from -2097152 to 2097151
} StrWithBreak;


#endif //C_EXAMPLE_BITFIELDS_H
36 changes: 36 additions & 0 deletions integration-tests/cpp-example/cxx_lib/structs/bitfields.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
#include "bitfields.hpp"
#include <cassert>
#include <limits>
#include <cstdio>

static int ALIGN = -30;

#define print_sizeof(S) printf("size of %*s : %zu bytes\n", ALIGN, #S, sizeof((S){}))

void print_sizeof_structs() {
print_sizeof(CppSpecificStruct);
}

CppSpecificStruct modify_and_return_copy(CppSpecificStruct& s) {
assert(s.b1 >= 0 && s.b1 <= 127);
assert(s.breaking >= std::numeric_limits<long long>::min());
assert(s.breaking <= std::numeric_limits<long long>::max());
assert(s.b2 >= -65536 && s.b2 <= 65535);
assert(s.b4 >= -2097152 && s.b4 <= 2097151);
assert(s.b5 >= std::numeric_limits<int>::min());
assert(s.b5 <= std::numeric_limits<int>::max());
assert(s.b6 >= -8 && s.b6 <= 7);
s.b1 = s.b1 * 2 + 1;
s.breaking = std::numeric_limits<long long>::max();
if (s.b2 != -65536) {
s.b2 = -s.b2;
}
s.b3 ^= 1;
if (s.b5 > 0) {
s.b5 = 10;
} else {
s.b5 = -10;
}
s.b6 = (s.b1 > 0) + (s.b2 > 0) + (s.b3 > 0) + (s.b4 > 0) + (s.b5 > 0) + (s.b6 > 0);
return CppSpecificStruct(s);
}
29 changes: 29 additions & 0 deletions integration-tests/cpp-example/cxx_lib/structs/bitfields.hpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
#ifndef CPP_EXAMPLE_BITFIELDS_H
#define CPP_EXAMPLE_BITFIELDS_H

struct CppSpecificStruct {
// will **usually** occupy 40 bytes:
// 7 bits: value of b1
// 57 bits: unused
// 64 bits: value of breaking
// 17 bits: value of b2
// 1 bit: value of b3
// 22 bits: value of b4
// 24 bits: unused
// 32 bits: value of b5
// 34 bits: unused
// 4 bits: value of b6
// 58 bits: unused
unsigned b1 : 7; // from 0 to 127
long long breaking; // from LLONG_MIN to LLONG_MAX
signed b2 : 17; // from -65536 to 65535
bool b3 : 1; // from 0 to 1
int b4 : 22; // from -2097152 to 2097151
unsigned : 0; // starts a new allocation unit
signed b5 : 66; // from INT_MIN to INT_MAX
signed b6 : 4; // from -8 to 7
};

CppSpecificStruct modify_and_return_copy(CppSpecificStruct& s);

#endif //CPP_EXAMPLE_BITFIELDS_H
2 changes: 1 addition & 1 deletion server/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ if (NOT DEFINED RUN_INFO)
endif ()

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

message("Project: ${PROJECT_NAME}")
Expand Down
Loading

0 comments on commit 69f5f2d

Please sign in to comment.