From 9f7135793b220a421a3b65a5071cfc0916579d63 Mon Sep 17 00:00:00 2001 From: Victor Samoilov Date: Mon, 22 May 2023 16:10:23 +0300 Subject: [PATCH 1/3] Factor out distance calculations for searchers in DistanceCalculator Fix style Add TargetReachability to update reachability of targets Fix current confidence rates: check reachability for stucked states, decrease from solver timeouts and divide more during branch Add skeleton for moving logic from searcher, without CoverageGuidance Move isStuck to ExecutionState Add handling of targetless states and reachedTargets Add block method in target forest Add history in ExecutionState Add enum for guidance Add first version of moving forest and distance calculation logic from searcher Change ExecutionState * to uint32_t in reachability Change interface of DistanceCalculator and pointer to reference Move heuristic to distanceCalculator Format Fix [fix] --- include/klee/Module/TargetForest.h | 1 + lib/Core/CMakeLists.txt | 1 + lib/Core/DistanceCalculator.cpp | 210 +++++++++++++++++++++++++++++ lib/Core/DistanceCalculator.h | 83 ++++++++++++ lib/Core/ExecutionState.h | 2 + lib/Core/Executor.cpp | 6 +- lib/Core/Executor.h | 2 + lib/Core/Searcher.cpp | 180 ++----------------------- lib/Core/Searcher.h | 28 +--- lib/Core/UserSearcher.cpp | 2 +- lib/Module/TargetForest.cpp | 10 ++ 11 files changed, 334 insertions(+), 191 deletions(-) create mode 100644 lib/Core/DistanceCalculator.cpp create mode 100644 lib/Core/DistanceCalculator.h 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..45851a6d26 --- /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 */ \ No newline at end of file diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index 8d9db68d2b..918db65bbb 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -203,6 +203,8 @@ class ExecutionState { public: using stack_ty = std::vector; + using TargetHashSet = + std::unordered_set, RefTargetHash, RefTargetCmp>; // Execution - Control Flow specific diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index e42a4a5bb8..28e1c6078d 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" @@ -446,6 +447,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), @@ -4182,7 +4184,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 +4524,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 diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index add4ff1b68..fb6744ff2f 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 diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index ab6ef2e1a9..979d34b142 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), + : baseSearcher(baseSearcher), distanceCalculator(distanceCalculator), stateHistory(stateHistory), pausedStates(pausedStates), bound(bound), theRNG(rng) { guidance = baseSearcher ? CoverageGuidance : ErrorGuidance; @@ -833,7 +677,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..c92e125c25 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,7 +203,7 @@ class GuidedSearcher final : public Searcher { Guidance guidance; std::unique_ptr baseSearcher; TargetForestHistoryToSearcherMap targetedSearchers; - CodeGraphDistance &codeGraphDistance; + DistanceCalculator &distanceCalculator; TargetCalculator &stateHistory; TargetHashSet reachedTargets; std::set &pausedStates; @@ -255,7 +241,7 @@ 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); ~GuidedSearcher() override = default; 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/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(); From 93a9327d951e05ddd8b2b3401346c643d5d782e9 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Thu, 22 Jun 2023 13:44:03 +0400 Subject: [PATCH 2/3] [fix] Collect full assigment for logging `computeInitialValues` --- lib/Solver/QueryLoggingSolver.cpp | 21 ++++++++++++++++++--- 1 file changed, 18 insertions(+), 3 deletions(-) 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!"); From 182cd7c182114856cb08c398d79a4e2b370fb894 Mon Sep 17 00:00:00 2001 From: dim8art Date: Thu, 27 Jul 2023 20:48:05 +0300 Subject: [PATCH 3/3] Reworking independent and concretizing solvers --- .github/workflows/build.yaml | 4 +- include/klee/ADT/DisjointSetUnion.h | 130 +++++++ include/klee/ADT/OrderMaintenanceTrie.h | 243 ++++++++++++ include/klee/ADT/PersistentArray.h | 192 +++++++++ include/klee/Expr/Assignment.h | 4 +- include/klee/Expr/Constraints.h | 17 +- .../klee/Expr/IndependentConstraintSetUnion.h | 42 ++ include/klee/Expr/IndependentSet.h | 108 ++++-- include/klee/Solver/SolverUtil.h | 10 + lib/Core/Executor.cpp | 14 +- lib/Expr/Assignment.cpp | 38 +- lib/Expr/CMakeLists.txt | 1 + lib/Expr/Constraints.cpp | 54 ++- lib/Expr/IndependentConstraintSetUnion.cpp | 140 +++++++ lib/Expr/IndependentSet.cpp | 367 +++++++++--------- lib/Solver/AssignmentValidatingSolver.cpp | 3 +- lib/Solver/ConcretizingSolver.cpp | 201 ++++++---- lib/Solver/IndependentSolver.cpp | 130 +++---- .../SymbolicSizes/ImplicitArrayExtension.c | 2 + 19 files changed, 1286 insertions(+), 414 deletions(-) create mode 100644 include/klee/ADT/DisjointSetUnion.h create mode 100644 include/klee/ADT/OrderMaintenanceTrie.h create mode 100644 include/klee/ADT/PersistentArray.h create mode 100644 include/klee/Expr/IndependentConstraintSetUnion.h create mode 100644 lib/Expr/IndependentConstraintSetUnion.cpp diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml index be44b5b4bd..0f1ef0fb1b 100644 --- a/.github/workflows/build.yaml +++ b/.github/workflows/build.yaml @@ -2,9 +2,9 @@ name: CI on: pull_request: - branches: [main, utbot-main] + branches: [IndependentSolverReworkFinal, main, utbot-main] push: - branches: [main, utbot-main] + branches: [IndependentSolverReworkFinal, main, utbot-main] # Defaults for building KLEE env: diff --git a/include/klee/ADT/DisjointSetUnion.h b/include/klee/ADT/DisjointSetUnion.h new file mode 100644 index 0000000000..df56cc8702 --- /dev/null +++ b/include/klee/ADT/DisjointSetUnion.h @@ -0,0 +1,130 @@ +#ifndef KLEE_DISJOINEDSETUNION_H +#define KLEE_DISJOINEDSETUNION_H +#include "klee/ADT/Ref.h" + +#include +#include +#include +#include + +namespace klee { + +template +class DisjointSetUnion { +protected: + std::unordered_map parent; + std::unordered_set roots; + std::unordered_map rank; + + std::unordered_set internalStorage; + std::unordered_map, HashType> disjointSets; + + ValueType find(const ValueType &v) { // findparent + assert(parent.find(v) != parent.end()); + if (v == parent[v]) + return v; + return parent[v] = find(parent[v]); + } + + ValueType constFind(const ValueType &v) const { + assert(parent.find(v) != parent.end()); + ValueType v1 = parent.find(v)->second; + if (v == v1) + return v; + return constFind(v1); + } + + void merge(ValueType a, ValueType b) { + a = find(a); + b = find(b); + if (a == b) { + return; + } + + if (rank[a] < rank[b]) { + std::swap(a, b); + } + parent[b] = a; + if (rank[a] == rank[b]) { + rank[a]++; + } + + roots.erase(b); + disjointSets[a] = SetType::merge(disjointSets[a], disjointSets[b]); + disjointSets[b] = nullptr; + } + + bool areJoined(const ValueType &i, const ValueType &j) const { + return constFind(i) == constFind(j); + } + +public: + using internalStorage_ty = std::unordered_set; + using disjointSets_ty = + std::unordered_map, HashType>; + using const_iterator = typename internalStorage_ty::const_iterator; + + const_iterator begin() const { return internalStorage.begin(); } + const_iterator end() const { return internalStorage.end(); } + + size_t numberOfValues() const noexcept { return internalStorage.size(); } + + size_t numberOfGroups() const noexcept { return disjointSets.size(); } + + bool empty() const noexcept { return numberOfValues() == 0; } + + ref findGroup(const ValueType &i) const { + return disjointSets.find(constFind(i))->second; + } + + ref findGroup(const_iterator it) const { + return disjointSets.find(constFind(*it))->second; + } + + void addValue(const ValueType value) { + if (internalStorage.find(value) != internalStorage.end()) { + return; + } + parent[value] = value; + roots.insert(value); + rank[value] = 0; + disjointSets[value] = new SetType(value); + + internalStorage.insert(value); + std::vector oldRoots(roots.begin(), roots.end()); + for (ValueType v : oldRoots) { + if (!areJoined(v, value) && + SetType::intersects(disjointSets[find(v)], + disjointSets[find(value)])) { + merge(v, value); + } + } + } + void getAllIndependentSets(std::vector> &result) const { + for (ValueType v : roots) + result.push_back(findGroup(v)); + } + + void add(const DisjointSetUnion &b) { + parent.insert(b.parent.begin(), b.parent.end()); + roots.insert(b.roots.begin(), b.roots.end()); + rank.insert(b.rank.begin(), b.rank.end()); + + internalStorage.insert(b.internalStorage.begin(), b.internalStorage.end()); + disjointSets.insert(b.disjointSets.begin(), b.disjointSets.end()); + } + DisjointSetUnion() {} + + DisjointSetUnion(const internalStorage_ty &is) { + for (ValueType v : is) { + addValue(v); + } + } + +public: + internalStorage_ty is() const { return internalStorage; } + + disjointSets_ty ds() const { return disjointSets; } +}; +} // namespace klee +#endif \ No newline at end of file diff --git a/include/klee/ADT/OrderMaintenanceTrie.h b/include/klee/ADT/OrderMaintenanceTrie.h new file mode 100644 index 0000000000..a21cf08049 --- /dev/null +++ b/include/klee/ADT/OrderMaintenanceTrie.h @@ -0,0 +1,243 @@ +#ifndef KLEE_ORDERMAINTENANCETRIE_H +#define KLEE_ORDERMAINTENANCETRIE_H +#include +#include +#include +#include +#include +#include +#include + +#define ITEMSIZE 64 // depth of tree +#define ALPHA 1.4 // balancing constant + +namespace klee { + +class OrderMaintenanaceTrie { +private: + struct Node { + + size_t height = 0; + size_t weight = 0; + size_t tag = 0; + + Node *parent = nullptr; + Node *left = nullptr; + Node *right = nullptr; + + Node(size_t h = 0, Node *p = nullptr) { + parent = p; + height = h; + } + + bool isFull() { + return std::pow(0.5, ITEMSIZE - height) * weight > + std::pow(1.0 / ALPHA, height); + } + ~Node() { + if (left) + delete left; + if (right) + delete right; + if (parent) { + if (this == parent->left) + parent->left = nullptr; + if (this == parent->right) + parent->right = nullptr; + } + Node *current = parent; + while (current) { + current->weight -= weight; + current = current->parent; + } + } + }; + +private: + Node *root; + +private: + Node *insert(size_t x) const { + std::bitset xbin(x); + Node *current = root; + for (int i = ITEMSIZE - 1; i > -1; i--) { + current->weight++; + if (!xbin[i]) { + if (!current->left) + current->left = new Node(current->height + 1, current); + current = current->left; + } else { + if (!current->right) + current->right = new Node(current->height + 1, current); + current = current->right; + } + } + current->tag = x; + return current; + } + + Node *find(size_t x) const { + std::bitset xbin(x); + Node *current = root; + for (int i = ITEMSIZE - 1; i > -1; i--) { + if (!xbin[i]) { + if (!current->left) + return nullptr; + current = current->left; + } else { + if (!current->right) + return nullptr; + current = current->right; + } + } + return current; + } + + Node *getNext(Node *x) const { + Node *current = x; + assert(current && "No such item in trie"); + while (current->parent && + (current == current->parent->right || !current->parent->left || + !current->parent->right)) { + current = current->parent; + } + if (!current->parent) + return nullptr; + + current = current->parent->right; + while (current->height != ITEMSIZE) { + if (current->left) + current = current->left; + else if (current->right) + current = current->right; + else + assert(false); + } + return current; + } + + Node *getNext(size_t x) const { + Node *current = find(x); + return getNext(current); + } + + bool getNextItem(size_t x, size_t &result) const { + if (!getNext(x)) + return false; + Node *next = getNext(x); + result = next->tag; + return true; + } + + void findAllLeafs(Node *item, std::vector &result) { + if (item->height == ITEMSIZE) + result.push_back(item); + if (item->left) { + findAllLeafs(item->left, result); + } + if (item->right) { + findAllLeafs(item->right, result); + } + } + + void rebalance(Node *item) { + while (item->parent && item->parent->isFull()) { + item = item->parent; + } + assert(item->parent && "Wrong choice of constants"); + std::vector leafs; + findAllLeafs(item, leafs); + assert(leafs.size() > 0); + size_t min; + min = leafs[0]->tag; + min = min >> (ITEMSIZE - item->height) << (ITEMSIZE - item->height); + size_t diff = ((1 << (ITEMSIZE - item->height)) - 1) / leafs.size(); + + for (Node *i : leafs) { + i->parent->left = nullptr; + i->parent->right = nullptr; + } + delete item; + for (Node *i : leafs) { + Node *newItem = insert(min); + *i = *(newItem); + Node *parent = newItem->parent; + if (newItem == parent->left) { + delete newItem; + parent->left = i; + } else { + delete newItem; + parent->right = i; + } + min += diff; + } + } + +public: + struct Iterator { + using iterator_category = std::input_iterator_tag; + using difference_type = std::ptrdiff_t; + using value_type = size_t; + using pointer = size_t *; + using reference = size_t &; + + private: + OrderMaintenanaceTrie::Node *leaf; + const OrderMaintenanaceTrie *owner; + + public: + Iterator(OrderMaintenanaceTrie::Node *leaf = nullptr, + const OrderMaintenanaceTrie *owner = nullptr) + : leaf(leaf), owner(owner) {} + + Iterator &operator++() { + if (!owner->getNext(leaf)) { + leaf = nullptr; + owner = nullptr; + return *this; + } + leaf = owner->getNext(leaf); + return *this; + } + + bool operator==(const Iterator &other) const { return leaf == other.leaf; } + + bool operator!=(const Iterator &other) const { return !(*this == other); } + + size_t operator*() const { + assert(leaf); + return leaf->tag; + } + }; + +public: + Iterator begin() { return Iterator(find(0), this); } + Iterator end() { return Iterator(nullptr, nullptr); } + + OrderMaintenanaceTrie() { + root = new Node(); + insert(0); + } + + ~OrderMaintenanaceTrie() { + std::vector leafs; + findAllLeafs(root, leafs); + delete root; + } + + Iterator insertAfter(Iterator it) { + size_t next = 0; + size_t p = *it; + if (!getNextItem(p, next) || next != p + 1) { + return Iterator(insert(p + 1), this); + } + Node *found = find(p); + rebalance(found); + return Iterator(insert(found->tag + 1), this); + } +}; +} // namespace klee + +#undef ITEMSIZE +#undef ALPHA +#endif \ No newline at end of file diff --git a/include/klee/ADT/PersistentArray.h b/include/klee/ADT/PersistentArray.h new file mode 100644 index 0000000000..61e1d36650 --- /dev/null +++ b/include/klee/ADT/PersistentArray.h @@ -0,0 +1,192 @@ +#ifndef KLEE_PERSISTENTARRAY_H +#define KLEE_PERSISTENTARRAY_H + +#include +#include +#include +#include +#include +#include +#include + +#include "OrderMaintenanceTrie.h" + +namespace klee { + +template class PersistentArray { +public: + struct Modification { + ValueType value; + OrderMaintenanaceTrie::Iterator listPosition; + Modification(ValueType v, OrderMaintenanaceTrie::Iterator lp = + OrderMaintenanaceTrie::Iterator()) + : value(v), listPosition(lp) {} + }; + + typedef std::list VersionList; + + struct Sublist { + typename VersionList::const_iterator initialElement; + typename VersionList::const_iterator modifiedElement; + Sublist(typename VersionList::const_iterator iE, + typename VersionList::const_iterator mE) { + initialElement = iE; + modifiedElement = mE; + } + }; + + struct positionCmp { + bool operator()(const Sublist &a, const Sublist &b) const { + return *(a.initialElement->listPosition) < + *(b.initialElement->listPosition); + } + }; + typedef std::set SublistSet; + +private: + std::shared_ptr versionList; + std::shared_ptr versionListOrder; + std::shared_ptr> sublists; + typename VersionList::const_iterator version; + + size_t capacity; + +public: + const typename VersionList::const_iterator getVersion() { return version; } + const std::shared_ptr getVersionList() { return versionList; } + const std::shared_ptr> getSublists() { + return sublists; + } + size_t size() const { return capacity; } + + PersistentArray() { + versionList = std::shared_ptr(new VersionList); + versionListOrder = + std::shared_ptr(new OrderMaintenanaceTrie); + sublists = + std::shared_ptr>(new std::vector()); + versionList->push_front( + Modification(ValueType(), versionListOrder->begin())); + version = versionList->begin(); + capacity = 0; + } + + PersistentArray(size_t n) { + versionList = new VersionList; + sublists = new std::vector(n); + versionList->push_front( + Modification(ValueType(), versionListOrder->begin())); + version = versionList->begin(); + for (auto &i : *sublists) { + i.insert(Sublist(version, version)); + } + capacity = n; + } + + static PersistentArray + storeInVersion(PersistentArray &array, const size_t &i, + const ValueType &b) { + // insert modification to versionList + assert(i < array.size() && i >= 0); + PersistentArray newArray(array); + typename VersionList::const_iterator v = newArray.version; + + Modification mod(b); + mod.listPosition = + newArray.versionListOrder->insertAfter(array.version->listPosition); + newArray.version = newArray.versionList->insert(++v, mod); + + // insert sublists created with modification to sublists array + + SublistSet &sI = (*newArray.sublists)[i]; + Sublist SLE(newArray.version, newArray.version); + typename SublistSet::iterator lowerBound = sI.lower_bound(SLE); + + typename VersionList::const_iterator nextElement = newArray.version; + nextElement++; + + if (lowerBound != sI.begin() && + nextElement != newArray.versionList->end()) { + Sublist prevSLE = *(--lowerBound); + sI.insert(Sublist(nextElement, prevSLE.modifiedElement)); + } + sI.insert(SLE); + return newArray; + } + + ValueType loadFromVersion(PersistentArray &array, + const size_t &i) { + Sublist sample(array.version, array.version); + SublistSet &sI = (*array.sublists)[i]; + + typename SublistSet::iterator result = sI.upper_bound(sample); + + if (result == sI.begin()) { + return ValueType(); + } + + return (--result)->modifiedElement->value; + } + + PersistentArray store(const size_t &i, const ValueType &b) { + return storeInVersion(*this, i, b); + } + + static PersistentArray + pushBackInVersion(PersistentArray &array, const ValueType &b) { + array.sublists->push_back( + {Sublist(array.versionList->begin(), array.versionList->begin())}); + PersistentArray newArray(array); + newArray.capacity++; + newArray = newArray.store(newArray.capacity - 1, b); + return newArray; + } + + PersistentArray push_back(const ValueType &b) { + return pushBackInVersion(*this, b); + } + + ValueType load(const size_t &i) { return loadFromVersion(*this, i); } + + ValueType operator[](const size_t &i) { return load(i); } + + bool operator==(const PersistentArray &b) const { + if (this->size() != b.size()) + return false; + for (int i = 0; i < this->size(); i++) { + if (this[i] != b[i]) + return false; + } + return true; + } + + bool operator!=(const PersistentArray &b) const { + return !(*this == b); + } + + bool operator<(const PersistentArray &b) const { + std::vector aInternal; + std::vector bInternal; + for (int i = 0; i < this->size(); i++) { + aInternal.push_back(this[i]); + } + for (int i = 0; i < b.size(); i++) { + bInternal.push_back(b[i]); + } + return aInternal < bInternal; + } + + bool operator>(const PersistentArray &b) const { + std::vector aInternal; + std::vector bInternal; + for (int i = 0; i < this->size(); i++) { + aInternal.push_back(this[i]); + } + for (int i = 0; i < b.size(); i++) { + bInternal.push_back(b[i]); + } + return aInternal > bInternal; + } +}; +} // namespace klee +#endif diff --git a/include/klee/Expr/Assignment.h b/include/klee/Expr/Assignment.h index a31ed3c22b..8116fbd839 100644 --- a/include/klee/Expr/Assignment.h +++ b/include/klee/Expr/Assignment.h @@ -53,9 +53,11 @@ class Assignment { } } + void add(const Assignment &b); + ref evaluate(const Array *mo, unsigned index) const; ref evaluate(ref e) const; - ConstraintSet createConstraintsFromAssignment() const; + constraints_ty createConstraintsFromAssignment() const; template bool satisfies(InputIterator begin, InputIterator end); diff --git a/include/klee/Expr/Constraints.h b/include/klee/Expr/Constraints.h index a14b9e191e..ad06d415ea 100644 --- a/include/klee/Expr/Constraints.h +++ b/include/klee/Expr/Constraints.h @@ -12,10 +12,14 @@ #include "klee/ADT/Ref.h" +#include "klee/ADT/DisjointSetUnion.h" +#include "klee/ADT/PersistentArray.h" #include "klee/Expr/Assignment.h" #include "klee/Expr/Expr.h" #include "klee/Expr/ExprHashMap.h" #include "klee/Expr/ExprUtil.h" +#include "klee/Expr/IndependentConstraintSetUnion.h" +#include "klee/Expr/IndependentSet.h" #include "klee/Expr/Path.h" #include "klee/Expr/Symcrete.h" @@ -55,7 +59,8 @@ class ConstraintSet { return _constraints < b._constraints || (_constraints == b._constraints && _symcretes < b._symcretes); } - + ConstraintSet getConcretizedVersion() const; + ConstraintSet getConcretizedVersion(const Assignment &c) const; void dump() const; void print(llvm::raw_ostream &os) const; @@ -64,11 +69,21 @@ class ConstraintSet { const constraints_ty &cs() const; const symcretes_ty &symcretes() const; const Assignment &concretization() const; + const IndependentConstraintSetUnion &independentElements() const; + + void getAllIndependentConstraintsSets( + const ref &queryExpr, + std::vector> &result) const; + + ref + getIndependentConstraints(const ref &queryExpr, + constraints_ty &result) const; private: constraints_ty _constraints; symcretes_ty _symcretes; Assignment _concretization; + IndependentConstraintSetUnion _independentElements; }; class PathConstraints { diff --git a/include/klee/Expr/IndependentConstraintSetUnion.h b/include/klee/Expr/IndependentConstraintSetUnion.h new file mode 100644 index 0000000000..a2f16b0f94 --- /dev/null +++ b/include/klee/Expr/IndependentConstraintSetUnion.h @@ -0,0 +1,42 @@ +#ifndef KLEE_INDEPENDENTCONSTRAINTSETUNION_H +#define KLEE_INDEPENDENTCONSTRAINTSETUNION_H + +#include "klee/Expr/Assignment.h" +#include "klee/Expr/Expr.h" +#include "klee/Expr/IndependentSet.h" + +namespace klee { +class IndependentConstraintSetUnion + : public DisjointSetUnion, IndependentConstraintSet, + util::ExprHash> { +public: + Assignment concretization; + +public: + ExprHashMap> concretizedExprs; + +public: + void updateConcretization(const Assignment &c); + void removeConcretization(const Assignment &remove); + void reEvaluateConcretization(const Assignment &newConcretization); + + IndependentConstraintSetUnion getConcretizedVersion() const; + IndependentConstraintSetUnion + getConcretizedVersion(const Assignment &c) const; + + IndependentConstraintSetUnion(); + IndependentConstraintSetUnion(const constraints_ty &is, + const SymcreteOrderedSet &os, + const Assignment &c); + + ref + getIndependentConstraints(const ref &e, constraints_ty &result) const; + void getAllIndependentConstraintSets( + const ref &e, + std::vector> &result) const; + void addExpr(const ref e); + void addSymcrete(const ref s); +}; +} // namespace klee + +#endif \ No newline at end of file diff --git a/include/klee/Expr/IndependentSet.h b/include/klee/Expr/IndependentSet.h index 581f42ac04..87e647b201 100644 --- a/include/klee/Expr/IndependentSet.h +++ b/include/klee/Expr/IndependentSet.h @@ -1,12 +1,18 @@ #ifndef KLEE_INDEPENDENTSET_H #define KLEE_INDEPENDENTSET_H +#include "klee/ADT/DisjointSetUnion.h" +#include "klee/ADT/ImmutableMap.h" +#include "klee/ADT/ImmutableSet.h" +#include "klee/Expr/Assignment.h" #include "klee/Expr/Expr.h" #include "klee/Expr/ExprHashMap.h" -#include "klee/Solver/Solver.h" +#include "klee/Expr/Symcrete.h" #include "llvm/Support/raw_ostream.h" -#include +#include #include +#include +#include namespace klee { @@ -36,7 +42,7 @@ template class DenseSet { return modified; } - bool intersects(const DenseSet &b) { + bool intersects(const DenseSet &b) const { for (typename set_ty::iterator it = s.begin(), ie = s.end(); it != ie; ++it) if (b.s.count(*it)) return true; @@ -70,54 +76,94 @@ inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, return os; } -class IndependentElementSet { +class IndependentConstraintSet { +private: + struct InnerSetUnion + : public DisjointSetUnion, IndependentConstraintSet, + util::ExprHash> { + using DisjointSetUnion, IndependentConstraintSet, + util::ExprHash>::DisjointSetUnion; + void addExpr(ref e) { + if (internalStorage.find(e) != internalStorage.end()) { + return; + } + parent[e] = e; + roots.insert(e); + rank[e] = 0; + disjointSets[e] = new IndependentConstraintSet(e); + + internalStorage.insert(e); + std::vector> oldRoots(roots.begin(), roots.end()); + for (ref v : oldRoots) { + if (!areJoined(v, e) && + IndependentConstraintSet::intersects(disjointSets[find(v)], + disjointSets[find(e)])) { + merge(v, e); + } + } + } + }; + public: - typedef std::map> elements_ty; + // All containers need to become persistent to make fast copy and faster merge + // possible + // map from concretized to normal + typedef ImmutableMap> elements_ty; elements_ty elements; // Represents individual elements of array accesses (arr[1]) - std::set + ImmutableSet wholeObjects; // Represents symbolically accessed arrays (arr[x]) constraints_ty exprs; // All expressions (constraints) that are associated // with this factor SymcreteOrderedSet symcretes; // All symcretes associated with this factor - IndependentElementSet(); - IndependentElementSet(ref e); - IndependentElementSet(ref s); - IndependentElementSet(const IndependentElementSet &ies); + Assignment concretization; + + InnerSetUnion concretizedSets; + + ref addExpr(ref e) const; + ref + updateConcretization(const Assignment &delta, + ExprHashMap> &changedExprs) const; + ref + removeConcretization(const Assignment &delta, + ExprHashMap> &changedExprs) const; - IndependentElementSet &operator=(const IndependentElementSet &ies); + void + addValuesToAssignment(const std::vector &objects, + const std::vector> &values, + Assignment &assign) const; + + IndependentConstraintSet(); + IndependentConstraintSet(ref e); + IndependentConstraintSet(ref s); + IndependentConstraintSet(const ref &ics); + + IndependentConstraintSet &operator=(const IndependentConstraintSet &ies); void print(llvm::raw_ostream &os) const; - // more efficient when this is the smaller set - bool intersects(const IndependentElementSet &b); + static bool intersects(ref a, + ref b); - // returns true iff set is changed by addition - bool add(const IndependentElementSet &b); + static ref + merge(ref a, + ref b); + + // Extracts which arrays are referenced from a particular independent set. + // Examines both the actual known array accesses arr[1] plus the undetermined + // accesses arr[x].Z + void calculateArrayReferences(std::vector &returnVector) const; + + mutable class ReferenceCounter _refCount; }; inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, - const IndependentElementSet &ies) { + const IndependentConstraintSet &ies) { ies.print(os); return os; } -// Breaks down a constraint into all of it's individual pieces, returning a -// list of IndependentElementSets or the independent factors. -// -// Caller takes ownership of returned std::list. -std::list * -getAllIndependentConstraintsSets(const Query &query); - -IndependentElementSet getIndependentConstraints(const Query &query, - constraints_ty &result); - -// Extracts which arrays are referenced from a particular independent set. -// Examines both the actual known array accesses arr[1] plus the undetermined -// accesses arr[x]. -void calculateArrayReferences(const IndependentElementSet &ie, - std::vector &returnVector); } // namespace klee #endif /* KLEE_INDEPENDENTSET_H */ diff --git a/include/klee/Solver/SolverUtil.h b/include/klee/Solver/SolverUtil.h index d61c188cc0..9833381f61 100644 --- a/include/klee/Solver/SolverUtil.h +++ b/include/klee/Solver/SolverUtil.h @@ -5,6 +5,7 @@ #include "klee/Expr/Constraints.h" #include "klee/Expr/Expr.h" #include "klee/Expr/ExprHashMap.h" +#include "klee/Expr/IndependentSet.h" #include "klee/System/Time.h" namespace klee { @@ -80,6 +81,15 @@ struct Query { (lhs.constraints == rhs.constraints && lhs.expr < rhs.expr); } + void getAllIndependentConstraintsSets( + std::vector> &result) const { + constraints.getAllIndependentConstraintsSets(expr, result); + } + + ref + getIndependentConstraints(constraints_ty &result) const { + return constraints.getIndependentConstraints(expr, result); + } /// Dump query void dump() const; }; diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 28e1c6078d..b9ec9df856 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -443,8 +443,8 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, InterpreterHandler *ih) : Interpreter(opts), interpreterHandler(ih), searcher(nullptr), externalDispatcher(new ExternalDispatcher(ctx)), statsTracker(0), - pathWriter(0), symPathWriter(0), - specialFunctionHandler(0), timers{time::Span(TimerInterval)}, + pathWriter(0), symPathWriter(0), specialFunctionHandler(0), + timers{time::Span(TimerInterval)}, concretizationManager(new ConcretizationManager(EqualitySubstitution)), codeGraphDistance(new CodeGraphDistance()), distanceCalculator(new DistanceCalculator(*codeGraphDistance)), @@ -5062,11 +5062,13 @@ MemoryObject *Executor::allocate(ExecutionState &state, ref size, ZExtExpr::create(size, pointerWidthInBits)}; constraints_ty required; - IndependentElementSet eltsClosure = getIndependentConstraints( - Query(state.constraints.cs(), ZExtExpr::create(size, pointerWidthInBits)), - required); + ref eltsClosure = + Query(state.constraints.cs(), ZExtExpr::create(size, pointerWidthInBits)) + .getIndependentConstraints( + + required); /* Collect dependent size symcretes. */ - for (ref symcrete : eltsClosure.symcretes) { + for (ref symcrete : eltsClosure->symcretes) { if (isa(symcrete)) { symbolicSizesTerms.push_back( ZExtExpr::create(symcrete->symcretized, pointerWidthInBits)); diff --git a/lib/Expr/Assignment.cpp b/lib/Expr/Assignment.cpp index b176b8ed7b..798b774221 100644 --- a/lib/Expr/Assignment.cpp +++ b/lib/Expr/Assignment.cpp @@ -29,8 +29,24 @@ void Assignment::dump() const { } } -ConstraintSet Assignment::createConstraintsFromAssignment() const { - ConstraintSet result; +void Assignment::add(const Assignment &b) { + for (bindings_ty::const_iterator it = b.bindings.begin(); + it != b.bindings.end(); it++) { + if (bindings.find(it->first) == bindings.end()) { + bindings[it->first] = {}; + } + SparseStorage &s = bindings[it->first]; + size_t pos = s.size(); + s.resize(s.size() + it->second.size()); + for (unsigned char c : it->second) { + s.store(pos, c); + pos++; + } + } +} + +constraints_ty Assignment::createConstraintsFromAssignment() const { + constraints_ty result; for (const auto &binding : bindings) { const auto &array = binding.first; const auto &values = binding.second; @@ -40,17 +56,15 @@ ConstraintSet Assignment::createConstraintsFromAssignment() const { uint64_t arraySize = arrayConstantSize->getZExtValue(); if (arraySize <= 8 && array->getRange() == Expr::Int8) { ref e = Expr::createTempRead(array, arraySize * array->getRange()); - result.addConstraint(EqExpr::create(e, evaluate(e)), {}); + result.insert(EqExpr::create(e, evaluate(e))); } else { for (unsigned arrayIndex = 0; arrayIndex < arraySize; ++arrayIndex) { unsigned char value = values.load(arrayIndex); - result.addConstraint( - EqExpr::create( - ReadExpr::create( - UpdateList(array, 0), - ConstantExpr::alloc(arrayIndex, array->getDomain())), - ConstantExpr::alloc(value, array->getRange())), - {}); + result.insert(EqExpr::create( + ReadExpr::create( + UpdateList(array, 0), + ConstantExpr::alloc(arrayIndex, array->getDomain())), + ConstantExpr::alloc(value, array->getRange()))); } } } @@ -89,7 +103,9 @@ Assignment Assignment::part(const SymcreteOrderedSet &symcretes) const { Assignment ret(allowFreeValues); for (auto symcrete : symcretes) { for (auto array : symcrete->dependentArrays()) { - ret.bindings.insert({array, bindings.at(array)}); + if (bindings.find(array) != bindings.end()) { + ret.bindings.insert({array, bindings.at(array)}); + } } } return ret; diff --git a/lib/Expr/CMakeLists.txt b/lib/Expr/CMakeLists.txt index 648abee448..d46995f482 100644 --- a/lib/Expr/CMakeLists.txt +++ b/lib/Expr/CMakeLists.txt @@ -22,6 +22,7 @@ klee_add_component(kleaverExpr ExprSMTLIBPrinter.cpp ExprUtil.cpp ExprVisitor.cpp + IndependentConstraintSetUnion.cpp IndependentSet.cpp Path.cpp SourceBuilder.cpp diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp index 4ea34c677a..528ecb3ffc 100644 --- a/lib/Expr/Constraints.cpp +++ b/lib/Expr/Constraints.cpp @@ -246,18 +246,21 @@ class ExprReplaceVisitor3 : public ExprVisitor { ConstraintSet::ConstraintSet(constraints_ty cs, symcretes_ty symcretes, Assignment concretization) - : _constraints(cs), _symcretes(symcretes), _concretization(concretization) { -} + : _constraints(cs), _symcretes(symcretes), _concretization(concretization), + _independentElements(_constraints, _symcretes, _concretization) {} -ConstraintSet::ConstraintSet() : _concretization(Assignment(true)) {} +ConstraintSet::ConstraintSet() + : _concretization(Assignment(true)), + _independentElements({}, {}, _concretization) {} void ConstraintSet::addConstraint(ref e, const Assignment &delta) { _constraints.insert(e); - + _independentElements.addExpr(e); // Update bindings for (auto i : delta.bindings) { _concretization.bindings[i.first] = i.second; } + _independentElements.updateConcretization(delta); } IDType Symcrete::idCounter = 0; @@ -265,9 +268,13 @@ IDType Symcrete::idCounter = 0; void ConstraintSet::addSymcrete(ref s, const Assignment &concretization) { _symcretes.insert(s); + _independentElements.addSymcrete(s); + Assignment dependentConcretization(true); for (auto i : s->dependentArrays()) { _concretization.bindings[i] = concretization.bindings.at(i); + dependentConcretization.bindings[i] = concretization.bindings.at(i); } + _independentElements.updateConcretization(dependentConcretization); } bool ConstraintSet::isSymcretized(ref expr) const { @@ -285,6 +292,28 @@ void ConstraintSet::rewriteConcretization(const Assignment &a) { _concretization.bindings[i.first] = i.second; } } + _independentElements.updateConcretization(a); +} + +ConstraintSet ConstraintSet::getConcretizedVersion() const { + ConstraintSet cs; + cs._independentElements = _independentElements.getConcretizedVersion(); + + for (ref e : cs._independentElements.is()) { + cs._constraints.insert(e); + } + return cs; +} + +ConstraintSet ConstraintSet::getConcretizedVersion( + const Assignment &newConcretization) const { + ConstraintSet cs; + cs._independentElements = + _independentElements.getConcretizedVersion(newConcretization); + for (ref e : cs._independentElements.is()) { + cs._constraints.insert(e); + } + return cs; } void ConstraintSet::print(llvm::raw_ostream &os) const { @@ -311,6 +340,11 @@ const constraints_ty &ConstraintSet::cs() const { return _constraints; } const symcretes_ty &ConstraintSet::symcretes() const { return _symcretes; } +const IndependentConstraintSetUnion & +ConstraintSet::independentElements() const { + return _independentElements; +} + const Path &PathConstraints::path() const { return _path; } const ExprHashMap &PathConstraints::indexes() const { @@ -581,6 +615,18 @@ Simplificator::composeExprDependencies(const ExprHashMap &upper, return result; } +void ConstraintSet::getAllIndependentConstraintsSets( + const ref &queryExpr, + std::vector> &result) const { + _independentElements.getAllIndependentConstraintSets(queryExpr, result); +} + +ref +ConstraintSet::getIndependentConstraints(const ref &queryExpr, + constraints_ty &result) const { + return _independentElements.getIndependentConstraints(queryExpr, result); +} + std::vector ConstraintSet::gatherArrays() const { std::vector arrays; findObjects(_constraints.begin(), _constraints.end(), arrays); diff --git a/lib/Expr/IndependentConstraintSetUnion.cpp b/lib/Expr/IndependentConstraintSetUnion.cpp new file mode 100644 index 0000000000..8bb8e0d6ea --- /dev/null +++ b/lib/Expr/IndependentConstraintSetUnion.cpp @@ -0,0 +1,140 @@ +#include "klee/Expr/IndependentConstraintSetUnion.h" + +namespace klee { +void IndependentConstraintSetUnion::updateConcretization( + const Assignment &delta) { + for (ref e : roots) { + ref &ics = disjointSets[e]; + Assignment part = delta.part(ics->symcretes); + ics = ics->updateConcretization(part, concretizedExprs); + } + for (auto it : delta.bindings) { + concretization.bindings[it.first] = it.second; + } +} + +void IndependentConstraintSetUnion::removeConcretization( + const Assignment &remove) { + for (ref e : roots) { + ref &ics = disjointSets[e]; + Assignment part = remove.part(ics->symcretes); + ics = ics->removeConcretization(part, concretizedExprs); + } + for (auto it : remove.bindings) { + concretization.bindings.erase(it.first); + } +} +void IndependentConstraintSetUnion::reEvaluateConcretization( + const Assignment &newConcretization) { + Assignment delta(true); + Assignment removed(true); + for (const auto it : concretization) { + if (newConcretization.bindings.count(it.first) == 0) { + removed.bindings.insert(it); + } else if (newConcretization.bindings.at(it.first) != it.second) { + delta.bindings.insert(*(newConcretization.bindings.find(it.first))); + } + } + updateConcretization(delta); + removeConcretization(removed); +} +IndependentConstraintSetUnion::IndependentConstraintSetUnion() + : concretization(Assignment(true)) {} + +ref +IndependentConstraintSetUnion::getIndependentConstraints( + const ref &e, constraints_ty &result) const { + ref compare = new IndependentConstraintSet(e); + + for (ref i : internalStorage) { + ref a = constFind(i); + ref ics = disjointSets.find(a)->second; + if (IndependentConstraintSet::intersects(ics, compare)) { + for (ref expr : ics->exprs) { + result.insert(expr); + } + } + } + return compare; +} + +void IndependentConstraintSetUnion::getAllIndependentConstraintSets( + const ref &e, + std::vector> &result) const { + IndependentConstraintSetUnion u = *this; + ConstantExpr *CE = dyn_cast(e); + ref neg; + if (CE) { + assert(CE && CE->isFalse() && + "the expr should always be false and " + "therefore not included in factors"); + u.getAllIndependentSets(result); + } else { + // factor that contains query expr should be checked first + neg = Expr::createIsZero(e); + u.addExpr(neg); + result.push_back(u.findGroup(neg)); + for (ref v : u.roots) { + if (!u.areJoined(v, neg)) { + result.push_back(u.findGroup(v)); + } + } + } +} +void IndependentConstraintSetUnion::addExpr(const ref e) { + addValue(e); + disjointSets[find(e)] = disjointSets[find(e)]->addExpr(e); +} +void IndependentConstraintSetUnion::addSymcrete(const ref s) { + ref value = s->symcretized; + if (internalStorage.find(value) != internalStorage.end()) { + return; + } + parent[value] = value; + roots.insert(value); + rank[value] = 0; + disjointSets[value] = new IndependentConstraintSet(s); + + internalStorage.insert(value); + std::vector> oldRoots(roots.begin(), roots.end()); + for (ref v : oldRoots) { + if (!areJoined(v, value) && + IndependentConstraintSet::intersects(disjointSets[find(v)], + disjointSets[find(value)])) { + merge(v, value); + } + } + disjointSets[find(value)] = disjointSets[find(value)]->addExpr(value); +} + +IndependentConstraintSetUnion::IndependentConstraintSetUnion( + const constraints_ty &is, const SymcreteOrderedSet &os, const Assignment &c) + : concretization(Assignment(true)) { + for (ref e : is) { + addValue(e); + } + for (ref s : os) { + addSymcrete(s); + } + updateConcretization(c); +} + +IndependentConstraintSetUnion +IndependentConstraintSetUnion::getConcretizedVersion() const { + IndependentConstraintSetUnion icsu; + for (ref i : roots) { + ref root = disjointSets.at(i); + icsu.add(root->concretizedSets); + } + icsu.concretizedExprs = concretizedExprs; + return icsu; +} + +IndependentConstraintSetUnion +IndependentConstraintSetUnion::getConcretizedVersion( + const Assignment &newConcretization) const { + IndependentConstraintSetUnion icsu = *this; + icsu.reEvaluateConcretization(newConcretization); + return icsu.getConcretizedVersion(); +} +} // namespace klee \ No newline at end of file diff --git a/lib/Expr/IndependentSet.cpp b/lib/Expr/IndependentSet.cpp index d4fade9ef1..2dd50cb196 100644 --- a/lib/Expr/IndependentSet.cpp +++ b/lib/Expr/IndependentSet.cpp @@ -1,6 +1,7 @@ #include "klee/Expr/IndependentSet.h" #include "klee/ADT/Ref.h" +#include "klee/Expr/Assignment.h" #include "klee/Expr/Constraints.h" #include "klee/Expr/ExprHashMap.h" #include "klee/Expr/ExprUtil.h" @@ -16,9 +17,88 @@ namespace klee { -IndependentElementSet::IndependentElementSet() {} +ref +IndependentConstraintSet::addExpr(ref e) const { + ref ics = new IndependentConstraintSet(this); + ics->concretizedSets.addValue(concretization.evaluate(e)); + return ics; +} + +ref +IndependentConstraintSet::updateConcretization( + const Assignment &delta, ExprHashMap> &concretizedExprs) const { + ref ics = new IndependentConstraintSet(this); + if (delta.bindings.size() == 0) { + return ics; + } + for (auto i : delta.bindings) { + ics->concretization.bindings[i.first] = i.second; + } + InnerSetUnion DSU; + for (ref i : exprs) { + ref e = ics->concretization.evaluate(i); + concretizedExprs[i] = e; + DSU.addValue(e); + } + for (ref s : symcretes) { + DSU.addValue(EqExpr::create(ics->concretization.evaluate(s->symcretized), + s->symcretized)); + } + ics->concretizedSets = DSU; + return ics; +} + +ref +IndependentConstraintSet::removeConcretization( + const Assignment &delta, ExprHashMap> &concretizedExprs) const { + ref ics = new IndependentConstraintSet(this); + if (delta.bindings.size() == 0) { + return ics; + } + for (auto i : delta.bindings) { + ics->concretization.bindings.erase(i.first); + } + InnerSetUnion DSU; + for (ref i : exprs) { + ref e = ics->concretization.evaluate(i); + concretizedExprs[i] = e; + DSU.addValue(e); + } + for (ref s : symcretes) { + DSU.addValue(EqExpr::create(ics->concretization.evaluate(s->symcretized), + s->symcretized)); + } + + ics->concretizedSets = DSU; + return ics; +} -IndependentElementSet::IndependentElementSet(ref e) { +void IndependentConstraintSet::addValuesToAssignment( + const std::vector &objects, + const std::vector> &values, + Assignment &assign) const { + for (unsigned i = 0; i < values.size(); i++) { + if (assign.bindings.count(objects[i])) { + SparseStorage &value = assign.bindings[objects[i]]; + assert(value.size() == values[i].size() && + "we're talking about the same array here"); + DenseSet ds = (elements.find(objects[i]))->second; + for (std::set::iterator it2 = ds.begin(); it2 != ds.end(); + it2++) { + unsigned index = *it2; + value.store(index, values[i].load(index)); + } + } else { + assign.bindings[objects[i]] = values[i]; + } + } +} + +IndependentConstraintSet::IndependentConstraintSet() + : concretization(Assignment(true)) {} + +IndependentConstraintSet::IndependentConstraintSet(ref e) + : concretization(Assignment(true)) { exprs.insert(e); // Track all reads in the program. Determines whether reads are // concrete or symbolic. If they are symbolic, "collapses" array @@ -39,19 +119,24 @@ IndependentElementSet::IndependentElementSet(ref e) { if (ConstantExpr *CE = dyn_cast(re->index)) { // if index constant, then add to set of constraints operating // on that array (actually, don't add constraint, just set index) - DenseSet &dis = elements[array]; + DenseSet dis; + if (elements.find(array) != elements.end()) { + dis = (elements.find(array))->second; + } dis.add((unsigned)CE->getZExtValue(32)); + elements = elements.replace({array, dis}); } else { elements_ty::iterator it2 = elements.find(array); if (it2 != elements.end()) - elements.erase(it2); - wholeObjects.insert(array); + elements = elements.remove(it2->first); + wholeObjects = wholeObjects.insert(array); } } } } -IndependentElementSet::IndependentElementSet(ref s) { +IndependentConstraintSet::IndependentConstraintSet(ref s) + : concretization(Assignment(true)) { symcretes.insert(s); for (Symcrete &dependentSymcrete : s->dependentSymcretes()) { @@ -93,35 +178,45 @@ IndependentElementSet::IndependentElementSet(ref s) { if (ConstantExpr *CE = dyn_cast(re->index)) { // if index constant, then add to set of constraints operating // on that array (actually, don't add constraint, just set index) - DenseSet &dis = elements[array]; + DenseSet dis; + if (elements.find(array) != elements.end()) { + dis = (elements.find(array))->second; + } dis.add((unsigned)CE->getZExtValue(32)); + elements = elements.replace({array, dis}); } else { elements_ty::iterator it2 = elements.find(array); if (it2 != elements.end()) - elements.erase(it2); - wholeObjects.insert(array); + elements = elements.remove(it2->first); + wholeObjects = wholeObjects.insert(array); } } } } -IndependentElementSet::IndependentElementSet(const IndependentElementSet &ies) - : elements(ies.elements), wholeObjects(ies.wholeObjects), exprs(ies.exprs) { -} - -IndependentElementSet & -IndependentElementSet::operator=(const IndependentElementSet &ies) { - elements = ies.elements; - wholeObjects = ies.wholeObjects; - exprs = ies.exprs; +IndependentConstraintSet::IndependentConstraintSet( + const ref &ics) + : elements(ics->elements), wholeObjects(ics->wholeObjects), + exprs(ics->exprs), symcretes(ics->symcretes), + concretization(ics->concretization), + concretizedSets(ics->concretizedSets) {} + +IndependentConstraintSet & +IndependentConstraintSet::operator=(const IndependentConstraintSet &ics) { + elements = ics.elements; + wholeObjects = ics.wholeObjects; + exprs = ics.exprs; + symcretes = ics.symcretes; + concretization = ics.concretization; + concretizedSets = ics.concretizedSets; return *this; } -void IndependentElementSet::print(llvm::raw_ostream &os) const { +void IndependentConstraintSet::print(llvm::raw_ostream &os) const { os << "{"; bool first = true; - for (std::set::iterator it = wholeObjects.begin(), - ie = wholeObjects.end(); + for (ImmutableSet::iterator it = wholeObjects.begin(), + ie = wholeObjects.end(); it != ie; ++it) { const Array *array = *it; @@ -133,7 +228,7 @@ void IndependentElementSet::print(llvm::raw_ostream &os) const { os << "MO" << array->getIdentifier(); } - for (elements_ty::const_iterator it = elements.begin(), ie = elements.end(); + for (elements_ty::iterator it = elements.begin(), ie = elements.end(); it != ie; ++it) { const Array *array = it->first; const DenseSet &dis = it->second; @@ -149,216 +244,104 @@ void IndependentElementSet::print(llvm::raw_ostream &os) const { os << "}"; } -// more efficient when this is the smaller set -bool IndependentElementSet::intersects(const IndependentElementSet &b) { +bool IndependentConstraintSet::intersects( + ref a, + ref b) { + if (a->exprs.size() + a->symcretes.size() > + b->exprs.size() + b->symcretes.size()) { + std::swap(a, b); + } // If there are any symbolic arrays in our query that b accesses - for (std::set::iterator it = wholeObjects.begin(), - ie = wholeObjects.end(); + for (ImmutableSet::iterator it = a->wholeObjects.begin(), + ie = a->wholeObjects.end(); it != ie; ++it) { const Array *array = *it; - if (b.wholeObjects.count(array) || - b.elements.find(array) != b.elements.end()) + if (b->wholeObjects.count(array) || + b->elements.find(array) != b->elements.end()) return true; } - for (elements_ty::iterator it = elements.begin(), ie = elements.end(); + for (elements_ty::iterator it = a->elements.begin(), ie = a->elements.end(); it != ie; ++it) { const Array *array = it->first; // if the array we access is symbolic in b - if (b.wholeObjects.count(array)) + if (b->wholeObjects.count(array)) return true; - elements_ty::const_iterator it2 = b.elements.find(array); + elements_ty::iterator it2 = b->elements.find(array); // if any of the elements we access are also accessed by b - if (it2 != b.elements.end()) { - if (it->second.intersects(it2->second)) + if (it2 != b->elements.end()) { + if (it->second.intersects(it2->second)) { return true; + } } } // No need to check symcretes here, arrays must be sufficient. return false; } -// returns true iff set is changed by addition -bool IndependentElementSet::add(const IndependentElementSet &b) { - for (auto expr : b.exprs) { - exprs.insert(expr); - } +ref +IndependentConstraintSet::merge(ref A, + ref B) { + ref a = new IndependentConstraintSet(A); + ref b = new IndependentConstraintSet(B); - for (const ref &symcrete : b.symcretes) { - symcretes.insert(symcrete); + if (a->exprs.size() + a->symcretes.size() < + b->exprs.size() + b->symcretes.size()) { + std::swap(a, b); + } + for (ref expr : b->exprs) { + a->exprs.insert(expr); + } + for (const ref &symcrete : b->symcretes) { + a->symcretes.insert(symcrete); } - bool modified = false; - for (std::set::const_iterator it = b.wholeObjects.begin(), - ie = b.wholeObjects.end(); + for (ImmutableSet::iterator it = b->wholeObjects.begin(), + ie = b->wholeObjects.end(); it != ie; ++it) { const Array *array = *it; - elements_ty::iterator it2 = elements.find(array); - if (it2 != elements.end()) { - modified = true; - elements.erase(it2); - wholeObjects.insert(array); + elements_ty::iterator it2 = a->elements.find(array); + if (it2 != a->elements.end()) { + a->elements = a->elements.remove(it2->first); + a->wholeObjects = a->wholeObjects.insert(array); } else { - if (!wholeObjects.count(array)) { - modified = true; - wholeObjects.insert(array); + if (!a->wholeObjects.count(array)) { + a->wholeObjects = a->wholeObjects.insert(array); } } } - for (elements_ty::const_iterator it = b.elements.begin(), - ie = b.elements.end(); + for (elements_ty::iterator it = b->elements.begin(), ie = b->elements.end(); it != ie; ++it) { const Array *array = it->first; - if (!wholeObjects.count(array)) { - elements_ty::iterator it2 = elements.find(array); - if (it2 == elements.end()) { - modified = true; - elements.insert(*it); + if (!a->wholeObjects.count(array)) { + elements_ty::iterator it2 = a->elements.find(array); + if (it2 == a->elements.end()) { + a->elements = a->elements.insert(*it); } else { - // Now need to see if there are any (z=?)'s - if (it2->second.add(it->second)) - modified = true; + DenseSet dis = it2->second; + dis.add(it->second); + a->elements = a->elements.replace({array, dis}); } } } - return modified; -} - -// Breaks down a constraint into all of it's individual pieces, returning a -// list of IndependentElementSets or the independent factors. -// -// Caller takes ownership of returned std::list. -std::list * -getAllIndependentConstraintsSets(const Query &query) { - std::list *factors = - new std::list(); - ConstantExpr *CE = dyn_cast(query.expr); - if (CE) { - assert(CE && CE->isFalse() && - "the expr should always be false and " - "therefore not included in factors"); - } else { - ref neg = Expr::createIsZero(query.expr); - factors->push_back(IndependentElementSet(neg)); - } - - for (const auto &constraint : query.constraints.cs()) { - // iterate through all the previously separated constraints. Until we - // actually return, factors is treated as a queue of expressions to be - // evaluated. If the queue property isn't maintained, then the exprs - // could be returned in an order different from how they came it, negatively - // affecting later stages. - factors->push_back(IndependentElementSet(constraint)); - } - - for (const auto &symcrete : query.constraints.symcretes()) { - factors->push_back(IndependentElementSet(symcrete)); - } - - bool doneLoop = false; - do { - doneLoop = true; - std::list *done = - new std::list; - while (factors->size() > 0) { - IndependentElementSet current = factors->front(); - factors->pop_front(); - // This list represents the set of factors that are separate from current. - // Those that are not inserted into this list (queue) intersect with - // current. - std::list *keep = - new std::list; - while (factors->size() > 0) { - IndependentElementSet compare = factors->front(); - factors->pop_front(); - if (current.intersects(compare)) { - if (current.add(compare)) { - // Means that we have added (z=y)added to (x=y) - // Now need to see if there are any (z=?)'s - doneLoop = false; - } - } else { - keep->push_back(compare); - } - } - done->push_back(current); - delete factors; - factors = keep; - } - delete factors; - factors = done; - } while (!doneLoop); - - return factors; -} - -IndependentElementSet getIndependentConstraints(const Query &query, - constraints_ty &result) { - IndependentElementSet eltsClosure(query.expr); - std::vector, IndependentElementSet>> worklist; - - for (const auto &constraint : query.constraints.cs()) - worklist.push_back( - std::make_pair(constraint, IndependentElementSet(constraint))); - - for (const ref &symcrete : query.constraints.symcretes()) { - worklist.push_back( - std::make_pair(symcrete->symcretized, IndependentElementSet(symcrete))); - } - - // XXX This should be more efficient (in terms of low level copy stuff). - bool done = false; - do { - done = true; - std::vector, IndependentElementSet>> newWorklist; - for (std::vector, IndependentElementSet>>::iterator - it = worklist.begin(), - ie = worklist.end(); - it != ie; ++it) { - if (it->second.intersects(eltsClosure)) { - if (eltsClosure.add(it->second)) - done = false; - result.insert(it->first); - // Means that we have added (z=y)added to (x=y) - // Now need to see if there are any (z=?)'s - } else { - newWorklist.push_back(*it); - } - } - worklist.swap(newWorklist); - } while (!done); - - // KLEE_DEBUG( - // std::set> reqset(result.begin(), result.end()); - // errs() << "--\n"; errs() << "Q: " << query.expr << "\n"; - // errs() << "\telts: " << IndependentElementSet(query.expr) << "\n"; - // int i = 0; for (const auto &constraint - // : query.constraints) { - // errs() << "C" << i++ << ": " << constraint; - // errs() << " " - // << (reqset.count(constraint) ? "(required)" : "(independent)") - // << "\n"; - // errs() << "\telts: " << IndependentElementSet(constraint) << "\n"; - // } errs() << "elts closure: " - // << eltsClosure << "\n";); - - return eltsClosure; + b->addValuesToAssignment(b->concretization.keys(), b->concretization.values(), + a->concretization); + a->concretizedSets.add(b->concretizedSets); + return a; } -void calculateArrayReferences(const IndependentElementSet &ie, - std::vector &returnVector) { +void IndependentConstraintSet::calculateArrayReferences( + std::vector &returnVector) const { std::set thisSeen; - for (std::map>::const_iterator it = - ie.elements.begin(); - it != ie.elements.end(); it++) { + for (IndependentConstraintSet::elements_ty::iterator it = elements.begin(); + it != elements.end(); ++it) { thisSeen.insert(it->first); } - for (std::set::iterator it = ie.wholeObjects.begin(); - it != ie.wholeObjects.end(); it++) { - assert(*it); + for (ImmutableSet::iterator it = wholeObjects.begin(); + it != wholeObjects.end(); ++it) { thisSeen.insert(*it); } for (std::set::iterator it = thisSeen.begin(); - it != thisSeen.end(); it++) { + it != thisSeen.end(); ++it) { returnVector.push_back(*it); } } diff --git a/lib/Solver/AssignmentValidatingSolver.cpp b/lib/Solver/AssignmentValidatingSolver.cpp index 993af59043..3bdab35df2 100644 --- a/lib/Solver/AssignmentValidatingSolver.cpp +++ b/lib/Solver/AssignmentValidatingSolver.cpp @@ -168,7 +168,8 @@ void AssignmentValidatingSolver::dumpAssignmentQuery( const Query &query, const Assignment &assignment) { // Create a Query that is augmented with constraints that // enforce the given assignment. - auto constraints = assignment.createConstraintsFromAssignment(); + auto constraints = + ConstraintSet(assignment.createConstraintsFromAssignment(), {}, {}); // Add Constraints from `query` assert(!query.containsSymcretes()); diff --git a/lib/Solver/ConcretizingSolver.cpp b/lib/Solver/ConcretizingSolver.cpp index 8d1886ae57..f4058d2b2b 100644 --- a/lib/Solver/ConcretizingSolver.cpp +++ b/lib/Solver/ConcretizingSolver.cpp @@ -54,18 +54,59 @@ class ConcretizingSolver : public SolverImpl { private: bool assertConcretization(const Query &query, const Assignment &assign) const; + bool getBrokenArrays(const Query &query, const Assignment &diff, + ref &result, + std::vector &brokenArrays); bool relaxSymcreteConstraints(const Query &query, ref &result); Query constructConcretizedQuery(const Query &, const Assignment &); + Query getConcretizedVersion(const Query &); + +private: + void reverseConcretization(ValidityCore &validityCore, + const ExprHashMap> &reverse, + ref reverseExpr); + void reverseConcretization(ref &res, + const ExprHashMap> &reverse, + ref reverseExpr); }; Query ConcretizingSolver::constructConcretizedQuery(const Query &query, const Assignment &assign) { - ConstraintSet constraints = assign.createConstraintsFromAssignment(); - for (auto e : query.constraints.cs()) { - constraints.addConstraint(e, {}); + ConstraintSet cs = query.constraints; + ref concretizedExpr = assign.evaluate(query.expr); + return Query(cs.getConcretizedVersion(assign), concretizedExpr); +} + +Query ConcretizingSolver::getConcretizedVersion(const Query &query) { + ConstraintSet cs = query.constraints; + ref concretizedExpr = cs.concretization().evaluate(query.expr); + return Query(cs.getConcretizedVersion(), concretizedExpr); +} + +void ConcretizingSolver::reverseConcretization( + ValidityCore &validityCore, const ExprHashMap> &reverse, + ref reverseExpr) { + validityCore.expr = reverseExpr; + for (auto e : reverse) { + if (validityCore.constraints.find(e.second) != + validityCore.constraints.end()) { + validityCore.constraints.erase(e.second); + validityCore.constraints.insert(e.first); + } } - return Query(constraints, query.expr); +} + +void ConcretizingSolver::reverseConcretization( + ref &res, const ExprHashMap> &reverse, + ref reverseExpr) { + if (!isa(res)) { + return; + } + ValidityCore validityCore; + res->tryGetValidityCore(validityCore); + reverseConcretization(validityCore, reverse, reverseExpr); + res = new ValidResponse(validityCore); } bool ConcretizingSolver::assertConcretization(const Query &query, @@ -79,6 +120,41 @@ bool ConcretizingSolver::assertConcretization(const Query &query, return true; } +bool ConcretizingSolver::getBrokenArrays( + const Query &query, const Assignment &assign, ref &result, + std::vector &brokenArrays) { + Query concretizedQuery = constructConcretizedQuery(query, assign); + ref CE = dyn_cast(concretizedQuery.expr); + if (CE && CE->isTrue()) { + findObjects(query.expr, brokenArrays); + result = new UnknownResponse(); + return true; + } + const ExprHashMap> &reverse = + concretizedQuery.constraints.independentElements().concretizedExprs; + ref reverseExpr = query.expr; + if (!solver->impl->check(concretizedQuery, result)) { + return false; + } + reverseConcretization(result, reverse, reverseExpr); + + /* No unsat cores were found for the query, so we can try to find new + * solution. */ + if (isa(result)) { + return true; + } + + ValidityCore validityCore; + bool success = result->tryGetValidityCore(validityCore); + assert(success); + + constraints_ty allValidityCoreConstraints = validityCore.constraints; + allValidityCoreConstraints.insert(validityCore.expr); + findObjects(allValidityCoreConstraints.begin(), + allValidityCoreConstraints.end(), brokenArrays); + return true; +} + bool ConcretizingSolver::relaxSymcreteConstraints(const Query &query, ref &result) { if (!query.containsSizeSymcretes()) { @@ -110,28 +186,17 @@ bool ConcretizingSolver::relaxSymcreteConstraints(const Query &query, bool wereConcretizationsRemoved = true; while (wereConcretizationsRemoved) { wereConcretizationsRemoved = false; - if (!solver->impl->check(constructConcretizedQuery(query, assignment), - result)) { + + std::vector currentlyBrokenSymcretizedArrays; + if (!getBrokenArrays(query, assignment, result, + currentlyBrokenSymcretizedArrays)) { return false; } - /* No unsat cores were found for the query, so we can try to find new - * solution. */ if (isa(result)) { break; } - ValidityCore validityCore; - bool success = result->tryGetValidityCore(validityCore); - assert(success); - - constraints_ty allValidityCoreConstraints = validityCore.constraints; - allValidityCoreConstraints.insert(validityCore.expr); - std::vector currentlyBrokenSymcretizedArrays; - findObjects(allValidityCoreConstraints.begin(), - allValidityCoreConstraints.end(), - currentlyBrokenSymcretizedArrays); - std::queue arrayQueue; std::queue addressQueue; @@ -161,6 +226,7 @@ bool ConcretizingSolver::relaxSymcreteConstraints(const Query &query, assignment.bindings.erase(addressQueue.front()); addressQueue.pop(); } + if (!solver->impl->check(constructConcretizedQuery(query, assignment), result)) { return false; @@ -299,8 +365,14 @@ bool ConcretizingSolver::relaxSymcreteConstraints(const Query &query, assignment.bindings[addressArray] = storage; } - if (!solver->impl->check(constructConcretizedQuery(query, assignment), - result)) { + Query concretizedQuery = constructConcretizedQuery(query, assignment); + ref CE = dyn_cast(concretizedQuery.expr); + if (CE && CE->isTrue()) { + result = new UnknownResponse(); + return true; + } + + if (!solver->impl->check(concretizedQuery, result)) { return false; } @@ -352,59 +424,21 @@ bool ConcretizingSolver::computeValidity( assert(assertConcretization(query, assign) && "Assignment does not contain concretization for all symcrete arrays!"); - auto concretizedQuery = constructConcretizedQuery(query, assign); - if (!solver->impl->computeValidity(concretizedQuery, queryResult, - negatedQueryResult)) { + if (!check(query, queryResult) || + !check(query.negateExpr(), negatedQueryResult)) { return false; } - - std::vector> queryResultValues, - negatedQueryResultValues; - - std::vector objects = assign.keys(); - - assert(isa(queryResult) || - isa(negatedQueryResult)); - - // *No more than one* of queryResult and negatedQueryResult is possible, - // i.e. `mustBeTrue` with values from `assign`. - // Take one which is `mustBeTrue` with symcretes from `assign` - // and try to relax them to `mayBeFalse`. This solution should be - // appropriate for the remain branch. - - if (isa(queryResult)) { - concretizationManager->add( - query, - cast(negatedQueryResult)->initialValuesFor(objects)); - if (!relaxSymcreteConstraints(query, queryResult)) { - return false; - } - if (ref queryInvalidResponse = - dyn_cast(queryResult)) { - concretizationManager->add( - query.negateExpr(), queryInvalidResponse->initialValuesFor(objects)); - } - } else if (isa(negatedQueryResult)) { - concretizationManager->add( - query.negateExpr(), - cast(queryResult)->initialValuesFor(objects)); - if (!relaxSymcreteConstraints(query.negateExpr(), negatedQueryResult)) { - return false; - } - if (ref negatedQueryInvalidResponse = - dyn_cast(negatedQueryResult)) { - concretizationManager->add( - query, negatedQueryInvalidResponse->initialValuesFor(objects)); - } - } else { + if (!isa(queryResult) && + isa(negatedQueryResult)) { + concretizationManager->add(query, cast(negatedQueryResult) + ->initialValuesFor(assign.keys())); + } + if (isa(queryResult) && + !isa(negatedQueryResult)) { concretizationManager->add( query.negateExpr(), - cast(queryResult)->initialValuesFor(objects)); - concretizationManager->add( - query, - cast(negatedQueryResult)->initialValuesFor(objects)); + cast(queryResult)->initialValuesFor(assign.keys())); } - return true; } @@ -417,12 +451,15 @@ bool ConcretizingSolver::check(const Query &query, assert(assertConcretization(query, assign) && "Assignment does not contain concretization for all symcrete arrays!"); - auto concretizedQuery = constructConcretizedQuery(query, assign); - if (!solver->impl->check(concretizedQuery, result)) { - return false; - } + auto concretizedQuery = getConcretizedVersion(query); - if (isa(result)) { + ref CE = dyn_cast(concretizedQuery.expr); + if (!CE || !CE->isTrue()) { + if (!solver->impl->check(concretizedQuery, result)) { + return false; + } + } + if ((CE && CE->isTrue()) || isa(result)) { if (!relaxSymcreteConstraints(query, result)) { return false; } @@ -462,8 +499,7 @@ bool ConcretizingSolver::computeTruth(const Query &query, bool &isValid) { query.constraints.concretization().evaluate(query.expr))) { isValid = CE->isTrue(); } else { - auto concretizedQuery = constructConcretizedQuery(query, assign); - + auto concretizedQuery = getConcretizedVersion(query); if (!solver->impl->computeTruth(concretizedQuery, isValid)) { return false; } @@ -502,7 +538,7 @@ bool ConcretizingSolver::computeValidityCore(const Query &query, assert(assertConcretization(query, assign) && "Assignment does not contain concretization for all symcrete arrays!"); - Query concretizedQuery = constructConcretizedQuery(query, assign); + Query concretizedQuery = getConcretizedVersion(query); if (ref CE = dyn_cast( query.constraints.concretization().evaluate(query.expr))) { @@ -556,7 +592,7 @@ bool ConcretizingSolver::computeValue(const Query &query, ref &result) { result = expr; return true; } - auto concretizedQuery = constructConcretizedQuery(query, assign); + auto concretizedQuery = getConcretizedVersion(query); return solver->impl->computeValue(concretizedQuery, result); } @@ -572,7 +608,7 @@ bool ConcretizingSolver::computeInitialValues( assert(assertConcretization(query, assign) && "Assignment does not contain concretization for all symcrete arrays!"); - auto concretizedQuery = constructConcretizedQuery(query, assign); + auto concretizedQuery = getConcretizedVersion(query); if (!solver->impl->computeInitialValues(concretizedQuery, objects, values, hasSolution)) { return false; @@ -591,9 +627,10 @@ bool ConcretizingSolver::computeInitialValues( assign = resultInvalidResponse->initialValuesFor(assign.keys()); concretizationManager->add(query.negateExpr(), assign); values = std::vector>(); - return solver->impl->computeInitialValues( - constructConcretizedQuery(query, assign), objects, values, - hasSolution); + return solver->impl + ->computeInitialValues( // initialvaluesfor objects and values + constructConcretizedQuery(query, assign), objects, values, + hasSolution); } } else { concretizationManager->add(query.negateExpr(), assign); diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 1c0a5c9cb5..8d12b7023d 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -58,31 +58,31 @@ class IndependentSolver : public SolverImpl { bool IndependentSolver::computeValidity(const Query &query, PartialValidity &result) { constraints_ty required; - IndependentElementSet eltsClosure = - getIndependentConstraints(query, required); + ref eltsClosure = + query.getIndependentConstraints(required); ConstraintSet tmp( - required, eltsClosure.symcretes, - query.constraints.concretization().part(eltsClosure.symcretes)); + required, eltsClosure->symcretes, + query.constraints.concretization().part(eltsClosure->symcretes)); return solver->impl->computeValidity(query.withConstraints(tmp), result); } bool IndependentSolver::computeTruth(const Query &query, bool &isValid) { constraints_ty required; - IndependentElementSet eltsClosure = - getIndependentConstraints(query, required); + ref eltsClosure = + query.getIndependentConstraints(required); ConstraintSet tmp( - required, eltsClosure.symcretes, - query.constraints.concretization().part(eltsClosure.symcretes)); + required, eltsClosure->symcretes, + query.constraints.concretization().part(eltsClosure->symcretes)); return solver->impl->computeTruth(query.withConstraints(tmp), isValid); } bool IndependentSolver::computeValue(const Query &query, ref &result) { constraints_ty required; - IndependentElementSet eltsClosure = - getIndependentConstraints(query, required); + ref eltsClosure = + query.getIndependentConstraints(required); ConstraintSet tmp( - required, eltsClosure.symcretes, - query.constraints.concretization().part(eltsClosure.symcretes)); + required, eltsClosure->symcretes, + query.constraints.concretization().part(eltsClosure->symcretes)); return solver->impl->computeValue(query.withConstraints(tmp), result); } @@ -144,17 +144,14 @@ bool IndependentSolver::computeInitialValues( // This is important in case we don't have any constraints but // we need initial values for requested array objects. hasSolution = true; - // FIXME: When we switch to C++11 this should be a std::unique_ptr so we don't - // need to remember to manually call delete - std::list *factors = - getAllIndependentConstraintsSets(query); + std::vector> factors; + query.getAllIndependentConstraintsSets(factors); // Used to rearrange all of the answers into the correct order - std::map> retMap; - for (std::list::iterator it = factors->begin(); - it != factors->end(); ++it) { + Assignment retMap(true); + for (ref it : factors) { std::vector arraysInFactor; - calculateArrayReferences(*it, arraysInFactor); + it->calculateArrayReferences(arraysInFactor); // Going to use this as the "fresh" expression for the Query() invocation // below assert(it->exprs.size() >= 1 && "No null/empty factors"); @@ -168,58 +165,44 @@ bool IndependentSolver::computeInitialValues( Query(tmp, ConstantExpr::alloc(0, Expr::Bool)), arraysInFactor, tempValues, hasSolution)) { values.clear(); - delete factors; + return false; } else if (!hasSolution) { values.clear(); - delete factors; + return true; } else { assert(tempValues.size() == arraysInFactor.size() && "Should be equal number arrays and answers"); - for (unsigned i = 0; i < tempValues.size(); i++) { - if (retMap.count(arraysInFactor[i])) { - // We already have an array with some partially correct answers, - // so we need to place the answers to the new query into the right - // spot while avoiding the undetermined values also in the array - SparseStorage *tempPtr = &retMap[arraysInFactor[i]]; - assert(tempPtr->size() == tempValues[i].size() && - "we're talking about the same array here"); - klee::DenseSet *ds = &(it->elements[arraysInFactor[i]]); - for (std::set::iterator it2 = ds->begin(); it2 != ds->end(); - it2++) { - unsigned index = *it2; - tempPtr->store(index, tempValues[i].load(index)); - } - } else { - // Dump all the new values into the array - retMap[arraysInFactor[i]] = tempValues[i]; - } - } + // We already have an array with some partially correct answers, + // so we need to place the answers to the new query into the right + // spot while avoiding the undetermined values also in the array + it->addValuesToAssignment(arraysInFactor, tempValues, retMap); } } - Assignment solutionAssignment(retMap, true); for (std::vector::const_iterator it = objects.begin(); it != objects.end(); it++) { const Array *arr = *it; - if (!retMap.count(arr)) { + if (!retMap.bindings.count(arr)) { // this means we have an array that is somehow related to the // constraint, but whose values aren't actually required to // satisfy the query. ref arrayConstantSize = - dyn_cast(solutionAssignment.evaluate(arr->size)); + dyn_cast(retMap.evaluate(arr->size)); assert(arrayConstantSize && "Array of symbolic size had not receive value for size!"); SparseStorage ret(arrayConstantSize->getZExtValue()); values.push_back(ret); } else { - values.push_back(retMap[arr]); + values.push_back(retMap.bindings[arr]); } } - assert(assertCreatedPointEvaluatesToTrue(query, objects, values, retMap) && + + assert(assertCreatedPointEvaluatesToTrue(query, objects, values, + retMap.bindings) && "should satisfy the equation"); - delete factors; + return true; } @@ -228,17 +211,14 @@ bool IndependentSolver::check(const Query &query, ref &result) { // This is important in case we don't have any constraints but // we need initial values for requested array objects. - // FIXME: When we switch to C++11 this should be a std::unique_ptr so we don't - // need to remember to manually call delete - std::list *factors = - getAllIndependentConstraintsSets(query); + std::vector> factors; + query.getAllIndependentConstraintsSets(factors); // Used to rearrange all of the answers into the correct order - std::map> retMap; - for (std::list::iterator it = factors->begin(); - it != factors->end(); ++it) { + Assignment retMap; + for (ref it : factors) { std::vector arraysInFactor; - calculateArrayReferences(*it, arraysInFactor); + it->calculateArrayReferences(arraysInFactor); // Going to use this as the "fresh" expression for the Query() invocation // below assert(it->exprs.size() >= 1 && "No null/empty factors"); @@ -264,10 +244,8 @@ bool IndependentSolver::check(const Query &query, ref &result) { query.constraints.concretization().part(it->symcretes)), factorExpr), tempResult)) { - delete factors; return false; } else if (isa(tempResult)) { - delete factors; result = tempResult; return true; } else { @@ -276,34 +254,20 @@ bool IndependentSolver::check(const Query &query, ref &result) { assert(success && "Can not get initial values (Independent solver)!"); assert(tempValues.size() == arraysInFactor.size() && "Should be equal number arrays and answers"); - for (unsigned i = 0; i < tempValues.size(); i++) { - if (retMap.count(arraysInFactor[i])) { - // We already have an array with some partially correct answers, - // so we need to place the answers to the new query into the right - // spot while avoiding the undetermined values also in the array - SparseStorage *tempPtr = &retMap[arraysInFactor[i]]; - assert(tempPtr->size() == tempValues[i].size() && - "we're talking about the same array here"); - klee::DenseSet *ds = &(it->elements[arraysInFactor[i]]); - for (std::set::iterator it2 = ds->begin(); it2 != ds->end(); - it2++) { - unsigned index = *it2; - tempPtr->store(index, tempValues[i].load(index)); - } - } else { - // Dump all the new values into the array - retMap[arraysInFactor[i]] = tempValues[i]; - } - } + // We already have an array with some partially correct answers, + // so we need to place the answers to the new query into the right + // spot while avoiding the undetermined values also in the array + it->addValuesToAssignment(arraysInFactor, tempValues, retMap); } } - result = new InvalidResponse(retMap); + result = new InvalidResponse(retMap.bindings); std::map> bindings; bool success = result->tryGetInitialValues(bindings); assert(success); - assert(assertCreatedPointEvaluatesToTrue(query, bindings, retMap) && + + assert(assertCreatedPointEvaluatesToTrue(query, bindings, retMap.bindings) && "should satisfy the equation"); - delete factors; + return true; } @@ -311,11 +275,11 @@ bool IndependentSolver::computeValidityCore(const Query &query, ValidityCore &validityCore, bool &isValid) { constraints_ty required; - IndependentElementSet eltsClosure = - getIndependentConstraints(query, required); + ref eltsClosure = + query.getIndependentConstraints(required); ConstraintSet tmp( - required, eltsClosure.symcretes, - query.constraints.concretization().part(eltsClosure.symcretes)); + required, eltsClosure->symcretes, + query.constraints.concretization().part(eltsClosure->symcretes)); return solver->impl->computeValidityCore(query.withConstraints(tmp), validityCore, isValid); } diff --git a/test/Feature/SymbolicSizes/ImplicitArrayExtension.c b/test/Feature/SymbolicSizes/ImplicitArrayExtension.c index 389a1adcab..2f97c3aa17 100644 --- a/test/Feature/SymbolicSizes/ImplicitArrayExtension.c +++ b/test/Feature/SymbolicSizes/ImplicitArrayExtension.c @@ -1,6 +1,8 @@ // REQUIRES: z3 // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out +// RUN: rm -rf %t.klee-outfailnew +// RUN: %klee --output-dir=%t.klee-outfailnew --out-of-mem-allocs=true --solver-backend=z3 --use-query-log=all:kquery,solver:kquery --write-kqueries %t1.bc 2> %t2.log // RUN: %klee --output-dir=%t.klee-out --out-of-mem-allocs=true --solver-backend=z3 %t1.bc 2>&1 | FileCheck %s #include "klee/klee.h"