Skip to content

Commit ca6983b

Browse files
mikhailramalhomikhailramalho
committedJul 25, 2018
[analyzer] Create generic SMT Expr class
Summary: New base class for all future SMT Exprs. No major changes except moving `areEquivalent` and `getFloatSemantics` outside of `Z3Expr` to keep the class minimal. Reviewers: NoQ, george.karpenkov Reviewed By: george.karpenkov Subscribers: xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D49551 llvm-svn: 337917
·
llvmorg-21-initllvmorg-7.0.0-rc1
1 parent cb9e68d commit ca6983b

File tree

2 files changed

+101
-53
lines changed

2 files changed

+101
-53
lines changed
 

Diff for: ‎clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h

+57
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
//== SMTExpr.h --------------------------------------------------*- C++ -*--==//
2+
//
3+
// The LLVM Compiler Infrastructure
4+
//
5+
// This file is distributed under the University of Illinois Open Source
6+
// License. See LICENSE.TXT for details.
7+
//
8+
//===----------------------------------------------------------------------===//
9+
//
10+
// This file defines a SMT generic Expr API, which will be the base class
11+
// for every SMT solver expr specific class.
12+
//
13+
//===----------------------------------------------------------------------===//
14+
15+
#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTEXPR_H
16+
#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTEXPR_H
17+
18+
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
19+
20+
namespace clang {
21+
namespace ento {
22+
23+
class SMTExpr {
24+
public:
25+
SMTExpr() = default;
26+
virtual ~SMTExpr() = default;
27+
28+
bool operator<(const SMTExpr &Other) const {
29+
llvm::FoldingSetNodeID ID1, ID2;
30+
Profile(ID1);
31+
Other.Profile(ID2);
32+
return ID1 < ID2;
33+
}
34+
35+
virtual void Profile(llvm::FoldingSetNodeID &ID) const {
36+
static int Tag = 0;
37+
ID.AddPointer(&Tag);
38+
}
39+
40+
friend bool operator==(SMTExpr const &LHS, SMTExpr const &RHS) {
41+
return LHS.equal_to(RHS);
42+
}
43+
44+
virtual void print(raw_ostream &OS) const = 0;
45+
46+
LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
47+
48+
protected:
49+
virtual bool equal_to(SMTExpr const &other) const = 0;
50+
};
51+
52+
using SMTExprRef = std::shared_ptr<SMTExpr>;
53+
54+
} // namespace ento
55+
} // namespace clang
56+
57+
#endif

Diff for: ‎clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

+44-53
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@
1212
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
1313
#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
1414
#include "clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h"
15+
#include "clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h"
1516
#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h"
1617

1718
#include "clang/Config/config.h"
@@ -162,40 +163,25 @@ class Z3Sort : public SMTSort {
162163
}
163164
}; // end class Z3Sort
164165

