Static Value-Flow Analysis
Public Member Functions | Static Public Member Functions | Static Public Attributes | Private Attributes | Friends | List of all members
SVF::Z3Expr Class Reference

#include <Z3Expr.h>

Public Member Functions

 Z3Expr ()
 
 Z3Expr (const z3::expr &_e)
 
 Z3Expr (int i)
 
 Z3Expr (const Z3Expr &z3Expr)
 
 Z3Expr (float f)
 
 Z3Expr (double f)
 
virtual ~Z3Expr ()=default
 
Z3Expr & operator= (const Z3Expr &rhs)
 
const z3::expr & getExpr () const
 
u32_t id () const
 get id More...
 
u32_t hash () const
 get hash id More...
 
const std::string to_string () const
 
bool is_numeral () const
 
bool is_bool () const
 
Z3Expr simplify () const
 
int64_t get_numeral_int64 () const
 
int get_numeral_int () const
 
z3::sort get_sort () const
 

Static Public Member Functions

static z3::solver & getSolver ()
 Get z3 solver, singleton design here to make sure we only have one context. More...
 
static z3::context & getContext ()
 Get z3 context, singleton design here to make sure we only have one context. More...
 
static void releaseContext ()
 release z3 context More...
 
static void releaseSolver ()
 release z3 solver More...
 
static z3::expr nullExpr ()
 null expression More...
 
static std::string dumpStr (const Z3Expr &z3Expr)
 output Z3 expression as a string More...
 
static u32_t getExprSize (const Z3Expr &z3Expr)
 get the number of subexpression of a Z3 expression More...
 
static Z3Expr getTrueCond ()
 Return the unique true condition. More...
 
static Z3Expr getFalseCond ()
 Return the unique false condition. More...
 
static Z3Expr NEG (const Z3Expr &z3Expr)
 compute NEG More...
 
static Z3Expr AND (const Z3Expr &lhs, const Z3Expr &rhs)
 compute AND, used for branch condition More...
 
static Z3Expr OR (const Z3Expr &lhs, const Z3Expr &rhs)
 compute OR, used for branch condition More...
 

Static Public Attributes

static z3::context * ctx = nullptr
 
static z3::solver * solver = nullptr
 

Private Attributes

z3::expr e
 

Friends

Z3Expr operator== (const Z3Expr &lhs, const Z3Expr &rhs)
 
Z3Expr operator!= (const Z3Expr &lhs, const Z3Expr &rhs)
 
Z3Expr operator> (const Z3Expr &lhs, const Z3Expr &rhs)
 
Z3Expr operator< (const Z3Expr &lhs, const Z3Expr &rhs)
 
Z3Expr operator<= (const Z3Expr &lhs, const Z3Expr &rhs)
 
Z3Expr operator>= (const Z3Expr &lhs, const Z3Expr &rhs)
 
Z3Expr operator+ (const Z3Expr &lhs, const Z3Expr &rhs)
 
Z3Expr operator- (const Z3Expr &lhs, const Z3Expr &rhs)
 
Z3Expr operator* (const Z3Expr &lhs, const Z3Expr &rhs)
 
Z3Expr operator/ (const Z3Expr &lhs, const Z3Expr &rhs)
 
Z3Expr operator% (const Z3Expr &lhs, const Z3Expr &rhs)
 
Z3Expr operator^ (const Z3Expr &lhs, const Z3Expr &rhs)
 
Z3Expr operator& (const Z3Expr &lhs, const Z3Expr &rhs)
 
Z3Expr operator| (const Z3Expr &lhs, const Z3Expr &rhs)
 
Z3Expr ashr (const Z3Expr &lhs, const Z3Expr &rhs)
 
Z3Expr shl (const Z3Expr &lhs, const Z3Expr &rhs)
 
Z3Expr int2bv (u32_t n, const Z3Expr &e)
 
Z3Expr bv2int (const Z3Expr &e, bool isSigned)
 
