LLVM  14.0.0git
SMTAPI.h
Go to the documentation of this file.
1 //===- SMTAPI.h -------------------------------------------------*- C++ -*-===//
2 //
3 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4 // See https://llvm.org/LICENSE.txt for license information.
5 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6 //
7 //===----------------------------------------------------------------------===//
8 //
9 // This file defines a SMT generic Solver API, which will be the base class
10 // for every SMT solver specific class.
11 //
12 //===----------------------------------------------------------------------===//
13 
14 #ifndef LLVM_SUPPORT_SMTAPI_H
15 #define LLVM_SUPPORT_SMTAPI_H
16 
17 #include "llvm/ADT/APFloat.h"
18 #include "llvm/ADT/APSInt.h"
19 #include "llvm/ADT/FoldingSet.h"
21 #include <memory>
22 
23 namespace llvm {
24 
25 /// Generic base class for SMT sorts
26 class SMTSort {
27 public:
28  SMTSort() = default;
29  virtual ~SMTSort() = default;
30 
31  /// Returns true if the sort is a bitvector, calls isBitvectorSortImpl().
32  virtual bool isBitvectorSort() const { return isBitvectorSortImpl(); }
33 
34  /// Returns true if the sort is a floating-point, calls isFloatSortImpl().
35  virtual bool isFloatSort() const { return isFloatSortImpl(); }
36 
37  /// Returns true if the sort is a boolean, calls isBooleanSortImpl().
38  virtual bool isBooleanSort() const { return isBooleanSortImpl(); }
39 
40  /// Returns the bitvector size, fails if the sort is not a bitvector
41  /// Calls getBitvectorSortSizeImpl().
42  virtual unsigned getBitvectorSortSize() const {
43  assert(isBitvectorSort() && "Not a bitvector sort!");
44  unsigned Size = getBitvectorSortSizeImpl();
45  assert(Size && "Size is zero!");
46  return Size;
47  };
48 
49  /// Returns the floating-point size, fails if the sort is not a floating-point
50  /// Calls getFloatSortSizeImpl().
51  virtual unsigned getFloatSortSize() const {
52  assert(isFloatSort() && "Not a floating-point sort!");
53  unsigned Size = getFloatSortSizeImpl();
54  assert(Size && "Size is zero!");
55  return Size;
56  };
57 
58  virtual void Profile(llvm::FoldingSetNodeID &ID) const = 0;
59 
60  bool operator<(const SMTSort &Other) const {
61  llvm::FoldingSetNodeID ID1, ID2;
62  Profile(ID1);
63  Other.Profile(ID2);
64  return ID1 < ID2;
65  }
66 
67  friend bool operator==(SMTSort const &LHS, SMTSort const &RHS) {
68  return LHS.equal_to(RHS);
69  }
70 
71  virtual void print(raw_ostream &OS) const = 0;
72 
73  LLVM_DUMP_METHOD void dump() const;
74 
75 protected:
76  /// Query the SMT solver and returns true if two sorts are equal (same kind
77  /// and bit width). This does not check if the two sorts are the same objects.
78  virtual bool equal_to(SMTSort const &other) const = 0;
79 
80  /// Query the SMT solver and checks if a sort is bitvector.
81  virtual bool isBitvectorSortImpl() const = 0;
82 
83  /// Query the SMT solver and checks if a sort is floating-point.
84  virtual bool isFloatSortImpl() const = 0;
85 
86  /// Query the SMT solver and checks if a sort is boolean.
87  virtual bool isBooleanSortImpl() const = 0;
88 
89  /// Query the SMT solver and returns the sort bit width.
90  virtual unsigned getBitvectorSortSizeImpl() const = 0;
91 
92  /// Query the SMT solver and returns the sort bit width.
93  virtual unsigned getFloatSortSizeImpl() const = 0;
94 };
95 
96 /// Shared pointer for SMTSorts, used by SMTSolver API.
97 using SMTSortRef = const SMTSort *;
98 
99 /// Generic base class for SMT exprs
100 class SMTExpr {
101 public:
102  SMTExpr() = default;
103  virtual ~SMTExpr() = default;
104 
105  bool operator<(const SMTExpr &Other) const {
106  llvm::FoldingSetNodeID ID1, ID2;
107  Profile(ID1);
108  Other.Profile(ID2);
109  return ID1 < ID2;
110  }
111 
112  virtual void Profile(llvm::FoldingSetNodeID &ID) const = 0;
113 
114  friend bool operator==(SMTExpr const &LHS, SMTExpr const &RHS) {
115  return LHS.equal_to(RHS);
116  }
117 
118  virtual void print(raw_ostream &OS) const = 0;
119 
120  LLVM_DUMP_METHOD void dump() const;
121 
122 protected:
123  /// Query the SMT solver and returns true if two sorts are equal (same kind
124  /// and bit width). This does not check if the two sorts are the same objects.
125  virtual bool equal_to(SMTExpr const &other) const = 0;
126 };
127 
128 /// Shared pointer for SMTExprs, used by SMTSolver API.
129 using SMTExprRef = const SMTExpr *;
130 
131 /// Generic base class for SMT Solvers
132 ///
133 /// This class is responsible for wrapping all sorts and expression generation,
134 /// through the mk* methods. It also provides methods to create SMT expressions
135 /// straight from clang's AST, through the from* methods.
136 class SMTSolver {
137 public:
138  SMTSolver() = default;
139  virtual ~SMTSolver() = default;
140 
141  LLVM_DUMP_METHOD void dump() const;
142 
143  // Returns an appropriate floating-point sort for the given bitwidth.
145  switch (BitWidth) {
146  case 16:
147  return getFloat16Sort();
148  case 32:
149  return getFloat32Sort();
150  case 64:
151  return getFloat64Sort();
152  case 128:
153  return getFloat128Sort();
154  default:;
155  }
156  llvm_unreachable("Unsupported floating-point bitwidth!");
157  }
158 
159  // Returns a boolean sort.
160  virtual SMTSortRef getBoolSort() = 0;
161 
162  // Returns an appropriate bitvector sort for the given bitwidth.
163  virtual SMTSortRef getBitvectorSort(const unsigned BitWidth) = 0;
164 
165  // Returns a floating-point sort of width 16
166  virtual SMTSortRef getFloat16Sort() = 0;
167 
168  // Returns a floating-point sort of width 32
169  virtual SMTSortRef getFloat32Sort() = 0;
170 
171  // Returns a floating-point sort of width 64
172  virtual SMTSortRef getFloat64Sort() = 0;
173 
174  // Returns a floating-point sort of width 128
175  virtual SMTSortRef getFloat128Sort() = 0;
176 
177  // Returns an appropriate sort for the given AST.
178  virtual SMTSortRef getSort(const SMTExprRef &AST) = 0;
179 
180  /// Given a constraint, adds it to the solver
181  virtual void addConstraint(const SMTExprRef &Exp) const = 0;
182 
183  /// Creates a bitvector addition operation
184  virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
185 
186  /// Creates a bitvector subtraction operation
187  virtual SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
188 
189  /// Creates a bitvector multiplication operation
190  virtual SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
191 
192  /// Creates a bitvector signed modulus operation
193  virtual SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
194 
195  /// Creates a bitvector unsigned modulus operation
196  virtual SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
197 
198  /// Creates a bitvector signed division operation
199  virtual SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
200 
201  /// Creates a bitvector unsigned division operation
202  virtual SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
203 
204  /// Creates a bitvector logical shift left operation
205  virtual SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
206 
207  /// Creates a bitvector arithmetic shift right operation
208  virtual SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
209 
210  /// Creates a bitvector logical shift right operation
211  virtual SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
212 
213  /// Creates a bitvector negation operation
214  virtual SMTExprRef mkBVNeg(const SMTExprRef &Exp) = 0;
215 
216  /// Creates a bitvector not operation
217  virtual SMTExprRef mkBVNot(const SMTExprRef &Exp) = 0;
218 
219  /// Creates a bitvector xor operation
220  virtual SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
221 
222  /// Creates a bitvector or operation
223  virtual SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
224 
225  /// Creates a bitvector and operation
226  virtual SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
227 
228  /// Creates a bitvector unsigned less-than operation
229  virtual SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
230 
231  /// Creates a bitvector signed less-than operation
232  virtual SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
233 
234  /// Creates a bitvector unsigned greater-than operation
235  virtual SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
236 
237  /// Creates a bitvector signed greater-than operation
238  virtual SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
239 
240  /// Creates a bitvector unsigned less-equal-than operation
241  virtual SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
242 
243  /// Creates a bitvector signed less-equal-than operation
244  virtual SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
245 
246  /// Creates a bitvector unsigned greater-equal-than operation
247  virtual SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
248 
249  /// Creates a bitvector signed greater-equal-than operation
250  virtual SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
251 
252  /// Creates a boolean not operation
253  virtual SMTExprRef mkNot(const SMTExprRef &Exp) = 0;
254 
255  /// Creates a boolean equality operation
256  virtual SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
257 
258  /// Creates a boolean and operation
259  virtual SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
260 
261  /// Creates a boolean or operation
262  virtual SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
263 
264  /// Creates a boolean ite operation
265  virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
266  const SMTExprRef &F) = 0;
267 
268  /// Creates a bitvector sign extension operation
269  virtual SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) = 0;
270 
271  /// Creates a bitvector zero extension operation
272  virtual SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) = 0;
273 
274  /// Creates a bitvector extract operation
275  virtual SMTExprRef mkBVExtract(unsigned High, unsigned Low,
276  const SMTExprRef &Exp) = 0;
277 
278  /// Creates a bitvector concat operation
279  virtual SMTExprRef mkBVConcat(const SMTExprRef &LHS,
280  const SMTExprRef &RHS) = 0;
281 
282  /// Creates a predicate that checks for overflow in a bitvector addition
283  /// operation
284  virtual SMTExprRef mkBVAddNoOverflow(const SMTExprRef &LHS,
285  const SMTExprRef &RHS,
286  bool isSigned) = 0;
287 
288  /// Creates a predicate that checks for underflow in a signed bitvector
289  /// addition operation
290  virtual SMTExprRef mkBVAddNoUnderflow(const SMTExprRef &LHS,
291  const SMTExprRef &RHS) = 0;
292 
293  /// Creates a predicate that checks for overflow in a signed bitvector
294  /// subtraction operation
295  virtual SMTExprRef mkBVSubNoOverflow(const SMTExprRef &LHS,
296  const SMTExprRef &RHS) = 0;
297 
298  /// Creates a predicate that checks for underflow in a bitvector subtraction
299  /// operation
300  virtual SMTExprRef mkBVSubNoUnderflow(const SMTExprRef &LHS,
301  const SMTExprRef &RHS,
302  bool isSigned) = 0;
303 
304  /// Creates a predicate that checks for overflow in a signed bitvector
305  /// division/modulus operation
306  virtual SMTExprRef mkBVSDivNoOverflow(const SMTExprRef &LHS,
307  const SMTExprRef &RHS) = 0;
308 
309  /// Creates a predicate that checks for overflow in a bitvector negation
310  /// operation
311  virtual SMTExprRef mkBVNegNoOverflow(const SMTExprRef &Exp) = 0;
312 
313  /// Creates a predicate that checks for overflow in a bitvector multiplication
314  /// operation
315  virtual SMTExprRef mkBVMulNoOverflow(const SMTExprRef &LHS,
316  const SMTExprRef &RHS,
317  bool isSigned) = 0;
318 
319  /// Creates a predicate that checks for underflow in a signed bitvector
320  /// multiplication operation
321  virtual SMTExprRef mkBVMulNoUnderflow(const SMTExprRef &LHS,
322  const SMTExprRef &RHS) = 0;
323 
324  /// Creates a floating-point negation operation
325  virtual SMTExprRef mkFPNeg(const SMTExprRef &Exp) = 0;
326 
327  /// Creates a floating-point isInfinite operation
328  virtual SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) = 0;
329 
330  /// Creates a floating-point isNaN operation
331  virtual SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) = 0;
332 
333  /// Creates a floating-point isNormal operation
334  virtual SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) = 0;
335 
336  /// Creates a floating-point isZero operation
337  virtual SMTExprRef mkFPIsZero(const SMTExprRef &Exp) = 0;
338 
339  /// Creates a floating-point multiplication operation
340  virtual SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
341 
342  /// Creates a floating-point division operation
343  virtual SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
344 
345  /// Creates a floating-point remainder operation
346  virtual SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
347 
348  /// Creates a floating-point addition operation
349  virtual SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
350 
351  /// Creates a floating-point subtraction operation
352  virtual SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
353 
354  /// Creates a floating-point less-than operation
355  virtual SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
356 
357  /// Creates a floating-point greater-than operation
358  virtual SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
359 
360  /// Creates a floating-point less-than-or-equal operation
361  virtual SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
362 
363  /// Creates a floating-point greater-than-or-equal operation
364  virtual SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
365 
366  /// Creates a floating-point equality operation
367  virtual SMTExprRef mkFPEqual(const SMTExprRef &LHS,
368  const SMTExprRef &RHS) = 0;
369 
370  /// Creates a floating-point conversion from floatint-point to floating-point
371  /// operation
372  virtual SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) = 0;
373 
374  /// Creates a floating-point conversion from signed bitvector to
375  /// floatint-point operation
376  virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From,
377  const SMTSortRef &To) = 0;
378 
379  /// Creates a floating-point conversion from unsigned bitvector to
380  /// floatint-point operation
381  virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From,
382  const SMTSortRef &To) = 0;
383 
384  /// Creates a floating-point conversion from floatint-point to signed
385  /// bitvector operation
386  virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth) = 0;
387 
388  /// Creates a floating-point conversion from floatint-point to unsigned
389  /// bitvector operation
390  virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth) = 0;
391 
392  /// Creates a new symbol, given a name and a sort
393  virtual SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) = 0;
394 
395  // Returns an appropriate floating-point rounding mode.
396  virtual SMTExprRef getFloatRoundingMode() = 0;
397 
398  // If the a model is available, returns the value of a given bitvector symbol
399  virtual llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth,
400  bool isUnsigned) = 0;
401 
402  // If the a model is available, returns the value of a given boolean symbol
403  virtual bool getBoolean(const SMTExprRef &Exp) = 0;
404 
405  /// Constructs an SMTExprRef from a boolean.
406  virtual SMTExprRef mkBoolean(const bool b) = 0;
407 
408  /// Constructs an SMTExprRef from a finite APFloat.
409  virtual SMTExprRef mkFloat(const llvm::APFloat Float) = 0;
410 
411  /// Constructs an SMTExprRef from an APSInt and its bit width
412  virtual SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) = 0;
413 
414  /// Given an expression, extract the value of this operand in the model.
415  virtual bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) = 0;
416 
417  /// Given an expression extract the value of this operand in the model.
418  virtual bool getInterpretation(const SMTExprRef &Exp,
419  llvm::APFloat &Float) = 0;
420 
421  /// Check if the constraints are satisfiable
422  virtual Optional<bool> check() const = 0;
423 
424  /// Push the current solver state
425  virtual void push() = 0;
426 
427  /// Pop the previous solver state
428  virtual void pop(unsigned NumStates = 1) = 0;
429 
430  /// Reset the solver and remove all constraints.
431  virtual void reset() = 0;
432 
433  /// Checks if the solver supports floating-points.
434  virtual bool isFPSupported() = 0;
435 
436  virtual void print(raw_ostream &OS) const = 0;
437 };
438 
439 /// Shared pointer for SMTSolvers.
440 using SMTSolverRef = std::shared_ptr<SMTSolver>;
441 
442 /// Convenience method to create and Z3Solver object
444 
445 } // namespace llvm
446 
447 #endif
llvm::Check::Size
@ Size
Definition: FileCheck.h:73
i
i
Definition: README.txt:29
llvm::SMTSolver::mkBVSub
virtual SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector subtraction operation.
llvm::SMTSolver
Generic base class for SMT Solvers.
Definition: SMTAPI.h:136
llvm::SMTSolver::mkFPEqual
virtual SMTExprRef mkFPEqual(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point equality operation.
llvm::SMTSolver::mkFPRem
virtual SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point remainder operation.
LLVM_DUMP_METHOD
#define LLVM_DUMP_METHOD
Mark debug helper function definitions like dump() that should not be stripped from debug builds.
Definition: Compiler.h:491
llvm::SMTSolver::mkFPGt
virtual SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point greater-than operation.
llvm
---------------------— PointerInfo ------------------------------------—
Definition: AllocatorList.h:23
llvm::SMTSolver::mkIte
virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T, const SMTExprRef &F)=0
Creates a boolean ite operation.
llvm::SMTSolver::mkBVMul
virtual SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector multiplication operation.
llvm::SMTSolver::mkBVXor
virtual SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector xor operation.
llvm::SMTSolver::mkBVSubNoUnderflow
virtual SMTExprRef mkBVSubNoUnderflow(const SMTExprRef &LHS, const SMTExprRef &RHS, bool isSigned)=0
Creates a predicate that checks for underflow in a bitvector subtraction operation.
llvm::SMTSolver::mkBVMulNoOverflow
virtual SMTExprRef mkBVMulNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS, bool isSigned)=0
Creates a predicate that checks for overflow in a bitvector multiplication operation.
llvm::SMTSolver::mkFPtoFP
virtual SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To)=0
Creates a floating-point conversion from floatint-point to floating-point operation.
llvm::SMTSolver::mkFloat
virtual SMTExprRef mkFloat(const llvm::APFloat Float)=0
Constructs an SMTExprRef from a finite APFloat.
llvm::SMTSolver::mkFPIsInfinite
virtual SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp)=0
Creates a floating-point isInfinite operation.
High
uint64_t High
Definition: NVVMIntrRange.cpp:61
llvm::SMTSolver::mkFPIsNaN
virtual SMTExprRef mkFPIsNaN(const SMTExprRef &Exp)=0
Creates a floating-point isNaN operation.
llvm::CreateZ3Solver
SMTSolverRef CreateZ3Solver()
Convenience method to create and Z3Solver object.
Definition: Z3Solver.cpp:903
llvm::SMTSort::isBitvectorSortImpl
virtual bool isBitvectorSortImpl() const =0
Query the SMT solver and checks if a sort is bitvector.
llvm::SMTSolver::pop
virtual void pop(unsigned NumStates=1)=0
Pop the previous solver state.
llvm::SMTSolver::mkBVSle
virtual SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed less-equal-than operation.
llvm::SMTSolver::getFloat32Sort
virtual SMTSortRef getFloat32Sort()=0
llvm::SMTSolver::mkBVUDiv
virtual SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned division operation.
llvm::SMTSolver::mkBVURem
virtual SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned modulus operation.
llvm::SMTSolver::mkFPNeg
virtual SMTExprRef mkFPNeg(const SMTExprRef &Exp)=0
Creates a floating-point negation operation.
llvm::SMTSolver::mkSymbol
virtual SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort)=0
Creates a new symbol, given a name and a sort.
llvm::Optional< bool >
llvm::SMTSolver::mkFPIsNormal
virtual SMTExprRef mkFPIsNormal(const SMTExprRef &Exp)=0
Creates a floating-point isNormal operation.
llvm::SMTSolver::mkBVSignExt
virtual SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp)=0
Creates a bitvector sign extension operation.
llvm::SMTSolver::mkBVAnd
virtual SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector and operation.
llvm::SMTSolver::mkBVZeroExt
virtual SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp)=0
Creates a bitvector zero extension operation.
llvm::SMTSolver::mkBVOr
virtual SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector or operation.
llvm::SMTSolver::mkBVShl
virtual SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector logical shift left operation.
llvm::SMTSolver::check
virtual Optional< bool > check() const =0
Check if the constraints are satisfiable.
llvm::SMTSolver::mkFPDiv
virtual SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point division operation.
F
#define F(x, y, z)
Definition: MD5.cpp:56
llvm::SMTSolver::mkBVNegNoOverflow
virtual SMTExprRef mkBVNegNoOverflow(const SMTExprRef &Exp)=0
Creates a predicate that checks for overflow in a bitvector negation operation.
llvm::SMTSolver::mkBitvector
virtual SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth)=0
Constructs an SMTExprRef from an APSInt and its bit width.
llvm::SMTSolver::mkEqual
virtual SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a boolean equality operation.
llvm::SMTSolver::reset
virtual void reset()=0
Reset the solver and remove all constraints.
llvm::SMTSort::getBitvectorSortSizeImpl
virtual unsigned getBitvectorSortSizeImpl() const =0
Query the SMT solver and returns the sort bit width.
llvm::SMTSort::getBitvectorSortSize
virtual unsigned getBitvectorSortSize() const
Returns the bitvector size, fails if the sort is not a bitvector Calls getBitvectorSortSizeImpl().
Definition: SMTAPI.h:42
llvm::SMTSolver::mkBVExtract
virtual SMTExprRef mkBVExtract(unsigned High, unsigned Low, const SMTExprRef &Exp)=0
Creates a bitvector extract operation.
llvm::SMTSolver::getBitvector
virtual llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth, bool isUnsigned)=0
llvm::SMTSolver::mkBVLshr
virtual SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector logical shift right operation.
llvm::SMTSolver::mkBVSgt
virtual SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed greater-than operation.
b
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
Definition: README.txt:418
llvm::SMTSolver::mkFPIsZero
virtual SMTExprRef mkFPIsZero(const SMTExprRef &Exp)=0
Creates a floating-point isZero operation.
llvm::SMTSort::equal_to
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).
llvm::SMTSolver::addConstraint
virtual void addConstraint(const SMTExprRef &Exp) const =0
Given a constraint, adds it to the solver.
llvm::APSInt
An arbitrary precision integer that knows its signedness.
Definition: APSInt.h:22
llvm::raw_ostream
This class implements an extremely fast bulk output stream that can only output to a stream.
Definition: raw_ostream.h:53
APFloat.h
This file declares a class to represent arbitrary precision floating point values and provide a varie...
llvm::SMTExpr::dump
LLVM_DUMP_METHOD void dump() const
Definition: Z3Solver.cpp:915
llvm::SMTExpr::operator<
bool operator<(const SMTExpr &Other) const
Definition: SMTAPI.h:105
llvm::SMTExpr::print
virtual void print(raw_ostream &OS) const =0
llvm::SMTSolver::mkBVUle
virtual SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned less-equal-than operation.
llvm::SMTSolver::mkBVSDiv
virtual SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed division operation.
llvm::SMTSolver::getSort
virtual SMTSortRef getSort(const SMTExprRef &AST)=0
llvm::APFloat
Definition: APFloat.h:701
llvm::SMTSolver::getFloat64Sort
virtual SMTSortRef getFloat64Sort()=0
llvm::SMTSolver::mkBVSlt
virtual SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed less-than operation.
llvm::SMTSolver::mkBVAshr
virtual SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector arithmetic shift right operation.
llvm::SMTSolver::getInterpretation
virtual bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int)=0
Given an expression, extract the value of this operand in the model.
llvm::SMTSolver::getBoolSort
virtual SMTSortRef getBoolSort()=0
llvm::SMTSolverRef
std::shared_ptr< SMTSolver > SMTSolverRef
Shared pointer for SMTSolvers.
Definition: SMTAPI.h:440
llvm::SMTSort::isBooleanSortImpl
virtual bool isBooleanSortImpl() const =0
Query the SMT solver and checks if a sort is boolean.
llvm::SMTExpr
Generic base class for SMT exprs.
Definition: SMTAPI.h:100
llvm::SMTSolver::SMTSolver
SMTSolver()=default
llvm::SMTSort::isFloatSortImpl
virtual bool isFloatSortImpl() const =0
Query the SMT solver and checks if a sort is floating-point.
llvm::SMTSort::getFloatSortSize
virtual unsigned getFloatSortSize() const
Returns the floating-point size, fails if the sort is not a floating-point Calls getFloatSortSizeImpl...
Definition: SMTAPI.h:51
llvm::SMTSolver::getBoolean
virtual bool getBoolean(const SMTExprRef &Exp)=0
llvm::SMTSolver::~SMTSolver
virtual ~SMTSolver()=default
llvm::SMTSolver::getFloatSort
SMTSortRef getFloatSort(unsigned BitWidth)
Definition: SMTAPI.h:144
llvm::SMTSolver::mkSBVtoFP
virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From, const SMTSortRef &To)=0
Creates a floating-point conversion from signed bitvector to floatint-point operation.
llvm::SMTSolver::mkBVAddNoOverflow
virtual SMTExprRef mkBVAddNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS, bool isSigned)=0
Creates a predicate that checks for overflow in a bitvector addition operation.
llvm::SMTSolver::mkUBVtoFP
virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From, const SMTSortRef &To)=0
Creates a floating-point conversion from unsigned bitvector to floatint-point operation.
llvm::SMTSort::getFloatSortSizeImpl
virtual unsigned getFloatSortSizeImpl() const =0
Query the SMT solver and returns the sort bit width.
llvm::SMTSort::print
virtual void print(raw_ostream &OS) const =0
llvm::SMTSolver::mkFPtoUBV
virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth)=0
Creates a floating-point conversion from floatint-point to unsigned bitvector operation.
llvm::SMTSolver::push
virtual void push()=0
Push the current solver state.
assert
assert(ImpDefSCC.getReg()==AMDGPU::SCC &&ImpDefSCC.isDef())
llvm::SMTSolver::print
virtual void print(raw_ostream &OS) const =0
APSInt.h
llvm::SMTSolver::mkBVMulNoUnderflow
virtual SMTExprRef mkBVMulNoUnderflow(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a predicate that checks for underflow in a signed bitvector multiplication operation.
llvm::SMTSolver::mkFPLe
virtual SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point less-than-or-equal operation.
llvm::SMTSort::operator<
bool operator<(const SMTSort &Other) const
Definition: SMTAPI.h:60
llvm::SMTSolver::mkBVSDivNoOverflow
virtual SMTExprRef mkBVSDivNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a predicate that checks for overflow in a signed bitvector division/modulus operation.
llvm::SMTSort::~SMTSort
virtual ~SMTSort()=default
Cond
SmallVector< MachineOperand, 4 > Cond
Definition: BasicBlockSections.cpp:179
llvm_unreachable
#define llvm_unreachable(msg)
Marks that the current location is not supposed to be reachable.
Definition: ErrorHandling.h:136
llvm::SMTExpr::Profile
virtual void Profile(llvm::FoldingSetNodeID &ID) const =0
llvm::SMTSort::dump
LLVM_DUMP_METHOD void dump() const
Definition: Z3Solver.cpp:914
llvm::SMTSolver::mkBVNeg
virtual SMTExprRef mkBVNeg(const SMTExprRef &Exp)=0
Creates a bitvector negation operation.
llvm::FoldingSetNodeID
FoldingSetNodeID - This class is used to gather all the unique data bits of a node.
Definition: FoldingSet.h:313
llvm::SMTSolver::mkBVUgt
virtual SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned greater-than operation.
FoldingSet.h
llvm::SMTSolver::getFloatRoundingMode
virtual SMTExprRef getFloatRoundingMode()=0
llvm::SMTSolver::mkBVConcat
virtual SMTExprRef mkBVConcat(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector concat operation.
llvm::SMTSolver::mkBVUge
virtual SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned greater-equal-than operation.
llvm::SMTSolver::mkFPtoSBV
virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth)=0
Creates a floating-point conversion from floatint-point to signed bitvector operation.
llvm::GraphProgram::Name
Name
Definition: GraphWriter.h:52
llvm::SMTSolver::getBitvectorSort
virtual SMTSortRef getBitvectorSort(const unsigned BitWidth)=0
llvm::SMTSort::Profile
virtual void Profile(llvm::FoldingSetNodeID &ID) const =0
llvm::SMTSolver::mkFPAdd
virtual SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point addition operation.
llvm::SMTSolver::mkAnd
virtual SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a boolean and operation.
llvm::SMTSolver::mkBVAddNoUnderflow
virtual SMTExprRef mkBVAddNoUnderflow(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a predicate that checks for underflow in a signed bitvector addition operation.
llvm::BitWidth
constexpr unsigned BitWidth
Definition: BitmaskEnum.h:147
llvm::SMTSolver::mkBVAdd
virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector addition operation.
llvm::SMTSolver::isFPSupported
virtual bool isFPSupported()=0
Checks if the solver supports floating-points.
llvm::SMTSolver::mkFPGe
virtual SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point greater-than-or-equal operation.
llvm::SMTSort::operator==
friend bool operator==(SMTSort const &LHS, SMTSort const &RHS)
Definition: SMTAPI.h:67
llvm::SMTExpr::~SMTExpr
virtual ~SMTExpr()=default
llvm::SMTSolver::mkBoolean
virtual SMTExprRef mkBoolean(const bool b)=0
Constructs an SMTExprRef from a boolean.
llvm::SMTSolver::mkBVNot
virtual SMTExprRef mkBVNot(const SMTExprRef &Exp)=0
Creates a bitvector not operation.
llvm::SMTSolver::mkBVUlt
virtual SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned less-than operation.
llvm::SMTSolver::dump
LLVM_DUMP_METHOD void dump() const
Definition: Z3Solver.cpp:916
llvm::SMTSolver::mkBVSRem
virtual SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed modulus operation.
llvm::SMTSort::SMTSort
SMTSort()=default
llvm::SMTSort::isBitvectorSort
virtual bool isBitvectorSort() const
Returns true if the sort is a bitvector, calls isBitvectorSortImpl().
Definition: SMTAPI.h:32
llvm::SMTSolver::getFloat16Sort
virtual SMTSortRef getFloat16Sort()=0
llvm::SMTSolver::mkBVSge
virtual SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed greater-equal-than operation.
llvm::SMTSolver::mkFPSub
virtual SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point subtraction operation.
llvm::SMTSort::isFloatSort
virtual bool isFloatSort() const
Returns true if the sort is a floating-point, calls isFloatSortImpl().
Definition: SMTAPI.h:35
llvm::SMTSolver::getFloat128Sort
virtual SMTSortRef getFloat128Sort()=0
llvm::SMTExpr::SMTExpr
SMTExpr()=default
llvm::SMTExpr::equal_to
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).
llvm::SMTSolver::mkBVSubNoOverflow
virtual SMTExprRef mkBVSubNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a predicate that checks for overflow in a signed bitvector subtraction operation.
llvm::SMTSolver::mkOr
virtual SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a boolean or operation.
llvm::SMTSolver::mkNot
virtual SMTExprRef mkNot(const SMTExprRef &Exp)=0
Creates a boolean not operation.
From
BlockVerifier::State From
Definition: BlockVerifier.cpp:55
raw_ostream.h
llvm::SMTSort::isBooleanSort
virtual bool isBooleanSort() const
Returns true if the sort is a boolean, calls isBooleanSortImpl().
Definition: SMTAPI.h:38
llvm::SMTSort
Generic base class for SMT sorts.
Definition: SMTAPI.h:26
llvm::SMTSolver::mkFPMul
virtual SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point multiplication operation.
llvm::SMTExpr::operator==
friend bool operator==(SMTExpr const &LHS, SMTExpr const &RHS)
Definition: SMTAPI.h:114
llvm::SMTSolver::mkFPLt
virtual SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point less-than operation.
Other
Optional< std::vector< StOtherPiece > > Other
Definition: ELFYAML.cpp:1172
llvm::Intrinsic::ID
unsigned ID
Definition: TargetTransformInfo.h:37