Fix unbalanced block exception when pretty printing heap terms (#3726)

unp1 · web-flow · commit 75480229499c · 2026-01-28T05:13:56.000Z
diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java
@@ -169,7 +169,9 @@ public static String quickPrintTerm(JTerm t, Services services) {
     public static String quickPrintTerm(JTerm t, Services services, boolean usePrettyPrinting,
             boolean useUnicodeSymbols) {
         var p = quickPrinter(services, usePrettyPrinting, useUnicodeSymbols);
+        p.layouter().beginC();
         p.printTerm(t);
+        p.layouter().end();
         return p.result();
     }
 
@@ -780,6 +782,7 @@ public void printConstrainedFormula(SequentFormula cfma) {
      * @param t the Term to be printed
      */
     public void printTerm(JTerm t) {
+        layouter.beginC();
         if (notationInfo.getAbbrevMap().isEnabled(t)) {
             layouter.startTerm(0);
             layouter.print(notationInfo.getAbbrevMap().getAbbrev(t));
@@ -797,6 +800,7 @@ public void printTerm(JTerm t) {
         if (t.hasLabels()) {
             printLabels(t);
         }
+        layouter.end();
     }
 
     /**
@@ -989,7 +993,7 @@ protected boolean printEmbeddedHeapConstructorTerm(JTerm t) {
 
         Notation notation = notationInfo.getNotation(t.op());
         if (notation instanceof HeapConstructorNotation heapNotation) {
-            heapNotation.printEmbeddedHeap(t, this);
+            heapNotation.print(t, this);
             return true;
         } else {
             printTerm(t);
@@ -1001,7 +1005,7 @@ public void printClassName(String className) {
         layouter.print(className);
     }
 
-    public void printHeapConstructor(JTerm t, boolean closingBrace) {
+    public void printHeapConstructor(JTerm t) {
         assert t.boundVars().isEmpty();
 
         final HeapLDT heapLDT = getHeapLDT();
@@ -1045,10 +1049,9 @@ public void printHeapConstructor(JTerm t, boolean closingBrace) {
 
             layouter.print(")]").end();
 
-            if (closingBrace) {
+            if (!hasEmbedded) {
                 layouter.end();
             }
-
         } else {
             printFunctionTerm(t);
         }
@@ -1753,7 +1756,7 @@ public String result() {
     protected void maybeParens(JTerm t, int ass) {
         if (t.op() instanceof SchemaVariable && instantiations != null
                 && instantiations.getInstantiation((SchemaVariable) t.op()) instanceof JTerm) {
-            t = (JTerm) instantiations.getInstantiation((SchemaVariable) t.op());
+            t = instantiations.getInstantiation((SchemaVariable) t.op());
         }
 
         if (notationInfo.getNotation(t.op()).getPriority() < ass) {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/Notation.java b/key.core/src/main/java/de/uka/ilkd/key/pp/Notation.java
@@ -392,11 +392,7 @@ public HeapConstructorNotation() {
         }
 
         public void print(JTerm t, LogicPrinter sp) {
-            sp.printHeapConstructor(t, true);
-        }
-
-        public void printEmbeddedHeap(JTerm t, LogicPrinter sp) {
-            sp.printHeapConstructor(t, false);
+            sp.printHeapConstructor(t);
         }
     }
 
diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/StorePrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/StorePrinter.java
@@ -25,7 +25,7 @@ class StorePrinter extends FieldPrinter {
      * Common code for all pretty-printed store variants. This section is executed at the beginning
      * of pretty-printing.
      */
-    private void initPrettyPrint(LogicPrinter lp, final JTerm heapTerm) {
+    private boolean initPrettyPrint(LogicPrinter lp, final JTerm heapTerm) {
         lp.layouter.startTerm(4);
 
         lp.layouter.markStartSub();
@@ -39,6 +39,8 @@ private void initPrettyPrint(LogicPrinter lp, final JTerm heapTerm) {
         }
 
         lp.layouter.print("[");
+
+        return hasEmbedded;
     }
 
     /*
@@ -96,7 +98,7 @@ void printStore(LogicPrinter lp, JTerm t, boolean closingBrace) {
     private void printStoreOnArrayElement(LogicPrinter lp, final JTerm heapTerm,
             final JTerm objectTerm,
             final JTerm fieldTerm, final JTerm valueTerm, boolean closingBrace) {
-        initPrettyPrint(lp, heapTerm);
+        boolean embedded = initPrettyPrint(lp, heapTerm);
 
         PosTableLayouter layouter = lp.layouter();
         layouter.markStartSub();
@@ -114,7 +116,7 @@ private void printStoreOnArrayElement(LogicPrinter lp, final JTerm heapTerm,
 
         layouter.print("]");
 
-        finishPrettyPrint(lp, valueTerm, closingBrace);
+        finishPrettyPrint(lp, valueTerm, !embedded);
     }
 
     /*
@@ -123,7 +125,7 @@ private void printStoreOnArrayElement(LogicPrinter lp, final JTerm heapTerm,
     private void printStoreOnJavaFieldConstant(LogicPrinter lp, final JTerm heapTerm,
             final JTerm objectTerm,
             final JTerm fieldTerm, final JTerm valueTerm, boolean closingBrace) {
-        initPrettyPrint(lp, heapTerm);
+        boolean embedded = initPrettyPrint(lp, heapTerm);
 
         lp.layouter.markStartSub();
         lp.printTerm(objectTerm);
@@ -137,13 +139,13 @@ private void printStoreOnJavaFieldConstant(LogicPrinter lp, final JTerm heapTerm
         lp.printLabels(fieldTerm);
         lp.layouter.markEndSub();
 
-        finishPrettyPrint(lp, valueTerm, closingBrace);
+        finishPrettyPrint(lp, valueTerm, !embedded);
     }
 
     private void printStoreOnGenericFieldConstant(LogicPrinter lp, final JTerm heapTerm,
             final JTerm objectTerm,
             final JTerm fieldTerm, final JTerm valueTerm, boolean closingBrace) {
-        initPrettyPrint(lp, heapTerm);
+        boolean embedded = initPrettyPrint(lp, heapTerm);
 
         lp.layouter.markStartSub();
         lp.printTerm(objectTerm);
@@ -156,7 +158,7 @@ private void printStoreOnGenericFieldConstant(LogicPrinter lp, final JTerm heapT
         lp.layouter.print(HeapLDT.getPrettyFieldName(fieldTerm.op()));
         lp.layouter.markEndSub();
 
-        finishPrettyPrint(lp, valueTerm, closingBrace);
+        finishPrettyPrint(lp, valueTerm, !embedded);
     }
 
     /*
@@ -165,7 +167,7 @@ private void printStoreOnGenericFieldConstant(LogicPrinter lp, final JTerm heapT
     private void printStoreOnStaticField(LogicPrinter lp, final JTerm heapTerm,
             final JTerm fieldTerm,
             final JTerm valueTerm, boolean closingBrace) {
-        initPrettyPrint(lp, heapTerm);
+        boolean embedded = initPrettyPrint(lp, heapTerm);
 
         String className = HeapLDT.getClassName((Function) fieldTerm.op());
 
@@ -187,7 +189,7 @@ private void printStoreOnStaticField(LogicPrinter lp, final JTerm heapTerm,
         lp.layouter.print(HeapLDT.getPrettyFieldName(fieldTerm.op()));
         lp.layouter.markEndSub();
 
-        finishPrettyPrint(lp, valueTerm, closingBrace);
+        finishPrettyPrint(lp, valueTerm, !embedded);
     }
 
 }
diff --git a/key.core/src/test/java/de/uka/ilkd/key/pp/LogicPrinterTest.java b/key.core/src/test/java/de/uka/ilkd/key/pp/LogicPrinterTest.java
@@ -6,6 +6,7 @@
 import java.io.IOException;
 
 import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.logic.JTerm;
 import de.uka.ilkd.key.logic.NamespaceSet;
 import de.uka.ilkd.key.logic.op.JModality;
 import de.uka.ilkd.key.nparser.KeyIO;
@@ -52,4 +53,41 @@ void printModalityTerm() {
         lp.printTaclet(taclet, inst, true, false);
         assertTrue(true);
     }
+
+    @Test
+    void printAnonUpdateTerm1() {
+        Services services = TacletForTests.services().copy(false);
+        KeyIO io = new KeyIO(services, services.getNamespaces());
+        JTerm problem = null;
+        try {
+            problem = (JTerm) io
+                    .load(
+                        """
+                                 \\functions {
+                                    Heap h1;
+                                    Heap h2;
+                                    Heap h3;
+                                    Field fld;
+                                 }
+
+                                 \\programVariables { Object o; }
+
+                                 \\problem {
+                                      anon(store(h1, o, fld, null), union(union(allFields(o), singleton(o,fld)), allObjects(fld)), h2) = h3
+                                 }
+                                """)
+                    .loadCompleteProblem().getProblem().succedent().getFirst().formula();
+        } catch (IOException e) {
+            throw new RuntimeException(e);
+        }
+        try {
+            LogicPrinter.quickPrintTerm(problem, services);
+        } catch (Exception e) {
+            fail(e.getMessage());
+            return;
+        }
+        assertTrue(true);
+    }
+
+
 }

Original file line number	Diff line number	Diff line change
`@@ -392,11 +392,7 @@ public HeapConstructorNotation() {`
`392`	`392`	`}`
`393`	`393`
`394`	`394`	`public void print(JTerm t, LogicPrinter sp) {`
`395`		`- sp.printHeapConstructor(t, true);`
`396`		`- }`
`397`		`-`
`398`		`- public void printEmbeddedHeap(JTerm t, LogicPrinter sp) {`
`399`		`- sp.printHeapConstructor(t, false);`
	`395`	`+ sp.printHeapConstructor(t);`
`400`	`396`	`}`
`401`	`397`	`}`
`402`	`398`