Z3Expr operator&& (const Z3Expr &lhs, const Z3Expr &rhs)
 
Z3Expr operator|| (const Z3Expr &lhs, const Z3Expr &rhs)
 
Z3Expr operator! (const Z3Expr &lhs)
 
Z3Expr ite (const Z3Expr &cond, const Z3Expr &lhs, const Z3Expr &rhs)
 
std::ostream & operator<< (std::ostream &out, const Z3Expr &expr)
 
bool eq (const Z3Expr &lhs, const Z3Expr &rhs)
 

Detailed Description

Definition at line 38 of file Z3Expr.h.

Constructor & Destructor Documentation

◆ Z3Expr() [1/6]

SVF::Z3Expr::Z3Expr ( )
inline

Definition at line 51 of file Z3Expr.h.

51  : e(nullExpr())
52  {
53  }
SVF::Z3Expr::nullExpr
static z3::expr nullExpr()
null expression
Definition: Z3Expr.h:105
SVF::Z3Expr::e
z3::expr e
Definition: Z3Expr.h:45

◆ Z3Expr() [2/6]

SVF::Z3Expr::Z3Expr ( const z3::expr &  _e)
inline

Definition at line 55 of file Z3Expr.h.

55  : e(_e)
56  {
57  }

◆ Z3Expr() [3/6]

SVF::Z3Expr::Z3Expr ( int  i)
inline

Definition at line 59 of file Z3Expr.h.

59  : e(getContext().int_val(i))
60  {
61  }
SVF::Z3Expr::getContext
static z3::context & getContext()
Get z3 context, singleton design here to make sure we only have one context.
Definition: Z3Expr.cpp:66

◆ Z3Expr() [4/6]

SVF::Z3Expr::Z3Expr ( const Z3Expr &  z3Expr)
inline

Definition at line 63 of file Z3Expr.h.

63  : e(z3Expr.getExpr())
64  {
65  }

◆ Z3Expr() [5/6]

SVF::Z3Expr::Z3Expr ( float  f)
inline

Definition at line 67 of file Z3Expr.h.

67  : Z3Expr((double) f)
68  {
69  }
SVF::Z3Expr::Z3Expr
Z3Expr()
Definition: Z3Expr.h:51

◆ Z3Expr() [6/6]

SVF::Z3Expr::Z3Expr ( double  f)
inline

Definition at line 71 of file Z3Expr.h.

71  : e(getContext().real_val(std::to_string(f).c_str()))
72  {
73  }

◆ ~Z3Expr()

virtual SVF::Z3Expr::~Z3Expr ( )
virtualdefault

Member Function Documentation

◆ AND()

Z3Expr SVF::Z3Expr::AND ( const Z3Expr &  lhs,
const Z3Expr &  rhs 
)
static

compute AND, used for branch condition

Definition at line 92 of file Z3Expr.cpp.

