From 52897578a3bbd88f6eeefc5755f5c1295cef8bf9 Mon Sep 17 00:00:00 2001 From: Vladislav Kalugin Date: Tue, 25 Jul 2023 17:03:05 +0300 Subject: [PATCH] Add annotation implementation and tests --- .github/workflows/build.yaml | 1 - .gitmodules | 7 +- CMakeLists.txt | 17 +- include/klee/Config/config.h.cmin | 3 + include/klee/Core/Interpreter.h | 21 +- include/klee/Core/MockBuilder.h | 51 +- include/klee/Module/Annotation.h | 110 ++-- lib/Core/ExecutionState.cpp | 2 +- lib/Core/Executor.cpp | 108 +--- lib/Core/Executor.h | 21 +- lib/Core/MockBuilder.cpp | 576 ++++++++++++++---- lib/Core/SpecialFunctionHandler.cpp | 61 +- lib/Module/Annotation.cpp | 387 +++++++++--- lib/Module/CMakeLists.txt | 7 + lib/Solver/Z3Builder.cpp | 5 - runtime/Mocks/models.c | 6 +- scripts/cooddy_annotations.py | 41 ++ json => submodules/json | 0 optional => submodules/optional | 0 submodules/pugiconfig.hpp | 81 +++ submodules/pugixml | 1 + test/CMakeLists.txt | 1 + test/Feature/Annotation/AllocSource.c | 66 ++ test/Feature/Annotation/AllocSource.json | 40 ++ test/Feature/Annotation/BrokenAnnotation.json | 11 + test/Feature/Annotation/Deref.c | 104 ++++ test/Feature/Annotation/Deref.json | 67 ++ test/Feature/Annotation/EmptyAnnotation.json | 1 + test/Feature/Annotation/General.c | 43 ++ test/Feature/Annotation/General.json | 24 + test/Feature/Annotation/InitNull.c | 68 +++ test/Feature/Annotation/InitNull.json | 40 ++ test/Feature/Annotation/InitNullEmpty.json | 32 + test/Feature/MockPointersDeterministic.c | 5 +- test/Replay/libkleeruntest/replay_mocks.c | 8 +- test/lit.cfg | 8 +- test/lit.site.cfg.in | 1 + tools/klee/main.cpp | 92 ++- unittests/Annotations/AnnotationsTest.cpp | 81 +-- 39 files changed, 1712 insertions(+), 486 deletions(-) create mode 100755 scripts/cooddy_annotations.py rename json => submodules/json (100%) rename optional => submodules/optional (100%) create mode 100644 submodules/pugiconfig.hpp create mode 160000 submodules/pugixml create mode 100644 test/Feature/Annotation/AllocSource.c create mode 100644 test/Feature/Annotation/AllocSource.json create mode 100644 test/Feature/Annotation/BrokenAnnotation.json create mode 100644 test/Feature/Annotation/Deref.c create mode 100644 test/Feature/Annotation/Deref.json create mode 100644 test/Feature/Annotation/EmptyAnnotation.json create mode 100644 test/Feature/Annotation/General.c create mode 100644 test/Feature/Annotation/General.json create mode 100644 test/Feature/Annotation/InitNull.c create mode 100644 test/Feature/Annotation/InitNull.json create mode 100644 test/Feature/Annotation/InitNullEmpty.json diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml index 96f09aee22..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: 11 SOLVERS: STP UCLIBC_VERSION: 0 USE_TCMALLOC: 0 diff --git a/.gitmodules b/.gitmodules index d21b6002fc..499a72a1e0 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,6 +1,9 @@ [submodule "json"] - path = json + path = submodules/json url = https://github.com/nlohmann/json.git [submodule "optional"] - path = optional + path = submodules/optional url = https://github.com/martinmoene/optional-lite.git +[submodule "submodules/pugixml"] + path = submodules/pugixml + url = https://github.com/zeux/pugixml.git diff --git a/CMakeLists.txt b/CMakeLists.txt index 18d853e189..3aa00e964a 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -667,8 +667,21 @@ configure_file(${CMAKE_SOURCE_DIR}/include/klee/Config/CompileTimeInfo.h.cmin ################################################################################ include_directories("${CMAKE_BINARY_DIR}/include") include_directories("${CMAKE_SOURCE_DIR}/include") -include_directories("${CMAKE_SOURCE_DIR}/json/include") -include_directories("${CMAKE_SOURCE_DIR}/optional/include") +include_directories("${CMAKE_SOURCE_DIR}/submodules/json/include") +include_directories("${CMAKE_SOURCE_DIR}/submodules/optional/include") + + +option(ENABLE_XML_ANNOTATION "Enable XML annotation" ON) + +if (ENABLE_XML_ANNOTATION) + message(STATUS "XML annotation is enabled") + file(COPY "${CMAKE_SOURCE_DIR}/submodules/pugiconfig.hpp" + DESTINATION "${CMAKE_SOURCE_DIR}/submodules/pugixml/src") + include_directories("${CMAKE_SOURCE_DIR}/submodules/pugixml/src") +else() + message(STATUS "XML annotation is disabled") + set(ENABLE_XML_ANNOTATION 0) +endif() # set(KLEE_INCLUDE_DIRS ${CMAKE_SOURCE_DIR}/include ${CMAKE_BINARY_DIR}/include) ################################################################################ diff --git a/include/klee/Config/config.h.cmin b/include/klee/Config/config.h.cmin index 91dbaf6868..d85622daf6 100644 --- a/include/klee/Config/config.h.cmin +++ b/include/klee/Config/config.h.cmin @@ -122,4 +122,7 @@ macro for that. That would simplify the C++ code. */ /* Install directory for KLEE runtime */ #define KLEE_INSTALL_RUNTIME_DIR "@KLEE_INSTALL_RUNTIME_DIR@" +/* Enable XML annotation parser */ +#define ENABLE_XML_ANNOTATION "@ENABLE_XML_ANNOTATION@" + #endif /* KLEE_CONFIG_H */ diff --git a/include/klee/Core/Interpreter.h b/include/klee/Core/Interpreter.h index ec7d291e2c..bdebe1a221 100644 --- a/include/klee/Core/Interpreter.h +++ b/include/klee/Core/Interpreter.h @@ -93,25 +93,31 @@ class Interpreter { std::string OptSuffix; std::string MainCurrentName; std::string MainNameAfterMock; + std::string AnnotationsFile; bool Optimize; bool Simplify; bool CheckDivZero; bool CheckOvershift; + bool AnnotateOnlyExternal; bool WithFPRuntime; bool WithPOSIXRuntime; ModuleOptions(const std::string &_LibraryDir, const std::string &_EntryPoint, const std::string &_OptSuffix, const std::string &_MainCurrentName, - const std::string &_MainNameAfterMock, bool _Optimize, + const std::string &_MainNameAfterMock, + const std::string &_AnnotationsFile, bool _Optimize, bool _Simplify, bool _CheckDivZero, bool _CheckOvershift, - bool _WithFPRuntime, bool _WithPOSIXRuntime) + bool _AnnotateOnlyExternal, bool _WithFPRuntime, + bool _WithPOSIXRuntime) : LibraryDir(_LibraryDir), EntryPoint(_EntryPoint), OptSuffix(_OptSuffix), MainCurrentName(_MainCurrentName), - MainNameAfterMock(_MainNameAfterMock), Optimize(_Optimize), + MainNameAfterMock(_MainNameAfterMock), + AnnotationsFile(_AnnotationsFile), Optimize(_Optimize), Simplify(_Simplify), CheckDivZero(_CheckDivZero), - CheckOvershift(_CheckOvershift), WithFPRuntime(_WithFPRuntime), - WithPOSIXRuntime(_WithPOSIXRuntime) {} + CheckOvershift(_CheckOvershift), + AnnotateOnlyExternal(_AnnotateOnlyExternal), + WithFPRuntime(_WithFPRuntime), WithPOSIXRuntime(_WithPOSIXRuntime) {} }; enum LogType { @@ -164,10 +170,7 @@ class Interpreter { std::set &&mainModuleGlobals, FLCtoOpcode &&origInstructions, const std::set &ignoredExternals, - const Annotations &annotations) = 0; - - virtual std::map - getAllExternals(const std::set &ignoredExternals) = 0; + std::vector> redefinitions) = 0; // supply a tree stream writer which the interpreter will use // to record the concrete path (as a stream of '0' and '1' bytes). diff --git a/include/klee/Core/MockBuilder.h b/include/klee/Core/MockBuilder.h index 0ff22bd890..7c788b705a 100644 --- a/include/klee/Core/MockBuilder.h +++ b/include/klee/Core/MockBuilder.h @@ -1,6 +1,7 @@ #ifndef KLEE_MOCKBUILDER_H #define KLEE_MOCKBUILDER_H +#include "klee/Core/Interpreter.h" #include "klee/Module/Annotation.h" #include "llvm/IR/IRBuilder.h" @@ -16,30 +17,52 @@ class MockBuilder { const llvm::Module *userModule; std::unique_ptr mockModule; std::unique_ptr> builder; - std::map externals; - Annotations annotations; - const std::string mockEntrypoint, userEntrypoint; + const Interpreter::ModuleOptions &opts; + + std::set ignoredExternals; + std::vector> redefinitions; + + InterpreterHandler *interpreterHandler; + + AnnotationsMap annotations; 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); - void buildAnnotationForExternalFunctionParams(llvm::Function *func, - Annotation &annotation); - llvm::Value *goByOffset(llvm::Value *value, - const std::vector &offset); + void + buildCallKleeMakeSymbolic(const std::string &kleeMakeSymbolicFunctionName, + llvm::Value *source, llvm::Type *type, + const std::string &symbolicName); + + void buildAnnotationForExternalFunctionArgs( + llvm::Function *func, + const std::vector> &statementsNotAllign); + void buildAnnotationForExternalFunctionReturn( + llvm::Function *func, const std::vector &statements); + void buildAnnotationForExternalFunctionProperties( + llvm::Function *func, const std::set &properties); + + std::map getExternalFunctions(); + std::map getExternalGlobals(); + + std::pair + goByOffset(llvm::Value *value, const std::vector &offset); public: - MockBuilder(const llvm::Module *initModule, std::string mockEntrypoint, - std::string userEntrypoint, - std::map externals, - Annotations annotations); + MockBuilder(const llvm::Module *initModule, + const Interpreter::ModuleOptions &opts, + const std::set &ignoredExternals, + std::vector> &redefinitions, + InterpreterHandler *interpreterHandler); std::unique_ptr build(); + void buildAllocSource(llvm::Value *prev, llvm::Type *elemType, + const Statement::AllocSource *allocSourcePtr); + void processingValue(llvm::Value *prev, llvm::Type *elemType, + const Statement::AllocSource *allocSourcePtr, + const Statement::InitNull *initNullPtr); }; } // namespace klee diff --git a/include/klee/Module/Annotation.h b/include/klee/Module/Annotation.h index 6defdd15b3..448c74f913 100644 --- a/include/klee/Module/Annotation.h +++ b/include/klee/Module/Annotation.h @@ -9,78 +9,98 @@ #include "nlohmann/json.hpp" #include "nonstd/optional.hpp" +#include "klee/Config/config.h" + +#include "llvm/IR/Module.h" + using nonstd::nullopt; using nonstd::optional; using json = nlohmann::json; namespace klee { -// Annotation format: https://github.com/UnitTestBot/klee/discussions/92 -struct Annotation { - enum class StatementKind { - Unknown, +namespace Statement { +enum class Kind { + Unknown, - Deref, - InitNull, - }; + Deref, + InitNull, + AllocSource, +}; - enum class Property { - Unknown, +enum class Property { + Unknown, - Determ, - Noreturn, - }; + Deterministic, + Noreturn, +}; - struct StatementUnknown { - explicit StatementUnknown(const std::string &str); - virtual ~StatementUnknown(); +struct Unknown { +protected: + std::string rawAnnotation; + std::string rawOffset; + std::string rawValue; - virtual Annotation::StatementKind getStatementName() const; - virtual bool operator==(const StatementUnknown &other) const; +public: + std::vector offset; - std::string statementStr; - std::vector offset; + explicit Unknown(const std::string &str = "Unknown"); + virtual ~Unknown(); - protected: - void parseOffset(const std::string &offsetStr); - void parseOnlyOffset(const std::string &str); - }; + virtual bool operator==(const Unknown &other) const; + [[nodiscard]] virtual Kind getKind() const; - struct StatementDeref final : public StatementUnknown { - explicit StatementDeref(const std::string &str); + [[nodiscard]] const std::vector &getOffset() const; + [[nodiscard]] std::string toString() const; +}; - Annotation::StatementKind getStatementName() const override; - }; +struct Deref final : public Unknown { + explicit Deref(const std::string &str = "Deref"); - struct StatementInitNull final : public StatementUnknown { - explicit StatementInitNull(const std::string &str); + [[nodiscard]] Kind getKind() const override; +}; - Annotation::StatementKind getStatementName() const override; +struct InitNull final : public Unknown { + explicit InitNull(const std::string &str = "InitNull"); + + [[nodiscard]] Kind getKind() const override; +}; + +struct AllocSource final : public Unknown { +public: + enum Type { + Alloc = 1, // malloc, calloc, realloc + New = 2, // operator new + NewBrackets = 3, // operator new[] + OpenFile = 4, // open file (fopen, open) + MutexLock = 5 // mutex lock (pthread_mutex_lock) }; - using StatementPtr = std::shared_ptr; - using StatementPtrs = std::vector; + Type value; - bool operator==(const Annotation &other) const; + explicit AllocSource(const std::string &str = "AllocSource::1"); - std::string functionName; - std::vector statements; - std::set properties; + [[nodiscard]] Kind getKind() const override; }; -using Annotations = std::map; +using Ptr = std::shared_ptr; +bool operator==(const Ptr &first, const Ptr &second); +} // namespace Statement -const std::map toProperties{ - {"determ", Annotation::Property::Determ}, - {"noreturn", Annotation::Property::Noreturn}, -}; +// Annotation format: https://github.com/UnitTestBot/klee/discussions/92 +struct Annotation { + std::string functionName; + std::vector returnStatements; + std::vector> argsStatements; + std::set properties; -Annotations parseAnnotationsFile(const json &annotationsJson); -Annotations parseAnnotationsFile(const std::string &path); + bool operator==(const Annotation &other) const; +}; -bool operator==(const Annotation::StatementPtr &first, - const Annotation::StatementPtr &second); +using AnnotationsMap = std::map; +AnnotationsMap parseAnnotationsJson(const json &annotationsJson); +AnnotationsMap parseAnnotations(const std::string &path, const llvm::Module *m); } // namespace klee #endif // KLEE_ANNOTATION_H diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index bf60649ddc..13fe280a7d 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -22,10 +22,10 @@ #include "klee/Support/CompilerWarning.h" DISABLE_WARNING_PUSH DISABLE_WARNING_DEPRECATED_DECLARATIONS +#include "klee/Support/ErrorHandling.h" #include "llvm/IR/Function.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" -#include "klee/Support/ErrorHandling.h" DISABLE_WARNING_POP #include diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 50ab891b7e..d349f5334a 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -469,9 +469,9 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, InterpreterHandler *ih) : Interpreter(opts), interpreterHandler(ih), searcher(nullptr), externalDispatcher(new ExternalDispatcher(ctx)), statsTracker(0), - pathWriter(0), symPathWriter(0), specialFunctionHandler(0), - timers{time::Span(TimerInterval)}, guidanceKind(opts.Guidance), - codeGraphInfo(new CodeGraphInfo()), + pathWriter(0), symPathWriter(0), + specialFunctionHandler(0), timers{time::Span(TimerInterval)}, + guidanceKind(opts.Guidance), codeGraphInfo(new CodeGraphInfo()), distanceCalculator(new DistanceCalculator(*codeGraphInfo)), targetCalculator(new TargetCalculator(*codeGraphInfo)), targetManager(new TargetManager(guidanceKind, *distanceCalculator, @@ -547,7 +547,7 @@ llvm::Module *Executor::setModule( const ModuleOptions &opts, std::set &&mainModuleFunctions, std::set &&mainModuleGlobals, FLCtoOpcode &&origInstructions, const std::set &ignoredExternals, - const Annotations &annotations) { + std::vector> redefinitions) { assert(!kmodule && !userModules.empty() && "can only register one module"); // XXX gross @@ -586,28 +586,15 @@ llvm::Module *Executor::setModule( kmodule->instrument(opts); } - if (ExternalCalls == ExternalCallPolicy::All && - interpreterOpts.MockStrategy != MockStrategy::None) { - // TODO: move this to function - std::map externals = - getAllExternals(ignoredExternals); - MockBuilder builder(kmodule->module.get(), opts.MainCurrentName, - opts.MainNameAfterMock, externals, annotations); - 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); + if (interpreterOpts.MockStrategy != MockStrategy::None || + !opts.AnnotationsFile.empty()) { + MockBuilder mockBuilder(kmodule->module.get(), opts, ignoredExternals, + redefinitions, interpreterHandler); + std::unique_ptr mockModule = mockBuilder.build(); std::vector> mockModules; mockModules.push_back(std::move(mockModule)); - kmodule->link(mockModules, 0); + kmodule->link(mockModules, 1); for (auto &global : kmodule->module->globals()) { if (global.isDeclaration()) { @@ -673,37 +660,6 @@ llvm::Module *Executor::setModule( 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; @@ -5145,7 +5101,7 @@ ObjectState *Executor::bindObjectInState(ExecutionState &state, // will put multiple copies on this list, but it doesn't really // matter because all we use this list for is to unbind the object // on function return. - if (isLocal && state.stack.size() > 0) { + if (isLocal && !state.stack.empty()) { state.stack.valueStack().back().allocas.push_back(mo->id); } return os; @@ -6612,48 +6568,6 @@ 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(kmodule.get(), *kf->function, - 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(kmodule.get(), *kf->function, args); - break; - } - executeMakeSymbolic(state, mo, type, source, false); - const ObjectState *os = state.addressSpace.findObject(mo->id).second; - auto result = os->read(0, width); - bindLocal(target, state, result); -} - /***/ ExecutionState *Executor::formState(Function *f) { diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 0372aeb5bd..338efa3c12 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -422,9 +422,6 @@ 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); @@ -699,6 +696,9 @@ class Executor : public Interpreter { const KBlock *getKBlock(const llvm::BasicBlock *bb) const; const KFunction *getKFunction(const llvm::Function *f) const; + std::map + getAllExternals(const std::set &ignoredExternals) const; + public: Executor(llvm::LLVMContext &ctx, const InterpreterOptions &opts, InterpreterHandler *ie); @@ -726,18 +726,15 @@ class Executor : public Interpreter { replayPosition = 0; } - llvm::Module * - setModule(std::vector> &userModules, - std::vector> &libsModules, - const ModuleOptions &opts, + llvm::Module *setModule( + std::vector> &userModules, + std::vector> &libsModules, + const ModuleOptions &opts, std::set &&mainModuleFunctions, std::set &&mainModuleGlobals, FLCtoOpcode &&origInstructions, - const std::set &ignoredExternals, - const Annotations &annotations) override; - - std::map - getAllExternals(const std::set &ignoredExternals) override; + const std::set &ignoredExternals, + std::vector> redefinitions) override; void useSeeds(const std::vector *seeds) override { usingSeeds = seeds; diff --git a/lib/Core/MockBuilder.cpp b/lib/Core/MockBuilder.cpp index 0545c34115..421231f482 100644 --- a/lib/Core/MockBuilder.cpp +++ b/lib/Core/MockBuilder.cpp @@ -1,28 +1,97 @@ #include "klee/Core/MockBuilder.h" +#include "klee/Config/Version.h" #include "klee/Module/Annotation.h" #include "klee/Support/ErrorHandling.h" + #include "llvm/IR/IRBuilder.h" #include "llvm/IR/Module.h" +#include "llvm/Support/raw_ostream.h" #include #include namespace klee { -MockBuilder::MockBuilder(const llvm::Module *initModule, - std::string mockEntrypoint, std::string userEntrypoint, - std::map externals, - Annotations annotations) - : userModule(initModule), externals(std::move(externals)), - annotations(std::move(annotations)), - mockEntrypoint(std::move(mockEntrypoint)), - userEntrypoint(std::move(userEntrypoint)) {} +template +void inline removeAliases(const llvm::Module *userModule, + std::map &externals) { + for (const auto &alias : userModule->aliases()) { + auto it = externals.find(alias.getName().str()); + if (it != externals.end()) { + externals.erase(it); + } + } +} + +std::map +MockBuilder::getExternalFunctions() { + std::map externals; + for (const auto &f : userModule->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())); + } + } + removeAliases(userModule, externals); + + return externals; +} + +std::map MockBuilder::getExternalGlobals() { + std::map externals; + for (const auto &global : userModule->globals()) { + if (global.isDeclaration() && + !ignoredExternals.count(global.getName().str())) { + externals.insert(std::make_pair(global.getName(), global.getValueType())); + } + } + removeAliases(userModule, externals); + + for (const auto &e : externals) { + klee_message("Mocking external variable %s", e.first.c_str()); + } + + return externals; +} + +MockBuilder::MockBuilder( + const llvm::Module *initModule, const Interpreter::ModuleOptions &opts, + const std::set &ignoredExternals, + std::vector> &redefinitions, + InterpreterHandler *interpreterHandler) + : userModule(initModule), opts(opts), ignoredExternals(ignoredExternals), + redefinitions(redefinitions), interpreterHandler(interpreterHandler) { + annotations = parseAnnotations(opts.AnnotationsFile, userModule); +} std::unique_ptr MockBuilder::build() { initMockModule(); buildMockMain(); buildExternalFunctionsDefinitions(); + + if (!mockModule) { + klee_error("Unable to generate mocks"); + } + + { + std::unique_ptr of( + interpreterHandler->openOutputFile("redefinitions.txt")); + for (const auto &i : redefinitions) { + *of << i.first << " " << i.second << "\n"; + } + } + + { + auto mainFn = mockModule->getFunction(opts.MainCurrentName); + mainFn->setName(opts.EntryPoint); + std::unique_ptr of( + interpreterHandler->openOutputFile("externals.ll")); + *of << *mockModule; + mainFn->setName(opts.MainCurrentName); + } + return std::move(mockModule); } @@ -38,17 +107,18 @@ void MockBuilder::initMockModule() { // 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); + llvm::Function *userMainFn = userModule->getFunction(opts.MainNameAfterMock); if (!userMainFn) { - klee_error("Entry function '%s' not found in module.", - userEntrypoint.c_str()); + klee_error("Mock: Entry function '%s' not found in module", + opts.MainNameAfterMock.c_str()); } - mockModule->getOrInsertFunction(mockEntrypoint, userMainFn->getFunctionType(), + mockModule->getOrInsertFunction(opts.MainCurrentName, + userMainFn->getFunctionType(), userMainFn->getAttributes()); - llvm::Function *mockMainFn = mockModule->getFunction(mockEntrypoint); + llvm::Function *mockMainFn = mockModule->getFunction(opts.MainCurrentName); if (!mockMainFn) { - klee_error("Entry function '%s' not found in module.", - mockEntrypoint.c_str()); + klee_error("Mock: Entry function '%s' not found in module", + opts.MainCurrentName.c_str()); } auto globalsInitBlock = llvm::BasicBlock::Create(mockModule->getContext(), "entry", mockMainFn); @@ -57,7 +127,7 @@ void MockBuilder::buildMockMain() { buildExternalGlobalsDefinitions(); auto userMainCallee = mockModule->getOrInsertFunction( - userEntrypoint, userMainFn->getFunctionType()); + opts.MainNameAfterMock, userMainFn->getFunctionType()); std::vector args; args.reserve(userMainFn->arg_size()); for (auto it = mockMainFn->arg_begin(); it != mockMainFn->arg_end(); it++) { @@ -68,16 +138,12 @@ void MockBuilder::buildMockMain() { } void MockBuilder::buildExternalGlobalsDefinitions() { - for (const auto &it : externals) { - if (it.second->isFunctionTy()) { - continue; - } - const std::string &extName = it.first; - llvm::Type *type = it.second; + auto externalGlobals = getExternalGlobals(); + for (const auto &[extName, type] : externalGlobals) { mockModule->getOrInsertGlobal(extName, type); auto *global = mockModule->getGlobalVariable(extName); if (!global) { - klee_error("Unable to add global variable '%s' to module", + klee_error("Mock: Unable to add global variable '%s' to module", extName.c_str()); } global->setLinkage(llvm::GlobalValue::ExternalLinkage); @@ -85,27 +151,38 @@ void MockBuilder::buildExternalGlobalsDefinitions() { continue; } - auto *zeroInitializer = llvm::Constant::getNullValue(it.second); + auto *zeroInitializer = llvm::Constant::getNullValue(type); if (!zeroInitializer) { - klee_error("Unable to get zero initializer for '%s'", extName.c_str()); + klee_error("Mock: Unable to get zero initializer for '%s'", + extName.c_str()); } global->setInitializer(zeroInitializer); - buildCallKleeMakeSymbol("klee_make_symbolic", global, type, - "@obj_" + extName); + buildCallKleeMakeSymbolic("klee_make_symbolic", global, type, + "external_" + extName); } } void MockBuilder::buildExternalFunctionsDefinitions() { - for (const auto &it : externals) { - if (!it.second->isFunctionTy()) { - continue; + auto externalFunctions = getExternalFunctions(); + + if (!opts.AnnotateOnlyExternal) { + for (const auto &annotation : annotations) { + llvm::Function *func = userModule->getFunction(annotation.first); + if (func) { + auto ext = externalFunctions.find(annotation.first); + if (ext == externalFunctions.end()) { + externalFunctions[annotation.first] = func->getFunctionType(); + } + } } - std::string extName = it.first; - auto *type = llvm::cast(it.second); + } + + for (const auto &[extName, type] : externalFunctions) { mockModule->getOrInsertFunction(extName, type); llvm::Function *func = mockModule->getFunction(extName); if (!func) { - klee_error("Unable to find function '%s' in module", extName.c_str()); + klee_error("Mock: Unable to find function '%s' in module", + extName.c_str()); } if (!func->empty()) { continue; @@ -114,43 +191,52 @@ void MockBuilder::buildExternalFunctionsDefinitions() { llvm::BasicBlock::Create(mockModule->getContext(), "entry", func); builder->SetInsertPoint(BB); - if (!func->getReturnType()->isSized()) { - builder->CreateRet(nullptr); - continue; - } + const auto nameToAnnotations = annotations.find(extName); + if (nameToAnnotations != annotations.end()) { + klee_message("Annotation function %s", extName.c_str()); + const auto &annotation = nameToAnnotations->second; - const auto annotation = annotations.find(extName); - if (annotation != annotations.end()) { - buildAnnotationForExternalFunctionParams(func, annotation->second); - } + // if (llvm::Function *f = userModule->getFunction(extName)) { + // std::string replacedName = extName + "_replaced_by_mock"; + // klee_message("Renamed symbol %s to %s", + // f->getName().str().c_str(), + // replacedName.c_str()); + // redefinitions.emplace_back(f->getName(), extName); + // f->setName(replacedName); + // } - 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); + buildAnnotationForExternalFunctionArgs(func, annotation.argsStatements); + buildAnnotationForExternalFunctionReturn(func, + annotation.returnStatements); + buildAnnotationForExternalFunctionProperties(func, annotation.properties); + } else { + klee_message("Mocking external function %s", extName.c_str()); + // Default annotation for externals return + buildAnnotationForExternalFunctionReturn( + func, {std::make_shared()}); + } } } -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( +void MockBuilder::buildCallKleeMakeSymbolic( + const std::string &kleeMakeSymbolicFunctionName, llvm::Value *source, + llvm::Type *type, const std::string &symbolicName) { + auto *kleeMakeSymbolicName = 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( + auto kleeMakeSymbolicCallee = mockModule->getOrInsertFunction( + kleeMakeSymbolicFunctionName, kleeMakeSymbolicName); + 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); + auto globalSymbolicName = builder->CreateGlobalString("@" + symbolicName); + auto gep = builder->CreateConstInBoundsGEP2_64( + globalSymbolicName->getValueType(), globalSymbolicName, 0, 0); builder->CreateCall( - kleeMakeSymbolCallee, - {bitcastInst, + kleeMakeSymbolicCallee, + {bitCastInst, llvm::ConstantInt::get( mockModule->getContext(), llvm::APInt(64, mockModule->getDataLayout().getTypeStoreSize(type), @@ -158,67 +244,351 @@ void MockBuilder::buildCallKleeMakeSymbol(const std::string &klee_function_name, gep}); } -// TODO: add method for return value of external functions. -void MockBuilder::buildAnnotationForExternalFunctionParams( - llvm::Function *func, Annotation &annotation) { - for (size_t i = 1; i < annotation.statements.size(); i++) { - const auto arg = func->getArg(i - 1); - for (const auto &statement : annotation.statements[i]) { - llvm::Value *elem = goByOffset(arg, statement->offset); - switch (statement->getStatementName()) { - case Annotation::StatementKind::Deref: { - if (!elem->getType()->isPointerTy()) { - klee_error("Incorrect annotation offset."); - } - builder->CreateLoad(elem); - break; - } - case Annotation::StatementKind::InitNull: { - // TODO - } - case Annotation::StatementKind::Unknown: - default: - __builtin_unreachable(); - } - } - } - - for (const auto &property : annotation.properties) { - switch (property) { - case Annotation::Property::Determ: { - // TODO - } - case Annotation::Property::Noreturn: { - // TODO - } - case Annotation::Property::Unknown: - default: - __builtin_unreachable(); - } - } -} - -llvm::Value *MockBuilder::goByOffset(llvm::Value *value, - const std::vector &offset) { +std::pair +MockBuilder::goByOffset(llvm::Value *value, + const std::vector &offset) { + llvm::Value *prev = nullptr; llvm::Value *current = value; for (const auto &inst : offset) { if (inst == "*") { if (!current->getType()->isPointerTy()) { klee_error("Incorrect annotation offset."); } - current = builder->CreateLoad(current); + prev = current; + current = builder->CreateLoad(current->getType()->getPointerElementType(), + current); } else if (inst == "&") { auto addr = builder->CreateAlloca(current->getType()); + prev = current; current = builder->CreateStore(current, addr); } else { const size_t index = std::stol(inst); - if (!(current->getType()->isPointerTy() || current->getType()->isArrayTy())) { + if (!(current->getType()->isPointerTy() || + current->getType()->isArrayTy())) { klee_error("Incorrect annotation offset."); } - current = builder->CreateConstInBoundsGEP1_64(current, index); + prev = current; + current = builder->CreateConstInBoundsGEP1_64(current->getType(), current, + index); + } + } + return {prev, current}; +} + +inline llvm::Type *getTypeByOffset(llvm::Type *value, + const std::vector &offset) { + llvm::Type *current = value; + for (const auto &inst : offset) { + if (inst == "*") { + if (!current->isPointerTy()) { + return nullptr; + } + current = current->getPointerElementType(); + } else if (inst == "&") { + // no needed + } else { + const size_t index = std::stol(inst); + if (current->isArrayTy() || current->isPointerTy()) { + current = current->getContainedType(index); + } else { + return nullptr; + } } } return current; } +inline bool isCorrectStatements(const std::vector &statements, + const llvm::Argument *arg) { + return std::any_of(statements.begin(), statements.end(), + [arg](const Statement::Ptr &statement) { + auto argType = + getTypeByOffset(arg->getType(), statement->offset); + switch (statement->getKind()) { + case Statement::Kind::Deref: + case Statement::Kind::InitNull: + return argType->isPointerTy(); + case Statement::Kind::AllocSource: + assert(false); + case Statement::Kind::Unknown: + default: + return true; + } + }); +} + +bool tryAlign(llvm::Function *func, + const std::vector> &statements, + std::vector> &res) { + if (func->arg_size() == statements.size()) { + res = statements; + return true; + } + + for (size_t i = 0, j = 0; j < func->arg_size() && i < statements.size();) { + while (true) { +#if LLVM_VERSION_CODE >= LLVM_VERSION(10, 0) + auto arg = func->getArg(j); +#else + auto arg = &func->arg_begin()[j]; +#endif + if (isCorrectStatements(statements[i], arg)) { + break; + } + res.emplace_back(); + j++; + if (j >= func->arg_size()) { + break; + } + } + res.push_back(statements[i]); + j++; + i++; + } + if (func->arg_size() == statements.size()) { + return true; + } + return false; +} + +std::map, std::vector> +unifyByOffset(const std::vector &statements) { + std::map, std::vector> res; + for (const auto &i : statements) { + res[i->offset].push_back(i); + } + return res; +} + +void MockBuilder::buildAnnotationForExternalFunctionArgs( + llvm::Function *func, + const std::vector> &statementsNotAlign) { + std::vector> statements; + bool flag = tryAlign(func, statementsNotAlign, statements); + if (!flag) { + klee_warning("Annotation: can't align function arguments %s", + func->getName().str().c_str()); + return; + } + for (size_t i = 0; i < statements.size(); i++) { +#if LLVM_VERSION_CODE >= LLVM_VERSION(10, 0) + const auto arg = func->getArg(i); +#else + const auto arg = &func->arg_begin()[i]; +#endif + auto statementsMap = unifyByOffset(statements[i]); + for (const auto &[offset, statementsOffset] : statementsMap) { + auto [prev, elem] = goByOffset(arg, offset); + + Statement::AllocSource *allocSourcePtr = nullptr; + Statement::InitNull *initNullPtr = nullptr; + + for (const auto &statement : statementsOffset) { + switch (statement->getKind()) { + case Statement::Kind::Deref: { + if (!elem->getType()->isPointerTy()) { + klee_error("Annotation: Deref arg not pointer"); + } + + std::string derefCondName = "condition_deref_arg_" + + std::to_string(i) + "_deref_" + + func->getName().str(); + + auto intType = llvm::IntegerType::get(mockModule->getContext(), 1); + auto *derefCond = builder->CreateAlloca(intType, nullptr); + buildCallKleeMakeSymbolic("klee_make_mock", derefCond, intType, + derefCondName); + + llvm::BasicBlock *fromIf = builder->GetInsertBlock(); + llvm::Function *curFunc = fromIf->getParent(); + + llvm::BasicBlock *derefBB = llvm::BasicBlock::Create( + mockModule->getContext(), derefCondName, curFunc); + llvm::BasicBlock *contBB = llvm::BasicBlock::Create( + mockModule->getContext(), "continue_" + derefCondName); + auto brValue = builder->CreateLoad(intType, derefCond); + builder->CreateCondBr(brValue, derefBB, contBB); + + builder->SetInsertPoint(derefBB); + builder->CreateLoad(elem->getType()->getPointerElementType(), elem); + builder->CreateBr(contBB); + + curFunc->getBasicBlockList().push_back(contBB); + builder->SetInsertPoint(contBB); + break; + } + case Statement::Kind::AllocSource: { + if (prev != nullptr) { + allocSourcePtr = (Statement::AllocSource *)statement.get(); + } else { + klee_message("Annotation: not valid annotation %s", + statement->toString().c_str()); + } + break; + } + case Statement::Kind::InitNull: { + if (prev != nullptr) { + initNullPtr = (Statement::InitNull *)statement.get(); + } else { + klee_message("Annotation: not valid annotation %s", + statement->toString().c_str()); + } + break; + } + case Statement::Kind::Unknown: + default: + klee_message("Annotation not implemented %s", + statement->toString().c_str()); + break; + } + } + + processingValue(prev, elem->getType(), allocSourcePtr, initNullPtr); + } + } +} + +void MockBuilder::processingValue(llvm::Value *prev, llvm::Type *elemType, + const Statement::AllocSource *allocSourcePtr, + const Statement::InitNull *initNullPtr) { + if (initNullPtr) { + auto intType = llvm::IntegerType::get(mockModule->getContext(), 1); + auto *allocCond = builder->CreateAlloca(intType, nullptr); + buildCallKleeMakeSymbolic("klee_make_mock", allocCond, intType, + "initPtrCond"); + + llvm::BasicBlock *fromIf = builder->GetInsertBlock(); + llvm::Function *curFunc = fromIf->getParent(); + + llvm::BasicBlock *initNullBB = + llvm::BasicBlock::Create(mockModule->getContext(), "initNullBR"); + llvm::BasicBlock *contBB = + llvm::BasicBlock::Create(mockModule->getContext(), "continueBR"); + auto brValue = builder->CreateLoad(intType, allocCond); + if (allocSourcePtr) { + llvm::BasicBlock *allocBB = llvm::BasicBlock::Create( + mockModule->getContext(), "allocArg", curFunc); + builder->CreateCondBr(brValue, allocBB, initNullBB); + builder->SetInsertPoint(allocBB); + buildAllocSource(prev, elemType, allocSourcePtr); + builder->CreateBr(contBB); + } else { + builder->CreateCondBr(brValue, initNullBB, contBB); + } + curFunc->getBasicBlockList().push_back(initNullBB); + builder->SetInsertPoint(initNullBB); + builder->CreateStore( + llvm::ConstantPointerNull::get(llvm::cast(elemType)), + prev); + builder->CreateBr(contBB); + + curFunc->getBasicBlockList().push_back(contBB); + builder->SetInsertPoint(contBB); + } else if (allocSourcePtr) { + buildAllocSource(prev, elemType, allocSourcePtr); + } +} + +void MockBuilder::buildAllocSource( + llvm::Value *prev, llvm::Type *elemType, + const Statement::AllocSource *allocSourcePtr) { + if (allocSourcePtr->value != Statement::AllocSource::Alloc) { + klee_warning("Annotation: AllocSource \"%d\" not implemented use alloc", + allocSourcePtr->value); + } + auto valueType = elemType->getPointerElementType(); + auto sizeValue = llvm::ConstantInt::get( + mockModule->getContext(), + llvm::APInt(64, mockModule->getDataLayout().getTypeStoreSize(valueType), + false)); + auto int8PtrTy = llvm::IntegerType::getInt64Ty(mockModule->getContext()); + auto mallocInstr = + llvm::CallInst::CreateMalloc(builder->GetInsertBlock(), int8PtrTy, + valueType, sizeValue, nullptr, nullptr); + auto mallocValue = builder->Insert(mallocInstr, llvm::Twine("MallocValue")); + builder->CreateStore(mallocValue, prev); +} + +void MockBuilder::buildAnnotationForExternalFunctionReturn( + llvm::Function *func, const std::vector &statements) { + auto returnType = func->getReturnType(); + if (!returnType->isSized()) { // void return type + builder->CreateRet(nullptr); + return; + } + + Statement::AllocSource *allocSourcePtr = nullptr; + Statement::InitNull *initNullPtr = nullptr; + + for (const auto &statement : statements) { + switch (statement->getKind()) { + case Statement::Kind::Deref: + klee_warning("Annotation: unused Deref for return function \"%s\"", + func->getName().str().c_str()); + break; + case Statement::Kind::AllocSource: { + allocSourcePtr = returnType->isPointerTy() + ? (Statement::AllocSource *)statement.get() + : nullptr; + break; + } + case Statement::Kind::InitNull: { + initNullPtr = returnType->isPointerTy() + ? (Statement::InitNull *)statement.get() + : nullptr; + break; + } + case Statement::Kind::Unknown: + default: + klee_message("Annotation not implemented %s", + statement->toString().c_str()); + break; + } + } + std::string retName = "ret_" + func->getName().str(); + llvm::Value *retValuePtr = builder->CreateAlloca(returnType, nullptr); + + if (!returnType->isPointerTy() || !allocSourcePtr) { + buildCallKleeMakeSymbolic("klee_make_mock", retValuePtr, returnType, + func->getName().str()); + if (returnType->isPointerTy() && !initNullPtr) { + llvm::Value *retValue = + builder->CreateLoad(returnType, retValuePtr, retName); + auto cmpResult = + builder->CreateICmpNE(retValue, + llvm::ConstantPointerNull::get( + llvm::cast(returnType)), + "condition_init_null" + retName); + + auto *kleeAssumeType = llvm::FunctionType::get( + llvm::Type::getVoidTy(mockModule->getContext()), + {llvm::Type::getInt64Ty(mockModule->getContext())}, false); + + auto kleeAssumeFunc = + mockModule->getOrInsertFunction("klee_assume", kleeAssumeType); + auto cmpResult64 = builder->CreateZExt( + cmpResult, llvm::Type::getInt64Ty(mockModule->getContext())); + builder->CreateCall(kleeAssumeFunc, {cmpResult64}); + } + } else { + processingValue(retValuePtr, returnType, allocSourcePtr, initNullPtr); + } + llvm::Value *retValue = builder->CreateLoad(returnType, retValuePtr, retName); + builder->CreateRet(retValue); +} + +void MockBuilder::buildAnnotationForExternalFunctionProperties( + llvm::Function *func, const std::set &properties) { + for (const auto &property : properties) { + switch (property) { + case Statement::Property::Deterministic: + case Statement::Property::Noreturn: + case Statement::Property::Unknown: + default: + klee_message("Property not implemented"); + break; + } + } +} + } // namespace klee diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 3f19786383..35cb912a90 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -957,7 +957,66 @@ void SpecialFunctionHandler::handleMakeMock(ExecutionState &state, state, "Empty name of function in klee_make_mock"); return; } - executor.executeMakeMock(state, target, arguments); + + KFunction *kf = target->parent->parent; + + Executor::ExactResolutionList rl; + executor.resolveExact(state, arguments[0], + executor.typeSystemManager->getUnknownType(), rl, + "make_symbolic"); + + for (Executor::ExactResolutionList::iterator it = rl.begin(), ie = rl.end(); + it != ie; ++it) { + ObjectPair op = it->second->addressSpace.findObject(it->first); + const MemoryObject *mo = op.first; + mo->setName(name); + mo->updateTimestamp(); + + const ObjectState *old = op.second; + ExecutionState *s = it->second; + + if (old->readOnly) { + executor.terminateStateOnUserError( + *s, "cannot make readonly object symbolic"); + return; + } + + bool res; + bool success __attribute__((unused)) = executor.solver->mustBeTrue( + s->constraints.cs(), + EqExpr::create( + ZExtExpr::create(arguments[1], Context::get().getPointerWidth()), + mo->getSizeExpr()), + res, s->queryMetaData); + assert(success && "FIXME: Unhandled solver failure"); + + if (res) { + ref source; + switch (executor.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(executor.kmodule.get(), *kf->function, + executor.updateNameVersion(state, name)); + break; + case MockStrategy::Deterministic: + std::vector> args(kf->numArgs); + for (size_t i = 0; i < kf->numArgs; i++) { + args[i] = executor.getArgumentCell(state, kf, i).value; + } + source = SourceBuilder::mockDeterministic(executor.kmodule.get(), + *kf->function, args); + break; + } + executor.executeMakeSymbolic(state, mo, old->getDynamicType(), source, + false); + } else { + executor.terminateStateOnUserError(*s, + "Wrong size given to klee_make_mock"); + } + } } void SpecialFunctionHandler::handleMarkGlobal( diff --git a/lib/Module/Annotation.cpp b/lib/Module/Annotation.cpp index 5c40769054..8063e0284f 100644 --- a/lib/Module/Annotation.cpp +++ b/lib/Module/Annotation.cpp @@ -3,121 +3,198 @@ #include "klee/Support/ErrorHandling.h" #include +#include +#include -namespace { - -using namespace klee; - -Annotation::StatementPtr toStatement(const std::string &name, - const std::string &str) { - if (name == "Deref") { - return std::make_shared(str); - } else if (name == "InitNull") { - return std::make_shared(str); - } else { - return std::make_shared(str); - } -} - -} // namespace +#ifdef ENABLE_XML_ANNOTATION +#include "pugixml.hpp" +#endif namespace klee { -Annotation::StatementUnknown::StatementUnknown(const std::string &str) - : statementStr(str) { - parseOnlyOffset(str); +static inline std::string toLower(const std::string &str) { + std::string strLower; + strLower.reserve(str.size()); + std::transform(str.begin(), str.end(), std::back_inserter(strLower), tolower); + return strLower; } -Annotation::StatementUnknown::~StatementUnknown() = default; +namespace Statement { -Annotation::StatementKind -Annotation::StatementUnknown::getStatementName() const { - return Annotation::StatementKind::Unknown; -} +Unknown::Unknown(const std::string &str) { + { + const size_t firstColonPos = str.find(':'); + const size_t startOffset = firstColonPos + 1; + const size_t secondColonPos = str.find(':', startOffset); + const size_t offsetLength = (secondColonPos == std::string::npos) + ? std::string::npos + : secondColonPos - startOffset; -bool Annotation::StatementUnknown::operator==( - const Annotation::StatementUnknown &other) const { - return (statementStr == other.statementStr) && (offset == other.offset); -} + rawAnnotation = str.substr(0, firstColonPos); + if (firstColonPos == std::string::npos) { + return; + } + rawOffset = str.substr(startOffset, offsetLength); + if (secondColonPos != std::string::npos) { + rawValue = str.substr(secondColonPos + 1, std::string::npos); + } + } -void Annotation::StatementUnknown::parseOffset(const std::string &offsetStr) { - size_t pos = 0; - while (pos < offsetStr.size()) { - if (offsetStr[pos] == '*') { + for (size_t pos = 0; pos < rawOffset.size(); pos++) { + switch (rawOffset[pos]) { + case '*': { offset.emplace_back("*"); - pos++; - } else if (offsetStr[pos] == '&') { + break; + } + case '&': { offset.emplace_back("&"); - pos++; - } else if (offsetStr[pos] == '[') { - size_t posEndExpr = offsetStr.find(']', pos); + break; + } + case '[': { + size_t posEndExpr = rawOffset.find(']', pos); if (posEndExpr == std::string::npos) { - klee_error("Incorrect annotation offset format."); + klee_error("Annotation: Incorrect offset format \"%s\"", str.c_str()); } - offset.push_back(offsetStr.substr(pos + 1, posEndExpr - 1 - pos)); - pos = posEndExpr + 1; + offset.push_back(rawOffset.substr(pos + 1, posEndExpr - 1 - pos)); + pos = posEndExpr; + break; + } + default: { + klee_warning("Annotation: Incorrect offset format \"%s\"", str.c_str()); + break; + } + } + } +} + +Unknown::~Unknown() = default; + +Kind Unknown::getKind() const { return Kind::Unknown; } + +const std::vector &Unknown::getOffset() const { return offset; } +std::string Unknown::toString() const { + if (rawValue.empty()) { + if (rawOffset.empty()) { + return rawAnnotation; } else { - klee_error("Incorrect annotation offset format."); + return rawAnnotation + ":" + rawOffset; } } + return rawAnnotation + ":" + rawOffset + ":" + rawValue; } -void Annotation::StatementUnknown::parseOnlyOffset(const std::string &str) { - const size_t delimiterAfterName = str.find(':'); - if (delimiterAfterName == std::string::npos) { - return; +bool Unknown::operator==(const Unknown &other) const { + if (this->getKind() == other.getKind()) { + return toString() == other.toString(); } - const size_t delimiterAfterOffset = str.find(':', delimiterAfterName + 1); - const size_t offsetLength = - (delimiterAfterOffset == std::string::npos) - ? std::string::npos - : delimiterAfterOffset - delimiterAfterName - 1; - parseOffset(str.substr(delimiterAfterName + 1, offsetLength)); + return false; } -Annotation::StatementDeref::StatementDeref(const std::string &str) - : StatementUnknown(str) {} +/* + * InitNull:*[5]: + * {kind}:{offset}:{data} + */ + +Deref::Deref(const std::string &str) : Unknown(str) {} + +Kind Deref::getKind() const { return Kind::Deref; } + +InitNull::InitNull(const std::string &str) : Unknown(str) {} -Annotation::StatementKind Annotation::StatementDeref::getStatementName() const { - return Annotation::StatementKind::Deref; +Kind InitNull::getKind() const { return Kind::InitNull; } + +AllocSource::AllocSource(const std::string &str) : Unknown(str) { + if (!std::all_of(rawValue.begin(), rawValue.end(), isdigit)) { + klee_error("Annotation: Incorrect value format \"%s\"", rawValue.c_str()); + } + if (rawValue.empty()) { + value = AllocSource::Type::Alloc; + } else { + value = static_cast(std::stoi(rawValue)); + } } -Annotation::StatementInitNull::StatementInitNull(const std::string &str) - : StatementUnknown(str) {} +Kind AllocSource::getKind() const { return Kind::AllocSource; } + +const std::map StringToKindMap = { + {"deref", Statement::Kind::Deref}, + {"initnull", Statement::Kind::InitNull}, + {"allocsource", Statement::Kind::AllocSource}}; -Annotation::StatementKind -Annotation::StatementInitNull::getStatementName() const { - return Annotation::StatementKind::InitNull; +inline Statement::Kind stringToKind(const std::string &str) { + auto it = StringToKindMap.find(toLower(str)); + if (it != StringToKindMap.end()) { + return it->second; + } + return Statement::Kind::Unknown; } -bool Annotation::operator==(const Annotation &other) const { - return (functionName == other.functionName) && - (statements == other.statements) && (properties == other.properties); +Ptr stringToKindPtr(const std::string &str) { + std::string statementStr = toLower(str.substr(0, str.find(':'))); + switch (stringToKind(statementStr)) { + case Statement::Kind::Unknown: + return std::make_shared(str); + case Statement::Kind::Deref: + return std::make_shared(str); + case Statement::Kind::InitNull: + return std::make_shared(str); + case Statement::Kind::AllocSource: + return std::make_shared(str); + } } -void from_json(const json &j, Annotation::StatementPtr &statement) { +const std::map StringToPropertyMap{ + {"deterministic", Property::Deterministic}, + {"noreturn", Property::Noreturn}, +}; + +inline Property stringToProperty(const std::string &str) { + auto it = StringToPropertyMap.find(toLower(str)); + if (it != StringToPropertyMap.end()) { + return it->second; + } + return Property::Unknown; +} + +void from_json(const json &j, Ptr &statement) { if (!j.is_string()) { - klee_error("Incorrect annotation format."); + klee_error("Annotation: Incorrect statement format"); } const std::string jStr = j.get(); - statement = toStatement(jStr.substr(0, jStr.find(':')), jStr); + statement = Statement::stringToKindPtr(jStr); } -void from_json(const json &j, Annotation::Property &property) { +void from_json(const json &j, Property &property) { if (!j.is_string()) { - klee_error("Incorrect properties format in annotations file."); + klee_error("Annotation: Incorrect properties format"); } const std::string jStr = j.get(); - property = Annotation::Property::Unknown; - const auto propertyPtr = toProperties.find(jStr); - if (propertyPtr != toProperties.end()) { + property = Statement::Property::Unknown; + const auto propertyPtr = Statement::StringToPropertyMap.find(jStr); + if (propertyPtr != Statement::StringToPropertyMap.end()) { property = propertyPtr->second; } } -Annotations parseAnnotationsFile(const json &annotationsJson) { - Annotations annotations; +bool operator==(const Statement::Ptr &first, const Statement::Ptr &second) { + if (first->getKind() != second->getKind()) { + return false; + } + + return *first.get() == *second.get(); +} +} // namespace Statement + +bool Annotation::operator==(const Annotation &other) const { + return (functionName == other.functionName) && + (returnStatements == other.returnStatements) && + (argsStatements == other.argsStatements) && + (properties == other.properties); +} + +AnnotationsMap parseAnnotationsJson(const json &annotationsJson) { + AnnotationsMap annotations; for (auto &item : annotationsJson.items()) { Annotation annotation; annotation.functionName = item.key(); @@ -125,50 +202,158 @@ Annotations parseAnnotationsFile(const json &annotationsJson) { const json &j = item.value(); if (!j.is_object() || !j.contains("annotation") || !j.contains("properties")) { - klee_error("Incorrect annotations file format."); + klee_error("Annotation: Incorrect file format"); + } + { + std::vector> tmp = + j.at("annotation").get>>(); + + if (tmp.empty()) { + klee_error("Annotation: function \"%s\" should has return", + annotation.functionName.c_str()); + } + annotation.returnStatements = tmp[0]; + annotation.argsStatements = + std::vector>(tmp.begin() + 1, tmp.end()); } - annotation.statements = - j.at("annotation").get>(); annotation.properties = - j.at("properties").get>(); + j.at("properties").get>(); annotations[item.key()] = annotation; } return annotations; } -Annotations parseAnnotationsFile(const std::string &path) { - std::ifstream annotationsFile(path); - if (!annotationsFile.good()) { - klee_error("Opening %s failed.", path.c_str()); +#ifdef ENABLE_XML_ANNOTATION + +namespace annotationXml { + +const std::map StringToKindMap = { + {"C_NULLDEREF", Statement::Kind::Deref}, + {"C_NULLRETURN", Statement::Kind::InitNull}}; + +inline Statement::Kind xmlTypeToKind(const std::string &str) { + auto it = StringToKindMap.find(str); + if (it != StringToKindMap.end()) { + return it->second; } + klee_message("Annotations: unknown xml type \"%s\"", str.c_str()); + return Statement::Kind::Unknown; +} - json annotationsJson = json::parse(annotationsFile, nullptr, false); - if (annotationsJson.is_discarded()) { - klee_error("Parsing JSON %s failed.", path.c_str()); +const std::map xmlPropertyMap = {}; + +inline Statement::Property xmlTypeToProperty(const std::string &str) { + auto it = xmlPropertyMap.find(str); + if (it != xmlPropertyMap.end()) { + return it->second; } + return Statement::Property::Unknown; +} - return parseAnnotationsFile(annotationsJson); +AnnotationsMap parseAnnotationsXml(const pugi::xml_document &annotationsXml, + const llvm::Module *m) { + AnnotationsMap result; + for (pugi::xml_node rules : annotationsXml.child("RuleSet")) { + for (pugi::xml_node customRule : rules) { + for (pugi::xml_node keyword : customRule.child("Keywords")) { + std::string name = keyword.attribute("name").value(); + std::string isRegex = keyword.attribute("isRegex").value(); + if (toLower(isRegex) == "true") { + klee_warning("Annotation: regexp currently not implemented"); + continue; + } + std::string value = keyword.attribute("value").value(); + std::string type = keyword.attribute("type").value(); + std::string pairedTo = keyword.attribute("pairedTo").value(); + + llvm::Function *func = m->getFunction(name); + if (!func) { + continue; + } + + auto it = result.find(name); + if (result.find(name) == result.end()) { + Annotation newAnnotation; + newAnnotation.functionName = name; + newAnnotation.argsStatements = + std::vector>(func->arg_size()); + + result[name] = std::move(newAnnotation); + it = result.find(name); + } + Annotation &curAnnotation = it->second; + Statement::Kind curKind = xmlTypeToKind(type); + + switch (curKind) { + case Statement::Kind::InitNull: { + curAnnotation.returnStatements.push_back( + std::make_shared()); + break; + } + case Statement::Kind::Deref: { + size_t i = 0; + for (const auto &arg : func->args()) { + if (arg.getType()->isPointerTy()) { + curAnnotation.argsStatements[i].push_back( + std::make_shared()); + ++i; + } + } + break; + } + case Statement::Kind::AllocSource: { + assert(false); + } + case Statement::Kind::Unknown: + break; + } + + Statement::Property curProperty = xmlTypeToProperty(type); + + switch (curProperty) { + case Statement::Property::Deterministic: + case Statement::Property::Noreturn: + case Statement::Property::Unknown: + break; + } + } + } + } + return result; } +} // namespace annotationXml +#endif -bool operator==(const Annotation::StatementPtr &first, - const Annotation::StatementPtr &second) { - if (first->getStatementName() != second->getStatementName()) { - return false; +AnnotationsMap parseAnnotations(const std::string &path, + const llvm::Module *m) { + if (path.empty()) { + return {}; } + std::ifstream annotationsFile(path); + if (!annotationsFile.good()) { + klee_error("Annotation: Opening %s failed.", path.c_str()); + } +#ifdef ENABLE_XML_ANNOTATION + if (toLower(std::filesystem::path(path).extension()) == ".xml") { + + pugi::xml_document doc; + pugi::xml_parse_result result = doc.load_file(path.c_str()); + if (!result) { + klee_error("Annotation: Parsing XML %s failed.", path.c_str()); + } + + return annotationXml::parseAnnotationsXml(doc, m); + } else { +#else + { +#endif + json annotationsJson = json::parse(annotationsFile, nullptr, false); + if (annotationsJson.is_discarded()) { + klee_error("Annotation: Parsing JSON %s failed.", path.c_str()); + } - switch (first->getStatementName()) { - case Annotation::StatementKind::Unknown: - return (*dynamic_cast(first.get()) == - *dynamic_cast(second.get())); - case Annotation::StatementKind::Deref: - return (*dynamic_cast(first.get()) == - *dynamic_cast(second.get())); - case Annotation::StatementKind::InitNull: - return (*dynamic_cast(first.get()) == - *dynamic_cast(second.get())); - default: - __builtin_unreachable(); + return parseAnnotationsJson(annotationsJson); } } diff --git a/lib/Module/CMakeLists.txt b/lib/Module/CMakeLists.txt index e4539d1dc3..d6abe7b4c6 100644 --- a/lib/Module/CMakeLists.txt +++ b/lib/Module/CMakeLists.txt @@ -31,6 +31,13 @@ set(KLEE_MODULE_COMPONENT_SRCS TargetForest.cpp ) +if (ENABLE_XML_ANNOTATION) + set(KLEE_MODULE_COMPONENT_SRCS + ${KLEE_MODULE_COMPONENT_SRCS} + ../../submodules/pugixml/src/pugixml.cpp + ) +endif() + add_library(kleeModule ${KLEE_MODULE_COMPONENT_SRCS} ) diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp index efaf94e559..261d8092c9 100644 --- a/lib/Solver/Z3Builder.cpp +++ b/lib/Solver/Z3Builder.cpp @@ -329,11 +329,6 @@ Z3ASTHandle Z3Builder::getArrayForUpdate(const Array *root, const UpdateNode *un) { // Iterate over the update nodes, until we find a cached version of the node, // or no more update nodes remain - if (root->source->isMock()) { - klee_error("Updates applied to mock array %s are not allowed", - root->getName().c_str()); - } - // FIXME: This really needs to be non-recursive. Z3ASTHandle un_expr; std::vector update_nodes; for (; un && !_arr_hash.lookupUpdateNodeExpr(un, un_expr); diff --git a/runtime/Mocks/models.c b/runtime/Mocks/models.c index ad95634b47..a389ad5a34 100644 --- a/runtime/Mocks/models.c +++ b/runtime/Mocks/models.c @@ -6,7 +6,7 @@ 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; + unsigned char retNull; klee_make_symbolic(&retNull, sizeof(retNull), "retNullMalloc"); if (retNull) { return 0; @@ -16,7 +16,7 @@ void *__klee_wrapped_malloc(size_t size) { } void *__klee_wrapped_calloc(size_t num, size_t size) { - char retNull; + unsigned char retNull; klee_make_symbolic(&retNull, sizeof(retNull), "retNullCalloc"); if (retNull) { return 0; @@ -26,7 +26,7 @@ void *__klee_wrapped_calloc(size_t num, size_t size) { } void *__klee_wrapped_realloc(void *ptr, size_t new_size) { - char retNull; + unsigned char retNull; klee_make_symbolic(&retNull, sizeof(retNull), "retNullRealloc"); if (retNull) { return 0; diff --git a/scripts/cooddy_annotations.py b/scripts/cooddy_annotations.py new file mode 100755 index 0000000000..11b05eca0d --- /dev/null +++ b/scripts/cooddy_annotations.py @@ -0,0 +1,41 @@ +#!/bin/python3 + +import json +import re +from argparse import ArgumentParser + + +Cooddy_name_pattern = re.compile(r"^(?P.*)\((?P[^()]*)\)$") + + +def getNames(name: str) : + m = Cooddy_name_pattern.fullmatch(name) + if m: + return m.group("name"), m.group("mangled_name") + return name, name + + +def transform(utbot_json, coody_json): + for coody_name, annotation in coody_json.items(): + funcName, mangledName = getNames(coody_name) + utbot_json[mangledName] = {"name": funcName, "annotation": annotation, "properties": []} + + +def main(): + parser = ArgumentParser( + prog='cooddy_annotations.py', + description='This script transforms .json annotations used by Cooddy static analyzer into annotations understandable by KLEE') + parser.add_argument('filenames', metavar='Path', nargs='+', help="Cooddy annotation .json file path") + parser.add_argument('Output', help="Target file path for produced KLEE annotation") + args = parser.parse_args() + utbot_json = dict() + for filename in args.filenames: + with open(filename) as file: + j = json.load(file) + transform(utbot_json, j) + with open(args.Output, 'w') as file: + json.dump(utbot_json, file, indent=" ") + + +if __name__ == "__main__": + main() diff --git a/json b/submodules/json similarity index 100% rename from json rename to submodules/json diff --git a/optional b/submodules/optional similarity index 100% rename from optional rename to submodules/optional diff --git a/submodules/pugiconfig.hpp b/submodules/pugiconfig.hpp new file mode 100644 index 0000000000..69e4d77899 --- /dev/null +++ b/submodules/pugiconfig.hpp @@ -0,0 +1,81 @@ +/** + * pugixml parser - version 1.13 + * -------------------------------------------------------- + * Copyright (C) 2006-2022, by Arseny Kapoulkine (arseny.kapoulkine@gmail.com) + * Report bugs and download new versions at https://pugixml.org/ + * + * This library is distributed under the MIT License. See notice at the end + * of this file. + * + * This work is based on the pugxml parser, which is: + * Copyright (C) 2003, by Kristen Wegner (kristen@tima.net) + */ + +#ifndef HEADER_PUGICONFIG_HPP +#define HEADER_PUGICONFIG_HPP + +// Uncomment this to enable wchar_t mode +// #define PUGIXML_WCHAR_MODE + +// Uncomment this to enable compact mode +// #define PUGIXML_COMPACT + +// Uncomment this to disable XPath +// #define PUGIXML_NO_XPATH + +// Uncomment this to disable STL +// #define PUGIXML_NO_STL + +// Uncomment this to disable exceptions +#define PUGIXML_NO_EXCEPTIONS + +// Set this to control attributes for public classes/functions, i.e.: +// to export all public symbols from DLL +// #define PUGIXML_API __declspec(dllexport) +// to import all classes from DLL +// #define PUGIXML_CLASS __declspec(dllimport) +// to set calling conventions to all public functions to fastcall +// #define PUGIXML_FUNCTION __fastcall +// In absence of PUGIXML_CLASS/PUGIXML_FUNCTION definitions PUGIXML_API +// is used instead + +// Tune these constants to adjust memory-related behavior +// #define PUGIXML_MEMORY_PAGE_SIZE 32768 +// #define PUGIXML_MEMORY_OUTPUT_STACK 10240 +// #define PUGIXML_MEMORY_XPATH_PAGE_SIZE 4096 + +// Tune this constant to adjust max nesting for XPath queries +// #define PUGIXML_XPATH_DEPTH_LIMIT 1024 + +// Uncomment this to switch to header-only version +// #define PUGIXML_HEADER_ONLY + +// Uncomment this to enable long long support +// #define PUGIXML_HAS_LONG_LONG + +#endif + +/** + * Copyright (c) 2006-2022 Arseny Kapoulkine + * + * Permission is hereby granted, free of charge, to any person + * obtaining a copy of this software and associated documentation + * files (the "Software"), to deal in the Software without + * restriction, including without limitation the rights to use, + * copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the + * Software is furnished to do so, subject to the following + * conditions: + * + * The above copyright notice and this permission notice shall be + * included in all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, + * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES + * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT + * HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, + * WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING + * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR + * OTHER DEALINGS IN THE SOFTWARE. + */ diff --git a/submodules/pugixml b/submodules/pugixml new file mode 160000 index 0000000000..980cf57ff4 --- /dev/null +++ b/submodules/pugixml @@ -0,0 +1 @@ +Subproject commit 980cf57ff4d21e4734c847f0772c1f98fcbff86f diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 17723d865f..c7d14ed87e 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}") set(NATIVE_CXX "${CMAKE_CXX_COMPILER} ${CMAKE_CXX_FLAGS} -I ${CMAKE_SOURCE_DIR}/include") set(TARGET_TRIPLE "${TARGET_TRIPLE}") diff --git a/test/Feature/Annotation/AllocSource.c b/test/Feature/Annotation/AllocSource.c new file mode 100644 index 0000000000..2dc8cc4fe4 --- /dev/null +++ b/test/Feature/Annotation/AllocSource.c @@ -0,0 +1,66 @@ +// REQUIRES: z3 +// RUN: %clang -DAllocSource1 %s -g -emit-llvm %O0opt -c -o %t1.bc +// RUN: rm -rf %t1.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/AllocSource.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t1.bc 2>&1 | FileCheck %s -check-prefix=CHECK-ALLOCSOURCE1 + +// RUN: %clang -DAllocSource2 %s -g -emit-llvm %O0opt -c -o %t2.bc +// RUN: rm -rf %t2.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t2.klee-out-1 --annotations=%S/AllocSource.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t2.bc 2>&1 | FileCheck %s -check-prefix=CHECK-ALLOCSOURCE2 + +// RUN: %clang -DAllocSource3 %s -g -emit-llvm %O0opt -c -o %t3.bc +// RUN: rm -rf %t3.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t3.klee-out-1 --annotations=%S/AllocSource.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t3.bc 2>&1 | FileCheck %s -check-prefix=CHECK-ALLOCSOURCE3 + +// RUN: %clang -DAllocSource4 %s -g -emit-llvm %O0opt -c -o %t4.bc +// RUN: rm -rf %t4.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t4.klee-out-1 --annotations=%S/AllocSource.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t4.bc 2>&1 | FileCheck %s -check-prefix=CHECK-ALLOCSOURCE4 + +#include + +#ifdef AllocSource1 +void maybeAllocSource1(int *a); +#endif +void maybeAllocSource2(int **a); +int *maybeAllocSource3(); +int **maybeAllocSource4(); + +int main() { + int *a = 0; +#ifdef AllocSource1 + // CHECK-ALLOCSOURCE1: not valid annotation + maybeAllocSource1(a); + // CHECK-ALLOCSOURCE1: Not Allocated + // CHECK-ALLOCSOURCE1: partially completed paths = 1 + // CHECK-ALLOCSOURCE1: generated tests = 1 +#endif + +#ifdef AllocSource2 + maybeAllocSource2(&a); + // CHECK-NOT-ALLOCSOURCE2 : memory error: null pointer exception + // CHECK-NOT-ALLOCSOURCE2: Not Allocated + // CHECK-ALLOCSOURCE2: partially completed paths = 0 + // CHECK-ALLOCSOURCE2: generated tests = 1 +#endif + +#ifdef AllocSource3 + a = maybeAllocSource3(); + // CHECK-NOT-ALLOCSOURCE3 : memory error: null pointer exception + // CHECK-NOT-ALLOCSOURCE3: Not Allocated + // CHECK-ALLOCSOURCE3: partially completed paths = 0 + // CHECK-ALLOCSOURCE3: generated tests = 1 +#endif + +#ifdef AllocSource4 + a = *maybeAllocSource4(); + // CHECK-NOT-ALLOCSOURCE4: memory error: null pointer exception + // CHECK-NOT-ALLOCSOURCE4: Not Allocated + // CHECK-ALLOCSOURCE4 : memory error: out of bound pointer + // CHECK-ALLOCSOURCE4: partially completed paths = 1 + // CHECK-ALLOCSOURCE4: generated tests = 1 +#endif + + assert(a != 0 && "Not Allocated"); + *a = 42; + + return 0; +} diff --git a/test/Feature/Annotation/AllocSource.json b/test/Feature/Annotation/AllocSource.json new file mode 100644 index 0000000000..a31051c64d --- /dev/null +++ b/test/Feature/Annotation/AllocSource.json @@ -0,0 +1,40 @@ +{ + "maybeAllocSource1": { + "name": "maybeAllocSource1", + "annotation": [ + [], + [ + "AllocSource::1" + ] + ], + "properties": [] + }, + "maybeAllocSource2": { + "name": "maybeAllocSource2", + "annotation": [ + [], + [ + "AllocSource:*:1" + ] + ], + "properties": [] + }, + "maybeAllocSource3": { + "name": "maybeAllocSource3", + "annotation": [ + [ + "AllocSource::1" + ] + ], + "properties": [] + }, + "maybeAllocSource4": { + "name": "maybeAllocSource4", + "annotation": [ + [ + "AllocSource::1" + ] + ], + "properties": [] + } +} diff --git a/test/Feature/Annotation/BrokenAnnotation.json b/test/Feature/Annotation/BrokenAnnotation.json new file mode 100644 index 0000000000..0b5c90598f --- /dev/null +++ b/test/Feature/Annotation/BrokenAnnotation.json @@ -0,0 +1,11 @@ +{ + "maybeDeref1": { + "name": "maybeDeref1", + "annotation": [ + [], + [ + "Deref" + ], + "properties": [] + } +} diff --git a/test/Feature/Annotation/Deref.c b/test/Feature/Annotation/Deref.c new file mode 100644 index 0000000000..cb4097e890 --- /dev/null +++ b/test/Feature/Annotation/Deref.c @@ -0,0 +1,104 @@ +// REQUIRES: z3 +// RUN: %clang -DDeref1 %s -g -emit-llvm %O0opt -c -o %t1.bc +// RUN: rm -rf %t1.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/Deref.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t1.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF1 + +// RUN: %clang -DDeref2 %s -g -emit-llvm %O0opt -c -o %t2.bc +// RUN: rm -rf %t2.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t2.klee-out-1 --annotations=%S/Deref.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t2.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF2 + +// RUN: %clang -DDeref3 %s -g -emit-llvm %O0opt -c -o %t3.bc +// RUN: rm -rf %t3.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t3.klee-out-1 --annotations=%S/Deref.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t3.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF3 + +// RUN: %clang -DDeref4 %s -g -emit-llvm %O0opt -c -o %t4.bc +// RUN: rm -rf %t4.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t4.klee-out-1 --annotations=%S/Deref.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t4.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF4 + +// RUN: %clang -DDeref5 %s -g -emit-llvm %O0opt -c -o %t5.bc +// RUN: rm -rf %t5.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t5.klee-out-1 --annotations=%S/Deref.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t5.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF5 + +// RUN: %clang -DDeref6 %s -g -emit-llvm %O0opt -c -o %t6.bc +// RUN: rm -rf %t6.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t6.klee-out-1 --annotations=%S/Deref.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t6.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF6 + +// RUN: %clang -DHASVALUE -DDeref1 -DDeref2 -DDeref3 -DDeref4 -DDeref5 -DDeref6 %s -g -emit-llvm %O0opt -c -o %t7.bc +// RUN: rm -rf %t7.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t7.klee-out-1 --annotations=%S/Deref.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t7.bc 2>&1 | FileCheck %s -check-prefix=CHECK-NODEREF +// CHECK-NODEREF-NOT: memory error: null pointer exception + +// RUN: %clang -DDeref1 -DDeref2 -DDeref3 -DDeref4 -DDeref5 -DDeref6 %s -g -emit-llvm %O0opt -c -o %t8.bc +// RUN: rm -rf %t8.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t8.klee-out-1 --annotations=%S/EmptyAnnotation.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t8.bc 2>&1 | FileCheck %s -check-prefix=CHECK-EMPTY +// CHECK-EMPTY-NOT: memory error: null pointer exception +// CHECK-EMPTY: partially completed paths = 0 +// CHECK-EMPTY: generated tests = 1 + +void maybeDeref1(int *a); +void maybeDeref2(int **a); +void maybeDeref3(int **a); +void maybeDeref4(int b, int *a); +void maybeDeref5(int *a, int b); +void maybeDeref6(int *a, int *b); + +int main() { + int c = 42; +#ifdef HASVALUE + int *a = &c; + int **b = &a; +#else + int *a = 0; + int **b = 0; +#endif + +#ifdef Deref1 + // CHECK-DEREF1: memory error: null pointer exception + maybeDeref1(a); + // CHECK-DEREF1: memory error: out of bound pointer + maybeDeref1((int *)42); + // CHECK-DEREF1: partially completed paths = 2 + // CHECK-DEREF1: generated tests = 3 +#endif + +#ifdef Deref2 + // CHECK-DEREF2: memory error: null pointer exception + maybeDeref2(b); + maybeDeref2(&a); + // CHECK-DEREF2: partially completed paths = 1 + // CHECK-DEREF2: generated tests = 3 +#endif + +#ifdef Deref3 + // CHECK-DEREF3: memory error: null pointer exception + maybeDeref3(&a); + // CHECK-DEREF3: memory error: null pointer exception + maybeDeref3(b); + // CHECK-DEREF3: partially completed paths = 2 + // CHECK-DEREF3: generated tests = 2 +#endif + +#ifdef Deref4 + // CHECK-DEREF4: memory error: null pointer exception + maybeDeref4(0, a); + // CHECK-DEREF4: partially completed paths = 1 + // CHECK-DEREF4: generated tests = 2 +#endif + +#ifdef Deref5 + // CHECK-DEREF5: memory error: null pointer exception + maybeDeref5(a, 0); + // CHECK-DEREF5: partially completed paths = 1 + // CHECK-DEREF5: generated tests = 2 +#endif + +#ifdef Deref6 + // CHECK-DEREF6: memory error: null pointer exception + maybeDeref6(a, &c); + // CHECK-DEREF6: memory error: null pointer exception + maybeDeref6(&c, a); + // CHECK-DEREF6: partially completed paths = 2 + // CHECK-DEREF6: generated tests = 3 +#endif + return 0; +} diff --git a/test/Feature/Annotation/Deref.json b/test/Feature/Annotation/Deref.json new file mode 100644 index 0000000000..02ce7ecbc3 --- /dev/null +++ b/test/Feature/Annotation/Deref.json @@ -0,0 +1,67 @@ +{ + "maybeDeref1": { + "name": "maybeDeref1", + "annotation": [ + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "maybeDeref2": { + "name": "maybeDeref2", + "annotation": [ + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "maybeDeref3": { + "name": "maybeDeref3", + "annotation": [ + [], + [ + "Deref:*" + ] + ], + "properties": [] + }, + "maybeDeref4": { + "name": "maybeDeref4", + "annotation": [ + [], + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "maybeDeref5": { + "name": "maybeDeref5", + "annotation": [ + [], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "maybeDeref6": { + "name": "maybeDeref6", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ] + ], + "properties": [] + } +} diff --git a/test/Feature/Annotation/EmptyAnnotation.json b/test/Feature/Annotation/EmptyAnnotation.json new file mode 100644 index 0000000000..0967ef424b --- /dev/null +++ b/test/Feature/Annotation/EmptyAnnotation.json @@ -0,0 +1 @@ +{} diff --git a/test/Feature/Annotation/General.c b/test/Feature/Annotation/General.c new file mode 100644 index 0000000000..76a122dc9d --- /dev/null +++ b/test/Feature/Annotation/General.c @@ -0,0 +1,43 @@ +// REQUIRES: z3 +// RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc +// RUN: rm -rf %t1.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/BrokenAnnotation.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t1.bc 2>%t.stderr.log || echo "Exit status must be 0" +// RUN: FileCheck -check-prefix=CHECK-JSON --input-file=%t.stderr.log %s +// CHECK-JSON: Annotation: Parsing JSON + +// RUN: %clang -DPTRARG %s -g -emit-llvm %O0opt -c -o %t2.bc +// RUN: rm -rf %t2.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t2.klee-out-1 --annotations=%S/General.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t2.bc 2>&1 | FileCheck %s -check-prefix=CHECK + +// RUN: %clang -DPTRRET %s -g -emit-llvm %O0opt -c -o %t3.bc +// RUN: rm -rf %t3.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t3.klee-out-1 --annotations=%S/General.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t3.bc 2>&1 | FileCheck %s -check-prefix=CHECK + +#include + +struct ST { + int a; + int b; +}; + +void ptrArg(struct ST, int **a); +int *ptrRet(); + +int main() { + int *a = 15; +#ifdef PTRARG + struct ST st; + ptrArg(st, &a); +#endif + +#ifdef PTRRET + a = ptrRet(); +#endif + + // CHECK: memory error: null pointer exception + // CHECK: partially completed paths = 1 + // CHECK: generated tests = 2 + *a = 42; + + return 0; +} diff --git a/test/Feature/Annotation/General.json b/test/Feature/Annotation/General.json new file mode 100644 index 0000000000..606550656f --- /dev/null +++ b/test/Feature/Annotation/General.json @@ -0,0 +1,24 @@ +{ + "ptrArg": { + "name": "ptrArg", + "annotation": [ + [], + [], + [ + "InitNull:*", + "AllocSource:*:1" + ] + ], + "properties": [] + }, + "ptrRet": { + "name": "ptrRet", + "annotation": [ + [ + "InitNull", + "AllocSource::1" + ] + ], + "properties": [] + } +} diff --git a/test/Feature/Annotation/InitNull.c b/test/Feature/Annotation/InitNull.c new file mode 100644 index 0000000000..2f4d0c7b8c --- /dev/null +++ b/test/Feature/Annotation/InitNull.c @@ -0,0 +1,68 @@ +// REQUIRES: z3 +// RUN: %clang -DInitNull1 %s -g -emit-llvm %O0opt -c -o %t1.bc +// RUN: rm -rf %t1.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/InitNull.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t1.bc 2>&1 | FileCheck %s -check-prefix=CHECK-INITNULL1 + +// RUN: %clang -DInitNull2 %s -g -emit-llvm %O0opt -c -o %t2.bc +// RUN: rm -rf %t2.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t2.klee-out-1 --annotations=%S/InitNull.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t2.bc 2>&1 | FileCheck %s -check-prefix=CHECK-INITNULL2 + +// RUN: %clang -DInitNull3 %s -g -emit-llvm %O0opt -c -o %t3.bc +// RUN: rm -rf %t3.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t3.klee-out-1 --annotations=%S/InitNull.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t3.bc 2>&1 | FileCheck %s -check-prefix=CHECK-INITNULL3 + +// RUN: %clang -DInitNull4 %s -g -emit-llvm %O0opt -c -o %t4.bc +// RUN: rm -rf %t4.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t4.klee-out-1 --annotations=%S/InitNull.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t4.bc 2>&1 | FileCheck %s -check-prefix=CHECK-INITNULL4 + +// RUN: %clang -DInitNull1 -DInitNull2 -DInitNull3 -DInitNull4 %s -g -emit-llvm %O0opt -c -o %t5.bc +// RUN: rm -rf %t5.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t5.klee-out-1 --annotations=%S/InitNullEmpty.json --external-calls=all --mock-all-externals --mock-external-calls --mock-linked-externals --mock-strategy=naive -emit-all-errors=true %t5.bc 2>&1 | FileCheck %s -check-prefix=CHECK-EMPTY +// CHECK-EMPTY: ASSERTION FAIL: a != 0 && "A is Null" +// CHECK-EMPTY: ASSERTION FAIL: a != 0 && "A is Null" +// CHECK-EMPTY: partially completed paths = 2 + +#include + +#ifdef InitNull1 +void maybeInitNull1(int *a); +#endif +void maybeInitNull2(int **a); +int *maybeInitNull3(); +int **maybeInitNull4(); + +int main() { + int c = 42; + int *a = &c; +#ifdef InitNull1 + // CHECK-INITNULL1: not valid annotation + maybeInitNull1(a); + // CHECK-INITNULL1-NOT: A is Null + // CHECK-INITNULL1: partially completed paths = 0 + // CHECK-INITNULL1: generated tests = 1 +#endif + +#ifdef InitNull2 + maybeInitNull2(&a); + // CHECK-INITNULL2: ASSERTION FAIL: a != 0 && "A is Null" + // CHECK-INITNULL2: partially completed paths = 1 + // CHECK-INITNULL2: generated tests = 2 +#endif + +#ifdef InitNull3 + a = maybeInitNull3(); + // CHECK-INITNULL3: ASSERTION FAIL: a != 0 && "A is Null" + // CHECK-INITNULL3: partially completed paths = 1 + // CHECK-INITNULL3: generated tests = 2 +#endif + +#ifdef InitNull4 + a = *maybeInitNull4(); + // CHECK-INITNULL4: ASSERTION FAIL: a != 0 && "A is Null" + // CHECK-INITNULL4: partially completed paths = 3 +#endif + + assert(a != 0 && "A is Null"); + + return 0; +} diff --git a/test/Feature/Annotation/InitNull.json b/test/Feature/Annotation/InitNull.json new file mode 100644 index 0000000000..fdd88c757a --- /dev/null +++ b/test/Feature/Annotation/InitNull.json @@ -0,0 +1,40 @@ +{ + "maybeInitNull1": { + "name": "maybeInitNull1", + "annotation": [ + [], + [ + "InitNull" + ] + ], + "properties": [] + }, + "maybeInitNull2": { + "name": "maybeInitNull2", + "annotation": [ + [], + [ + "InitNull:*" + ] + ], + "properties": [] + }, + "maybeInitNull3": { + "name": "maybeInitNull3", + "annotation": [ + [ + "InitNull" + ] + ], + "properties": [] + }, + "maybeInitNull4": { + "name": "maybeInitNull4", + "annotation": [ + [ + "InitNull:*" + ] + ], + "properties": [] + } +} diff --git a/test/Feature/Annotation/InitNullEmpty.json b/test/Feature/Annotation/InitNullEmpty.json new file mode 100644 index 0000000000..535d0a767b --- /dev/null +++ b/test/Feature/Annotation/InitNullEmpty.json @@ -0,0 +1,32 @@ +{ + "maybeInitNull1": { + "name": "maybeInitNull1", + "annotation": [ + [], + [] + ], + "properties": [] + }, + "maybeInitNull2": { + "name": "maybeInitNull2", + "annotation": [ + [], + [] + ], + "properties": [] + }, + "maybeInitNull3": { + "name": "maybeInitNull3", + "annotation": [ + [] + ], + "properties": [] + }, + "maybeInitNull4": { + "name": "maybeInitNull4", + "annotation": [ + [] + ], + "properties": [] + } +} diff --git a/test/Feature/MockPointersDeterministic.c b/test/Feature/MockPointersDeterministic.c index d8c871588d..7788138852 100644 --- a/test/Feature/MockPointersDeterministic.c +++ b/test/Feature/MockPointersDeterministic.c @@ -2,8 +2,9 @@ // 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: memory error: out of bound pointer // CHECK-1: KLEE: done: completed paths = 1 // CHECK-1: KLEE: done: partially completed paths = 2 // CHECK-1: KLEE: done: generated tests = 3 @@ -20,4 +21,4 @@ int main() { assert(0 && "age is deterministic"); } return *age(); -} \ No newline at end of file +} diff --git a/test/Replay/libkleeruntest/replay_mocks.c b/test/Replay/libkleeruntest/replay_mocks.c index cfd151a9e5..bb9c9e7691 100644 --- a/test/Replay/libkleeruntest/replay_mocks.c +++ b/test/Replay/libkleeruntest/replay_mocks.c @@ -1,12 +1,14 @@ // 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 -o %t.klee-out/a.out %libkleeruntest %t.klee-out/externals.ll %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.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..83d7a0f2a3 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: @@ -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')) 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 diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 0b329acc40..e17f954543 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -12,13 +12,10 @@ #include "klee/ADT/KTest.h" #include "klee/ADT/TreeStream.h" #include "klee/Config/Version.h" -#include "klee/Core/Annotation.h" #include "klee/Core/Context.h" #include "klee/Core/Interpreter.h" #include "klee/Core/TargetedExecutionReporter.h" #include "klee/Module/LocationInfo.h" -#include "klee/Core/FunctionAnnotation.h" -#include "klee/Module/Annotation.h" #include "klee/Module/SarifReport.h" #include "klee/Module/TargetForest.h" #include "klee/Solver/SolverCmdLine.h" @@ -400,8 +397,12 @@ cl::OptionCategory AnnotCat("Annotations category"); cl::opt AnnotationsFile("annotations", cl::desc("Path to the annotation JSON file"), - cl::value_desc("path file"), - cl::cat(AnnotCat)); + cl::value_desc("path file"), cl::cat(AnnotCat)); + +cl::opt AnnotateOnlyExternal( + "annotate-only-external", + cl::desc("Ignore annotations for defined function (default=false)"), + cl::init(false), cl::cat(AnnotCat)); } // namespace @@ -1077,10 +1078,25 @@ static const char *dontCareExternals[] = { #endif // static information, pretty ok to return - "getegid", "geteuid", "getgid", "getuid", "getpid", "gethostname", - "getpgrp", "getppid", "getpagesize", "getpriority", "getgroups", - "getdtablesize", "getrlimit", "getrlimit64", "getcwd", "getwd", - "gettimeofday", "uname", "ioctl", + "getegid", + "geteuid", + "getgid", + "getuid", + "getpid", + "gethostname", + "getpgrp", + "getppid", + "getpagesize", + "getpriority", + "getgroups", + "getdtablesize", + "getrlimit", + "getrlimit64", + "getcwd", + "getwd", + "gettimeofday", + "uname", + "ioctl", // fp stuff we just don't worry about yet "frexp", @@ -1317,7 +1333,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 @@ -1615,34 +1631,30 @@ void mockLinkedExternals( const Interpreter::ModuleOptions &Opts, llvm::LLVMContext &ctx, llvm::Module *mainModule, std::vector> &loadedLibsModules, - llvm::raw_string_ostream *redefineFile) { + std::vector> &redefinitions) { 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)) { + if (!klee::loadFileAsOneModule(Path.c_str(), ctx, loadedLibsModules, + 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; - } + for (const auto &fmodel : loadedLibsModules.back()->functions()) { + if (fmodel.getName().str().substr(0, 15) != "__klee_wrapped_") { + continue; + } + if (llvm::Function *f = + mainModule->getFunction(fmodel.getName().str().substr(15))) { klee_message("Renamed symbol %s to %s", f->getName().str().c_str(), fmodel.getName().str().c_str()); - *redefineFile << f->getName() << ' ' << fmodel.getName() << '\n'; + redefinitions.emplace_back(f->getName(), fmodel.getName()); f->setName(fmodel.getName()); } - loadedLibsModules.push_back(std::move(module)); } } @@ -1807,12 +1819,6 @@ int main(int argc, char **argv, char **envp) { klee_warning("Module and host target triples do not match: '%s' != '%s'\n" "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 bit_suffix = "64"; // Fall back to 64bit if (module_triple.find("i686") != std::string::npos || @@ -1831,13 +1837,15 @@ int main(int argc, char **argv, char **envp) { std::string LibraryDir = KleeHandler::getRunTimeLibraryPath(argv[0]); Interpreter::ModuleOptions Opts( - LibraryDir.c_str(), EntryPoint, opt_suffix, + LibraryDir, EntryPoint, opt_suffix, /*MainCurrentName=*/EntryPoint, /*MainNameAfterMock=*/"__klee_mock_wrapped_main", + /*AnnotationsFile=*/AnnotationsFile, /*Optimize=*/OptimizeModule, /*Simplify*/ SimplifyModule, /*CheckDivZero=*/CheckDivZero, /*CheckOvershift=*/CheckOvershift, + /*AnnotateOnlyExternal=*/AnnotateOnlyExternal, /*WithFPRuntime=*/WithFPRuntime, /*WithPOSIXRuntime=*/WithPOSIXRuntime); @@ -1861,15 +1869,13 @@ 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); + std::vector> redefinitions; if (MockLinkedExternals) { mockLinkedExternals(Opts, ctx, mainModule, loadedLibsModules, - &o_redefinitions); + redefinitions); } - if (MockUnlinkedStrategy != MockStrategy::None) { - o_redefinitions << EntryPoint << ' ' << Opts.MainNameAfterMock << '\n'; + redefinitions.emplace_back(EntryPoint, Opts.MainNameAfterMock); } if (WithPOSIXRuntime) { @@ -2037,10 +2043,6 @@ int main(int argc, char **argv, char **envp) { UseGuidedSearch = Interpreter::GuidanceKind::ErrorGuidance; } - const Annotations annotations = (AnnotationsFile.empty()) - ? Annotations() - : parseAnnotationsFile(AnnotationsFile); - Interpreter::InterpreterOptions IOpts(paths); IOpts.MakeConcreteSymbolic = MakeConcreteSymbolic; IOpts.Guidance = UseGuidedSearch; @@ -2080,13 +2082,7 @@ int main(int argc, char **argv, char **envp) { ignoredExternals.insert("syscall"); } - Opts.MainCurrentName = initialMainFn->getName().str(); - - if (MockLinkedExternals || MockUnlinkedStrategy != MockStrategy::None) { - o_redefinitions.flush(); - auto f_redefinitions = handler->openOutputFile("redefinitions.txt"); - *f_redefinitions << redefinitions; - } + Opts.MainCurrentName = entryFn->getName().str(); // Get the desired main function. klee_main initializes uClibc // locale and other data and then calls main. @@ -2094,7 +2090,7 @@ int main(int argc, char **argv, char **envp) { auto finalModule = interpreter->setModule( loadedUserModules, loadedLibsModules, Opts, std::move(mainModuleFunctions), std::move(mainModuleGlobals), - std::move(origInstructions), ignoredExternals, annotations); + std::move(origInstructions), ignoredExternals, redefinitions); Function *mainFn = finalModule->getFunction(EntryPoint); if (!mainFn) { klee_error("Entry function '%s' not found in module.", EntryPoint.c_str()); diff --git a/unittests/Annotations/AnnotationsTest.cpp b/unittests/Annotations/AnnotationsTest.cpp index 9d67ab9461..b48bcf7004 100644 --- a/unittests/Annotations/AnnotationsTest.cpp +++ b/unittests/Annotations/AnnotationsTest.cpp @@ -10,15 +10,18 @@ TEST(AnnotationsTest, Empty) { const json j = json::parse(R"( { "foo" : { - "annotation" : [], + "annotation" : [[]], "properties" : [] } } )"); - const Annotations expected = Annotations{ - {"foo", Annotation{"foo", std::vector(), - std::set()}}}; - const Annotations actual = parseAnnotationsFile(j); + const AnnotationsMap expected = { + {"foo", + {/*functionName*/ "foo", + /*returnStatements*/ std::vector(), + /*argsStatements*/ std::vector>(), + /*properties*/ std::set()}}}; + const AnnotationsMap actual = parseAnnotationsJson(j); ASSERT_EQ(expected, actual); } @@ -26,17 +29,20 @@ TEST(AnnotationsTest, KnownProperties) { const json j = json::parse(R"( { "foo" : { - "annotation" : [], - "properties" : ["determ", "noreturn", "determ"] + "annotation" : [[]], + "properties" : ["deterministic", "noreturn", "deterministic"] } } )"); - const std::set properties{ - Annotation::Property::Determ, Annotation::Property::Noreturn}; - const Annotations expected = Annotations{ - {"foo", Annotation{"foo", std::vector(), - properties}}}; - const Annotations actual = parseAnnotationsFile(j); + const std::set properties{ + Statement::Property::Deterministic, Statement::Property::Noreturn}; + const AnnotationsMap expected = { + {"foo", + {/*functionName*/ "foo", + /*returnStatements*/ std::vector(), + /*argsStatements*/ std::vector>(), + /*properties*/ properties}}}; + const AnnotationsMap actual = parseAnnotationsJson(j); ASSERT_EQ(expected, actual); } @@ -44,18 +50,21 @@ TEST(AnnotationsTest, UnknownProperties) { const json j = json::parse(R"( { "foo" : { - "annotation" : [], - "properties" : ["derm", "noreturn", "determ"] + "annotation" : [[]], + "properties" : ["noname", "noreturn", "deterministic"] } } )"); - const std::set properties{ - Annotation::Property::Determ, Annotation::Property::Noreturn, - Annotation::Property::Unknown}; - const Annotations expected = Annotations{ - {"foo", Annotation{"foo", std::vector(), - properties}}}; - const Annotations actual = parseAnnotationsFile(j); + const std::set properties{ + Statement::Property::Deterministic, Statement::Property::Noreturn, + Statement::Property::Unknown}; + const AnnotationsMap expected = { + {"foo", + {/*functionName*/ "foo", + /*returnStatements*/ std::vector(), + /*argsStatements*/ std::vector>(), + /*properties*/ properties}}}; + const AnnotationsMap actual = parseAnnotationsJson(j); ASSERT_EQ(expected, actual); } @@ -68,9 +77,9 @@ TEST(AnnotationsTest, UnknownAnnotations) { } } )"); - const Annotations actual = parseAnnotationsFile(j); - ASSERT_EQ(actual.at("foo").statements[1][0]->getStatementName(), - Annotation::StatementKind::Unknown); + const AnnotationsMap actual = parseAnnotationsJson(j); + ASSERT_EQ(actual.at("foo").argsStatements[0][0]->getKind(), + Statement::Kind::Unknown); } TEST(AnnotationsTest, KnownAnnotations) { @@ -82,13 +91,13 @@ TEST(AnnotationsTest, KnownAnnotations) { } } )"); - const Annotations actual = parseAnnotationsFile(j); - ASSERT_EQ(actual.at("foo").statements[0][0]->getStatementName(), - Annotation::StatementKind::InitNull); - ASSERT_EQ(actual.at("foo").statements[1][0]->getStatementName(), - Annotation::StatementKind::Deref); - ASSERT_EQ(actual.at("foo").statements[1][1]->getStatementName(), - Annotation::StatementKind::InitNull); + const AnnotationsMap actual = parseAnnotationsJson(j); + ASSERT_EQ(actual.at("foo").returnStatements[0]->getKind(), + Statement::Kind::InitNull); + ASSERT_EQ(actual.at("foo").argsStatements[0][0]->getKind(), + Statement::Kind::Deref); + ASSERT_EQ(actual.at("foo").argsStatements[0][1]->getKind(), + Statement::Kind::InitNull); } TEST(AnnotationsTest, WithOffsets) { @@ -100,9 +109,9 @@ TEST(AnnotationsTest, WithOffsets) { } } )"); - const Annotations actual = parseAnnotationsFile(j); - ASSERT_EQ(actual.at("foo").statements[0][0]->getStatementName(), - Annotation::StatementKind::InitNull); + const AnnotationsMap actual = parseAnnotationsJson(j); + ASSERT_EQ(actual.at("foo").returnStatements[0]->getKind(), + Statement::Kind::InitNull); const std::vector expectedOffset{"*", "10", "*", "&"}; - ASSERT_EQ(actual.at("foo").statements[0][0]->offset, expectedOffset); + ASSERT_EQ(actual.at("foo").returnStatements[0]->offset, expectedOffset); }