Skip to content

Commit 4ad5f55

Browse files
committed
Update klee
1 parent 7444333 commit 4ad5f55

File tree

8 files changed

+54
-15
lines changed

8 files changed

+54
-15
lines changed

build.sh

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
set -e
33
set -o pipefail
44
pwd=$PWD
5-
chmod +x $pwd/submodules/klee/build.sh $pwd/submodules/Bear/build.sh $pwd/server/build.sh
6-
cd $pwd/submodules/klee && ./build.sh
5+
chmod +x $pwd/submodules/build-klee.sh $pwd/submodules/Bear/build.sh $pwd/server/build.sh
6+
cd $pwd/submodules && ./build-klee.sh
77
cd $pwd/submodules/Bear && ./build.sh
88
cd $pwd/server && ./build.sh

docs/contributor-guides/advanced/symbolic-stdin.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -249,7 +249,7 @@ TEST(regression, check_password_test_10)
249249
In the previous version, UnitTestBot didn't preprocess functions that were using `stdin` before sending the bitcode to
250250
KLEE. Having added the interactive mode, we faced difficulties: KLEE couldn't work with multiple entry points
251251
that used `stdin` in one launch. The fact is that KLEE substitutes the original entry point to POSIX wrapper, which
252-
initializes environment and adds the `stdin`, `stdin-stat`, `stdin-read`, and `model-version` symbolic variables.
252+
initializes environment and adds the `stdin`, `stdin_stat`, `stdin_read`, and `model_version` symbolic variables.
253253
Then KLEE launches this wrapper as if the wrapper was the initial entry point.
254254
255255
UnitTestBot doesn't use these KLEE wrappers now. Instead, UnitTestBot creates the POSIX wrapper for every
@@ -304,4 +304,4 @@ TEST(regression, file_fgetc_test_1)
304304
int actual = file_fgetc(fA, fB, fC);
305305
EXPECT_EQ(4, actual);
306306
}
307-
```
307+
```

