r337917 - [analyzer] Create generic SMT Expr class
Mikhail R. Gadelha via cfe-commits
cfe-commits at lists.llvm.org
Wed Jul 25 05:49:19 PDT 2018
Author: mramalho
Date: Wed Jul 25 05:49:19 2018
New Revision: 337917
URL: http://llvm.org/viewvc/llvm-project?rev=337917&view=rev
Log:
[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
Added:
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h
Modified:
cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
Added: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h?rev=337917&view=auto
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h (added)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h Wed Jul 25 05:49:19 2018
@@ -0,0 +1,57 @@
+//== SMTExpr.h --------------------------------------------------*- C++ -*--==//
+//
+// The LLVM Compiler Infrastructure
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+//
+// This file defines a SMT generic Expr API, which will be the base class
+// for every SMT solver expr specific class.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTEXPR_H
+#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTEXPR_H
+
+#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
+
+namespace clang {
+namespace ento {
+
+class SMTExpr {
+public:
+ SMTExpr() = default;
+ virtual ~SMTExpr() = default;
+
+ bool operator<(const SMTExpr &Other) const {
+ llvm::FoldingSetNodeID ID1, ID2;
+ Profile(ID1);
+ Other.Profile(ID2);
+ return ID1 < ID2;
+ }
+
+ virtual void Profile(llvm::FoldingSetNodeID &ID) const {
+ static int Tag = 0;
+ ID.AddPointer(&Tag);
+ }
+
+ friend bool operator==(SMTExpr const &LHS, SMTExpr const &RHS) {
+ return LHS.equal_to(RHS);
+ }
+
+ virtual void print(raw_ostream &OS) const = 0;
+
+ LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
+
+protected:
+ virtual bool equal_to(SMTExpr const &other) const = 0;
+};
+
+using SMTExprRef = std::shared_ptr<SMTExpr>;
+
+} // namespace ento
+} // namespace clang
+
+#endif
Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=337917&r1=337916&r2=337917&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Wed Jul 25 05:49:19 2018
@@ -12,6 +12,7 @@
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h"
#include "clang/Config/config.h"
@@ -162,40 +163,25 @@ public:
}
}; // end class Z3Sort
-class Z3Expr {
- friend class Z3Model;
+class Z3Expr : public SMTExpr {
friend class Z3Solver;
Z3Context &Context;
Z3_ast AST;
- Z3Expr(Z3Context &C, Z3_ast ZA) : Context(C), AST(ZA) {
- assert(C.Context != nullptr);
+ Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) {
Z3_inc_ref(Context.Context, AST);
}
- // Determine whether two float semantics are equivalent
- static bool areEquivalent(const llvm::fltSemantics &LHS,
- const llvm::fltSemantics &RHS) {
- return (llvm::APFloat::semanticsPrecision(LHS) ==
- llvm::APFloat::semanticsPrecision(RHS)) &&
- (llvm::APFloat::semanticsMinExponent(LHS) ==
- llvm::APFloat::semanticsMinExponent(RHS)) &&
- (llvm::APFloat::semanticsMaxExponent(LHS) ==
- llvm::APFloat::semanticsMaxExponent(RHS)) &&
- (llvm::APFloat::semanticsSizeInBits(LHS) ==
- llvm::APFloat::semanticsSizeInBits(RHS));
- }
-
public:
/// Override implicit copy constructor for correct reference counting.
- Z3Expr(const Z3Expr &Copy) : Context(Copy.Context), AST(Copy.AST) {
+ Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) {
Z3_inc_ref(Context.Context, AST);
}
/// Provide move constructor
- Z3Expr(Z3Expr &&Move) : Context(Move.Context), AST(nullptr) {
+ Z3Expr(Z3Expr &&Move) : SMTExpr(), Context(Move.Context), AST(nullptr) {
*this = std::move(Move);
}
@@ -215,40 +201,18 @@ public:
Z3_dec_ref(Context.Context, AST);
}
- /// Get the corresponding IEEE floating-point type for a given bitwidth.
- static const llvm::fltSemantics &getFloatSemantics(unsigned BitWidth) {
- switch (BitWidth) {
- default:
- llvm_unreachable("Unsupported floating-point semantics!");
- break;
- case 16:
- return llvm::APFloat::IEEEhalf();
- case 32:
- return llvm::APFloat::IEEEsingle();
- case 64:
- return llvm::APFloat::IEEEdouble();
- case 128:
- return llvm::APFloat::IEEEquad();
- }
- }
-
- void Profile(llvm::FoldingSetNodeID &ID) const {
+ void Profile(llvm::FoldingSetNodeID &ID) const override {
ID.AddInteger(Z3_get_ast_hash(Context.Context, AST));
}
- bool operator<(const Z3Expr &Other) const {
- llvm::FoldingSetNodeID ID1, ID2;
- Profile(ID1);
- Other.Profile(ID2);
- return ID1 < ID2;
- }
-
/// Comparison of AST equality, not model equivalence.
- bool operator==(const Z3Expr &Other) const {
+ bool equal_to(SMTExpr const &Other) const override {
assert(Z3_is_eq_sort(Context.Context, Z3_get_sort(Context.Context, AST),
- Z3_get_sort(Context.Context, Other.AST)) &&
+ Z3_get_sort(Context.Context,
+ static_cast<const Z3Expr &>(Other).AST)) &&
"AST's must have the same sort");
- return Z3_is_eq_ast(Context.Context, AST, Other.AST);
+ return Z3_is_eq_ast(Context.Context, AST,
+ static_cast<const Z3Expr &>(Other).AST);
}
/// Override implicit move constructor for correct reference counting.
@@ -259,11 +223,9 @@ public:
return *this;
}
- void print(raw_ostream &OS) const {
+ void print(raw_ostream &OS) const override {
OS << Z3_ast_to_string(Context.Context, AST);
}
-
- LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
}; // end class Z3Expr
class Z3Model {
@@ -312,6 +274,36 @@ public:
LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
}; // end class Z3Model
+/// Get the corresponding IEEE floating-point type for a given bitwidth.
+static const llvm::fltSemantics &getFloatSemantics(unsigned BitWidth) {
+ switch (BitWidth) {
+ default:
+ llvm_unreachable("Unsupported floating-point semantics!");
+ break;
+ case 16:
+ return llvm::APFloat::IEEEhalf();
+ case 32:
+ return llvm::APFloat::IEEEsingle();
+ case 64:
+ return llvm::APFloat::IEEEdouble();
+ case 128:
+ return llvm::APFloat::IEEEquad();
+ }
+}
+
+// Determine whether two float semantics are equivalent
+static bool areEquivalent(const llvm::fltSemantics &LHS,
+ const llvm::fltSemantics &RHS) {
+ return (llvm::APFloat::semanticsPrecision(LHS) ==
+ llvm::APFloat::semanticsPrecision(RHS)) &&
+ (llvm::APFloat::semanticsMinExponent(LHS) ==
+ llvm::APFloat::semanticsMinExponent(RHS)) &&
+ (llvm::APFloat::semanticsMaxExponent(LHS) ==
+ llvm::APFloat::semanticsMaxExponent(RHS)) &&
+ (llvm::APFloat::semanticsSizeInBits(LHS) ==
+ llvm::APFloat::semanticsSizeInBits(RHS));
+}
+
class Z3Solver {
friend class Z3ConstraintManager;
@@ -812,14 +804,13 @@ public:
llvm::APSInt Int(Sort.getFloatSortSize(), true);
const llvm::fltSemantics &Semantics =
- Z3Expr::getFloatSemantics(Sort.getFloatSortSize());
+ getFloatSemantics(Sort.getFloatSortSize());
Z3Sort BVSort = getBitvectorSort(Sort.getFloatSortSize());
if (!toAPSInt(BVSort, AST, Int, true)) {
return false;
}
- if (useSemantics &&
- !Z3Expr::areEquivalent(Float.getSemantics(), Semantics)) {
+ if (useSemantics && !areEquivalent(Float.getSemantics(), Semantics)) {
assert(false && "Floating-point types don't match!");
return false;
}
More information about the cfe-commits
mailing list