Add annotations json parser

include/klee/Core/Interpreter.h

@@ -10,6 +10,7 @@
 #define KLEE_INTERPRETER_H
 
 #include "TerminationTypes.h"
+#include "klee/Module/Annotation.h"
 
 #include "klee/Module/SarifReport.h"
 
@@ -157,7 +158,8 @@ 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) = 0;
+            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;

include/klee/Core/MockBuilder.h

@@ -1,6 +1,8 @@
 #ifndef KLEE_MOCKBUILDER_H
 #define KLEE_MOCKBUILDER_H
 
+#include "klee/Module/Annotation.h"
+
 #include "llvm/IR/IRBuilder.h"
 #include "llvm/IR/Module.h"
 
@@ -15,6 +17,7 @@ class MockBuilder {
   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;
 
@@ -25,11 +28,16 @@ class MockBuilder {
   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);
 
 public:
   MockBuilder(const llvm::Module *initModule, std::string mockEntrypoint,
               std::string userEntrypoint,
-              std::map<std::string, llvm::Type *> externals);
+              std::map<std::string, llvm::Type *> externals,
+              Annotations annotations);
 
   std::unique_ptr<llvm::Module> build();
 };

include/klee/Module/Annotation.h

@@ -0,0 +1,86 @@
+#ifndef KLEE_ANNOTATION_H
+#define KLEE_ANNOTATION_H
+
+#include "map"
+#include "set"
+#include "string"
+#include "vector"
+
+#include "nlohmann/json.hpp"
+#include "nonstd/optional.hpp"
+
+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,
+
+    Deref,
+    InitNull,
+  };
+
+  enum class Property {
+    Unknown,
+
+    Determ,
+    Noreturn,
+  };
+
+  struct StatementUnknown {
+    explicit StatementUnknown(const std::string &str);
+    virtual ~StatementUnknown();
+
+    virtual Annotation::StatementKind getStatementName() const;
+    virtual bool operator==(const StatementUnknown &other) const;
+
+    std::string statementStr;
+    std::vector<std::string> offset;
+
+  protected:
+    void parseOffset(const std::string &offsetStr);
+    void parseOnlyOffset(const std::string &str);
+  };
+
+  struct StatementDeref final : public StatementUnknown {
+    explicit StatementDeref(const std::string &str);
+
+    Annotation::StatementKind getStatementName() const override;
+  };
+
+  struct StatementInitNull final : public StatementUnknown {
+    explicit StatementInitNull(const std::string &str);
+
+    Annotation::StatementKind getStatementName() const override;
+  };
+
+  using StatementPtr = std::shared_ptr<StatementUnknown>;
+  using StatementPtrs = std::vector<StatementPtr>;
+
+  bool operator==(const Annotation &other) const;
+
+  std::string functionName;
+  std::vector<StatementPtrs> statements;
+  std::set<Property> properties;
+};
+
+using Annotations = std::map<std::string, Annotation>;
+
+const std::map<std::string, Annotation::Property> toProperties{
+    {"determ", Annotation::Property::Determ},
+    {"noreturn", Annotation::Property::Noreturn},
+};
+
+Annotations parseAnnotationsFile(const json &annotationsJson);
+Annotations parseAnnotationsFile(const std::string &path);
+
+bool operator==(const Annotation::StatementPtr &first,
+                const Annotation::StatementPtr &second);
+
+} // namespace klee
+
+#endif // KLEE_ANNOTATION_H

lib/Core/Executor.cpp

@@ -537,7 +537,8 @@ 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 std::set<std::string> &ignoredExternals,
+                    const Annotations &annotations) {
   assert(!kmodule && !userModules.empty() &&
          "can only register one module"); // XXX gross
 
@@ -582,7 +583,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);
+                        opts.MainNameAfterMock, externals, annotations);
     std::unique_ptr<llvm::Module> mockModule = builder.build();
     if (!mockModule) {
       klee_error("Unable to generate mocks");

lib/Core/Executor.h

@@ -733,7 +733,8 @@ 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) override;
+            const std::set<std::string> &ignoredExternals,
+            const Annotations &annotations) override;
 
   std::map<std::string, llvm::Type *>
   getAllExternals(const std::set<std::string> &ignoredExternals) override;

