Skip to content

Commit 2c50df5

Browse files
S1eGaS1eGa
committed
[feat] Added error classification on 'confident' and 'possible'.
1 parent c61034f commit 2c50df5

File tree

6 files changed

+130
-44
lines changed

6 files changed

+130
-44
lines changed

‎include/klee/Core/TerminationTypes.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -85,6 +85,8 @@ enum class StateTerminationType : std::uint8_t {
8585
/// \endcond
8686
};
8787

88+
enum StateTerminationConfidenceCategory { CONFIDENT, PROBABLY };
89+
8890
namespace HaltExecution {
8991
enum Reason {
9092
NotHalt = 0,

‎lib/Core/ExecutionState.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -317,6 +317,9 @@ class ExecutionState {
317317

318318
// Overall state of the state - Data specific
319319

320+
/// @brief: TODO:
321+
bool lastBrConfidently = true;
322+
320323
/// @brief Exploration depth, i.e., number of times KLEE branched for this
321324
/// state
322325
std::uint32_t depth = 0;

‎lib/Core/Executor.cpp

Lines changed: 82 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,7 @@
4040
#include "klee/Config/config.h"
4141
#include "klee/Core/Interpreter.h"
4242
#include "klee/Core/MockBuilder.h"
43+
#include "klee/Core/TerminationTypes.h"
4344
#include "klee/Expr/ArrayExprOptimizer.h"
4445
#include "klee/Expr/ArrayExprVisitor.h"
4546
#include "klee/Expr/Assignment.h"
@@ -2724,6 +2725,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
27242725
if (bi->getMetadata("md.ret")) {
27252726
state.stack.forceReturnLocation(locationOf(state));
27262727
}
2728+
state.lastBrConfidently = true;
27272729

27282730
transferToBasicBlock(bi->getSuccessor(0), bi->getParent(), state);
27292731
} else {
@@ -2743,6 +2745,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
27432745
maxNewStateStackSize =
27442746
std::max(maxNewStateStackSize,
27452747
branches.first->stack.stackRegisterSize() * 8);
2748+
branches.first->lastBrConfidently = false;
2749+
branches.second->lastBrConfidently = false;
2750+
} else {
2751+
(branches.first ? branches.first : branches.second)->lastBrConfidently =
2752+
true;
27462753
}
27472754

27482755
// NOTE: There is a hidden dependency here, markBranchVisited
@@ -4014,9 +4021,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
40144021
if (iIdx >= vt->getNumElements()) {
40154022
// Out of bounds write
40164023
terminateStateOnProgramError(
4017-
state, new ErrorEvent(locationOf(state),
4018-
StateTerminationType::BadVectorAccess,
4019-
"Out of bounds write when inserting element"));
4024+
state,
4025+
new ErrorEvent(locationOf(state),
4026+
StateTerminationType::BadVectorAccess,
4027+
"Out of bounds write when inserting element"),
4028+
StateTerminationConfidenceCategory::CONFIDENT);
40204029
return;
40214030
}
40224031

@@ -4057,9 +4066,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
40574066
if (iIdx >= vt->getNumElements()) {
40584067
// Out of bounds read
40594068
terminateStateOnProgramError(
4060-
state, new ErrorEvent(locationOf(state),
4061-
StateTerminationType::BadVectorAccess,
4062-
"Out of bounds read when extracting element"));
4069+
state,
4070+
new ErrorEvent(locationOf(state),
4071+
StateTerminationType::BadVectorAccess,
4072+
"Out of bounds read when extracting element"),
4073+
StateTerminationConfidenceCategory::CONFIDENT);
40634074
return;
40644075
}
40654076

@@ -4963,28 +4974,41 @@ void Executor::terminateStateOnTargetError(ExecutionState &state,
49634974
terminationType = StateTerminationType::User;
49644975
}
49654976
terminateStateOnProgramError(
4966-
state, new ErrorEvent(locationOf(state), terminationType, messaget));
4977+
state, new ErrorEvent(locationOf(state), terminationType, messaget),
4978+
StateTerminationConfidenceCategory::CONFIDENT);
49674979
}
49684980

