From 7f9bbbfdd5260ee73e811cd3a32fffddd17bc809 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Tue, 31 Mar 2026 22:29:29 +0200 Subject: [PATCH] Support for TextBlockLiterals - added example and test case - update KeyJavaPipelineTest.java --- .../MostSimpleInner.java | 0 .../MostSimpleInner.java | 0 .../MostSimpleInner.java | 0 .../04_JmlDocRemoval/MostSimpleInner.java | 5 + .../MostSimpleInner.java | 0 .../MostSimpleInner.java | 0 .../MostSimpleInner.java | 0 .../MostSimpleInner.java | 0 .../MostSimpleInner.java | 0 .../MostSimpleInner.java | 0 .../MostSimpleInner.java | 0 .../MostSimpleInner.java | 0 .../MostSimpleInner.java | 0 .../MostSimpleInner.java | 189 ++++++++++++++ .../Test.java | 0 .../Test.java | 0 .../Test.java | 0 .../expected/04_JmlDocRemoval/Test.java | 24 ++ .../Test.java | 0 .../Test.java | 0 .../Test.java | 0 .../Test.java | 0 .../Test.java | 0 .../Test.java | 0 .../Test.java | 0 .../Test.java | 0 .../Test.java | 0 .../Test.java | 240 ++++++++++++++++++ .../java/transformations/KeYJavaPipeline.java | 1 + .../ClassInitializeMethodBuilder.java | 2 +- .../ClassPreparationMethodBuilder.java | 2 +- .../ConstantStringExpressionEvaluator.java | 2 +- .../ConstructorNormalformBuilder.java | 2 +- .../pipeline/CreateBuilder.java | 2 +- .../pipeline/CreateObjectBuilder.java | 2 +- .../pipeline/EnumClassBuilder.java | 2 +- .../pipeline/ImplicitFieldAdder.java | 2 +- .../InstanceAllocationMethodBuilder.java | 2 +- .../pipeline/JMLCommentTransformer.java | 2 +- .../pipeline/JMLTransformer.java | 4 +- .../pipeline/JavaTransformer.java | 76 ++---- .../pipeline/JavaTransformerAbstract.java | 79 ++++++ .../pipeline/JmlDocRemoval.java | 2 +- .../pipeline/LocalClassTransformation.java | 2 +- .../pipeline/PrepareObjectBuilder.java | 2 +- .../pipeline/TextblockTransformer.java | 26 ++ .../src/test/java/KeyJavaPipelineTest.java | 16 +- .../pipeline/TextblockTransformerTest.java | 52 ++++ .../proof/runallproofs/ProofCollections.java | 3 + .../pipeline/Textblock.expected.java | 28 ++ .../transformations/pipeline/Textblock.java | 83 ++++++ .../Java/TextBlockLiterals/README.txt | 8 + .../TextBlockLiterals/TextBlockLiterals.java | 14 + .../Java/TextBlockLiterals/project.key | 8 + key.ui/examples/index/samplesIndex.txt | 4 + 55 files changed, 807 insertions(+), 79 deletions(-) rename key.core/pipelineTests/innerclass/expected/{01_EnumClassBuilder => 01_TextblockTransformer}/MostSimpleInner.java (100%) rename key.core/pipelineTests/innerclass/expected/{02_JMLTransformer => 02_EnumClassBuilder}/MostSimpleInner.java (100%) rename key.core/pipelineTests/innerclass/expected/{03_JmlDocRemoval => 03_JMLTransformer}/MostSimpleInner.java (100%) create mode 100644 key.core/pipelineTests/innerclass/expected/04_JmlDocRemoval/MostSimpleInner.java rename key.core/pipelineTests/innerclass/expected/{04_ImplicitFieldAdder => 05_ImplicitFieldAdder}/MostSimpleInner.java (100%) rename key.core/pipelineTests/innerclass/expected/{05_InstanceAllocationMethodBuilder => 06_InstanceAllocationMethodBuilder}/MostSimpleInner.java (100%) rename key.core/pipelineTests/innerclass/expected/{06_ConstructorNormalformBuilder => 07_ConstructorNormalformBuilder}/MostSimpleInner.java (100%) rename key.core/pipelineTests/innerclass/expected/{07_ClassPreparationMethodBuilder => 08_ClassPreparationMethodBuilder}/MostSimpleInner.java (100%) rename key.core/pipelineTests/innerclass/expected/{08_ClassInitializeMethodBuilder => 09_ClassInitializeMethodBuilder}/MostSimpleInner.java (100%) rename key.core/pipelineTests/innerclass/expected/{09_PrepareObjectBuilder => 10_PrepareObjectBuilder}/MostSimpleInner.java (100%) rename key.core/pipelineTests/innerclass/expected/{10_CreateBuilder => 11_CreateBuilder}/MostSimpleInner.java (100%) rename key.core/pipelineTests/innerclass/expected/{11_CreateObjectBuilder => 12_CreateObjectBuilder}/MostSimpleInner.java (100%) rename key.core/pipelineTests/innerclass/expected/{12_LocalClassTransformation => 13_LocalClassTransformation}/MostSimpleInner.java (100%) create mode 100644 key.core/pipelineTests/innerclass/expected/14_ConstantStringExpressionEvaluator/MostSimpleInner.java rename key.core/pipelineTests/simple/expected/{01_EnumClassBuilder => 01_TextblockTransformer}/Test.java (100%) rename key.core/pipelineTests/simple/expected/{02_JMLTransformer => 02_EnumClassBuilder}/Test.java (100%) rename key.core/pipelineTests/simple/expected/{03_JmlDocRemoval => 03_JMLTransformer}/Test.java (100%) create mode 100644 key.core/pipelineTests/simple/expected/04_JmlDocRemoval/Test.java rename key.core/pipelineTests/simple/expected/{04_ImplicitFieldAdder => 05_ImplicitFieldAdder}/Test.java (100%) rename key.core/pipelineTests/simple/expected/{05_InstanceAllocationMethodBuilder => 06_InstanceAllocationMethodBuilder}/Test.java (100%) rename key.core/pipelineTests/simple/expected/{06_ConstructorNormalformBuilder => 07_ConstructorNormalformBuilder}/Test.java (100%) rename key.core/pipelineTests/simple/expected/{07_ClassPreparationMethodBuilder => 08_ClassPreparationMethodBuilder}/Test.java (100%) rename key.core/pipelineTests/simple/expected/{08_ClassInitializeMethodBuilder => 09_ClassInitializeMethodBuilder}/Test.java (100%) rename key.core/pipelineTests/simple/expected/{09_PrepareObjectBuilder => 10_PrepareObjectBuilder}/Test.java (100%) rename key.core/pipelineTests/simple/expected/{10_CreateBuilder => 11_CreateBuilder}/Test.java (100%) rename key.core/pipelineTests/simple/expected/{11_CreateObjectBuilder => 12_CreateObjectBuilder}/Test.java (100%) rename key.core/pipelineTests/simple/expected/{12_LocalClassTransformation => 13_LocalClassTransformation}/Test.java (100%) create mode 100644 key.core/pipelineTests/simple/expected/14_ConstantStringExpressionEvaluator/Test.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JavaTransformerAbstract.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/TextblockTransformer.java create mode 100644 key.core/src/test/java/de/uka/ilkd/key/java/transformations/pipeline/TextblockTransformerTest.java create mode 100644 key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/Textblock.expected.java create mode 100644 key.core/src/test/resources/de/uka/ilkd/key/java/transformations/pipeline/Textblock.java create mode 100644 key.ui/examples/Java/TextBlockLiterals/README.txt create mode 100644 key.ui/examples/Java/TextBlockLiterals/TextBlockLiterals.java create mode 100644 key.ui/examples/Java/TextBlockLiterals/project.key diff --git a/key.core/pipelineTests/innerclass/expected/01_EnumClassBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/01_TextblockTransformer/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/01_EnumClassBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/01_TextblockTransformer/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/02_JMLTransformer/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/02_EnumClassBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/02_JMLTransformer/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/02_EnumClassBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/03_JmlDocRemoval/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/03_JMLTransformer/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/03_JmlDocRemoval/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/03_JMLTransformer/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/04_JmlDocRemoval/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/04_JmlDocRemoval/MostSimpleInner.java new file mode 100644 index 00000000000..a7764c2a007 --- /dev/null +++ b/key.core/pipelineTests/innerclass/expected/04_JmlDocRemoval/MostSimpleInner.java @@ -0,0 +1,5 @@ +public class MostSimpleInner { + + public static class MyInnerClass { + } +} diff --git a/key.core/pipelineTests/innerclass/expected/04_ImplicitFieldAdder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/05_ImplicitFieldAdder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/04_ImplicitFieldAdder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/05_ImplicitFieldAdder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/05_InstanceAllocationMethodBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/06_InstanceAllocationMethodBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/05_InstanceAllocationMethodBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/06_InstanceAllocationMethodBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/06_ConstructorNormalformBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/07_ConstructorNormalformBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/06_ConstructorNormalformBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/07_ConstructorNormalformBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/07_ClassPreparationMethodBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/08_ClassPreparationMethodBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/07_ClassPreparationMethodBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/08_ClassPreparationMethodBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/08_ClassInitializeMethodBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/09_ClassInitializeMethodBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/08_ClassInitializeMethodBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/09_ClassInitializeMethodBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/09_PrepareObjectBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/10_PrepareObjectBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/09_PrepareObjectBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/10_PrepareObjectBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/10_CreateBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/11_CreateBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/10_CreateBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/11_CreateBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/11_CreateObjectBuilder/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/12_CreateObjectBuilder/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/11_CreateObjectBuilder/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/12_CreateObjectBuilder/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/12_LocalClassTransformation/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/13_LocalClassTransformation/MostSimpleInner.java similarity index 100% rename from key.core/pipelineTests/innerclass/expected/12_LocalClassTransformation/MostSimpleInner.java rename to key.core/pipelineTests/innerclass/expected/13_LocalClassTransformation/MostSimpleInner.java diff --git a/key.core/pipelineTests/innerclass/expected/14_ConstantStringExpressionEvaluator/MostSimpleInner.java b/key.core/pipelineTests/innerclass/expected/14_ConstantStringExpressionEvaluator/MostSimpleInner.java new file mode 100644 index 00000000000..decd2bad906 --- /dev/null +++ b/key.core/pipelineTests/innerclass/expected/14_ConstantStringExpressionEvaluator/MostSimpleInner.java @@ -0,0 +1,189 @@ +public class MostSimpleInner { + + public static class MyInnerClass { + + @javax.annotation.processing.Generated() + static private boolean $classInitializationInProgress; + + @javax.annotation.processing.Generated() + static private boolean $classErroneous; + + @javax.annotation.processing.Generated() + static private boolean $classInitialized; + + @javax.annotation.processing.Generated() + static private boolean $classPrepared; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv_free; + + public static MyInnerClass $allocate(); + + public MyInnerClass() { + } + + public void $init() { + super.$init(); + super.$init(); + } + + static private void $clprepare() { + } + + static public void $clinit() { + if (!@($classInitialized)) { + if (!@($classInitializationInProgress)) { + if (!@($classPrepared)) { + //Created by ClassInitializeMethodBuilder.java:219 + @($clprepare()); + } + if (@($classErroneous)) { + throw new java.lang.NoClassDefFoundError(); + } + //Created by ClassInitializeMethodBuilder.java:243 + @($classInitializationInProgress) = true; + try { + @(java.lang.Object.$clinit()); + }//Created by ClassInitializeMethodBuilder.java:194 + catch (java.lang.Error err) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw err; + } catch (java.lang.Throwable twa) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw new java.lang.ExceptionInInitializerError(twa); + } + //Created by ClassInitializeMethodBuilder.java:249 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:251 + @($classErroneous) = false; + //Created by ClassInitializeMethodBuilder.java:253 + @($classInitialized) = true; + } + } + } + + protected void $prepare() { + super.$prepare(); + } + + private void $prepareEnter() { + super.$prepare(); + } + + public MyInnerClass $create() { + //Created by CreateBuilder.java:57 + this.$initialized = false; + $prepareEnter(); + return this; + } + + public static MyInnerClass $createObject() { + MyInnerClass __NEW__; + //Created by CreateObjectBuilder.java:70 + __NEW__ = MyInnerClass.$allocate(); + __NEW__.$create()@MyInnerClass + return __NEW__; + } + } + + @javax.annotation.processing.Generated() + static private boolean $classInitializationInProgress; + + @javax.annotation.processing.Generated() + static private boolean $classErroneous; + + @javax.annotation.processing.Generated() + static private boolean $classInitialized; + + @javax.annotation.processing.Generated() + static private boolean $classPrepared; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv_free; + + public static MostSimpleInner $allocate(); + + public MostSimpleInner() { + } + + public void $init() { + super.$init(); + super.$init(); + } + + static private void $clprepare() { + } + + static public void $clinit() { + if (!@($classInitialized)) { + if (!@($classInitializationInProgress)) { + if (!@($classPrepared)) { + //Created by ClassInitializeMethodBuilder.java:219 + @($clprepare()); + } + if (@($classErroneous)) { + throw new java.lang.NoClassDefFoundError(); + } + //Created by ClassInitializeMethodBuilder.java:243 + @($classInitializationInProgress) = true; + try { + @(java.lang.Object.$clinit()); + }//Created by ClassInitializeMethodBuilder.java:194 + catch (java.lang.Error err) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw err; + } catch (java.lang.Throwable twa) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw new java.lang.ExceptionInInitializerError(twa); + } + //Created by ClassInitializeMethodBuilder.java:249 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:251 + @($classErroneous) = false; + //Created by ClassInitializeMethodBuilder.java:253 + @($classInitialized) = true; + } + } + } + + protected void $prepare() { + super.$prepare(); + } + + private void $prepareEnter() { + super.$prepare(); + } + + public MostSimpleInner $create() { + //Created by CreateBuilder.java:57 + this.$initialized = false; + $prepareEnter(); + return this; + } + + public static MostSimpleInner $createObject() { + MostSimpleInner __NEW__; + //Created by CreateObjectBuilder.java:70 + __NEW__ = MostSimpleInner.$allocate(); + __NEW__.$create()@MostSimpleInner + return __NEW__; + } +} diff --git a/key.core/pipelineTests/simple/expected/01_EnumClassBuilder/Test.java b/key.core/pipelineTests/simple/expected/01_TextblockTransformer/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/01_EnumClassBuilder/Test.java rename to key.core/pipelineTests/simple/expected/01_TextblockTransformer/Test.java diff --git a/key.core/pipelineTests/simple/expected/02_JMLTransformer/Test.java b/key.core/pipelineTests/simple/expected/02_EnumClassBuilder/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/02_JMLTransformer/Test.java rename to key.core/pipelineTests/simple/expected/02_EnumClassBuilder/Test.java diff --git a/key.core/pipelineTests/simple/expected/03_JmlDocRemoval/Test.java b/key.core/pipelineTests/simple/expected/03_JMLTransformer/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/03_JmlDocRemoval/Test.java rename to key.core/pipelineTests/simple/expected/03_JMLTransformer/Test.java diff --git a/key.core/pipelineTests/simple/expected/04_JmlDocRemoval/Test.java b/key.core/pipelineTests/simple/expected/04_JmlDocRemoval/Test.java new file mode 100644 index 00000000000..dba29c488a0 --- /dev/null +++ b/key.core/pipelineTests/simple/expected/04_JmlDocRemoval/Test.java @@ -0,0 +1,24 @@ +public class Test { + + public static int abc; + + static { + // should be resolved to 2 + abc = 1 + 1; + } + + public int memberVar; + + { + memberVar = 42; + } +} + +public class SubClass extends Test { + + public int memberVar; + + { + memberVar = 41; + } +} diff --git a/key.core/pipelineTests/simple/expected/04_ImplicitFieldAdder/Test.java b/key.core/pipelineTests/simple/expected/05_ImplicitFieldAdder/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/04_ImplicitFieldAdder/Test.java rename to key.core/pipelineTests/simple/expected/05_ImplicitFieldAdder/Test.java diff --git a/key.core/pipelineTests/simple/expected/05_InstanceAllocationMethodBuilder/Test.java b/key.core/pipelineTests/simple/expected/06_InstanceAllocationMethodBuilder/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/05_InstanceAllocationMethodBuilder/Test.java rename to key.core/pipelineTests/simple/expected/06_InstanceAllocationMethodBuilder/Test.java diff --git a/key.core/pipelineTests/simple/expected/06_ConstructorNormalformBuilder/Test.java b/key.core/pipelineTests/simple/expected/07_ConstructorNormalformBuilder/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/06_ConstructorNormalformBuilder/Test.java rename to key.core/pipelineTests/simple/expected/07_ConstructorNormalformBuilder/Test.java diff --git a/key.core/pipelineTests/simple/expected/07_ClassPreparationMethodBuilder/Test.java b/key.core/pipelineTests/simple/expected/08_ClassPreparationMethodBuilder/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/07_ClassPreparationMethodBuilder/Test.java rename to key.core/pipelineTests/simple/expected/08_ClassPreparationMethodBuilder/Test.java diff --git a/key.core/pipelineTests/simple/expected/08_ClassInitializeMethodBuilder/Test.java b/key.core/pipelineTests/simple/expected/09_ClassInitializeMethodBuilder/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/08_ClassInitializeMethodBuilder/Test.java rename to key.core/pipelineTests/simple/expected/09_ClassInitializeMethodBuilder/Test.java diff --git a/key.core/pipelineTests/simple/expected/09_PrepareObjectBuilder/Test.java b/key.core/pipelineTests/simple/expected/10_PrepareObjectBuilder/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/09_PrepareObjectBuilder/Test.java rename to key.core/pipelineTests/simple/expected/10_PrepareObjectBuilder/Test.java diff --git a/key.core/pipelineTests/simple/expected/10_CreateBuilder/Test.java b/key.core/pipelineTests/simple/expected/11_CreateBuilder/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/10_CreateBuilder/Test.java rename to key.core/pipelineTests/simple/expected/11_CreateBuilder/Test.java diff --git a/key.core/pipelineTests/simple/expected/11_CreateObjectBuilder/Test.java b/key.core/pipelineTests/simple/expected/12_CreateObjectBuilder/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/11_CreateObjectBuilder/Test.java rename to key.core/pipelineTests/simple/expected/12_CreateObjectBuilder/Test.java diff --git a/key.core/pipelineTests/simple/expected/12_LocalClassTransformation/Test.java b/key.core/pipelineTests/simple/expected/13_LocalClassTransformation/Test.java similarity index 100% rename from key.core/pipelineTests/simple/expected/12_LocalClassTransformation/Test.java rename to key.core/pipelineTests/simple/expected/13_LocalClassTransformation/Test.java diff --git a/key.core/pipelineTests/simple/expected/14_ConstantStringExpressionEvaluator/Test.java b/key.core/pipelineTests/simple/expected/14_ConstantStringExpressionEvaluator/Test.java new file mode 100644 index 00000000000..44f496647fc --- /dev/null +++ b/key.core/pipelineTests/simple/expected/14_ConstantStringExpressionEvaluator/Test.java @@ -0,0 +1,240 @@ +public class Test { + + public static int abc; + + static { + // should be resolved to 2 + abc = 1 + 1; + } + + public int memberVar; + + { + memberVar = 42; + } + + @javax.annotation.processing.Generated() + static private boolean $classInitializationInProgress; + + @javax.annotation.processing.Generated() + static private boolean $classErroneous; + + @javax.annotation.processing.Generated() + static private boolean $classInitialized; + + @javax.annotation.processing.Generated() + static private boolean $classPrepared; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv_free; + + public static Test $allocate(); + + public Test() { + } + + private void $objectInitializer0() { + memberVar = 42; + } + + public void $init() { + super.$init(); + $objectInitializer0(); + super.$init(); + $objectInitializer0(); + } + + private void $objectInitializer0() { + memberVar = 42; + } + + static private void $clprepare() { + } + + static public void $clinit() { + if (!@($classInitialized)) { + if (!@($classInitializationInProgress)) { + if (!@($classPrepared)) { + //Created by ClassInitializeMethodBuilder.java:219 + @($clprepare()); + } + if (@($classErroneous)) { + throw new java.lang.NoClassDefFoundError(); + } + //Created by ClassInitializeMethodBuilder.java:243 + @($classInitializationInProgress) = true; + try { + @(java.lang.Object.$clinit()); + { + // should be resolved to 2 + abc = 1 + 1; + } + }//Created by ClassInitializeMethodBuilder.java:194 + catch (java.lang.Error err) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw err; + } catch (java.lang.Throwable twa) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw new java.lang.ExceptionInInitializerError(twa); + } + //Created by ClassInitializeMethodBuilder.java:249 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:251 + @($classErroneous) = false; + //Created by ClassInitializeMethodBuilder.java:253 + @($classInitialized) = true; + } + } + } + + protected void $prepare() { + super.$prepare(); + //Created by PrepareObjectBuilder.java:94 + this.memberVar = 0; + } + + private void $prepareEnter() { + super.$prepare(); + //Created by PrepareObjectBuilder.java:94 + this.memberVar = 0; + } + + public Test $create() { + //Created by CreateBuilder.java:57 + this.$initialized = false; + $prepareEnter(); + return this; + } + + public static Test $createObject() { + Test __NEW__; + //Created by CreateObjectBuilder.java:70 + __NEW__ = Test.$allocate(); + __NEW__.$create()@Test + return __NEW__; + } +} + +public class SubClass extends Test { + + public int memberVar; + + { + memberVar = 41; + } + + @javax.annotation.processing.Generated() + static private boolean $classInitializationInProgress; + + @javax.annotation.processing.Generated() + static private boolean $classErroneous; + + @javax.annotation.processing.Generated() + static private boolean $classInitialized; + + @javax.annotation.processing.Generated() + static private boolean $classPrepared; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv; + + @javax.annotation.processing.Generated() + static public model boolean $staticInv_free; + + public static SubClass $allocate(); + + public SubClass() { + } + + private void $objectInitializer0() { + memberVar = 41; + } + + public void $init() { + super.$init(); + $objectInitializer0(); + super.$init(); + $objectInitializer0(); + } + + private void $objectInitializer0() { + memberVar = 41; + } + + static private void $clprepare() { + } + + static public void $clinit() { + if (!@($classInitialized)) { + if (!@($classInitializationInProgress)) { + if (!@($classPrepared)) { + //Created by ClassInitializeMethodBuilder.java:219 + @($clprepare()); + } + if (@($classErroneous)) { + throw new java.lang.NoClassDefFoundError(); + } + //Created by ClassInitializeMethodBuilder.java:243 + @($classInitializationInProgress) = true; + try { + @(Test.$clinit()); + }//Created by ClassInitializeMethodBuilder.java:194 + catch (java.lang.Error err) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw err; + } catch (java.lang.Throwable twa) { + //Created by ClassInitializeMethodBuilder.java:154 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:155 + @($classErroneous) = true; + throw new java.lang.ExceptionInInitializerError(twa); + } + //Created by ClassInitializeMethodBuilder.java:249 + @($classInitializationInProgress) = false; + //Created by ClassInitializeMethodBuilder.java:251 + @($classErroneous) = false; + //Created by ClassInitializeMethodBuilder.java:253 + @($classInitialized) = true; + } + } + } + + protected void $prepare() { + super.$prepare(); + //Created by PrepareObjectBuilder.java:94 + this.memberVar = 0; + } + + private void $prepareEnter() { + super.$prepare(); + //Created by PrepareObjectBuilder.java:94 + this.memberVar = 0; + } + + public SubClass $create() { + //Created by CreateBuilder.java:57 + this.$initialized = false; + $prepareEnter(); + return this; + } + + public static SubClass $createObject() { + SubClass __NEW__; + //Created by CreateObjectBuilder.java:70 + __NEW__ = SubClass.$allocate(); + __NEW__.$create()@SubClass + return __NEW__; + } +} 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..fb58865513f 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 @@ -38,6 +38,7 @@ public List getSteps() { 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)); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ClassInitializeMethodBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ClassInitializeMethodBuilder.java index b4a84bbbd88..b95e50aa311 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ClassInitializeMethodBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ClassInitializeMethodBuilder.java @@ -41,7 +41,7 @@ * <clprepare> responsible for the class * preparation. */ -public class ClassInitializeMethodBuilder extends JavaTransformer { +public class ClassInitializeMethodBuilder extends JavaTransformerAbstract { public static final String CLASS_INITIALIZE_IDENTIFIER = "$clinit"; /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ClassPreparationMethodBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ClassPreparationMethodBuilder.java index 8c7c3fdf1f2..c6b7bd3e40b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ClassPreparationMethodBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ClassPreparationMethodBuilder.java @@ -42,7 +42,7 @@ * <clprepare> responsible for the class * preparation. */ -public class ClassPreparationMethodBuilder extends JavaTransformer { +public class ClassPreparationMethodBuilder extends JavaTransformerAbstract { private static final Logger LOGGER = LoggerFactory.getLogger(ClassPreparationMethodBuilder.class); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ConstantStringExpressionEvaluator.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ConstantStringExpressionEvaluator.java index e81be4b6201..7061b68e91c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ConstantStringExpressionEvaluator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ConstantStringExpressionEvaluator.java @@ -40,7 +40,7 @@ import com.github.javaparser.ast.type.*; import com.github.javaparser.ast.visitor.VoidVisitorAdapter; -public class ConstantStringExpressionEvaluator extends JavaTransformer { +public class ConstantStringExpressionEvaluator extends JavaTransformerAbstract { public ConstantStringExpressionEvaluator(TransformationPipelineServices services) { super(services); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ConstructorNormalformBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ConstructorNormalformBuilder.java index e146499007e..d4aab99e260 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ConstructorNormalformBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ConstructorNormalformBuilder.java @@ -39,7 +39,7 @@ * methodcall <init>. The visibility of * the normalform is the same as for the original constructor. */ -public class ConstructorNormalformBuilder extends JavaTransformer { +public class ConstructorNormalformBuilder extends JavaTransformerAbstract { /** * creates the constructor normalform builder */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/CreateBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/CreateBuilder.java index eb3a272bb6f..c525e3eea82 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/CreateBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/CreateBuilder.java @@ -39,7 +39,7 @@ * another implicit method lt;prepare> for setting the fields * default values. */ -public class CreateBuilder extends JavaTransformer { +public class CreateBuilder extends JavaTransformerAbstract { public static final String IMPLICIT_CREATE = "$create"; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/CreateObjectBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/CreateObjectBuilder.java index 6d37700ab4e..73d178a509f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/CreateObjectBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/CreateObjectBuilder.java @@ -41,7 +41,7 @@ * another implicit method lt;prepare> for setting the fields * default values. */ -public class CreateObjectBuilder extends JavaTransformer { +public class CreateObjectBuilder extends JavaTransformerAbstract { public static final String IMPLICIT_OBJECT_CREATE = "$createObject"; public static final String NEW_OBJECT_VAR_NAME = "__NEW__"; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/EnumClassBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/EnumClassBuilder.java index 20cecd81a90..13a0b353371 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/EnumClassBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/EnumClassBuilder.java @@ -19,7 +19,7 @@ /// @author mulbrich, drodt /// @since 2006-11-20 /// @version 2026-03-03 -public class EnumClassBuilder extends JavaTransformer { +public class EnumClassBuilder extends JavaTransformerAbstract { /// a mapping of enums to the newly created class declarations. final Map substitutes = new LinkedHashMap<>(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ImplicitFieldAdder.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ImplicitFieldAdder.java index ff95eb023dc..d3f58684bb3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ImplicitFieldAdder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/ImplicitFieldAdder.java @@ -38,7 +38,7 @@ * them will access these fields, this transformer has to be executed * before the other transformers are called. */ -public class ImplicitFieldAdder extends JavaTransformer { +public class ImplicitFieldAdder extends JavaTransformerAbstract { /** * flag set if java.lang.Object has been already transformed diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/InstanceAllocationMethodBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/InstanceAllocationMethodBuilder.java index b5c11ce27bf..6198056db28 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/InstanceAllocationMethodBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/InstanceAllocationMethodBuilder.java @@ -27,7 +27,7 @@ * to allocate a new object of the type it is declared in and to return it. * The functionality will be described using taclets */ -public class InstanceAllocationMethodBuilder extends JavaTransformer { +public class InstanceAllocationMethodBuilder extends JavaTransformerAbstract { public InstanceAllocationMethodBuilder(TransformationPipelineServices services) { super(services); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLCommentTransformer.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLCommentTransformer.java index e2b3dcbd311..da3e18a6179 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLCommentTransformer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLCommentTransformer.java @@ -29,7 +29,7 @@ * JavaParser. It should not be used anymore. */ @Deprecated(forRemoval = true) -public class JMLCommentTransformer extends JavaTransformer { +public class JMLCommentTransformer extends JavaTransformerAbstract { public static final DataKey> BEFORE_COMMENTS = new DataKey<>() { }; public static final DataKey> AFTER_COMMENTS = new DataKey<>() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLTransformer.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLTransformer.java index c24de23403f..a3ccddb756c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLTransformer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JMLTransformer.java @@ -55,7 +55,7 @@ /// /// Support for ghost statements. /// -/// After execution this {@link JavaTransformer}, contracts are attached to +/// After execution this {@link JavaTransformerAbstract}, contracts are attached to /// {@link MethodDeclaration}, or {@link BlockStmt}, {@link FieldDeclaration} and /// {@link MethodDeclaration} were introduced for ghost and model declarations, /// JML statements (assume, assert, ...) are inserted into the bodies using @@ -75,7 +75,7 @@ /// @author pfeifer /// @author ulbrich @SuppressWarnings("OptionalGetWithoutIsPresent") -public final class JMLTransformer extends JavaTransformer { +public final class JMLTransformer extends JavaTransformerAbstract { public static final EnumSet JAVA_MODS = EnumSet.of(JMLModifier.ABSTRACT, JMLModifier.FINAL, JMLModifier.PRIVATE, JMLModifier.PROTECTED, JMLModifier.PUBLIC, JMLModifier.STATIC); 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..554523c61eb 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,67 +4,35 @@ 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). + * A transformation of Java ASTs in an early loading stage. *

- * 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}
    • - *
+ * A {@link JavaTransformer} 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} *

- * 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. + * Implementation should be stateless as instances are reused accross {@link CompilationUnit}s but + * not across + * loading requests. + * + * @author weigl */ @NullMarked -public abstract class JavaTransformer { - /** - * Further services and helper function for this pipeline step. - */ - protected final TransformationPipelineServices services; - - /** - * a cache object that stores information which is needed by - * and common to many transformations. it includes the - * compilation units, the declared classes, and information - * for local classes. - */ - protected final TransformationPipelineServices.TransformerCache cache; - - /** - * creates a transformer for the recoder model - * - * @param services - * the CrossReferenceServiceConfiguration to access - * model information - */ - public JavaTransformer(TransformationPipelineServices services) { - this.services = services; - this.cache = services.getCache(); +public interface JavaTransformer { + /// Modifying the given `td` without constraints. + default void apply(TypeDeclaration td) { } - /** - * The method is called for each type declaration of the compilation - * unit and initiates the syntactical transformation. If you want to - * descend in inner classes you have to implement the recursion by - * yourself. - */ - public void apply(TypeDeclaration td) {} - - public void apply(CompilationUnit cu) { + /// Transform the given {@link CompilationUnit} in place. The default implementation + /// iterates over all {@link TypeDeclaration}, and calls {@link #apply(TypeDeclaration)}. + default void apply(CompilationUnit cu) { for (TypeDeclaration type : cu.getTypes()) { apply(type); for (var m : type.getMembers()) { @@ -74,14 +42,4 @@ public void apply(CompilationUnit cu) { } } } - - public static RuntimeException reportError(Node node, String message, Object... args) { - var path = node.findCompilationUnit().flatMap(CompilationUnit::getStorage) - .map(it -> it.getPath().toString()) - .orElse(""); - var line = node.getRange().map(it -> it.begin.line).orElse(-1); - var col = node.getRange().map(it -> it.begin.column).orElse(-1); - var pos = " at " + path + ":" + line + ":" + col; - return new IllegalStateException(String.format(message + pos, args)); - } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JavaTransformerAbstract.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JavaTransformerAbstract.java new file mode 100644 index 00000000000..4c7792c8986 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JavaTransformerAbstract.java @@ -0,0 +1,79 @@ +/* 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; + +/** + * {@link JavaTransformer} 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 JavaTransformerAbstract implements JavaTransformer { + /** + * Further services and helper function for this pipeline step. + */ + protected final TransformationPipelineServices services; + + /** + * a cache object that stores information which is needed by + * and common to many transformations. it includes the + * compilation units, the declared classes, and information + * for local classes. + */ + protected final TransformationPipelineServices.TransformerCache cache; + + /** + * creates a transformer for the recoder model + * + * @param services the CrossReferenceServiceConfiguration to access + * model information + */ + public JavaTransformerAbstract(TransformationPipelineServices services) { + this.services = services; + this.cache = services.getCache(); + } + + /** + * The method is called for each type declaration of the compilation + * unit and initiates the syntactical transformation. If you want to + * descend in inner classes you have to implement the recursion by + * yourself. + */ + @Override + public void apply(TypeDeclaration td) { + } + + @Override + public void apply(CompilationUnit cu) { + for (TypeDeclaration type : cu.getTypes()) { + apply(type); + for (var m : type.getMembers()) { + if (m instanceof TypeDeclaration ty) { + apply(ty); + } + } + } + } + + public static RuntimeException reportError(Node node, String message, Object... args) { + var path = node.findCompilationUnit().flatMap(CompilationUnit::getStorage) + .map(it -> it.getPath().toString()) + .orElse(""); + var line = node.getRange().map(it -> it.begin.line).orElse(-1); + var col = node.getRange().map(it -> it.begin.column).orElse(-1); + var pos = " at " + path + ":" + line + ":" + col; + return new IllegalStateException(String.format(message + pos, args)); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JmlDocRemoval.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JmlDocRemoval.java index cd1d0721a2b..d862d1d42a1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JmlDocRemoval.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/JmlDocRemoval.java @@ -16,7 +16,7 @@ * @author Alexander Weigl * @version 1 (3/3/26) */ -public class JmlDocRemoval extends JavaTransformer { +public class JmlDocRemoval extends JavaTransformerAbstract { public JmlDocRemoval(@NonNull TransformationPipelineServices services) { super(services); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/LocalClassTransformation.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/LocalClassTransformation.java index 77164286d9f..27cb871c8f0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/LocalClassTransformation.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/LocalClassTransformation.java @@ -32,7 +32,7 @@ * * @author engelc */ -public class LocalClassTransformation extends JavaTransformer { +public class LocalClassTransformation extends JavaTransformerAbstract { public LocalClassTransformation(TransformationPipelineServices services) { super(services); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/PrepareObjectBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/PrepareObjectBuilder.java index 98e84919d1d..e0425349d97 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/PrepareObjectBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/PrepareObjectBuilder.java @@ -42,7 +42,7 @@ * Creates the preparation method for pre-initilizing the object fields * with their default settings. */ -public class PrepareObjectBuilder extends JavaTransformer { +public class PrepareObjectBuilder extends JavaTransformerAbstract { public PrepareObjectBuilder(TransformationPipelineServices services) { super(services); } 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..4db01c65f65 --- /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 JavaTransformer { + @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..07f9985230a 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.JavaTransformerAbstract; import de.uka.ilkd.key.java.transformations.pipeline.TransformationPipelineServices; import de.uka.ilkd.key.nparser.NamespaceBuilder; import de.uka.ilkd.key.proof.init.JavaProfile; @@ -105,10 +106,15 @@ private Stream generatePipelineTests(Path testFolder) throws IOExce var expected = testFolder.resolve("expected"); var actual = testFolder.resolve("actual"); - return Files.walk(expected) - .filter(Files::isRegularFile) - .map(it -> DynamicTest.dynamicTest(it.toString(), - () -> checkEqualFile(it, expected, actual))); + if (Files.exists(expected)) { + return Files.walk(expected) + .filter(Files::isRegularFile) + .map(it -> DynamicTest.dynamicTest(it.toString(), + () -> checkEqualFile(it, expected, actual))); + } else { + Files.createDirectories(expected); + return Stream.empty(); + } } private void checkEqualFile(Path expectedFile, Path expectedFolder, Path actualFolder) @@ -123,7 +129,7 @@ private void checkEqualFile(Path expectedFile, Path expectedFolder, Path actualF Truth.assertThat(actual).isEqualTo(expected); } - private static class DebugOutputTransformer extends JavaTransformer { + private static class DebugOutputTransformer extends JavaTransformerAbstract { final Path outputFolder; final Set alreadyWritten = new HashSet<>(); private static final Logger LOGGER = LoggerFactory.getLogger(DebugOutputTransformer.class); 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/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java index 19491d1632d..aa17ce320cc 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java @@ -1018,6 +1018,9 @@ public static ProofCollection automaticJavaDL() throws IOException { g = c.group("PolymorphicSorts"); g.loadable("standard_key/polymorphic/pseq.key"); + g = c.group("JavaFeatures"); + g.loadable("Java/TextBlockLiterals/project.key"); + // use for debugging purposes. // c.keep("VSTTE10"); String s = System.getenv(ENV_KEY_RAP_FUN_KEEP); 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 diff --git a/key.ui/examples/Java/TextBlockLiterals/README.txt b/key.ui/examples/Java/TextBlockLiterals/README.txt new file mode 100644 index 00000000000..ffb245ce84d --- /dev/null +++ b/key.ui/examples/Java/TextBlockLiterals/README.txt @@ -0,0 +1,8 @@ +example.name = Text Block Literals +example.path = Java 25 +example.file = project.key +example.additionalFile.1 = TextBlockLiterals.java + +Text Block Literals are supported in KeY. They are reduced to normal String literals. + +The proof obligation is verifiable without user interaction. diff --git a/key.ui/examples/Java/TextBlockLiterals/TextBlockLiterals.java b/key.ui/examples/Java/TextBlockLiterals/TextBlockLiterals.java new file mode 100644 index 00000000000..10227cf77cf --- /dev/null +++ b/key.ui/examples/Java/TextBlockLiterals/TextBlockLiterals.java @@ -0,0 +1,14 @@ +public final class TextBlockLiterals { + /*@ ensures true; requires true; */ + public void m() { + String textBlock = """ + line 1 + line 2 + line 3 + """; + + String oldFashionedLiteral = "line 1\nline 2\nline 3\n"; + + assert(textBlock.equals(oldFashionedLiteral)); + } +} \ No newline at end of file diff --git a/key.ui/examples/Java/TextBlockLiterals/project.key b/key.ui/examples/Java/TextBlockLiterals/project.key new file mode 100644 index 00000000000..d61f0f7e40f --- /dev/null +++ b/key.ui/examples/Java/TextBlockLiterals/project.key @@ -0,0 +1,8 @@ +\profile "Java Profile"; +\javaSource "."; + +\proofObligation { + "class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + "contract" : "TextBlockLiterals[TextBlockLiterals::m()].JML operation contract.0", + "name" : "TextBlockLiterals[TextBlockLiterals::m()].JML operation contract.0" +} diff --git a/key.ui/examples/index/samplesIndex.txt b/key.ui/examples/index/samplesIndex.txt index 673e17f3d38..fd477b2abff 100644 --- a/key.ui/examples/index/samplesIndex.txt +++ b/key.ui/examples/index/samplesIndex.txt @@ -20,6 +20,10 @@ firstTouch/09-Quicktour/README.txt firstTouch/10-SITA/README.txt firstTouch/11-StateMerging/README.txt +# Java Features +Java/TextBlockLiterals/README.txt + + # The KeY Book (note: the comments here are only for maintainability, if you want to move an entry to a different section, look into the individual txt file!) ## Chapter 15 - Using the KeY Prover newBook/Using_KeY/Building_Propositional_Proofs/README.txt