CIRCT  20.0.0git
SMTToZ3LLVM.h
Go to the documentation of this file.
1 //===- SMTToZ3LLVM.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 #ifndef CIRCT_CONVERSION_SMTTOZ3LLVM_H
10 #define CIRCT_CONVERSION_SMTTOZ3LLVM_H
11 
12 #include "circt/Support/LLVM.h"
14 #include "mlir/Dialect/LLVMIR/LLVMDialect.h"
15 #include "llvm/ADT/StringRef.h"
16 #include <memory>
17 
18 namespace circt {
19 
20 #define GEN_PASS_DECL_LOWERSMTTOZ3LLVM
21 #include "circt/Conversion/Passes.h.inc"
22 
23 /// A symbol cache for LLVM globals and functions relevant to SMT lowering
24 /// patterns.
26  /// Creates the LLVM global operations to store the pointers to the solver and
27  /// the context and returns a 'SMTGlobalHandler' initialized with those new
28  /// globals.
29  static SMTGlobalsHandler create(OpBuilder &builder, ModuleOp module);
30 
31  /// Initializes the caches and keeps track of the given globals to store the
32  /// pointers to the SMT solver and context. It is assumed that the passed
33  /// global operations are of the correct (or at least compatible) form. E.g.,
34  /// ```
35  /// llvm.mlir.global internal @ctx() {alignment = 8 : i64} : !llvm.ptr {
36  /// %0 = llvm.mlir.zero : !llvm.ptr
37  /// llvm.return %0 : !llvm.ptr
38  /// }
39  /// ```
40  SMTGlobalsHandler(ModuleOp module, mlir::LLVM::GlobalOp solver,
41  mlir::LLVM::GlobalOp ctx);
42 
43  /// Initializes the caches and keeps track of the given globals to store the
44  /// pointers to the SMT solver and context. It is assumed that the passed
45  /// global operations are of the correct (or at least compatible) form. E.g.,
46  /// ```
47  /// llvm.mlir.global internal @ctx() {alignment = 8 : i64} : !llvm.ptr {
48  /// %0 = llvm.mlir.zero : !llvm.ptr
49  /// llvm.return %0 : !llvm.ptr
50  /// }
51  /// ```
52  SMTGlobalsHandler(Namespace &&names, mlir::LLVM::GlobalOp solver,
53  mlir::LLVM::GlobalOp ctx);
54 
55  /// The global storing the pointer to the SMT solver object currently active.
56  const mlir::LLVM::GlobalOp solver;
57 
58  /// The global storing the pointer to the SMT context object currently active.
59  const mlir::LLVM::GlobalOp ctx;
60 
62  DenseMap<StringAttr, mlir::LLVM::LLVMFuncOp> funcMap;
63  DenseMap<Block *, Value> ctxCache;
64  DenseMap<Block *, Value> solverCache;
65  DenseMap<StringAttr, mlir::LLVM::GlobalOp> stringCache;
66 };
67 
68 /// Populate the given type converter with the SMT to LLVM type conversions.
69 void populateSMTToZ3LLVMTypeConverter(TypeConverter &converter);
70 
71 /// Add the SMT to LLVM IR conversion patterns to 'patterns'. A
72 /// 'SMTGlobalHandler' object has to be passed which acts as a symbol cache for
73 /// LLVM globals and functions.
75  RewritePatternSet &patterns, TypeConverter &converter,
76  SMTGlobalsHandler &globals, const LowerSMTToZ3LLVMOptions &options);
77 
78 } // namespace circt
79 
80 #endif // CIRCT_CONVERSION_SMTTOZ3LLVM_H
A namespace that is used to store existing names and generate new names in some scope within the IR.
Definition: Namespace.h:30
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.
Definition: DebugAnalysis.h:21
void populateSMTToZ3LLVMTypeConverter(TypeConverter &converter)
Populate the given type converter with the SMT to LLVM type conversions.
void populateSMTToZ3LLVMConversionPatterns(RewritePatternSet &patterns, TypeConverter &converter, SMTGlobalsHandler &globals, const LowerSMTToZ3LLVMOptions &options)
Add the SMT to LLVM IR conversion patterns to 'patterns'.
A symbol cache for LLVM globals and functions relevant to SMT lowering patterns.
Definition: SMTToZ3LLVM.h:25
DenseMap< StringAttr, mlir::LLVM::GlobalOp > stringCache
Definition: SMTToZ3LLVM.h:65
DenseMap< StringAttr, mlir::LLVM::LLVMFuncOp > funcMap
Definition: SMTToZ3LLVM.h:62
DenseMap< Block *, Value > solverCache
Definition: SMTToZ3LLVM.h:64
static SMTGlobalsHandler create(OpBuilder &builder, ModuleOp module)
Creates the LLVM global operations to store the pointers to the solver and the context and returns a ...
SMTGlobalsHandler(ModuleOp module, mlir::LLVM::GlobalOp solver, mlir::LLVM::GlobalOp ctx)
Initializes the caches and keeps track of the given globals to store the pointers to the SMT solver a...
const mlir::LLVM::GlobalOp ctx
The global storing the pointer to the SMT context object currently active.
Definition: SMTToZ3LLVM.h:59
const mlir::LLVM::GlobalOp solver
The global storing the pointer to the SMT solver object currently active.
Definition: SMTToZ3LLVM.h:56
DenseMap< Block *, Value > ctxCache
Definition: SMTToZ3LLVM.h:63