Static Value-Flow Analysis
Loading...
Searching...
No Matches
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
u32_t hash () const
 get hash id
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.
static z3::context & getContext ()
 Get z3 context, singleton design here to make sure we only have one context.
static void releaseContext ()
 release z3 context
static void releaseSolver ()
 release z3 solver
static z3::expr nullExpr ()
 null expression
static std::string dumpStr (const Z3Expr &z3Expr)
 output Z3 expression as a string
static u32_t getExprSize (const Z3Expr &z3Expr)
 get the number of subexpression of a Z3 expression
static Z3Expr getTrueCond ()
 Return the unique true condition.
static Z3Expr getFalseCond ()
 Return the unique false condition.
static Z3Expr NEG (const Z3Expr &z3Expr)
 compute NEG
static Z3Expr AND (const Z3Expr &lhs, const Z3Expr &rhs)
 compute AND, used for branch condition
static Z3Expr OR (const Z3Expr &lhs, const Z3Expr &rhs)
 compute OR, used for branch condition

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 }

◆ 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:185
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}
SVF::u32_t
unsigned u32_t
Definition GeneralType.h:67

◆ getFalseCond()

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()

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 ( ) 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()

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()

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 }

◆ 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.15.0