From a8f96d3e178146b9cc67e8dab3b4c2bbaa52d9de Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Wed, 17 Jul 2024 14:53:01 +0200 Subject: [PATCH 1/2] Support let-else pattern. --- engine/lib/import_thir.ml | 135 ++++++++++++++++++++++---------------- 1 file changed, 80 insertions(+), 55 deletions(-) diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 586fa94ab..547919d8a 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -370,6 +370,84 @@ end) : EXPR = struct let v = Global_ident.of_name Value Rust_primitives__hax__dropped_body in { span; typ; e = GlobalVar v } + and c_block ~expr ~span ~stmts ~ty : expr = + let full_span = Span.of_thir span in + let typ = c_ty span ty in + (* if there is no expression & the last expression is ⊥, just use that *) + let lift_last_statement_as_expr_if_possible expr stmts (ty : Thir.ty) = + match (ty, expr, List.drop_last stmts, List.last stmts) with + | ( Thir.Never, + None, + Some stmts, + Some ({ kind = Thir.Expr { expr; _ }; _ } : Thir.stmt) ) -> + (stmts, Some expr) + | _ -> (stmts, expr) + in + let o_stmts, o_expr = + lift_last_statement_as_expr_if_possible expr stmts ty + in + let init = + Option.map + ~f:(fun e -> + let e = c_expr e in + { e with e = Block (e, W.block) }) + o_expr + |> Option.value ~default:(unit_expr full_span) + in + List.fold_right o_stmts ~init ~f:(fun { kind; _ } body -> + match kind with + | Expr { expr = rhs; _ } -> + let rhs = c_expr rhs in + let e = + Let { monadic = None; lhs = wild_pat rhs.span rhs.typ; rhs; body } + in + { e; typ; span = Span.union rhs.span body.span } + | Let + { + else_block = Some { expr; span; stmts; _ }; + pattern = lhs; + initializer' = Some rhs; + _; + } -> + let lhs = c_pat lhs in + let rhs = c_expr rhs in + let else_block = c_block ~expr ~span ~stmts ~ty in + let lhs_body_span = Span.union lhs.span body.span in + let e = + Match + { + arms = + [ + { arm = { arm_pat = lhs; body }; span = lhs_body_span }; + { + arm = + { + arm_pat = + { + p = PWild; + span = else_block.span; + typ = lhs.typ; + }; + body = { else_block with typ = body.typ }; + }; + span = else_block.span; + }; + ]; + scrutinee = rhs; + } + in + { e; typ; span = full_span } + | Let { initializer' = None; _ } -> + unimplemented ~issue_id:156 [ span ] + "Sorry, Hax does not support declare-first let bindings (see \ + https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) \ + for now." + | Let { pattern = lhs; initializer' = Some rhs; _ } -> + let lhs = c_pat lhs in + let rhs = c_expr rhs in + let e = Let { monadic = None; lhs; rhs; body } in + { e; typ; span = Span.union rhs.span body.span }) + and c_expr_unwrapped (e : Thir.decorated_for__expr_kind) : expr = (* TODO: eliminate that `call`, use the one from `ast_utils` *) let call f args = @@ -516,61 +594,8 @@ end) : EXPR = struct | Let _ -> unimplemented [ e.span ] "Let" | Block { safety_mode = BuiltinUnsafe | ExplicitUnsafe; _ } -> unsafe_block [ e.span ] - | Block o -> - (* if there is no expression & the last expression is ⊥, just use that *) - let lift_last_statement_as_expr_if_possible expr stmts (ty : Thir.ty) - = - match (ty, expr, List.drop_last stmts, List.last stmts) with - | ( Thir.Never, - None, - Some stmts, - Some ({ kind = Thir.Expr { expr; _ }; _ } : Thir.stmt) ) -> - (stmts, Some expr) - | _ -> (stmts, expr) - in - let o_stmts, o_expr = - lift_last_statement_as_expr_if_possible o.expr o.stmts e.ty - in - let init = - Option.map - ~f:(fun e -> - let e = c_expr e in - { e with e = Block (e, W.block) }) - o_expr - |> Option.value ~default:(unit_expr span) - in - let { e; _ } = - List.fold_right o_stmts ~init ~f:(fun { kind; _ } body -> - match kind with - | Expr { expr = rhs; _ } -> - let rhs = c_expr rhs in - let e = - Let - { - monadic = None; - lhs = wild_pat rhs.span rhs.typ; - rhs; - body; - } - in - { e; typ; span = Span.union rhs.span body.span } - | Let { else_block = Some _; _ } -> - unimplemented ~issue_id:155 [ e.span ] - "Sorry, Hax does not support [let-else] (see \ - https://doc.rust-lang.org/rust-by-example/flow_control/let_else.html) \ - for now." - | Let { initializer' = None; _ } -> - unimplemented ~issue_id:156 [ e.span ] - "Sorry, Hax does not support declare-first let bindings \ - (see \ - https://doc.rust-lang.org/rust-by-example/variable_bindings/declare.html) \ - for now." - | Let { pattern = lhs; initializer' = Some rhs; _ } -> - let lhs = c_pat lhs in - let rhs = c_expr rhs in - let e = Let { monadic = None; lhs; rhs; body } in - { e; typ; span = Span.union rhs.span body.span }) - in + | Block { expr; span; stmts; _ } -> + let { e; _ } = c_block ~expr ~span ~stmts ~ty:e.ty in e | Assign { lhs; rhs } -> let lhs = c_expr lhs in From bc2fa68b6fd5d793ce58ad375c2d2f9a34efe750 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Wed, 17 Jul 2024 15:54:43 +0200 Subject: [PATCH 2/2] Add test for let-else. --- .../toolchain__let-else into-coq.snap | 55 +++++++++++++ .../toolchain__let-else into-fstar.snap | 45 +++++++++++ .../toolchain__let-else into-ssprove.snap | 80 +++++++++++++++++++ tests/Cargo.lock | 4 + tests/Cargo.toml | 1 + tests/let-else/Cargo.toml | 9 +++ tests/let-else/src/lib.rs | 13 +++ 7 files changed, 207 insertions(+) create mode 100644 test-harness/src/snapshots/toolchain__let-else into-coq.snap create mode 100644 test-harness/src/snapshots/toolchain__let-else into-fstar.snap create mode 100644 test-harness/src/snapshots/toolchain__let-else into-ssprove.snap create mode 100644 tests/let-else/Cargo.toml create mode 100644 tests/let-else/src/lib.rs diff --git a/test-harness/src/snapshots/toolchain__let-else into-coq.snap b/test-harness/src/snapshots/toolchain__let-else into-coq.snap new file mode 100644 index 000000000..85110e910 --- /dev/null +++ b/test-harness/src/snapshots/toolchain__let-else into-coq.snap @@ -0,0 +1,55 @@ +--- +source: test-harness/src/harness.rs +expression: snapshot +info: + kind: + Translate: + backend: coq + info: + name: let-else + manifest: let-else/Cargo.toml + description: ~ + spec: + optional: false + broken: false + issue_id: ~ + positive: true + snapshot: + stderr: false + stdout: true + include_flag: ~ + backend_options: ~ +--- +exit = 0 + +[stdout] +diagnostics = [] + +[stdout.files] +"Let_else.v" = ''' +(* File automatically generated by Hacspec *) +From Hacspec Require Import Hacspec_Lib MachineIntegers. +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. + +(*Not implemented yet? todo(item)*) + +Definition let_else (opt : t_Option_t int32) : bool := + run match opt with + | Option_Some x => + ControlFlow_Continue true + | _ => + ControlFlow_Break false + end. + +Definition let_else_different_type (opt : t_Option_t int32) : bool := + run (let hoist1 := match opt with + | Option_Some x => + ControlFlow_Continue (Option_Some (x.+(@repr WORDSIZE32 1))) + | _ => + ControlFlow_Break false + end : t_Option_t int32 in + ControlFlow_Continue (let_else hoist1)). +''' diff --git a/test-harness/src/snapshots/toolchain__let-else into-fstar.snap b/test-harness/src/snapshots/toolchain__let-else into-fstar.snap new file mode 100644 index 000000000..44ed74878 --- /dev/null +++ b/test-harness/src/snapshots/toolchain__let-else into-fstar.snap @@ -0,0 +1,45 @@ +--- +source: test-harness/src/harness.rs +expression: snapshot +info: + kind: + Translate: + backend: fstar + info: + name: let-else + manifest: let-else/Cargo.toml + description: ~ + spec: + optional: false + broken: false + issue_id: ~ + positive: true + snapshot: + stderr: false + stdout: true + include_flag: ~ + backend_options: ~ +--- +exit = 0 + +[stdout] +diagnostics = [] + +[stdout.files] +"Let_else.fst" = ''' +module Let_else +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +let let_else (opt: Core.Option.t_Option u32) : bool = + match opt with + | Core.Option.Option_Some x -> true + | _ -> false + +let let_else_different_type (opt: Core.Option.t_Option u32) : bool = + match opt with + | Core.Option.Option_Some x -> + let_else (Core.Option.Option_Some (x +! 1ul <: u32) <: Core.Option.t_Option u32) + | _ -> false +''' diff --git a/test-harness/src/snapshots/toolchain__let-else into-ssprove.snap b/test-harness/src/snapshots/toolchain__let-else into-ssprove.snap new file mode 100644 index 000000000..3fe94349f --- /dev/null +++ b/test-harness/src/snapshots/toolchain__let-else into-ssprove.snap @@ -0,0 +1,80 @@ +--- +source: test-harness/src/harness.rs +expression: snapshot +info: + kind: + Translate: + backend: ssprove + info: + name: let-else + manifest: let-else/Cargo.toml + description: ~ + spec: + optional: false + broken: false + issue_id: ~ + positive: true + snapshot: + stderr: false + stdout: true + include_flag: ~ + backend_options: ~ +--- +exit = 0 + +[stdout] +diagnostics = [] + +[stdout.files] +"Let_else.v" = ''' +(* File automatically generated by Hacspec *) +Set Warnings "-notation-overridden,-ambiguous-paths". +From Crypt Require Import choice_type Package Prelude. +Import PackageNotation. +From extructures Require Import ord fset. +From mathcomp Require Import word_ssrZ word. +From Jasmin Require Import word. + +From Coq Require Import ZArith. +From Coq Require Import Strings.String. +Import List.ListNotations. +Open Scope list_scope. +Open Scope Z_scope. +Open Scope bool_scope. + +From Hacspec Require Import ChoiceEquality. +From Hacspec Require Import LocationUtility. +From Hacspec Require Import Hacspec_Lib_Comparable. +From Hacspec Require Import Hacspec_Lib_Pre. +From Hacspec Require Import Hacspec_Lib. + +Open Scope hacspec_scope. +Import choice.Choice.Exports. + +Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations. + +(*Not implemented yet? todo(item)*) + +Equations let_else {L1 : {fset Location}} {I1 : Interface} (opt : both L1 I1 (t_Option int32)) : both L1 I1 'bool := + let_else opt := + solve_lift (run (matchb opt with + | Option_Some_case x => + letb x := ret_both ((x) : (int32)) in + ControlFlow_Continue (solve_lift (ret_both (true : 'bool))) + | _ => + ControlFlow_Break (solve_lift (ret_both (false : 'bool))) + end)) : both L1 I1 'bool. +Fail Next Obligation. + +Equations let_else_different_type {L1 : {fset Location}} {I1 : Interface} (opt : both L1 I1 (t_Option int32)) : both L1 I1 'bool := + let_else_different_type opt := + solve_lift (run (letm[choice_typeMonad.result_bind_code 'bool] hoist1 := matchb opt with + | Option_Some_case x => + letb x := ret_both ((x) : (int32)) in + ControlFlow_Continue (Option_Some (solve_lift (x .+ (ret_both (1 : int32))))) + | _ => + ControlFlow_Break (solve_lift (ret_both (false : 'bool))) + end in + ControlFlow_Continue (let_else hoist1))) : both L1 I1 'bool. +Fail Next Obligation. +''' diff --git a/tests/Cargo.lock b/tests/Cargo.lock index fe5e3ca74..faa17b103 100644 --- a/tests/Cargo.lock +++ b/tests/Cargo.lock @@ -415,6 +415,10 @@ version = "1.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" +[[package]] +name = "let-else" +version = "0.1.0" + [[package]] name = "libc" version = "0.2.147" diff --git a/tests/Cargo.toml b/tests/Cargo.toml index 8142bf4a4..ce7f7c898 100644 --- a/tests/Cargo.toml +++ b/tests/Cargo.toml @@ -5,6 +5,7 @@ members = [ "slices", "naming", "if-let", + "let-else", "enum-repr", "pattern-or", "side-effects", diff --git a/tests/let-else/Cargo.toml b/tests/let-else/Cargo.toml new file mode 100644 index 000000000..bb5cd3d8b --- /dev/null +++ b/tests/let-else/Cargo.toml @@ -0,0 +1,9 @@ +[package] +name = "let-else" +version = "0.1.0" +edition = "2021" + +[dependencies] + +[package.metadata.hax-tests] +into."fstar+coq+ssprove" = { broken = false, snapshot = "stdout", issue_id = "155" } diff --git a/tests/let-else/src/lib.rs b/tests/let-else/src/lib.rs new file mode 100644 index 000000000..c040d1c07 --- /dev/null +++ b/tests/let-else/src/lib.rs @@ -0,0 +1,13 @@ +#![allow(dead_code)] + +pub fn let_else(opt: Option) -> bool { + let Some(x) = opt else { return false }; + true +} + +pub fn let_else_different_type(opt: Option) -> bool { + let_else({ + let Some(x) = opt else { return false }; + Some(x + 1) + }) +}