r353372 - Moved the whole SMT API to a single file. NFC.
Mikhail R. Gadelha via cfe-commits
cfe-commits at lists.llvm.org
Wed Feb 6 19:18:21 PST 2019
Author: mramalho
Date: Wed Feb 6 19:18:21 2019
New Revision: 353372
URL: http://llvm.org/viewvc/llvm-project?rev=353372&view=rev
Log:
Moved the whole SMT API to a single file. NFC.
There is no advantage in having them in separate files, I doubt some will ever use them separately.
This also makes it easier to move the API to LLVM.
Differential Revision: https://reviews.llvm.org/D54977
Added:
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h
Removed:
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h
Modified:
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
Added: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h?rev=353372&view=auto
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h (added)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h Wed Feb 6 19:18:21 2019
@@ -0,0 +1,404 @@
+//== SMTSolver.h ------------------------------------------------*- C++ -*--==//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// This file defines a SMT generic Solver API, which will be the base class
+// for every SMT solver specific class.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
+#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
+
+#include "clang/Basic/TargetInfo.h"
+#include "llvm/ADT/APSInt.h"
+
+namespace clang {
+namespace ento {
+
+/// Generic base class for SMT sorts
+class SMTSort {
+public:
+ SMTSort() = default;
+ virtual ~SMTSort() = default;
+
+ /// Returns true if the sort is a bitvector, calls isBitvectorSortImpl().
+ virtual bool isBitvectorSort() const { return isBitvectorSortImpl(); }
+
+ /// Returns true if the sort is a floating-point, calls isFloatSortImpl().
+ virtual bool isFloatSort() const { return isFloatSortImpl(); }
+
+ /// Returns true if the sort is a boolean, calls isBooleanSortImpl().
+ virtual bool isBooleanSort() const { return isBooleanSortImpl(); }
+
+ /// Returns the bitvector size, fails if the sort is not a bitvector
+ /// Calls getBitvectorSortSizeImpl().
+ virtual unsigned getBitvectorSortSize() const {
+ assert(isBitvectorSort() && "Not a bitvector sort!");
+ unsigned Size = getBitvectorSortSizeImpl();
+ assert(Size && "Size is zero!");
+ return Size;
+ };
+
+ /// Returns the floating-point size, fails if the sort is not a floating-point
+ /// Calls getFloatSortSizeImpl().
+ virtual unsigned getFloatSortSize() const {
+ assert(isFloatSort() && "Not a floating-point sort!");
+ unsigned Size = getFloatSortSizeImpl();
+ assert(Size && "Size is zero!");
+ return Size;
+ };
+
+ virtual void Profile(llvm::FoldingSetNodeID &ID) const = 0;
+
+ bool operator<(const SMTSort &Other) const {
+ llvm::FoldingSetNodeID ID1, ID2;
+ Profile(ID1);
+ Other.Profile(ID2);
+ return ID1 < ID2;
+ }
+
+ 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:
+ /// Query the SMT solver and returns true if two sorts are equal (same kind
+ /// and bit width). This does not check if the two sorts are the same objects.
+ virtual bool equal_to(SMTSort const &other) const = 0;
+
+ /// Query the SMT solver and checks if a sort is bitvector.
+ virtual bool isBitvectorSortImpl() const = 0;
+
+ /// Query the SMT solver and checks if a sort is floating-point.
+ virtual bool isFloatSortImpl() const = 0;
+
+ /// Query the SMT solver and checks if a sort is boolean.
+ virtual bool isBooleanSortImpl() const = 0;
+
+ /// Query the SMT solver and returns the sort bit width.
+ virtual unsigned getBitvectorSortSizeImpl() const = 0;
+
+ /// Query the SMT solver and returns the sort bit width.
+ virtual unsigned getFloatSortSizeImpl() const = 0;
+};
+
+/// Shared pointer for SMTSorts, used by SMTSolver API.
+using SMTSortRef = const SMTSort *;
+
+/// Generic base class for SMT exprs
+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 = 0;
+
+ 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:
+ /// Query the SMT solver and returns true if two sorts are equal (same kind
+ /// and bit width). This does not check if the two sorts are the same objects.
+ virtual bool equal_to(SMTExpr const &other) const = 0;
+};
+
+/// Shared pointer for SMTExprs, used by SMTSolver API.
+using SMTExprRef = const SMTExpr *;
+
+/// Generic base class for SMT Solvers
+///
+/// This class is responsible for wrapping all sorts and expression generation,
+/// through the mk* methods. It also provides methods to create SMT expressions
+/// straight from clang's AST, through the from* methods.
+class SMTSolver {
+public:
+ SMTSolver() = default;
+ virtual ~SMTSolver() = default;
+
+ LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
+
+ // Returns an appropriate floating-point sort for the given bitwidth.
+ SMTSortRef getFloatSort(unsigned BitWidth) {
+ switch (BitWidth) {
+ case 16:
+ return getFloat16Sort();
+ case 32:
+ return getFloat32Sort();
+ case 64:
+ return getFloat64Sort();
+ case 128:
+ return getFloat128Sort();
+ default:;
+ }
+ llvm_unreachable("Unsupported floating-point bitwidth!");
+ }
+
+ // Returns a boolean sort.
+ virtual SMTSortRef getBoolSort() = 0;
+
+ // Returns an appropriate bitvector sort for the given bitwidth.
+ virtual SMTSortRef getBitvectorSort(const unsigned BitWidth) = 0;
+
+ // Returns a floating-point sort of width 16
+ virtual SMTSortRef getFloat16Sort() = 0;
+
+ // Returns a floating-point sort of width 32
+ virtual SMTSortRef getFloat32Sort() = 0;
+
+ // Returns a floating-point sort of width 64
+ virtual SMTSortRef getFloat64Sort() = 0;
+
+ // Returns a floating-point sort of width 128
+ virtual SMTSortRef getFloat128Sort() = 0;
+
+ // Returns an appropriate sort for the given AST.
+ virtual SMTSortRef getSort(const SMTExprRef &AST) = 0;
+
+ /// Given a constraint, adds it to the solver
+ virtual void addConstraint(const SMTExprRef &Exp) const = 0;
+
+ /// Creates a bitvector addition operation
+ virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a bitvector subtraction operation
+ virtual SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a bitvector multiplication operation
+ virtual SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a bitvector signed modulus operation
+ virtual SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a bitvector unsigned modulus operation
+ virtual SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a bitvector signed division operation
+ virtual SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a bitvector unsigned division operation
+ virtual SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a bitvector logical shift left operation
+ virtual SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a bitvector arithmetic shift right operation
+ virtual SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a bitvector logical shift right operation
+ virtual SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a bitvector negation operation
+ virtual SMTExprRef mkBVNeg(const SMTExprRef &Exp) = 0;
+
+ /// Creates a bitvector not operation
+ virtual SMTExprRef mkBVNot(const SMTExprRef &Exp) = 0;
+
+ /// Creates a bitvector xor operation
+ virtual SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a bitvector or operation
+ virtual SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a bitvector and operation
+ virtual SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a bitvector unsigned less-than operation
+ virtual SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a bitvector signed less-than operation
+ virtual SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a bitvector unsigned greater-than operation
+ virtual SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a bitvector signed greater-than operation
+ virtual SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a bitvector unsigned less-equal-than operation
+ virtual SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a bitvector signed less-equal-than operation
+ virtual SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a bitvector unsigned greater-equal-than operation
+ virtual SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a bitvector signed greater-equal-than operation
+ virtual SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a boolean not operation
+ virtual SMTExprRef mkNot(const SMTExprRef &Exp) = 0;
+
+ /// Creates a boolean equality operation
+ virtual SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a boolean and operation
+ virtual SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a boolean or operation
+ virtual SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a boolean ite operation
+ virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
+ const SMTExprRef &F) = 0;
+
+ /// Creates a bitvector sign extension operation
+ virtual SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) = 0;
+
+ /// Creates a bitvector zero extension operation
+ virtual SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) = 0;
+
+ /// Creates a bitvector extract operation
+ virtual SMTExprRef mkBVExtract(unsigned High, unsigned Low,
+ const SMTExprRef &Exp) = 0;
+
+ /// Creates a bitvector concat operation
+ virtual SMTExprRef mkBVConcat(const SMTExprRef &LHS,
+ const SMTExprRef &RHS) = 0;
+
+ /// Creates a floating-point negation operation
+ virtual SMTExprRef mkFPNeg(const SMTExprRef &Exp) = 0;
+
+ /// Creates a floating-point isInfinite operation
+ virtual SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) = 0;
+
+ /// Creates a floating-point isNaN operation
+ virtual SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) = 0;
+
+ /// Creates a floating-point isNormal operation
+ virtual SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) = 0;
+
+ /// Creates a floating-point isZero operation
+ virtual SMTExprRef mkFPIsZero(const SMTExprRef &Exp) = 0;
+
+ /// Creates a floating-point multiplication operation
+ virtual SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a floating-point division operation
+ virtual SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a floating-point remainder operation
+ virtual SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a floating-point addition operation
+ virtual SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a floating-point subtraction operation
+ virtual SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a floating-point less-than operation
+ virtual SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a floating-point greater-than operation
+ virtual SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a floating-point less-than-or-equal operation
+ virtual SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a floating-point greater-than-or-equal operation
+ virtual SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+
+ /// Creates a floating-point equality operation
+ virtual SMTExprRef mkFPEqual(const SMTExprRef &LHS,
+ const SMTExprRef &RHS) = 0;
+
+ /// Creates a floating-point conversion from floatint-point to floating-point
+ /// operation
+ virtual SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) = 0;
+
+ /// Creates a floating-point conversion from signed bitvector to
+ /// floatint-point operation
+ virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From,
+ const SMTSortRef &To) = 0;
+
+ /// Creates a floating-point conversion from unsigned bitvector to
+ /// floatint-point operation
+ virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From,
+ const SMTSortRef &To) = 0;
+
+ /// Creates a floating-point conversion from floatint-point to signed
+ /// bitvector operation
+ virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth) = 0;
+
+ /// Creates a floating-point conversion from floatint-point to unsigned
+ /// bitvector operation
+ virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth) = 0;
+
+ /// Creates a new symbol, given a name and a sort
+ virtual SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) = 0;
+
+ // Returns an appropriate floating-point rounding mode.
+ virtual SMTExprRef getFloatRoundingMode() = 0;
+
+ // If the a model is available, returns the value of a given bitvector symbol
+ virtual llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth,
+ bool isUnsigned) = 0;
+
+ // If the a model is available, returns the value of a given boolean symbol
+ virtual bool getBoolean(const SMTExprRef &Exp) = 0;
+
+ /// Constructs an SMTExprRef from a boolean.
+ virtual SMTExprRef mkBoolean(const bool b) = 0;
+
+ /// Constructs an SMTExprRef from a finite APFloat.
+ virtual SMTExprRef mkFloat(const llvm::APFloat Float) = 0;
+
+ /// Constructs an SMTExprRef from an APSInt and its bit width
+ virtual SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) = 0;
+
+ /// Given an expression, extract the value of this operand in the model.
+ virtual bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) = 0;
+
+ /// Given an expression extract the value of this operand in the model.
+ virtual bool getInterpretation(const SMTExprRef &Exp,
+ llvm::APFloat &Float) = 0;
+
+ /// Check if the constraints are satisfiable
+ virtual Optional<bool> check() const = 0;
+
+ /// Push the current solver state
+ virtual void push() = 0;
+
+ /// Pop the previous solver state
+ virtual void pop(unsigned NumStates = 1) = 0;
+
+ /// Reset the solver and remove all constraints.
+ virtual void reset() = 0;
+
+ /// Checks if the solver supports floating-points.
+ virtual bool isFPSupported() = 0;
+
+ virtual void print(raw_ostream &OS) const = 0;
+};
+
+/// Shared pointer for SMTSolvers.
+using SMTSolverRef = std::shared_ptr<SMTSolver>;
+
+/// Convenience method to create and Z3Solver object
+SMTSolverRef CreateZ3Solver();
+
+} // namespace ento
+} // namespace clang
+
+#endif
Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h?rev=353372&r1=353371&r2=353372&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h Wed Feb 6 19:18:21 2019
@@ -15,7 +15,7 @@
#include "clang/AST/Expr.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h"
namespace clang {
Removed: 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=353371&view=auto
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h (removed)
@@ -1,58 +0,0 @@
-//== SMTExpr.h --------------------------------------------------*- C++ -*--==//
-//
-// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
-// See https://llvm.org/LICENSE.txt for license information.
-// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
-//
-//===----------------------------------------------------------------------===//
-//
-// 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/Basic/TargetInfo.h"
-#include "llvm/ADT/FoldingSet.h"
-
-namespace clang {
-namespace ento {
-
-/// Generic base class for SMT exprs
-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 = 0;
-
- 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:
- /// Query the SMT solver and returns true if two sorts are equal (same kind
- /// and bit width). This does not check if the two sorts are the same objects.
- virtual bool equal_to(SMTExpr const &other) const = 0;
-};
-
-/// Shared pointer for SMTExprs, used by SMTSolver API.
-using SMTExprRef = const SMTExpr *;
-
-} // namespace ento
-} // namespace clang
-
-#endif
Removed: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h?rev=353371&view=auto
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h (removed)
@@ -1,299 +0,0 @@
-//== SMTSolver.h ------------------------------------------------*- C++ -*--==//
-//
-// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
-// See https://llvm.org/LICENSE.txt for license information.
-// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
-//
-//===----------------------------------------------------------------------===//
-//
-// This file defines a SMT generic Solver API, which will be the base class
-// for every SMT solver specific class.
-//
-//===----------------------------------------------------------------------===//
-
-#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
-#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
-
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h"
-#include "llvm/ADT/APSInt.h"
-
-namespace clang {
-namespace ento {
-
-/// Generic base class for SMT Solvers
-///
-/// This class is responsible for wrapping all sorts and expression generation,
-/// through the mk* methods. It also provides methods to create SMT expressions
-/// straight from clang's AST, through the from* methods.
-class SMTSolver {
-public:
- SMTSolver() = default;
- virtual ~SMTSolver() = default;
-
- LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
-
- // Returns an appropriate floating-point sort for the given bitwidth.
- SMTSortRef getFloatSort(unsigned BitWidth) {
- switch (BitWidth) {
- case 16:
- return getFloat16Sort();
- case 32:
- return getFloat32Sort();
- case 64:
- return getFloat64Sort();
- case 128:
- return getFloat128Sort();
- default:;
- }
- llvm_unreachable("Unsupported floating-point bitwidth!");
- }
-
- // Returns a boolean sort.
- virtual SMTSortRef getBoolSort() = 0;
-
- // Returns an appropriate bitvector sort for the given bitwidth.
- virtual SMTSortRef getBitvectorSort(const unsigned BitWidth) = 0;
-
- // Returns a floating-point sort of width 16
- virtual SMTSortRef getFloat16Sort() = 0;
-
- // Returns a floating-point sort of width 32
- virtual SMTSortRef getFloat32Sort() = 0;
-
- // Returns a floating-point sort of width 64
- virtual SMTSortRef getFloat64Sort() = 0;
-
- // Returns a floating-point sort of width 128
- virtual SMTSortRef getFloat128Sort() = 0;
-
- // Returns an appropriate sort for the given AST.
- virtual SMTSortRef getSort(const SMTExprRef &AST) = 0;
-
- /// Given a constraint, adds it to the solver
- virtual void addConstraint(const SMTExprRef &Exp) const = 0;
-
- /// Creates a bitvector addition operation
- virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a bitvector subtraction operation
- virtual SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a bitvector multiplication operation
- virtual SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a bitvector signed modulus operation
- virtual SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a bitvector unsigned modulus operation
- virtual SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a bitvector signed division operation
- virtual SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a bitvector unsigned division operation
- virtual SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a bitvector logical shift left operation
- virtual SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a bitvector arithmetic shift right operation
- virtual SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a bitvector logical shift right operation
- virtual SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a bitvector negation operation
- virtual SMTExprRef mkBVNeg(const SMTExprRef &Exp) = 0;
-
- /// Creates a bitvector not operation
- virtual SMTExprRef mkBVNot(const SMTExprRef &Exp) = 0;
-
- /// Creates a bitvector xor operation
- virtual SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a bitvector or operation
- virtual SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a bitvector and operation
- virtual SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a bitvector unsigned less-than operation
- virtual SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a bitvector signed less-than operation
- virtual SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a bitvector unsigned greater-than operation
- virtual SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a bitvector signed greater-than operation
- virtual SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a bitvector unsigned less-equal-than operation
- virtual SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a bitvector signed less-equal-than operation
- virtual SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a bitvector unsigned greater-equal-than operation
- virtual SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a bitvector signed greater-equal-than operation
- virtual SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a boolean not operation
- virtual SMTExprRef mkNot(const SMTExprRef &Exp) = 0;
-
- /// Creates a boolean equality operation
- virtual SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a boolean and operation
- virtual SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a boolean or operation
- virtual SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a boolean ite operation
- virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
- const SMTExprRef &F) = 0;
-
- /// Creates a bitvector sign extension operation
- virtual SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) = 0;
-
- /// Creates a bitvector zero extension operation
- virtual SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) = 0;
-
- /// Creates a bitvector extract operation
- virtual SMTExprRef mkBVExtract(unsigned High, unsigned Low,
- const SMTExprRef &Exp) = 0;
-
- /// Creates a bitvector concat operation
- virtual SMTExprRef mkBVConcat(const SMTExprRef &LHS,
- const SMTExprRef &RHS) = 0;
-
- /// Creates a floating-point negation operation
- virtual SMTExprRef mkFPNeg(const SMTExprRef &Exp) = 0;
-
- /// Creates a floating-point isInfinite operation
- virtual SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) = 0;
-
- /// Creates a floating-point isNaN operation
- virtual SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) = 0;
-
- /// Creates a floating-point isNormal operation
- virtual SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) = 0;
-
- /// Creates a floating-point isZero operation
- virtual SMTExprRef mkFPIsZero(const SMTExprRef &Exp) = 0;
-
- /// Creates a floating-point multiplication operation
- virtual SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a floating-point division operation
- virtual SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a floating-point remainder operation
- virtual SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a floating-point addition operation
- virtual SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a floating-point subtraction operation
- virtual SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a floating-point less-than operation
- virtual SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a floating-point greater-than operation
- virtual SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a floating-point less-than-or-equal operation
- virtual SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a floating-point greater-than-or-equal operation
- virtual SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
-
- /// Creates a floating-point equality operation
- virtual SMTExprRef mkFPEqual(const SMTExprRef &LHS,
- const SMTExprRef &RHS) = 0;
-
- /// Creates a floating-point conversion from floatint-point to floating-point
- /// operation
- virtual SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) = 0;
-
- /// Creates a floating-point conversion from signed bitvector to
- /// floatint-point operation
- virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From,
- const SMTSortRef &To) = 0;
-
- /// Creates a floating-point conversion from unsigned bitvector to
- /// floatint-point operation
- virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From,
- const SMTSortRef &To) = 0;
-
- /// Creates a floating-point conversion from floatint-point to signed
- /// bitvector operation
- virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth) = 0;
-
- /// Creates a floating-point conversion from floatint-point to unsigned
- /// bitvector operation
- virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth) = 0;
-
- /// Creates a new symbol, given a name and a sort
- virtual SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) = 0;
-
- // Returns an appropriate floating-point rounding mode.
- virtual SMTExprRef getFloatRoundingMode() = 0;
-
- // If the a model is available, returns the value of a given bitvector symbol
- virtual llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth,
- bool isUnsigned) = 0;
-
- // If the a model is available, returns the value of a given boolean symbol
- virtual bool getBoolean(const SMTExprRef &Exp) = 0;
-
- /// Constructs an SMTExprRef from a boolean.
- virtual SMTExprRef mkBoolean(const bool b) = 0;
-
- /// Constructs an SMTExprRef from a finite APFloat.
- virtual SMTExprRef mkFloat(const llvm::APFloat Float) = 0;
-
- /// Constructs an SMTExprRef from an APSInt and its bit width
- virtual SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) = 0;
-
- /// Given an expression, extract the value of this operand in the model.
- virtual bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) = 0;
-
- /// Given an expression extract the value of this operand in the model.
- virtual bool getInterpretation(const SMTExprRef &Exp,
- llvm::APFloat &Float) = 0;
-
- /// Check if the constraints are satisfiable
- virtual Optional<bool> check() const = 0;
-
- /// Push the current solver state
- virtual void push() = 0;
-
- /// Pop the previous solver state
- virtual void pop(unsigned NumStates = 1) = 0;
-
- /// Reset the solver and remove all constraints.
- virtual void reset() = 0;
-
- /// Checks if the solver supports floating-points.
- virtual bool isFPSupported() = 0;
-
- virtual void print(raw_ostream &OS) const = 0;
-};
-
-/// Shared pointer for SMTSolvers.
-using SMTSolverRef = std::shared_ptr<SMTSolver>;
-
-/// Convenience method to create and Z3Solver object
-SMTSolverRef CreateZ3Solver();
-
-} // namespace ento
-} // namespace clang
-
-#endif
Removed: 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=353371&view=auto
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h (removed)
@@ -1,99 +0,0 @@
-//== SMTSort.h --------------------------------------------------*- C++ -*--==//
-//
-// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
-// See https://llvm.org/LICENSE.txt for license information.
-// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
-//
-//===----------------------------------------------------------------------===//
-//
-// 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
-
-#include "clang/Basic/TargetInfo.h"
-
-namespace clang {
-namespace ento {
-
-/// Generic base class for SMT sorts
-class SMTSort {
-public:
- SMTSort() = default;
- virtual ~SMTSort() = default;
-
- /// Returns true if the sort is a bitvector, calls isBitvectorSortImpl().
- virtual bool isBitvectorSort() const { return isBitvectorSortImpl(); }
-
- /// Returns true if the sort is a floating-point, calls isFloatSortImpl().
- virtual bool isFloatSort() const { return isFloatSortImpl(); }
-
- /// Returns true if the sort is a boolean, calls isBooleanSortImpl().
- virtual bool isBooleanSort() const { return isBooleanSortImpl(); }
-
- /// Returns the bitvector size, fails if the sort is not a bitvector
- /// Calls getBitvectorSortSizeImpl().
- virtual unsigned getBitvectorSortSize() const {
- assert(isBitvectorSort() && "Not a bitvector sort!");
- unsigned Size = getBitvectorSortSizeImpl();
- assert(Size && "Size is zero!");
- return Size;
- };
-
- /// Returns the floating-point size, fails if the sort is not a floating-point
- /// Calls getFloatSortSizeImpl().
- virtual unsigned getFloatSortSize() const {
- assert(isFloatSort() && "Not a floating-point sort!");
- unsigned Size = getFloatSortSizeImpl();
- assert(Size && "Size is zero!");
- return Size;
- };
-
- virtual void Profile(llvm::FoldingSetNodeID &ID) const = 0;
-
- bool operator<(const SMTSort &Other) const {
- llvm::FoldingSetNodeID ID1, ID2;
- Profile(ID1);
- Other.Profile(ID2);
- return ID1 < ID2;
- }
-
- 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:
- /// Query the SMT solver and returns true if two sorts are equal (same kind
- /// and bit width). This does not check if the two sorts are the same objects.
- virtual bool equal_to(SMTSort const &other) const = 0;
-
- /// Query the SMT solver and checks if a sort is bitvector.
- virtual bool isBitvectorSortImpl() const = 0;
-
- /// Query the SMT solver and checks if a sort is floating-point.
- virtual bool isFloatSortImpl() const = 0;
-
- /// Query the SMT solver and checks if a sort is boolean.
- virtual bool isBooleanSortImpl() const = 0;
-
- /// Query the SMT solver and returns the sort bit width.
- virtual unsigned getBitvectorSortSizeImpl() const = 0;
-
- /// Query the SMT solver and returns the sort bit width.
- virtual unsigned getFloatSortSizeImpl() const = 0;
-};
-
-/// Shared pointer for SMTSorts, used by SMTSolver API.
-using SMTSortRef = const SMTSort *;
-
-} // namespace ento
-} // namespace clang
-
-#endif
More information about the cfe-commits
mailing list