[fix] Update build.yaml and add come fixes

UnitTestBot · Jul 24, 2023 · 6c48e67 · 6c48e67
1 parent 5d4ff44
commit 6c48e67
Show file tree

Hide file tree

Showing 112 changed files with 443 additions and 89 deletions.
diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml
@@ -21,7 +21,6 @@ env:
   LLVM_VERSION: 11
   MINISAT_VERSION: "master"
   REQUIRES_RTTI: 0
-  SOLVERS: STP:Z3
   STP_VERSION: 2.3.3
   TCMALLOC_VERSION: 2.9.1
   UCLIBC_VERSION: klee_uclibc_v1.3
@@ -56,35 +55,43 @@ jobs:
           - name: "LLVM 14"
             env:
               LLVM_VERSION: 14
+              SOLVERS: Z3
           - name: "LLVM 13"
             env:
               LLVM_VERSION: 13
+              SOLVERS: Z3
           - name: "LLVM 12"
             env:
               LLVM_VERSION: 12
+              SOLVERS: Z3
           - name: "LLVM 11, Doxygen"
             env:
               LLVM_VERSION: 11
               ENABLE_DOXYGEN: 1
+              SOLVERS: Z3
           - name: "LLVM 10"
             env:
               LLVM_VERSION: 10
+              SOLVERS: Z3
           - name: "LLVM 9"
             env:
               LLVM_VERSION: 9
+              SOLVERS: Z3
           # Sanitizer builds. Do unoptimized build otherwise the optimizer
           # might remove problematic code
           - name: "ASan"
             env:
               SANITIZER_BUILD: address
               ENABLE_OPTIMIZED: 0
               USE_TCMALLOC: 0
+              SOLVERS: STP
               SANITIZER_LLVM_VERSION: 12
           - name: "UBSan"
             env:
               SANITIZER_BUILD: undefined
               ENABLE_OPTIMIZED: 0
               USE_TCMALLOC: 0
+              SOLVERS: STP
               SANITIZER_LLVM_VERSION: 12
           - name: "MSan"
             env:
@@ -112,6 +119,7 @@ jobs:
           # Check we can build latest klee-uclibc branch
           - name: "Latest klee-uclibc"
             env:
+              SOLVERS: Z3
               UCLIBC_VERSION: klee_0_9_29
           # Check at least one build with Asserts disabled.
           - name: "Asserts disabled"
@@ -121,6 +129,7 @@ jobs:
           # Check without TCMALLOC and with an optimised runtime library
           - name: "No TCMalloc, optimised runtime"
             env:
+              SOLVERS: STP
               USE_TCMALLOC: 0
               KLEE_RUNTIME_BUILD: "Release+Debug+Asserts"
     steps:
@@ -132,6 +141,7 @@ jobs:
         env: ${{ matrix.env }}
         run: scripts/build/build.sh klee --docker --create-final-image
       - name: Run tests
+        env: ${{ matrix.env }}
         run: scripts/build/run-tests.sh --run-docker --debug
 
   macOS:
@@ -175,7 +185,7 @@ jobs:
         include:
           - name: "STP"
             env:
-              SOLVERS: STP:Z3
+              SOLVERS: STP
           - name: "Z3"
             env:
               SOLVERS: Z3
@@ -195,6 +205,7 @@ jobs:
         env: ${{ matrix.env }}
         run: scripts/build/build.sh klee --docker --create-final-image
       - name: Run tests
+        env: ${{ matrix.env }}
         run: scripts/build/run-tests.sh --coverage --upload-coverage --run-docker --debug
 
   clang-format:

diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -17,7 +17,7 @@ project(KLEE CXX C)
 # Project version
 ###############################################################################
 set(KLEE_VERSION_MAJOR 3)
