[SMT] Added support for :pattern attribute #6976

luisacicolini · 2024-05-01T12:29:33Z

This PR addressess issue #6913 to enable the support of attributes in the SMTLIB export pass.

TaoBi22

A few minor points but looks pretty good to me!

integration_test/Target/ExportSMTLIB/attributes.mlir

lib/Target/ExportSMTLIB/ExportSMTLIB.cpp

test.smt

test_export.mlir

lib/Target/ExportSMTLIB/ExportSMTLIB.cpp

maerhart

Thanks a lot for working on this!

maerhart · 2024-05-01T13:33:22Z

lib/Target/ExportSMTLIB/ExportSMTLIB.cpp

+
+
+


Nit: unnecessarily big whitespace

maerhart · 2024-05-01T13:37:12Z

lib/Target/ExportSMTLIB/ExportSMTLIB.cpp

@@ -332,8 +339,11 @@ struct ExpressionVisitor
    worklist.push_back(yieldedValue);
    unsigned indentExt = operatorString.size() + 2;
    VisitorInfo newInfo(info.stream, info.valueMap,
-                        info.indentLevel + indentExt, 0);
-    newInfo.stream.indent(newInfo.indentLevel);
+                        info.indentLevel + indentExt, info.openParens);


Why would we want to pass on the number of open parens to the body region? Wouldn't it close the scopes of let expressions that might still be used at a later point?

Suggested change

info.indentLevel + indentExt, info.openParens);

info.indentLevel + indentExt, 0);

Right, I was having some problem wiht parentheses and I was testing what this changed, but forgot to put it back afterwards! thanks

lib/Target/ExportSMTLIB/ExportSMTLIB.cpp

maerhart · 2024-05-01T13:43:59Z

lib/Target/ExportSMTLIB/ExportSMTLIB.cpp

@@ -343,7 +353,42 @@ struct ExpressionVisitor
      info.stream << ")";

    if (weight != 0)
-      info.stream << " :weight " << weight << ")";
+      info.stream << " :weight " << weight;
+    if(!patterns.empty()){


Forgot to run git-clang-format?

yes 🤦‍♀️

maerhart · 2024-05-01T13:44:38Z

lib/Target/ExportSMTLIB/ExportSMTLIB.cpp

+        for (auto [i, arg] : llvm::enumerate(p.getArguments())) {
+          info.valueMap.insert(arg, argNames[i].str());
+        }


Nit: loops where the body is just one statement usually omit the curly braces

maerhart · 2024-05-01T13:49:47Z

test/Target/ExportSMTLIB/attributes.mlir

+  // CHECK:                           (let (([[V31:.+]] (=> [[V30:.+]] true)))
+  // CHECK:                           [[V31:.+]])) :weight 2
+  // CHECK                            :pattern ( ( let (([[V32:.+]] (= [[V28:.+]] [[V29:.+]])))
+  // CHECK:                   [[V32:.+]]))))))


test/Target/ExportSMTLIB/attributes.mlir

maerhart · 2024-05-01T13:55:12Z

lib/Target/ExportSMTLIB/ExportSMTLIB.cpp

-    newInfo.stream.indent(newInfo.indentLevel);
+                        info.indentLevel + indentExt, info.openParens);
+    if(weight !=0 || !patterns.empty())
+      newInfo.stream.indent(0);


Can you explain why we want 0 indentation here instead of info.indentLevel as well?

