Go to the documentation of this file.
14 #ifndef LLVM_SUPPORT_SMTAPI_H
15 #define LLVM_SUPPORT_SMTAPI_H
45 assert(Size &&
"Size is zero!");
54 assert(Size &&
"Size is zero!");
400 bool isUnsigned) = 0;
425 virtual void push() = 0;
428 virtual void pop(
unsigned NumStates = 1) = 0;
431 virtual void reset() = 0;
virtual SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector subtraction operation.
Generic base class for SMT Solvers.
virtual SMTExprRef mkFPEqual(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point equality operation.
virtual SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point remainder operation.
#define LLVM_DUMP_METHOD
Mark debug helper function definitions like dump() that should not be stripped from debug builds.
virtual SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point greater-than operation.
This is an optimization pass for GlobalISel generic memory operations.
virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T, const SMTExprRef &F)=0
Creates a boolean ite operation.
virtual SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector multiplication operation.
virtual SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector xor operation.
virtual SMTExprRef mkBVSubNoUnderflow(const SMTExprRef &LHS, const SMTExprRef &RHS, bool isSigned)=0
Creates a predicate that checks for underflow in a bitvector subtraction operation.
virtual SMTExprRef mkBVMulNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS, bool isSigned)=0
Creates a predicate that checks for overflow in a bitvector multiplication operation.
virtual SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To)=0
Creates a floating-point conversion from floatint-point to floating-point operation.
virtual SMTExprRef mkFloat(const llvm::APFloat Float)=0
Constructs an SMTExprRef from a finite APFloat.
virtual SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp)=0
Creates a floating-point isInfinite operation.
virtual SMTExprRef mkFPIsNaN(const SMTExprRef &Exp)=0
Creates a floating-point isNaN operation.
SMTSolverRef CreateZ3Solver()
Convenience method to create and Z3Solver object.
virtual bool isBitvectorSortImpl() const =0
Query the SMT solver and checks if a sort is bitvector.
virtual void pop(unsigned NumStates=1)=0
Pop the previous solver state.
virtual SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed less-equal-than operation.
virtual SMTSortRef getFloat32Sort()=0
virtual SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned division operation.
virtual SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned modulus operation.
virtual SMTExprRef mkFPNeg(const SMTExprRef &Exp)=0
Creates a floating-point negation operation.
virtual SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort)=0
Creates a new symbol, given a name and a sort.
virtual SMTExprRef mkFPIsNormal(const SMTExprRef &Exp)=0
Creates a floating-point isNormal operation.
virtual SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp)=0
Creates a bitvector sign extension operation.
virtual SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector and operation.
virtual SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp)=0
Creates a bitvector zero extension operation.
virtual SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector or operation.
virtual SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector logical shift left operation.
virtual Optional< bool > check() const =0
Check if the constraints are satisfiable.
virtual SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point division operation.
virtual SMTExprRef mkBVNegNoOverflow(const SMTExprRef &Exp)=0
Creates a predicate that checks for overflow in a bitvector negation operation.
virtual SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth)=0
Constructs an SMTExprRef from an APSInt and its bit width.
virtual SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a boolean equality operation.
virtual void reset()=0
Reset the solver and remove all constraints.
virtual unsigned getBitvectorSortSizeImpl() const =0
Query the SMT solver and returns the sort bit width.
virtual unsigned getBitvectorSortSize() const
Returns the bitvector size, fails if the sort is not a bitvector Calls getBitvectorSortSizeImpl().
virtual SMTExprRef mkBVExtract(unsigned High, unsigned Low, const SMTExprRef &Exp)=0
Creates a bitvector extract operation.
virtual llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth, bool isUnsigned)=0
virtual SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector logical shift right operation.
virtual SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed greater-than operation.
the resulting code requires compare and branches when and if the revised code is with conditional branches instead of More there is a byte word extend before each where there should be only and the condition codes are not remembered when the same two values are compared twice More LSR enhancements i8 and i32 load store addressing modes are identical int b
virtual SMTExprRef mkFPIsZero(const SMTExprRef &Exp)=0
Creates a floating-point isZero operation.
virtual bool equal_to(SMTSort const &other) const =0
Query the SMT solver and returns true if two sorts are equal (same kind and bit width).
virtual void addConstraint(const SMTExprRef &Exp) const =0
Given a constraint, adds it to the solver.
An arbitrary precision integer that knows its signedness.
This class implements an extremely fast bulk output stream that can only output to a stream.
LLVM_DUMP_METHOD void dump() const
bool operator<(const SMTExpr &Other) const
virtual void print(raw_ostream &OS) const =0
virtual SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned less-equal-than operation.
unsigned ID
LLVM IR allows to use arbitrary numbers as calling convention identifiers.
virtual SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed division operation.
virtual SMTSortRef getSort(const SMTExprRef &AST)=0
virtual SMTSortRef getFloat64Sort()=0
virtual SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed less-than operation.
virtual SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector arithmetic shift right operation.
virtual bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int)=0
Given an expression, extract the value of this operand in the model.
virtual SMTSortRef getBoolSort()=0
std::shared_ptr< SMTSolver > SMTSolverRef
Shared pointer for SMTSolvers.
virtual bool isBooleanSortImpl() const =0
Query the SMT solver and checks if a sort is boolean.
Generic base class for SMT exprs.
virtual bool isFloatSortImpl() const =0
Query the SMT solver and checks if a sort is floating-point.
virtual unsigned getFloatSortSize() const
Returns the floating-point size, fails if the sort is not a floating-point Calls getFloatSortSizeImpl...
virtual bool getBoolean(const SMTExprRef &Exp)=0
virtual ~SMTSolver()=default
SMTSortRef getFloatSort(unsigned BitWidth)
virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From, const SMTSortRef &To)=0
Creates a floating-point conversion from signed bitvector to floatint-point operation.
virtual SMTExprRef mkBVAddNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS, bool isSigned)=0
Creates a predicate that checks for overflow in a bitvector addition operation.
virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From, const SMTSortRef &To)=0
Creates a floating-point conversion from unsigned bitvector to floatint-point operation.
virtual unsigned getFloatSortSizeImpl() const =0
Query the SMT solver and returns the sort bit width.
virtual void print(raw_ostream &OS) const =0
virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth)=0
Creates a floating-point conversion from floatint-point to unsigned bitvector operation.
virtual void push()=0
Push the current solver state.
assert(ImpDefSCC.getReg()==AMDGPU::SCC &&ImpDefSCC.isDef())
virtual void print(raw_ostream &OS) const =0
virtual SMTExprRef mkBVMulNoUnderflow(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a predicate that checks for underflow in a signed bitvector multiplication operation.
virtual SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point less-than-or-equal operation.
bool operator<(const SMTSort &Other) const
virtual SMTExprRef mkBVSDivNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a predicate that checks for overflow in a signed bitvector division/modulus operation.
virtual ~SMTSort()=default
SmallVector< MachineOperand, 4 > Cond
#define llvm_unreachable(msg)
Marks that the current location is not supposed to be reachable.
virtual void Profile(llvm::FoldingSetNodeID &ID) const =0
LLVM_DUMP_METHOD void dump() const
virtual SMTExprRef mkBVNeg(const SMTExprRef &Exp)=0
Creates a bitvector negation operation.
FoldingSetNodeID - This class is used to gather all the unique data bits of a node.
virtual SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned greater-than operation.
virtual SMTExprRef getFloatRoundingMode()=0
virtual SMTExprRef mkBVConcat(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector concat operation.
virtual SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned greater-equal-than operation.
virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth)=0
Creates a floating-point conversion from floatint-point to signed bitvector operation.
virtual SMTSortRef getBitvectorSort(const unsigned BitWidth)=0
virtual void Profile(llvm::FoldingSetNodeID &ID) const =0
virtual SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point addition operation.
virtual SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a boolean and operation.
virtual SMTExprRef mkBVAddNoUnderflow(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a predicate that checks for underflow in a signed bitvector addition operation.
constexpr unsigned BitWidth
virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector addition operation.
virtual bool isFPSupported()=0
Checks if the solver supports floating-points.
virtual SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point greater-than-or-equal operation.
friend bool operator==(SMTSort const &LHS, SMTSort const &RHS)
virtual ~SMTExpr()=default
virtual SMTExprRef mkBoolean(const bool b)=0
Constructs an SMTExprRef from a boolean.
virtual SMTExprRef mkBVNot(const SMTExprRef &Exp)=0
Creates a bitvector not operation.
virtual SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned less-than operation.
LLVM_DUMP_METHOD void dump() const
virtual SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed modulus operation.
virtual bool isBitvectorSort() const
Returns true if the sort is a bitvector, calls isBitvectorSortImpl().
virtual SMTSortRef getFloat16Sort()=0
virtual SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed greater-equal-than operation.
virtual SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point subtraction operation.
virtual bool isFloatSort() const
Returns true if the sort is a floating-point, calls isFloatSortImpl().
virtual SMTSortRef getFloat128Sort()=0
virtual bool equal_to(SMTExpr const &other) const =0
Query the SMT solver and returns true if two sorts are equal (same kind and bit width).
virtual SMTExprRef mkBVSubNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a predicate that checks for overflow in a signed bitvector subtraction operation.
virtual SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a boolean or operation.
virtual SMTExprRef mkNot(const SMTExprRef &Exp)=0
Creates a boolean not operation.
BlockVerifier::State From
virtual bool isBooleanSort() const
Returns true if the sort is a boolean, calls isBooleanSortImpl().
Generic base class for SMT sorts.
virtual SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point multiplication operation.
friend bool operator==(SMTExpr const &LHS, SMTExpr const &RHS)
virtual SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point less-than operation.
Optional< std::vector< StOtherPiece > > Other