add xml annotation support

Author: ladisgin

.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

CMakeLists.txt

@@ -657,8 +657,19 @@ 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")
+  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)
 
 ################################################################################

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 */

include/klee/Core/Interpreter.h

@@ -88,6 +88,7 @@ class Interpreter {
     std::string OptSuffix;
     std::string MainCurrentName;
     std::string MainNameAfterMock;
+    std::string AnnotationsFile;
     bool Optimize;
     bool Simplify;
     bool CheckDivZero;
@@ -98,12 +99,14 @@ class Interpreter {
     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)
         : 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) {}
@@ -158,11 +161,7 @@ class Interpreter {
             const std::unordered_set<std::string> &mainModuleFunctions,
             const std::unordered_set<std::string> &mainModuleGlobals,
             std::unique_ptr<InstructionInfoTable> origInfos,
-            const std::set<std::string> &ignoredExternals,
-            const AnnotationsMap &annotations) = 0;
-
-  virtual std::map<std::string, llvm::Type *>
-  getAllExternals(const std::set<std::string> &ignoredExternals) = 0;
+            const std::set<std::string> &ignoredExternals) = 0;
 
   // supply a tree stream writer which the interpreter will use
   // to record the concrete path (as a stream of '0' and '1' bytes).

include/klee/Core/MockBuilder.h

@@ -45,7 +45,7 @@ class MockBuilder {
   MockBuilder(const llvm::Module *initModule, std::string mockEntrypoint,
               std::string userEntrypoint,
               std::map<std::string, llvm::Type *> externals,
-              AnnotationsMap annotations);
+              const std::string &annotationsFile);
 
   std::unique_ptr<llvm::Module> build();
 };

include/klee/Module/Annotation.h

@@ -9,6 +9,10 @@
 #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;
@@ -37,11 +41,11 @@ struct Unknown {
   virtual bool operator==(const Unknown &other) const;
   [[nodiscard]] virtual Kind getKind() const;
 
-  std::string statementStr;
+  std::string str;
   std::vector<std::string> offset;
 
 private:
-  void parseOffset(const std::string &str);
+  void initOffset();
 };
 
 struct Deref final : public Unknown {
@@ -69,16 +73,11 @@ struct Annotation {
   std::vector<Statement::Ptr> returnStatements;
   std::vector<std::vector<Statement::Ptr>> argsStatements;
   std::set<Statement::Property> properties;
-
-  static void printWarrning(const std::string &message,
-                            const std::string &functionName);
 };
 
 using AnnotationsMap = std::map<std::string, Annotation>;
 
-AnnotationsMap parseAnnotationsPath(const std::string &path);
-AnnotationsMap parseAnnotationsJson(const json &annotationsJson);
-
+AnnotationsMap parseAnnotations(const std::string &path, const llvm::Module *m);
 } // namespace klee
 
 #endif // KLEE_ANNOTATION_H

lib/Core/Executor.cpp

