Skip to content

Commit

Permalink
[style]
Browse files Browse the repository at this point in the history
  • Loading branch information
ocelaiwo committed Sep 30, 2024
1 parent c43bb04 commit 93a4929
Show file tree
Hide file tree
Showing 23 changed files with 87 additions and 100 deletions.
22 changes: 12 additions & 10 deletions include/klee/ADT/ImmutableList.h
Original file line number Diff line number Diff line change
Expand Up @@ -39,9 +39,9 @@ template <typename T> class ImmutableList {
}
}

ImmutableListNode(std::shared_ptr<ImmutableListNode> prev, size_t prev_len, std::vector<T> values)
: prev(prev), prev_len(prev_len), values(std::move(values)) {
}
ImmutableListNode(std::shared_ptr<ImmutableListNode> prev, size_t prev_len,
std::vector<T> values)
: prev(prev), prev_len(prev_len), values(std::move(values)) {}
};

std::shared_ptr<ImmutableListNode> node;
Expand Down Expand Up @@ -108,7 +108,8 @@ template <typename T> class ImmutableList {
if (!node) {
return;
}
node = std::make_shared<ImmutableListNode>(node->prev, node->prev_len, node->values);
node = std::make_shared<ImmutableListNode>(node->prev, node->prev_len,
node->values);
node->values.pop_back();
}

Expand All @@ -129,11 +130,10 @@ template <typename T> class ImmutableList {
return *it;
}

const T& front() const {
return at(0);
}
const T &front() const { return at(0); }

