Add annotation implementation and tests

UnitTestBot · Aug 29, 2023 · a1aa217 · a1aa217
1 parent cb4a318
commit a1aa217
Show file tree

Hide file tree

Showing 39 changed files with 1,724 additions and 498 deletions.
diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml
@@ -139,7 +139,6 @@ jobs:
     runs-on: macos-latest
     env:
       BASE: /tmp
-      LLVM_VERSION: 11
       SOLVERS: STP
       UCLIBC_VERSION: 0
       USE_TCMALLOC: 0

diff --git a/.gitmodules b/.gitmodules
@@ -1,6 +1,9 @@
 [submodule "json"]
-	path = json
+	path = submodules/json
 	url = https://github.com/nlohmann/json.git
 [submodule "optional"]
-	path = optional
+	path = submodules/optional
 	url = https://github.com/martinmoene/optional-lite.git
+[submodule "submodules/pugixml"]
+	path = submodules/pugixml
+	url = https://github.com/zeux/pugixml.git
diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -657,8 +657,21 @@ configure_file(${CMAKE_SOURCE_DIR}/include/klee/Config/CompileTimeInfo.h.cmin
 ################################################################################
 include_directories("${CMAKE_BINARY_DIR}/include")
 include_directories("${CMAKE_SOURCE_DIR}/include")
-include_directories("${CMAKE_SOURCE_DIR}/json/include")
-include_directories("${CMAKE_SOURCE_DIR}/optional/include")
+include_directories("${CMAKE_SOURCE_DIR}/submodules/json/include")
+include_directories("${CMAKE_SOURCE_DIR}/submodules/optional/include")
+
+
+option(ENABLE_XML_ANNOTATION "Enable XML annotation" ON)
+
+if (ENABLE_XML_ANNOTATION)
+  message(STATUS "XML annotation is enabled")
+  file(COPY "${CMAKE_SOURCE_DIR}/submodules/pugiconfig.hpp"
+          DESTINATION "${CMAKE_SOURCE_DIR}/submodules/pugixml/src")
+  include_directories("${CMAKE_SOURCE_DIR}/submodules/pugixml/src")
+else()
+  message(STATUS "XML annotation is disabled")
+  set(ENABLE_XML_ANNOTATION 0)
+endif()
 # set(KLEE_INCLUDE_DIRS ${CMAKE_SOURCE_DIR}/include ${CMAKE_BINARY_DIR}/include)
 
 ################################################################################

diff --git a/include/klee/Config/config.h.cmin b/include/klee/Config/config.h.cmin
@@ -119,4 +119,7 @@ macro for that. That would simplify the C++ code.  */
 /* Install directory for KLEE runtime */
 #define KLEE_INSTALL_RUNTIME_DIR "@KLEE_INSTALL_RUNTIME_DIR@"
 
+/* Enable XML annotation parser */
+#define ENABLE_XML_ANNOTATION "@ENABLE_XML_ANNOTATION@"
+
 #endif /* KLEE_CONFIG_H */
diff --git a/include/klee/Core/Interpreter.h b/include/klee/Core/Interpreter.h
@@ -88,25 +88,31 @@ class Interpreter {
     std::string OptSuffix;
     std::string MainCurrentName;
     std::string MainNameAfterMock;
+    std::string AnnotationsFile;
     bool Optimize;
     bool Simplify;
     bool CheckDivZero;
     bool CheckOvershift;
+    bool AnnotateOnlyExternal;
     bool WithFPRuntime;
     bool WithPOSIXRuntime;
 
     ModuleOptions(const std::string &_LibraryDir,
                   const std::string &_EntryPoint, const std::string &_OptSuffix,
                   const std::string &_MainCurrentName,
-                  const std::string &_MainNameAfterMock, bool _Optimize,
+                  const std::string &_MainNameAfterMock,
+                  const std::string &_AnnotationsFile, bool _Optimize,
                   bool _Simplify, bool _CheckDivZero, bool _CheckOvershift,
-                  bool _WithFPRuntime, bool _WithPOSIXRuntime)
+                  bool _AnnotateOnlyExternal, bool _WithFPRuntime,
+                  bool _WithPOSIXRuntime)
         : LibraryDir(_LibraryDir), EntryPoint(_EntryPoint),
           OptSuffix(_OptSuffix), MainCurrentName(_MainCurrentName),
-          MainNameAfterMock(_MainNameAfterMock), Optimize(_Optimize),
+          MainNameAfterMock(_MainNameAfterMock),
+          AnnotationsFile(_AnnotationsFile), Optimize(_Optimize),
           Simplify(_Simplify), CheckDivZero(_CheckDivZero),
-          CheckOvershift(_CheckOvershift), WithFPRuntime(_WithFPRuntime),
-          WithPOSIXRuntime(_WithPOSIXRuntime) {}
+          CheckOvershift(_CheckOvershift),
+          AnnotateOnlyExternal(_AnnotateOnlyExternal),
+          WithFPRuntime(_WithFPRuntime), WithPOSIXRuntime(_WithPOSIXRuntime) {}
   };
 
   enum LogType {
@@ -159,10 +165,7 @@ class Interpreter {
             const std::unordered_set<std::string> &mainModuleGlobals,
             std::unique_ptr<InstructionInfoTable> origInfos,
             const std::set<std::string> &ignoredExternals,
-            const Annotations &annotations) = 0;
-
-  virtual std::map<std::string, llvm::Type *>
-  getAllExternals(const std::set<std::string> &ignoredExternals) = 0;
+            std::vector<std::pair<std::string, std::string>> redefinitions) = 0;
 
   // supply a tree stream writer which the interpreter will use
   // to record the concrete path (as a stream of '0' and '1' bytes).

