Annotations

configs/options.json

@@ -18,21 +18,20 @@
             "program": "${buildPath}/bin/klee",
             "args": [
                 "--use-guided-search=error",
-                "--mock-external-calls",
                 "--posix-runtime",
                 "--check-out-of-memory",
                 "--suppress-external-warnings",
                 "--libc=klee",
                 "--skip-not-lazy-initialized",
                 "--external-calls=all",
+                "--mock-policy=all",
                 "--output-source=false",
                 "--output-istats=false",
                 "--output-stats=false",
                 "--max-time=${maxTime}s",
                 "--max-sym-alloc=${maxSymAlloc}",
                 "--max-forks=${maxForks}",
                 "--max-solver-time=${maxSolverTime}s",
-                "--mock-all-externals",
                 "--smart-resolve-entry-function",
                 "--extern-calls-can-return-null",
                 "--align-symbolic-pointers=false",
@@ -49,4 +48,4 @@
             ]
         }
     ]
-}
+}

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"
 
@@ -29,6 +30,7 @@ class BasicBlock;
 class Function;
 class LLVMContext;
 class Module;
+class Type;
 class raw_ostream;
 class raw_fd_ostream;
 } // namespace llvm
@@ -63,6 +65,23 @@ using FLCtoOpcode = std::unordered_map<
     std::unordered_map<
         unsigned, std::unordered_map<unsigned, std::unordered_set<unsigned>>>>;
 
