Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
34 changes: 26 additions & 8 deletions include/klee/Core/Interpreter.h
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@ class BasicBlock;
class Function;
class LLVMContext;
class Module;
class Type;
class raw_ostream;
class raw_fd_ostream;
} // namespace llvm
Expand Down Expand Up @@ -61,6 +62,13 @@ class InterpreterHandler {
const char *suffix) = 0;
};

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 @@ -77,6 +85,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 @@ -86,13 +96,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 @@ -110,10 +123,11 @@ class Interpreter {
unsigned MakeConcreteSymbolic;
GuidanceKind Guidance;
nonstd::optional<SarifReport> Paths;
enum MockStrategy MockStrategy;

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

protected:
Expand Down Expand Up @@ -142,7 +156,11 @@ class Interpreter {
const ModuleOptions &opts,
const std::unordered_set<std::string> &mainModuleFunctions,
const std::unordered_set<std::string> &mainModuleGlobals,
std::unique_ptr<InstructionInfoTable> origInfos) = 0;
std::unique_ptr<InstructionInfoTable> origInfos,
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
1 change: 1 addition & 0 deletions include/klee/Expr/IndependentSet.h
Original file line number Diff line number Diff line change
Expand Up @@ -86,6 +86,7 @@ class IndependentElementSet {
constraints_ty exprs; // All expressions (constraints) that are associated
// with this factor
SymcreteOrderedSet symcretes; // All symcretes associated with this factor
std::set<std::string> uninterpretedFunctions;

IndependentElementSet();
IndependentElementSet(ref<Expr> e);
Expand Down
8 changes: 8 additions & 0 deletions include/klee/Expr/SourceBuilder.h
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,8 @@
#include "klee/Expr/SymbolicSource.h"
#include "klee/Module/KModule.h"

#include "llvm/IR/Function.h"

namespace klee {

class SourceBuilder {
Expand All @@ -28,6 +30,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);
};

}; // namespace klee
Expand Down
58 changes: 57 additions & 1 deletion include/klee/Expr/SymbolicSource.h
Original file line number Diff line number Diff line change
Expand Up @@ -17,10 +17,12 @@ DISABLE_WARNING_POP

namespace klee {

class Expr;
class Array;
class Expr;
class ConstantExpr;
class KModule;
struct KFunction;

class SymbolicSource {
protected:
Expand All @@ -41,7 +43,9 @@ class SymbolicSource {
LazyInitializationSize,
Instruction,
Argument,
Irreproducible
Irreproducible,
MockNaive,
MockDeterministic
};

public:
Expand Down Expand Up @@ -361,6 +365,58 @@ class IrreproducibleSource : 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 @@ -18,6 +18,7 @@
#include "klee/Module/KInstruction.h"
#include "klee/Module/KModule.h"
#include "klee/Support/Casting.h"
#include "klee/Support/ErrorHandling.h"
#include "klee/Support/OptionCategories.h"

#include "klee/Support/CompilerWarning.h"
Expand Down
129 changes: 128 additions & 1 deletion lib/Core/Executor.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@
#include "ImpliedValue.h"
#include "Memory.h"
#include "MemoryManager.h"
#include "MockBuilder.h"
#include "PForest.h"
#include "PTree.h"
#include "Searcher.h"
Expand Down Expand Up @@ -465,6 +466,11 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,

guidanceKind = opts.Guidance;

if (CoreSolverToUse != Z3_SOLVER &&
interpreterOpts.MockStrategy == MockStrategy::Deterministic) {
klee_error("Deterministic mocks can be generated with Z3 solver only.\n");
}

const time::Span maxTime{MaxTime};
if (maxTime)
timers.add(std::make_unique<Timer>(maxTime, [&] {
Expand Down Expand Up @@ -530,10 +536,22 @@ Executor::setModule(std::vector<std::unique_ptr<llvm::Module>> &userModules,
const ModuleOptions &opts,
const std::unordered_set<std::string> &mainModuleFunctions,
const std::unordered_set<std::string> &mainModuleGlobals,
std::unique_ptr<InstructionInfoTable> origInfos) {
std::unique_ptr<InstructionInfoTable> origInfos,
const std::set<std::string> &ignoredExternals) {
assert(!kmodule && !userModules.empty() &&
"can only register one module"); // XXX gross

if (ExternalCalls == ExternalCallPolicy::All &&
interpreterOpts.MockStrategy != MockStrategy::None) {
llvm::Function *mainFn =
userModules.front()->getFunction(opts.MainCurrentName);
if (!mainFn) {
klee_error("Entry function '%s' not found in module.",
opts.MainCurrentName.c_str());
}
mainFn->setName(opts.MainNameAfterMock);
}

kmodule = std::make_unique<KModule>();

// 1.) Link the modules together && 2.) Apply different instrumentation
Expand All @@ -558,6 +576,42 @@ Executor::setModule(std::vector<std::unique_ptr<llvm::Module>> &userModules,
kmodule->instrument(opts);
}

if (ExternalCalls == ExternalCallPolicy::All &&
interpreterOpts.MockStrategy != MockStrategy::None) {
// TODO: move this to function
std::map<std::string, llvm::Type *> externals =
getAllExternals(ignoredExternals);
MockBuilder builder(kmodule->module.get(), opts.MainCurrentName,
opts.MainNameAfterMock, externals);
std::unique_ptr<llvm::Module> mockModule = builder.build();
if (!mockModule) {
klee_error("Unable to generate mocks");
}
// TODO: change this to bc file
std::unique_ptr<llvm::raw_fd_ostream> f(
interpreterHandler->openOutputFile("externals.ll"));
auto mainFn = mockModule->getFunction(opts.MainCurrentName);
mainFn->setName(opts.EntryPoint);
*f << *mockModule;
mainFn->setName(opts.MainCurrentName);

std::vector<std::unique_ptr<llvm::Module>> mockModules;
mockModules.push_back(std::move(mockModule));
kmodule->link(mockModules, 0);

for (auto &global : kmodule->module->globals()) {
if (global.isDeclaration()) {
llvm::Constant *zeroInitializer =
llvm::Constant::getNullValue(global.getValueType());
if (!zeroInitializer) {
klee_error("Unable to get zero initializer for '%s'",
global.getName().str().c_str());
}
global.setInitializer(zeroInitializer);
}
}
}

// 3.) Optimise and prepare for KLEE

// Create a list of functions that should be preserved if used
Expand Down Expand Up @@ -609,6 +663,37 @@ Executor::setModule(std::vector<std::unique_ptr<llvm::Module>> &userModules,
return kmodule->module.get();
}

std::map<std::string, llvm::Type *>
Executor::getAllExternals(const std::set<std::string> &ignoredExternals) {
std::map<std::string, llvm::Type *> externals;
for (const auto &f : kmodule->module->functions()) {
if (f.isDeclaration() && !f.use_empty() &&
!ignoredExternals.count(f.getName().str()))
// NOTE: here we detect all the externals, even linked.
externals.insert(std::make_pair(f.getName(), f.getFunctionType()));
}

for (const auto &global : kmodule->module->globals()) {
if (global.isDeclaration() &&
!ignoredExternals.count(global.getName().str()))
externals.insert(std::make_pair(global.getName(), global.getValueType()));
}

for (const auto &alias : kmodule->module->aliases()) {
auto it = externals.find(alias.getName().str());
if (it != externals.end()) {
externals.erase(it);
}
}

for (const auto &e : externals) {
klee_message("Mocking external %s %s",
e.second->isFunctionTy() ? "function" : "variable",
e.first.c_str());
}
return externals;
}

Executor::~Executor() {
delete typeSystemManager;
delete externalDispatcher;
Expand Down Expand Up @@ -6439,6 +6524,48 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
}
}

void Executor::executeMakeMock(ExecutionState &state, KInstruction *target,
std::vector<ref<Expr>> &arguments) {
KFunction *kf = target->parent->parent;
std::string name = "@call_" + kf->getName().str();
uint64_t width =
kmodule->targetData->getTypeSizeInBits(kf->function->getReturnType());
KType *type = typeSystemManager->getWrappedType(
llvm::PointerType::get(kf->function->getReturnType(),
kmodule->targetData->getAllocaAddrSpace()));

IDType moID;
bool success = state.addressSpace.resolveOne(cast<ConstantExpr>(arguments[0]),
type, moID);
assert(success && "memory object for mock should already be allocated");
const MemoryObject *mo = state.addressSpace.findObject(moID).first;
assert(mo && "memory object for mock should already be allocated");
mo->setName(name);

ref<SymbolicSource> source;
switch (interpreterOpts.MockStrategy) {
case MockStrategy::None:
klee_error("klee_make_mock is not allowed when mock strategy is none");
break;
case MockStrategy::Naive:
source = SourceBuilder::mockNaive(kmodule.get(), *kf->function,
updateNameVersion(state, name));
break;
case MockStrategy::Deterministic:
std::vector<ref<Expr>> args(kf->numArgs);
for (size_t i = 0; i < kf->numArgs; i++) {
args[i] = getArgumentCell(state, kf, i).value;
}
source =
SourceBuilder::mockDeterministic(kmodule.get(), *kf->function, args);
break;
}
executeMakeSymbolic(state, mo, type, source, false);
const ObjectState *os = state.addressSpace.findObject(mo->id).second;
auto result = os->read(0, width);
bindLocal(target, state, result);
}

/***/

ExecutionState *Executor::formState(Function *f) {
Expand Down
Loading