Skip to content

Commit

Permalink
Add mocks:
Browse files Browse the repository at this point in the history
- Generation in two modes: naive and determinitic
- Mocks are reproducible
- Special mocks for allocators: malloc, calloc, realloc
  • Loading branch information
Lana243 authored and misonijnik committed Feb 22, 2024
1 parent 7f6fd2d commit 3340a08
Show file tree
Hide file tree
Showing 32 changed files with 957 additions and 45 deletions.
1 change: 1 addition & 0 deletions .github/workflows/build.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -146,6 +146,7 @@ jobs:
runs-on: macos-latest
env:
BASE: /tmp
LLVM_VERSION: 11
SOLVERS: STP
UCLIBC_VERSION: 0
USE_TCMALLOC: 0
Expand Down
34 changes: 26 additions & 8 deletions include/klee/Core/Interpreter.h
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@ class BasicBlock;
class Function;
class LLVMContext;
class Module;
class Type;
class raw_ostream;
class raw_fd_ostream;
} // namespace llvm
Expand Down Expand Up @@ -63,6 +64,13 @@ using FLCtoOpcode = std::unordered_map<
std::unordered_map<
unsigned, std::unordered_map<unsigned, std::unordered_set<unsigned>>>>;

enum class MockStrategy {
None, // No mocks are generated
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
};

class Interpreter {
public:
enum class GuidanceKind {
Expand All @@ -79,6 +87,8 @@ class Interpreter {
std::string LibraryDir;
std::string EntryPoint;
std::string OptSuffix;
std::string MainCurrentName;
std::string MainNameAfterMock;
bool Optimize;
bool Simplify;
bool CheckDivZero;
Expand All @@ -88,13 +98,16 @@ class Interpreter {

ModuleOptions(const std::string &_LibraryDir,
const std::string &_EntryPoint, const std::string &_OptSuffix,
bool _Optimize, bool _Simplify, bool _CheckDivZero,
bool _CheckOvershift, bool _WithFPRuntime,
bool _WithPOSIXRuntime)
const std::string &_MainCurrentName,
const std::string &_MainNameAfterMock, bool _Optimize,
bool _Simplify, bool _CheckDivZero, bool _CheckOvershift,
bool _WithFPRuntime, bool _WithPOSIXRuntime)
: LibraryDir(_LibraryDir), EntryPoint(_EntryPoint),
OptSuffix(_OptSuffix), Optimize(_Optimize), Simplify(_Simplify),
CheckDivZero(_CheckDivZero), CheckOvershift(_CheckOvershift),
WithFPRuntime(_WithFPRuntime), WithPOSIXRuntime(_WithPOSIXRuntime) {}
OptSuffix(_OptSuffix), MainCurrentName(_MainCurrentName),
MainNameAfterMock(_MainNameAfterMock), Optimize(_Optimize),
Simplify(_Simplify), CheckDivZero(_CheckDivZero),
CheckOvershift(_CheckOvershift), WithFPRuntime(_WithFPRuntime),
WithPOSIXRuntime(_WithPOSIXRuntime) {}
};

enum LogType {
Expand All @@ -112,10 +125,11 @@ class Interpreter {
unsigned MakeConcreteSymbolic;
GuidanceKind Guidance;
std::optional<SarifReport> Paths;
enum MockStrategy MockStrategy;

InterpreterOptions(std::optional<SarifReport> Paths)
: MakeConcreteSymbolic(false), Guidance(GuidanceKind::NoGuidance),
Paths(std::move(Paths)) {}
Paths(std::move(Paths)), MockStrategy(MockStrategy::None) {}
};

protected:
Expand Down Expand Up @@ -144,7 +158,11 @@ class Interpreter {
const ModuleOptions &opts,
std::set<std::string> &&mainModuleFunctions,
std::set<std::string> &&mainModuleGlobals,
FLCtoOpcode &&origInstructions) = 0;
FLCtoOpcode &&origInstructions,
const std::set<std::string> &ignoredExternals) = 0;

virtual std::map<std::string, llvm::Type *>
getAllExternals(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).
Expand Down
39 changes: 39 additions & 0 deletions include/klee/Core/MockBuilder.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
#ifndef KLEE_MOCKBUILDER_H
#define KLEE_MOCKBUILDER_H

#include "llvm/IR/IRBuilder.h"
#include "llvm/IR/Module.h"

#include <set>
#include <string>

namespace klee {

class MockBuilder {
private:
const llvm::Module *userModule;
std::unique_ptr<llvm::Module> mockModule;
std::unique_ptr<llvm::IRBuilder<>> builder;
std::map<std::string, llvm::Type *> externals;

const std::string mockEntrypoint, userEntrypoint;

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);

public:
MockBuilder(const llvm::Module *initModule, std::string mockEntrypoint,
std::string userEntrypoint,
std::map<std::string, llvm::Type *> externals);

std::unique_ptr<llvm::Module> build();
};

} // namespace klee

#endif // KLEE_MOCKBUILDER_H
8 changes: 8 additions & 0 deletions include/klee/Expr/SourceBuilder.h
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,8 @@

#include "klee/Expr/SymbolicSource.h"

#include "llvm/IR/Function.h"

namespace klee {

class KInstruction;
Expand Down Expand Up @@ -39,6 +41,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);
};

Expand Down
56 changes: 56 additions & 0 deletions include/klee/Expr/SymbolicSource.h
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand All @@ -48,6 +50,8 @@ class SymbolicSource {
Instruction,
Argument,
Irreproducible,
MockNaive,
MockDeterministic,
Alpha
};

Expand Down Expand Up @@ -383,6 +387,58 @@ 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) {}

Kind getKind() const override { return Kind::MockNaive; }
std::string getName() const override { return "mockNaive"; }

static bool classof(const SymbolicSource *S) {
return S->getKind() == Kind::MockNaive;
}

unsigned computeHash() override;

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);

Kind getKind() const override { return Kind::MockDeterministic; }
std::string getName() const override { return "mockDeterministic"; }

static bool classof(const SymbolicSource *S) {
return S->getKind() == Kind::MockDeterministic;
}

unsigned computeHash() override;

int internalCompare(const SymbolicSource &b) const override;
};

} // namespace klee

#endif /* KLEE_SYMBOLICSOURCE_H */
1 change: 1 addition & 0 deletions include/klee/klee.h
Original file line number Diff line number Diff line change
Expand Up @@ -201,5 +201,6 @@ long double klee_rintl(long double d);
// stdin/stdout
void klee_init_env(int *argcPtr, char ***argvPtr);
void check_stdin_read();
void *__klee_wrapped_malloc(size_t size);

#endif /* KLEE_H */
1 change: 1 addition & 0 deletions lib/Core/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ add_library(kleeCore
Memory.cpp
MemoryManager.cpp
PForest.cpp
MockBuilder.cpp
PTree.cpp
Searcher.cpp
SeedInfo.cpp
Expand Down
1 change: 1 addition & 0 deletions lib/Core/ExecutionState.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ DISABLE_WARNING_DEPRECATED_DECLARATIONS
#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>
Expand Down
Loading

0 comments on commit 3340a08

Please sign in to comment.