Merge pull request #1287 from jiawei-95/new

add symbolic abstraction
SVF-tools · Dec 18, 2023 · e09c431 · e09c431
2 parents e6570fa + 4f1f17a
commit e09c431
Show file tree

Hide file tree

Showing 4 changed files with 260 additions and 53 deletions.
diff --git a/svf/include/AbstractExecution/IntervalExeState.h b/svf/include/AbstractExecution/IntervalExeState.h
@@ -55,6 +55,7 @@ namespace SVF
 class IntervalExeState : public ExeState
 {
     friend class SVFIR2ItvExeState;
+    friend class RelationSolver;
 
 public:
     typedef Map<u32_t, IntervalValue> VarToValMap;
@@ -113,7 +114,7 @@ class IntervalExeState : public ExeState
     }
 
     /// Set all value bottom
-    IntervalExeState bottom()
+    IntervalExeState bottom() const
     {
         IntervalExeState inv = *this;
         for (auto &item: inv._varToItvVal)
@@ -124,7 +125,7 @@ class IntervalExeState : public ExeState
     }
 
     /// Set all value top
-    IntervalExeState top()
+    IntervalExeState top() const
     {
         IntervalExeState inv = *this;
         for (auto &item: inv._varToItvVal)

diff --git a/svf/include/AbstractExecution/NumericLiteral.h b/svf/include/AbstractExecution/NumericLiteral.h
@@ -437,4 +437,14 @@ class NumericLiteral
 
 }; // end class NumericLiteral
 } // end namespace SVF
+
+/// Specialise hash for NumericLiteral
+template<>
+struct std::hash<SVF::NumericLiteral>
+{
+    size_t operator()(const SVF::NumericLiteral &n) const
+    {
+        return n.getNumeral();
+    }
+};
 #endif //Z3_EXAMPLE_Number_H
diff --git a/svf/include/AbstractExecution/RelationSolver.h b/svf/include/AbstractExecution/RelationSolver.h
@@ -44,24 +44,38 @@ class RelationSolver
     IntervalExeState (the last element of inputs) for RSY or bilateral solver */
 
     /// Return Z3Expr according to valToValMap
-    Z3Expr gamma_hat(IntervalExeState &exeState);
+    Z3Expr gamma_hat(const IntervalExeState &exeState) const;
 
     /// Return Z3Expr according to another valToValMap
-    Z3Expr gamma_hat(IntervalExeState &alpha, IntervalExeState &exeState);
+    Z3Expr gamma_hat(const IntervalExeState &alpha, const IntervalExeState &exeState) const;
 
     /// Return Z3Expr from a NodeID
-    Z3Expr gamma_hat(u32_t id, IntervalExeState &exeState);
+    Z3Expr gamma_hat(u32_t id, const IntervalExeState &exeState) const;
 
-    IntervalExeState abstract_consequence(IntervalExeState &lower, IntervalExeState &upper, IntervalExeState &domain);
+    IntervalExeState abstract_consequence(const IntervalExeState &lower, const IntervalExeState &upper, const IntervalExeState &domain) const;
 
-    IntervalExeState beta(Map<u32_t, double> &sigma, IntervalExeState &exeState);
+    IntervalExeState beta(const Map<u32_t, double> &sigma, const IntervalExeState &exeState) const;
+
+
+    /// Return Z3 expression lazily based on SVFVar ID
+    virtual inline Z3Expr toZ3Expr(u32_t varId) const
+    {
+        return Z3Expr::getContext().int_const(std::to_string(varId).c_str());
+    }
 
     /* two optional solvers: RSY and bilateral */
 
-    IntervalExeState bilateral(IntervalExeState domain, Z3Expr phi, u32_t descend_check = 0);
+    IntervalExeState bilateral(const IntervalExeState& domain, const Z3Expr &phi, u32_t descend_check = 0);
+
+    IntervalExeState RSY(const IntervalExeState& domain, const Z3Expr &phi);
+
+    Map<u32_t, NumericLiteral> BoxedOptSolver(const Z3Expr& phi, Map<u32_t, NumericLiteral>& ret, Map<u32_t, NumericLiteral>& low_values, Map<u32_t, NumericLiteral>& high_values);
+
+    IntervalExeState BS(const IntervalExeState& domain, const Z3Expr &phi);
 
-    IntervalExeState RSY(IntervalExeState domain, const Z3Expr &phi);
+    void updateMap(Map<u32_t, NumericLiteral>& map, u32_t key, const NumericLiteral& value);
 
+    void decide_cpa_ext(const Z3Expr &phi, Map<u32_t, Z3Expr>&, Map<u32_t, NumericLiteral>&, Map<u32_t, NumericLiteral>&, Map<u32_t, NumericLiteral>&, Map<u32_t, NumericLiteral>&);
 };
 }