From 35fd8bc6f86627975963ca695ebaf3ab040a3b2c Mon Sep 17 00:00:00 2001 From: Yurii Kostyukov Date: Sat, 10 Dec 2022 11:19:20 +0300 Subject: [PATCH] [feat] Return confidence and give advise --- include/klee/Core/Interpreter.h | 5 +- include/klee/Core/TargetedExecutionReporter.h | 37 ++++ include/klee/Core/TerminationTypes.h | 19 ++ include/klee/Module/Locations.h | 46 +++-- lib/Core/CMakeLists.txt | 1 + lib/Core/ExecutionState.h | 3 + lib/Core/Executor.cpp | 174 +++++++++++++++--- lib/Core/Executor.h | 16 +- lib/Core/Searcher.cpp | 9 +- lib/Core/Searcher.h | 3 + lib/Core/SpecialFunctionHandler.cpp | 2 +- lib/Core/StatsTracker.cpp | 4 +- lib/Core/Target.cpp | 29 ++- lib/Core/Target.h | 62 ++----- lib/Core/TargetForest.cpp | 19 +- lib/Core/TargetForest.h | 27 +-- lib/Core/TargetedExecutionManager.cpp | 61 ++---- lib/Core/TargetedExecutionManager.h | 25 ++- lib/Core/TargetedExecutionReporter.cpp | 59 ++++++ lib/Core/UserSearcher.cpp | 2 + lib/Module/Locations.cpp | 57 +++++- lib/Runner/parse_static_analysis_json.cpp | 23 +-- lib/Runner/run_klee.cpp | 13 +- 23 files changed, 496 insertions(+), 200 deletions(-) create mode 100644 include/klee/Core/TargetedExecutionReporter.h create mode 100644 lib/Core/TargetedExecutionReporter.cpp diff --git a/include/klee/Core/Interpreter.h b/include/klee/Core/Interpreter.h index 6ad4ca544c3..7b677c1ab8e 100644 --- a/include/klee/Core/Interpreter.h +++ b/include/klee/Core/Interpreter.h @@ -15,6 +15,8 @@ #include #include +#include "TerminationTypes.h" + struct KTest; struct TestCase; @@ -32,6 +34,7 @@ class ExecutionState; struct PathForest; class Interpreter; class TreeStreamWriter; +struct LocatedEvent; class InterpreterHandler { public: @@ -176,7 +179,7 @@ class Interpreter { char **envp) = 0; /*** Runtime options ***/ - virtual void setHaltExecution(bool value) = 0; + virtual void setHaltExecution(HaltExecution::Reason value) = 0; virtual void setInhibitForking(bool value) = 0; diff --git a/include/klee/Core/TargetedExecutionReporter.h b/include/klee/Core/TargetedExecutionReporter.h new file mode 100644 index 00000000000..a287df2c977 --- /dev/null +++ b/include/klee/Core/TargetedExecutionReporter.h @@ -0,0 +1,37 @@ +//===-- TargetedExecutionReporter.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_TARGETEDEXECUTIONREPORTER_H +#define KLEE_TARGETEDEXECUTIONREPORTER_H + +#include "klee/Module/Locations.h" + +namespace klee { + +namespace confidence { + using ty = double; + static ty MinConfidence = 0.0; + static ty MaxConfidence = 100.0; + static ty Confident = 90.0; + static ty VeryConfident = 99.0; + bool isConfident(ty conf); + bool isVeryConfident(ty conf); + bool isNormal(ty conf); + std::string toString(ty conf); + ty min(ty left, ty right); +}; + +void reportFalsePositive( + confidence::ty confidence, + LocatedEvent &event, + std::string whatToIncrease); + +} + +#endif diff --git a/include/klee/Core/TerminationTypes.h b/include/klee/Core/TerminationTypes.h index 66bfdc9f6b7..819cf9e11c2 100644 --- a/include/klee/Core/TerminationTypes.h +++ b/include/klee/Core/TerminationTypes.h @@ -55,4 +55,23 @@ enum class StateTerminationType : std::uint8_t { #undef MARK }; +namespace HaltExecution { + enum Reason { + NotHalt = 0, + MaxTests, + MaxInstructions, + MaxSteppedInstructions, + MaxTime, + BCovCheckInterval, + NoMoreStates, + ReachedTarget, + ErrorOnWhichShouldExit, + Interrupt, + MaxDepth, + MaxStackFrames, + MaxSolverTime, + Unspecified + }; +}; + #endif diff --git a/include/klee/Module/Locations.h b/include/klee/Module/Locations.h index 7e63ce39718..a0325499a15 100644 --- a/include/klee/Module/Locations.h +++ b/include/klee/Module/Locations.h @@ -17,6 +17,7 @@ #include "klee/Module/KInstruction.h" #include "klee/Module/KModule.h" #include "klee/Module/InstructionInfoTable.h" +#include "klee/ADT/Ref.h" namespace klee { @@ -49,6 +50,9 @@ class Location { const std::string function; const std::string filename; + /// @brief Required by klee::ref-managed objects + class ReferenceCounter _refCount; + Location(const std::string &f, const std::string &function, unsigned line, unsigned offset, unsigned column, unsigned instructionOpcode) : line(line), offset(offset), column(column), instructionOpcode(instructionOpcode), function(function), filename(f) {} Location(const std::string &f, const std::string &function) @@ -68,19 +72,14 @@ class Location { std::set initInstructions(KModule *origModule, KModule *kleeModule, std::ostringstream &error); + int compare(const Location &other) const; + friend bool operator <(const Location& lhs, const Location& rhs) { - return - lhs.line < rhs.line || (lhs.line == rhs.line && - (lhs.offset < rhs.offset || (lhs.offset == rhs.offset && - (lhs.filename < rhs.filename || (lhs.filename == rhs.filename && - (lhs.function < rhs.function || (lhs.function == rhs.function && - (lhs.instructions < rhs.instructions)))))))); + return lhs.compare(rhs) < 0; } friend bool operator==(const Location &lhs, const Location &rhs) { - return lhs.line == rhs.line && lhs.offset == rhs.offset && - lhs.filename == rhs.filename && lhs.function == rhs.function && - lhs.instructions == rhs.instructions; + return lhs.compare(rhs) == 0; } friend bool operator!=(const Location &lhs, const Location &rhs) { @@ -89,16 +88,37 @@ class Location { }; struct LocatedEvent { - Location location; +private: + ref location; ReachWithError error; - unsigned id = 0; + unsigned id; + +public: + LocatedEvent(Location *location, ReachWithError error, unsigned id) + : location(location), error(error), id(id) {} + + LocatedEvent(Location *location, unsigned id) + : LocatedEvent(location, ReachWithError::None, id) {} - LocatedEvent(Location location, ReachWithError error) : location(location), error(error) {} + LocatedEvent(Location *location) + : LocatedEvent(location, 0) {} + + explicit LocatedEvent() : LocatedEvent(nullptr) {} bool hasFunctionWithOffset() { - return location.hasFunctionWithOffset(); + return location->hasFunctionWithOffset(); } + int compare(const LocatedEvent &other) const; + bool operator<(const LocatedEvent &other) const; + bool operator==(const LocatedEvent &other) const; + ReachWithError getError() const { return error; } + const char *getErrorString() const { return ReachWithErrorNames[error]; } + unsigned getId() const { return id; } + ref getLocation() const { return location; } + bool shouldFailOnThisTarget() const { return error != ReachWithError::None; } + void setErrorReachableIfNone(); + std::string toString() const; }; diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt index 7544683d425..310103fc46e 100644 --- a/lib/Core/CMakeLists.txt +++ b/lib/Core/CMakeLists.txt @@ -14,6 +14,7 @@ klee_add_component(kleeCore CoreStats.cpp CXXTypeSystem/CXXTypeManager.cpp ExecutionState.cpp + TargetedExecutionReporter.cpp TargetForest.cpp TargetedExecutionManager.cpp Executor.cpp diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index 6b07e4e867f..7b7f0ec9222 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -18,6 +18,7 @@ #include "klee/ADT/ImmutableSet.h" #include "klee/ADT/TreeStream.h" +#include "klee/Core/TerminationTypes.h" #include "klee/Expr/Assignment.h" #include "klee/Expr/Constraints.h" #include "klee/Expr/Expr.h" @@ -287,6 +288,8 @@ class ExecutionState { ReachWithError error = ReachWithError::None; + HaltExecution::Reason terminationReasonType = HaltExecution::NotHalt; + ExprHashMap, llvm::Type *>> gepExprBases; public: diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 09a00771b54..86e39d1bc27 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -34,6 +34,7 @@ #include "klee/Config/config.h" #include "klee/Config/Version.h" #include "klee/Core/Interpreter.h" +#include "klee/Core/TargetedExecutionReporter.h" #include "klee/Expr/ArrayExprOptimizer.h" #include "klee/Expr/ArrayExprVisitor.h" #include "klee/Expr/Assignment.h" @@ -553,13 +554,118 @@ bool Interpreter::hasTargetForest() const { return false; } +TargetedHaltsOnTraces::TargetedHaltsOnTraces(ref &forest) { + auto leafs = forest->leafs(); + for (auto finalTargetPair : *leafs) { + traceToHaltTypeToConfidence.emplace(finalTargetPair.first, HaltTypeToConfidence()); + } + delete leafs; +} + +void TargetedHaltsOnTraces::subtractConfidencesFrom(TargetForest &forest, HaltExecution::Reason reason) { + auto leafs = forest.leafs(); + for (auto finalTargetPair : *leafs) { + auto &haltTypeToConfidence = traceToHaltTypeToConfidence.at(finalTargetPair.first); + auto confidence = finalTargetPair.second; + auto it = haltTypeToConfidence.find(reason); + if (it == haltTypeToConfidence.end()) { + haltTypeToConfidence.emplace(reason, confidence); + } else { + haltTypeToConfidence[reason] = it->second + confidence; + } + } + delete leafs; +} + +void TargetedHaltsOnTraces::totalConfidenceAndTopContributor( + const HaltTypeToConfidence &haltTypeToConfidence, + confidence::ty *confidence, + HaltExecution::Reason *reason) +{ + *confidence = confidence::MaxConfidence; + HaltExecution::Reason maxReason = HaltExecution::MaxTime; + confidence::ty maxConfidence = confidence::MinConfidence; + for (auto p : haltTypeToConfidence) { + auto r = p.first; + auto c = p.second; + if (c > maxConfidence) { + maxConfidence = c; + maxReason = r; + } + *confidence -= c; + } + *reason = maxReason; +} + +std::string getAdviseWhatToIncreaseConfidenceRate(HaltExecution::Reason reason) { + std::string what = ""; + switch (reason) { + case HaltExecution::MaxSolverTime: + what = MaxCoreSolverTime.ArgStr.str(); + break; + case HaltExecution::MaxStackFrames: + what = RuntimeMaxStackFrames.ArgStr.str(); + break; + case HaltExecution::MaxTests: + what = "max-tests"; //TODO: taken from run_klee.cpp + break; + case HaltExecution::MaxInstructions: + what = MaxInstructions.ArgStr.str(); + break; + case HaltExecution::MaxSteppedInstructions: + what = MaxSteppedInstructions.ArgStr.str(); + break; + case HaltExecution::BCovCheckInterval: + what = "bcov-check-interval"; //TODO: taken from StatsTracker.cpp + break; + case HaltExecution::MaxDepth: + what = MaxDepth.ArgStr.str(); + break; + case HaltExecution::ErrorOnWhichShouldExit: // this should never be the case + case HaltExecution::ReachedTarget: // this should never be the case + case HaltExecution::NoMoreStates: // this should never be the case + case HaltExecution::Interrupt: // it is ok to advise to increase time if we were interrupted by user + case HaltExecution::MaxTime: +#ifndef ENABLE_KLEE_DEBUG + default: +#endif + what = MaxTime.ArgStr.str(); + break; +#ifdef ENABLE_KLEE_DEBUG + default: + what = std::to_string(reason); + break; +#endif + } + return what; +} + +void TargetedHaltsOnTraces::reportFalsePositives(bool canReachSomeTarget) { + confidence::ty confidence; + HaltExecution::Reason reason; + for (const auto &targetWithConfidences : traceToHaltTypeToConfidence) { + auto target = targetWithConfidences.first; + if (!target->shouldFailOnThisTarget()) + continue; + if (target->isReported) + continue; + totalConfidenceAndTopContributor(targetWithConfidences.second, &confidence, &reason); + if (canReachSomeTarget && confidence::isVeryConfident(confidence)) {// We should not be so sure if there are states that can reach some targets + confidence = confidence::VeryConfident; + reason = HaltExecution::MaxTime; + } + reportFalsePositive(confidence, *target, getAdviseWhatToIncreaseConfidenceRate(reason)); + target->isReported = true; + } +} + Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, InterpreterHandler *ih) : Interpreter(opts), interpreterHandler(ih), searcher(0), externalDispatcher(new ExternalDispatcher(ctx)), statsTracker(0), pathWriter(0), symPathWriter(0), specialFunctionHandler(0), timers{time::Span(TimerInterval)}, codeGraphDistance(new CodeGraphDistance()), replayKTest(0), replayPath(0), usingSeeds(0), - atMemoryLimit(false), inhibitForking(false), haltExecution(false), + atMemoryLimit(false), inhibitForking(false), haltExecution(HaltExecution::NotHalt), ivcEnabled(false), debugLogBuffer(debugBufferString) { @@ -571,7 +677,7 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, if (maxTime) timers.add(std::make_unique(maxTime, [&] { klee_message("HaltTimer invoked"); - setHaltExecution(true); + setHaltExecution(HaltExecution::MaxTime); })); } @@ -1635,10 +1741,10 @@ void Executor::stepInstruction(ExecutionState &state) { ++state.pc; if (stats::instructions == MaxInstructions) - haltExecution = true; + haltExecution = HaltExecution::MaxInstructions; if (MaxSteppedInstructions && state.steppedInstructions >= MaxSteppedInstructions) - haltExecution = true; + haltExecution = HaltExecution::MaxSteppedInstructions; } static inline const llvm::fltSemantics *fpWidthToSemantics(unsigned width) { @@ -3836,7 +3942,7 @@ void Executor::updateStates(ExecutionState *current) { if (searcher) { searcher->update(current, addedStates, removedStates); } - + states.insert(addedStates.begin(), addedStates.end()); addedStates.clear(); @@ -3854,6 +3960,7 @@ void Executor::updateStates(ExecutionState *current) { processForest->remove(es->ptreeNode); delete es; } + removedButReachableStates.clear(); removedStates.clear(); } @@ -3973,16 +4080,17 @@ bool Executor::checkMemoryUsage() { return false; } -bool Executor::decreaseConfidenceFromStoppedStates(std::set &left_states) { +bool Executor::decreaseConfidenceFromStoppedStates(SetOfStates &left_states, HaltExecution::Reason reason) { bool hasStateWhichCanReachSomeTarget = false; for (auto state : left_states) { if (state->targetForest.empty()) continue; hasStateWhichCanReachSomeTarget = true; + auto realReason = reason ? reason : state->terminationReasonType; if (state->progress_velocity >= 0) { assert(targets.count(state->targetForest.getEntryFunction()) != 0); targets.at(state->targetForest.getEntryFunction()) - ->subtract_confidences_from(state->targetForest); + .subtractConfidencesFrom(state->targetForest, realReason); } } return hasStateWhichCanReachSomeTarget; @@ -4104,16 +4212,15 @@ void Executor::run(std::vector initialStates) { } if (searcher->empty()) - haltExecution = true; + haltExecution = HaltExecution::NoMoreStates; } if (guidanceKind == GuidanceKind::ErrorGuidance) { bool canReachNew1 = decreaseConfidenceFromStoppedStates(pausedStates); - bool canReachNew2 = decreaseConfidenceFromStoppedStates(states); + bool canReachNew2 = decreaseConfidenceFromStoppedStates(states, haltExecution); for (auto &startBlockAndWhiteList : targets) { - targetedExecutionManager.reportFalsePositives(startBlockAndWhiteList.second, - canReachNew1 || canReachNew2); + startBlockAndWhiteList.second.reportFalsePositives(canReachNew1 || canReachNew2); } } @@ -4121,7 +4228,7 @@ void Executor::run(std::vector initialStates) { searcher = nullptr; doDumpStates(); - haltExecution = false; + haltExecution = HaltExecution::NotHalt; } void Executor::runWithTarget(ExecutionState &state, KFunction *kf, @@ -4253,7 +4360,7 @@ void Executor::targetedRun(ExecutionState &initialState, KBlock *target, Executi *resultState = state.copy(); terminateStateOnTerminator(state); updateStates(&state); - haltExecution = true; + haltExecution = HaltExecution::ReachedTarget; break; } @@ -4265,7 +4372,7 @@ void Executor::targetedRun(ExecutionState &initialState, KBlock *target, Executi doDumpStates(); if (*resultState) - haltExecution = false; + haltExecution = HaltExecution::NotHalt; } std::string Executor::getAddressInfo(ExecutionState &state, ref address, @@ -4325,7 +4432,21 @@ std::string Executor::getAddressInfo(ExecutionState &state, ref address, return info.str(); } -void Executor::terminateState(ExecutionState &state) { +HaltExecution::Reason fromStateTerminationType(StateTerminationType t) { + switch (t) { + case StateTerminationType::MaxDepth: + return HaltExecution::MaxDepth; + case StateTerminationType::OutOfStackMemory: + return HaltExecution::MaxStackFrames; + case StateTerminationType::Solver: + return HaltExecution::MaxSolverTime; + default: + return HaltExecution::Unspecified; + } +} + +void Executor::terminateState(ExecutionState &state, StateTerminationType terminationType) { + state.terminationReasonType = fromStateTerminationType(terminationType); if (replayKTest && replayPosition!=replayKTest->numObjects) { klee_warning_once(replayKTest, "replay did not consume all objects in test input."); @@ -4372,14 +4493,15 @@ void Executor::unpauseState(ExecutionState &state) { } void Executor::terminateStateOnExit(ExecutionState &state) { + auto terminationType = StateTerminationType::Exit; if (shouldWriteTest(state) || (AlwaysOutputSeeds && seedMap.count(&state))) interpreterHandler->processTestCase( state, nullptr, - terminationTypeFileExtension(StateTerminationType::Exit).c_str()); + terminationTypeFileExtension(terminationType).c_str()); interpreterHandler->incPathsCompleted(); targetCalculator->update(state); - terminateState(state); + terminateState(state, terminationType); } void Executor::terminateStateEarly(ExecutionState &state, const Twine &message, @@ -4391,7 +4513,7 @@ void Executor::terminateStateEarly(ExecutionState &state, const Twine &message, state, (message + "\n").str().c_str(), terminationTypeFileExtension(terminationType).c_str()); } - terminateState(state); + terminateState(state, terminationType); } void Executor::terminateStateOnTerminator(ExecutionState &state) { @@ -4399,7 +4521,7 @@ void Executor::terminateStateOnTerminator(ExecutionState &state) { interpreterHandler->processTestCase(state, nullptr, nullptr); } targetCalculator->update(state); - terminateState(state); + terminateState(state, StateTerminationType::SilentExit); } void Executor::terminateStateOnUserError(ExecutionState &state, const llvm::Twine &message) { @@ -4535,10 +4657,10 @@ void Executor::terminateStateOnError(ExecutionState &state, } targetCalculator->update(state); - terminateState(state); + terminateState(state, terminationType); if (shouldExitOn(terminationType)) - haltExecution = true; + haltExecution = HaltExecution::ErrorOnWhichShouldExit; } void Executor::terminateStateOnExecError(ExecutionState &state, @@ -5805,23 +5927,25 @@ void Executor::runThroughLocationsInternal(ExecutionState *state, PathForest *pa state->popFrame(); } - targets = targetedExecutionManager.prepareTargets(kmoduleOrig.get(), kmodule.get(), paths); - if (targets.empty()) { + auto prepTargets = targetedExecutionManager.prepareTargets(kmoduleOrig.get(), kmodule.get(), paths); + if (prepTargets.empty()) { klee_warning("No targets found in --error-guided mode"); return; } std::vector initialStates; - for (auto &startBlockAndWhiteList : targets) { + for (auto &startBlockAndWhiteList : prepTargets) { auto kf = startBlockAndWhiteList.first; if (startBlockAndWhiteList.second->empty()) { klee_warning("No targets found for %s", kf->function->getName().str().c_str()); continue; } + auto whitelist = startBlockAndWhiteList.second; + targets.emplace(kf, TargetedHaltsOnTraces(whitelist)); ExecutionState *initialState = state->withStackFrame(caller, kf); prepareSymbolicArgs(*initialState, kf); - prepareTargetedExecution(initialState, startBlockAndWhiteList.second); + prepareTargetedExecution(initialState, whitelist); initialStates.push_back(initialState); } runGuided(initialStates); diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 5e2035b5282..5ecf7896830 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -118,6 +118,7 @@ class Executor : public Interpreter { RNG theRNG; private: + using SetOfStates = std::set; /* Set of Intrinsic::ID. Plain type is used here to avoid including llvm in the header */ static const std::unordered_set supportedFPIntrinsics; static const std::unordered_set modelledFPIntrinsics; @@ -132,8 +133,9 @@ class Executor : public Interpreter { MemoryManager *memory; TypeManager *typeSystemManager; - std::set states; - std::set pausedStates; + SetOfStates states; + SetOfStates pausedStates; + SetOfStates removedButReachableStates; StatsTracker *statsTracker; TreeStreamWriter *pathWriter, *symPathWriter; SpecialFunctionHandler *specialFunctionHandler; @@ -200,7 +202,7 @@ class Executor : public Interpreter { /// Signals the executor to halt execution at the next instruction /// step. - std::atomic_bool haltExecution; + HaltExecution::Reason haltExecution = HaltExecution::NotHalt; /// Whether implied-value concretization is enabled. Currently /// false, it is buggy (it needs to validate its writes). @@ -232,7 +234,7 @@ class Executor : public Interpreter { /// `nullptr` if merging is disabled MergingSearcher *mergingSearcher = nullptr; - std::unordered_map> targets; + std::unordered_map targets; /// Typeids used during exception handling std::vector> eh_typeids; @@ -466,7 +468,7 @@ class Executor : public Interpreter { llvm::Instruction** lastInstruction); /// Remove state from queue and delete state - void terminateState(ExecutionState &state); + void terminateState(ExecutionState &state, StateTerminationType terminationType); // pause state void pauseState(ExecutionState &state); @@ -525,7 +527,7 @@ class Executor : public Interpreter { void increaseProgressVelocity(ExecutionState &state, KBlock *block); - bool decreaseConfidenceFromStoppedStates(std::set &left_states); + bool decreaseConfidenceFromStoppedStates(SetOfStates &left_states, HaltExecution::Reason reason = HaltExecution::NotHalt); template void computeOffsetsSeqTy(KGEPInstruction *kgepi, @@ -634,7 +636,7 @@ class Executor : public Interpreter { /*** Runtime options ***/ - void setHaltExecution(bool value) override { haltExecution = value; } + void setHaltExecution(HaltExecution::Reason value) override { haltExecution = value; } void setInhibitForking(bool value) override { inhibitForking = value; } diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index a5c3e3b6b3c..32d50344aa4 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -290,7 +290,6 @@ TargetedSearcher::tryGetWeight(ExecutionState *es, weight_type &weight) { BasicBlock *bb = es->getPCBlock(); KBlock *kb = es->pc->parent->parent->blockMap[bb]; - KInstruction *ki = es->pc; unsigned int minCallWeight = UINT_MAX, minSfNum = UINT_MAX, sfNum = 0; for (auto sfi = es->stack.rbegin(), sfe = es->stack.rend(); sfi != sfe; @@ -447,18 +446,22 @@ void TargetedSearcher::removeReached() { GuidedSearcher::GuidedSearcher( Searcher *baseSearcher, CodeGraphDistance &codeGraphDistance, TargetCalculator &stateHistory, + std::set &removedButReachableStates, std::set &pausedStates, std::size_t bound, RNG &rng) : guidance(CoverageGuidance), baseSearcher(baseSearcher), codeGraphDistance(codeGraphDistance), stateHistory(&stateHistory), + removedButReachableStates(removedButReachableStates), pausedStates(pausedStates), bound(bound), theRNG(rng) {} GuidedSearcher::GuidedSearcher( CodeGraphDistance &codeGraphDistance, + std::set &removedButReachableStates, std::set &pausedStates, std::size_t bound, RNG &rng) : guidance(ErrorGuidance), baseSearcher(nullptr), codeGraphDistance(codeGraphDistance), stateHistory(nullptr), + removedButReachableStates(removedButReachableStates), pausedStates(pausedStates), bound(bound), theRNG(rng) {} ExecutionState &GuidedSearcher::selectState() { @@ -701,8 +704,10 @@ void GuidedSearcher::innerUpdate( bool canReach = updateTargetedSearcher(history, target, nullptr, tmpAddedStates, tmpRemovedStates); - if (canReach) + if (canReach) { reachableStatesOfTarget.insert(target); + removedButReachableStates.insert(state); + } tmpAddedStates.clear(); tmpRemovedStates.clear(); } diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index b5dbfbfc500..ad32be66e4b 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -203,6 +203,7 @@ namespace klee { CodeGraphDistance &codeGraphDistance; TargetCalculator *stateHistory; TargetForestHisoryToTargetSet reachedTargets; + std::set &removedButReachableStates; std::set &pausedStates; std::size_t bound; RNG &theRNG; @@ -235,10 +236,12 @@ namespace klee { GuidedSearcher( Searcher *baseSearcher, CodeGraphDistance &codeGraphDistance, TargetCalculator &stateHistory, + std::set &removedButReachableStates, std::set &pausedStates, std::size_t bound, RNG &rng); GuidedSearcher( CodeGraphDistance &codeGraphDistance, + std::set &removedButReachableStates, std::set &pausedStates, std::size_t bound, RNG &rng); ~GuidedSearcher() override = default; diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 2ca6ff6a81e..2123d0e2f10 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -623,7 +623,7 @@ void SpecialFunctionHandler::handleAssume(ExecutionState &state, assert(success && "FIXME: Unhandled solver failure"); if (res) { if (SilentKleeAssume) { - executor.terminateState(state); + executor.terminateState(state, StateTerminationType::SilentExit); } else { executor.terminateStateOnUserError( state, "invalid klee_assume call (provably false)"); diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index f5ed2d88f8c..a7f15b5eacf 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -301,8 +301,8 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename, totalBranches = 2 * fullBranches + partialBranches; } else { klee_message( - "HaltTimer invoked due to absense of progress in branch coverage"); - executor.setHaltExecution(true); + "HaltTimer invoked due to absence of progress in branch coverage"); + executor.setHaltExecution(HaltExecution::BCovCheckInterval); } })); } diff --git a/lib/Core/Target.cpp b/lib/Core/Target.cpp index a4b81abd870..504083e197c 100644 --- a/lib/Core/Target.cpp +++ b/lib/Core/Target.cpp @@ -36,7 +36,7 @@ llvm::cl::opt TargetCalculatorMode( std::string Target::toString() const { std::ostringstream repr; - repr << "Target " << id << ": "; + repr << "Target " << getId() << ": "; if (shouldFailOnThisTarget()) { repr << "error in "; } @@ -50,9 +50,7 @@ std::string Target::toString() const { Target::EquivTargetHashSet Target::cachedTargets; Target::TargetHashSet Target::targets; -ref Target::create(Location *_location, KBlock *_block, - ReachWithError error, unsigned id) { - Target *target = new Target(_location, _block, error, id); +ref Target::getFromCacheOrReturn(Target *target) { std::pair success = cachedTargets.insert(target); if (success.second) { @@ -66,12 +64,29 @@ ref Target::create(Location *_location, KBlock *_block, return target; } -ref Target::create(KBlock *_block, ReachWithError error) { - return create(nullptr, _block, error, 0); +ref Target::create(LocatedEvent *_le, KBlock *_block) { + Target *target = new Target(_le, _block); + return getFromCacheOrReturn(target); } ref Target::create(KBlock *_block) { - return create(_block, ReachWithError::None); + return create(nullptr, _block); +} + +int Target::compare(const Target &other) const { + if (block != other.block) { + return block < other.block ? -1 : 1; + } + return this->LocatedEvent::compare(other); +} + +bool Target::operator<(const Target &other) const { + return + block < other.block || (block == other.block && this->LocatedEvent::operator<(other)); +} + +bool Target::operator==(const Target &other) const { + return block == other.block && this->LocatedEvent::operator==(other); } Target::~Target() { diff --git a/lib/Core/Target.h b/lib/Core/Target.h index 1d77641a16d..69b58b0e5be 100644 --- a/lib/Core/Target.h +++ b/lib/Core/Target.h @@ -38,21 +38,19 @@ struct TargetCmp; enum TargetCalculateBy { Default, Blocks, Transitions }; -struct Target { +struct Target : LocatedEvent { private: typedef std::unordered_set EquivTargetHashSet; typedef std::unordered_set TargetHashSet; static EquivTargetHashSet cachedTargets; static TargetHashSet targets; - Location *location; KBlock *block; - ReachWithError error; - unsigned id = 0; - explicit Target(Location *_location, KBlock *_block, ReachWithError error, - unsigned id) - : location(_location), block(_block), error(error), id(id) {} + explicit Target(LocatedEvent *_le, KBlock *_block) + : LocatedEvent(_le ? *_le : LocatedEvent()), block(_block) {} + + static ref getFromCacheOrReturn(Target *target); public: bool isReported = false; @@ -60,56 +58,18 @@ struct Target { class ReferenceCounter _refCount; - static ref create(Location *_location, KBlock *_block, - ReachWithError error, unsigned id); - static ref create(KBlock *_block, ReachWithError error); - static ref - create(KBlock *_block); // TODO: [Aleksandr Misonizhnik], I think, this - // constructor should be entirely deleted - - int compare(const Target &other) const { - if (error != other.error) { - return error < other.error ? -1 : 1; - } - if (block != other.block) { - return block < other.block ? -1 : 1; - } - if (location == nullptr || other.location == nullptr) { - if (location != other.location) { - return location < other.location ? -1 : 1; - } else { - return 0; - } - } - if (*location != *other.location) { - return (*location < *other.location) ? -1 : 1; - } - if (id != other.id) { - return id < other.id ? -1 : 1; - } - return 0; - } + static ref create(LocatedEvent *_le, KBlock *_block); + static ref create(KBlock *_block); - bool operator<(const Target &other) const { - return - block < other.block || (block == other.block && - (error < other.error || (error == other.error && - (location < other.location || (location == other.location && - (id < other.id)))))); - } + int compare(const Target &other) const; - bool operator==(const Target &other) const { - return block == other.block && error == other.error && - location == other.location && id == other.id; - } + bool operator<(const Target &other) const; + + bool operator==(const Target &other) const; bool atReturn() const { return isa(block); } KBlock *getBlock() const { return block; } - ReachWithError getError() const { return error; } - unsigned getId() const { return id; } - Location *getLocation() const { return location; } - bool shouldFailOnThisTarget() const { return error != ReachWithError::None; } bool isNull() const { return block == nullptr; } diff --git a/lib/Core/TargetForest.cpp b/lib/Core/TargetForest.cpp index 55d2c6ca0cc..db6df5ed4fb 100644 --- a/lib/Core/TargetForest.cpp +++ b/lib/Core/TargetForest.cpp @@ -10,12 +10,11 @@ #include "TargetForest.h" #include "klee/Module/KModule.h" #include "klee/Module/KInstruction.h" +#include "klee/Core/TargetedExecutionReporter.h" using namespace klee; using namespace llvm; -const TargetForest::confidence_ty TargetForest::MAX_CONFIDENCE = 100.0; - void TargetForest::Layer::pathForestToTargetForest( TargetForest::Layer *self, PathForest *pathForest, @@ -326,8 +325,8 @@ bool TargetForest::allNodesRefCountOne() const { } void TargetForest::Layer::addLeafs( - std::vector, TargetForest::confidence_ty> > *leafs, - TargetForest::confidence_ty parentConfidence) const { + std::vector, confidence::ty> > *leafs, + confidence::ty parentConfidence) const { for (const auto &targetAndForest : forest) { auto target = targetAndForest.first; auto layer = targetAndForest.second; @@ -340,8 +339,8 @@ void TargetForest::Layer::addLeafs( } } -std::vector, TargetForest::confidence_ty> > *TargetForest::leafs() const { - auto leafs = new std::vector, TargetForest::confidence_ty> >(); +std::vector, confidence::ty> > *TargetForest::leafs() const { + auto leafs = new std::vector, confidence::ty> >(); forest->addLeafs(leafs, forest->getConfidence()); return leafs; } @@ -349,10 +348,10 @@ std::vector, TargetForest::confidence_ty> > *TargetForest: void TargetForest::subtract_confidences_from(TargetForest &other) { if (other.empty()) return; - forest->subtract_confidences_from(other.forest, other.forest->getConfidence()); + forest->subtract_confidences_from(other.forest, forest->getConfidence()); } -void TargetForest::Layer::subtract_confidences_from(ref other, TargetForest::confidence_ty parentConfidence) { +void TargetForest::Layer::subtract_confidences_from(ref other, confidence::ty parentConfidence) { for (auto &targetAndForest : forest) { auto target = targetAndForest.first; auto &layer = targetAndForest.second; @@ -361,8 +360,8 @@ void TargetForest::Layer::subtract_confidences_from(ref other, TargetFore layer->subtract_confidences_from(other, layer->getConfidence(parentConfidence)); else { layer->confidence = layer->getConfidence(parentConfidence) - other_layer_it->second->confidence; - if (layer->confidence < 0) { - layer->confidence = 0.00; // TODO: we have some bug which we do not want the user to see + if (confidence::isNormal(layer->confidence)) { + layer->confidence = confidence::MinConfidence; // TODO: we have some bug which we do not want the user to see } } } diff --git a/lib/Core/TargetForest.h b/lib/Core/TargetForest.h index 8dc9154584a..8825c82a7bb 100644 --- a/lib/Core/TargetForest.h +++ b/lib/Core/TargetForest.h @@ -19,6 +19,7 @@ #include "klee/ADT/Ref.h" #include "klee/Module/KModule.h" #include "klee/Module/Locations.h" +#include "klee/Core/TargetedExecutionReporter.h" #include @@ -32,23 +33,23 @@ struct TargetsHistoryCmp; class TargetForest { public: using TargetsSet = std::unordered_set, RefTargetHash, RefTargetCmp>; - using confidence_ty = double; private: - static const confidence_ty MAX_CONFIDENCE; class Layer { using InternalLayer = std::unordered_map, ref, RefTargetHash, RefTargetCmp>; InternalLayer forest; /// @brief Confidence in % that this layer (i.e., parent target node) can be reached - confidence_ty confidence; + confidence::ty confidence; - Layer(const InternalLayer &forest, confidence_ty confidence) : forest(forest), confidence(confidence) {} + Layer(const InternalLayer &forest, confidence::ty confidence) : forest(forest), confidence(confidence) {} explicit Layer(const Layer *layer) : Layer(layer->forest, layer->confidence) {} explicit Layer(const ref layer) : Layer(layer.get()) {} void unionWith(Layer *other); void block(ref target); - confidence_ty getConfidence(confidence_ty parentConfidence) const { return fmin(parentConfidence, confidence); } + confidence::ty getConfidence(confidence::ty parentConfidence) const { + return confidence::min(parentConfidence, confidence); + } static void pathForestToTargetForest( Layer *self, @@ -67,7 +68,7 @@ class TargetForest { /// @brief Required by klee::ref-managed objects class ReferenceCounter _refCount; - explicit Layer() : confidence(MAX_CONFIDENCE) {} + explicit Layer() : confidence(confidence::MaxConfidence) {} Layer(PathForest *pathForest, std::unordered_map &loc2Targets, std::unordered_set &broken_traces); iterator find(ref b) const { return forest.find(b); } @@ -85,16 +86,16 @@ class TargetForest { Layer *blockLeaf(ref leaf) const; bool allNodesRefCountOne() const; void dump(unsigned n) const; - void addLeafs(std::vector, confidence_ty> > *leafs, - confidence_ty parentConfidence) const; + void addLeafs(std::vector, confidence::ty> > *leafs, + confidence::ty parentConfidence) const; void propagateConfidenceToChildren(); - void subtract_confidences_from(ref other, confidence_ty parentConfidence); - void addTargetWithConfidence(ref target, confidence_ty confidence); + void subtract_confidences_from(ref other, confidence::ty parentConfidence); + void addTargetWithConfidence(ref target, confidence::ty confidence); ref deep_copy(); Layer *copy(); void divideConfidenceBy(unsigned factor); Layer *divideConfidenceBy(std::multiset > &reachableStatesOfTarget); - confidence_ty getConfidence() const { return getConfidence(MAX_CONFIDENCE); } + confidence::ty getConfidence() const { return getConfidence(confidence::MaxConfidence); } void collectHowManyEventsInTracesWereReached(std::unordered_map> &trace2eventCount) const { collectHowManyEventsInTracesWereReached(trace2eventCount, 0, 0); } @@ -187,9 +188,9 @@ class TargetForest { const ref getHistory() { return history; }; const ref getTargets() { return forest; }; void dump() const; - std::vector, confidence_ty> > *leafs() const; + std::vector, confidence::ty> > *leafs() const; void subtract_confidences_from(TargetForest &other); - void addTargetWithConfidence(ref target, confidence_ty confidence) { forest->addTargetWithConfidence(target, confidence); } + void addTargetWithConfidence(ref target, confidence::ty confidence) { forest->addTargetWithConfidence(target, confidence); } ref deep_copy(); void divideConfidenceBy(unsigned factor) { forest->divideConfidenceBy(factor); } void divideConfidenceBy(std::multiset > &reachableStatesOfTarget) { diff --git a/lib/Core/TargetedExecutionManager.cpp b/lib/Core/TargetedExecutionManager.cpp index 8bd8d412d78..bc0a5d02405 100644 --- a/lib/Core/TargetedExecutionManager.cpp +++ b/lib/Core/TargetedExecutionManager.cpp @@ -86,7 +86,7 @@ void collectLocations(PathForest *pathForest) { } ref addNewLocation(LocatedEvent *le, KBlock *block) const { - auto error = le->error; + auto error = le->getError(); auto error2targetIt = tem->location2targets.find(le); TargetedExecutionManager::Error2Targets *error2target = nullptr; if (error2targetIt == tem->location2targets.end()) { @@ -106,9 +106,9 @@ ref addNewLocation(LocatedEvent *le, KBlock *block) const { ref target; if (error != None) { - target = Target::create(&le->location, block, error, le->id); + target = Target::create(le, block); } else { - target = Target::create(block, error); + target = Target::create(block); } targets->push_back(target); @@ -131,13 +131,13 @@ void prepareFilenameLineLocations(std::unordered_mapsecond; } - auto &loc = le->location; - if (!lem.isInside(loc, fi)) + auto loc = le->getLocation(); + if (!lem.isInside(*loc, fi)) continue; bool addedNewTargets = false; for (const auto &kblock : kfunc->blocks) { auto b = kblock.get(); - if (!loc.isInside(b)) + if (!loc->isInside(b)) continue; auto target = addNewLocation(le, b); targetsForThisLoc->insert(target); @@ -156,19 +156,19 @@ void prepareFunctionOffsetLocations( std::unordered_set &broken_traces) { for (auto le : functionOffsetLocations) { - auto &loc = le->location; + auto loc = le->getLocation(); KBlock *block = nullptr; auto it = tem->location2targets.find(le); if (it == tem->location2targets.end()) { std::ostringstream error; - auto instrs = loc.initInstructions(origModule, kmodule, error); + auto instrs = loc->initInstructions(origModule, kmodule, error); if (instrs.empty()) { klee_warning("Trace %u is malformed! %s at location %s, so skipping this trace.", - le->id, error.str().c_str(), loc.toString().c_str()); - broken_traces.insert(le->id); + le->getId(), error.str().c_str(), loc->toString().c_str()); + broken_traces.insert(le->getId()); continue; } - if (le->error == ReachWithError::None) { + if (le->shouldFailOnThisTarget()) { for (auto instr : instrs) { block = instr->parent; addNewLocation(le, block); @@ -186,7 +186,7 @@ void prepareFunctionOffsetLocations( auto targets = new TargetForest::TargetsSet(); for (auto &p : *it->second) { for (auto &t : *p.second) { - if (t->shouldFailOnThisTarget() && t->getId() != loc->id) + if (t->shouldFailOnThisTarget() && t->getId() != loc->getId()) continue; targets->insert(t); } @@ -199,7 +199,7 @@ void prepareFunctionOffsetLocations( void addBrokenTraces(PathForest *pathForest, std::unordered_set &all_broken_traces) { for (auto &p : pathForest->layer) { - all_broken_traces.insert(p.first->id); + all_broken_traces.insert(p.first->getId()); addBrokenTraces(p.second, all_broken_traces); } } @@ -212,7 +212,7 @@ void collectBrokenTraces(PathForest *pathForest, for (auto &p : pathForest->layer) { auto it = loc2Targets.find(p.first); if (it == loc2Targets.end()) { - all_broken_traces.insert(p.first->id); + all_broken_traces.insert(p.first->getId()); addBrokenTraces(p.second, all_broken_traces); continue; } @@ -252,36 +252,9 @@ TargetedExecutionManager::prepareTargets(KModule *origModule, KModule *kmodule, return whitelists; } -void TargetedExecutionManager::reportFalsePositives(ref &targets, bool canReachSomeTarget) { - if (targets.isNull()) - return; - std::unordered_map> trace2eventCount; - targets->collectHowManyEventsInTracesWereReached(trace2eventCount); - auto leafs = targets->leafs(); - for (const auto &targetWithConfidence : *leafs) { - auto target = targetWithConfidence.first; - auto confidence = targetWithConfidence.second; - if (!target->shouldFailOnThisTarget()) - continue; - if (target->isReported) - continue; - if (canReachSomeTarget) { - if (confidence > 99.0) // We should not be so sure if there are states that can reach some targets - confidence = 99.00; - auto eventCount = trace2eventCount[target->getId()]; - klee_warning("Time limit; reached only %u out of %u events at trace %u", eventCount.first, eventCount.second, target->getId()); - } else { - klee_warning("%s False Positive at trace %u", - ReachWithErrorNames[target->getError()], target->getId()); - } - target->isReported = true; - } - delete leafs; -} - void TargetedExecutionManager::reportFalseNegative(ExecutionState &state, ReachWithError error) { - klee_warning("%s False Negative at: %s", ReachWithErrorNames[error], + klee_warning("100.00%% %s False Negative at: %s", ReachWithErrorNames[error], state.prevPC->getSourceLocation().c_str()); } @@ -313,9 +286,9 @@ bool TargetedExecutionManager::reportTruePositive(ExecutionState &state, ReachWi atLeastOneReported = true; assert(!target->isReported); if (target->getError() == ReachWithError::Reachable) { - klee_warning("%s Reachable at trace %u", ReachWithErrorNames[target->getError()], target->getId()); + klee_warning("100.00%% %s Reachable at trace %u", target->getErrorString(), target->getId()); } else { - klee_warning("%s True Positive at trace %u", ReachWithErrorNames[target->getError()], target->getId()); + klee_warning("100.00%% %s True Positive at trace %u", target->getErrorString(), target->getId()); } target->isReported = true; } diff --git a/lib/Core/TargetedExecutionManager.h b/lib/Core/TargetedExecutionManager.h index 4938cd5c527..05423d89116 100644 --- a/lib/Core/TargetedExecutionManager.h +++ b/lib/Core/TargetedExecutionManager.h @@ -17,11 +17,32 @@ #include "Target.h" #include "TargetForest.h" #include "klee/Module/KModule.h" +#include "klee/Core/TargetedExecutionReporter.h" #include namespace klee { +class TargetedHaltsOnTraces { + using HaltTypeToConfidence = std::unordered_map; + using TraceToHaltTypeToConfidence = std::unordered_map, HaltTypeToConfidence, RefTargetHash, RefTargetCmp>; + TraceToHaltTypeToConfidence traceToHaltTypeToConfidence; + + static void + totalConfidenceAndTopContributor( + const HaltTypeToConfidence &haltTypeToConfidence, + confidence::ty *confidence, + HaltExecution::Reason *reason); + +public: + explicit TargetedHaltsOnTraces(ref &forest); + + void subtractConfidencesFrom(TargetForest &forest, HaltExecution::Reason reason); + + /* Report for targeted static analysis mode */ + void reportFalsePositives(bool canReachSomeTarget); +}; + class TargetedExecutionManager { struct TargetPreparator; @@ -41,10 +62,6 @@ class TargetedExecutionManager { std::unordered_map> prepareTargets(KModule *origModule, KModule *kmodule, PathForest *paths); - /* Report for targeted static analysis mode */ - void reportFalsePositives(ref &targets, - bool canReachSomeTarget); - void reportFalseNegative(ExecutionState &state, ReachWithError error); // Return true if report is successful diff --git a/lib/Core/TargetedExecutionReporter.cpp b/lib/Core/TargetedExecutionReporter.cpp new file mode 100644 index 00000000000..8b76b811973 --- /dev/null +++ b/lib/Core/TargetedExecutionReporter.cpp @@ -0,0 +1,59 @@ +//===-- TargetedExecutionReporter.cpp --------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include "klee/Core/TargetedExecutionReporter.h" +#include "klee/Support/ErrorHandling.h" + +#include + +using namespace klee; + +void klee::reportFalsePositive( + confidence::ty confidence, + LocatedEvent &event, + std::string whatToIncrease) +{ + std::ostringstream out; + out << event.getErrorString() << " False Positive at trace " << event.getId(); + if (!confidence::isConfident(confidence)) { + out << ". Advice: " << "increase --" << whatToIncrease << " command line parameter value"; + } + klee_warning("%s%% %s", confidence::toString(confidence).c_str(), out.str().c_str()); +} + +bool confidence::isConfident(ty conf) { + return conf > Confident; +} + +bool confidence::isVeryConfident(ty conf) { + return conf > VeryConfident; +} + +template +std::string string_format( const std::string& format, Args ... args ) +{ // from https://stackoverflow.com/a/26221725/10547926 + int size_s = std::snprintf( nullptr, 0, format.c_str(), args ... ) + 1; // Extra space for '\0' + if( size_s <= 0 ) return ""; + auto size = static_cast( size_s ); + std::unique_ptr buf( new char[ size ] ); + std::snprintf( buf.get(), size, format.c_str(), args ... ); + return std::string( buf.get(), buf.get() + size - 1 ); // We don't want the '\0' inside +} + +std::string confidence::toString(ty conf) { + return string_format("%.2f", conf); +} + +confidence::ty confidence::min(confidence::ty left, confidence::ty right) { + return fmin(left, right); +} + +bool confidence::isNormal(confidence::ty conf) { + return confidence::MinConfidence <= conf && conf <= confidence::MaxConfidence; +} diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp index 130e598ddb7..140a0b6c2e6 100644 --- a/lib/Core/UserSearcher.cpp +++ b/lib/Core/UserSearcher.cpp @@ -171,12 +171,14 @@ Searcher *klee::constructUserSearcher(Executor &executor) { if (executor.guidanceKind == Interpreter::GuidanceKind::CoverageGuidance) { searcher = new GuidedSearcher( searcher, *executor.codeGraphDistance.get(), *executor.targetCalculator, + executor.removedButReachableStates, executor.pausedStates, MaxCycles - 1, executor.theRNG); } if (executor.guidanceKind == Interpreter::GuidanceKind::ErrorGuidance) { delete searcher; searcher = new GuidedSearcher(*executor.codeGraphDistance.get(), + executor.removedButReachableStates, executor.pausedStates, MaxCycles - 1, executor.theRNG); } diff --git a/lib/Module/Locations.cpp b/lib/Module/Locations.cpp index 0e34d1f9e5f..2bd23680d83 100644 --- a/lib/Module/Locations.cpp +++ b/lib/Module/Locations.cpp @@ -107,8 +107,63 @@ bool Location::isInside(KBlock *block) const { return line <= last; // and `first <= line` from above } +int Location::compare(const Location &other) const { + if (line < other.line) + return -1; + if (line > other.line) + return 1; + if (offset < other.offset) + return -1; + if (offset > other.offset) + return 1; + if (filename < other.filename) + return -1; + if (filename > other.filename) + return 1; + if (function < other.function) + return -1; + if (function > other.function) + return 1; + return 0; +} + +int LocatedEvent::compare(const LocatedEvent &other) const { + if (error != other.error) { + return error < other.error ? -1 : 1; + } + if (id != other.id) { + return id < other.id ? -1 : 1; + } + if (location.isNull()) { + return other.location.isNull() ? 0 : 1; + } else if (other.location.isNull()) { + return -1; + } + if (*location != *other.location) { + return (*location < *other.location) ? -1 : 1; + } + return 0; +} + +bool LocatedEvent::operator<(const LocatedEvent &other) const { + return + error < other.error || (error == other.error && + (location < other.location || (location == other.location && + (id < other.id)))); +} + +bool LocatedEvent::operator==(const LocatedEvent &other) const { + return error == other.error && location == other.location && id == other.id; +} + +void LocatedEvent::setErrorReachableIfNone() { + if (shouldFailOnThisTarget()) + return; + error = ReachWithError::Reachable; +} + std::string LocatedEvent::toString() const { - return location.toString(); + return location->toString(); } void PathForest::addSubTree(LocatedEvent * loc, PathForest *subTree) { diff --git a/lib/Runner/parse_static_analysis_json.cpp b/lib/Runner/parse_static_analysis_json.cpp index d5703397853..c5338b632bf 100644 --- a/lib/Runner/parse_static_analysis_json.cpp +++ b/lib/Runner/parse_static_analysis_json.cpp @@ -89,14 +89,14 @@ class TraceParser { struct cmpLocatedEvent { bool operator()(const LocatedEvent& a, const LocatedEvent& b) const { - return a.location < b.location; + return *a.getLocation() < *b.getLocation(); } }; std::map locatedEvents; LocatedEvent *locatedEvent(LocatedEvent *event) { - if (event->error != ReachWithError::None) + if (event->shouldFailOnThisTarget()) return event; auto it = locatedEvents.find(*event); if (it == locatedEvents.end()) { @@ -127,12 +127,12 @@ ReachWithError parseError(json &traceEvent) { return ReachWithError::None; } -LocatedEvent *parseTraceEvent(json &traceEvent) { +LocatedEvent *parseTraceEvent(json &traceEvent, unsigned id) { auto location = traceEvent.at("location"); std::string file = location.at("file"); auto error = parseError(traceEvent); unsigned reportLine = location.at("reportLine"); - LocatedEvent *le = nullptr; + Location *loc = nullptr; if (location.contains("function") && location.contains("column") && location.contains("instructionOpcode")) { std::string function = location.at("function"); @@ -142,10 +142,11 @@ LocatedEvent *parseTraceEvent(json &traceEvent) { if (location.contains("instructionOffset")) { offset = location.at("instructionOffset"); } - le = new LocatedEvent(Location(file, function, reportLine, offset, column, instructionOpcode), error); + loc = new Location(file, function, reportLine, offset, column, instructionOpcode); } else { - le = new LocatedEvent(Location(file, reportLine), error); + loc = new Location(file, reportLine); } + auto le = new LocatedEvent(loc, error, id); return locatedEvent(le); } @@ -167,7 +168,7 @@ LocatedEvent *deduceEntryPoint(json &trace, unsigned id) { return nullptr; } auto p = frames.entryPoint(); - auto le = new LocatedEvent(Location(p->first, p->second), ReachWithError::None); + auto le = new LocatedEvent(new Location(p->first, p->second), id); // llvm::errs() << "Deduced entry point: " << p->first << ' ' << p->second << '\n'; return locatedEvent(le); } @@ -176,18 +177,14 @@ std::vector *parseTrace(json &trace, unsigned id) { auto entryPoint = deduceEntryPoint(trace, id); if (!entryPoint) return nullptr; - entryPoint->id = id; auto out = new std::vector(); out->reserve(trace.size() + 1); out->push_back(entryPoint); for (auto traceEvent : trace) { - auto le = parseTraceEvent(traceEvent); - le->id = id; + auto le = parseTraceEvent(traceEvent, id); out->push_back(le); } - if (out->back()->error == ReachWithError::None) { - out->back()->error = ReachWithError::Reachable; - } + out->back()->setErrorReachableIfNone(); return out; } diff --git a/lib/Runner/run_klee.cpp b/lib/Runner/run_klee.cpp index 191a1dae6ac..eadf7d83e63 100644 --- a/lib/Runner/run_klee.cpp +++ b/lib/Runner/run_klee.cpp @@ -15,6 +15,7 @@ #include "klee/ADT/TreeStream.h" #include "klee/Config/Version.h" #include "klee/Core/Interpreter.h" +#include "klee/Core/TargetedExecutionReporter.h" #include "klee/Module/Locations.h" #include "klee/ADT/KTest.h" #include "klee/ADT/TestCaseUtils.h" @@ -848,7 +849,7 @@ void KleeHandler::processTestCase(ExecutionState &state, m_numGeneratedTests++; if (m_numGeneratedTests == MaxTests) - m_interpreter->setHaltExecution(true); + m_interpreter->setHaltExecution(HaltExecution::MaxTests); if (WriteTestInfo) { time::Span elapsed_time(time::getWallTime() - start_time); @@ -1332,7 +1333,7 @@ static std::atomic_bool interrupted{false}; // Pulled out so it can be easily called from a debugger. extern "C" void halt_execution() { - theInterpreter->setHaltExecution(true); + theInterpreter->setHaltExecution(HaltExecution::Interrupt); } extern "C" @@ -1356,8 +1357,8 @@ static void interrupt_handle() { auto event = p.first; auto nextTree = p.second; if (nextTree->empty()) { - if (event->error != ReachWithError::None) { - klee_warning("Time limit; not started investigating at trace %u", event->id); + if (event->shouldFailOnThisTarget()) { + reportFalsePositive(confidence::MinConfidence, *event, "max-time"); } } else { q.push_back(nextTree); @@ -1520,11 +1521,11 @@ static PathForest *parseStaticAnalysisInput() { return parseInputPathTree(AnalysisReproduce); if (AnalysisFile == "" || AnalysisSink == 0) klee_error("--analysis-reproduce JSON file with error paths to be checked is not provided in error-guidance mode"); - auto sinkLoc = new LocatedEvent(Location(AnalysisFile, AnalysisSink), ReachWithError::NullPointerException); + auto sinkLoc = new LocatedEvent(new Location(AnalysisFile, AnalysisSink), ReachWithError::NullPointerException); auto sink = new PathForest(); sink->addLeaf(sinkLoc); unsigned sourceLine = AnalysisSource == 0 ? AnalysisSink : AnalysisSource; - auto sourceLoc = new LocatedEvent(Location(AnalysisFile, sourceLine), ReachWithError::None); + auto sourceLoc = new LocatedEvent(new Location(AnalysisFile, sourceLine)); auto source = new PathForest(); source->addSubTree(sourceLoc, sink); return source;