From 6bda50e1d2b9238a1651971489e29c6cd6cc3f6c Mon Sep 17 00:00:00 2001
From: Roberto Rosmaninho <robertogomes@dcc.ufmg.br>
Date: Tue, 26 Sep 2023 13:27:28 -0300
Subject: [PATCH] Check if macros were expanded in `ensures` and `requires`
 (#3662)

Fixes #3585

This is a simple PR that extends the verification of expanded macros
from checking just the rule `body` also to check its `ensures` and
`requires`.
---
 .../regression-new/checks/expandMacroEnsures.k      | 13 +++++++++++++
 .../regression-new/checks/expandMacroEnsures.k.out  |  9 +++++++++
 .../regression-new/checks/expandMacroRequires.k     | 13 +++++++++++++
 .../regression-new/checks/expandMacroRequires.k.out |  9 +++++++++
 .../java/org/kframework/compile/ExpandMacros.java   | 10 +++++++---
 5 files changed, 51 insertions(+), 3 deletions(-)
 create mode 100644 k-distribution/tests/regression-new/checks/expandMacroEnsures.k
 create mode 100644 k-distribution/tests/regression-new/checks/expandMacroEnsures.k.out
 create mode 100644 k-distribution/tests/regression-new/checks/expandMacroRequires.k
 create mode 100644 k-distribution/tests/regression-new/checks/expandMacroRequires.k.out

diff --git a/k-distribution/tests/regression-new/checks/expandMacroEnsures.k b/k-distribution/tests/regression-new/checks/expandMacroEnsures.k
new file mode 100644
index 00000000000..80d10078ad0
--- /dev/null
+++ b/k-distribution/tests/regression-new/checks/expandMacroEnsures.k
@@ -0,0 +1,13 @@
+// Copyright (c) K Team. All Rights Reserved.
+
+module EXPANDMACROENSURES
+    imports INT
+    imports BOOL
+
+    syntax Int  ::= #foo ( Int ) [function]
+    syntax Bool ::= #baz ( Int ) [alias]
+
+//    rule #baz ( X ) => X // NOTE I should be defined !!
+
+    rule #foo( X ) => X       ensures  #baz( X )
+endmodule
diff --git a/k-distribution/tests/regression-new/checks/expandMacroEnsures.k.out b/k-distribution/tests/regression-new/checks/expandMacroEnsures.k.out
new file mode 100644
index 00000000000..d293d876591
--- /dev/null
+++ b/k-distribution/tests/regression-new/checks/expandMacroEnsures.k.out
@@ -0,0 +1,9 @@
+[Error] Compiler: Rule contains macro symbol that was not expanded
+	Source(expandMacroEnsures.k)
+	Location(12,10,12,49)
+	12 |	    rule #foo( X ) => X       ensures  #baz( X )
+	   .	         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+[Error] Compiler: Had 1 structural errors after macro expansion.
+  while executing phase "expand macros" on sentence at
+	Source(expandMacroEnsures.k)
+	Location(12,10,12,49)
diff --git a/k-distribution/tests/regression-new/checks/expandMacroRequires.k b/k-distribution/tests/regression-new/checks/expandMacroRequires.k
new file mode 100644
index 00000000000..53eca08228e
--- /dev/null
+++ b/k-distribution/tests/regression-new/checks/expandMacroRequires.k
@@ -0,0 +1,13 @@
+// Copyright (c) K Team. All Rights Reserved.
+
+module EXPANDMACROREQUIRES
+    imports INT
+    imports BOOL
+
+    syntax Int  ::= #foo ( Int ) [function]
+    syntax Bool ::= #bar ( Int ) [alias]
+
+//    rule #bar ( X ) => X >Int 0 // NOTE I should be defined !!
+
+    rule #foo( X ) => X       requires #bar( X )
+endmodule
diff --git a/k-distribution/tests/regression-new/checks/expandMacroRequires.k.out b/k-distribution/tests/regression-new/checks/expandMacroRequires.k.out
new file mode 100644
index 00000000000..597759a38f0
--- /dev/null
+++ b/k-distribution/tests/regression-new/checks/expandMacroRequires.k.out
@@ -0,0 +1,9 @@
+[Error] Compiler: Rule contains macro symbol that was not expanded
+	Source(expandMacroRequires.k)
+	Location(12,10,12,49)
+	12 |	    rule #foo( X ) => X       requires #bar( X )
+	   .	         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+[Error] Compiler: Had 1 structural errors after macro expansion.
+  while executing phase "expand macros" on sentence at
+	Source(expandMacroRequires.k)
+	Location(12,10,12,49)
diff --git a/kernel/src/main/java/org/kframework/compile/ExpandMacros.java b/kernel/src/main/java/org/kframework/compile/ExpandMacros.java
index 8d251fb3ec4..0e6978b69c2 100644
--- a/kernel/src/main/java/org/kframework/compile/ExpandMacros.java
+++ b/kernel/src/main/java/org/kframework/compile/ExpandMacros.java
@@ -188,16 +188,20 @@ private Sentence check(Sentence s) {
          * contain macros that have not been expanded.
          */
         if (s instanceof RuleOrClaim){
-            new VisitK() {
+            VisitK visitor = new VisitK() {
                 @Override
                 public void apply(KApply k) {
                     Option<Att> atts = mod.attributesFor().get(k.klabel());
                     if (atts.isDefined() && mod.attributesFor().apply(k.klabel()).getMacro().isDefined()) {
                         errors.add(KEMException.compilerError("Rule contains macro symbol that was not expanded", s));
                     }
-                    k.klist().items().stream().forEach(i -> super.apply(i));
+                    k.klist().items().forEach(super::apply);
                 }
-            }.accept(((RuleOrClaim) s).body());
+            };
+
+            visitor.accept(((RuleOrClaim) s).body());
+            visitor.accept(((RuleOrClaim) s).requires());
+            visitor.accept(((RuleOrClaim) s).ensures());
         }
 
         if (!errors.isEmpty()) {