Update klee (#644)

Fix test after update klee Update z3 in Dockerfile_base
UnitTestBot · Oct 20, 2023 · df7f800 · df7f800
1 parent 88fa5f3
commit df7f800
Show file tree

Hide file tree

Showing 22 changed files with 425 additions and 284 deletions.
diff --git a/.github/workflows/matrix.json b/.github/workflows/matrix.json
@@ -1,7 +1,7 @@
 {
   "include": [
     {
-      "DOCKER_TAG": "2022.10.0",
+      "DOCKER_TAG": "2023.10.0",
       "OPERATING_SYSTEM_TAG": "18.04",
       "LLVM_VERSION_MAJOR": "10"
     }

diff --git a/build.sh b/build.sh
@@ -2,7 +2,7 @@
 set -e
 set -o pipefail
 pwd=$PWD
-chmod +x $pwd/submodules/klee/build.sh $pwd/submodules/Bear/build.sh $pwd/server/build.sh
-cd $pwd/submodules/klee && ./build.sh
+chmod +x $pwd/submodules/build-klee.sh $pwd/submodules/Bear/build.sh $pwd/server/build.sh
+cd $pwd/submodules && ./build-klee.sh
 cd $pwd/submodules/Bear && ./build.sh
 cd $pwd/server && ./build.sh
diff --git a/docker/Dockerfile_base b/docker/Dockerfile_base
@@ -74,7 +74,7 @@ RUN git clone --single-branch --branch "release/${LLVM_VERSION_MAJOR}.x" --depth
 WORKDIR $UTBOT_ALL/llvm-project
 RUN mkdir build && cd build \
     && $UTBOT_CMAKE_BINARY \
-    -DCMAKE_BUILD_TYPE="Release" \
+    -DCMAKE_BUILD_TYPE=MinSizeRel \
     -DCMAKE_INSTALL_PREFIX=$UTBOT_INSTALL_DIR \
     -DLLVM_INCLUDE_TESTS=OFF \
     -DLLVM_BINUTILS_INCDIR=$UTBOT_ALL/llvm_gold_plugin \
@@ -125,7 +125,7 @@ RUN cd $UTBOT_ALL/grpc && git submodule update --init
 RUN cd $UTBOT_ALL/grpc \
   && mkdir -p cmake/build \
   && cd cmake/build \
-  && $UTBOT_CMAKE_BINARY -DgRPC_INSTALL=ON -DgRPC_BUILD_TESTS=OFF -DCMAKE_INSTALL_PREFIX=$UTBOT_INSTALL_DIR ../.. \
+  && $UTBOT_CMAKE_BINARY -DgRPC_INSTALL=ON -DgRPC_BUILD_TESTS=OFF -DCMAKE_BUILD_TYPE=MinSizeRel -DCMAKE_INSTALL_PREFIX=$UTBOT_INSTALL_DIR ../.. \
   && make -j`nproc` \
   && make install \
   && cd $UTBOT_ALL \
@@ -142,9 +142,9 @@ USER utbot
 
 # Install z3
 USER root
-RUN git clone --single-branch -b z3-4.8.7 --depth=1 https://github.com/Z3Prover/z3.git $UTBOT_ALL/z3-src
+RUN git clone --single-branch -b z3-4.8.17 --depth=1 https://github.com/Z3Prover/z3.git $UTBOT_ALL/z3-src
 RUN cd $UTBOT_ALL/z3-src && mkdir build && cd build && \
-    $UTBOT_CMAKE_BINARY -G "Ninja" -DCMAKE_INSTALL_PREFIX=$UTBOT_INSTALL_DIR .. && \
+    $UTBOT_CMAKE_BINARY -G "Ninja" -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=$UTBOT_INSTALL_DIR .. && \
     $UTBOT_CMAKE_BINARY --build . --target install && \
     cd $UTBOT_ALL && \
     rm -rf $UTBOT_ALL/z3-src
@@ -171,7 +171,7 @@ RUN npm config set strict-ssl false
 RUN npm cache clean -f
 RUN sudo -E npm install -g n
 RUN echo insecure > ~/.curlrc
-RUN sudo -E n stable
+RUN sudo -E n 16
 RUN sudo -E apt remove -y --purge nodejs npm
 
 # Install cmake which can generate link_commands.json. Installing cmake the second time in order to build base image faster since this cmake may be changed frequently.

diff --git a/docs/contributor-guides/advanced/symbolic-stdin.md b/docs/contributor-guides/advanced/symbolic-stdin.md
@@ -249,7 +249,7 @@ TEST(regression, check_password_test_10)
 In the previous version, UnitTestBot didn't preprocess functions that were using `stdin` before sending the bitcode to 
 KLEE. Having added the interactive mode, we faced difficulties: KLEE couldn't work with multiple entry points 
 that used `stdin` in one launch. The fact is that KLEE substitutes the original entry point to POSIX wrapper, which 
-initializes environment and adds the `stdin`, `stdin-stat`, `stdin-read`, and `model-version` symbolic variables. 
+initializes environment and adds the `stdin`, `stdin_stat`, `stdin_read`, and `model_version` symbolic variables. 
 Then KLEE launches this wrapper as if the wrapper was the initial entry point.
 
 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)
     int actual = file_fgetc(fA, fB, fC);
     EXPECT_EQ(4, actual);
 }
-```
+```
diff --git a/server/build.sh b/server/build.sh
@@ -3,6 +3,6 @@
 mkdir -p build
 cd build
 
-$UTBOT_CMAKE_BINARY -G "Ninja" -DCMAKE_INSTALL_PREFIX=$UTBOT_ALL/server-install ..
+$UTBOT_CMAKE_BINARY -G "Ninja" -DCMAKE_BUILD_TYPE=RelWithDebInfo -DCMAKE_INSTALL_PREFIX=$UTBOT_ALL/server-install ..
 $UTBOT_CMAKE_BINARY --build .
 $UTBOT_CMAKE_BINARY --install .
diff --git a/server/src/KleeRunner.cpp b/server/src/KleeRunner.cpp
@@ -222,7 +222,7 @@ KleeRunner::createKleeParams(const tests::TestMethod &testMethod,
         "--utbot",
         "--posix-runtime",
         "--skip-not-lazy-initialized",
-        "--type-system=CXX",
+        "--min-number-elements-li=1",
         "--fp-runtime",
         "--only-output-states-covering-new",
         "--allocate-determ",
@@ -235,10 +235,12 @@ KleeRunner::createKleeParams(const tests::TestMethod &testMethod,
         "--check-overshift=false",
         "--skip-not-symbolic-objects",
         "--use-tbaa",
+        "--ubsan-runtime",
         "--output-dir=" + kleeOut.string()
     };
     if (Paths::isCXXFile(testMethod.sourceFilePath)) {
-        argvData.emplace_back("--libcxx=true");
+        argvData.emplace_back("--use-advanced-type-system=true");
+//        argvData.emplace_back("--libcxx=true");
     }
     if (settingsContext.useDeterministicSearcher) {
         argvData.emplace_back("--search=dfs");

diff --git a/server/src/SARIFGenerator.cpp b/server/src/SARIFGenerator.cpp
@@ -66,9 +66,9 @@ namespace sarif {
                         if (lineInDescriptor.empty() || lineInDescriptor[0] == '#')
                             continue;
                         if (isspace(lineInDescriptor[0])) {
-                            if (key == "Stack") {
+                            if (key == "ExecutionStack") {
                                 const std::regex stack_regex(
-                                    R"regex(\s+#(.*) in ([^ ]*) [(][^)]*[)] at ([^:]*):(\d+))regex");
+                                    R"regex(\s+#(.*) in ([^ ]*)[(][^)]*[)] at ([^:]*):(\d+))regex");
                                 std::smatch stack_match;
                                 if (!std::regex_match(lineInDescriptor, stack_match, stack_regex)) {
                                     LOG_S(ERROR) << "wrong `Stack` line: " << lineInDescriptor;
@@ -129,10 +129,10 @@ namespace sarif {
                             if (pos == std::string::npos) {
                                 LOG_S(ERROR) << "no key:" << lineInDescriptor;
                             } else {
-                                if (key == "Stack") {
+                                if (key == "ExecutionStack") {
                                     // Check stack validity
                                     if (firstCallInStack) {
-                                        LOG_S(ERROR) << "no visible stack in descriptor:" << descriptor;
+                                        LOG_S(ERROR) << "no visible ExecutionStack in descriptor:" << descriptor;
                                     } else {
                                         canAddThisTestToSARIF = true;
                                     }
@@ -147,7 +147,7 @@ namespace sarif {
                                     result["kind"] = "fail";
                                 } else if (key == ERROR_ID_KEY) {
                                     result["ruleId"] = value;
-                                } else if (key == "Stack") {
+                                } else if (key == "ExecutionStack") {
                                     stackLocations = json();
                                     codeFlowsLocations = json();
                                 } else if (key == TEST_FILE_KEY) {

diff --git a/server/src/Tests.cpp b/server/src/Tests.cpp
@@ -675,7 +675,7 @@ void KTestObjectParser::assignTypeUnnamedVar(
             curType.paramValue.lazyValues.emplace_back(name, std::nullopt, testParamView);
         }
 
-        for (auto const &[offset, indObj, indexOffset] : testCase.objects[curType.jsonInd].pointers) {
+        for (auto const &[offset, indObj, indexOffset]: testCase.objects[curType.jsonInd].pointers) {
             if (indexOffset != 0) {
                 continue;
             }
@@ -1065,12 +1065,12 @@ void KTestObjectParser::processGlobalParamPreValue(Tests::TestCaseDescription &t
 
 void KTestObjectParser::processSymbolicStdin(Tests::TestCaseDescription &testCaseDescription,
                                              const std::vector<RawKleeParam> &rawKleeParams) {
-    auto &&read = getKleeParamOrThrow(rawKleeParams, "stdin-read");
+    auto &&read = getKleeParamOrThrow(rawKleeParams, KleeUtils::STDIN_READ_NAME);
     std::string &&view =
-        testParameterView(read, { types::Type::longlongType(), "stdin-read" },
-                          types::PointerUsage::PARAMETER, testCaseDescription.objects,
-                          testCaseDescription.lazyReferences)
-            ->getEntryValue(nullptr);
+            testParameterView(read, {types::Type::longlongType(), KleeUtils::STDIN_READ_NAME},
+                              types::PointerUsage::PARAMETER, testCaseDescription.objects,
+                              testCaseDescription.lazyReferences)
+                    ->getEntryValue(nullptr);
     if (view == "0LL") {
         return;
     } else {
@@ -1080,7 +1080,7 @@ void KTestObjectParser::processSymbolicStdin(Tests::TestCaseDescription &testCas
             LOG_S(ERROR) << message;
             throw UnImplementedException(message);
         }
-        auto &&stdinBuffer = getKleeParamOrThrow(rawKleeParams, "stdin");
+        auto &&stdinBuffer = getKleeParamOrThrow(rawKleeParams, KleeUtils::STDIN_NAME);
         auto &&testParamView = stringLiteralView(stdinBuffer.rawData, usedStdinBytesCount);
         testCaseDescription.stdinValue = Tests::TestCaseParamValue(types::Type::getStdinParamName(),
                                                                    std::nullopt, testParamView);

diff --git a/server/src/Tests.h b/server/src/Tests.h
@@ -888,8 +888,7 @@ namespace tests {
     std::enable_if_t<std::is_floating_point<T>::value, std::string>
     primitiveValueToString(T value) {
         std::stringstream ss;
-        ss << std::scientific;
-        ss << value;
+        ss << std::scientific << value;
         return ss.str();
     }
 

diff --git a/server/src/fetchers/FunctionDeclsMatchCallback.cpp b/server/src/fetchers/FunctionDeclsMatchCallback.cpp
@@ -22,6 +22,9 @@ FunctionDeclsMatchCallback::FunctionDeclsMatchCallback(const Fetcher *parent,
 void FunctionDeclsMatchCallback::run(const MatchFinder::MatchResult &Result) {
     ExecUtils::throwIfCancelled();
     if (const FunctionDecl *FS = ClangUtils::getFunctionOrConstructor(Result)) {
+        if (FS->isTemplated()) {
+            return;
+        }
         ExecUtils::throwIfCancelled();
         SourceManager &sourceManager = Result.Context->getSourceManager();
         fs::path sourceFilePath = ClangUtils::getSourceFilePath(sourceManager);

diff --git a/server/src/types/Types.cpp b/server/src/types/Types.cpp
@@ -114,7 +114,7 @@ types::Type types::Type::baseTypeObj(size_t depth) const {
     type.mKinds.erase(type.mKinds.begin(), type.mKinds.begin() + depth);
     type.dimension = type.getDimension();
     type.mTypeId = mBaseTypeId;
-    type.mBaseTypeId = {};
+    type.mBaseTypeId = mBaseTypeId;
     return type;
 }
 

diff --git a/server/src/utils/KleeUtils.h b/server/src/utils/KleeUtils.h
@@ -12,6 +12,9 @@ namespace KleeUtils {
     static inline const std::string RESULT_VARIABLE_NAME = "utbot_result";
     static inline const std::string NOT_NULL_VARIABLE_NAME = "utbot_return_not_null";
 
+    static inline const std::string STDIN_READ_NAME = "stdin_read";
+    static inline const std::string STDIN_NAME = "stdin";
+
     std::string getRenamedOperator(std::string_view methodName);
 
     std::string entryPointFunction(const tests::Tests &tests,

diff --git a/server/src/utils/PrinterUtils.cpp b/server/src/utils/PrinterUtils.cpp
@@ -161,15 +161,15 @@ namespace PrinterUtils {
     }
 
     std::string getFileParamKTestJSON(char fileName) {
-        return StringUtils::stringFormat("%c-data", fileName);
+        return StringUtils::stringFormat("%c_data", fileName);
     }
 
     std::string getFileReadBytesParamKTestJSON(char fileName) {
-        return StringUtils::stringFormat("%c-data-read", fileName);
+        return StringUtils::stringFormat("%c_data_read", fileName);
     }
 
     std::string getFileWriteBytesParamKTestJSON(char fileName) {
-        return StringUtils::stringFormat("%c-data-write", fileName);
+        return StringUtils::stringFormat("%c_data_write", fileName);
     }
 
     void removeThreadLocalQualifiers(std::string &decl) {