diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/KeYJavaPipeline.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/KeYJavaPipeline.java index da9dff5027c..2f34115f416 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/KeYJavaPipeline.java +++ b/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 steps = new LinkedList<>(); + private final List steps = new LinkedList<>(); private static final Logger LOGGER = LoggerFactory.getLogger(KeYJavaPipeline.class); @@ -32,12 +32,13 @@ public TransformationPipelineServices getPipelineServices() { return pipelineServices; } - public List getSteps() { + public List 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 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(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JavaTransformer.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JavaTransformer.java index 0d3926d68fe..b1ea4e54bcf 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JavaTransformer.java +++ b/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). - *

- * 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 - *

    - *
  • {@link ImplicitFieldAdder}
    • - *
  • {@link CreateObjectBuilder}
    • - *
  • {@link PrepareObjectBuilder}
    • - *
- *

- * 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); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/SimpleJavaTransformer.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/SimpleJavaTransformer.java new file mode 100644 index 00000000000..3f3b2718acd --- /dev/null +++ b/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. + *

+ * 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); + } + } + } + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/TextblockTransformer.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/TextblockTransformer.java new file mode 100644 index 00000000000..1cf0807a5e0 --- /dev/null +++ b/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); + } + } +} diff --git a/key.core/src/test/java/KeyJavaPipelineTest.java b/key.core/src/test/java/KeyJavaPipelineTest.java index 3a65205eda1..375a2949ba6 100644 --- a/key.core/src/test/java/KeyJavaPipelineTest.java +++ b/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())); diff --git a/key.core/src/test/java/de/uka/ilkd/key/java/transformations/pipeline/TextblockTransformerTest.java b/key.core/src/test/java/de/uka/ilkd/key/java/transformations/pipeline/TextblockTransformerTest.java new file mode 100644 index 00000000000..32128fec93b --- /dev/null +++ b/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 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); + } +} diff --git a/key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/Textblock.expected.java b/key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/Textblock.expected.java new file mode 100644 index 00000000000..d1b1c3006af --- /dev/null +++ b/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 . + String html = "\n \n

Hello, world

\n \n\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"; +} diff --git a/key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/Textblock.java b/key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/Textblock.java new file mode 100644 index 00000000000..74eceab127a --- /dev/null +++ b/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 . + String html = """ + + +

Hello, world

+ + + """; + + // 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 + """; + +} \ No newline at end of file