Why is the replaced newInfo.stream.indent(newInfo.indentLevel); not the right thing to do here (assuming we move the ( ! printing just after this line).

It is actually correct! I had misunderstood your previous comment, thanks

maerhart · 2024-05-01T13:57:37Z

lib/Target/ExportSMTLIB/ExportSMTLIB.cpp

+        Value yieldedValue = p.front().getTerminator()->getOperand(0);
+
+        worklist.push_back(yieldedValue);


The smt.yield operation can have more than one operand in pattern regions, but only one in the body region. So, there should probably another loop here iterating over all operands.

Quick questin about this, when (in the tests) I try to add multiple operands I get this error 2 operands present, but expected 1

That's interesting. Are you sure you have added it to the yield in the pattern region and not to the body? For me it worked in this regression test:

circt/test/Conversion/SMTToZ3LLVM/smt-to-z3-llvm.mlir

Lines 365 to 378 in 62fbb3a

%58 = smt.forall {

^bb0(%arg2: !smt.int, %arg3: !smt.int):

%59 = smt.eq %arg2, %arg3 : !smt.int

smt.yield %59 : !smt.bool

} patterns {

^bb0(%arg2: !smt.int, %arg3: !smt.int):

%59 = smt.int.add %arg2, %arg3

smt.yield %59 : !smt.int

}, {

^bb0(%arg2: !smt.int, %arg3: !smt.int):

%59 = smt.int.add %arg2, %arg3

%60 = smt.int.sub %arg2, %arg3

smt.yield %59, %60 : !smt.int, !smt.int

}

oh thanks for the reference! There was actually another syntax error I had not considered

maerhart · 2024-05-01T14:04:21Z

llvm

Accidental LLVM bump?

Co-authored-by: Bea Healy <57840981+TaoBi22@users.noreply.github.com>

This reverts commit 70f2a62.

TaoBi22 · 2024-05-05T20:02:15Z

Sorry @luisacicolini, looks like rebasing with the correct LLVM commit made GitHub think I was the author of the commits on the branch!

luisacicolini · 2024-05-05T20:59:01Z

No worries @TaoBi22 and thanks a lot for your help! Sorry for the delay in working on your commits @maerhart, had some issues with llvm and struggled a bit, luckily @TaoBi22 came to rescue. Getting everything done asap :)

maerhart · 2024-05-06T07:46:40Z

No worries, there's no need to stress. If you need help with something, let me know :)

luisacicolini · 2024-05-14T11:42:38Z

@maerhart all fixed now, this currently only supports single patterns, will open a new PR for the multi pattern :)
[EDIT: it actually required fewer changes than I thought, so everything is here now]

%t

lib/Target/ExportSMTLIB/ExportSMTLIB.cpp

luisacicolini · 2024-05-15T14:02:28Z

Adding multi patterns turned out to require just a few changes compared to this version, so now everything is pushed here :)

maerhart

Thanks! This looks really nice already, just one indentation issue and maybe improve the regression tests a little.

lib/Target/ExportSMTLIB/ExportSMTLIB.cpp

test/Target/ExportSMTLIB/attributes.mlir

maerhart · 2024-05-17T08:03:45Z

test/Target/ExportSMTLIB/attributes.mlir

+  // CHECK:                               :pattern ((let (([[V39:.+]] (= [[V34]] 3)))
+  // CHECK:                               [[V39]]) (let (([[V40:.+]] (= [[V35]] 4)))


It might be a good idea to add {{$}} at the end of a line to check that there aren't any extra closing parentheses since we had issues with that before.

lib/Target/ExportSMTLIB/ExportSMTLIB.cpp

maerhart · 2024-05-17T08:12:45Z

lib/Target/ExportSMTLIB/ExportSMTLIB.cpp

-    newInfo.stream.indent(newInfo.indentLevel);
+                        info.indentLevel + indentExt, info.openParens);
+    if(weight !=0 || !patterns.empty())
+      newInfo.stream.indent(0);


