Skip to content

Commit

Permalink
[fix]
Browse files Browse the repository at this point in the history
  • Loading branch information
misonijnik committed Oct 12, 2023
1 parent dc829b0 commit 3f26228
Show file tree
Hide file tree
Showing 2 changed files with 49 additions and 44 deletions.
32 changes: 2 additions & 30 deletions include/klee/Expr/SymbolicSource.h
Original file line number Diff line number Diff line change
Expand Up @@ -119,20 +119,7 @@ class UninitializedSource : public SymbolicSource {

unsigned computeHash() override;

int internalCompare(const SymbolicSource &b) const override {
if (getKind() != b.getKind()) {
return getKind() < b.getKind() ? -1 : 1;
}
const UninitializedSource &ub = static_cast<const UninitializedSource &>(b);

if (version == ub.version && allocSite == ub.allocSite) {
return 0;
}

return std::tie(version, allocSite) < std::tie(ub.version, ub.allocSite)
? -1
: 1;
}
int internalCompare(const SymbolicSource &b) const override;
};

class SymbolicSizeConstantAddressSource : public SymbolicSource {
Expand All @@ -159,22 +146,7 @@ class SymbolicSizeConstantAddressSource : public SymbolicSource {

virtual unsigned computeHash() override;

virtual int internalCompare(const SymbolicSource &b) const override {
if (getKind() != b.getKind()) {
return getKind() < b.getKind() ? -1 : 1;
}
const SymbolicSizeConstantAddressSource &ub =
static_cast<const SymbolicSizeConstantAddressSource &>(b);

if (version == ub.version && allocSite == ub.allocSite && size == ub.size) {
return 0;
}

return std::tie(version, allocSite, size) <
std::tie(ub.version, ub.allocSite, size)
? -1
: 1;
}
virtual int internalCompare(const SymbolicSource &b) const override;
};

class MakeSymbolicSource : public SymbolicSource {
Expand Down
61 changes: 47 additions & 14 deletions lib/Expr/SymbolicSource.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -69,6 +69,46 @@ unsigned UninitializedSource::computeHash() {
return hashValue;
}

int UninitializedSource::internalCompare(const SymbolicSource &b) const {
if (getKind() != b.getKind()) {
return getKind() < b.getKind() ? -1 : 1;
}
const UninitializedSource &ub = static_cast<const UninitializedSource &>(b);

if (version != ub.version) {
return version < ub.version ? -1 : 1;
}

if (allocSite != ub.allocSite) {
return allocSite->getGlobalIndex() < ub.allocSite->getGlobalIndex() ? -1
: 1;
}

return 0;
}

int SymbolicSizeConstantAddressSource::internalCompare(
const SymbolicSource &b) const {
if (getKind() != b.getKind()) {
return getKind() < b.getKind() ? -1 : 1;
}
const SymbolicSizeConstantAddressSource &ub =
static_cast<const SymbolicSizeConstantAddressSource &>(b);

if (version != ub.version) {
return version < ub.version ? -1 : 1;
}
if (size != ub.size) {
return size < ub.size ? -1 : 1;
}
if (allocSite != ub.allocSite) {
return allocSite->getGlobalIndex() < ub.allocSite->getGlobalIndex() ? -1
: 1;
}

return 0;
}

unsigned SymbolicSizeConstantAddressSource::computeHash() {
unsigned res = getKind();
res = res * MAGIC_HASH_CONSTANT + version;
Expand Down Expand Up @@ -124,21 +164,14 @@ int InstructionSource::internalCompare(const SymbolicSource &b) const {
}
assert(km == ib.km);
auto function = allocSite.getParent()->getParent();
auto bFunction = ib.allocSite.getParent()->getParent();
if (km->getFunctionId(function) != km->getFunctionId(bFunction)) {
return km->getFunctionId(function) < km->getFunctionId(bFunction) ? -1 : 1;
}
auto kf = km->functionMap.at(function);
auto block = allocSite.getParent();
auto bBlock = ib.allocSite.getParent();
if (kf->blockMap[block]->getId() != kf->blockMap[bBlock]->getId()) {
return kf->blockMap[block]->getId() < kf->blockMap[bBlock]->getId() ? -1
: 1;
}
if (kf->instructionMap[&allocSite]->getIndex() !=
kf->instructionMap[&ib.allocSite]->getIndex()) {
return kf->instructionMap[&allocSite]->getIndex() <
kf->instructionMap[&ib.allocSite]->getIndex()
auto bfunction = ib.allocSite.getParent()->getParent();
auto bkf = km->functionMap.at(bfunction);

if (kf->instructionMap[&allocSite]->getGlobalIndex() !=
bkf->instructionMap[&ib.allocSite]->getGlobalIndex()) {
return kf->instructionMap[&allocSite]->getGlobalIndex() <
bkf->instructionMap[&ib.allocSite]->getGlobalIndex()
? -1
: 1;
}
Expand Down

0 comments on commit 3f26228

Please sign in to comment.