From 3f262280ab493595b11a5e98fb9772b6d7f1d8a8 Mon Sep 17 00:00:00 2001
From: Aleksandr Misonizhnik <misonijnik@gmail.com>
Date: Fri, 13 Oct 2023 00:27:31 +0400
Subject: [PATCH] [fix]

---
 include/klee/Expr/SymbolicSource.h | 32 +---------------
 lib/Expr/SymbolicSource.cpp        | 61 +++++++++++++++++++++++-------
 2 files changed, 49 insertions(+), 44 deletions(-)

diff --git a/include/klee/Expr/SymbolicSource.h b/include/klee/Expr/SymbolicSource.h
index 064169423e8..92b506db208 100644
--- a/include/klee/Expr/SymbolicSource.h
+++ b/include/klee/Expr/SymbolicSource.h
@@ -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 {
@@ -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 {
diff --git a/lib/Expr/SymbolicSource.cpp b/lib/Expr/SymbolicSource.cpp
index ffbf94959c1..1f78147c2b8 100644
--- a/lib/Expr/SymbolicSource.cpp
+++ b/lib/Expr/SymbolicSource.cpp
@@ -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;
@@ -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;
   }