From da9865b0b1a3cafe26484e5364f9cab17c6ecaf4 Mon Sep 17 00:00:00 2001 From: Lana243 Date: Fri, 16 Jun 2023 14:15:47 +0300 Subject: [PATCH 01/25] Add mocks: - Generation in two modes: naive and determinitic - Mocks are reproducible - Special mocks for allocators: malloc, calloc, realloc --- include/klee/Core/Interpreter.h | 23 +++- include/klee/Core/MockBuilder.h | 37 ++++++ include/klee/Expr/IndependentSet.h | 1 + include/klee/Expr/SourceBuilder.h | 6 + include/klee/Expr/SymbolicSource.h | 32 ++++- include/klee/klee.h | 1 + lib/Core/CMakeLists.txt | 1 + lib/Core/Executor.cpp | 120 +++++++++++++++++- lib/Core/Executor.h | 6 +- lib/Core/MockBuilder.cpp | 151 +++++++++++++++++++++++ lib/Core/SpecialFunctionHandler.cpp | 23 ++++ lib/Core/SpecialFunctionHandler.h | 1 + lib/Expr/IndependentSet.cpp | 17 ++- lib/Expr/SourceBuilder.cpp | 17 ++- lib/Expr/SymbolicSource.cpp | 7 ++ lib/Solver/Z3Builder.cpp | 29 +++++ lib/Solver/Z3Builder.h | 7 ++ runtime/CMakeLists.txt | 2 + runtime/Mocks/CMakeLists.txt | 19 +++ runtime/Mocks/models.c | 36 ++++++ runtime/Runtest/CMakeLists.txt | 2 + runtime/Runtest/intrinsics.c | 11 +- test/Feature/MockPointersDeterministic.c | 24 ++++ test/Feature/MockStrategies.c | 37 ++++++ tools/klee/main.cpp | 139 +++++++++++++++++++-- 25 files changed, 724 insertions(+), 25 deletions(-) create mode 100644 include/klee/Core/MockBuilder.h create mode 100644 lib/Core/MockBuilder.cpp create mode 100644 runtime/Mocks/CMakeLists.txt create mode 100644 runtime/Mocks/models.c create mode 100644 test/Feature/MockPointersDeterministic.c create mode 100644 test/Feature/MockStrategies.c diff --git a/include/klee/Core/Interpreter.h b/include/klee/Core/Interpreter.h index 5cd177ca00..96f53a3fa2 100644 --- a/include/klee/Core/Interpreter.h +++ b/include/klee/Core/Interpreter.h @@ -61,6 +61,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 { @@ -77,6 +84,8 @@ class Interpreter { std::string LibraryDir; std::string EntryPoint; std::string OptSuffix; + std::string MainCurrentName; + std::string MainNameAfterMock; bool Optimize; bool Simplify; bool CheckDivZero; @@ -86,11 +95,13 @@ 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, + 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), + OptSuffix(_OptSuffix), MainCurrentName(_MainCurrentName), + MainNameAfterMock(_MainNameAfterMock), Optimize(_Optimize), Simplify(_Simplify), CheckDivZero(_CheckDivZero), CheckOvershift(_CheckOvershift), WithFPRuntime(_WithFPRuntime), WithPOSIXRuntime(_WithPOSIXRuntime) {} }; @@ -108,12 +119,13 @@ class Interpreter { /// symbolic values. This is used to test the correctness of the /// symbolic execution on concrete programs. unsigned MakeConcreteSymbolic; + enum MockStrategy MockStrategy; GuidanceKind Guidance; nonstd::optional Paths; InterpreterOptions(nonstd::optional Paths) : MakeConcreteSymbolic(false), Guidance(GuidanceKind::NoGuidance), - Paths(std::move(Paths)) {} + Paths(std::move(Paths)), MockStrategy(MockStrategy::None) {} }; protected: @@ -142,7 +154,8 @@ class Interpreter { const ModuleOptions &opts, const std::unordered_set &mainModuleFunctions, const std::unordered_set &mainModuleGlobals, - std::unique_ptr origInfos) = 0; + std::unique_ptr origInfos, + const std::set &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). diff --git a/include/klee/Core/MockBuilder.h b/include/klee/Core/MockBuilder.h new file mode 100644 index 0000000000..781711fa62 --- /dev/null +++ b/include/klee/Core/MockBuilder.h @@ -0,0 +1,37 @@ +#ifndef KLEE_MOCKBUILDER_H +#define KLEE_MOCKBUILDER_H + +#include "llvm/IR/IRBuilder.h" +#include "llvm/IR/Module.h" + +#include +#include + +namespace klee { + +class MockBuilder { +private: + const llvm::Module *userModule; + std::unique_ptr mockModule; + std::unique_ptr> builder; + std::map externals; + + const std::string mockEntrypoint, userEntrypoint; + + void buildGlobalsDefinition(); + void buildFunctionsDefinition(); + 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 externals); + + std::unique_ptr build(); +}; + +} // namespace klee + +#endif // KLEE_MOCKBUILDER_H diff --git a/include/klee/Expr/IndependentSet.h b/include/klee/Expr/IndependentSet.h index 9173d90678..0027228cf4 100644 --- a/include/klee/Expr/IndependentSet.h +++ b/include/klee/Expr/IndependentSet.h @@ -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 uninterpretedFunctions; IndependentElementSet(); IndependentElementSet(ref e); diff --git a/include/klee/Expr/SourceBuilder.h b/include/klee/Expr/SourceBuilder.h index 7b57e2f8c9..43d7cea9c9 100644 --- a/include/klee/Expr/SourceBuilder.h +++ b/include/klee/Expr/SourceBuilder.h @@ -5,6 +5,8 @@ #include "klee/Expr/SymbolicSource.h" #include "klee/Module/KModule.h" +#include "llvm/IR/Function.h" + namespace klee { class SourceBuilder { @@ -28,6 +30,10 @@ class SourceBuilder { static ref value(const llvm::Value &_allocSite, int _index, KModule *km); static ref irreproducible(const std::string &name); + static ref mockNaive(); + static ref mockDeterministic(std::string _name, + std::vector> _args, + unsigned _returnTypeWidth); }; }; // namespace klee diff --git a/include/klee/Expr/SymbolicSource.h b/include/klee/Expr/SymbolicSource.h index be65580f7b..c638c66a86 100644 --- a/include/klee/Expr/SymbolicSource.h +++ b/include/klee/Expr/SymbolicSource.h @@ -17,6 +17,7 @@ DISABLE_WARNING_POP namespace klee { +class Expr; class Array; class Expr; class ConstantExpr; @@ -41,7 +42,9 @@ class SymbolicSource { LazyInitializationSize, Instruction, Argument, - Irreproducible + Irreproducible, + MockNaive, + MockDeterministic }; public: @@ -361,6 +364,33 @@ class IrreproducibleSource : public SymbolicSource { } }; +class MockNaiveSource : public SymbolicSource { +public: + Kind getKind() const override { return Kind::MockNaive; } + std::string getName() const override { return "mock"; } + + static bool classof(const SymbolicSource *S) { + return S->getKind() == Kind::MockNaive; + } +}; + +class MockDeterministicSource : public SymbolicSource { +public: + std::string name; + std::vector> args; + unsigned returnTypeWidth; + + Kind getKind() const override { return Kind::MockDeterministic; } + std::string getName() const override { return "mock"; } + + static bool classof(const SymbolicSource *S) { + return S->getKind() == Kind::MockDeterministic; + } + + MockDeterministicSource(std::string _name, std::vector> _args, + unsigned _returnTypeWidth); +}; + } // namespace klee #endif /* KLEE_SYMBOLICSOURCE_H */ diff --git a/include/klee/klee.h b/include/klee/klee.h index 9c40ef335c..5995ff2e24 100644 --- a/include/klee/klee.h +++ b/include/klee/klee.h @@ -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 */ diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt index edcd9eeb5b..7d2aa7d74e 100644 --- a/lib/Core/CMakeLists.txt +++ b/lib/Core/CMakeLists.txt @@ -22,6 +22,7 @@ add_library(kleeCore Memory.cpp MemoryManager.cpp PForest.cpp + MockBuilder.cpp PTree.cpp Searcher.cpp SeedInfo.cpp diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index d219f82761..8f028a6b83 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -38,6 +38,7 @@ #include "klee/Config/Version.h" #include "klee/Config/config.h" #include "klee/Core/Interpreter.h" +#include "klee/Core/MockBuilder.h" #include "klee/Expr/ArrayExprOptimizer.h" #include "klee/Expr/ArrayExprVisitor.h" #include "klee/Expr/Assignment.h" @@ -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(maxTime, [&] { @@ -530,10 +536,21 @@ Executor::setModule(std::vector> &userModules, const ModuleOptions &opts, const std::unordered_set &mainModuleFunctions, const std::unordered_set &mainModuleGlobals, - std::unique_ptr origInfos) { + std::unique_ptr origInfos, + const std::set &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(); // 1.) Link the modules together && 2.) Apply different instrumentation @@ -558,6 +575,67 @@ Executor::setModule(std::vector> &userModules, kmodule->instrument(opts); } + if (ExternalCalls == ExternalCallPolicy::All && + interpreterOpts.MockStrategy != MockStrategy::None) { + // TODO: move this to function + std::map externals; + for (const auto &f : kmodule->module->functions()) { + if (f.isDeclaration() && !f.use_empty() && + !ignoredExternals.count(f.getName().str())) + 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()); + } + + MockBuilder builder(kmodule->module.get(), opts.MainCurrentName, + opts.MainNameAfterMock, externals); + std::unique_ptr mockModule = builder.build(); + + if (!mockModule) { + klee_error("Unable to generate mocks"); + } + + // TODO: change this to bc file + std::unique_ptr f( + interpreterHandler->openOutputFile("externals.ll")); + auto mainFn = mockModule->getFunction(opts.MainCurrentName); + mainFn->setName(opts.EntryPoint); + *f << *mockModule; + mainFn->setName(opts.MainCurrentName); + + std::vector> 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 @@ -6439,6 +6517,46 @@ void Executor::executeMakeSymbolic(ExecutionState &state, } } +void Executor::executeMakeMock(ExecutionState &state, KInstruction *target, + std::vector> &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(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 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(); + break; + case MockStrategy::Deterministic: + std::vector> args(kf->numArgs); + for (size_t i = 0; i < kf->numArgs; i++) { + args[i] = getArgumentCell(state, kf, i).value; + } + source = SourceBuilder::mockDeterministic(name, args, width); + break; + } + executeMakeSymbolic(state, mo, type, name, source, true); + const ObjectState *os = state.addressSpace.findObject(mo->id).second; + auto result = os->read(0, width); + bindLocal(target, state, result); +} + /***/ ExecutionState *Executor::formState(Function *f) { diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 582c22f0f0..0c0d384444 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -420,6 +420,9 @@ class Executor : public Interpreter { KType *type, const ref source, bool isLocal); + void executeMakeMock(ExecutionState &state, KInstruction *target, + std::vector> &arguments); + void updateStateWithSymcretes(ExecutionState &state, const Assignment &assignment); @@ -724,7 +727,8 @@ class Executor : public Interpreter { const ModuleOptions &opts, const std::unordered_set &mainModuleFunctions, const std::unordered_set &mainModuleGlobals, - std::unique_ptr origInfos) override; + std::unique_ptr origInfos, + const std::set &ignoredExternals) override; void useSeeds(const std::vector *seeds) override { usingSeeds = seeds; diff --git a/lib/Core/MockBuilder.cpp b/lib/Core/MockBuilder.cpp new file mode 100644 index 0000000000..89ac5059b4 --- /dev/null +++ b/lib/Core/MockBuilder.cpp @@ -0,0 +1,151 @@ +#include "klee/Core/MockBuilder.h" + +#include "klee/Support/ErrorHandling.h" +#include "llvm/IR/IRBuilder.h" +#include "llvm/IR/Module.h" + +#include + +namespace klee { + +MockBuilder::MockBuilder(const llvm::Module *initModule, + std::string mockEntrypoint, std::string userEntrypoint, + std::map externals) + : userModule(initModule), externals(std::move(externals)), + mockEntrypoint(std::move(mockEntrypoint)), + userEntrypoint(std::move(userEntrypoint)) {} + +std::unique_ptr MockBuilder::build() { + mockModule = std::make_unique(userModule->getName().str() + + "__klee_externals", + userModule->getContext()); + mockModule->setTargetTriple(userModule->getTargetTriple()); + mockModule->setDataLayout(userModule->getDataLayout()); + builder = std::make_unique>(mockModule->getContext()); + + // Set up entrypoint in new module. Here we'll define globals and then call + // user's entrypoint. + llvm::Function *mainFn = userModule->getFunction(userEntrypoint); + if (!mainFn) { + klee_error("Entry function '%s' not found in module.", + userEntrypoint.c_str()); + } + mockModule->getOrInsertFunction(mockEntrypoint, mainFn->getFunctionType(), + mainFn->getAttributes()); + + buildGlobalsDefinition(); + buildFunctionsDefinition(); + return std::move(mockModule); +} + +void MockBuilder::buildGlobalsDefinition() { + llvm::Function *mainFn = mockModule->getFunction(mockEntrypoint); + if (!mainFn) { + klee_error("Entry function '%s' not found in module.", + mockEntrypoint.c_str()); + } + auto globalsInitBlock = + llvm::BasicBlock::Create(mockModule->getContext(), "entry", mainFn); + builder->SetInsertPoint(globalsInitBlock); + + for (const auto &it : externals) { + if (it.second->isFunctionTy()) { + continue; + } + const std::string &extName = it.first; + llvm::Type *type = it.second; + mockModule->getOrInsertGlobal(extName, type); + auto *global = mockModule->getGlobalVariable(extName); + if (!global) { + klee_error("Unable to add global variable '%s' to module", + extName.c_str()); + } + global->setLinkage(llvm::GlobalValue::ExternalLinkage); + if (!type->isSized()) { + continue; + } + + auto *zeroInitializer = llvm::Constant::getNullValue(it.second); + if (!zeroInitializer) { + klee_error("Unable to get zero initializer for '%s'", extName.c_str()); + } + global->setInitializer(zeroInitializer); + buildCallKleeMakeSymbol("klee_make_symbolic", global, type, + "@obj_" + extName); + } + + auto *userMainFn = userModule->getFunction(userEntrypoint); + if (!userMainFn) { + klee_error("Entry function '%s' not found in module.", + userEntrypoint.c_str()); + } + auto userMainCallee = mockModule->getOrInsertFunction( + userEntrypoint, userMainFn->getFunctionType()); + std::vector args; + args.reserve(userMainFn->arg_size()); + for (size_t i = 0; i < mainFn->arg_size(); i++) { + args.push_back(mainFn->getArg(i)); + } + auto callUserMain = builder->CreateCall(userMainCallee, args); + builder->CreateRet(callUserMain); +} + +void MockBuilder::buildFunctionsDefinition() { + for (const auto &it : externals) { + if (!it.second->isFunctionTy()) { + continue; + } + std::string extName = it.first; + auto *type = llvm::cast(it.second); + mockModule->getOrInsertFunction(extName, type); + llvm::Function *func = mockModule->getFunction(extName); + if (!func) { + klee_error("Unable to find function '%s' in module", extName.c_str()); + } + if (!func->empty()) { + continue; + } + auto *BB = + llvm::BasicBlock::Create(mockModule->getContext(), "entry", func); + builder->SetInsertPoint(BB); + + if (!func->getReturnType()->isSized()) { + builder->CreateRet(nullptr); + continue; + } + + auto *mockReturnValue = + builder->CreateAlloca(func->getReturnType(), nullptr); + buildCallKleeMakeSymbol("klee_make_mock", mockReturnValue, + func->getReturnType(), "@call_" + extName); + auto *loadInst = builder->CreateLoad(mockReturnValue, "klee_var"); + builder->CreateRet(loadInst); + } +} + +void MockBuilder::buildCallKleeMakeSymbol(const std::string &klee_function_name, + llvm::Value *source, llvm::Type *type, + const std::string &symbol_name) { + auto *klee_mk_symb_type = llvm::FunctionType::get( + llvm::Type::getVoidTy(mockModule->getContext()), + {llvm::Type::getInt8PtrTy(mockModule->getContext()), + llvm::Type::getInt64Ty(mockModule->getContext()), + llvm::Type::getInt8PtrTy(mockModule->getContext())}, + false); + auto kleeMakeSymbolCallee = + mockModule->getOrInsertFunction(klee_function_name, klee_mk_symb_type); + auto bitcastInst = builder->CreateBitCast( + source, llvm::Type::getInt8PtrTy(mockModule->getContext())); + auto str_name = builder->CreateGlobalString(symbol_name); + auto gep = builder->CreateConstInBoundsGEP2_64(str_name, 0, 0); + builder->CreateCall( + kleeMakeSymbolCallee, + {bitcastInst, + llvm::ConstantInt::get( + mockModule->getContext(), + llvm::APInt(64, mockModule->getDataLayout().getTypeStoreSize(type), + false)), + gep}); +} + +} // namespace klee diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 60c65f14ba..8f97931cc7 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -112,6 +112,7 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = { #endif add("klee_is_symbolic", handleIsSymbolic, true), add("klee_make_symbolic", handleMakeSymbolic, false), + add("klee_make_mock", handleMakeMock, false), add("klee_mark_global", handleMarkGlobal, false), add("klee_prefer_cex", handlePreferCex, false), add("klee_posix_prefer_cex", handlePosixPreferCex, false), @@ -934,6 +935,28 @@ void SpecialFunctionHandler::handleMakeSymbolic( } } +void SpecialFunctionHandler::handleMakeMock(ExecutionState &state, + KInstruction *target, + std::vector> &arguments) { + std::string name; + + if (arguments.size() != 3) { + executor.terminateStateOnUserError(state, + "Incorrect number of arguments to " + "klee_make_mock(void*, size_t, char*)"); + return; + } + + name = arguments[2]->isZero() ? "" : readStringAtAddress(state, arguments[2]); + + if (name.length() == 0) { + executor.terminateStateOnUserError( + state, "Empty name of function in klee_make_mock"); + return; + } + executor.executeMakeMock(state, target, arguments); +} + void SpecialFunctionHandler::handleMarkGlobal( ExecutionState &state, KInstruction *target, std::vector> &arguments) { diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h index 78f920450e..6528b98c36 100644 --- a/lib/Core/SpecialFunctionHandler.h +++ b/lib/Core/SpecialFunctionHandler.h @@ -127,6 +127,7 @@ class SpecialFunctionHandler { HANDLER(handleGetValue); HANDLER(handleIsSymbolic); HANDLER(handleMakeSymbolic); + HANDLER(handleMakeMock); HANDLER(handleMalloc); HANDLER(handleMemalign); HANDLER(handleMarkGlobal); diff --git a/lib/Expr/IndependentSet.cpp b/lib/Expr/IndependentSet.cpp index d4fade9ef1..355c3a2ca9 100644 --- a/lib/Expr/IndependentSet.cpp +++ b/lib/Expr/IndependentSet.cpp @@ -35,6 +35,11 @@ IndependentElementSet::IndependentElementSet(ref e) { if (re->updates.root->isConstantArray() && !re->updates.head) continue; + if (ref mockSource = + dyn_cast_or_null(array->source)) { + uninterpretedFunctions.insert(mockSource->name); + } + if (!wholeObjects.count(array)) { if (ConstantExpr *CE = dyn_cast(re->index)) { // if index constant, then add to set of constraints operating @@ -106,14 +111,15 @@ IndependentElementSet::IndependentElementSet(ref s) { } IndependentElementSet::IndependentElementSet(const IndependentElementSet &ies) - : elements(ies.elements), wholeObjects(ies.wholeObjects), exprs(ies.exprs) { -} + : elements(ies.elements), wholeObjects(ies.wholeObjects), exprs(ies.exprs), + uninterpretedFunctions(ies.uninterpretedFunctions) {} IndependentElementSet & IndependentElementSet::operator=(const IndependentElementSet &ies) { elements = ies.elements; wholeObjects = ies.wholeObjects; exprs = ies.exprs; + uninterpretedFunctions = ies.uninterpretedFunctions; return *this; } @@ -173,6 +179,13 @@ bool IndependentElementSet::intersects(const IndependentElementSet &b) { return true; } } + for (std::set::iterator it = uninterpretedFunctions.begin(), + ie = uninterpretedFunctions.end(); + it != ie; ++it) { + if (b.uninterpretedFunctions.count(*it)) { + return true; + } + } // No need to check symcretes here, arrays must be sufficient. return false; } diff --git a/lib/Expr/SourceBuilder.cpp b/lib/Expr/SourceBuilder.cpp index a667a19ba2..e29ea8142e 100644 --- a/lib/Expr/SourceBuilder.cpp +++ b/lib/Expr/SourceBuilder.cpp @@ -86,4 +86,19 @@ ref SourceBuilder::irreproducible(const std::string &name) { ref r(new IrreproducibleSource(name + llvm::utostr(++id))); r->computeHash(); return r; -} \ No newline at end of file +} + +ref SourceBuilder::mockNaive() { + ref r(new MockNaiveSource()); + r->computeHash(); + return r; +} + +ref +SourceBuilder::mockDeterministic(std::string name, std::vector> args, + unsigned returnTypeWidth) { + ref r(new MockDeterministicSource(std::move(name), std::move(args), + returnTypeWidth)); + r->computeHash(); + return r; +} diff --git a/lib/Expr/SymbolicSource.cpp b/lib/Expr/SymbolicSource.cpp index 0e7f8b1086..6081fbb895 100644 --- a/lib/Expr/SymbolicSource.cpp +++ b/lib/Expr/SymbolicSource.cpp @@ -1,4 +1,5 @@ #include "klee/Expr/SymbolicSource.h" +#include "klee/Expr/Expr.h" #include "klee/Expr/Expr.h" #include "klee/Expr/ExprPPrinter.h" @@ -163,4 +164,10 @@ unsigned InstructionSource::computeHash() { return hashValue; } +MockDeterministicSource::MockDeterministicSource(std::string _name, + std::vector> _args, + unsigned _returnTypeWidth) + : name(std::move(_name)), args(std::move(_args)), + returnTypeWidth(_returnTypeWidth) {} + } // namespace klee diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp index 39cdf1918d..d62b08118e 100644 --- a/lib/Solver/Z3Builder.cpp +++ b/lib/Solver/Z3Builder.cpp @@ -257,6 +257,35 @@ Z3ASTHandle Z3Builder::getInitialArray(const Array *root) { array_expr = buildConstantArray(unique_name.c_str(), root->getDomain(), root->getRange(), symbolicSizeConstantSource->defaultValue); + } else if (ref mockDeterministicSource = + dyn_cast(root->source)) { + size_t num_args = mockDeterministicSource->args.size(); + std::vector argsHandled(num_args); + std::vector argsSortHandled(num_args); + std::vector args(num_args); + std::vector argsSort(num_args); + for (size_t i = 0; i < num_args; i++) { + ref kid = mockDeterministicSource->args[i]; + int kidWidth = kid->getWidth(); + argsHandled[i] = construct(kid, &kidWidth); + args[i] = argsHandled[i]; + argsSortHandled[i] = Z3SortHandle(Z3_get_sort(ctx, args[i]), ctx); + argsSort[i] = argsSortHandled[i]; + } + + Z3SortHandle domainSort = getBvSort(root->getDomain()); + Z3SortHandle rangeSort = getBvSort(root->getRange()); + Z3SortHandle retValSort = getArraySort(domainSort, rangeSort); + + Z3FuncDeclHandle func; + func = Z3FuncDeclHandle( + Z3_mk_func_decl( + ctx, + Z3_mk_string_symbol(ctx, mockDeterministicSource->name.c_str()), + num_args, argsSort.data(), retValSort), + ctx); + array_expr = + Z3ASTHandle(Z3_mk_app(ctx, func, num_args, args.data()), ctx); } else { array_expr = buildArray(unique_name.c_str(), root->getDomain(), root->getRange()); diff --git a/lib/Solver/Z3Builder.h b/lib/Solver/Z3Builder.h index 001ac13a9c..d906f455c4 100644 --- a/lib/Solver/Z3Builder.h +++ b/lib/Solver/Z3Builder.h @@ -91,6 +91,13 @@ typedef Z3NodeHandle Z3SortHandle; template <> void Z3NodeHandle::dump() __attribute__((used)); template <> unsigned Z3NodeHandle::hash() __attribute__((used)); +// Specialize for Z3_func_decl +template <> inline ::Z3_ast Z3NodeHandle::as_ast() { + return ::Z3_func_decl_to_ast(context, node); +} +typedef Z3NodeHandle Z3FuncDeclHandle; +template <> void Z3NodeHandle::dump() __attribute__((used)); + // Specialise for Z3_ast template <> inline ::Z3_ast Z3NodeHandle::as_ast() { return node; } typedef Z3NodeHandle Z3ASTHandle; diff --git a/runtime/CMakeLists.txt b/runtime/CMakeLists.txt index ada82c0f33..d1c8a17d2f 100644 --- a/runtime/CMakeLists.txt +++ b/runtime/CMakeLists.txt @@ -90,12 +90,14 @@ add_subdirectory(Freestanding) add_subdirectory(Intrinsic) add_subdirectory(klee-libc) add_subdirectory(Fortify) +add_subdirectory(Mocks) set(RUNTIME_LIBRARIES RuntimeFreestanding RuntimeIntrinsic RuntimeKLEELibc RuntimeFortify + RuntimeMocks ) if (ENABLE_KLEE_EH_CXX) diff --git a/runtime/Mocks/CMakeLists.txt b/runtime/Mocks/CMakeLists.txt new file mode 100644 index 0000000000..efd6497470 --- /dev/null +++ b/runtime/Mocks/CMakeLists.txt @@ -0,0 +1,19 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# + +set(LIB_PREFIX "RuntimeMocks") +set(SRC_FILES + models.c + ) + +# Build it +include("${CMAKE_SOURCE_DIR}/cmake/compile_bitcode_library.cmake") +prefix_with_path("${SRC_FILES}" "${CMAKE_CURRENT_SOURCE_DIR}/" runtime_mocks_files) + +add_bitcode_library_targets("${LIB_PREFIX}" "${runtime_mocks_files}" "" "") diff --git a/runtime/Mocks/models.c b/runtime/Mocks/models.c new file mode 100644 index 0000000000..ad95634b47 --- /dev/null +++ b/runtime/Mocks/models.c @@ -0,0 +1,36 @@ +#include "stddef.h" + +extern void klee_make_symbolic(void *array, size_t nbytes, const char *name); +extern void *malloc(size_t size); +extern void *calloc(size_t num, size_t size); +extern void *realloc(void *ptr, size_t new_size); + +void *__klee_wrapped_malloc(size_t size) { + char retNull; + klee_make_symbolic(&retNull, sizeof(retNull), "retNullMalloc"); + if (retNull) { + return 0; + } + void *array = malloc(size); + return array; +} + +void *__klee_wrapped_calloc(size_t num, size_t size) { + char retNull; + klee_make_symbolic(&retNull, sizeof(retNull), "retNullCalloc"); + if (retNull) { + return 0; + } + void *array = calloc(num, size); + return array; +} + +void *__klee_wrapped_realloc(void *ptr, size_t new_size) { + char retNull; + klee_make_symbolic(&retNull, sizeof(retNull), "retNullRealloc"); + if (retNull) { + return 0; + } + void *array = realloc(ptr, new_size); + return array; +} diff --git a/runtime/Runtest/CMakeLists.txt b/runtime/Runtest/CMakeLists.txt index df5f2c23be..33d190a262 100644 --- a/runtime/Runtest/CMakeLists.txt +++ b/runtime/Runtest/CMakeLists.txt @@ -9,6 +9,8 @@ add_library(kleeRuntest SHARED intrinsics.c + # Mocks: + ${CMAKE_SOURCE_DIR}/runtime/Mocks/models.c # HACK: ${CMAKE_SOURCE_DIR}/lib/Basic/KTest.cpp ) diff --git a/runtime/Runtest/intrinsics.c b/runtime/Runtest/intrinsics.c index 34a9e9d2c8..3e6bdd8efd 100644 --- a/runtime/Runtest/intrinsics.c +++ b/runtime/Runtest/intrinsics.c @@ -72,8 +72,7 @@ void recursively_allocate(KTestObject *obj, size_t index, void *addr, return; } -void klee_make_symbolic(void *array, size_t nbytes, const char *name) { - +static void klee_make_symbol(void *array, size_t nbytes, const char *name) { if (!name) name = "unnamed"; @@ -154,6 +153,14 @@ void klee_make_symbolic(void *array, size_t nbytes, const char *name) { } } +void klee_make_symbolic(void *array, size_t nbytes, const char *name) { + klee_make_symbol(array, nbytes, name); +} + +void klee_make_mock(void *ret_array, size_t ret_nbytes, const char *fname) { + klee_make_symbol(ret_array, ret_nbytes, fname); +} + void klee_silent_exit(int x) { exit(x); } uintptr_t klee_choose(uintptr_t n) { diff --git a/test/Feature/MockPointersDeterministic.c b/test/Feature/MockPointersDeterministic.c new file mode 100644 index 0000000000..f113440f33 --- /dev/null +++ b/test/Feature/MockPointersDeterministic.c @@ -0,0 +1,24 @@ +// REQUIRES: z3 +// RUN: %clang %s -g -emit-llvm %O0opt -c -o %t.bc + +// RUN: rm -rf %t.klee-out-1 +// RUN: %klee --solver-backend=z3 --use-independent-solver=false --output-dir=%t.klee-out-1 --skip-not-lazy-initialized --external-calls=all --mock-strategy=deterministic %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-1 +// CHECK-1: memory error: null pointer exception +// CHECK-1: KLEE: done: completed paths = 1 +// CHECK-1: KLEE: done: partially completed paths = 1 +// CHECK-1: KLEE: done: generated tests = 2 +// XFAIL: * + +#include + +extern int *age(); + +int main() { + if (age() != age()) { + assert(0 && "age is deterministic"); + } + if (*age() != *age()) { + assert(0 && "age is deterministic"); + } + return *age(); +} \ No newline at end of file diff --git a/test/Feature/MockStrategies.c b/test/Feature/MockStrategies.c new file mode 100644 index 0000000000..a47437e292 --- /dev/null +++ b/test/Feature/MockStrategies.c @@ -0,0 +1,37 @@ +// REQUIRES: z3 +// RUN: %clang %s -g -emit-llvm %O0opt -c -o %t.bc + +// RUN: rm -rf %t.klee-out-1 +// RUN: %klee --output-dir=%t.klee-out-1 --external-calls=all --mock-strategy=none %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-1 +// CHECK-1: failed external call +// CHECK-1: KLEE: done: completed paths = 1 +// CHECK-1: KLEE: done: generated tests = 2 + +// RUN: rm -rf %t.klee-out-2 +// RUN: %klee --output-dir=%t.klee-out-2 --external-calls=all --mock-strategy=naive %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-2 +// CHECK-2: ASSERTION FAIL: 0 +// CHECK-2: KLEE: done: completed paths = 2 +// CHECK-2: KLEE: done: generated tests = 3 + +// RUN: rm -rf %t.klee-out-3 +// RUN: not %klee --output-dir=%t.klee-out-3 --solver-backend=stp --external-calls=all --mock-strategy=deterministic %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-3 +// CHECK-3: KLEE: ERROR: Deterministic mocks can be generated with Z3 solver only. + +// RUN: rm -rf %t.klee-out-4 +// RUN: %klee --output-dir=%t.klee-out-4 --use-independent-solver=false --solver-backend=z3 --external-calls=all --mock-strategy=deterministic %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-4 +// CHECK-4: KLEE: done: completed paths = 2 +// CHECK-4: KLEE: done: generated tests = 2 + +#include + +extern int foo(int x, int y); + +int main() { + int a, b; + klee_make_symbolic(&a, sizeof(a), "a"); + klee_make_symbolic(&b, sizeof(b), "b"); + if (a == b && foo(a + b, b) != foo(2 * b, a)) { + assert(0); + } + return 0; +} diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 68525c7f52..ede0995404 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -341,6 +341,33 @@ cl::opt Libcxx( "libcxx", cl::desc("Link the llvm libc++ library into the bitcode (default=false)"), cl::init(false), cl::cat(LinkCat)); + +/*** Mocking options ***/ + +cl::OptionCategory MockCat("Mock category"); + +cl::opt MockLinkedExternals( + "mock-linked-externals", + cl::desc("Mock modelled linked externals (default=false)"), cl::init(false), + cl::cat(MockCat)); + +cl::opt MockUnlinkedStrategy( + "mock-strategy", cl::init(MockStrategy::None), + cl::desc("Specify strategy for mocking external calls"), + cl::values( + clEnumValN(MockStrategy::None, "none", + "External calls are not mocked (default)"), + clEnumValN(MockStrategy::Naive, "naive", + "Every time external function is called, new symbolic value " + "is generated for its return value"), + clEnumValN( + MockStrategy::Deterministic, "deterministic", + "NOTE: this option is compatible with Z3 solver only. Each " + "external function is treated as a deterministic " + "function. Therefore, when function is called many times " + "with equal arguments, every time equal values will be returned.")), + cl::init(MockStrategy::None), cl::cat(MockCat)); + } // namespace namespace klee { @@ -755,7 +782,7 @@ std::string KleeHandler::getRunTimeLibraryPath(const char *argv0) { void KleeHandler::setOutputDirectory(const std::string &directoryName) { // create output directory - if (directoryName == "") { + if (directoryName.empty()) { klee_error("Empty name of new directory"); } SmallString<128> directory(directoryName); @@ -860,7 +887,8 @@ static const char *modelledExternals[] = { "klee_check_memory_access", "klee_define_fixed_object", "klee_get_errno", "klee_get_valuef", "klee_get_valued", "klee_get_valuel", "klee_get_valuell", "klee_get_value_i32", "klee_get_value_i64", "klee_get_obj_size", - "klee_is_symbolic", "klee_make_symbolic", "klee_mark_global", + "klee_is_symbolic", "klee_make_symbolic", "klee_make_mock", + "klee_mark_global", "klee_open_merge", "klee_close_merge", "klee_prefer_cex", "klee_posix_prefer_cex", "klee_print_expr", "klee_print_range", "klee_report_error", "klee_set_forking", "klee_silent_exit", "klee_warning", "klee_warning_once", "klee_stack_trace", @@ -954,12 +982,14 @@ static const char *dontCareExternals[] = { "getwd", "gettimeofday", "uname", + "ioctl", // fp stuff we just don't worry about yet "frexp", "ldexp", "__isnan", "__signbit", + "llvm.dbg.label", }; // Extra symbols we aren't going to warn about with klee-libc @@ -1189,7 +1219,7 @@ createLibCWrapper(std::vector> &userModules, args.push_back(llvm::ConstantExpr::getBitCast( cast(inModuleReference.getCallee()), ft->getParamType(0))); - args.push_back(&*(stub->arg_begin())); // argc + args.push_back(&*(stub->arg_begin())); // argc auto arg_it = stub->arg_begin(); args.push_back(&*(++arg_it)); // argv args.push_back(Constant::getNullValue(ft->getParamType(3))); // app_init @@ -1432,6 +1462,41 @@ void wait_until_any_child_dies( } } +void mockLinkedExternals( + const Interpreter::ModuleOptions &Opts, llvm::LLVMContext &ctx, + llvm::Module *mainModule, + std::vector> &loadedLibsModules, + llvm::raw_string_ostream *redefineFile) { + std::string errorMsg; + std::vector> mockModules; + SmallString<128> Path(Opts.LibraryDir); + llvm::sys::path::append(Path, + "libkleeRuntimeMocks" + Opts.OptSuffix + ".bca"); + klee_message("NOTE: Using mocks model %s for linked externals", Path.c_str()); + if (!klee::loadFileAsOneModule(Path.c_str(), ctx, mockModules, errorMsg)) { + klee_error("error loading mocks model '%s': %s", Path.c_str(), + errorMsg.c_str()); + } + + for (auto &module : mockModules) { + for (const auto &fmodel : module->functions()) { + if (fmodel.getName().str().substr(0, 15) != "__klee_wrapped_") { + continue; + } + llvm::Function *f = + mainModule->getFunction(fmodel.getName().str().substr(15)); + if (!f) { + continue; + } + klee_message("Renamed symbol %s to %s", f->getName().str().c_str(), + fmodel.getName().str().c_str()); + *redefineFile << f->getName() << ' ' << fmodel.getName() << '\n'; + f->setName(fmodel.getName()); + } + loadedLibsModules.push_back(std::move(module)); + } +} + int main(int argc, char **argv, char **envp) { if (theInterpreter) { theInterpreter = nullptr; @@ -1524,9 +1589,10 @@ int main(int argc, char **argv, char **envp) { sys::SetInterruptFunction(interrupt_handle); - // Load the bytecode... std::string errorMsg; LLVMContext ctx; + + // Load the bytecode... std::vector> loadedUserModules; std::vector> loadedLibsModules; if (!klee::loadFileAsOneModule(InputFile, ctx, loadedUserModules, errorMsg)) { @@ -1543,6 +1609,10 @@ int main(int argc, char **argv, char **envp) { } llvm::Module *mainModule = loadedUserModules.front().get(); + llvm::Function *initialMainFn = mainModule->getFunction(EntryPoint); + if (!initialMainFn) { + klee_error("Unable to find entrypoint function %s", EntryPoint.c_str()); + } std::unique_ptr origInfos; std::unique_ptr assemblyFS; @@ -1603,13 +1673,16 @@ int main(int argc, char **argv, char **envp) { } std::string LibraryDir = KleeHandler::getRunTimeLibraryPath(argv[0]); - Interpreter::ModuleOptions Opts(LibraryDir.c_str(), EntryPoint, opt_suffix, - /*Optimize=*/OptimizeModule, - /*Simplify*/ SimplifyModule, - /*CheckDivZero=*/CheckDivZero, - /*CheckOvershift=*/CheckOvershift, - /*WithFPRuntime=*/WithFPRuntime, - /*WithPOSIXRuntime=*/WithPOSIXRuntime); + Interpreter::ModuleOptions Opts( + LibraryDir.c_str(), EntryPoint, opt_suffix, + /*MainCurrentName=*/EntryPoint, + /*MainNameAfterMock=*/"__klee_mock_wrapped_main", + /*Optimize=*/OptimizeModule, + /*Simplify*/ SimplifyModule, + /*CheckDivZero=*/CheckDivZero, + /*CheckOvershift=*/CheckOvershift, + /*WithFPRuntime=*/WithFPRuntime, + /*WithPOSIXRuntime=*/WithPOSIXRuntime); // Get the main function for (auto &module : loadedUserModules) { @@ -1631,6 +1704,17 @@ int main(int argc, char **argv, char **envp) { if (!entryFn) klee_error("Entry function '%s' not found in module.", EntryPoint.c_str()); + std::string redefinitions; + llvm::raw_string_ostream o_redefinitions(redefinitions); + if (MockLinkedExternals) { + mockLinkedExternals(Opts, ctx, mainModule, loadedLibsModules, + &o_redefinitions); + } + + if (MockUnlinkedStrategy != MockStrategy::None) { + o_redefinitions << EntryPoint << ' ' << Opts.MainNameAfterMock << '\n'; + } + if (WithPOSIXRuntime) { SmallString<128> Path(Opts.LibraryDir); llvm::sys::path::append(Path, "libkleeRuntimePOSIX" + opt_suffix + ".bca"); @@ -1806,12 +1890,43 @@ int main(int argc, char **argv, char **envp) { } handler->getInfoStream() << "PID: " << getpid() << "\n"; + if (MockLinkedExternals || MockUnlinkedStrategy != MockStrategy::None) { + o_redefinitions.flush(); + auto f_redefinitions = handler->openOutputFile("redefinitions.txt"); + *f_redefinitions << redefinitions; + } + // Get the desired main function. klee_main initializes uClibc // locale and other data and then calls main. + std::set ignoredExternals; + ignoredExternals.insert(modelledExternals, + modelledExternals + NELEMS(modelledExternals)); + ignoredExternals.insert(dontCareExternals, + dontCareExternals + NELEMS(dontCareExternals)); + ignoredExternals.insert(unsafeExternals, + unsafeExternals + NELEMS(unsafeExternals)); + + switch (Libc) { + case LibcType::KleeLibc: + ignoredExternals.insert(dontCareKlee, dontCareKlee + NELEMS(dontCareKlee)); + break; + case LibcType::UcLibc: + ignoredExternals.insert(dontCareUclibc, + dontCareUclibc + NELEMS(dontCareUclibc)); + break; + case LibcType::FreestandingLibc: /* silence compiler warning */ + break; + } + + if (WithPOSIXRuntime) { + ignoredExternals.insert("syscall"); + } + + Opts.MainCurrentName = initialMainFn->getName(); auto finalModule = interpreter->setModule( loadedUserModules, loadedLibsModules, Opts, mainModuleFunctions, - mainModuleGlobals, std::move(origInfos)); + mainModuleGlobals, std::move(origInfos), ignoredExternals); externalsAndGlobalsCheck(finalModule); if (InteractiveMode) { From c7d571574a36d6273e1c9837aab7ed5007aa02fb Mon Sep 17 00:00:00 2001 From: Lana243 Date: Mon, 19 Jun 2023 18:01:39 +0300 Subject: [PATCH 02/25] Refactoring --- include/klee/Expr/SourceBuilder.h | 7 +++--- include/klee/Expr/SymbolicSource.h | 27 ++++++++++---------- lib/Core/ExecutionState.cpp | 11 +++++--- lib/Core/Executor.cpp | 6 ++--- lib/Expr/IndependentSet.cpp | 3 ++- lib/Expr/SourceBuilder.cpp | 14 +++-------- lib/Expr/SymbolicSource.cpp | 40 ++++++++++++++++++++++++++---- lib/Solver/Z3Builder.cpp | 3 ++- tools/klee/main.cpp | 1 + 9 files changed, 71 insertions(+), 41 deletions(-) diff --git a/include/klee/Expr/SourceBuilder.h b/include/klee/Expr/SourceBuilder.h index 43d7cea9c9..996ea3b592 100644 --- a/include/klee/Expr/SourceBuilder.h +++ b/include/klee/Expr/SourceBuilder.h @@ -30,10 +30,9 @@ class SourceBuilder { static ref value(const llvm::Value &_allocSite, int _index, KModule *km); static ref irreproducible(const std::string &name); - static ref mockNaive(); - static ref mockDeterministic(std::string _name, - std::vector> _args, - unsigned _returnTypeWidth); + static ref mockDeterministic(KModule *kModule, + KFunction *kFunction, + std::vector> args); }; }; // namespace klee diff --git a/include/klee/Expr/SymbolicSource.h b/include/klee/Expr/SymbolicSource.h index c638c66a86..4000bd8e82 100644 --- a/include/klee/Expr/SymbolicSource.h +++ b/include/klee/Expr/SymbolicSource.h @@ -22,6 +22,7 @@ class Array; class Expr; class ConstantExpr; class KModule; +class KFunction; class SymbolicSource { protected: @@ -43,7 +44,6 @@ class SymbolicSource { Instruction, Argument, Irreproducible, - MockNaive, MockDeterministic }; @@ -364,31 +364,30 @@ class IrreproducibleSource : public SymbolicSource { } }; -class MockNaiveSource : public SymbolicSource { +class MockSource : public SymbolicSource { public: - Kind getKind() const override { return Kind::MockNaive; } - std::string getName() const override { return "mock"; } - - static bool classof(const SymbolicSource *S) { - return S->getKind() == Kind::MockNaive; - } + KFunction *kFunction; + explicit MockSource(KFunction *_kFunction) : kFunction(_kFunction) {} }; -class MockDeterministicSource : public SymbolicSource { +class MockDeterministicSource : public MockSource { public: - std::string name; + KModule *kModule; std::vector> args; - unsigned returnTypeWidth; Kind getKind() const override { return Kind::MockDeterministic; } - std::string getName() const override { return "mock"; } + std::string getName() const override { return "mockDeterministic"; } static bool classof(const SymbolicSource *S) { return S->getKind() == Kind::MockDeterministic; } - MockDeterministicSource(std::string _name, std::vector> _args, - unsigned _returnTypeWidth); + virtual unsigned computeHash() override; + + virtual int internalCompare(const SymbolicSource &b) const override; + + MockDeterministicSource(KModule *_kModule, KFunction *_kFunction, + std::vector> _args); }; } // namespace klee diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 9288283849..71d6911ae2 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -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" @@ -189,10 +190,14 @@ void ExecutionState::pushFrame(KInstIterator caller, KFunction *kf) { void ExecutionState::popFrame() { const StackFrame &sf = stack.back(); for (const auto id : sf.allocas) { + //klee_message("%lu", id); const MemoryObject *memoryObject = addressSpace.findObject(id).first; - assert(memoryObject); - removePointerResolutions(memoryObject); - addressSpace.unbindObject(memoryObject); + //assert(memoryObject); + if (memoryObject) { + // TODO: fix this + removePointerResolutions(memoryObject); + addressSpace.unbindObject(memoryObject); + } } stack.pop_back(); --stackBalance; diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 8f028a6b83..2991e2d9e2 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -6541,17 +6541,17 @@ void Executor::executeMakeMock(ExecutionState &state, KInstruction *target, klee_error("klee_make_mock is not allowed when mock strategy is none"); break; case MockStrategy::Naive: - source = SourceBuilder::mockNaive(); + source = SourceBuilder::makeSymbolic(name, updateNameVersion(state, name)); break; case MockStrategy::Deterministic: std::vector> args(kf->numArgs); for (size_t i = 0; i < kf->numArgs; i++) { args[i] = getArgumentCell(state, kf, i).value; } - source = SourceBuilder::mockDeterministic(name, args, width); + source = SourceBuilder::mockDeterministic(kmodule.get(), kf, args); break; } - executeMakeSymbolic(state, mo, type, name, source, true); + executeMakeSymbolic(state, mo, type, source, true); const ObjectState *os = state.addressSpace.findObject(mo->id).second; auto result = os->read(0, width); bindLocal(target, state, result); diff --git a/lib/Expr/IndependentSet.cpp b/lib/Expr/IndependentSet.cpp index 355c3a2ca9..b3e1a4b2a6 100644 --- a/lib/Expr/IndependentSet.cpp +++ b/lib/Expr/IndependentSet.cpp @@ -6,6 +6,7 @@ #include "klee/Expr/ExprUtil.h" #include "klee/Expr/SymbolicSource.h" #include "klee/Expr/Symcrete.h" +#include "klee/Module/KModule.h" #include "klee/Solver/Solver.h" #include @@ -37,7 +38,7 @@ IndependentElementSet::IndependentElementSet(ref e) { if (ref mockSource = dyn_cast_or_null(array->source)) { - uninterpretedFunctions.insert(mockSource->name); + uninterpretedFunctions.insert(mockSource->kFunction->function->getName()); } if (!wholeObjects.count(array)) { diff --git a/lib/Expr/SourceBuilder.cpp b/lib/Expr/SourceBuilder.cpp index e29ea8142e..01ad90c9ab 100644 --- a/lib/Expr/SourceBuilder.cpp +++ b/lib/Expr/SourceBuilder.cpp @@ -88,17 +88,11 @@ ref SourceBuilder::irreproducible(const std::string &name) { return r; } -ref SourceBuilder::mockNaive() { - ref r(new MockNaiveSource()); - r->computeHash(); - return r; -} - ref -SourceBuilder::mockDeterministic(std::string name, std::vector> args, - unsigned returnTypeWidth) { - ref r(new MockDeterministicSource(std::move(name), std::move(args), - returnTypeWidth)); +SourceBuilder::mockDeterministic(KModule *kModule, KFunction *kFunction, + std::vector> args) { + ref r( + new MockDeterministicSource(kModule, kFunction, std::move(args))); r->computeHash(); return r; } diff --git a/lib/Expr/SymbolicSource.cpp b/lib/Expr/SymbolicSource.cpp index 6081fbb895..c363e4e511 100644 --- a/lib/Expr/SymbolicSource.cpp +++ b/lib/Expr/SymbolicSource.cpp @@ -164,10 +164,40 @@ unsigned InstructionSource::computeHash() { return hashValue; } -MockDeterministicSource::MockDeterministicSource(std::string _name, - std::vector> _args, - unsigned _returnTypeWidth) - : name(std::move(_name)), args(std::move(_args)), - returnTypeWidth(_returnTypeWidth) {} +unsigned MockDeterministicSource::computeHash() { + unsigned res = getKind() * SymbolicSource::MAGIC_HASH_CONSTANT; + res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + + kModule->functionIDMap.at(kFunction->function); + for (const auto &arg : args) { + res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + arg->hash(); + } + return res; +} + +int MockDeterministicSource::internalCompare(const SymbolicSource &b) const { + if (getKind() != b.getKind()) { + return getKind() < b.getKind() ? -1 : 1; + } + const auto &mdb = static_cast(b); + unsigned funcID = kModule->functionIDMap.at(kFunction->function); + unsigned bFuncID = mdb.kModule->functionIDMap.at(mdb.kFunction->function); + if (funcID != bFuncID) { + return funcID < bFuncID ? -1 : 1; + } + assert(args.size() == mdb.args.size() && + "the same functions should have the same arguments number"); + for (unsigned i = 0; i < args.size(); i++) { + if (!args[i]->equals(*mdb.args[i])) { + return args[i]->compare(*mdb.args[i]); + } + } + return 0; +} + +MockDeterministicSource::MockDeterministicSource(KModule *_kModule, + KFunction *_kFunction, + std::vector> _args) + : MockSource(_kFunction), kModule(_kModule), args(std::move(_args)) { +} } // namespace klee diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp index d62b08118e..e7243c9ee9 100644 --- a/lib/Solver/Z3Builder.cpp +++ b/lib/Solver/Z3Builder.cpp @@ -13,6 +13,7 @@ #include "klee/ADT/Bits.h" #include "klee/Expr/Expr.h" #include "klee/Expr/SymbolicSource.h" +#include "klee/Module/KModule.h" #include "klee/Solver/Solver.h" #include "klee/Solver/SolverStats.h" #include "klee/Support/ErrorHandling.h" @@ -281,7 +282,7 @@ Z3ASTHandle Z3Builder::getInitialArray(const Array *root) { func = Z3FuncDeclHandle( Z3_mk_func_decl( ctx, - Z3_mk_string_symbol(ctx, mockDeterministicSource->name.c_str()), + Z3_mk_string_symbol(ctx, mockDeterministicSource->kFunction->function->getName().str().c_str()), num_args, argsSort.data(), retValSort), ctx); array_expr = diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index ede0995404..21fc71d6e3 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -1879,6 +1879,7 @@ int main(int argc, char **argv, char **envp) { Interpreter::InterpreterOptions IOpts(paths); IOpts.MakeConcreteSymbolic = MakeConcreteSymbolic; IOpts.Guidance = UseGuidedSearch; + IOpts.MockStrategy = MockUnlinkedStrategy; std::unique_ptr interpreter( Interpreter::create(ctx, IOpts, handler.get())); theInterpreter = interpreter.get(); From e953fd549effb2a33c5107328b8bf71b01bf996f Mon Sep 17 00:00:00 2001 From: Lana243 Date: Wed, 21 Jun 2023 17:36:09 +0300 Subject: [PATCH 03/25] Fixing tests --- include/klee/Expr/SymbolicSource.h | 2 +- lib/Core/ExecutionState.cpp | 10 +++------- lib/Core/Executor.cpp | 2 +- lib/Expr/IndependentSet.cpp | 3 ++- 4 files changed, 7 insertions(+), 10 deletions(-) diff --git a/include/klee/Expr/SymbolicSource.h b/include/klee/Expr/SymbolicSource.h index 4000bd8e82..b7f82aabd2 100644 --- a/include/klee/Expr/SymbolicSource.h +++ b/include/klee/Expr/SymbolicSource.h @@ -22,7 +22,7 @@ class Array; class Expr; class ConstantExpr; class KModule; -class KFunction; +struct KFunction; class SymbolicSource { protected: diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 71d6911ae2..f5fcdd6857 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -190,14 +190,10 @@ void ExecutionState::pushFrame(KInstIterator caller, KFunction *kf) { void ExecutionState::popFrame() { const StackFrame &sf = stack.back(); for (const auto id : sf.allocas) { - //klee_message("%lu", id); const MemoryObject *memoryObject = addressSpace.findObject(id).first; - //assert(memoryObject); - if (memoryObject) { - // TODO: fix this - removePointerResolutions(memoryObject); - addressSpace.unbindObject(memoryObject); - } + assert(memoryObject); + removePointerResolutions(memoryObject); + addressSpace.unbindObject(memoryObject); } stack.pop_back(); --stackBalance; diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 2991e2d9e2..af204b856d 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -6551,7 +6551,7 @@ void Executor::executeMakeMock(ExecutionState &state, KInstruction *target, source = SourceBuilder::mockDeterministic(kmodule.get(), kf, args); break; } - executeMakeSymbolic(state, mo, type, source, true); + 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); diff --git a/lib/Expr/IndependentSet.cpp b/lib/Expr/IndependentSet.cpp index b3e1a4b2a6..a41b3addc0 100644 --- a/lib/Expr/IndependentSet.cpp +++ b/lib/Expr/IndependentSet.cpp @@ -38,7 +38,8 @@ IndependentElementSet::IndependentElementSet(ref e) { if (ref mockSource = dyn_cast_or_null(array->source)) { - uninterpretedFunctions.insert(mockSource->kFunction->function->getName()); + uninterpretedFunctions.insert( + mockSource->kFunction->function->getName().str()); } if (!wholeObjects.count(array)) { From 4ff7c195b50258aeb768c7637191e11484fe3c30 Mon Sep 17 00:00:00 2001 From: Lana243 Date: Wed, 21 Jun 2023 17:52:50 +0300 Subject: [PATCH 04/25] Fixing tests --- include/klee/Core/Interpreter.h | 2 +- lib/Core/MockBuilder.cpp | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/include/klee/Core/Interpreter.h b/include/klee/Core/Interpreter.h index 96f53a3fa2..fb12bae287 100644 --- a/include/klee/Core/Interpreter.h +++ b/include/klee/Core/Interpreter.h @@ -119,9 +119,9 @@ class Interpreter { /// symbolic values. This is used to test the correctness of the /// symbolic execution on concrete programs. unsigned MakeConcreteSymbolic; - enum MockStrategy MockStrategy; GuidanceKind Guidance; nonstd::optional Paths; + enum MockStrategy MockStrategy; InterpreterOptions(nonstd::optional Paths) : MakeConcreteSymbolic(false), Guidance(GuidanceKind::NoGuidance), diff --git a/lib/Core/MockBuilder.cpp b/lib/Core/MockBuilder.cpp index 89ac5059b4..b1b93c8b6d 100644 --- a/lib/Core/MockBuilder.cpp +++ b/lib/Core/MockBuilder.cpp @@ -83,8 +83,8 @@ void MockBuilder::buildGlobalsDefinition() { userEntrypoint, userMainFn->getFunctionType()); std::vector args; args.reserve(userMainFn->arg_size()); - for (size_t i = 0; i < mainFn->arg_size(); i++) { - args.push_back(mainFn->getArg(i)); + for (auto it = mainFn->arg_begin(); it != mainFn->arg_end(); it++) { + args.push_back(it); } auto callUserMain = builder->CreateCall(userMainCallee, args); builder->CreateRet(callUserMain); From 84eafda343ccc1f8262dd58167ef964111fc1d78 Mon Sep 17 00:00:00 2001 From: Lana243 Date: Wed, 21 Jun 2023 18:29:29 +0300 Subject: [PATCH 05/25] Fixing tests --- tools/klee/main.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 21fc71d6e3..6e659853d9 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -1611,7 +1611,7 @@ int main(int argc, char **argv, char **envp) { llvm::Module *mainModule = loadedUserModules.front().get(); llvm::Function *initialMainFn = mainModule->getFunction(EntryPoint); if (!initialMainFn) { - klee_error("Unable to find entrypoint function %s", EntryPoint.c_str()); + klee_error("Entry function '%s' not found in module.", EntryPoint.c_str()); } std::unique_ptr origInfos; std::unique_ptr assemblyFS; From 8ae21d1d9ee3244d30eb1df000853cb884d7562c Mon Sep 17 00:00:00 2001 From: Lana243 Date: Wed, 21 Jun 2023 18:36:09 +0300 Subject: [PATCH 06/25] Fixing clang format --- include/klee/Core/Interpreter.h | 11 ++++++----- lib/Core/Executor.cpp | 7 +++++-- lib/Expr/SymbolicSource.cpp | 3 +-- lib/Solver/Z3Builder.cpp | 5 ++++- 4 files changed, 16 insertions(+), 10 deletions(-) diff --git a/include/klee/Core/Interpreter.h b/include/klee/Core/Interpreter.h index fb12bae287..3a74cda51d 100644 --- a/include/klee/Core/Interpreter.h +++ b/include/klee/Core/Interpreter.h @@ -97,13 +97,14 @@ class Interpreter { const std::string &_EntryPoint, const std::string &_OptSuffix, const std::string &_MainCurrentName, const std::string &_MainNameAfterMock, bool _Optimize, - bool _Simplify, bool _CheckDivZero, bool _CheckOvershift,bool _WithFPRuntime, - bool _WithPOSIXRuntime) + bool _Simplify, bool _CheckDivZero, bool _CheckOvershift, + bool _WithFPRuntime, bool _WithPOSIXRuntime) : LibraryDir(_LibraryDir), EntryPoint(_EntryPoint), OptSuffix(_OptSuffix), MainCurrentName(_MainCurrentName), - MainNameAfterMock(_MainNameAfterMock), Optimize(_Optimize), Simplify(_Simplify), - CheckDivZero(_CheckDivZero), CheckOvershift(_CheckOvershift), - WithFPRuntime(_WithFPRuntime), WithPOSIXRuntime(_WithPOSIXRuntime) {} + MainNameAfterMock(_MainNameAfterMock), Optimize(_Optimize), + Simplify(_Simplify), CheckDivZero(_CheckDivZero), + CheckOvershift(_CheckOvershift), WithFPRuntime(_WithFPRuntime), + WithPOSIXRuntime(_WithPOSIXRuntime) {} }; enum LogType { diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index af204b856d..631784c7f7 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -543,7 +543,8 @@ Executor::setModule(std::vector> &userModules, if (ExternalCalls == ExternalCallPolicy::All && interpreterOpts.MockStrategy != MockStrategy::None) { - llvm::Function *mainFn = userModules.front()->getFunction(opts.MainCurrentName); + llvm::Function *mainFn = + userModules.front()->getFunction(opts.MainCurrentName); if (!mainFn) { klee_error("Entry function '%s' not found in module.", opts.MainCurrentName.c_str()); @@ -600,7 +601,9 @@ Executor::setModule(std::vector> &userModules, } for (const auto &e : externals) { - klee_message("Mocking external %s %s", e.second->isFunctionTy() ? "function" : "variable", e.first.c_str()); + klee_message("Mocking external %s %s", + e.second->isFunctionTy() ? "function" : "variable", + e.first.c_str()); } MockBuilder builder(kmodule->module.get(), opts.MainCurrentName, diff --git a/lib/Expr/SymbolicSource.cpp b/lib/Expr/SymbolicSource.cpp index c363e4e511..3cabe03e21 100644 --- a/lib/Expr/SymbolicSource.cpp +++ b/lib/Expr/SymbolicSource.cpp @@ -197,7 +197,6 @@ int MockDeterministicSource::internalCompare(const SymbolicSource &b) const { MockDeterministicSource::MockDeterministicSource(KModule *_kModule, KFunction *_kFunction, std::vector> _args) - : MockSource(_kFunction), kModule(_kModule), args(std::move(_args)) { -} + : MockSource(_kFunction), kModule(_kModule), args(std::move(_args)) {} } // namespace klee diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp index e7243c9ee9..ffa191df27 100644 --- a/lib/Solver/Z3Builder.cpp +++ b/lib/Solver/Z3Builder.cpp @@ -282,7 +282,10 @@ Z3ASTHandle Z3Builder::getInitialArray(const Array *root) { func = Z3FuncDeclHandle( Z3_mk_func_decl( ctx, - Z3_mk_string_symbol(ctx, mockDeterministicSource->kFunction->function->getName().str().c_str()), + Z3_mk_string_symbol( + ctx, mockDeterministicSource->kFunction->function->getName() + .str() + .c_str()), num_args, argsSort.data(), retValSort), ctx); array_expr = From 46fd299802b8527e57cdd5a394e131b94fe0ba7c Mon Sep 17 00:00:00 2001 From: Lana243 Date: Thu, 22 Jun 2023 15:05:54 +0300 Subject: [PATCH 07/25] Fixing tests --- tools/klee/main.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 6e659853d9..64d0593fb3 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -1609,10 +1609,6 @@ int main(int argc, char **argv, char **envp) { } llvm::Module *mainModule = loadedUserModules.front().get(); - llvm::Function *initialMainFn = mainModule->getFunction(EntryPoint); - if (!initialMainFn) { - klee_error("Entry function '%s' not found in module.", EntryPoint.c_str()); - } std::unique_ptr origInfos; std::unique_ptr assemblyFS; @@ -1656,6 +1652,11 @@ int main(int argc, char **argv, char **envp) { "This may cause unexpected crashes or assertion violations.", module_triple.c_str(), host_triple.c_str()); + llvm::Function *initialMainFn = mainModule->getFunction(EntryPoint); + if (!initialMainFn) { + klee_error("Entry function '%s' not found in module.", EntryPoint.c_str()); + } + // Detect architecture std::string opt_suffix = "64"; // Fall back to 64bit if (module_triple.find("i686") != std::string::npos || From d4b709f3baab12b1d581d3bb792e1c08c92e7849 Mon Sep 17 00:00:00 2001 From: Lana243 Date: Thu, 22 Jun 2023 17:57:12 +0300 Subject: [PATCH 08/25] Implement parser and printer for new sources --- include/klee/Expr/SourceBuilder.h | 3 +++ include/klee/Expr/SymbolicSource.h | 35 +++++++++++++++++++++------ lib/Core/Executor.cpp | 3 ++- lib/Expr/ExprPPrinter.cpp | 10 ++++++++ lib/Expr/Parser.cpp | 35 +++++++++++++++++++++++++++ lib/Expr/SourceBuilder.cpp | 8 ++++++ lib/Expr/SymbolicSource.cpp | 39 ++++++++++++++++++++++++------ 7 files changed, 117 insertions(+), 16 deletions(-) diff --git a/include/klee/Expr/SourceBuilder.h b/include/klee/Expr/SourceBuilder.h index 996ea3b592..7020320cbf 100644 --- a/include/klee/Expr/SourceBuilder.h +++ b/include/klee/Expr/SourceBuilder.h @@ -30,6 +30,9 @@ class SourceBuilder { static ref value(const llvm::Value &_allocSite, int _index, KModule *km); static ref irreproducible(const std::string &name); + static ref mockNaive(KModule *kModule, + KFunction *kFunction, + unsigned version); static ref mockDeterministic(KModule *kModule, KFunction *kFunction, std::vector> args); diff --git a/include/klee/Expr/SymbolicSource.h b/include/klee/Expr/SymbolicSource.h index b7f82aabd2..89b98b0ff1 100644 --- a/include/klee/Expr/SymbolicSource.h +++ b/include/klee/Expr/SymbolicSource.h @@ -44,6 +44,7 @@ class SymbolicSource { Instruction, Argument, Irreproducible, + MockNaive, MockDeterministic }; @@ -366,15 +367,38 @@ class IrreproducibleSource : public SymbolicSource { class MockSource : public SymbolicSource { public: + KModule *kModule; KFunction *kFunction; - explicit MockSource(KFunction *_kFunction) : kFunction(_kFunction) {} + MockSource(KModule *_kModule, KFunction *_kFunction) + : kModule(_kModule), kFunction(_kFunction) {} +}; + +class MockNaiveSource : public MockSource { +public: + const unsigned version; + + MockNaiveSource(KModule *_kModule, KFunction *_kFunction, unsigned _version) + : MockSource(_kModule, _kFunction), 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: - KModule *kModule; std::vector> args; + MockDeterministicSource(KModule *_kModule, KFunction *_kFunction, + std::vector> _args); + Kind getKind() const override { return Kind::MockDeterministic; } std::string getName() const override { return "mockDeterministic"; } @@ -382,12 +406,9 @@ class MockDeterministicSource : public MockSource { return S->getKind() == Kind::MockDeterministic; } - virtual unsigned computeHash() override; - - virtual int internalCompare(const SymbolicSource &b) const override; + unsigned computeHash() override; - MockDeterministicSource(KModule *_kModule, KFunction *_kFunction, - std::vector> _args); + int internalCompare(const SymbolicSource &b) const override; }; } // namespace klee diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 631784c7f7..dd85007d9f 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -6544,7 +6544,8 @@ void Executor::executeMakeMock(ExecutionState &state, KInstruction *target, klee_error("klee_make_mock is not allowed when mock strategy is none"); break; case MockStrategy::Naive: - source = SourceBuilder::makeSymbolic(name, updateNameVersion(state, name)); + source = SourceBuilder::mockNaive(kmodule.get(), kf, + updateNameVersion(state, name)); break; case MockStrategy::Deterministic: std::vector> args(kf->numArgs); diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp index bde8d30d6d..244de118a1 100644 --- a/lib/Expr/ExprPPrinter.cpp +++ b/lib/Expr/ExprPPrinter.cpp @@ -413,6 +413,16 @@ class PPrinter : public ExprPPrinter { << " " << s->index; } else if (auto s = dyn_cast(source)) { PC << s->name; + } else if (auto s = dyn_cast(source)) { + PC << s->kFunction->getName() << ' ' << s->version; + } else if (auto s = dyn_cast(source)) { + PC << s->kFunction->getName() << ' '; + PC << " ( "; + for (const auto &it : s->args) { + print(it, PC); + PC << ' '; + } + PC << ')'; } else { assert(0 && "Not implemented"); } diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index b072cec826..6738b767ff 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -330,6 +330,8 @@ class ParserImpl : public Parser { SourceResult ParseLazyInitializationSizeSource(); SourceResult ParseInstructionSource(); SourceResult ParseArgumentSource(); + SourceResult ParseMockNaiveSource(); + SourceResult ParseMockDeterministicSource(); /*** Diagnostics ***/ @@ -501,6 +503,12 @@ SourceResult ParserImpl::ParseSource() { } else if (type == "argument") { assert(km); source = ParseArgumentSource(); + } else if (type == "mockNaive") { + assert(km); + source = ParseMockNaiveSource(); + } else if (type == "mockDeterministic") { + assert(km); + source = ParseMockDeterministicSource(); } else { assert(0); } @@ -599,6 +607,33 @@ SourceResult ParserImpl::ParseInstructionSource() { return SourceBuilder::instruction(*KI->inst, index, km); } +SourceResult ParserImpl::ParseMockNaiveSource() { + auto name = Tok.getString(); + auto kf = km->functionNameMap[name]; + ConsumeExpectedToken(Token::Identifier); + auto versionExpr = ParseNumber(64).get(); + auto version = dyn_cast(versionExpr); + assert(version); + return SourceBuilder::mockNaive(km, kf, version->getZExtValue()); +} + +SourceResult ParserImpl::ParseMockDeterministicSource() { + auto name = Tok.getString(); + auto kf = km->functionNameMap[name]; + ConsumeExpectedToken(Token::Identifier); + ConsumeLParen(); + std::vector> args; + args.reserve(kf->numArgs); + for (unsigned i = 0; i < kf->numArgs; i++) { + auto expr = ParseExpr(TypeResult()); + if (!expr.isValid()) { + return {false, nullptr}; + } + args.push_back(expr.get()); + } + return SourceBuilder::mockDeterministic(km, kf, args); +} + /// ParseCommandDecl - Parse a command declaration. The lexer should /// be positioned at the opening '('. /// diff --git a/lib/Expr/SourceBuilder.cpp b/lib/Expr/SourceBuilder.cpp index 01ad90c9ab..c19625509b 100644 --- a/lib/Expr/SourceBuilder.cpp +++ b/lib/Expr/SourceBuilder.cpp @@ -88,6 +88,14 @@ ref SourceBuilder::irreproducible(const std::string &name) { return r; } +ref SourceBuilder::mockNaive(KModule *kModule, + KFunction *kFunction, + unsigned int version) { + ref r(new MockNaiveSource(kModule, kFunction, version)); + r->computeHash(); + return r; +} + ref SourceBuilder::mockDeterministic(KModule *kModule, KFunction *kFunction, std::vector> args) { diff --git a/lib/Expr/SymbolicSource.cpp b/lib/Expr/SymbolicSource.cpp index 3cabe03e21..733e267623 100644 --- a/lib/Expr/SymbolicSource.cpp +++ b/lib/Expr/SymbolicSource.cpp @@ -1,7 +1,6 @@ #include "klee/Expr/SymbolicSource.h" #include "klee/Expr/Expr.h" -#include "klee/Expr/Expr.h" #include "klee/Expr/ExprPPrinter.h" #include "klee/Expr/ExprUtil.h" #include "klee/Module/KInstruction.h" @@ -164,8 +163,36 @@ unsigned InstructionSource::computeHash() { return hashValue; } +unsigned MockNaiveSource::computeHash() { + unsigned res = (getKind() * SymbolicSource::MAGIC_HASH_CONSTANT) + version; + unsigned funcID = kModule->functionIDMap.at(kFunction->function); + res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + funcID; + return res; +} + +int MockNaiveSource::internalCompare(const SymbolicSource &b) const { + if (getKind() != b.getKind()) { + return getKind() < b.getKind() ? -1 : 1; + } + const MockNaiveSource &mnb = static_cast(b); + if (version != mnb.version) { + return version < mnb.version ? -1 : 1; + } + unsigned funcID = kModule->functionIDMap.at(kFunction->function); + unsigned bFuncID = mnb.kModule->functionIDMap.at(mnb.kFunction->function); + if (funcID != bFuncID) { + return funcID < bFuncID ? -1 : 1; + } + return 0; +} + +MockDeterministicSource::MockDeterministicSource(KModule *_kModule, + KFunction *_kFunction, + std::vector> _args) + : MockSource(_kModule, _kFunction), args(std::move(_args)) {} + unsigned MockDeterministicSource::computeHash() { - unsigned res = getKind() * SymbolicSource::MAGIC_HASH_CONSTANT; + unsigned res = getKind(); res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + kModule->functionIDMap.at(kFunction->function); for (const auto &arg : args) { @@ -178,7 +205,8 @@ int MockDeterministicSource::internalCompare(const SymbolicSource &b) const { if (getKind() != b.getKind()) { return getKind() < b.getKind() ? -1 : 1; } - const auto &mdb = static_cast(b); + const MockDeterministicSource &mdb = + static_cast(b); unsigned funcID = kModule->functionIDMap.at(kFunction->function); unsigned bFuncID = mdb.kModule->functionIDMap.at(mdb.kFunction->function); if (funcID != bFuncID) { @@ -194,9 +222,4 @@ int MockDeterministicSource::internalCompare(const SymbolicSource &b) const { return 0; } -MockDeterministicSource::MockDeterministicSource(KModule *_kModule, - KFunction *_kFunction, - std::vector> _args) - : MockSource(_kFunction), kModule(_kModule), args(std::move(_args)) {} - } // namespace klee From 1ab56ed6240a25c18c90813e76841dbb2e31262d Mon Sep 17 00:00:00 2001 From: Lana243 Date: Thu, 22 Jun 2023 18:22:24 +0300 Subject: [PATCH 09/25] Fix clang format --- include/klee/Expr/SourceBuilder.h | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/include/klee/Expr/SourceBuilder.h b/include/klee/Expr/SourceBuilder.h index 7020320cbf..aec9450440 100644 --- a/include/klee/Expr/SourceBuilder.h +++ b/include/klee/Expr/SourceBuilder.h @@ -30,8 +30,7 @@ class SourceBuilder { static ref value(const llvm::Value &_allocSite, int _index, KModule *km); static ref irreproducible(const std::string &name); - static ref mockNaive(KModule *kModule, - KFunction *kFunction, + static ref mockNaive(KModule *kModule, KFunction *kFunction, unsigned version); static ref mockDeterministic(KModule *kModule, KFunction *kFunction, From 3787535d04e94e9c2d482624f7578545122c5b22 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Mon, 26 Jun 2023 16:29:10 +0400 Subject: [PATCH 10/25] [fix] Enable test --- test/Feature/MockPointersDeterministic.c | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/test/Feature/MockPointersDeterministic.c b/test/Feature/MockPointersDeterministic.c index f113440f33..d8c871588d 100644 --- a/test/Feature/MockPointersDeterministic.c +++ b/test/Feature/MockPointersDeterministic.c @@ -2,12 +2,11 @@ // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t.bc // RUN: rm -rf %t.klee-out-1 -// RUN: %klee --solver-backend=z3 --use-independent-solver=false --output-dir=%t.klee-out-1 --skip-not-lazy-initialized --external-calls=all --mock-strategy=deterministic %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t.klee-out-1 --skip-not-lazy-initialized --external-calls=all --mock-strategy=deterministic %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-1 // CHECK-1: memory error: null pointer exception // CHECK-1: KLEE: done: completed paths = 1 -// CHECK-1: KLEE: done: partially completed paths = 1 -// CHECK-1: KLEE: done: generated tests = 2 -// XFAIL: * +// CHECK-1: KLEE: done: partially completed paths = 2 +// CHECK-1: KLEE: done: generated tests = 3 #include From 9164895112f27b3df5747ffa53a43507f417015c Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Tue, 27 Jun 2023 13:07:20 +0400 Subject: [PATCH 11/25] [fix] --- include/klee/Expr/SourceBuilder.h | 10 +++++----- include/klee/Expr/SymbolicSource.h | 23 ++++++++++++++--------- lib/Core/Executor.cpp | 4 ++-- lib/Expr/ExprPPrinter.cpp | 14 ++++++++------ lib/Expr/ExprUtil.cpp | 10 ++++++++++ lib/Expr/IndependentSet.cpp | 2 +- lib/Expr/Parser.cpp | 5 +++-- lib/Expr/SourceBuilder.cpp | 12 +++++------- lib/Expr/SymbolicSource.cpp | 26 ++++++++++++++------------ lib/Solver/Z3Builder.cpp | 2 +- 10 files changed, 63 insertions(+), 45 deletions(-) diff --git a/include/klee/Expr/SourceBuilder.h b/include/klee/Expr/SourceBuilder.h index aec9450440..8796d44504 100644 --- a/include/klee/Expr/SourceBuilder.h +++ b/include/klee/Expr/SourceBuilder.h @@ -30,11 +30,11 @@ class SourceBuilder { static ref value(const llvm::Value &_allocSite, int _index, KModule *km); static ref irreproducible(const std::string &name); - static ref mockNaive(KModule *kModule, KFunction *kFunction, - unsigned version); - static ref mockDeterministic(KModule *kModule, - KFunction *kFunction, - std::vector> args); + static ref mockNaive(const KModule *kModule, + const llvm::Function &kFunction, unsigned version); + static ref mockDeterministic(const KModule *kModule, + const llvm::Function &kFunction, + const std::vector> &args); }; }; // namespace klee diff --git a/include/klee/Expr/SymbolicSource.h b/include/klee/Expr/SymbolicSource.h index 89b98b0ff1..bbcaf05e69 100644 --- a/include/klee/Expr/SymbolicSource.h +++ b/include/klee/Expr/SymbolicSource.h @@ -367,18 +367,23 @@ class IrreproducibleSource : public SymbolicSource { class MockSource : public SymbolicSource { public: - KModule *kModule; - KFunction *kFunction; - MockSource(KModule *_kModule, KFunction *_kFunction) - : kModule(_kModule), kFunction(_kFunction) {} + 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(KModule *_kModule, KFunction *_kFunction, unsigned _version) - : MockSource(_kModule, _kFunction), version(_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"; } @@ -394,10 +399,10 @@ class MockNaiveSource : public MockSource { class MockDeterministicSource : public MockSource { public: - std::vector> args; + const std::vector> args; - MockDeterministicSource(KModule *_kModule, KFunction *_kFunction, - std::vector> _args); + MockDeterministicSource(const KModule *_km, const llvm::Function &_function, + const std::vector> &_args); Kind getKind() const override { return Kind::MockDeterministic; } std::string getName() const override { return "mockDeterministic"; } diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index dd85007d9f..724f38bc7d 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -6544,7 +6544,7 @@ void Executor::executeMakeMock(ExecutionState &state, KInstruction *target, klee_error("klee_make_mock is not allowed when mock strategy is none"); break; case MockStrategy::Naive: - source = SourceBuilder::mockNaive(kmodule.get(), kf, + source = SourceBuilder::mockNaive(kmodule.get(), *kf->function, updateNameVersion(state, name)); break; case MockStrategy::Deterministic: @@ -6552,7 +6552,7 @@ void Executor::executeMakeMock(ExecutionState &state, KInstruction *target, for (size_t i = 0; i < kf->numArgs; i++) { args[i] = getArgumentCell(state, kf, i).value; } - source = SourceBuilder::mockDeterministic(kmodule.get(), kf, args); + source = SourceBuilder::mockDeterministic(kmodule.get(), *kf->function, args); break; } executeMakeSymbolic(state, mo, type, source, false); diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp index 244de118a1..c544c23b26 100644 --- a/lib/Expr/ExprPPrinter.cpp +++ b/lib/Expr/ExprPPrinter.cpp @@ -414,13 +414,15 @@ class PPrinter : public ExprPPrinter { } else if (auto s = dyn_cast(source)) { PC << s->name; } else if (auto s = dyn_cast(source)) { - PC << s->kFunction->getName() << ' ' << s->version; + PC << s->km->functionMap.at(&s->function)->getName() << ' ' << s->version; } else if (auto s = dyn_cast(source)) { - PC << s->kFunction->getName() << ' '; - PC << " ( "; - for (const auto &it : s->args) { - print(it, PC); - PC << ' '; + PC << s->km->functionMap.at(&s->function)->getName() << ' '; + PC << "("; + for (unsigned i = 0; i < s->args.size(); i++) { + print(s->args[i], PC); + if (i != s->args.size() - 1) { + PC << " "; + } } PC << ')'; } else { diff --git a/lib/Expr/ExprUtil.cpp b/lib/Expr/ExprUtil.cpp index 87bed5d731..518e922dc8 100644 --- a/lib/Expr/ExprUtil.cpp +++ b/lib/Expr/ExprUtil.cpp @@ -54,6 +54,16 @@ void klee::findReads(ref e, bool visitUpdates, cast(re->updates.root->source)->pointer); } + if (ref mockSource = + dyn_cast_or_null( + re->updates.root->source)) { + for (auto arg : mockSource->args) { + if (visited.insert(arg).second) { + stack.push_back(arg); + } + } + } + if (visitUpdates) { // XXX this is probably suboptimal. We want to avoid a potential // explosion traversing update lists which can be quite diff --git a/lib/Expr/IndependentSet.cpp b/lib/Expr/IndependentSet.cpp index a41b3addc0..16872b6fd7 100644 --- a/lib/Expr/IndependentSet.cpp +++ b/lib/Expr/IndependentSet.cpp @@ -39,7 +39,7 @@ IndependentElementSet::IndependentElementSet(ref e) { if (ref mockSource = dyn_cast_or_null(array->source)) { uninterpretedFunctions.insert( - mockSource->kFunction->function->getName().str()); + mockSource->function.getName().str()); } if (!wholeObjects.count(array)) { diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index 6738b767ff..1196471f71 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -614,7 +614,7 @@ SourceResult ParserImpl::ParseMockNaiveSource() { auto versionExpr = ParseNumber(64).get(); auto version = dyn_cast(versionExpr); assert(version); - return SourceBuilder::mockNaive(km, kf, version->getZExtValue()); + return SourceBuilder::mockNaive(km, *kf->function, version->getZExtValue()); } SourceResult ParserImpl::ParseMockDeterministicSource() { @@ -631,7 +631,8 @@ SourceResult ParserImpl::ParseMockDeterministicSource() { } args.push_back(expr.get()); } - return SourceBuilder::mockDeterministic(km, kf, args); + ConsumeRParen(); + return SourceBuilder::mockDeterministic(km, *kf->function, args); } /// ParseCommandDecl - Parse a command declaration. The lexer should diff --git a/lib/Expr/SourceBuilder.cpp b/lib/Expr/SourceBuilder.cpp index c19625509b..305186cb6f 100644 --- a/lib/Expr/SourceBuilder.cpp +++ b/lib/Expr/SourceBuilder.cpp @@ -88,19 +88,17 @@ ref SourceBuilder::irreproducible(const std::string &name) { return r; } -ref SourceBuilder::mockNaive(KModule *kModule, - KFunction *kFunction, - unsigned int version) { - ref r(new MockNaiveSource(kModule, kFunction, version)); +ref SourceBuilder::mockNaive(const KModule *km, const llvm::Function &function,unsigned int version) { + ref r(new MockNaiveSource(km, function, version)); r->computeHash(); return r; } ref -SourceBuilder::mockDeterministic(KModule *kModule, KFunction *kFunction, - std::vector> args) { +SourceBuilder::mockDeterministic(const KModule *km, const llvm::Function &function, + const std::vector> &args) { ref r( - new MockDeterministicSource(kModule, kFunction, std::move(args))); + new MockDeterministicSource(km, function, args)); r->computeHash(); return r; } diff --git a/lib/Expr/SymbolicSource.cpp b/lib/Expr/SymbolicSource.cpp index 733e267623..063ea1235b 100644 --- a/lib/Expr/SymbolicSource.cpp +++ b/lib/Expr/SymbolicSource.cpp @@ -165,8 +165,9 @@ unsigned InstructionSource::computeHash() { unsigned MockNaiveSource::computeHash() { unsigned res = (getKind() * SymbolicSource::MAGIC_HASH_CONSTANT) + version; - unsigned funcID = kModule->functionIDMap.at(kFunction->function); + unsigned funcID = km->functionIDMap.at(&function); res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + funcID; + hashValue = res; return res; } @@ -178,26 +179,27 @@ int MockNaiveSource::internalCompare(const SymbolicSource &b) const { if (version != mnb.version) { return version < mnb.version ? -1 : 1; } - unsigned funcID = kModule->functionIDMap.at(kFunction->function); - unsigned bFuncID = mnb.kModule->functionIDMap.at(mnb.kFunction->function); + unsigned funcID = km->functionIDMap.at(&function); + unsigned bFuncID = mnb.km->functionIDMap.at(&mnb.function); if (funcID != bFuncID) { return funcID < bFuncID ? -1 : 1; } return 0; } -MockDeterministicSource::MockDeterministicSource(KModule *_kModule, - KFunction *_kFunction, - std::vector> _args) - : MockSource(_kModule, _kFunction), args(std::move(_args)) {} +MockDeterministicSource::MockDeterministicSource(const KModule *km, + const llvm::Function &function, + const std::vector> &_args) + : MockSource(km, function), args(_args) {} unsigned MockDeterministicSource::computeHash() { unsigned res = getKind(); res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + - kModule->functionIDMap.at(kFunction->function); + km->functionIDMap.at(&function); for (const auto &arg : args) { res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + arg->hash(); } + hashValue = res; return res; } @@ -207,16 +209,16 @@ int MockDeterministicSource::internalCompare(const SymbolicSource &b) const { } const MockDeterministicSource &mdb = static_cast(b); - unsigned funcID = kModule->functionIDMap.at(kFunction->function); - unsigned bFuncID = mdb.kModule->functionIDMap.at(mdb.kFunction->function); + unsigned funcID = km->functionIDMap.at(&function); + unsigned bFuncID = mdb.km->functionIDMap.at(&mdb.function); if (funcID != bFuncID) { return funcID < bFuncID ? -1 : 1; } assert(args.size() == mdb.args.size() && "the same functions should have the same arguments number"); for (unsigned i = 0; i < args.size(); i++) { - if (!args[i]->equals(*mdb.args[i])) { - return args[i]->compare(*mdb.args[i]); + if (args[i] != mdb.args[i]) { + return args[i] < mdb.args[i] ? -1 : 1; } } return 0; diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp index ffa191df27..879af1f616 100644 --- a/lib/Solver/Z3Builder.cpp +++ b/lib/Solver/Z3Builder.cpp @@ -283,7 +283,7 @@ Z3ASTHandle Z3Builder::getInitialArray(const Array *root) { Z3_mk_func_decl( ctx, Z3_mk_string_symbol( - ctx, mockDeterministicSource->kFunction->function->getName() + ctx, mockDeterministicSource->function.getName() .str() .c_str()), num_args, argsSort.data(), retValSort), From c91095f907c63218b2f21ca14aa609fcadc816e9 Mon Sep 17 00:00:00 2001 From: Lana243 Date: Tue, 27 Jun 2023 14:35:37 +0300 Subject: [PATCH 12/25] Refactoring --- include/klee/Core/Interpreter.h | 4 ++ include/klee/Core/MockBuilder.h | 6 ++- include/klee/Expr/SourceBuilder.h | 9 +++-- include/klee/Expr/SymbolicSource.h | 3 +- lib/Core/Executor.cpp | 65 ++++++++++++++++-------------- lib/Core/Executor.h | 3 ++ lib/Core/MockBuilder.cpp | 65 +++++++++++++++--------------- lib/Expr/IndependentSet.cpp | 3 +- lib/Expr/SourceBuilder.cpp | 10 +++-- lib/Expr/SymbolicSource.cpp | 6 +-- lib/Solver/Z3Builder.cpp | 5 +-- test/Feature/MockStrategies.c | 2 +- 12 files changed, 99 insertions(+), 82 deletions(-) diff --git a/include/klee/Core/Interpreter.h b/include/klee/Core/Interpreter.h index 3a74cda51d..8d47552eeb 100644 --- a/include/klee/Core/Interpreter.h +++ b/include/klee/Core/Interpreter.h @@ -32,6 +32,7 @@ class BasicBlock; class Function; class LLVMContext; class Module; +class Type; class raw_ostream; class raw_fd_ostream; } // namespace llvm @@ -158,6 +159,9 @@ class Interpreter { std::unique_ptr origInfos, const std::set &ignoredExternals) = 0; + virtual std::map + getAllExternals(const std::set &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). virtual void setPathWriter(TreeStreamWriter *tsw) = 0; diff --git a/include/klee/Core/MockBuilder.h b/include/klee/Core/MockBuilder.h index 781711fa62..70949b10a7 100644 --- a/include/klee/Core/MockBuilder.h +++ b/include/klee/Core/MockBuilder.h @@ -18,8 +18,10 @@ class MockBuilder { const std::string mockEntrypoint, userEntrypoint; - void buildGlobalsDefinition(); - void buildFunctionsDefinition(); + 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); diff --git a/include/klee/Expr/SourceBuilder.h b/include/klee/Expr/SourceBuilder.h index 8796d44504..827dc092e9 100644 --- a/include/klee/Expr/SourceBuilder.h +++ b/include/klee/Expr/SourceBuilder.h @@ -31,10 +31,11 @@ class SourceBuilder { KModule *km); static ref irreproducible(const std::string &name); static ref mockNaive(const KModule *kModule, - const llvm::Function &kFunction, unsigned version); - static ref mockDeterministic(const KModule *kModule, - const llvm::Function &kFunction, - const std::vector> &args); + const llvm::Function &kFunction, + unsigned version); + static ref + mockDeterministic(const KModule *kModule, const llvm::Function &kFunction, + const std::vector> &args); }; }; // namespace klee diff --git a/include/klee/Expr/SymbolicSource.h b/include/klee/Expr/SymbolicSource.h index bbcaf05e69..2f52844268 100644 --- a/include/klee/Expr/SymbolicSource.h +++ b/include/klee/Expr/SymbolicSource.h @@ -373,7 +373,8 @@ class MockSource : public SymbolicSource { : km(_km), function(_function) {} static bool classof(const SymbolicSource *S) { - return S->getKind() == Kind::MockNaive || S->getKind() == Kind::MockDeterministic; + return S->getKind() == Kind::MockNaive || + S->getKind() == Kind::MockDeterministic; } }; diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 724f38bc7d..5c3c1453e5 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -579,41 +579,14 @@ Executor::setModule(std::vector> &userModules, if (ExternalCalls == ExternalCallPolicy::All && interpreterOpts.MockStrategy != MockStrategy::None) { // TODO: move this to function - std::map externals; - for (const auto &f : kmodule->module->functions()) { - if (f.isDeclaration() && !f.use_empty() && - !ignoredExternals.count(f.getName().str())) - 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()); - } - + std::map externals = + getAllExternals(ignoredExternals); MockBuilder builder(kmodule->module.get(), opts.MainCurrentName, opts.MainNameAfterMock, externals); std::unique_ptr mockModule = builder.build(); - if (!mockModule) { klee_error("Unable to generate mocks"); } - // TODO: change this to bc file std::unique_ptr f( interpreterHandler->openOutputFile("externals.ll")); @@ -690,6 +663,37 @@ Executor::setModule(std::vector> &userModules, return kmodule->module.get(); } +std::map +Executor::getAllExternals(const std::set &ignoredExternals) { + std::map 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; @@ -6552,7 +6556,8 @@ void Executor::executeMakeMock(ExecutionState &state, KInstruction *target, for (size_t i = 0; i < kf->numArgs; i++) { args[i] = getArgumentCell(state, kf, i).value; } - source = SourceBuilder::mockDeterministic(kmodule.get(), *kf->function, args); + source = + SourceBuilder::mockDeterministic(kmodule.get(), *kf->function, args); break; } executeMakeSymbolic(state, mo, type, source, false); diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 0c0d384444..3575f64f3b 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -730,6 +730,9 @@ class Executor : public Interpreter { std::unique_ptr origInfos, const std::set &ignoredExternals) override; + std::map + getAllExternals(const std::set &ignoredExternals) override; + void useSeeds(const std::vector *seeds) override { usingSeeds = seeds; } diff --git a/lib/Core/MockBuilder.cpp b/lib/Core/MockBuilder.cpp index b1b93c8b6d..2392458241 100644 --- a/lib/Core/MockBuilder.cpp +++ b/lib/Core/MockBuilder.cpp @@ -16,38 +16,54 @@ MockBuilder::MockBuilder(const llvm::Module *initModule, userEntrypoint(std::move(userEntrypoint)) {} std::unique_ptr MockBuilder::build() { + initMockModule(); + buildMockMain(); + buildExternalFunctionsDefinitions(); + return std::move(mockModule); +} + +void MockBuilder::initMockModule() { mockModule = std::make_unique(userModule->getName().str() + "__klee_externals", userModule->getContext()); mockModule->setTargetTriple(userModule->getTargetTriple()); mockModule->setDataLayout(userModule->getDataLayout()); builder = std::make_unique>(mockModule->getContext()); +} - // Set up entrypoint in new module. Here we'll define globals and then call - // user's entrypoint. - llvm::Function *mainFn = userModule->getFunction(userEntrypoint); - if (!mainFn) { +// Set up entrypoint in new module. Here we'll define external globals and then +// call user's entrypoint. +void MockBuilder::buildMockMain() { + llvm::Function *userMainFn = userModule->getFunction(userEntrypoint); + if (!userMainFn) { klee_error("Entry function '%s' not found in module.", userEntrypoint.c_str()); } - mockModule->getOrInsertFunction(mockEntrypoint, mainFn->getFunctionType(), - mainFn->getAttributes()); - - buildGlobalsDefinition(); - buildFunctionsDefinition(); - return std::move(mockModule); -} - -void MockBuilder::buildGlobalsDefinition() { - llvm::Function *mainFn = mockModule->getFunction(mockEntrypoint); - if (!mainFn) { + mockModule->getOrInsertFunction(mockEntrypoint, userMainFn->getFunctionType(), + userMainFn->getAttributes()); + llvm::Function *mockMainFn = mockModule->getFunction(mockEntrypoint); + if (!mockMainFn) { klee_error("Entry function '%s' not found in module.", mockEntrypoint.c_str()); } auto globalsInitBlock = - llvm::BasicBlock::Create(mockModule->getContext(), "entry", mainFn); + llvm::BasicBlock::Create(mockModule->getContext(), "entry", mockMainFn); builder->SetInsertPoint(globalsInitBlock); + // Define all the external globals + buildExternalGlobalsDefinitions(); + + auto userMainCallee = mockModule->getOrInsertFunction( + userEntrypoint, userMainFn->getFunctionType()); + std::vector args; + args.reserve(userMainFn->arg_size()); + for (auto it = mockMainFn->arg_begin(); it != mockMainFn->arg_end(); it++) { + args.push_back(it); + } + auto callUserMain = builder->CreateCall(userMainCallee, args); + builder->CreateRet(callUserMain); +} +void MockBuilder::buildExternalGlobalsDefinitions() { for (const auto &it : externals) { if (it.second->isFunctionTy()) { continue; @@ -73,24 +89,9 @@ void MockBuilder::buildGlobalsDefinition() { buildCallKleeMakeSymbol("klee_make_symbolic", global, type, "@obj_" + extName); } - - auto *userMainFn = userModule->getFunction(userEntrypoint); - if (!userMainFn) { - klee_error("Entry function '%s' not found in module.", - userEntrypoint.c_str()); - } - auto userMainCallee = mockModule->getOrInsertFunction( - userEntrypoint, userMainFn->getFunctionType()); - std::vector args; - args.reserve(userMainFn->arg_size()); - for (auto it = mainFn->arg_begin(); it != mainFn->arg_end(); it++) { - args.push_back(it); - } - auto callUserMain = builder->CreateCall(userMainCallee, args); - builder->CreateRet(callUserMain); } -void MockBuilder::buildFunctionsDefinition() { +void MockBuilder::buildExternalFunctionsDefinitions() { for (const auto &it : externals) { if (!it.second->isFunctionTy()) { continue; diff --git a/lib/Expr/IndependentSet.cpp b/lib/Expr/IndependentSet.cpp index 16872b6fd7..0e491e4416 100644 --- a/lib/Expr/IndependentSet.cpp +++ b/lib/Expr/IndependentSet.cpp @@ -38,8 +38,7 @@ IndependentElementSet::IndependentElementSet(ref e) { if (ref mockSource = dyn_cast_or_null(array->source)) { - uninterpretedFunctions.insert( - mockSource->function.getName().str()); + uninterpretedFunctions.insert(mockSource->function.getName().str()); } if (!wholeObjects.count(array)) { diff --git a/lib/Expr/SourceBuilder.cpp b/lib/Expr/SourceBuilder.cpp index 305186cb6f..c40ce3dccd 100644 --- a/lib/Expr/SourceBuilder.cpp +++ b/lib/Expr/SourceBuilder.cpp @@ -88,17 +88,19 @@ ref SourceBuilder::irreproducible(const std::string &name) { return r; } -ref SourceBuilder::mockNaive(const KModule *km, const llvm::Function &function,unsigned int version) { +ref SourceBuilder::mockNaive(const KModule *km, + const llvm::Function &function, + unsigned int version) { ref r(new MockNaiveSource(km, function, version)); r->computeHash(); return r; } ref -SourceBuilder::mockDeterministic(const KModule *km, const llvm::Function &function, +SourceBuilder::mockDeterministic(const KModule *km, + const llvm::Function &function, const std::vector> &args) { - ref r( - new MockDeterministicSource(km, function, args)); + ref r(new MockDeterministicSource(km, function, args)); r->computeHash(); return r; } diff --git a/lib/Expr/SymbolicSource.cpp b/lib/Expr/SymbolicSource.cpp index 063ea1235b..0831277d96 100644 --- a/lib/Expr/SymbolicSource.cpp +++ b/lib/Expr/SymbolicSource.cpp @@ -187,9 +187,9 @@ int MockNaiveSource::internalCompare(const SymbolicSource &b) const { return 0; } -MockDeterministicSource::MockDeterministicSource(const KModule *km, - const llvm::Function &function, - const std::vector> &_args) +MockDeterministicSource::MockDeterministicSource( + const KModule *km, const llvm::Function &function, + const std::vector> &_args) : MockSource(km, function), args(_args) {} unsigned MockDeterministicSource::computeHash() { diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp index 879af1f616..799ce046d5 100644 --- a/lib/Solver/Z3Builder.cpp +++ b/lib/Solver/Z3Builder.cpp @@ -283,9 +283,8 @@ Z3ASTHandle Z3Builder::getInitialArray(const Array *root) { Z3_mk_func_decl( ctx, Z3_mk_string_symbol( - ctx, mockDeterministicSource->function.getName() - .str() - .c_str()), + ctx, + mockDeterministicSource->function.getName().str().c_str()), num_args, argsSort.data(), retValSort), ctx); array_expr = diff --git a/test/Feature/MockStrategies.c b/test/Feature/MockStrategies.c index a47437e292..524fbba3a2 100644 --- a/test/Feature/MockStrategies.c +++ b/test/Feature/MockStrategies.c @@ -18,7 +18,7 @@ // CHECK-3: KLEE: ERROR: Deterministic mocks can be generated with Z3 solver only. // RUN: rm -rf %t.klee-out-4 -// RUN: %klee --output-dir=%t.klee-out-4 --use-independent-solver=false --solver-backend=z3 --external-calls=all --mock-strategy=deterministic %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-4 +// RUN: %klee --output-dir=%t.klee-out-4 --solver-backend=z3 --external-calls=all --mock-strategy=deterministic %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-4 // CHECK-4: KLEE: done: completed paths = 2 // CHECK-4: KLEE: done: generated tests = 2 From 4097878675f58c297fc6f3edc2b7f8e8eb20f8e8 Mon Sep 17 00:00:00 2001 From: Lana243 Date: Tue, 27 Jun 2023 18:45:13 +0300 Subject: [PATCH 13/25] Add script for replaying tests and test case --- scripts/run_tests_with_mocks.py | 26 +++++++++++++++++++++++ test/Replay/libkleeruntest/replay_mocks.c | 13 ++++++++++++ test/lit.cfg | 4 ++++ 3 files changed, 43 insertions(+) create mode 100755 scripts/run_tests_with_mocks.py create mode 100644 test/Replay/libkleeruntest/replay_mocks.c diff --git a/scripts/run_tests_with_mocks.py b/scripts/run_tests_with_mocks.py new file mode 100755 index 0000000000..16644e9387 --- /dev/null +++ b/scripts/run_tests_with_mocks.py @@ -0,0 +1,26 @@ +#!/usr/bin/env python + +# This script builds executable file using initial bitcode file and artifacts produced by KLEE. +# To run the script provide all the arguments you want to pass to clang for building executable. +# +# NOTE: Pre-last argument should be a path to KLEE output directory which contains redefinitions.txt and externals.ll. +# NOTE: Last argument is path to initial bitcode. +# +# Example: python3 run_tests_with_mocks.py -I ~/klee/include/ -L ~/klee/build/lib/ -lkleeRuntest klee-last a.bc +# +# You can read more about replaying test cases here: http://klee.github.io/tutorials/testing-function/ + +import subprocess as sp +import sys +import os + +klee_out_dir = sys.argv[-2] +bitcode = sys.argv[-1] + +filename = os.path.splitext(bitcode)[0] +object_file = f'{filename}.o' +sp.run(f'clang -c {bitcode} -o {object_file}', shell=True) +sp.run(f'llvm-objcopy {object_file} --redefine-syms {klee_out_dir}/redefinitions.txt', shell=True) +clang_args = ' '.join(sys.argv[1:len(sys.argv) - 2]) +print(f'clang {clang_args} {klee_out_dir}/externals.ll {object_file}') +sp.run(f'clang {clang_args} {klee_out_dir}/externals.ll {object_file}', shell=True) diff --git a/test/Replay/libkleeruntest/replay_mocks.c b/test/Replay/libkleeruntest/replay_mocks.c new file mode 100644 index 0000000000..d234925eb0 --- /dev/null +++ b/test/Replay/libkleeruntest/replay_mocks.c @@ -0,0 +1,13 @@ +// RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --external-calls=all --mock-strategy=naive %t.bc +// RUN: %runmocks %libkleeruntest -o %t.klee-out/a.out %t.klee-out %t.bc +// RUN: test -f %t.klee-out/test000001.ktest + +extern int foo(int); + +int main() { + int a; + klee_make_symbolic(&a, sizeof(a), "a"); + return foo(a); +} diff --git a/test/lit.cfg b/test/lit.cfg index 75978e47b7..cef5c7b4eb 100644 --- a/test/lit.cfg +++ b/test/lit.cfg @@ -97,6 +97,10 @@ for name in subs: lit_config.fatal('{0} is not set'.format(name)) config.substitutions.append( ('%' + name, value)) +config.substitutions.append( + ('%runmocks', os.path.join(klee_src_root, 'scripts/run_tests_with_mocks.py')) +) + # Add a substitution for lli. config.substitutions.append( ('%lli', os.path.join(llvm_tools_dir, 'lli')) From 99cf70834c9a63b9c5dd428f5e7218ea00251703 Mon Sep 17 00:00:00 2001 From: Lana243 Date: Tue, 27 Jun 2023 19:00:23 +0300 Subject: [PATCH 14/25] Fix --- scripts/run_tests_with_mocks.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/run_tests_with_mocks.py b/scripts/run_tests_with_mocks.py index 16644e9387..5843a37ad0 100755 --- a/scripts/run_tests_with_mocks.py +++ b/scripts/run_tests_with_mocks.py @@ -1,4 +1,4 @@ -#!/usr/bin/env python +#!/usr/bin/env python3 # This script builds executable file using initial bitcode file and artifacts produced by KLEE. # To run the script provide all the arguments you want to pass to clang for building executable. From 15d5097001875cf2a75cacfb426cc6909ba8b0e8 Mon Sep 17 00:00:00 2001 From: Lana243 Date: Wed, 28 Jun 2023 14:19:17 +0300 Subject: [PATCH 15/25] Updated test --- test/Replay/libkleeruntest/replay_mocks.c | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/test/Replay/libkleeruntest/replay_mocks.c b/test/Replay/libkleeruntest/replay_mocks.c index d234925eb0..43e86937f2 100644 --- a/test/Replay/libkleeruntest/replay_mocks.c +++ b/test/Replay/libkleeruntest/replay_mocks.c @@ -3,11 +3,14 @@ // RUN: %klee --output-dir=%t.klee-out --external-calls=all --mock-strategy=naive %t.bc // RUN: %runmocks %libkleeruntest -o %t.klee-out/a.out %t.klee-out %t.bc // RUN: test -f %t.klee-out/test000001.ktest +// RUN: env KTEST_FILE=%t.klee-out/test000001.ktest %t.klee-out/a.out + +extern int variable; extern int foo(int); int main() { int a; klee_make_symbolic(&a, sizeof(a), "a"); - return foo(a); + return variable + foo(a); } From 31b93c5e19a9975cd774ece46817f889f6813bd4 Mon Sep 17 00:00:00 2001 From: Lana243 Date: Wed, 28 Jun 2023 15:07:47 +0300 Subject: [PATCH 16/25] Fix test --- test/Replay/libkleeruntest/replay_mocks.c | 4 +++- test/lit.cfg | 5 +++++ 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/test/Replay/libkleeruntest/replay_mocks.c b/test/Replay/libkleeruntest/replay_mocks.c index 43e86937f2..25bf1bb7b4 100644 --- a/test/Replay/libkleeruntest/replay_mocks.c +++ b/test/Replay/libkleeruntest/replay_mocks.c @@ -1,7 +1,9 @@ // RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --external-calls=all --mock-strategy=naive %t.bc -// RUN: %runmocks %libkleeruntest -o %t.klee-out/a.out %t.klee-out %t.bc +// RUN: %clang -c %t.bc -o %t.o +// RUN: %llvmobjcopy --redefine-syms %t.klee-out/redefinitions.txt %t.o +// RUN: %clang -o %t.klee-out/a.out %libkleeruntest %t.klee-out/externals.ll %t.o // RUN: test -f %t.klee-out/test000001.ktest // RUN: env KTEST_FILE=%t.klee-out/test000001.ktest %t.klee-out/a.out diff --git a/test/lit.cfg b/test/lit.cfg index cef5c7b4eb..b1eb82cf48 100644 --- a/test/lit.cfg +++ b/test/lit.cfg @@ -118,6 +118,11 @@ config.substitutions.append( ('%llvmlink', os.path.join(llvm_tools_dir, 'llvm-link')) ) +# Add a substitution for llvm-objcopy +config.substitutions.append( + ('%llvmobjcopy', os.path.join(llvm_tools_dir, 'llvm-objcopy')) +) + # Add a substition for libkleeruntest config.substitutions.append( ('%libkleeruntestdir', os.path.dirname(config.libkleeruntest)) From 8c9f8e63b5bb21e97aae47bb60bfaacd19b0ba6e Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Wed, 28 Jun 2023 22:31:45 +0400 Subject: [PATCH 17/25] [fix] Update test and build.yml --- lib/Core/Executor.cpp | 2 +- lib/Core/MockBuilder.cpp | 7 ++++++- {include/klee => lib}/Core/MockBuilder.h | 4 ++++ lib/Expr/SymbolicSource.cpp | 2 +- test/Feature/MockPointersDeterministic.c | 2 +- test/Replay/libkleeruntest/replay_mocks.c | 1 + tools/klee/main.cpp | 23 +++++++++++------------ 7 files changed, 25 insertions(+), 16 deletions(-) rename {include/klee => lib}/Core/MockBuilder.h (89%) diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 5c3c1453e5..5a1c3c2721 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -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" @@ -38,7 +39,6 @@ #include "klee/Config/Version.h" #include "klee/Config/config.h" #include "klee/Core/Interpreter.h" -#include "klee/Core/MockBuilder.h" #include "klee/Expr/ArrayExprOptimizer.h" #include "klee/Expr/ArrayExprVisitor.h" #include "klee/Expr/Assignment.h" diff --git a/lib/Core/MockBuilder.cpp b/lib/Core/MockBuilder.cpp index 2392458241..020d3d081c 100644 --- a/lib/Core/MockBuilder.cpp +++ b/lib/Core/MockBuilder.cpp @@ -1,8 +1,13 @@ -#include "klee/Core/MockBuilder.h" +#include "MockBuilder.h" #include "klee/Support/ErrorHandling.h" + +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/IR/IRBuilder.h" #include "llvm/IR/Module.h" +DISABLE_WARNING_POP #include diff --git a/include/klee/Core/MockBuilder.h b/lib/Core/MockBuilder.h similarity index 89% rename from include/klee/Core/MockBuilder.h rename to lib/Core/MockBuilder.h index 70949b10a7..ae1d983221 100644 --- a/include/klee/Core/MockBuilder.h +++ b/lib/Core/MockBuilder.h @@ -1,8 +1,12 @@ #ifndef KLEE_MOCKBUILDER_H #define KLEE_MOCKBUILDER_H +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/IR/IRBuilder.h" #include "llvm/IR/Module.h" +DISABLE_WARNING_POP #include #include diff --git a/lib/Expr/SymbolicSource.cpp b/lib/Expr/SymbolicSource.cpp index 0831277d96..3857d53db7 100644 --- a/lib/Expr/SymbolicSource.cpp +++ b/lib/Expr/SymbolicSource.cpp @@ -1,6 +1,6 @@ #include "klee/Expr/SymbolicSource.h" -#include "klee/Expr/Expr.h" +#include "klee/Expr/Expr.h" #include "klee/Expr/ExprPPrinter.h" #include "klee/Expr/ExprUtil.h" #include "klee/Module/KInstruction.h" diff --git a/test/Feature/MockPointersDeterministic.c b/test/Feature/MockPointersDeterministic.c index d8c871588d..16450714e3 100644 --- a/test/Feature/MockPointersDeterministic.c +++ b/test/Feature/MockPointersDeterministic.c @@ -2,7 +2,7 @@ // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t.bc // RUN: rm -rf %t.klee-out-1 -// RUN: %klee --solver-backend=z3 --output-dir=%t.klee-out-1 --skip-not-lazy-initialized --external-calls=all --mock-strategy=deterministic %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t.klee-out-1 --min-number-elements-li=0 --use-sym-size-li --skip-not-lazy-initialized --external-calls=all --mock-strategy=deterministic %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-1 // CHECK-1: memory error: null pointer exception // CHECK-1: KLEE: done: completed paths = 1 // CHECK-1: KLEE: done: partially completed paths = 2 diff --git a/test/Replay/libkleeruntest/replay_mocks.c b/test/Replay/libkleeruntest/replay_mocks.c index 25bf1bb7b4..cfd151a9e5 100644 --- a/test/Replay/libkleeruntest/replay_mocks.c +++ b/test/Replay/libkleeruntest/replay_mocks.c @@ -1,3 +1,4 @@ +// REQUIRES: geq-llvm-11.0 // RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --external-calls=all --mock-strategy=naive %t.bc diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 64d0593fb3..e8b3672302 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -888,10 +888,10 @@ static const char *modelledExternals[] = { "klee_get_valuef", "klee_get_valued", "klee_get_valuel", "klee_get_valuell", "klee_get_value_i32", "klee_get_value_i64", "klee_get_obj_size", "klee_is_symbolic", "klee_make_symbolic", "klee_make_mock", - "klee_mark_global", "klee_open_merge", "klee_close_merge", - "klee_prefer_cex", "klee_posix_prefer_cex", "klee_print_expr", - "klee_print_range", "klee_report_error", "klee_set_forking", - "klee_silent_exit", "klee_warning", "klee_warning_once", "klee_stack_trace", + "klee_mark_global", "klee_prefer_cex", "klee_posix_prefer_cex", + "klee_print_expr", "klee_print_range", "klee_report_error", + "klee_set_forking", "klee_silent_exit", "klee_warning", "klee_warning_once", + "klee_stack_trace", #ifdef SUPPORT_KLEE_EH_CXX "_klee_eh_Unwind_RaiseException_impl", "klee_eh_typeid_for", #endif @@ -1219,7 +1219,7 @@ createLibCWrapper(std::vector> &userModules, args.push_back(llvm::ConstantExpr::getBitCast( cast(inModuleReference.getCallee()), ft->getParamType(0))); - args.push_back(&*(stub->arg_begin())); // argc + args.push_back(&*(stub->arg_begin())); // argc auto arg_it = stub->arg_begin(); args.push_back(&*(++arg_it)); // argv args.push_back(Constant::getNullValue(ft->getParamType(3))); // app_init @@ -1589,10 +1589,9 @@ int main(int argc, char **argv, char **envp) { sys::SetInterruptFunction(interrupt_handle); + // Load the bytecode... std::string errorMsg; LLVMContext ctx; - - // Load the bytecode... std::vector> loadedUserModules; std::vector> loadedLibsModules; if (!klee::loadFileAsOneModule(InputFile, ctx, loadedUserModules, errorMsg)) { @@ -1652,11 +1651,6 @@ int main(int argc, char **argv, char **envp) { "This may cause unexpected crashes or assertion violations.", module_triple.c_str(), host_triple.c_str()); - llvm::Function *initialMainFn = mainModule->getFunction(EntryPoint); - if (!initialMainFn) { - klee_error("Entry function '%s' not found in module.", EntryPoint.c_str()); - } - // Detect architecture std::string opt_suffix = "64"; // Fall back to 64bit if (module_triple.find("i686") != std::string::npos || @@ -1696,6 +1690,11 @@ int main(int argc, char **argv, char **envp) { if (EntryPoint.empty()) klee_error("entry-point cannot be empty"); + llvm::Function *initialMainFn = mainModule->getFunction(EntryPoint); + if (!initialMainFn) { + klee_error("Entry function '%s' not found in module.", EntryPoint.c_str()); + } + for (auto &module : loadedUserModules) { entryFn = module->getFunction(EntryPoint); if (entryFn) From 8b3cf70fdd6b4b0ca6981f737d048f5fc0111742 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Mon, 24 Jul 2023 06:06:36 +0400 Subject: [PATCH 18/25] [fixup] Fix the test --- test/Replay/libkleeruntest/replay_mocks.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/Replay/libkleeruntest/replay_mocks.c b/test/Replay/libkleeruntest/replay_mocks.c index cfd151a9e5..5bf420753e 100644 --- a/test/Replay/libkleeruntest/replay_mocks.c +++ b/test/Replay/libkleeruntest/replay_mocks.c @@ -4,7 +4,7 @@ // RUN: %klee --output-dir=%t.klee-out --external-calls=all --mock-strategy=naive %t.bc // RUN: %clang -c %t.bc -o %t.o // RUN: %llvmobjcopy --redefine-syms %t.klee-out/redefinitions.txt %t.o -// RUN: %clang -o %t.klee-out/a.out %libkleeruntest %t.klee-out/externals.ll %t.o +// RUN: %clang %libkleeruntest -Wl,-rpath %libkleeruntestdir %t.klee-out/externals.ll -o %t.klee-out/a.out %t.o // RUN: test -f %t.klee-out/test000001.ktest // RUN: env KTEST_FILE=%t.klee-out/test000001.ktest %t.klee-out/a.out From 3bd5a74c20de0481cdd9ab3c9400d70fa1b3388d Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Mon, 24 Jul 2023 06:07:00 +0400 Subject: [PATCH 19/25] [fix] Add include --- lib/Core/MockBuilder.h | 1 + 1 file changed, 1 insertion(+) diff --git a/lib/Core/MockBuilder.h b/lib/Core/MockBuilder.h index ae1d983221..eff3fdeb02 100644 --- a/lib/Core/MockBuilder.h +++ b/lib/Core/MockBuilder.h @@ -8,6 +8,7 @@ DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/IR/Module.h" DISABLE_WARNING_POP +#include #include #include From ef6c71283a13433f39ab0c6af3db10607479eff6 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Mon, 24 Jul 2023 11:47:57 +0400 Subject: [PATCH 20/25] [fix] Fix build --- lib/Core/MockBuilder.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/lib/Core/MockBuilder.cpp b/lib/Core/MockBuilder.cpp index 020d3d081c..ba2713eec8 100644 --- a/lib/Core/MockBuilder.cpp +++ b/lib/Core/MockBuilder.cpp @@ -124,7 +124,12 @@ void MockBuilder::buildExternalFunctionsDefinitions() { builder->CreateAlloca(func->getReturnType(), nullptr); buildCallKleeMakeSymbol("klee_make_mock", mockReturnValue, func->getReturnType(), "@call_" + extName); +#if LLVM_VERSION_CODE >= LLVM_VERSION(14, 0) + auto *loadInst = + builder->CreateLoad(func->getReturnType(), mockReturnValue, "klee_var"); +#else auto *loadInst = builder->CreateLoad(mockReturnValue, "klee_var"); +#endif builder->CreateRet(loadInst); } } @@ -143,7 +148,12 @@ void MockBuilder::buildCallKleeMakeSymbol(const std::string &klee_function_name, auto bitcastInst = builder->CreateBitCast( source, llvm::Type::getInt8PtrTy(mockModule->getContext())); auto str_name = builder->CreateGlobalString(symbol_name); +#if LLVM_VERSION_CODE >= LLVM_VERSION(14, 0) + auto gep = builder->CreateConstInBoundsGEP2_64( + llvm::Type::getInt8PtrTy(mockModule->getContext()), str_name, 0, 0); +#else auto gep = builder->CreateConstInBoundsGEP2_64(str_name, 0, 0); +#endif builder->CreateCall( kleeMakeSymbolCallee, {bitcastInst, From 9144b59256392a62b80906fe7476f7edf6d53bd0 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Wed, 26 Jul 2023 22:24:20 +0400 Subject: [PATCH 21/25] [fix] CI --- .github/workflows/build.yaml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml index dc2c95350c..8dd403ade7 100644 --- a/.github/workflows/build.yaml +++ b/.github/workflows/build.yaml @@ -139,6 +139,7 @@ jobs: runs-on: macos-latest env: BASE: /tmp + LLVM_VERSION: 13 SOLVERS: STP UCLIBC_VERSION: 0 USE_TCMALLOC: 0 From 69d9229d0b877c452ab45ffcb24ee067bae7ac5b Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Thu, 27 Jul 2023 00:20:39 +0400 Subject: [PATCH 22/25] [fix] `buildCallKleeMakeSymbol` --- lib/Core/MockBuilder.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/lib/Core/MockBuilder.cpp b/lib/Core/MockBuilder.cpp index ba2713eec8..c30b8fda55 100644 --- a/lib/Core/MockBuilder.cpp +++ b/lib/Core/MockBuilder.cpp @@ -147,10 +147,10 @@ void MockBuilder::buildCallKleeMakeSymbol(const std::string &klee_function_name, mockModule->getOrInsertFunction(klee_function_name, klee_mk_symb_type); auto bitcastInst = builder->CreateBitCast( source, llvm::Type::getInt8PtrTy(mockModule->getContext())); - auto str_name = builder->CreateGlobalString(symbol_name); + auto str_name = builder->CreateGlobalStringPtr(symbol_name); #if LLVM_VERSION_CODE >= LLVM_VERSION(14, 0) - auto gep = builder->CreateConstInBoundsGEP2_64( - llvm::Type::getInt8PtrTy(mockModule->getContext()), str_name, 0, 0); + auto ptrTy = llvm::Type::getInt8PtrTy(mockModule->getContext()); + auto gep = builder->CreateConstInBoundsGEP1_64(ptrTy, str_name, 0); #else auto gep = builder->CreateConstInBoundsGEP2_64(str_name, 0, 0); #endif From 4be9c8dcc8a01dc1614abf259c4256dcf4ce0b0d Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Thu, 27 Jul 2023 03:28:48 +0400 Subject: [PATCH 23/25] [fix] --- .github/workflows/build.yaml | 1 - lib/Core/MockBuilder.cpp | 13 +++++++++---- test/CMakeLists.txt | 1 + test/Replay/libkleeruntest/replay_mocks.c | 5 +++-- test/lit.cfg | 2 +- test/lit.site.cfg.in | 1 + 6 files changed, 15 insertions(+), 8 deletions(-) diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml index 8dd403ade7..dc2c95350c 100644 --- a/.github/workflows/build.yaml +++ b/.github/workflows/build.yaml @@ -139,7 +139,6 @@ jobs: runs-on: macos-latest env: BASE: /tmp - LLVM_VERSION: 13 SOLVERS: STP UCLIBC_VERSION: 0 USE_TCMALLOC: 0 diff --git a/lib/Core/MockBuilder.cpp b/lib/Core/MockBuilder.cpp index c30b8fda55..1c430e9fa0 100644 --- a/lib/Core/MockBuilder.cpp +++ b/lib/Core/MockBuilder.cpp @@ -147,12 +147,17 @@ void MockBuilder::buildCallKleeMakeSymbol(const std::string &klee_function_name, mockModule->getOrInsertFunction(klee_function_name, klee_mk_symb_type); auto bitcastInst = builder->CreateBitCast( source, llvm::Type::getInt8PtrTy(mockModule->getContext())); - auto str_name = builder->CreateGlobalStringPtr(symbol_name); + auto str_name = builder->CreateGlobalString(symbol_name); + auto mockReturnValue = builder->CreateAlloca(str_name->getType()); + builder->CreateStore(str_name, mockReturnValue); + auto mockStr = builder->CreateLoad(str_name->getType(), mockReturnValue); + auto bitcastStr = builder->CreateBitCast( + mockStr, llvm::Type::getInt8PtrTy(mockModule->getContext())); #if LLVM_VERSION_CODE >= LLVM_VERSION(14, 0) - auto ptrTy = llvm::Type::getInt8PtrTy(mockModule->getContext()); - auto gep = builder->CreateConstInBoundsGEP1_64(ptrTy, str_name, 0); + auto ptrTy = llvm::Type::getInt8Ty(mockModule->getContext()); + auto gep = builder->CreateConstInBoundsGEP1_64(ptrTy, bitcastStr, 0); #else - auto gep = builder->CreateConstInBoundsGEP2_64(str_name, 0, 0); + auto gep = builder->CreateConstInBoundsGEP1_64(bitcastStr, 0); #endif builder->CreateCall( kleeMakeSymbolCallee, diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 17723d865f..b9d8615b0a 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -15,6 +15,7 @@ set(LLVM_TOOLS_DIR "${LLVM_TOOLS_BINARY_DIR}") set(LLVMCC "${LLVMCC} -I${CMAKE_SOURCE_DIR}/include") set(LLVMCXX "${LLVMCXX} -I${CMAKE_SOURCE_DIR}/include") set(NATIVE_CC "${CMAKE_C_COMPILER} ${CMAKE_C_FLAGS} -I ${CMAKE_SOURCE_DIR}/include") +set(NATIVE_OBJCOPY "${CMAKE_OBJCOPY} -I ${CMAKE_SOURCE_DIR}/include") set(NATIVE_CXX "${CMAKE_CXX_COMPILER} ${CMAKE_CXX_FLAGS} -I ${CMAKE_SOURCE_DIR}/include") set(TARGET_TRIPLE "${TARGET_TRIPLE}") diff --git a/test/Replay/libkleeruntest/replay_mocks.c b/test/Replay/libkleeruntest/replay_mocks.c index 5bf420753e..e6b08b2926 100644 --- a/test/Replay/libkleeruntest/replay_mocks.c +++ b/test/Replay/libkleeruntest/replay_mocks.c @@ -1,12 +1,13 @@ // REQUIRES: geq-llvm-11.0 +// REQUIRES: not-darwin // RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --external-calls=all --mock-strategy=naive %t.bc // RUN: %clang -c %t.bc -o %t.o // RUN: %llvmobjcopy --redefine-syms %t.klee-out/redefinitions.txt %t.o -// RUN: %clang %libkleeruntest -Wl,-rpath %libkleeruntestdir %t.klee-out/externals.ll -o %t.klee-out/a.out %t.o +// RUN: %cc %libkleeruntest -Wl,-rpath %libkleeruntestdir %t.klee-out/externals.ll -o %t_runner %t.o // RUN: test -f %t.klee-out/test000001.ktest -// RUN: env KTEST_FILE=%t.klee-out/test000001.ktest %t.klee-out/a.out +// RUN: env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner extern int variable; diff --git a/test/lit.cfg b/test/lit.cfg index b1eb82cf48..069d97a3f5 100644 --- a/test/lit.cfg +++ b/test/lit.cfg @@ -90,7 +90,7 @@ if config.test_exec_root is None: # Add substitutions from lit.site.cfg -subs = [ 'clangxx', 'clang', 'cc', 'cxx', 'O0opt', 'c_prefixes_8', 'c_prefixes_10', 'cpp_prefixes_10' ] +subs = [ 'clangxx', 'clang', 'cc', 'objcopy', 'cxx', 'O0opt', 'c_prefixes_8', 'c_prefixes_10', 'cpp_prefixes_10' ] for name in subs: value = getattr(config, name, None) if value == None: diff --git a/test/lit.site.cfg.in b/test/lit.site.cfg.in index 15bc4a20a5..010cc5d152 100644 --- a/test/lit.site.cfg.in +++ b/test/lit.site.cfg.in @@ -35,6 +35,7 @@ config.clang = "@LLVMCC@" config.clangxx = "@LLVMCXX@" config.cc = "@NATIVE_CC@" +config.objcopy = "@NATIVE_OBJCOPY@" config.cxx = "@NATIVE_CXX@" # NOTE: any changes to compiler flags also have to be applied to From 6bff4fc956cac9bd20b26f86084b68fe0da71dfd Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Fri, 28 Jul 2023 01:18:14 +0400 Subject: [PATCH 24/25] [fix] --- test/Replay/libkleeruntest/replay_mocks.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/Replay/libkleeruntest/replay_mocks.c b/test/Replay/libkleeruntest/replay_mocks.c index e6b08b2926..411df3e9db 100644 --- a/test/Replay/libkleeruntest/replay_mocks.c +++ b/test/Replay/libkleeruntest/replay_mocks.c @@ -5,7 +5,7 @@ // RUN: %klee --output-dir=%t.klee-out --external-calls=all --mock-strategy=naive %t.bc // RUN: %clang -c %t.bc -o %t.o // RUN: %llvmobjcopy --redefine-syms %t.klee-out/redefinitions.txt %t.o -// RUN: %cc %libkleeruntest -Wl,-rpath %libkleeruntestdir %t.klee-out/externals.ll -o %t_runner %t.o +// RUN: %clang %s %libkleeruntest -Wl,-rpath %libkleeruntestdir %t.klee-out/externals.ll -o %t_runner %t.o // RUN: test -f %t.klee-out/test000001.ktest // RUN: env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner From 6f911818204052bd99ea7a8bab2cdda016212d49 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Fri, 28 Jul 2023 16:30:20 +0400 Subject: [PATCH 25/25] [fix] --- test/CMakeLists.txt | 2 +- test/Replay/libkleeruntest/replay_mocks.c | 5 +++-- test/lit.cfg | 6 ++++++ 3 files changed, 10 insertions(+), 3 deletions(-) diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index b9d8615b0a..c7d14ed87e 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -15,7 +15,7 @@ set(LLVM_TOOLS_DIR "${LLVM_TOOLS_BINARY_DIR}") set(LLVMCC "${LLVMCC} -I${CMAKE_SOURCE_DIR}/include") set(LLVMCXX "${LLVMCXX} -I${CMAKE_SOURCE_DIR}/include") set(NATIVE_CC "${CMAKE_C_COMPILER} ${CMAKE_C_FLAGS} -I ${CMAKE_SOURCE_DIR}/include") -set(NATIVE_OBJCOPY "${CMAKE_OBJCOPY} -I ${CMAKE_SOURCE_DIR}/include") +set(NATIVE_OBJCOPY "${CMAKE_OBJCOPY}") set(NATIVE_CXX "${CMAKE_CXX_COMPILER} ${CMAKE_CXX_FLAGS} -I ${CMAKE_SOURCE_DIR}/include") set(TARGET_TRIPLE "${TARGET_TRIPLE}") diff --git a/test/Replay/libkleeruntest/replay_mocks.c b/test/Replay/libkleeruntest/replay_mocks.c index 411df3e9db..bb9c9e7691 100644 --- a/test/Replay/libkleeruntest/replay_mocks.c +++ b/test/Replay/libkleeruntest/replay_mocks.c @@ -4,8 +4,9 @@ // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --external-calls=all --mock-strategy=naive %t.bc // RUN: %clang -c %t.bc -o %t.o -// RUN: %llvmobjcopy --redefine-syms %t.klee-out/redefinitions.txt %t.o -// RUN: %clang %s %libkleeruntest -Wl,-rpath %libkleeruntestdir %t.klee-out/externals.ll -o %t_runner %t.o +// RUN: %llc %t.klee-out/externals.ll -filetype=obj -o %t_externals.o +// RUN: %objcopy --redefine-syms %t.klee-out/redefinitions.txt %t.o +// RUN: %cc -no-pie %t_externals.o %t.o %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner // RUN: test -f %t.klee-out/test000001.ktest // RUN: env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner diff --git a/test/lit.cfg b/test/lit.cfg index 069d97a3f5..83d7a0f2a3 100644 --- a/test/lit.cfg +++ b/test/lit.cfg @@ -105,6 +105,12 @@ config.substitutions.append( config.substitutions.append( ('%lli', os.path.join(llvm_tools_dir, 'lli')) ) + +# Add a substitution for llc. +config.substitutions.append( + ('%llc', os.path.join(llvm_tools_dir, 'llc')) +) + # Add a substitution for llvm-as config.substitutions.append( ('%llvmas', os.path.join(llvm_tools_dir, 'llvm-as'))