diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 51910bfe924..a476d886c1f 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -28,7 +28,7 @@ jobs: keyext.exploration, keyext.slicing, key.ncore, key.ui, key.core, key.core.rifl, key.core.testgen, keyext.isabelletranslation, keyext.ui.testgen, key.ncore.calculus, key.util, key.core.example, keyext.caching, - keyext.proofmanagement, key.removegenerics ] + keyext.proofmanagement, key.removegenerics, keyext.rusty ] continue-on-error: true runs-on: ${{ matrix.os }} env: diff --git a/.gitmodules b/.gitmodules index aa7a27fd971..b52ff417ef8 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,6 +1,6 @@ [submodule "keyext.rusty/rust-wrapper/rust"] path = keyext.rusty/rust-wrapper/rust url = git@github.com:rust-lang/rust.git -[submodule "rust-wrapper"] - path = rust-wrapper - url = https://github.com/Drodt/KeY-rustc-wrapper.git +[submodule "rml"] + path = rml + url = https://github.com/yseulp/rml.git diff --git a/keyext.rusty/example/Cargo.lock b/keyext.rusty/example/Cargo.lock new file mode 100644 index 00000000000..9dc6e3e5830 --- /dev/null +++ b/keyext.rusty/example/Cargo.lock @@ -0,0 +1,7 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 4 + +[[package]] +name = "example" +version = "0.1.0" diff --git a/keyext.rusty/example/target/.rustc_info.json b/keyext.rusty/example/target/.rustc_info.json new file mode 100644 index 00000000000..f2b75b6e98e --- /dev/null +++ b/keyext.rusty/example/target/.rustc_info.json @@ -0,0 +1 @@ +{"rustc_fingerprint":6139828803497917698,"outputs":{"17747080675513052775":{"success":true,"status":"","code":0,"stdout":"rustc 1.88.0 (6b00bc388 2025-06-23)\nbinary: rustc\ncommit-hash: 6b00bc3880198600130e1cf62b8f8a93494488cc\ncommit-date: 2025-06-23\nhost: x86_64-unknown-linux-gnu\nrelease: 1.88.0\nLLVM version: 20.1.5\n","stderr":""},"11857020428658561806":{"success":true,"status":"","code":0,"stdout":"___\nlib___.rlib\nlib___.so\nlib___.so\nlib___.a\nlib___.so\n/home/yseulp/.rustup/toolchains/stable-x86_64-unknown-linux-gnu\noff\npacked\nunpacked\n___\ndebug_assertions\npanic=\"unwind\"\nproc_macro\ntarget_abi=\"\"\ntarget_arch=\"x86_64\"\ntarget_endian=\"little\"\ntarget_env=\"gnu\"\ntarget_family=\"unix\"\ntarget_feature=\"fxsr\"\ntarget_feature=\"sse\"\ntarget_feature=\"sse2\"\ntarget_has_atomic=\"16\"\ntarget_has_atomic=\"32\"\ntarget_has_atomic=\"64\"\ntarget_has_atomic=\"8\"\ntarget_has_atomic=\"ptr\"\ntarget_os=\"linux\"\ntarget_pointer_width=\"64\"\ntarget_vendor=\"unknown\"\nunix\n","stderr":""},"7971740275564407648":{"success":true,"status":"","code":0,"stdout":"___\nlib___.rlib\nlib___.so\nlib___.so\nlib___.a\nlib___.so\n/home/yseulp/.rustup/toolchains/stable-x86_64-unknown-linux-gnu\noff\npacked\nunpacked\n___\ndebug_assertions\npanic=\"unwind\"\nproc_macro\ntarget_abi=\"\"\ntarget_arch=\"x86_64\"\ntarget_endian=\"little\"\ntarget_env=\"gnu\"\ntarget_family=\"unix\"\ntarget_feature=\"fxsr\"\ntarget_feature=\"sse\"\ntarget_feature=\"sse2\"\ntarget_has_atomic=\"16\"\ntarget_has_atomic=\"32\"\ntarget_has_atomic=\"64\"\ntarget_has_atomic=\"8\"\ntarget_has_atomic=\"ptr\"\ntarget_os=\"linux\"\ntarget_pointer_width=\"64\"\ntarget_vendor=\"unknown\"\nunix\n","stderr":""}},"successes":{}} \ No newline at end of file diff --git a/keyext.rusty/example/target/CACHEDIR.TAG b/keyext.rusty/example/target/CACHEDIR.TAG new file mode 100644 index 00000000000..20d7c319cda --- /dev/null +++ b/keyext.rusty/example/target/CACHEDIR.TAG @@ -0,0 +1,3 @@ +Signature: 8a477f597d28d172789f06886806bc55 +# This file is a cache directory tag created by cargo. +# For information about cache directory tags see https://bford.info/cachedir/ diff --git a/keyext.rusty/example/target/debug/.cargo-lock b/keyext.rusty/example/target/debug/.cargo-lock new file mode 100644 index 00000000000..e69de29bb2d diff --git a/keyext.rusty/example/target/debug/.fingerprint/example-14b6227221523c01/dep-lib-example b/keyext.rusty/example/target/debug/.fingerprint/example-14b6227221523c01/dep-lib-example new file mode 100644 index 00000000000..024be490456 Binary files /dev/null and b/keyext.rusty/example/target/debug/.fingerprint/example-14b6227221523c01/dep-lib-example differ diff --git a/keyext.rusty/example/target/debug/.fingerprint/example-14b6227221523c01/invoked.timestamp b/keyext.rusty/example/target/debug/.fingerprint/example-14b6227221523c01/invoked.timestamp new file mode 100644 index 00000000000..e00328da5aa --- /dev/null +++ b/keyext.rusty/example/target/debug/.fingerprint/example-14b6227221523c01/invoked.timestamp @@ -0,0 +1 @@ +This file has an mtime of when this was started. \ No newline at end of file diff --git a/keyext.rusty/example/target/debug/.fingerprint/example-14b6227221523c01/lib-example b/keyext.rusty/example/target/debug/.fingerprint/example-14b6227221523c01/lib-example new file mode 100644 index 00000000000..238eeb96de1 --- /dev/null +++ b/keyext.rusty/example/target/debug/.fingerprint/example-14b6227221523c01/lib-example @@ -0,0 +1 @@ +94ed5a9cb32ba0b1 \ No newline at end of file diff --git a/keyext.rusty/example/target/debug/.fingerprint/example-14b6227221523c01/lib-example.json b/keyext.rusty/example/target/debug/.fingerprint/example-14b6227221523c01/lib-example.json new file mode 100644 index 00000000000..c8ecd585543 --- /dev/null +++ b/keyext.rusty/example/target/debug/.fingerprint/example-14b6227221523c01/lib-example.json @@ -0,0 +1 @@ +{"rustc":11410426090777951712,"features":"[]","declared_features":"[]","target":18343425508367059059,"profile":17672942494452627365,"path":10763286916239946207,"deps":[],"local":[{"CheckDepInfo":{"dep_info":"debug/.fingerprint/example-14b6227221523c01/dep-lib-example","checksum":false}}],"rustflags":[],"config":2069994364910194474,"compile_kind":0} \ No newline at end of file diff --git a/keyext.rusty/example/target/debug/.fingerprint/example-b6d004a4079f250b/dep-test-lib-example b/keyext.rusty/example/target/debug/.fingerprint/example-b6d004a4079f250b/dep-test-lib-example new file mode 100644 index 00000000000..024be490456 Binary files /dev/null and b/keyext.rusty/example/target/debug/.fingerprint/example-b6d004a4079f250b/dep-test-lib-example differ diff --git a/keyext.rusty/example/target/debug/.fingerprint/example-b6d004a4079f250b/invoked.timestamp b/keyext.rusty/example/target/debug/.fingerprint/example-b6d004a4079f250b/invoked.timestamp new file mode 100644 index 00000000000..e00328da5aa --- /dev/null +++ b/keyext.rusty/example/target/debug/.fingerprint/example-b6d004a4079f250b/invoked.timestamp @@ -0,0 +1 @@ +This file has an mtime of when this was started. \ No newline at end of file diff --git a/keyext.rusty/example/target/debug/.fingerprint/example-b6d004a4079f250b/test-lib-example b/keyext.rusty/example/target/debug/.fingerprint/example-b6d004a4079f250b/test-lib-example new file mode 100644 index 00000000000..abcb529180d --- /dev/null +++ b/keyext.rusty/example/target/debug/.fingerprint/example-b6d004a4079f250b/test-lib-example @@ -0,0 +1 @@ +d855d1ce1ee45f13 \ No newline at end of file diff --git a/keyext.rusty/example/target/debug/.fingerprint/example-b6d004a4079f250b/test-lib-example.json b/keyext.rusty/example/target/debug/.fingerprint/example-b6d004a4079f250b/test-lib-example.json new file mode 100644 index 00000000000..bc38dfd2c8b --- /dev/null +++ b/keyext.rusty/example/target/debug/.fingerprint/example-b6d004a4079f250b/test-lib-example.json @@ -0,0 +1 @@ +{"rustc":11410426090777951712,"features":"[]","declared_features":"[]","target":18343425508367059059,"profile":3316208278650011218,"path":10763286916239946207,"deps":[],"local":[{"CheckDepInfo":{"dep_info":"debug/.fingerprint/example-b6d004a4079f250b/dep-test-lib-example","checksum":false}}],"rustflags":[],"config":2069994364910194474,"compile_kind":0} \ No newline at end of file diff --git a/keyext.rusty/example/target/debug/deps/example-14b6227221523c01.d b/keyext.rusty/example/target/debug/deps/example-14b6227221523c01.d new file mode 100644 index 00000000000..6266b28aa8e --- /dev/null +++ b/keyext.rusty/example/target/debug/deps/example-14b6227221523c01.d @@ -0,0 +1,5 @@ +/home/yseulp/uni/thesis/key/keyext.rusty/example/target/debug/deps/example-14b6227221523c01.d: src/lib.rs + +/home/yseulp/uni/thesis/key/keyext.rusty/example/target/debug/deps/libexample-14b6227221523c01.rmeta: src/lib.rs + +src/lib.rs: diff --git a/keyext.rusty/example/target/debug/deps/example-b6d004a4079f250b.d b/keyext.rusty/example/target/debug/deps/example-b6d004a4079f250b.d new file mode 100644 index 00000000000..94775bddd8f --- /dev/null +++ b/keyext.rusty/example/target/debug/deps/example-b6d004a4079f250b.d @@ -0,0 +1,5 @@ +/home/yseulp/uni/thesis/key/keyext.rusty/example/target/debug/deps/example-b6d004a4079f250b.d: src/lib.rs + +/home/yseulp/uni/thesis/key/keyext.rusty/example/target/debug/deps/libexample-b6d004a4079f250b.rmeta: src/lib.rs + +src/lib.rs: diff --git a/keyext.rusty/example/target/debug/deps/libexample-14b6227221523c01.rmeta b/keyext.rusty/example/target/debug/deps/libexample-14b6227221523c01.rmeta new file mode 100644 index 00000000000..3ac4d2c7114 Binary files /dev/null and b/keyext.rusty/example/target/debug/deps/libexample-14b6227221523c01.rmeta differ diff --git a/keyext.rusty/example/target/debug/deps/libexample-b6d004a4079f250b.rmeta b/keyext.rusty/example/target/debug/deps/libexample-b6d004a4079f250b.rmeta new file mode 100644 index 00000000000..e69de29bb2d diff --git a/keyext.rusty/example/target/debug/incremental/example-2lbgrvj3209f0/s-ha26rz6d0i-0cdzzv0-etu67dn3wqmfwljkewuqvtk4d/dep-graph.bin b/keyext.rusty/example/target/debug/incremental/example-2lbgrvj3209f0/s-ha26rz6d0i-0cdzzv0-etu67dn3wqmfwljkewuqvtk4d/dep-graph.bin new file mode 100644 index 00000000000..dc90969980b Binary files /dev/null and b/keyext.rusty/example/target/debug/incremental/example-2lbgrvj3209f0/s-ha26rz6d0i-0cdzzv0-etu67dn3wqmfwljkewuqvtk4d/dep-graph.bin differ diff --git a/keyext.rusty/example/target/debug/incremental/example-2lbgrvj3209f0/s-ha26rz6d0i-0cdzzv0-etu67dn3wqmfwljkewuqvtk4d/query-cache.bin b/keyext.rusty/example/target/debug/incremental/example-2lbgrvj3209f0/s-ha26rz6d0i-0cdzzv0-etu67dn3wqmfwljkewuqvtk4d/query-cache.bin new file mode 100644 index 00000000000..28ee982ca84 Binary files /dev/null and b/keyext.rusty/example/target/debug/incremental/example-2lbgrvj3209f0/s-ha26rz6d0i-0cdzzv0-etu67dn3wqmfwljkewuqvtk4d/query-cache.bin differ diff --git a/keyext.rusty/example/target/debug/incremental/example-2lbgrvj3209f0/s-ha26rz6d0i-0cdzzv0-etu67dn3wqmfwljkewuqvtk4d/work-products.bin b/keyext.rusty/example/target/debug/incremental/example-2lbgrvj3209f0/s-ha26rz6d0i-0cdzzv0-etu67dn3wqmfwljkewuqvtk4d/work-products.bin new file mode 100644 index 00000000000..682eda3aedc Binary files /dev/null and b/keyext.rusty/example/target/debug/incremental/example-2lbgrvj3209f0/s-ha26rz6d0i-0cdzzv0-etu67dn3wqmfwljkewuqvtk4d/work-products.bin differ diff --git a/keyext.rusty/example/target/debug/incremental/example-2lbgrvj3209f0/s-ha26rz6d0i-0cdzzv0.lock b/keyext.rusty/example/target/debug/incremental/example-2lbgrvj3209f0/s-ha26rz6d0i-0cdzzv0.lock new file mode 100644 index 00000000000..e69de29bb2d diff --git a/keyext.rusty/example/target/debug/incremental/example-3gcxqz3mtddmu/s-ha26rz6cy2-0hr1jw4-8t7yx7dw304uy3njz7rdlw1y7/dep-graph.bin b/keyext.rusty/example/target/debug/incremental/example-3gcxqz3mtddmu/s-ha26rz6cy2-0hr1jw4-8t7yx7dw304uy3njz7rdlw1y7/dep-graph.bin new file mode 100644 index 00000000000..53ad609df98 Binary files /dev/null and b/keyext.rusty/example/target/debug/incremental/example-3gcxqz3mtddmu/s-ha26rz6cy2-0hr1jw4-8t7yx7dw304uy3njz7rdlw1y7/dep-graph.bin differ diff --git a/keyext.rusty/example/target/debug/incremental/example-3gcxqz3mtddmu/s-ha26rz6cy2-0hr1jw4-8t7yx7dw304uy3njz7rdlw1y7/query-cache.bin b/keyext.rusty/example/target/debug/incremental/example-3gcxqz3mtddmu/s-ha26rz6cy2-0hr1jw4-8t7yx7dw304uy3njz7rdlw1y7/query-cache.bin new file mode 100644 index 00000000000..f9408230b2e Binary files /dev/null and b/keyext.rusty/example/target/debug/incremental/example-3gcxqz3mtddmu/s-ha26rz6cy2-0hr1jw4-8t7yx7dw304uy3njz7rdlw1y7/query-cache.bin differ diff --git a/keyext.rusty/example/target/debug/incremental/example-3gcxqz3mtddmu/s-ha26rz6cy2-0hr1jw4-8t7yx7dw304uy3njz7rdlw1y7/work-products.bin b/keyext.rusty/example/target/debug/incremental/example-3gcxqz3mtddmu/s-ha26rz6cy2-0hr1jw4-8t7yx7dw304uy3njz7rdlw1y7/work-products.bin new file mode 100644 index 00000000000..682eda3aedc Binary files /dev/null and b/keyext.rusty/example/target/debug/incremental/example-3gcxqz3mtddmu/s-ha26rz6cy2-0hr1jw4-8t7yx7dw304uy3njz7rdlw1y7/work-products.bin differ diff --git a/keyext.rusty/example/target/debug/incremental/example-3gcxqz3mtddmu/s-ha26rz6cy2-0hr1jw4.lock b/keyext.rusty/example/target/debug/incremental/example-3gcxqz3mtddmu/s-ha26rz6cy2-0hr1jw4.lock new file mode 100644 index 00000000000..e69de29bb2d diff --git a/keyext.rusty/src/main/antlr/RustySchemaLexer.g4 b/keyext.rusty/src/main/antlr/RustySchemaLexer.g4 index 379a0affcdc..ba9c32ee7f3 100644 --- a/keyext.rusty/src/main/antlr/RustySchemaLexer.g4 +++ b/keyext.rusty/src/main/antlr/RustySchemaLexer.g4 @@ -27,4 +27,8 @@ PANIC FN_FRAME: 'fn_frame!'; + GHOST: 'ghost!'; + + SNAPSHOT: 'snapshot!'; + PANIC_FRAME: 'panic_frame!'; \ No newline at end of file diff --git a/keyext.rusty/src/main/antlr/RustySchemaParser.g4 b/keyext.rusty/src/main/antlr/RustySchemaParser.g4 index 3eac63cbf07..284c1073a31 100644 --- a/keyext.rusty/src/main/antlr/RustySchemaParser.g4 +++ b/keyext.rusty/src/main/antlr/RustySchemaParser.g4 @@ -48,6 +48,8 @@ expr | closureExpr # ClosureExpression_ | exprWithBlock # ExpressionWithBlock_ | PANIC LPAREN RPAREN # EmptyPanic + | GHOST blockExpr # GhostBlockExpression + | SNAPSHOT LPAREN schemaVariable RPAREN # SnapshotExpression ; stmt diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/RustInfo.java b/keyext.rusty/src/main/java/org/key_project/rusty/RustInfo.java index 0aa2f2c9904..edb83adb816 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/RustInfo.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/RustInfo.java @@ -79,6 +79,10 @@ public KeYRustyType getKeYRustyType(Type type) { var krt = new KeYRustyType(f); type2KRTCache.put(type, krt); return krt; + } else if (type instanceof GhostType g) { + var krt = new KeYRustyType(g, g.getSort(services)); + type2KRTCache.put(type, krt); + return krt; } else { throw new IllegalArgumentException("Unsupported type: " + type); } diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/ast/ConstDef.java b/keyext.rusty/src/main/java/org/key_project/rusty/ast/ConstDef.java new file mode 100644 index 00000000000..d960edffb25 --- /dev/null +++ b/keyext.rusty/src/main/java/org/key_project/rusty/ast/ConstDef.java @@ -0,0 +1,33 @@ +/* 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 org.key_project.rusty.ast; + +import org.key_project.logic.SyntaxElement; +import org.key_project.logic.op.Function; +import org.key_project.rusty.ast.expr.Expr; +import org.key_project.rusty.ast.ty.RustType; +import org.key_project.rusty.ast.visitor.Visitor; + +import org.jspecify.annotations.NonNull; + +public record ConstDef(String name, RustType rustType, Expr expr, Function fn) implements Item { + @Override + public void visit(Visitor v) { + v.performActionOnConstDef(this); + } + + @Override + public @NonNull SyntaxElement getChild(int n) { + if (n == 0) + return rustType; + if (n == 1) + return expr; + throw new IndexOutOfBoundsException(); + } + + @Override + public int getChildCount() { + return 2; + } +} diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/ast/EnumDef.java b/keyext.rusty/src/main/java/org/key_project/rusty/ast/EnumDef.java new file mode 100644 index 00000000000..67f4ca471a0 --- /dev/null +++ b/keyext.rusty/src/main/java/org/key_project/rusty/ast/EnumDef.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 org.key_project.rusty.ast; + +import org.key_project.logic.SyntaxElement; +import org.key_project.rusty.ast.visitor.Visitor; + +import org.jspecify.annotations.NonNull; + +public record EnumDef() implements Item { + @Override + public void visit(Visitor v) { + v.performActionOnEnumDef(this); + } + + @Override + public @NonNull SyntaxElement getChild(int n) { + throw new IndexOutOfBoundsException("No children"); + } + + @Override + public int getChildCount() { + return 0; + } +} diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/ast/HirConverter.java b/keyext.rusty/src/main/java/org/key_project/rusty/ast/HirConverter.java index 4ada049ed62..aed31bea609 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/ast/HirConverter.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/ast/HirConverter.java @@ -25,6 +25,7 @@ import org.key_project.rusty.ast.stmt.LetStatement; import org.key_project.rusty.ast.stmt.Statement; import org.key_project.rusty.ast.ty.*; +import org.key_project.rusty.logic.op.IProgramVariable; import org.key_project.rusty.logic.op.ParametricFunctionDecl; import org.key_project.rusty.logic.op.ProgramFunction; import org.key_project.rusty.logic.op.ProgramVariable; @@ -48,8 +49,6 @@ import org.key_project.rusty.speclang.FnSpecConverter; import org.key_project.rusty.speclang.LoopSpecConverter; import org.key_project.rusty.speclang.spec.FnSpec; -import org.key_project.rusty.speclang.spec.LoopSpec; -import org.key_project.rusty.speclang.spec.SpecMap; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; @@ -59,30 +58,15 @@ public class HirConverter { private final Services services; - private final @Nullable Map fnSpecs; - private final @Nullable Map loopSpecs; private final Map adts = new HashMap<>(); private final FnSpecConverter fnSpecConverter; private final LoopSpecConverter loopSpecConverter; private @Nullable GenericParam[] currentParams = null; - public HirConverter(Services services, @Nullable SpecMap specs) { + public HirConverter(Services services) { this.services = services; fnSpecConverter = new FnSpecConverter(services); loopSpecConverter = new LoopSpecConverter(services); - if (specs != null) { - fnSpecs = new HashMap<>(specs.fnSpecs().length); - loopSpecs = new HashMap<>(specs.loopSpecs().length); - for (var e : specs.fnSpecs()) { - fnSpecs.put(e.id(), e.value()); - } - for (var e : specs.loopSpecs()) { - loopSpecs.put(e.id(), e.value()); - } - } else { - fnSpecs = null; - loopSpecs = null; - } } public Services getServices() { @@ -132,8 +116,8 @@ public Crate convertCrate(org.key_project.rusty.parser.hir.Crate crate) { Crate crate1 = new Crate(convertMod(crate.topMod())); for (var fn : fnsToComplete.keySet()) { currentFn = fn; - var spec = fn2Spec.get(fn); var hirFn = fnsToComplete.get(fn); + var specCases = hirFn.specCases(); convertGenerics(hirFn.tyGenerics()); if (hirFn.generics() != null) { org.key_project.rusty.parser.hir.GenericParam[] params = hirFn.generics().params(); @@ -165,11 +149,10 @@ public Crate convertCrate(org.key_project.rusty.parser.hir.Crate crate) { fn.setParams(new ImmutableArray<>(params)); fn.setBody((BlockExpression) convertExpr(hirFn.body().value())); services.getRustInfo().registerFunction(fn); - if (spec != null) { + if (specCases.length > 0) { var contracts = - fnSpecConverter.convert(spec, - Objects.requireNonNull(services.getRustInfo().getFunction(fn), - "Could not get function for " + fn)); + fnSpecConverter.convert(specCases, + Objects.requireNonNull(services.getRustInfo().getFunction(fn))); for (var contract : contracts) { services.getSpecificationRepository().addContract(contract); } @@ -199,19 +182,35 @@ private Mod convertMod(org.key_project.rusty.parser.hir.Mod mod) { // above case org.key_project.rusty.parser.hir.item.Struct s -> null; // Handled by ADT // conversion above + case org.key_project.rusty.parser.hir.item.Const c -> convertConstDef(c); default -> throw new IllegalArgumentException("Unknown item: " + item); }; } + private Item convertConstDef(org.key_project.rusty.parser.hir.item.Const c) { + var rustTy = convertHirTy(c.ty()); + assert c.body().params().length == 0; + org.key_project.rusty.parser.hir.expr.Expr value = c.body().value(); + var expr = convertExpr(value); + // TODO: Get type in second step + var ty = convertTy(rawTypes.get(value.hirId())); + String name = c.ident().name(); + var fn = new RFunction(new Name(name), ty.getSort(services)); + return new ConstDef(name, rustTy, expr, fn); + } + private Item convertUse(org.key_project.rusty.parser.hir.item.Use use) { var path = convertPath(use.path(), rs -> { var lst = Arrays.stream(rs).map(this::convertRes).toList(); return new ImmutableArray<>(lst); }); var kind = switch (use.useKind()) { - case org.key_project.rusty.parser.hir.item.Use.UseKind.Single -> Use.UseKind.Single; - case org.key_project.rusty.parser.hir.item.Use.UseKind.Glob -> Use.UseKind.Glob; - case org.key_project.rusty.parser.hir.item.Use.UseKind.ListStem -> Use.UseKind.ListStem; + case org.key_project.rusty.parser.hir.item.Use.UseKind.Single ignored -> + Use.UseKind.Single; + case org.key_project.rusty.parser.hir.item.Use.UseKind.Glob ignored -> Use.UseKind.Glob; + case org.key_project.rusty.parser.hir.item.Use.UseKind.ListStem ignored -> + Use.UseKind.ListStem; + default -> throw new IllegalArgumentException("Unknown use kind: " + use); }; return new Use(path, kind); } @@ -223,11 +222,6 @@ private Function convertFn(Fn fn, LocalDefId id) { @SuppressWarnings("argument.type.incompatible") Function function = new Function(name, Function.ImplicitSelfKind.None, null, retTy, null); - if (fnSpecs != null) { - var spec = fnSpecs.get(new DefId(id.localDefIndex(), 0)); - if (spec != null) - fn2Spec.put(function, Objects.requireNonNull(spec, name.toString())); - } localFns.put(id, function); fnsToComplete.put(function, fn); return function; @@ -281,10 +275,18 @@ private Expr convertExpr(org.key_project.rusty.parser.hir.expr.Expr expr) { case ExprKind.Struct e -> convertStructExpr(e); case ExprKind.Repeat e -> convertRepeat(e, ty); // case ExprKind.Yield e -> convertYieldExpr(e); + case ExprKind.GhostBlockExpr e -> convertGhostBlockExpr(e); + case ExprKind.Snapshot e -> convertSnapshotExpr(e); default -> throw new IllegalArgumentException("Unknown expression: " + expr); }; } + private SnapshotExpression convertSnapshotExpr(ExprKind.Snapshot e) { + var body = e.expr(); + IProgramVariable pv = (IProgramVariable) convertExpr(body); + return new SnapshotExpression(pv); + } + private ConstBlockExpression convertConstBlockExpr(ExprKind.ConstBlock e) { var body = (BlockExpression) convertExpr(e.block().body().value()); return new ConstBlockExpression(body); @@ -409,6 +411,12 @@ private BlockExpression convertBlockExpr(ExprKind.BlockExpr expr) { return new BlockExpression(ImmutableList.fromList(stmts), value); } + private GhostBlockExpression convertGhostBlockExpr(ExprKind.GhostBlockExpr expr) { + var stmts = Arrays.stream(expr.block().stmts()).map(this::convertStmt).toList(); + var value = expr.block().expr() == null ? null : convertExpr(expr.block().expr()); + return new GhostBlockExpression(ImmutableList.fromList(stmts), value); + } + private LiteralExpression convertLitExpr(Lit expr, Type type) { return switch (expr.node()) { case LitKind.Bool(var v) -> new BooleanLiteralExpression(v); @@ -453,9 +461,8 @@ private LoopExpression convertLoopExpr(ExprKind.Loop l, HirId id, Type type) { var body = convertBlockExpr(new ExprKind.BlockExpr(l.block())); var le = new InfiniteLoopExpression(null, body); - if (loopSpecs != null && loopSpecs.containsKey(id)) { - var ls = loopSpecConverter.convert(loopSpecs.get(id), - Objects.requireNonNull(currentFn, "Missing local fn"), + if (l.spec() != null) { + var ls = loopSpecConverter.convert(l.spec(), Objects.requireNonNull(currentFn), le, pvs); services.getSpecificationRepository().addLoopSpec(ls); } @@ -882,6 +889,9 @@ private Adt getAdt(AdtDef def) { Adt adt = switch (def.kind()) { case Struct -> { assert def.variants().size() == 1; + if (def.pathStr().equals("rml_contracts::Ghost")) { + yield new GenericGhostType(generics, services); + } if (generics.isEmpty()) { var fields = convertFields(def.pathStr(), def.variants().get(0).fields()); yield new Struct(name, fields, null, null); @@ -990,6 +1000,7 @@ private Type convertAdtTy(AdtDef def, GenericTyArgKind[] args) { case Enum e -> e; case GenericStruct g -> g.instantiate(convertGenericArgs(args), services); case Struct s -> s; + case GenericGhostType g -> g.instantiate(convertGenericArgs(args), services); default -> throw new IllegalArgumentException("Unknown adt: " + adt); }; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/ast/HirRustyReader.java b/keyext.rusty/src/main/java/org/key_project/rusty/ast/HirRustyReader.java index 67331a47a47..8f768599fbf 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/ast/HirRustyReader.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/ast/HirRustyReader.java @@ -91,8 +91,8 @@ public RustyBlock readBlock(String block, Context context) { var wrapperOutput = getWrapperOutput(tmpDir); var beforeConversion = System.nanoTime(); - var converter = new HirConverter(services, null); - var converted = converter.convertCrate(wrapperOutput.crate()); + var converter = new HirConverter(services); + var converted = converter.convertCrate(wrapperOutput); LOGGER.debug("HIR conversion took {}", PerfScope.formatTime(System.nanoTime() - beforeConversion)); BlockExpression body = converted.getVerificationTarget().body(); @@ -144,11 +144,11 @@ public RustyBlock readBlock(String block, Context context) { } } - public static Crate.WrapperOutput getWrapperOutput(Path path) throws IOException { + public static Crate getWrapperOutput(Path path) throws IOException { return getWrapperOutput(path, false); } - public static Crate.WrapperOutput getWrapperOutput(Path path, boolean clean) + public static Crate getWrapperOutput(Path path, boolean clean) throws IOException { var startTime = System.nanoTime(); long rustCEnd; @@ -156,7 +156,7 @@ public static Crate.WrapperOutput getWrapperOutput(Path path, boolean clean) Process cleanCmd = Runtime.getRuntime().exec(new String[] { "cargo", "clean" }, null, path.toFile()); cleanCmd.waitFor(); - var command = new String[] { "cargo", "key", "-o", "hir.json" }; + var command = new String[] { "cargo", "rml", "-o", "hir.json" }; Process cmd = Runtime.getRuntime().exec(command, null, path.toFile()); var stdErr = cmd.getErrorStream(); var errReader = new BufferedReader(new InputStreamReader(stdErr)); @@ -176,7 +176,7 @@ public static Crate.WrapperOutput getWrapperOutput(Path path, boolean clean) LOGGER.debug("rustc took {}", PerfScope.formatTime(rustCEnd - startTime)); } var hir = Files.readString(path.resolve("hir.json"), Charset.defaultCharset()); - Crate.WrapperOutput output = Crate.parseJSON(hir); + Crate output = Crate.parseJSON(hir); LOGGER.debug("JSON parsing took {}", PerfScope.formatTime(System.nanoTime() - rustCEnd)); return output; } diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/ast/SchemaConverter.java b/keyext.rusty/src/main/java/org/key_project/rusty/ast/SchemaConverter.java index d8826595efc..f2f9ac4dfe7 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/ast/SchemaConverter.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/ast/SchemaConverter.java @@ -229,8 +229,18 @@ else if (ctx instanceof RustySchemaParser.StructExpression_Context x) { (ProgramSV) lookupSchemaVariable(cb.schemaVariable().getText().substring(2)); return new ConstBlockExpression(sv); } + if (ctx instanceof RustySchemaParser.GhostBlockExpressionContext gh) { + var block = convertBlockExpr(gh.blockExpr()); + return new GhostBlockExpression(block.getStatements(), block.getValue()); + } + if (ctx instanceof RustySchemaParser.SnapshotExpressionContext se) { + var sv = + (ProgramSV) lookupSchemaVariable(se.schemaVariable().getText().substring(2)); + return new SnapshotExpression(sv); + } throw new UnsupportedOperationException( "Unknown expr: " + ctx.getText() + " class: " + ctx.getClass()); + } private Expr convertLiteralExpr( diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/ast/StructDef.java b/keyext.rusty/src/main/java/org/key_project/rusty/ast/StructDef.java new file mode 100644 index 00000000000..5a51cf5dc47 --- /dev/null +++ b/keyext.rusty/src/main/java/org/key_project/rusty/ast/StructDef.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 org.key_project.rusty.ast; + +import org.key_project.logic.SyntaxElement; +import org.key_project.rusty.ast.visitor.Visitor; + +import org.jspecify.annotations.NonNull; + +public record StructDef() implements Item { + @Override + public void visit(Visitor v) { + v.performActionOnStructDef(this); + } + + @Override + public @NonNull SyntaxElement getChild(int n) { + throw new IndexOutOfBoundsException("No children"); + } + + @Override + public int getChildCount() { + return 0; + } +} diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/ast/abstraction/GenericGhostType.java b/keyext.rusty/src/main/java/org/key_project/rusty/ast/abstraction/GenericGhostType.java new file mode 100644 index 00000000000..be06cbe8d0a --- /dev/null +++ b/keyext.rusty/src/main/java/org/key_project/rusty/ast/abstraction/GenericGhostType.java @@ -0,0 +1,43 @@ +/* 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 org.key_project.rusty.ast.abstraction; + +import org.key_project.logic.Name; +import org.key_project.rusty.Services; +import org.key_project.rusty.logic.sort.ParametricSortDecl; +import org.key_project.util.collection.ImmutableArray; + +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + +public class GenericGhostType implements GenericAdt { + private final ParametricSortDecl ghostSort; + private final ImmutableArray params; + private final Name name = new Name("rml_contracts::Ghost"); + + public GenericGhostType(ImmutableArray params, Services services) { + ghostSort = services.getLDTs().getGhostLDT().parametricSort(); + this.params = params; + } + + @Override + public @Nullable ParametricSortDecl sortDecl() { + return ghostSort; + } + + @Override + public Type instantiate(ImmutableArray args, Services services) { + return GhostType.get(((GenericTyArgType) args.get(0)).type()); + } + + @Override + public ImmutableArray params() { + return params; + } + + @Override + public @NonNull Name name() { + return name; + } +} diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/ast/abstraction/GhostType.java b/keyext.rusty/src/main/java/org/key_project/rusty/ast/abstraction/GhostType.java new file mode 100644 index 00000000000..71c46b8b391 --- /dev/null +++ b/keyext.rusty/src/main/java/org/key_project/rusty/ast/abstraction/GhostType.java @@ -0,0 +1,68 @@ +/* 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 org.key_project.rusty.ast.abstraction; + +import java.util.HashMap; +import java.util.Map; + +import org.key_project.logic.Name; +import org.key_project.logic.sort.Sort; +import org.key_project.rusty.Services; +import org.key_project.rusty.ast.ty.GhostRustType; +import org.key_project.rusty.ast.ty.RustType; +import org.key_project.rusty.logic.sort.ParametricSortDecl; +import org.key_project.rusty.logic.sort.ParametricSortInstance; +import org.key_project.rusty.logic.sort.SortArg; +import org.key_project.util.collection.ImmutableList; + +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + +public class GhostType implements Type { + private final Type inner; + private final Name name; + + static final Map cache = new HashMap<>(); + + public static GhostType get(Type inner) { + return cache.computeIfAbsent(inner, i -> new GhostType(inner)); + } + + private GhostType(Type inner) { + this.inner = inner; + name = new Name("Ghost<" + inner.toString() + ">"); + } + + @Override + public @Nullable Sort getSort(Services services) { + Sort inner = this.inner.getSort(services); + ParametricSortDecl pSort = services.getLDTs().getGhostLDT().parametricSort(); + assert pSort != null; + return ParametricSortInstance.get(pSort, ImmutableList.of(new SortArg(inner))); + } + + + @Override + public RustType toRustType(Services services) { + return new GhostRustType(inner.toRustType(services)); + } + + @Override + public Type instantiate(Map instMap, Services services) { + var it = inner.instantiate(instMap, services); + if (it == inner) + return this; + return get(it); + + } + + @Override + public @NonNull Name name() { + return name; + } + + private Type inner() { + return inner; + } +} diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/ast/expr/AbstractBlockExpression.java b/keyext.rusty/src/main/java/org/key_project/rusty/ast/expr/AbstractBlockExpression.java new file mode 100644 index 00000000000..87f497c04bb --- /dev/null +++ b/keyext.rusty/src/main/java/org/key_project/rusty/ast/expr/AbstractBlockExpression.java @@ -0,0 +1,160 @@ +/* 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 org.key_project.rusty.ast.expr; + +import java.util.ArrayList; +import java.util.Objects; + +import org.key_project.logic.SyntaxElement; +import org.key_project.rusty.Services; +import org.key_project.rusty.ast.ElseBranch; +import org.key_project.rusty.ast.ProgramPrefixUtil; +import org.key_project.rusty.ast.abstraction.TupleType; +import org.key_project.rusty.ast.abstraction.Type; +import org.key_project.rusty.ast.stmt.Statement; +import org.key_project.rusty.logic.PosInProgram; +import org.key_project.rusty.logic.PossibleProgramPrefix; +import org.key_project.util.ExtList; +import org.key_project.util.collection.ImmutableArray; +import org.key_project.util.collection.ImmutableList; + +import org.checkerframework.checker.initialization.qual.UnknownInitialization; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + +public abstract class AbstractBlockExpression + implements Expr, PossibleProgramPrefix, ThenBranch, ElseBranch { + + protected final ImmutableList statements; + protected final @Nullable Expr value; + private final int prefixLength; + + private int hashCode = -1; + + protected AbstractBlockExpression(ImmutableList statements, @Nullable Expr value) { + this.statements = statements; + this.value = value; + ProgramPrefixUtil.ProgramPrefixInfo info = ProgramPrefixUtil.computeEssentials(this); + this.prefixLength = info.length(); + } + + protected AbstractBlockExpression(ExtList children) { + this.statements = ImmutableList.of(children.collect(Statement.class)); + this.value = children.get(Expr.class); + ProgramPrefixUtil.ProgramPrefixInfo info = ProgramPrefixUtil.computeEssentials(this); + this.prefixLength = info.length(); + } + + @Override + public @NonNull SyntaxElement getChild(@UnknownInitialization AbstractBlockExpression this, + int n) { + assert statements != null; + if (0 <= n && n < statements.size()) + return Objects.requireNonNull(statements.get(n)); + if (n == statements.size() && value != null) + return value; + throw new IndexOutOfBoundsException( + getClass().getSimpleName() + " has less than " + n + " children"); + } + + @Override + public int getChildCount(@UnknownInitialization AbstractBlockExpression this) { + assert statements != null; + return statements.size() + (value == null ? 0 : 1); + } + + public ImmutableList getStatements() { + return statements; + } + + public @Nullable Expr getValue() { + return value; + } + + @Override + public abstract void visit(org.key_project.rusty.ast.visitor.Visitor v); + + @Override + public boolean isPrefix(@UnknownInitialization AbstractBlockExpression this) { + return getChildCount() != 0; + } + + @Override + public boolean hasNextPrefixElement(@UnknownInitialization AbstractBlockExpression this) { + return getChildCount() != 0 && getChild(0) instanceof PossibleProgramPrefix; + } + + @Override + public PossibleProgramPrefix getNextPrefixElement( + @UnknownInitialization AbstractBlockExpression this) { + if (hasNextPrefixElement()) { + return (PossibleProgramPrefix) getChild(0); + } + throw new IndexOutOfBoundsException("No next prefix element " + this); + } + + @Override + public PossibleProgramPrefix getLastPrefixElement() { + return hasNextPrefixElement() ? getNextPrefixElement().getLastPrefixElement() : this; + } + + @Override + public ImmutableArray getPrefixElements() { + return computePrefixElements(this); + } + + @Override + public PosInProgram getFirstActiveChildPos() { + return PosInProgram.ZERO; + } + + @Override + public int getPrefixLength(@UnknownInitialization AbstractBlockExpression this) { + return prefixLength; + } + + public static ImmutableArray computePrefixElements( + PossibleProgramPrefix current) { + final ArrayList prefix = new ArrayList<>(); + prefix.add(current); + + while (current.hasNextPrefixElement()) { + current = current.getNextPrefixElement(); + prefix.add(current); + } + + return new ImmutableArray<>(prefix); + } + + @Override + public Type type(Services services) { + return value == null ? TupleType.UNIT : value.type(services); + } + + @Override + public int hashCode() { + if (hashCode != -1) { + return hashCode; + } + final int h = computeHashCode(); + this.hashCode = h; + return h; + } + + public int computeHashCode() { + return Objects.hash(getClass(), statements, value, prefixLength); + } + + @Override + public boolean equals(@Nullable Object o) { + if (o == this) + return true; + if (o == null || getClass() != o.getClass()) + return false; + AbstractBlockExpression that = (AbstractBlockExpression) o; + return this.prefixLength == that.prefixLength + && Objects.equals(this.statements, that.statements) + && Objects.equals(this.value, that.value); + } +} diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/ast/expr/BlockExpression.java b/keyext.rusty/src/main/java/org/key_project/rusty/ast/expr/BlockExpression.java index 47337956a70..bdca256bb22 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/ast/expr/BlockExpression.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/ast/expr/BlockExpression.java @@ -3,170 +3,43 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.rusty.ast.expr; -import java.util.ArrayList; -import java.util.Objects; - -import org.key_project.logic.SyntaxElement; -import org.key_project.rusty.Services; -import org.key_project.rusty.ast.ElseBranch; -import org.key_project.rusty.ast.ProgramPrefixUtil; -import org.key_project.rusty.ast.abstraction.TupleType; -import org.key_project.rusty.ast.abstraction.Type; -import org.key_project.rusty.ast.stmt.Statement; import org.key_project.rusty.ast.visitor.Visitor; -import org.key_project.rusty.logic.PosInProgram; -import org.key_project.rusty.logic.PossibleProgramPrefix; import org.key_project.util.ExtList; -import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; -import org.checkerframework.checker.initialization.qual.UnknownInitialization; -import org.jspecify.annotations.NonNull; import org.jspecify.annotations.Nullable; -public class BlockExpression implements Expr, PossibleProgramPrefix, ThenBranch, ElseBranch { - protected final ImmutableList statements; - protected final @Nullable Expr value; - private final int prefixLength; - - private int hashCode = -1; +public class BlockExpression extends AbstractBlockExpression { - public BlockExpression(ImmutableList statements, @Nullable Expr value) { - this.statements = statements; - this.value = value; - ProgramPrefixUtil.ProgramPrefixInfo info = ProgramPrefixUtil.computeEssentials(this); - prefixLength = info.length(); + public BlockExpression(ImmutableList statements, + @Nullable Expr value) { + super(statements, value); } public BlockExpression(ExtList children) { - statements = ImmutableList.of(children.collect(Statement.class)); - value = children.get(Expr.class); - ProgramPrefixUtil.ProgramPrefixInfo info = ProgramPrefixUtil.computeEssentials(this); - prefixLength = info.length(); + super(children); } @Override - public @NonNull SyntaxElement getChild(@UnknownInitialization BlockExpression this, int n) { - assert statements != null; - if (0 <= n && n < statements.size()) - return Objects.requireNonNull(statements.get(n)); - if (n == statements.size() && value != null) - return value; - throw new IndexOutOfBoundsException("BlockExpression has less than " + n + " children"); - } - - @Override - public int getChildCount(@UnknownInitialization BlockExpression this) { - assert statements != null; - return statements.size() + (value == null ? 0 : 1); - } - - public ImmutableList getStatements() { - return statements; - } - - public @Nullable Expr getValue() { - return value; + public void visit(Visitor v) { + v.performActionOnBlockExpression(this); } @Override public String toString() { var sb = new StringBuilder(); sb.append("{\n"); - for (var s : statements) { + for (var s : getStatements()) { sb.append("\t"); sb.append(s.toString()); sb.append("\n"); } - if (value != null) { + if (getValue() != null) { sb.append("\t"); - sb.append(value); + sb.append(getValue()); sb.append("\n"); } sb.append("}"); return sb.toString(); } - - @Override - public void visit(Visitor v) { - v.performActionOnBlockExpression(this); - } - - @Override - public boolean isPrefix(@UnknownInitialization BlockExpression this) { - return getChildCount() != 0; - } - - @Override - public boolean hasNextPrefixElement(@UnknownInitialization BlockExpression this) { - return getChildCount() != 0 && getChild(0) instanceof PossibleProgramPrefix; - } - - @Override - public PossibleProgramPrefix getNextPrefixElement(@UnknownInitialization BlockExpression this) { - if (hasNextPrefixElement()) { - return (PossibleProgramPrefix) getChild(0); - } - throw new IndexOutOfBoundsException("No next prefix element " + this); - } - - @Override - public PossibleProgramPrefix getLastPrefixElement() { - return hasNextPrefixElement() ? getNextPrefixElement().getLastPrefixElement() : this; - } - - @Override - public ImmutableArray getPrefixElements() { - return computePrefixElements(this); - } - - @Override - public PosInProgram getFirstActiveChildPos() { - return PosInProgram.ZERO; - } - - @Override - public int getPrefixLength(@UnknownInitialization BlockExpression this) { - return prefixLength; - } - - /// computes the prefix elements for the given array of statment block - public static ImmutableArray computePrefixElements( - PossibleProgramPrefix current) { - final ArrayList prefix = new ArrayList<>(); - prefix.add(current); - - while (current.hasNextPrefixElement()) { - current = current.getNextPrefixElement(); - prefix.add(current); - } - - return new ImmutableArray<>(prefix); - } - - @Override - public Type type(Services services) { - return value == null ? TupleType.UNIT : value.type(services); - } - - @Override - public int hashCode() { - if (hashCode == -1) { - return hashCode; - } - final int hash = computeHashCode(); - this.hashCode = hash; - return hash; - } - - @Override - public boolean equals(@Nullable Object o) { - if (o == this) - return true; - if (o == null || getClass() != o.getClass()) - return false; - BlockExpression that = (BlockExpression) o; - return prefixLength == that.prefixLength && Objects.equals(statements, that.statements) - && Objects.equals(value, that.value); - } } diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/ast/expr/GhostBlockExpression.java b/keyext.rusty/src/main/java/org/key_project/rusty/ast/expr/GhostBlockExpression.java new file mode 100644 index 00000000000..52054465fa8 --- /dev/null +++ b/keyext.rusty/src/main/java/org/key_project/rusty/ast/expr/GhostBlockExpression.java @@ -0,0 +1,45 @@ +/* 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 org.key_project.rusty.ast.expr; + +import org.key_project.rusty.ast.visitor.Visitor; +import org.key_project.util.ExtList; +import org.key_project.util.collection.ImmutableList; + +import org.jspecify.annotations.Nullable; + +public class GhostBlockExpression extends AbstractBlockExpression { + + public GhostBlockExpression(ImmutableList statements, + @Nullable Expr value) { + super(statements, value); + } + + public GhostBlockExpression(ExtList children) { + super(children); + } + + @Override + public void visit(Visitor v) { + v.performActionOnGhostBlockExpression(this); + } + + @Override + public String toString() { + StringBuilder sb = new StringBuilder(); + sb.append("ghost! {"); + for (int i = 0; i < getStatements().size(); i++) { + if (i > 0) + sb.append("; "); + sb.append(getStatements().get(i)); + } + if (getValue() != null) { + if (!getStatements().isEmpty()) + sb.append("; "); + sb.append(getValue()); + } + sb.append("}"); + return sb.toString(); + } +} diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/ast/expr/SnapshotExpression.java b/keyext.rusty/src/main/java/org/key_project/rusty/ast/expr/SnapshotExpression.java new file mode 100644 index 00000000000..3b42fa3126d --- /dev/null +++ b/keyext.rusty/src/main/java/org/key_project/rusty/ast/expr/SnapshotExpression.java @@ -0,0 +1,62 @@ +/* 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 org.key_project.rusty.ast.expr; + + +import org.key_project.logic.SyntaxElement; +import org.key_project.rusty.Services; +import org.key_project.rusty.ast.abstraction.Type; +import org.key_project.rusty.ast.visitor.Visitor; +import org.key_project.rusty.logic.op.IProgramVariable; +import org.key_project.util.ExtList; + +public class SnapshotExpression implements Expr { + + private final IProgramVariable pv; + + public SnapshotExpression(IProgramVariable pv) { + this.pv = pv; + } + + public SnapshotExpression(ExtList children) { + pv = children.get(IProgramVariable.class); + } + + + @Override + public void visit(Visitor v) { + v.performActionOnSnapshotExpression(this); + } + + @Override + public String toString() { + StringBuilder sb = new StringBuilder(); + sb.append("snapshot! ("); + sb.append(pv); + sb.append(")"); + return sb.toString(); + } + + @Override + public Type type(Services services) { + return pv.type(services); + } + + @Override + public SyntaxElement getChild(int n) { + if (n == 0) + return pv; + throw new IndexOutOfBoundsException(); + } + + @Override + public int getChildCount() { + return 1; + } + + + public IProgramVariable getPv() { + return pv; + } +} diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/ast/ty/GhostRustType.java b/keyext.rusty/src/main/java/org/key_project/rusty/ast/ty/GhostRustType.java new file mode 100644 index 00000000000..96d070c5106 --- /dev/null +++ b/keyext.rusty/src/main/java/org/key_project/rusty/ast/ty/GhostRustType.java @@ -0,0 +1,35 @@ +/* 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 org.key_project.rusty.ast.ty; + +import org.key_project.logic.SyntaxElement; +import org.key_project.rusty.ast.abstraction.GhostType; +import org.key_project.rusty.ast.abstraction.Type; +import org.key_project.rusty.ast.visitor.Visitor; + +import org.jspecify.annotations.NonNull; + +public record GhostRustType(RustType inner) implements RustType { + @Override + public Type type() { + return GhostType.get(inner.type()); + } + + @Override + public void visit(Visitor v) { + v.performActionOnGhostRustType(this); + } + + @Override + public @NonNull SyntaxElement getChild(int n) { + if (n == 0) + return inner; + throw new IndexOutOfBoundsException("GhostRustType has only one child"); + } + + @Override + public int getChildCount() { + return 1; + } +} diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/ast/visitor/CreatingASTVisitor.java b/keyext.rusty/src/main/java/org/key_project/rusty/ast/visitor/CreatingASTVisitor.java index 6dab054da08..5b065eba986 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/ast/visitor/CreatingASTVisitor.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/ast/visitor/CreatingASTVisitor.java @@ -92,6 +92,22 @@ public void performActionOnBlockExpression(BlockExpression x) { } } + @Override + public void performActionOnGhostBlockExpression(GhostBlockExpression x) { + ExtList changeList = getTop(); + if (!changeList.isEmpty() && changeList.getFirst() == CHANGED) { + changeList.removeFirst(); + if (!preservesPositionInfo) { + // TODO changeList.removeFirstOccurrence(PositionInfo.class); + } + var newBlock = new GhostBlockExpression(changeList); + addChild(newBlock); + changed(); + } else { + doDefaultAction(x); + } + } + @Override public void performActionOnContextBlockExpression(ContextBlockExpression x) { ExtList changeList = getTop(); @@ -122,11 +138,16 @@ public void performActionOnIntegerLiteralExpression(IntegerLiteralExpression x) doDefaultAction(x); } + @Override + public void performActionOnSnapshotExpression(SnapshotExpression x) { doDefaultAction(x); } + + @Override public void performActionOnProgramVariable(ProgramVariable x) { throw new RuntimeException("TODO @ DD"); } + @Override public void performActionOnSchemaVariable(SchemaVariable x) { throw new RuntimeException("TODO @ DD"); diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/ast/visitor/ProgramContextAdder.java b/keyext.rusty/src/main/java/org/key_project/rusty/ast/visitor/ProgramContextAdder.java index 919e1b32c3e..dfce687dbe8 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/ast/visitor/ProgramContextAdder.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/ast/visitor/ProgramContextAdder.java @@ -58,6 +58,7 @@ protected RustyProgramElement wrap(@Nullable RustyProgramElement context, case FunctionFrame ff -> createFunctionFrameWrapper(ff, (BlockExpression) body); case LoopScope ls -> createLoopScopeWrapper(ls, (BlockExpression) body); case PanicFrame pf -> createPanicFrameWrapper(pf, (BlockExpression) body); + case GhostBlockExpression ge -> createGhostBlockExprWrapper(ge, body); case null, default -> throw new RuntimeException( new UnexpectedException( "Unexpected block type: " + (context != null ? context.getClass() : null))); @@ -143,6 +144,10 @@ private RustyProgramElement createWrapperBody(@Nullable RustyProgramElement wrap } else if (wrapper instanceof ExpressionStatement es) { assert putIn.getStatements().isEmpty() : putIn.toString(); return new ExpressionStatement(Objects.requireNonNull(putIn.getValue()), es.hasSemi()); + } else if (wrapper instanceof GhostBlockExpression gb) { + var be = new BlockExpression(gb.getStatements(), gb.getValue()); + be = (BlockExpression) createWrapperBody(be, putIn, suffix); + return new GhostBlockExpression(be.getStatements(), be.getValue()); } else { throw new RuntimeException("Unexpected context : " + wrapper); } @@ -174,6 +179,20 @@ private LoopScope createLoopScopeWrapper(LoopScope old, BlockExpression body) { return new LoopScope(old.getIndex(), old.getReturnVar(), body); } + private RustyProgramElement createGhostBlockExprWrapper(GhostBlockExpression wrapper, + RustyProgramElement replacement) { + int childCount = wrapper.getChildCount(); + if (childCount <= 1) { + if (replacement instanceof GhostBlockExpression ge) + return ge; + if (replacement instanceof Expr e) + return new GhostBlockExpression(ImmutableSLList.nil(), e); + } + var body = wrapper.getStatements().tail(); + body = body.prepend(wrapExprIfNecessary(replacement)); + return new GhostBlockExpression(body, wrapper.getValue()); + } + private PanicFrame createPanicFrameWrapper(PanicFrame wrapper, BlockExpression replacement) { return new PanicFrame(wrapper.getPanicVar(), replacement); diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/ast/visitor/RustyASTVisitor.java b/keyext.rusty/src/main/java/org/key_project/rusty/ast/visitor/RustyASTVisitor.java index 13891767d85..6390bf46920 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/ast/visitor/RustyASTVisitor.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/ast/visitor/RustyASTVisitor.java @@ -65,6 +65,12 @@ public void performActionOnBlockExpression(BlockExpression x) { doDefaultAction(x); } + @Override + public void performActionOnGhostBlockExpression(GhostBlockExpression x) { + doDefaultAction(x); + } + + @Override public void performActionOnBooleanLiteralExpression(BooleanLiteralExpression x) { doDefaultAction(x); @@ -414,4 +420,26 @@ public void performActionOnPathRustType(PathRustType x) { public void performActionOnPanicFrame(PanicFrame x) { doDefaultAction(x); } + + @Override + public void performActionOnGhostRustType(GhostRustType x) { + doDefaultAction(x); + } + + public void performActionOnSnapshotExpression(SnapshotExpression x) { doDefaultAction(x); } + + @Override + public void performActionOnStructDef(StructDef x) { + doDefaultAction(x); + } + + @Override + public void performActionOnEnumDef(EnumDef x) { + doDefaultAction(x); + } + + @Override + public void performActionOnConstDef(ConstDef x) { + doDefaultAction(x); + } } diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/ast/visitor/Visitor.java b/keyext.rusty/src/main/java/org/key_project/rusty/ast/visitor/Visitor.java index 239dee1499b..a68cc3e3a15 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/ast/visitor/Visitor.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/ast/visitor/Visitor.java @@ -147,6 +147,10 @@ public interface Visitor { void performActionOnTupleRustType(TupleRustType x); + void performActionOnGhostBlockExpression(GhostBlockExpression x); + + void performActionOnSnapshotExpression(SnapshotExpression x); + void performActionOnPathExpr(PathExpr x); void performActionOnPath(Path x); @@ -162,4 +166,12 @@ public interface Visitor { void performActionOnPathRustType(PathRustType x); void performActionOnPanicFrame(PanicFrame x); + + void performActionOnGhostRustType(GhostRustType x); + + void performActionOnStructDef(StructDef x); + + void performActionOnEnumDef(EnumDef x); + + void performActionOnConstDef(ConstDef x); } diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/ldt/GhostLDT.java b/keyext.rusty/src/main/java/org/key_project/rusty/ldt/GhostLDT.java new file mode 100644 index 00000000000..5e47bdc79e9 --- /dev/null +++ b/keyext.rusty/src/main/java/org/key_project/rusty/ldt/GhostLDT.java @@ -0,0 +1,68 @@ +/* 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 org.key_project.rusty.ldt; + +import org.key_project.logic.Name; +import org.key_project.logic.Term; +import org.key_project.logic.op.Function; +import org.key_project.rusty.Services; +import org.key_project.rusty.ast.expr.BinaryExpression; +import org.key_project.rusty.ast.expr.LiteralExpression; +import org.key_project.rusty.logic.op.ParametricFunctionDecl; + +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + +public class GhostLDT extends LDT { + public static final Name NAME = new Name("Ghost"); + + private final ParametricFunctionDecl ghost; + private final ParametricFunctionDecl unwrap; + + public GhostLDT(Services services) { + super(NAME, services); + + ghost = addParametricFunction(services, "ghost"); + unwrap = addParametricFunction(services, "unwrap_ghost"); + } + + public ParametricFunctionDecl getGhost() { + return ghost; + } + + public ParametricFunctionDecl getUnwrap() { + return unwrap; + } + + @Override + public @Nullable Term translateLiteral(LiteralExpression lit, Services services) { + return null; + } + + @Override + public @Nullable Function getFunctionFor(BinaryExpression.Operator op, Services services) { + return null; + } + + @Override + public boolean isResponsible(BinaryExpression.Operator op, Term[] subs, Services services) { + return false; + } + + @Override + public boolean isResponsible(BinaryExpression.Operator op, Term sub, Services services) { + return false; + } + + @Override + public boolean isResponsible(BinaryExpression.Operator op, Term left, Term right, + Services services) { + return false; + } + + @Override + public @NonNull Name name() { + return NAME; + } +} diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/ldt/LDTs.java b/keyext.rusty/src/main/java/org/key_project/rusty/ldt/LDTs.java index 86972ff88e4..5e9e6e35539 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/ldt/LDTs.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/ldt/LDTs.java @@ -25,6 +25,7 @@ public class LDTs implements Iterable { private final TupleLDT tupleLDT; private final SRefLDT sRefLDT; private final MRefLDT mRefLDT; + private final GhostLDT ghostLDT; private final Map map; public LDTs(Services services) { @@ -38,6 +39,7 @@ public LDTs(Services services) { tupleLDT = new TupleLDT(services); sRefLDT = new SRefLDT(services); mRefLDT = new MRefLDT(services); + ghostLDT = new GhostLDT(services); map = new HashMap<>(); map.put(boolLDT.name(), boolLDT); map.put(intLDT.name(), intLDT); @@ -49,6 +51,7 @@ public LDTs(Services services) { map.put(tupleLDT.name(), tupleLDT); map.put(sRefLDT.name(), sRefLDT); map.put(mRefLDT.name(), mRefLDT); + map.put(ghostLDT.name(), ghostLDT); } public BoolLDT getBoolLDT() { @@ -91,6 +94,10 @@ public MRefLDT getmRefLDT() { return mRefLDT; } + public GhostLDT getGhostLDT() { + return ghostLDT; + } + public @Nullable LDT get(Name name) { return map.get(name); } diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/logic/op/IProgramVariable.java b/keyext.rusty/src/main/java/org/key_project/rusty/logic/op/IProgramVariable.java index 8e4b7750f56..099cb812586 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/logic/op/IProgramVariable.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/logic/op/IProgramVariable.java @@ -5,6 +5,7 @@ import org.key_project.logic.op.SortedOperator; import org.key_project.rusty.ast.RustyProgramElement; +import org.key_project.rusty.ast.expr.Expr; -public interface IProgramVariable extends RustyProgramElement, SortedOperator { +public interface IProgramVariable extends RustyProgramElement, SortedOperator, Expr { } diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/Crate.java b/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/Crate.java index 9f0af9decad..93b9addd43f 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/Crate.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/Crate.java @@ -8,6 +8,7 @@ import org.key_project.rusty.parser.hir.hirty.PrimHirTy; import org.key_project.rusty.parser.hir.item.FnRetTy; import org.key_project.rusty.parser.hir.item.ItemKind; +import org.key_project.rusty.parser.hir.item.Use; import org.key_project.rusty.parser.hir.item.VariantData; import org.key_project.rusty.parser.hir.pat.ByRef; import org.key_project.rusty.parser.hir.pat.PatExprKind; @@ -15,7 +16,6 @@ import org.key_project.rusty.parser.hir.stmt.LocalSource; import org.key_project.rusty.parser.hir.stmt.StmtKind; import org.key_project.rusty.parser.hir.ty.*; -import org.key_project.rusty.speclang.spec.SpecMap; import org.key_project.rusty.speclang.spec.TermKind; import org.key_project.rusty.speclang.spec.TermStmtKind; @@ -23,10 +23,7 @@ import com.google.gson.GsonBuilder; public record Crate(Mod topMod, HirTyMapping[] types, DefIdAdtMapping[] adts) { - public record WrapperOutput(Crate crate, SpecMap specs) { - } - - public static WrapperOutput parseJSON(String json) { + public static Crate parseJSON(String json) { var gson = new GsonBuilder().setFieldNamingPolicy(FieldNamingPolicy.LOWER_CASE_WITH_UNDERSCORES) .registerTypeAdapter(ItemKind.class, new ItemKind.Adapter()) @@ -59,6 +56,7 @@ public static WrapperOutput parseJSON(String json) { .registerTypeAdapter(TyGenericParamDefKind.class, new TyGenericParamDefKind.Adapter()) .registerTypeAdapter(GenericArg.class, new GenericArg.Adapter()) + .registerTypeAdapter(Use.UseKind.class, new Use.UseKind.Adapter()) .registerTypeAdapter(ConstExprKind.class, new ConstExprKind.Adapter()) .registerTypeAdapter(TermStmtKind.class, new TermStmtKind.Adapter()) .registerTypeAdapter(ParamName.class, new ParamName.Adapter()) @@ -66,6 +64,6 @@ public static WrapperOutput parseJSON(String json) { .registerTypeAdapter(LifetimeParamKind.class, new LifetimeParamKind.Adapter()) .registerTypeAdapter(VariantData.class, new VariantData.Adapter()) .create(); - return gson.fromJson(json, WrapperOutput.class); + return gson.fromJson(json, Crate.class); } } diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/expr/ExprKind.java b/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/expr/ExprKind.java index 55a966d0651..0d445658f3a 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/expr/ExprKind.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/expr/ExprKind.java @@ -5,6 +5,7 @@ import org.key_project.rusty.parser.hir.*; import org.key_project.rusty.parser.hir.hirty.HirTy; +import org.key_project.rusty.speclang.spec.LoopSpec; import org.jspecify.annotations.Nullable; @@ -46,7 +47,8 @@ record Let(LetExpr let) implements ExprKind { record If(Expr cond, Expr then, @Nullable Expr els) implements ExprKind { } - record Loop(Block block, @Nullable Label label, Span span) implements ExprKind { + record Loop(Block block, @Nullable Label label, Span span, @Nullable LoopSpec spec) + implements ExprKind { } record Match(Expr expr, Arm[] arms, MatchSource src) implements ExprKind { @@ -58,6 +60,14 @@ record Closure(ClosureExpr closure) implements ExprKind { record BlockExpr(Block block) implements ExprKind { } + record GhostBlockExpr(Block block) implements ExprKind { + + } + + record Snapshot(Expr expr) implements ExprKind { + + } + record Assign(Expr left, Expr right, Span span) implements ExprKind { } @@ -114,6 +124,8 @@ class Adapter extends HirAdapter { case "Match" -> Match.class; case "Closure" -> Closure.class; case "Block" -> BlockExpr.class; + case "GhostBlock" -> GhostBlockExpr.class; + case "Snapshot" -> Snapshot.class; case "Assign" -> Assign.class; case "AssignOp" -> AssignOp.class; case "Field" -> Field.class; diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/item/Const.java b/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/item/Const.java index e1e51e39ed9..3a25be4ff3e 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/item/Const.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/item/Const.java @@ -3,7 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.rusty.parser.hir.item; +import org.key_project.rusty.parser.hir.Ident; import org.key_project.rusty.parser.hir.hirty.HirTy; -public record Const(HirTy ty, Body body) implements ItemKind { +public record Const(Ident ident, HirTy ty, Body body) implements ItemKind { } diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/item/Fn.java b/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/item/Fn.java index 058facd6fe9..72f0a68f18d 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/item/Fn.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/item/Fn.java @@ -5,7 +5,8 @@ import org.key_project.rusty.parser.hir.Ident; import org.key_project.rusty.parser.hir.ty.TyGenerics; +import org.key_project.rusty.speclang.spec.SpecCase; -public record Fn(Ident ident, FnSig sig, Generics generics, Body body, TyGenerics tyGenerics) - implements ItemKind { +public record Fn(Ident ident, FnSig sig, Generics generics, Body body, SpecCase[] specCases, + TyGenerics tyGenerics) implements ItemKind { } diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/item/FnRetTy.java b/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/item/FnRetTy.java index b89fbfb6e2a..b4e6ba6f2c3 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/item/FnRetTy.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/item/FnRetTy.java @@ -3,15 +3,13 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.rusty.parser.hir.item; -import java.lang.reflect.Type; +import org.key_project.rusty.parser.hir.HirAdapter; import org.key_project.rusty.parser.hir.Span; import org.key_project.rusty.parser.hir.hirty.HirTy; -import com.google.gson.JsonDeserializationContext; -import com.google.gson.JsonDeserializer; -import com.google.gson.JsonElement; -import com.google.gson.JsonParseException; +import org.jspecify.annotations.Nullable; + public interface FnRetTy { record Return(HirTy ty) implements FnRetTy { @@ -20,17 +18,14 @@ record Return(HirTy ty) implements FnRetTy { record DefaultReturn(Span span) implements FnRetTy { } - class Adapter implements JsonDeserializer { + class Adapter extends HirAdapter { @Override - public FnRetTy deserialize(JsonElement jsonElement, Type type, - JsonDeserializationContext jsonDeserializationContext) throws JsonParseException { - var obj = jsonElement.getAsJsonObject(); - if (obj.has("Return")) { - return new Return( - jsonDeserializationContext.deserialize(obj.get("Return"), HirTy.class)); - } - return new DefaultReturn( - jsonDeserializationContext.deserialize(obj.get("DefaultReturn"), Span.class)); + public @Nullable Class getType(String tag) { + return switch (tag) { + case "Return" -> Return.class; + case "DefaultReturn" -> DefaultReturn.class; + default -> null; + }; } } } diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/item/ItemKind.java b/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/item/ItemKind.java index daf268f3d88..166eafa4824 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/item/ItemKind.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/item/ItemKind.java @@ -16,8 +16,8 @@ class Adapter extends HirAdapter { case "ExternCrate" -> ExternCrate.class; case "Fn" -> Fn.class; case "Const" -> Const.class; - case "Enum" -> Enum.class; case "Struct" -> Struct.class; + case "Enum" -> Enum.class; default -> null; }; } diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/item/Use.java b/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/item/Use.java index 4a29d194481..92aa3d07b56 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/item/Use.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/parser/hir/item/Use.java @@ -3,12 +3,33 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.rusty.parser.hir.item; +import org.key_project.rusty.parser.hir.HirAdapter; +import org.key_project.rusty.parser.hir.Ident; import org.key_project.rusty.parser.hir.Path; import org.key_project.rusty.parser.hir.Res; +import org.jspecify.annotations.Nullable; + public record Use(Path path, UseKind useKind) implements ItemKind { - public enum UseKind { - Single, Glob, ListStem + public interface UseKind { + record Single(Ident ident) implements UseKind { + } + record Glob() implements UseKind { + } + record ListStem() implements UseKind { + } + + class Adapter extends HirAdapter { + @Override + public @Nullable Class getType(String tag) { + return switch (tag) { + case "Single" -> Single.class; + case "Glob" -> Glob.class; + case "ListStem" -> ListStem.class; + default -> null; + }; + } + } } } diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/pp/PrettyPrinter.java b/keyext.rusty/src/main/java/org/key_project/rusty/pp/PrettyPrinter.java index 8b36a4fd5c8..8f982e4f532 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/pp/PrettyPrinter.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/pp/PrettyPrinter.java @@ -179,6 +179,31 @@ public void performActionOnBlockExpression(BlockExpression x) { } } + @Override + public void performActionOnGhostBlockExpression(GhostBlockExpression x) { + layouter.keyWord("ghost!"); + layouter.print(" "); + + if (x.getChildCount() == 0) { + markStart(x); + layouter.print("{}"); + markEnd(x); + } else { + beginBlock(); + for (Statement stmt : x.getStatements()) { + layouter.nl(); + stmt.visit(this); + } + if (x.getValue() != null) { + layouter.nl(); + x.getValue().visit(this); + } + endBlock(); + } + } + + + @Override public void performActionOnBooleanLiteralExpression(BooleanLiteralExpression x) { layouter.keyWord(x.getValue() ? "true" : "false"); @@ -765,4 +790,45 @@ public void performActionOnPanicFrame(PanicFrame x) { x.getBody().visit(this); layouter.print(")"); } + + @Override + public void performActionOnGhostRustType(GhostRustType x) { + layouter.keyWord("Ghost"); + layouter.print("<"); + x.inner().visit(this); + layouter.print(">"); + } + + public void performActionOnSnapshotExpression(SnapshotExpression x) { + layouter.keyWord("snapshot!"); + layouter.print("("); + x.getPv().visit(this); + layouter.print(")"); + } + + @Override + public void performActionOnStructDef(StructDef x) { + layouter.keyWord("struct"); + layouter.print(" "); + // TODO + } + + @Override + public void performActionOnEnumDef(EnumDef x) { + layouter.keyWord("enum"); + layouter.print(" "); + // TODO + } + + public void performActionOnConstDef(ConstDef x) { + layouter.keyWord("const"); + layouter.print(" "); + layouter.print(x.name()); + layouter.print(": "); + x.rustType().visit(this); + layouter.print(" = "); + x.expr().visit(this); + layouter.print(";"); + layouter.brk(); + } } diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/proof/TacletIndex.java b/keyext.rusty/src/main/java/org/key_project/rusty/proof/TacletIndex.java index f4c0f684094..e0362684ef2 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/proof/TacletIndex.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/proof/TacletIndex.java @@ -15,6 +15,7 @@ import org.key_project.rusty.ast.RustyProgramElement; import org.key_project.rusty.ast.expr.BlockExpression; import org.key_project.rusty.ast.expr.FunctionFrame; +import org.key_project.rusty.ast.expr.GhostBlockExpression; import org.key_project.rusty.ast.expr.LoopScope; import org.key_project.rusty.ast.expr.PanicFrame; import org.key_project.rusty.ast.stmt.ExpressionStatement; @@ -487,7 +488,7 @@ private static class PrefixOccurrences { /// the classes that represent prefix elements of a Rust block static final Class[] prefixClasses = new Class[] { BlockExpression.class, ExpressionStatement.class, LoopScope.class, - FunctionFrame.class, PanicFrame.class }; + FunctionFrame.class, PanicFrame.class, GhostBlockExpression.class }; /// number of prefix types static final int PREFIXTYPES = prefixClasses.length; @@ -497,7 +498,7 @@ private static class PrefixOccurrences { /// fields to indicate the position of the next relevant child (the next possible prefix /// element or real statement - static final int[] nextChild = { 0, 0, 2, 1, 1 }; + static final int[] nextChild = { 0, 0, 2, 1, 1, 0 }; PrefixOccurrences() { reset(); diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/proof/init/ProblemInitializer.java b/keyext.rusty/src/main/java/org/key_project/rusty/proof/init/ProblemInitializer.java index 352e11951c7..e91149174ce 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/proof/init/ProblemInitializer.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/proof/init/ProblemInitializer.java @@ -162,8 +162,8 @@ private void readRust(EnvInput envInput, InitConfig initConfig) throws ProofInpu var output = HirRustyReader.getWrapperOutput(Path.of(rustPath).toAbsolutePath().normalize()); var beforeConversion = System.nanoTime(); - var converter = new HirConverter(initConfig.getServices(), output.specs()); - converter.convertCrate(output.crate()); + var converter = new HirConverter(initConfig.getServices()); + converter.convertCrate(output); LOGGER.debug("HIR conversion took {}", PerfScope.formatTime(System.nanoTime() - beforeConversion)); } catch (IOException e) { diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/proof/mgt/RuleJustificationInfo.java b/keyext.rusty/src/main/java/org/key_project/rusty/proof/mgt/RuleJustificationInfo.java index 41cbfdc86df..048ea12b811 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/proof/mgt/RuleJustificationInfo.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/proof/mgt/RuleJustificationInfo.java @@ -25,7 +25,7 @@ public void addJustification(Rule r, RuleJustification j) { for (RuleKey key : rule2Justification.keySet()) { if (key.equals(ruleKey) && r != key.r) { throw new IllegalArgumentException( - "A rule named " + r.name() + "has already been registered."); + "A rule named " + r.name() + " has already been registered."); } } } else { diff --git a/keyext.rusty/src/main/java/org/key_project/rusty/speclang/FnSpecConverter.java b/keyext.rusty/src/main/java/org/key_project/rusty/speclang/FnSpecConverter.java index 250cd0d971f..af7e18d38c3 100644 --- a/keyext.rusty/src/main/java/org/key_project/rusty/speclang/FnSpecConverter.java +++ b/keyext.rusty/src/main/java/org/key_project/rusty/speclang/FnSpecConverter.java @@ -26,10 +26,11 @@ public FnSpecConverter(Services services) { super(services); } - public List convert(FnSpec fnSpec, ProgramFunction target) { + public List convert(SpecCase[] fnSpecCases, + ProgramFunction target) { setLocalParams(target.getFunction().getLocalIdsToGenericParams()); List contracts = - Arrays.stream(fnSpec.cases()).flatMap(c -> convert(c, target)).toList(); + Arrays.stream(fnSpecCases).flatMap(c -> convert(c, target)).toList(); clearLocalParams(); return contracts; } diff --git a/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/ghost.key b/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/ghost.key new file mode 100644 index 00000000000..b4bd1f2539b --- /dev/null +++ b/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/ghost.key @@ -0,0 +1,8 @@ +\sorts { + Ghost<[E]>; +} + +\functions { + ghost<[E]>(E) -> Ghost<[E]>; + unwrap_ghost<[E]>(Ghost<[E]>) -> E; +} diff --git a/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/ldt.key b/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/ldt.key index 889871b0f07..f90ba763b4e 100644 --- a/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/ldt.key +++ b/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/ldt.key @@ -14,4 +14,5 @@ never, field, rustHeader, - wellfound; + wellfound, + ghost; diff --git a/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/loopScopeRules.key b/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/loopScopeRules.key index ed78a16ea4d..d1866c315c3 100644 --- a/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/loopScopeRules.key +++ b/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/loopScopeRules.key @@ -282,4 +282,10 @@ \replacewith(\modality{#allmodal}{c# break s#se #c}\endmodality (post)) \heuristics(simplify_prog) }; + + blockContinue { + \find(\modality{#allmodal}{c# { continue; s#slist }; #c}\endmodality (post)) + \replacewith(\modality{#allmodal}{c# continue; #c}\endmodality (post)) + \heuristics(simplify_prog) + }; } diff --git a/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/rustRules.key b/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/rustRules.key index ff38a07e7fc..a3d04bb8c99 100644 --- a/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/rustRules.key +++ b/keyext.rusty/src/main/resources/org/key_project/rusty/proof/rules/rustRules.key @@ -357,9 +357,50 @@ \heuristics(simplify_prog) }; - // ---- Break ---- // - // See loop rules / labeled block rules + // ---- Ghost ---- // + + ghost_block_simple_expr { + \find(\modality{#allmodal}{c# ghost! { s#se } #c}\endmodality (post)) + \replacewith(\modality{#allmodal}{c# s#se #c}\endmodality (post)) + \heuristics(simplify_prog, simplify_prog_subset) + }; + + assign_ghost_block_simple_expr { + \find(\modality{#allmodal}{c# s#loc = ghost! { s#se } #c}\endmodality (post)) + \varcond(\hasSort(se, \sort(El)), \hasSort(loc, \sort(Ghost<[El]>))) + \replacewith({loc := ghost<[El]>(se)}\modality{#allmodal}{c# () #c}\endmodality (post)) + \heuristics(simplify_prog, simplify_prog_subset) + }; + + ghost_empty_block { + \find(\modality{#allmodal}{c# ghost!{ } #c}\endmodality (post)) + \replacewith(\modality{#allmodal}{c# () #c}\endmodality (post)) + \heuristics(simplify_prog) + }; + + assign_empty_ghost_block { + \find(\modality{#allmodal}{c# s#loc = ghost! { } #c}\endmodality (post)) + \varcond(\hasSort(loc, \sort(Ghost<[El]>))) + \replacewith({loc := ghost<[El]>(unit)}\modality{#allmodal}{c# () #c}\endmodality (post)) + \heuristics(simplify_prog, simplify_prog_subset) + }; + + // ---- snapshot ---- // + ghost_snapshot { // (DD) there should be a ghost! around the snapshot, right? + \find(\modality{#allmodal}{c# ghost! {snapshot!(s#se) }#c}\endmodality (post)) + \replacewith(\modality{#allmodal}{c# s#se #c}\endmodality (post)) + \heuristics(simplify_prog, simplify_prog_subset) + }; + + assign_ghost_snapshot_block_simple_expr { + \find(\modality{#allmodal}{c# s#loc = ghost! { snapshot!(s#se) } #c}\endmodality (post)) + \varcond(\hasSort(se, \sort(El)), \hasSort(loc, \sort(Ghost<[El]>))) + \replacewith({loc:=ghost<[El]>(se)}\modality{#allmodal}{c# () #c}\endmodality (post)) + \heuristics(simplify_prog, simplify_prog_subset) + }; + + // ---- Break ---- // break_label_unfold { \find(\modality{#allmodal}{c# break s#lbl s#nse #c}\endmodality (post)) \varcond(\newTypeOf(v, nse)) @@ -525,6 +566,22 @@ \heuristics(simplify_prog, simplify_prog_subset) }; + // TODO: remove, once deref of ghost works better + assign_ghost_array_index { + \schemaVar \term int N; + \schemaVar \program RustUsizeExpression idx; + \find(\modality{#allmodal}{c# s#loc = s#se[s#idx] #c}\endmodality (post)) + \sameUpdateLevel + \varcond(\hasSort(loc, \sort(El)), \hasSort(se, \sort(Ghost<[Array<[El, const N]>]>))) + "Normal execution": + \replacewith({loc := arr_get<[El, const N]>(unwrap_ghost<[Array<[El, const N]>]>(se), idx)}\modality{#allmodal}{c# () #c}\endmodality (post)) + \add(N > idx ==>); + "s#idx out of bounds": + \replacewith(\modality{#allmodal}{c# panic!() #c}\endmodality (post)) + \add(!(N > idx) ==>) + \heuristics(simplify_prog) + }; + // ---- Literal expr ---- // // Nothing to do @@ -842,7 +899,7 @@ \replacewith(\modality{#allmodal}{c# { let s#v0 : s#typeof(s#e) = s#e; let s#v1 : s#typeof(s#nse) = s#nse; - s#e0 = s#v0 == s#v1 } + s#loc = s#v0 == s#v1 } #c}\endmodality (post)) \heuristics(simplify_prog) \displayname "equality" diff --git a/keyext.rusty/src/test/java/org/key_project/rusty/proof/ProofCollections.java b/keyext.rusty/src/test/java/org/key_project/rusty/proof/ProofCollections.java index 16924683478..96f75b26fc8 100644 --- a/keyext.rusty/src/test/java/org/key_project/rusty/proof/ProofCollections.java +++ b/keyext.rusty/src/test/java/org/key_project/rusty/proof/ProofCollections.java @@ -36,6 +36,7 @@ public static ProofCollection automaticRustyDL() throws IOException { settings.setVerboseOutput(true); var c = new ProofCollection(settings); + var simple = c.group("simple"); simple.provable("simple.key"); simple.loadable("man-simple.proof"); @@ -89,6 +90,14 @@ public static ProofCollection automaticRustyDL() throws IOException { option.provable("option.key"); option.loadable("man-option.proof"); + var ghost = c.group("ghost"); + ghost.provable("double_array_with_ghost.key"); + ghost.provable("double_array_without_ghost.key"); + ghost.provable("reverse_array_with_ghost.key"); + ghost.provable("reverse_array_without_ghost.key"); + ghost.provable("if_with_ghost.key"); + ghost.provable("if_without_ghost.key"); + var algos = c.group("algorithms"); algos.provable("binary-search/binary-search.key"); diff --git a/keyext.rusty/src/test/resources/testcase/examples/binary-search/Cargo.lock b/keyext.rusty/src/test/resources/testcase/examples/binary-search/Cargo.lock index f44e357dd58..5db81d84444 100644 --- a/keyext.rusty/src/test/resources/testcase/examples/binary-search/Cargo.lock +++ b/keyext.rusty/src/test/resources/testcase/examples/binary-search/Cargo.lock @@ -121,6 +121,7 @@ name = "rml-proc-dummy" version = "0.1.0" dependencies = [ "proc-macro2", + "quote", "rml-syn", "syn", ] diff --git a/keyext.rusty/src/test/resources/testcase/examples/binary-search/Cargo.toml b/keyext.rusty/src/test/resources/testcase/examples/binary-search/Cargo.toml index af844377603..69a4da67482 100644 --- a/keyext.rusty/src/test/resources/testcase/examples/binary-search/Cargo.toml +++ b/keyext.rusty/src/test/resources/testcase/examples/binary-search/Cargo.toml @@ -5,7 +5,7 @@ version = "0.1.0" edition = "2024" [dependencies] -rml-contracts = { path = "../../../../../../../rust-wrapper/rml/crates/rml-contracts" } +rml-contracts = { path = "../../../../../../../rml/crates/rml-contracts" } [lints.rust] unexpected_cfgs = { level = "warn", check-cfg = ['cfg(rml)', 'cfg(doc_cfg)'] } diff --git a/keyext.rusty/src/test/resources/testcase/examples/double_array_with_ghost.key b/keyext.rusty/src/test/resources/testcase/examples/double_array_with_ghost.key new file mode 100644 index 00000000000..43aaa7c5caa --- /dev/null +++ b/keyext.rusty/src/test/resources/testcase/examples/double_array_with_ghost.key @@ -0,0 +1,12 @@ +\programSource "./ghost"; + +\proofObligation +{ + "class": "org.key_project.rusty.proof.init.loader.FunctionOperationContractPOLoader", + "contract": "double_array_with_ghost.normal specification case 0.0", + "name": "double_array_with_ghost.normal specification case 0.0" +} + +\proof{ + //Beweis +} \ No newline at end of file diff --git a/keyext.rusty/src/test/resources/testcase/examples/double_array_without_ghost.key b/keyext.rusty/src/test/resources/testcase/examples/double_array_without_ghost.key new file mode 100644 index 00000000000..137c6237ca5 --- /dev/null +++ b/keyext.rusty/src/test/resources/testcase/examples/double_array_without_ghost.key @@ -0,0 +1,12 @@ +\programSource "./ghost"; + +\proofObligation +{ + "class": "org.key_project.rusty.proof.init.loader.FunctionOperationContractPOLoader", + "contract": "double_array_without_ghost.normal specification case 0.0", + "name": "double_array_without_ghost.normal specification case 0.0" +} + +\proof{ + //Beweis +} \ No newline at end of file diff --git a/keyext.rusty/src/test/resources/testcase/examples/fm26/Cargo.lock b/keyext.rusty/src/test/resources/testcase/examples/fm26/Cargo.lock index cdcb3ea448a..eded793beb2 100644 --- a/keyext.rusty/src/test/resources/testcase/examples/fm26/Cargo.lock +++ b/keyext.rusty/src/test/resources/testcase/examples/fm26/Cargo.lock @@ -109,6 +109,7 @@ name = "rml-proc-dummy" version = "0.1.0" dependencies = [ "proc-macro2", + "quote", "rml-syn", "syn", ] diff --git a/keyext.rusty/src/test/resources/testcase/examples/fm26/Cargo.toml b/keyext.rusty/src/test/resources/testcase/examples/fm26/Cargo.toml index af844377603..69a4da67482 100644 --- a/keyext.rusty/src/test/resources/testcase/examples/fm26/Cargo.toml +++ b/keyext.rusty/src/test/resources/testcase/examples/fm26/Cargo.toml @@ -5,7 +5,7 @@ version = "0.1.0" edition = "2024" [dependencies] -rml-contracts = { path = "../../../../../../../rust-wrapper/rml/crates/rml-contracts" } +rml-contracts = { path = "../../../../../../../rml/crates/rml-contracts" } [lints.rust] unexpected_cfgs = { level = "warn", check-cfg = ['cfg(rml)', 'cfg(doc_cfg)'] } diff --git a/keyext.rusty/src/test/resources/testcase/examples/ghost/Cargo.lock b/keyext.rusty/src/test/resources/testcase/examples/ghost/Cargo.lock new file mode 100644 index 00000000000..0b555ddf1ec --- /dev/null +++ b/keyext.rusty/src/test/resources/testcase/examples/ghost/Cargo.lock @@ -0,0 +1,247 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 4 + +[[package]] +name = "bitflags" +version = "2.9.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6a65b545ab31d687cff52899d4890855fec459eb6afe0da6417b8a18da87aa29" + +[[package]] +name = "bumpalo" +version = "3.19.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "46c5e41b57b8bba42a04676d81cb89e9ee8e859a1a66f80a5a72e1cb76b34d43" + +[[package]] +name = "cfg-if" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9555578bc9e57714c812a1f84e4fc5b4d21fcb063490c624de019f7464c91268" + +[[package]] +name = "getrandom" +version = "0.3.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "26145e563e54f2cadc477553f1ec5ee650b00862f0a58bcd12cbdc5f0ea2d2f4" +dependencies = [ + "cfg-if", + "libc", + "r-efi", + "wasi", +] + +[[package]] +name = "js-sys" +version = "0.3.77" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1cfaf33c695fc6e08064efbc1f72ec937429614f25eef83af942d0e227c3a28f" +dependencies = [ + "once_cell", + "wasm-bindgen", +] + +[[package]] +name = "key-rust-path" +version = "0.1.0" +dependencies = [ + "rml-contracts", +] + +[[package]] +name = "libc" +version = "0.2.175" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6a82ae493e598baaea5209805c49bbf2ea7de956d50d7da0da1164f9c6d28543" + +[[package]] +name = "log" +version = "0.4.27" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "13dc2df351e3202783a1fe0d44375f7295ffb4049267b0f3018346dc122a1d94" + +[[package]] +name = "once_cell" +version = "1.21.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "42f5e15c9953c5e4ccceeb2e7382a716482c34515315f7b03532b8b4e8393d2d" + +[[package]] +name = "paste" +version = "1.0.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "57c0d7b74b563b49d38dae00a0c37d4d6de9b432382b2892f0574ddcae73fd0a" + +[[package]] +name = "proc-macro2" +version = "1.0.101" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "89ae43fd86e4158d6db51ad8e2b80f313af9cc74f5c0e03ccb87de09998732de" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "quote" +version = "1.0.40" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1885c039570dc00dcb4ff087a89e185fd56bae234ddc7f056a945bf36467248d" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "r-efi" +version = "5.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "69cdb34c158ceb288df11e18b4bd39de994f6657d83847bdffdbd7f346754b0f" + +[[package]] +name = "rml-contracts" +version = "0.1.0" +dependencies = [ + "rml-proc", + "rml-proc-dummy", +] + +[[package]] +name = "rml-proc" +version = "0.1.0" +dependencies = [ + "proc-macro2", + "quote", + "rml-syn", + "syn", + "uuid", +] + +[[package]] +name = "rml-proc-dummy" +version = "0.1.0" +dependencies = [ + "proc-macro2", + "quote", + "rml-syn", + "syn", +] + +[[package]] +name = "rml-syn" +version = "0.1.0" +dependencies = [ + "paste", + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "rustversion" +version = "1.0.22" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b39cdef0fa800fc44525c84ccb54a029961a8215f9619753635a9c0d2538d46d" + +[[package]] +name = "syn" +version = "2.0.106" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ede7c438028d4436d71104916910f5bb611972c5cfd7f89b8300a8186e6fada6" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "unicode-ident" +version = "1.0.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5a5f39404a5da50712a4c1eecf25e90dd62b613502b7e925fd4e4d19b5c96512" + +[[package]] +name = "uuid" +version = "1.18.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f33196643e165781c20a5ead5582283a7dacbb87855d867fbc2df3f81eddc1be" +dependencies = [ + "getrandom", + "js-sys", + "wasm-bindgen", +] + +[[package]] +name = "wasi" +version = "0.14.2+wasi-0.2.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9683f9a5a998d873c0d21fcbe3c083009670149a8fab228644b8bd36b2c48cb3" +dependencies = [ + "wit-bindgen-rt", +] + +[[package]] +name = "wasm-bindgen" +version = "0.2.100" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1edc8929d7499fc4e8f0be2262a241556cfc54a0bea223790e71446f2aab1ef5" +dependencies = [ + "cfg-if", + "once_cell", + "rustversion", + "wasm-bindgen-macro", +] + +[[package]] +name = "wasm-bindgen-backend" +version = "0.2.100" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2f0a0651a5c2bc21487bde11ee802ccaf4c51935d0d3d42a6101f98161700bc6" +dependencies = [ + "bumpalo", + "log", + "proc-macro2", + "quote", + "syn", + "wasm-bindgen-shared", +] + +[[package]] +name = "wasm-bindgen-macro" +version = "0.2.100" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7fe63fc6d09ed3792bd0897b314f53de8e16568c2b3f7982f468c0bf9bd0b407" +dependencies = [ + "quote", + "wasm-bindgen-macro-support", +] + +[[package]] +name = "wasm-bindgen-macro-support" +version = "0.2.100" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8ae87ea40c9f689fc23f209965b6fb8a99ad69aeeb0231408be24920604395de" +dependencies = [ + "proc-macro2", + "quote", + "syn", + "wasm-bindgen-backend", + "wasm-bindgen-shared", +] + +[[package]] +name = "wasm-bindgen-shared" +version = "0.2.100" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1a05d73b933a847d6cccdda8f838a22ff101ad9bf93e33684f39c1f5f0eece3d" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "wit-bindgen-rt" +version = "0.39.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6f42320e61fe2cfd34354ecb597f86f413484a798ba44a8ca1165c58d42da6c1" +dependencies = [ + "bitflags", +] diff --git a/keyext.rusty/src/test/resources/testcase/examples/ghost/Cargo.toml b/keyext.rusty/src/test/resources/testcase/examples/ghost/Cargo.toml new file mode 100644 index 00000000000..a095057fca9 --- /dev/null +++ b/keyext.rusty/src/test/resources/testcase/examples/ghost/Cargo.toml @@ -0,0 +1,11 @@ +[package] +name = "key-rust-path" +authors = ["KeY"] +version = "0.1.0" +edition = "2024" + +[dependencies] +rml-contracts = { path = "../../../../../../../rml/crates/rml-contracts" } + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(rml)', 'cfg(doc_cfg)'] } \ No newline at end of file diff --git a/keyext.rusty/src/test/resources/testcase/examples/ghost/rust-toolchain.toml b/keyext.rusty/src/test/resources/testcase/examples/ghost/rust-toolchain.toml new file mode 100644 index 00000000000..c237da77270 --- /dev/null +++ b/keyext.rusty/src/test/resources/testcase/examples/ghost/rust-toolchain.toml @@ -0,0 +1,10 @@ +[toolchain] +channel = "nightly-2025-05-20" +components = [ + "rustc-dev", + "llvm-tools-preview", + "rust-std", + "rustfmt", + "clippy", +] +profile = "minimal" \ No newline at end of file diff --git a/keyext.rusty/src/test/resources/testcase/examples/ghost/src/lib.rs b/keyext.rusty/src/test/resources/testcase/examples/ghost/src/lib.rs new file mode 100644 index 00000000000..19d80f4b272 --- /dev/null +++ b/keyext.rusty/src/test/resources/testcase/examples/ghost/src/lib.rs @@ -0,0 +1,423 @@ +#![feature(stmt_expr_attributes)] +#![feature(proc_macro_hygiene)] +#![allow(clippy::all)] +#![allow(dead_code)] + +extern crate rml_contracts; +use rml_contracts::*; + +#[spec { ensures(result == 2) }] +pub fn double_array_with_ghost(a: [i32; 10]) -> i32 { + let old_a = ghost! { snapshot!(a) }; + + let mut i: usize = 0; + let len: usize = 10; + let mut b = a; + let mut v: usize = len; + + #[invariant(0 <= v && v <= len)] + #[invariant(v == len - i)] + #[variant(v)] + loop { + if i < len { + b[i] = b[i] * 2; + + ghost! { + let all_doubled = b[i] == old_a[i] * 2; + }; + + i += 1; + v -= 1; + continue; + } else { + break; + } + } + + 2 +} + +#[spec { ensures(result == 2) }] +pub fn double_array_without_ghost(a: [i32; 10]) -> i32 { + let old_a = a; + + let mut i: usize = 0; + let len: usize = 10; + let mut b = a; + let mut v: usize = len; + + #[invariant(0 <= v && v <= len)] + #[invariant(v == len - i)] + #[variant(v)] + loop { + if i < len { + b[i] = b[i] * 2; + + let all_doubled = b[i] == old_a[i] * 2; + + i += 1; + v -= 1; + continue; + } else { + break; + } + } + + 2 +} + +#[spec {ensures(result == 2)}] +pub fn reverse_array_with_ghost(a: [i32; 10]) -> i32 { + let mut b = a; + + let old_b = ghost! { snapshot!(b) }; + + let mut i = 0; + let len = 10; + let mut v = len / 2; + + #[invariant(0 <= i && i <= len / 2)] + #[invariant(0 <= v && v <= len / 2)] + #[invariant(v == (len / 2) - i)] + #[variant(v)] + loop { + if i < len / 2 { + let j = (len - 1) - i; + + let tmp= b[i]; + b[i] = b[j]; + b[j] = tmp; + + ghost! { + let left= b[i] == old_b[j]; + let right = b[j] == old_b[i]; + let check = left && right; + }; + + i += 1; + v -= 1; + continue; + } else { + break; + } + } + + ghost! { + let proof = b[0] == old_b[len - 1] && b[len - 1] == old_b[0]; + let check = proof; + }; + + 2 +} + +#[spec {ensures(result == 2)}] +pub fn reverse_array_without_ghost(a: [i32; 10]) -> i32 { + let mut b = a; + + let old_b = a; + + let mut i = 0; + let len = 10; + let mut v = len / 2; + + #[invariant(0 <= i && i <= len / 2)] + #[invariant(0 <= v && v <= len / 2)] + #[invariant(v == (len / 2) - i)] + #[variant(v)] + loop { + if i < len / 2 { + let j = (len - 1) - i; + + let tmp= b[i]; + b[i] = b[j]; + b[j] = tmp; + + let left= b[i] == old_b[j]; + let right = b[j] == old_b[i]; + let check = left && right; + + + i += 1; + v -= 1; + continue; + } else { + break; + } + } + let proof = b[0] == old_b[len - 1] && b[len - 1] == old_b[0]; + let check = proof; + + 2 +} +#[spec { + ensures(result > a && result > b) +}] +pub fn if_with_ghost(a: u32, b: u32) -> u32 { + let old_a = a; + let old_b = b; + + let res = + if a > b { + let r = a + 1; + + ghost! { + let test_cond = old_a > old_b; + let test_a = r > old_a; + let test_b = r > old_b; + let test_final = test_cond && test_a && test_b; + }; + + r + } else { + let r = b + 2; + + ghost! { + let test_cond = !(old_a > old_b); + let test_b = r > old_b; + let test_a = r > old_a; + let test_final = test_cond && test_b && test_a; + }; + + r + }; + + res +} + +#[spec { + ensures(result > a && result > b) +}] +pub fn if_without_ghost(a: u32, b: u32) -> u32 { + let old_a = a; + let old_b = b; + + let res = + if a > b { + let r = a + 1; + + let test_cond = old_a > old_b; + let test_a = r > old_a; + let test_b = r > old_b; + let test_final = test_cond && test_a && test_b; + + r + } else { + let r = b + 2; + + let test_cond = !(old_a > old_b); + let test_b = r > old_b; + let test_a = r > old_a; + let test_final = test_cond && test_b && test_a; + + r + }; + + res +} + + +/* +// An GHOSTHOUSE exmaple for the RQ3 +pub struct Person { + pub id: usize, + pub close_to_panic: u8, // 0..=100 + pub aborted: bool, +} +#[derive(Copy, Clone)] +pub enum Room { + Entrance, + CreepyBasement, + Laboratory, + Kitchen, + TortureRoom, +} + + +pub const ROOM_COUNT: usize = 5; + +pub fn room_as_usize(room: Room) -> usize { + match room { + Room::Entrance => 0, + Room::CreepyBasement => 1, + Room::Laboratory => 2, + Room::Kitchen => 3, + Room::TortureRoom => 4, + } +} + +pub enum HouseError { + RoomOccupied, + VisitorAborted, + InvalidPanicValue, +} + +pub struct GhostHouse { + visitor_location: Room, + visitor: Person, + occupancy: [bool; ROOM_COUNT], // true = occupied + room_fear: [u8; ROOM_COUNT], // 0..=100 per room +} + +pub fn new_ghost_house(visitor: Person) -> Result { + if visitor.close_to_panic > 100 { + return Err(HouseError::InvalidPanicValue); + } + let mut occ = [false; ROOM_COUNT]; + let entrance_idx = room_as_usize(Room::Entrance); + occ[entrance_idx] = true; + + let room_fear: [u8; ROOM_COUNT] = [ + 5, // Entrance + 10, // CreepyBasement + 7, // Laboratory + 3, // Kitchen + 15, // TortureRoom + ]; + + let gh = GhostHouse{ + visitor_location: Room::Entrance, + visitor, + occupancy: occ, + room_fear, + }; + + let loc_idx = room_as_usize(gh.visitor_location); + let check_occupancy = gh.occupancy[entrance_idx]; + let check_panic = gh.visitor.close_to_panic; + + ghost!{ + let at_entrance = loc_idx == entrance_idx; + //proof_assert!(at_entrance); + + let entrance_occ = check_occupancy == true; + //proof_assert!(entrance_occ); + + let panic_range = check_panic <= 100; + //proof_assert!(panic_range); + + let _checks = (at_entrance, entrance_occ, panic_range); + }; + + Ok(gh) +} +pub fn move_to(gh: &mut GhostHouse, target: Room) -> Result<(), HouseError> { + if gh.visitor.aborted { + return Err(HouseError::VisitorAborted); + } + + let t = room_as_usize(target); + let current_loc = gh.visitor_location; + let mut flags = gh.occupancy; + let current = room_as_usize(gh.visitor_location); + + if flags[t] { + return Err(HouseError::RoomOccupied); + } + + let old_flags = ghost!{snapshot!(flags)}; + let old_loc = ghost!{snapshot!(current_loc)}; + let old_loc_idx = room_as_usize(current_loc); + + ghost!{ + let pre_current_occupied = (*old_flags)[old_loc_idx] == true; + //proof_assert!(pre_current_occupied); + + let pre_target_free = (*old_flags)[t] == false; + //proof_assert!(pre_target_free); + + let idx_distinct = old_loc_idx != t; + //proof_assert!(idx_distinct); + + let _checks1 = (pre_current_occupied, pre_target_free, idx_distinct); + }; + + flags[current] = false; + flags[t] = true; + let new_loc = target; + + let new_flags = ghost!{snapshot!(flags)}; + let new_loc_s = ghost!{snapshot!(new_loc)}; + + let new_loc_idx = room_as_usize(new_loc); + + ghost!{ + let post_loc_updated = new_loc_idx == t; + //proof_assert!(post_loc_updated); + + let post_current_free = (*new_flags)[old_loc_idx] == false; + //proof_assert!(post_current_free); + + let post_target_occ = (*new_flags)[t] == true; + //proof_assert!(post_target_occ); + + let _checks2 = (post_loc_updated, post_current_free, post_target_occ); + }; + + gh.occupancy = flags; + gh.visitor_location = new_loc; + + Ok(()) +} + +/// Ghost scares the visitor, increasing panic. +pub fn scare(gh: &mut GhostHouse, intensity: u8) -> Result<(), HouseError> { + if gh.visitor.aborted { + return Err(HouseError::VisitorAborted); + } + + let mut panic = gh.visitor.close_to_panic; + let mut aborted = gh.visitor.aborted; + let old_panic = ghost! { snapshot!(panic) }; + let old_aborted = ghost! { snapshot!(aborted) }; + + ghost! { + let _pre_aborted = old_aborted == false; + //proof_assert!(_pre_aborted); + + let _pre_range = old_panic <= 100; + //proof_assert!(_pre_range); + + let _checks1 = (_pre_aborted, _pre_range); + }; + + let mut new_panic: u8; + if (255 - panic) < intensity { + new_panic = 255; + } else { + new_panic = panic + intensity; + } + + if new_panic > 100 { + new_panic = 100; + } + + panic = new_panic; + + if panic >= 90 { + aborted = true; + } + + let new_panic = ghost! { snapshot!(panic) }; + let new_aborted = ghost! { snapshot!(aborted) }; + + ghost! { + let panic_not_decreased = new_panic >= old_panic; + //proof_assert!(panic_not_decreased); + + let panic_bounded = new_panic <= 100; + //proof_assert!(panic_bounded); + + let aborted_monotonic = old_aborted == true || new_aborted == true; + //proof_assert!(aborted_monotonic); + + let _checks2 = (panic_not_decreased, panic_bounded, aborted_monotonic); + }; + + gh.visitor.close_to_panic = panic; + gh.visitor.aborted = aborted; + + Ok(()) +} + + +*/ \ No newline at end of file diff --git a/keyext.rusty/src/test/resources/testcase/examples/if_with_ghost.key b/keyext.rusty/src/test/resources/testcase/examples/if_with_ghost.key new file mode 100644 index 00000000000..25bdbec7323 --- /dev/null +++ b/keyext.rusty/src/test/resources/testcase/examples/if_with_ghost.key @@ -0,0 +1,12 @@ +\programSource "./ghost"; + +\proofObligation +{ + "class": "org.key_project.rusty.proof.init.loader.FunctionOperationContractPOLoader", + "contract": "if_with_ghost.normal specification case 0.0", + "name": "if_with_ghost.normal specification case 0.0" +} + +\proof{ + //Beweis +} \ No newline at end of file diff --git a/keyext.rusty/src/test/resources/testcase/examples/if_without_ghost.key b/keyext.rusty/src/test/resources/testcase/examples/if_without_ghost.key new file mode 100644 index 00000000000..6e1b4b61705 --- /dev/null +++ b/keyext.rusty/src/test/resources/testcase/examples/if_without_ghost.key @@ -0,0 +1,12 @@ +\programSource "./ghost"; + +\proofObligation +{ + "class": "org.key_project.rusty.proof.init.loader.FunctionOperationContractPOLoader", + "contract": "if_without_ghost.normal specification case 0.0", + "name": "if_without_ghost.normal specification case 0.0" +} + +\proof{ + //Beweis +} \ No newline at end of file diff --git a/keyext.rusty/src/test/resources/testcase/examples/option/Cargo.lock b/keyext.rusty/src/test/resources/testcase/examples/option/Cargo.lock index ad84360dcb1..871def1b3bd 100644 --- a/keyext.rusty/src/test/resources/testcase/examples/option/Cargo.lock +++ b/keyext.rusty/src/test/resources/testcase/examples/option/Cargo.lock @@ -121,6 +121,7 @@ name = "rml-proc-dummy" version = "0.1.0" dependencies = [ "proc-macro2", + "quote", "rml-syn", "syn", ] diff --git a/keyext.rusty/src/test/resources/testcase/examples/option/Cargo.toml b/keyext.rusty/src/test/resources/testcase/examples/option/Cargo.toml index b66db8ce30c..a095057fca9 100644 --- a/keyext.rusty/src/test/resources/testcase/examples/option/Cargo.toml +++ b/keyext.rusty/src/test/resources/testcase/examples/option/Cargo.toml @@ -5,7 +5,7 @@ version = "0.1.0" edition = "2024" [dependencies] -rml-contracts = { path = "../../../../../../../rust-wrapper/rml/crates/rml-contracts" } +rml-contracts = { path = "../../../../../../../rml/crates/rml-contracts" } [lints.rust] unexpected_cfgs = { level = "warn", check-cfg = ['cfg(rml)', 'cfg(doc_cfg)'] } \ No newline at end of file diff --git a/keyext.rusty/src/test/resources/testcase/examples/reverse_array_with_ghost.key b/keyext.rusty/src/test/resources/testcase/examples/reverse_array_with_ghost.key new file mode 100644 index 00000000000..96b838c3c4e --- /dev/null +++ b/keyext.rusty/src/test/resources/testcase/examples/reverse_array_with_ghost.key @@ -0,0 +1,12 @@ +\programSource "./ghost"; + +\proofObligation +{ + "class": "org.key_project.rusty.proof.init.loader.FunctionOperationContractPOLoader", + "contract": "reverse_array_with_ghost.normal specification case 0.0", + "name": "reverse_array_with_ghost.normal specification case 0.0" +} + +\proof{ + //Beweis +} \ No newline at end of file diff --git a/keyext.rusty/src/test/resources/testcase/examples/reverse_array_without_ghost.key b/keyext.rusty/src/test/resources/testcase/examples/reverse_array_without_ghost.key new file mode 100644 index 00000000000..7cc91abcf36 --- /dev/null +++ b/keyext.rusty/src/test/resources/testcase/examples/reverse_array_without_ghost.key @@ -0,0 +1,12 @@ +\programSource "./ghost"; + +\proofObligation +{ + "class": "org.key_project.rusty.proof.init.loader.FunctionOperationContractPOLoader", + "contract": "reverse_array_without_ghost.normal specification case 0.0", + "name": "reverse_array_without_ghost.normal specification case 0.0" +} + +\proof{ + //Beweis +} \ No newline at end of file diff --git a/keyext.rusty/src/test/resources/testcase/examples/rustSrc/Cargo.lock b/keyext.rusty/src/test/resources/testcase/examples/rustSrc/Cargo.lock index 25d17cc0cea..3bef7ce5b96 100644 --- a/keyext.rusty/src/test/resources/testcase/examples/rustSrc/Cargo.lock +++ b/keyext.rusty/src/test/resources/testcase/examples/rustSrc/Cargo.lock @@ -121,6 +121,7 @@ name = "rml-proc-dummy" version = "0.1.0" dependencies = [ "proc-macro2", + "quote", "rml-syn", "syn", ] diff --git a/keyext.rusty/src/test/resources/testcase/examples/rustSrc/Cargo.toml b/keyext.rusty/src/test/resources/testcase/examples/rustSrc/Cargo.toml index b66db8ce30c..a095057fca9 100644 --- a/keyext.rusty/src/test/resources/testcase/examples/rustSrc/Cargo.toml +++ b/keyext.rusty/src/test/resources/testcase/examples/rustSrc/Cargo.toml @@ -5,7 +5,7 @@ version = "0.1.0" edition = "2024" [dependencies] -rml-contracts = { path = "../../../../../../../rust-wrapper/rml/crates/rml-contracts" } +rml-contracts = { path = "../../../../../../../rml/crates/rml-contracts" } [lints.rust] unexpected_cfgs = { level = "warn", check-cfg = ['cfg(rml)', 'cfg(doc_cfg)'] } \ No newline at end of file diff --git a/rml b/rml new file mode 160000 index 00000000000..8b2e7503f54 --- /dev/null +++ b/rml @@ -0,0 +1 @@ +Subproject commit 8b2e7503f545ca9f28ff1423bdeb47ed38fdcd9e diff --git a/rust-wrapper b/rust-wrapper deleted file mode 160000 index 8d1ae0d9825..00000000000 --- a/rust-wrapper +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 8d1ae0d9825d3ae695e78c0817de0b3b0d85efab