34 using namespace SVFUtil;
42 u32_t meets_in_a_row = 0;
46 p.set(
":timeout",
static_cast<unsigned>(600));
51 while (lower != upper)
53 if (meets_in_a_row == descend_check)
59 consequence = abstract_consequence(lower, upper, domain);
62 Z3Expr rhs = !(gamma_hat(consequence, domain));
66 z3::check_result checkRes = solver.check();
68 if (checkRes == z3::sat)
70 z3::model m = solver.get_model();
71 for (
u32_t i = 0; i < m.size(); i++)
73 z3::func_decl v = m[i];
77 solution.emplace(std::stoi(v.name().str()),
78 m.get_const_interp(v).get_numeral_int());
82 if (solution.find(
item.first) == solution.end())
84 solution.emplace(
item.first, 0);
98 if (checkRes == z3::unknown)
101 if (solver.reason_unknown() ==
"timeout")
120 p.set(
":timeout",
static_cast<unsigned>(600));
124 Z3Expr rhs = !(gamma_hat(lower, domain));
128 z3::check_result checkRes = solver.check();
130 if (checkRes == z3::sat)
132 z3::model m = solver.get_model();
133 for (
u32_t i = 0; i < m.size(); i++)
135 z3::func_decl v = m[i];
139 solution.emplace(std::stoi(v.name().str()),
140 m.get_const_interp(v).get_numeral_int());
144 if (solution.find(
item.first) == solution.end())
146 solution.emplace(
item.first, 0);
152 newLower.
joinWith(beta(solution, domain));
158 if (checkRes == z3::unknown)
161 if (solver.reason_unknown() ==
"timeout")
188 proposed[it->first] = lower[it->first].getInterval();
191 if (!(proposed >= upper))
207 if (interval.
isTop())
225 if (interval.
isTop())
237 assert(it != exeState.
getVarToVal().end() &&
"id not in varToVal?");
238 Z3Expr v = toIntZ3Expr(
id);
240 Z3Expr res = (v >= (int)it->second.getInterval().lb().getNumeral() &&
241 v <= (int)it->second.getInterval().ub().getNumeral());
252 sigma.at(
item.first), sigma.at(
item.first));
259 auto it = map.find(key);
262 map.emplace(key, value);
275 s32_t infinity = INT32_MAX/2 - 1;
288 updateMap(low_values,
item.first, -infinity);
292 updateMap(high_values,
item.first, infinity);
295 if (
item.first > bias)
296 bias =
item.first + 1;
305 updateMap(low_values, reverse_key, -infinity);
309 updateMap(high_values, reverse_key, infinity);
313 new_phi = (new_phi && (toIntZ3Expr(reverse_key) == -1 * toIntZ3Expr(
item.first)));
316 BoxedOptSolver(new_phi.
simplify(), ret, low_values, high_values);
319 for (
const auto&
item: ret)
321 if (
item.first >= bias)
326 if (
item.second == (infinity))
328 retInv[
item.first - bias].getInterval().ub());
335 if (
item.second == (infinity))
353 for (
const auto&
item : ret)
356 if (low_values.at(
item.first) <= (high_values.at(
item.first)))
358 s32_t mid = (low_values.at(
item.first) + (high_values.at(
item.first) - low_values.at(
item.first)) / 2);
359 updateMap(mid_values,
item.first, mid);
360 Z3Expr expr = (toIntVal(mid) <= v && v <= toIntVal(high_values.at(
item.first)));
361 L_phi[
item.first] = expr;
367 decide_cpa_ext(phi, L_phi, mid_values, ret, low_values, high_values);
383 for (
const auto&
item : L_phi)
384 join_expr = (join_expr ||
item.second);
385 join_expr = (join_expr && phi).simplify();
388 solver.add(join_expr.
getExpr());
390 z3::check_result checkRes = solver.check();
392 if (checkRes == z3::sat)
394 z3::model m = solver.get_model();
396 for(
const auto &
item : L_phi)
399 int value = m.eval(toIntZ3Expr(
id).getExpr()).get_numeral_int();
403 Z3Expr expr = (
item.second && toIntZ3Expr(
id) == value);
407 if (solver.check() == z3::sat)
409 updateMap(ret,
id, (value));
410 updateMap(low_values,
id, ret.at(
id) + 1);
412 s32_t mid = (low_values.at(
id) + high_values.at(
id) + 1) / 2;
413 updateMap(mid_values,
id, mid);
414 Z3Expr v = toIntZ3Expr(
id);
416 Z3Expr expr = (toIntVal(mid_values.at(
id)) <= v && v <= toIntVal(high_values.at(
id)));
425 for (
const auto&
item : L_phi)
426 high_values.at(
item.first) = mid_values.at(
item.first) - 1;
AbstractState bottom() const
Set all value bottom.
void joinWith(const AbstractState &other)
domain join with other, important! other widen this.
const VarToAbsValMap & getVarToVal() const
get var2val map
virtual bool inVarToValTable(u32_t id) const
whether the variable is in varToVal table
AbstractState top() const
Set all value top.
void meetWith(const AbstractState &other)
domain meet with other, important! other widen this.
static BoundedInt plus_infinity()
bool is_minus_infinity() const
s64_t getNumeral() const
Retrieves the numeral value of the BoundedInt object.
bool is_plus_infinity() const
s64_t getIntNumeral() const
static BoundedInt minus_infinity()
const BoundedInt & lb() const
Return the lower bound.
const BoundedInt & ub() const
Return the upper bound.
static IntervalValue top()
Create the IntervalValue [-inf, +inf].
Z3Expr gamma_hat(const AbstractState &exeState) const
Return Z3Expr according to valToValMap.
AbstractState RSY(const AbstractState &domain, const Z3Expr &phi)
AbstractState bilateral(const AbstractState &domain, const Z3Expr &phi, u32_t descend_check=0)
Map< u32_t, s32_t > BoxedOptSolver(const Z3Expr &phi, Map< u32_t, s32_t > &ret, Map< u32_t, s32_t > &low_values, Map< u32_t, s32_t > &high_values)
AbstractState beta(const Map< u32_t, s32_t > &sigma, const AbstractState &exeState) const
void updateMap(Map< u32_t, s32_t > &map, u32_t key, const s32_t &value)
AbstractState abstract_consequence(const AbstractState &lower, const AbstractState &upper, const AbstractState &domain) const
void decide_cpa_ext(const Z3Expr &phi, Map< u32_t, Z3Expr > &, Map< u32_t, s32_t > &, Map< u32_t, s32_t > &, Map< u32_t, s32_t > &, Map< u32_t, s32_t > &)
AbstractState BS(const AbstractState &domain, const Z3Expr &phi)
static z3::solver & getSolver()
Get z3 solver, singleton design here to make sure we only have one context.
const z3::expr & getExpr() const
static z3::context & getContext()
Get z3 context, singleton design here to make sure we only have one context.
std::unordered_map< Key, Value, Hash, KeyEqual, Allocator > Map