Skip to content

Commit

Permalink
[feat] Handling of NPE moved to separate function.
Browse files Browse the repository at this point in the history
  • Loading branch information
@S1eGa
S1eGa committed Feb 27, 2024
1 parent b79686c commit a863e39
Show file tree
Hide file tree
Showing 2 changed files with 104 additions and 103 deletions.
204 changes: 101 additions & 103 deletions lib/Core/Executor.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5471,6 +5471,100 @@ void Executor::executeFree(ExecutionState &state, ref<Expr> address,
}
}

ExecutionState *Executor::handleNullPointerException(ExecutionState &state,
ref<Expr> base) {
StatePair branches =
forkInternal(state, Expr::createIsZero(base), BranchType::MemOp);
ExecutionState *bound = branches.first;
if (!bound) {
return branches.second;
}

// 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<const Array *> 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<Expr> allExcludedVectorsOfMarkers = Expr::createTrue();

bool convinced = false;
for (int tpCheckIteration = 0; tpCheckIteration < 2; ++tpCheckIteration) {
ref<SolverResponse> isConfidentResponse;
if (!solver->getResponse(bound->constraints.cs(),
allExcludedVectorsOfMarkers, isConfidentResponse,
bound->queryMetaData)) {
terminateStateOnSolverError(*bound, "Query timeout");
}

if (isa<ValidResponse>(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<SparseStorage<unsigned char>> boundSetSolution;
isConfidentResponse->tryGetInitialValuesFor(markersArrays,
boundSetSolution);
Assignment nonConfidentResponseAssignment(markersArrays,
boundSetSolution);

// Exclude this combinations of markers

ref<Expr> conjExcludedVectorOfMarkers = Expr::createTrue();
for (ref<Expr> 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);
}

return branches.second;
}

bool Executor::resolveExact(ExecutionState &estate, ref<Expr> address,
KType *type, ExactResolutionList &results,
const std::string &name) {
Expand All @@ -5496,20 +5590,12 @@ bool Executor::resolveExact(ExecutionState &estate, ref<Expr> address,
Simplificator::simplifyExpr(estate.constraints.cs(), base).simplified;
uniqueBase = toUnique(estate, uniqueBase);

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 (!branches.second) {
address = Expr::createPointer(0);
ExecutionState *handledNPEState = handleNullPointerException(estate, base);
if (!handledNPEState) {
return false;
}

ExecutionState &state = *branches.second;
ExecutionState &state = *handledNPEState;

ResolutionList rl;
bool mayBeOutOfBound = true;
Expand Down Expand Up @@ -6266,97 +6352,9 @@ void Executor::executeMemoryOperation(

ref<Expr> uniqueBase = toUnique(estate, base);

StatePair branches =
forkInternal(estate, Expr::createIsZero(base), BranchType::MemOp);
ExecutionState *bound = branches.first;

if (bound) {
// 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<const Array *> 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<Expr> allExcludedVectorsOfMarkers = Expr::createTrue();

bool convinced = false;
for (int tpCheckIteration = 0; tpCheckIteration < 2; ++tpCheckIteration) {
ref<SolverResponse> isConfidentResponse;
if (!solver->getResponse(bound->constraints.cs(),
allExcludedVectorsOfMarkers,
isConfidentResponse, bound->queryMetaData)) {
terminateStateOnSolverError(*bound, "Query timeout");
}

if (isa<ValidResponse>(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<SparseStorage<unsigned char>> boundSetSolution;
isConfidentResponse->tryGetInitialValuesFor(markersArrays,
boundSetSolution);
Assignment nonConfidentResponseAssignment(markersArrays,
boundSetSolution);

// Exclude this combinations of markers

ref<Expr> conjExcludedVectorOfMarkers = Expr::createTrue();
for (ref<Expr> 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)
ExecutionState *state = handleNullPointerException(estate, base);
if (!state)
return;
ExecutionState *state = branches.second;

// fast path: single in-bounds resolution
IDType idFastResult;
Expand Down Expand Up @@ -6542,7 +6540,7 @@ void Executor::executeMemoryOperation(
maxNewWriteableOSSize =
std::max(maxNewWriteableOSSize, wos->getSparseStorageEntries());
if (wos->readOnly) {
branches =
StatePair branches =
forkInternal(*state, Expr::createIsZero(unboundConditions[i]),
BranchType::MemOp);
assert(branches.first);
Expand Down
3 changes: 3 additions & 0 deletions lib/Core/Executor.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -413,6 +413,9 @@ class Executor : public Interpreter {
const std::vector<Assignment> &resolveConcretizations,
std::vector<ref<Expr>> &results);

ExecutionState *handleNullPointerException(ExecutionState &state,
ref<Expr> base);

// do address resolution / object binding / out of bounds checking
// and perform the operation
void executeMemoryOperation(ExecutionState &state, bool isWrite,
Expand Down

0 comments on commit a863e39

Please sign in to comment.