165-
class Z3Expr {
166-
friend class Z3Model;
166+
class Z3Expr : public SMTExpr {
167167
friend class Z3Solver;
168168

169169
Z3Context &Context;
170170

171171
Z3_ast AST;
172172

173-
Z3Expr(Z3Context &C, Z3_ast ZA) : Context(C), AST(ZA) {
174-
assert(C.Context != nullptr);
173+
Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) {
175174
Z3_inc_ref(Context.Context, AST);
176175
}
177176

178-
// Determine whether two float semantics are equivalent
179-
static bool areEquivalent(const llvm::fltSemantics &LHS,
180-
const llvm::fltSemantics &RHS) {
181-
return (llvm::APFloat::semanticsPrecision(LHS) ==
182-
llvm::APFloat::semanticsPrecision(RHS)) &&
183-
(llvm::APFloat::semanticsMinExponent(LHS) ==
184-
llvm::APFloat::semanticsMinExponent(RHS)) &&
185-
(llvm::APFloat::semanticsMaxExponent(LHS) ==
186-
llvm::APFloat::semanticsMaxExponent(RHS)) &&
187-
(llvm::APFloat::semanticsSizeInBits(LHS) ==
188-
llvm::APFloat::semanticsSizeInBits(RHS));
189-
}
190-
191177
public:
192178
/// Override implicit copy constructor for correct reference counting.
193-
Z3Expr(const Z3Expr &Copy) : Context(Copy.Context), AST(Copy.AST) {
179+
Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) {
194180
Z3_inc_ref(Context.Context, AST);
195181
}
196182

197183
/// Provide move constructor
198-
Z3Expr(Z3Expr &&Move) : Context(Move.Context), AST(nullptr) {
184+
Z3Expr(Z3Expr &&Move) : SMTExpr(), Context(Move.Context), AST(nullptr) {
199185
*this = std::move(Move);
200186
}
201187

@@ -215,40 +201,18 @@ class Z3Expr {
215201
Z3_dec_ref(Context.Context, AST);
216202
}
217203

218-
/// Get the corresponding IEEE floating-point type for a given bitwidth.
219-
static const llvm::fltSemantics &getFloatSemantics(unsigned BitWidth) {
220-
switch (BitWidth) {
221-
default:
222-
llvm_unreachable("Unsupported floating-point semantics!");
223-
break;
224-
case 16:
225-
return llvm::APFloat::IEEEhalf();
226-
case 32:
227-
return llvm::APFloat::IEEEsingle();
228-
case 64:
229-
return llvm::APFloat::IEEEdouble();
230-
case 128:
231-
return llvm::APFloat::IEEEquad();
232-
}
233-
}
234-
235-
void Profile(llvm::FoldingSetNodeID &ID) const {
204+
void Profile(llvm::FoldingSetNodeID &ID) const override {
236205
ID.AddInteger(Z3_get_ast_hash(Context.Context, AST));
237206
}
238207

239-
bool operator<(const Z3Expr &Other) const {
240-
llvm::FoldingSetNodeID ID1, ID2;
241-
Profile(ID1);
242-
Other.Profile(ID2);
243-
return ID1 < ID2;
244-
}
245-
246208
/// Comparison of AST equality, not model equivalence.
247-
bool operator==(const Z3Expr &Other) const {
209+
bool equal_to(SMTExpr const &Other) const override {
248210
assert(Z3_is_eq_sort(Context.Context, Z3_get_sort(Context.Context, AST),
249-
Z3_get_sort(Context.Context, Other.AST)) &&
211+
Z3_get_sort(Context.Context,
212+
static_cast<const Z3Expr &>(Other).AST)) &&
250213
"AST's must have the same sort");
251-
return Z3_is_eq_ast(Context.Context, AST, Other.AST);
214+
return Z3_is_eq_ast(Context.Context, AST,
215+
static_cast<const Z3Expr &>(Other).AST);
252216
}
253217

254218
/// Override implicit move constructor for correct reference counting.
@@ -259,11 +223,9 @@ class Z3Expr {
259223
return *this;
260224
}
261225

262-
void print(raw_ostream &OS) const {
226+
void print(raw_ostream &OS) const override {
263227
OS << Z3_ast_to_string(Context.Context, AST);
264228
}
265-
266-
LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
267229
}; // end class Z3Expr
268230

269231
class Z3Model {
@@ -312,6 +274,36 @@ class Z3Model {
312274
LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
313275
}; // end class Z3Model
314276

277+
/// Get the corresponding IEEE floating-point type for a given bitwidth.
278+
static const llvm::fltSemantics &getFloatSemantics(unsigned BitWidth) {
279+
switch (BitWidth) {
280+
default:
281+
llvm_unreachable("Unsupported floating-point semantics!");
282+
break;
283+
case 16:
284+
return llvm::APFloat::IEEEhalf();
285+
case 32:
286+
return llvm::APFloat::IEEEsingle();
287+
case 64:
288+
return llvm::APFloat::IEEEdouble();
289+
case 128:
290+
return llvm::APFloat::IEEEquad();
291+
}
292+
}
293+
294+
// Determine whether two float semantics are equivalent
295+
static bool areEquivalent(const llvm::fltSemantics &LHS,
296+
const llvm::fltSemantics &RHS) {
297+
return (llvm::APFloat::semanticsPrecision(LHS) ==
298+
llvm::APFloat::semanticsPrecision(RHS)) &&
299+
(llvm::APFloat::semanticsMinExponent(LHS) ==
300+
llvm::APFloat::semanticsMinExponent(RHS)) &&
301+
(llvm::APFloat::semanticsMaxExponent(LHS) ==
302+
llvm::APFloat::semanticsMaxExponent(RHS)) &&
303+
(llvm::APFloat::semanticsSizeInBits(LHS) ==
304+
llvm::APFloat::semanticsSizeInBits(RHS));
305+
}
306+
315307
class Z3Solver {
316308
friend class Z3ConstraintManager;
317309

@@ -812,14 +804,13 @@ class Z3Solver {
812804

813805
llvm::APSInt Int(Sort.getFloatSortSize(), true);
814806
const llvm::fltSemantics &Semantics =
815-
Z3Expr::getFloatSemantics(Sort.getFloatSortSize());
807+
getFloatSemantics(Sort.getFloatSortSize());
816808
Z3Sort BVSort = getBitvectorSort(Sort.getFloatSortSize());
817809
if (!toAPSInt(BVSort, AST, Int, true)) {
818810
return false;
819811
}
820812

821-
if (useSemantics &&
822-
!Z3Expr::areEquivalent(Float.getSemantics(), Semantics)) {
813+
if (useSemantics && !areEquivalent(Float.getSemantics(), Semantics)) {
823814
assert(false && "Floating-point types don't match!");
824815
return false;
825816
}

0 commit comments

Comments
 (0)
Please sign in to comment.