4969-
void Executor::terminateStateOnError(ExecutionState &state,
4970-
const llvm::Twine &messaget,
4971-
StateTerminationType terminationType,
4972-
const llvm::Twine &info,
4973-
const char *suffix) {
4981+
void Executor::terminateStateOnError(
4982+
ExecutionState &state, const llvm::Twine &messaget,
4983+
StateTerminationType terminationType,
4984+
StateTerminationConfidenceCategory confidence, const llvm::Twine &info,
4985+
const char *suffix) {
49744986
std::string message = messaget.str();
4975-
static std::set<std::pair<Instruction *, std::string>> emittedErrors;
4987+
static std::set<
4988+
std::pair<Instruction *,
4989+
std::pair<StateTerminationConfidenceCategory, std::string>>>
4990+
emittedErrors;
49764991
const KInstruction *ki = getLastNonKleeInternalInstruction(state);
49774992
Instruction *lastInst = ki->inst();
49784993

4979-
if ((EmitAllErrors ||
4980-
emittedErrors.insert(std::make_pair(lastInst, message)).second) &&
4994+
if ((EmitAllErrors || emittedErrors
4995+
.insert(std::make_pair(
4996+
lastInst, std::make_pair(confidence, message)))
4997+
.second) &&
49814998
shouldWriteTest(state, true)) {
49824999
std::string filepath = ki->getSourceFilepath();
5000+
5001+
std::string prefix =
5002+
(confidence == StateTerminationConfidenceCategory::CONFIDENT
5003+
? "ERROR"
5004+
: "POSSIBLE ERROR");
5005+
49835006
if (!filepath.empty()) {
4984-
klee_message("ERROR: %s:%zu: %s", filepath.c_str(), ki->getLine(),
4985-
message.c_str());
5007+
klee_message((prefix + ": %s:%zu: %s").c_str(), filepath.c_str(),
5008+
ki->getLine(), message.c_str());
49865009
} else {
4987-
klee_message("ERROR: (location information missing) %s", message.c_str());
5010+
klee_message((prefix + ": (location information missing) %s").c_str(),
5011+
message.c_str());
49885012
}
49895013
if (!EmitAllErrors)
49905014
klee_message("NOTE: now ignoring this error at this location");
@@ -5030,13 +5054,14 @@ void Executor::terminateStateOnExecError(ExecutionState &state,
50305054
assert(reason > StateTerminationType::USERERR &&
50315055
reason <= StateTerminationType::EXECERR);
50325056
++stats::terminationExecutionError;
5033-
terminateStateOnError(state, message, reason, "");
5057+
terminateStateOnError(state, message, reason,
5058+
StateTerminationConfidenceCategory::CONFIDENT, "");
50345059
}
50355060

5036-
void Executor::terminateStateOnProgramError(ExecutionState &state,
5037-
const ref<ErrorEvent> &reason,
5038-
const llvm::Twine &info,
5039-
const char *suffix) {
5061+
void Executor::terminateStateOnProgramError(
5062+
ExecutionState &state, const ref<ErrorEvent> &reason,
5063+
StateTerminationConfidenceCategory confidence, const llvm::Twine &info,
5064+
const char *suffix) {
50405065
assert(reason->ruleID > StateTerminationType::SOLVERERR &&
50415066
reason->ruleID <= StateTerminationType::PROGERR);
50425067
++stats::terminationProgramError;
@@ -5055,19 +5080,22 @@ void Executor::terminateStateOnProgramError(ExecutionState &state,
50555080
}
50565081
state.eventsRecorder.record(reason);
50575082

5058-
terminateStateOnError(state, reason->message, reason->ruleID, info, suffix);
5083+
terminateStateOnError(state, reason->message, reason->ruleID, confidence,
5084+
info, suffix);
50595085
}
50605086

50615087
void Executor::terminateStateOnSolverError(ExecutionState &state,
50625088
const llvm::Twine &message) {
50635089
++stats::terminationSolverError;
5064-
terminateStateOnError(state, message, StateTerminationType::Solver, "");
5090+
terminateStateOnError(state, message, StateTerminationType::Solver,
5091+
StateTerminationConfidenceCategory::CONFIDENT, "");
50655092
}
50665093

50675094
void Executor::terminateStateOnUserError(ExecutionState &state,
50685095
const llvm::Twine &message) {
50695096
++stats::terminationUserError;
5070-
terminateStateOnError(state, message, StateTerminationType::User, "");
5097+
terminateStateOnError(state, message, StateTerminationType::User,
5098+
StateTerminationConfidenceCategory::CONFIDENT, "");
50715099
}
50725100

50735101
// XXX shoot me
@@ -5416,13 +5444,20 @@ void Executor::executeFree(ExecutionState &state, ref<Expr> address,
54165444
new ErrorEvent(new AllocEvent(mo->allocSite),
54175445
locationOf(*it->second), StateTerminationType::Free,
54185446
"free of alloca"),
5447+
rl.size() != 1 ? StateTerminationConfidenceCategory::PROBABLY
5448+
: StateTerminationConfidenceCategory::CONFIDENT,
54195449
getAddressInfo(*it->second, address));
54205450
} else if (mo->isGlobal) {
5451+
if (rl.size() != 1) {
5452+
klee_warning("Following error if likely false positive");
5453+
}
54215454
terminateStateOnProgramError(
54225455
*it->second,
54235456
new ErrorEvent(new AllocEvent(mo->allocSite),
54245457
locationOf(*it->second), StateTerminationType::Free,
54255458
"free of global"),
5459+
rl.size() != 1 ? StateTerminationConfidenceCategory::PROBABLY
5460+
: StateTerminationConfidenceCategory::CONFIDENT,
54265461
getAddressInfo(*it->second, address));
54275462
} else {
54285463
it->second->removePointerResolutions(mo);
@@ -5518,6 +5553,8 @@ bool Executor::resolveExact(ExecutionState &estate, ref<Expr> address,
55185553
*unbound,
55195554
new ErrorEvent(locationOf(*unbound), StateTerminationType::Ptr,
55205555
"memory error: invalid pointer: " + name),
5556+
!results.empty() ? StateTerminationConfidenceCategory::PROBABLY
5557+
: StateTerminationConfidenceCategory::CONFIDENT,
55215558
getAddressInfo(*unbound, address));
55225559
}
55235560
}
@@ -5607,7 +5644,7 @@ void Executor::concretizeSize(ExecutionState &state, ref<Expr> size,
56075644
new ErrorEvent(locationOf(*hugeSize.second),
56085645
StateTerminationType::Model,
56095646
"concretized symbolic size"),
5610-
info.str());
5647+
StateTerminationConfidenceCategory::CONFIDENT, info.str());
56115648
}
56125649
}
56135650
}
@@ -6309,7 +6346,8 @@ void Executor::executeMemoryOperation(
63096346
*state,
63106347
new ErrorEvent(new AllocEvent(mo->allocSite), locationOf(*state),
63116348
StateTerminationType::ReadOnly,
6312-
"memory error: object read only"));
6349+
"memory error: object read only"),
6350+
StateTerminationConfidenceCategory::CONFIDENT);
63136351
} else {
63146352
wos->write(mo->getOffsetExpr(address), value);
63156353
}
@@ -6371,6 +6409,10 @@ void Executor::executeMemoryOperation(
63716409
return;
63726410
}
63736411