-set(KLEE_VERSION_MINOR 0)
+set(KLEE_VERSION_MINOR 0-utbot)
 set(KLEE_VERSION "${KLEE_VERSION_MAJOR}.${KLEE_VERSION_MINOR}")
 
 # If a patch is needed, we can add KLEE_VERSION_PATCH

diff --git a/build.sh b/build.sh
@@ -35,7 +35,7 @@ REQUIRES_RTTI=1
 
 ## Solvers Required options
 # SOLVERS=STP
-SOLVERS=Z3
+SOLVERS=STP:Z3
 
 ## Google Test Required options
 GTEST_VERSION=1.11.0

diff --git a/include/klee/ADT/Bits.h b/include/klee/ADT/Bits.h
@@ -12,7 +12,11 @@
 
 #include "klee/Config/Version.h"
 
+#include "klee/Support/CompilerWarning.h"
+DISABLE_WARNING_PUSH
+DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/Support/DataTypes.h"
+DISABLE_WARNING_POP
 
 #include <cassert>
 #include <cstddef>

diff --git a/include/klee/Expr/IndependentSet.h b/include/klee/Expr/IndependentSet.h
@@ -4,7 +4,13 @@
 #include "klee/Expr/Expr.h"
 #include "klee/Expr/ExprHashMap.h"
 #include "klee/Solver/Solver.h"
+
+#include "klee/Support/CompilerWarning.h"
+DISABLE_WARNING_PUSH
+DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/Support/raw_ostream.h"
+DISABLE_WARNING_POP
+
 #include <list>
 #include <set>
 

diff --git a/include/klee/Expr/SymbolicSource.h b/include/klee/Expr/SymbolicSource.h
@@ -3,9 +3,13 @@
 
 #include "klee/ADT/Ref.h"
 
+#include "klee/Support/CompilerWarning.h"
+DISABLE_WARNING_PUSH
+DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/ADT/StringExtras.h"
 #include "llvm/IR/Argument.h"
 #include "llvm/IR/Instruction.h"
+DISABLE_WARNING_POP
 
 #include <set>
 #include <string>

diff --git a/include/klee/Expr/Symcrete.h b/include/klee/Expr/Symcrete.h
@@ -4,7 +4,11 @@
 #include "klee/ADT/Ref.h"
 #include "klee/Expr/ExprUtil.h"
 
+#include "klee/Support/CompilerWarning.h"
+DISABLE_WARNING_PUSH
+DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/Support/Casting.h"
+DISABLE_WARNING_POP
 
 #include <cstdint>
 #include <vector>

diff --git a/include/klee/Module/InstructionInfoTable.h b/include/klee/Module/InstructionInfoTable.h
@@ -10,8 +10,13 @@
 #ifndef KLEE_INSTRUCTIONINFOTABLE_H
 #define KLEE_INSTRUCTIONINFOTABLE_H
 
-#include <llvm/ADT/Optional.h>
-#include <llvm/Support/raw_ostream.h>
+#include "klee/Support/CompilerWarning.h"
+DISABLE_WARNING_PUSH
+DISABLE_WARNING_DEPRECATED_DECLARATIONS
+#include "llvm/ADT/Optional.h"
+#include "llvm/Support/raw_ostream.h"
+DISABLE_WARNING_POP
+
 #include <memory>
 #include <string>
 #include <unordered_map>

diff --git a/include/klee/Module/KInstruction.h b/include/klee/Module/KInstruction.h
@@ -13,8 +13,12 @@
 #include "klee/Config/Version.h"
 #include "klee/Module/InstructionInfoTable.h"
 
+#include "klee/Support/CompilerWarning.h"
+DISABLE_WARNING_PUSH
+DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/Support/DataTypes.h"
 #include "llvm/Support/raw_ostream.h"
+DISABLE_WARNING_POP
 
 #include <vector>
 

diff --git a/include/klee/Module/KModule.h b/include/klee/Module/KModule.h
@@ -15,8 +15,12 @@
 #include "klee/Module/InstructionInfoTable.h"
 #include "klee/Module/KCallable.h"
 
