From 0379144709c2bc47b6fc4bc42c5fe00a24d01a0d Mon Sep 17 00:00:00 2001 From: Taras Bereznyak Date: Thu, 4 Nov 2021 13:33:01 +0300 Subject: Fixed fail with preferCex, removed relation from first argument --- lib/Core/ExecutionState.cpp | 5 +++++ lib/Core/ExecutionState.h | 6 ++++++ lib/Core/Executor.cpp | 34 +++++++++++++--------------------- lib/Core/Memory.h | 6 ------ lib/Core/SpecialFunctionHandler.cpp | 8 +------- 5 files changed, 25 insertions(+), 34 deletions(-) (limited to 'lib') diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 47a3b3c6..2f585f96 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -103,6 +103,7 @@ ExecutionState::ExecutionState(const ExecutionState& state): symPathOS(state.symPathOS), coveredLines(state.coveredLines), symbolics(state.symbolics), + cexPreferences(state.cexPreferences), arrayNames(state.arrayNames), openMergeStack(state.openMergeStack), steppedInstructions(state.steppedInstructions), @@ -358,3 +359,7 @@ void ExecutionState::addConstraint(ref e) { ConstraintManager c(constraints); c.addConstraint(e); } + +void ExecutionState::addCexPreference(const ref &cond) { + cexPreferences = cexPreferences.insert(cond); +} diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index f91790d5..8f5e57e8 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -13,6 +13,7 @@ #include "AddressSpace.h" #include "MergeHandler.h" +#include "klee/ADT/ImmutableSet.h" #include "klee/ADT/TreeStream.h" #include "klee/Expr/Constraints.h" #include "klee/Expr/Expr.h" @@ -207,6 +208,10 @@ public: // FIXME: Move to a shared list structure (not critical). std::vector, const Array *>> symbolics; + /// @brief A set of boolean expressions + /// the user has requested be true of a counterexample. + ImmutableSet> cexPreferences; + /// @brief Set of used array names for this state. Used to avoid collisions. std::set arrayNames; @@ -259,6 +264,7 @@ public: void addSymbolic(const MemoryObject *mo, const Array *array); void addConstraint(ref e); + void addCexPreference(const ref &cond); bool merge(const ExecutionState &b); void dumpStack(llvm::raw_ostream &out) const; diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index dcb078df..3d6ea4ae 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -4560,27 +4560,19 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, // the preferred constraints. See test/Features/PreferCex.c for // an example) While this process can be very expensive, it can // also make understanding individual test cases much easier. - for (unsigned i = 0; i != state.symbolics.size(); ++i) { - const auto &mo = state.symbolics[i].first; - std::vector< ref >::const_iterator pi = - mo->cexPreferences.begin(), pie = mo->cexPreferences.end(); - for (; pi != pie; ++pi) { - bool mustBeTrue; - // Attempt to bound byte to constraints held in cexPreferences - bool success = - solver->mustBeTrue(extendedConstraints, Expr::createIsZero(*pi), - mustBeTrue, state.queryMetaData); - // If it isn't possible to constrain this particular byte in the desired - // way (normally this would mean that the byte can't be constrained to - // be between 0 and 127 without making the entire constraint list UNSAT) - // then just continue on to the next byte. - if (!success) break; - // If the particular constraint operated on in this iteration through - // the loop isn't implied then add it to the list of constraints. - if (!mustBeTrue) - cm.addConstraint(*pi); - } - if (pi!=pie) break; + for (auto& pi: state.cexPreferences) { + bool mustBeTrue; + // Attempt to bound byte to constraints held in cexPreferences + bool success = + solver->mustBeTrue(extendedConstraints, Expr::createIsZero(pi), + mustBeTrue, state.queryMetaData); + // If it isn't possible to add the condition without making the entire list + // UNSAT, then just continue to the next condition + if (!success) break; + // If the particular constraint operated on in this iteration through + // the loop isn't implied then add it to the list of constraints. + if (!mustBeTrue) + cm.addConstraint(pi); } std::vector< std::vector > values; diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h index e88d5f55..d5189df5 100644 --- a/lib/Core/Memory.h +++ b/lib/Core/Memory.h @@ -64,12 +64,6 @@ public: /// should be either the allocating instruction or the global object /// it was allocated for (or whatever else makes sense). const llvm::Value *allocSite; - - /// A list of boolean expressions the user has requested be true of - /// a counterexample. Mutable since we play a little fast and loose - /// with allowing it to be added to during execution (although - /// should sensibly be only at creation time). - mutable std::vector< ref > cexPreferences; // DO NOT IMPLEMENT MemoryObject(const MemoryObject &b); diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 27ca385c..94c4dc3c 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -549,13 +549,7 @@ void SpecialFunctionHandler::handlePreferCex(ExecutionState &state, if (cond->getWidth() != Expr::Bool) cond = NeExpr::create(cond, ConstantExpr::alloc(0, cond->getWidth())); - Executor::ExactResolutionList rl; - executor.resolveExact(state, arguments[0], rl, "prefex_cex"); - - assert(rl.size() == 1 && - "prefer_cex target must resolve to precisely one object"); - - rl[0].first.first->cexPreferences.push_back(cond); + state.addCexPreference(cond); } void SpecialFunctionHandler::handlePosixPreferCex(ExecutionState &state, -- cgit 1.4.1