diff --git a/build.sh b/build.sh index 12f4182699..7108975de4 100755 --- a/build.sh +++ b/build.sh @@ -1,35 +1,51 @@ -#!/bin/bash -# This script is used to build KLEE as UTBot backend - -set -e -set -o pipefail -mkdir -p build -cd build - -$UTBOT_CMAKE_BINARY -G Ninja \ - -DCMAKE_PREFIX_PATH=$UTBOT_INSTALL_DIR/lib/cmake/z3 \ - -DCMAKE_LIBRARY_PATH=$UTBOT_INSTALL_DIR/lib \ - -DCMAKE_INCLUDE_PATH=$UTBOT_INSTALL_DIR/include \ - -DENABLE_SOLVER_Z3=TRUE \ - -DENABLE_POSIX_RUNTIME=TRUE \ - -DENABLE_KLEE_UCLIBC=ON \ - -DKLEE_UCLIBC_PATH=$UTBOT_ALL/klee-uclibc \ - -DENABLE_FLOATING_POINT=TRUE \ - -DENABLE_FP_RUNTIME=TRUE \ - -DLLVM_CONFIG_BINARY=$UTBOT_INSTALL_DIR/bin/llvm-config \ - -DLLVMCC=/utbot_distr/install/bin/clang \ - -DLLVMCXX=/utbot_distr/install/bin/clang++ \ - -DENABLE_UNIT_TESTS=TRUE \ - -DENABLE_SYSTEM_TESTS=TRUE \ - -DGTEST_SRC_DIR=$UTBOT_ALL/gtest \ - -DGTEST_INCLUDE_DIR=$UTBOT_ALL/gtest/googletest/include \ - -DCMAKE_INSTALL_PREFIX=$UTBOT_ALL/klee \ - -DENABLE_KLEE_LIBCXX=TRUE \ - -DKLEE_LIBCXX_DIR=$UTBOT_ALL/libcxx/install \ - -DKLEE_LIBCXX_INCLUDE_DIR=$UTBOT_ALL/libcxx/install/include/c++/v1 \ - -DENABLE_KLEE_EH_CXX=TRUE \ - -DKLEE_LIBCXXABI_SRC_DIR=$UTBOT_ALL/libcxx/libcxxabi \ - .. - -$UTBOT_CMAKE_BINARY --build . -$UTBOT_CMAKE_BINARY --install . +#!/bin/sh + +# For more build options, visit +# https://klee.github.io/build-script/ + +# Base folder where dependencies and KLEE itself are installed +BASE=$HOME/klee_build + +## KLEE Required options +# Build type for KLEE. The options are: +# Release +# Release+Debug +# Release+Asserts +# Release+Debug+Asserts +# Debug +# Debug+Asserts +# KLEE_RUNTIME_BUILD="Debug+Asserts" +KLEE_RUNTIME_BUILD="Debug" # "Debug+Asserts" + +COVERAGE=0 +ENABLE_DOXYGEN=0 +USE_TCMALLOC=0 +USE_LIBCXX=1 +# Also required despite not being mentioned in the guide +SQLITE_VERSION="3370200" + + +## LLVM Required options +LLVM_VERSION=11 +ENABLE_OPTIMIZED=1 +ENABLE_DEBUG=0 +DISABLE_ASSERTIONS=1 +REQUIRES_RTTI=1 + +## Solvers Required options +# SOLVERS=STP +SOLVERS=Z3 + +## Google Test Required options +GTEST_VERSION=1.11.0 + +## UClibC Required options +UCLIBC_VERSION=klee_0_9_29 +# LLVM_VERSION is also required for UClibC + +## Z3 Required options +Z3_VERSION=4.8.15 +STP_VERSION=2.3.3 +MINISAT_VERSION=master + +BASE="$BASE" KLEE_RUNTIME_BUILD=$KLEE_RUNTIME_BUILD COVERAGE=$COVERAGE ENABLE_DOXYGEN=$ENABLE_DOXYGEN USE_TCMALLOC=$USE_TCMALLOC USE_LIBCXX=$USE_LIBCXX LLVM_VERSION=$LLVM_VERSION ENABLE_OPTIMIZED=$ENABLE_OPTIMIZED ENABLE_DEBUG=$ENABLE_DEBUG DISABLE_ASSERTIONS=$DISABLE_ASSERTIONS REQUIRES_RTTI=$REQUIRES_RTTI SOLVERS=$SOLVERS GTEST_VERSION=$GTEST_VERSION UCLIBC_VERSION=$UCLIBC_VERSION STP_VERSION=$STP_VERSION MINISAT_VERSION=$MINISAT_VERSION Z3_VERSION=$Z3_VERSION SQLITE_VERSION=$SQLITE_VERSION ./scripts/build/build.sh klee --install-system-deps diff --git a/configs/options.json b/configs/options.json new file mode 100644 index 0000000000..736bb70193 --- /dev/null +++ b/configs/options.json @@ -0,0 +1,45 @@ +{ + "inputs" : { + "buildPath" : "", + "sarifTracesFilePath" : ".json", + "bytecodeFilePath" : ".bc", + "maxTime" : "240", + "maxSolverTime" : "5", + "maxForks" : "200", + "maxSymAlloc" : "32", + "symbolicAllocationThreshhold" : "2048" + }, + "configurations": [ + { + "program": "${buildPath}/bin/klee", + "args": [ + "--use-guided-search=error", + "--mock-external-calls", + "--posix-runtime", + "--check-out-of-memory", + "--suppress-external-warnings", + "--libc=klee", + "--skip-not-lazy-initialized", + "--external-calls=all", + "--output-source=false", + "--output-istats=false", + "--output-stats=false", + "--max-time=${maxTime}s", + "--max-sym-alloc=${maxSymAlloc}", + "--max-forks=${maxForks}", + "--max-solver-time=${maxSolverTime}s", + "--mock-all-externals", + "--smart-resolve-entry-function", + "--extern-calls-can-return-null", + "--align-symbolic-pointers=false", + "--write-no-tests", + "--write-kpaths", + "--use-lazy-initialization=only", + "--rewrite-equalities=simple", + "--symbolic-allocation-threshhold=${symbolicAllocationThreshhold}", + "--analysis-reproduce=${sarifTracesFilePath}", + "${bytecodeFilePath}" + ] + } + ] +} \ No newline at end of file diff --git a/include/klee/Expr/ExprEvaluator.h b/include/klee/Expr/ExprEvaluator.h index 93a78eb82b..cafecaa45f 100644 --- a/include/klee/Expr/ExprEvaluator.h +++ b/include/klee/Expr/ExprEvaluator.h @@ -17,15 +17,16 @@ namespace klee { class ExprEvaluator : public ExprVisitor { protected: Action evalRead(const UpdateList &ul, unsigned index); - Action visitRead(const ReadExpr &re); - Action visitExpr(const Expr &e); + Action visitRead(const ReadExpr &re) override; + Action visitSelect(const SelectExpr &se) override; + Action visitExpr(const Expr &e) override; Action protectedDivOperation(const BinaryExpr &e); - Action visitUDiv(const UDivExpr &e); - Action visitSDiv(const SDivExpr &e); - Action visitURem(const URemExpr &e); - Action visitSRem(const SRemExpr &e); - Action visitExprPost(const Expr &e); + Action visitUDiv(const UDivExpr &e) override; + Action visitSDiv(const SDivExpr &e) override; + Action visitURem(const URemExpr &e) override; + Action visitSRem(const SRemExpr &e) override; + Action visitExprPost(const Expr &e) override; public: ExprEvaluator() {} diff --git a/include/klee/Expr/Symcrete.h b/include/klee/Expr/Symcrete.h index aacfa44b83..c8ebab70c0 100644 --- a/include/klee/Expr/Symcrete.h +++ b/include/klee/Expr/Symcrete.h @@ -84,7 +84,10 @@ typedef std::set, SymcreteLess> SymcreteOrderedSet; class AddressSymcrete : public Symcrete { public: - AddressSymcrete(ref s, SymcreteKind kind) : Symcrete(s, kind) { + const Array *addressArray; + + AddressSymcrete(const Array *_addressArray, ref s, SymcreteKind kind) + : Symcrete(s, kind), addressArray(_addressArray) { assert((kind == SymcreteKind::SK_ALLOC_ADDRESS || kind == SymcreteKind::SK_LI_ADDRESS) && "wrong kind"); @@ -98,8 +101,8 @@ class AddressSymcrete : public Symcrete { class AllocAddressSymcrete : public AddressSymcrete { public: - AllocAddressSymcrete(ref s) - : AddressSymcrete(s, SymcreteKind::SK_ALLOC_ADDRESS) {} + AllocAddressSymcrete(const Array *addressArray, ref s) + : AddressSymcrete(addressArray, s, SymcreteKind::SK_ALLOC_ADDRESS) {} static bool classof(const Symcrete *symcrete) { return symcrete->getKind() == SymcreteKind::SK_ALLOC_ADDRESS; @@ -108,8 +111,8 @@ class AllocAddressSymcrete : public AddressSymcrete { class LazyInitializedAddressSymcrete : public AddressSymcrete { public: - LazyInitializedAddressSymcrete(ref s) - : AddressSymcrete(s, SymcreteKind::SK_LI_ADDRESS) {} + LazyInitializedAddressSymcrete(const Array *addressArray, ref s) + : AddressSymcrete(addressArray, s, SymcreteKind::SK_LI_ADDRESS) {} static bool classof(const Symcrete *symcrete) { return symcrete->getKind() == SymcreteKind::SK_LI_ADDRESS; diff --git a/include/klee/Module/TargetForest.h b/include/klee/Module/TargetForest.h index 91cd347309..eac93e8ef4 100644 --- a/include/klee/Module/TargetForest.h +++ b/include/klee/Module/TargetForest.h @@ -298,6 +298,7 @@ class TargetForest { void add(ref); void remove(ref); void blockIn(ref, ref); + void block(const ref &); const ref getHistory() { return history; }; const ref getTargets() { return forest; }; void dump() const; diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt index 202fa2fcec..b064c749f3 100644 --- a/lib/Core/CMakeLists.txt +++ b/lib/Core/CMakeLists.txt @@ -13,6 +13,7 @@ klee_add_component(kleeCore Context.cpp CoreStats.cpp CXXTypeSystem/CXXTypeManager.cpp + DistanceCalculator.cpp ExecutionState.cpp Executor.cpp ExecutorUtil.cpp diff --git a/lib/Core/DistanceCalculator.cpp b/lib/Core/DistanceCalculator.cpp new file mode 100644 index 0000000000..b87fbcf18a --- /dev/null +++ b/lib/Core/DistanceCalculator.cpp @@ -0,0 +1,210 @@ +//===-- DistanceCalculator.cpp --------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include "DistanceCalculator.h" +#include "ExecutionState.h" +#include "klee/Module/CodeGraphDistance.h" +#include "klee/Module/KInstruction.h" +#include "klee/Module/Target.h" + +using namespace llvm; +using namespace klee; + +DistanceResult DistanceCalculator::getDistance(ExecutionState &es, + ref target) { + return getDistance(es.pc, es.prevPC, es.initPC, es.stack, es.error, target); +} + +DistanceResult +DistanceCalculator::getDistance(KInstruction *pc, KInstruction *prevPC, + KInstruction *initPC, + const ExecutionState::stack_ty &stack, + ReachWithError error, ref target) { + weight_type weight = 0; + + BasicBlock *pcBlock = pc->inst->getParent(); + BasicBlock *prevPCBlock = prevPC->inst->getParent(); + + if (!target->shouldFailOnThisTarget() && target->atReturn()) { + if (prevPC->parent == target->getBlock() && + prevPC == target->getBlock()->getLastInstruction()) { + return DistanceResult(Done); + } else if (pc->parent == target->getBlock()) { + return DistanceResult(Continue); + } + } + + if (target->shouldFailOnThisTarget() && target->isTheSameAsIn(prevPC) && + target->isThatError(error)) { + return DistanceResult(Done); + } + + BasicBlock *bb = pcBlock; + KBlock *kb = pc->parent->parent->blockMap[bb]; + const auto &distanceToTargetFunction = + codeGraphDistance.getBackwardDistance(target->getBlock()->parent); + unsigned int minCallWeight = UINT_MAX, minSfNum = UINT_MAX, sfNum = 0; + for (auto sfi = stack.rbegin(), sfe = stack.rend(); sfi != sfe; sfi++) { + unsigned callWeight; + if (distanceInCallGraph(sfi->kf, kb, callWeight, distanceToTargetFunction, + target)) { + callWeight *= 2; + if (callWeight == 0 && target->shouldFailOnThisTarget()) { + return target->isTheSameAsIn(kb->getFirstInstruction()) && + target->isThatError(error) + ? DistanceResult(Done) + : DistanceResult(Continue); + } else { + callWeight += sfNum; + } + + if (callWeight < minCallWeight) { + minCallWeight = callWeight; + minSfNum = sfNum; + } + } + + if (sfi->caller) { + kb = sfi->caller->parent; + bb = kb->basicBlock; + } + sfNum++; + + if (minCallWeight < sfNum) + break; + } + + WeightResult res = Miss; + bool isInsideFunction = true; + if (minCallWeight == 0) { + res = tryGetTargetWeight(pc, initPC, pcBlock, prevPCBlock, weight, target); + } else if (minSfNum == 0) { + res = tryGetPreTargetWeight(pc, initPC, pcBlock, prevPCBlock, weight, + distanceToTargetFunction, target); + isInsideFunction = false; + } else if (minSfNum != UINT_MAX) { + res = tryGetPostTargetWeight(pc, initPC, pcBlock, prevPCBlock, weight, + target); + isInsideFunction = false; + } + if (Done == res && target->shouldFailOnThisTarget()) { + if (!target->isThatError(error)) { + res = Continue; + } + } + + return DistanceResult(res, weight, isInsideFunction); +} + +bool DistanceCalculator::distanceInCallGraph( + KFunction *kf, KBlock *kb, unsigned int &distance, + const std::unordered_map + &distanceToTargetFunction, + ref target) { + distance = UINT_MAX; + const std::unordered_map &dist = + codeGraphDistance.getDistance(kb); + KBlock *targetBB = target->getBlock(); + KFunction *targetF = targetBB->parent; + + if (kf == targetF && dist.count(targetBB) != 0) { + distance = 0; + return true; + } + + for (auto &kCallBlock : kf->kCallBlocks) { + if (dist.count(kCallBlock) != 0) { + for (auto &calledFunction : kCallBlock->calledFunctions) { + KFunction *calledKFunction = kf->parent->functionMap[calledFunction]; + if (distanceToTargetFunction.count(calledKFunction) != 0 && + distance > distanceToTargetFunction.at(calledKFunction) + 1) { + distance = distanceToTargetFunction.at(calledKFunction) + 1; + } + } + } + } + return distance != UINT_MAX; +} + +WeightResult DistanceCalculator::tryGetLocalWeight( + KInstruction *pc, KInstruction *initPC, BasicBlock *pcBlock, + BasicBlock *prevPCBlock, weight_type &weight, + const std::vector &localTargets, ref target) { + KFunction *currentKF = pc->parent->parent; + KBlock *initKB = initPC->parent; + KBlock *currentKB = currentKF->blockMap[pcBlock]; + KBlock *prevKB = currentKF->blockMap[prevPCBlock]; + const std::unordered_map &dist = + codeGraphDistance.getDistance(currentKB); + weight = UINT_MAX; + for (auto &end : localTargets) { + if (dist.count(end) > 0) { + unsigned int w = dist.at(end); + weight = std::min(w, weight); + } + } + + if (weight == UINT_MAX) + return Miss; + if (weight == 0 && (initKB == currentKB || prevKB != currentKB || + target->shouldFailOnThisTarget())) { + return Done; + } + + return Continue; +} + +WeightResult DistanceCalculator::tryGetPreTargetWeight( + KInstruction *pc, KInstruction *initPC, BasicBlock *pcBlock, + BasicBlock *prevPCBlock, weight_type &weight, + const std::unordered_map + &distanceToTargetFunction, + ref target) { + KFunction *currentKF = pc->parent->parent; + std::vector localTargets; + for (auto &kCallBlock : currentKF->kCallBlocks) { + for (auto &calledFunction : kCallBlock->calledFunctions) { + KFunction *calledKFunction = + currentKF->parent->functionMap[calledFunction]; + if (distanceToTargetFunction.count(calledKFunction) > 0) { + localTargets.push_back(kCallBlock); + } + } + } + + if (localTargets.empty()) + return Miss; + + WeightResult res = tryGetLocalWeight(pc, initPC, pcBlock, prevPCBlock, weight, + localTargets, target); + return res == Done ? Continue : res; +} + +WeightResult DistanceCalculator::tryGetPostTargetWeight( + KInstruction *pc, KInstruction *initPC, BasicBlock *pcBlock, + BasicBlock *prevPCBlock, weight_type &weight, ref target) { + KFunction *currentKF = pc->parent->parent; + std::vector &localTargets = currentKF->returnKBlocks; + + if (localTargets.empty()) + return Miss; + + WeightResult res = tryGetLocalWeight(pc, initPC, pcBlock, prevPCBlock, weight, + localTargets, target); + return res == Done ? Continue : res; +} + +WeightResult DistanceCalculator::tryGetTargetWeight( + KInstruction *pc, KInstruction *initPC, BasicBlock *pcBlock, + BasicBlock *prevPCBlock, weight_type &weight, ref target) { + std::vector localTargets = {target->getBlock()}; + WeightResult res = tryGetLocalWeight(pc, initPC, pcBlock, prevPCBlock, weight, + localTargets, target); + return res; +} diff --git a/lib/Core/DistanceCalculator.h b/lib/Core/DistanceCalculator.h new file mode 100644 index 0000000000..8f46a3696c --- /dev/null +++ b/lib/Core/DistanceCalculator.h @@ -0,0 +1,83 @@ +//===-- DistanceCalculator.h ------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_DISTANCE_CALCULATOR_H +#define KLEE_DISTANCE_CALCULATOR_H + +#include "ExecutionState.h" + +namespace llvm { +class BasicBlock; +} // namespace llvm + +namespace klee { +class CodeGraphDistance; +struct Target; + +enum WeightResult : std::uint8_t { + Continue, + Done, + Miss, +}; + +using weight_type = unsigned; + +struct DistanceResult { + WeightResult result; + weight_type weight; + bool isInsideFunction; + + explicit DistanceResult(WeightResult result_, weight_type weight_ = 0, + bool isInsideFunction_ = true) + : result(result_), weight(weight_), isInsideFunction(isInsideFunction_) {} +}; + +class DistanceCalculator { +public: + explicit DistanceCalculator(CodeGraphDistance &codeGraphDistance_) + : codeGraphDistance(codeGraphDistance_) {} + + DistanceResult getDistance(ExecutionState &es, ref target); + DistanceResult getDistance(KInstruction *pc, KInstruction *prevPC, + KInstruction *initPC, + const ExecutionState::stack_ty &stack, + ReachWithError error, ref target); + +private: + CodeGraphDistance &codeGraphDistance; + + bool distanceInCallGraph(KFunction *kf, KBlock *kb, unsigned int &distance, + const std::unordered_map + &distanceToTargetFunction, + ref target); + WeightResult tryGetLocalWeight(KInstruction *pc, KInstruction *initPC, + llvm::BasicBlock *pcBlock, + llvm::BasicBlock *prevPCBlock, + weight_type &weight, + const std::vector &localTargets, + ref target); + WeightResult + tryGetPreTargetWeight(KInstruction *pc, KInstruction *initPC, + llvm::BasicBlock *pcBlock, + llvm::BasicBlock *prevPCBlock, weight_type &weight, + const std::unordered_map + &distanceToTargetFunction, + ref target); + WeightResult tryGetTargetWeight(KInstruction *pc, KInstruction *initPC, + llvm::BasicBlock *pcBlock, + llvm::BasicBlock *prevPCBlock, + weight_type &weight, ref target); + WeightResult tryGetPostTargetWeight(KInstruction *pc, KInstruction *initPC, + llvm::BasicBlock *pcBlock, + llvm::BasicBlock *prevPCBlock, + weight_type &weight, ref target); +}; +} // namespace klee + +#endif /* KLEE_DISTANCE_CALCULATOR_H */ diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 909d4b64f0..38012e861e 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -277,6 +277,14 @@ void ExecutionState::removePointerResolutions(const MemoryObject *mo) { } } +void ExecutionState::removePointerResolutions(ref address, + unsigned size) { + if (!isa(address)) { + resolvedPointers[address].clear(); + resolvedSubobjects[MemorySubobject(address, size)].clear(); + } +} + // base address mo and ignore non pure reads in setinitializationgraph void ExecutionState::addPointerResolution(ref address, const MemoryObject *mo, @@ -287,6 +295,16 @@ void ExecutionState::addPointerResolution(ref address, } } +void ExecutionState::addUniquePointerResolution(ref address, + const MemoryObject *mo, + unsigned size) { + if (!isa(address)) { + removePointerResolutions(address, size); + resolvedPointers[address].insert(mo->id); + resolvedSubobjects[MemorySubobject(address, size)].insert(mo->id); + } +} + bool ExecutionState::resolveOnSymbolics(const ref &addr, IDType &result) const { uint64_t address = addr->getZExtValue(); @@ -386,10 +404,12 @@ void ExecutionState::increaseLevel() { KModule *kmodule = kf->parent; if (prevPC->inst->isTerminator() && kmodule->inMainModule(kf->function)) { - multilevel.insert(srcbb); + multilevel[srcbb]++; level.insert(srcbb); } - transitionLevel.insert(std::make_pair(srcbb, dstbb)); + if (srcbb != dstbb) { + transitionLevel.insert(std::make_pair(srcbb, dstbb)); + } } bool ExecutionState::isTransfered() { return getPrevPCBlock() != getPCBlock(); } diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index 8d9db68d2b..d15170bbd5 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -31,6 +31,7 @@ #include #include #include +#include #include #include #include @@ -203,6 +204,8 @@ class ExecutionState { public: using stack_ty = std::vector; + using TargetHashSet = + std::unordered_set, RefTargetHash, RefTargetCmp>; // Execution - Control Flow specific @@ -232,7 +235,7 @@ class ExecutionState { std::uint32_t depth = 0; /// @brief Exploration level, i.e., number of times KLEE cycled for this state - std::unordered_multiset multilevel; + std::unordered_map multilevel; std::unordered_set level; std::unordered_set transitionLevel; @@ -361,8 +364,11 @@ class ExecutionState { std::pair, ref> &resolution) const; void removePointerResolutions(const MemoryObject *mo); + void removePointerResolutions(ref address, unsigned size); void addPointerResolution(ref address, const MemoryObject *mo, unsigned size = 0); + void addUniquePointerResolution(ref address, const MemoryObject *mo, + unsigned size = 0); bool resolveOnSymbolics(const ref &addr, IDType &result) const; void addConstraint(ref e, const Assignment &c); diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index e42a4a5bb8..610d853911 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -13,6 +13,7 @@ #include "CXXTypeSystem/CXXTypeManager.h" #include "Context.h" #include "CoreStats.h" +#include "DistanceCalculator.h" #include "ExecutionState.h" #include "ExternalDispatcher.h" #include "GetElementPtrTypeIterator.h" @@ -162,12 +163,6 @@ cl::opt "to the used type system (default=true)"), cl::init(true), cl::cat(ExecCat)); -cl::opt - OutOfMemAllocs("out-of-mem-allocs", - cl::desc("Model malloc behavior, i.e. model NULL on 0 " - "or huge symbolic allocations."), - cl::init(false), cl::cat(ExecCat)); - cl::opt ExternCallsCanReturnNull("extern-calls-can-return-null", cl::init(false), cl::desc("Enable case when extern call can crash " @@ -408,7 +403,7 @@ bool allLeafsAreConstant(const ref &expr) { ArrayExprHelper::collectAlternatives(*sel, alternatives); for (auto leaf : alternatives) { - if (!isa(expr)) { + if (!isa(leaf)) { return false; } } @@ -446,6 +441,7 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, specialFunctionHandler(0), timers{time::Span(TimerInterval)}, concretizationManager(new ConcretizationManager(EqualitySubstitution)), codeGraphDistance(new CodeGraphDistance()), + distanceCalculator(new DistanceCalculator(*codeGraphDistance)), targetedExecutionManager(*codeGraphDistance), replayKTest(0), replayPath(0), usingSeeds(0), atMemoryLimit(false), inhibitForking(false), haltExecution(HaltExecution::NotHalt), ivcEnabled(false), @@ -1271,6 +1267,8 @@ Executor::StatePair Executor::fork(ExecutionState ¤t, ref condition, } void Executor::addConstraint(ExecutionState &state, ref condition) { + condition = + Simplificator::simplifyExpr(state.constraints.cs(), condition).simplified; if (ConstantExpr *CE = dyn_cast(condition)) { if (!CE->isTrue()) llvm::report_fatal_error("attempt to add invalid constraint"); @@ -4182,7 +4180,7 @@ void Executor::targetedRun(ExecutionState &initialState, KBlock *target, states.insert(&initialState); TargetedSearcher *targetedSearcher = - new TargetedSearcher(Target::create(target), *codeGraphDistance); + new TargetedSearcher(Target::create(target), *distanceCalculator); searcher = targetedSearcher; std::vector newStates(states.begin(), states.end()); @@ -4522,6 +4520,8 @@ void Executor::terminateStateOnExecError(ExecutionState &state, void Executor::terminateStateOnSolverError(ExecutionState &state, const llvm::Twine &message) { terminateStateOnError(state, message, StateTerminationType::Solver, ""); + SetOfStates states = {&state}; + decreaseConfidenceFromStoppedStates(states, HaltExecution::MaxSolverTime); } // XXX shoot me @@ -4800,10 +4800,12 @@ void Executor::executeAlloc(ExecutionState &state, ref size, bool isLocal, if (allocationAlignment == 0) { allocationAlignment = getAllocationAlignment(allocSite); } - ref upperBoundSizeConstraint = UleExpr::create( - ZExtExpr::create(size, Context::get().getPointerWidth()), - Expr::createPointer(isa(size) ? MaxConstantAllocationSize - : MaxSymbolicAllocationSize)); + ref upperBoundSizeConstraint = Expr::createTrue(); + if (!isa(size)) { + upperBoundSizeConstraint = UleExpr::create( + ZExtExpr::create(size, Context::get().getPointerWidth()), + Expr::createPointer(MaxSymbolicAllocationSize)); + } /* If size greater then upper bound for size, then we will follow the malloc semantic and return NULL. Otherwise continue execution. */ @@ -4819,6 +4821,10 @@ void Executor::executeAlloc(ExecutionState &state, ref size, bool isLocal, } if (inBounds != PValidity::MustBeFalse && inBounds != PValidity::MayBeFalse) { + if (inBounds != PValidity::MustBeTrue) { + addConstraint(state, upperBoundSizeConstraint); + } + MemoryObject *mo = allocate(state, size, isLocal, /*isGlobal=*/false, allocSite, allocationAlignment); if (!mo) { @@ -4839,21 +4845,8 @@ void Executor::executeAlloc(ExecutionState &state, ref size, bool isLocal, Expr::createPointer(0), address); } - if (inBounds == PValidity::MustBeTrue) { - bindLocal(target, state, address); - } else { - if (OutOfMemAllocs) { - ref isNull = EqExpr::create(address, Expr::createPointer(0)); - addConstraint(state, EqExpr::create(upperBoundSizeConstraint, - Expr::createIsZero(isNull))); - ref result = SelectExpr::create( - upperBoundSizeConstraint, address, Expr::createPointer(0)); - bindLocal(target, state, result); - } else { - addConstraint(state, upperBoundSizeConstraint); - bindLocal(target, state, address); - } - } + // state.addPointerResolution(address, mo); + bindLocal(target, state, address); if (reallocFrom) { unsigned count = std::min(reallocFrom->size, os->size); @@ -4865,7 +4858,7 @@ void Executor::executeAlloc(ExecutionState &state, ref size, bool isLocal, } } } else { - bindLocal(target, state, Expr::createPointer(0)); + terminateStateEarly(state, "", StateTerminationType::SilentExit); } } @@ -4911,31 +4904,74 @@ void Executor::executeFree(ExecutionState &state, ref address, } } -bool Executor::resolveExact(ExecutionState &state, ref p, KType *type, - ExactResolutionList &results, +bool Executor::resolveExact(ExecutionState &estate, ref address, + KType *type, ExactResolutionList &results, const std::string &name) { + ref base = address; + + if (estate.isGEPExpr(address)) { + base = estate.gepExprBases[address].first; + } + + if (SimplifySymIndices) { + if (!isa(address)) + address = Simplificator::simplifyExpr(estate.constraints.cs(), address) + .simplified; + if (!isa(base)) + base = + Simplificator::simplifyExpr(estate.constraints.cs(), base).simplified; + } + + address = optimizer.optimizeExpr(address, true); + base = optimizer.optimizeExpr(base, true); + + ref uniqueBase = + Simplificator::simplifyExpr(estate.constraints.cs(), base).simplified; + uniqueBase = toUnique(estate, uniqueBase); + + StatePair branches = + fork(estate, Expr::createIsZero(base), true, BranchType::MemOp); + ExecutionState *bound = branches.first; + if (bound) { + if (!isReadFromSymbolicArray(uniqueBase) || + guidanceKind != GuidanceKind::ErrorGuidance) { + terminateStateOnTargetError(*bound, ReachWithError::NullPointerException); + } else { + terminateStateEarly(*bound, "", StateTerminationType::SilentExit); + } + } + if (!branches.second) { + address = Expr::createPointer(0); + } + + ExecutionState &state = *branches.second; + ResolutionList rl; bool mayBeOutOfBound = true; bool hasLazyInitialized = false; bool incomplete = false; /* We do not need this variable here, just a placeholder for resolve */ - bool success = - resolveMemoryObjects(state, p, type, state.prevPC, 0, rl, mayBeOutOfBound, - hasLazyInitialized, incomplete); + bool success = resolveMemoryObjects( + state, address, type, state.prevPC, 0, rl, mayBeOutOfBound, + hasLazyInitialized, incomplete, + LazyInitialization == LazyInitializationPolicy::Only); assert(success); ExecutionState *unbound = &state; - for (ResolutionList::iterator it = rl.begin(), ie = rl.end(); it != ie; - ++it) { - const MemoryObject *mo = unbound->addressSpace.findObject(*it).first; - ref inBounds = EqExpr::create(p, mo->getBaseExpr()); - + for (unsigned i = 0; i < rl.size(); ++i) { + const MemoryObject *mo = unbound->addressSpace.findObject(rl.at(i)).first; + ref inBounds; + if (i + 1 == rl.size() && hasLazyInitialized) { + inBounds = Expr::createTrue(); + } else { + inBounds = EqExpr::create(address, mo->getBaseExpr()); + } StatePair branches = fork(*unbound, inBounds, true, BranchType::ResolvePointer); if (branches.first) - results.push_back(std::make_pair(*it, branches.first)); + results.push_back(std::make_pair(rl.at(i), branches.first)); unbound = branches.second; if (!unbound) // Fork failure @@ -4952,7 +4988,7 @@ bool Executor::resolveExact(ExecutionState &state, ref p, KType *type, } else { terminateStateOnError(*unbound, "memory error: invalid pointer: " + name, StateTerminationType::Ptr, - getAddressInfo(*unbound, p)); + getAddressInfo(*unbound, address)); } } return true; @@ -5038,8 +5074,9 @@ MemoryObject *Executor::allocate(ExecutionState &state, ref size, ref addressSymcrete = lazyInitializationSource ? cast( - new LazyInitializedAddressSymcrete(addressExpr)) - : cast(new AllocAddressSymcrete(addressExpr)); + new LazyInitializedAddressSymcrete(addressArray, addressExpr)) + : cast( + new AllocAddressSymcrete(addressArray, addressExpr)); ref sizeSymcrete = lazyInitializationSource ? cast(new LazyInitializedSizeSymcrete( @@ -5149,15 +5186,38 @@ bool Executor::resolveMemoryObjects( for (auto resolution : state.resolvedPointers.at(address)) { mayBeResolvedMemoryObjects.push_back(resolution); } + } else if (state.resolvedPointers.count(base)) { + for (auto resolution : state.resolvedPointers.at(base)) { + mayBeResolvedMemoryObjects.push_back(resolution); + } } else { // we are on an error path (no resolution, multiple resolution, one // resolution with out of bounds) - bool baseWasResolved = state.resolvedPointers.count(base) == 0; + bool baseWasNotResolved = state.resolvedPointers.count(base) == 0; address = optimizer.optimizeExpr(address, true); ref checkOutOfBounds = Expr::createTrue(); - if (!onlyLazyInitialize) { + ref baseUniqueExpr = toUnique(state, base); + + bool checkAddress = isa(address) || isa(address) || + state.isGEPExpr(address); + if (!checkAddress && isa(address)) { + checkAddress = true; + std::vector> alternatives; + ArrayExprHelper::collectAlternatives(*cast(address), + alternatives); + for (auto alt : alternatives) { + checkAddress &= isa(alt) || isa(alt) || + isa(alt) || state.isGEPExpr(alt); + } + } + + mayLazyInitialize = LazyInitialization != LazyInitializationPolicy::None && + !isa(baseUniqueExpr) && + baseWasNotResolved && checkAddress; + + if (!onlyLazyInitialize || !mayLazyInitialize) { ResolutionList rl; ResolutionList rlSkipped; @@ -5173,31 +5233,10 @@ bool Executor::resolveMemoryObjects( ref inBounds = mo->getBoundsCheckPointer(address, bytes); ref notInBounds = Expr::createIsZero(inBounds); mayBeResolvedMemoryObjects.push_back(mo->id); - state.addPointerResolution(address, mo); - state.addPointerResolution(base, mo); checkOutOfBounds = AndExpr::create(checkOutOfBounds, notInBounds); } } - ref baseUniqueExpr = toUnique(state, base); - - bool checkAddress = isa(address) || isa(address) || - state.isGEPExpr(address); - if (!checkAddress && isa(address)) { - checkAddress = true; - std::vector> alternatives; - ArrayExprHelper::collectAlternatives(*cast(address), - alternatives); - for (auto alt : alternatives) { - checkAddress &= isa(alt) || isa(alt) || - isa(alt) || state.isGEPExpr(alt); - } - } - - mayLazyInitialize = LazyInitialization != LazyInitializationPolicy::None && - !isa(baseUniqueExpr) && baseWasResolved && - checkAddress; - if (mayLazyInitialize) { solver->setTimeout(coreSolverTimeout); bool success = solver->mayBeTrue(state.constraints.cs(), checkOutOfBounds, @@ -5216,8 +5255,6 @@ bool Executor::resolveMemoryObjects( ObjectPair pa = state.addressSpace.findObject(idLazyInitialization); const MemoryObject *mo = pa.first; mayBeResolvedMemoryObjects.push_back(mo->id); - state.addPointerResolution(address, mo); - state.addPointerResolution(base, mo); } else { mayLazyInitialize = false; } @@ -5230,7 +5267,7 @@ bool Executor::resolveMemoryObjects( bool Executor::checkResolvedMemoryObjects( ExecutionState &state, ref address, KInstruction *target, unsigned bytes, const std::vector &mayBeResolvedMemoryObjects, - std::vector &resolvedMemoryObjects, + bool hasLazyInitialized, std::vector &resolvedMemoryObjects, std::vector> &resolveConditions, std::vector> &unboundConditions, ref &checkOutOfBounds, bool &mayBeOutOfBound) { @@ -5245,45 +5282,124 @@ bool Executor::checkResolvedMemoryObjects( } checkOutOfBounds = Expr::createTrue(); - for (unsigned int i = 0; i < mayBeResolvedMemoryObjects.size(); ++i) { + if (mayBeResolvedMemoryObjects.size() == 1) { const MemoryObject *mo = - state.addressSpace.findObject(mayBeResolvedMemoryObjects.at(i)).first; + state.addressSpace.findObject(*mayBeResolvedMemoryObjects.begin()) + .first; + + state.addPointerResolution(address, mo); + state.addPointerResolution(base, mo); ref inBounds = mo->getBoundsCheckPointer(address, bytes); ref baseInBounds = Expr::createTrue(); + ref notInBounds = Expr::createIsZero(inBounds); if (state.isGEPExpr(address)) { baseInBounds = AndExpr::create(baseInBounds, mo->getBoundsCheckPointer(base, size)); + } + + if (hasLazyInitialized) { baseInBounds = AndExpr::create( baseInBounds, Expr::createIsZero(mo->getOffsetExpr(base))); } - ref notInBounds = Expr::createIsZero(inBounds); + inBounds = AndExpr::create(inBounds, baseInBounds); + inBounds = optimizer.optimizeExpr(inBounds, true); + inBounds = Simplificator::simplifyExpr(state.constraints.cs(), inBounds) + .simplified; + notInBounds = + Simplificator::simplifyExpr(state.constraints.cs(), notInBounds) + .simplified; - bool mayBeInBounds; + PartialValidity result; solver->setTimeout(coreSolverTimeout); - bool success = solver->mayBeTrue(state.constraints.cs(), - AndExpr::create(inBounds, baseInBounds), - mayBeInBounds, state.queryMetaData); + bool success = solver->evaluate(state.constraints.cs(), inBounds, result, + state.queryMetaData); solver->setTimeout(time::Span()); if (!success) { return false; } - if (!mayBeInBounds) { - continue; + + mayBeOutOfBound = PValidity::MustBeFalse == result || + PValidity::MayBeFalse == result || + PValidity::TrueOrFalse == result; + bool mayBeInBound = PValidity::MustBeTrue == result || + PValidity::MayBeTrue == result || + PValidity::TrueOrFalse == result; + bool mustBeInBounds = PValidity::MustBeTrue == result; + bool mustBeOutOfBound = PValidity::MustBeFalse == result; + + if (mayBeInBound) { + state.addPointerResolution(address, mo, bytes); + state.addPointerResolution(base, mo, size); + resolvedMemoryObjects.push_back(mo->id); + if (mustBeInBounds) { + resolveConditions.push_back(Expr::createTrue()); + unboundConditions.push_back(Expr::createFalse()); + checkOutOfBounds = Expr::createFalse(); + } else { + resolveConditions.push_back(inBounds); + unboundConditions.push_back(notInBounds); + checkOutOfBounds = notInBounds; + } + } else if (mayBeOutOfBound) { + if (mustBeOutOfBound) { + checkOutOfBounds = Expr::createTrue(); + } else { + checkOutOfBounds = notInBounds; + } } + } else { + for (unsigned int i = 0; i < mayBeResolvedMemoryObjects.size(); ++i) { + const MemoryObject *mo = + state.addressSpace.findObject(mayBeResolvedMemoryObjects.at(i)).first; - state.addPointerResolution(address, mo, bytes); - state.addPointerResolution(base, mo, size); + state.addPointerResolution(address, mo); + state.addPointerResolution(base, mo); - inBounds = AndExpr::create(inBounds, baseInBounds); + ref inBounds = mo->getBoundsCheckPointer(address, bytes); + ref baseInBounds = Expr::createTrue(); + ref notInBounds = Expr::createIsZero(inBounds); - resolveConditions.push_back(inBounds); - resolvedMemoryObjects.push_back(mo->id); - unboundConditions.push_back(notInBounds); - if (mayBeOutOfBound) { - checkOutOfBounds = AndExpr::create(checkOutOfBounds, notInBounds); + if (state.isGEPExpr(address)) { + baseInBounds = AndExpr::create(baseInBounds, + mo->getBoundsCheckPointer(base, size)); + } + + if (hasLazyInitialized && i == mayBeResolvedMemoryObjects.size() - 1) { + baseInBounds = AndExpr::create( + baseInBounds, Expr::createIsZero(mo->getOffsetExpr(base))); + } + + inBounds = AndExpr::create(inBounds, baseInBounds); + inBounds = Simplificator::simplifyExpr(state.constraints.cs(), inBounds) + .simplified; + notInBounds = + Simplificator::simplifyExpr(state.constraints.cs(), notInBounds) + .simplified; + + bool mayBeInBounds; + solver->setTimeout(coreSolverTimeout); + bool success = solver->mayBeTrue(state.constraints.cs(), inBounds, + mayBeInBounds, state.queryMetaData); + solver->setTimeout(time::Span()); + if (!success) { + return false; + } + if (!mayBeInBounds) { + continue; + } + + state.addPointerResolution(address, mo, bytes); + state.addPointerResolution(base, mo, size); + + resolveConditions.push_back(inBounds); + resolvedMemoryObjects.push_back(mo->id); + unboundConditions.push_back(notInBounds); + if (mayBeOutOfBound) { + checkOutOfBounds = AndExpr::create(checkOutOfBounds, notInBounds); + } } } @@ -5296,9 +5412,11 @@ bool Executor::checkResolvedMemoryObjects( return false; } } + if (!mayBeOutOfBound) { checkOutOfBounds = Expr::createFalse(); } + return true; } @@ -5465,13 +5583,13 @@ void Executor::executeMemoryOperation( // fast path: single in-bounds resolution IDType idFastResult; - bool success; + bool success = false; - if (state->resolvedPointers.count(address) && - state->resolvedPointers.at(address).size() == 1) { + if (state->resolvedPointers.count(base) && + state->resolvedPointers.at(base).size() == 1) { success = true; - idFastResult = *state->resolvedPointers[address].begin(); - } else { + idFastResult = *state->resolvedPointers[base].begin(); + } else if (allLeafsAreConstant(address)) { solver->setTimeout(coreSolverTimeout); if (!state->addressSpace.resolveOne(*state, solver, address, targetType, @@ -5494,13 +5612,6 @@ void Executor::executeMemoryOperation( ref inBounds = mo->getBoundsCheckPointer(address, bytes); - if (state->isGEPExpr(address)) { - inBounds = - AndExpr::create(inBounds, mo->getBoundsCheckPointer(base, size)); - inBounds = AndExpr::create(inBounds, - Expr::createIsZero(mo->getOffsetExpr(base))); - } - inBounds = optimizer.optimizeExpr(inBounds, true); inBounds = Simplificator::simplifyExpr(state->constraints.cs(), inBounds) .simplified; @@ -5594,8 +5705,8 @@ void Executor::executeMemoryOperation( if (!checkResolvedMemoryObjects( *state, address, target, bytes, mayBeResolvedMemoryObjects, - resolvedMemoryObjects, resolveConditions, unboundConditions, - checkOutOfBounds, mayBeOutOfBound)) { + hasLazyInitialized, resolvedMemoryObjects, resolveConditions, + unboundConditions, checkOutOfBounds, mayBeOutOfBound)) { terminateStateOnSolverError(*state, "Query timed out (executeMemoryOperation)"); return; @@ -5647,25 +5758,26 @@ void Executor::executeMemoryOperation( ObjectState *wos = state->addressSpace.getWriteable(mo, os); if (wos->readOnly) { - branches = - fork(*state, resolveConditions[i], true, BranchType::MemOp); + branches = fork(*state, Expr::createIsZero(unboundConditions[i]), + true, BranchType::MemOp); assert(branches.first); terminateStateOnError(*branches.first, "memory error: object read only", StateTerminationType::ReadOnly); state = branches.second; } else { - ref result = - SelectExpr::create(resolveConditions[i], value, results[i]); + ref result = SelectExpr::create( + Expr::createIsZero(unboundConditions[i]), value, results[i]); wos->write(mo->getOffsetExpr(address), result); } } } else { - ref result = results[resolveConditions.size() - 1]; - for (unsigned int i = 0; i < resolveConditions.size(); ++i) { - unsigned int index = resolveConditions.size() - 1 - i; - result = SelectExpr::create(resolveConditions[index], results[index], - result); + ref result = results[unboundConditions.size() - 1]; + for (unsigned int i = 0; i < unboundConditions.size(); ++i) { + unsigned int index = unboundConditions.size() - 1 - i; + result = + SelectExpr::create(Expr::createIsZero(unboundConditions[index]), + results[index], result); } bindLocal(target, *state, result); } @@ -5692,8 +5804,8 @@ void Executor::executeMemoryOperation( const MemoryObject *mo = op.first; const ObjectState *os = op.second; - bound->addPointerResolution(address, mo); - bound->addPointerResolution(base, mo); + bound->addUniquePointerResolution(address, mo); + bound->addUniquePointerResolution(base, mo); /* FIXME: Notice, that here we are creating a new instance of object for every memory operation in order to handle type changes. This might @@ -5849,6 +5961,9 @@ IDType Executor::lazyInitializeLocalObject(ExecutionState &state, state.addConstraint(EqExpr::create(address, op.first->getBaseExpr()), {}); state.addConstraint( Expr::createIsZero(EqExpr::create(address, Expr::createPointer(0))), {}); + if (isa(size)) { + addConstraint(state, EqExpr::create(size, op.first->getSizeExpr())); + } return id; } diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index add4ff1b68..8aa39b241a 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -70,6 +70,7 @@ class AddressManager; class Array; struct Cell; class CodeGraphDistance; +class DistanceCalculator; class ExecutionState; class ExternalDispatcher; class Expr; @@ -142,6 +143,7 @@ class Executor : public Interpreter { std::unique_ptr concretizationManager; std::unique_ptr processForest; std::unique_ptr codeGraphDistance; + std::unique_ptr distanceCalculator; std::unique_ptr targetCalculator; /// Used to track states that have been added during the current @@ -360,7 +362,7 @@ class Executor : public Interpreter { bool checkResolvedMemoryObjects( ExecutionState &state, ref address, KInstruction *target, unsigned bytes, const std::vector &mayBeResolvedMemoryObjects, - std::vector &resolvedMemoryObjects, + bool hasLazyInitialized, std::vector &resolvedMemoryObjects, std::vector> &resolveConditions, std::vector> &unboundConditions, ref &checkOutOfBounds, bool &mayBeOutOfBound); diff --git a/lib/Core/MemoryManager.cpp b/lib/Core/MemoryManager.cpp index 309dff8601..6d601ce3e2 100644 --- a/lib/Core/MemoryManager.cpp +++ b/lib/Core/MemoryManager.cpp @@ -117,6 +117,8 @@ MemoryObject *MemoryManager::allocate(uint64_t size, bool isLocal, ref sizeExpr, unsigned timestamp, IDType id) { if (size > MaxConstantAllocationSize) { + klee_warning_once( + 0, "Large alloc: %" PRIu64 " bytes. KLEE models out of memory.", size); return 0; } diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index ab6ef2e1a9..91e9f67e0c 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -19,7 +19,6 @@ #include "klee/ADT/DiscretePDF.h" #include "klee/ADT/RNG.h" #include "klee/ADT/WeightedQueue.h" -#include "klee/Module/CodeGraphDistance.h" #include "klee/Module/InstructionInfoTable.h" #include "klee/Module/KInstruction.h" #include "klee/Module/KModule.h" @@ -150,133 +149,15 @@ static unsigned int ulog2(unsigned int val) { /// TargetedSearcher::TargetedSearcher(ref target, - CodeGraphDistance &_distance) + DistanceCalculator &_distanceCalculator) : states(std::make_unique< WeightedQueue>()), - target(target), codeGraphDistance(_distance), - distanceToTargetFunction( - codeGraphDistance.getBackwardDistance(target->getBlock()->parent)) {} + target(target), distanceCalculator(_distanceCalculator) {} ExecutionState &TargetedSearcher::selectState() { return *states->choose(0); } -bool TargetedSearcher::distanceInCallGraph(KFunction *kf, KBlock *kb, - unsigned int &distance) { - distance = UINT_MAX; - const std::unordered_map &dist = - codeGraphDistance.getDistance(kb); - KBlock *targetBB = target->getBlock(); - KFunction *targetF = targetBB->parent; - - if (kf == targetF && dist.count(targetBB) != 0) { - distance = 0; - return true; - } - - for (auto &kCallBlock : kf->kCallBlocks) { - if (dist.count(kCallBlock) != 0) { - for (auto &calledFunction : kCallBlock->calledFunctions) { - KFunction *calledKFunction = kf->parent->functionMap[calledFunction]; - if (distanceToTargetFunction.count(calledKFunction) != 0 && - distance > distanceToTargetFunction.at(calledKFunction) + 1) { - distance = distanceToTargetFunction.at(calledKFunction) + 1; - } - } - } - } - return distance != UINT_MAX; -} - -TargetedSearcher::WeightResult -TargetedSearcher::tryGetLocalWeight(ExecutionState *es, weight_type &weight, - const std::vector &localTargets) { - unsigned int intWeight = es->steppedMemoryInstructions; - KFunction *currentKF = es->pc->parent->parent; - KBlock *initKB = es->initPC->parent; - KBlock *currentKB = currentKF->blockMap[es->getPCBlock()]; - KBlock *prevKB = currentKF->blockMap[es->getPrevPCBlock()]; - const std::unordered_map &dist = - codeGraphDistance.getDistance(currentKB); - unsigned int localWeight = UINT_MAX; - for (auto &end : localTargets) { - if (dist.count(end) > 0) { - unsigned int w = dist.at(end); - localWeight = std::min(w, localWeight); - } - } - - if (localWeight == UINT_MAX) - return Miss; - if (localWeight == 0 && (initKB == currentKB || prevKB != currentKB || - target->shouldFailOnThisTarget())) { - return Done; - } - - intWeight += localWeight; - weight = ulog2(intWeight); // number on [0,32)-discrete-interval - return Continue; -} - -TargetedSearcher::WeightResult -TargetedSearcher::tryGetPreTargetWeight(ExecutionState *es, - weight_type &weight) { - KFunction *currentKF = es->pc->parent->parent; - std::vector localTargets; - for (auto &kCallBlock : currentKF->kCallBlocks) { - for (auto &calledFunction : kCallBlock->calledFunctions) { - KFunction *calledKFunction = - currentKF->parent->functionMap[calledFunction]; - if (distanceToTargetFunction.count(calledKFunction) > 0) { - localTargets.push_back(kCallBlock); - } - } - } - - if (localTargets.empty()) - return Miss; - - WeightResult res = tryGetLocalWeight(es, weight, localTargets); - weight = weight + 32; // number on [32,64)-discrete-interval - return res == Done ? Continue : res; -} - -TargetedSearcher::WeightResult -TargetedSearcher::tryGetPostTargetWeight(ExecutionState *es, - weight_type &weight) { - KFunction *currentKF = es->pc->parent->parent; - std::vector &localTargets = currentKF->returnKBlocks; - - if (localTargets.empty()) - return Miss; - - WeightResult res = tryGetLocalWeight(es, weight, localTargets); - weight = weight + 32; // number on [32,64)-discrete-interval - return res == Done ? Continue : res; -} - -TargetedSearcher::WeightResult -TargetedSearcher::tryGetTargetWeight(ExecutionState *es, weight_type &weight) { - std::vector localTargets = {target->getBlock()}; - WeightResult res = tryGetLocalWeight(es, weight, localTargets); - return res; -} - -TargetedSearcher::WeightResult -TargetedSearcher::tryGetWeight(ExecutionState *es, weight_type &weight) { - if (target->atReturn() && !target->shouldFailOnThisTarget()) { - if (es->prevPC->parent == target->getBlock() && - es->prevPC == target->getBlock()->getLastInstruction()) { - return Done; - } else if (es->pc->parent == target->getBlock()) { - weight = 0; - return Continue; - } - } - - if (target->shouldFailOnThisTarget() && target->isTheSameAsIn(es->prevPC) && - target->isThatError(es->error)) { - return Done; - } - +WeightResult TargetedSearcher::tryGetWeight(ExecutionState *es, + weight_type &weight) { BasicBlock *bb = es->getPCBlock(); KBlock *kb = es->pc->parent->parent->blockMap[bb]; KInstruction *ki = es->pc; @@ -285,51 +166,14 @@ TargetedSearcher::tryGetWeight(ExecutionState *es, weight_type &weight) { states->tryGetWeight(es, weight)) { return Continue; } - unsigned int minCallWeight = UINT_MAX, minSfNum = UINT_MAX, sfNum = 0; - for (auto sfi = es->stack.rbegin(), sfe = es->stack.rend(); sfi != sfe; - sfi++) { - unsigned callWeight; - if (distanceInCallGraph(sfi->kf, kb, callWeight)) { - callWeight *= 2; - if (callWeight == 0 && target->shouldFailOnThisTarget()) { - weight = 0; - return target->isTheSameAsIn(kb->getFirstInstruction()) && - target->isThatError(es->error) - ? Done - : Continue; - } else { - callWeight += sfNum; - } - if (callWeight < minCallWeight) { - minCallWeight = callWeight; - minSfNum = sfNum; - } - } - - if (sfi->caller) { - kb = sfi->caller->parent; - bb = kb->basicBlock; - } - sfNum++; - - if (minCallWeight < sfNum) - break; + auto distRes = distanceCalculator.getDistance(*es, target); + weight = ulog2(distRes.weight + es->steppedMemoryInstructions); // [0, 32] + if (!distRes.isInsideFunction) { + weight += 32; // [32, 64] } - WeightResult res = Miss; - if (minCallWeight == 0) - res = tryGetTargetWeight(es, weight); - else if (minSfNum == 0) - res = tryGetPreTargetWeight(es, weight); - else if (minSfNum != UINT_MAX) - res = tryGetPostTargetWeight(es, weight); - if (Done == res && target->shouldFailOnThisTarget()) { - if (!target->isThatError(es->error)) { - res = Continue; - } - } - return res; + return distRes.result; } void TargetedSearcher::update( @@ -436,10 +280,10 @@ void TargetedSearcher::removeReached() { /// GuidedSearcher::GuidedSearcher( - CodeGraphDistance &codeGraphDistance, TargetCalculator &stateHistory, + DistanceCalculator &distanceCalculator, TargetCalculator &stateHistory, std::set &pausedStates, - std::size_t bound, RNG &rng, Searcher *baseSearcher) - : baseSearcher(baseSearcher), codeGraphDistance(codeGraphDistance), + unsigned long long bound, RNG &rng, Searcher *baseSearcher) + : baseSearcher(baseSearcher), distanceCalculator(distanceCalculator), stateHistory(stateHistory), pausedStates(pausedStates), bound(bound), theRNG(rng) { guidance = baseSearcher ? CoverageGuidance : ErrorGuidance; @@ -468,7 +312,7 @@ ExecutionState &GuidedSearcher::selectState() { bool GuidedSearcher::isStuck(ExecutionState &state) { KInstruction *prevKI = state.prevPC; return (prevKI->inst->isTerminator() && - state.multilevel.count(state.getPCBlock()) > bound); + state.multilevel[state.getPCBlock()] > bound); } bool GuidedSearcher::updateTargetedSearcher( @@ -622,15 +466,17 @@ void GuidedSearcher::innerUpdate( targetlessStates.push_back(current); } - if (!baseRemovedStates.empty()) { - std::vector alt = baseRemovedStates; - for (const auto state : alt) { - auto it = pausedStates.find(state); - if (it != pausedStates.end()) { - pausedStates.erase(it); - baseRemovedStates.erase(std::remove(baseRemovedStates.begin(), - baseRemovedStates.end(), state), - baseRemovedStates.end()); + if (ErrorGuidance == guidance) { + if (!removedStates.empty()) { + std::vector alt = removedStates; + for (const auto state : alt) { + auto it = pausedStates.find(state); + if (it != pausedStates.end()) { + pausedStates.erase(it); + baseRemovedStates.erase(std::remove(baseRemovedStates.begin(), + baseRemovedStates.end(), state), + baseRemovedStates.end()); + } } } } @@ -833,7 +679,7 @@ bool GuidedSearcher::tryAddTarget(ref history, assert(targetedSearchers.count(history) == 0 || targetedSearchers.at(history).count(target) == 0); targetedSearchers[history][target] = - std::make_unique(target, codeGraphDistance); + std::make_unique(target, distanceCalculator); auto it = std::find_if( historiesAndTargets.begin(), historiesAndTargets.end(), [&history, &target]( diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index f307f46a77..436e8dcdd4 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -10,6 +10,7 @@ #ifndef KLEE_SEARCHER_H #define KLEE_SEARCHER_H +#include "DistanceCalculator.h" #include "ExecutionState.h" #include "PForest.h" #include "PTree.h" @@ -34,13 +35,14 @@ class raw_ostream; } // namespace llvm namespace klee { -class CodeGraphDistance; +class DistanceCalculator; template class DiscretePDF; template class WeightedQueue; class ExecutionState; class Executor; class TargetCalculator; class TargetForest; +class TargetReachability; /// A Searcher implements an exploration strategy for the Executor by selecting /// states for further exploration using different strategies or heuristics. @@ -129,33 +131,17 @@ class RandomSearcher final : public Searcher { /// TargetedSearcher picks a state /*COMMENT*/. class TargetedSearcher final : public Searcher { -public: - enum WeightResult : std::uint8_t { - Continue, - Done, - Miss, - }; - private: - typedef unsigned weight_type; - std::unique_ptr> states; ref target; - CodeGraphDistance &codeGraphDistance; - const std::unordered_map &distanceToTargetFunction; + DistanceCalculator &distanceCalculator; std::set reachedOnLastUpdate; - bool distanceInCallGraph(KFunction *kf, KBlock *kb, unsigned int &distance); - WeightResult tryGetLocalWeight(ExecutionState *es, weight_type &weight, - const std::vector &localTargets); - WeightResult tryGetPreTargetWeight(ExecutionState *es, weight_type &weight); - WeightResult tryGetTargetWeight(ExecutionState *es, weight_type &weight); - WeightResult tryGetPostTargetWeight(ExecutionState *es, weight_type &weight); WeightResult tryGetWeight(ExecutionState *es, weight_type &weight); public: - TargetedSearcher(ref target, CodeGraphDistance &distance); + TargetedSearcher(ref target, DistanceCalculator &distanceCalculator); ~TargetedSearcher() override; ExecutionState &selectState() override; @@ -217,11 +203,11 @@ class GuidedSearcher final : public Searcher { Guidance guidance; std::unique_ptr baseSearcher; TargetForestHistoryToSearcherMap targetedSearchers; - CodeGraphDistance &codeGraphDistance; + DistanceCalculator &distanceCalculator; TargetCalculator &stateHistory; TargetHashSet reachedTargets; std::set &pausedStates; - std::size_t bound; + unsigned long long bound; RNG &theRNG; unsigned index{1}; @@ -255,9 +241,9 @@ class GuidedSearcher final : public Searcher { public: GuidedSearcher( - CodeGraphDistance &codeGraphDistance, TargetCalculator &stateHistory, + DistanceCalculator &distanceCalculator, TargetCalculator &stateHistory, std::set &pausedStates, - std::size_t bound, RNG &rng, Searcher *baseSearcher = nullptr); + unsigned long long bound, RNG &rng, Searcher *baseSearcher = nullptr); ~GuidedSearcher() override = default; ExecutionState &selectState() override; void update(ExecutionState *current, diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp index c2e9f0bb63..72800087b9 100644 --- a/lib/Core/UserSearcher.cpp +++ b/lib/Core/UserSearcher.cpp @@ -183,7 +183,7 @@ Searcher *klee::constructUserSearcher(Executor &executor, searcher = nullptr; } searcher = new GuidedSearcher( - *executor.codeGraphDistance.get(), *executor.targetCalculator, + *executor.distanceCalculator, *executor.targetCalculator, executor.pausedStates, MaxCycles - 1, executor.theRNG, searcher); } diff --git a/lib/Expr/Assignment.cpp b/lib/Expr/Assignment.cpp index b176b8ed7b..d43db33870 100644 --- a/lib/Expr/Assignment.cpp +++ b/lib/Expr/Assignment.cpp @@ -22,7 +22,7 @@ void Assignment::dump() const { } for (bindings_ty::const_iterator i = bindings.begin(), e = bindings.end(); i != e; ++i) { - llvm::errs() << (*i).first->getIdentifier() << "\n["; + llvm::errs() << (*i).first->getName() << "\n["; for (int j = 0, k = (*i).second.size(); j < k; ++j) llvm::errs() << (int)(*i).second.load(j) << ","; llvm::errs() << "]\n"; @@ -34,7 +34,8 @@ ConstraintSet Assignment::createConstraintsFromAssignment() const { for (const auto &binding : bindings) { const auto &array = binding.first; const auto &values = binding.second; - ref arrayConstantSize = dyn_cast(array->size); + ref arrayConstantSize = + dyn_cast(evaluate(array->size)); assert(arrayConstantSize && "Size of symbolic array should be computed in assignment."); uint64_t arraySize = arrayConstantSize->getZExtValue(); diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp index 4ea34c677a..88f0e137a8 100644 --- a/lib/Expr/Constraints.cpp +++ b/lib/Expr/Constraints.cpp @@ -149,40 +149,9 @@ class ExprReplaceVisitor2 : public ExprVisitor { : Action::changeTo(visit(sexpr.falseExpr)); } - std::vector> splittedCond; - Expr::splitAnds(cond, splittedCond); - - ExprHashMap> localReplacements; - for (auto scond : splittedCond) { - if (const EqExpr *ee = dyn_cast(scond)) { - if (isa(ee->left)) { - localReplacements.insert(std::make_pair(ee->right, ee->left)); - } else { - localReplacements.insert( - std::make_pair(scond, ConstantExpr::alloc(1, Expr::Bool))); - } - } else { - localReplacements.insert( - std::make_pair(scond, ConstantExpr::alloc(1, Expr::Bool))); - } - } - - replacements.push_back(localReplacements); - visited.pushFrame(); auto trueExpr = visit(sexpr.trueExpr); - visited.popFrame(); - replacements.pop_back(); - - // Reuse for false branch replacements - localReplacements.clear(); - localReplacements.insert( - std::make_pair(cond, ConstantExpr::alloc(0, Expr::Bool))); - replacements.push_back(localReplacements); - visited.pushFrame(); auto falseExpr = visit(sexpr.falseExpr); - visited.popFrame(); - replacements.pop_back(); if (trueExpr != sexpr.trueExpr || falseExpr != sexpr.falseExpr) { ref seres = SelectExpr::create(cond, trueExpr, falseExpr); @@ -427,18 +396,28 @@ Simplificator::simplifyExpr(const constraints_ty &constraints, for (auto &constraint : constraints) { if (const EqExpr *ee = dyn_cast(constraint)) { + ref left = ee->left; + ref right = ee->right; + if (right < left) { + left = ee->right; + right = ee->left; + } if (isa(ee->left)) { equalities.insert(std::make_pair(ee->right, ee->left)); equalitiesParents.insert({ee->right, constraint}); } else { - equalities.insert( - std::make_pair(constraint, ConstantExpr::alloc(1, Expr::Bool))); + equalities.insert(std::make_pair(constraint, Expr::createTrue())); + equalities.insert(std::make_pair(right, left)); equalitiesParents.insert({constraint, constraint}); + equalitiesParents.insert({right, constraint}); } } else { - equalities.insert( - std::make_pair(constraint, ConstantExpr::alloc(1, Expr::Bool))); + equalities.insert(std::make_pair(constraint, Expr::createTrue())); equalitiesParents.insert({constraint, constraint}); + if (const NotExpr *ne = dyn_cast(constraint)) { + equalities.insert(std::make_pair(ne->expr, Expr::createFalse())); + equalitiesParents.insert({ne->expr, constraint}); + } } } @@ -522,12 +501,11 @@ Simplificator::gatherReplacements(constraints_ty constraints) { result.equalitiesParents.insert({ee->right, constraint}); } else { result.equalities.insert( - std::make_pair(constraint, ConstantExpr::alloc(1, Expr::Bool))); + std::make_pair(constraint, Expr::createTrue())); result.equalitiesParents.insert({constraint, constraint}); } } else { - result.equalities.insert( - std::make_pair(constraint, ConstantExpr::alloc(1, Expr::Bool))); + result.equalities.insert(std::make_pair(constraint, Expr::createTrue())); result.equalitiesParents.insert({constraint, constraint}); } } @@ -540,13 +518,11 @@ void Simplificator::addReplacement(Replacements &replacements, ref expr) { replacements.equalities.insert(std::make_pair(ee->right, ee->left)); replacements.equalitiesParents.insert({ee->right, expr}); } else { - replacements.equalities.insert( - std::make_pair(expr, ConstantExpr::alloc(1, Expr::Bool))); + replacements.equalities.insert(std::make_pair(expr, Expr::createTrue())); replacements.equalitiesParents.insert({expr, expr}); } } else { - replacements.equalities.insert( - std::make_pair(expr, ConstantExpr::alloc(1, Expr::Bool))); + replacements.equalities.insert(std::make_pair(expr, Expr::createTrue())); replacements.equalitiesParents.insert({expr, expr}); } } diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index 2969d72c9b..5b8bed1008 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -1579,6 +1579,32 @@ ref SelectExpr::create(ref c, ref t, ref f) { return AndExpr::create(c, t); } } + } else if (isa(t) || isa(f)) { + if (SelectExpr *se = dyn_cast(t)) { // c1 ? (c2 ? t2 : f2) : f1 + if (se->trueExpr == + f) { // c1 ? (c2 ? f1 : f2) : f1 <=> c1 /\ not c2 ? f2 : f1 + return SelectExpr::create( + AndExpr::create(c, Expr::createIsZero(se->cond)), se->falseExpr, f); + } + if (se->falseExpr == + f) { // c1 ? (c2 ? t2 : f1) : f1 <=> c1 /\ c2 ? t2 : f1 + return SelectExpr::create(AndExpr::create(c, se->cond), se->trueExpr, + f); + } + } + if (SelectExpr *se = dyn_cast(f)) { // c1 ? t1 : (c2 ? t2 : f2) + if (se->trueExpr == + t) { // c1 ? t1 : (c2 ? t1 : f2) <=> not c1 /\ not c2 ? f2 : t1 + return SelectExpr::create(AndExpr::create(Expr::createIsZero(c), + Expr::createIsZero(se->cond)), + se->falseExpr, t); + } + if (se->falseExpr == + t) { // c1 ? t1 : (c2 ? t2 : t1) <=> not c1 /\ c2 ? t2 : t1 + return SelectExpr::create( + AndExpr::create(Expr::createIsZero(c), se->cond), se->trueExpr, t); + } + } } return SelectExpr::alloc(c, t, f); @@ -1813,6 +1839,10 @@ static ref AddExpr_createPartialR(const ref &cl, Expr *r) { } else if (rk == Expr::Sub && isa(r->getKid(0))) { // A + (B-c) == (A+B) - c return SubExpr::create(AddExpr::create(cl, r->getKid(0)), r->getKid(1)); + } else if (rk == Expr::Select) { + SelectExpr *se = cast(r); + return SelectExpr::create(se->cond, AddExpr::create(cl, se->trueExpr), + AddExpr::create(cl, se->falseExpr)); } else { return AddExpr::alloc(cl, r); } @@ -2118,7 +2148,6 @@ static ref EqExpr_create(const ref &l, const ref &r) { if (al->right == ar->right) { return EqExpr::create(al->left, ar->left); } - return EqExpr::alloc(l, r); } else if (isa(l) || isa(r)) { if (SelectExpr *se = dyn_cast(l)) { return SelectExpr::create(se->cond, EqExpr::create(se->trueExpr, r), @@ -2128,10 +2157,9 @@ static ref EqExpr_create(const ref &l, const ref &r) { return SelectExpr::create(se->cond, EqExpr::create(se->trueExpr, l), EqExpr::create(se->falseExpr, l)); } - return EqExpr::alloc(l, r); - } else { - return EqExpr::alloc(l, r); } + + return EqExpr::alloc(l, r); } /// Tries to optimize EqExpr cl == rd, where cl is a ConstantExpr and @@ -2235,6 +2263,9 @@ static ref EqExpr_createPartialR(const ref &cl, Expr *r) { return EqExpr_createPartialR( cast(SubExpr::create(se->left, cl)), se->right.get()); } + if (cl->isZero()) { + return EqExpr::create(se->left, se->right); + } } else if (rk == Expr::Read && ConstArrayOpt) { return TryConstArrayOpt(cl, static_cast(r)); } @@ -2276,9 +2307,11 @@ static ref UltExpr_create(const ref &l, const ref &r) { static ref UleExpr_create(const ref &l, const ref &r) { if (l->getWidth() == Expr::Bool) { // !(l && !r) return OrExpr::create(Expr::createIsZero(l), r); - } else { - return UleExpr::alloc(l, r); + } else if (r->isZero()) { + return EqExpr::create(l, r); } + + return UleExpr::alloc(l, r); } static ref SltExpr_create(const ref &l, const ref &r) { diff --git a/lib/Expr/ExprEvaluator.cpp b/lib/Expr/ExprEvaluator.cpp index 9419cd2762..bcadb59156 100644 --- a/lib/Expr/ExprEvaluator.cpp +++ b/lib/Expr/ExprEvaluator.cpp @@ -76,6 +76,16 @@ ExprVisitor::Action ExprEvaluator::visitRead(const ReadExpr &re) { } } +ExprVisitor::Action ExprEvaluator::visitSelect(const SelectExpr &se) { + auto cond = visit(se.cond); + if (auto CE = dyn_cast(cond)) { + return CE->isTrue() ? Action::changeTo(visit(se.trueExpr)) + : Action::changeTo(visit(se.falseExpr)); + } + + return Action::doChildren(); +} + // we need to check for div by zero during partial evaluation, // if this occurs then simply ignore the 0 divisor and use the // original expression. diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp index d5d3c4cf96..bf222af763 100644 --- a/lib/Expr/ExprPPrinter.cpp +++ b/lib/Expr/ExprPPrinter.cpp @@ -530,6 +530,7 @@ void ExprPPrinter::printSignleArray(llvm::raw_ostream &os, const Array *a) { void ExprPPrinter::printSignleSource(llvm::raw_ostream &os, const ref s) { PPrinter p(os); + p.printArrayDecls = true; PrintContext PC(os); p.printSource(s, PC); } diff --git a/lib/Module/SarifReport.cpp b/lib/Module/SarifReport.cpp index a185a896ef..e0880646b9 100644 --- a/lib/Module/SarifReport.cpp +++ b/lib/Module/SarifReport.cpp @@ -77,6 +77,8 @@ tryConvertRuleJson(const std::string &ruleId, const std::string &toolName, } else { return {ReachWithError::UseAfterFree, ReachWithError::DoubleFree}; } + } else if ("core.Reach" == ruleId) { + return {ReachWithError::Reachable}; } else { return {}; } diff --git a/lib/Module/TargetForest.cpp b/lib/Module/TargetForest.cpp index d3c80efd30..bc54d1949e 100644 --- a/lib/Module/TargetForest.cpp +++ b/lib/Module/TargetForest.cpp @@ -15,6 +15,8 @@ #include "klee/Module/KModule.h" #include "klee/Module/TargetHash.h" +#include "klee/Support/ErrorHandling.h" + using namespace klee; using namespace llvm; @@ -510,6 +512,14 @@ void TargetForest::blockIn(ref subtarget, ref target) { forest = forest->blockLeafInChild(subtarget, target); } +void TargetForest::block(const ref &target) { + if (!forest->deepFind(target)) { + return; + } + + forest = forest->blockLeaf(target); +} + void TargetForest::dump() const { llvm::errs() << "History:\n"; history->dump(); diff --git a/lib/Solver/ConcretizingSolver.cpp b/lib/Solver/ConcretizingSolver.cpp index 8d1886ae57..b7f2b93404 100644 --- a/lib/Solver/ConcretizingSolver.cpp +++ b/lib/Solver/ConcretizingSolver.cpp @@ -196,6 +196,18 @@ bool ConcretizingSolver::relaxSymcreteConstraints(const Query &query, } } + for (const ref &symcrete : currentlyBrokenSymcretes) { + constraints_ty required; + IndependentElementSet eltsClosure = getIndependentConstraints( + Query(query.constraints, + AndExpr::create(query.expr, + Expr::createIsZero(symcrete->symcretized))), + required); + for (ref symcrete : eltsClosure.symcretes) { + currentlyBrokenSymcretes.insert(symcrete); + } + } + for (const ref &symcrete : currentlyBrokenSymcretes) { brokenSymcretes.insert(symcrete); for (const Array *array : symcrete->dependentArrays()) { @@ -230,7 +242,6 @@ bool ConcretizingSolver::relaxSymcreteConstraints(const Query &query, Simplificator::simplifyExpr(query.constraints, symbolicSizesSum) .simplified; - ref minimalValueOfSum; ref response; /* Compute assignment for symcretes. */ @@ -249,6 +260,7 @@ bool ConcretizingSolver::relaxSymcreteConstraints(const Query &query, } if (!response->tryGetInitialValuesFor(objects, brokenSymcretizedValues)) { + ref minimalValueOfSum; /* Receive model with a smallest sum as possible. */ if (!solver->impl->computeMinimalUnsignedValue( Query(queryConstraints, symbolicSizesSum), minimalValueOfSum)) { @@ -271,6 +283,13 @@ bool ConcretizingSolver::relaxSymcreteConstraints(const Query &query, assignment.bindings[objects[idx]] = brokenSymcretizedValues[idx]; } + ExprHashMap> concretizations; + + for (ref symcrete : query.constraints.symcretes()) { + concretizations[symcrete->symcretized] = + assignment.evaluate(symcrete->symcretized); + } + for (const ref &symcrete : brokenSymcretes) { ref sizeSymcrete = dyn_cast(symcrete); @@ -280,15 +299,10 @@ bool ConcretizingSolver::relaxSymcreteConstraints(const Query &query, /* Receive address array linked with this size array to request address * concretization. */ - uint64_t newSize = - cast(assignment.evaluate(symcrete->symcretized)) - ->getZExtValue(); - - /* TODO: we should be sure that `addressSymcrete` constains only one - * dependent array. */ - assert(sizeSymcrete->addressSymcrete.dependentArrays().size() == 1); - const Array *addressArray = - sizeSymcrete->addressSymcrete.dependentArrays().back(); + ref condcretized = assignment.evaluate(symcrete->symcretized); + + uint64_t newSize = cast(condcretized)->getZExtValue(); + void *address = addressGenerator->allocate( sizeSymcrete->addressSymcrete.symcretized, newSize); unsigned char *charAddressIterator = @@ -296,11 +310,22 @@ bool ConcretizingSolver::relaxSymcreteConstraints(const Query &query, SparseStorage storage(sizeof(address)); storage.store(0, charAddressIterator, charAddressIterator + sizeof(address)); - assignment.bindings[addressArray] = storage; + + concretizations[sizeSymcrete->addressSymcrete.symcretized] = + ConstantExpr::create( + reinterpret_cast(address), + sizeSymcrete->addressSymcrete.symcretized->getWidth()); + } + + ref concretizationCondition = query.expr; + for (const auto &concretization : concretizations) { + concretizationCondition = + OrExpr::create(Expr::createIsZero(EqExpr::create( + concretization.first, concretization.second)), + concretizationCondition); } - if (!solver->impl->check(constructConcretizedQuery(query, assignment), - result)) { + if (!solver->impl->check(query.withExpr(concretizationCondition), result)) { return false; } diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp index 32f1d7d996..ce53f40a7e 100644 --- a/lib/Solver/QueryLoggingSolver.cpp +++ b/lib/Solver/QueryLoggingSolver.cpp @@ -10,6 +10,7 @@ #include "klee/Config/config.h" #include "klee/Expr/Constraints.h" +#include "klee/Expr/ExprUtil.h" #include "klee/Statistics/Statistics.h" #include "klee/Support/ErrorHandling.h" #include "klee/Support/FileHandling.h" @@ -169,8 +170,17 @@ bool QueryLoggingSolver::computeInitialValues( std::vector> &values, bool &hasSolution) { startQuery(query, "InitialValues", 0, &objects); - bool success = - solver->impl->computeInitialValues(query, objects, values, hasSolution); + ExprHashSet expressions; + expressions.insert(query.constraints.cs().begin(), + query.constraints.cs().end()); + expressions.insert(query.expr); + + std::vector allObjects; + findSymbolicObjects(expressions.begin(), expressions.end(), allObjects); + std::vector> allValues; + + bool success = solver->impl->computeInitialValues(query, allObjects, + allValues, hasSolution); finishQuery(success); @@ -178,6 +188,11 @@ bool QueryLoggingSolver::computeInitialValues( logBuffer << queryCommentSign << " Solvable: " << (hasSolution ? "true" : "false") << "\n"; if (hasSolution) { + ref invalidResponse = + new InvalidResponse(allObjects, allValues); + success = invalidResponse->tryGetInitialValuesFor(objects, values); + assert(success); + Assignment allSolutionAssignment(allObjects, allValues, true); std::vector>::iterator values_it = values.begin(); @@ -190,7 +205,7 @@ bool QueryLoggingSolver::computeInitialValues( logBuffer << queryCommentSign << " " << array->getIdentifier() << " = ["; ref arrayConstantSize = - dyn_cast(solutionAssignment.evaluate(array->size)); + dyn_cast(allSolutionAssignment.evaluate(array->size)); assert(arrayConstantSize && "Array of symbolic size had not receive value for size!"); diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 3a104701fe..70aa655708 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -325,12 +325,7 @@ bool Query::containsSizeSymcretes() const { } void Query::dump() const { - llvm::errs() << "Constraints [\n"; - - for (const auto &constraint : constraints.cs()) - constraint->dump(); // TODO - - llvm::errs() << "]\n"; + constraints.dump(); llvm::errs() << "Query [\n"; expr->dump(); llvm::errs() << "]\n"; diff --git a/test/Feature/SymbolicSizes/FirstAndLastElements.c b/test/Feature/SymbolicSizes/FirstAndLastElements.c index ae92970c91..800af271e4 100644 --- a/test/Feature/SymbolicSizes/FirstAndLastElements.c +++ b/test/Feature/SymbolicSizes/FirstAndLastElements.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --out-of-mem-allocs=true --use-merged-pointer-dereference=true %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --check-out-of-memory --use-merged-pointer-dereference=true %t1.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/SymbolicSizes/ImplicitArrayExtension.c b/test/Feature/SymbolicSizes/ImplicitArrayExtension.c index 389a1adcab..56ff1843e5 100644 --- a/test/Feature/SymbolicSizes/ImplicitArrayExtension.c +++ b/test/Feature/SymbolicSizes/ImplicitArrayExtension.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --out-of-mem-allocs=true --solver-backend=z3 %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --check-out-of-memory --solver-backend=z3 %t1.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/SymbolicSizes/ImplicitSizeConcretization.c b/test/Feature/SymbolicSizes/ImplicitSizeConcretization.c index 1c13f15cd6..974623d058 100644 --- a/test/Feature/SymbolicSizes/ImplicitSizeConcretization.c +++ b/test/Feature/SymbolicSizes/ImplicitSizeConcretization.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --out-of-mem-allocs --output-dir=%t.klee-out --use-merged-pointer-dereference=true %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --check-out-of-memory --output-dir=%t.klee-out --use-merged-pointer-dereference=true %t1.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/SymbolicSizes/MinimizeSize.c b/test/Feature/SymbolicSizes/MinimizeSize.c index 7ee93ff88d..a67bca1cb6 100644 --- a/test/Feature/SymbolicSizes/MinimizeSize.c +++ b/test/Feature/SymbolicSizes/MinimizeSize.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --out-of-mem-allocs=true --solver-backend=z3 --use-merged-pointer-dereference=true %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --check-out-of-memory --solver-backend=z3 --use-merged-pointer-dereference=true %t1.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/SymbolicSizes/MultipleAllocations.c b/test/Feature/SymbolicSizes/MultipleAllocations.c index 1e5c6a5130..69d9633abf 100644 --- a/test/Feature/SymbolicSizes/MultipleAllocations.c +++ b/test/Feature/SymbolicSizes/MultipleAllocations.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --out-of-mem-allocs=true --solver-backend=z3 %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --check-out-of-memory --solver-backend=z3 %t1.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include @@ -13,6 +13,6 @@ int main() { char *s2 = (char *)malloc(n / 2); // 0, 0 char *s3 = (char *)malloc(n / 3 - 2); // 6, 3, 0 - // CHECK: MultipleAllocations.c:[[@LINE+1]]: memory error: out of bound pointer + // CHECK-NOT: MultipleAllocations.c:[[@LINE+1]]: memory error: out of bound pointer s1[1] = 29; } diff --git a/test/Feature/SymbolicSizes/NegativeIndexArray.c b/test/Feature/SymbolicSizes/NegativeIndexArray.c index ee27bcf30a..37c413bd51 100644 --- a/test/Feature/SymbolicSizes/NegativeIndexArray.c +++ b/test/Feature/SymbolicSizes/NegativeIndexArray.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --out-of-mem-allocs --use-merged-pointer-dereference=true %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --check-out-of-memory --use-merged-pointer-dereference=true %t1.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include "stdlib.h" diff --git a/test/Feature/SymbolicSizes/NegativeSize.c b/test/Feature/SymbolicSizes/NegativeSize.c index f4e9b3db81..ea8ab6d955 100644 --- a/test/Feature/SymbolicSizes/NegativeSize.c +++ b/test/Feature/SymbolicSizes/NegativeSize.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --out-of-mem-allocs=true --solver-backend=z3 %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --check-out-of-memory --solver-backend=z3 %t1.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/SymbolicSizes/RecomputeModelTwoArrays.c b/test/Feature/SymbolicSizes/RecomputeModelTwoArrays.c index c266e7c398..83c52cab06 100644 --- a/test/Feature/SymbolicSizes/RecomputeModelTwoArrays.c +++ b/test/Feature/SymbolicSizes/RecomputeModelTwoArrays.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --out-of-mem-allocs=true --solver-backend=z3 --use-merged-pointer-dereference=true %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --check-out-of-memory --solver-backend=z3 --use-merged-pointer-dereference=true %t1.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Feature/SymbolicSizes/SymbolicArrayOnStack.c b/test/Feature/SymbolicSizes/SymbolicArrayOnStack.c index 11b1d9e622..26a0e18fff 100644 --- a/test/Feature/SymbolicSizes/SymbolicArrayOnStack.c +++ b/test/Feature/SymbolicSizes/SymbolicArrayOnStack.c @@ -1,18 +1,18 @@ // REQUIRES: z3 // RUN: %clang %s -emit-llvm %O0opt -c -g -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --out-of-mem-allocs=true --solver-backend=z3 --use-merged-pointer-dereference=true %t.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --check-out-of-memory --solver-backend=z3 --use-merged-pointer-dereference=true %t.bc 2>&1 | FileCheck %s #include "klee/klee.h" int main() { int x = klee_int("x"); int f[x]; - // CHECK-DAG: SymbolicArrayOnStack.c:[[@LINE+2]]: memory error: out of bound pointer - // CHECK-DAG: SymbolicArrayOnStack.c:[[@LINE+1]]: memory error: null pointer exception + // CHECK: SymbolicArrayOnStack.c:[[@LINE+2]]: memory error: out of bound pointer + // CHECK-NOT: SymbolicArrayOnStack.c:[[@LINE+1]]: memory error: null pointer exception f[0] = 10; } // CHECK: KLEE: done: completed paths = 1 -// CHECK: KLEE: done: partially completed paths = 2 -// CHECK: KLEE: done: generated tests = 3 +// CHECK: KLEE: done: partially completed paths = 1 +// CHECK: KLEE: done: generated tests = 2 diff --git a/test/Feature/SymbolicSizes/SymbolicArrayOnStackWithSkipSymbolics.c b/test/Feature/SymbolicSizes/SymbolicArrayOnStackWithSkipSymbolics.c index ebd31bac29..af5a4df6dd 100644 --- a/test/Feature/SymbolicSizes/SymbolicArrayOnStackWithSkipSymbolics.c +++ b/test/Feature/SymbolicSizes/SymbolicArrayOnStackWithSkipSymbolics.c @@ -1,18 +1,18 @@ // REQUIRES: z3 // RUN: %clang %s -emit-llvm %O0opt -c -g -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --out-of-mem-allocs=true --skip-not-symbolic-objects --use-merged-pointer-dereference=true %t.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --check-out-of-memory --skip-not-symbolic-objects --use-merged-pointer-dereference=true %t.bc 2>&1 | FileCheck %s #include "klee/klee.h" int main() { int x = klee_int("x"); int f[x]; - // CHECK-DAG: SymbolicArrayOnStackWithSkipSymbolics.c:[[@LINE+2]]: memory error: out of bound pointer - // CHECK-DAG: SymbolicArrayOnStackWithSkipSymbolics.c:[[@LINE+1]]: memory error: null pointer exception + // CHECK: SymbolicArrayOnStackWithSkipSymbolics.c:[[@LINE+2]]: memory error: out of bound pointer + // CHECK-NOT: SymbolicArrayOnStackWithSkipSymbolics.c:[[@LINE+1]]: memory error: null pointer exception f[0] = 10; } // CHECK: KLEE: done: completed paths = 1 -// CHECK: KLEE: done: partially completed paths = 2 -// CHECK: KLEE: done: generated tests = 3 +// CHECK: KLEE: done: partially completed paths = 1 +// CHECK: KLEE: done: generated tests = 2 diff --git a/test/Feature/SymbolicSizes/VoidStar.c b/test/Feature/SymbolicSizes/VoidStar.c index 9194ad2866..cd64f3d10a 100644 --- a/test/Feature/SymbolicSizes/VoidStar.c +++ b/test/Feature/SymbolicSizes/VoidStar.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --out-of-mem-allocs=true --skip-not-lazy-initialized --use-merged-pointer-dereference=true %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --check-out-of-memory --skip-not-lazy-initialized --use-merged-pointer-dereference=true %t1.bc 2>&1 | FileCheck %s #include "klee/klee.h" #include diff --git a/test/Solver/CexCacheValidityCoresCheck.c b/test/Solver/CexCacheValidityCoresCheck.c index 3ad96f999d..a0d68efe75 100644 --- a/test/Solver/CexCacheValidityCoresCheck.c +++ b/test/Solver/CexCacheValidityCoresCheck.c @@ -2,10 +2,10 @@ // RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t1.klee-out // RUN: rm -rf %t2.klee-out -// RUN: %klee --output-dir=%t1.klee-out -cex-cache-validity-cores=false --solver-backend=z3 %t1.bc -// RUN: %klee --output-dir=%t2.klee-out -cex-cache-validity-cores=true --solver-backend=z3 %t1.bc -// RUN: %klee-stats --print-columns 'QCexCHits' --table-format=csv %t1.klee-out > %t1.stats -// RUN: %klee-stats --print-columns 'QCexCHits' --table-format=csv %t2.klee-out > %t2.stats +// RUN: %klee --output-dir=%t1.klee-out --cex-cache-validity-cores=false --solver-backend=z3 %t1.bc +// RUN: %klee --output-dir=%t2.klee-out --cex-cache-validity-cores=true --solver-backend=z3 %t1.bc +// RUN: %klee-stats --print-columns 'QCexCHits,Queries' --table-format=csv %t1.klee-out > %t1.stats +// RUN: %klee-stats --print-columns 'QCexCHits,Queries' --table-format=csv %t2.klee-out > %t2.stats // RUN: FileCheck -check-prefix=CHECK-CACHE-OFF -input-file=%t1.stats %s // RUN: FileCheck -check-prefix=CHECK-CACHE-ON -input-file=%t2.stats %s #include "klee/klee.h" @@ -29,7 +29,7 @@ int main(int argc, char **argv) { } } } -// CHECK-CACHE-ON: QCexCHits -// CHECK-CACHE-ON: 466 -// CHECK-CACHE-OFF: QCexCHits -// CHECK-CACHE-OFF: 410 +// CHECK-CACHE-ON: QCexCHits,Queries +// CHECK-CACHE-ON: 277,124 +// CHECK-CACHE-OFF: QCexCHits,Queries +// CHECK-CACHE-OFF: 226,175 diff --git a/utbot-build.sh b/utbot-build.sh new file mode 100755 index 0000000000..12f4182699 --- /dev/null +++ b/utbot-build.sh @@ -0,0 +1,35 @@ +#!/bin/bash +# This script is used to build KLEE as UTBot backend + +set -e +set -o pipefail +mkdir -p build +cd build + +$UTBOT_CMAKE_BINARY -G Ninja \ + -DCMAKE_PREFIX_PATH=$UTBOT_INSTALL_DIR/lib/cmake/z3 \ + -DCMAKE_LIBRARY_PATH=$UTBOT_INSTALL_DIR/lib \ + -DCMAKE_INCLUDE_PATH=$UTBOT_INSTALL_DIR/include \ + -DENABLE_SOLVER_Z3=TRUE \ + -DENABLE_POSIX_RUNTIME=TRUE \ + -DENABLE_KLEE_UCLIBC=ON \ + -DKLEE_UCLIBC_PATH=$UTBOT_ALL/klee-uclibc \ + -DENABLE_FLOATING_POINT=TRUE \ + -DENABLE_FP_RUNTIME=TRUE \ + -DLLVM_CONFIG_BINARY=$UTBOT_INSTALL_DIR/bin/llvm-config \ + -DLLVMCC=/utbot_distr/install/bin/clang \ + -DLLVMCXX=/utbot_distr/install/bin/clang++ \ + -DENABLE_UNIT_TESTS=TRUE \ + -DENABLE_SYSTEM_TESTS=TRUE \ + -DGTEST_SRC_DIR=$UTBOT_ALL/gtest \ + -DGTEST_INCLUDE_DIR=$UTBOT_ALL/gtest/googletest/include \ + -DCMAKE_INSTALL_PREFIX=$UTBOT_ALL/klee \ + -DENABLE_KLEE_LIBCXX=TRUE \ + -DKLEE_LIBCXX_DIR=$UTBOT_ALL/libcxx/install \ + -DKLEE_LIBCXX_INCLUDE_DIR=$UTBOT_ALL/libcxx/install/include/c++/v1 \ + -DENABLE_KLEE_EH_CXX=TRUE \ + -DKLEE_LIBCXXABI_SRC_DIR=$UTBOT_ALL/libcxx/libcxxabi \ + .. + +$UTBOT_CMAKE_BINARY --build . +$UTBOT_CMAKE_BINARY --install .