From 0af69a7671cc0b119e31046a8a7bcb14a09b8b5c Mon Sep 17 00:00:00 2001 From: Drodt Date: Wed, 10 Jun 2026 13:01:40 +0200 Subject: [PATCH 1/3] Start on var types --- .../ilkd/key/java/loader/JavaParserFactory.java | 11 +++++++++++ .../de/uka/ilkd/key/proof/rules/javaRules.key | 14 ++++++++++++++ .../standard_key/java_dl/typeInference.key | 10 ++++++++++ .../java_dl/typeInference_java/TypeInference.java | 7 +++++++ 4 files changed, 42 insertions(+) create mode 100644 key.ui/examples/standard_key/java_dl/typeInference.key create mode 100644 key.ui/examples/standard_key/java_dl/typeInference_java/TypeInference.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JavaParserFactory.java b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JavaParserFactory.java index a47df45f6f1..0c846670cca 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JavaParserFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JavaParserFactory.java @@ -16,10 +16,13 @@ import com.github.javaparser.JavaParser; import com.github.javaparser.ParseResult; import com.github.javaparser.ParserConfiguration; +import com.github.javaparser.Processor; import com.github.javaparser.ast.CompilationUnit; +import com.github.javaparser.ast.Node; import com.github.javaparser.ast.body.TypeDeclaration; import com.github.javaparser.ast.key.sv.KeyContextStatementBlock; import com.github.javaparser.ast.stmt.BlockStmt; +import com.github.javaparser.ast.validator.postprocessors.Java10PostProcessor; import com.github.javaparser.resolution.Navigator; import com.github.javaparser.resolution.TypeSolver; import com.github.javaparser.resolution.declarations.ResolvedReferenceTypeDeclaration; @@ -95,6 +98,14 @@ private ParserConfiguration getConfiguration() { config.setStoreTokens(true); } config.setLanguageLevel(ParserConfiguration.LanguageLevel.RAW); + config.getProcessors().add(() -> new Processor() { + @Override + public void postProcess(ParseResult result, + ParserConfiguration configuration) { + var pp = new Java10PostProcessor(); + pp.postProcess(result, configuration); + } + }); config.setSymbolResolver(getSymbolSolver()); return config; } diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key index 2b717039620..9b666fbffa0 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key @@ -433,6 +433,20 @@ \displayname "variableDeclaration" }; + variableDeclarationAssignVar { + \find(\modality{#allmodal}{.. var #v0 = #vi; ...}\endmodality (post)) + \replacewith(\modality{#allmodal}{.. #typeof(#v0) #v0; #v0 = #vi ...}\endmodality (post)) + \heuristics(simplify_prog, simplify_prog_subset) + \displayname "variableDeclaration" + }; + + variableDeclarationFinalAssignVar { + \find(\modality{#allmodal}{.. final var #v0 = #vi; ...}\endmodality (post)) + \replacewith(\modality{#allmodal}{.. final #typeof(#v0) #v0; #v0 = #vi ...}\endmodality (post)) + \heuristics(simplify_prog, simplify_prog_subset) + \displayname "variableDeclaration" + }; + /* variableDeclarationNullable { \find(\modality{#allmodal}{.. nullable #t #v0; ...}\endmodality (post)) diff --git a/key.ui/examples/standard_key/java_dl/typeInference.key b/key.ui/examples/standard_key/java_dl/typeInference.key new file mode 100644 index 00000000000..190de49695b --- /dev/null +++ b/key.ui/examples/standard_key/java_dl/typeInference.key @@ -0,0 +1,10 @@ +\javaSource "typeInference_java/"; + +\programVariables { + int _a; + int _b; +} + +\problem { + _a + _b + 3 = m(_a, _b) +} \ No newline at end of file diff --git a/key.ui/examples/standard_key/java_dl/typeInference_java/TypeInference.java b/key.ui/examples/standard_key/java_dl/typeInference_java/TypeInference.java new file mode 100644 index 00000000000..d6d33b7bdc6 --- /dev/null +++ b/key.ui/examples/standard_key/java_dl/typeInference_java/TypeInference.java @@ -0,0 +1,7 @@ +class TypeInference { + static int m(int a, int b) { + var x = a + 1; + final var y = b + 2; + return x + y; + } +} \ No newline at end of file From d0545ca77b65524b72310eb2b8b4fb698d7d3efc Mon Sep 17 00:00:00 2001 From: Drodt Date: Wed, 10 Jun 2026 13:20:11 +0200 Subject: [PATCH 2/3] Handle VarType --- .../uka/ilkd/key/java/loader/JP2KeYConverter.java | 3 ++- .../de/uka/ilkd/key/proof/rules/javaRules.key | 14 -------------- .../key/proof/runallproofs/ProofCollections.java | 1 + .../standard_key/java_dl/typeInference.key | 2 +- 4 files changed, 4 insertions(+), 16 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java index 0820a14a8d2..c9b38d27514 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java @@ -2158,7 +2158,8 @@ public Object visit(ReceiverParameter n, Void arg) { @Override public Object visit(VarType n, Void arg) { - return getKeYJavaType(n.resolve()); + var kjt = getKeYJavaType(n.resolve()); + return new TypeRef(kjt); } @Override diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key index 9b666fbffa0..2b717039620 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key @@ -433,20 +433,6 @@ \displayname "variableDeclaration" }; - variableDeclarationAssignVar { - \find(\modality{#allmodal}{.. var #v0 = #vi; ...}\endmodality (post)) - \replacewith(\modality{#allmodal}{.. #typeof(#v0) #v0; #v0 = #vi ...}\endmodality (post)) - \heuristics(simplify_prog, simplify_prog_subset) - \displayname "variableDeclaration" - }; - - variableDeclarationFinalAssignVar { - \find(\modality{#allmodal}{.. final var #v0 = #vi; ...}\endmodality (post)) - \replacewith(\modality{#allmodal}{.. final #typeof(#v0) #v0; #v0 = #vi ...}\endmodality (post)) - \heuristics(simplify_prog, simplify_prog_subset) - \displayname "variableDeclaration" - }; - /* variableDeclarationNullable { \find(\modality{#allmodal}{.. nullable #t #v0; ...}\endmodality (post)) 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 2e935059e3e..a686edbe37d 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 @@ -653,6 +653,7 @@ public static ProofCollection automaticJavaDL() throws IOException { g.provable("../../key.core/src/test/resources/testcase/classpath/classpath.key"); g.notprovable("heap/inconsistent_represents/MyClass_m.key"); g.notprovable("heap/inconsistent_represents/MyClass_n.key"); + g.provable("standard_key/java_dl/typeInference.key"); g = c.group("FOL"); diff --git a/key.ui/examples/standard_key/java_dl/typeInference.key b/key.ui/examples/standard_key/java_dl/typeInference.key index 190de49695b..30f633a313e 100644 --- a/key.ui/examples/standard_key/java_dl/typeInference.key +++ b/key.ui/examples/standard_key/java_dl/typeInference.key @@ -6,5 +6,5 @@ } \problem { - _a + _b + 3 = m(_a, _b) + _a + _b + 3 = TypeInference.m(_a, _b) } \ No newline at end of file From c6baf8e897e5967778ce1cfc6c897ae23fb53459 Mon Sep 17 00:00:00 2001 From: Drodt Date: Wed, 10 Jun 2026 16:39:15 +0200 Subject: [PATCH 3/3] Fix strategy settings in test --- key.ui/examples/standard_key/java_dl/typeInference.key | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/key.ui/examples/standard_key/java_dl/typeInference.key b/key.ui/examples/standard_key/java_dl/typeInference.key index 30f633a313e..6338156850c 100644 --- a/key.ui/examples/standard_key/java_dl/typeInference.key +++ b/key.ui/examples/standard_key/java_dl/typeInference.key @@ -1,3 +1,12 @@ +\settings { + "Strategy": { + "options" : { + "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON", + "QUERY_NEW_OPTIONS_KEY" : "QUERY_ON" + } + } +} + \javaSource "typeInference_java/"; \programVariables {