Skip to content

Commit

Permalink
Merge pull request #988 from hacspec/return-break-continue
Browse files Browse the repository at this point in the history
feat(engine) Rewrite control flow inside loops.
  • Loading branch information
W95Psp authored Oct 24, 2024
2 parents 96b4203 + 011c076 commit f5550da
Show file tree
Hide file tree
Showing 31 changed files with 1,148 additions and 155 deletions.
1 change: 1 addition & 0 deletions engine/backends/coq/coq/coq_backend.ml
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,7 @@ module SubtypeToInputLanguage
and type for_index_loop = Features.Off.for_index_loop
and type quote = Features.Off.quote
and type state_passing_loop = Features.Off.state_passing_loop
and type fold_like_loop = Features.Off.fold_like_loop
and type dyn = Features.Off.dyn
and type match_guard = Features.Off.match_guard
and type trait_item_default = Features.Off.trait_item_default
Expand Down
3 changes: 3 additions & 0 deletions engine/backends/coq/ssprove/ssprove_backend.ml
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ include
include On.While_loop
include On.For_index_loop
include On.State_passing_loop
include On.Fold_like_loop
end)
(struct
let backend = Diagnostics.Backend.SSProve
Expand Down Expand Up @@ -63,6 +64,7 @@ struct
include Features.SUBTYPE.On.While_loop
include Features.SUBTYPE.On.For_index_loop
include Features.SUBTYPE.On.State_passing_loop
include Features.SUBTYPE.On.Fold_like_loop
end)

let metadata = Phase_utils.Metadata.make (Reject (NotInBackendLang backend))
Expand Down Expand Up @@ -1123,6 +1125,7 @@ struct
};
label;
witness;
control_flow = None;
};
typ = e.typ;
span = e.span;
Expand Down
1 change: 1 addition & 0 deletions engine/backends/easycrypt/easycrypt_backend.ml
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,7 @@ module RejectNotEC (FA : Features.T) = struct
let monadic_binding = reject
let arbitrary_lhs = reject
let state_passing_loop = reject
let fold_like_loop = reject
let nontrivial_lhs = reject
let block = reject
let for_loop = reject
Expand Down
9 changes: 4 additions & 5 deletions engine/backends/fstar/fstar_backend.ml
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,7 @@ module SubtypeToInputLanguage
and type while_loop = Features.Off.while_loop
and type for_index_loop = Features.Off.for_index_loop
and type state_passing_loop = Features.Off.state_passing_loop
and type fold_like_loop = Features.Off.fold_like_loop
and type match_guard = Features.Off.match_guard
and type trait_item_default = Features.Off.trait_item_default) =
struct
Expand Down Expand Up @@ -1750,13 +1751,11 @@ module TransformToInputLanguage =
|> Side_effect_utils.Hoist
|> Phases.Hoist_disjunctive_patterns
|> Phases.Simplify_match_return
|> Phases.Rewrite_control_flow
|> Phases.Drop_needless_returns
|> Phases.Local_mutation
|> Phases.Reject.Continue
|> Phases.Cf_into_monads
|> Phases.Reject.EarlyExit
|> Phases.Rewrite_control_flow
|> Phases.Drop_return_break_continue
|> Phases.Functionalize_loops
|> Phases.Reject.Question_mark
|> Phases.Reject.As_pattern
|> Phases.Traits_specs
|> Phases.Simplify_hoisting
Expand Down
2 changes: 1 addition & 1 deletion engine/backends/proverif/proverif_backend.ml
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,7 @@ struct
let lifetime = reject
let monadic_action = reject
let monadic_binding = reject
let fold_like_loop = reject
let block = reject
let dyn = reject
let match_guard = reject
Expand Down Expand Up @@ -912,7 +913,6 @@ module TransformToInputLanguage =
|> Phases.Trivialize_assign_lhs
|> Side_effect_utils.Hoist
|> Phases.Simplify_match_return
|> Phases.Drop_needless_returns
|> Phases.Local_mutation
|> Phases.Reject.Continue
|> Phases.Reject.Dyn
Expand Down
17 changes: 15 additions & 2 deletions engine/lib/ast.ml
Original file line number Diff line number Diff line change
Expand Up @@ -241,6 +241,13 @@ functor
and pat = { p : pat'; span : span; typ : ty }
and field_pat = { field : global_ident; pat : pat }

(* This marker describes what control flow is present in a loop.
It is added by phase `DropReturnBreakContinue` and the
information is used in `FunctionalizeLoops`. We need it because
we replace the control flow nodes of the AST by some encoding
in the `ControlFlow` enum. *)
and cf_kind = BreakOnly | BreakOrReturn

and expr' =
(* pure fragment *)
| If of { cond : expr; then_ : expr; else_ : expr option }
Expand Down Expand Up @@ -285,18 +292,24 @@ functor
body : expr;
kind : loop_kind;
state : loop_state option;
control_flow : (cf_kind * F.fold_like_loop) option;
label : string option;
witness : F.loop;
}
(* ControlFlow *)
| Break of { e : expr; label : string option; witness : F.break * F.loop }
| Break of {
e : expr;
acc : (expr * F.state_passing_loop) option;
label : string option;
witness : F.break * F.loop;
}
| Return of { e : expr; witness : F.early_exit }
| 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 : (expr * F.state_passing_loop) option;
acc : (expr * F.state_passing_loop) option;
label : string option;
witness : F.continue * F.loop;
}
Expand Down
162 changes: 162 additions & 0 deletions engine/lib/ast_builder.ml
Original file line number Diff line number Diff line change
Expand Up @@ -22,17 +22,175 @@ module Make (F : Features.T) = struct
let ty_tuple_or_id : ty list -> ty = function
| [ ty ] -> ty
| types -> ty_tuple types

