clang  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_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
15 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
16 
17 #include "clang/Basic/TargetInfo.h"
18 #include "llvm/ADT/APSInt.h"
19 #include "llvm/ADT/FoldingSet.h"
20 
21 namespace clang {
22 namespace ento {
23 
24 /// Generic base class for SMT sorts
25 class SMTSort {
26 public:
27  SMTSort() = default;
28  virtual ~SMTSort() = default;
29 
30  /// Returns true if the sort is a bitvector, calls isBitvectorSortImpl().
31  virtual bool isBitvectorSort() const { return isBitvectorSortImpl(); }
32 
33  /// Returns true if the sort is a floating-point, calls isFloatSortImpl().
34  virtual bool isFloatSort() const { return isFloatSortImpl(); }
35 
36  /// Returns true if the sort is a boolean, calls isBooleanSortImpl().
37  virtual bool isBooleanSort() const { return isBooleanSortImpl(); }
38 
39  /// Returns the bitvector size, fails if the sort is not a bitvector
40  /// Calls getBitvectorSortSizeImpl().
41  virtual unsigned getBitvectorSortSize() const {
42  assert(isBitvectorSort() && "Not a bitvector sort!");
43  unsigned Size = getBitvectorSortSizeImpl();
44  assert(Size && "Size is zero!");
45  return Size;
46  };
47 
48  /// Returns the floating-point size, fails if the sort is not a floating-point
49  /// Calls getFloatSortSizeImpl().
50  virtual unsigned getFloatSortSize() const {
51  assert(isFloatSort() && "Not a floating-point sort!");
52  unsigned Size = getFloatSortSizeImpl();
53  assert(Size && "Size is zero!");
54  return Size;
55  };
56 
57  virtual void Profile(llvm::FoldingSetNodeID &ID) const = 0;
58 
59  bool operator<(const SMTSort &Other) const {
60  llvm::FoldingSetNodeID ID1, ID2;
61  Profile(ID1);
62  Other.Profile(ID2);
63  return ID1 < ID2;
64  }
65 
66  friend bool operator==(SMTSort const &LHS, SMTSort const &RHS) {
67  return LHS.equal_to(RHS);
68  }
69 
70  virtual void print(raw_ostream &OS) const = 0;
71 
72  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
73 
74 protected:
75  /// Query the SMT solver and returns true if two sorts are equal (same kind
76  /// and bit width). This does not check if the two sorts are the same objects.
77  virtual bool equal_to(SMTSort const &other) const = 0;
78 
79  /// Query the SMT solver and checks if a sort is bitvector.
80  virtual bool isBitvectorSortImpl() const = 0;
81 
82  /// Query the SMT solver and checks if a sort is floating-point.
83  virtual bool isFloatSortImpl() const = 0;
84 
85  /// Query the SMT solver and checks if a sort is boolean.
86  virtual bool isBooleanSortImpl() const = 0;
87 
88  /// Query the SMT solver and returns the sort bit width.
89  virtual unsigned getBitvectorSortSizeImpl() const = 0;
90 
91  /// Query the SMT solver and returns the sort bit width.
92  virtual unsigned getFloatSortSizeImpl() const = 0;
93 };
94 
95 /// Shared pointer for SMTSorts, used by SMTSolver API.
96 using SMTSortRef = const SMTSort *;
97 
98 /// Generic base class for SMT exprs
99 class SMTExpr {
100 public:
101  SMTExpr() = default;
102  virtual ~SMTExpr() = default;
103 
104  bool operator<(const SMTExpr &Other) const {
105  llvm::FoldingSetNodeID ID1, ID2;
106  Profile(ID1);
107  Other.Profile(ID2);
108  return ID1 < ID2;
109  }
110 
111  virtual void Profile(llvm::FoldingSetNodeID &ID) const = 0;
112 
113  friend bool operator==(SMTExpr const &LHS, SMTExpr const &RHS) {
114  return LHS.equal_to(RHS);
115  }
116 
117  virtual void print(raw_ostream &OS) const = 0;
118 
119  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
120 
121 protected:
122  /// Query the SMT solver and returns true if two sorts are equal (same kind
123  /// and bit width). This does not check if the two sorts are the same objects.
124  virtual bool equal_to(SMTExpr const &other) const = 0;
125 };
126 
127 /// Shared pointer for SMTExprs, used by SMTSolver API.
128 using SMTExprRef = const SMTExpr *;
129 
130 /// Generic base class for SMT Solvers
131 ///
132 /// This class is responsible for wrapping all sorts and expression generation,
133 /// through the mk* methods. It also provides methods to create SMT expressions
134 /// straight from clang's AST, through the from* methods.
135 class SMTSolver {
136 public:
137  SMTSolver() = default;
138  virtual ~SMTSolver() = default;
139 
140  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
141 
142  // Returns an appropriate floating-point sort for the given bitwidth.
143  SMTSortRef getFloatSort(unsigned BitWidth) {
144  switch (BitWidth) {
145  case 16:
146  return getFloat16Sort();
147  case 32:
148  return getFloat32Sort();
149  case 64:
150  return getFloat64Sort();
151  case 128:
152  return getFloat128Sort();
153  default:;
154  }
155  llvm_unreachable("Unsupported floating-point bitwidth!");
156  }
157 
158  // Returns a boolean sort.
159  virtual SMTSortRef getBoolSort() = 0;
160 
161  // Returns an appropriate bitvector sort for the given bitwidth.
162  virtual SMTSortRef getBitvectorSort(const unsigned BitWidth) = 0;
163 
164  // Returns a floating-point sort of width 16
165  virtual SMTSortRef getFloat16Sort() = 0;
166 
167  // Returns a floating-point sort of width 32
168  virtual SMTSortRef getFloat32Sort() = 0;
169 
170  // Returns a floating-point sort of width 64
171  virtual SMTSortRef getFloat64Sort() = 0;
172 
173  // Returns a floating-point sort of width 128
174  virtual SMTSortRef getFloat128Sort() = 0;
175 
176  // Returns an appropriate sort for the given AST.
177  virtual SMTSortRef getSort(const SMTExprRef &AST) = 0;
178 
179  /// Given a constraint, adds it to the solver
180  virtual void addConstraint(const SMTExprRef &Exp) const = 0;
181 
182  /// Creates a bitvector addition operation
183  virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
184 
185  /// Creates a bitvector subtraction operation
186  virtual SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
187 
188  /// Creates a bitvector multiplication operation
189  virtual SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
190 
191  /// Creates a bitvector signed modulus operation
192  virtual SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
193 
194  /// Creates a bitvector unsigned modulus operation
195  virtual SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
196 
197  /// Creates a bitvector signed division operation
198  virtual SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
199 
200  /// Creates a bitvector unsigned division operation
201  virtual SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
202 
203  /// Creates a bitvector logical shift left operation
204  virtual SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
205 
206  /// Creates a bitvector arithmetic shift right operation
207  virtual SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
208 
209  /// Creates a bitvector logical shift right operation
210  virtual SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
211 
212  /// Creates a bitvector negation operation
213  virtual SMTExprRef mkBVNeg(const SMTExprRef &Exp) = 0;
214 
215  /// Creates a bitvector not operation
216  virtual SMTExprRef mkBVNot(const SMTExprRef &Exp) = 0;
217 
218  /// Creates a bitvector xor operation
219  virtual SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
220 
221  /// Creates a bitvector or operation
222  virtual SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
223 
224  /// Creates a bitvector and operation
225  virtual SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
226 
227  /// Creates a bitvector unsigned less-than operation
228  virtual SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
229 
230  /// Creates a bitvector signed less-than operation
231  virtual SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
232 
233  /// Creates a bitvector unsigned greater-than operation
234  virtual SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
235 
236  /// Creates a bitvector signed greater-than operation
237  virtual SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
238 
239  /// Creates a bitvector unsigned less-equal-than operation
240  virtual SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
241 
242  /// Creates a bitvector signed less-equal-than operation
243  virtual SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
244 
245  /// Creates a bitvector unsigned greater-equal-than operation
246  virtual SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
247 
248  /// Creates a bitvector signed greater-equal-than operation
249  virtual SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
250 
251  /// Creates a boolean not operation
252  virtual SMTExprRef mkNot(const SMTExprRef &Exp) = 0;
253 
254  /// Creates a boolean equality operation
255  virtual SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
256 
257  /// Creates a boolean and operation
258  virtual SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
259 
260  /// Creates a boolean or operation
261  virtual SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
262 
263  /// Creates a boolean ite operation
264  virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
265  const SMTExprRef &F) = 0;
266 
267  /// Creates a bitvector sign extension operation
268  virtual SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) = 0;
269 
270  /// Creates a bitvector zero extension operation
271  virtual SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) = 0;
272 
273  /// Creates a bitvector extract operation
274  virtual SMTExprRef mkBVExtract(unsigned High, unsigned Low,
275  const SMTExprRef &Exp) = 0;
276 
277  /// Creates a bitvector concat operation
278  virtual SMTExprRef mkBVConcat(const SMTExprRef &LHS,
279  const SMTExprRef &RHS) = 0;
280 
281  /// Creates a floating-point negation operation
282  virtual SMTExprRef mkFPNeg(const SMTExprRef &Exp) = 0;
283 
284  /// Creates a floating-point isInfinite operation
285  virtual SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) = 0;
286 
287  /// Creates a floating-point isNaN operation
288  virtual SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) = 0;
289 
290  /// Creates a floating-point isNormal operation
291  virtual SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) = 0;
292 
293  /// Creates a floating-point isZero operation
294  virtual SMTExprRef mkFPIsZero(const SMTExprRef &Exp) = 0;
295 
296  /// Creates a floating-point multiplication operation
297  virtual SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
298 
299  /// Creates a floating-point division operation
300  virtual SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
301 
302  /// Creates a floating-point remainder operation
303  virtual SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
304 
305  /// Creates a floating-point addition operation
306  virtual SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
307 
308  /// Creates a floating-point subtraction operation
309  virtual SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
310 
311  /// Creates a floating-point less-than operation
312  virtual SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
313 
314  /// Creates a floating-point greater-than operation
315  virtual SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
316 
317  /// Creates a floating-point less-than-or-equal operation
318  virtual SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
319 
320  /// Creates a floating-point greater-than-or-equal operation
321  virtual SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
322 
323  /// Creates a floating-point equality operation
324  virtual SMTExprRef mkFPEqual(const SMTExprRef &LHS,
325  const SMTExprRef &RHS) = 0;
326 
327  /// Creates a floating-point conversion from floatint-point to floating-point
328  /// operation
329  virtual SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) = 0;
330 
331  /// Creates a floating-point conversion from signed bitvector to
332  /// floatint-point operation
333  virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From,
334  const SMTSortRef &To) = 0;
335 
336  /// Creates a floating-point conversion from unsigned bitvector to
337  /// floatint-point operation
338  virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From,
339  const SMTSortRef &To) = 0;
340 
341  /// Creates a floating-point conversion from floatint-point to signed
342  /// bitvector operation
343  virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth) = 0;
344 
345  /// Creates a floating-point conversion from floatint-point to unsigned
346  /// bitvector operation
347  virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth) = 0;
348 
349  /// Creates a new symbol, given a name and a sort
350  virtual SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) = 0;
351 
352  // Returns an appropriate floating-point rounding mode.
353  virtual SMTExprRef getFloatRoundingMode() = 0;
354 
355  // If the a model is available, returns the value of a given bitvector symbol
356  virtual llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth,
357  bool isUnsigned) = 0;
358 
359  // If the a model is available, returns the value of a given boolean symbol
360  virtual bool getBoolean(const SMTExprRef &Exp) = 0;
361 
362  /// Constructs an SMTExprRef from a boolean.
363  virtual SMTExprRef mkBoolean(const bool b) = 0;
364 
365  /// Constructs an SMTExprRef from a finite APFloat.
366  virtual SMTExprRef mkFloat(const llvm::APFloat Float) = 0;
367 
368  /// Constructs an SMTExprRef from an APSInt and its bit width
369  virtual SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) = 0;
370 
371  /// Given an expression, extract the value of this operand in the model.
372  virtual bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) = 0;
373 
374  /// Given an expression extract the value of this operand in the model.
375  virtual bool getInterpretation(const SMTExprRef &Exp,
376  llvm::APFloat &Float) = 0;
377 
378  /// Check if the constraints are satisfiable
379  virtual Optional<bool> check() const = 0;
380 
381  /// Push the current solver state
382  virtual void push() = 0;
383 
384  /// Pop the previous solver state
385  virtual void pop(unsigned NumStates = 1) = 0;
386 
387  /// Reset the solver and remove all constraints.
388  virtual void reset() = 0;
389 
390  /// Checks if the solver supports floating-points.
391  virtual bool isFPSupported() = 0;
392 
393  virtual void print(raw_ostream &OS) const = 0;
394 };
395 
396 /// Shared pointer for SMTSolvers.
397 using SMTSolverRef = std::shared_ptr<SMTSolver>;
398 
399 /// Convenience method to create and Z3Solver object
401 
402 } // namespace ento
403 } // namespace clang
404 
405 #endif
SMTSortRef getFloatSort(unsigned BitWidth)
Definition: SMTAPI.h:143
virtual unsigned getFloatSortSize() const
Returns the floating-point size, fails if the sort is not a floating-point Calls getFloatSortSizeImpl...
Definition: SMTAPI.h:50
virtual bool isFloatSort() const
Returns true if the sort is a floating-point, calls isFloatSortImpl().
Definition: SMTAPI.h:34
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).
Generic base class for SMT exprs.
Definition: SMTAPI.h:99
virtual bool isBooleanSort() const
Returns true if the sort is a boolean, calls isBooleanSortImpl().
Definition: SMTAPI.h:37
virtual void print(raw_ostream &OS) const =0
friend bool operator==(SMTSort const &LHS, SMTSort const &RHS)
Definition: SMTAPI.h:66
virtual void Profile(llvm::FoldingSetNodeID &ID) const =0
virtual unsigned getFloatSortSizeImpl() const =0
Query the SMT solver and returns the sort bit width.
LLVM_DUMP_METHOD void dump() const
Definition: SMTAPI.h:72
virtual void Profile(llvm::FoldingSetNodeID &ID) const =0
virtual unsigned getBitvectorSortSizeImpl() const =0
Query the SMT solver and returns the sort bit width.
virtual bool isBitvectorSort() const
Returns true if the sort is a bitvector, calls isBitvectorSortImpl().
Definition: SMTAPI.h:31
LLVM_DUMP_METHOD void dump() const
Definition: SMTAPI.h:140
bool operator<(const SMTSort &Other) const
Definition: SMTAPI.h:59
friend bool operator==(SMTExpr const &LHS, SMTExpr const &RHS)
Definition: SMTAPI.h:113
LLVM_DUMP_METHOD void dump() const
Definition: SMTAPI.h:119
SMTSolverRef CreateZ3Solver()
Convenience method to create and Z3Solver object.
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).
Dataflow Directional Tag Classes.
std::shared_ptr< SMTSolver > SMTSolverRef
Shared pointer for SMTSolvers.
Definition: SMTAPI.h:397
Generic base class for SMT Solvers.
Definition: SMTAPI.h:135
Indicates that the tracking object is a descendant of a referenced-counted OSObject, used in the Darwin kernel.
virtual bool isBooleanSortImpl() const =0
Query the SMT solver and checks if a sort is boolean.
virtual bool isBitvectorSortImpl() const =0
Query the SMT solver and checks if a sort is bitvector.
virtual ~SMTSort()=default
Defines the clang::TargetInfo interface.
Generic base class for SMT sorts.
Definition: SMTAPI.h:25
virtual bool isFloatSortImpl() const =0
Query the SMT solver and checks if a sort is floating-point.
bool operator<(const SMTExpr &Other) const
Definition: SMTAPI.h:104
virtual unsigned getBitvectorSortSize() const
Returns the bitvector size, fails if the sort is not a bitvector Calls getBitvectorSortSizeImpl().
Definition: SMTAPI.h:41