[feat] Expand Target

misonijnik · Nov 15, 2022 · 9368da9 · 9368da9
1 parent 08ccd1a
commit 9368da9
Show file tree

Hide file tree

Showing 4 changed files with 64 additions and 14 deletions.
diff --git a/include/klee/Module/Locations.h b/include/klee/Module/Locations.h
@@ -58,10 +58,21 @@ class Location {
 
   friend bool operator <(const Location& lhs, const Location& rhs) {
     return
-           lhs.line < rhs.line     ||     (lhs.line == rhs.line &&
-        (lhs.offset < rhs.offset   ||   (lhs.offset == rhs.offset &&
-      (lhs.filename < rhs.filename || (lhs.filename == rhs.filename &&
-      (lhs.function < rhs.function))))));
+            lhs.line < rhs.line     ||     (lhs.line == rhs.line &&
+         (lhs.offset < rhs.offset   ||   (lhs.offset == rhs.offset &&
+       (lhs.filename < rhs.filename || (lhs.filename == rhs.filename &&
+       (lhs.function < rhs.function || (lhs.function == rhs.function &&
+    (lhs.instruction < rhs.instruction))))))));
+  }
+
+  friend bool operator==(const Location &lhs, const Location &rhs) {
+    return lhs.line == rhs.line && lhs.offset == rhs.offset &&
+           lhs.filename == rhs.filename && lhs.function == rhs.function &&
+           lhs.instruction == rhs.instruction;
+  }
+
+  friend bool operator!=(const Location &lhs, const Location &rhs) {
+    return !(lhs == rhs);
   }
 };
 

diff --git a/lib/Core/Target.cpp b/lib/Core/Target.cpp
@@ -49,8 +49,9 @@ std::string Target::toString() const {
 Target::EquivTargetHashSet Target::cachedTargets;
 Target::TargetHashSet Target::targets;
 
-ref<Target> Target::create(KBlock *_block, ReachWithError error) {
-  Target *target = new Target(_block, error);
+ref<Target> Target::create(Location *_location, KBlock *_block,
+                           ReachWithError error, unsigned id) {
+  Target *target = new Target(_location, _block, error, id);
   std::pair<TargetHashSet::const_iterator, bool> success =
       cachedTargets.insert(target);
   if (success.second) {
@@ -64,7 +65,13 @@ ref<Target> Target::create(KBlock *_block, ReachWithError error) {
   return target;
 }
 
-ref<Target> Target::create(KBlock *_block) { return create(_block, ReachWithError::None); }
+ref<Target> Target::create(KBlock *_block, ReachWithError error) {
+  return create(nullptr, _block, error, 0);
+}
+
+ref<Target> Target::create(KBlock *_block) {
+  return create(_block, ReachWithError::None);
+}
 
 Target::~Target() {
   if (targets.find(this) != targets.end()) {

diff --git a/lib/Core/Target.h b/lib/Core/Target.h
@@ -45,35 +45,60 @@ struct Target {
   typedef std::unordered_set<Target *, TargetHash, TargetCmp> TargetHashSet;
   static EquivTargetHashSet cachedTargets;
   static TargetHashSet targets;
+  Location *location;
   KBlock *block;
   ReachWithError error;
+  unsigned id = 0;
 
-  explicit Target(KBlock *_block, ReachWithError error)
-      : block(_block), error(error) {}
+  explicit Target(Location *_location, KBlock *_block, ReachWithError error,
+                  unsigned id)
+      : location(_location), block(_block), error(error), id(id) {}
 
 public:
   /// @brief Required by klee::ref-managed objects
   class ReferenceCounter _refCount;
 
+  static ref<Target> create(Location *_location, KBlock *_block,
+                            ReachWithError error, unsigned id);
   static ref<Target> create(KBlock *_block, ReachWithError error);
   static ref<Target>
   create(KBlock *_block); // TODO: [Aleksandr Misonizhnik], I think, this
                           // constructor should be entirely deleted
 
   int compare(const Target &other) const {
-    if (error != other.error)
+    if (error != other.error) {
       return error < other.error ? -1 : 1;
-    if (block != other.block)
+    }
+    if (block != other.block) {
       return block < other.block ? -1 : 1;
+    }
+    if (location == nullptr || other.location == nullptr) {
+      if (location != other.location) {
+        return location < other.location ? -1 : 1;
+      } else {
+        return 0;
+      }
+    }
+    if (*location != *other.location) {
+      return (*location < *other.location) ? -1 : 1;
+    }
+    if (id != other.id) {
+      return id < other.id ? -1 : 1;
+    }
     return 0;
   }
 
   bool operator<(const Target &other) const {
-    return block < other.block || (block == other.block && error < other.error);
+    return
+        block < other.block    || (block == other.block &&
+       (error < other.error    || (error == other.error &&
+    (location < other.location || (location == other.location &&
+          (id < other.id))))));
   }
 
   bool operator==(const Target &other) const {
-    return block == other.block && error == other.error;
+    return block == other.block && error == other.error &&
+           location == other.location && id == other.id;
   }
 
   bool atReturn() const { return isa<KReturnBlock>(block); }

diff --git a/lib/Core/TargetedExecutionManager.cpp b/lib/Core/TargetedExecutionManager.cpp
@@ -103,7 +103,14 @@ ref<Target> addNewLocation(LocatedEvent *le, KBlock *block) {
   } else {
     targets = targetsIt->second;
   }
-  ref<Target> target = Target::create(block, error);
+
+  ref<Target> target;
+  if (error != None) {
+    target = Target::create(&le->location, block, error, le->id);
+  } else {
+    target = Target::create(block, error);
+  }
+
   targets->push_back(target);
   tem->target2location.insert(std::make_pair(target, le));
   return target;