From 92e7d3377e503661e418e4a8dc5305df34d93628 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Mon, 9 Dec 2024 11:01:20 +0100 Subject: [PATCH] Remove rejected type ascription patterns from generated f*. --- engine/backends/fstar/fstar_backend.ml | 3 +- .../toolchain__literals into-fstar.snap | 50 +++++++++---------- .../toolchain__patterns into-fstar.snap | 41 +++++++++++++++ tests/Cargo.lock | 14 ++++-- tests/Cargo.toml | 1 + tests/patterns/Cargo.toml | 9 ++++ tests/patterns/src/lib.rs | 15 ++++++ 7 files changed, 102 insertions(+), 31 deletions(-) create mode 100644 test-harness/src/snapshots/toolchain__patterns into-fstar.snap create mode 100644 tests/patterns/Cargo.toml create mode 100644 tests/patterns/src/lib.rs diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index f179ffe38..3518e40c4 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -401,8 +401,9 @@ struct let ppat = ppat' false in match p.p with | PWild -> F.wild - | PAscription { typ; pat } -> + | PAscription { typ; pat = { p = PBinding _; _ } as pat } -> F.pat @@ F.AST.PatAscribed (ppat pat, (pty p.span typ, None)) + | PAscription { pat; _ } -> ppat pat | PBinding { mut = Immutable; diff --git a/test-harness/src/snapshots/toolchain__literals into-fstar.snap b/test-harness/src/snapshots/toolchain__literals into-fstar.snap index efe3f1ef0..f3bb80621 100644 --- a/test-harness/src/snapshots/toolchain__literals into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__literals into-fstar.snap @@ -38,7 +38,7 @@ type t_Foo = { f_field:u8 } let v_CONSTANT: t_Foo = { f_field = 3uy } <: t_Foo let casts (x8: u8) (x16: u16) (x32: u32) (x64: u64) (xs: usize) : Prims.unit = - let (_: u64):u64 = + let _:u64 = ((((cast (x8 <: u8) <: u64) +! (cast (x16 <: u16) <: u64) <: u64) +! (cast (x32 <: u32) <: u64) <: u64) +! @@ -47,28 +47,28 @@ let casts (x8: u8) (x16: u16) (x32: u32) (x64: u64) (xs: usize) : Prims.unit = u64) +! (cast (xs <: usize) <: u64) in - let (_: u32):u32 = + let _:u32 = ((((cast (x8 <: u8) <: u32) +! (cast (x16 <: u16) <: u32) <: u32) +! x32 <: u32) +! (cast (x64 <: u64) <: u32) <: u32) +! (cast (xs <: usize) <: u32) in - let (_: u16):u16 = + let _:u16 = ((((cast (x8 <: u8) <: u16) +! x16 <: u16) +! (cast (x32 <: u32) <: u16) <: u16) +! (cast (x64 <: u64) <: u16) <: u16) +! (cast (xs <: usize) <: u16) in - let (_: u8):u8 = + let _:u8 = (((x8 +! (cast (x16 <: u16) <: u8) <: u8) +! (cast (x32 <: u32) <: u8) <: u8) +! (cast (x64 <: u64) <: u8) <: u8) +! (cast (xs <: usize) <: u8) in - let (_: i64):i64 = + let _:i64 = ((((cast (x8 <: u8) <: i64) +! (cast (x16 <: u16) <: i64) <: i64) +! (cast (x32 <: u32) <: i64) <: i64) +! @@ -77,7 +77,7 @@ let casts (x8: u8) (x16: u16) (x32: u32) (x64: u64) (xs: usize) : Prims.unit = i64) +! (cast (xs <: usize) <: i64) in - let (_: i32):i32 = + let _:i32 = ((((cast (x8 <: u8) <: i32) +! (cast (x16 <: u16) <: i32) <: i32) +! (cast (x32 <: u32) <: i32) <: i32) +! @@ -86,7 +86,7 @@ let casts (x8: u8) (x16: u16) (x32: u32) (x64: u64) (xs: usize) : Prims.unit = i32) +! (cast (xs <: usize) <: i32) in - let (_: i16):i16 = + let _:i16 = ((((cast (x8 <: u8) <: i16) +! (cast (x16 <: u16) <: i16) <: i16) +! (cast (x32 <: u32) <: i16) <: i16) +! @@ -95,7 +95,7 @@ let casts (x8: u8) (x16: u16) (x32: u32) (x64: u64) (xs: usize) : Prims.unit = i16) +! (cast (xs <: usize) <: i16) in - let (_: i8):i8 = + let _:i8 = ((((cast (x8 <: u8) <: i8) +! (cast (x16 <: u16) <: i8) <: i8) +! (cast (x32 <: u32) <: i8) <: i8) +! @@ -115,7 +115,7 @@ let math_integers (x: Hax_lib.Int.t_Int) : Prims.Pure u8 (requires x > (0 <: Hax_lib.Int.t_Int) && x < (16 <: Hax_lib.Int.t_Int)) (fun _ -> Prims.l_True) = - let (_: Hax_lib.Int.t_Int):Hax_lib.Int.t_Int = Rust_primitives.Hax.Int.from_machine (sz 3) in + let _:Hax_lib.Int.t_Int = Rust_primitives.Hax.Int.from_machine (sz 3) in let _:bool = ((-340282366920938463463374607431768211455000) <: Hax_lib.Int.t_Int) > (340282366920938463463374607431768211455000 <: Hax_lib.Int.t_Int) @@ -129,26 +129,26 @@ let math_integers (x: Hax_lib.Int.t_Int) let _:Hax_lib.Int.t_Int = x - x in let _:Hax_lib.Int.t_Int = x * x in let _:Hax_lib.Int.t_Int = x / x in - let (_: i16):i16 = Hax_lib.Int.impl__Int__to_i16 x in - let (_: i32):i32 = Hax_lib.Int.impl__Int__to_i32 x in - let (_: i64):i64 = Hax_lib.Int.impl__Int__to_i64 x in - let (_: i128):i128 = Hax_lib.Int.impl__Int__to_i128 x in - let (_: isize):isize = Hax_lib.Int.impl__Int__to_isize x in - let (_: u16):u16 = Hax_lib.Int.impl__Int__to_u16 x in - let (_: u32):u32 = Hax_lib.Int.impl__Int__to_u32 x in - let (_: u64):u64 = Hax_lib.Int.impl__Int__to_u64 x in - let (_: u128):u128 = Hax_lib.Int.impl__Int__to_u128 x in - let (_: usize):usize = Hax_lib.Int.impl__Int__to_usize x in + let _:i16 = Hax_lib.Int.impl__Int__to_i16 x in + let _:i32 = Hax_lib.Int.impl__Int__to_i32 x in + let _:i64 = Hax_lib.Int.impl__Int__to_i64 x in + let _:i128 = Hax_lib.Int.impl__Int__to_i128 x in + let _:isize = Hax_lib.Int.impl__Int__to_isize x in + let _:u16 = Hax_lib.Int.impl__Int__to_u16 x in + let _:u32 = Hax_lib.Int.impl__Int__to_u32 x in + let _:u64 = Hax_lib.Int.impl__Int__to_u64 x in + let _:u128 = Hax_lib.Int.impl__Int__to_u128 x in + let _:usize = Hax_lib.Int.impl__Int__to_usize x in Hax_lib.Int.impl__Int__to_u8 (x + (x * x <: Hax_lib.Int.t_Int) <: Hax_lib.Int.t_Int) let null: char = '\0' let numeric (_: Prims.unit) : Prims.unit = - let (_: usize):usize = sz 123 in - let (_: isize):isize = isz (-42) in - let (_: isize):isize = isz 42 in - let (_: i32):i32 = (-42l) in - let (_: u128):u128 = pub_u128 22222222222222222222 in + let _:usize = sz 123 in + let _:isize = isz (-42) in + let _:isize = isz 42 in + let _:i32 = (-42l) in + let _:u128 = pub_u128 22222222222222222222 in () let patterns (_: Prims.unit) : Prims.unit = @@ -190,7 +190,7 @@ let panic_with_msg (_: Prims.unit) : Prims.unit = Rust_primitives.Hax.t_Never) let empty_array (_: Prims.unit) : Prims.unit = - let (_: t_Slice u8):t_Slice u8 = + let _:t_Slice u8 = (let list:Prims.list u8 = [] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 0); Rust_primitives.Hax.array_of_list 0 list) diff --git a/test-harness/src/snapshots/toolchain__patterns into-fstar.snap b/test-harness/src/snapshots/toolchain__patterns into-fstar.snap new file mode 100644 index 000000000..77025089e --- /dev/null +++ b/test-harness/src/snapshots/toolchain__patterns into-fstar.snap @@ -0,0 +1,41 @@ +--- +source: test-harness/src/harness.rs +expression: snapshot +info: + kind: + Translate: + backend: fstar + info: + name: patterns + manifest: patterns/Cargo.toml + description: ~ + spec: + optional: false + broken: false + issue_id: ~ + positive: true + snapshot: + stderr: true + stdout: true + include_flag: ~ + backend_options: ~ +--- +exit = 0 +stderr = 'Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs' + +[stdout] +diagnostics = [] + +[stdout.files] +"Patterns.fst" = ''' +module Patterns +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +type t_Other = | Other : i32 -> t_Other + +type t_Test = | Test_C1 : t_Other -> t_Test + +let impl__test (self: t_Test) : i32 = match self with | Test_C1 c -> c._0 +''' diff --git a/tests/Cargo.lock b/tests/Cargo.lock index 5fcbe4dc7..1a2c1f3b8 100644 --- a/tests/Cargo.lock +++ b/tests/Cargo.lock @@ -320,7 +320,7 @@ checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888" [[package]] name = "hax-lib" -version = "0.1.0-alpha.1" +version = "0.1.0-rc.1" dependencies = [ "hax-lib-macros", "num-bigint", @@ -329,7 +329,7 @@ dependencies = [ [[package]] name = "hax-lib-macros" -version = "0.1.0-alpha.1" +version = "0.1.0-rc.1" dependencies = [ "hax-lib-macros-types", "paste", @@ -341,7 +341,7 @@ dependencies = [ [[package]] name = "hax-lib-macros-types" -version = "0.1.0-alpha.1" +version = "0.1.0-rc.1" dependencies = [ "proc-macro2", "quote", @@ -352,14 +352,14 @@ dependencies = [ [[package]] name = "hax-lib-protocol" -version = "0.1.0-alpha.1" +version = "0.1.0-rc.1" dependencies = [ "libcrux", ] [[package]] name = "hax-lib-protocol-macros" -version = "0.1.0-alpha.1" +version = "0.1.0-rc.1" dependencies = [ "proc-macro-error", "proc-macro2", @@ -664,6 +664,10 @@ checksum = "57c0d7b74b563b49d38dae00a0c37d4d6de9b432382b2892f0574ddcae73fd0a" name = "pattern-or" version = "0.1.0" +[[package]] +name = "patterns" +version = "0.1.0" + [[package]] name = "ping-pong" version = "0.1.0" diff --git a/tests/Cargo.toml b/tests/Cargo.toml index df3b03ffa..5e73e647e 100644 --- a/tests/Cargo.toml +++ b/tests/Cargo.toml @@ -23,6 +23,7 @@ members = [ "dyn", "reordering", "nested-derefs", + "patterns", "proverif-minimal", "proverif-basic-structs", "proverif-ping-pong", diff --git a/tests/patterns/Cargo.toml b/tests/patterns/Cargo.toml new file mode 100644 index 000000000..f6b4e63d6 --- /dev/null +++ b/tests/patterns/Cargo.toml @@ -0,0 +1,9 @@ +[package] +name = "patterns" +version = "0.1.0" +edition = "2021" + +[dependencies] + +[package.metadata.hax-tests] +into."fstar" = { issue_id = "1170" } \ No newline at end of file diff --git a/tests/patterns/src/lib.rs b/tests/patterns/src/lib.rs new file mode 100644 index 000000000..058e37b70 --- /dev/null +++ b/tests/patterns/src/lib.rs @@ -0,0 +1,15 @@ +#![allow(dead_code)] + +struct Other<'a>(&'a i32); + +enum Test<'a> { + C1(Other<'a>), +} + +impl<'a> Test<'a> { + fn test(&self) -> i32 { + match self { + Self::C1(c) => *c.0, + } + } +}