[Mlir-commits] [mlir] 54e70ac - [mlir][SMT] remove custom forall/exists builder because of asan memory leak
Maksim Levental
llvmlistbot at llvm.org
Fri Apr 11 17:12:43 PDT 2025
Author: Maksim Levental
Date: 2025-04-11T20:12:36-04:00
New Revision: 54e70ac7650f1c22f687937d1a082e4152f97b22
URL: https://github.com/llvm/llvm-project/commit/54e70ac7650f1c22f687937d1a082e4152f97b22
DIFF: https://github.com/llvm/llvm-project/commit/54e70ac7650f1c22f687937d1a082e4152f97b22.diff
LOG: [mlir][SMT] remove custom forall/exists builder because of asan memory leak
Added:
Modified:
mlir/include/mlir/Dialect/SMT/IR/SMTOps.td
mlir/lib/Dialect/SMT/IR/SMTOps.cpp
mlir/unittests/Dialect/SMT/CMakeLists.txt
Removed:
mlir/unittests/Dialect/SMT/QuantifierTest.cpp
################################################################################
diff --git a/mlir/include/mlir/Dialect/SMT/IR/SMTOps.td b/mlir/include/mlir/Dialect/SMT/IR/SMTOps.td
index 1872c00b74f1a..af73955caee54 100644
--- a/mlir/include/mlir/Dialect/SMT/IR/SMTOps.td
+++ b/mlir/include/mlir/Dialect/SMT/IR/SMTOps.td
@@ -448,18 +448,6 @@ class QuantifierOp<string mnemonic> : SMTOp<mnemonic, [
VariadicRegion<SizedRegion<1>>:$patterns);
let results = (outs BoolType:$result);
- let builders = [
- OpBuilder<(ins
- "TypeRange":$boundVarTypes,
- "function_ref<Value(OpBuilder &, Location, ValueRange)>":$bodyBuilder,
- CArg<"std::optional<ArrayRef<StringRef>>", "std::nullopt">:$boundVarNames,
- CArg<"function_ref<ValueRange(OpBuilder &, Location, ValueRange)>",
- "{}">:$patternBuilder,
- CArg<"uint32_t", "0">:$weight,
- CArg<"bool", "false">:$noPattern)>
- ];
- let skipDefaultBuilders = true;
-
let assemblyFormat = [{
($boundVarNames^)? (`no_pattern` $noPattern^)? (`weight` $weight^)?
attr-dict-with-keyword $body (`patterns` $patterns^)?
diff --git a/mlir/lib/Dialect/SMT/IR/SMTOps.cpp b/mlir/lib/Dialect/SMT/IR/SMTOps.cpp
index 8977a3abc125d..604dd26da1982 100644
--- a/mlir/lib/Dialect/SMT/IR/SMTOps.cpp
+++ b/mlir/lib/Dialect/SMT/IR/SMTOps.cpp
@@ -432,16 +432,6 @@ LogicalResult ForallOp::verifyRegions() {
return verifyQuantifierRegions(*this);
}
-void ForallOp::build(
- OpBuilder &odsBuilder, OperationState &odsState, TypeRange boundVarTypes,
- function_ref<Value(OpBuilder &, Location, ValueRange)> bodyBuilder,
- std::optional<ArrayRef<StringRef>> boundVarNames,
- function_ref<ValueRange(OpBuilder &, Location, ValueRange)> patternBuilder,
- uint32_t weight, bool noPattern) {
- buildQuantifier<Properties>(odsBuilder, odsState, boundVarTypes, bodyBuilder,
- boundVarNames, patternBuilder, weight, noPattern);
-}
-
//===----------------------------------------------------------------------===//
// ExistsOp
//===----------------------------------------------------------------------===//
@@ -458,15 +448,5 @@ LogicalResult ExistsOp::verifyRegions() {
return verifyQuantifierRegions(*this);
}
-void ExistsOp::build(
- OpBuilder &odsBuilder, OperationState &odsState, TypeRange boundVarTypes,
- function_ref<Value(OpBuilder &, Location, ValueRange)> bodyBuilder,
- std::optional<ArrayRef<StringRef>> boundVarNames,
- function_ref<ValueRange(OpBuilder &, Location, ValueRange)> patternBuilder,
- uint32_t weight, bool noPattern) {
- buildQuantifier<Properties>(odsBuilder, odsState, boundVarTypes, bodyBuilder,
- boundVarNames, patternBuilder, weight, noPattern);
-}
-
#define GET_OP_CLASSES
#include "mlir/Dialect/SMT/IR/SMT.cpp.inc"
diff --git a/mlir/unittests/Dialect/SMT/CMakeLists.txt b/mlir/unittests/Dialect/SMT/CMakeLists.txt
index a1331467febaa..86e16d6194ea9 100644
--- a/mlir/unittests/Dialect/SMT/CMakeLists.txt
+++ b/mlir/unittests/Dialect/SMT/CMakeLists.txt
@@ -1,6 +1,5 @@
add_mlir_unittest(MLIRSMTTests
AttributeTest.cpp
- QuantifierTest.cpp
TypeTest.cpp
)
diff --git a/mlir/unittests/Dialect/SMT/QuantifierTest.cpp b/mlir/unittests/Dialect/SMT/QuantifierTest.cpp
deleted file mode 100644
index 7bb0c1808ca0a..0000000000000
--- a/mlir/unittests/Dialect/SMT/QuantifierTest.cpp
+++ /dev/null
@@ -1,187 +0,0 @@
-//===- QuantifierTest.cpp - SMT quantifier operation unit tests -----------===//
-//
-// 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/Dialect/SMT/IR/SMTOps.h"
-#include "gtest/gtest.h"
-
-using namespace mlir;
-using namespace smt;
-
-namespace {
-
-//===----------------------------------------------------------------------===//
-// Test custom builders of ExistsOp
-//===----------------------------------------------------------------------===//
-
-TEST(QuantifierTest, ExistsBuilderWithPattern) {
- MLIRContext context;
- context.loadDialect<SMTDialect>();
- Location loc(UnknownLoc::get(&context));
-
- OpBuilder builder(&context);
- auto boolTy = BoolType::get(&context);
-
- ExistsOp existsOp = builder.create<ExistsOp>(
- loc, TypeRange{boolTy, boolTy},
- [](OpBuilder &builder, Location loc, ValueRange boundVars) {
- return builder.create<AndOp>(loc, boundVars);
- },
- std::nullopt,
- [](OpBuilder &builder, Location loc, ValueRange boundVars) {
- return boundVars;
- },
- /*weight=*/2);
-
- SmallVector<char, 1024> buffer;
- llvm::raw_svector_ostream stream(buffer);
- existsOp.print(stream);
-
- ASSERT_STREQ(
- stream.str().str().c_str(),
- "%0 = smt.exists weight 2 {\n^bb0(%arg0: !smt.bool, "
- "%arg1: !smt.bool):\n %0 = smt.and %arg0, %arg1\n smt.yield %0 : "
- "!smt.bool\n} patterns {\n^bb0(%arg0: !smt.bool, %arg1: !smt.bool):\n "
- "smt.yield %arg0, %arg1 : !smt.bool, !smt.bool\n}\n");
-}
-
-TEST(QuantifierTest, ExistsBuilderNoPattern) {
- MLIRContext context;
- context.loadDialect<SMTDialect>();
- Location loc(UnknownLoc::get(&context));
-
- OpBuilder builder(&context);
- auto boolTy = BoolType::get(&context);
-
- ExistsOp existsOp = builder.create<ExistsOp>(
- loc, TypeRange{boolTy, boolTy},
- [](OpBuilder &builder, Location loc, ValueRange boundVars) {
- return builder.create<AndOp>(loc, boundVars);
- },
- ArrayRef<StringRef>{"a", "b"}, nullptr, /*weight=*/0, /*noPattern=*/true);
-
- SmallVector<char, 1024> buffer;
- llvm::raw_svector_ostream stream(buffer);
- existsOp.print(stream);
-
- ASSERT_STREQ(stream.str().str().c_str(),
- "%0 = smt.exists [\"a\", \"b\"] no_pattern {\n^bb0(%arg0: "
- "!smt.bool, %arg1: !smt.bool):\n %0 = smt.and %arg0, %arg1\n "
- "smt.yield %0 : !smt.bool\n}\n");
-}
-
-TEST(QuantifierTest, ExistsBuilderDefault) {
- MLIRContext context;
- context.loadDialect<SMTDialect>();
- Location loc(UnknownLoc::get(&context));
-
- OpBuilder builder(&context);
- auto boolTy = BoolType::get(&context);
-
- ExistsOp existsOp = builder.create<ExistsOp>(
- loc, TypeRange{boolTy, boolTy},
- [](OpBuilder &builder, Location loc, ValueRange boundVars) {
- return builder.create<AndOp>(loc, boundVars);
- },
- ArrayRef<StringRef>{"a", "b"});
-
- SmallVector<char, 1024> buffer;
- llvm::raw_svector_ostream stream(buffer);
- existsOp.print(stream);
-
- ASSERT_STREQ(stream.str().str().c_str(),
- "%0 = smt.exists [\"a\", \"b\"] {\n^bb0(%arg0: !smt.bool, "
- "%arg1: !smt.bool):\n %0 = smt.and %arg0, %arg1\n smt.yield "
- "%0 : !smt.bool\n}\n");
-}
-
-//===----------------------------------------------------------------------===//
-// Test custom builders of ForallOp
-//===----------------------------------------------------------------------===//
-
-TEST(QuantifierTest, ForallBuilderWithPattern) {
- MLIRContext context;
- context.loadDialect<SMTDialect>();
- Location loc(UnknownLoc::get(&context));
-
- OpBuilder builder(&context);
- auto boolTy = BoolType::get(&context);
-
- ForallOp forallOp = builder.create<ForallOp>(
- loc, TypeRange{boolTy, boolTy},
- [](OpBuilder &builder, Location loc, ValueRange boundVars) {
- return builder.create<AndOp>(loc, boundVars);
- },
- ArrayRef<StringRef>{"a", "b"},
- [](OpBuilder &builder, Location loc, ValueRange boundVars) {
- return boundVars;
- },
- /*weight=*/2);
-
- SmallVector<char, 1024> buffer;
- llvm::raw_svector_ostream stream(buffer);
- forallOp.print(stream);
-
- ASSERT_STREQ(
- stream.str().str().c_str(),
- "%0 = smt.forall [\"a\", \"b\"] weight 2 {\n^bb0(%arg0: !smt.bool, "
- "%arg1: !smt.bool):\n %0 = smt.and %arg0, %arg1\n smt.yield %0 : "
- "!smt.bool\n} patterns {\n^bb0(%arg0: !smt.bool, %arg1: !smt.bool):\n "
- "smt.yield %arg0, %arg1 : !smt.bool, !smt.bool\n}\n");
-}
-
-TEST(QuantifierTest, ForallBuilderNoPattern) {
- MLIRContext context;
- context.loadDialect<SMTDialect>();
- Location loc(UnknownLoc::get(&context));
-
- OpBuilder builder(&context);
- auto boolTy = BoolType::get(&context);
-
- ForallOp forallOp = builder.create<ForallOp>(
- loc, TypeRange{boolTy, boolTy},
- [](OpBuilder &builder, Location loc, ValueRange boundVars) {
- return builder.create<AndOp>(loc, boundVars);
- },
- ArrayRef<StringRef>{"a", "b"}, nullptr, /*weight=*/0, /*noPattern=*/true);
-
- SmallVector<char, 1024> buffer;
- llvm::raw_svector_ostream stream(buffer);
- forallOp.print(stream);
-
- ASSERT_STREQ(stream.str().str().c_str(),
- "%0 = smt.forall [\"a\", \"b\"] no_pattern {\n^bb0(%arg0: "
- "!smt.bool, %arg1: !smt.bool):\n %0 = smt.and %arg0, %arg1\n "
- "smt.yield %0 : !smt.bool\n}\n");
-}
-
-TEST(QuantifierTest, ForallBuilderDefault) {
- MLIRContext context;
- context.loadDialect<SMTDialect>();
- Location loc(UnknownLoc::get(&context));
-
- OpBuilder builder(&context);
- auto boolTy = BoolType::get(&context);
-
- ForallOp forallOp = builder.create<ForallOp>(
- loc, TypeRange{boolTy, boolTy},
- [](OpBuilder &builder, Location loc, ValueRange boundVars) {
- return builder.create<AndOp>(loc, boundVars);
- },
- std::nullopt);
-
- SmallVector<char, 1024> buffer;
- llvm::raw_svector_ostream stream(buffer);
- forallOp.print(stream);
-
- ASSERT_STREQ(stream.str().str().c_str(),
- "%0 = smt.forall {\n^bb0(%arg0: !smt.bool, "
- "%arg1: !smt.bool):\n %0 = smt.and %arg0, %arg1\n smt.yield "
- "%0 : !smt.bool\n}\n");
-}
-
-} // namespace
More information about the Mlir-commits
mailing list