Support for TextBlockLiterals

Author: wadoon

key.core/src/main/java/de/uka/ilkd/key/java/transformations/KeYJavaPipeline.java

@@ -20,7 +20,7 @@
  */
 public class KeYJavaPipeline {
     private final TransformationPipelineServices pipelineServices;
-    private final List<JavaTransformer> steps = new LinkedList<>();
+    private final List<SimpleJavaTransformer> steps = new LinkedList<>();
     private static final Logger LOGGER = LoggerFactory.getLogger(KeYJavaPipeline.class);
 
 
@@ -32,12 +32,13 @@ public TransformationPipelineServices getPipelineServices() {
         return pipelineServices;
     }
 
-    public List<JavaTransformer> getSteps() {
+    public List<SimpleJavaTransformer> getSteps() {
         return steps;
     }
 
     public static KeYJavaPipeline createDefault(TransformationPipelineServices pipelineServices) {
         KeYJavaPipeline p = new KeYJavaPipeline(pipelineServices);
+        p.add(new TextblockTransformer());
         p.add(new EnumClassBuilder(pipelineServices));
         p.add(new JMLTransformer(pipelineServices));
         p.add(new JmlDocRemoval(pipelineServices));
@@ -56,7 +57,7 @@ public static KeYJavaPipeline createDefault(TransformationPipelineServices pipel
         return p;
     }
 
-    public void add(JavaTransformer step) {
+    public void add(SimpleJavaTransformer step) {
         steps.add(step);
     }
 
@@ -70,7 +71,7 @@ public void apply(Collection<CompilationUnit> compilationUnits) {
                     .map(it -> it.getPath().toUri())
                     .orElse(null);
 
-            for (JavaTransformer step : steps) {
+            for (SimpleJavaTransformer step : steps) {
                 long start = System.currentTimeMillis();
                 step.apply(compilationUnit);
                 long stop = System.currentTimeMillis();

key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JavaTransformer.java

@@ -4,33 +4,23 @@
 package de.uka.ilkd.key.java.transformations.pipeline;
 
 
-
 import com.github.javaparser.ast.CompilationUnit;
 import com.github.javaparser.ast.Node;
 import com.github.javaparser.ast.body.TypeDeclaration;
 import org.jspecify.annotations.NullMarked;
 
 /**
- * The JavaDL requires some implicit fields, that are available in each
- * Java class. The name of the implicit fields starts usually with a dollar sign.
- * (in the age of recoder it was enclosed in angle brackets).
- * <p>
- * To access the fields in a uniform way, they are added as usual
- * fields to the classes, in particular this allows us to parse them in
- * easier.
- * For further information see also
- * <ul>
- * <li>{@link ImplicitFieldAdder}</li>
- * <li>{@link CreateObjectBuilder}</li>
- * <li>{@link PrepareObjectBuilder}</li>
- * </ul>
- * <p>
- * Performance of these classes was low, so information that is shared between
- * all instances of a transformation set has been outsourced to a transformation
- * cache.
+ * {@link SimpleJavaTransformer} with an internal state towards the current
+ * {@link TransformationPipelineServices}
+ * and {@link TransformationPipelineServices.TransformerCache}. These fields are set by the
+ * constructor, and given by
+ * the {@link de.uka.ilkd.key.java.transformations.KeYJavaPipeline}.
+ *
+ * @author weigl
+ * @see de.uka.ilkd.key.java.transformations.KeYJavaPipeline
  */
 @NullMarked
-public abstract class JavaTransformer {
+public abstract class JavaTransformer implements SimpleJavaTransformer {
     /**
      * Further services and helper function for this pipeline step.
      */
@@ -47,8 +37,7 @@ public abstract class JavaTransformer {
     /**
      * creates a transformer for the recoder model
      *
-     * @param services
-     *        the CrossReferenceServiceConfiguration to access
+     * @param services the CrossReferenceServiceConfiguration to access
      *        model information
      */
     public JavaTransformer(TransformationPipelineServices services) {
@@ -62,8 +51,11 @@ public JavaTransformer(TransformationPipelineServices services) {
      * descend in inner classes you have to implement the recursion by
      * yourself.
      */
-    public void apply(TypeDeclaration<?> td) {}
+    @Override
+    public void apply(TypeDeclaration<?> td) {
+    }
 
+    @Override
     public void apply(CompilationUnit cu) {
         for (TypeDeclaration<?> type : cu.getTypes()) {
             apply(type);

key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/SimpleJavaTransformer.java

@@ -0,0 +1,42 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.java.transformations.pipeline;
+
+
+import com.github.javaparser.ast.CompilationUnit;
+import com.github.javaparser.ast.Node;
+import com.github.javaparser.ast.body.TypeDeclaration;
+import org.jspecify.annotations.NullMarked;
+
+/**
+ * A transformation of Java ASTs in an early loading stage.
+ * <p>
+ * A {@link SimpleJavaTransformer} defines a transformation on mutable {@link Node}.
+ * As an entry an transformer receives the compilation unit. Traversal of it is left to the
+ * implementation of the transformer. The code should be transformed in-place. Creation of new
+ * {@link CompilationUnit}
+ * is not possible, but the creation of new {@link TypeDeclaration}
+ *
+ * Implementation should be stateless as instances are reused accross {@link CompilationUnit}s but
+ * not across
+ * loading requests.
+ *
+ * @author weigl
+ */
+@NullMarked
+public interface SimpleJavaTransformer {
+    default void apply(TypeDeclaration<?> td) {
+    }
+
+    default void apply(CompilationUnit cu) {
+        for (TypeDeclaration<?> type : cu.getTypes()) {
+            apply(type);
+            for (var m : type.getMembers()) {
+                if (m instanceof TypeDeclaration<?> ty) {
+                    apply(ty);
+                }
+            }
+        }
+    }
+}

key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/TextblockTransformer.java

@@ -0,0 +1,26 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.java.transformations.pipeline;
+
+import com.github.javaparser.ast.body.TypeDeclaration;
+import com.github.javaparser.ast.expr.StringLiteralExpr;
+import com.github.javaparser.ast.expr.TextBlockLiteralExpr;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (3/31/26)
+ */
+public class TextblockTransformer implements SimpleJavaTransformer {
+    @Override
+    public void apply(TypeDeclaration<?> td) {
+        for (var textblock : td.findAll(TextBlockLiteralExpr.class)) {
+            var s = textblock.getValue().stripIndent().translateEscapes()
+                    .replace("\\\n", "")
+                    .replace("\"", "\\\"");
+            var literal = new StringLiteralExpr(s);
+            textblock.replace(literal);
+        }
+    }
+}

key.core/src/test/java/KeyJavaPipelineTest.java

@@ -14,6 +14,7 @@
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.transformations.KeYJavaPipeline;
 import de.uka.ilkd.key.java.transformations.pipeline.JavaTransformer;
+import de.uka.ilkd.key.java.transformations.pipeline.SimpleJavaTransformer;
 import de.uka.ilkd.key.java.transformations.pipeline.TransformationPipelineServices;
 import de.uka.ilkd.key.nparser.NamespaceBuilder;
 import de.uka.ilkd.key.proof.init.JavaProfile;
@@ -78,7 +79,7 @@ public KeYJavaPipeline createPipelineTest(Path testFolder) throws IOException {
             var kjp = KeYJavaPipeline.createDefault(tservices);
             var kjp2 = new KeYJavaPipeline(tservices);
             var cnt = 0;
-            for (JavaTransformer step : kjp.getSteps()) {
+            for (SimpleJavaTransformer step : kjp.getSteps()) {
                 kjp2.add(step);
                 final var file = testFolder.resolve("actual").resolve(
                     String.format("%02d_%s", ++cnt, step.getClass().getSimpleName()));

key.core/src/test/java/de/uka/ilkd/key/java/transformations/pipeline/TextblockTransformerTest.java

@@ -0,0 +1,52 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.java.transformations.pipeline;
+
+import java.io.IOException;
+import java.io.InputStream;
+
+import org.key_project.util.java.IOUtil;
+
+import com.github.javaparser.JavaParser;
+import com.github.javaparser.ParseResult;
+import com.github.javaparser.ParserConfiguration;
+import com.github.javaparser.ast.CompilationUnit;
+import com.google.common.truth.Truth;
+import org.junit.jupiter.api.Test;
+
+import static org.junit.jupiter.api.Assertions.assertNotNull;
+import static org.junit.jupiter.api.Assertions.fail;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (3/31/26)
+ */
+class TextblockTransformerTest {
+    @Test
+    void transform() throws IOException {
+        final InputStream expected = getClass().getResourceAsStream("Textblock.expected.java");
+        final InputStream input = getClass().getResourceAsStream("Textblock.java");
+        assertNotNull(input);
+        assertNotNull(expected);
+
+        JavaParser parser = new JavaParser();
+        parser.getParserConfiguration().setLanguageLevel(ParserConfiguration.LanguageLevel.RAW);
+
+        ParseResult<CompilationUnit> result = parser.parse(input);
+        if (!result.isSuccessful()) {
+            result.getProblems().forEach(System.err::println);
+            fail("Parsing of fixture failed.");
+        }
+
+
+        CompilationUnit cu = result.getResult().get();
+
+        TextblockTransformer transformer = new TextblockTransformer();
+        transformer.apply(cu);
+
+        String expectedJava = IOUtil.readFrom(expected);
+        Truth.assertThat(cu.toString()).isEqualTo(expectedJava);
+    }
+}

key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/Textblock.expected.java

@@ -0,0 +1,28 @@
+public class Textblock {
+
+    // Expected One large string w/o newlines
+    String text = "Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua.";
+
+    // Expected: strip indentation and new lines. Four spaces before <body>.
+    String html = "<html>\n    <body>\n        <p>Hello, world</p>\n    </body>\n</html>\n";
+
+    // Expected: String with newlines and escaped quotes.
+    String query = "SELECT \"EMP_ID\", \"LAST_NAME\" FROM \"EMPLOYEE_TB\"\nWHERE \"CITY\" = 'INDIANAPOLIS'\nORDER BY \"EMP_ID\", \"LAST_NAME\";\n";
+
+    Object obj = ("function hello() {\n    print('\"Hello, world\"');\n}") + "hello();\n";
+
+    //expected "line 1\nlines 2\nline 3\n"
+    String simple = "line 1\nline 2\nline 3\n";
+
+    //Expected: newlines and escaped quotes
+    String code = "String text = \"\"\"\n    A text block inside a text block\n\"\"\";\n";
+
+    String abc = ("     1 \"\n     2 \"\"\n     3 \"\"\"\n     4 \"\"\"\"\n     5 \"\"\"\"\"\n     6 \"\"\"\"\"\"\n     7 \"\"\"\"\"\"\"\n     8 \"\"\"\"\"\"\"\"\n     9 \"\"\"\"\"\"\"\"\"\n    10 \"\"\"\"\"\"\"\"\"\"\n    11 \"\"\"\"\"\"\"\"\"\"\"\n    12 \"\"\"\"\"\"\"\"\"\"\"\"\n");
+
+    String text = "Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua.";
+
+    String colors = "red   \ngreen \nblue  \n";
+
+    // attention trailing whitespaces!
+    String colors = "red\ngreen\nblue\n";
+}

key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/Textblock.java

@@ -0,0 +1,83 @@
+public class Textblock {
+
+    // Expected One large string w/o newlines
+    String text = """
+            Lorem ipsum dolor sit amet, consectetur adipiscing \
+            elit, sed do eiusmod tempor incididunt ut labore \
+            et dolore magna aliqua.\
+            """;
+
+    // Expected: strip indentation and new lines. Four spaces before <body>.
+    String html = """
+            <html>
+                <body>
+                    <p>Hello, world</p>
+                </body>
+            </html>
+            """;
+
+    // Expected: String with newlines and escaped quotes.
+    String query = """
+            SELECT "EMP_ID", "LAST_NAME" FROM "EMPLOYEE_TB"
+            WHERE "CITY" = 'INDIANAPOLIS'
+            ORDER BY "EMP_ID", "LAST_NAME";
+            """;
+
+    Object obj = ("""
+            function hello() {
+                print('"Hello, world"');
+            }""")+
+            """
+            hello();
+            """;
+
+    //expected "line 1\nlines 2\nline 3\n"
+    String simple = """
+            line 1
+            line 2
+            line 3
+            """;
+
+    //Expected: newlines and escaped quotes
+    String code =
+            """
+                    String text = \"""
+                        A text block inside a text block
+                    \""";
+                    """;
+
+    String abc = ("""
+                 1 "
+                 2 ""
+                 3 ""\"
+                 4 ""\""
+                 5 ""\"""
+                 6 ""\"""\"
+                 7 ""\"""\""
+                 8 ""\"""\"""
+                 9 ""\"""\"""\"
+                10 ""\"""\"""\""
+                11 ""\"""\"""\"""
+                12 ""\"""\"""\"""\"
+            """);
+
+    String text = """
+            Lorem ipsum dolor sit amet, consectetur adipiscing \
+            elit, sed do eiusmod tempor incididunt ut labore \
+            et dolore magna aliqua.\
+            """;
+
+    String colors = """
+            red  \s
+            green\s
+            blue \s
+            """;
+
+    // attention trailing whitespaces!
+    String colors = """
+            red      
+            green     
+            blue      
+            """;
+
+}