CIRCT  20.0.0git
SMTVisitors.h
Go to the documentation of this file.
1 //===- SMTVisitors.h - SMT Dialect Visitors ---------------------*- 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 visitors that make it easier to work with the SMT IR.
10 //
11 //===----------------------------------------------------------------------===//
12 
13 #ifndef CIRCT_DIALECT_SMT_SMTVISITORS_H
14 #define CIRCT_DIALECT_SMT_SMTVISITORS_H
15 
17 #include "llvm/ADT/TypeSwitch.h"
18 
19 namespace circt {
20 namespace smt {
21 
22 /// This helps visit SMT nodes.
23 template <typename ConcreteType, typename ResultType = void,
24  typename... ExtraArgs>
25 class SMTOpVisitor {
26 public:
27  ResultType dispatchSMTOpVisitor(Operation *op, ExtraArgs... args) {
28  auto *thisCast = static_cast<ConcreteType *>(this);
29  return TypeSwitch<Operation *, ResultType>(op)
30  .template Case<
31  // Constants
32  BoolConstantOp, IntConstantOp, BVConstantOp,
33  // Bit-vector arithmetic
34  BVNegOp, BVAddOp, BVMulOp, BVURemOp, BVSRemOp, BVSModOp, BVShlOp,
35  BVLShrOp, BVAShrOp, BVUDivOp, BVSDivOp,
36  // Bit-vector bitwise
37  BVNotOp, BVAndOp, BVOrOp, BVXOrOp,
38  // Other bit-vector ops
39  ConcatOp, ExtractOp, RepeatOp, BVCmpOp,
40  // Int arithmetic
41  IntAddOp, IntMulOp, IntSubOp, IntDivOp, IntModOp, IntCmpOp,
42  // Core Ops
43  EqOp, DistinctOp, IteOp,
44  // Variable/symbol declaration
45  DeclareFunOp, ApplyFuncOp,
46  // solver interaction
47  SolverOp, AssertOp, ResetOp, PushOp, PopOp, CheckOp,
48  // Boolean logic
49  NotOp, AndOp, OrOp, XOrOp, ImpliesOp,
50  // Arrays
51  ArrayStoreOp, ArraySelectOp, ArrayBroadcastOp,
52  // Quantifiers
53  ForallOp, ExistsOp, YieldOp>([&](auto expr) -> ResultType {
54  return thisCast->visitSMTOp(expr, args...);
55  })
56  .Default([&](auto expr) -> ResultType {
57  return thisCast->visitInvalidSMTOp(op, args...);
58  });
59  }
60 
61  /// This callback is invoked on any non-expression operations.
62  ResultType visitInvalidSMTOp(Operation *op, ExtraArgs... args) {
63  op->emitOpError("unknown SMT node");
64  abort();
65  }
66 
67  /// This callback is invoked on any SMT operations that are not
68  /// handled by the concrete visitor.
69  ResultType visitUnhandledSMTOp(Operation *op, ExtraArgs... args) {
70  return ResultType();
71  }
72 
73 #define HANDLE(OPTYPE, OPKIND) \
74  ResultType visitSMTOp(OPTYPE op, ExtraArgs... args) { \
75  return static_cast<ConcreteType *>(this)->visit##OPKIND##SMTOp(op, \
76  args...); \
77  }
78 
79  // Constants
80  HANDLE(BoolConstantOp, Unhandled);
81  HANDLE(IntConstantOp, Unhandled);
82  HANDLE(BVConstantOp, Unhandled);
83 
84  // Bit-vector arithmetic
85  HANDLE(BVNegOp, Unhandled);
86  HANDLE(BVAddOp, Unhandled);
87  HANDLE(BVMulOp, Unhandled);
88  HANDLE(BVURemOp, Unhandled);
89  HANDLE(BVSRemOp, Unhandled);
90  HANDLE(BVSModOp, Unhandled);
91  HANDLE(BVShlOp, Unhandled);
92  HANDLE(BVLShrOp, Unhandled);
93  HANDLE(BVAShrOp, Unhandled);
94  HANDLE(BVUDivOp, Unhandled);
95  HANDLE(BVSDivOp, Unhandled);
96 
97  // Bit-vector bitwise operations
98  HANDLE(BVNotOp, Unhandled);
99  HANDLE(BVAndOp, Unhandled);
100  HANDLE(BVOrOp, Unhandled);
101  HANDLE(BVXOrOp, Unhandled);
102 
103  // Other bit-vector operations
104  HANDLE(ConcatOp, Unhandled);
105  HANDLE(ExtractOp, Unhandled);
106  HANDLE(RepeatOp, Unhandled);
107  HANDLE(BVCmpOp, Unhandled);
108 
109  // Int arithmetic
110  HANDLE(IntAddOp, Unhandled);
111  HANDLE(IntMulOp, Unhandled);
112  HANDLE(IntSubOp, Unhandled);
113  HANDLE(IntDivOp, Unhandled);
114  HANDLE(IntModOp, Unhandled);
115 
116  HANDLE(IntCmpOp, Unhandled);
117 
118  HANDLE(EqOp, Unhandled);
119  HANDLE(DistinctOp, Unhandled);
120  HANDLE(IteOp, Unhandled);
121 
122  HANDLE(DeclareFunOp, Unhandled);
123  HANDLE(ApplyFuncOp, Unhandled);
124 
125  HANDLE(SolverOp, Unhandled);
126  HANDLE(AssertOp, Unhandled);
127  HANDLE(ResetOp, Unhandled);
128  HANDLE(PushOp, Unhandled);
129  HANDLE(PopOp, Unhandled);
130  HANDLE(CheckOp, Unhandled);
131 
132  // Boolean logic operations
133  HANDLE(NotOp, Unhandled);
134  HANDLE(AndOp, Unhandled);
135  HANDLE(OrOp, Unhandled);
136  HANDLE(XOrOp, Unhandled);
137  HANDLE(ImpliesOp, Unhandled);
138 
139  // Array operations
140  HANDLE(ArrayStoreOp, Unhandled);
141  HANDLE(ArraySelectOp, Unhandled);
142  HANDLE(ArrayBroadcastOp, Unhandled);
143 
144  // Quantifier operations
145  HANDLE(ForallOp, Unhandled);
146  HANDLE(ExistsOp, Unhandled);
147  HANDLE(YieldOp, Unhandled);
148 
149 #undef HANDLE
150 };
151 
152 /// This helps visit SMT types.
153 template <typename ConcreteType, typename ResultType = void,
154  typename... ExtraArgs>
156 public:
157  ResultType dispatchSMTTypeVisitor(Type type, ExtraArgs... args) {
158  auto *thisCast = static_cast<ConcreteType *>(this);
159  return TypeSwitch<Type, ResultType>(type)
160  .template Case<BoolType, IntType, BitVectorType, ArrayType, SMTFuncType,
161  SortType>([&](auto expr) -> ResultType {
162  return thisCast->visitSMTType(expr, args...);
163  })
164  .Default([&](auto expr) -> ResultType {
165  return thisCast->visitInvalidSMTType(type, args...);
166  });
167  }
168 
169  /// This callback is invoked on any non-expression types.
170  ResultType visitInvalidSMTType(Type type, ExtraArgs... args) { abort(); }
171 
172  /// This callback is invoked on any SMT type that are not
173  /// handled by the concrete visitor.
174  ResultType visitUnhandledSMTType(Type type, ExtraArgs... args) {
175  return ResultType();
176  }
177 
178 #define HANDLE(TYPE, KIND) \
179  ResultType visitSMTType(TYPE op, ExtraArgs... args) { \
180  return static_cast<ConcreteType *>(this)->visit##KIND##SMTType(op, \
181  args...); \
182  }
183 
184  HANDLE(BoolType, Unhandled);
185  HANDLE(IntegerType, Unhandled);
186  HANDLE(BitVectorType, Unhandled);
187  HANDLE(ArrayType, Unhandled);
188  HANDLE(SMTFuncType, Unhandled);
189  HANDLE(SortType, Unhandled);
190 
191 #undef HANDLE
192 };
193 
194 } // namespace smt
195 } // namespace circt
196 
197 #endif // CIRCT_DIALECT_SMT_SMTVISITORS_H
This helps visit SMT nodes.
Definition: SMTVisitors.h:25
HANDLE(YieldOp, Unhandled)
HANDLE(PushOp, Unhandled)
HANDLE(BVAddOp, Unhandled)
HANDLE(DeclareFunOp, Unhandled)
HANDLE(BVOrOp, Unhandled)
HANDLE(PopOp, Unhandled)
HANDLE(ForallOp, Unhandled)
HANDLE(NotOp, Unhandled)
HANDLE(BVLShrOp, Unhandled)
HANDLE(ResetOp, Unhandled)
ResultType visitUnhandledSMTOp(Operation *op, ExtraArgs... args)
This callback is invoked on any SMT operations that are not handled by the concrete visitor.
Definition: SMTVisitors.h:69
HANDLE(BVUDivOp, Unhandled)
HANDLE(BVConstantOp, Unhandled)
ResultType visitInvalidSMTOp(Operation *op, ExtraArgs... args)
This callback is invoked on any non-expression operations.
Definition: SMTVisitors.h:62
HANDLE(BVAndOp, Unhandled)
HANDLE(BVMulOp, Unhandled)
HANDLE(IntConstantOp, Unhandled)
HANDLE(IntDivOp, Unhandled)
HANDLE(ApplyFuncOp, Unhandled)
HANDLE(IntModOp, Unhandled)
HANDLE(BVNotOp, Unhandled)
HANDLE(AndOp, Unhandled)
HANDLE(EqOp, Unhandled)
HANDLE(BVShlOp, Unhandled)
HANDLE(SolverOp, Unhandled)
HANDLE(IteOp, Unhandled)
HANDLE(RepeatOp, Unhandled)
HANDLE(OrOp, Unhandled)
HANDLE(BVSRemOp, Unhandled)
HANDLE(IntSubOp, Unhandled)
HANDLE(DistinctOp, Unhandled)
HANDLE(ImpliesOp, Unhandled)
HANDLE(BVAShrOp, Unhandled)
HANDLE(ArraySelectOp, Unhandled)
HANDLE(BVNegOp, Unhandled)
HANDLE(XOrOp, Unhandled)
HANDLE(ArrayBroadcastOp, Unhandled)
HANDLE(BVSDivOp, Unhandled)
HANDLE(ExistsOp, Unhandled)
HANDLE(ArrayStoreOp, Unhandled)
ResultType dispatchSMTOpVisitor(Operation *op, ExtraArgs... args)
Definition: SMTVisitors.h:27
HANDLE(IntMulOp, Unhandled)
HANDLE(BVURemOp, Unhandled)
HANDLE(BVXOrOp, Unhandled)
HANDLE(IntAddOp, Unhandled)
HANDLE(ExtractOp, Unhandled)
HANDLE(BVSModOp, Unhandled)
HANDLE(ConcatOp, Unhandled)
HANDLE(IntCmpOp, Unhandled)
HANDLE(AssertOp, Unhandled)
HANDLE(CheckOp, Unhandled)
HANDLE(BVCmpOp, Unhandled)
HANDLE(BoolConstantOp, Unhandled)
This helps visit SMT types.
Definition: SMTVisitors.h:155
HANDLE(BitVectorType, Unhandled)
HANDLE(ArrayType, Unhandled)
HANDLE(BoolType, Unhandled)
HANDLE(SMTFuncType, Unhandled)
ResultType visitUnhandledSMTType(Type type, ExtraArgs... args)
This callback is invoked on any SMT type that are not handled by the concrete visitor.
Definition: SMTVisitors.h:174
HANDLE(SortType, Unhandled)
ResultType dispatchSMTTypeVisitor(Type type, ExtraArgs... args)
Definition: SMTVisitors.h:157
HANDLE(IntegerType, Unhandled)
ResultType visitInvalidSMTType(Type type, ExtraArgs... args)
This callback is invoked on any non-expression types.
Definition: SMTVisitors.h:170
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.
Definition: DebugAnalysis.h:21