Why is the replaced newInfo.stream.indent(newInfo.indentLevel); not the right thing to do here (assuming we move the ( ! printing just after this line).

maerhart

Awesome, thanks!

luisacicolini requested a review from maerhart as a code owner May 1, 2024 12:29

TaoBi22 approved these changes May 1, 2024

View reviewed changes

maerhart reviewed May 1, 2024

View reviewed changes

luisacicolini and others added 10 commits May 5, 2024 20:18

first attempt

8d460ac

support for pattern attribbute:

35392fe

Update lib/Target/ExportSMTLIB/ExportSMTLIB.cpp

cc58393

Co-authored-by: Bea Healy <57840981+TaoBi22@users.noreply.github.com>

Update lib/Target/ExportSMTLIB/ExportSMTLIB.cpp

ec6bc79

Co-authored-by: Bea Healy <57840981+TaoBi22@users.noreply.github.com>

Update test.smt

cfcab8b

Co-authored-by: Bea Healy <57840981+TaoBi22@users.noreply.github.com>

addressed comments

05549d4

updated llvm

b676263

Revert "updated llvm"

8906bee

This reverts commit 70f2a62.

reverted commit

9f41543

Revert "updated llvm"

7ec49a4

This reverts commit 70f2a62.

TaoBi22 force-pushed the smtlib_add_pattern branch from 6da87b8 to 0824f09 Compare May 5, 2024 19:55

TaoBi22 added 2 commits May 5, 2024 20:55

Sync LLVM with upstream

0824f09

clang-format

333de80

Luisa Cicolini added 5 commits May 7, 2024 21:46

temporary needed to sewitch branch and commit

7120ba8

resolved nits

07188fa

clang formatted

768a117

switching branch

d4d95cf

fixed integration tests

6e7e530

TaoBi22 approved these changes May 14, 2024

View reviewed changes

%t Outdated Show resolved Hide resolved

lib/Target/ExportSMTLIB/ExportSMTLIB.cpp Outdated Show resolved Hide resolved

lib/Target/ExportSMTLIB/ExportSMTLIB.cpp Outdated Show resolved Hide resolved

Luisa Cicolini and others added 4 commits May 14, 2024 13:09

fixed nits

3e19cba

Delete %t

f6016ab

fixed filecheck

3ffbfaa

fixed filecheck tests

dc2b281

multi-patterns

6c072fc

maerhart reviewed May 17, 2024

View reviewed changes

fixed comments and added inlined tests

41970a0

maerhart approved these changes May 28, 2024

View reviewed changes

maerhart merged commit fa0e614 into llvm:main May 28, 2024
4 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[SMT] Added support for :pattern attribute #6976

[SMT] Added support for :pattern attribute #6976

luisacicolini commented May 1, 2024

TaoBi22 left a comment

maerhart left a comment

maerhart May 1, 2024

maerhart May 1, 2024

luisacicolini May 2, 2024

maerhart May 1, 2024

luisacicolini May 2, 2024

maerhart May 1, 2024

maerhart May 1, 2024

maerhart May 1, 2024

maerhart May 17, 2024

luisacicolini May 17, 2024

maerhart May 1, 2024

luisacicolini May 6, 2024

maerhart May 6, 2024

luisacicolini May 6, 2024

maerhart May 1, 2024

TaoBi22 commented May 5, 2024 •

edited

luisacicolini commented May 5, 2024

maerhart commented May 6, 2024

luisacicolini commented May 14, 2024 •

edited

luisacicolini commented May 15, 2024

maerhart left a comment

maerhart May 17, 2024

maerhart May 17, 2024

maerhart left a comment

	info.indentLevel + indentExt, info.openParens);
	info.indentLevel + indentExt, 0);

		Value yieldedValue = p.front().getTerminator()->getOperand(0);

		worklist.push_back(yieldedValue);

	%58 = smt.forall {
	^bb0(%arg2: !smt.int, %arg3: !smt.int):
	%59 = smt.eq %arg2, %arg3 : !smt.int
	smt.yield %59 : !smt.bool
	} patterns {
	^bb0(%arg2: !smt.int, %arg3: !smt.int):
	%59 = smt.int.add %arg2, %arg3
	smt.yield %59 : !smt.int
	}, {
	^bb0(%arg2: !smt.int, %arg3: !smt.int):
	%59 = smt.int.add %arg2, %arg3
	%60 = smt.int.sub %arg2, %arg3
	smt.yield %59, %60 : !smt.int, !smt.int
	}

		// CHECK: :pattern ((let (([[V39:.+]] (= [[V34]] 3)))
		// CHECK: [[V39]]) (let (([[V40:.+]] (= [[V35]] 4)))

[SMT] Added support for :pattern attribute #6976

[SMT] Added support for :pattern attribute #6976

Conversation

luisacicolini commented May 1, 2024

TaoBi22 left a comment

Choose a reason for hiding this comment

maerhart left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

TaoBi22 commented May 5, 2024 • edited

luisacicolini commented May 5, 2024

maerhart commented May 6, 2024

luisacicolini commented May 14, 2024 • edited

luisacicolini commented May 15, 2024

maerhart left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

maerhart left a comment

Choose a reason for hiding this comment

TaoBi22 commented May 5, 2024 •

edited

luisacicolini commented May 14, 2024 •

edited