6412+
bool mayBeFalsePositive =
6413+
resolvedMemoryObjects.size() > 1 ||
6414+
(resolvedMemoryObjects.size() == 1 && mayBeOutOfBound);
6415+
63746416
ExecutionState *unbound = nullptr;
63756417
if (MergedPointerDereference) {
63766418
ref<Expr> guard;
@@ -6428,7 +6470,10 @@ void Executor::executeMemoryOperation(
64286470
new ErrorEvent(new AllocEvent(mo->allocSite),
64296471
locationOf(*branches.first),
64306472
StateTerminationType::ReadOnly,
6431-
"memory error: object read only"));
6473+
"memory error: object read only"),
6474+
mayBeFalsePositive
6475+
? StateTerminationConfidenceCategory::PROBABLY
6476+
: StateTerminationConfidenceCategory::CONFIDENT);
64326477
state = branches.second;
64336478
} else {
64346479
ref<Expr> result = SelectExpr::create(
@@ -6500,7 +6545,10 @@ void Executor::executeMemoryOperation(
65006545
*bound,
65016546
new ErrorEvent(new AllocEvent(mo->allocSite), locationOf(*bound),
65026547
StateTerminationType::ReadOnly,
6503-
"memory error: object read only"));
6548+
"memory error: object read only"),
6549+
mayBeFalsePositive
6550+
? StateTerminationConfidenceCategory::PROBABLY
6551+
: StateTerminationConfidenceCategory::CONFIDENT);
65046552
} else {
65056553
wos->write(mo->getOffsetExpr(address), value);
65066554
}
@@ -6552,6 +6600,8 @@ void Executor::executeMemoryOperation(
65526600
new ErrorEvent(new AllocEvent(baseObjectPair.first->allocSite),
65536601
locationOf(*unbound), StateTerminationType::Ptr,
65546602
"memory error: out of bound pointer"),
6603+
mayBeFalsePositive ? StateTerminationConfidenceCategory::PROBABLY
6604+
: StateTerminationConfidenceCategory::CONFIDENT,
65556605
getAddressInfo(*unbound, address));
65566606
return;
65576607
}
@@ -6561,6 +6611,8 @@ void Executor::executeMemoryOperation(
65616611
*unbound,
65626612
new ErrorEvent(locationOf(*unbound), StateTerminationType::Ptr,
65636613
"memory error: out of bound pointer"),
6614+
mayBeFalsePositive ? StateTerminationConfidenceCategory::PROBABLY
6615+
: StateTerminationConfidenceCategory::CONFIDENT,
65646616
getAddressInfo(*unbound, address));
65656617
}
65666618
}

‎lib/Core/Executor.h

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -618,6 +618,7 @@ class Executor : public Interpreter {
618618
/// below.
619619
void terminateStateOnError(ExecutionState &state, const llvm::Twine &message,
620620
StateTerminationType reason,
621+
StateTerminationConfidenceCategory confidence,
621622
const llvm::Twine &longMessage = "",
622623
const char *suffix = nullptr);
623624

@@ -629,10 +630,10 @@ class Executor : public Interpreter {
629630

630631
/// Call error handler and terminate state in case of program errors
631632
/// (e.g. free()ing globals, out-of-bound accesses)
632-
void terminateStateOnProgramError(ExecutionState &state,
633-
const ref<ErrorEvent> &reason,
634-
const llvm::Twine &longMessage = "",
635-
const char *suffix = nullptr);
633+
void terminateStateOnProgramError(
634+
ExecutionState &state, const ref<ErrorEvent> &reason,
635+
StateTerminationConfidenceCategory confidence,
636+
const llvm::Twine &longMessage = "", const char *suffix = nullptr);
636637

637638
void terminateStateOnTerminator(ExecutionState &state);
638639

0 commit comments

Comments
 (0)