From 65c8f5bcf1a0641ac1394527d5b7755366b74432 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 18 Jan 2024 15:10:15 +0100 Subject: [PATCH] doc(engine/phases/question-marks): add some documentation --- engine/lib/ast.ml | 10 +- .../phase_reconstruct_question_marks.ml | 32 +++-- .../phase_reconstruct_question_marks.mli | 24 ++++ engine/lib/utils.ml | 2 + .../toolchain__side-effects into-fstar.snap | 113 +++++++++++------- tests/side-effects/src/lib.rs | 35 ++++-- 6 files changed, 135 insertions(+), 81 deletions(-) diff --git a/engine/lib/ast.ml b/engine/lib/ast.ml index 0b5744f90..ff6fd5a8b 100644 --- a/engine/lib/ast.ml +++ b/engine/lib/ast.ml @@ -346,12 +346,10 @@ functor (* ControlFlow *) | Break of { e : expr; label : string option; witness : F.break * F.loop } | Return of { e : expr; witness : F.early_exit } - | QuestionMark of { - e : expr; - return_typ : ty; - (** [converted_typ] is the converted type: when you do [e?], a convertion might be inserted by Rust on the fly (e.g. [Something::from_residual(e)]) *) - witness : F.question_mark; - } + | QuestionMark of { e : expr; return_typ : ty; witness : F.question_mark } + (** The expression `e?`. In opposition to Rust, no implicit + coercion is applied on the (potential) error payload of + `e`. Coercion should be made explicit within `e`. *) | Continue of { e : (F.state_passing_loop * expr) option; label : string option; diff --git a/engine/lib/phases/phase_reconstruct_question_marks.ml b/engine/lib/phases/phase_reconstruct_question_marks.ml index f4ab3c72a..c2bf99dff 100644 --- a/engine/lib/phases/phase_reconstruct_question_marks.ml +++ b/engine/lib/phases/phase_reconstruct_question_marks.ml @@ -30,12 +30,10 @@ module%inlined_contents Make (FA : Features.T) = struct open A + (** The types supported for [e] in a [e?] expression *) type qm_kind = QMResult of { success : ty; error : ty } | QMOption of ty - let return_typ_of_qm_kind = function - | QMResult { error; _ } -> error - | QMOption _ -> UA.unit_typ - + (** Interpret a type [t] as a [qm_kind] *) let qm_kind_of_typ span (t : ty) : qm_kind = let is_result = Global_ident.eq_name Core__result__Result in let is_option = Global_ident.eq_name Core__option__Option in @@ -49,19 +47,9 @@ module%inlined_contents Make (FA : Features.T) = struct got: " ^ [%show: ty] t) - type t = { - start : expr; - end_ : expr; - var : local_ident; - var_typ : ty; - body : expr; - state : loop_state option; - label : string option; - witness : FA.loop; - } - [@@deriving show] - - (** expect residual impl result 27 *) + (** Expects [impl] to be an impl. expr. for the trait + `std::ops::FromResidual` for the type [Result<_, _>], and + extract its parent [From] impl expr *) let expect_residual_impl_result (impl : impl_expr) : impl_expr option = match impl with | ImplApp @@ -70,6 +58,7 @@ module%inlined_contents Make (FA : Features.T) = struct Some from_impl | _ -> None + (** Expects [t] to be [Result], and returns [(S, E)] *) let expect_result_type (t : ty) : (ty * ty) option = match t with | TApp { ident; args = [ GType s; GType e ] } @@ -77,11 +66,12 @@ module%inlined_contents Make (FA : Features.T) = struct Some (s, e) | _ -> None + (** Construct [Result] *) let make_result_type (success : ty) (error : ty) : ty = let ident = Global_ident.of_name Type Core__result__Result in TApp { ident; args = [ GType success; GType error ] } - (** Retype a `Err::<_, E>(x)` literal, as `Err::(x)` *) + (** Retype a [Err::<_, E>(x)] literal, as [Err::(x)] *) let retype_err_literal (e : expr) (success : ty) (error : ty) = match e.e with | Construct { constructor; _ } @@ -89,6 +79,9 @@ module%inlined_contents Make (FA : Features.T) = struct { e with typ = make_result_type success error } | _ -> e + (** [map_err e error_dest impl] creates the expression + [e.map_err(from)] with the proper types and impl + informations. *) let map_err (e : expr) (error_dest : ty) impl : expr option = let* success, error_src = expect_result_type e.typ in let* impl = expect_residual_impl_result impl in @@ -103,6 +96,9 @@ module%inlined_contents Make (FA : Features.T) = struct in Some call + (** [extract e] returns [Some (x, ty)] if [e] was a `y?` + desugared by rustc. `y` is `x` plus possibly a coercion. [ty] is + the return type of the function. *) let extract (e : expr) : (expr * ty) option = let extract_return (e : expr) = match e.e with diff --git a/engine/lib/phases/phase_reconstruct_question_marks.mli b/engine/lib/phases/phase_reconstruct_question_marks.mli index 4d94add95..16c135311 100644 --- a/engine/lib/phases/phase_reconstruct_question_marks.mli +++ b/engine/lib/phases/phase_reconstruct_question_marks.mli @@ -1,9 +1,33 @@ +(** In THIR, there are no construct for question marks. Instead, Rustc +desugars `e?` into the following: + +{@rust[ +match core::ops::try_trait::branch(y) { + core::ops::control_flow::Break(residual) => { + never_to_any( + {return core::ops::try_trait::from_residual(residual)}, + ) + } + core::ops::control_flow::Continue(val) => val, +}) +]} + +This phase does the opposite rewrite. + +While `e?` in Rust might implies an implicit coercion, in our AST, a +question mark is expected to already be of the right type. This phase +inlines a coercion (of the shape `x.map_err(from)`, in the case of a +`Result`). +*) + open! Prelude +(** This phase can be applied to any feature set. *) module Make (F : Features.T) : sig include module type of struct module FA = F + (** This phase outputs an AST with question marks. *) module FB = struct include F include Features.On.Question_mark diff --git a/engine/lib/utils.ml b/engine/lib/utils.ml index 5aaa123a0..0222ff516 100644 --- a/engine/lib/utils.ml +++ b/engine/lib/utils.ml @@ -23,6 +23,8 @@ let tup2 a b = (a, b) let ( let* ) x f = Option.bind ~f x let some_if_true = function true -> Some () | _ -> None +(** [let*? () = guard in body] acts as a guard: if [guard] holds, then +[body] is executed, otherwise [None] is returned. *) let ( let*? ) (type a) (x : bool) (f : unit -> a option) = let* () = some_if_true x in f () diff --git a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap index f209e65a9..cea3bad93 100644 --- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap @@ -18,10 +18,45 @@ info: stderr: true stdout: true --- -exit = 0 +exit = 101 stderr = ''' Compiling side-effects v0.1.0 (WORKSPACE_ROOT/side-effects) - Finished dev [unoptimized + debuginfo] target(s) in XXs''' +error[E0428]: the name `direct_result_1` is defined multiple times + --> side-effects/src/lib.rs:73:1 + | +67 | fn direct_result_1(y: Result<(), u32>) -> Result { + | --------------------------------------------------------- previous definition of the value `direct_result_1` here +... +73 | fn direct_result_1(y: Result) -> Result { + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ `direct_result_1` redefined here + | + = note: `direct_result_1` must be defined only once in the value namespace of this module + +error[E0061]: this enum variant takes 1 argument but 0 arguments were supplied + --> side-effects/src/lib.rs:69:5 + | +69 | Ok() + | ^^-- an argument of type `i8` is missing + | +note: tuple variant defined here + --> /nix/store/bax026mb31q65yyh0c2jrwx5xynkhhs4-rust-default-1.72.0-nightly-2023-06-02/lib/rustlib/src/rust/library/core/src/result.rs:506:5 + | +506 | Ok(#[stable(feature = "rust1", since = "1.0.0")] T), + | ^^ +help: provide the argument + | +69 | Ok(/* i8 */) + | ~~~~~~~~~~ + +error: While trying to reach a body's THIR defintion, got a typechecking error. + --> side-effects/src/lib.rs:67:1 + | +67 | fn direct_result_1(y: Result<(), u32>) -> Result { + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +Some errors have detailed explanations: E0061, E0428. +For more information about an error, try `rustc --explain E0061`. +error: could not compile `side-effects` (lib) due to 3 previous errors''' [stdout] diagnostics = [] @@ -36,22 +71,18 @@ open FStar.Mul let add3 (x y z: u32) : u32 = Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add x y <: u32) z -let direct_result_1_ (y: Core.Result.t_Result i8 u32) : Core.Result.t_Result i8 u32 = +let direct_result_1_ (_: Prims.unit) : Rust_primitives.Hax.t_Never = + Rust_primitives.Hax.failure "(AST import) Fatal error: something we considered as impossible occurred! Please report this by submitting an issue on GitHub!\nDetails: [import_thir:literal] got an error literal: this means the Rust compiler or Hax's frontend probably reported errors above.\n" + "{ Types.attributes = [];\n contents =\n Types.Literal {\n lit =\n { Types.node = Types.Err;\n span =\n { Types.filename =\n (Types.Real (Types.LocalPath \"side-effects/src/lib.rs\"));\n hi = { Types.col = \"0\"; line = \"1\" };\n lo = { Types.col = \"0\"; line = \"1\" } }\n };\n neg = false};\n hir_id = None;\n span =\n { Types.filename = (Types.Real (Types.LocalPath \"side-effects/src/lib.rs\"));\n hi = { Types.col = \"57\"; line = \"67\" };\n lo = { Types.col = \"0\"; line = \"67\" } };\n ty = Types.Never }" + +let direct_result_1_1 (y: Core.Result.t_Result i8 u16) : Core.Result.t_Result i8 u32 = Rust_primitives.Hax.Control_flow_monad.Mresult.run (let| hoist1:i8 = - Core.Result.impl__map_err y (Core.Convert.f_from <: u32 -> u32) + Core.Result.impl__map_err y (Core.Convert.f_from <: u16 -> u32) in Core.Result.Result_Ok (Core.Result.Result_Ok hoist1 <: Core.Result.t_Result i8 u32) <: Core.Result.t_Result (Core.Result.t_Result i8 u32) u32) -let direct_result_2_ (y: Core.Result.t_Result Prims.unit u32) : Core.Result.t_Result i8 u32 = - Rust_primitives.Hax.Control_flow_monad.Mresult.run (let| _:Prims.unit = - Core.Result.impl__map_err y (Core.Convert.f_from <: u32 -> u32) - in - Core.Result.Result_Ok (Core.Result.Result_Ok 1y <: Core.Result.t_Result i8 u32) - <: - Core.Result.t_Result (Core.Result.t_Result i8 u32) u32) - let early_returns (x: u32) : u32 = Rust_primitives.Hax.Control_flow_monad.Mexception.run (let! _:Prims.unit = if x >. 3ul @@ -96,20 +127,6 @@ let early_returns (x: u32) : u32 = <: Core.Ops.Control_flow.t_ControlFlow u32 u32) -let into_err (x: u8) : Core.Result.t_Result u8 u64 = - Rust_primitives.Hax.Control_flow_monad.Mresult.run (let| _:Prims.unit = - if x >. 200uy - then - Core.Result.impl__map_err (Core.Result.Result_Err x <: Core.Result.t_Result Prims.unit u8) - (Core.Convert.f_from <: u8 -> u64) - else Core.Result.Result_Ok () <: Core.Result.t_Result Prims.unit u64 - in - Core.Result.Result_Ok - (Core.Result.Result_Ok (Core.Num.impl__u8__wrapping_add x 54uy) <: Core.Result.t_Result u8 u64 - ) - <: - Core.Result.t_Result (Core.Result.t_Result u8 u64) u64) - let local_mutation (x: u32) : u32 = let y:u32 = 0ul in let x:u32 = Core.Num.impl__u32__wrapping_add x 1ul in @@ -232,27 +249,35 @@ type t_Bar = { f_b:(t_Array (bool & bool) (sz 6) & bool) } -let monad_lifting (_: Prims.unit) : Core.Result.t_Result t_A t_B = - Rust_primitives.Hax.Control_flow_monad.Mexception.run (let! hoist33:t_A = - Core.Ops.Control_flow.ControlFlow_Continue - (Core.Result.impl__map_err (Core.Result.Result_Err (B <: t_B) - <: - Core.Result.t_Result t_A t_B) - (Core.Convert.f_from <: t_B -> t_B)) +let monad_lifting (x: u8) : Core.Result.t_Result t_A t_B = + Rust_primitives.Hax.Control_flow_monad.Mexception.run (if x >. 123uy <: bool + then + let! hoist33:t_A = + Core.Ops.Control_flow.ControlFlow_Continue + (Core.Result.impl__map_err (Core.Result.Result_Err (B <: t_B) + <: + Core.Result.t_Result t_A t_B) + (Core.Convert.f_from <: t_B -> t_B)) + <: + Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result t_A t_B) + (Core.Result.t_Result t_A t_B) + in + let hoist34:Core.Result.t_Result t_A t_B = + Core.Result.Result_Ok hoist33 <: Core.Result.t_Result t_A t_B + in + let! hoist35:Rust_primitives.Hax.t_Never = + Core.Ops.Control_flow.ControlFlow.v_Break hoist34 + in + Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist35) <: Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result t_A t_B) (Core.Result.t_Result t_A t_B) - in - let hoist34:Core.Result.t_Result t_A t_B = - Core.Result.Result_Ok hoist33 <: Core.Result.t_Result t_A t_B - in - let! hoist35:Rust_primitives.Hax.t_Never = - Core.Ops.Control_flow.ControlFlow.v_Break hoist34 - in - Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist35) - <: - Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result t_A t_B) - (Core.Result.t_Result t_A t_B)) + else + Core.Ops.Control_flow.ControlFlow_Continue + (Core.Result.Result_Ok (A <: t_A) <: Core.Result.t_Result t_A t_B) + <: + Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result t_A t_B) + (Core.Result.t_Result t_A t_B)) type t_Foo = { f_x:bool; diff --git a/tests/side-effects/src/lib.rs b/tests/side-effects/src/lib.rs index dd0916b03..677f86fc2 100644 --- a/tests/side-effects/src/lib.rs +++ b/tests/side-effects/src/lib.rs @@ -1,8 +1,11 @@ #![allow(dead_code)] + +/// Helper function fn add3(x: u32, y: u32, z: u32) -> u32 { x.wrapping_add(y).wrapping_add(z) } +/// Exercise local mutation with control flow and loops fn local_mutation(mut x: u32) -> u32 { let mut y = 0; if { @@ -39,6 +42,7 @@ fn local_mutation(mut x: u32) -> u32 { } } +/// Exercise early returns with control flow and loops fn early_returns(mut x: u32) -> u32 { return (123u32.wrapping_add( if { @@ -59,14 +63,18 @@ fn early_returns(mut x: u32) -> u32 { .wrapping_add(x); } -fn direct_result_1(y: Result) -> Result { - Ok(y?) -} -fn direct_result_2(y: Result<(), u32>) -> Result { +/// Question mark without error coercion +fn direct_result_1(y: Result<(), u32>) -> Result { y?; - Ok(1) + Ok() +} + +/// Question mark with an error coercion +fn direct_result_1(y: Result) -> Result { + Ok(y?) } +/// Test question mark on `Option`s with some control flow fn options(x: Option, y: Option, z: Option) -> Option { let v = match (if x? > 10 { Some(x?.wrapping_add(3)) @@ -80,6 +88,7 @@ fn options(x: Option, y: Option, z: Option) -> Option { Some(v.wrapping_add(x?).wrapping_add(y?)) } +/// Test question mark on `Result`s with local mutation fn question_mark(mut x: u32) -> Result { if x > 40u32 { let mut y = 0; @@ -98,15 +107,13 @@ fn question_mark(mut x: u32) -> Result { struct A; struct B; -fn monad_lifting() -> Result { - return Ok(Err(B)?); -} - -fn into_err(x: u8) -> Result { - if x > 200 { - Err(x)? +/// Combine `?` and early return +fn monad_lifting(x: u8) -> Result { + if x > 123 { + return Ok(Err(B)?); + } else { + Ok(A) } - Ok(x.wrapping_add(54)) } struct Bar { @@ -119,6 +126,8 @@ struct Foo { z: [Bar; 6], bar: Bar, } + +/// Test assignation on non-trivial places fn assign_non_trivial_lhs(mut foo: Foo) -> Foo { foo.x = true; foo.bar.a = true;