Skip to content

Commit

Permalink
Drop return/break/continue inside closures.
Browse files Browse the repository at this point in the history
  • Loading branch information
@maximebuyse
maximebuyse committed Nov 5, 2024
1 parent acb0c3d commit 28d8ffd
Show file tree
Hide file tree
Showing 4 changed files with 182 additions and 103 deletions.
15 changes: 14 additions & 1 deletion engine/lib/phases/phase_drop_return_break_continue.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -118,6 +118,18 @@ module%inlined_contents Make (F : Features.T) = struct
in exit nodes. **)
end

let closure_visitor =
let module Visitors = Ast_visitors.Make (F) in
object
inherit [_] Visitors.map as super

method! visit_expr' () e =
match e with
| Closure ({ body; _ } as closure) ->
Closure { closure with body = visitor#visit_expr None body }
| _ -> super#visit_expr' () e
end

[%%inline_defs dmutability + dsafety_kind]

let rec dexpr' (span : span) (expr : A.expr') : B.expr' =
Expand Down Expand Up @@ -157,7 +169,8 @@ module%inlined_contents Make (F : Features.T) = struct
[%%inline_defs "Item.*" - ditems]

let ditems (items : A.item list) : B.item list =
List.concat_map items ~f:(visitor#visit_item None >> ditem)
List.concat_map items
~f:(visitor#visit_item None >> closure_visitor#visit_item () >> ditem)
end

include Implem
Expand Down
119 changes: 70 additions & 49 deletions test-harness/src/snapshots/toolchain__side-effects into-fstar.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,6 +58,27 @@ let f (x: u8) : Core.Result.t_Result u16 u16 =
<:
Core.Result.t_Result u16 u16
'''
"Side_effects.Issue_1089_.fst" = '''
module Side_effects.Issue_1089_
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
open Core
open FStar.Mul

let test (x y: Core.Option.t_Option i32) : Core.Option.t_Option i32 =
match
Core.Option.impl__map #i32
#(Core.Option.t_Option i32)
x
(fun i ->
let i:i32 = i in
match y with
| Core.Option.Option_Some hoist1 ->
Core.Option.Option_Some (i +! hoist1 <: i32) <: Core.Option.t_Option i32
| Core.Option.Option_None -> Core.Option.Option_None <: Core.Option.t_Option i32)
with
| Core.Option.Option_Some some -> some
| Core.Option.Option_None -> Core.Option.Option_None <: Core.Option.t_Option i32
'''
"Side_effects.fst" = '''
module Side_effects
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
Expand Down Expand Up @@ -185,7 +206,7 @@ let direct_result_question_mark (y: Core.Result.t_Result Prims.unit u32)
let direct_result_question_mark_coercion (y: Core.Result.t_Result i8 u16)
: Core.Result.t_Result i8 u32 =
match y with
| Core.Result.Result_Ok hoist1 -> Core.Result.Result_Ok hoist1 <: Core.Result.t_Result i8 u32
| Core.Result.Result_Ok hoist5 -> Core.Result.Result_Ok hoist5 <: Core.Result.t_Result i8 u32
| Core.Result.Result_Err err ->
Core.Result.Result_Err (Core.Convert.f_from #u32 #u16 #FStar.Tactics.Typeclasses.solve err)
<:
Expand All @@ -201,12 +222,12 @@ let early_returns (x: u32) : u32 =
match true with
| true -> 34ul
| _ ->
let x, hoist5:(u32 & u32) = x, 3ul <: (u32 & u32) in
Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add 123ul hoist5 <: u32) x
let x, hoist9:(u32 & u32) = x, 3ul <: (u32 & u32) in
Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add 123ul hoist9 <: u32) x
else
let x:u32 = x +! 9ul in
let x, hoist5:(u32 & u32) = x, x +! 1ul <: (u32 & u32) in
Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add 123ul hoist5 <: u32) x
let x, hoist9:(u32 & u32) = x, x +! 1ul <: (u32 & u32) in
Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add 123ul hoist9 <: u32) x

/// Exercise local mutation with control flow and loops
let local_mutation (x: u32) : u32 =
Expand Down Expand Up @@ -234,7 +255,7 @@ let local_mutation (x: u32) : u32 =
in
Core.Num.impl__u32__wrapping_add x y
else
let (x, y), hoist15:((u32 & u32) & u32) =
let (x, y), hoist19:((u32 & u32) & u32) =
match x with
| 12ul ->
let y:u32 = Core.Num.impl__u32__wrapping_add x y in
Expand All @@ -246,47 +267,47 @@ let local_mutation (x: u32) : u32 =
((u32 & u32) & u32)
| _ -> (x, y <: (u32 & u32)), 0ul <: ((u32 & u32) & u32)
in
let x:u32 = hoist15 in
let x:u32 = hoist19 in
Core.Num.impl__u32__wrapping_add x y

/// Combine `?` and early return
let monad_lifting (x: u8) : Core.Result.t_Result t_A t_B =
if x >. 123uy
then
match Core.Result.Result_Err (B <: t_B) <: Core.Result.t_Result t_A t_B with
| Core.Result.Result_Ok hoist16 -> Core.Result.Result_Ok hoist16 <: Core.Result.t_Result t_A t_B
| Core.Result.Result_Ok hoist20 -> Core.Result.Result_Ok hoist20 <: Core.Result.t_Result t_A t_B
| Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result t_A t_B
else Core.Result.Result_Ok (A <: t_A) <: Core.Result.t_Result t_A t_B

