1 //== SMTSolver.h ------------------------------------------------*- C++ -*--==//
2 //
3 //                     The LLVM Compiler Infrastructure
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9 //
10 //  This file defines a SMT generic Solver API, which will be the base class
11 //  for every SMT solver specific class.
12 //
13 //===----------------------------------------------------------------------===//
14 
15 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
16 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
17 
18 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h"
19 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h"
20 #include "llvm/ADT/APSInt.h"
21 
22 namespace clang {
23 namespace ento {
24 
25 /// Generic base class for SMT Solvers
26 ///
27 /// This class is responsible for wrapping all sorts and expression generation,
28 /// through the mk* methods. It also provides methods to create SMT expressions
29 /// straight from clang's AST, through the from* methods.
30 class SMTSolver {
31 public:
32   SMTSolver() = default;
33   virtual ~SMTSolver() = default;
34 
dump()35   LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
36 
37   // Returns an appropriate floating-point sort for the given bitwidth.
getFloatSort(unsigned BitWidth)38   SMTSortRef getFloatSort(unsigned BitWidth) {
39     switch (BitWidth) {
40     case 16:
41       return getFloat16Sort();
42     case 32:
43       return getFloat32Sort();
44     case 64:
45       return getFloat64Sort();
46     case 128:
47       return getFloat128Sort();
48     default:;
49     }
50     llvm_unreachable("Unsupported floating-point bitwidth!");
51   }
52 
53   // Returns a boolean sort.
54   virtual SMTSortRef getBoolSort() = 0;
55 
56   // Returns an appropriate bitvector sort for the given bitwidth.
57   virtual SMTSortRef getBitvectorSort(const unsigned BitWidth) = 0;
58 
59   // Returns a floating-point sort of width 16
60   virtual SMTSortRef getFloat16Sort() = 0;
61 
62   // Returns a floating-point sort of width 32
63   virtual SMTSortRef getFloat32Sort() = 0;
64 
65   // Returns a floating-point sort of width 64
66   virtual SMTSortRef getFloat64Sort() = 0;
67 
68   // Returns a floating-point sort of width 128
69   virtual SMTSortRef getFloat128Sort() = 0;
70 
71   // Returns an appropriate sort for the given AST.
72   virtual SMTSortRef getSort(const SMTExprRef &AST) = 0;
73 
74   // Returns a new SMTExprRef from an SMTExpr
75   virtual SMTExprRef newExprRef(const SMTExpr &E) const = 0;
76 
77   /// Given a constraint, adds it to the solver
78   virtual void addConstraint(const SMTExprRef &Exp) const = 0;
79 
80   /// Creates a bitvector addition operation
81   virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
82 
83   /// Creates a bitvector subtraction operation
84   virtual SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
85 
86   /// Creates a bitvector multiplication operation
87   virtual SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
88 
89   /// Creates a bitvector signed modulus operation
90   virtual SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
91 
92   /// Creates a bitvector unsigned modulus operation
93   virtual SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
94 
95   /// Creates a bitvector signed division operation
96   virtual SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
97 
98   /// Creates a bitvector unsigned division operation
99   virtual SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
100 
101   /// Creates a bitvector logical shift left operation
102   virtual SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
103 
104   /// Creates a bitvector arithmetic shift right operation
105   virtual SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
106 
107   /// Creates a bitvector logical shift right operation
108   virtual SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
109 
110   /// Creates a bitvector negation operation
111   virtual SMTExprRef mkBVNeg(const SMTExprRef &Exp) = 0;
112 
113   /// Creates a bitvector not operation
114   virtual SMTExprRef mkBVNot(const SMTExprRef &Exp) = 0;
115 
116   /// Creates a bitvector xor operation
117   virtual SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
118 
119   /// Creates a bitvector or operation
120   virtual SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
121 
122   /// Creates a bitvector and operation
123   virtual SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
124 
125   /// Creates a bitvector unsigned less-than operation
126   virtual SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
127 
128   /// Creates a bitvector signed less-than operation
129   virtual SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
130 
131   /// Creates a bitvector unsigned greater-than operation
132   virtual SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
133 
134   /// Creates a bitvector signed greater-than operation
135   virtual SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
136 
137   /// Creates a bitvector unsigned less-equal-than operation
138   virtual SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
139 
140   /// Creates a bitvector signed less-equal-than operation
141   virtual SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
142 
143   /// Creates a bitvector unsigned greater-equal-than operation
144   virtual SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
145 
146   /// Creates a bitvector signed greater-equal-than operation
147   virtual SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
148 
149   /// Creates a boolean not operation
150   virtual SMTExprRef mkNot(const SMTExprRef &Exp) = 0;
151 
152   /// Creates a boolean equality operation
153   virtual SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
154 
155   /// Creates a boolean and operation
156   virtual SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
157 
158   /// Creates a boolean or operation
159   virtual SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
160 
161   /// Creates a boolean ite operation
162   virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
163                            const SMTExprRef &F) = 0;
164 
165   /// Creates a bitvector sign extension operation
166   virtual SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) = 0;
167 
168   /// Creates a bitvector zero extension operation
169   virtual SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) = 0;
170 
171   /// Creates a bitvector extract operation
172   virtual SMTExprRef mkBVExtract(unsigned High, unsigned Low,
173                                  const SMTExprRef &Exp) = 0;
174 
175   /// Creates a bitvector concat operation
176   virtual SMTExprRef mkBVConcat(const SMTExprRef &LHS,
177                                 const SMTExprRef &RHS) = 0;
178 
179   /// Creates a floating-point negation operation
180   virtual SMTExprRef mkFPNeg(const SMTExprRef &Exp) = 0;
181 
182   /// Creates a floating-point isInfinite operation
183   virtual SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) = 0;
184 
185   /// Creates a floating-point isNaN operation
186   virtual SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) = 0;
187 
188   /// Creates a floating-point isNormal operation
189   virtual SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) = 0;
190 
191   /// Creates a floating-point isZero operation
192   virtual SMTExprRef mkFPIsZero(const SMTExprRef &Exp) = 0;
193 
194   /// Creates a floating-point multiplication operation
195   virtual SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
196 
197   /// Creates a floating-point division operation
198   virtual SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
199 
200   /// Creates a floating-point remainder operation
201   virtual SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
202 
203   /// Creates a floating-point addition operation
204   virtual SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
205 
206   /// Creates a floating-point subtraction operation
207   virtual SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
208 
209   /// Creates a floating-point less-than operation
210   virtual SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
211 
212   /// Creates a floating-point greater-than operation
213   virtual SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
214 
215   /// Creates a floating-point less-than-or-equal operation
216   virtual SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
217 
218   /// Creates a floating-point greater-than-or-equal operation
219   virtual SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
220 
221   /// Creates a floating-point equality operation
222   virtual SMTExprRef mkFPEqual(const SMTExprRef &LHS,
223                                const SMTExprRef &RHS) = 0;
224 
225   /// Creates a floating-point conversion from floatint-point to floating-point
226   /// operation
227   virtual SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) = 0;
228 
229   /// Creates a floating-point conversion from signed bitvector to
230   /// floatint-point operation
231   virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From,
232                                const SMTSortRef &To) = 0;
233 
234   /// Creates a floating-point conversion from unsigned bitvector to
235   /// floatint-point operation
236   virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From,
237                                const SMTSortRef &To) = 0;
238 
239   /// Creates a floating-point conversion from floatint-point to signed
240   /// bitvector operation
241   virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth) = 0;
242 
243   /// Creates a floating-point conversion from floatint-point to unsigned
244   /// bitvector operation
245   virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth) = 0;
246 
247   /// Creates a new symbol, given a name and a sort
248   virtual SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) = 0;
249 
250   // Returns an appropriate floating-point rounding mode.
251   virtual SMTExprRef getFloatRoundingMode() = 0;
252 
253   // If the a model is available, returns the value of a given bitvector symbol
254   virtual llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth,
255                                     bool isUnsigned) = 0;
256 
257   // If the a model is available, returns the value of a given boolean symbol
258   virtual bool getBoolean(const SMTExprRef &Exp) = 0;
259 
260   /// Constructs an SMTExprRef from a boolean.
261   virtual SMTExprRef mkBoolean(const bool b) = 0;
262 
263   /// Constructs an SMTExprRef from a finite APFloat.
264   virtual SMTExprRef mkFloat(const llvm::APFloat Float) = 0;
265 
266   /// Constructs an SMTExprRef from an APSInt and its bit width
267   virtual SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) = 0;
268 
269   /// Given an expression, extract the value of this operand in the model.
270   virtual bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) = 0;
271 
272   /// Given an expression extract the value of this operand in the model.
273   virtual bool getInterpretation(const SMTExprRef &Exp,
274                                  llvm::APFloat &Float) = 0;
275 
276   /// Check if the constraints are satisfiable
277   virtual Optional<bool> check() const = 0;
278 
279   /// Push the current solver state
280   virtual void push() = 0;
281 
282   /// Pop the previous solver state
283   virtual void pop(unsigned NumStates = 1) = 0;
284 
285   /// Reset the solver and remove all constraints.
286   virtual void reset() = 0;
287 
288   /// Checks if the solver supports floating-points.
289   virtual bool isFPSupported() = 0;
290 
291   virtual void print(raw_ostream &OS) const = 0;
292 };
293 
294 /// Shared pointer for SMTSolvers.
295 using SMTSolverRef = std::shared_ptr<SMTSolver>;
296 
297 /// Convenience method to create and Z3Solver object
298 SMTSolverRef CreateZ3Solver();
299 
300 } // namespace ento
301 } // namespace clang
302 
303 #endif
304