diff --git a/include/klee/Core/MockBuilder.h b/include/klee/Core/MockBuilder.h
@@ -1,6 +1,7 @@
 #ifndef KLEE_MOCKBUILDER_H
 #define KLEE_MOCKBUILDER_H
 
+#include "klee/Core/Interpreter.h"
 #include "klee/Module/Annotation.h"
 
 #include "llvm/IR/IRBuilder.h"
@@ -16,30 +17,52 @@ class MockBuilder {
   const llvm::Module *userModule;
   std::unique_ptr<llvm::Module> mockModule;
   std::unique_ptr<llvm::IRBuilder<>> builder;
-  std::map<std::string, llvm::Type *> externals;
-  Annotations annotations;
 
-  const std::string mockEntrypoint, userEntrypoint;
+  const Interpreter::ModuleOptions &opts;
+
+  std::set<std::string> ignoredExternals;
+  std::vector<std::pair<std::string, std::string>> redefinitions;
+
+  InterpreterHandler *interpreterHandler;
+
+  AnnotationsMap annotations;
 
   void initMockModule();
   void buildMockMain();
   void buildExternalGlobalsDefinitions();
   void buildExternalFunctionsDefinitions();
-  void buildCallKleeMakeSymbol(const std::string &klee_function_name,
-                               llvm::Value *source, llvm::Type *type,
-                               const std::string &symbol_name);
-  void buildAnnotationForExternalFunctionParams(llvm::Function *func,
-                                          Annotation &annotation);
-  llvm::Value *goByOffset(llvm::Value *value,
-                          const std::vector<std::string> &offset);
+  void
+  buildCallKleeMakeSymbolic(const std::string &kleeMakeSymbolicFunctionName,
+                            llvm::Value *source, llvm::Type *type,
+                            const std::string &symbolicName);
+
+  void buildAnnotationForExternalFunctionArgs(
+      llvm::Function *func,
+      const std::vector<std::vector<Statement::Ptr>> &statementsNotAllign);
+  void buildAnnotationForExternalFunctionReturn(
+      llvm::Function *func, const std::vector<Statement::Ptr> &statements);
+  void buildAnnotationForExternalFunctionProperties(
+      llvm::Function *func, const std::set<Statement::Property> &properties);
+
+  std::map<std::string, llvm::FunctionType *> getExternalFunctions();
+  std::map<std::string, llvm::Type *> getExternalGlobals();
+
+  std::pair<llvm::Value *, llvm::Value *>
+  goByOffset(llvm::Value *value, const std::vector<std::string> &offset);
 
 public:
-  MockBuilder(const llvm::Module *initModule, std::string mockEntrypoint,
-              std::string userEntrypoint,
-              std::map<std::string, llvm::Type *> externals,
-              Annotations annotations);
+  MockBuilder(const llvm::Module *initModule,
+              const Interpreter::ModuleOptions &opts,
+              const std::set<std::string> &ignoredExternals,
+              std::vector<std::pair<std::string, std::string>> &redefinitions,
+              InterpreterHandler *interpreterHandler);
 
   std::unique_ptr<llvm::Module> build();
+  void buildAllocSource(llvm::Value *prev, llvm::Type *elemType,
+                        const Statement::AllocSource *allocSourcePtr);
+  void processingValue(llvm::Value *prev, llvm::Type *elemType,
+                       const Statement::AllocSource *allocSourcePtr,
+                       const Statement::InitNull *initNullPtr);
 };
 
 } // namespace klee

diff --git a/include/klee/Module/Annotation.h b/include/klee/Module/Annotation.h
@@ -9,78 +9,98 @@
 #include "nlohmann/json.hpp"
 #include "nonstd/optional.hpp"
 
