Skip to content

Commit 1969095

Browse files
S1eGaS1eGa
committed
[test, WIP] Added tests from GSAC competition.
1 parent 4be861f commit 1969095

39 files changed

Lines changed: 1902 additions & 1 deletion

File tree

‎lib/Core/Executor.cpp‎

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -968,6 +968,14 @@ void Executor::allocateGlobalObjects(ExecutionState &state) {
968968
const KGlobalVariable *kv = kmodule->globalMap.at(&v).get();
969969
ref<CodeLocation> vCodeLocation = CodeLocation::create(
970970
kv, kv->getSourceFilepath(), kv->getLine(), std::nullopt);
971+
972+
if (!isa<ConstantExpr>(size)) {
973+
addConstraint(
974+
state, UleExpr::create(
975+
ZExtExpr::create(size, Context::get().getPointerWidth()),
976+
Expr::createPointer(MaxSymbolicAllocationSize)));
977+
}
978+
971979
MemoryObject *mo = allocate(state, size, /*isLocal=*/false,
972980
/*isGlobal=*/true, /*allocSite=*/vCodeLocation,
973981
/*alignment=*/globalObjectAlignment);
@@ -7316,7 +7324,8 @@ bool resolveOnSymbolics(const std::vector<klee::Symbolic> &symbolics,
73167324
for (const auto &res : symbolics) {
73177325
const auto &mo = res.memoryObject;
73187326
// Check if the provided address is between start and end of the object
7319-
// [mo->address, mo->address + mo->size) or the object is a 0-sized object.
7327+
// [mo->address, mo->address + mo->size) or the object is a 0-sized
7328+
// object.
73207329
ref<klee::ConstantExpr> size =
73217330
cast<klee::ConstantExpr>(assn.evaluate(mo->getSizeExpr()));
73227331
if ((size->getZExtValue() == 0 && address == mo->address) ||

‎test/SARIF/GSAC/ContextSensitive/ContextSensitive.c‎

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
// RUN: %clang -emit-llvm -g -c %s -o %t.bc
2+
// RUN: rm -rf %t.klee-out
3+
// RUN: %klee -write-sarifs --use-sym-size-alloc --use-sym-size-li --skip-not-symbolic-objects --posix-runtime --libc=uclibc -cex-cache-validity-cores --output-dir=%t.klee-out %t.bc > %t.log
4+
// RUN: python3 %S/../../checker.py %t.klee-out/report.sarif %S/pattern.sarif
5+
6+
/***************************************************************************************
7+
* Title: GSAC
8+
* Author: https://github.com/GSACTech
9+
* Date: 2023
10+
* Code version: 1.0
11+
* Availability: https://github.com/GSACTech/contest
12+
*
13+
***************************************************************************************/
14+
#include <stdlib.h>
15+
16+
int *foo(int size) {
17+
int *data = (int *)malloc(size * sizeof(int));
18+
return data;
19+
}
20+
21+
int main() {
22+
int size = 5;
23+
int *first_data = foo(size++); // Call of 'foo(5)'
24+
int *second_data = foo(size--); // Call of 'foo(6)'
25+
26+
for (int i = 0; i <= size; i++) {
27+
// Length of 'first_data' is 5 and 'size' also is 5
28+
first_data[i] = i; // buffer-overflow
29+
}
30+
for (int i = 0; i <= size; i++) {
31+
// Length of 'second_data' is 6
32+
second_data[i] = i;
33+
}
34+
free(first_data);
35+
free(second_data);
36+
}

‎test/SARIF/GSAC/ContextSensitive/pattern.sarif‎

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
{
2+
"runs": [
3+
{
4+
"results": [
5+
{
6+
"codeFlows": [
7+
{
8+
"threadFlows": [
9+
{
10+
"locations": [
11+
{
12+
"location": {
13+
"message": {
14+
"text": "Heap memory allocation"
15+
},
16+
"physicalLocation": {
17+
"artifactLocation": {
18+
"uri": "ContextSensitive.c"
19+
},
20+
"region": {
21+
"endColumn": null,
22+
"endLine": null,
23+
"startColumn": 22,
24+
"startLine": 17
25+
}
26+
}
27+
}
28+
},
29+
{
30+
"location": {
31+
"message": {
32+
"text": "memory error: out of bound pointer"
33+
},
34+
"physicalLocation": {
35+
"artifactLocation": {
36+
"uri": "ContextSensitive.c"
37+
},
38+
"region": {
39+
"endColumn": null,
40+
"endLine": null,
41+
"startColumn": 19,
42+
"startLine": 28
43+
}
44+
}
45+
}
46+
}
47+
]
48+
}
49+
]
50+
}
51+
]
52+
}
53+
]
54+
}
55+
],
56+
"version": "2.1.0"
57+
}

‎test/SARIF/GSAC/EASY02/EASY02.c‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
// RUN: %clang -emit-llvm -g -c %s -o %t.bc
2+
// RUN: rm -rf %t.klee-out
3+
// RUN: %klee -write-sarifs --use-sym-size-alloc --use-sym-size-li --skip-not-symbolic-objects --posix-runtime --libc=uclibc -cex-cache-validity-cores --output-dir=%t.klee-out %t.bc > %t.log
4+
// RUN: python3 %S/../../checker.py %t.klee-out/report.sarif %S/pattern.sarif
5+
6+
/***************************************************************************************
7+
* Title: GSAC
8+
* Author: https://github.com/GSACTech
9+
* Date: 2023
10+
* Code version: 1.0
11+
* Availability: https://github.com/GSACTech/contest
12+
*
13+
***************************************************************************************/
14+
15+
#include <stdlib.h>
16+
17+
int main() {
18+
int size = 10;
19+
int *arr = malloc(size * sizeof(int)); // Memory allocation
20+
// Access is out of bounds
21+
arr[size] = 4; // buffer-overflow
22+
free(arr);
23+
}

‎test/SARIF/GSAC/EASY02/pattern.sarif‎

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
{
2+
"runs": [
3+
{
4+
"results": [
5+
{
6+
"codeFlows": [
7+
{
8+
"threadFlows": [
9+
{
10+
"locations": [
11+
{
12+
"location": {
13+
"message": {
14+
"text": "Heap memory allocation"
15+
},
16+
"physicalLocation": {
17+
"artifactLocation": {
18+
"uri": "EASY02.c"
19+
},
20+
"region": {
21+
"endColumn": null,
22+
"endLine": null,
23+
"startColumn": 14,
24+
"startLine": 19
25+
}
26+
}
27+
}
28+
},
29+
{
30+
"location": {
31+
"message": {
32+
"text": "memory error: out of bound pointer"
33+
},
34+
"physicalLocation": {
35+
"artifactLocation": {
36+
"uri": "EASY02.c"
37+
},
38+
"region": {
39+
"endColumn": null,
40+
"endLine": null,
41+
"startColumn": 13,
42+
"startLine": 21
43+
}
44+
}
45+
}
46+
}
47+
]
48+
}
49+
]
50+
}
51+
]
52+
}
53+
]
54+
}
55+
],
56+
"version": "2.1.0"
57+
}

‎test/SARIF/GSAC/EASY02_fix/EASY02_fix.c‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
// RUN: %clang -emit-llvm -g -c %s -o %t.bc
2+
// RUN: rm -rf %t.klee-out
3+
// RUN: %klee -write-sarifs --use-sym-size-alloc --use-sym-size-li --skip-not-symbolic-objects --posix-runtime --libc=uclibc -cex-cache-validity-cores --output-dir=%t.klee-out %t.bc > %t.log
4+
// RUN: test ! -f %t.klee-out/report.sarif
5+
6+
/***************************************************************************************
7+
* Title: GSAC
8+
* Author: https://github.com/GSACTech
9+
* Date: 2023
10+
* Code version: 1.0
11+
* Availability: https://github.com/GSACTech/contest
12+
*
13+
***************************************************************************************/
14+
15+
#include <stdlib.h>
16+
17+
int main() {
18+
int size = 10;
19+
int *arr = malloc(size * sizeof(int));
20+
arr[size - 1] = 4;
21+
free(arr);
22+
}

‎test/SARIF/GSAC/EASY03/EASY03.c‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
// RUN: %clang -emit-llvm -g -c %s -o %t.bc
2+
// RUN: rm -rf %t.klee-out
3+
// RUN: %klee -write-sarifs --use-sym-size-alloc --use-sym-size-li --skip-not-symbolic-objects --posix-runtime --libc=uclibc -cex-cache-validity-cores --output-dir=%t.klee-out %t.bc > %t.log
4+
// RUN: python3 %S/../../checker.py %t.klee-out/report.sarif %S/pattern.sarif
5+
6+
/***************************************************************************************
7+
* Title: GSAC
8+
* Author: https://github.com/GSACTech
9+
* Date: 2023
10+
* Code version: 1.0
11+
* Availability: https://github.com/GSACTech/contest
12+
*
13+
***************************************************************************************/
14+
15+
#include <stdlib.h>
16+
17+
int main() {
18+
int *data;
19+
int size = 5;
20+
data = malloc(size * sizeof(int)); // Memory allocation
21+
for (int i = 0; i <= size; i++) { // Last iteration of this cycle is (size + 1)_th
22+
// In the last iteration access is out of bounds
23+
data[i] = i; // buffer-overflow
24+
}
25+
free(data);
26+
}

‎test/SARIF/GSAC/EASY03/pattern.sarif‎

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
{
2+
"runs": [
3+
{
4+
"results": [
5+
{
6+
"codeFlows": [
7+
{
8+
"threadFlows": [
9+
{
10+
"locations": [
11+
{
12+
"location": {
13+
"message": {
14+
"text": "Heap memory allocation"
15+
},
16+
"physicalLocation": {
17+
"artifactLocation": {
18+
"uri": "EASY03.c"
19+
},
20+
"region": {
21+
"endColumn": null,
22+
"endLine": null,
23+
"startColumn": 10,
24+
"startLine": 20
25+
}
26+
}
27+
}
28+
},
29+
{
30+
"location": {
31+
"message": {
32+
"text": "memory error: out of bound pointer"
33+
},
34+
"physicalLocation": {
35+
"artifactLocation": {
36+
"uri": "EASY03.c"
37+
},
38+
"region": {
39+
"endColumn": null,
40+
"endLine": null,
41+
"startColumn": 13,
42+
"startLine": 23
43+
}
44+
}
45+
}
46+
}
47+
]
48+
}
49+
]
50+
}
51+
]
52+
}
53+
]
54+
}
55+
],
56+
"version": "2.1.0"
57+
}

‎test/SARIF/GSAC/EASY03_fix/EASY03_fix.c‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
// RUN: %clang -emit-llvm -g -c %s -o %t.bc
2+
// RUN: rm -rf %t.klee-out
3+
// RUN: %klee -write-sarifs --use-sym-size-alloc --use-sym-size-li --skip-not-symbolic-objects --posix-runtime --libc=uclibc -cex-cache-validity-cores --output-dir=%t.klee-out %t.bc > %t.log
4+
// RUN: test ! -f %t.klee-out/report.sarif
5+
6+
/***************************************************************************************
7+
* Title: GSAC
8+
* Author: https://github.com/GSACTech
9+
* Date: 2023
10+
* Code version: 1.0
11+
* Availability: https://github.com/GSACTech/contest
12+
*
13+
***************************************************************************************/
14+
15+
#include <stdlib.h>
16+
17+
int main() {
18+
int *data;
19+
int size = 5;
20+
data = malloc(size * sizeof(int));
21+
for (int i = 0; i < size; i++) {
22+
data[i] = i;
23+
}
24+
free(data);
25+
}

‎test/SARIF/GSAC/FieldSensitive/FieldSensitive.c‎

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
// RUN: %clang -emit-llvm -g -c %s -o %t.bc
2+
// RUN: rm -rf %t.klee-out
3+
// RUN: %klee -write-sarifs --use-sym-size-alloc --use-sym-size-li --skip-not-symbolic-objects --posix-runtime --libc=uclibc -cex-cache-validity-cores --output-dir=%t.klee-out %t.bc > %t.log
4+
// RUN: python3 %S/../../checker.py %t.klee-out/report.sarif %S/pattern.sarif
5+
6+
/***************************************************************************************
7+
* Title: GSAC
8+
* Author: https://github.com/GSACTech
9+
* Date: 2023
10+
* Code version: 1.0
11+
* Availability: https://github.com/GSACTech/contest
12+
*
13+
***************************************************************************************/
14+
15+
#include <stdlib.h>
16+
17+
struct Data {
18+
int *first_data;
19+
int *second_data;
20+
};
21+
22+
void foo(struct Data *data, int size) {
23+
data->second_data = (int *)malloc(size * sizeof(int)); // Allocated 20 bytes of memory
24+
size++;
25+
data->first_data = (int *)malloc(size * sizeof(int)); // Allocated 24 bytes of memory
26+
}
27+
28+
int main() {
29+
int size = 5;
30+
struct Data data;
31+
foo(&data, size);
32+
for (int i = 0; i <= size; i++) {
33+
data.first_data[i] = i;
34+
}
35+
// Length of 'second_data' is 5 and 'size' also is 5
36+
for (int i = 0; i <= size; i++) {
37+
data.second_data[i] = i; // buffer-overflow
38+
}
39+
free(data.first_data);
40+
free(data.second_data);
41+
}

0 commit comments

Comments
 (0)