93 {
94  if (eq(lhs, Z3Expr::getFalseCond()) || eq(rhs, Z3Expr::getFalseCond()))
95  {
96  return Z3Expr::getFalseCond();
97  }
98  else if (eq(lhs, Z3Expr::getTrueCond()))
99  {
100  return rhs;
101  }
102  else if (eq(rhs, Z3Expr::getTrueCond()))
103  {
104  return lhs;
105  }
106  else
107  {
108  Z3Expr expr = (lhs && rhs).simplify();
109  // check subexpression size and option limit
110  if (Z3Expr::getExprSize(expr) > Options::MaxZ3Size())
111  {
112  getSolver().push();
113  getSolver().add(expr.getExpr());
114  z3::check_result res = getSolver().check();
115  getSolver().pop();
116  if (res != z3::unsat)
117  {
118  return lhs;
119  }
120  else
121  {
122  return Z3Expr::getFalseCond();
123  }
124  }
125  return expr;
126  }
127 }
SVF::Options::MaxZ3Size
static const Option< u32_t > MaxZ3Size
Definition: Options.h:193
SVF::Z3Expr::getSolver
static z3::solver & getSolver()
Get z3 solver, singleton design here to make sure we only have one context.
Definition: Z3Expr.cpp:56
SVF::Z3Expr::getExprSize
static u32_t getExprSize(const Z3Expr &z3Expr)
get the number of subexpression of a Z3 expression
Definition: Z3Expr.cpp:76
SVF::Z3Expr::getTrueCond
static Z3Expr getTrueCond()
Return the unique true condition.
Definition: Z3Expr.h:288
SVF::Z3Expr::eq
friend bool eq(const Z3Expr &lhs, const Z3Expr &rhs)
Definition: Z3Expr.h:269
SVF::Z3Expr::getFalseCond
static Z3Expr getFalseCond()
Return the unique false condition.
Definition: Z3Expr.h:295
SVF::Z3Expr::simplify
Z3Expr simplify() const
Definition: Z3Expr.h:137

◆ dumpStr()

std::string SVF::Z3Expr::dumpStr ( const Z3Expr &  z3Expr)
static

output Z3 expression as a string

Definition at line 168 of file Z3Expr.cpp.

169 {
170  std::ostringstream out;
171  out << z3Expr.getExpr();
172  return out.str();
173 }

◆ get_numeral_int()

int SVF::Z3Expr::get_numeral_int ( ) const
inline

Definition at line 147 of file Z3Expr.h.

148  {
149  return e.get_numeral_int();
150  }

◆ get_numeral_int64()

int64_t SVF::Z3Expr::get_numeral_int64 ( ) const
inline

Definition at line 142 of file Z3Expr.h.

143  {
144  return e.get_numeral_int64();
145  }

◆ get_sort()

z3::sort SVF::Z3Expr::get_sort ( ) const
inline

Definition at line 274 of file Z3Expr.h.

275  {
276  return getExpr().get_sort();
277  }
SVF::Z3Expr::getExpr
const z3::expr & getExpr() const
Definition: Z3Expr.h:86

◆ getContext()

z3::context & SVF::Z3Expr::getContext ( )
static

Get z3 context, singleton design here to make sure we only have one context.

Definition at line 66 of file Z3Expr.cpp.

67 {
68  if (ctx == nullptr)
69  {
70  ctx = new z3::context();
71  }
72  return *ctx;
73 }
SVF::Z3Expr::ctx
static z3::context * ctx
Definition: Z3Expr.h:41

◆ getExpr()

const z3::expr& SVF::Z3Expr::getExpr ( ) const
inline

Definition at line 86 of file Z3Expr.h.

87  {
88  return e;
89  }

◆ getExprSize()

u32_t SVF::Z3Expr::getExprSize ( const Z3Expr &  z3Expr)
static

get the number of subexpression of a Z3 expression

Definition at line 76 of file Z3Expr.cpp.

77 {
78  u32_t res = 1;
79  if (z3Expr.getExpr().num_args() == 0)
80  {
81  return 1;
82  }
83  for (u32_t i = 0; i < z3Expr.getExpr().num_args(); ++i)
84  {
85  Z3Expr expr = z3Expr.getExpr().arg(i);
86  res += getExprSize(expr);
87  }
88  return res;
89 }
u32_t
unsigned u32_t
Definition: CommandLine.h:18

◆ getFalseCond()

static Z3Expr SVF::Z3Expr::getFalseCond ( )
inlinestatic

Return the unique false condition.

Definition at line 295 of file Z3Expr.h.

296  {
297  return getContext().bool_val(false);
298  }

◆ getSolver()

z3::solver & SVF::Z3Expr::getSolver ( )
static

Get z3 solver, singleton design here to make sure we only have one context.

Definition at line 56 of file Z3Expr.cpp.

