refactor some api in intervalValue

SVF-tools · May 20, 2024 · 5a37d48 · 5a37d48
1 parent 64dc0bf
commit 5a37d48
Show file tree

Hide file tree

Showing 5 changed files with 43 additions and 8 deletions.
diff --git a/svf/include/AE/Core/AbstractState.h b/svf/include/AE/Core/AbstractState.h
@@ -393,7 +393,7 @@ class AbstractState
             auto it = rhs.find(item.first);
             if (it == rhs.end()) return false;
             // judge from expr id
-            if (item.second.getInterval().geq(it->second.getInterval())) return false;
+            if (item.second.getInterval().contain(it->second.getInterval())) return false;
         }
         return true;
     }
@@ -409,7 +409,8 @@ class AbstractState
             // judge from expr id
             if (it->second.isInterval() && item.second.isInterval())
             {
-                if (!it->second.getInterval().geq(item.second.getInterval()))
+                if (!it->second.getInterval().contain(
+                        item.second.getInterval()))
                     return false;
             }
 

diff --git a/svf/include/AE/Core/IntervalValue.h b/svf/include/AE/Core/IntervalValue.h
@@ -299,7 +299,8 @@ class IntervalValue
     }
 
     /// Check current IntervalValue is smaller than or equal to the other
-    bool leq(const IntervalValue &other) const
+    /// this: [2,3], other: [1, 4], return true
+    bool isSubset(const IntervalValue &other) const
     {
         if (this->isBottom())
         {
@@ -317,7 +318,8 @@ class IntervalValue
     }
 
     /// Check current IntervalValue is greater than or equal to the other
-    bool geq(const IntervalValue &other) const
+    /// this: [1,4], other: [2,3], return true
+    bool contain(const IntervalValue &other) const
     {
         if (this->isBottom())
         {
@@ -333,6 +335,38 @@ class IntervalValue
         }
     }
 
+    /// Check the upper bound of this Interval is less than or equal to the lower bound
+    /// e.g. [1, 3] < [3, 5] return true, lhs.ub <= rhs.lb
+    bool leq(const IntervalValue &other) const {
+        if (this->isBottom()) {
+            return true;
+        }
+        else if (other.isBottom())
+        {
+            return false;
+        }
+        else
+        {
+            return this->_ub.leq(other._lb);
+        }
+    }
+
+    /// Check the lower bound of this Interval is greater than or equal to the upper bound
+    /// e.g. [3, 5] > [1, 3] return true, lhs.lb >= rhs.ub
+    bool geq(const IntervalValue &other) const {
+        if (this->isBottom())                {
+            return true;
+        }
+        else if (other.isBottom())
+        {
+            return false;
+        }
+        else
+        {
+            return this->_lb.geq(other._ub);
+        }
+    }
+
 
     /// Equality comparison
     bool equals(const IntervalValue &other) const

diff --git a/svf/include/MemoryModel/ConditionalPT.h b/svf/include/MemoryModel/ConditionalPT.h
@@ -454,7 +454,7 @@ class CondPointsToSet
         }
     }
 
-    /// Check whether this CondPointsToSet is a subset of RHS
+    /// Check whether this CondPointsToSet is a isSubset of RHS
     inline bool isSubset(const CondPointsToSet<Cond>& rhs) const
     {
         if (pointsTo().size() > rhs.pointsTo().size())

diff --git a/svf/include/Util/NodeIDAllocator.h b/svf/include/Util/NodeIDAllocator.h
@@ -146,7 +146,7 @@ class NodeIDAllocator
         /// Returns vector mapping previously allocated node IDs to a smarter allocation
         /// based on the points-to sets in pta accessed through keys.
         /// The second part of the keys pairs are the number of (potential) occurrences of that points-to set
-        /// or a subset, depending on the client's wish.
+        /// or a isSubset, depending on the client's wish.
         /// TODO: interfaces are getting unwieldy, an initialised object may be better.
         /// TODO: kind of sucks pta can't be const here because getPts isn't.
         static std::vector<NodeID> cluster(BVDataPTAImpl *pta, const std::vector<std::pair<NodeID, unsigned>> keys, std::vector<std::pair<hclust_fast_methods, std::vector<NodeID>>> &candidates, std::string evalSubtitle="");

diff --git a/svf/include/Util/iterator.h b/svf/include/Util/iterator.h
@@ -19,10 +19,10 @@ namespace SVF
 {
 
 /// CRTP base class which implements the entire standard iterator facade
-/// in terms of a minimal subset of the interface.
+/// in terms of a minimal isSubset of the interface.
 ///
 /// Use this when it is reasonable to implement most of the iterator
-/// functionality in terms of a core subset. If you need special behavior or
+/// functionality in terms of a core isSubset. If you need special behavior or
 /// there are performance implications for this, you may want to override the
 /// relevant members instead.
 ///