+#include "klee/Support/CompilerWarning.h"
+DISABLE_WARNING_PUSH
+DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/ADT/ArrayRef.h"
 #include "llvm/IR/CFG.h"
+DISABLE_WARNING_POP
 
 #include <deque>
 #include <map>

diff --git a/include/klee/Module/KType.h b/include/klee/Module/KType.h
@@ -18,7 +18,7 @@ class TypeManager;
 
 template <class> class ref;
 
-enum TypeSystemKind { LLVM, CXX };
+enum class TypeSystemKind { Default, Advanced };
 class KType {
   friend TypeManager;
 

diff --git a/include/klee/Module/Target.h b/include/klee/Module/Target.h
@@ -14,12 +14,16 @@
 #include "klee/ADT/Ref.h"
 #include "klee/Module/KModule.h"
 #include "klee/Module/SarifReport.h"
+#include "klee/Support/OptionCategories.h"
 #include "klee/System/Time.h"
 
-#include "klee/Support/OptionCategories.h"
+#include "klee/Support/CompilerWarning.h"
+DISABLE_WARNING_PUSH
+DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/Support/Casting.h"
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/raw_ostream.h"
+DISABLE_WARNING_POP
 
 #include <map>
 #include <queue>

diff --git a/include/klee/Support/Casting.h b/include/klee/Support/Casting.h
@@ -12,7 +12,11 @@
 
 #include "klee/Config/Version.h"
 
+#include "klee/Support/CompilerWarning.h"
+DISABLE_WARNING_PUSH
+DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/Support/Casting.h"
+DISABLE_WARNING_POP
 
 namespace klee {
 

diff --git a/include/klee/Support/CompilerWarning.h b/include/klee/Support/CompilerWarning.h
@@ -7,6 +7,7 @@
 //
 //===----------------------------------------------------------------------===//
 
+// clang-format off
 #ifndef KLEE_INCLUDE_KLEE_SUPPORT_COMPILERWARNING_H
 #define KLEE_INCLUDE_KLEE_SUPPORT_COMPILERWARNING_H
 
@@ -23,8 +24,8 @@
 #if LLVM_VERSION_CODE >= LLVM_VERSION(14, 0)
 #define DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #else
-#define DISABLE_WARNING_DEPRECATED_DECLARATIONS                                \
-  DISABLE_WARNING(-Wdeprecated - declarations)
+#define DISABLE_WARNING_DEPRECATED_DECLARATIONS
+  DISABLE_WARNING(-Wdeprecated-declarations)
 #endif
 
 #else
@@ -37,3 +38,4 @@
 #endif
 
 #endif // KLEE_INCLUDE_KLEE_SUPPORT_COMPILERWARNING_H
+// clang-format off
diff --git a/include/klee/Support/CompressionStream.h b/include/klee/Support/CompressionStream.h
@@ -11,7 +11,12 @@
 #define KLEE_COMPRESSIONSTREAM_H
 
 #include "zlib.h"
+
+#include "klee/Support/CompilerWarning.h"
+DISABLE_WARNING_PUSH
+DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/Support/raw_ostream.h"
+DISABLE_WARNING_POP
 
 namespace klee {
 const size_t BUFSIZE = 128 * 1024;

diff --git a/include/klee/Support/Debug.h b/include/klee/Support/Debug.h
@@ -11,7 +11,12 @@
 #define KLEE_DEBUG_H
 
 #include "klee/Config/config.h"
+
+#include "klee/Support/CompilerWarning.h"
+DISABLE_WARNING_PUSH
+DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/Support/Debug.h"
+DISABLE_WARNING_POP
 
 // We define wrappers around the LLVM DEBUG macros that are conditionalized on
 // whether the LLVM we are building against has the symbols needed by these

diff --git a/include/klee/Support/PrintContext.h b/include/klee/Support/PrintContext.h
@@ -12,7 +12,11 @@
 
 #include "klee/Expr/Expr.h"
 
+#include "klee/Support/CompilerWarning.h"
+DISABLE_WARNING_PUSH
+DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/Support/raw_ostream.h"
+DISABLE_WARNING_POP
 
 #include <sstream>
 #include <stack>

diff --git a/include/klee/Support/RoundingModeUtil.h b/include/klee/Support/RoundingModeUtil.h
@@ -7,7 +7,12 @@
 //
 //===----------------------------------------------------------------------===//
 #ifndef KLEE_ROUNDING_MODE_UTIL_H
+
+#include "klee/Support/CompilerWarning.h"
+DISABLE_WARNING_PUSH
+DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/ADT/APFloat.h"
+DISABLE_WARNING_POP
 
 namespace klee {
 

diff --git a/include/klee/Support/Timer.h b/include/klee/Support/Timer.h
@@ -12,7 +12,11 @@
 
 #include "klee/System/Time.h"
 
+#include "klee/Support/CompilerWarning.h"
+DISABLE_WARNING_PUSH
+DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/ADT/SmallVector.h"
+DISABLE_WARNING_POP
 
 #include <functional>
 #include <memory>

diff --git a/include/klee/util/APFloatEval.h b/include/klee/util/APFloatEval.h
@@ -9,8 +9,13 @@
 
 #ifndef KLEE_APFLOAT_EVAL_H
 #define KLEE_APFLOAT_EVAL_H
+
+#include "klee/Support/CompilerWarning.h"
+DISABLE_WARNING_PUSH
+DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/ADT/APFloat.h"
 #include "llvm/Support/ErrorHandling.h"
+DISABLE_WARNING_POP
 
 namespace klee {
 

diff --git a/lib/Core/CXXTypeSystem/CXXTypeManager.cpp b/lib/Core/CXXTypeSystem/CXXTypeManager.cpp
@@ -8,13 +8,16 @@
 #include "klee/Module/KModule.h"
 #include "klee/Module/KType.h"
 
+#include "klee/Support/CompilerWarning.h"
+DISABLE_WARNING_PUSH
+DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/IR/DebugInfoMetadata.h"
 #include "llvm/IR/DerivedTypes.h"
 #include "llvm/IR/Metadata.h"
 #include "llvm/IR/Module.h"
 #include "llvm/IR/Type.h"
-
 #include "llvm/Support/Casting.h"
+DISABLE_WARNING_POP
 
 #include <algorithm>
 #include <cassert>
@@ -213,7 +216,7 @@ static ref<Expr> getComplexPointerRestrictions(
 /* C++ KType base class */
 cxxtypes::KCXXType::KCXXType(llvm::Type *type, TypeManager *parent)
     : KType(type, parent) {
-  typeSystemKind = TypeSystemKind::CXX;
+  typeSystemKind = TypeSystemKind::Advanced;
   typeKind = DEFAULT;
 }
 
@@ -261,7 +264,7 @@ cxxtypes::CXXTypeKind cxxtypes::KCXXType::getTypeKind() const {
 }
 
 bool cxxtypes::KCXXType::classof(const KType *requestedType) {
-  return requestedType->getTypeSystemKind() == TypeSystemKind::CXX;
+  return requestedType->getTypeSystemKind() == TypeSystemKind::Advanced;
 }
 
 /* Composite type */

diff --git a/lib/Core/CXXTypeSystem/CXXTypeManager.h b/lib/Core/CXXTypeSystem/CXXTypeManager.h
@@ -6,7 +6,11 @@
 #include "klee/Expr/ExprHashMap.h"
 #include "klee/Module/KType.h"
 
+#include "klee/Support/CompilerWarning.h"
+DISABLE_WARNING_PUSH
+DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/Support/raw_ostream.h"
+DISABLE_WARNING_POP
 
 #include <map>
 #include <string>