25#include <mlir/IR/Builders.h>
26#include <mlir/IR/SymbolTable.h>
27#include <mlir/Transforms/Inliner.h>
28#include <mlir/Transforms/InliningUtils.h>
30#include <llvm/Support/Debug.h>
36#define GEN_PASS_DEF_COMPUTECONSTRAINTOPRODUCTPASS
40#define DEBUG_TYPE "llzk-compute-constrain-to-product-pass"
53 OpBuilder funcBuilder(compute);
56 compute.walk([&funcBuilder](Operation *op) {
60 constrain.walk([&funcBuilder](Operation *op) {
66 funcBuilder, funcBuilder.getFusedLoc({compute.getLoc(), constrain.getLoc()}),
70 Block *entryBlock = productFunc.addEntryBlock();
71 funcBuilder.setInsertionPointToStart(entryBlock);
78 llvm::SmallVector<Value> args {productFunc.getArguments()};
82 args.insert(args.begin(), computeCall->getResult(0));
84 ReturnOp::create(funcBuilder, funcBuilder.getUnknownLoc(), computeCall->getResult(0));
87 InlinerInterface inliner(productFunc.getContext());
88 InlinerConfig inlinerConfig;
89 if (failed(inlineCall(
90 inliner, inlinerConfig.getCloneCallback(), computeCall, compute, &compute.
getBody(),
true
95 if (failed(inlineCall(
96 inliner, inlinerConfig.getCloneCallback(), constrainCall,
constrain, &
constrain.getBody(),
102 computeCall->erase();
103 constrainCall->erase();
117 llvm::SetVector<CallOp> computeCalls, constrainCalls;
118 product.walk([&](
CallOp callOp) {
120 computeCalls.insert(callOp);
122 constrainCalls.insert(callOp);
126 llvm::SetVector<std::pair<CallOp, CallOp>> alignedCalls;
130 auto doCallsMatch = [&](CallOp compute, CallOp constrain) ->
bool {
132 llvm::outs() <<
"Asking for equivalence between calls\n"
133 << compute <<
"\nand\n"
134 << constrain <<
"\n\n";
135 llvm::outs() <<
"In block:\n\n" << *compute->getBlock() <<
'\n';
140 if (computeStruct != constrainStruct) {
143 if (compute.getNumOperands() == 0) {
146 for (
unsigned i = 0, e = compute->getNumOperands() - 1; i < e; i++) {
147 if (!equivalence.areSignalsEquivalent(compute->getOperand(i), constrain->getOperand(i + 1))) {
155 for (
auto compute : computeCalls) {
157 auto matches = llvm::filter_to_vector(constrainCalls, [&](CallOp constrain) {
158 return doCallsMatch(compute, constrain);
161 if (matches.size() == 1) {
162 alignedCalls.insert({compute, matches[0]});
163 computeCalls.remove(compute);
164 constrainCalls.remove(matches[0]);
168 if (!computeCalls.empty() && constrainCalls.empty()) {
169 product.emitWarning()
174 for (
auto [compute, constrain] : alignedCalls) {
177 if (failed(calleeTgt)) {
180 auto newRoot = calleeTgt->get()->getParentOfType<StructDefOp>();
182 FuncDefOp newProduct =
183 alignFuncs(newRoot, newRoot.getComputeFuncOp(), newRoot.getConstrainFuncOp());
189 OpBuilder callBuilder(compute);
191 callBuilder, callBuilder.getFusedLoc({compute.getLoc(), constrain.getLoc()}), newProduct,
192 compute.getOperands()
194 compute->replaceAllUsesWith(newCall.getResults());
206 if (!computeFunc || !constrainFunc) {
219LogicalResult alignStartingAt(
223 if (!isValidRoot(root)) {
235class PassImpl :
public llzk::impl::ComputeConstrainToProductPassBase<PassImpl> {
236 using Base = ComputeConstrainToProductPassBase<PassImpl>;
239 void runOnOperation()
override {
240 ModuleOp
mod = getOperation();
243 SymbolTableCollection tables;
244 LightweightSignalEquivalenceAnalysis equivalence {
245 getAnalysis<LightweightSignalEquivalenceAnalysis>()
249 mod.walk([&root,
this](StructDefOp structDef) {
256 mod.emitError().append(
"could not find root struct \"", rootStruct,
"\"").report();
261 if (failed(alignStartingAt(root, tables, equivalence))) {
std::vector< component::StructDefOp > alignedStructs
function::FuncDefOp alignFuncs(component::StructDefOp root, function::FuncDefOp compute, function::FuncDefOp constrain)
mlir::LogicalResult alignCalls(function::FuncDefOp product)
::llvm::StringRef getSymName()
::llzk::function::FuncDefOp getProductFuncOp()
Gets the FuncDefOp that defines the product function in this structure, if present,...
::llzk::function::FuncDefOp getConstrainFuncOp()
Gets the FuncDefOp that defines the constrain function in this structure, if present,...
::llzk::function::FuncDefOp getComputeFuncOp()
Gets the FuncDefOp that defines the compute function in this structure, if present,...
bool calleeIsStructConstrain()
Return true iff the callee function name is FUNC_NAME_CONSTRAIN within a StructDefOp.
bool calleeIsStructCompute()
Return true iff the callee function name is FUNC_NAME_COMPUTE within a StructDefOp.
::mlir::SymbolRefAttr getCallee()
static CallOp create(::mlir::OpBuilder &builder, ::mlir::Location location, ::mlir::TypeRange resultTypes, ::mlir::SymbolRefAttr callee, ::mlir::ValueRange argOperands={}, ::llvm::ArrayRef<::mlir::Attribute > templateParams={})
::mlir::FailureOr<::llzk::SymbolLookupResult<::llzk::function::FuncDefOp > > getCalleeTarget(::mlir::SymbolTableCollection &tables)
Resolve and return the target FuncDefOp for this CallOp.
static FuncDefOp create(::mlir::OpBuilder &builder, ::mlir::Location location, ::llvm::StringRef name, ::mlir::FunctionType type, ::llvm::ArrayRef<::mlir::NamedAttribute > attrs={}, ::llvm::ArrayRef<::mlir::DictionaryAttr > argAttrs={})
::mlir::FunctionType getFunctionType()
void setAllowNonNativeFieldOpsAttr(bool newValue=true)
Add (resp. remove) the allow_non_native_field_ops attribute to (resp. from) the function def.
bool hasAllowNonNativeFieldOpsAttr()
Return true iff the function def has the allow_non_native_field_ops attribute.
::mlir::Region & getBody()
static ReturnOp create(::mlir::OpBuilder &builder, ::mlir::Location location)
constexpr char FUNC_NAME_COMPUTE[]
Symbol name for the witness generation (and resp.
mlir::SymbolRefAttr getPrefixAsSymbolRefAttr(mlir::SymbolRefAttr symbol)
Return SymbolRefAttr like the one given but with the leaf/final element removed.
ExpressionValue mod(const llvm::SMTSolverRef &solver, const ExpressionValue &lhs, const ExpressionValue &rhs)
constexpr char PRODUCT_SOURCE[]
Name of the attribute on aligned product program ops that specifies where they came from.
constexpr char FUNC_NAME_CONSTRAIN[]
constexpr char FUNC_NAME_PRODUCT[]
constexpr char DERIVED_ATTR_NAME[]
Name of the attribute on a @product func that has been automatically aligned from @compute + @constra...