@@ -537,8 +537,7 @@ Executor::setModule(std::vector<std::unique_ptr<llvm::Module>> &userModules,
                     const std::unordered_set<std::string> &mainModuleFunctions,
                     const std::unordered_set<std::string> &mainModuleGlobals,
                     std::unique_ptr<InstructionInfoTable> origInfos,
-                    const std::set<std::string> &ignoredExternals,
-                    const AnnotationsMap &annotations) {
+                    const std::set<std::string> &ignoredExternals) {
   assert(!kmodule && !userModules.empty() &&
          "can only register one module"); // XXX gross
 
@@ -583,7 +582,7 @@ Executor::setModule(std::vector<std::unique_ptr<llvm::Module>> &userModules,
     std::map<std::string, llvm::Type *> externals =
         getAllExternals(ignoredExternals);
     MockBuilder builder(kmodule->module.get(), opts.MainCurrentName,
-                        opts.MainNameAfterMock, externals, annotations);
+                        opts.MainNameAfterMock, externals, opts.AnnotationsFile);
     std::unique_ptr<llvm::Module> mockModule = builder.build();
     if (!mockModule) {
       klee_error("Unable to generate mocks");
@@ -662,7 +661,7 @@ Executor::setModule(std::vector<std::unique_ptr<llvm::Module>> &userModules,
 }
 
 std::map<std::string, llvm::Type *>
-Executor::getAllExternals(const std::set<std::string> &ignoredExternals) {
+Executor::getAllExternals(const std::set<std::string> &ignoredExternals) const {
   std::map<std::string, llvm::Type *> externals;
   for (const auto &f : kmodule->module->functions()) {
     if (f.isDeclaration() && !f.use_empty() &&

lib/Core/Executor.h

@@ -421,8 +421,8 @@ class Executor : public Interpreter {
                            KType *type, const ref<SymbolicSource> source,
                            bool isLocal);
 
-//  void executeMakeMock(ExecutionState &state, KInstruction *target,
-//                       std::vector<ref<Expr>> &arguments);
+  //  void executeMakeMock(ExecutionState &state, KInstruction *target,
+  //                       std::vector<ref<Expr>> &arguments);
 
   void updateStateWithSymcretes(ExecutionState &state,
                                 const Assignment &assignment);
@@ -699,6 +699,9 @@ class Executor : public Interpreter {
   const KBlock *getKBlock(const llvm::BasicBlock *bb) const;
   const KFunction *getKFunction(const llvm::Function *f) const;
 
+  std::map<std::string, llvm::Type *>
+  getAllExternals(const std::set<std::string> &ignoredExternals) const;
+
 public:
   Executor(llvm::LLVMContext &ctx, const InterpreterOptions &opts,
            InterpreterHandler *ie);
@@ -733,11 +736,7 @@ class Executor : public Interpreter {
             const std::unordered_set<std::string> &mainModuleFunctions,
             const std::unordered_set<std::string> &mainModuleGlobals,
             std::unique_ptr<InstructionInfoTable> origInfos,
-            const std::set<std::string> &ignoredExternals,
-            const AnnotationsMap &annotations) override;
-
-  std::map<std::string, llvm::Type *>
-  getAllExternals(const std::set<std::string> &ignoredExternals) override;
+            const std::set<std::string> &ignoredExternals) override;
 
   void useSeeds(const std::vector<struct KTest *> *seeds) override {
     usingSeeds = seeds;

lib/Core/MockBuilder.cpp

@@ -14,11 +14,12 @@ namespace klee {
 MockBuilder::MockBuilder(const llvm::Module *initModule,
                          std::string mockEntrypoint, std::string userEntrypoint,
                          std::map<std::string, llvm::Type *> externals,
-                         AnnotationsMap annotations)
+                         const std::string &annotationsFile)
     : userModule(initModule), externals(std::move(externals)),
-      annotations(std::move(annotations)),
       mockEntrypoint(std::move(mockEntrypoint)),
-      userEntrypoint(std::move(userEntrypoint)) {}
+      userEntrypoint(std::move(userEntrypoint)) {
+  annotations = parseAnnotations(annotationsFile, userModule);
+}
 
 std::unique_ptr<llvm::Module> MockBuilder::build() {
   initMockModule();
@@ -41,14 +42,14 @@ void MockBuilder::initMockModule() {
 void MockBuilder::buildMockMain() {
   llvm::Function *userMainFn = userModule->getFunction(userEntrypoint);
   if (!userMainFn) {
-    klee_error("Entry function '%s' not found in module.",
+    klee_error("Mock: Entry function '%s' not found in module",
                userEntrypoint.c_str());
   }
   mockModule->getOrInsertFunction(mockEntrypoint, userMainFn->getFunctionType(),
                                   userMainFn->getAttributes());
   llvm::Function *mockMainFn = mockModule->getFunction(mockEntrypoint);
   if (!mockMainFn) {
-    klee_error("Entry function '%s' not found in module.",
+    klee_error("Mock: Entry function '%s' not found in module",
                mockEntrypoint.c_str());
   }
   auto globalsInitBlock =
@@ -78,7 +79,7 @@ void MockBuilder::buildExternalGlobalsDefinitions() {
     mockModule->getOrInsertGlobal(extName, type);
     auto *global = mockModule->getGlobalVariable(extName);
     if (!global) {
-      klee_error("Unable to add global variable '%s' to module",
+      klee_error("Mock: Unable to add global variable '%s' to module",
                  extName.c_str());
     }
     global->setLinkage(llvm::GlobalValue::ExternalLinkage);
@@ -88,14 +89,16 @@ void MockBuilder::buildExternalGlobalsDefinitions() {
 
     auto *zeroInitializer = llvm::Constant::getNullValue(it.second);
     if (!zeroInitializer) {
-      klee_error("Unable to get zero initializer for '%s'", extName.c_str());
+      klee_error("Mock: Unable to get zero initializer for '%s'",
+                 extName.c_str());
     }
     global->setInitializer(zeroInitializer);
     buildCallKleeMakeSymbolic("klee_make_symbolic", global, type,
                               "external_" + extName);
   }
 }
 
+// TODO: discuss should we annotate not external function
 void MockBuilder::buildExternalFunctionsDefinitions() {
   for (const auto &it : externals) {
     if (!it.second->isFunctionTy()) {
@@ -106,7 +109,8 @@ void MockBuilder::buildExternalFunctionsDefinitions() {
     mockModule->getOrInsertFunction(extName, type);
     llvm::Function *func = mockModule->getFunction(extName);
     if (!func) {
-      klee_error("Unable to find function '%s' in module", extName.c_str());
+      klee_error("Mock: Unable to find function '%s' in module",
+                 extName.c_str());
     }
     if (!func->empty()) {
       continue;
@@ -322,7 +326,7 @@ void MockBuilder::buildAnnotationForExternalFunctionReturn(
     switch (statement->getKind()) {
     case Statement::Kind::Deref:
       klee_warning("Annotation: unused Deref for return function \"%s\"",
-                   func->getName());
+                   func->getName().str().c_str());
       break;
     case Statement::Kind::InitNull: {
       if (!returnType->isPointerTy()) {