From e68a37c61e32d75a0893f2c5bd46d2eafdbbacc1 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Fri, 10 May 2024 16:17:33 +0200
Subject: [PATCH] Fixing macro substitution for label statements

---
 .../scala/viper/silver/parser/MacroExpander.scala  | 13 +++++++++++++
 src/test/resources/all/issues/silver/0787a.vpr     | 14 ++++++++++++++
 src/test/resources/all/issues/silver/0787b.vpr     | 14 ++++++++++++++
 3 files changed, 41 insertions(+)
 create mode 100644 src/test/resources/all/issues/silver/0787a.vpr
 create mode 100644 src/test/resources/all/issues/silver/0787b.vpr

diff --git a/src/main/scala/viper/silver/parser/MacroExpander.scala b/src/main/scala/viper/silver/parser/MacroExpander.scala
index 082b1ba30..5cc216f37 100644
--- a/src/main/scala/viper/silver/parser/MacroExpander.scala
+++ b/src/main/scala/viper/silver/parser/MacroExpander.scala
@@ -481,6 +481,19 @@ object MacroExpander {
           freeVars += varUse.name
           (varUse, ctx)
         }
+      case (label@PLabel(lbl, lName, invs), ctx) if !ctx.c.boundVars.contains(lName.name) =>
+        if (ctx.c.paramToArgMap.contains(lName.name)) {
+          val replacement = ctx.c.paramToArgMap(lName.name).deepCopyAll
+          val replaced = replacement match {
+            case r: PIdnUseExp => PIdnDef(r.name)(r.pos)
+            case r =>
+              throw MacroException(s"macro expansion cannot substitute expression `${replacement.pretty}` at ${replacement.pos._1} in non-expression position at ${lName.pos._1}.", replacement.pos)
+          }
+          (PLabel(lbl, replaced, invs)(label.pos), ctx.updateContext(ctx.c.copy(paramToArgMap = ctx.c.paramToArgMap.empty)))
+        } else {
+          freeVars += lName.name
+          (label, ctx)
+        }
     }, ReplaceContext())
     (replacer, freeVars)
   }
diff --git a/src/test/resources/all/issues/silver/0787a.vpr b/src/test/resources/all/issues/silver/0787a.vpr
new file mode 100644
index 000000000..9602de622
--- /dev/null
+++ b/src/test/resources/all/issues/silver/0787a.vpr
@@ -0,0 +1,14 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+method main()
+{
+    m(some_name)
+}
+
+define m(label_name)
+{
+    goto label_name
+    label label_name
+}
\ No newline at end of file
diff --git a/src/test/resources/all/issues/silver/0787b.vpr b/src/test/resources/all/issues/silver/0787b.vpr
new file mode 100644
index 000000000..1dafbea9e
--- /dev/null
+++ b/src/test/resources/all/issues/silver/0787b.vpr
@@ -0,0 +1,14 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+method main()
+{
+    //:: ExpectedOutput(parser.error)
+    m(3)
+}
+
+define m(label_name)
+{
+    label label_name
+}
\ No newline at end of file