lib/Core/MockBuilder.cpp

@@ -1,17 +1,21 @@
 #include "klee/Core/MockBuilder.h"
 
+#include "klee/Module/Annotation.h"
 #include "klee/Support/ErrorHandling.h"
 #include "llvm/IR/IRBuilder.h"
 #include "llvm/IR/Module.h"
 
 #include <memory>
+#include <utility>
 
 namespace klee {
 
 MockBuilder::MockBuilder(const llvm::Module *initModule,
                          std::string mockEntrypoint, std::string userEntrypoint,
-                         std::map<std::string, llvm::Type *> externals)
+                         std::map<std::string, llvm::Type *> externals,
+                         Annotations annotations)
     : userModule(initModule), externals(std::move(externals)),
+      annotations(std::move(annotations)),
       mockEntrypoint(std::move(mockEntrypoint)),
       userEntrypoint(std::move(userEntrypoint)) {}
 
@@ -115,6 +119,11 @@ void MockBuilder::buildExternalFunctionsDefinitions() {
       continue;
     }
 
+    const auto annotation = annotations.find(extName);
+    if (annotation != annotations.end()) {
+      buildAnnotationForExternalFunctionParams(func, annotation->second);
+    }
+
     auto *mockReturnValue =
         builder->CreateAlloca(func->getReturnType(), nullptr);
     buildCallKleeMakeSymbol("klee_make_mock", mockReturnValue,
@@ -149,4 +158,67 @@ void MockBuilder::buildCallKleeMakeSymbol(const std::string &klee_function_name,
        gep});
 }
 
+// TODO: add method for return value of external functions.
+void MockBuilder::buildAnnotationForExternalFunctionParams(
+    llvm::Function *func, Annotation &annotation) {
+  for (size_t i = 1; i < annotation.statements.size(); i++) {
+    const auto arg = func->getArg(i - 1);
+    for (const auto &statement : annotation.statements[i]) {
+      llvm::Value *elem = goByOffset(arg, statement->offset);
+      switch (statement->getStatementName()) {
+      case Annotation::StatementKind::Deref: {
+        if (!elem->getType()->isPointerTy()) {
+          klee_error("Incorrect annotation offset.");
+        }
+        builder->CreateLoad(elem);
+        break;
+      }
+      case Annotation::StatementKind::InitNull: {
+        // TODO
+      }
+      case Annotation::StatementKind::Unknown:
+      default:
+        __builtin_unreachable();
+      }
+    }
+  }
+
+  for (const auto &property : annotation.properties) {
+    switch (property) {
+    case Annotation::Property::Determ: {
+      // TODO
+    }
+    case Annotation::Property::Noreturn: {
+      // TODO
+    }
+    case Annotation::Property::Unknown:
+    default:
+      __builtin_unreachable();
+    }
+  }
+}
+
+llvm::Value *MockBuilder::goByOffset(llvm::Value *value,
+                                     const std::vector<std::string> &offset) {
+  llvm::Value *current = value;
+  for (const auto &inst : offset) {
+    if (inst == "*") {
+      if (!current->getType()->isPointerTy()) {
+        klee_error("Incorrect annotation offset.");
+      }
+      current = builder->CreateLoad(current);
+    } else if (inst == "&") {
+      auto addr = builder->CreateAlloca(current->getType());
+      current = builder->CreateStore(current, addr);
+    } else {
+      const size_t index = std::stol(inst);
+      if (!(current->getType()->isPointerTy() || current->getType()->isArrayTy())) {
+        klee_error("Incorrect annotation offset.");
+      }
+      current = builder->CreateConstInBoundsGEP1_64(current, index);
+    }
+  }
+  return current;
+}
+
 } // namespace klee