/// Test question mark on `Option`s with some control flow
let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.Option.t_Option u8 =
match x with
| Core.Option.Option_Some hoist22 ->
if hoist22 >. 10uy
| Core.Option.Option_Some hoist26 ->
if hoist26 >. 10uy
then
match x with
| Core.Option.Option_Some hoist24 ->
| Core.Option.Option_Some hoist28 ->
(match
Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist24 3uy)
Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist28 3uy)
<:
Core.Option.t_Option u8
with
| Core.Option.Option_Some hoist30 ->
(match hoist30 with
| Core.Option.Option_Some hoist34 ->
(match hoist34 with
| 3uy ->
(match Core.Option.Option_None <: Core.Option.t_Option u8 with
| Core.Option.Option_Some some ->
let v:u8 = some in
(match x with
| Core.Option.Option_Some hoist31 ->
| Core.Option.Option_Some hoist35 ->
(match y with
| Core.Option.Option_Some hoist32 ->
| Core.Option.Option_Some hoist36 ->
Core.Option.Option_Some
(Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
hoist31
hoist35
<:
u8)
hoist32)
hoist36)
<:
Core.Option.t_Option u8
| Core.Option.Option_None ->
Expand All @@ -296,18 +317,18 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
| Core.Option.Option_None -> Core.Option.Option_None <: Core.Option.t_Option u8)
| 4uy ->
(match z with
| Core.Option.Option_Some hoist19 ->
let v:u8 = 4uy +! (if hoist19 >. 4uL <: bool then 0uy else 3uy) in
| Core.Option.Option_Some hoist23 ->
let v:u8 = 4uy +! (if hoist23 >. 4uL <: bool then 0uy else 3uy) in
(match x with
| Core.Option.Option_Some hoist31 ->
| Core.Option.Option_Some hoist35 ->
(match y with
| Core.Option.Option_Some hoist32 ->
| Core.Option.Option_Some hoist36 ->
Core.Option.Option_Some
(Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
hoist31
hoist35
<:
u8)
hoist32)
hoist36)
<:
Core.Option.t_Option u8
| Core.Option.Option_None ->
Expand All @@ -318,14 +339,14 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
| _ ->
let v:u8 = 12uy in
match x with
| Core.Option.Option_Some hoist31 ->
| Core.Option.Option_Some hoist35 ->
(match y with
| Core.Option.Option_Some hoist32 ->
| Core.Option.Option_Some hoist36 ->
Core.Option.Option_Some
(Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v hoist31
(Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v hoist35
<:
u8)
hoist32)
hoist36)
<:
Core.Option.t_Option u8
| Core.Option.Option_None -> Core.Option.Option_None <: Core.Option.t_Option u8
Expand All @@ -335,30 +356,30 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
| Core.Option.Option_None -> Core.Option.Option_None <: Core.Option.t_Option u8
else
(match x with
| Core.Option.Option_Some hoist27 ->
| Core.Option.Option_Some hoist31 ->
(match y with
| Core.Option.Option_Some hoist26 ->
| Core.Option.Option_Some hoist30 ->
(match
Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist27 hoist26)
Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist31 hoist30)
<:
Core.Option.t_Option u8
with
| Core.Option.Option_Some hoist30 ->
(match hoist30 with
| Core.Option.Option_Some hoist34 ->
(match hoist34 with
| 3uy ->
(match Core.Option.Option_None <: Core.Option.t_Option u8 with
| Core.Option.Option_Some some ->
let v:u8 = some in
(match x with
| Core.Option.Option_Some hoist31 ->
| Core.Option.Option_Some hoist35 ->
(match y with
| Core.Option.Option_Some hoist32 ->
| Core.Option.Option_Some hoist36 ->
Core.Option.Option_Some
(Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
hoist31
hoist35
<:
u8)
hoist32)
hoist36)
<:
Core.Option.t_Option u8
| Core.Option.Option_None ->
Expand All @@ -369,18 +390,18 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
Core.Option.Option_None <: Core.Option.t_Option u8)
| 4uy ->
(match z with
| Core.Option.Option_Some hoist19 ->
let v:u8 = 4uy +! (if hoist19 >. 4uL <: bool then 0uy else 3uy) in
| Core.Option.Option_Some hoist23 ->
let v:u8 = 4uy +! (if hoist23 >. 4uL <: bool then 0uy else 3uy) in
(match x with
| Core.Option.Option_Some hoist31 ->
| Core.Option.Option_Some hoist35 ->
(match y with
| Core.Option.Option_Some hoist32 ->
| Core.Option.Option_Some hoist36 ->
Core.Option.Option_Some
(Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
hoist31
hoist35
<:
u8)
hoist32)
hoist36)
<:
Core.Option.t_Option u8
| Core.Option.Option_None ->
Expand All @@ -392,15 +413,15 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
| _ ->
let v:u8 = 12uy in
match x with
| Core.Option.Option_Some hoist31 ->
| Core.Option.Option_Some hoist35 ->
(match y with
| Core.Option.Option_Some hoist32 ->
| Core.Option.Option_Some hoist36 ->
Core.Option.Option_Some
(Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
hoist31
hoist35
<:
u8)
hoist32)
hoist36)
<:
Core.Option.t_Option u8
| Core.Option.Option_None ->
Expand Down Expand Up @@ -440,8 +461,8 @@ let simplifiable_question_mark (c: bool) (x: Core.Option.t_Option i32) : Core.Op
if c
then
match x with
| Core.Option.Option_Some hoist36 ->
let a:i32 = hoist36 +! 10l in
| Core.Option.Option_Some hoist40 ->
let a:i32 = hoist40 +! 10l in
let b:i32 = 20l in
Core.Option.Option_Some (a +! b) <: Core.Option.t_Option i32
| Core.Option.Option_None -> Core.Option.Option_None <: Core.Option.t_Option i32
Expand Down
Loading

0 comments on commit 28d8ffd

Please sign in to comment.