[WIP]add AbstractValue (#1423)

* first commit of Abstract Value and its related changes * update symabs * some modification * fix some bugs for big prog * rename some key data structure * rename some data struct * rename abstractInterpretation --------- Co-authored-by: bjjwwang <bjjwwang@github.com> Co-authored-by: jiawei-95 <jiawei.ren95@foxmail.com>
SVF-tools · Apr 4, 2024 · 0d210da · 0d210da
1 parent 72dcf10
commit 0d210da
Show file tree

Hide file tree

Showing 20 changed files with 2,106 additions and 1,709 deletions.
diff --git a/svf-llvm/tools/AE/ae.cpp b/svf-llvm/tools/AE/ae.cpp
diff --git a/svf/include/AE/Core/AbstractState.h b/svf/include/AE/Core/AbstractState.h
diff --git a/svf/include/AE/Core/AbstractValue.h b/svf/include/AE/Core/AbstractValue.h
diff --git a/svf/include/AE/Core/AddressValue.h b/svf/include/AE/Core/AddressValue.h
@@ -33,44 +33,43 @@
 #define AddressMask 0x7f000000
 #define FlippedAddressMask (AddressMask^0xffffffff)
 // the address of the black hole, getVirtualMemAddress(2);
-#define BlackHoleAddr 0x7f000000 + 2;
+#define BlackHoleAddr 0x7f000000 + 2
 
-#include "AE/Core/AbstractValue.h"
 #include "Util/GeneralType.h"
+#include <sstream>
 
 namespace SVF
 {
-class AddressValue : public AbstractValue
+class AddressValue
 {
 public:
     typedef Set<u32_t> AddrSet;
 private:
     AddrSet _addrs;
 public:
     /// Default constructor
-    AddressValue() : AbstractValue(AddressK) {}
+    AddressValue() {}
 
     /// Constructor
-    AddressValue(const Set<u32_t> &addrs) : AbstractValue(AddressK), _addrs(addrs) {}
+    AddressValue(const Set<u32_t> &addrs) :  _addrs(addrs) {}
 
-    AddressValue(u32_t addr) : AbstractValue(AddressK), _addrs({addr}) {}
+    AddressValue(u32_t addr) :  _addrs({addr}) {}
 
     /// Default destructor
     ~AddressValue() = default;
 
     /// Copy constructor
-    AddressValue(const AddressValue &other) : AbstractValue(AddressK), _addrs(other._addrs) {}
+    AddressValue(const AddressValue &other) : _addrs(other._addrs) {}
 
     /// Move constructor
-    AddressValue(AddressValue &&other) noexcept: AbstractValue(AddressK), _addrs(std::move(other._addrs)) {}
+    AddressValue(AddressValue &&other) noexcept: _addrs(std::move(other._addrs)) {}
 
     /// Copy operator=
     AddressValue &operator=(const AddressValue &other)
     {
         if (!this->equals(other))
         {
             _addrs = other._addrs;
-            AbstractValue::operator=(other);
         }
         return *this;
     }
@@ -81,7 +80,6 @@ class AddressValue : public AbstractValue
         if (this != &other)
         {
             _addrs = std::move(other._addrs);
-            AbstractValue::operator=(std::move(other));
         }
         return *this;
     }
@@ -91,17 +89,6 @@ class AddressValue : public AbstractValue
         return _addrs == rhs._addrs;
     }
 
-    bool operator==(const AddressValue &rhs) const
-    {
-        return _addrs == rhs._addrs;
-    }
-
-    /// Operator !=
-    bool operator!=(const AddressValue &rhs) const
-    {
-        return _addrs != rhs._addrs;
-    }
-
     AddrSet::const_iterator begin() const
     {
         return _addrs.cbegin();
@@ -181,26 +168,45 @@ class AddressValue : public AbstractValue
         return !v.empty();
     }
 
-    inline bool isTop() const override
+    inline bool isTop() const
     {
-        return *this == BlackHoleAddr;
+        return *this->begin() == BlackHoleAddr;
     }
 
-    inline bool isBottom() const override
+    inline bool isBottom() const
     {
         return empty();
     }
 
     inline void setTop()
     {
-        *this = BlackHoleAddr;
+        *this = AddressValue(BlackHoleAddr);
     }
 
     inline void setBottom()
     {
         _addrs.clear();
     }
 
+    const std::string toString() const
+    {
+        std::string str;
+        std::stringstream rawStr(str);
+        if (this->isBottom())
+        {
+            rawStr << "⊥";
+        }
+        else
+        {
+            rawStr << "[";
+            for (auto it = _addrs.begin(), eit = _addrs.end(); it!= eit; ++it) {
+                rawStr << *it << ", ";
+            }
+            rawStr << "]";
+        }
+        return rawStr.str();
+    }
+
     /// The physical address starts with 0x7f...... + idx
     static inline u32_t getVirtualMemAddress(u32_t idx)
     {

diff --git a/svf/include/AE/Core/ExeState.h b/svf/include/AE/Core/ExeState.h
@@ -39,7 +39,7 @@
 namespace SVF
 {
 
-class IntervalExeState;
+class SparseAbstractState;
 
 /*!
  * Base execution state
@@ -196,7 +196,7 @@ class ExeState
             auto it = rhs.find(item.first);
             if (it == rhs.end())
                 return false;
-            if (item.second != it->second)
+            if (item.second.equals(it->second))
             {
                 return false;
             }