(** This gives the type of a value in the `ControlFlow` enum *)
let ty_cf ~(continue_type : ty) ~(break_type : ty) : ty =
TApp
{
ident = Global_ident.of_name Type Core__ops__control_flow__ControlFlow;
args = [ GType break_type; GType continue_type ];
}

(** This gives the type of a value encoded in the `ControlFlow` enum.
In case a `return_type` is provided the encoding is nested:
`return v` is `Break (Break v)`
`break v` is `Break (Continue (v, acc))` *)
let ty_cf_return ~(acc_type : ty) ~(break_type : ty)
~(return_type : ty option) : ty =
let break_type = ty_tuple [ break_type; acc_type ] in
match return_type with
| Some ret_ty ->
let break_type = ty_cf ~break_type:ret_ty ~continue_type:break_type in
ty_cf ~break_type ~continue_type:acc_type
| None -> ty_cf ~break_type ~continue_type:acc_type
end

include NoSpan

module Explicit = struct
let ty_unit : ty = TApp { ident = `TupleType 0; args = [] }
let expr_unit = expr_GlobalVar (`TupleCons 0) ~typ:ty_unit

let expr_tuple ~(span : span) (tuple : expr list) =
let len = List.length tuple in
let fields = List.mapi ~f:(fun i x -> (`TupleField (i, len), x)) tuple in
let typ = NoSpan.ty_tuple @@ List.map ~f:(fun { typ; _ } -> typ) tuple in
expr_Construct ~span ~typ ~constructor:(`TupleCons len) ~is_record:false
~is_struct:true ~fields ~base:None

let pat_PBinding ~typ = pat_PBinding ~inner_typ:typ ~typ

let arm ~span arm_pat ?(guard = None) body =
{ arm = { arm_pat; body; guard }; span }

let pat_Constructor_CF ~(span : span) ~(typ : ty)
(cf : [ `Break | `Continue ]) (pat : pat) =
match cf with
| `Break ->
{
p =
PConstruct
{
constructor =
Global_ident.of_name
(Constructor { is_struct = false })
Core__ops__control_flow__ControlFlow__Break;
fields =
[
{
field =
Global_ident.of_name Field
Core__ops__control_flow__ControlFlow__Break__0;
pat;
};
];
is_record = false;
is_struct = false;
};
typ;
span;
}
| `Continue ->
{
p =
PConstruct
{
constructor =
Global_ident.of_name
(Constructor { is_struct = false })
Core__ops__control_flow__ControlFlow__Continue;
fields =
[
{
field =
Global_ident.of_name Field
Core__ops__control_flow__ControlFlow__Continue__0;
pat;
};
];
is_record = false;
is_struct = false;
};
typ;
span;
}

let call_Constructor' (constructor : global_ident) is_struct
(args : expr list) span ret_typ =
let mk_field =
let len = List.length args in
fun n -> `TupleField (len, n)
in
let fields = List.mapi ~f:(fun i arg -> (mk_field i, arg)) args in
{
e =
Construct
{ constructor; is_record = false; is_struct; fields; base = None };
typ = ret_typ;
span;
}

let call_Constructor (constructor_name : Concrete_ident.name)
(is_struct : bool) (args : expr list) span ret_typ =
call_Constructor'
(`Concrete
(Concrete_ident.of_name (Constructor { is_struct }) constructor_name))
is_struct args span ret_typ

let expr'_Constructor_CF ~(span : span) ~(break_type : ty)
?(continue_type : ty = ty_unit) (cf : [ `Break | `Continue ]) (e : expr)
=
let typ = NoSpan.ty_cf ~continue_type ~break_type in
match cf with
| `Break ->
call_Constructor Core__ops__control_flow__ControlFlow__Break false
[ e ] span typ
| `Continue ->
call_Constructor Core__ops__control_flow__ControlFlow__Continue false
[ e ] span typ

