update AE library

svf/include/AE/Core/BoundedZ3Expr.h

@@ -53,6 +53,8 @@ class BoundedZ3Expr : public Z3Expr
 
     BoundedZ3Expr(s64_t i) : Z3Expr(getContext().int_val((int64_t)i)) {}
 
+    BoundedZ3Expr(double i) : Z3Expr(getContext().real_val(std::to_string(i).c_str())) {}
+
     BoundedZ3Expr(const BoundedZ3Expr &z3Expr) : Z3Expr(z3Expr) {}
 
     inline BoundedZ3Expr &operator=(const BoundedZ3Expr &rhs)

svf/include/AE/Core/IntervalValue.h

@@ -101,7 +101,7 @@ class IntervalValue final : public AbstractValue
 
     explicit IntervalValue(u32_t n) : IntervalValue((s64_t) n) {}
 
-    explicit IntervalValue(double n) : IntervalValue((s64_t) n) {}
+    explicit IntervalValue(double n) : AbstractValue(AbstractValue::IntervalK), _lb(n), _ub(n) {}
 
     explicit IntervalValue(NumericLiteral n) : IntervalValue(n, n) {}
 

svf/include/AE/Core/NumericLiteral.h

@@ -134,6 +134,12 @@ class NumericLiteral
         return _n.getNumeral();
     }
 
+    /// Return Expr
+    inline Z3Expr getExpr() const
+    {
+        return _n.getExpr();
+    }
+
     inline double getRealNumeral() const
     {
         return _n.getRealNumeral();

svf/include/AE/Core/RelationSolver.h

@@ -54,7 +54,7 @@ class RelationSolver
 
     IntervalESBase abstract_consequence(const IntervalESBase &lower, const IntervalESBase &upper, const IntervalESBase &domain) const;
 
-    IntervalESBase beta(const Map<u32_t, double> &sigma, const IntervalESBase &exeState) const;
+    IntervalESBase beta(const Map<u32_t, s32_t> &sigma, const IntervalESBase &exeState) const;
 
 
     /// Return Z3 expression lazily based on SVFVar ID

svf/include/Util/Options.h

@@ -274,6 +274,9 @@ class Options
     static const Option<bool> RunUncallFuncs;
 
     static const Option<bool> ICFGMergeAdjacentNodes;
+
+    // float precision for symbolic abstraction
+    static const Option<u32_t> AEPrecision;
 };
 }  // namespace SVF
 

svf/include/Util/Z3Expr.h

@@ -44,8 +44,7 @@ class Z3Expr
 private:
     z3::expr e;
 
-    Z3Expr(float f); // placeholder don't support floating point expression
-    Z3Expr(double f); // placeholder don't support floating point expression
+
 
 public:
 
@@ -65,6 +64,14 @@ class Z3Expr
     {
     }
 
+    Z3Expr(float f) : Z3Expr((double) f)
+    {
+    }
+
+    Z3Expr(double f): e(getContext().real_val(std::to_string(f).c_str()))
+    {
+    }
+
     virtual ~Z3Expr() = default;
 
     inline Z3Expr &operator=(const Z3Expr &rhs)

svf/lib/AE/Core/RelationSolver.cpp

@@ -27,6 +27,9 @@
  *
  */
 #include "AE/Core/RelationSolver.h"
+#include <cmath>
+#include "Util/Options.h"
+
 using namespace SVF;
 using namespace SVFUtil;
 
@@ -59,7 +62,7 @@ IntervalESBase RelationSolver::bilateral(const IntervalESBase &domain, const Z3E
         Z3Expr rhs = !(gamma_hat(consequence, domain));
         solver.push();
         solver.add(phi.getExpr() && rhs.getExpr());
-        Map<u32_t, double> solution;
+        Map<u32_t, s32_t> solution;
         z3::check_result checkRes = solver.check();
         /// find any solution, which is sat
         if (checkRes == z3::sat)
@@ -121,7 +124,7 @@ IntervalESBase RelationSolver::RSY(const IntervalESBase& domain, const Z3Expr& p
         Z3Expr rhs = !(gamma_hat(lower, domain));
         solver.push();
         solver.add(phi.getExpr() && rhs.getExpr());
-        Map<u32_t, double> solution;
+        Map<u32_t, s32_t> solution;
         z3::check_result checkRes = solver.check();
         /// find any solution, which is sat
         if (checkRes == z3::sat)
@@ -238,7 +241,7 @@ Z3Expr RelationSolver::gamma_hat(u32_t id, const IntervalESBase& exeState) const
     return res;
 }
 
-IntervalESBase RelationSolver::beta(const Map<u32_t, double>& sigma,
+IntervalESBase RelationSolver::beta(const Map<u32_t, s32_t>& sigma,
                                     const IntervalESBase& exeState) const
 {
     IntervalESBase res;
@@ -268,7 +271,9 @@ IntervalESBase RelationSolver::BS(const IntervalESBase& domain, const Z3Expr &ph
     /// because key of _varToItvVal is u32_t, -key may out of range for int
     /// so we do key + bias for -key
     u32_t bias = 0;
-    int infinity = (INT32_MAX) - 1;
+    s32_t infinity = INT32_MAX - 1;
+
+    // int infinity = (INT32_MAX) - 1;
     // int infinity = 20;
     Map<u32_t, NumericLiteral> ret;
     Map<u32_t, NumericLiteral> low_values, high_values;
@@ -343,7 +348,7 @@ Map<u32_t, NumericLiteral> RelationSolver::BoxedOptSolver(const Z3Expr& phi, Map
             {
                 NumericLiteral mid = (low_values.at(item.first) + (high_values.at(item.first) - low_values.at(item.first)) / 2);
                 updateMap(mid_values, item.first, mid);
-                Z3Expr expr = ((int)mid.getNumeral() <= v && v <= (int)high_values.at(item.first).getNumeral());
+                Z3Expr expr = (mid.getExpr() <= v && v <= high_values.at(item.first).getExpr());
                 L_phi[item.first] = expr;
             }
         }
@@ -399,7 +404,7 @@ void RelationSolver::decide_cpa_ext(const Z3Expr& phi,
                     updateMap(mid_values, id, mid);
                     Z3Expr v = toZ3Expr(id);
                     // Z3Expr v = Z3Expr::getContext().int_const(std::to_string(id).c_str());
-                    Z3Expr expr = ((int)mid_values.at(id).getNumeral() <= v && v <= (int)high_values.at(id).getNumeral());
+                    Z3Expr expr = (mid_values.at(id).getExpr() <= v && v <= high_values.at(id).getExpr());
                     L_phi[id] = expr;
                 }
                 solver.pop();

svf/lib/Util/Options.cpp

@@ -853,4 +853,12 @@ const Option<bool> Options::RunUncallFuncs(
     "run-uncall-fun","Skip Gep Unknown Index",false);
 const Option<bool> Options::ICFGMergeAdjacentNodes(
     "icfg-merge-adjnodes","ICFG Simplification - Merge Adjacent Nodes in the Same Basic Block.",false);
+
+
+const Option<u32_t> Options::AEPrecision(
+    "precision",
+    "symbolic abstraction precision for float",
+    0
+);
+
 } // namespace SVF.