From b79686c336498a8d3849aa205e8cf4fcef5df921 Mon Sep 17 00:00:00 2001 From: Sergey Morozov Date: Tue, 20 Feb 2024 18:39:01 +0300 Subject: [PATCH] [feat] Distinct kinds of NPE. --- lib/Core/ExecutionState.cpp | 4 +- lib/Core/ExecutionState.h | 3 ++ lib/Core/Executor.cpp | 89 +++++++++++++++++++++++++++++++++++-- lib/Expr/ExprUtil.cpp | 4 ++ 4 files changed, 95 insertions(+), 5 deletions(-) diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index fa14493607..873188506c 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -160,7 +160,9 @@ ExecutionState::~ExecutionState() { ExecutionState::ExecutionState(const ExecutionState &state) : initPC(state.initPC), pc(state.pc), prevPC(state.prevPC), stack(state.stack), stackBalance(state.stackBalance), - incomingBBIndex(state.incomingBBIndex), depth(state.depth), + incomingBBIndex(state.incomingBBIndex), + lastBrConfidently(state.lastBrConfidently), + outOfMemoryMarkers(state.outOfMemoryMarkers), depth(state.depth), level(state.level), addressSpace(state.addressSpace), constraints(state.constraints), eventsRecorder(state.eventsRecorder), targetForest(state.targetForest), pathOS(state.pathOS), diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index c3191d5ca8..c593e2c05e 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -320,6 +320,9 @@ class ExecutionState { /// @brief: TODO: bool lastBrConfidently = true; + /// @brief: TODO: + ImmutableList> outOfMemoryMarkers; + /// @brief Exploration depth, i.e., number of times KLEE branched for this /// state std::uint32_t depth = 0; diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 778998681e..9b7235b6a3 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -62,6 +62,7 @@ #include "klee/Solver/Common.h" #include "klee/Solver/Solver.h" #include "klee/Solver/SolverCmdLine.h" +#include "klee/Solver/SolverUtil.h" #include "klee/Statistics/TimerStatIncrementer.h" #include "klee/Support/Casting.h" #include "klee/Support/ErrorHandling.h" @@ -5398,6 +5399,7 @@ void Executor::executeAlloc(ExecutionState &state, ref size, bool isLocal, makeMockValue(state, "symCheckOutOfMemory", Expr::Bool); address = SelectExpr::create(symCheckOutOfMemoryExpr, Expr::createPointer(0), address); + state.outOfMemoryMarkers.push_back(symCheckOutOfMemoryExpr); } // state.addPointerResolution(address, mo); @@ -6267,12 +6269,91 @@ void Executor::executeMemoryOperation( StatePair branches = forkInternal(estate, Expr::createIsZero(base), BranchType::MemOp); ExecutionState *bound = branches.first; + if (bound) { - auto error = isReadFromSymbolicArray(uniqueBase) - ? ReachWithError::MayBeNullPointerException - : ReachWithError::MustBeNullPointerException; - terminateStateOnTargetError(*bound, error); + // If there are no markers on `malloc` returning nullptr, + // then `confidence` depends on presence of `unbound` state. + if (!bound->outOfMemoryMarkers.empty()) { + // bound constraints already contain `Expr::createIsZero()` + std::vector markersArrays; + markersArrays.reserve(bound->outOfMemoryMarkers.size()); + findSymbolicObjects(bound->outOfMemoryMarkers.begin(), + bound->outOfMemoryMarkers.end(), markersArrays); + + // Do some iterations (2-3) to figure out if error is confident. + ref allExcludedVectorsOfMarkers = Expr::createTrue(); + + bool convinced = false; + for (int tpCheckIteration = 0; tpCheckIteration < 2; ++tpCheckIteration) { + ref isConfidentResponse; + if (!solver->getResponse(bound->constraints.cs(), + allExcludedVectorsOfMarkers, + isConfidentResponse, bound->queryMetaData)) { + terminateStateOnSolverError(*bound, "Query timeout"); + } + + if (isa(isConfidentResponse)) { + reportStateOnTargetError(*bound, + ReachWithError::MustBeNullPointerException); + + terminateStateOnProgramError( + *bound, + new ErrorEvent(locationOf(*bound), StateTerminationType::Ptr, + "memory error: null pointer exception"), + StateTerminationConfidenceCategory::CONFIDENT); + convinced = true; + break; + } + + // Receive current values of markers + std::vector> boundSetSolution; + isConfidentResponse->tryGetInitialValuesFor(markersArrays, + boundSetSolution); + Assignment nonConfidentResponseAssignment(markersArrays, + boundSetSolution); + + // Exclude this combinations of markers + + ref conjExcludedVectorOfMarkers = Expr::createTrue(); + for (ref marker : bound->outOfMemoryMarkers) { + conjExcludedVectorOfMarkers = AndExpr::create( + conjExcludedVectorOfMarkers, + EqExpr::create(marker, + nonConfidentResponseAssignment.evaluate(marker))); + } + + allExcludedVectorsOfMarkers = + OrExpr::create(allExcludedVectorsOfMarkers, + NotExpr::create(conjExcludedVectorOfMarkers)); + } + + if (!convinced) { + reportStateOnTargetError(*bound, + ReachWithError::MayBeNullPointerException); + + terminateStateOnProgramError( + *bound, + new ErrorEvent(locationOf(*bound), StateTerminationType::Ptr, + "memory error: null pointer exception"), + StateTerminationConfidenceCategory::PROBABLY); + } + + } else { + auto error = branches.second != nullptr + ? ReachWithError::MayBeNullPointerException + : ReachWithError::MustBeNullPointerException; + reportStateOnTargetError(*bound, error); + + terminateStateOnProgramError( + *bound, + new ErrorEvent(locationOf(*bound), StateTerminationType::Ptr, + "memory error: null pointer exception"), + branches.second != nullptr + ? StateTerminationConfidenceCategory::PROBABLY + : StateTerminationConfidenceCategory::CONFIDENT); + } } + if (!branches.second) return; ExecutionState *state = branches.second; diff --git a/lib/Expr/ExprUtil.cpp b/lib/Expr/ExprUtil.cpp index 518e922dc8..0d94d022b3 100644 --- a/lib/Expr/ExprUtil.cpp +++ b/lib/Expr/ExprUtil.cpp @@ -8,6 +8,7 @@ //===----------------------------------------------------------------------===// #include "klee/Expr/ExprUtil.h" +#include "klee/ADT/ImmutableList.h" #include "klee/Expr/Expr.h" #include "klee/Expr/ExprHashMap.h" #include "klee/Expr/ExprVisitor.h" @@ -186,6 +187,9 @@ template void klee::findSymbolicObjects(B, B, std::vector &); typedef ExprHashSet::iterator C; template void klee::findSymbolicObjects(C, C, std::vector &); +typedef ImmutableList>::iterator D; +template void klee::findSymbolicObjects(D, D, std::vector &); + typedef std::vector>::iterator A; template void klee::findObjects(A, A, std::vector &);