+enum class MockStrategyKind {
+  Naive,        // For each function call new symbolic value is generated
+  Deterministic // Each function is treated as uninterpreted function in SMT.
+                // Compatible with Z3 solver only
+};
+
+enum class MockPolicy {
+  None,   // No mock function generated
+  Failed, // Generate symbolic value for failed external calls
+  All     // Generate IR module with all external values
+};
+
+enum class MockMutableGlobalsPolicy {
+  None, // No mock for globals
+  All,  // Mock globals on module build stage and generate bc module for it
+};
+
 class Interpreter {
 public:
   enum class GuidanceKind {
@@ -79,21 +98,32 @@ class Interpreter {
     std::string LibraryDir;
     std::string EntryPoint;
     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,
-                  bool _Optimize, bool _Simplify, bool _CheckDivZero,
-                  bool _CheckOvershift, bool _WithFPRuntime,
+                  const std::string &_MainCurrentName,
+                  const std::string &_MainNameAfterMock,
+                  const std::string &_AnnotationsFile, bool _Optimize,
+                  bool _Simplify, bool _CheckDivZero, bool _CheckOvershift,
+                  bool _AnnotateOnlyExternal, bool _WithFPRuntime,
                   bool _WithPOSIXRuntime)
         : LibraryDir(_LibraryDir), EntryPoint(_EntryPoint),
-          OptSuffix(_OptSuffix), Optimize(_Optimize), Simplify(_Simplify),
-          CheckDivZero(_CheckDivZero), CheckOvershift(_CheckOvershift),
+          OptSuffix(_OptSuffix), MainCurrentName(_MainCurrentName),
+          MainNameAfterMock(_MainNameAfterMock),
+          AnnotationsFile(_AnnotationsFile), Optimize(_Optimize),
+          Simplify(_Simplify), CheckDivZero(_CheckDivZero),
+          CheckOvershift(_CheckOvershift),
+          AnnotateOnlyExternal(_AnnotateOnlyExternal),
           WithFPRuntime(_WithFPRuntime), WithPOSIXRuntime(_WithPOSIXRuntime) {}
   };
 
@@ -112,10 +142,15 @@ class Interpreter {
     unsigned MakeConcreteSymbolic;
     GuidanceKind Guidance;
     std::optional<SarifReport> Paths;
+    MockPolicy Mock;
+    MockStrategyKind MockStrategy;
+    MockMutableGlobalsPolicy MockMutableGlobals;
 
     InterpreterOptions(std::optional<SarifReport> Paths)
         : MakeConcreteSymbolic(false), Guidance(GuidanceKind::NoGuidance),
-          Paths(std::move(Paths)) {}
+          Paths(std::move(Paths)), Mock(MockPolicy::None),
+          MockStrategy(MockStrategyKind::Naive),
+          MockMutableGlobals(MockMutableGlobalsPolicy::None) {}
   };
 
 protected:
@@ -138,13 +173,13 @@ class Interpreter {
   ///                module
   /// \return The final module after it has been optimized, checks
   /// inserted, and modified for interpretation.
-  virtual llvm::Module *
-  setModule(std::vector<std::unique_ptr<llvm::Module>> &userModules,
-            std::vector<std::unique_ptr<llvm::Module>> &libsModules,
-            const ModuleOptions &opts,
-            std::set<std::string> &&mainModuleFunctions,
-            std::set<std::string> &&mainModuleGlobals,
-            FLCtoOpcode &&origInstructions) = 0;
+  virtual llvm::Module *setModule(
+      std::vector<std::unique_ptr<llvm::Module>> &userModules,
+      std::vector<std::unique_ptr<llvm::Module>> &libsModules,
+      const ModuleOptions &opts, std::set<std::string> &&mainModuleFunctions,
+      std::set<std::string> &&mainModuleGlobals, FLCtoOpcode &&origInstructions,
+      const std::set<std::string> &ignoredExternals,
+      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).

include/klee/Core/MockBuilder.h

@@ -0,0 +1,87 @@
+//===-- MockBuilder.h -------------------------------------------*- C++ -*-===//
+//
+//                     The KLEEF Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_MOCKBUILDER_H
+#define KLEE_MOCKBUILDER_H
+
+#include "klee/Core/Interpreter.h"
+#include "klee/Module/Annotation.h"
+
+#include "llvm/IR/IRBuilder.h"
+#include "llvm/IR/Module.h"
+
+#include <set>
+#include <string>
+
+namespace klee {
+
+class MockBuilder {
+private:
+  const llvm::Module *userModule;
+  llvm::LLVMContext &ctx;
+  std::unique_ptr<llvm::Module> mockModule;
+  std::unique_ptr<llvm::IRBuilder<>> builder;
+
+  const Interpreter::ModuleOptions &opts;
+  const Interpreter::InterpreterOptions &interpreterOptions;
+
+  std::set<std::string> ignoredExternals;
+  std::vector<std::pair<std::string, std::string>> redefinitions;
+
+  InterpreterHandler *interpreterHandler;
+
+  std::set<std::string> &mainModuleFunctions;
+  std::set<std::string> &mainModuleGlobals;
+
+  AnnotationsMap annotations;
+
+  void initMockModule();
+  void buildMockMain();
+  void buildExternalGlobalsDefinitions();
+  void buildExternalFunctionsDefinitions();
+  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,
+              const Interpreter::ModuleOptions &opts,
+              const Interpreter::InterpreterOptions &interpreterOptions,
+              const std::set<std::string> &ignoredExternals,
+              std::vector<std::pair<std::string, std::string>> &redefinitions,
+              InterpreterHandler *interpreterHandler,
+              std::set<std::string> &mainModuleFunctions,
+              std::set<std::string> &mainModuleGlobals);
+
+  std::unique_ptr<llvm::Module> build();
+  void buildAllocSource(llvm::Value *prev, llvm::Type *elemType,
+                        const Statement::Alloc *allocSourcePtr);
+  void buildFree(llvm::Value *elem, const Statement::Free *freePtr);
+  void processingValue(llvm::Value *prev, llvm::Type *elemType,
+                       const Statement::Alloc *allocSourcePtr,
+                       bool initNullPtr);
+};
+
+} // namespace klee
+
+#endif // KLEE_MOCKBUILDER_H

include/klee/Expr/AlphaBuilder.h

@@ -34,7 +34,7 @@ class AlphaBuilder final : public ExprVisitor {
 
 public:
   AlphaBuilder(ArrayCache &_arrayCache);
-  constraints_ty visitConstraints(constraints_ty cs);
+  constraints_ty visitConstraints(const constraints_ty &cs);
   ref<Expr> build(ref<Expr> v);
   const Array *buildArray(const Array *arr) { return visitArray(arr); }
   ref<Expr> reverseBuild(ref<Expr> v);

include/klee/Expr/IndependentSet.h

@@ -120,6 +120,8 @@ class IndependentConstraintSet {
 
   std::shared_ptr<InnerSetUnion> concretizedSets;
 
+  std::set<std::string> uninterpretedFunctions;
+
   ref<const IndependentConstraintSet> addExpr(ref<Expr> e) const;
   ref<const IndependentConstraintSet>
   updateConcretization(const Assignment &delta,

include/klee/Expr/SourceBuilder.h

@@ -39,6 +39,12 @@ class SourceBuilder {
   static ref<SymbolicSource> value(const llvm::Value &_allocSite, int _index,
                                    KModule *km);
   static ref<SymbolicSource> irreproducible(const std::string &name);
+  static ref<SymbolicSource> mockNaive(const KModule *kModule,
+                                       const llvm::Function &kFunction,
+                                       unsigned version);
+  static ref<SymbolicSource>
+  mockDeterministic(const KModule *kModule, const llvm::Function &kFunction,
+                    const std::vector<ref<Expr>> &args);
   static ref<SymbolicSource> alpha(int _index);
 };
 

include/klee/Expr/SymbolicSource.h

@@ -20,11 +20,13 @@ DISABLE_WARNING_POP
 
 namespace klee {
 
+class Expr;
 class Array;
 class Expr;
 class ConstantExpr;
 struct KGlobalVariable;
 class KModule;
+struct KFunction;
 struct KValue;
 struct KInstruction;
 
@@ -48,6 +50,8 @@ class SymbolicSource {
     Instruction,
     Argument,
     Irreproducible,
+    MockNaive,
+    MockDeterministic,
     Alpha
   };
 
@@ -357,8 +361,8 @@ class AlphaSource : public SymbolicSource {
   const unsigned index;
 
   AlphaSource(unsigned _index) : index(_index) {}
-  Kind getKind() const override { return Kind::Alpha; }
-  virtual std::string getName() const override { return "alpha"; }
+  [[nodiscard]] Kind getKind() const override { return Kind::Alpha; }
+  [[nodiscard]] virtual std::string getName() const override { return "alpha"; }
 
   static bool classof(const SymbolicSource *S) {
     return S->getKind() == Kind::Alpha;
@@ -383,6 +387,62 @@ class AlphaSource : public SymbolicSource {
   }
 };
 
+class MockSource : public SymbolicSource {
+public:
+  const KModule *km;
+  const llvm::Function &function;
+  MockSource(const KModule *_km, const llvm::Function &_function)
+      : km(_km), function(_function) {}
+
+  static bool classof(const SymbolicSource *S) {
+    return S->getKind() == Kind::MockNaive ||
+           S->getKind() == Kind::MockDeterministic;
+  }
+};
+
+class MockNaiveSource : public MockSource {
+public:
+  const unsigned version;
+
+  MockNaiveSource(const KModule *km, const llvm::Function &function,
+                  unsigned _version)
+      : MockSource(km, function), version(_version) {}
+
+  [[nodiscard]] Kind getKind() const override { return Kind::MockNaive; }
+  [[nodiscard]] std::string getName() const override { return "mockNaive"; }
+
+  static bool classof(const SymbolicSource *S) {
+    return S->getKind() == Kind::MockNaive;
+  }
+
+  unsigned computeHash() override;
+
+  [[nodiscard]] int internalCompare(const SymbolicSource &b) const override;
+};
+
+class MockDeterministicSource : public MockSource {
+public:
+  const std::vector<ref<Expr>> args;
+
+  MockDeterministicSource(const KModule *_km, const llvm::Function &_function,
+                          const std::vector<ref<Expr>> &_args);
+
+  [[nodiscard]] Kind getKind() const override {
+    return Kind::MockDeterministic;
+  }
+  [[nodiscard]] std::string getName() const override {
+    return "mockDeterministic";
+  }
+
+  static bool classof(const SymbolicSource *S) {
+    return S->getKind() == Kind::MockDeterministic;
+  }
+
+  unsigned computeHash() override;
+
+  [[nodiscard]] int internalCompare(const SymbolicSource &b) const override;
+};
+
 } // namespace klee
 
 #endif /* KLEE_SYMBOLICSOURCE_H */