From c8b06fdb7a82e0a7b68c48800b82738b14b1b82a Mon Sep 17 00:00:00 2001 From: Lana243 Date: Fri, 16 Jun 2023 14:15:47 +0300 Subject: [PATCH 1/2] [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) From 934dd5d03012b5d593201ffd40be3e67131f1104 Mon Sep 17 00:00:00 2001 From: Yurii Kostyukov Date: Tue, 22 Aug 2023 10:48:25 +0300 Subject: [PATCH 2/2] [feat] Cooddy NPE location handling --- include/klee/Core/TargetedExecutionReporter.h | 4 +- include/klee/Module/KInstruction.h | 1 + include/klee/Module/SarifReport.h | 218 +++++-- include/klee/Module/Target.h | 31 +- lib/Core/Executor.cpp | 2 +- lib/Core/TargetManager.cpp | 47 +- lib/Core/TargetedExecutionManager.cpp | 32 +- lib/Core/TargetedExecutionReporter.cpp | 5 +- lib/Module/SarifReport.cpp | 608 +++++++++++++++--- lib/Module/Target.cpp | 31 +- lib/Module/TargetForest.cpp | 2 +- test/Industry/MacroLocalization.c | 27 + test/Industry/MacroLocalization.c.sarif | 155 +++++ test/Industry/StrangeBugInIFDS.c | 27 + test/Industry/StrangeBugInIFDS.c.sarif | 173 +++++ test/Industry/if2.c | 2 +- 16 files changed, 1146 insertions(+), 219 deletions(-) create mode 100644 test/Industry/MacroLocalization.c create mode 100644 test/Industry/MacroLocalization.c.sarif create mode 100644 test/Industry/StrangeBugInIFDS.c create mode 100644 test/Industry/StrangeBugInIFDS.c.sarif diff --git a/include/klee/Core/TargetedExecutionReporter.h b/include/klee/Core/TargetedExecutionReporter.h index 01b87b4e80..8b5f7fe3d5 100644 --- a/include/klee/Core/TargetedExecutionReporter.h +++ b/include/klee/Core/TargetedExecutionReporter.h @@ -30,8 +30,8 @@ ty min(ty left, ty right); }; // namespace confidence void reportFalsePositive(confidence::ty confidence, - const std::vector &errors, - const std::string &id, std::string whatToIncrease); + const ReachWithErrors &errors, const std::string &id, + std::string whatToIncrease); } // namespace klee diff --git a/include/klee/Module/KInstruction.h b/include/klee/Module/KInstruction.h index 5c64de152c..86dae99a17 100644 --- a/include/klee/Module/KInstruction.h +++ b/include/klee/Module/KInstruction.h @@ -30,6 +30,7 @@ class Instruction; namespace klee { class Executor; class KModule; +struct KFunction; struct KBlock; /// KInstruction - Intermediate instruction representation used diff --git a/include/klee/Module/SarifReport.h b/include/klee/Module/SarifReport.h index 09a59d4d25..ec71b49658 100644 --- a/include/klee/Module/SarifReport.h +++ b/include/klee/Module/SarifReport.h @@ -16,6 +16,7 @@ #include #include "klee/ADT/Ref.h" +#include "llvm/IR/IntrinsicInst.h" #include #include @@ -52,9 +53,10 @@ enum ReachWithError { Reachable, None, }; +using ReachWithErrors = std::vector; const char *getErrorString(ReachWithError error); -std::string getErrorsString(const std::vector &errors); +std::string getErrorsString(const ReachWithErrors &errors); struct FunctionInfo; struct KBlock; @@ -63,11 +65,16 @@ struct ArtifactLocationJson { optional uri; }; +struct Message { + std::string text; +}; + struct RegionJson { optional startLine; optional endLine; optional startColumn; optional endColumn; + optional message; }; struct PhysicalLocationJson { @@ -92,10 +99,6 @@ struct CodeFlowJson { std::vector threadFlows; }; -struct Message { - std::string text; -}; - struct Fingerprints { std::string cooddy_uid; }; @@ -137,7 +140,7 @@ struct SarifReportJson { NLOHMANN_DEFINE_TYPE_NON_INTRUSIVE_WITH_DEFAULT(ArtifactLocationJson, uri) NLOHMANN_DEFINE_TYPE_NON_INTRUSIVE_WITH_DEFAULT(RegionJson, startLine, endLine, - startColumn, endColumn) + startColumn, endColumn, message) NLOHMANN_DEFINE_TYPE_NON_INTRUSIVE_WITH_DEFAULT(PhysicalLocationJson, artifactLocation, region) @@ -165,6 +168,148 @@ NLOHMANN_DEFINE_TYPE_NON_INTRUSIVE_WITH_DEFAULT(RunJson, results, tool) NLOHMANN_DEFINE_TYPE_NON_INTRUSIVE_WITH_DEFAULT(SarifReportJson, runs) +enum class Precision { NotFound = 0, Line = 1, Column = 2, Instruction = 3 }; + +template struct WithPrecision { + T *ptr; + Precision precision; + + explicit WithPrecision(T *p, Precision pr) : ptr(p), precision(pr) {} + explicit WithPrecision(T *p) : WithPrecision(p, Precision::NotFound) {} + explicit WithPrecision() : WithPrecision(nullptr) {} + + void setNotFound() { precision = Precision::NotFound; } + bool isNotFound() const { return precision == Precision::NotFound; } +}; + +struct KBlock; +struct KInstruction; + +using BlockWithPrecision = WithPrecision; +using InstrWithPrecision = WithPrecision; + +inline size_t hash_combine2(std::size_t s, std::size_t v) { + return s ^ (v + 0x9e3779b9 + (s << 6) + (s >> 2)); +} + +template inline void hash_combine(std::size_t &s, const T &v) { + std::hash h; + s = hash_combine2(s, h(v)); +} + +enum class ReachWithoutError { + Reach = 0, + Return, + NPESource, + Free, + BranchFalse, + BranchTrue, + Call, + AfterCall +}; + +struct EventKind final { + const bool isError; + const ReachWithErrors kinds; + const ReachWithoutError kind; + size_t hashValue = 0; + void computeHash() { + hash_combine(hashValue, isError); + for (auto k : kinds) + hash_combine(hashValue, k); + hash_combine(hashValue, kind); + } + EventKind(ReachWithErrors &&kinds) + : isError(true), kinds(kinds), kind(ReachWithoutError::Reach) { + computeHash(); + } + EventKind(ReachWithoutError kind) : isError(false), kind(kind) { + computeHash(); + } +}; +} // namespace klee + +namespace std { +template <> struct hash { + size_t operator()(const klee::EventKind &k) const { return k.hashValue; } +}; +} // namespace std + +namespace klee { +enum class ToolName { Unknown = 0, SecB, clang, CppCheck, Infer, Cooddy }; + +class LineColumnRange; + +struct LocRange { + virtual LineColumnRange getRange() const = 0; + virtual ~LocRange() = default; + virtual Precision maxPrecision() const = 0; + virtual size_t hash() const = 0; + virtual std::string toString() const = 0; + bool hasInside(KInstruction *ki) const; + void hasInside(InstrWithPrecision &kp); + virtual void setRange(const KInstruction *ki) = 0; + +protected: + virtual bool hasInsideInternal(InstrWithPrecision &kp) const = 0; +}; + +class LineColumnRange final : public LocRange { + size_t startLine; + size_t startColumn; + size_t endLine; + size_t endColumn; + static const size_t empty = std::numeric_limits::max(); + + bool inline onlyLine() const { return startColumn == empty; } + +public: + explicit LineColumnRange(size_t startLine, size_t startColumn, size_t endLine, + size_t endColumn) + : startLine(startLine), startColumn(startColumn), endLine(endLine), + endColumn(endColumn) { + assert(startLine <= endLine); + assert(startLine != endLine || startColumn <= endColumn); + } + explicit LineColumnRange(size_t startLine, size_t endLine) + : LineColumnRange(startLine, empty, endLine, empty) {} + explicit LineColumnRange(const KInstruction *ki) { setRange(ki); } + + void setRange(const KInstruction *ki) final; + + LineColumnRange getRange() const final { return *this; } + + void clearColumns() { startColumn = (endColumn = empty); } + + Precision maxPrecision() const final { + return onlyLine() ? Precision::Line : Precision::Column; + } + + size_t hash() const final { + size_t hashValue = 0; + hashValue = hash_combine2(hashValue, startLine); + hashValue = hash_combine2(hashValue, endLine); + hashValue = hash_combine2(hashValue, startColumn); + return hash_combine2(hashValue, endColumn); + } + + std::string toString() const final { + if (onlyLine()) + return std::to_string(startLine) + "-" + std::to_string(endLine); + return std::to_string(startLine) + ":" + std::to_string(startColumn) + "-" + + std::to_string(endLine) + ":" + std::to_string(endColumn); + } + + bool hasInsideInternal(InstrWithPrecision &kp) const final; + + bool operator==(const LineColumnRange &p) const { + return startLine == p.startLine && endLine == p.endLine && + startColumn == p.startColumn && endColumn == p.endColumn; + } +}; + +using OpCode = unsigned; + struct Location { struct LocationHash { std::size_t operator()(const Location *l) const { return l->hash(); } @@ -184,35 +329,30 @@ struct Location { } }; std::string filename; - unsigned int startLine; - unsigned int endLine; - optional startColumn; - optional endColumn; + std::unique_ptr range; - static ref create(std::string filename_, unsigned int startLine_, + static ref create(std::string &&filename_, unsigned int startLine_, optional endLine_, optional startColumn_, - optional endColumn_); + optional endColumn_, + ToolName toolName, EventKind &kind); - ~Location(); - std::size_t hash() const { return hashValue; } + virtual ~Location(); + virtual std::size_t hash() const { return hashValue; } /// @brief Required by klee::ref-managed objects class ReferenceCounter _refCount; - bool operator==(const Location &other) const { - return filename == other.filename && startLine == other.startLine && - endLine == other.endLine && startColumn == other.startColumn && - endColumn == other.endColumn; - } + bool operator==(const Location &other) const; bool isInside(const std::string &name) const; using Instructions = std::unordered_map< unsigned int, - std::unordered_map>>; + std::unordered_map>>; - bool isInside(KBlock *block, const Instructions &origInsts) const; + void isInside(InstrWithPrecision &kp, const Instructions &origInsts) const; + void isInside(BlockWithPrecision &bp, const Instructions &origInsts) const; std::string toString() const; @@ -226,28 +366,20 @@ struct Location { static LocationHashSet locations; size_t hashValue = 0; - void computeHash() { - hash_combine(hashValue, filename); - hash_combine(hashValue, startLine); - hash_combine(hashValue, endLine); - hash_combine(hashValue, startColumn); - hash_combine(hashValue, endColumn); - } + void computeHash(EventKind &kind); - template inline void hash_combine(std::size_t &s, const T &v) { - std::hash h; - s ^= h(v) + 0x9e3779b9 + (s << 6) + (s >> 2); - } + static Location *createCooddy(std::string &&filename_, LineColumnRange &range, + EventKind &kind); - Location(std::string filename_, unsigned int startLine_, - optional endLine_, optional startColumn_, - optional endColumn_) - : filename(filename_), startLine(startLine_), - endLine(endLine_.has_value() ? *endLine_ : startLine_), - startColumn(startColumn_), - endColumn(endColumn_.has_value() ? endColumn_ : startColumn_) { - computeHash(); +protected: + Location(std::string &&filename_, std::unique_ptr range, + EventKind &kind) + : filename(std::move(filename_)), range(std::move(range)) { + computeHash(kind); } + + virtual void isInsideInternal(BlockWithPrecision &bp, + const Instructions &origInsts) const; }; struct RefLocationHash { @@ -262,9 +394,9 @@ struct RefLocationCmp { struct Result { std::vector> locations; - std::vector> metadatas; - std::string id; - std::vector errors; + const std::vector> metadatas; + const std::string id; + const ReachWithErrors errors; }; struct SarifReport { diff --git a/include/klee/Module/Target.h b/include/klee/Module/Target.h index 98eb3c900a..e54047dcde 100644 --- a/include/klee/Module/Target.h +++ b/include/klee/Module/Target.h @@ -36,16 +36,6 @@ DISABLE_WARNING_POP namespace klee { using nonstd::optional; -struct ErrorLocation { - unsigned int startLine; - unsigned int endLine; - optional startColumn; - optional endColumn; - - ErrorLocation(const klee::ref &loc); - ErrorLocation(const KInstruction *ki); -}; - class ReproduceErrorTarget; class Target { @@ -174,23 +164,22 @@ class CoverBranchTarget : public Target { class ReproduceErrorTarget : public Target { private: - std::vector - errors; // None - if it is not terminated in error trace - std::string id; // "" - if it is not terminated in error trace - ErrorLocation loc; // TODO(): only for check in reportTruePositive + ReachWithErrors errors; // None - if it is not terminated in error trace + std::string id; // "" - if it is not terminated in error trace + LineColumnRange loc; // TODO(): only for check in reportTruePositive protected: - explicit ReproduceErrorTarget(const std::vector &_errors, - const std::string &_id, ErrorLocation _loc, + explicit ReproduceErrorTarget(const ReachWithErrors &_errors, + const std::string &_id, LineColumnRange _loc, KBlock *_block) - : Target(_block), errors(_errors), id(_id), loc(_loc) { + : Target(_block), errors(_errors), id(_id), loc(std::move(_loc)) { assert(errors.size() > 0); std::sort(errors.begin(), errors.end()); } public: - static ref create(const std::vector &_errors, - const std::string &_id, ErrorLocation _loc, + static ref create(const ReachWithErrors &_errors, + const std::string &_id, LineColumnRange _loc, KBlock *_block); Kind getKind() const override { return Kind::ReproduceError; } @@ -207,12 +196,12 @@ class ReproduceErrorTarget : public Target { bool isReported = false; - const std::vector &getErrors() const { return errors; } + const ReachWithErrors &getErrors() const { return errors; } bool isThatError(ReachWithError err) const { return std::find(errors.begin(), errors.end(), err) != errors.end(); } - bool isTheSameAsIn(const KInstruction *instr) const; + bool isTheSameAsIn(KInstruction *instr) const; }; } // namespace klee diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index fbb1cad498..1c901b4d99 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -6707,7 +6707,7 @@ void Executor::runFunctionAsMain(Function *f, int argc, char **argv, KBlock *kCallBlock = kfunction->entryKBlock; forest->add(ReproduceErrorTarget::create( {ReachWithError::Reachable}, "", - ErrorLocation(kCallBlock->getFirstInstruction()), kCallBlock)); + LineColumnRange(kCallBlock->getFirstInstruction()), kCallBlock)); prepTargets.emplace(kEntryFunction, forest); } diff --git a/lib/Core/TargetManager.cpp b/lib/Core/TargetManager.cpp index 9dcaedcd86..1af337b436 100644 --- a/lib/Core/TargetManager.cpp +++ b/lib/Core/TargetManager.cpp @@ -152,29 +152,34 @@ void TargetManager::updateTargets(ExecutionState &state) { return; } - auto stateTargets = targets(state); - auto &stateTargetForest = targetForest(state); - - for (auto target : stateTargets) { - if (!stateTargetForest.contains(target)) { - continue; - } + bool needRecheck; + do { + needRecheck = false; + auto stateTargets = targets(state); + auto &stateTargetForest = targetForest(state); + + for (auto target : stateTargets) { + if (!stateTargetForest.contains(target)) { + continue; + } - DistanceResult stateDistance = distance(state, target); - switch (stateDistance.result) { - case WeightResult::Continue: - updateContinue(state, target); - break; - case WeightResult::Miss: - updateMiss(state, target); - break; - case WeightResult::Done: - updateDone(state, target); - break; - default: - assert(0 && "unreachable"); + DistanceResult stateDistance = distance(state, target); + switch (stateDistance.result) { + case WeightResult::Continue: + updateContinue(state, target); + break; + case WeightResult::Miss: + updateMiss(state, target); + break; + case WeightResult::Done: + updateDone(state, target); + needRecheck = true; + break; + default: + assert(0 && "unreachable"); + } } - } + } while (needRecheck); } void TargetManager::update(ExecutionState *current, diff --git a/lib/Core/TargetedExecutionManager.cpp b/lib/Core/TargetedExecutionManager.cpp index a46a12e3c9..2b4e12a3fd 100644 --- a/lib/Core/TargetedExecutionManager.cpp +++ b/lib/Core/TargetedExecutionManager.cpp @@ -182,6 +182,11 @@ cl::opt cl::desc("stop execution after visiting some basic block this " "amount of times (default=0)."), cl::init(0), cl::cat(TerminationCat)); + +cl::opt DebugLocalization( + "debug-localization", cl::init(false), + cl::desc("Debug error traces localization (default=false)."), + cl::cat(DebugCat)); } // namespace klee TargetedHaltsOnTraces::TargetedHaltsOnTraces(ref &forest) { @@ -327,6 +332,8 @@ TargetedExecutionManager::prepareAllLocations(KModule *kmodule, for (auto it = locations.begin(); it != locations.end(); ++it) { auto loc = *it; + auto precision = Precision::Line; + Blocks blocks; for (const auto &[fileName, origInstsInFile] : kmodule->origInstructions) { if (kmodule->origInstructions.count(fileName) == 0) { continue; @@ -341,16 +348,29 @@ TargetedExecutionManager::prepareAllLocations(KModule *kmodule, const auto kfunc = kmodule->functionMap[func]; for (const auto &kblock : kfunc->blocks) { - auto b = kblock.get(); - if (!loc->isInside(b, origInstsInFile)) { + BlockWithPrecision bp(kblock.get(), precision); + loc->isInside(bp, origInstsInFile); + if (bp.precision < precision) { continue; + } else if (bp.precision == precision) { + blocks.insert(bp.ptr); + } else { + blocks.clear(); + blocks.insert(bp.ptr); + precision = bp.precision; } - locToBlocks[loc].insert(b); } } } + if (DebugLocalization && !blocks.empty()) { + llvm::errs() << loc->toString() << " # " << (int)precision << " ~> "; + for (auto b : blocks) { + llvm::errs() << b->toString() << "; "; + } + llvm::errs() << "\n"; + } + locToBlocks.emplace(loc, std::move(blocks)); } - return locToBlocks; } @@ -417,7 +437,7 @@ bool TargetedExecutionManager::tryResolveLocations( } } resolvedLocations.push_back(location); - } else if (index == result.locations.size() - 1) { + } else if (index + 1 == result.locations.size()) { klee_warning( "Trace %s is malformed! %s at location %s, so skipping this trace.", result.id.c_str(), getErrorsString(result.errors).c_str(), @@ -519,6 +539,8 @@ TargetedExecutionManager::prepareTargets(KModule *kmodule, SarifReport paths) { whitelists[kf] = whitelist; } whitelists[kf]->addTrace(result, locToBlocks); + if (DebugLocalization) + whitelists[kf]->dump(); } return whitelists; diff --git a/lib/Core/TargetedExecutionReporter.cpp b/lib/Core/TargetedExecutionReporter.cpp index b45569336f..56e5ee77e8 100644 --- a/lib/Core/TargetedExecutionReporter.cpp +++ b/lib/Core/TargetedExecutionReporter.cpp @@ -15,12 +15,11 @@ using namespace klee; void klee::reportFalsePositive(confidence::ty confidence, - const std::vector &errors, + const ReachWithErrors &errors, const std::string &id, std::string whatToIncrease) { std::ostringstream out; - std::vector errorsSet(errors.begin(), errors.end()); - out << getErrorsString(errorsSet) << " False Positive at trace " << id; + out << getErrorsString(errors) << " False Positive at trace " << id; if (!confidence::isConfident(confidence)) { out << ". Advice: " << "increase --" << whatToIncrease << " command line parameter value"; diff --git a/lib/Module/SarifReport.cpp b/lib/Module/SarifReport.cpp index 3923d32ead..3393070dcd 100644 --- a/lib/Module/SarifReport.cpp +++ b/lib/Module/SarifReport.cpp @@ -7,11 +7,14 @@ // //===----------------------------------------------------------------------===// +#include + #include "klee/Module/SarifReport.h" #include "klee/Module/KInstruction.h" #include "klee/Module/KModule.h" #include "klee/Support/ErrorHandling.h" +#include "llvm/Support/CommandLine.h" #include "klee/Support/CompilerWarning.h" DISABLE_WARNING_PUSH @@ -25,34 +28,10 @@ using namespace klee; namespace { bool isOSSeparator(char c) { return c == '/' || c == '\\'; } -optional> -tryConvertLocationJson(const LocationJson &locationJson) { - const auto &physicalLocation = locationJson.physicalLocation; - if (!physicalLocation.has_value()) { - return nonstd::nullopt; - } - - const auto &artifactLocation = physicalLocation->artifactLocation; - if (!artifactLocation.has_value() || !artifactLocation->uri.has_value()) { - return nonstd::nullopt; - } - - const auto filename = std::move(*(artifactLocation->uri)); - - const auto ®ion = physicalLocation->region; - if (!region.has_value() || !region->startLine.has_value()) { - return nonstd::nullopt; - } - - return Location::create(std::move(filename), *(region->startLine), - region->endLine, region->startColumn, - region->endColumn); -} - -std::vector -tryConvertRuleJson(const std::string &ruleId, const std::string &toolName, - const optional &errorMessage) { - if (toolName == "SecB") { +ReachWithErrors tryConvertRuleJson(const std::string &ruleId, ToolName toolName, + const optional &errorMessage) { + switch (toolName) { + case ToolName::SecB: if ("NullDereference" == ruleId) { return {ReachWithError::MustBeNullPointerException}; } else if ("CheckAfterDeref" == ruleId) { @@ -63,10 +42,9 @@ tryConvertRuleJson(const std::string &ruleId, const std::string &toolName, return {ReachWithError::UseAfterFree}; } else if ("Reached" == ruleId) { return {ReachWithError::Reachable}; - } else { - return {}; } - } else if (toolName == "clang") { + return {}; + case ToolName::clang: if ("core.NullDereference" == ruleId) { return {ReachWithError::MayBeNullPointerException, ReachWithError::MustBeNullPointerException}; @@ -84,28 +62,25 @@ tryConvertRuleJson(const std::string &ruleId, const std::string &toolName, } } else if ("core.Reach" == ruleId) { return {ReachWithError::Reachable}; - } else { - return {}; } - } else if (toolName == "CppCheck") { + return {}; + case ToolName::CppCheck: if ("nullPointer" == ruleId || "ctunullpointer" == ruleId) { return {ReachWithError::MayBeNullPointerException, ReachWithError::MustBeNullPointerException}; // TODO: check it out } else if ("doubleFree" == ruleId) { return {ReachWithError::DoubleFree}; - } else { - return {}; } - } else if (toolName == "Infer") { + return {}; + case ToolName::Infer: if ("NULL_DEREFERENCE" == ruleId || "NULLPTR_DEREFERENCE" == ruleId) { return {ReachWithError::MayBeNullPointerException, ReachWithError::MustBeNullPointerException}; // TODO: check it out } else if ("USE_AFTER_DELETE" == ruleId || "USE_AFTER_FREE" == ruleId) { return {ReachWithError::UseAfterFree, ReachWithError::DoubleFree}; - } else { - return {}; } - } else if (toolName == "Cooddy") { + return {}; + case ToolName::Cooddy: if ("NULL.DEREF" == ruleId || "NULL.UNTRUSTED.DEREF" == ruleId) { return {ReachWithError::MayBeNullPointerException, ReachWithError::MustBeNullPointerException}; @@ -113,30 +88,133 @@ tryConvertRuleJson(const std::string &ruleId, const std::string &toolName, return {ReachWithError::DoubleFree}; } else if ("MEM.USE.FREE" == ruleId) { return {ReachWithError::UseAfterFree}; - } else { - return {}; } - } else { + return {}; + case ToolName::Unknown: return {}; } } +bool startsWith(const std::string &s, const std::string &prefix) { + return s.rfind(prefix, 0) == 0; +} + +bool endsWith(const std::string &s, const std::string &suffix) { + ssize_t maybe_index = s.size() - suffix.size(); + return maybe_index > 0 && + (s.find(suffix, maybe_index) == (size_t)maybe_index); +} + +ReachWithoutError tryConvertCooddyNoErrorKind(const klee::Message &msg) { + const auto &message = msg.text; + if ("Assume return here" == message) + return ReachWithoutError::Return; + if (startsWith(message, "Null pointer returned as")) + return ReachWithoutError::AfterCall; + if (startsWith(message, "Use after free returned as")) + return ReachWithoutError::AfterCall; + if ("Null pointer source" == message) + return ReachWithoutError::NPESource; + if ("Free" == message) + return ReachWithoutError::Free; + if (startsWith(message, "Function ") && endsWith(message, " is executed")) + return ReachWithoutError::Call; + if (startsWith(message, "Null pointer passed as")) + return ReachWithoutError::Call; + if (startsWith(message, "Use after free passed as")) + return ReachWithoutError::Call; + if (endsWith(message, " is false")) + return ReachWithoutError::BranchFalse; + if (endsWith(message, " is true")) + return ReachWithoutError::BranchTrue; + return ReachWithoutError::Reach; +} + +ReachWithoutError tryConvertNoErrorKind(ToolName toolName, + const klee::Message &message) { + switch (toolName) { + case ToolName::Cooddy: + return tryConvertCooddyNoErrorKind(message); + default: + return ReachWithoutError::Reach; + } +} + +ReachWithErrors tryConvertErrorKind(ToolName toolName, + const optional &ruleId, + const optional &msg) { + if (!ruleId.has_value()) { + return {ReachWithError::Reachable}; + } else { + return tryConvertRuleJson(*ruleId, toolName, msg); + } +} + +EventKind convertKindJson(ToolName toolName, + const optional &ruleId, + const std::optional &mOpt) { + if (!mOpt.has_value()) + return EventKind(ReachWithoutError::Reach); + const auto &message = *mOpt; + auto noError = tryConvertNoErrorKind(toolName, message); + if (noError != ReachWithoutError::Reach) + return EventKind(noError); + return EventKind(tryConvertErrorKind(toolName, ruleId, mOpt)); +} + +optional, EventKind>> +tryConvertLocationJson(ToolName toolName, const optional &ruleId, + const LocationJson &locationJson) { + const auto &physicalLocation = locationJson.physicalLocation; + if (!physicalLocation.has_value()) { + return nonstd::nullopt; + } + + const auto &artifactLocation = physicalLocation->artifactLocation; + if (!artifactLocation.has_value() || !artifactLocation->uri.has_value()) { + return nonstd::nullopt; + } + + const auto ®ion = physicalLocation->region; + if (!region.has_value() || !region->startLine.has_value()) { + return nonstd::nullopt; + } + + auto kind = convertKindJson(toolName, ruleId, region->message); + auto filename = *(artifactLocation->uri); + + auto loc = Location::create(std::move(filename), *(region->startLine), + region->endLine, region->startColumn, + region->endColumn, toolName, kind); + return std::make_pair(loc, std::move(kind)); +} + +void recoverCallChain(std::vector> &locations, + std::vector &kinds) { + std::list> result; + auto lit = locations.begin(); + auto kit = kinds.begin(), kite = kinds.end(); + for (; kit != kite; kit++, lit++) { + if (kit->kind == ReachWithoutError::AfterCall) + result.push_front(*lit); + else + result.push_back(*lit); + } + locations.assign(result.begin(), result.end()); +} + optional tryConvertResultJson(const ResultJson &resultJson, - const std::string &toolName, + ToolName toolName, const std::string &id) { - std::vector errors = {}; - if (!resultJson.ruleId.has_value()) { - errors = {ReachWithError::Reachable}; - } else { - errors = - tryConvertRuleJson(*resultJson.ruleId, toolName, resultJson.message); - if (errors.size() == 0) { - klee_warning("undefined error in %s result", id.c_str()); - return nonstd::nullopt; - } + auto errors = + tryConvertErrorKind(toolName, resultJson.ruleId, resultJson.message); + if (errors.size() == 0) { + klee_warning("undefined error in %s result", id.c_str()); + return nonstd::nullopt; } std::vector> locations; + std::vector kinds; std::vector> metadatas; if (resultJson.codeFlows.size() > 0) { @@ -149,17 +227,21 @@ optional tryConvertResultJson(const ResultJson &resultJson, return nonstd::nullopt; } - auto maybeLocation = tryConvertLocationJson(*threadFlowLocation.location); - if (maybeLocation.has_value()) { - locations.push_back(*maybeLocation); + auto mblk = tryConvertLocationJson(toolName, resultJson.ruleId, + *threadFlowLocation.location); + if (mblk.has_value()) { + locations.push_back(mblk->first); + kinds.push_back(mblk->second); metadatas.push_back(std::move(threadFlowLocation.metadata)); } } } else { assert(resultJson.locations.size() == 1); - auto maybeLocation = tryConvertLocationJson(resultJson.locations[0]); - if (maybeLocation.has_value()) { - locations.push_back(*maybeLocation); + auto mblk = tryConvertLocationJson(toolName, resultJson.ruleId, + resultJson.locations[0]); + if (mblk.has_value()) { + locations.push_back(mblk->first); + kinds.push_back(mblk->second); } } @@ -167,12 +249,18 @@ optional tryConvertResultJson(const ResultJson &resultJson, return nonstd::nullopt; } + recoverCallChain(locations, kinds); + return Result{std::move(locations), std::move(metadatas), id, std::move(errors)}; } } // anonymous namespace namespace klee { +llvm::cl::opt LocationAccuracy( + "location-accuracy", cl::init(false), + cl::desc("Check location with line and column accuracy (default=false)")); + static const char *ReachWithErrorNames[] = { "DoubleFree", "UseAfterFree", @@ -183,11 +271,39 @@ static const char *ReachWithErrorNames[] = { "None", }; +void LineColumnRange::setRange(const KInstruction *ki) { + startLine = (endLine = ki->getLine()); + startColumn = (endColumn = ki->getColumn()); +} + +bool LineColumnRange::hasInsideInternal(InstrWithPrecision &kp) const { + auto line = kp.ptr->getLine(); + if (!(startLine <= line && line <= endLine)) { + kp.setNotFound(); + return false; + } + if (onlyLine()) { + kp.precision = Precision::Line; + return false; + } + auto column = kp.ptr->getColumn(); + auto ok = true; + if (line == startLine) + ok = column >= startColumn; + if (line == endLine) + ok = ok && column <= endColumn; + if (ok) + kp.precision = Precision::Column; + else + kp.precision = Precision::Line; + return false; +} + const char *getErrorString(ReachWithError error) { return ReachWithErrorNames[error]; } -std::string getErrorsString(const std::vector &errors) { +std::string getErrorsString(const ReachWithErrors &errors) { if (errors.size() == 1) { return getErrorString(*errors.begin()); } @@ -239,24 +355,38 @@ class NumericTraceId : public TraceId { void getNextId(const klee::ResultJson &resultJson) override { id++; } }; -TraceId *createTraceId(const std::string &toolName, - const std::vector &results) { - if (toolName == "Cooddy") - return new CooddyTraceId(); +std::unique_ptr +createTraceId(ToolName toolName, const std::vector &results) { + if (toolName == ToolName::Cooddy) + return std::make_unique(); else if (results.size() > 0 && results[0].id.has_value()) - return new GetterTraceId(); - return new NumericTraceId(); + return std::make_unique(); + return std::make_unique(); } void setResultId(const ResultJson &resultJson, bool useProperId, unsigned &id) { if (useProperId) { - assert(resultJson.id.has_value() && "all results must have an proper id"); + assert(resultJson.id.has_value() && "all results must have a proper id"); id = resultJson.id.value(); } else { ++id; } } +ToolName convertToolName(const std::string &toolName) { + if ("SecB" == toolName) + return ToolName::SecB; + if ("clang" == toolName) + return ToolName::clang; + if ("CppCheck" == toolName) + return ToolName::CppCheck; + if ("Infer" == toolName) + return ToolName::Infer; + if ("Cooddy" == toolName) + return ToolName::Cooddy; + return ToolName::Unknown; +} + SarifReport convertAndFilterSarifJson(const SarifReportJson &reportJson) { SarifReport report; @@ -267,9 +397,9 @@ SarifReport convertAndFilterSarifJson(const SarifReportJson &reportJson) { assert(reportJson.runs.size() == 1); const RunJson &run = reportJson.runs[0]; - const std::string toolName = run.tool.driver.name; + auto toolName = convertToolName(run.tool.driver.name); - TraceId *id = createTraceId(toolName, run.results); + auto id = createTraceId(toolName, run.results); for (const auto &resultJson : run.results) { id->getNextId(resultJson); @@ -279,7 +409,6 @@ SarifReport convertAndFilterSarifJson(const SarifReportJson &reportJson) { report.results.push_back(*maybeResult); } } - delete id; return report; } @@ -287,12 +416,230 @@ SarifReport convertAndFilterSarifJson(const SarifReportJson &reportJson) { Location::EquivLocationHashSet Location::cachedLocations; Location::LocationHashSet Location::locations; -ref Location::create(std::string filename_, unsigned int startLine_, +bool LocRange::hasInside(KInstruction *ki) const { + if (isa(ki->inst)) + return false; + InstrWithPrecision kp(ki); + hasInsideInternal(kp); + auto suitable = maxPrecision(); + return kp.precision >= suitable; +} + +void LocRange::hasInside(InstrWithPrecision &kp) { + if (kp.precision > maxPrecision()) { + kp.setNotFound(); + return; + } + if (hasInsideInternal(kp)) + setRange(kp.ptr); +} + +class InstructionRange : public LocRange { + LineColumnRange range; + OpCode opCode; + +public: + InstructionRange(LineColumnRange &&range, OpCode opCode) + : range(std::move(range)), opCode(opCode) {} + + LineColumnRange getRange() const final { return range; } + + Precision maxPrecision() const final { return Precision::Instruction; } + + size_t hash() const final { return hash_combine2(range.hash(), opCode); } + + std::string toString() const final { + return range.toString() + " " + std::to_string(opCode); + } + + void setRange(const KInstruction *ki) final { range.setRange(ki); } + + bool hasInsideInternal(InstrWithPrecision &kp) const final { + range.hasInsideInternal(kp); + if (kp.isNotFound()) + return false; + if (kp.ptr->inst->getOpcode() != opCode) + return false; + if (hasInsidePrecise(kp.ptr)) { + kp.precision = Precision::Instruction; + return true; + } else { + kp.precision = std::min(kp.precision, Precision::Column); + return false; + } + } + +protected: + virtual bool hasInsidePrecise(const KInstruction *ki) const { return true; } +}; + +namespace Cooddy { +using namespace llvm; + +class StoreNullRange final : public InstructionRange { + using InstructionRange::InstructionRange; + +public: + StoreNullRange(LineColumnRange &&range) + : InstructionRange(std::move(range), Instruction::Store) {} + + bool hasInsidePrecise(const KInstruction *ki) const final { + auto stinst = dyn_cast(ki->inst); + if (!stinst) + return false; + auto value = dyn_cast(stinst->getValueOperand()); + if (!value) + return false; + return value->isNullValue(); + } +}; + +class BranchRange final : public InstructionRange { + using InstructionRange::InstructionRange; + +public: + BranchRange(LineColumnRange &&range) + : InstructionRange(std::move(range), Instruction::Br) {} + + bool hasInsidePrecise(const KInstruction *ki) const final { + return ki->inst->getNumSuccessors() == 2; + } +}; + +struct OpCodeLoc final : public Location { + using Location::Location; + OpCodeLoc(std::string &&filename_, LineColumnRange &&range, EventKind &kind, + OpCode opCode) + : Location(std::move(filename_), + std::make_unique(std::move(range), opCode), + kind) {} +}; + +struct AfterLoc : public Location { + using Location::Location; + void isInsideInternal(BlockWithPrecision &bp, + const Instructions &origInsts) const final; + +protected: + virtual void isInsideInternal(BlockWithPrecision &bp, + const InstrWithPrecision &afterInst) const = 0; +}; + +struct AfterBlockLoc final : public AfterLoc { + using AfterLoc::AfterLoc; + AfterBlockLoc(std::string &&filename_, std::unique_ptr range, + EventKind &kind, unsigned indexOfNext) + : AfterLoc(std::move(filename_), std::move(range), kind), + indexOfNext(indexOfNext) {} + void isInsideInternal(BlockWithPrecision &bp, + const InstrWithPrecision &afterInst) const final; + +private: + unsigned indexOfNext; +}; + +struct AfterInstLoc final : public AfterLoc { + using AfterLoc::AfterLoc; + AfterInstLoc(std::string &&filename_, std::unique_ptr range, + EventKind &kind, OpCode opCode) + : AfterLoc(std::move(filename_), std::move(range), kind), opCode(opCode) { + } + void isInsideInternal(BlockWithPrecision &bp, + const InstrWithPrecision &afterInst) const final; + +private: + OpCode opCode; +}; +} // namespace Cooddy + +LineColumnRange create(unsigned int startLine_, optional endLine_, + optional startColumn_, + optional endColumn_) { + auto endLine = endLine_.has_value() ? *endLine_ : startLine_; + if (LocationAccuracy && startColumn_.has_value()) { + auto endColumn = endColumn_.has_value() ? *endColumn_ : *startColumn_; + return LineColumnRange(startLine_, *startColumn_, endLine, endColumn); + } + return LineColumnRange(startLine_, endLine); +} + +bool Location::operator==(const Location &other) const { + return filename == other.filename && + range->getRange() == other.range->getRange(); +} + +void Location::computeHash(EventKind &kind) { + hash_combine(hashValue, filename); + hash_combine(hashValue, range->hash()); + hash_combine(hashValue, kind); +} + +Location *Location::createCooddy(std::string &&filename_, + LineColumnRange &range, EventKind &kind) { + if (kind.isError) { + if (kind.kinds.size() == 1) { + switch (kind.kinds[0]) { + case ReachWithError::DoubleFree: + return new Cooddy::OpCodeLoc(std::move(filename_), std::move(range), + kind, Instruction::Call); + default: + return nullptr; + } + } else if (std::find(kind.kinds.begin(), kind.kinds.end(), + ReachWithError::MustBeNullPointerException) != + kind.kinds.end()) { + // the thing that Cooddy reports is too complex, so we fallback to just + // lines + range.clearColumns(); + return nullptr; + // return new Cooddy::OpCodeLoc(std::move(filename_), std::move(range), + // kind, Instruction::Load); + } + return nullptr; + } + switch (kind.kind) { + case ReachWithoutError::Return: + return new Cooddy::OpCodeLoc(std::move(filename_), std::move(range), kind, + Instruction::Ret); + case ReachWithoutError::NPESource: + return new Location( + std::move(filename_), + std::make_unique(std::move(range)), kind); + case ReachWithoutError::BranchTrue: + case ReachWithoutError::BranchFalse: { + auto succ = kind.kind == ReachWithoutError::BranchTrue ? 0 : 1; + return new Cooddy::AfterBlockLoc( + std::move(filename_), + std::make_unique(std::move(range)), kind, succ); + } + case ReachWithoutError::Free: + case ReachWithoutError::Call: + case ReachWithoutError::AfterCall: + return new Cooddy::OpCodeLoc(std::move(filename_), std::move(range), kind, + Instruction::Call); + case ReachWithoutError::Reach: + return nullptr; + } +} + +ref Location::create(std::string &&filename_, unsigned int startLine_, optional endLine_, optional startColumn_, - optional endColumn_) { - Location *loc = - new Location(filename_, startLine_, endLine_, startColumn_, endColumn_); + optional endColumn_, + ToolName toolName, EventKind &kind) { + auto range = klee::create(startLine_, endLine_, startColumn_, endColumn_); + Location *loc = nullptr; + switch (toolName) { + case ToolName::Cooddy: + loc = createCooddy(std::move(filename_), range, kind); + break; + default: + break; + } + if (!loc) + loc = + new Location(std::move(filename_), + std::make_unique(std::move(range)), kind); std::pair success = cachedLocations.insert(loc); if (success.second) { @@ -325,32 +672,103 @@ bool Location::isInside(const std::string &name) const { : (m == -1 && isOSSeparator(filename[n]))); } -bool Location::isInside(KBlock *block, const Instructions &origInsts) const { - auto first = block->getFirstInstruction(); - auto last = block->getLastInstruction(); - if (!startColumn.has_value()) { - if (first->getLine() > endLine) - return false; - return startLine <= last->getLine(); // and `first <= line` from above - } else { - for (size_t i = 0; i < block->numInstructions; ++i) { - auto inst = block->instructions[i]; - auto opCode = block->instructions[i]->inst->getOpcode(); - if (!isa(block->instructions[i]->inst) && - inst->getLine() <= endLine && inst->getLine() >= startLine && - inst->getColumn() <= *endColumn && - inst->getColumn() >= *startColumn && - origInsts.at(inst->getLine()).at(inst->getColumn()).count(opCode) != - 0) { - return true; +void Location::isInside(InstrWithPrecision &kp, + const Instructions &origInsts) const { + auto ki = kp.ptr; + // TODO: exterminate origInsts! + auto it = origInsts.find(ki->getLine()); + if (it == origInsts.end()) { + kp.setNotFound(); + return; + } + auto it2 = it->second.find(ki->getColumn()); + if (it2 == it->second.end()) { + kp.setNotFound(); + return; + } + if (!it2->second.count(ki->inst->getOpcode())) { + kp.setNotFound(); + return; + } + range->hasInside(kp); +} + +void Location::isInside(BlockWithPrecision &bp, + const Instructions &origInsts) const { + if (bp.precision > range->maxPrecision()) + bp.setNotFound(); + else + isInsideInternal(bp, origInsts); +} + +void Location::isInsideInternal(BlockWithPrecision &bp, + const Instructions &origInsts) const { + bool found = false; + for (size_t i = 0; i < bp.ptr->numInstructions; ++i) { + InstrWithPrecision kp(bp.ptr->instructions[i], bp.precision); + isInside(kp, origInsts); + if (kp.precision >= bp.precision) { + bp.precision = kp.precision; + found = true; + if (kp.precision >= range->maxPrecision()) { + bp.ptr = kp.ptr->parent; + return; } } + } + if (!found) + bp.setNotFound(); +} - return false; +void Cooddy::AfterLoc::isInsideInternal(BlockWithPrecision &bp, + const Instructions &origInsts) const { + // if (x + y > z && aaa->bbb->ccc->ddd) + // ^^^^^^^^^^^^^^^^^ first, skip all this + // second skip this ^^^^^^^^ (where Cooddy event points) + // finally, get this ^ (real location of needed instruction) + auto inside = false; + InstrWithPrecision afterInst(nullptr, bp.precision); + for (size_t i = 0; i < bp.ptr->numInstructions; ++i) { + afterInst.ptr = bp.ptr->instructions[i]; + auto kp = afterInst; + Location::isInside(kp, origInsts); + if (kp.precision >= afterInst.precision) { // first: go until Cooddy event + afterInst.precision = kp.precision; + inside = true; // first: reached Cooddy event + } else if (inside) // second: skip until left Coody event + break; + } + if (!inside) { // no Cooddy event in this Block + bp.setNotFound(); + return; + } + isInsideInternal(bp, afterInst); +} + +void Cooddy::AfterBlockLoc::isInsideInternal( + BlockWithPrecision &bp, const InstrWithPrecision &afterInst) const { + if (afterInst.precision != Precision::Instruction) { + bp.setNotFound(); + return; + } + auto nextBlock = + bp.ptr->basicBlock->getTerminator()->getSuccessor(indexOfNext); + bp.ptr = bp.ptr->parent->blockMap.at(nextBlock); + bp.precision = afterInst.precision; + range->setRange(bp.ptr->getFirstInstruction()); +} + +void Cooddy::AfterInstLoc::isInsideInternal( + BlockWithPrecision &bp, const InstrWithPrecision &afterInst) const { + if (afterInst.ptr->inst->getOpcode() != opCode) { + bp.precision = std::min(afterInst.precision, Precision::Column); + return; } + bp.precision = Precision::Instruction; + range->setRange(afterInst.ptr); } std::string Location::toString() const { - return filename + ":" + std::to_string(startLine); + return filename + ":" + range->toString(); } } // namespace klee diff --git a/lib/Module/Target.cpp b/lib/Module/Target.cpp index d2dde07919..02167f902a 100644 --- a/lib/Module/Target.cpp +++ b/lib/Module/Target.cpp @@ -20,21 +20,6 @@ using namespace llvm; using namespace klee; -namespace klee { -llvm::cl::opt LocationAccuracy( - "location-accuracy", cl::init(false), - cl::desc("Check location with line and column accuracy (default=false)")); -} - -ErrorLocation::ErrorLocation(const klee::ref &loc) - : startLine(loc->startLine), endLine(loc->endLine), - startColumn(loc->startColumn), endColumn(loc->endColumn) {} - -ErrorLocation::ErrorLocation(const KInstruction *ki) { - startLine = (endLine = ki->getLine()); - startColumn = (endColumn = ki->getLine()); -} - std::string ReproduceErrorTarget::toString() const { std::ostringstream repr; repr << "Target " << getId() << ": "; @@ -75,10 +60,9 @@ ref Target::createCachedTarget(ref target) { return (ref)*(success.first); } -ref -ReproduceErrorTarget::create(const std::vector &_errors, - const std::string &_id, ErrorLocation _loc, - KBlock *_block) { +ref ReproduceErrorTarget::create(const ReachWithErrors &_errors, + const std::string &_id, + LineColumnRange _loc, KBlock *_block) { ReproduceErrorTarget *target = new ReproduceErrorTarget(_errors, _id, _loc, _block); return createCachedTarget(target); @@ -100,13 +84,8 @@ ref CoverBranchTarget::create(KBlock *_block, unsigned _branchCase) { return createCachedTarget(target); } -bool ReproduceErrorTarget::isTheSameAsIn(const KInstruction *instr) const { - const auto &errLoc = loc; - return instr->getLine() >= errLoc.startLine && - instr->getLine() <= errLoc.endLine && - (!LocationAccuracy || !errLoc.startColumn.has_value() || - (instr->getColumn() >= *errLoc.startColumn && - instr->getColumn() <= *errLoc.endColumn)); +bool ReproduceErrorTarget::isTheSameAsIn(KInstruction *instr) const { + return loc.hasInside(instr); } int Target::compare(const Target &b) const { return internalCompare(b); } diff --git a/lib/Module/TargetForest.cpp b/lib/Module/TargetForest.cpp index cb2f8a907e..655b83baf4 100644 --- a/lib/Module/TargetForest.cpp +++ b/lib/Module/TargetForest.cpp @@ -118,7 +118,7 @@ void TargetForest::Layer::addTrace( ref target = nullptr; if (i == result.locations.size() - 1) { target = ReproduceErrorTarget::create(result.errors, result.id, - ErrorLocation(loc), block); + loc->range->getRange(), block); } else { target = ReachBlockTarget::create(block); } diff --git a/test/Industry/MacroLocalization.c b/test/Industry/MacroLocalization.c new file mode 100644 index 0000000000..65f8c92b69 --- /dev/null +++ b/test/Industry/MacroLocalization.c @@ -0,0 +1,27 @@ +#include + +#define RETURN_NULL_OTHERWISE(sth) if ((sth) != 42) { \ + return NULL; \ + } + +int *foo(int *status) { + int st = *status; + RETURN_NULL_OTHERWISE(st); + return status; +} + +int main(int x) { + int *result = foo(&x); + return *result; +} + +// REQUIRES: z3 +// RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --debug-localization --location-accuracy --analysis-reproduce=%s.sarif %t1.bc 2>&1 | FileCheck %s + +// CHECK: Industry/MacroLocalization.c:15-15 # 1 +// CHECK: Industry/MacroLocalization.c:9:3-9:28 1 # 2 +// CHECK: Industry/MacroLocalization.c:9:3-9:3 33 # 3 +// CHECK: Industry/MacroLocalization.c:14:17-14:17 56 # 3 +// CHECK: KLEE: WARNING: 100.00% NullPointerException True Positive at trace bc7beead5f814c9deac02e8e9e6eef08 diff --git a/test/Industry/MacroLocalization.c.sarif b/test/Industry/MacroLocalization.c.sarif new file mode 100644 index 0000000000..4e97a41888 --- /dev/null +++ b/test/Industry/MacroLocalization.c.sarif @@ -0,0 +1,155 @@ +{ + "$schema": "https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json", + "version": "2.1.0", + "runs": [ + { + "tool": { + "driver": { + "name": "Cooddy", + "version": "v1_101", + "properties": { + "revisionTag": "bbceeffcbd252fd8a86aa2ed68549f3d713505ac" + } + } + }, + "invocations": [ + { + "executionSuccessful": true, + "exitCode": 0, + "commandLine": "build/release/cooddy --scope /home/user/pool --reporter sarif", + "executableLocation": { + "uri": "file:///home/user/src/cooddy/build/release/cooddy" + }, + "arguments": [ + "--scope", + "/home/user/pool", + "--reporter", + "sarif" + ], + "properties": { + "profileUri": "file:///home/user/src/cooddy/build/release/.cooddy/default.profile.json", + "annotationUris": [ + "file:///home/user/src/cooddy/build/release/.cooddy/.annotations.json", + "file:///home/user/src/cooddy/build/release/.cooddy/.java-annotations.json", + "file:///home/user/src/cooddy/build/release/.cooddy/.tinyxml-annotations.json", + "file:///home/user/src/cooddy/build/release/.cooddy/.huawei-annotations.json" + ] + }, + "startTimeUtc": "2023-07-05T13:43:00.892Z", + "endTimeUtc": "2023-07-05T13:50:26.467Z" + } + ], + "columnKind": "unicodeCodePoints", + "results": [ + { + "message": { + "text": "Dereferencing of \"result\" which can be null" + }, + "level": "error", + "ruleId": "NULL.DEREF", + "fingerprints": { + "cooddy.uid": "bc7beead5f814c9deac02e8e9e6eef08" + }, + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "Industry/MacroLocalization.c" + }, + "region": { + "startLine": 15, + "endLine": 15, + "startColumn": 11, + "endColumn": 17 + } + } + } + ], + "codeFlows": [ + { + "threadFlows": [ + { + "locations": [ + { + "location": { + "physicalLocation": { + "artifactLocation": { + "uri": "Industry/MacroLocalization.c" + }, + "region": { + "startLine": 9, + "endLine": 9, + "startColumn": 3, + "endColumn": 28, + "message": { + "text": "Null pointer source" + } + } + } + } + }, + { + "location": { + "physicalLocation": { + "artifactLocation": { + "uri": "Industry/MacroLocalization.c" + }, + "region": { + "startLine": 9, + "endLine": 9, + "startColumn": 3, + "endColumn": 28, + "message": { + "text": "Assume return here" + } + } + } + } + }, + { + "location": { + "physicalLocation": { + "artifactLocation": { + "uri": "Industry/MacroLocalization.c" + }, + "region": { + "startLine": 14, + "endLine": 14, + "startColumn": 17, + "endColumn": 23, + "message": { + "text": "Null pointer returned as the result" + } + } + } + } + }, + { + "location": { + "physicalLocation": { + "artifactLocation": { + "uri": "Industry/MacroLocalization.c" + }, + "region": { + "startLine": 15, + "endLine": 15, + "startColumn": 11, + "endColumn": 17, + "message": { + "text": "Dereferencing of \"result\" which can be null" + } + } + } + } + } + ] + } + ] + } + ], + "verdict": "TP" + } + ] + } + ] +} \ No newline at end of file diff --git a/test/Industry/StrangeBugInIFDS.c b/test/Industry/StrangeBugInIFDS.c new file mode 100644 index 0000000000..5f055a7f9c --- /dev/null +++ b/test/Industry/StrangeBugInIFDS.c @@ -0,0 +1,27 @@ +#include +#include + +typedef struct { int magic; } Struct; + +void Exec(void **para) { + if (para == NULL) + return; // event 3 + *para = malloc(sizeof(Struct)); +} + +void* Alloc() { + void *buf = NULL; // event 1 + Exec(&buf); // event 2 + return buf; // event 4 +} + +void Init() { + Struct *p = Alloc(); + p->magic = 42; // event 5| +} +// REQUIRES: z3 +// RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --analysis-reproduce=%s.sarif %t1.bc 2>&1 | FileCheck %s + +// CHECK: KLEE: WARNING: 100.00% (MayBeNullPointerException|NullPointerException) False Positive at trace somebigid123 diff --git a/test/Industry/StrangeBugInIFDS.c.sarif b/test/Industry/StrangeBugInIFDS.c.sarif new file mode 100644 index 0000000000..37a925b760 --- /dev/null +++ b/test/Industry/StrangeBugInIFDS.c.sarif @@ -0,0 +1,173 @@ +{ + "$schema": "https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json", + "version": "2.1.0", + "runs": [ + { + "tool": { + "driver": { + "name": "Cooddy", + "version": "v1_101", + "properties": { + "revisionTag": "bbceeffcbd252fd8a86aa2ed68549f3d713505ac" + } + } + }, + "invocations": [ + { + "executionSuccessful": true, + "exitCode": 0, + "commandLine": "build/release/cooddy --scope /home/user/pool --reporter sarif", + "executableLocation": { + "uri": "file:///home/user/src/cooddy/build/release/cooddy" + }, + "arguments": [ + "--scope", + "/home/user/pool", + "--reporter", + "sarif" + ], + "properties": { + "profileUri": "file:///home/user/src/cooddy/build/release/.cooddy/default.profile.json", + "annotationUris": [ + "file:///home/user/src/cooddy/build/release/.cooddy/.annotations.json", + "file:///home/user/src/cooddy/build/release/.cooddy/.java-annotations.json", + "file:///home/user/src/cooddy/build/release/.cooddy/.tinyxml-annotations.json", + "file:///home/user/src/cooddy/build/release/.cooddy/.huawei-annotations.json" + ] + }, + "startTimeUtc": "2023-07-05T13:43:00.892Z", + "endTimeUtc": "2023-07-05T13:50:26.467Z" + } + ], + "columnKind": "unicodeCodePoints", + "results": [ + { + "message": { + "text": "Dereferencing of \"p\" which can be null" + }, + "level": "error", + "ruleId": "NULL.DEREF", + "fingerprints": { + "cooddy.uid": "somebigid123" + }, + "locations": [ + { + "physicalLocation": { + "artifactLocation": { + "uri": "Industry/StrangeBugInIFDS.c" + }, + "region": { + "startLine": 19, + "endLine": 19, + "startColumn": 3, + "endColumn": 4 + } + } + } + ], + "codeFlows": [ + { + "threadFlows": [ + { + "locations": [ + { + "location": { + "physicalLocation": { + "artifactLocation": { + "uri": "Industry/StrangeBugInIFDS.c" + }, + "region": { + "startLine": 6, + "endLine": 6, + "startColumn": 15, + "endColumn": 19, + "message": { + "text": "Null pointer source" + } + } + } + } + }, + { + "location": { + "physicalLocation": { + "artifactLocation": { + "uri": "Industry/StrangeBugInIFDS.c" + }, + "region": { + "startLine": 7, + "endLine": 7, + "startColumn": 8, + "endColumn": 12, + "message": { + "text": "Null pointer passed as 1st argument" + } + } + } + } + }, + { + "location": { + "physicalLocation": { + "artifactLocation": { + "uri": "Industry/StrangeBugInIFDS.c" + }, + "region": { + "startLine": 13, + "endLine": 13, + "startColumn": 5, + "endColumn": 11, + "message": { + "text": "Assume return here" + } + } + } + } + }, + { + "location": { + "physicalLocation": { + "artifactLocation": { + "uri": "Industry/StrangeBugInIFDS.c" + }, + "region": { + "startLine": 8, + "endLine": 8, + "startColumn": 10, + "endColumn": 13, + "message": { + "text": "Null pointer returned as the result" + } + } + } + } + }, + { + "location": { + "physicalLocation": { + "artifactLocation": { + "uri": "Industry/StrangeBugInIFDS.c" + }, + "region": { + "startLine": 19, + "endLine": 19, + "startColumn": 3, + "endColumn": 4, + "message": { + "text": "Dereferencing of \"p\" which can be null" + } + } + } + } + } + ] + } + ] + } + ], + "verdict": "TP" + } + ] + } + ] +} \ No newline at end of file diff --git a/test/Industry/if2.c b/test/Industry/if2.c index d52edf529f..55695c0edb 100644 --- a/test/Industry/if2.c +++ b/test/Industry/if2.c @@ -11,7 +11,7 @@ int main(int x) { // REQUIRES: z3 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --search=bfs --max-stepped-instructions=20 --max-cycles-before-stuck=0 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --search=bfs --max-stepped-instructions=19 --max-cycles-before-stuck=0 --location-accuracy --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s -check-prefix=CHECK-NONE // CHECK-NONE: KLEE: WARNING: 50.00% NullPointerException False Positive at trace 1 // RUN: FileCheck -input-file=%t.klee-out/messages.txt %s -check-prefix=CHECK-DISTANCE