[Mlir-commits] [mlir] [mlir][smt] add arith-to-smt (PR #131484)
Maksim Levental
llvmlistbot at llvm.org
Thu Jun 12 07:55:51 PDT 2025
https://github.com/makslevental updated https://github.com/llvm/llvm-project/pull/131484
>From c752791e84c2ed6b3cab28cfdad1186cc4e812a2 Mon Sep 17 00:00:00 2001
From: max <maksim.levental at gmail.com>
Date: Sat, 15 Mar 2025 21:53:52 -0400
Subject: [PATCH] [mlir][smt] add arith-to-smt
---
.../mlir/Conversion/ArithToSMT/ArithToSMT.h | 30 ++
mlir/include/mlir/Conversion/Passes.h | 1 +
mlir/include/mlir/Conversion/Passes.td | 13 +
mlir/include/mlir/InitAllPasses.h | 1 +
mlir/lib/Conversion/ArithToSMT/ArithToSMT.cpp | 351 ++++++++++++++++++
mlir/lib/Conversion/ArithToSMT/CMakeLists.txt | 14 +
mlir/lib/Conversion/CMakeLists.txt | 1 +
.../Conversion/ArithToSMT/arith-to-smt.mlir | 87 +++++
8 files changed, 498 insertions(+)
create mode 100644 mlir/include/mlir/Conversion/ArithToSMT/ArithToSMT.h
create mode 100644 mlir/lib/Conversion/ArithToSMT/ArithToSMT.cpp
create mode 100644 mlir/lib/Conversion/ArithToSMT/CMakeLists.txt
create mode 100644 mlir/test/Conversion/ArithToSMT/arith-to-smt.mlir
diff --git a/mlir/include/mlir/Conversion/ArithToSMT/ArithToSMT.h b/mlir/include/mlir/Conversion/ArithToSMT/ArithToSMT.h
new file mode 100644
index 0000000000000..5bb76321199ee
--- /dev/null
+++ b/mlir/include/mlir/Conversion/ArithToSMT/ArithToSMT.h
@@ -0,0 +1,30 @@
+//===- ArithToSMT.h - Arith to SMT dialect conversion ---------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef MLIR_CONVERSION_ARITHTOSMT_H
+#define MLIR_CONVERSION_ARITHTOSMT_H
+
+#include "mlir/Pass/Pass.h"
+#include <memory>
+
+namespace mlir {
+
+class TypeConverter;
+class RewritePatternSet;
+
+#define GEN_PASS_DECL_CONVERTARITHTOSMT
+#include "mlir/Conversion/Passes.h.inc"
+
+namespace arith {
+/// Get the Arith to SMT conversion patterns.
+void populateArithToSMTConversionPatterns(TypeConverter &converter,
+ RewritePatternSet &patterns);
+} // namespace arith
+} // namespace mlir
+
+#endif // MLIR_CONVERSION_ARITHTOSMT_H
diff --git a/mlir/include/mlir/Conversion/Passes.h b/mlir/include/mlir/Conversion/Passes.h
index c9d2a54433736..9b1b2b893b6f5 100644
--- a/mlir/include/mlir/Conversion/Passes.h
+++ b/mlir/include/mlir/Conversion/Passes.h
@@ -15,6 +15,7 @@
#include "mlir/Conversion/ArithToArmSME/ArithToArmSME.h"
#include "mlir/Conversion/ArithToEmitC/ArithToEmitCPass.h"
#include "mlir/Conversion/ArithToLLVM/ArithToLLVM.h"
+#include "mlir/Conversion/ArithToSMT/ArithToSMT.h"
#include "mlir/Conversion/ArithToSPIRV/ArithToSPIRV.h"
#include "mlir/Conversion/ArmNeon2dToIntr/ArmNeon2dToIntr.h"
#include "mlir/Conversion/ArmSMEToLLVM/ArmSMEToLLVM.h"
diff --git a/mlir/include/mlir/Conversion/Passes.td b/mlir/include/mlir/Conversion/Passes.td
index b496ee0114910..dca3f5e454781 100644
--- a/mlir/include/mlir/Conversion/Passes.td
+++ b/mlir/include/mlir/Conversion/Passes.td
@@ -1493,4 +1493,17 @@ def ConvertVectorToXeGPU : Pass<"convert-vector-to-xegpu"> {
];
}
+//===----------------------------------------------------------------------===//
+// ConvertArithToSMT
+//===----------------------------------------------------------------------===//
+
+def ConvertArithToSMT : Pass<"convert-arith-to-smt"> {
+ let summary = "Convert arith ops and constants to SMT ops";
+ let dependentDialects = [
+ "smt::SMTDialect",
+ "arith::ArithDialect",
+ "mlir::func::FuncDialect"
+ ];
+}
+
#endif // MLIR_CONVERSION_PASSES
diff --git a/mlir/include/mlir/InitAllPasses.h b/mlir/include/mlir/InitAllPasses.h
index dd8b292a87344..bb8dff47ab480 100644
--- a/mlir/include/mlir/InitAllPasses.h
+++ b/mlir/include/mlir/InitAllPasses.h
@@ -95,6 +95,7 @@ inline void registerAllPasses() {
arm_sve::registerArmSVEPasses();
emitc::registerEmitCPasses();
xegpu::registerXeGPUPasses();
+ registerConvertArithToSMTPass();
// Dialect pipelines
bufferization::registerBufferizationPipelines();
diff --git a/mlir/lib/Conversion/ArithToSMT/ArithToSMT.cpp b/mlir/lib/Conversion/ArithToSMT/ArithToSMT.cpp
new file mode 100644
index 0000000000000..6b8714a5a1c44
--- /dev/null
+++ b/mlir/lib/Conversion/ArithToSMT/ArithToSMT.cpp
@@ -0,0 +1,351 @@
+//===- ArithToSMT.cpp
+//------------------------------------------------------===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#include "mlir/Conversion/ArithToSMT/ArithToSMT.h"
+#include "mlir/Dialect/Arith/IR/Arith.h"
+#include "mlir/Dialect/Func/IR/FuncOps.h"
+#include "mlir/Dialect/SMT/IR/SMTOps.h"
+#include "mlir/Pass/Pass.h"
+#include "mlir/Transforms/DialectConversion.h"
+#include "mlir/Transforms/GreedyPatternRewriteDriver.h"
+#include "mlir/Transforms/WalkPatternRewriteDriver.h"
+
+#include "llvm/Support/Debug.h"
+
+namespace mlir {
+#define GEN_PASS_DEF_CONVERTARITHTOSMT
+#include "mlir/Conversion/Passes.h.inc"
+} // namespace mlir
+
+using namespace mlir;
+
+//===----------------------------------------------------------------------===//
+// Conversion patterns
+//===----------------------------------------------------------------------===//
+
+namespace {
+
+/// Lower a arith::CmpIOp operation to a smt::BVCmpOp, smt::EqOp or
+/// smt::DistinctOp
+///
+struct CmpIOpConversion : OpConversionPattern<arith::CmpIOp> {
+ using OpConversionPattern<arith::CmpIOp>::OpConversionPattern;
+
+ LogicalResult
+ matchAndRewrite(arith::CmpIOp op, OpAdaptor adaptor,
+ ConversionPatternRewriter &rewriter) const override {
+ if (adaptor.getPredicate() == arith::CmpIPredicate::eq) {
+ rewriter.replaceOpWithNewOp<smt::EqOp>(op, adaptor.getLhs(),
+ adaptor.getRhs());
+ return success();
+ }
+
+ if (adaptor.getPredicate() == arith::CmpIPredicate::ne) {
+ rewriter.replaceOpWithNewOp<smt::DistinctOp>(op, adaptor.getLhs(),
+ adaptor.getRhs());
+ return success();
+ }
+
+ smt::BVCmpPredicate pred;
+ switch (adaptor.getPredicate()) {
+ case arith::CmpIPredicate::sge:
+ pred = smt::BVCmpPredicate::sge;
+ break;
+ case arith::CmpIPredicate::sgt:
+ pred = smt::BVCmpPredicate::sgt;
+ break;
+ case arith::CmpIPredicate::sle:
+ pred = smt::BVCmpPredicate::sle;
+ break;
+ case arith::CmpIPredicate::slt:
+ pred = smt::BVCmpPredicate::slt;
+ break;
+ case arith::CmpIPredicate::uge:
+ pred = smt::BVCmpPredicate::uge;
+ break;
+ case arith::CmpIPredicate::ugt:
+ pred = smt::BVCmpPredicate::ugt;
+ break;
+ case arith::CmpIPredicate::ule:
+ pred = smt::BVCmpPredicate::ule;
+ break;
+ case arith::CmpIPredicate::ult:
+ pred = smt::BVCmpPredicate::ult;
+ break;
+ default:
+ llvm_unreachable("all cases handled above");
+ }
+
+ rewriter.replaceOpWithNewOp<smt::BVCmpOp>(op, pred, adaptor.getLhs(),
+ adaptor.getRhs());
+ return success();
+ }
+};
+
+/// Lower a arith::SubOp operation to an smt::BVNegOp + smt::BVAddOp
+struct SubOpConversion : OpConversionPattern<arith::SubIOp> {
+ using OpConversionPattern<arith::SubIOp>::OpConversionPattern;
+
+ LogicalResult
+ matchAndRewrite(arith::SubIOp op, OpAdaptor adaptor,
+ ConversionPatternRewriter &rewriter) const override {
+ Value negRhs = rewriter.create<smt::BVNegOp>(op.getLoc(), adaptor.getRhs());
+ rewriter.replaceOpWithNewOp<smt::BVAddOp>(op, adaptor.getLhs(), negRhs);
+ return success();
+ }
+};
+
+/// Lower the SourceOp to the TargetOp one-to-one.
+template <typename SourceOp, typename TargetOp>
+struct OneToOneOpConversion : OpConversionPattern<SourceOp> {
+ using OpConversionPattern<SourceOp>::OpConversionPattern;
+ using OpAdaptor = typename SourceOp::Adaptor;
+
+ LogicalResult
+ matchAndRewrite(SourceOp op, OpAdaptor adaptor,
+ ConversionPatternRewriter &rewriter) const override {
+
+ rewriter.replaceOpWithNewOp<TargetOp>(
+ op,
+ OpConversionPattern<SourceOp>::typeConverter->convertType(
+ op.getResult().getType()),
+ adaptor.getOperands());
+ return success();
+ }
+};
+
+struct CeilDivSIOpConversion : OpConversionPattern<arith::CeilDivSIOp> {
+ using OpConversionPattern<arith::CeilDivSIOp>::OpConversionPattern;
+
+ LogicalResult
+ matchAndRewrite(arith::CeilDivSIOp op, OpAdaptor adaptor,
+ ConversionPatternRewriter &rewriter) const override {
+ auto numPlusDenom = rewriter.createOrFold<arith::AddIOp>(
+ op.getLoc(), adaptor.getLhs(), adaptor.getRhs());
+ auto bitWidth =
+ llvm::cast<IntegerType>(getElementTypeOrSelf(adaptor.getLhs()))
+ .getWidth();
+ auto one = rewriter.create<arith::ConstantIntOp>(op.getLoc(), 1, bitWidth);
+ auto numPlusDenomMinusOne =
+ rewriter.createOrFold<arith::SubIOp>(op.getLoc(), numPlusDenom, one);
+ rewriter.replaceOpWithNewOp<arith::DivSIOp>(op, numPlusDenomMinusOne,
+ adaptor.getRhs());
+ return success();
+ }
+};
+
+/// Lower the SourceOp to the TargetOp special-casing if the second operand is
+/// zero to return a new symbolic value.
+template <typename SourceOp, typename TargetOp>
+struct DivisionOpConversion : OpConversionPattern<SourceOp> {
+ using OpConversionPattern<SourceOp>::OpConversionPattern;
+ using OpAdaptor = typename SourceOp::Adaptor;
+
+ LogicalResult
+ matchAndRewrite(SourceOp op, OpAdaptor adaptor,
+ ConversionPatternRewriter &rewriter) const override {
+ Location loc = op.getLoc();
+ auto type = dyn_cast<smt::BitVectorType>(adaptor.getRhs().getType());
+ if (!type)
+ return failure();
+
+ auto resultType = OpConversionPattern<SourceOp>::typeConverter->convertType(
+ op.getResult().getType());
+ Value zero =
+ rewriter.create<smt::BVConstantOp>(loc, APInt(type.getWidth(), 0));
+ Value isZero = rewriter.create<smt::EqOp>(loc, adaptor.getRhs(), zero);
+ Value symbolicVal = rewriter.create<smt::DeclareFunOp>(loc, resultType);
+ Value division =
+ rewriter.create<TargetOp>(loc, resultType, adaptor.getOperands());
+ rewriter.replaceOpWithNewOp<smt::IteOp>(op, isZero, symbolicVal, division);
+ return success();
+ }
+};
+
+/// Converts an operation with a variadic number of operands to a chain of
+/// binary operations assuming left-associativity of the operation.
+template <typename SourceOp, typename TargetOp>
+struct VariadicToBinaryOpConversion : OpConversionPattern<SourceOp> {
+ using OpConversionPattern<SourceOp>::OpConversionPattern;
+ using OpAdaptor = typename SourceOp::Adaptor;
+
+ LogicalResult
+ matchAndRewrite(SourceOp op, OpAdaptor adaptor,
+ ConversionPatternRewriter &rewriter) const override {
+
+ ValueRange operands = adaptor.getOperands();
+ if (operands.size() < 2)
+ return failure();
+
+ Value runner = operands[0];
+ for (Value operand : operands.drop_front())
+ runner = rewriter.create<TargetOp>(op.getLoc(), runner, operand);
+
+ rewriter.replaceOp(op, runner);
+ return success();
+ }
+};
+
+/// Lower a arith::ConstantOp operation to smt::BVConstantOp
+struct ArithConstantIntOpConversion
+ : OpConversionPattern<arith::ConstantIntOp> {
+ using OpConversionPattern<arith::ConstantIntOp>::OpConversionPattern;
+
+ LogicalResult
+ matchAndRewrite(arith::ConstantIntOp op, OpAdaptor adaptor,
+ ConversionPatternRewriter &rewriter) const override {
+ auto v = llvm::cast<IntegerAttr>(adaptor.getValue());
+ if (v.getValue().getBitWidth() < 1)
+ return rewriter.notifyMatchFailure(op.getLoc(),
+ "0-bit constants not supported");
+ // TODO(max): signed/unsigned/signless semenatics
+ rewriter.replaceOpWithNewOp<smt::BVConstantOp>(op, v.getValue());
+ return success();
+ }
+};
+
+} // namespace
+
+void populateArithToSMTTypeConverter(TypeConverter &converter) {
+ // The semantics of the builtin integer at the MLIR core level is currently
+ // not very well defined. It is used for two-valued, four-valued, and possible
+ // other multi-valued logic. Here, we interpret it as two-valued for now.
+ // From a formal perspective, MLIR would ideally define its own types for
+ // two-valued, four-valued, nine-valued (etc.) logic each. In MLIR upstream
+ // the integer type also carries poison information (which we don't have in
+ // MLIR?).
+ converter.addConversion([](IntegerType type) -> std::optional<Type> {
+ if (type.getWidth() <= 0)
+ return std::nullopt;
+ return smt::BitVectorType::get(type.getContext(), type.getWidth());
+ });
+
+ // Default target materialization to convert from illegal types to legal
+ // types, e.g., at the boundary of an inlined child block.
+ converter.addTargetMaterialization([&](OpBuilder &builder, Type resultType,
+ ValueRange inputs,
+ Location loc) -> Value {
+ return builder
+ .create<mlir::UnrealizedConversionCastOp>(loc, resultType, inputs)
+ ->getResult(0);
+ });
+
+ // Convert a 'smt.bool'-typed value to a 'smt.bv<N>'-typed value
+ converter.addTargetMaterialization(
+ [&](OpBuilder &builder, smt::BitVectorType resultType, ValueRange inputs,
+ Location loc) -> Value {
+ if (inputs.size() != 1)
+ return Value();
+
+ if (!isa<smt::BoolType>(inputs[0].getType()))
+ return Value();
+
+ unsigned width = resultType.getWidth();
+ Value constZero = builder.create<smt::BVConstantOp>(loc, 0, width);
+ Value constOne = builder.create<smt::BVConstantOp>(loc, 1, width);
+ return builder.create<smt::IteOp>(loc, inputs[0], constOne, constZero);
+ });
+
+ // Convert an unrealized conversion cast from 'smt.bool' to i1
+ // into a direct conversion from 'smt.bool' to 'smt.bv<1>'.
+ converter.addTargetMaterialization(
+ [&](OpBuilder &builder, smt::BitVectorType resultType, ValueRange inputs,
+ Location loc) -> Value {
+ if (inputs.size() != 1 || resultType.getWidth() != 1)
+ return Value();
+
+ auto intType = dyn_cast<IntegerType>(inputs[0].getType());
+ if (!intType || intType.getWidth() != 1)
+ return Value();
+
+ auto castOp =
+ inputs[0].getDefiningOp<mlir::UnrealizedConversionCastOp>();
+ if (!castOp || castOp.getInputs().size() != 1)
+ return Value();
+
+ if (!isa<smt::BoolType>(castOp.getInputs()[0].getType()))
+ return Value();
+
+ Value constZero = builder.create<smt::BVConstantOp>(loc, 0, 1);
+ Value constOne = builder.create<smt::BVConstantOp>(loc, 1, 1);
+ return builder.create<smt::IteOp>(loc, castOp.getInputs()[0], constOne,
+ constZero);
+ });
+
+ // Convert a 'smt.bv<1>'-typed value to a 'smt.bool'-typed value
+ converter.addTargetMaterialization(
+ [&](OpBuilder &builder, smt::BoolType resultType, ValueRange inputs,
+ Location loc) -> Value {
+ if (inputs.size() != 1)
+ return Value();
+
+ auto bvType = dyn_cast<smt::BitVectorType>(inputs[0].getType());
+ if (!bvType || bvType.getWidth() != 1)
+ return Value();
+
+ Value constOne = builder.create<smt::BVConstantOp>(loc, 1, 1);
+ return builder.create<smt::EqOp>(loc, inputs[0], constOne);
+ });
+
+ // Default source materialization to convert from illegal types to legal
+ // types, e.g., at the boundary of an inlined child block.
+ converter.addSourceMaterialization([&](OpBuilder &builder, Type resultType,
+ ValueRange inputs,
+ Location loc) -> Value {
+ return builder
+ .create<mlir::UnrealizedConversionCastOp>(loc, resultType, inputs)
+ ->getResult(0);
+ });
+}
+
+namespace {
+struct ConvertArithToSMT
+ : public impl::ConvertArithToSMTBase<ConvertArithToSMT> {
+ using Base::Base;
+
+ void runOnOperation() override {
+ RewritePatternSet patterns(&getContext());
+ patterns.add<CeilDivSIOpConversion>(&getContext());
+ walkAndApplyPatterns(getOperation(), std::move(patterns));
+
+ ConversionTarget target(getContext());
+ target.addIllegalDialect<arith::ArithDialect>();
+ target.addLegalDialect<smt::SMTDialect>();
+
+ TypeConverter converter;
+ populateArithToSMTTypeConverter(converter);
+ patterns.clear();
+ arith::populateArithToSMTConversionPatterns(converter, patterns);
+
+ if (failed(mlir::applyPartialConversion(getOperation(), target,
+ std::move(patterns))))
+ return signalPassFailure();
+ }
+};
+} // namespace
+
+namespace mlir::arith {
+void populateArithToSMTConversionPatterns(TypeConverter &converter,
+ RewritePatternSet &patterns) {
+ patterns.add<ArithConstantIntOpConversion, CmpIOpConversion, SubOpConversion,
+ OneToOneOpConversion<arith::ShLIOp, smt::BVShlOp>,
+ OneToOneOpConversion<arith::ShRUIOp, smt::BVLShrOp>,
+ OneToOneOpConversion<arith::ShRSIOp, smt::BVAShrOp>,
+ DivisionOpConversion<arith::DivSIOp, smt::BVSDivOp>,
+ DivisionOpConversion<arith::DivUIOp, smt::BVUDivOp>,
+ DivisionOpConversion<arith::RemSIOp, smt::BVSRemOp>,
+ DivisionOpConversion<arith::RemUIOp, smt::BVURemOp>,
+ VariadicToBinaryOpConversion<arith::AddIOp, smt::BVAddOp>,
+ VariadicToBinaryOpConversion<arith::MulIOp, smt::BVMulOp>,
+ VariadicToBinaryOpConversion<arith::AndIOp, smt::BVAndOp>,
+ VariadicToBinaryOpConversion<arith::OrIOp, smt::BVOrOp>,
+ VariadicToBinaryOpConversion<arith::XOrIOp, smt::BVXOrOp>>(
+ converter, patterns.getContext());
+}
+} // namespace mlir::arith
\ No newline at end of file
diff --git a/mlir/lib/Conversion/ArithToSMT/CMakeLists.txt b/mlir/lib/Conversion/ArithToSMT/CMakeLists.txt
new file mode 100644
index 0000000000000..ef9df95568cb4
--- /dev/null
+++ b/mlir/lib/Conversion/ArithToSMT/CMakeLists.txt
@@ -0,0 +1,14 @@
+add_mlir_conversion_library(MLIRCombToSMT
+ ArithToSMT.cpp
+
+ DEPENDS
+ MLIRConversionPassIncGen
+
+ LINK_COMPONENTS
+ Core
+
+ LINK_LIBS PUBLIC
+ MLIRArithDialect
+ MLIRSMT
+ MLIRTransforms
+)
diff --git a/mlir/lib/Conversion/CMakeLists.txt b/mlir/lib/Conversion/CMakeLists.txt
index e4b4974600577..9c573a5d81e39 100644
--- a/mlir/lib/Conversion/CMakeLists.txt
+++ b/mlir/lib/Conversion/CMakeLists.txt
@@ -5,6 +5,7 @@ add_subdirectory(ArithToAMDGPU)
add_subdirectory(ArithToArmSME)
add_subdirectory(ArithToEmitC)
add_subdirectory(ArithToLLVM)
+add_subdirectory(ArithToSMT)
add_subdirectory(ArithToSPIRV)
add_subdirectory(ArmNeon2dToIntr)
add_subdirectory(ArmSMEToSCF)
diff --git a/mlir/test/Conversion/ArithToSMT/arith-to-smt.mlir b/mlir/test/Conversion/ArithToSMT/arith-to-smt.mlir
new file mode 100644
index 0000000000000..a1cf033a461c5
--- /dev/null
+++ b/mlir/test/Conversion/ArithToSMT/arith-to-smt.mlir
@@ -0,0 +1,87 @@
+// RUN: mlir-opt %s --convert-arith-to-smt | FileCheck %s
+
+// CHECK-LABEL: func @test
+// CHECK-SAME: ([[A0:%.+]]: !smt.bv<32>, [[A1:%.+]]: !smt.bv<32>, [[A2:%.+]]: !smt.bv<32>, [[A3:%.+]]: !smt.bv<32>, [[A4:%.+]]: !smt.bv<1>, [[ARG5:%.+]]: !smt.bv<4>)
+func.func @test(%a0: !smt.bv<32>, %a1: !smt.bv<32>, %a2: !smt.bv<32>, %a3: !smt.bv<32>, %a4: !smt.bv<1>, %a5: !smt.bv<4>) {
+ %arg0 = builtin.unrealized_conversion_cast %a0 : !smt.bv<32> to i32
+ %arg1 = builtin.unrealized_conversion_cast %a1 : !smt.bv<32> to i32
+ %arg2 = builtin.unrealized_conversion_cast %a2 : !smt.bv<32> to i32
+ %arg3 = builtin.unrealized_conversion_cast %a3 : !smt.bv<32> to i32
+ %arg4 = builtin.unrealized_conversion_cast %a4 : !smt.bv<1> to i1
+ %arg5 = builtin.unrealized_conversion_cast %a5 : !smt.bv<4> to i4
+
+ // CHECK: [[ZERO:%.+]] = smt.bv.constant #smt.bv<0> : !smt.bv<32>
+ // CHECK-NEXT: [[IS_ZERO:%.+]] = smt.eq [[A1]], [[ZERO]] : !smt.bv<32>
+ // CHECK-NEXT: [[UNDEF:%.+]] = smt.declare_fun : !smt.bv<32>
+ // CHECK-NEXT: [[DIV:%.+]] = smt.bv.sdiv [[A0]], [[A1]] : !smt.bv<32>
+ // CHECK-NEXT: smt.ite [[IS_ZERO]], [[UNDEF]], [[DIV]] : !smt.bv<32>
+ %0 = arith.divsi %arg0, %arg1 : i32
+ // CHECK-NEXT: [[ZERO:%.+]] = smt.bv.constant #smt.bv<0> : !smt.bv<32>
+ // CHECK-NEXT: [[IS_ZERO:%.+]] = smt.eq [[A1]], [[ZERO]] : !smt.bv<32>
+ // CHECK-NEXT: [[UNDEF:%.+]] = smt.declare_fun : !smt.bv<32>
+ // CHECK-NEXT: [[DIV:%.+]] = smt.bv.udiv [[A0]], [[A1]] : !smt.bv<32>
+ // CHECK-NEXT: smt.ite [[IS_ZERO]], [[UNDEF]], [[DIV]] : !smt.bv<32>
+ %1 = arith.divui %arg0, %arg1 : i32
+ // CHECK-NEXT: [[ZERO:%.+]] = smt.bv.constant #smt.bv<0> : !smt.bv<32>
+ // CHECK-NEXT: [[IS_ZERO:%.+]] = smt.eq [[A1]], [[ZERO]] : !smt.bv<32>
+ // CHECK-NEXT: [[UNDEF:%.+]] = smt.declare_fun : !smt.bv<32>
+ // CHECK-NEXT: [[DIV:%.+]] = smt.bv.srem [[A0]], [[A1]] : !smt.bv<32>
+ // CHECK-NEXT: smt.ite [[IS_ZERO]], [[UNDEF]], [[DIV]] : !smt.bv<32>
+ %2 = arith.remsi %arg0, %arg1 : i32
+ // CHECK-NEXT: [[ZERO:%.+]] = smt.bv.constant #smt.bv<0> : !smt.bv<32>
+ // CHECK-NEXT: [[IS_ZERO:%.+]] = smt.eq [[A1]], [[ZERO]] : !smt.bv<32>
+ // CHECK-NEXT: [[UNDEF:%.+]] = smt.declare_fun : !smt.bv<32>
+ // CHECK-NEXT: [[DIV:%.+]] = smt.bv.urem [[A0]], [[A1]] : !smt.bv<32>
+ // CHECK-NEXT: smt.ite [[IS_ZERO]], [[UNDEF]], [[DIV]] : !smt.bv<32>
+ %3 = arith.remui %arg0, %arg1 : i32
+
+ // CHECK-NEXT: [[NEG:%.+]] = smt.bv.neg [[A1]] : !smt.bv<32>
+ // CHECK-NEXT: smt.bv.add [[A0]], [[NEG]] : !smt.bv<32>
+ %7 = arith.subi %arg0, %arg1 : i32
+
+ // CHECK-NEXT: [[A5:%.+]] = smt.bv.add [[A0]], [[A1]] : !smt.bv<32>
+ %8 = arith.addi %arg0, %arg1 : i32
+ // CHECK-NEXT: [[B1:%.+]] = smt.bv.mul [[A0]], [[A1]] : !smt.bv<32>
+ %9 = arith.muli %arg0, %arg1 : i32
+ // CHECK-NEXT: [[C1:%.+]] = smt.bv.and [[A0]], [[A1]] : !smt.bv<32>
+ %10 = arith.andi %arg0, %arg1 : i32
+ // CHECK-NEXT: [[D1:%.+]] = smt.bv.or [[A0]], [[A1]] : !smt.bv<32>
+ %11 = arith.ori %arg0, %arg1 : i32
+ // CHECK-NEXT: [[E1:%.+]] = smt.bv.xor [[A0]], [[A1]] : !smt.bv<32>
+ %12 = arith.xori %arg0, %arg1 : i32
+
+ // CHECK-NEXT: smt.eq [[A0]], [[A1]] : !smt.bv<32>
+ %14 = arith.cmpi eq, %arg0, %arg1 : i32
+ // CHECK-NEXT: smt.distinct [[A0]], [[A1]] : !smt.bv<32>
+ %15 = arith.cmpi ne, %arg0, %arg1 : i32
+ // CHECK-NEXT: smt.bv.cmp sle [[A0]], [[A1]] : !smt.bv<32>
+ %20 = arith.cmpi sle, %arg0, %arg1 : i32
+ // CHECK-NEXT: smt.bv.cmp slt [[A0]], [[A1]] : !smt.bv<32>
+ %21 = arith.cmpi slt, %arg0, %arg1 : i32
+ // CHECK-NEXT: smt.bv.cmp ule [[A0]], [[A1]] : !smt.bv<32>
+ %22 = arith.cmpi ule, %arg0, %arg1 : i32
+ // CHECK-NEXT: smt.bv.cmp ult [[A0]], [[A1]] : !smt.bv<32>
+ %23 = arith.cmpi ult, %arg0, %arg1 : i32
+ // CHECK-NEXT: smt.bv.cmp sge [[A0]], [[A1]] : !smt.bv<32>
+ %24 = arith.cmpi sge, %arg0, %arg1 : i32
+ // CHECK-NEXT: smt.bv.cmp sgt [[A0]], [[A1]] : !smt.bv<32>
+ %25 = arith.cmpi sgt, %arg0, %arg1 : i32
+ // CHECK-NEXT: smt.bv.cmp uge [[A0]], [[A1]] : !smt.bv<32>
+ %26 = arith.cmpi uge, %arg0, %arg1 : i32
+ // CHECK-NEXT: smt.bv.cmp ugt [[A0]], [[A1]] : !smt.bv<32>
+ %27 = arith.cmpi ugt, %arg0, %arg1 : i32
+
+ // CHECK-NEXT: %{{.*}} = smt.bv.shl [[A0]], [[A1]] : !smt.bv<32>
+ %32 = arith.shli %arg0, %arg1 : i32
+ // CHECK-NEXT: %{{.*}} = smt.bv.ashr [[A0]], [[A1]] : !smt.bv<32>
+ %33 = arith.shrsi %arg0, %arg1 : i32
+ // CHECK-NEXT: %{{.*}} = smt.bv.lshr [[A0]], [[A1]] : !smt.bv<32>
+ %34 = arith.shrui %arg0, %arg1 : i32
+
+ // The arith.cmpi folder is called before the conversion patterns and produces
+ // a `arith.constant` operation.
+ // CHECK-NEXT: smt.bv.constant #smt.bv<-1> : !smt.bv<1>
+ %35 = arith.cmpi eq, %arg0, %arg0 : i32
+
+ return
+}
More information about the Mlir-commits
mailing list