From 25e302b07ee5adb10601b834585d7e1933892a65 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 7 Mar 2024 15:37:22 +0100 Subject: [PATCH 01/12] fix(engine/phases): DropSizedTrait: fix `phase_id` --- engine/lib/diagnostics.ml | 1 + engine/lib/phases/phase_drop_sized_trait.ml | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/engine/lib/diagnostics.ml b/engine/lib/diagnostics.ml index 4967e93ae..26b3075b0 100644 --- a/engine/lib/diagnostics.ml +++ b/engine/lib/diagnostics.ml @@ -28,6 +28,7 @@ module Phase = struct | Identity | DropReferences | DropBlocks + | DropSizedTrait | RefMut | ResugarForLoops | ResugarWhileLoops diff --git a/engine/lib/phases/phase_drop_sized_trait.ml b/engine/lib/phases/phase_drop_sized_trait.ml index 2ed404b2f..569e0ce70 100644 --- a/engine/lib/phases/phase_drop_sized_trait.ml +++ b/engine/lib/phases/phase_drop_sized_trait.ml @@ -4,7 +4,7 @@ module Make (F : Features.T) = Phase_utils.MakeMonomorphicPhase (F) (struct - let phase_id = Diagnostics.Phase.TraitsSpecs + let phase_id = Diagnostics.Phase.DropSizedTrait open Ast.Make (F) module U = Ast_utils.Make (F) From f584861a3acc70307d03d90affb34ef6995a1e4f Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 7 Mar 2024 15:38:18 +0100 Subject: [PATCH 02/12] feat(engine/phases): intro `drop_needless_returns` --- engine/lib/phases.ml | 1 + .../lib/phases/phase_drop_needless_returns.ml | 48 +++++++++++++++++++ .../phases/phase_drop_needless_returns.mli | 4 ++ 3 files changed, 53 insertions(+) create mode 100644 engine/lib/phases/phase_drop_needless_returns.ml create mode 100644 engine/lib/phases/phase_drop_needless_returns.mli diff --git a/engine/lib/phases.ml b/engine/lib/phases.ml index 2f2982243..2b7f30f45 100644 --- a/engine/lib/phases.ml +++ b/engine/lib/phases.ml @@ -11,4 +11,5 @@ module Functionalize_loops = Phase_functionalize_loops.Make module Reject = Phase_reject module Local_mutation = Phase_local_mutation.Make module Traits_specs = Phase_traits_specs.Make +module Drop_needless_returns = Phase_drop_needless_returns.Make module Drop_sized_trait = Phase_drop_sized_trait.Make diff --git a/engine/lib/phases/phase_drop_needless_returns.ml b/engine/lib/phases/phase_drop_needless_returns.ml new file mode 100644 index 000000000..e4a59355e --- /dev/null +++ b/engine/lib/phases/phase_drop_needless_returns.ml @@ -0,0 +1,48 @@ +open! Prelude + +module Make (F : Features.T) = + Phase_utils.MakeMonomorphicPhase + (F) + (struct + let phase_id = Diagnostics.Phase.DropNeedlessReturns + + open Ast.Make (F) + module U = Ast_utils.Make (F) + module Visitors = Ast_visitors.Make (F) + + module Error = Phase_utils.MakeError (struct + let ctx = Diagnostics.Context.Phase phase_id + end) + + let visitor = + object (self) + inherit [_] Visitors.map as _super + + method! visit_expr () e = + match e with + | { e = Return { e; _ }; _ } -> e + (* we know [e] is on an exit position: the return is + thus useless, we can skip it *) + | { e = Let { monadic = None; lhs; rhs; body }; _ } -> + let body = self#visit_expr () body in + { e with e = Let { monadic = None; lhs; rhs; body } } + (* If a let expression is an exit node, then it's body + is as well *) + | { e = Match { scrutinee; arms }; _ } -> + let arms = List.map ~f:(self#visit_arm ()) arms in + { e with e = Match { scrutinee; arms } } + | { e = If { cond; then_; else_ }; _ } -> + let then_ = self#visit_expr () then_ in + let else_ = Option.map ~f:(self#visit_expr ()) else_ in + { e with e = If { cond; then_; else_ } } + | _ -> e + (** The invariant here is that [visit_expr] is called only + on expressions that are on exit positions. [visit_expr] + is first called on root expressions, which are (by + definition) exit nodes. Then, [visit_expr] itself makes + recursive calls to sub expressions that are themselves + in exit nodes. **) + end + + let ditems = List.map ~f:(visitor#visit_item ()) + end) diff --git a/engine/lib/phases/phase_drop_needless_returns.mli b/engine/lib/phases/phase_drop_needless_returns.mli new file mode 100644 index 000000000..b53603f1e --- /dev/null +++ b/engine/lib/phases/phase_drop_needless_returns.mli @@ -0,0 +1,4 @@ +(** This phase transforms `return e` expressions into `e` when `return +e` is on an exit position. *) + +module Make : Phase_utils.UNCONSTRAINTED_MONOMORPHIC_PHASE From d8c35655e420f471e4e9a3ecde9dba1ba35cf413 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 7 Mar 2024 16:52:33 +0100 Subject: [PATCH 03/12] feat(engine/phases): intro `simplify_question_marks` --- engine/lib/diagnostics.ml | 1 + engine/lib/phases.ml | 1 + .../phases/phase_simplify_question_marks.ml | 302 ++++++++++++++++++ .../phases/phase_simplify_question_marks.mli | 42 +++ 4 files changed, 346 insertions(+) create mode 100644 engine/lib/phases/phase_simplify_question_marks.ml create mode 100644 engine/lib/phases/phase_simplify_question_marks.mli diff --git a/engine/lib/diagnostics.ml b/engine/lib/diagnostics.ml index 26b3075b0..46ca9d02b 100644 --- a/engine/lib/diagnostics.ml +++ b/engine/lib/diagnostics.ml @@ -34,6 +34,7 @@ module Phase = struct | ResugarWhileLoops | ResugarForIndexLoops | ResugarQuestionMarks + | SimplifyQuestionMarks | HoistSideEffects | LocalMutation | TrivializeAssignLhs diff --git a/engine/lib/phases.ml b/engine/lib/phases.ml index 2b7f30f45..24870e141 100644 --- a/engine/lib/phases.ml +++ b/engine/lib/phases.ml @@ -5,6 +5,7 @@ module Drop_blocks = Phase_drop_blocks.Make module Reconstruct_for_loops = Phase_reconstruct_for_loops.Make module Reconstruct_while_loops = Phase_reconstruct_while_loops.Make module Reconstruct_question_marks = Phase_reconstruct_question_marks.Make +module Simplify_question_marks = Phase_simplify_question_marks.Make module Trivialize_assign_lhs = Phase_trivialize_assign_lhs.Make module Cf_into_monads = Phase_cf_into_monads.Make module Functionalize_loops = Phase_functionalize_loops.Make diff --git a/engine/lib/phases/phase_simplify_question_marks.ml b/engine/lib/phases/phase_simplify_question_marks.ml new file mode 100644 index 000000000..4182a43d2 --- /dev/null +++ b/engine/lib/phases/phase_simplify_question_marks.ml @@ -0,0 +1,302 @@ +open! Prelude + +module%inlined_contents Make (FA : Features.T) = struct + open Ast + + module FB = struct + include FA + include Features.On.Question_mark + end + + include + Phase_utils.MakeBase (FA) (FB) + (struct + let phase_id = Diagnostics.Phase.ResugarQuestionMarks + end) + + module Implem : ImplemT.T = struct + let metadata = metadata + + module UA = Ast_utils.Make (FA) + module UB = Ast_utils.Make (FB) + + module S = struct + include Features.SUBTYPE.Id + include Features.SUBTYPE.On.Question_mark + end + + module QuestionMarks = struct + [@@@warning "-9"] + + open A + + (** The types supported for [e] in a [e?] expression *) + type qm_kind = QMResult of { success : ty; error : ty } | QMOption of ty + + (** 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 + match t with + | TApp { ident; args = [ GType s; GType e ] } when is_result ident -> + QMResult { success = s; error = e } + | TApp { ident; args = [ GType s ] } when is_option ident -> QMOption s + | _ -> + Error.assertion_failure span + ("expected something of type Option<_> or Result<_, _>, instead, \ + got: " + ^ [%show: ty] t) + + (** 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 + { impl = Concrete { trait; _ }; args = [ _; _; _; from_impl ] } + when Concrete_ident.eq_name Core__result__Impl_27 trait -> + 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 ] } + when Global_ident.eq_name Core__result__Result ident -> + 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)] *) + let retype_err_literal (e : expr) (success : ty) (error : ty) = + match e.e with + | Construct { constructor; _ } + when Global_ident.eq_name Core__result__Result__Err constructor -> + { e with typ = make_result_type success error } + | _ -> e + + let convert_from (e : expr) (error_dest : ty) impl : expr option = + let error_src = e.typ in + let* impl = expect_residual_impl_result impl in + let*? _ = [%eq: ty] error_src error_dest |> not in + let from_typ = TArrow ([ error_src ], error_dest) in + Some + (UA.call ~kind:(AssociatedItem Value) ~impl Core__convert__From__from + [ e ] e.span from_typ) + + (** [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 + let from_typ = TArrow ([ error_src ], error_dest) in + let from = + UA.call ~kind:(AssociatedItem Value) ~impl Core__convert__From__from + [] e.span from_typ + in + let call = + UA.call Core__result__Impl__map_err [ e; from ] e.span + (make_result_type success error_dest) + in + Some call + + let mk_pconstruct ~is_struct ~is_record ~span ~typ + (constructor : Concrete_ident_generated.name) + (fields : (Concrete_ident_generated.name * pat) list) = + let name = + Global_ident.of_name (Constructor { is_struct }) constructor + in + let args = + List.map + ~f:(fun (field, pat) -> + let field = Global_ident.of_name Field field in + { field; pat }) + fields + in + let p = PConstruct { name; args; is_record; is_struct } in + { p; span; typ } + + (** [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 option = + let extract_return (e : expr) = + match e.e with + | Return + { + e = + { + e = + App + { + f = { e = GlobalVar f }; + args = [ { e = LocalVar residual_var; _ } ]; + impl = Some impl; + }; + typ = return_typ; + _; + }; + witness; + } -> + Some (f, residual_var, return_typ, impl, witness) + | _ -> None + in + let extract_pat_app_bd (p : pat) : (global_ident * local_ident) option = + match p.p with + | PConstruct + { + name; + args = + [ + { + pat = + { + p = + PBinding { mut = Immutable; var; subpat = None; _ }; + _; + }; + _; + }; + ]; + _; + } -> + Some (name, var) + | _ -> None + in + match e.e with + | Match + { + scrutinee = + { e = App { f = { e = GlobalVar n; _ }; args = [ expr ] }; _ }; + arms = + [ + { arm = { arm_pat = pat_break; body }; _ }; + { + arm = + { + arm_pat = pat_continue; + body = { e = LocalVar continue_var; _ }; + }; + _; + }; + ]; + } + when Global_ident.eq_name Core__ops__try_trait__Try__branch n -> + let* body = + UA.Expect.concrete_app1 Rust_primitives__hax__never_to_any body + in + let* f, residual_var, fun_return_typ, residual_impl, return_witness + = + extract_return body + in + let* f_break, residual_var' = extract_pat_app_bd pat_break in + let* f_continue, continue_var' = extract_pat_app_bd pat_continue in + let*? _ = [%equal: local_ident] residual_var residual_var' in + let*? _ = [%equal: local_ident] continue_var continue_var' in + let*? _ = + Global_ident.eq_name Core__ops__control_flow__ControlFlow__Break + f_break + && Global_ident.eq_name + Core__ops__control_flow__ControlFlow__Continue f_continue + && Global_ident.eq_name + Core__ops__try_trait__FromResidual__from_residual f + in + let kind = qm_kind_of_typ e.span in + let span = expr.span in + let mk_var name : local_ident = + { name; id = Local_ident.mk_id Expr (-1) } + in + let mk_cons = + mk_pconstruct ~is_struct:false ~is_record:false ~span + ~typ:expr.typ + in + let expr = + match (kind expr.typ, kind fun_return_typ) with + | ( QMResult { error = local_err; success = local_success }, + QMResult { error = return_err; _ } ) -> + let var_ok, var_err = (mk_var "ok", mk_var "err") in + let arm_ok : A.arm = + let pat = UA.make_var_pat var_ok local_success span in + let arm_pat = + mk_cons Core__result__Result__Ok + [ (Core__result__Result__Ok__0, pat) ] + in + let body = + { typ = local_success; e = LocalVar var_ok; span } + in + { arm = { arm_pat; body }; span } + in + let arm_err = + let pat = UA.make_var_pat var_err local_err span in + let arm_pat = + mk_cons Core__result__Result__Err + [ (Core__result__Result__Err__0, pat) ] + in + let err = { typ = local_err; e = LocalVar var_err; span } in + let err = + convert_from err return_err residual_impl + |> Option.value ~default:err + in + let err = + UA.call_Constructor Core__result__Result__Err false + [ err ] e.span fun_return_typ + in + let e = Return { e = err; witness = return_witness } in + let return = { typ = local_success; e; span } in + { arm = { arm_pat; body = return }; span } + in + let arms, typ = ([ arm_ok; arm_err ], local_success) in + { e = Match { scrutinee = expr; arms }; typ; span } + | QMOption local_success, QMOption _ -> + let var_some = mk_var "some" in + let arm_some : A.arm = + let pat = UA.make_var_pat var_some local_success span in + let arm_pat = + mk_cons Core__option__Option__Some + [ (Core__option__Option__Some__0, pat) ] + in + let body = + { typ = local_success; e = LocalVar var_some; span } + in + { arm = { arm_pat; body }; span } + in + let arm_none = + let arm_pat = mk_cons Core__option__Option__None [] in + let none = + UA.call_Constructor Core__option__Option__None false [] + e.span fun_return_typ + in + let e = Return { e = none; witness = return_witness } in + let return = { typ = local_success; e; span } in + { arm = { arm_pat; body = return }; span } + in + let arms, typ = ([ arm_some; arm_none ], local_success) in + { e = Match { scrutinee = expr; arms }; typ; span } + | _ -> + Error.assertion_failure e.span + "expected expr.typ and fun_return_typ to be both Options \ + or both Results" + in + Some expr + | _ -> None + end + + [%%inline_defs dmutability] + + let rec dexpr_unwrapped (expr : A.expr) : B.expr = + QuestionMarks.extract expr |> Option.value ~default:expr + |> [%inline_body dexpr_unwrapped] + [@@inline_ands bindings_of dexpr] + + [%%inline_defs "Item.*"] + end + + include Implem + module FA = FA +end +[@@add "subtype.ml"] diff --git a/engine/lib/phases/phase_simplify_question_marks.mli b/engine/lib/phases/phase_simplify_question_marks.mli new file mode 100644 index 000000000..16c135311 --- /dev/null +++ b/engine/lib/phases/phase_simplify_question_marks.mli @@ -0,0 +1,42 @@ +(** 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 + end + + module A = Ast.Make (F) + module B = Ast.Make (FB) + module ImplemT = Phase_utils.MakePhaseImplemT (A) (B) + end + + include ImplemT.T +end From 1dade1823e14d06ecc7e39c8286017ea69348665 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 7 Mar 2024 16:53:15 +0100 Subject: [PATCH 04/12] feat(engine/phases): intro `simplify_match_return` --- engine/lib/diagnostics.ml | 1 + engine/lib/phases.ml | 1 + .../lib/phases/phase_simplify_match_return.ml | 113 ++++++++++++++++++ .../phases/phase_simplify_match_return.mli | 4 + 4 files changed, 119 insertions(+) create mode 100644 engine/lib/phases/phase_simplify_match_return.ml create mode 100644 engine/lib/phases/phase_simplify_match_return.mli diff --git a/engine/lib/diagnostics.ml b/engine/lib/diagnostics.ml index 46ca9d02b..aa734ad72 100644 --- a/engine/lib/diagnostics.ml +++ b/engine/lib/diagnostics.ml @@ -41,6 +41,7 @@ module Phase = struct | CfIntoMonads | FunctionalizeLoops | TraitsSpecs + | SimplifyMatchReturn | DummyA | DummyB | DummyC diff --git a/engine/lib/phases.ml b/engine/lib/phases.ml index 24870e141..36b6e9b5d 100644 --- a/engine/lib/phases.ml +++ b/engine/lib/phases.ml @@ -14,3 +14,4 @@ module Local_mutation = Phase_local_mutation.Make module Traits_specs = Phase_traits_specs.Make module Drop_needless_returns = Phase_drop_needless_returns.Make module Drop_sized_trait = Phase_drop_sized_trait.Make +module Simplify_match_return = Phase_simplify_match_return.Make diff --git a/engine/lib/phases/phase_simplify_match_return.ml b/engine/lib/phases/phase_simplify_match_return.ml new file mode 100644 index 000000000..06ef17f22 --- /dev/null +++ b/engine/lib/phases/phase_simplify_match_return.ml @@ -0,0 +1,113 @@ +open! Prelude + +module Make (F : Features.T) = + Phase_utils.MakeMonomorphicPhase + (F) + (struct + let phase_id = Diagnostics.Phase.SimplifyMatchReturn + + open Ast.Make (F) + module U = Ast_utils.Make (F) + module Visitors = Ast_visitors.Make (F) + + module Error = Phase_utils.MakeError (struct + let ctx = Diagnostics.Context.Phase phase_id + end) + + let inline_matches = + object + inherit [_] Visitors.map as super + + method! visit_expr () e = + match e with + | { + e = + Let + { + monadic = None; + lhs; + rhs = + { + e = + Match + { + scrutinee; + arms = + [ + arm; + ({ + arm = + { + body = + { + e = Return _ as return; + span = return_span; + _; + }; + _; + }; + _; + } as diverging_arm); + ]; + }; + _; + } as match_expr; + body; + }; + _; + } -> + let arm_body = arm.arm.body in + let arm_pat = arm.arm.arm_pat in + let arm_pat, let_expr = + ((* if the match produces only a variable *) + let* var = + match arm_body.e with LocalVar v -> Some v | _ -> None + in + let found = ref false in + let arm_pat = + (object + inherit [_] Visitors.map as super + + method! visit_pat () p = + match p.p with + | PBinding b when [%eq: Local_ident.t] b.var var -> + found := true; + lhs + | _ -> super#visit_pat () p + end) + #visit_pat + () arm_pat + in + let*? _ = !found in + Some (arm_pat, body)) + |> Option.value + ~default: + ( arm_pat, + { + e with + e = + Let { monadic = None; lhs; rhs = arm_body; body }; + } ) + in + let arm = { arm with arm = { arm_pat; body = let_expr } } in + let diverging_arm = + { + diverging_arm with + arm = + { + diverging_arm.arm with + body = { e = return; span = return_span; typ = e.typ }; + }; + } + in + let result = + let e' = Match { scrutinee; arms = [ arm; diverging_arm ] } in + let span = match_expr.span in + { span; typ = e.typ; e = e' } + in + super#visit_expr () result + | _ -> super#visit_expr () e + end + + let ditems = List.map ~f:(inline_matches#visit_item ()) + end) diff --git a/engine/lib/phases/phase_simplify_match_return.mli b/engine/lib/phases/phase_simplify_match_return.mli new file mode 100644 index 000000000..34d511662 --- /dev/null +++ b/engine/lib/phases/phase_simplify_match_return.mli @@ -0,0 +1,4 @@ +(** This phase rewrites `let pat = match ... { ... => ..., ... => return ... }; e` + into `match ... { ... => let pat = ...; e}`. *) + +module Make : Phase_utils.UNCONSTRAINTED_MONOMORPHIC_PHASE From 469821a184f9a03a515ded1d62a4897083f6a451 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 7 Mar 2024 16:54:03 +0100 Subject: [PATCH 05/12] fix(engine): fix `drop_needless_returns` id --- engine/lib/diagnostics.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/engine/lib/diagnostics.ml b/engine/lib/diagnostics.ml index aa734ad72..6f871f739 100644 --- a/engine/lib/diagnostics.ml +++ b/engine/lib/diagnostics.ml @@ -42,6 +42,7 @@ module Phase = struct | FunctionalizeLoops | TraitsSpecs | SimplifyMatchReturn + | DropNeedlessReturns | DummyA | DummyB | DummyC From 2781c98d421cb05631e9ee9b93f1201e2dcab272 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 7 Mar 2024 16:55:46 +0100 Subject: [PATCH 06/12] fix(backends/fstar): use the new phases --- engine/backends/fstar/fstar_backend.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 7e1ecc9b8..2c14445b6 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -1338,6 +1338,7 @@ module TransformToInputLanguage = [%functor_application Phases.Reject.RawOrMutPointer(Features.Rust) |> Phases.Drop_sized_trait + |> Phases.Simplify_question_marks |> Phases.And_mut_defsite |> Phases.Reconstruct_for_loops |> Phases.Reconstruct_while_loops @@ -1346,8 +1347,9 @@ module TransformToInputLanguage = |> Phases.Drop_blocks |> Phases.Drop_references |> Phases.Trivialize_assign_lhs - |> Phases.Reconstruct_question_marks |> Side_effect_utils.Hoist + |> Phases.Simplify_match_return + |> Phases.Drop_needless_returns |> Phases.Local_mutation |> Phases.Reject.Continue |> Phases.Cf_into_monads From ccb75f6fa33a764838e6b73b2ec014e27d002d84 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Tue, 12 Mar 2024 09:04:48 +0100 Subject: [PATCH 07/12] refactor(engine): local ident kinds: intro `SideEffectHoistVar` --- engine/lib/local_ident.ml | 3 ++- engine/lib/local_ident.mli | 18 ++++++++++++++++-- engine/lib/side_effect_utils.ml | 2 +- 3 files changed, 19 insertions(+), 4 deletions(-) diff --git a/engine/lib/local_ident.ml b/engine/lib/local_ident.ml index f652ea246..0c4536578 100644 --- a/engine/lib/local_ident.ml +++ b/engine/lib/local_ident.ml @@ -1,7 +1,7 @@ open! Prelude module T = struct - type kind = Typ | Cnst | Expr | LILifetime | Final + type kind = Typ | Cnst | Expr | LILifetime | Final | SideEffectHoistVar [@@deriving show, yojson, hash, compare, sexp, eq] type id = kind * int [@@deriving show, yojson, hash, compare, sexp, eq] @@ -13,6 +13,7 @@ module T = struct let make_final name = { name; id = mk_id Final 0 } let is_final { id; _ } = [%matches? Final] @@ fst id + let is_side_effect_hoist_var {id; _} = [%matches? SideEffectHoistVar] @@ fst id end include Base.Comparator.Make (T) diff --git a/engine/lib/local_ident.mli b/engine/lib/local_ident.mli index 0fdf1f1ab..40f90f4ee 100644 --- a/engine/lib/local_ident.mli +++ b/engine/lib/local_ident.mli @@ -1,5 +1,17 @@ module T : sig - type kind = Typ | Cnst | Expr | LILifetime | Final + type kind = + Typ + (** type namespace *) + | Cnst + (** Generic constant namespace *) + | Expr + (** Expression namespace *) + | LILifetime + (** Lifetime namespace *) + | Final + (** Frozen identifier: such an identifier will *not* be rewritten by the name policy *) + | SideEffectHoistVar + (** A variable generated by `Side_effect_utils` *) [@@deriving show, yojson, hash, compare, sexp, eq] type id [@@deriving show, yojson, hash, compare, sexp, eq] @@ -9,9 +21,11 @@ module T : sig type t = { name : string; id : id } [@@deriving show, yojson, hash, compare, sexp, eq] - (* Create a frozen final local identifier: such an indentifier won't be rewritten by a name policy *) + (** Creates a frozen final local identifier: such an indentifier won't be rewritten by a name policy *) val make_final : string -> t val is_final : t -> bool + + val is_side_effect_hoist_var : t -> bool end include module type of struct diff --git a/engine/lib/side_effect_utils.ml b/engine/lib/side_effect_utils.ml index eecb35e53..07923e089 100644 --- a/engine/lib/side_effect_utils.ml +++ b/engine/lib/side_effect_utils.ml @@ -154,7 +154,7 @@ struct self.fresh_id <- self.fresh_id + 1; { name = "hoist" ^ Int.to_string self.fresh_id; - id = Local_ident.mk_id Expr (-1) (* todo *); + id = Local_ident.mk_id SideEffectHoistVar (-1) (* todo *); } let empty = { fresh_id = 0 } From 89df2d7925edd9f27100ef1b272a23c19bb745dd Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Tue, 12 Mar 2024 09:05:38 +0100 Subject: [PATCH 08/12] feat(engine/phases): intro `simplify_hoisting` This commit introduces a phase that simplifies the pattern: ``` /// Note `let` below is NOT monadic let hoistN = e in body ``` into `body[hoistN/e]`, when: - the local ident `hoistN` is of kind `SideEffectHoistVar` (we know it was produced by the side effect utils module); - `body` contains exactly one occurence of `hoistN`. That simplifies greatly the extracted code. --- engine/backends/fstar/fstar_backend.ml | 1 + engine/lib/diagnostics.ml | 1 + engine/lib/local_ident.ml | 4 +- engine/lib/local_ident.mli | 23 +++---- engine/lib/phases.ml | 1 + engine/lib/phases/phase_simplify_hoisting.ml | 66 +++++++++++++++++++ engine/lib/phases/phase_simplify_hoisting.mli | 4 ++ 7 files changed, 85 insertions(+), 15 deletions(-) create mode 100644 engine/lib/phases/phase_simplify_hoisting.ml create mode 100644 engine/lib/phases/phase_simplify_hoisting.mli diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 2c14445b6..dad9a981e 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -1357,6 +1357,7 @@ module TransformToInputLanguage = |> Phases.Functionalize_loops |> Phases.Reject.As_pattern |> Phases.Traits_specs + |> Phases.Simplify_hoisting |> SubtypeToInputLanguage |> Identity ] diff --git a/engine/lib/diagnostics.ml b/engine/lib/diagnostics.ml index 6f871f739..f42be273e 100644 --- a/engine/lib/diagnostics.ml +++ b/engine/lib/diagnostics.ml @@ -42,6 +42,7 @@ module Phase = struct | FunctionalizeLoops | TraitsSpecs | SimplifyMatchReturn + | SimplifyHoisting | DropNeedlessReturns | DummyA | DummyB diff --git a/engine/lib/local_ident.ml b/engine/lib/local_ident.ml index 0c4536578..0d13358c5 100644 --- a/engine/lib/local_ident.ml +++ b/engine/lib/local_ident.ml @@ -13,7 +13,9 @@ module T = struct let make_final name = { name; id = mk_id Final 0 } let is_final { id; _ } = [%matches? Final] @@ fst id - let is_side_effect_hoist_var {id; _} = [%matches? SideEffectHoistVar] @@ fst id + + let is_side_effect_hoist_var { id; _ } = + [%matches? SideEffectHoistVar] @@ fst id end include Base.Comparator.Make (T) diff --git a/engine/lib/local_ident.mli b/engine/lib/local_ident.mli index 40f90f4ee..2ad0db981 100644 --- a/engine/lib/local_ident.mli +++ b/engine/lib/local_ident.mli @@ -1,17 +1,12 @@ module T : sig type kind = - Typ - (** type namespace *) - | Cnst - (** Generic constant namespace *) - | Expr - (** Expression namespace *) - | LILifetime - (** Lifetime namespace *) - | Final - (** Frozen identifier: such an identifier will *not* be rewritten by the name policy *) - | SideEffectHoistVar - (** A variable generated by `Side_effect_utils` *) + | Typ (** type namespace *) + | Cnst (** Generic constant namespace *) + | Expr (** Expression namespace *) + | LILifetime (** Lifetime namespace *) + | Final + (** Frozen identifier: such an identifier will *not* be rewritten by the name policy *) + | SideEffectHoistVar (** A variable generated by `Side_effect_utils` *) [@@deriving show, yojson, hash, compare, sexp, eq] type id [@@deriving show, yojson, hash, compare, sexp, eq] @@ -21,10 +16,10 @@ module T : sig type t = { name : string; id : id } [@@deriving show, yojson, hash, compare, sexp, eq] - (** Creates a frozen final local identifier: such an indentifier won't be rewritten by a name policy *) val make_final : string -> t - val is_final : t -> bool + (** Creates a frozen final local identifier: such an indentifier won't be rewritten by a name policy *) + val is_final : t -> bool val is_side_effect_hoist_var : t -> bool end diff --git a/engine/lib/phases.ml b/engine/lib/phases.ml index 36b6e9b5d..84a7d87a5 100644 --- a/engine/lib/phases.ml +++ b/engine/lib/phases.ml @@ -15,3 +15,4 @@ module Traits_specs = Phase_traits_specs.Make module Drop_needless_returns = Phase_drop_needless_returns.Make module Drop_sized_trait = Phase_drop_sized_trait.Make module Simplify_match_return = Phase_simplify_match_return.Make +module Simplify_hoisting = Phase_simplify_hoisting.Make diff --git a/engine/lib/phases/phase_simplify_hoisting.ml b/engine/lib/phases/phase_simplify_hoisting.ml new file mode 100644 index 000000000..69dd9dcdc --- /dev/null +++ b/engine/lib/phases/phase_simplify_hoisting.ml @@ -0,0 +1,66 @@ +open! Prelude + +module Make (F : Features.T) = + Phase_utils.MakeMonomorphicPhase + (F) + (struct + let phase_id = Diagnostics.Phase.SimplifyHoisting + + open Ast.Make (F) + module U = Ast_utils.Make (F) + module Visitors = Ast_visitors.Make (F) + + module Error = Phase_utils.MakeError (struct + let ctx = Diagnostics.Context.Phase phase_id + end) + + let inline_matches = + object + inherit [_] Visitors.map as super + + method! visit_expr () e = + match e with + | { + e = + Let + { + monadic = None; + lhs = + { + p = + PBinding + { + mut = Immutable; + mode = ByValue; + var; + subpat = None; + _; + }; + _; + }; + rhs; + body; + }; + _; + } + when Local_ident.is_side_effect_hoist_var var -> + let body, count = + (object + inherit [_] Visitors.mapreduce as super + method zero = 0 + method plus = ( + ) + + method! visit_expr () e = + match e.e with + | LocalVar v when [%eq: Local_ident.t] v var -> (rhs, 1) + | _ -> super#visit_expr () e + end) + #visit_expr + () body + in + if [%eq: int] count 1 then body else super#visit_expr () e + | _ -> super#visit_expr () e + end + + let ditems = List.map ~f:(inline_matches#visit_item ()) + end) diff --git a/engine/lib/phases/phase_simplify_hoisting.mli b/engine/lib/phases/phase_simplify_hoisting.mli new file mode 100644 index 000000000..34d511662 --- /dev/null +++ b/engine/lib/phases/phase_simplify_hoisting.mli @@ -0,0 +1,4 @@ +(** This phase rewrites `let pat = match ... { ... => ..., ... => return ... }; e` + into `match ... { ... => let pat = ...; e}`. *) + +module Make : Phase_utils.UNCONSTRAINTED_MONOMORPHIC_PHASE From 4027f8eab2c2eb392bbacb1e189e9a45a750d479 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Tue, 12 Mar 2024 10:22:08 +0100 Subject: [PATCH 09/12] fix(engine/visitors): fix `visit_list` --- engine/lib/ast_visitors.ml | 31 +++++++++++-------------------- engine/lib/utils.ml | 1 + 2 files changed, 12 insertions(+), 20 deletions(-) diff --git a/engine/lib/ast_visitors.ml b/engine/lib/ast_visitors.ml index f953a41a3..db23d9006 100644 --- a/engine/lib/ast_visitors.ml +++ b/engine/lib/ast_visitors.ml @@ -1,4 +1,6 @@ open Ast +open! Utils +open Base module Make = functor @@ -729,7 +731,7 @@ functor method visit_list : 'a. ('env -> 'a -> 'a) -> 'env -> 'a list -> 'a list = - fun v env this -> Base.List.map ~f:(fun x -> v env x) this + fun v env -> Base.List.map ~f:(v env) method visit_option : 'a. ('env -> 'a -> 'a) -> 'env -> 'a option -> 'a option = @@ -1883,15 +1885,11 @@ functor method visit_list : 'a. ('env -> 'a -> 'a * 'acc) -> 'env -> 'a list -> 'a list * 'acc = - fun v env this -> - let acc = ref self#zero in - ( Base.List.map - ~f:(fun x -> - let x, acc' = v env x in - acc := self#plus !acc acc'; - x) - this, - !acc ) + fun v env -> + Base.List.fold_map ~init:self#zero ~f:(fun acc x -> + let x, acc' = v env x in + (self#plus acc acc', x)) + >> swap method visit_option : 'a. @@ -2946,16 +2944,9 @@ functor method visit_list : 'a. ('env -> 'a -> 'acc) -> 'env -> 'a list -> 'acc = fun v env this -> - let acc = ref self#zero in - let _ = - Base.List.map - ~f:(fun x -> - let acc' = v env x in - acc := self#plus !acc acc'; - ()) - this - in - !acc + Base.List.fold ~init:self#zero + ~f:(fun acc -> v env >> self#plus acc) + this method visit_option : 'a. ('env -> 'a -> 'acc) -> 'env -> 'a option -> 'acc = diff --git a/engine/lib/utils.ml b/engine/lib/utils.ml index 262b5be8f..06242dc92 100644 --- a/engine/lib/utils.ml +++ b/engine/lib/utils.ml @@ -20,6 +20,7 @@ let uncurry f (x, y) = f x y let curry3 f x y z = f (x, y, z) let uncurry3 f (x, y, z) = f x y z let tup2 a b = (a, b) +let swap (a, b) = (b, a) let ( let* ) x f = Option.bind ~f x let some_if_true = function true -> Some () | _ -> None From 51c40a03912087fe7a20d6e67a17d9d26d0c617b Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Tue, 12 Mar 2024 10:22:33 +0100 Subject: [PATCH 10/12] fix(engine/simplify-hoisting): make the phase recursive --- engine/lib/phases/phase_simplify_hoisting.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/engine/lib/phases/phase_simplify_hoisting.ml b/engine/lib/phases/phase_simplify_hoisting.ml index 69dd9dcdc..008f152fa 100644 --- a/engine/lib/phases/phase_simplify_hoisting.ml +++ b/engine/lib/phases/phase_simplify_hoisting.ml @@ -15,7 +15,7 @@ module Make (F : Features.T) = end) let inline_matches = - object + object (self) inherit [_] Visitors.map as super method! visit_expr () e = @@ -58,7 +58,8 @@ module Make (F : Features.T) = #visit_expr () body in - if [%eq: int] count 1 then body else super#visit_expr () e + if [%eq: int] count 1 then self#visit_expr () body + else super#visit_expr () e | _ -> super#visit_expr () e end From 7533949c2a10c85cab8e8cc572986d7e44dee93a Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Tue, 12 Mar 2024 10:23:01 +0100 Subject: [PATCH 11/12] chore: update test snapshots --- ..._mut-ref-functionalization into-fstar.snap | 3 +- .../toolchain__side-effects into-fstar.snap | 268 +++++++++++------- 2 files changed, 168 insertions(+), 103 deletions(-) diff --git a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap index 3f8d1c09f..13e0089db 100644 --- a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap @@ -227,8 +227,7 @@ let j (x: t_Bar) : (t_Bar & u8) = let out:u8 = 123uy in let tmp0, out1:(t_Bar & u8) = i x in let x:t_Bar = tmp0 in - let hoist1:u8 = out1 in - let hax_temp_output:u8 = hoist1 +! out in + let hax_temp_output:u8 = out1 +! out in x, hax_temp_output <: (t_Bar & u8) type t_Pair (v_T: Type) = { 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 e154b698e..3c3bef810 100644 --- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap @@ -17,6 +17,8 @@ info: snapshot: stderr: true stdout: true + include_flag: ~ + backend_options: ~ --- exit = 0 stderr = ''' @@ -38,21 +40,16 @@ let add3 (x y z: u32) : u32 = let direct_result_question_mark (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 0y <: Core.Result.t_Result i8 u32) - <: - Core.Result.t_Result (Core.Result.t_Result i8 u32) u32) + match y with + | Core.Result.Result_Ok _ -> Core.Result.Result_Ok 0y <: Core.Result.t_Result i8 u32 + | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result i8 u32 let direct_result_question_mark_coercion (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 <: 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) + match y with + | Core.Result.Result_Ok hoist1 -> Core.Result.Result_Ok hoist1 <: Core.Result.t_Result i8 u32 + | Core.Result.Result_Err err -> + Core.Result.Result_Err (Core.Convert.f_from err) <: Core.Result.t_Result i8 u32 let early_returns (x: u32) : u32 = Rust_primitives.Hax.Control_flow_monad.Mexception.run (let! _:Prims.unit = @@ -67,9 +64,8 @@ let early_returns (x: u32) : u32 = <: Core.Ops.Control_flow.t_ControlFlow u32 Prims.unit in - let hoist3:bool = x >. 30ul in let! x, hoist5:(u32 & u32) = - if hoist3 + if x >. 30ul then match true with | true -> @@ -91,9 +87,16 @@ let early_returns (x: u32) : u32 = <: Core.Ops.Control_flow.t_ControlFlow u32 (u32 & u32) in - let hoist6:u32 = Core.Num.impl__u32__wrapping_add 123ul hoist5 in - let hoist7:u32 = Core.Num.impl__u32__wrapping_add hoist6 x in - let! hoist8:Rust_primitives.Hax.t_Never = Core.Ops.Control_flow.ControlFlow.v_Break hoist7 in + let! hoist8:Rust_primitives.Hax.t_Never = + Core.Ops.Control_flow.ControlFlow.v_Break (Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add + 123ul + hoist5 + <: + u32) + x + <: + u32) + in Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist8) <: Core.Ops.Control_flow.t_ControlFlow u32 u32) @@ -101,21 +104,20 @@ let early_returns (x: u32) : u32 = let local_mutation (x: u32) : u32 = let y:u32 = 0ul in let x:u32 = Core.Num.impl__u32__wrapping_add x 1ul in - let hoist9:bool = x >. 3ul in - if hoist9 + if x >. 3ul then let x:u32 = Core.Num.impl__u32__wrapping_sub x 3ul in let y:u32 = x /! 2ul in let y:u32 = Core.Num.impl__u32__wrapping_add y 2ul in - let hoist10:u32 = 0ul in - let hoist11:Core.Ops.Range.t_Range u32 = - { Core.Ops.Range.f_start = hoist10; Core.Ops.Range.f_end = 10ul } - <: - Core.Ops.Range.t_Range u32 - in - let hoist12:Core.Ops.Range.t_Range u32 = Core.Iter.Traits.Collect.f_into_iter hoist11 in let y:u32 = - Core.Iter.Traits.Iterator.f_fold hoist12 + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({ + Core.Ops.Range.f_start = 0ul; + Core.Ops.Range.f_end = 10ul + } + <: + Core.Ops.Range.t_Range u32) + <: + Core.Ops.Range.t_Range u32) y (fun y i -> let y:u32 = y in @@ -130,86 +132,153 @@ let local_mutation (x: u32) : u32 = let y:u32 = Core.Num.impl__u32__wrapping_add x y in (x, y <: (u32 & u32)), 3ul <: ((u32 & u32) & u32) | 13ul -> - let hoist14:u32 = x in let x:u32 = Core.Num.impl__u32__wrapping_add x 1ul in - let hoist13:u32 = Core.Num.impl__u32__wrapping_add 123ul x in - (x, y <: (u32 & u32)), add3 hoist14 hoist13 x <: ((u32 & u32) & u32) + (x, y <: (u32 & u32)), add3 x (Core.Num.impl__u32__wrapping_add 123ul x <: u32) x + <: + ((u32 & u32) & u32) | _ -> (x, y <: (u32 & u32)), 0ul <: ((u32 & u32) & u32) in let x:u32 = hoist15 in Core.Num.impl__u32__wrapping_add x y let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.Option.t_Option u8 = - Rust_primitives.Hax.Control_flow_monad.Moption.run (let? hoist19:u8 = x in - let hoist20:bool = hoist19 >. 10uy in - let? hoist26:Core.Option.t_Option u8 = - if hoist20 - then - let? hoist21:u8 = x in - Core.Option.Option_Some - (let hoist22:u8 = Core.Num.impl__u8__wrapping_add hoist21 3uy in - Core.Option.Option_Some hoist22 <: Core.Option.t_Option u8) - <: - Core.Option.t_Option (Core.Option.t_Option u8) - else - let? hoist24:u8 = x in - let? hoist23:u8 = y in - Core.Option.Option_Some - (let hoist25:u8 = Core.Num.impl__u8__wrapping_add hoist24 hoist23 in - Core.Option.Option_Some hoist25 <: Core.Option.t_Option u8) - <: - Core.Option.t_Option (Core.Option.t_Option u8) - in - let? hoist27:u8 = hoist26 in - let? v:u8 = - match hoist27 with - | 3uy -> Core.Option.Option_None <: Core.Option.t_Option u8 - | 4uy -> - let? hoist16:u64 = z in - Core.Option.Option_Some - (let hoist17:bool = hoist16 >. 4uL in - let hoist18:u8 = if hoist17 then 0uy else 3uy in - 4uy +! hoist18) - <: - Core.Option.t_Option u8 - | _ -> Core.Option.Option_Some 12uy <: Core.Option.t_Option u8 - in - let? hoist28:u8 = x in - let hoist30:u8 = Core.Num.impl__u8__wrapping_add v hoist28 in - let? hoist29:u8 = y in - Core.Option.Option_Some - (let hoist31:u8 = Core.Num.impl__u8__wrapping_add hoist30 hoist29 in - Core.Option.Option_Some hoist31 <: Core.Option.t_Option u8) - <: - Core.Option.t_Option (Core.Option.t_Option u8)) + Rust_primitives.Hax.Control_flow_monad.Mexception.run (match x with + | Core.Option.Option_Some hoist19 -> + let! hoist26:Core.Option.t_Option u8 = + if hoist19 >. 10uy + then + match x with + | Core.Option.Option_Some hoist21 -> + Core.Ops.Control_flow.ControlFlow_Continue + (Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist21 3uy) + <: + Core.Option.t_Option u8) + <: + Core.Ops.Control_flow.t_ControlFlow (Core.Option.t_Option u8) + (Core.Option.t_Option u8) + | Core.Option.Option_None -> + Core.Ops.Control_flow.ControlFlow.v_Break (Core.Option.Option_None + <: + Core.Option.t_Option u8) + else + match x with + | Core.Option.Option_Some hoist24 -> + (match y with + | Core.Option.Option_Some hoist23 -> + Core.Ops.Control_flow.ControlFlow_Continue + (Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist24 hoist23) + <: + Core.Option.t_Option u8) + <: + Core.Ops.Control_flow.t_ControlFlow (Core.Option.t_Option u8) + (Core.Option.t_Option u8) + | Core.Option.Option_None -> + Core.Ops.Control_flow.ControlFlow.v_Break (Core.Option.Option_None + <: + Core.Option.t_Option u8)) + | Core.Option.Option_None -> + Core.Ops.Control_flow.ControlFlow.v_Break (Core.Option.Option_None + <: + Core.Option.t_Option u8) + in + (match hoist26 with + | Core.Option.Option_Some hoist27 -> + let! v:u8 = + match hoist27 with + | 3uy -> + (match Core.Option.Option_None <: Core.Option.t_Option u8 with + | Core.Option.Option_Some some -> + Core.Ops.Control_flow.ControlFlow_Continue some + <: + Core.Ops.Control_flow.t_ControlFlow (Core.Option.t_Option u8) u8 + | Core.Option.Option_None -> + Core.Ops.Control_flow.ControlFlow.v_Break (Core.Option.Option_None + <: + Core.Option.t_Option u8)) + | 4uy -> + (match z with + | Core.Option.Option_Some hoist16 -> + Core.Ops.Control_flow.ControlFlow_Continue + (4uy +! (if hoist16 >. 4uL <: bool then 0uy else 3uy)) + <: + Core.Ops.Control_flow.t_ControlFlow (Core.Option.t_Option u8) u8 + | Core.Option.Option_None -> + Core.Ops.Control_flow.ControlFlow.v_Break (Core.Option.Option_None + <: + Core.Option.t_Option u8)) + | _ -> + Core.Ops.Control_flow.ControlFlow_Continue 12uy + <: + Core.Ops.Control_flow.t_ControlFlow (Core.Option.t_Option u8) u8 + in + Core.Ops.Control_flow.ControlFlow_Continue + (match x with + | Core.Option.Option_Some hoist28 -> + (match y with + | Core.Option.Option_Some hoist29 -> + Core.Option.Option_Some + (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v hoist28 + <: + u8) + hoist29) + <: + Core.Option.t_Option u8 + | Core.Option.Option_None -> Core.Option.Option_None <: Core.Option.t_Option u8) + | Core.Option.Option_None -> Core.Option.Option_None <: Core.Option.t_Option u8) + <: + Core.Ops.Control_flow.t_ControlFlow (Core.Option.t_Option u8) (Core.Option.t_Option u8) + | Core.Option.Option_None -> + Core.Ops.Control_flow.ControlFlow_Continue + (Core.Option.Option_None <: Core.Option.t_Option u8) + <: + Core.Ops.Control_flow.t_ControlFlow (Core.Option.t_Option u8) (Core.Option.t_Option u8)) + | Core.Option.Option_None -> + Core.Ops.Control_flow.ControlFlow_Continue + (Core.Option.Option_None <: Core.Option.t_Option u8) + <: + Core.Ops.Control_flow.t_ControlFlow (Core.Option.t_Option u8) (Core.Option.t_Option u8)) let question_mark (x: u32) : Core.Result.t_Result u32 u32 = - Rust_primitives.Hax.Control_flow_monad.Mresult.run (let| x:u32 = + Rust_primitives.Hax.Control_flow_monad.Mexception.run (let! x:u32 = if x >. 40ul then let y:u32 = 0ul in let x:u32 = Core.Num.impl__u32__wrapping_add x 3ul in let y:u32 = Core.Num.impl__u32__wrapping_add x y in let x:u32 = Core.Num.impl__u32__wrapping_add x y in - let hoist32:bool = x >. 90ul in - if hoist32 + if x >. 90ul then - let| _:Prims.unit = - Core.Result.impl__map_err (Core.Result.Result_Err 12uy - <: - Core.Result.t_Result Prims.unit u8) - (Core.Convert.f_from <: u8 -> u32) - in - Core.Result.Result_Ok x <: Core.Result.t_Result u32 u32 - else Core.Result.Result_Ok x <: Core.Result.t_Result u32 u32 - else Core.Result.Result_Ok x <: Core.Result.t_Result u32 u32 + match Core.Result.Result_Err 12uy <: Core.Result.t_Result Prims.unit u8 with + | Core.Result.Result_Ok ok -> + Core.Ops.Control_flow.ControlFlow_Continue x + <: + Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result u32 u32) u32 + | Core.Result.Result_Err err -> + let! _:Prims.unit = + Core.Ops.Control_flow.ControlFlow.v_Break (Core.Result.Result_Err + (Core.Convert.f_from err <: u8 -> u32) + <: + Core.Result.t_Result u32 u32) + in + Core.Ops.Control_flow.ControlFlow_Continue x + <: + Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result u32 u32) u32 + else + Core.Ops.Control_flow.ControlFlow_Continue x + <: + Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result u32 u32) u32 + else + Core.Ops.Control_flow.ControlFlow_Continue x + <: + Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result u32 u32) u32 in - Core.Result.Result_Ok + Core.Ops.Control_flow.ControlFlow_Continue (Core.Result.Result_Ok (Core.Num.impl__u32__wrapping_add 3ul x) <: Core.Result.t_Result u32 u32) <: - Core.Result.t_Result (Core.Result.t_Result u32 u32) u32) + Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result u32 u32) + (Core.Result.t_Result u32 u32)) type t_A = | A : t_A @@ -223,26 +292,23 @@ type t_Bar = { 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) + match Core.Result.Result_Err (B <: t_B) <: Core.Result.t_Result t_A t_B with + | Core.Result.Result_Ok hoist33 -> + let! hoist35:Rust_primitives.Hax.t_Never = + Core.Ops.Control_flow.ControlFlow.v_Break (Core.Result.Result_Ok hoist33 <: Core.Result.t_Result t_A t_B) - (Core.Convert.f_from <: t_B -> t_B)) + 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) + | Core.Result.Result_Err err -> + Core.Ops.Control_flow.ControlFlow_Continue + (Core.Result.Result_Err err <: 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) - 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) From f3e21a389c56a95232cf3655222a5d8909d1599f Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Tue, 12 Mar 2024 15:18:31 +0100 Subject: [PATCH 12/12] feat(engine): introduce `ppx_phases_index` --- engine/lib/dune | 4 +- engine/lib/phases.ml | 19 +-- .../phase_reconstruct_question_marks.mli | 4 +- engine/utils/ppx_phases_index/README.md | 5 + engine/utils/ppx_phases_index/dune | 12 ++ .../ppx_phases_index/ppx_phases_index.ml | 120 ++++++++++++++++++ 6 files changed, 143 insertions(+), 21 deletions(-) create mode 100644 engine/utils/ppx_phases_index/README.md create mode 100644 engine/utils/ppx_phases_index/dune create mode 100644 engine/utils/ppx_phases_index/ppx_phases_index.ml diff --git a/engine/lib/dune b/engine/lib/dune index a6b068a3e..5c73e0d79 100644 --- a/engine/lib/dune +++ b/engine/lib/dune @@ -15,7 +15,8 @@ ocamlgraph) (preprocessor_deps ; `ppx_inline` is used on the `Subtype` module, thus we need it at PPX time - (file subtype.ml)) + (file subtype.ml) + (source_tree phases)) (preprocess (pps ppx_yojson_conv @@ -26,6 +27,7 @@ ppx_deriving.eq ppx_string ppx_inline + ppx_phases_index ppx_generate_features ppx_functor_application ppx_enumerate diff --git a/engine/lib/phases.ml b/engine/lib/phases.ml index 84a7d87a5..cd3a582c2 100644 --- a/engine/lib/phases.ml +++ b/engine/lib/phases.ml @@ -1,18 +1,3 @@ -module Direct_and_mut = Phase_direct_and_mut.Make -module And_mut_defsite = Phase_and_mut_defsite.Make -module Drop_references = Phase_drop_references.Make -module Drop_blocks = Phase_drop_blocks.Make -module Reconstruct_for_loops = Phase_reconstruct_for_loops.Make -module Reconstruct_while_loops = Phase_reconstruct_while_loops.Make -module Reconstruct_question_marks = Phase_reconstruct_question_marks.Make -module Simplify_question_marks = Phase_simplify_question_marks.Make -module Trivialize_assign_lhs = Phase_trivialize_assign_lhs.Make -module Cf_into_monads = Phase_cf_into_monads.Make -module Functionalize_loops = Phase_functionalize_loops.Make +[%%phases_index ()] + module Reject = Phase_reject -module Local_mutation = Phase_local_mutation.Make -module Traits_specs = Phase_traits_specs.Make -module Drop_needless_returns = Phase_drop_needless_returns.Make -module Drop_sized_trait = Phase_drop_sized_trait.Make -module Simplify_match_return = Phase_simplify_match_return.Make -module Simplify_hoisting = Phase_simplify_hoisting.Make diff --git a/engine/lib/phases/phase_reconstruct_question_marks.mli b/engine/lib/phases/phase_reconstruct_question_marks.mli index 16c135311..f7ac4504e 100644 --- a/engine/lib/phases/phase_reconstruct_question_marks.mli +++ b/engine/lib/phases/phase_reconstruct_question_marks.mli @@ -18,11 +18,9 @@ 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 diff --git a/engine/utils/ppx_phases_index/README.md b/engine/utils/ppx_phases_index/README.md new file mode 100644 index 000000000..1b5fb3885 --- /dev/null +++ b/engine/utils/ppx_phases_index/README.md @@ -0,0 +1,5 @@ +# `ppx_phases_index` + +This PPX looks for a `phases` folder in the sources, and generate a +module binding for each, inlining the documentation, so that we can +have a nice index of all the phases with their documentation. diff --git a/engine/utils/ppx_phases_index/dune b/engine/utils/ppx_phases_index/dune new file mode 100644 index 000000000..6f7affb65 --- /dev/null +++ b/engine/utils/ppx_phases_index/dune @@ -0,0 +1,12 @@ +(library + (name ppx_phases_index) + (package hax-engine) + (kind ppx_rewriter) + (libraries ppxlib base) + (preprocess + (pps ppxlib.metaquot ppx_deriving.eq ppx_compare ppx_deriving.show))) + +(env + (_ + (flags + (:standard -warn-error -A -warn-error +8)))) diff --git a/engine/utils/ppx_phases_index/ppx_phases_index.ml b/engine/utils/ppx_phases_index/ppx_phases_index.ml new file mode 100644 index 000000000..48d1e58e0 --- /dev/null +++ b/engine/utils/ppx_phases_index/ppx_phases_index.ml @@ -0,0 +1,120 @@ +open Base +open Ppxlib + +let name = "phases_index" +let ( let* ) x f = Option.bind ~f x + +let map_first_letter (f : string -> string) (s : string) = + let first, rest = String.(prefix s 1, drop_prefix s 1) in + f first ^ rest + +let uppercase_first_char = map_first_letter String.uppercase + +let locate_phases_directory () : string = + let rec find path = + match path with + | path when String.(Stdlib.Filename.basename path = "phases") -> Some path + | path when Stdlib.Sys.is_directory path -> + Stdlib.Sys.readdir path + |> Array.filter ~f:(fun name -> not (String.is_prefix ~prefix:"." name)) + |> Array.find_map ~f:(fun name -> + find @@ Stdlib.Filename.concat path name) + | _ -> None + in + find (Stdlib.Sys.getcwd ()) + |> Option.value_exn + ~message:"ppx_phases_index: could not locate folder [phases]" + +let list_phases loc : (string * string * _ option) list = + let dir = locate_phases_directory () in + Stdlib.Sys.readdir dir |> Array.to_list + |> List.filter_map ~f:(fun filename -> + let* module_name = String.chop_suffix ~suffix:".mli" filename in + let* _ = + match String.chop_suffix ~suffix:".pp" module_name with + | Some _ -> None + | None -> Some () + in + let* phase_name = String.chop_prefix ~prefix:"phase_" module_name in + let module_name = uppercase_first_char module_name in + let phase_name = uppercase_first_char phase_name in + Some (filename, module_name, phase_name)) + |> List.map ~f:(fun (filename, module_name, phase_name) -> + let path = Stdlib.Filename.concat dir filename in + let str = + Stdlib.open_in path |> Lexing.from_channel |> Parse.interface + in + let str = + List.filter + ~f:(function { psig_desc = Psig_open _; _ } -> false | _ -> true) + str + in + match str with + | [ _ ] -> (module_name, phase_name, None) + | [ { psig_desc = Psig_attribute attr; _ }; _ ] -> + (module_name, phase_name, Some attr) + | [] -> failwith ("Empty phase" ^ filename) + | _ -> + failwith + ("Invalid phase" ^ filename ^ ": got " + ^ Int.to_string (List.length str))) + +let rename (l : (string * string) list) = + let h (s : string) = + List.find_map + ~f:(fun (s', replace) -> if String.equal s s' then Some replace else None) + l + |> Option.value ~default:s + in + object + inherit Ast_traverse.map + method! string = h + method! label = h + + method! longident = + let rec r = function + | Lapply (x, y) -> Lapply (r x, r y) + | Ldot (x, y) -> Ldot (r x, h y) + | Lident x -> Lident (h x) + in + r + end + +let expand ~(ctxt : Expansion_context.Extension.t) (str : structure_item) : + structure_item = + let loc = Expansion_context.Extension.extension_point_loc ctxt in + let (module S) = Ppxlib.Ast_builder.make loc in + let modules = + list_phases loc + |> List.map ~f:(fun (module_name, phase_name, attrs) -> + let h x = { txt = Lident x; loc } in + let original = + S.pmod_ident { txt = Ldot (Lident module_name, "Make"); loc } + in + let b = + S.module_binding + ~name:{ txt = Some phase_name; loc } + ~expr:original + in + let attrs = Option.to_list attrs in + let attrs = + List.map + ~f:(fun attr -> + let n = attr.attr_name in + if String.equal n.txt "ocaml.text" then + { attr with attr_name = { n with txt = "ocaml.doc" } } + else attr) + attrs + in + let b = { b with pmb_attributes = attrs } in + S.pstr_module b) + in + S.pstr_include (S.include_infos (S.pmod_structure modules)) + +let ext = + Extension.V3.declare name Extension.Context.structure_item + Ast_pattern.(pstr (__ ^:: nil)) + expand + +let rule = Ppxlib.Context_free.Rule.extension ext +let () = Ppxlib.Driver.register_transformation ~rules:[ rule ] name