Skip to content

Commit 76f9bdf

Browse files
authored
Integrate new version of klee (#579)
1 parent 17bf7e7 commit 76f9bdf

24 files changed

+1290
-368
lines changed
Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
#include "hard-linked-list.h"
2+
#include <stddef.h>
3+
4+
int hard_list_and_pointers(struct Node *node) {
5+
if (node == NULL) {
6+
return 0;
7+
}
8+
if (node->x == NULL || node->data == NULL) {
9+
return -1;
10+
}
11+
if (node->x == &(node->data->x) && *node->x == node->data->x) {
12+
return 1;
13+
}
14+
if (node->next == NULL) {
15+
return -2;
16+
}
17+
if (node->next->x == NULL || node->next->data == NULL) {
18+
return -3;
19+
}
20+
if (node->next->data == node->data && &(node->next->data->y) == node->x && node->next->data->y == *node->x) {
21+
return 2;
22+
}
23+
return 3;
24+
}
Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
#ifndef HARD_LINKED_LIST_H
2+
#define HARD_LINKED_LIST_H
3+
4+
struct Data {
5+
int x;
6+
int y;
7+
};
8+
9+
struct Node {
10+
int *x;
11+
struct Data *data;
12+
struct Node *next;
13+
};
14+
15+
#endif

server/src/KleeRunner.cpp

Lines changed: 37 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -138,35 +138,35 @@ static void processMethod(MethodKtests &ktestChunk,
138138
bool hasError = false;
139139
for (auto const &entry : fs::directory_iterator(kleeOut)) {
140140
auto const &path = entry.path();
141-
if (Paths::isKtestJson(path)) {
141+
if (Paths::isKtest(path)) {
142142
if (Paths::hasEarly(path)) {
143143
hasTimeout = true;
144144
} else if (Paths::hasInternalError(path)) {
145145
hasError = true;
146146
} else {
147-
std::unique_ptr<TestCase, decltype(&TestCase_free)> ktestData{
148-
TC_fromFile(path.c_str()), TestCase_free
147+
std::unique_ptr<KTest, decltype(&kTest_free)> ktestData{
148+
kTest_fromFile(path.c_str()), kTest_free
149149
};
150150
if (ktestData == nullptr) {
151-
LOG_S(WARNING) << "Unable to open .ktestjson file";
151+
LOG_S(WARNING) << "Unable to open .ktest file";
152152
continue;
153153
}
154154
const std::vector<fs::path> &errorDescriptorFiles =
155-
Paths::getErrorDescriptors(path);
155+
Paths::getErrorDescriptors(path);
156156

157157
UTBotKTest::Status status = errorDescriptorFiles.empty()
158-
? UTBotKTest::Status::SUCCESS
159-
: UTBotKTest::Status::FAILED;
160-
std::vector<ConcretizedObject> kTestObjects(
161-
ktestData->objects, ktestData->objects + ktestData->n_objects);
158+
? UTBotKTest::Status::SUCCESS
159+
: UTBotKTest::Status::FAILED;
160+
std::vector<KTestObject> kTestObjects(ktestData->objects,
161+
ktestData->objects + ktestData->numObjects);
162162

163-
std::vector<UTBotKTestObject> objects = CollectionUtils::transform(
164-
kTestObjects, [](const ConcretizedObject &kTestObject) {
163+
std::vector<UTBotKTestObject> objects =
164+
CollectionUtils::transform(kTestObjects, [](const KTestObject &kTestObject) {
165165
return UTBotKTestObject{ kTestObject };
166166
});
167167

168-
std::vector<std::string> errorDescriptors = CollectionUtils::transform(
169-
errorDescriptorFiles, [](const fs::path &errorFile) {
168+
std::vector<std::string> errorDescriptors =
169+
CollectionUtils::transform(errorDescriptorFiles, [](const fs::path &errorFile) {
170170
std::ifstream fileWithError(errorFile.c_str(), std::ios_base::in);
171171
std::string content((std::istreambuf_iterator<char>(fileWithError)),
172172
std::istreambuf_iterator<char>());
@@ -209,29 +209,32 @@ std::pair<std::vector<std::string>, fs::path>
209209
KleeRunner::createKleeParams(const tests::TestMethod &testMethod,
210210
const tests::Tests &tests,
211211
const std::string &methodNameOrEmptyForFolder) {
212-
fs::path kleeOut = Paths::kleeOutDirForEntrypoints(projectContext,
213-
tests.sourceFilePath,
212+
fs::path kleeOut = Paths::kleeOutDirForEntrypoints(projectContext, tests.sourceFilePath,
214213
methodNameOrEmptyForFolder);
215214
fs::create_directories(kleeOut.parent_path());
216215

217-
std::vector<std::string> argvData = { "klee",
218-
"--entry-point=" + KleeUtils::entryPointFunction(tests, testMethod.methodName, true),
219-
"--libc=klee",
220-
"--utbot",
221-
"--posix-runtime",
222-
"--type-system=CXX",
223-
"--fp-runtime",
224-
"--only-output-states-covering-new",
225-
"--allocate-determ",
226-
"--external-calls=all",
227-
"--timer-interval=1000ms",
228-
"--bcov-check-interval=8s",
229-
"-istats-write-interval=5s",
230-
"--disable-verify",
231-
"--check-div-zero=false",
232-
"--check-overshift=false",
233-
"--skip-not-lazy-and-symbolic-pointers",
234-
"--output-dir=" + kleeOut.string()};
216+
std::vector<std::string> argvData = {
217+
"klee",
218+
"--entry-point=" + KleeUtils::entryPointFunction(tests, testMethod.methodName, true),
219+
"--libc=klee",
220+
"--utbot",
221+
"--posix-runtime",
222+
"--skip-not-lazy-initialized",
223+
"--type-system=CXX",
224+
"--fp-runtime",
225+
"--only-output-states-covering-new",
226+
"--allocate-determ",
227+
"--external-calls=all",
228+
"--timer-interval=1000ms",
229+
"--use-cov-check=instruction-based",
230+
"-istats-write-interval=5s",
231+
"--disable-verify",
232+
"--check-div-zero=false",
233+
"--check-overshift=false",
234+
"--skip-not-symbolic-objects",
235+
"--use-tbaa",
236+
"--output-dir=" + kleeOut.string()
237+
};
235238
if (settingsContext.useDeterministicSearcher) {
236239
argvData.emplace_back("--search=dfs");
237240
}
@@ -240,7 +243,7 @@ KleeRunner::createKleeParams(const tests::TestMethod &testMethod,
240243
argvData.emplace_back("--allocate-determ-size=" + std::to_string(1));
241244
argvData.emplace_back("--allocate-determ-start-address=" + std::to_string(0x10000));
242245
}
243-
return {argvData, kleeOut};
246+
return { argvData, kleeOut };
244247
}
245248

246249
void KleeRunner::addTailKleeInitParams(std::vector<std::string> &argvData, const std::string &bitcodeFilePath)

0 commit comments

Comments
 (0)