(** We use the following encoding of return, break and continue in the `ControlFlow` enum:
Return e -> Break (Break e)
Break e -> Break ((Continue(e, acc)))
Continue -> Continue(acc)
In case there is no return we simplify to:
Break e -> (Break (e, acc))
Continue -> (continue (acc))
*)
let expr_Constructor_CF ~(span : span) ~(break_type : ty option)
~(return_type : ty option) ~(acc : expr) ?(e : expr = expr_unit ~span)
(cf : [ `Return | `Break | `Continue ]) =
let break_type = Option.value ~default:ty_unit break_type in
match cf with
| `Return ->
let continue_type = NoSpan.ty_tuple [ break_type; acc.typ ] in
let inner =
expr'_Constructor_CF ~break_type:e.typ ~continue_type ~span `Break e
in
expr'_Constructor_CF ~span ~break_type:inner.typ
~continue_type:acc.typ `Break inner
| `Break ->
let tuple = expr_tuple ~span [ e; acc ] in
let inner =
match return_type with
| Some ret_typ ->
expr'_Constructor_CF ~span ~break_type:ret_typ
~continue_type:tuple.typ `Continue tuple
| None -> tuple
in
expr'_Constructor_CF ~span ~break_type:inner.typ
~continue_type:acc.typ `Break inner
| `Continue ->
let break_type =
let tuple_type = NoSpan.ty_tuple [ break_type; acc.typ ] in
match return_type with
| Some ret_typ ->
NoSpan.ty_cf ~break_type:ret_typ ~continue_type:tuple_type
| None -> tuple_type
in
expr'_Constructor_CF ~span ~break_type ~continue_type:acc.typ
`Continue acc
end

include Explicit
Expand All @@ -44,6 +202,10 @@ module Make (F : Features.T) = struct

let pat_PBinding = Explicit.pat_PBinding ~span
let expr_unit = expr_unit ~span
let expr_tuple = expr_tuple ~span
let pat_Constructor_CF = pat_Constructor_CF ~span
let expr'_Constructor_CF = expr'_Constructor_CF ~span
let expr_Constructor_CF = expr_Constructor_CF ~span
let arm ?(guard = None) = arm ~span ?guard
end

Expand Down
4 changes: 3 additions & 1 deletion engine/lib/diagnostics.ml
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,8 @@ module Phase = struct
| NotInBackendLang of Backend.t
| ArbitraryLhs
| Continue
| Break
| QuestionMark
| RawOrMutPointer
| EarlyExit
| AsPattern
Expand Down Expand Up @@ -51,7 +53,7 @@ module Phase = struct
| TraitsSpecs
| SimplifyMatchReturn
| SimplifyHoisting
| DropNeedlessReturns
| DropReturnBreakContinue
| TransformHaxLibInline
| NewtypeAsRefinement
| DummyA
Expand Down
2 changes: 2 additions & 0 deletions engine/lib/features.ml
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ loop,
for_index_loop,
while_loop,
state_passing_loop,
fold_like_loop,
continue,
break,
mutable_variable,
Expand Down Expand Up @@ -40,6 +41,7 @@ module Rust = struct
include Off.Monadic_action
include Off.Monadic_binding
include Off.State_passing_loop
include Off.Fold_like_loop
include Off.Quote
end

Expand Down
11 changes: 8 additions & 3 deletions engine/lib/generic_printer/generic_printer_template.ml
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ struct
method expr'_Borrow ~super:_ ~kind:_ ~e:_ ~witness:_ =
default_document_for "expr'_Borrow"

method expr'_Break ~super:_ ~e:_ ~label:_ ~witness:_ =
method expr'_Break ~super:_ ~e:_ ~acc:_ ~label:_ ~witness:_ =
default_document_for "expr'_Break"

method expr'_Closure ~super:_ ~params:_ ~body:_ ~captures:_ =
Expand All @@ -84,7 +84,7 @@ struct
method expr'_Construct_tuple ~super:_ ~components:_ =
default_document_for "expr'_Construct_tuple"

method expr'_Continue ~super:_ ~e:_ ~label:_ ~witness:_ =
method expr'_Continue ~super:_ ~acc:_ ~label:_ ~witness:_ =
default_document_for "expr'_Continue"

method expr'_EffectAction ~super:_ ~action:_ ~argument:_ =
Expand All @@ -105,7 +105,8 @@ struct
method expr'_Literal ~super:_ _x2 = default_document_for "expr'_Literal"
method expr'_LocalVar ~super:_ _x2 = default_document_for "expr'_LocalVar"

method expr'_Loop ~super:_ ~body:_ ~kind:_ ~state:_ ~label:_ ~witness:_ =
method expr'_Loop ~super:_ ~body:_ ~kind:_ ~state:_ ~control_flow:_
~label:_ ~witness:_ =
default_document_for "expr'_Loop"

method expr'_MacroInvokation ~super:_ ~macro:_ ~args:_ ~witness:_ =
Expand All @@ -122,6 +123,10 @@ struct
method expr'_Return ~super:_ ~e:_ ~witness:_ =
default_document_for "expr'_Return"

method cf_kind_BreakOrReturn =
default_document_for "cf_kind_BreakOrReturn"

method cf_kind_BreakOnly = default_document_for "cf_kind_BreakOnly"
method field_pat ~field:_ ~pat:_ = default_document_for "field_pat"

method generic_constraint_GCLifetime _x1 _x2 =
Expand Down
Loading

0 comments on commit f5550da

Please sign in to comment.