llvm.org GIT mirror llvm / 987a6ac
Moved everything SMT-related to LLVM and updated the cmake scripts. Differential Revision: https://reviews.llvm.org/D54978 git-svn-id: https://llvm.org/svn/llvm-project/llvm/trunk@356929 91177308-0d34-0410-b5e6-96231b3b80d8 Mikhail R. Gadelha 6 months ago
7 changed file(s) with 1387 addition(s) and 1 deletion(s). Raw diff Collapse all Expand all
376376
377377 option(LLVM_ENABLE_ZLIB "Use zlib for compression/decompression if available." ON)
378378
379 set(LLVM_Z3_INSTALL_DIR "" CACHE STRING "Install directory of the Z3 solver.")
380
381 find_package(Z3 4.7.1)
382
383 if (LLVM_Z3_INSTALL_DIR)
384 if (NOT Z3_FOUND)
385 message(FATAL_ERROR "Z3 >= 4.7.1 has not been found in LLVM_Z3_INSTALL_DIR: ${LLVM_Z3_INSTALL_DIR}.")
386 endif()
387 endif()
388
389 set(LLVM_ENABLE_Z3_SOLVER_DEFAULT "${Z3_FOUND}")
390
391 option(LLVM_ENABLE_Z3_SOLVER
392 "Enable Support for the Z3 constraint solver in LLVM."
393 ${LLVM_ENABLE_Z3_SOLVER_DEFAULT}
394 )
395
396 if (LLVM_ENABLE_Z3_SOLVER)
397 if (NOT Z3_FOUND)
398 message(FATAL_ERROR "LLVM_ENABLE_Z3_SOLVER cannot be enabled when Z3 is not available.")
399 endif()
400
401 set(LLVM_WITH_Z3 1)
402 endif()
403
379404 if( LLVM_TARGETS_TO_BUILD STREQUAL "all" )
380405 set( LLVM_TARGETS_TO_BUILD ${LLVM_ALL_TARGETS} )
381406 endif()
0 INCLUDE(CheckCXXSourceRuns)
1
2 # Function to check Z3's version
3 function(check_z3_version z3_include z3_lib)
4 # The program that will be executed to print Z3's version.
5 file(WRITE ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.c
6 "#include
7 #include
8 int main() {
9 unsigned int major, minor, build, rev;
10 Z3_get_version(&major, &minor, &build, &rev);
11 printf(\"%u.%u.%u\", major, minor, build);
12 return 0;
13 }")
14
15 # Get lib path
16 get_filename_component(z3_lib_path ${z3_lib} PATH)
17
18 try_run(
19 Z3_RETURNCODE
20 Z3_COMPILED
21 ${CMAKE_BINARY_DIR}
22 ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.c
23 COMPILE_DEFINITIONS -I"${z3_include}"
24 LINK_LIBRARIES -L${z3_lib_path} -lz3
25 RUN_OUTPUT_VARIABLE SRC_OUTPUT
26 )
27
28 if(Z3_COMPILED)
29 string(REGEX REPLACE "([0-9]*\\.[0-9]*\\.[0-9]*\\.[0-9]*)" "\\1"
30 z3_version "${SRC_OUTPUT}")
31 set(Z3_VERSION_STRING ${z3_version} PARENT_SCOPE)
32 endif()
33 endfunction(check_z3_version)
34
35 # Looking for Z3 in LLVM_Z3_INSTALL_DIR
36 find_path(Z3_INCLUDE_DIR NAMES z3.h
37 NO_DEFAULT_PATH
38 PATHS ${LLVM_Z3_INSTALL_DIR}/include
39 PATH_SUFFIXES libz3 z3
40 )
41
42 find_library(Z3_LIBRARIES NAMES z3 libz3
43 NO_DEFAULT_PATH
44 PATHS ${LLVM_Z3_INSTALL_DIR}
45 PATH_SUFFIXES lib bin
46 )
47
48 # If Z3 has not been found in LLVM_Z3_INSTALL_DIR look in the default directories
49 find_path(Z3_INCLUDE_DIR NAMES z3.h
50 PATH_SUFFIXES libz3 z3
51 )
52
53 find_library(Z3_LIBRARIES NAMES z3 libz3
54 PATH_SUFFIXES lib bin
55 )
56
57 # Searching for the version of the Z3 library is a best-effort task
58 unset(Z3_VERSION_STRING)
59
60 # First, try to check it dynamically, by compiling a small program that
61 # prints Z3's version
62 if(Z3_INCLUDE_DIR AND Z3_LIBRARIES)
63 # We do not have the Z3 binary to query for a version. Try to use
64 # a small C++ program to detect it via the Z3_get_version() API call.
65 check_z3_version(${Z3_INCLUDE_DIR} ${Z3_LIBRARIES})
66 endif()
67
68 # If the dynamic check fails, we might be cross compiling: if that's the case,
69 # check the version in the headers, otherwise, fail with a message
70 if(NOT Z3_VERSION_STRING AND (CMAKE_CROSSCOMPILING AND
71 Z3_INCLUDE_DIR AND
72 EXISTS "${Z3_INCLUDE_DIR}/z3_version.h"))
73 # TODO: print message warning that we couldn't find a compatible lib?
74
75 # Z3 4.8.1+ has the version is in a public header.
76 file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h"
77 z3_version_str REGEX "^#define[\t ]+Z3_MAJOR_VERSION[\t ]+.*")
78 string(REGEX REPLACE "^.*Z3_MAJOR_VERSION[\t ]+([0-9]).*$" "\\1"
79 Z3_MAJOR "${z3_version_str}")
80
81 file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h"
82 z3_version_str REGEX "^#define[\t ]+Z3_MINOR_VERSION[\t ]+.*")
83 string(REGEX REPLACE "^.*Z3_MINOR_VERSION[\t ]+([0-9]).*$" "\\1"
84 Z3_MINOR "${z3_version_str}")
85
86 file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h"
87 z3_version_str REGEX "^#define[\t ]+Z3_BUILD_NUMBER[\t ]+.*")
88 string(REGEX REPLACE "^.*Z3_BUILD_VERSION[\t ]+([0-9]).*$" "\\1"
89 Z3_BUILD "${z3_version_str}")
90
91 set(Z3_VERSION_STRING ${Z3_MAJOR}.${Z3_MINOR}.${Z3_BUILD})
92 unset(z3_version_str)
93 endif()
94
95 if(NOT Z3_VERSION_STRING)
96 # Give up: we are unable to obtain a version of the Z3 library. Be
97 # conservative and force the found version to 0.0.0 to make version
98 # checks always fail.
99 set(Z3_VERSION_STRING "0.0.0")
100 endif()
101
102 # handle the QUIETLY and REQUIRED arguments and set Z3_FOUND to TRUE if
103 # all listed variables are TRUE
104 include(FindPackageHandleStandardArgs)
105 FIND_PACKAGE_HANDLE_STANDARD_ARGS(Z3
106 REQUIRED_VARS Z3_LIBRARIES Z3_INCLUDE_DIR
107 VERSION_VAR Z3_VERSION_STRING)
108
109 mark_as_advanced(Z3_INCLUDE_DIR Z3_LIBRARIES)
4242 set(LLVM_ENABLE_ZLIB @LLVM_ENABLE_ZLIB@)
4343
4444 set(LLVM_LIBXML2_ENABLED @LLVM_LIBXML2_ENABLED@)
45
46 set(LLVM_WITH_Z3 @LLVM_WITH_Z3@)
4547
4648 set(LLVM_ENABLE_DIA_SDK @LLVM_ENABLE_DIA_SDK@)
4749
343343 /* Whether GlobalISel rule coverage is being collected */
344344 #cmakedefine01 LLVM_GISEL_COV_ENABLED
345345
346 /* Define if we have z3 and want to build it */
347 #cmakedefine LLVM_WITH_Z3 ${LLVM_WITH_Z3}
348
346349 /* Define to the default GlobalISel coverage file prefix */
347350 #cmakedefine LLVM_GISEL_COV_PREFIX "${LLVM_GISEL_COV_PREFIX}"
348351
0 //===- SMTAPI.h -------------------------------------------------*- C++ -*-===//
1 //
2 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
3 // See https://llvm.org/LICENSE.txt for license information.
4 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
5 //
6 //===----------------------------------------------------------------------===//
7 //
8 // This file defines a SMT generic Solver API, which will be the base class
9 // for every SMT solver specific class.
10 //
11 //===----------------------------------------------------------------------===//
12
13 #ifndef LLVM_SUPPORT_SMTAPI_H
14 #define LLVM_SUPPORT_SMTAPI_H
15
16 #include "llvm/ADT/APFloat.h"
17 #include "llvm/ADT/APSInt.h"
18 #include "llvm/ADT/FoldingSet.h"
19 #include "llvm/Support/raw_ostream.h"
20 #include
21
22 namespace llvm {
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 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;
398
399 /// Convenience method to create and Z3Solver object
400 SMTSolverRef CreateZ3Solver();
401
402 } // namespace llvm
403
404 #endif
4141 set (delayload_flags)
4242 if (MSVC)
4343 set (delayload_flags delayimp -delayload:shell32.dll -delayload:ole32.dll)
44 endif()
45
46 # Link Z3 if the user wants to build it.
47 if(LLVM_WITH_Z3)
48 set(Z3_LINK_FILES ${Z3_LIBRARIES})
49 else()
50 set(Z3_LINK_FILES "")
4451 endif()
4552
4653 add_llvm_library(LLVMSupport
151158 regfree.c
152159 regstrlcpy.c
153160 xxhash.cpp
161 Z3Solver.cpp
154162
155163 # System
156164 Atomic.cpp
176184 ${LLVM_MAIN_INCLUDE_DIR}/llvm/ADT
177185 ${LLVM_MAIN_INCLUDE_DIR}/llvm/Support
178186 ${Backtrace_INCLUDE_DIRS}
179 LINK_LIBS ${system_libs} ${delayload_flags}
187 LINK_LIBS ${system_libs} ${delayload_flags} ${Z3_LINK_FILES}
180188 )
181189
182190 set_property(TARGET LLVMSupport PROPERTY LLVM_SYSTEM_LIBS "${system_libs}")
191
192 if(LLVM_WITH_Z3)
193 target_include_directories(LLVMSupport SYSTEM
194 PRIVATE
195 ${Z3_INCLUDE_DIR}
196 )
197 endif()
0 //== Z3Solver.cpp -----------------------------------------------*- C++ -*--==//
1 //
2 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
3 // See https://llvm.org/LICENSE.txt for license information.
4 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
5 //
6 //===----------------------------------------------------------------------===//
7
8 #include "llvm/ADT/Twine.h"
9 #include "llvm/Config/config.h"
10 #include "llvm/Support/SMTAPI.h"
11 #include
12
13 using namespace llvm;
14
15 #if LLVM_WITH_Z3
16
17 #include
18
19 namespace {
20
21 /// Configuration class for Z3
22 class Z3Config {
23 friend class Z3Context;
24
25 Z3_config Config;
26
27 public:
28 Z3Config() : Config(Z3_mk_config()) {
29 // Enable model finding
30 Z3_set_param_value(Config, "model", "true");
31 // Disable proof generation
32 Z3_set_param_value(Config, "proof", "false");
33 // Set timeout to 15000ms = 15s
34 Z3_set_param_value(Config, "timeout", "15000");
35 }
36
37 ~Z3Config() { Z3_del_config(Config); }
38 }; // end class Z3Config
39
40 // Function used to report errors
41 void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) {
42 llvm::report_fatal_error("Z3 error: " +
43 llvm::Twine(Z3_get_error_msg(Context, Error)));
44 }
45
46 /// Wrapper for Z3 context
47 class Z3Context {
48 public:
49 Z3_context Context;
50
51 Z3Context() {
52 Context = Z3_mk_context_rc(Z3Config().Config);
53 // The error function is set here because the context is the first object
54 // created by the backend
55 Z3_set_error_handler(Context, Z3ErrorHandler);
56 }
57
58 virtual ~Z3Context() {
59 Z3_del_context(Context);
60 Context = nullptr;
61 }
62 }; // end class Z3Context
63
64 /// Wrapper for Z3 Sort
65 class Z3Sort : public SMTSort {
66 friend class Z3Solver;
67
68 Z3Context &Context;
69
70 Z3_sort Sort;
71
72 public:
73 /// Default constructor, mainly used by make_shared
74 Z3Sort(Z3Context &C, Z3_sort ZS) : Context(C), Sort(ZS) {
75 Z3_inc_ref(Context.Context, reinterpret_cast(Sort));
76 }
77
78 /// Override implicit copy constructor for correct reference counting.
79 Z3Sort(const Z3Sort &Other) : Context(Other.Context), Sort(Other.Sort) {
80 Z3_inc_ref(Context.Context, reinterpret_cast(Sort));
81 }
82
83 /// Override implicit copy assignment constructor for correct reference
84 /// counting.
85 Z3Sort &operator=(const Z3Sort &Other) {
86 Z3_inc_ref(Context.Context, reinterpret_cast(Other.Sort));
87 Z3_dec_ref(Context.Context, reinterpret_cast(Sort));
88 Sort = Other.Sort;
89 return *this;
90 }
91
92 Z3Sort(Z3Sort &&Other) = delete;
93 Z3Sort &operator=(Z3Sort &&Other) = delete;
94
95 ~Z3Sort() {
96 if (Sort)
97 Z3_dec_ref(Context.Context, reinterpret_cast(Sort));
98 }
99
100 void Profile(llvm::FoldingSetNodeID &ID) const override {
101 ID.AddInteger(
102 Z3_get_ast_id(Context.Context, reinterpret_cast(Sort)));
103 }
104
105 bool isBitvectorSortImpl() const override {
106 return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BV_SORT);
107 }
108
109 bool isFloatSortImpl() const override {
110 return (Z3_get_sort_kind(Context.Context, Sort) == Z3_FLOATING_POINT_SORT);
111 }
112
113 bool isBooleanSortImpl() const override {
114 return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BOOL_SORT);
115 }
116
117 unsigned getBitvectorSortSizeImpl() const override {
118 return Z3_get_bv_sort_size(Context.Context, Sort);
119 }
120
121 unsigned getFloatSortSizeImpl() const override {
122 return Z3_fpa_get_ebits(Context.Context, Sort) +
123 Z3_fpa_get_sbits(Context.Context, Sort);
124 }
125
126 bool equal_to(SMTSort const &Other) const override {
127 return Z3_is_eq_sort(Context.Context, Sort,
128 static_cast(Other).Sort);
129 }
130
131 void print(raw_ostream &OS) const override {
132 OS << Z3_sort_to_string(Context.Context, Sort);
133 }
134 }; // end class Z3Sort
135
136 static const Z3Sort &toZ3Sort(const SMTSort &S) {
137 return static_cast(S);
138 }
139
140 class Z3Expr : public SMTExpr {
141 friend class Z3Solver;
142
143 Z3Context &Context;
144
145 Z3_ast AST;
146
147 public:
148 Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) {
149 Z3_inc_ref(Context.Context, AST);
150 }
151
152 /// Override implicit copy constructor for correct reference counting.
153 Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) {
154 Z3_inc_ref(Context.Context, AST);
155 }
156
157 /// Override implicit copy assignment constructor for correct reference
158 /// counting.
159 Z3Expr &operator=(const Z3Expr &Other) {
160 Z3_inc_ref(Context.Context, Other.AST);
161 Z3_dec_ref(Context.Context, AST);
162 AST = Other.AST;
163 return *this;
164 }
165
166 Z3Expr(Z3Expr &&Other) = delete;
167 Z3Expr &operator=(Z3Expr &&Other) = delete;
168
169 ~Z3Expr() {
170 if (AST)
171 Z3_dec_ref(Context.Context, AST);
172 }
173
174 void Profile(llvm::FoldingSetNodeID &ID) const override {
175 ID.AddInteger(Z3_get_ast_id(Context.Context, AST));
176 }
177
178 /// Comparison of AST equality, not model equivalence.
179 bool equal_to(SMTExpr const &Other) const override {
180 assert(Z3_is_eq_sort(Context.Context, Z3_get_sort(Context.Context, AST),
181 Z3_get_sort(Context.Context,
182 static_cast(Other).AST)) &&
183 "AST's must have the same sort");
184 return Z3_is_eq_ast(Context.Context, AST,
185 static_cast(Other).AST);
186 }
187
188 void print(raw_ostream &OS) const override {
189 OS << Z3_ast_to_string(Context.Context, AST);
190 }
191 }; // end class Z3Expr
192
193 static const Z3Expr &toZ3Expr(const SMTExpr &E) {
194 return static_cast(E);
195 }
196
197 class Z3Model {
198 friend class Z3Solver;
199
200 Z3Context &Context;
201
202 Z3_model Model;
203
204 public:
205 Z3Model(Z3Context &C, Z3_model ZM) : Context(C), Model(ZM) {
206 Z3_model_inc_ref(Context.Context, Model);
207 }
208
209 Z3Model(const Z3Model &Other) = delete;
210 Z3Model(Z3Model &&Other) = delete;
211 Z3Model &operator=(Z3Model &Other) = delete;
212 Z3Model &operator=(Z3Model &&Other) = delete;
213
214 ~Z3Model() {
215 if (Model)
216 Z3_model_dec_ref(Context.Context, Model);
217 }
218
219 void print(raw_ostream &OS) const {
220 OS << Z3_model_to_string(Context.Context, Model);
221 }
222
223 LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
224 }; // end class Z3Model
225
226 /// Get the corresponding IEEE floating-point type for a given bitwidth.
227 static const llvm::fltSemantics &getFloatSemantics(unsigned BitWidth) {
228 switch (BitWidth) {
229 default:
230 llvm_unreachable("Unsupported floating-point semantics!");
231 break;
232 case 16:
233 return llvm::APFloat::IEEEhalf();
234 case 32:
235 return llvm::APFloat::IEEEsingle();
236 case 64:
237 return llvm::APFloat::IEEEdouble();
238 case 128:
239 return llvm::APFloat::IEEEquad();
240 }
241 }
242
243 // Determine whether two float semantics are equivalent
244 static bool areEquivalent(const llvm::fltSemantics &LHS,
245 const llvm::fltSemantics &RHS) {
246 return (llvm::APFloat::semanticsPrecision(LHS) ==
247 llvm::APFloat::semanticsPrecision(RHS)) &&
248 (llvm::APFloat::semanticsMinExponent(LHS) ==
249 llvm::APFloat::semanticsMinExponent(RHS)) &&
250 (llvm::APFloat::semanticsMaxExponent(LHS) ==
251 llvm::APFloat::semanticsMaxExponent(RHS)) &&
252 (llvm::APFloat::semanticsSizeInBits(LHS) ==
253 llvm::APFloat::semanticsSizeInBits(RHS));
254 }
255
256 class Z3Solver : public SMTSolver {
257 friend class Z3ConstraintManager;
258
259 Z3Context Context;
260
261 Z3_solver Solver;
262
263 // Cache Sorts
264 std::set CachedSorts;
265
266 // Cache Exprs
267 std::set CachedExprs;
268
269 public:
270 Z3Solver() : Solver(Z3_mk_simple_solver(Context.Context)) {
271 Z3_solver_inc_ref(Context.Context, Solver);
272 }
273
274 Z3Solver(const Z3Solver &Other) = delete;
275 Z3Solver(Z3Solver &&Other) = delete;
276 Z3Solver &operator=(Z3Solver &Other) = delete;
277 Z3Solver &operator=(Z3Solver &&Other) = delete;
278
279 ~Z3Solver() {
280 if (Solver)
281 Z3_solver_dec_ref(Context.Context, Solver);
282 }
283
284 void addConstraint(const SMTExprRef &Exp) const override {
285 Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST);
286 }
287
288 // Given an SMTSort, adds/retrives it from the cache and returns
289 // an SMTSortRef to the SMTSort in the cache
290 SMTSortRef newSortRef(const SMTSort &Sort) {
291 auto It = CachedSorts.insert(toZ3Sort(Sort));
292 return &(*It.first);
293 }
294
295 // Given an SMTExpr, adds/retrives it from the cache and returns
296 // an SMTExprRef to the SMTExpr in the cache
297 SMTExprRef newExprRef(const SMTExpr &Exp) {
298 auto It = CachedExprs.insert(toZ3Expr(Exp));
299 return &(*It.first);
300 }
301
302 SMTSortRef getBoolSort() override {
303 return newSortRef(Z3Sort(Context, Z3_mk_bool_sort(Context.Context)));
304 }
305
306 SMTSortRef getBitvectorSort(unsigned BitWidth) override {
307 return newSortRef(
308 Z3Sort(Context, Z3_mk_bv_sort(Context.Context, BitWidth)));
309 }
310
311 SMTSortRef getSort(const SMTExprRef &Exp) override {
312 return newSortRef(
313 Z3Sort(Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST)));
314 }
315
316 SMTSortRef getFloat16Sort() override {
317 return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_16(Context.Context)));
318 }
319
320 SMTSortRef getFloat32Sort() override {
321 return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_32(Context.Context)));
322 }
323
324 SMTSortRef getFloat64Sort() override {
325 return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_64(Context.Context)));
326 }
327
328 SMTSortRef getFloat128Sort() override {
329 return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_128(Context.Context)));
330 }
331
332 SMTExprRef mkBVNeg(const SMTExprRef &Exp) override {
333 return newExprRef(
334 Z3Expr(Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST)));
335 }
336
337 SMTExprRef mkBVNot(const SMTExprRef &Exp) override {
338 return newExprRef(
339 Z3Expr(Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST)));
340 }
341
342 SMTExprRef mkNot(const SMTExprRef &Exp) override {
343 return newExprRef(
344 Z3Expr(Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST)));
345 }
346
347 SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
348 return newExprRef(
349 Z3Expr(Context, Z3_mk_bvadd(Context.Context, toZ3Expr(*LHS).AST,
350 toZ3Expr(*RHS).AST)));
351 }
352
353 SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
354 return newExprRef(
355 Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST,
356 toZ3Expr(*RHS).AST)));
357 }
358
359 SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
360 return newExprRef(
361 Z3Expr(Context, Z3_mk_bvmul(Context.Context, toZ3Expr(*LHS).AST,
362 toZ3Expr(*RHS).AST)));
363 }
364
365 SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
366 return newExprRef(
367 Z3Expr(Context, Z3_mk_bvsrem(Context.Context, toZ3Expr(*LHS).AST,
368 toZ3Expr(*RHS).AST)));
369 }
370
371 SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
372 return newExprRef(
373 Z3Expr(Context, Z3_mk_bvurem(Context.Context, toZ3Expr(*LHS).AST,
374 toZ3Expr(*RHS).AST)));
375 }
376
377 SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
378 return newExprRef(
379 Z3Expr(Context, Z3_mk_bvsdiv(Context.Context, toZ3Expr(*LHS).AST,
380 toZ3Expr(*RHS).AST)));
381 }
382
383 SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
384 return newExprRef(
385 Z3Expr(Context, Z3_mk_bvudiv(Context.Context, toZ3Expr(*LHS).AST,
386 toZ3Expr(*RHS).AST)));
387 }
388
389 SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
390 return newExprRef(
391 Z3Expr(Context, Z3_mk_bvshl(Context.Context, toZ3Expr(*LHS).AST,
392 toZ3Expr(*RHS).AST)));
393 }
394
395 SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
396 return newExprRef(
397 Z3Expr(Context, Z3_mk_bvashr(Context.Context, toZ3Expr(*LHS).AST,
398 toZ3Expr(*RHS).AST)));
399 }
400
401 SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
402 return newExprRef(
403 Z3Expr(Context, Z3_mk_bvlshr(Context.Context, toZ3Expr(*LHS).AST,
404 toZ3Expr(*RHS).AST)));
405 }
406
407 SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
408 return newExprRef(
409 Z3Expr(Context, Z3_mk_bvxor(Context.Context, toZ3Expr(*LHS).AST,
410 toZ3Expr(*RHS).AST)));
411 }
412
413 SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
414 return newExprRef(
415 Z3Expr(Context, Z3_mk_bvor(Context.Context, toZ3Expr(*LHS).AST,
416 toZ3Expr(*RHS).AST)));
417 }
418
419 SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
420 return newExprRef(
421 Z3Expr(Context, Z3_mk_bvand(Context.Context, toZ3Expr(*LHS).AST,
422 toZ3Expr(*RHS).AST)));
423 }
424
425 SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
426 return newExprRef(
427 Z3Expr(Context, Z3_mk_bvult(Context.Context, toZ3Expr(*LHS).AST,
428 toZ3Expr(*RHS).AST)));
429 }
430
431 SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
432 return newExprRef(
433 Z3Expr(Context, Z3_mk_bvslt(Context.Context, toZ3Expr(*LHS).AST,
434 toZ3Expr(*RHS).AST)));
435 }
436
437 SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
438 return newExprRef(
439 Z3Expr(Context, Z3_mk_bvugt(Context.Context, toZ3Expr(*LHS).AST,
440 toZ3Expr(*RHS).AST)));
441 }
442
443 SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
444 return newExprRef(
445 Z3Expr(Context, Z3_mk_bvsgt(Context.Context, toZ3Expr(*LHS).AST,
446 toZ3Expr(*RHS).AST)));
447 }
448
449 SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
450 return newExprRef(
451 Z3Expr(Context, Z3_mk_bvule(Context.Context, toZ3Expr(*LHS).AST,
452 toZ3Expr(*RHS).AST)));
453 }
454
455 SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
456 return newExprRef(
457 Z3Expr(Context, Z3_mk_bvsle(Context.Context, toZ3Expr(*LHS).AST,
458 toZ3Expr(*RHS).AST)));
459 }
460
461 SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
462 return newExprRef(
463 Z3Expr(Context, Z3_mk_bvuge(Context.Context, toZ3Expr(*LHS).AST,
464 toZ3Expr(*RHS).AST)));
465 }
466
467 SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
468 return newExprRef(
469 Z3Expr(Context, Z3_mk_bvsge(Context.Context, toZ3Expr(*LHS).AST,
470 toZ3Expr(*RHS).AST)));
471 }
472
473 SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
474 Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
475 return newExprRef(Z3Expr(Context, Z3_mk_and(Context.Context, 2, Args)));
476 }
477
478 SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
479 Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
480 return newExprRef(Z3Expr(Context, Z3_mk_or(Context.Context, 2, Args)));
481 }
482
483 SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
484 return newExprRef(
485 Z3Expr(Context, Z3_mk_eq(Context.Context, toZ3Expr(*LHS).AST,
486 toZ3Expr(*RHS).AST)));
487 }
488
489 SMTExprRef mkFPNeg(const SMTExprRef &Exp) override {
490 return newExprRef(
491 Z3Expr(Context, Z3_mk_fpa_neg(Context.Context, toZ3Expr(*Exp).AST)));
492 }
493
494 SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) override {
495 return newExprRef(Z3Expr(
496 Context, Z3_mk_fpa_is_infinite(Context.Context, toZ3Expr(*Exp).AST)));
497 }
498
499 SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) override {
500 return newExprRef(
501 Z3Expr(Context, Z3_mk_fpa_is_nan(Context.Context, toZ3Expr(*Exp).AST)));
502 }
503
504 SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) override {
505 return newExprRef(Z3Expr(
506 Context, Z3_mk_fpa_is_normal(Context.Context, toZ3Expr(*Exp).AST)));
507 }
508
509 SMTExprRef mkFPIsZero(const SMTExprRef &Exp) override {
510 return newExprRef(Z3Expr(
511 Context, Z3_mk_fpa_is_zero(Context.Context, toZ3Expr(*Exp).AST)));
512 }
513
514 SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
515 SMTExprRef RoundingMode = getFloatRoundingMode();
516 return newExprRef(
517 Z3Expr(Context,
518 Z3_mk_fpa_mul(Context.Context, toZ3Expr(*LHS).AST,
519 toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
520 }
521
522 SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
523 SMTExprRef RoundingMode = getFloatRoundingMode();
524 return newExprRef(
525 Z3Expr(Context,
526 Z3_mk_fpa_div(Context.Context, toZ3Expr(*LHS).AST,
527 toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
528 }
529
530 SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
531 return newExprRef(
532 Z3Expr(Context, Z3_mk_fpa_rem(Context.Context, toZ3Expr(*LHS).AST,
533 toZ3Expr(*RHS).AST)));
534 }
535
536 SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
537 SMTExprRef RoundingMode = getFloatRoundingMode();
538 return newExprRef(
539 Z3Expr(Context,
540 Z3_mk_fpa_add(Context.Context, toZ3Expr(*LHS).AST,
541 toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
542 }
543
544 SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
545 SMTExprRef RoundingMode = getFloatRoundingMode();
546 return newExprRef(
547 Z3Expr(Context,
548 Z3_mk_fpa_sub(Context.Context, toZ3Expr(*LHS).AST,
549 toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
550 }
551
552 SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
553 return newExprRef(
554 Z3Expr(Context, Z3_mk_fpa_lt(Context.Context, toZ3Expr(*LHS).AST,
555 toZ3Expr(*RHS).AST)));
556 }
557
558 SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
559 return newExprRef(
560 Z3Expr(Context, Z3_mk_fpa_gt(Context.Context, toZ3Expr(*LHS).AST,
561 toZ3Expr(*RHS).AST)));
562 }
563
564 SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
565 return newExprRef(
566 Z3Expr(Context, Z3_mk_fpa_leq(Context.Context, toZ3Expr(*LHS).AST,
567 toZ3Expr(*RHS).AST)));
568 }
569
570 SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
571 return newExprRef(
572 Z3Expr(Context, Z3_mk_fpa_geq(Context.Context, toZ3Expr(*LHS).AST,
573 toZ3Expr(*RHS).AST)));
574 }
575
576 SMTExprRef mkFPEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
577 return newExprRef(
578 Z3Expr(Context, Z3_mk_fpa_eq(Context.Context, toZ3Expr(*LHS).AST,
579 toZ3Expr(*RHS).AST)));
580 }
581
582 SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
583 const SMTExprRef &F) override {
584 return newExprRef(
585 Z3Expr(Context, Z3_mk_ite(Context.Context, toZ3Expr(*Cond).AST,
586 toZ3Expr(*T).AST, toZ3Expr(*F).AST)));
587 }
588
589 SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) override {
590 return newExprRef(Z3Expr(
591 Context, Z3_mk_sign_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
592 }
593
594 SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) override {
595 return newExprRef(Z3Expr(
596 Context, Z3_mk_zero_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
597 }
598
599 SMTExprRef mkBVExtract(unsigned High, unsigned Low,
600 const SMTExprRef &Exp) override {
601 return newExprRef(Z3Expr(Context, Z3_mk_extract(Context.Context, High, Low,
602 toZ3Expr(*Exp).AST)));
603 }
604
605 SMTExprRef mkBVConcat(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
606 return newExprRef(
607 Z3Expr(Context, Z3_mk_concat(Context.Context, toZ3Expr(*LHS).AST,
608 toZ3Expr(*RHS).AST)));
609 }
610
611 SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) override {
612 SMTExprRef RoundingMode = getFloatRoundingMode();
613 return newExprRef(Z3Expr(
614 Context,
615 Z3_mk_fpa_to_fp_float(Context.Context, toZ3Expr(*RoundingMode).AST,
616 toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
617 }
618
619 SMTExprRef mkSBVtoFP(const SMTExprRef &From, const SMTSortRef &To) override {
620 SMTExprRef RoundingMode = getFloatRoundingMode();
621 return newExprRef(Z3Expr(
622 Context,
623 Z3_mk_fpa_to_fp_signed(Context.Context, toZ3Expr(*RoundingMode).AST,
624 toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
625 }
626
627 SMTExprRef mkUBVtoFP(const SMTExprRef &From, const SMTSortRef &To) override {
628 SMTExprRef RoundingMode = getFloatRoundingMode();
629 return newExprRef(Z3Expr(
630 Context,
631 Z3_mk_fpa_to_fp_unsigned(Context.Context, toZ3Expr(*RoundingMode).AST,
632 toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
633 }
634
635 SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth) override {
636 SMTExprRef RoundingMode = getFloatRoundingMode();
637 return newExprRef(Z3Expr(
638 Context, Z3_mk_fpa_to_sbv(Context.Context, toZ3Expr(*RoundingMode).AST,
639 toZ3Expr(*From).AST, ToWidth)));
640 }
641
642 SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth) override {
643 SMTExprRef RoundingMode = getFloatRoundingMode();
644 return newExprRef(Z3Expr(
645 Context, Z3_mk_fpa_to_ubv(Context.Context, toZ3Expr(*RoundingMode).AST,
646 toZ3Expr(*From).AST, ToWidth)));
647 }
648
649 SMTExprRef mkBoolean(const bool b) override {
650 return newExprRef(Z3Expr(Context, b ? Z3_mk_true(Context.Context)
651 : Z3_mk_false(Context.Context)));
652 }
653
654 SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) override {
655 const SMTSortRef Sort = getBitvectorSort(BitWidth);
656 return newExprRef(
657 Z3Expr(Context, Z3_mk_numeral(Context.Context, Int.toString(10).c_str(),
658 toZ3Sort(*Sort).Sort)));
659 }
660
661 SMTExprRef mkFloat(const llvm::APFloat Float) override {
662 SMTSortRef Sort =
663 getFloatSort(llvm::APFloat::semanticsSizeInBits(Float.getSemantics()));
664
665 llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), false);
666 SMTExprRef Z3Int = mkBitvector(Int, Int.getBitWidth());
667 return newExprRef(Z3Expr(
668 Context, Z3_mk_fpa_to_fp_bv(Context.Context, toZ3Expr(*Z3Int).AST,
669 toZ3Sort(*Sort).Sort)));
670 }
671
672 SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) override {
673 return newExprRef(
674 Z3Expr(Context, Z3_mk_const(Context.Context,
675 Z3_mk_string_symbol(Context.Context, Name),
676 toZ3Sort(*Sort).Sort)));
677 }
678
679 llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth,
680 bool isUnsigned) override {
681 return llvm::APSInt(
682 llvm::APInt(BitWidth,
683 Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST),
684 10),
685 isUnsigned);
686 }
687
688 bool getBoolean(const SMTExprRef &Exp) override {
689 return Z3_get_bool_value(Context.Context, toZ3Expr(*Exp).AST) == Z3_L_TRUE;
690 }
691
692 SMTExprRef getFloatRoundingMode() override {
693 // TODO: Don't assume nearest ties to even rounding mode
694 return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context)));
695 }
696
697 bool toAPFloat(const SMTSortRef &Sort, const SMTExprRef &AST,
698 llvm::APFloat &Float, bool useSemantics) {
699 assert(Sort->isFloatSort() && "Unsupported sort to floating-point!");
700
701 llvm::APSInt Int(Sort->getFloatSortSize(), true);
702 const llvm::fltSemantics &Semantics =
703 getFloatSemantics(Sort->getFloatSortSize());
704 SMTSortRef BVSort = getBitvectorSort(Sort->getFloatSortSize());
705 if (!toAPSInt(BVSort, AST, Int, true)) {
706 return false;
707 }
708
709 if (useSemantics && !areEquivalent(Float.getSemantics(), Semantics)) {
710 assert(false && "Floating-point types don't match!");
711 return false;
712 }
713
714 Float = llvm::APFloat(Semantics, Int);
715 return true;
716 }
717
718 bool toAPSInt(const SMTSortRef &Sort, const SMTExprRef &AST,
719 llvm::APSInt &Int, bool useSemantics) {
720 if (Sort->isBitvectorSort()) {
721 if (useSemantics && Int.getBitWidth() != Sort->getBitvectorSortSize()) {
722 assert(false && "Bitvector types don't match!");
723 return false;
724 }
725
726 // FIXME: This function is also used to retrieve floating-point values,
727 // which can be 16, 32, 64 or 128 bits long. Bitvectors can be anything
728 // between 1 and 64 bits long, which is the reason we have this weird
729 // guard. In the future, we need proper calls in the backend to retrieve
730 // floating-points and its special values (NaN, +/-infinity, +/-zero),
731 // then we can drop this weird condition.
732 if (Sort->getBitvectorSortSize() <= 64 ||
733 Sort->getBitvectorSortSize() == 128) {
734 Int = getBitvector(AST, Int.getBitWidth(), Int.isUnsigned());
735 return true;
736 }
737
738 assert(false && "Bitwidth not supported!");
739 return false;
740 }
741
742 if (Sort->isBooleanSort()) {
743 if (useSemantics && Int.getBitWidth() < 1) {
744 assert(false && "Boolean type doesn't match!");
745 return false;
746 }
747
748 Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), getBoolean(AST)),
749 Int.isUnsigned());
750 return true;
751 }
752
753 llvm_unreachable("Unsupported sort to integer!");
754 }
755
756 bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) override {
757 Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));
758 Z3_func_decl Func = Z3_get_app_decl(
759 Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));
760 if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE)
761 return false;
762
763 SMTExprRef Assign = newExprRef(
764 Z3Expr(Context,
765 Z3_model_get_const_interp(Context.Context, Model.Model, Func)));
766 SMTSortRef Sort = getSort(Assign);
767 return toAPSInt(Sort, Assign, Int, true);
768 }
769
770 bool getInterpretation(const SMTExprRef &Exp, llvm::APFloat &Float) override {
771 Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));
772 Z3_func_decl Func = Z3_get_app_decl(
773 Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));
774 if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE)
775 return false;
776
777 SMTExprRef Assign = newExprRef(
778 Z3Expr(Context,
779 Z3_model_get_const_interp(Context.Context, Model.Model, Func)));
780 SMTSortRef Sort = getSort(Assign);
781 return toAPFloat(Sort, Assign, Float, true);
782 }
783
784 Optional check() const override {
785 Z3_lbool res = Z3_solver_check(Context.Context, Solver);
786 if (res == Z3_L_TRUE)
787 return true;
788
789 if (res == Z3_L_FALSE)
790 return false;
791
792 return Optional();
793 }
794
795 void push() override { return Z3_solver_push(Context.Context, Solver); }
796
797 void pop(unsigned NumStates = 1) override {
798 assert(Z3_solver_get_num_scopes(Context.Context, Solver) >= NumStates);
799 return Z3_solver_pop(Context.Context, Solver, NumStates);
800 }
801
802 bool isFPSupported() override { return true; }
803
804 /// Reset the solver and remove all constraints.
805 void reset() override { Z3_solver_reset(Context.Context, Solver); }
806
807 void print(raw_ostream &OS) const override {
808 OS << Z3_solver_to_string(Context.Context, Solver);
809 }
810 }; // end class Z3Solver
811
812 } // end anonymous namespace
813
814 #endif
815
816 llvm::SMTSolverRef llvm::CreateZ3Solver() {
817 #if LLVM_WITH_Z3
818 return llvm::make_unique();
819 #else
820 llvm::report_fatal_error("LLVM was not compiled with Z3 support, rebuild "
821 "with -DLLVM_ENABLE_Z3_SOLVER=ON",
822 false);
823 return nullptr;
824 #endif
825 }