57 {
58  if (solver == nullptr)
59  {
60  solver = new z3::solver(getContext());
61  }
62  return *solver;
63 }
SVF::Z3Expr::solver
static z3::solver * solver
Definition: Z3Expr.h:42

◆ getTrueCond()

static Z3Expr SVF::Z3Expr::getTrueCond ( )
inlinestatic

Return the unique true condition.

Definition at line 288 of file Z3Expr.h.

289  {
290  return getContext().bool_val(true);
291  }

◆ hash()

u32_t SVF::Z3Expr::hash ( void  ) const
inline

get hash id

Definition at line 117 of file Z3Expr.h.

118  {
119  return e.hash();
120  }

◆ id()

u32_t SVF::Z3Expr::id ( ) const
inline

get id

Definition at line 111 of file Z3Expr.h.

112  {
113  return e.id();
114  }

◆ is_bool()

bool SVF::Z3Expr::is_bool ( ) const
inline

Definition at line 132 of file Z3Expr.h.

133  {
134  return e.is_bool();
135  }

◆ is_numeral()

bool SVF::Z3Expr::is_numeral ( ) const
inline

Definition at line 127 of file Z3Expr.h.

128  {
129  return e.is_numeral();
130  }

◆ NEG()

static Z3Expr SVF::Z3Expr::NEG ( const Z3Expr &  z3Expr)
inlinestatic

compute NEG

Definition at line 301 of file Z3Expr.h.

302  {
303  return (!z3Expr).simplify();
304  }

◆ nullExpr()

static z3::expr SVF::Z3Expr::nullExpr ( )
inlinestatic

null expression

Definition at line 105 of file Z3Expr.h.

106  {
107  return getContext().int_const("null");
108  }

◆ operator=()

Z3Expr& SVF::Z3Expr::operator= ( const Z3Expr &  rhs)
inline

Definition at line 77 of file Z3Expr.h.

78  {
79  if (this->id() != rhs.id())
80  {
81  e = rhs.getExpr();
82  }
83  return *this;
84  }

◆ OR()

Z3Expr SVF::Z3Expr::OR ( const Z3Expr &  lhs,
const Z3Expr &  rhs 
)
static

compute OR, used for branch condition

Definition at line 130 of file Z3Expr.cpp.

131 {
132  if (eq(lhs, Z3Expr::getTrueCond()) || eq(rhs, Z3Expr::getTrueCond()))
133  {
134  return Z3Expr::getTrueCond();
135  }
136  else if (eq(lhs, Z3Expr::getFalseCond()))
137  {
138  return rhs;
139  }
140  else if (eq(rhs, Z3Expr::getFalseCond()))
141  {
142  return lhs;
143  }
144  else
145  {
146  Z3Expr expr = (lhs || rhs).simplify();
147  // check subexpression size and option limit
148  if (Z3Expr::getExprSize(expr) > Options::MaxZ3Size())
149  {
150  getSolver().push();
151  getSolver().add(expr.getExpr());
152  z3::check_result res = getSolver().check();
153  getSolver().pop();
154  if (res != z3::unsat)
155  {
156  return Z3Expr::getTrueCond();
157  }
158  else
159  {
160  return Z3Expr::getFalseCond();
161  }
162  }
163  return expr;
164  }
165 }

◆ releaseContext()

void SVF::Z3Expr::releaseContext ( )
static

release z3 context

Definition at line 40 of file Z3Expr.cpp.

41 {
42  if(solver)
43  releaseSolver();
44  delete ctx;
45  ctx = nullptr;
46 }
SVF::Z3Expr::releaseSolver
static void releaseSolver()
release z3 solver
Definition: Z3Expr.cpp:49

◆ releaseSolver()

void SVF::Z3Expr::releaseSolver ( )
static

release z3 solver

Definition at line 49 of file Z3Expr.cpp.

50 {
51  delete solver;
52  solver = nullptr;
53 }

◆ simplify()

