r337916 - [analyzer] Create generic SMT Sort Class
Mikhail R. Gadelha via cfe-commits
cfe-commits at lists.llvm.org
Wed Jul 25 05:49:15 PDT 2018
Author: mramalho
Date: Wed Jul 25 05:49:15 2018
New Revision: 337916
URL: http://llvm.org/viewvc/llvm-project?rev=337916&view=rev
Log:
[analyzer] Create generic SMT Sort Class
Summary:
New base class for all future SMT sorts.
The only change is that the class implements methods `isBooleanSort()`, `isBitvectorSort()` and `isFloatSort()` so it doesn't rely on `Z3`'s enum.
Reviewers: NoQ, george.karpenkov
Reviewed By: george.karpenkov
Subscribers: xazax.hun, szepet, a.sidorin
Differential Revision: https://reviews.llvm.org/D49550
Added:
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h
Modified:
cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
Added: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h?rev=337916&view=auto
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h (added)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h Wed Jul 25 05:49:15 2018
@@ -0,0 +1,71 @@
+//== SMTSort.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 Sort API, which will be the base class
+// for every SMT solver sort specific class.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSORT_H
+#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSORT_H
+
+namespace clang {
+namespace ento {
+
+class SMTSort {
+public:
+ SMTSort() = default;
+ virtual ~SMTSort() = default;
+
+ virtual bool isBitvectorSort() const { return isBitvectorSortImpl(); }
+ virtual bool isFloatSort() const { return isFloatSortImpl(); }
+ virtual bool isBooleanSort() const { return isBooleanSortImpl(); }
+
+ virtual unsigned getBitvectorSortSize() const {
+ assert(isBitvectorSort() && "Not a bitvector sort!");
+ unsigned Size = getBitvectorSortSizeImpl();
+ assert(Size && "Size is zero!");
+ return Size;
+ };
+
+ virtual unsigned getFloatSortSize() const {
+ assert(isFloatSort() && "Not a floating-point sort!");
+ unsigned Size = getFloatSortSizeImpl();
+ assert(Size && "Size is zero!");
+ return Size;
+ };
+
+ friend bool operator==(SMTSort const &LHS, SMTSort 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(SMTSort const &other) const = 0;
+
+ virtual bool isBitvectorSortImpl() const = 0;
+
+ virtual bool isFloatSortImpl() const = 0;
+
+ virtual bool isBooleanSortImpl() const = 0;
+
+ virtual unsigned getBitvectorSortSizeImpl() const = 0;
+
+ virtual unsigned getFloatSortSizeImpl() const = 0;
+};
+
+using SMTSortRef = std::shared_ptr<SMTSort>;
+
+} // 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=337916&r1=337915&r2=337916&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Wed Jul 25 05:49:15 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/SMTSort.h"
#include "clang/Config/config.h"
@@ -84,27 +85,26 @@ public:
}
}; // end class Z3Context
-class Z3Sort {
- friend class Z3Expr;
+class Z3Sort : public SMTSort {
friend class Z3Solver;
Z3Context &Context;
Z3_sort Sort;
- Z3Sort(Z3Context &C, Z3_sort ZS) : Context(C), Sort(ZS) {
- assert(C.Context != nullptr);
+ Z3Sort(Z3Context &C, Z3_sort ZS) : SMTSort(), Context(C), Sort(ZS) {
Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
}
public:
/// Override implicit copy constructor for correct reference counting.
- Z3Sort(const Z3Sort &Copy) : Context(Copy.Context), Sort(Copy.Sort) {
+ Z3Sort(const Z3Sort &Copy)
+ : SMTSort(), Context(Copy.Context), Sort(Copy.Sort) {
Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
}
/// Provide move constructor
- Z3Sort(Z3Sort &&Move) : Context(Move.Context), Sort(nullptr) {
+ Z3Sort(Z3Sort &&Move) : SMTSort(), Context(Move.Context), Sort(nullptr) {
*this = std::move(Move);
}
@@ -124,24 +124,30 @@ public:
Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
}
- Z3_sort_kind getSortKind() const {
- return Z3_get_sort_kind(Context.Context, Sort);
+ bool isBitvectorSortImpl() const override {
+ return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BV_SORT);
+ }
+
+ bool isFloatSortImpl() const override {
+ return (Z3_get_sort_kind(Context.Context, Sort) == Z3_FLOATING_POINT_SORT);
}
- unsigned getBitvectorSortSize() const {
- assert(getSortKind() == Z3_BV_SORT && "Not a bitvector sort!");
+ bool isBooleanSortImpl() const override {
+ return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BOOL_SORT);
+ }
+
+ unsigned getBitvectorSortSizeImpl() const override {
return Z3_get_bv_sort_size(Context.Context, Sort);
}
- unsigned getFloatSortSize() const {
- assert(getSortKind() == Z3_FLOATING_POINT_SORT &&
- "Not a floating-point sort!");
+ unsigned getFloatSortSizeImpl() const override {
return Z3_fpa_get_ebits(Context.Context, Sort) +
Z3_fpa_get_sbits(Context.Context, Sort);
}
- bool operator==(const Z3Sort &Other) const {
- return Z3_is_eq_sort(Context.Context, Sort, Other.Sort);
+ bool equal_to(SMTSort const &Other) const override {
+ return Z3_is_eq_sort(Context.Context, Sort,
+ static_cast<const Z3Sort &>(Other).Sort);
}
Z3Sort &operator=(const Z3Sort &Move) {
@@ -151,11 +157,9 @@ public:
return *this;
}
- void print(raw_ostream &OS) const {
+ void print(raw_ostream &OS) const override {
OS << Z3_sort_to_string(Context.Context, Sort);
}
-
- LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
}; // end class Z3Sort
class Z3Expr {
@@ -804,8 +808,7 @@ public:
/// Construct an APFloat from a Z3Expr, given the AST representation
bool toAPFloat(const Z3Sort &Sort, const Z3_ast &AST, llvm::APFloat &Float,
bool useSemantics = true) {
- assert(Sort.getSortKind() == Z3_FLOATING_POINT_SORT &&
- "Unsupported sort to floating-point!");
+ assert(Sort.isFloatSort() && "Unsupported sort to floating-point!");
llvm::APSInt Int(Sort.getFloatSortSize(), true);
const llvm::fltSemantics &Semantics =
@@ -828,10 +831,7 @@ public:
/// Construct an APSInt from a Z3Expr, given the AST representation
bool toAPSInt(const Z3Sort &Sort, const Z3_ast &AST, llvm::APSInt &Int,
bool useSemantics = true) {
- switch (Sort.getSortKind()) {
- default:
- llvm_unreachable("Unsupported sort to integer!");
- case Z3_BV_SORT: {
+ if (Sort.isBitvectorSort()) {
if (useSemantics && Int.getBitWidth() != Sort.getBitvectorSortSize()) {
assert(false && "Bitvector types don't match!");
return false;
@@ -859,11 +859,13 @@ public:
}
return true;
}
- case Z3_BOOL_SORT:
+
+ if (Sort.isBooleanSort()) {
if (useSemantics && Int.getBitWidth() < 1) {
assert(false && "Boolean type doesn't match!");
return false;
}
+
Int = llvm::APSInt(
llvm::APInt(Int.getBitWidth(),
Z3_get_bool_value(Context.Context, AST) == Z3_L_TRUE ? 1
@@ -871,6 +873,8 @@ public:
Int.isUnsigned());
return true;
}
+
+ llvm_unreachable("Unsupported sort to integer!");
}
/// Given an expression and a model, extract the value of this operand in
More information about the cfe-commits
mailing list