Skip to content

Commit 85b5f35

Browse files
committed
[feat] Differentiate isCoveredNew and isCoveredNewError
1 parent 8798ea5 commit 85b5f35

File tree

4 files changed

+375
-12
lines changed

4 files changed

+375
-12
lines changed

lib/Core/ExecutionState.cpp

Lines changed: 11 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -121,7 +121,8 @@ ExecutionState::ExecutionState()
121121
depth(0), ptreeNode(nullptr), symbolics(), steppedInstructions(0),
122122
steppedMemoryInstructions(0), instsSinceCovNew(0),
123123
roundingMode(llvm::APFloat::rmNearestTiesToEven), coveredNew({}),
124-
forkDisabled(false), prevHistory_(TargetsHistory::create()),
124+
coveredNewError(new box<bool>(false)), forkDisabled(false),
125+
prevHistory_(TargetsHistory::create()),
125126
history_(TargetsHistory::create()) {
126127
setID();
127128
}
@@ -131,7 +132,8 @@ ExecutionState::ExecutionState(KFunction *kf)
131132
depth(0), ptreeNode(nullptr), symbolics(), steppedInstructions(0),
132133
steppedMemoryInstructions(0), instsSinceCovNew(0),
133134
roundingMode(llvm::APFloat::rmNearestTiesToEven), coveredNew({}),
134-
forkDisabled(false), prevHistory_(TargetsHistory::create()),
135+
coveredNewError(new box<bool>(false)), forkDisabled(false),
136+
prevHistory_(TargetsHistory::create()),
135137
history_(TargetsHistory::create()) {
136138
pushFrame(nullptr, kf);
137139
setID();
@@ -142,7 +144,8 @@ ExecutionState::ExecutionState(KFunction *kf, KBlock *kb)
142144
depth(0), ptreeNode(nullptr), symbolics(), steppedInstructions(0),
143145
steppedMemoryInstructions(0), instsSinceCovNew(0),
144146
roundingMode(llvm::APFloat::rmNearestTiesToEven), coveredNew({}),
145-
forkDisabled(false), prevHistory_(TargetsHistory::create()),
147+
coveredNewError(new box<bool>(false)), forkDisabled(false),
148+
prevHistory_(TargetsHistory::create()),
146149
history_(TargetsHistory::create()) {
147150
pushFrame(nullptr, kf);
148151
setID();
@@ -170,11 +173,11 @@ ExecutionState::ExecutionState(const ExecutionState &state)
170173
unwindingInformation(state.unwindingInformation
171174
? state.unwindingInformation->clone()
172175
: nullptr),
173-
coveredNew(state.coveredNew), forkDisabled(state.forkDisabled),
174-
returnValue(state.returnValue), gepExprBases(state.gepExprBases),
175-
prevTargets_(state.prevTargets_), targets_(state.targets_),
176-
prevHistory_(state.prevHistory_), history_(state.history_),
177-
isTargeted_(state.isTargeted_) {
176+
coveredNew(state.coveredNew), coveredNewError(state.coveredNewError),
177+
forkDisabled(state.forkDisabled), returnValue(state.returnValue),
178+
gepExprBases(state.gepExprBases), prevTargets_(state.prevTargets_),
179+
targets_(state.targets_), prevHistory_(state.prevHistory_),
180+
history_(state.history_), isTargeted_(state.isTargeted_) {
178181
queryMetaData.id = state.id;
179182
}
180183

lib/Core/ExecutionState.h

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -366,6 +366,7 @@ class ExecutionState {
366366

367367
/// @brief Whether a new instruction was covered in this state
368368
mutable std::deque<ref<box<bool>>> coveredNew;
369+
mutable ref<box<bool>> coveredNewError;
369370

370371
/// @brief Disables forking for this state. Set by user code
371372
bool forkDisabled = false;
@@ -507,7 +508,12 @@ class ExecutionState {
507508
bool isCoveredNew() const {
508509
return !coveredNew.empty() && coveredNew.back()->value;
509510
}
510-
void coverNew() const { coveredNew.push_back(new box<bool>(true)); }
511+
bool isCoveredNewError() const { return coveredNewError->value; }
512+
void coverNew() const {
513+
coveredNew.push_back(new box<bool>(true));
514+
coveredNewError->value = false;
515+
coveredNewError = new box<bool>(true);
516+
}
511517
void updateCoveredNew() const {
512518
while (!coveredNew.empty() && !coveredNew.front()->value) {
513519
coveredNew.pop_front();
@@ -519,6 +525,7 @@ class ExecutionState {
519525
}
520526
coveredNew.clear();
521527
}
528+
void clearCoveredNewError() const { coveredNewError->value = false; }
522529
};
523530

524531
struct ExecutionStateIDCompare {

lib/Core/Executor.cpp

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4355,9 +4355,9 @@ void Executor::initializeTypeManager() {
43554355
typeSystemManager->initModule();
43564356
}
43574357

4358-
static bool shouldWriteTest(const ExecutionState &state) {
4358+
static bool shouldWriteTest(const ExecutionState &state, bool isError = false) {
43594359
state.updateCoveredNew();
4360-
bool coveredNew = state.isCoveredNew();
4360+
bool coveredNew = isError ? state.isCoveredNewError() : state.isCoveredNew();
43614361
return !OnlyOutputStatesCoveringNew || coveredNew;
43624362
}
43634363

@@ -4721,7 +4721,7 @@ void Executor::terminateStateOnError(ExecutionState &state,
47214721

47224722
if ((EmitAllErrors ||
47234723
emittedErrors.insert(std::make_pair(lastInst, message)).second) &&
4724-
shouldWriteTest(state)) {
4724+
shouldWriteTest(state, true)) {
47254725
std::string filepath = ki->getSourceFilepath();
47264726
if (!filepath.empty()) {
47274727
klee_message("ERROR: %s:%zu: %s", filepath.c_str(), ki->getLine(),
@@ -4752,6 +4752,8 @@ void Executor::terminateStateOnError(ExecutionState &state,
47524752
if (!info_str.empty())
47534753
msg << "Info: \n" << info_str;
47544754

4755+
state.clearCoveredNewError();
4756+
47554757
const std::string ext = terminationTypeFileExtension(terminationType);
47564758
// use user provided suffix from klee_report_error()
47574759
const char *file_suffix = suffix ? suffix : ext.c_str();

0 commit comments

Comments
 (0)