From c8b06fdb7a82e0a7b68c48800b82738b14b1b82a Mon Sep 17 00:00:00 2001 From: Lana243 Date: Fri, 16 Jun 2023 14:15:47 +0300 Subject: [PATCH] [squash] of Annotations branch --- .gitmodules | 7 +- CMakeLists.txt | 17 +- include/klee/Config/config.h.cmin | 3 + include/klee/Core/Interpreter.h | 45 +- include/klee/Core/MockBuilder.h | 71 ++ include/klee/Expr/IndependentSet.h | 2 + include/klee/Expr/SourceBuilder.h | 8 + include/klee/Expr/SymbolicSource.h | 58 +- include/klee/Module/Annotation.h | 125 ++++ include/klee/klee.h | 1 + lib/Core/CMakeLists.txt | 1 + lib/Core/ExecutionState.cpp | 1 + lib/Core/Executor.cpp | 46 +- lib/Core/Executor.h | 17 +- lib/Core/MockBuilder.cpp | 620 ++++++++++++++++++ lib/Core/SpecialFunctionHandler.cpp | 82 +++ lib/Core/SpecialFunctionHandler.h | 1 + lib/Expr/ExprPPrinter.cpp | 12 + lib/Expr/ExprUtil.cpp | 10 + lib/Expr/IndependentSet.cpp | 16 +- lib/Expr/Parser.cpp | 36 + lib/Expr/SourceBuilder.cpp | 19 +- lib/Expr/SymbolicSource.cpp | 63 +- lib/Module/Annotation.cpp | 377 +++++++++++ lib/Module/CMakeLists.txt | 8 + lib/Solver/Z3Builder.cpp | 32 + lib/Solver/Z3Builder.h | 7 + runtime/CMakeLists.txt | 2 + runtime/Mocks/CMakeLists.txt | 19 + runtime/Mocks/models.c | 36 + runtime/Runtest/CMakeLists.txt | 2 + runtime/Runtest/intrinsics.c | 11 +- scripts/cooddy_annotations.py | 41 ++ scripts/run_tests_with_mocks.py | 26 + 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/Free.c | 45 ++ test/Feature/Annotation/Free.json | 31 + 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 | 24 + test/Feature/MockStrategies.c | 37 ++ test/Replay/libkleeruntest/replay_mocks.c | 21 + test/lit.cfg | 17 +- test/lit.site.cfg.in | 1 + tools/klee/main.cpp | 138 +++- unittests/Annotations/AnnotationsTest.cpp | 117 ++++ unittests/Annotations/CMakeLists.txt | 3 + unittests/CMakeLists.txt | 1 + 61 files changed, 2792 insertions(+), 44 deletions(-) create mode 100644 include/klee/Core/MockBuilder.h create mode 100644 include/klee/Module/Annotation.h create mode 100644 lib/Core/MockBuilder.cpp create mode 100644 lib/Module/Annotation.cpp create mode 100644 runtime/Mocks/CMakeLists.txt create mode 100644 runtime/Mocks/models.c create mode 100755 scripts/cooddy_annotations.py create mode 100755 scripts/run_tests_with_mocks.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/Free.c create mode 100644 test/Feature/Annotation/Free.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 create mode 100644 test/Feature/MockPointersDeterministic.c create mode 100644 test/Feature/MockStrategies.c create mode 100644 test/Replay/libkleeruntest/replay_mocks.c create mode 100644 unittests/Annotations/AnnotationsTest.cpp create mode 100644 unittests/Annotations/CMakeLists.txt 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 766380b486..2f1f63ff7c 100644 --- a/include/klee/Core/Interpreter.h +++ b/include/klee/Core/Interpreter.h @@ -10,6 +10,7 @@ #define KLEE_INTERPRETER_H #include "TerminationTypes.h" +#include "klee/Module/Annotation.h" #include "klee/Module/SarifReport.h" @@ -32,6 +33,7 @@ class BasicBlock; class Function; class LLVMContext; class Module; +class Type; class raw_ostream; class raw_fd_ostream; } // namespace llvm @@ -66,6 +68,13 @@ using FLCtoOpcode = std::unordered_map< std::unordered_map< unsigned, std::unordered_map>>>; +enum class MockStrategy { + None, // No mocks are generated + Naive, // For each function call new symbolic value is generated + Deterministic, // Each function is treated as uninterpreted function in SMT. + // Compatible with Z3 solver only +}; + class Interpreter { public: enum class GuidanceKind { @@ -82,21 +91,32 @@ class Interpreter { std::string LibraryDir; std::string EntryPoint; std::string OptSuffix; + std::string MainCurrentName; + std::string MainNameAfterMock; + std::string AnnotationsFile; bool Optimize; bool Simplify; bool CheckDivZero; bool CheckOvershift; + bool AnnotateOnlyExternal; bool WithFPRuntime; bool WithPOSIXRuntime; ModuleOptions(const std::string &_LibraryDir, const std::string &_EntryPoint, const std::string &_OptSuffix, - bool _Optimize, bool _Simplify, bool _CheckDivZero, - bool _CheckOvershift, bool _WithFPRuntime, + const std::string &_MainCurrentName, + const std::string &_MainNameAfterMock, + const std::string &_AnnotationsFile, bool _Optimize, + bool _Simplify, bool _CheckDivZero, bool _CheckOvershift, + bool _AnnotateOnlyExternal, bool _WithFPRuntime, bool _WithPOSIXRuntime) : LibraryDir(_LibraryDir), EntryPoint(_EntryPoint), - OptSuffix(_OptSuffix), Optimize(_Optimize), Simplify(_Simplify), - CheckDivZero(_CheckDivZero), CheckOvershift(_CheckOvershift), + OptSuffix(_OptSuffix), MainCurrentName(_MainCurrentName), + MainNameAfterMock(_MainNameAfterMock), + AnnotationsFile(_AnnotationsFile), Optimize(_Optimize), + Simplify(_Simplify), CheckDivZero(_CheckDivZero), + CheckOvershift(_CheckOvershift), + AnnotateOnlyExternal(_AnnotateOnlyExternal), WithFPRuntime(_WithFPRuntime), WithPOSIXRuntime(_WithPOSIXRuntime) {} }; @@ -115,10 +135,11 @@ class Interpreter { unsigned MakeConcreteSymbolic; GuidanceKind Guidance; nonstd::optional Paths; + enum MockStrategy MockStrategy; InterpreterOptions(nonstd::optional Paths) : MakeConcreteSymbolic(false), Guidance(GuidanceKind::NoGuidance), - Paths(std::move(Paths)) {} + Paths(std::move(Paths)), MockStrategy(MockStrategy::None) {} }; protected: @@ -141,13 +162,13 @@ class Interpreter { /// module /// \return The final module after it has been optimized, checks /// inserted, and modified for interpretation. - virtual llvm::Module * - setModule(std::vector> &userModules, - std::vector> &libsModules, - const ModuleOptions &opts, - std::set &&mainModuleFunctions, - std::set &&mainModuleGlobals, - FLCtoOpcode &&origInstructions) = 0; + virtual llvm::Module *setModule( + std::vector> &userModules, + std::vector> &libsModules, + const ModuleOptions &opts, std::set &&mainModuleFunctions, + std::set &&mainModuleGlobals, FLCtoOpcode &&origInstructions, + const std::set &ignoredExternals, + 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 new file mode 100644 index 0000000000..72ddfed001 --- /dev/null +++ b/include/klee/Core/MockBuilder.h @@ -0,0 +1,71 @@ +#ifndef KLEE_MOCKBUILDER_H +#define KLEE_MOCKBUILDER_H + +#include "klee/Core/Interpreter.h" +#include "klee/Module/Annotation.h" + +#include "llvm/IR/IRBuilder.h" +#include "llvm/IR/Module.h" + +#include +#include + +namespace klee { + +class MockBuilder { +private: + const llvm::Module *userModule; + std::unique_ptr mockModule; + std::unique_ptr> builder; + + const Interpreter::ModuleOptions &opts; + + std::set ignoredExternals; + std::vector> redefinitions; + + InterpreterHandler *interpreterHandler; + + AnnotationsMap annotations; + + void initMockModule(); + void buildMockMain(); + void buildExternalGlobalsDefinitions(); + void buildExternalFunctionsDefinitions(); + void + buildCallKleeMakeSymbolic(const std::string &kleeMakeSymbolicFunctionName, + llvm::Value *source, llvm::Type *type, + const std::string &symbolicName); + + void buildAnnotationForExternalFunctionArgs( + llvm::Function *func, + const std::vector> &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, + 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 buildFree(llvm::Value *elem, const Statement::Free *freePtr); + void processingValue(llvm::Value *prev, llvm::Type *elemType, + const Statement::AllocSource *allocSourcePtr, + const Statement::InitNull *initNullPtr); +}; + +} // namespace klee + +#endif // KLEE_MOCKBUILDER_H diff --git a/include/klee/Expr/IndependentSet.h b/include/klee/Expr/IndependentSet.h index a0878ea6c2..498bf1cc34 100644 --- a/include/klee/Expr/IndependentSet.h +++ b/include/klee/Expr/IndependentSet.h @@ -109,6 +109,8 @@ class IndependentConstraintSet { InnerSetUnion concretizedSets; + std::set uninterpretedFunctions; + ref addExpr(ref e) const; ref updateConcretization(const Assignment &delta, diff --git a/include/klee/Expr/SourceBuilder.h b/include/klee/Expr/SourceBuilder.h index 7b57e2f8c9..827dc092e9 100644 --- a/include/klee/Expr/SourceBuilder.h +++ b/include/klee/Expr/SourceBuilder.h @@ -5,6 +5,8 @@ #include "klee/Expr/SymbolicSource.h" #include "klee/Module/KModule.h" +#include "llvm/IR/Function.h" + namespace klee { class SourceBuilder { @@ -28,6 +30,12 @@ class SourceBuilder { static ref value(const llvm::Value &_allocSite, int _index, KModule *km); static ref irreproducible(const std::string &name); + static ref mockNaive(const KModule *kModule, + const llvm::Function &kFunction, + unsigned version); + static ref + mockDeterministic(const KModule *kModule, const llvm::Function &kFunction, + const std::vector> &args); }; }; // namespace klee diff --git a/include/klee/Expr/SymbolicSource.h b/include/klee/Expr/SymbolicSource.h index be65580f7b..2f52844268 100644 --- a/include/klee/Expr/SymbolicSource.h +++ b/include/klee/Expr/SymbolicSource.h @@ -17,10 +17,12 @@ DISABLE_WARNING_POP namespace klee { +class Expr; class Array; class Expr; class ConstantExpr; class KModule; +struct KFunction; class SymbolicSource { protected: @@ -41,7 +43,9 @@ class SymbolicSource { LazyInitializationSize, Instruction, Argument, - Irreproducible + Irreproducible, + MockNaive, + MockDeterministic }; public: @@ -361,6 +365,58 @@ class IrreproducibleSource : public SymbolicSource { } }; +class MockSource : public SymbolicSource { +public: + const KModule *km; + const llvm::Function &function; + MockSource(const KModule *_km, const llvm::Function &_function) + : km(_km), function(_function) {} + + static bool classof(const SymbolicSource *S) { + return S->getKind() == Kind::MockNaive || + S->getKind() == Kind::MockDeterministic; + } +}; + +class MockNaiveSource : public MockSource { +public: + const unsigned version; + + MockNaiveSource(const KModule *km, const llvm::Function &function, + unsigned _version) + : MockSource(km, function), version(_version) {} + + Kind getKind() const override { return Kind::MockNaive; } + std::string getName() const override { return "mockNaive"; } + + static bool classof(const SymbolicSource *S) { + return S->getKind() == Kind::MockNaive; + } + + unsigned computeHash() override; + + int internalCompare(const SymbolicSource &b) const override; +}; + +class MockDeterministicSource : public MockSource { +public: + const std::vector> args; + + MockDeterministicSource(const KModule *_km, const llvm::Function &_function, + const std::vector> &_args); + + Kind getKind() const override { return Kind::MockDeterministic; } + std::string getName() const override { return "mockDeterministic"; } + + static bool classof(const SymbolicSource *S) { + return S->getKind() == Kind::MockDeterministic; + } + + unsigned computeHash() override; + + int internalCompare(const SymbolicSource &b) const override; +}; + } // namespace klee #endif /* KLEE_SYMBOLICSOURCE_H */ diff --git a/include/klee/Module/Annotation.h b/include/klee/Module/Annotation.h new file mode 100644 index 0000000000..af2431acb7 --- /dev/null +++ b/include/klee/Module/Annotation.h @@ -0,0 +1,125 @@ +#ifndef KLEE_ANNOTATION_H +#define KLEE_ANNOTATION_H + +#include "map" +#include "set" +#include "string" +#include "vector" + +#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 { + +namespace Statement { +enum class Kind { + Unknown, + + Deref, + InitNull, + // TODO: rename to alloc + AllocSource, + Free +}; + +enum class Property { + Unknown, + + Deterministic, + Noreturn, +}; + +struct Unknown { +protected: + std::string rawAnnotation; + std::string rawOffset; + std::string rawValue; + +public: + std::vector offset; + + explicit Unknown(const std::string &str = "Unknown"); + virtual ~Unknown(); + + virtual bool operator==(const Unknown &other) const; + [[nodiscard]] virtual Kind getKind() const; + + [[nodiscard]] const std::vector &getOffset() const; + [[nodiscard]] std::string toString() const; +}; + +struct Deref final : public Unknown { + explicit Deref(const std::string &str = "Deref"); + + [[nodiscard]] Kind getKind() 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) + }; + + Type value; + + explicit AllocSource(const std::string &str = "AllocSource::1"); + + [[nodiscard]] Kind getKind() const override; +}; + +struct Free final : public Unknown { +public: + enum Type { + Free_ = 1, // Kind of free function + Delete = 2, // operator delete + DeleteBrackets = 3, // operator delete[] + CloseFile = 4, // close file + MutexUnlock = 5 // mutex unlock (pthread_mutex_unlock) + }; + + Type value; + + explicit Free(const std::string &str = "FreeSource::1"); + + [[nodiscard]] Kind getKind() const override; +}; + +using Ptr = std::shared_ptr; +bool operator==(const Ptr &first, const Ptr &second); +} // namespace Statement + +// Annotation format: https://github.com/UnitTestBot/klee/discussions/92 +struct Annotation { + std::string functionName; + std::vector returnStatements; + std::vector> argsStatements; + std::set properties; + + bool operator==(const Annotation &other) const; +}; + +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/include/klee/klee.h b/include/klee/klee.h index 9c40ef335c..5995ff2e24 100644 --- a/include/klee/klee.h +++ b/include/klee/klee.h @@ -201,5 +201,6 @@ long double klee_rintl(long double d); // stdin/stdout void klee_init_env(int *argcPtr, char ***argvPtr); void check_stdin_read(); +void *__klee_wrapped_malloc(size_t size); #endif /* KLEE_H */ diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt index 9d94da9169..9e0dbb715c 100644 --- a/lib/Core/CMakeLists.txt +++ b/lib/Core/CMakeLists.txt @@ -22,6 +22,7 @@ add_library(kleeCore Memory.cpp MemoryManager.cpp PForest.cpp + MockBuilder.cpp PTree.cpp Searcher.cpp SeedInfo.cpp diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 05142dd2c4..0c6f478565 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -22,6 +22,7 @@ #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" diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index c58e1a51ac..fbb1cad498 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -39,6 +39,7 @@ #include "klee/Config/Version.h" #include "klee/Config/config.h" #include "klee/Core/Interpreter.h" +#include "klee/Core/MockBuilder.h" #include "klee/Expr/ArrayExprOptimizer.h" #include "klee/Expr/ArrayExprVisitor.h" #include "klee/Expr/Assignment.h" @@ -480,6 +481,11 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, replayKTest(0), replayPath(0), usingSeeds(0), atMemoryLimit(false), inhibitForking(false), haltExecution(HaltExecution::NotHalt), ivcEnabled(false), debugLogBuffer(debugBufferString) { + if (CoreSolverToUse != Z3_SOLVER && + interpreterOpts.MockStrategy == MockStrategy::Deterministic) { + klee_error("Deterministic mocks can be generated with Z3 solver only.\n"); + } + const time::Span maxTime{MaxTime}; if (maxTime) timers.add(std::make_unique(maxTime, [&] { @@ -539,10 +545,23 @@ llvm::Module *Executor::setModule( std::vector> &userModules, std::vector> &libsModules, const ModuleOptions &opts, std::set &&mainModuleFunctions, - std::set &&mainModuleGlobals, FLCtoOpcode &&origInstructions) { + std::set &&mainModuleGlobals, FLCtoOpcode &&origInstructions, + const std::set &ignoredExternals, + std::vector> redefinitions) { assert(!kmodule && !userModules.empty() && "can only register one module"); // XXX gross + if (ExternalCalls == ExternalCallPolicy::All && + interpreterOpts.MockStrategy != MockStrategy::None) { + llvm::Function *mainFn = + userModules.front()->getFunction(opts.MainCurrentName); + if (!mainFn) { + klee_error("Entry function '%s' not found in module.", + opts.MainCurrentName.c_str()); + } + mainFn->setName(opts.MainNameAfterMock); + } + kmodule = std::make_unique(); // 1.) Link the modules together && 2.) Apply different instrumentation @@ -567,6 +586,29 @@ llvm::Module *Executor::setModule( kmodule->instrument(opts); } + 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, 1); + + for (auto &global : kmodule->module->globals()) { + if (global.isDeclaration()) { + llvm::Constant *zeroInitializer = + llvm::Constant::getNullValue(global.getValueType()); + if (!zeroInitializer) { + klee_error("Unable to get zero initializer for '%s'", + global.getName().str().c_str()); + } + global.setInitializer(zeroInitializer); + } + } + } + // 3.) Optimise and prepare for KLEE // Create a list of functions that should be preserved if used @@ -5056,7 +5098,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; diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index a7e0df7160..aa028dffe5 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -696,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); @@ -723,13 +726,13 @@ class Executor : public Interpreter { replayPosition = 0; } - llvm::Module * - setModule(std::vector> &userModules, - std::vector> &libsModules, - const ModuleOptions &opts, - std::set &&mainModuleFunctions, - std::set &&mainModuleGlobals, - FLCtoOpcode &&origInstructions) override; + llvm::Module *setModule( + std::vector> &userModules, + std::vector> &libsModules, + const ModuleOptions &opts, std::set &&mainModuleFunctions, + std::set &&mainModuleGlobals, FLCtoOpcode &&origInstructions, + 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 new file mode 100644 index 0000000000..cb0ef96a19 --- /dev/null +++ b/lib/Core/MockBuilder.cpp @@ -0,0 +1,620 @@ +#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 { + +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); +} + +void MockBuilder::initMockModule() { + mockModule = std::make_unique(userModule->getName().str() + + "__klee_externals", + userModule->getContext()); + mockModule->setTargetTriple(userModule->getTargetTriple()); + mockModule->setDataLayout(userModule->getDataLayout()); + builder = std::make_unique>(mockModule->getContext()); +} + +// Set up entrypoint in new module. Here we'll define external globals and then +// call user's entrypoint. +void MockBuilder::buildMockMain() { + llvm::Function *userMainFn = userModule->getFunction(opts.MainNameAfterMock); + if (!userMainFn) { + klee_error("Mock: Entry function '%s' not found in module", + opts.MainNameAfterMock.c_str()); + } + mockModule->getOrInsertFunction(opts.MainCurrentName, + userMainFn->getFunctionType(), + userMainFn->getAttributes()); + llvm::Function *mockMainFn = mockModule->getFunction(opts.MainCurrentName); + if (!mockMainFn) { + klee_error("Mock: Entry function '%s' not found in module", + opts.MainCurrentName.c_str()); + } + auto globalsInitBlock = + llvm::BasicBlock::Create(mockModule->getContext(), "entry", mockMainFn); + builder->SetInsertPoint(globalsInitBlock); + // Define all the external globals + buildExternalGlobalsDefinitions(); + + auto userMainCallee = mockModule->getOrInsertFunction( + opts.MainNameAfterMock, userMainFn->getFunctionType()); + std::vector args; + args.reserve(userMainFn->arg_size()); + for (auto it = mockMainFn->arg_begin(); it != mockMainFn->arg_end(); it++) { + args.push_back(it); + } + auto callUserMain = builder->CreateCall(userMainCallee, args); + builder->CreateRet(callUserMain); +} + +void MockBuilder::buildExternalGlobalsDefinitions() { + auto externalGlobals = getExternalGlobals(); + for (const auto &[extName, type] : externalGlobals) { + mockModule->getOrInsertGlobal(extName, type); + auto *global = mockModule->getGlobalVariable(extName); + if (!global) { + klee_error("Mock: Unable to add global variable '%s' to module", + extName.c_str()); + } + global->setLinkage(llvm::GlobalValue::ExternalLinkage); + if (!type->isSized()) { + continue; + } + + auto *zeroInitializer = llvm::Constant::getNullValue(type); + if (!zeroInitializer) { + klee_error("Mock: Unable to get zero initializer for '%s'", + extName.c_str()); + } + global->setInitializer(zeroInitializer); + buildCallKleeMakeSymbolic("klee_make_symbolic", global, type, + "external_" + extName); + } +} + +void MockBuilder::buildExternalFunctionsDefinitions() { + 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(); + } + } + } + } + + for (const auto &[extName, type] : externalFunctions) { + mockModule->getOrInsertFunction(extName, type); + llvm::Function *func = mockModule->getFunction(extName); + if (!func) { + klee_error("Mock: Unable to find function '%s' in module", + extName.c_str()); + } + if (!func->empty()) { + continue; + } + auto *BB = + llvm::BasicBlock::Create(mockModule->getContext(), "entry", func); + builder->SetInsertPoint(BB); + + const auto nameToAnnotations = annotations.find(extName); + if (nameToAnnotations != annotations.end()) { + klee_message("Annotation function %s", extName.c_str()); + const auto &annotation = nameToAnnotations->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); + // } + + 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::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 kleeMakeSymbolicCallee = mockModule->getOrInsertFunction( + kleeMakeSymbolicFunctionName, kleeMakeSymbolicName); + auto bitCastInst = builder->CreateBitCast( + source, llvm::Type::getInt8PtrTy(mockModule->getContext())); + auto globalSymbolicName = builder->CreateGlobalString("@" + symbolicName); + auto gep = builder->CreateConstInBoundsGEP2_64( + globalSymbolicName->getValueType(), globalSymbolicName, 0, 0); + builder->CreateCall( + kleeMakeSymbolicCallee, + {bitCastInst, + llvm::ConstantInt::get( + mockModule->getContext(), + llvm::APInt(64, mockModule->getDataLayout().getTypeStoreSize(type), + false)), + gep}); +} + +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."); + } + 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())) { + klee_error("Incorrect annotation offset."); + } + 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::Free *freePtr = 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::Free: { + if (elem->getType()->isPointerTy()) { + freePtr = (Statement::Free *)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; + } + } + if (freePtr) { + buildFree(elem, freePtr); + } + 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::buildFree(llvm::Value *elem, const Statement::Free *freePtr) { + if (freePtr->value != Statement::Free::Free_) { + klee_warning("Annotation: AllocSource \"%d\" not implemented use free", + freePtr->value); + } + auto freeInstr = llvm::CallInst::CreateFree(elem, builder->GetInsertBlock()); + builder->Insert(freeInstr); +} + +void MockBuilder::buildAnnotationForExternalFunctionReturn( + llvm::Function *func, const std::vector &statements) { + auto returnType = func->getReturnType(); + if (!returnType->isSized()) { // void return type + builder->CreateRet(nullptr); + return; + } + + // TODO: change to set + 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::Free: { + klee_warning("Annotation: unused \"Free\" for return"); + 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 a9d7457a88..647014cf96 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -112,6 +112,7 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = { #endif add("klee_is_symbolic", handleIsSymbolic, true), add("klee_make_symbolic", handleMakeSymbolic, false), + add("klee_make_mock", handleMakeMock, false), add("klee_mark_global", handleMarkGlobal, false), add("klee_prefer_cex", handlePreferCex, false), add("klee_posix_prefer_cex", handlePosixPreferCex, false), @@ -937,6 +938,87 @@ void SpecialFunctionHandler::handleMakeSymbolic( } } +void SpecialFunctionHandler::handleMakeMock(ExecutionState &state, + KInstruction *target, + std::vector> &arguments) { + std::string name; + + if (arguments.size() != 3) { + executor.terminateStateOnUserError(state, + "Incorrect number of arguments to " + "klee_make_mock(void*, size_t, char*)"); + return; + } + + name = arguments[2]->isZero() ? "" : readStringAtAddress(state, arguments[2]); + + if (name.length() == 0) { + executor.terminateStateOnUserError( + state, "Empty name of function in klee_make_mock"); + return; + } + + 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->getNumArgs()); + for (size_t i = 0; i < kf->getNumArgs(); 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( ExecutionState &state, KInstruction *target, std::vector> &arguments) { diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h index 78f920450e..6528b98c36 100644 --- a/lib/Core/SpecialFunctionHandler.h +++ b/lib/Core/SpecialFunctionHandler.h @@ -127,6 +127,7 @@ class SpecialFunctionHandler { HANDLER(handleGetValue); HANDLER(handleIsSymbolic); HANDLER(handleMakeSymbolic); + HANDLER(handleMakeMock); HANDLER(handleMalloc); HANDLER(handleMemalign); HANDLER(handleMarkGlobal); diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp index 165b438025..b863d22cc4 100644 --- a/lib/Expr/ExprPPrinter.cpp +++ b/lib/Expr/ExprPPrinter.cpp @@ -413,6 +413,18 @@ class PPrinter : public ExprPPrinter { << kf->getName().str() << " " << s->index; } else if (auto s = dyn_cast(source)) { PC << s->name; + } else if (auto s = dyn_cast(source)) { + PC << s->km->functionMap.at(&s->function)->getName() << ' ' << s->version; + } else if (auto s = dyn_cast(source)) { + PC << s->km->functionMap.at(&s->function)->getName() << ' '; + PC << "("; + for (unsigned i = 0; i < s->args.size(); i++) { + print(s->args[i], PC); + if (i != s->args.size() - 1) { + PC << " "; + } + } + PC << ')'; } else { assert(0 && "Not implemented"); } diff --git a/lib/Expr/ExprUtil.cpp b/lib/Expr/ExprUtil.cpp index 87bed5d731..518e922dc8 100644 --- a/lib/Expr/ExprUtil.cpp +++ b/lib/Expr/ExprUtil.cpp @@ -54,6 +54,16 @@ void klee::findReads(ref e, bool visitUpdates, cast(re->updates.root->source)->pointer); } + if (ref mockSource = + dyn_cast_or_null( + re->updates.root->source)) { + for (auto arg : mockSource->args) { + if (visited.insert(arg).second) { + stack.push_back(arg); + } + } + } + if (visitUpdates) { // XXX this is probably suboptimal. We want to avoid a potential // explosion traversing update lists which can be quite diff --git a/lib/Expr/IndependentSet.cpp b/lib/Expr/IndependentSet.cpp index 3acca539c9..36f18feda9 100644 --- a/lib/Expr/IndependentSet.cpp +++ b/lib/Expr/IndependentSet.cpp @@ -7,6 +7,7 @@ #include "klee/Expr/ExprUtil.h" #include "klee/Expr/SymbolicSource.h" #include "klee/Expr/Symcrete.h" +#include "klee/Module/KModule.h" #include "klee/Solver/Solver.h" #include @@ -132,6 +133,11 @@ void IndependentConstraintSet::initIndependentConstraintSet(ref e) { if (re->updates.root->isConstantArray() && !re->updates.head) continue; + if (ref mockSource = + dyn_cast_or_null(array->source)) { + uninterpretedFunctions.insert(mockSource->function.getName().str()); + } + if (!wholeObjects.count(array)) { if (ConstantExpr *CE = dyn_cast(re->index)) { // if index constant, then add to set of constraints operating @@ -210,7 +216,8 @@ IndependentConstraintSet::IndependentConstraintSet( const IndependentConstraintSet &ics) : elements(ics.elements), wholeObjects(ics.wholeObjects), exprs(ics.exprs), symcretes(ics.symcretes), concretization(ics.concretization), - concretizedSets(ics.concretizedSets) {} + concretizedSets(ics.concretizedSets), + uninterpretedFunctions(ics.uninterpretedFunctions) {} void IndependentConstraintSet::print(llvm::raw_ostream &os) const { os << "{"; @@ -274,6 +281,13 @@ bool IndependentConstraintSet::intersects( } } } + for (std::set::iterator it = a->uninterpretedFunctions.begin(), + ie = a->uninterpretedFunctions.end(); + it != ie; ++it) { + if (b->uninterpretedFunctions.count(*it)) { + return true; + } + } // No need to check symcretes here, arrays must be sufficient. return false; } diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index b072cec826..eab66bd1ae 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -330,6 +330,8 @@ class ParserImpl : public Parser { SourceResult ParseLazyInitializationSizeSource(); SourceResult ParseInstructionSource(); SourceResult ParseArgumentSource(); + SourceResult ParseMockNaiveSource(); + SourceResult ParseMockDeterministicSource(); /*** Diagnostics ***/ @@ -501,6 +503,12 @@ SourceResult ParserImpl::ParseSource() { } else if (type == "argument") { assert(km); source = ParseArgumentSource(); + } else if (type == "mockNaive") { + assert(km); + source = ParseMockNaiveSource(); + } else if (type == "mockDeterministic") { + assert(km); + source = ParseMockDeterministicSource(); } else { assert(0); } @@ -599,6 +607,34 @@ SourceResult ParserImpl::ParseInstructionSource() { return SourceBuilder::instruction(*KI->inst, index, km); } +SourceResult ParserImpl::ParseMockNaiveSource() { + auto name = Tok.getString(); + auto kf = km->functionNameMap[name]; + ConsumeExpectedToken(Token::Identifier); + auto versionExpr = ParseNumber(64).get(); + auto version = dyn_cast(versionExpr); + assert(version); + return SourceBuilder::mockNaive(km, *kf->function, version->getZExtValue()); +} + +SourceResult ParserImpl::ParseMockDeterministicSource() { + auto name = Tok.getString(); + auto kf = km->functionNameMap[name]; + ConsumeExpectedToken(Token::Identifier); + ConsumeLParen(); + std::vector> args; + args.reserve(kf->getNumArgs()); + for (unsigned i = 0; i < kf->getNumArgs(); i++) { + auto expr = ParseExpr(TypeResult()); + if (!expr.isValid()) { + return {false, nullptr}; + } + args.push_back(expr.get()); + } + ConsumeRParen(); + return SourceBuilder::mockDeterministic(km, *kf->function, args); +} + /// ParseCommandDecl - Parse a command declaration. The lexer should /// be positioned at the opening '('. /// diff --git a/lib/Expr/SourceBuilder.cpp b/lib/Expr/SourceBuilder.cpp index a667a19ba2..c40ce3dccd 100644 --- a/lib/Expr/SourceBuilder.cpp +++ b/lib/Expr/SourceBuilder.cpp @@ -86,4 +86,21 @@ ref SourceBuilder::irreproducible(const std::string &name) { ref r(new IrreproducibleSource(name + llvm::utostr(++id))); r->computeHash(); return r; -} \ No newline at end of file +} + +ref SourceBuilder::mockNaive(const KModule *km, + const llvm::Function &function, + unsigned int version) { + ref r(new MockNaiveSource(km, function, version)); + r->computeHash(); + return r; +} + +ref +SourceBuilder::mockDeterministic(const KModule *km, + const llvm::Function &function, + const std::vector> &args) { + ref r(new MockDeterministicSource(km, function, args)); + r->computeHash(); + return r; +} diff --git a/lib/Expr/SymbolicSource.cpp b/lib/Expr/SymbolicSource.cpp index 9d8d3b6e58..9d5261342a 100644 --- a/lib/Expr/SymbolicSource.cpp +++ b/lib/Expr/SymbolicSource.cpp @@ -1,6 +1,6 @@ #include "klee/Expr/SymbolicSource.h" - #include "klee/Expr/Expr.h" + #include "klee/Expr/ExprPPrinter.h" #include "klee/Expr/ExprUtil.h" #include "klee/Module/KInstruction.h" @@ -162,4 +162,65 @@ unsigned InstructionSource::computeHash() { return hashValue; } +unsigned MockNaiveSource::computeHash() { + unsigned res = (getKind() * SymbolicSource::MAGIC_HASH_CONSTANT) + version; + unsigned funcID = km->getFunctionId(&function); + res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + funcID; + hashValue = res; + return res; +} + +int MockNaiveSource::internalCompare(const SymbolicSource &b) const { + if (getKind() != b.getKind()) { + return getKind() < b.getKind() ? -1 : 1; + } + const MockNaiveSource &mnb = static_cast(b); + if (version != mnb.version) { + return version < mnb.version ? -1 : 1; + } + unsigned funcID = km->getFunctionId(&function); + unsigned bFuncID = mnb.km->getFunctionId(&mnb.function); + if (funcID != bFuncID) { + return funcID < bFuncID ? -1 : 1; + } + return 0; +} + +MockDeterministicSource::MockDeterministicSource( + const KModule *km, const llvm::Function &function, + const std::vector> &_args) + : MockSource(km, function), args(_args) {} + +unsigned MockDeterministicSource::computeHash() { + unsigned res = getKind(); + res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + + km->getFunctionId(&function); + for (const auto &arg : args) { + res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + arg->hash(); + } + hashValue = res; + return res; +} + +int MockDeterministicSource::internalCompare(const SymbolicSource &b) const { + if (getKind() != b.getKind()) { + return getKind() < b.getKind() ? -1 : 1; + } + const MockDeterministicSource &mdb = + static_cast(b); + unsigned funcID = km->getFunctionId(&function); + unsigned bFuncID = mdb.km->getFunctionId(&mdb.function); + if (funcID != bFuncID) { + return funcID < bFuncID ? -1 : 1; + } + assert(args.size() == mdb.args.size() && + "the same functions should have the same arguments number"); + for (unsigned i = 0; i < args.size(); i++) { + if (args[i] != mdb.args[i]) { + return args[i] < mdb.args[i] ? -1 : 1; + } + } + return 0; +} + } // namespace klee diff --git a/lib/Module/Annotation.cpp b/lib/Module/Annotation.cpp new file mode 100644 index 0000000000..01ea95e54f --- /dev/null +++ b/lib/Module/Annotation.cpp @@ -0,0 +1,377 @@ +#include "klee/Module/Annotation.h" + +#include "klee/Support/ErrorHandling.h" + +#include +#include +#include + +#ifdef ENABLE_XML_ANNOTATION +#include "pugixml.hpp" +#endif + +namespace klee { + +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; +} + +namespace Statement { + +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; + + 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); + } + } + + for (size_t pos = 0; pos < rawOffset.size(); pos++) { + switch (rawOffset[pos]) { + case '*': { + offset.emplace_back("*"); + break; + } + case '&': { + offset.emplace_back("&"); + break; + } + case '[': { + size_t posEndExpr = rawOffset.find(']', pos); + if (posEndExpr == std::string::npos) { + klee_error("Annotation: Incorrect offset format \"%s\"", str.c_str()); + } + 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 { + return rawAnnotation + ":" + rawOffset; + } + } + return rawAnnotation + ":" + rawOffset + ":" + rawValue; +} + +bool Unknown::operator==(const Unknown &other) const { + if (this->getKind() == other.getKind()) { + return toString() == other.toString(); + } + return false; +} + +/* + * 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) {} + +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)); + } +} + +Kind AllocSource::getKind() const { return Kind::AllocSource; } + +Free::Free(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 = Free::Type::Free_; + } else { + value = static_cast(std::stoi(rawValue)); + } +} + +Kind Free::getKind() const { return Kind::Free; } + +const std::map StringToKindMap = { + {"deref", Statement::Kind::Deref}, + {"initnull", Statement::Kind::InitNull}, + {"allocsource", Statement::Kind::AllocSource}, + {"freesource", Statement::Kind::Free}, + {"freesink", Statement::Kind::Free}}; + +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; +} + +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); + case Statement::Kind::Free: + return std::make_shared(str); + } +} + +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("Annotation: Incorrect statement format"); + } + const std::string jStr = j.get(); + statement = Statement::stringToKindPtr(jStr); +} + +void from_json(const json &j, Property &property) { + if (!j.is_string()) { + klee_error("Annotation: Incorrect properties format"); + } + const std::string jStr = j.get(); + + property = Statement::Property::Unknown; + const auto propertyPtr = Statement::StringToPropertyMap.find(jStr); + if (propertyPtr != Statement::StringToPropertyMap.end()) { + property = propertyPtr->second; + } +} + +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(); + + const json &j = item.value(); + if (!j.is_object() || !j.contains("annotation") || + !j.contains("properties")) { + 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.properties = + j.at("properties").get>(); + annotations[item.key()] = annotation; + } + return annotations; +} + +#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; +} + +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; +} + +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 + +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()); + } + + return parseAnnotationsJson(annotationsJson); + } +} + +} // namespace klee diff --git a/lib/Module/CMakeLists.txt b/lib/Module/CMakeLists.txt index 42ef35556b..d6abe7b4c6 100644 --- a/lib/Module/CMakeLists.txt +++ b/lib/Module/CMakeLists.txt @@ -7,6 +7,7 @@ # #===------------------------------------------------------------------------===# set(KLEE_MODULE_COMPONENT_SRCS + Annotation.cpp CallSplitter.cpp Checks.cpp CodeGraphInfo.cpp @@ -30,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 e80feae88c..261d8092c9 100644 --- a/lib/Solver/Z3Builder.cpp +++ b/lib/Solver/Z3Builder.cpp @@ -13,6 +13,7 @@ #include "klee/ADT/Bits.h" #include "klee/Expr/Expr.h" #include "klee/Expr/SymbolicSource.h" +#include "klee/Module/KModule.h" #include "klee/Solver/Solver.h" #include "klee/Solver/SolverStats.h" #include "klee/Support/ErrorHandling.h" @@ -257,6 +258,37 @@ Z3ASTHandle Z3Builder::getInitialArray(const Array *root) { array_expr = buildConstantArray(unique_name.c_str(), root->getDomain(), root->getRange(), symbolicSizeConstantSource->defaultValue); + } else if (ref mockDeterministicSource = + dyn_cast(root->source)) { + size_t num_args = mockDeterministicSource->args.size(); + std::vector argsHandled(num_args); + std::vector argsSortHandled(num_args); + std::vector args(num_args); + std::vector argsSort(num_args); + for (size_t i = 0; i < num_args; i++) { + ref kid = mockDeterministicSource->args[i]; + int kidWidth = kid->getWidth(); + argsHandled[i] = construct(kid, &kidWidth); + args[i] = argsHandled[i]; + argsSortHandled[i] = Z3SortHandle(Z3_get_sort(ctx, args[i]), ctx); + argsSort[i] = argsSortHandled[i]; + } + + Z3SortHandle domainSort = getBvSort(root->getDomain()); + Z3SortHandle rangeSort = getBvSort(root->getRange()); + Z3SortHandle retValSort = getArraySort(domainSort, rangeSort); + + Z3FuncDeclHandle func; + func = Z3FuncDeclHandle( + Z3_mk_func_decl( + ctx, + Z3_mk_string_symbol( + ctx, + mockDeterministicSource->function.getName().str().c_str()), + num_args, argsSort.data(), retValSort), + ctx); + array_expr = + Z3ASTHandle(Z3_mk_app(ctx, func, num_args, args.data()), ctx); } else { array_expr = buildArray(unique_name.c_str(), root->getDomain(), root->getRange()); diff --git a/lib/Solver/Z3Builder.h b/lib/Solver/Z3Builder.h index 7b407c6e3d..e6d10fed10 100644 --- a/lib/Solver/Z3Builder.h +++ b/lib/Solver/Z3Builder.h @@ -91,6 +91,13 @@ typedef Z3NodeHandle Z3SortHandle; template <> void Z3NodeHandle::dump() const __attribute__((used)); template <> unsigned Z3NodeHandle::hash() __attribute__((used)); +// Specialize for Z3_func_decl +template <> inline ::Z3_ast Z3NodeHandle::as_ast() const { + return ::Z3_func_decl_to_ast(context, node); +} +typedef Z3NodeHandle Z3FuncDeclHandle; +template <> void Z3NodeHandle::dump() const __attribute__((used)); + // Specialise for Z3_ast template <> inline ::Z3_ast Z3NodeHandle::as_ast() const { return node; diff --git a/runtime/CMakeLists.txt b/runtime/CMakeLists.txt index ada82c0f33..d1c8a17d2f 100644 --- a/runtime/CMakeLists.txt +++ b/runtime/CMakeLists.txt @@ -90,12 +90,14 @@ add_subdirectory(Freestanding) add_subdirectory(Intrinsic) add_subdirectory(klee-libc) add_subdirectory(Fortify) +add_subdirectory(Mocks) set(RUNTIME_LIBRARIES RuntimeFreestanding RuntimeIntrinsic RuntimeKLEELibc RuntimeFortify + RuntimeMocks ) if (ENABLE_KLEE_EH_CXX) diff --git a/runtime/Mocks/CMakeLists.txt b/runtime/Mocks/CMakeLists.txt new file mode 100644 index 0000000000..efd6497470 --- /dev/null +++ b/runtime/Mocks/CMakeLists.txt @@ -0,0 +1,19 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# + +set(LIB_PREFIX "RuntimeMocks") +set(SRC_FILES + models.c + ) + +# Build it +include("${CMAKE_SOURCE_DIR}/cmake/compile_bitcode_library.cmake") +prefix_with_path("${SRC_FILES}" "${CMAKE_CURRENT_SOURCE_DIR}/" runtime_mocks_files) + +add_bitcode_library_targets("${LIB_PREFIX}" "${runtime_mocks_files}" "" "") diff --git a/runtime/Mocks/models.c b/runtime/Mocks/models.c new file mode 100644 index 0000000000..a389ad5a34 --- /dev/null +++ b/runtime/Mocks/models.c @@ -0,0 +1,36 @@ +#include "stddef.h" + +extern void klee_make_symbolic(void *array, size_t nbytes, const char *name); +extern void *malloc(size_t size); +extern void *calloc(size_t num, size_t size); +extern void *realloc(void *ptr, size_t new_size); + +void *__klee_wrapped_malloc(size_t size) { + unsigned char retNull; + klee_make_symbolic(&retNull, sizeof(retNull), "retNullMalloc"); + if (retNull) { + return 0; + } + void *array = malloc(size); + return array; +} + +void *__klee_wrapped_calloc(size_t num, size_t size) { + unsigned char retNull; + klee_make_symbolic(&retNull, sizeof(retNull), "retNullCalloc"); + if (retNull) { + return 0; + } + void *array = calloc(num, size); + return array; +} + +void *__klee_wrapped_realloc(void *ptr, size_t new_size) { + unsigned char retNull; + klee_make_symbolic(&retNull, sizeof(retNull), "retNullRealloc"); + if (retNull) { + return 0; + } + void *array = realloc(ptr, new_size); + return array; +} diff --git a/runtime/Runtest/CMakeLists.txt b/runtime/Runtest/CMakeLists.txt index df5f2c23be..33d190a262 100644 --- a/runtime/Runtest/CMakeLists.txt +++ b/runtime/Runtest/CMakeLists.txt @@ -9,6 +9,8 @@ add_library(kleeRuntest SHARED intrinsics.c + # Mocks: + ${CMAKE_SOURCE_DIR}/runtime/Mocks/models.c # HACK: ${CMAKE_SOURCE_DIR}/lib/Basic/KTest.cpp ) diff --git a/runtime/Runtest/intrinsics.c b/runtime/Runtest/intrinsics.c index 34a9e9d2c8..3e6bdd8efd 100644 --- a/runtime/Runtest/intrinsics.c +++ b/runtime/Runtest/intrinsics.c @@ -72,8 +72,7 @@ void recursively_allocate(KTestObject *obj, size_t index, void *addr, return; } -void klee_make_symbolic(void *array, size_t nbytes, const char *name) { - +static void klee_make_symbol(void *array, size_t nbytes, const char *name) { if (!name) name = "unnamed"; @@ -154,6 +153,14 @@ void klee_make_symbolic(void *array, size_t nbytes, const char *name) { } } +void klee_make_symbolic(void *array, size_t nbytes, const char *name) { + klee_make_symbol(array, nbytes, name); +} + +void klee_make_mock(void *ret_array, size_t ret_nbytes, const char *fname) { + klee_make_symbol(ret_array, ret_nbytes, fname); +} + void klee_silent_exit(int x) { exit(x); } uintptr_t klee_choose(uintptr_t n) { diff --git a/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/scripts/run_tests_with_mocks.py b/scripts/run_tests_with_mocks.py new file mode 100755 index 0000000000..5843a37ad0 --- /dev/null +++ b/scripts/run_tests_with_mocks.py @@ -0,0 +1,26 @@ +#!/usr/bin/env python3 + +# This script builds executable file using initial bitcode file and artifacts produced by KLEE. +# To run the script provide all the arguments you want to pass to clang for building executable. +# +# NOTE: Pre-last argument should be a path to KLEE output directory which contains redefinitions.txt and externals.ll. +# NOTE: Last argument is path to initial bitcode. +# +# Example: python3 run_tests_with_mocks.py -I ~/klee/include/ -L ~/klee/build/lib/ -lkleeRuntest klee-last a.bc +# +# You can read more about replaying test cases here: http://klee.github.io/tutorials/testing-function/ + +import subprocess as sp +import sys +import os + +klee_out_dir = sys.argv[-2] +bitcode = sys.argv[-1] + +filename = os.path.splitext(bitcode)[0] +object_file = f'{filename}.o' +sp.run(f'clang -c {bitcode} -o {object_file}', shell=True) +sp.run(f'llvm-objcopy {object_file} --redefine-syms {klee_out_dir}/redefinitions.txt', shell=True) +clang_args = ' '.join(sys.argv[1:len(sys.argv) - 2]) +print(f'clang {clang_args} {klee_out_dir}/externals.ll {object_file}') +sp.run(f'clang {clang_args} {klee_out_dir}/externals.ll {object_file}', shell=True) diff --git a/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/Free.c b/test/Feature/Annotation/Free.c new file mode 100644 index 0000000000..fb364a8264 --- /dev/null +++ b/test/Feature/Annotation/Free.c @@ -0,0 +1,45 @@ +// REQUIRES: z3 +// RUN: %clang -DFree1 %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/Free.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-FREE1 + +// 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/Free.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-FREE2 + +// RUN: %clang -DFree3 %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/Free.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-FREE3 + +#include + +int *maybeAllocSource1(); +void maybeFree1(int *a); + +int main() { + int *a; +#ifdef Free1 + // CHECK-FREE1: memory error: invalid pointer: free + // CHECK-FREE1: KLEE: done: completed paths = 1 + // CHECK-FREE1: KLEE: done: partially completed paths = 1 + // CHECK-FREE1: KLEE: done: generated tests = 2 + a = malloc(sizeof(int)); + maybeFree1(a); + maybeFree1(a); +#endif + + a = maybeAllocSource1(); + maybeFree1(a); + // CHECK-NOT-FREE2: memory error: invalid pointer: free + // CHECK-FREE2: KLEE: done: completed paths = 1 + // CHECK-FREE2: KLEE: done: partially completed paths = 0 + // CHECK-FREE2: KLEE: done: generated tests = 1 +#ifdef Free3 + // CHECK-FREE3: memory error: invalid pointer: free + // CHECK-FREE3: KLEE: done: completed paths = 0 + // CHECK-FREE3: KLEE: done: partially completed paths = 1 + // CHECK-FREE3: KLEE: done: generated tests = 1 + maybeFree1(a); +#endif + return 0; +} diff --git a/test/Feature/Annotation/Free.json b/test/Feature/Annotation/Free.json new file mode 100644 index 0000000000..d8a9becf9d --- /dev/null +++ b/test/Feature/Annotation/Free.json @@ -0,0 +1,31 @@ +{ + "maybeFree1": { + "name": "maybeFree1", + "annotation": [ + [], + [ + "FreeSink::1" + ] + ], + "properties": [] + }, + "maybeFree2": { + "name": "maybeFree2", + "annotation": [ + [], + [ + "FreeSink:*:1" + ] + ], + "properties": [] + }, + "maybeAllocSource1": { + "name": "maybeAllocSource1", + "annotation": [ + [ + "AllocSource::1" + ] + ], + "properties": [] + } +} 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 new file mode 100644 index 0000000000..7788138852 --- /dev/null +++ b/test/Feature/MockPointersDeterministic.c @@ -0,0 +1,24 @@ +// REQUIRES: z3 +// RUN: %clang %s -g -emit-llvm %O0opt -c -o %t.bc + +// RUN: rm -rf %t.klee-out-1 +// RUN: %klee --solver-backend=z3 --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 + +#include + +extern int *age(); + +int main() { + if (age() != age()) { + assert(0 && "age is deterministic"); + } + if (*age() != *age()) { + assert(0 && "age is deterministic"); + } + return *age(); +} diff --git a/test/Feature/MockStrategies.c b/test/Feature/MockStrategies.c new file mode 100644 index 0000000000..524fbba3a2 --- /dev/null +++ b/test/Feature/MockStrategies.c @@ -0,0 +1,37 @@ +// REQUIRES: z3 +// RUN: %clang %s -g -emit-llvm %O0opt -c -o %t.bc + +// RUN: rm -rf %t.klee-out-1 +// RUN: %klee --output-dir=%t.klee-out-1 --external-calls=all --mock-strategy=none %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-1 +// CHECK-1: failed external call +// CHECK-1: KLEE: done: completed paths = 1 +// CHECK-1: KLEE: done: generated tests = 2 + +// RUN: rm -rf %t.klee-out-2 +// RUN: %klee --output-dir=%t.klee-out-2 --external-calls=all --mock-strategy=naive %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-2 +// CHECK-2: ASSERTION FAIL: 0 +// CHECK-2: KLEE: done: completed paths = 2 +// CHECK-2: KLEE: done: generated tests = 3 + +// RUN: rm -rf %t.klee-out-3 +// RUN: not %klee --output-dir=%t.klee-out-3 --solver-backend=stp --external-calls=all --mock-strategy=deterministic %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-3 +// CHECK-3: KLEE: ERROR: Deterministic mocks can be generated with Z3 solver only. + +// RUN: rm -rf %t.klee-out-4 +// RUN: %klee --output-dir=%t.klee-out-4 --solver-backend=z3 --external-calls=all --mock-strategy=deterministic %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-4 +// CHECK-4: KLEE: done: completed paths = 2 +// CHECK-4: KLEE: done: generated tests = 2 + +#include + +extern int foo(int x, int y); + +int main() { + int a, b; + klee_make_symbolic(&a, sizeof(a), "a"); + klee_make_symbolic(&b, sizeof(b), "b"); + if (a == b && foo(a + b, b) != foo(2 * b, a)) { + assert(0); + } + return 0; +} diff --git a/test/Replay/libkleeruntest/replay_mocks.c b/test/Replay/libkleeruntest/replay_mocks.c new file mode 100644 index 0000000000..bb9c9e7691 --- /dev/null +++ b/test/Replay/libkleeruntest/replay_mocks.c @@ -0,0 +1,21 @@ +// 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: %llc %t.klee-out/externals.ll -filetype=obj -o %t_externals.o +// RUN: %objcopy --redefine-syms %t.klee-out/redefinitions.txt %t.o +// RUN: %cc -no-pie %t_externals.o %t.o %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner +// RUN: test -f %t.klee-out/test000001.ktest +// RUN: env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner + +extern int variable; + +extern int foo(int); + +int main() { + int a; + klee_make_symbolic(&a, sizeof(a), "a"); + return variable + foo(a); +} diff --git a/test/lit.cfg b/test/lit.cfg index 75978e47b7..83d7a0f2a3 100644 --- a/test/lit.cfg +++ b/test/lit.cfg @@ -90,17 +90,27 @@ 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: lit_config.fatal('{0} is not set'.format(name)) config.substitutions.append( ('%' + name, value)) +config.substitutions.append( + ('%runmocks', os.path.join(klee_src_root, 'scripts/run_tests_with_mocks.py')) +) + # Add a substitution for lli. config.substitutions.append( ('%lli', os.path.join(llvm_tools_dir, 'lli')) ) + +# 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')) @@ -114,6 +124,11 @@ config.substitutions.append( ('%llvmlink', os.path.join(llvm_tools_dir, 'llvm-link')) ) +# Add a substitution for llvm-objcopy +config.substitutions.append( + ('%llvmobjcopy', os.path.join(llvm_tools_dir, 'llvm-objcopy')) +) + # Add a substition for libkleeruntest config.substitutions.append( ('%libkleeruntestdir', os.path.dirname(config.libkleeruntest)) 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 364254f278..9dc526dfa8 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -364,6 +364,45 @@ cl::opt XMLMetadataProgramHash( llvm::cl::desc("Test-Comp hash sum of original file for xml metadata"), llvm::cl::cat(TestCompCat)); +/*** Mocking options ***/ + +cl::OptionCategory MockCat("Mock category"); + +cl::opt MockLinkedExternals( + "mock-linked-externals", + cl::desc("Mock modelled linked externals (default=false)"), cl::init(false), + cl::cat(MockCat)); + +cl::opt MockUnlinkedStrategy( + "mock-strategy", cl::init(MockStrategy::None), + cl::desc("Specify strategy for mocking external calls"), + cl::values( + clEnumValN(MockStrategy::None, "none", + "External calls are not mocked (default)"), + clEnumValN(MockStrategy::Naive, "naive", + "Every time external function is called, new symbolic value " + "is generated for its return value"), + clEnumValN( + MockStrategy::Deterministic, "deterministic", + "NOTE: this option is compatible with Z3 solver only. Each " + "external function is treated as a deterministic " + "function. Therefore, when function is called many times " + "with equal arguments, every time equal values will be returned.")), + cl::init(MockStrategy::None), cl::cat(MockCat)); + +/*** Annotations options ***/ + +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::opt AnnotateOnlyExternal( + "annotate-only-external", + cl::desc("Ignore annotations for defined function (default=false)"), + cl::init(false), cl::cat(AnnotCat)); + } // namespace namespace klee { @@ -851,7 +890,7 @@ std::string KleeHandler::getRunTimeLibraryPath(const char *argv0) { void KleeHandler::setOutputDirectory(const std::string &directoryName) { // create output directory - if (directoryName == "") { + if (directoryName.empty()) { klee_error("Empty name of new directory"); } SmallString<128> directory(directoryName); @@ -956,7 +995,8 @@ static const char *modelledExternals[] = { "klee_check_memory_access", "klee_define_fixed_object", "klee_get_errno", "klee_get_valuef", "klee_get_valued", "klee_get_valuel", "klee_get_valuell", "klee_get_value_i32", "klee_get_value_i64", "klee_get_obj_size", - "klee_is_symbolic", "klee_make_symbolic", "klee_mark_global", + "klee_is_symbolic", "klee_make_symbolic", "klee_make_mock", + "klee_mark_global", "klee_open_merge", "klee_close_merge", "klee_prefer_cex", "klee_posix_prefer_cex", "klee_print_expr", "klee_print_range", "klee_report_error", "klee_set_forking", "klee_silent_exit", "klee_warning", "klee_warning_once", "klee_stack_trace", @@ -1050,12 +1090,14 @@ static const char *dontCareExternals[] = { "getwd", "gettimeofday", "uname", + "ioctl", // fp stuff we just don't worry about yet "frexp", "ldexp", "__isnan", "__signbit", + "llvm.dbg.label", }; // Extra symbols we aren't going to warn about with klee-libc @@ -1579,6 +1621,37 @@ void wait_until_any_child_dies( } } +void mockLinkedExternals( + const Interpreter::ModuleOptions &Opts, llvm::LLVMContext &ctx, + llvm::Module *mainModule, + std::vector> &loadedLibsModules, + 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, loadedLibsModules, + errorMsg)) { + klee_error("error loading mocks model '%s': %s", Path.c_str(), + errorMsg.c_str()); + } + + 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()); + redefinitions.emplace_back(f->getName(), fmodel.getName()); + f->setName(fmodel.getName()); + } + } +} + int main(int argc, char **argv, char **envp) { if (theInterpreter) { theInterpreter = nullptr; @@ -1671,9 +1744,10 @@ int main(int argc, char **argv, char **envp) { sys::SetInterruptFunction(interrupt_handle); - // Load the bytecode... std::string errorMsg; LLVMContext ctx; + + // Load the bytecode... std::vector> loadedUserModules; std::vector> loadedLibsModules; if (!klee::loadFileAsOneModule(InputFile, ctx, loadedUserModules, errorMsg)) { @@ -1739,7 +1813,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()); - // Detect architecture std::string bit_suffix = "64"; // Fall back to 64bit if (module_triple.find("i686") != std::string::npos || @@ -1757,13 +1830,18 @@ int main(int argc, char **argv, char **envp) { } std::string LibraryDir = KleeHandler::getRunTimeLibraryPath(argv[0]); - Interpreter::ModuleOptions Opts(LibraryDir.c_str(), EntryPoint, opt_suffix, - /*Optimize=*/OptimizeModule, - /*Simplify*/ SimplifyModule, - /*CheckDivZero=*/CheckDivZero, - /*CheckOvershift=*/CheckOvershift, - /*WithFPRuntime=*/WithFPRuntime, - /*WithPOSIXRuntime=*/WithPOSIXRuntime); + Interpreter::ModuleOptions Opts( + LibraryDir, 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); // Get the main function for (auto &module : loadedUserModules) { @@ -1785,6 +1863,15 @@ int main(int argc, char **argv, char **envp) { if (!entryFn) klee_error("Entry function '%s' not found in module.", EntryPoint.c_str()); + std::vector> redefinitions; + if (MockLinkedExternals) { + mockLinkedExternals(Opts, ctx, mainModule, loadedLibsModules, + redefinitions); + } + if (MockUnlinkedStrategy != MockStrategy::None) { + redefinitions.emplace_back(EntryPoint, Opts.MainNameAfterMock); + } + if (WithPOSIXRuntime) { SmallString<128> Path(Opts.LibraryDir); llvm::sys::path::append(Path, "libkleeRuntimePOSIX" + opt_suffix + ".bca"); @@ -1953,6 +2040,7 @@ int main(int argc, char **argv, char **envp) { Interpreter::InterpreterOptions IOpts(paths); IOpts.MakeConcreteSymbolic = MakeConcreteSymbolic; IOpts.Guidance = UseGuidedSearch; + IOpts.MockStrategy = MockUnlinkedStrategy; std::unique_ptr interpreter( Interpreter::create(ctx, IOpts, handler.get())); theInterpreter = interpreter.get(); @@ -1964,13 +2052,39 @@ int main(int argc, char **argv, char **envp) { } handler->getInfoStream() << "PID: " << getpid() << "\n"; + std::set ignoredExternals; + ignoredExternals.insert(modelledExternals, + modelledExternals + NELEMS(modelledExternals)); + ignoredExternals.insert(dontCareExternals, + dontCareExternals + NELEMS(dontCareExternals)); + ignoredExternals.insert(unsafeExternals, + unsafeExternals + NELEMS(unsafeExternals)); + + switch (Libc) { + case LibcType::KleeLibc: + ignoredExternals.insert(dontCareKlee, dontCareKlee + NELEMS(dontCareKlee)); + break; + case LibcType::UcLibc: + ignoredExternals.insert(dontCareUclibc, + dontCareUclibc + NELEMS(dontCareUclibc)); + break; + case LibcType::FreestandingLibc: /* silence compiler warning */ + break; + } + + if (WithPOSIXRuntime) { + ignoredExternals.insert("syscall"); + } + + Opts.MainCurrentName = entryFn->getName().str(); + // Get the desired main function. klee_main initializes uClibc // locale and other data and then calls main. auto finalModule = interpreter->setModule( loadedUserModules, loadedLibsModules, Opts, std::move(mainModuleFunctions), std::move(mainModuleGlobals), - std::move(origInstructions)); + std::move(origInstructions), ignoredExternals, redefinitions); externalsAndGlobalsCheck(finalModule); if (InteractiveMode) { diff --git a/unittests/Annotations/AnnotationsTest.cpp b/unittests/Annotations/AnnotationsTest.cpp new file mode 100644 index 0000000000..b48bcf7004 --- /dev/null +++ b/unittests/Annotations/AnnotationsTest.cpp @@ -0,0 +1,117 @@ +#include "gtest/gtest.h" + +#include "klee/Module/Annotation.h" + +#include + +using namespace klee; + +TEST(AnnotationsTest, Empty) { + const json j = json::parse(R"( +{ + "foo" : { + "annotation" : [[]], + "properties" : [] + } +} +)"); + const AnnotationsMap expected = { + {"foo", + {/*functionName*/ "foo", + /*returnStatements*/ std::vector(), + /*argsStatements*/ std::vector>(), + /*properties*/ std::set()}}}; + const AnnotationsMap actual = parseAnnotationsJson(j); + ASSERT_EQ(expected, actual); +} + +TEST(AnnotationsTest, KnownProperties) { + const json j = json::parse(R"( +{ + "foo" : { + "annotation" : [[]], + "properties" : ["deterministic", "noreturn", "deterministic"] + } +} +)"); + 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); +} + +TEST(AnnotationsTest, UnknownProperties) { + const json j = json::parse(R"( +{ + "foo" : { + "annotation" : [[]], + "properties" : ["noname", "noreturn", "deterministic"] + } +} +)"); + 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); +} + +TEST(AnnotationsTest, UnknownAnnotations) { + const json j = json::parse(R"( +{ + "foo" : { + "annotation" : [[], ["Ooo"]], + "properties" : [] + } +} +)"); + const AnnotationsMap actual = parseAnnotationsJson(j); + ASSERT_EQ(actual.at("foo").argsStatements[0][0]->getKind(), + Statement::Kind::Unknown); +} + +TEST(AnnotationsTest, KnownAnnotations) { + const json j = json::parse(R"( +{ + "foo" : { + "annotation" : [["InitNull"], ["Deref", "InitNull"]], + "properties" : [] + } +} +)"); + 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) { + const json j = json::parse(R"( +{ + "foo" : { + "annotation" : [["InitNull:*[10]*&"]], + "properties" : [] + } +} +)"); + 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").returnStatements[0]->offset, expectedOffset); +} diff --git a/unittests/Annotations/CMakeLists.txt b/unittests/Annotations/CMakeLists.txt new file mode 100644 index 0000000000..cb9a7b1df1 --- /dev/null +++ b/unittests/Annotations/CMakeLists.txt @@ -0,0 +1,3 @@ +add_klee_unit_test(AnnotationsTest + AnnotationsTest.cpp) +target_link_libraries(AnnotationsTest PRIVATE kleaverExpr kleaverSolver) diff --git a/unittests/CMakeLists.txt b/unittests/CMakeLists.txt index d4b4d1f9f7..edb1f46361 100644 --- a/unittests/CMakeLists.txt +++ b/unittests/CMakeLists.txt @@ -272,6 +272,7 @@ function(add_klee_unit_test target_name) endfunction() # Unit Tests +add_subdirectory(Annotations) add_subdirectory(Assignment) add_subdirectory(Expr) add_subdirectory(Ref)