Z3Expr SVF::Z3Expr::simplify ( ) const
inline

Definition at line 137 of file Z3Expr.h.

138  {
139  return e.simplify();
140  }

◆ to_string()

const std::string SVF::Z3Expr::to_string ( ) const
inline

Definition at line 122 of file Z3Expr.h.

123  {
124  return e.to_string();
125  }

Friends And Related Function Documentation

◆ ashr

Z3Expr ashr ( const Z3Expr &  lhs,
const Z3Expr &  rhs 
)
friend

Definition at line 223 of file Z3Expr.h.

224  {
225  return ashr(lhs.getExpr(), rhs.getExpr());
226  }
SVF::Z3Expr::ashr
friend Z3Expr ashr(const Z3Expr &lhs, const Z3Expr &rhs)
Definition: Z3Expr.h:223

◆ bv2int

Z3Expr bv2int ( const Z3Expr &  e,
bool  isSigned 
)
friend

Definition at line 238 of file Z3Expr.h.

239  {
240  return z3::bv2int(e.getExpr(), isSigned);
241  }

◆ eq

bool eq ( const Z3Expr &  lhs,
const Z3Expr &  rhs 
)
friend

Definition at line 269 of file Z3Expr.h.

270  {
271  return eq(lhs.getExpr().simplify(), rhs.getExpr().simplify());
272  }

◆ int2bv

Z3Expr int2bv ( u32_t  n,
const Z3Expr &  e 
)
friend

Definition at line 233 of file Z3Expr.h.

234  {
235  return int2bv(n, e.getExpr());
236  }
n
cJSON * n
Definition: cJSON.cpp:2558
SVF::Z3Expr::int2bv
friend Z3Expr int2bv(u32_t n, const Z3Expr &e)
Definition: Z3Expr.h:233

◆ ite

Z3Expr ite ( const Z3Expr &  cond,
const Z3Expr &  lhs,
const Z3Expr &  rhs 
)
friend

Definition at line 258 of file Z3Expr.h.

259  {
260  return ite(cond.getExpr(), lhs.getExpr(), rhs.getExpr());
261  }
SVF::Z3Expr::ite
friend Z3Expr ite(const Z3Expr &cond, const Z3Expr &lhs, const Z3Expr &rhs)
Definition: Z3Expr.h:258

◆ operator!

Z3Expr operator! ( const Z3Expr &  lhs)
friend

Definition at line 253 of file Z3Expr.h.

254  {
255  return !lhs.getExpr();
256  }

◆ operator!=

Z3Expr operator!= ( const Z3Expr &  lhs,
const Z3Expr &  rhs 
)
friend

Definition at line 158 of file Z3Expr.h.

159  {
160  return lhs.getExpr() != rhs.getExpr();
161  }

◆ operator%

Z3Expr operator% ( const Z3Expr &  lhs,
const Z3Expr &  rhs 
)
friend

Definition at line 203 of file Z3Expr.h.

204  {
205  return lhs.getExpr() % rhs.getExpr();
206  }

◆ operator&

Z3Expr operator& ( const Z3Expr &  lhs,
const Z3Expr &  rhs 
)
friend

Definition at line 213 of file Z3Expr.h.

214  {
215  return lhs.getExpr() & rhs.getExpr();
216  }

◆ operator&&

Z3Expr operator&& ( const Z3Expr &  lhs,
const Z3Expr &  rhs 
)
friend

Definition at line 243 of file Z3Expr.h.

244  {
245  return lhs.getExpr() && rhs.getExpr();
246  }

◆ operator*

Z3Expr operator* ( const Z3Expr &  lhs,
const Z3Expr &  rhs 
)
friend

Definition at line 193 of file Z3Expr.h.

194  {
195  return lhs.getExpr() * rhs.getExpr();
196  }

◆ operator+

Z3Expr operator+ ( const Z3Expr &  lhs,
const Z3Expr &  rhs 
)
friend

