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, 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(CheckOp, Unhandled);
128 
129  // Boolean logic operations
130  HANDLE(NotOp, Unhandled);
131  HANDLE(AndOp, Unhandled);
132  HANDLE(OrOp, Unhandled);
133  HANDLE(XOrOp, Unhandled);
134  HANDLE(ImpliesOp, Unhandled);
135 
136  // Array operations
137  HANDLE(ArrayStoreOp, Unhandled);
138  HANDLE(ArraySelectOp, Unhandled);
139  HANDLE(ArrayBroadcastOp, Unhandled);
140 
141  // Quantifier operations
142  HANDLE(ForallOp, Unhandled);
143  HANDLE(ExistsOp, Unhandled);
144  HANDLE(YieldOp, Unhandled);
145 
146 #undef HANDLE
147 };
148 
149 /// This helps visit SMT types.
150 template <typename ConcreteType, typename ResultType = void,
151  typename... ExtraArgs>
153 public:
154  ResultType dispatchSMTTypeVisitor(Type type, ExtraArgs... args) {
155  auto *thisCast = static_cast<ConcreteType *>(this);
156  return TypeSwitch<Type, ResultType>(type)
157  .template Case<BoolType, IntType, BitVectorType, ArrayType, SMTFuncType,
158  SortType>([&](auto expr) -> ResultType {
159  return thisCast->visitSMTType(expr, args...);
160  })
161  .Default([&](auto expr) -> ResultType {
162  return thisCast->visitInvalidSMTType(type, args...);
163  });
164  }
165 
166  /// This callback is invoked on any non-expression types.
167  ResultType visitInvalidSMTType(Type type, ExtraArgs... args) { abort(); }
168 
169  /// This callback is invoked on any SMT type that are not
170  /// handled by the concrete visitor.
171  ResultType visitUnhandledSMTType(Type type, ExtraArgs... args) {
172  return ResultType();
173  }
174 
175 #define HANDLE(TYPE, KIND) \
176  ResultType visitSMTType(TYPE op, ExtraArgs... args) { \
177  return static_cast<ConcreteType *>(this)->visit##KIND##SMTType(op, \
178  args...); \
179  }
180 
181  HANDLE(BoolType, Unhandled);
182  HANDLE(IntegerType, Unhandled);
183  HANDLE(BitVectorType, Unhandled);
184  HANDLE(ArrayType, Unhandled);
185  HANDLE(SMTFuncType, Unhandled);
186  HANDLE(SortType, Unhandled);
187 
188 #undef HANDLE
189 };
190 
191 } // namespace smt
192 } // namespace circt
193 
194 #endif // CIRCT_DIALECT_SMT_SMTVISITORS_H
This helps visit SMT nodes.
Definition: SMTVisitors.h:25
HANDLE(YieldOp, Unhandled)
HANDLE(BVAddOp, Unhandled)
HANDLE(DeclareFunOp, Unhandled)
HANDLE(BVOrOp, Unhandled)
HANDLE(ForallOp, Unhandled)
HANDLE(NotOp, Unhandled)
HANDLE(BVLShrOp, 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:152
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:171
HANDLE(SortType, Unhandled)
ResultType dispatchSMTTypeVisitor(Type type, ExtraArgs... args)
Definition: SMTVisitors.h:154
HANDLE(IntegerType, Unhandled)
ResultType visitInvalidSMTType(Type type, ExtraArgs... args)
This callback is invoked on any non-expression types.
Definition: SMTVisitors.h:167
The InstanceGraph op interface, see InstanceGraphInterface.td for more details.
Definition: DebugAnalysis.h:21