Skip to content

Commit

Permalink
[fix] Get rid of pointers comparison in maps
Browse files Browse the repository at this point in the history
  • Loading branch information
misonijnik committed Nov 15, 2024
1 parent 9518884 commit 04d0710
Show file tree
Hide file tree
Showing 12 changed files with 58 additions and 55 deletions.
6 changes: 3 additions & 3 deletions include/klee/Module/CodeGraphInfo.h
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ class CodeGraphInfo {
private:
blockToDistanceMap blockDistance;
blockToDistanceMap blockBackwardDistance;
std::set<KBlock *> blockCycles;
std::set<KBlock *, KBlockCompare> blockCycles;
blockDistanceList blockSortedDistance;
blockDistanceList blockSortedBackwardDistance;

Expand Down Expand Up @@ -71,7 +71,7 @@ class CodeGraphInfo {

void getNearestPredicateSatisfying(KBlock *from, KBlockPredicate predicate,
bool forward,
std::set<KBlock *, KBlockLess> &result);
std::set<KBlock *, KBlockCompare> &result);

const std::map<KBlock *, std::set<unsigned>> &
getFunctionBranches(KFunction *kf);
Expand All @@ -81,7 +81,7 @@ class CodeGraphInfo {
const std::map<KBlock *, std::set<unsigned>> &
getFunctionBlocks(KFunction *kf);

std::set<KBlock *, KBlockLess>
std::set<KBlock *, KBlockCompare>
getNearestPredicateSatisfying(KBlock *from, KBlockPredicate predicate,
bool forward);

Expand Down
6 changes: 6 additions & 0 deletions include/klee/Module/KInstruction.h
Original file line number Diff line number Diff line change
Expand Up @@ -181,6 +181,12 @@ struct CallStackFrame {
}
};

struct KInstructionCompare {
bool operator()(const KInstruction *a, const KInstruction *b) const {
return a->getID() < b->getID();
}
};

} // namespace klee

#endif /* KLEE_KINSTRUCTION_H */
32 changes: 10 additions & 22 deletions include/klee/Module/KModule.h
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,7 @@ class CodeGraphInfo;
class Executor;
class Expr;
class InterpreterHandler;
struct KBlockCompare;
struct KInstruction;
class KModule;
struct KFunction;
Expand All @@ -58,6 +59,10 @@ template <class T> class ref;

enum KBlockType { Base, Call, Return };

struct KBlockCompare {
bool operator()(const KBlock *a, const KBlock *b) const;
};