Definition at line 183 of file Z3Expr.h.

184  {
185  return lhs.getExpr() + rhs.getExpr();
186  }

◆ operator-

Z3Expr operator- ( const Z3Expr &  lhs,
const Z3Expr &  rhs 
)
friend

Definition at line 188 of file Z3Expr.h.

189  {
190  return lhs.getExpr() - rhs.getExpr();
191  }

◆ operator/

Z3Expr operator/ ( const Z3Expr &  lhs,
const Z3Expr &  rhs 
)
friend

Definition at line 198 of file Z3Expr.h.

199  {
200  return lhs.getExpr() / rhs.getExpr();
201  }

◆ operator<

Z3Expr operator< ( const Z3Expr &  lhs,
const Z3Expr &  rhs 
)
friend

Definition at line 168 of file Z3Expr.h.

169  {
170  return lhs.getExpr() < rhs.getExpr();
171  }

◆ operator<<

std::ostream& operator<< ( std::ostream &  out,
const Z3Expr &  expr 
)
friend

Definition at line 263 of file Z3Expr.h.

264  {
265  out << expr.getExpr();
266  return out;
267  }

◆ operator<=

Z3Expr operator<= ( const Z3Expr &  lhs,
const Z3Expr &  rhs 
)
friend

Definition at line 173 of file Z3Expr.h.

174  {
175  return lhs.getExpr() <= rhs.getExpr();
176  }

◆ operator==

Z3Expr operator== ( const Z3Expr &  lhs,
const Z3Expr &  rhs 
)
friend

Definition at line 153 of file Z3Expr.h.

154  {
155  return lhs.getExpr() == rhs.getExpr();
156  }

◆ operator>

Z3Expr operator> ( const Z3Expr &  lhs,
const Z3Expr &  rhs 
)
friend

Definition at line 163 of file Z3Expr.h.

164  {
165  return lhs.getExpr() > rhs.getExpr();
166  }

◆ operator>=

Z3Expr operator>= ( const Z3Expr &  lhs,
const Z3Expr &  rhs 
)
friend

Definition at line 178 of file Z3Expr.h.

179  {
180  return lhs.getExpr() >= rhs.getExpr();
181  }

◆ operator^

Z3Expr operator^ ( const Z3Expr &  lhs,
const Z3Expr &  rhs 
)
friend

Definition at line 208 of file Z3Expr.h.

209  {
210  return lhs.getExpr() ^ rhs.getExpr();
211  }

◆ operator|

Z3Expr operator| ( const Z3Expr &  lhs,
const Z3Expr &  rhs 
)
friend

Definition at line 218 of file Z3Expr.h.

219  {
220  return lhs.getExpr() | rhs.getExpr();
221  }

◆ operator||

Z3Expr operator|| ( const Z3Expr &  lhs,
const Z3Expr &  rhs 
)
friend

Definition at line 248 of file Z3Expr.h.

249  {
250  return lhs.getExpr() || rhs.getExpr();
251  }

◆ shl

Z3Expr shl ( const Z3Expr &  lhs,
const Z3Expr &  rhs 
)
friend

Definition at line 228 of file Z3Expr.h.

229  {
230  return shl(lhs.getExpr(), rhs.getExpr());
231  }
SVF::Z3Expr::shl
friend Z3Expr shl(const Z3Expr &lhs, const Z3Expr &rhs)
Definition: Z3Expr.h:228

Member Data Documentation

◆ ctx

z3::context * SVF::Z3Expr::ctx = nullptr
static

Definition at line 41 of file Z3Expr.h.

◆ e

z3::expr SVF::Z3Expr::e
private

Definition at line 45 of file Z3Expr.h.

◆ solver

z3::solver * SVF::Z3Expr::solver = nullptr
static

Definition at line 42 of file Z3Expr.h.

The documentation for this class was generated from the following files:
Generated by doxygen 1.9.1