+#include "klee/Config/config.h"
+
+#include "llvm/IR/Module.h"
+
 using nonstd::nullopt;
 using nonstd::optional;
 using json = nlohmann::json;
 
 namespace klee {
 
-// Annotation format: https://github.com/UnitTestBot/klee/discussions/92
-struct Annotation {
-  enum class StatementKind {
-    Unknown,
+namespace Statement {
+enum class Kind {
+  Unknown,
 
-    Deref,
-    InitNull,
-  };
+  Deref,
+  InitNull,
+  AllocSource,
+};
 
-  enum class Property {
-    Unknown,
+enum class Property {
+  Unknown,
 
-    Determ,
-    Noreturn,
-  };
+  Deterministic,
+  Noreturn,
+};
 
-  struct StatementUnknown {
-    explicit StatementUnknown(const std::string &str);
-    virtual ~StatementUnknown();
+struct Unknown {
+protected:
+  std::string rawAnnotation;
+  std::string rawOffset;
+  std::string rawValue;
 
-    virtual Annotation::StatementKind getStatementName() const;
-    virtual bool operator==(const StatementUnknown &other) const;
+public:
+  std::vector<std::string> offset;
 
-    std::string statementStr;
-    std::vector<std::string> offset;
+  explicit Unknown(const std::string &str = "Unknown");
+  virtual ~Unknown();
 
-  protected:
-    void parseOffset(const std::string &offsetStr);
-    void parseOnlyOffset(const std::string &str);
-  };
+  virtual bool operator==(const Unknown &other) const;
+  [[nodiscard]] virtual Kind getKind() const;
 
-  struct StatementDeref final : public StatementUnknown {
-    explicit StatementDeref(const std::string &str);
+  [[nodiscard]] const std::vector<std::string> &getOffset() const;
+  [[nodiscard]] std::string toString() const;
+};
 
-    Annotation::StatementKind getStatementName() const override;
-  };
+struct Deref final : public Unknown {
+  explicit Deref(const std::string &str = "Deref");
 
-  struct StatementInitNull final : public StatementUnknown {
-    explicit StatementInitNull(const std::string &str);
+  [[nodiscard]] Kind getKind() const override;
+};
 
-    Annotation::StatementKind getStatementName() const override;
+struct InitNull final : public Unknown {
+  explicit InitNull(const std::string &str = "InitNull");
+
+  [[nodiscard]] Kind getKind() const override;
+};
+
+struct AllocSource final : public Unknown {
+public:
+  enum Type {
+    Alloc = 1,       // malloc, calloc, realloc
+    New = 2,         // operator new
+    NewBrackets = 3, // operator new[]
+    OpenFile = 4,    // open file (fopen, open)
+    MutexLock = 5    // mutex lock (pthread_mutex_lock)
   };
 
-  using StatementPtr = std::shared_ptr<StatementUnknown>;
-  using StatementPtrs = std::vector<StatementPtr>;
+  Type value;
 
-  bool operator==(const Annotation &other) const;
+  explicit AllocSource(const std::string &str = "AllocSource::1");
 
-  std::string functionName;
-  std::vector<StatementPtrs> statements;
-  std::set<Property> properties;
+  [[nodiscard]] Kind getKind() const override;
 };
 
-using Annotations = std::map<std::string, Annotation>;
+using Ptr = std::shared_ptr<Unknown>;
+bool operator==(const Ptr &first, const Ptr &second);
+} // namespace Statement
 
-const std::map<std::string, Annotation::Property> toProperties{
-    {"determ", Annotation::Property::Determ},
-    {"noreturn", Annotation::Property::Noreturn},
-};
+// Annotation format: https://github.com/UnitTestBot/klee/discussions/92
+struct Annotation {
+  std::string functionName;
+  std::vector<Statement::Ptr> returnStatements;
+  std::vector<std::vector<Statement::Ptr>> argsStatements;
+  std::set<Statement::Property> properties;
 
-Annotations parseAnnotationsFile(const json &annotationsJson);
-Annotations parseAnnotationsFile(const std::string &path);
+  bool operator==(const Annotation &other) const;
+};
 
-bool operator==(const Annotation::StatementPtr &first,
-                const Annotation::StatementPtr &second);
+using AnnotationsMap = std::map<std::string, Annotation>;
 
+AnnotationsMap parseAnnotationsJson(const json &annotationsJson);
+AnnotationsMap parseAnnotations(const std::string &path, const llvm::Module *m);
 } // namespace klee
 
 #endif // KLEE_ANNOTATION_H
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
@@ -23,10 +23,10 @@
 #include "klee/Support/CompilerWarning.h"
 DISABLE_WARNING_PUSH
 DISABLE_WARNING_DEPRECATED_DECLARATIONS
+#include "klee/Support/ErrorHandling.h"
 #include "llvm/IR/Function.h"
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/raw_ostream.h"
-#include "klee/Support/ErrorHandling.h"
 DISABLE_WARNING_POP
 
 #include <cassert>