server/src/KleeRunner.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -222,7 +222,6 @@ KleeRunner::createKleeParams(const tests::TestMethod &testMethod,
222222
"--utbot",
223223
"--posix-runtime",
224224
"--skip-not-lazy-initialized",
225-
"--type-system=CXX",
226225
"--fp-runtime",
227226
"--only-output-states-covering-new",
228227
"--allocate-determ",
@@ -235,9 +234,11 @@ KleeRunner::createKleeParams(const tests::TestMethod &testMethod,
235234
"--check-overshift=false",
236235
"--skip-not-symbolic-objects",
237236
"--use-tbaa",
237+
"--ubsan-runtime",
238238
"--output-dir=" + kleeOut.string()
239239
};
240240
if (Paths::isCXXFile(testMethod.sourceFilePath)) {
241+
argvData.emplace_back("--use-advanced-type-system=true");
241242
argvData.emplace_back("--libcxx=true");
242243
}
243244
if (settingsContext.useDeterministicSearcher) {

server/src/Tests.cpp

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1063,12 +1063,12 @@ void KTestObjectParser::processGlobalParamPreValue(Tests::TestCaseDescription &t
10631063

10641064
void KTestObjectParser::processSymbolicStdin(Tests::TestCaseDescription &testCaseDescription,
10651065
const std::vector<RawKleeParam> &rawKleeParams) {
1066-
auto &&read = getKleeParamOrThrow(rawKleeParams, "stdin-read");
1066+
auto &&read = getKleeParamOrThrow(rawKleeParams, KleeUtils::STDIN_READ_NAME);
10671067
std::string &&view =
1068-
testParameterView(read, { types::Type::longlongType(), "stdin-read" },
1069-
types::PointerUsage::PARAMETER, testCaseDescription.objects,
1070-
testCaseDescription.lazyReferences)
1071-
->getEntryValue(nullptr);
1068+
testParameterView(read, {types::Type::longlongType(), KleeUtils::STDIN_READ_NAME},
1069+
types::PointerUsage::PARAMETER, testCaseDescription.objects,
1070+
testCaseDescription.lazyReferences)
1071+
->getEntryValue(nullptr);
10721072
if (view == "0LL") {
10731073
return;
10741074
} else {
@@ -1078,7 +1078,7 @@ void KTestObjectParser::processSymbolicStdin(Tests::TestCaseDescription &testCas
10781078
LOG_S(ERROR) << message;
10791079
throw UnImplementedException(message);
10801080
}
1081-
auto &&stdinBuffer = getKleeParamOrThrow(rawKleeParams, "stdin");
1081+
auto &&stdinBuffer = getKleeParamOrThrow(rawKleeParams, KleeUtils::STDIN_NAME);
10821082
auto &&testParamView = stringLiteralView(stdinBuffer.rawData, usedStdinBytesCount);
10831083
testCaseDescription.stdinValue = Tests::TestCaseParamValue(types::Type::getStdinParamName(),
10841084
std::nullopt, testParamView);

server/src/utils/KleeUtils.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,9 @@ namespace KleeUtils {
1212
static inline const std::string RESULT_VARIABLE_NAME = "utbot_result";
1313
static inline const std::string NOT_NULL_VARIABLE_NAME = "utbot_return_not_null";
1414

15+
static inline const std::string STDIN_READ_NAME = "stdin_read";
16+
static inline const std::string STDIN_NAME = "stdin";
17+
1518
std::string getRenamedOperator(std::string_view methodName);
1619

1720
std::string entryPointFunction(const tests::Tests &tests,

server/src/utils/PrinterUtils.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -161,15 +161,15 @@ namespace PrinterUtils {
161161
}
162162

163163
std::string getFileParamKTestJSON(char fileName) {
164-
return StringUtils::stringFormat("%c-data", fileName);
164+
return StringUtils::stringFormat("%c_data", fileName);
165165
}
166166

167167
std::string getFileReadBytesParamKTestJSON(char fileName) {
168-
return StringUtils::stringFormat("%c-data-read", fileName);
168+
return StringUtils::stringFormat("%c_data_read", fileName);
169169
}
170170

171171
std::string getFileWriteBytesParamKTestJSON(char fileName) {
172-
return StringUtils::stringFormat("%c-data-write", fileName);
172+
return StringUtils::stringFormat("%c_data_write", fileName);
173173
}
174174

175175
void removeThreadLocalQualifiers(std::string &decl) {

submodules/build-klee.sh

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
#!/bin/bash
2+
# This script is used to build KLEE as UTBot backend
3+
4+
set -e
5+
set -o pipefail
6+
cd klee
7+
mkdir -p build
8+
cd build
9+
10+
$UTBOT_CMAKE_BINARY -G Ninja \
11+
-DCMAKE_PREFIX_PATH=$UTBOT_INSTALL_DIR/lib/cmake/z3 \
12+
-DCMAKE_LIBRARY_PATH=$UTBOT_INSTALL_DIR/lib \
13+
-DCMAKE_INCLUDE_PATH=$UTBOT_INSTALL_DIR/include \
14+
-DENABLE_SOLVER_Z3=TRUE \
15+
-DENABLE_POSIX_RUNTIME=TRUE \
16+
-DENABLE_FLOATING_POINT=TRUE \
17+
-DENABLE_FP_RUNTIME=TRUE \
18+
-DLLVM_CONFIG_BINARY=$UTBOT_INSTALL_DIR/bin/llvm-config \
19+
-DLLVMCC=/utbot_distr/install/bin/clang \
20+
-DLLVMCXX=/utbot_distr/install/bin/clang++ \
21+
-DENABLE_UNIT_TESTS=TRUE \
22+
-DENABLE_SYSTEM_TESTS=TRUE \
23+
-DGTEST_SRC_DIR=$UTBOT_ALL/gtest \
24+
-DGTEST_INCLUDE_DIR=$UTBOT_ALL/gtest/googletest/include \
25+
-DCMAKE_INSTALL_PREFIX=$UTBOT_ALL/klee \
26+
-DENABLE_KLEE_LIBCXX=TRUE \
27+
-DKLEE_LIBCXX_DIR=$UTBOT_ALL/libcxx/install \
28+
-DKLEE_LIBCXX_INCLUDE_DIR=$UTBOT_ALL/libcxx/install/include/c++/v1 \
29+
-DENABLE_KLEE_EH_CXX=TRUE \
30+
-DKLEE_LIBCXXABI_SRC_DIR=$UTBOT_ALL/libcxx/libcxxabi \
31+
-DCMAKE_BUILD_TYPE=Release \
32+
..
33+
34+
$UTBOT_CMAKE_BINARY --build .
35+
$UTBOT_CMAKE_BINARY --install .

submodules/klee

Submodule klee updated 913 files

0 commit comments

Comments
 (0)