struct KBlock {
KFunction *parent;
llvm::BasicBlock *basicBlock;
Expand All @@ -72,8 +77,8 @@ struct KBlock {
KBlock &operator=(const KBlock &) = delete;
virtual ~KBlock() = default;

std::set<KBlock *> successors();
std::set<KBlock *> predecessors();
std::set<KBlock *, KBlockCompare> successors();
std::set<KBlock *, KBlockCompare> predecessors();

virtual KBlockType getKBlockType() const { return KBlockType::Base; }
static bool classof(const KBlock *) { return true; }
Expand Down Expand Up @@ -113,7 +118,7 @@ struct DefaultBlockPredicate : public InitializerPredicate {
};

struct TraceVerifyPredicate : public InitializerPredicate {
explicit TraceVerifyPredicate(std::set<KBlock *> specialPoints,
explicit TraceVerifyPredicate(std::set<KBlock *, KBlockCompare> specialPoints,
CodeGraphInfo &cgd, bool initJoinBlocks)
: specialPoints(specialPoints), cgd(cgd),
initJoinBlocks(initJoinBlocks){};
Expand All @@ -125,7 +130,7 @@ struct TraceVerifyPredicate : public InitializerPredicate {
~TraceVerifyPredicate() override {}

private:
std::set<KBlock *> specialPoints;
std::set<KBlock *, KBlockCompare> specialPoints;
std::set<KFunction *> interestingFns;
std::set<KFunction *> uninsterestingFns;

Expand Down Expand Up @@ -195,7 +200,7 @@ struct KFunction : public KCallable {
std::unordered_map<const llvm::BasicBlock *, KBlock *> blockMap;
KBlock *entryKBlock;
std::vector<KBlock *> returnKBlocks;
std::set<KBlock *> finalKBlocks;
std::set<KBlock *, KBlockCompare> finalKBlocks;
std::vector<KCallBlock *> kCallBlocks;

/// count of instructions in function
Expand Down Expand Up @@ -246,14 +251,6 @@ struct KFunction : public KCallable {
[[nodiscard]] inline unsigned getGlobalIndex() const { return globalIndex; }
};

struct KBlockCompare {
bool operator()(const KBlock *a, const KBlock *b) const {
return a->parent->getGlobalIndex() < b->parent->getGlobalIndex() ||
(a->parent->getGlobalIndex() == b->parent->getGlobalIndex() &&
a->getId() < b->getId());
}
};

struct KFunctionCompare {
bool operator()(const KFunction *a, const KFunction *b) const {
return a->getGlobalIndex() < b->getGlobalIndex();
Expand Down Expand Up @@ -376,15 +373,6 @@ class KModule {
unsigned getGlobalIndex(const llvm::Instruction *inst) const;
};

struct KBlockLess {
bool operator()(const KBlock *a, const KBlock *b) const {
if (a->parent->getGlobalIndex() != b->parent->getGlobalIndex()) {
return a->parent->getGlobalIndex() < b->parent->getGlobalIndex();
}
return a->getId() < b->getId();
}
};

} // namespace klee

#endif /* KLEE_KMODULE_H */
2 changes: 1 addition & 1 deletion lib/Core/ExecutionState.h
Original file line number Diff line number Diff line change
Expand Up @@ -276,7 +276,7 @@ class ExecutionState {
std::uint32_t depth = 0;

/// @brief Exploration level, i.e., number of times KLEE cycled for this state
std::set<KBlock *, KBlockLess> level;
std::set<KBlock *, KBlockCompare> level;

/// @brief Address space used by this state (e.g. Global and Heap)
AddressSpace addressSpace;
Expand Down
2 changes: 1 addition & 1 deletion lib/Core/Executor.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -5231,7 +5231,7 @@ void Executor::run(std::vector<ExecutionState *> initialStates,
}
} else {
if (ExecutionMode == ExecutionKind::Bidirectional) {
std::set<KFunction *> allowed;
std::set<KFunction *, KFunctionCompare> allowed;
for (auto &i : kmodule->functions) {
allowed.insert(i.get());
}
Expand Down
4 changes: 2 additions & 2 deletions lib/Core/Initializer.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -184,7 +184,7 @@ void ConflictCoreInitializer::addConflictInit(const Conflict &conflict,
}

void ConflictCoreInitializer::initializeFunctions(
std::set<KFunction *> functions) {
std::set<KFunction *, KFunctionCompare> functions) {
allowed = functions;
// for (auto function : functions) {
// if (dismantledFunctions.count(function)) {
Expand Down Expand Up @@ -214,7 +214,7 @@ void ConflictCoreInitializer::addErrorInit(ref<Target> errorTarget) {
auto errorT = dyn_cast<ReproduceErrorTarget>(errorTarget);
auto location = errorTarget->getBlock();
// Check direction
std::set<KBlock *, KBlockLess> nearest;
std::set<KBlock *, KBlockCompare> nearest;
if (predicate(errorTarget->getBlock()) && !errorT->isThatError(Reachable)) {
nearest.insert(errorTarget->getBlock()); // HOT FIX
} else {
Expand Down
13 changes: 8 additions & 5 deletions lib/Core/Initializer.h
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ class ConflictCoreInitializer : public Initializer {

void addConflictInit(const Conflict &, KBlock *) override;

void initializeFunctions(std::set<KFunction *> functions);
void initializeFunctions(std::set<KFunction *, KFunctionCompare> functions);
void addErrorInit(ref<Target> errorTarget);

void update(const pobs_ty &added, const pobs_ty &removed) override;
Expand All @@ -54,10 +54,12 @@ class ConflictCoreInitializer : public Initializer {
std::map<ref<Target>, unsigned> knownTargets;

// Targets collected for each initial instruction
std::map<KInstruction *, std::set<ref<Target>>> targetMap;
std::map<KInstruction *, std::set<ref<Target>>, KInstructionCompare>
targetMap;

// Reverse
std::map<ref<Target>, std::set<KInstruction *>> instructionMap;
std::map<ref<Target>, std::set<KInstruction *, KInstructionCompare>>
instructionMap;

// awaiting until the are proof obligations in one of their targets
std::list<KInstruction *> awaiting;
Expand All @@ -68,12 +70,13 @@ class ConflictCoreInitializer : public Initializer {

// For every (KI, Target) pair in this map, there is a state that starts
// at KI and has Target as one of its targets.
std::map<KInstruction *, std::set<ref<Target>>> initialized;
std::map<KInstruction *, std::set<ref<Target>>, KInstructionCompare>
initialized;

// Already dismantled functions don't need to be dismantled again
std::unordered_set<KFunction *> dismantledFunctions;

std::set<KFunction *> allowed;
std::set<KFunction *, KFunctionCompare> allowed;

void addInit(KInstruction *from, ref<Target> to);
void addPob(ProofObligation *pob);
Expand Down
4 changes: 2 additions & 2 deletions lib/Core/TargetedExecutionManager.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -535,7 +535,7 @@ TargetedExecutionManager::prepareTargets(KModule *kmodule, SarifReport paths) {
backwardWhitelists[result.id]->addTrace(result, kf, locToBlocks, true);
}

std::set<KFunction *> functionsToDismantle;
std::set<KFunction *, KFunctionCompare> functionsToDismantle;
for (auto wl : forwardWhitelists) {
auto kf = wl.first;
auto &dist = codeGraphInfo.getDistance(kf);
Expand Down Expand Up @@ -585,7 +585,7 @@ TargetedExecutionManager::prepareTargets(KModule *kmodule,
backwardWhitelists[traceID]->addTrace(path, true);
}

std::set<KFunction *> functionsToDismantle;
std::set<KFunction *, KFunctionCompare> functionsToDismantle;
for (auto wl : forwardWhitelists) {
auto kf = wl.first;
auto &dist = codeGraphInfo.getDistance(kf);
Expand Down
4 changes: 2 additions & 2 deletions lib/Core/TargetedExecutionManager.h
Original file line number Diff line number Diff line change
Expand Up @@ -121,8 +121,8 @@ class TargetedExecutionManager final : public Subscriber {
std::map<KFunction *, ref<TargetForest>, KFunctionCompare>
forwardWhitelists;
std::map<std::string, ref<TargetForest>> backwardWhitelists;
std::set<KFunction *> functionsToDismantle;
std::set<KBlock *> specialPoints;
std::set<KFunction *, KFunctionCompare> functionsToDismantle;
std::set<KBlock *, KBlockCompare> specialPoints;
};

explicit TargetedExecutionManager(CodeGraphInfo &codeGraphInfo_,
Expand Down
8 changes: 4 additions & 4 deletions lib/Module/CodeGraphInfo.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -182,7 +182,7 @@ const FunctionDistanceMap &CodeGraphInfo::getBackwardDistance(KFunction *kf) {

void CodeGraphInfo::getNearestPredicateSatisfying(
KBlock *from, KBlockPredicate predicate, bool forward,
std::set<KBlock *, KBlockLess> &result) {
std::set<KBlock *, KBlockCompare> &result) {
std::unordered_set<KBlock *> visited;
std::unordered_set<KBlock *> queued;

Expand Down Expand Up @@ -235,9 +235,9 @@ CodeGraphInfo::getFunctionConditionalBranches(KFunction *kf) {
return functionConditionalBranches.at(kf);
}

std::set<KBlock *, KBlockLess> CodeGraphInfo::getNearestPredicateSatisfying(
std::set<KBlock *, KBlockCompare> CodeGraphInfo::getNearestPredicateSatisfying(
KBlock *from, KBlockPredicate predicate, bool forward) {
std::set<KBlock *, KBlockLess> result;
std::set<KBlock *, KBlockCompare> result;
getNearestPredicateSatisfying(from, predicate, forward, result);
return result;
}
Expand Down Expand Up @@ -266,7 +266,7 @@ CodeGraphInfo::dismantleFunction(KFunction *kf, KBlockPredicate predicate) {
queue.pop();
used.insert(kblock);
std::set<KBlock *> visited;
std::set<KBlock *, KBlockLess> nearest;
std::set<KBlock *, KBlockCompare> nearest;
getNearestPredicateSatisfying(kblock, predicate, true, nearest);
for (auto to : nearest) {
dismantled.push_back({kblock, to});
Expand Down
14 changes: 10 additions & 4 deletions lib/Module/KModule.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -639,6 +639,12 @@ KFunction::~KFunction() {
delete[] instructions;
}

bool KBlockCompare::operator()(const KBlock *a, const KBlock *b) const {
return a->parent->getGlobalIndex() < b->parent->getGlobalIndex() ||
(a->parent->getGlobalIndex() == b->parent->getGlobalIndex() &&
a->getId() < b->getId());
}

KBlock::KBlock(
KFunction *_kfunction, llvm::BasicBlock *block, KModule *km,
const std::unordered_map<Instruction *, unsigned> &instructionToRegisterMap,
Expand Down Expand Up @@ -701,16 +707,16 @@ KReturnBlock::KReturnBlock(
: KBlock::KBlock(_kfunction, block, km, instructionToRegisterMap,
instructionsKF, globalIndexInc) {}

std::set<KBlock *> KBlock::successors() {
std::set<KBlock *> result;
std::set<KBlock *, KBlockCompare> KBlock::successors() {
std::set<KBlock *, KBlockCompare> result;
for (auto bb : llvm::successors(basicBlock)) {
result.insert(parent->blockMap[bb]);
}
return result;
}

std::set<KBlock *> KBlock::predecessors() {
std::set<KBlock *> result;
std::set<KBlock *, KBlockCompare> KBlock::predecessors() {
std::set<KBlock *, KBlockCompare> result;
for (auto bb : llvm::predecessors(basicBlock)) {
result.insert(parent->blockMap[bb]);
}
Expand Down
18 changes: 9 additions & 9 deletions test/Bidirectional/CoverageErrorCall/fib-sum-dec.c.good
Original file line number Diff line number Diff line change
Expand Up @@ -46,28 +46,28 @@
[backward] Pob: path: (0 (main: (fib: %return %13) -> %13 %14 %if.then ->) 0) @ [0, %entry, reach_error]
[backward] To-be pob: path: (0 (main: (fib: %entry %if.then %return %13) -> %13 %14 %if.then ->) 0) @ [0, %entry, reach_error]
[backward] Composition sucessful.
[initializer] From [0, %4, fib] to Target: [%entry, fib] scheduled
[initializer] From [0, %9, fib] to Target: [%entry, fib] scheduled
[initializer] From [0, %7, main] to Target: [%entry, fib] scheduled
[initializer] From [0, %10, main] to Target: [%entry, fib] scheduled
[initializer] From [0, %13, main] to Target: [%entry, fib] scheduled
[initializer] From [0, %4, fib] to Target: [%entry, fib] scheduled
[initializer] From [0, %9, fib] to Target: [%entry, fib] scheduled
[initialize, executor] From [0, %entry, sum] to:
[initialize, executor] Target: [%2, sum] (at the end)
[initialize, executor] From [0, %4, fib] to:
[initialize, executor] Target: [%entry, fib]
[initialize, executor] From [0, %9, fib] to:
[initialize, executor] Target: [%entry, fib]
[initialize, executor] From [0, %7, main] to:
[initialize, executor] Target: [%entry, fib]
[initialize, executor] From [0, %10, main] to:
[initialize, executor] Target: [%entry, fib]
[initialize, executor] From [0, %13, main] to:
[initialize, executor] Target: [%entry, fib]
[initialize, executor] From [0, %4, fib] to:
[initialize, executor] Target: [%entry, fib]
[initialize, executor] From [0, %9, fib] to:
[initialize, executor] Target: [%entry, fib]
[reached] Isolated state: path: (0 (main: %13 ->) 0) @ [0, %entry, fib]
[reached] Isolated state: path: (0 (main: %7 ->) 0) @ [0, %entry, fib]
[reached] Isolated state: path: (0 (main: %10 ->) 0) @ [0, %entry, fib]
[reached] Isolated state: path: (0 (fib: %9 ->) 0) @ [0, %entry, fib]
[reached] Isolated state: path: (0 (fib: %4 ->) 0) @ [0, %entry, fib]
[reached] Isolated state: path: (0 (fib: %9 ->) 0) @ [0, %entry, fib]
[reached] Isolated state: path: (0 (main: %13 ->) 0) @ [0, %entry, fib]
[reached] Isolated state: path: (0 (main: %10 ->) 0) @ [0, %entry, fib]
[reached] Isolated state: path: (0 (sum: %entry %2) 0) @ None
[backward] State: path: (0 (main: %13 ->) 0) @ [0, %entry, fib]
[backward] Pob: path: (0 (main: (fib: %entry %if.then %return %13) -> %13 %14 %if.then ->) 0) @ [0, %entry, reach_error]
Expand Down

0 comments on commit 04d0710

Please sign in to comment.