LLVM  9.0.0svn
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.
144  SMTSortRef getFloatSort(unsigned 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
virtual bool isBitvectorSortImpl() const =0
Query the SMT solver and checks if a sort is bitvector.
virtual unsigned getFloatSortSize() const
Returns the floating-point size, fails if the sort is not a floating-point Calls getFloatSortSizeImpl...
Definition: SMTAPI.h:51
This class represents lattice values for constants.
Definition: AllocatorList.h:23
#define LLVM_DUMP_METHOD
Mark debug helper function definitions like dump() that should not be stripped from debug builds...
Definition: Compiler.h:473
virtual void print(raw_ostream &OS) const =0
amdgpu Simplify well known AMD library false FunctionCallee Value const Twine & Name
SMTSort()=default
F(f)
LLVM_DUMP_METHOD void dump() const
Definition: Z3Solver.cpp:898
uint64_t High
Generic base class for SMT exprs.
Definition: SMTAPI.h:100
Generic base class for SMT Solvers.
Definition: SMTAPI.h:136
FoldingSetNodeID - This class is used to gather all the unique data bits of a node.
Definition: FoldingSet.h:305
friend bool operator==(SMTExpr const &LHS, SMTExpr const &RHS)
Definition: SMTAPI.h:114
virtual bool isBooleanSort() const
Returns true if the sort is a boolean, calls isBooleanSortImpl().
Definition: SMTAPI.h:38
This file declares a class to represent arbitrary precision floating point values and provide a varie...
bool operator<(const SMTSort &Other) const
Definition: SMTAPI.h:60
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).
#define llvm_unreachable(msg)
Marks that the current location is not supposed to be reachable.
virtual unsigned getBitvectorSortSizeImpl() const =0
Query the SMT solver and returns the sort bit width.
BlockVerifier::State From
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 bool isBitvectorSort() const
Returns true if the sort is a bitvector, calls isBitvectorSortImpl().
Definition: SMTAPI.h:32
virtual bool isFloatSort() const
Returns true if the sort is a floating-point, calls isFloatSortImpl().
Definition: SMTAPI.h:35
virtual ~SMTSort()=default
virtual unsigned getBitvectorSortSize() const
Returns the bitvector size, fails if the sort is not a bitvector Calls getBitvectorSortSizeImpl().
Definition: SMTAPI.h:42
Generic base class for SMT sorts.
Definition: SMTAPI.h:26
uint32_t Size
Definition: Profile.cpp:46
virtual bool isBooleanSortImpl() const =0
Query the SMT solver and checks if a sort is boolean.
virtual bool isFloatSortImpl() const =0
Query the SMT solver and checks if a sort is floating-point.
assert(ImpDefSCC.getReg()==AMDGPU::SCC &&ImpDefSCC.isDef())
virtual unsigned getFloatSortSizeImpl() const =0
Query the SMT solver and returns the sort bit width.
virtual void Profile(llvm::FoldingSetNodeID &ID) const =0
SMTSolverRef CreateZ3Solver()
Convenience method to create and Z3Solver object.
Definition: Z3Solver.cpp:887
SMTSortRef getFloatSort(unsigned BitWidth)
Definition: SMTAPI.h:144
This class implements an extremely fast bulk output stream that can only output to a stream...
Definition: raw_ostream.h:45
virtual void Profile(llvm::FoldingSetNodeID &ID) const =0
friend bool operator==(SMTSort const &LHS, SMTSort const &RHS)
Definition: SMTAPI.h:67
std::shared_ptr< SMTSolver > SMTSolverRef
Shared pointer for SMTSolvers.
Definition: SMTAPI.h:440
bool operator<(const SMTExpr &Other) const
Definition: SMTAPI.h:105