friend bool operator==(const ImmutableList<T> &lhs, const ImmutableList<T> &rhs) {
friend bool operator==(const ImmutableList<T> &lhs,
const ImmutableList<T> &rhs) {
if (lhs.size() != rhs.size()) {
return false;
}
Expand All @@ -151,11 +151,13 @@ template <typename T> class ImmutableList {
return true;
}

friend bool operator!=(const ImmutableList<T> &lhs, const ImmutableList<T> &rhs) {
friend bool operator!=(const ImmutableList<T> &lhs,
const ImmutableList<T> &rhs) {
return !(lhs == rhs);
}

friend bool operator<(const ImmutableList<T> &lhs, const ImmutableList<T> &rhs) {
friend bool operator<(const ImmutableList<T> &lhs,
const ImmutableList<T> &rhs) {
if (lhs.size() < rhs.size()) {
return true;
} else if (lhs.size() > rhs.size()) {
Expand Down
1 change: 0 additions & 1 deletion include/klee/Core/Interpreter.h
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,6 @@ enum class MockMutableGlobalsPolicy {
All, // Mock globals on module build stage and generate bc module for it
};


enum class ExecutionKind { Forward, Bidirectional };

class Interpreter {
Expand Down
1 change: 0 additions & 1 deletion include/klee/Expr/Constraints.h
Original file line number Diff line number Diff line change
Expand Up @@ -112,7 +112,6 @@ class ConstraintSet {
std::vector<ref<const IndependentConstraintSet>> &result) const;
};


class PathConstraints {
public:
using ordered_constraints_ty =
Expand Down
6 changes: 3 additions & 3 deletions include/klee/Expr/SourceBuilder.h
Original file line number Diff line number Diff line change
Expand Up @@ -29,9 +29,9 @@ class SourceBuilder {
symbolicSizeConstantAddress(unsigned version,
const KGlobalVariable *allocSite, ref<Expr> size);

static ref<SymbolicSource> symbolicSizeConstantAddress(unsigned version,
const KValue *allocSite,
ref<Expr> size);
static ref<SymbolicSource>
symbolicSizeConstantAddress(unsigned version, const KValue *allocSite,
ref<Expr> size);

static ref<SymbolicSource> makeSymbolic(const std::string &name,
unsigned version);
Expand Down
2 changes: 1 addition & 1 deletion include/klee/Expr/SymbolicSource.h
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@

#include "llvm/ADT/StringExtras.h"
#include "llvm/IR/Argument.h"
#include "llvm/IR/Instruction.h"
#include "llvm/IR/GlobalVariable.h"
#include "llvm/IR/Instruction.h"

#include <memory>
#include <set>
Expand Down
3 changes: 1 addition & 2 deletions include/klee/Module/CodeGraphInfo.h
Original file line number Diff line number Diff line change
Expand Up @@ -70,8 +70,7 @@ class CodeGraphInfo {
const FunctionDistanceMap &getBackwardDistance(KFunction *kf);

void getNearestPredicateSatisfying(KBlock *from, KBlockPredicate predicate,
bool forward,
KBlockSet &result);
bool forward, KBlockSet &result);

const KBlockMap<std::set<unsigned>> &getFunctionBranches(KFunction *kf);

Expand Down
2 changes: 0 additions & 2 deletions include/klee/Module/KInstruction.h
Original file line number Diff line number Diff line change
Expand Up @@ -136,7 +136,6 @@ struct KInstruction : public KValue {
}
};


struct CallStackFrame {
KInstruction *caller;
KFunction *kf;
Expand Down Expand Up @@ -173,7 +172,6 @@ struct CallStackFrame {
}
};


struct KGEPInstruction : KInstruction {
/// indices - The list of variable sized adjustments to add to the pointer
/// operand to execute the instruction. The first element is the operand
Expand Down
2 changes: 0 additions & 2 deletions include/klee/Module/KModule.h
Original file line number Diff line number Diff line change
Expand Up @@ -176,8 +176,6 @@ struct PredicateAdapter {
InitializerPredicate &predicate;
};



struct KBasicBlock : public KBlock {
public:
KBasicBlock(KFunction *, llvm::BasicBlock *, KModule *,
Expand Down
2 changes: 1 addition & 1 deletion include/klee/Module/TargetForest.h
Original file line number Diff line number Diff line change
Expand Up @@ -237,7 +237,7 @@ class TargetForest {
Layer(const InternalLayer &forest, const TargetsToVector &targetsToVector,
confidence::ty confidence)
: forest(forest), targetsToVector(targetsToVector),
confidence(confidence) {
confidence(confidence) {
for (auto &targetVect : targetsToVector) {
targets.insert(targetVect.first);
}
Expand Down
2 changes: 0 additions & 2 deletions lib/Core/BidirectionalSearcher.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,6 @@ llvm::cl::opt<unsigned> BackwardTicks("backward-ticks", llvm::cl::desc(""),
llvm::cl::init(25),
llvm::cl::cat(ExecCat));


BidirectionalSearcher::StepKind BidirectionalSearcher::selectStep() {
size_t initial_choice = ticker.getCurrent();
size_t choice = initial_choice;
Expand Down Expand Up @@ -141,7 +140,6 @@ BidirectionalSearcher::~BidirectionalSearcher() {
delete initializer;
}


ref<SearcherAction> ForwardOnlySearcher::selectAction() {
return new ForwardAction(&searcher->selectState());
}
Expand Down
53 changes: 27 additions & 26 deletions lib/Core/Composer.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -11,9 +11,8 @@ using namespace klee;
using namespace llvm;

bool ComposeHelper::collectMemoryObjects(
ExecutionState &state, ref<PointerExpr> address,
KInstruction *target, ref<Expr> &guard,
std::vector<ref<Expr>> &resolveConditions,
ExecutionState &state, ref<PointerExpr> address, KInstruction *target,
ref<Expr> &guard, std::vector<ref<Expr>> &resolveConditions,
std::vector<ref<Expr>> &unboundConditions,
ObjectResolutionList &resolvedMemoryObjects) {
bool mayBeOutOfBound = true;
Expand All @@ -28,10 +27,10 @@ bool ComposeHelper::collectMemoryObjects(
}

ref<Expr> checkOutOfBounds;
if (!checkResolvedMemoryObjects(
state, address, 0, mayBeResolvedMemoryObjects,
hasLazyInitialized, resolvedMemoryObjects, resolveConditions,
unboundConditions, checkOutOfBounds, mayBeOutOfBound)) {
if (!checkResolvedMemoryObjects(state, address, 0, mayBeResolvedMemoryObjects,
hasLazyInitialized, resolvedMemoryObjects,
resolveConditions, unboundConditions,
checkOutOfBounds, mayBeOutOfBound)) {
return false;
}

Expand All @@ -42,25 +41,25 @@ bool ComposeHelper::collectMemoryObjects(
return true;
}

bool ComposeHelper::tryResolveAddress(ExecutionState &state, ref<PointerExpr> address,
bool ComposeHelper::tryResolveAddress(ExecutionState &state,
ref<PointerExpr> address,
std::pair<ref<Expr>, ref<Expr>> &result) {
ref<Expr> guard;
std::vector<ref<Expr>> resolveConditions;
std::vector<ref<Expr>> unboundConditions;
ObjectResolutionList resolvedMemoryObjects;
KInstruction *target = nullptr;

if (!collectMemoryObjects(state, address, target, guard,
resolveConditions, unboundConditions,
resolvedMemoryObjects)) {
if (!collectMemoryObjects(state, address, target, guard, resolveConditions,
unboundConditions, resolvedMemoryObjects)) {
return false;
}

result.first = guard;
if (resolvedMemoryObjects.size() > 0) {
state.assumptions.insert(guard);
ref<Expr> resultAddress =
resolvedMemoryObjects.at(resolveConditions.size() - 1)->getBaseExpr();
resolvedMemoryObjects.at(resolveConditions.size() - 1)->getBaseExpr();

for (unsigned int i = 0; i < resolveConditions.size(); ++i) {
unsigned int index = resolveConditions.size() - 1 - i;
Expand All @@ -75,17 +74,17 @@ bool ComposeHelper::tryResolveAddress(ExecutionState &state, ref<PointerExpr> ad
return true;
}

bool ComposeHelper::tryResolveSize(ExecutionState &state, ref<PointerExpr> address,
bool ComposeHelper::tryResolveSize(ExecutionState &state,
ref<PointerExpr> address,
std::pair<ref<Expr>, ref<Expr>> &result) {
ref<Expr> guard;
std::vector<ref<Expr>> resolveConditions;
std::vector<ref<Expr>> unboundConditions;
ObjectResolutionList resolvedMemoryObjects;
KInstruction *target = nullptr;

if (!collectMemoryObjects(state, address, target, guard,
resolveConditions, unboundConditions,
resolvedMemoryObjects)) {
if (!collectMemoryObjects(state, address, target, guard, resolveConditions,
unboundConditions, resolvedMemoryObjects)) {
return false;
}

Expand All @@ -96,7 +95,7 @@ bool ComposeHelper::tryResolveSize(ExecutionState &state, ref<PointerExpr> addre
resolvedMemoryObjects.at(resolveConditions.size() - 1)->getSizeExpr();
for (unsigned int i = 0; i < resolveConditions.size(); ++i) {
unsigned int index = resolveConditions.size() - 1 - i;
ref<const MemoryObject> mo =resolvedMemoryObjects.at(index);
ref<const MemoryObject> mo = resolvedMemoryObjects.at(index);
resultSize = SelectExpr::create(resolveConditions[index],
mo->getSizeExpr(), resultSize);
}
Expand All @@ -119,9 +118,8 @@ bool ComposeHelper::tryResolveContent(
ObjectResolutionList mayBeResolvedMemoryObjects;
KInstruction *target = nullptr;

if (!resolveMemoryObjects(state, base, target, 0,
mayBeResolvedMemoryObjects, mayBeOutOfBound,
hasLazyInitialized, incomplete)) {
if (!resolveMemoryObjects(state, base, target, 0, mayBeResolvedMemoryObjects,
mayBeOutOfBound, hasLazyInitialized, incomplete)) {
return false;
}

Expand Down Expand Up @@ -302,8 +300,9 @@ ref<Expr> ComposeVisitor::processRead(const Array *root,
}
case SymbolicSource::Kind::LazyInitializationAddress: {
auto pointer =
visit(cast<LazyInitializationSource>(root->source)->pointer);
ref<PointerExpr> address = cast<PointerExpr>(PointerExpr::create(pointer));
visit(cast<LazyInitializationSource>(root->source)->pointer);
ref<PointerExpr> address =
cast<PointerExpr>(PointerExpr::create(pointer));
auto guardedAddress =
helper.fillLazyInitializationAddress(state, address);
safetyConstraints.insert(guardedAddress.first);
Expand All @@ -312,17 +311,19 @@ ref<Expr> ComposeVisitor::processRead(const Array *root,
}
case SymbolicSource::Kind::LazyInitializationSize: {
auto pointer =
visit(cast<LazyInitializationSource>(root->source)->pointer);
ref<PointerExpr> address = cast<PointerExpr>(PointerExpr::create(pointer));
visit(cast<LazyInitializationSource>(root->source)->pointer);
ref<PointerExpr> address =
cast<PointerExpr>(PointerExpr::create(pointer));
auto guardedSize = helper.fillLazyInitializationSize(state, address);
safetyConstraints.insert(guardedSize.first);
composedArray = guardedSize.second;
break;
}
case SymbolicSource::Kind::LazyInitializationContent: {
auto pointer =
visit(cast<LazyInitializationSource>(root->source)->pointer);
ref<PointerExpr> address = cast<PointerExpr>(PointerExpr::create(pointer));
visit(cast<LazyInitializationSource>(root->source)->pointer);
ref<PointerExpr> address =
cast<PointerExpr>(PointerExpr::create(pointer));
// index is not used because there are conditions composed before
// that act as the index check
auto guardedContent =
Expand Down
22 changes: 10 additions & 12 deletions lib/Core/Composer.h
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,7 @@ struct ComposeHelper {
ComposeHelper(Executor *_executor) : executor(_executor) {}

bool getResponse(const ExecutionState &state, ref<Expr> expr,
ref<SolverResponse> &queryResult,
SolverQueryMetaData &) {
ref<SolverResponse> &queryResult, SolverQueryMetaData &) {
executor->solver->setTimeout(executor->coreSolverTimeout);
bool success = executor->solver->getResponse(
state.constraints.withAssumtions(state.assumptions), expr, queryResult,
Expand All @@ -43,8 +42,7 @@ struct ComposeHelper {

bool evaluate(const ExecutionState &state, ref<Expr> expr,
ref<SolverResponse> &queryResult,
ref<SolverResponse> &negateQueryResult,
SolverQueryMetaData &) {
ref<SolverResponse> &negateQueryResult, SolverQueryMetaData &) {
executor->solver->setTimeout(executor->coreSolverTimeout);
bool success = executor->solver->evaluate(
state.constraints.withAssumtions(state.assumptions), expr, queryResult,
Expand All @@ -54,8 +52,7 @@ struct ComposeHelper {
}

bool resolveMemoryObjects(ExecutionState &state, ref<PointerExpr> address,
KInstruction *target,
unsigned bytes,
KInstruction *target, unsigned bytes,
ObjectResolutionList &mayBeResolvedMemoryObjects,
bool &mayBeOutOfBound, bool &mayLazyInitialize,
bool &incomplete) {
Expand All @@ -65,16 +62,16 @@ struct ComposeHelper {
}

bool checkResolvedMemoryObjects(
ExecutionState &state, ref<PointerExpr> address,
unsigned bytes, const ObjectResolutionList &mayBeResolvedMemoryObjects,
ExecutionState &state, ref<PointerExpr> address, unsigned bytes,
const ObjectResolutionList &mayBeResolvedMemoryObjects,
bool hasLazyInitialized, ObjectResolutionList &resolvedMemoryObjects,
std::vector<ref<Expr>> &resolveConditions,
std::vector<ref<Expr>> &unboundConditions, ref<Expr> &checkOutOfBounds,
bool &mayBeOutOfBound) {
return executor->checkResolvedMemoryObjects(
state, address, bytes, mayBeResolvedMemoryObjects,
hasLazyInitialized, resolvedMemoryObjects, resolveConditions,
unboundConditions, checkOutOfBounds, mayBeOutOfBound);
state, address, bytes, mayBeResolvedMemoryObjects, hasLazyInitialized,
resolvedMemoryObjects, resolveConditions, unboundConditions,
checkOutOfBounds, mayBeOutOfBound);
}

bool makeGuard(ExecutionState &state,
Expand Down Expand Up @@ -160,7 +157,8 @@ struct ComposeHelper {
}

std::pair<ref<Expr>, ref<Expr>>
fillLazyInitializationAddress(ExecutionState &state, ref<PointerExpr> pointer);
fillLazyInitializationAddress(ExecutionState &state,
ref<PointerExpr> pointer);

std::pair<ref<Expr>, ref<Expr>>
fillLazyInitializationSize(ExecutionState &state, ref<PointerExpr> pointer);
Expand Down
9 changes: 4 additions & 5 deletions lib/Core/DistanceCalculator.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -102,8 +102,7 @@ DistanceResult DistanceCalculator::computeDistance(KBlock *kb, TargetKind kind,
break;

case PreTarget:
res = tryGetPreTargetWeight(kb, weight, distanceToTargetFunction,
reversed);
res = tryGetPreTargetWeight(kb, weight, distanceToTargetFunction, reversed);
isInsideFunction = false;
break;

Expand Down Expand Up @@ -227,7 +226,8 @@ DistanceCalculator::tryGetLocalWeight(KBlock *kb, weight_type &weight,
WeightResult DistanceCalculator::tryGetPreTargetWeight(
KBlock *kb, weight_type &weight,
const std::unordered_map<KFunction *, unsigned int>
&distanceToTargetFunction, bool reversed) const {
&distanceToTargetFunction,
bool reversed) const {
KFunction *currentKF = kb->parent;
std::vector<KBlock *> localTargets;
for (auto kCallBlock : currentKF->kCallBlocks) {
Expand Down Expand Up @@ -265,7 +265,6 @@ WeightResult DistanceCalculator::tryGetTargetWeight(KBlock *kb,
KBlock *target,
bool reversed) const {
std::vector<KBlock *> localTargets = {target};
WeightResult res =
tryGetLocalWeight(kb, weight, localTargets, reversed);
WeightResult res = tryGetLocalWeight(kb, weight, localTargets, reversed);
return res;
}
3 changes: 2 additions & 1 deletion lib/Core/DistanceCalculator.h
Original file line number Diff line number Diff line change
Expand Up @@ -125,7 +125,8 @@ class DistanceCalculator {
WeightResult
tryGetPreTargetWeight(KBlock *kb, weight_type &weight,
const std::unordered_map<KFunction *, unsigned int>
&distanceToTargetFunction,bool reversed) const;
&distanceToTargetFunction,
bool reversed) const;

WeightResult tryGetTargetWeight(KBlock *kb, weight_type &weight,
KBlock *target, bool reversed) const;
Expand Down
Loading

0 comments on commit 93a4929

Please sign in to comment.