Skip to content

Commit

Permalink
Propagate return rewrite inside returns to avoid crash in side_effect…
Browse files Browse the repository at this point in the history 
…_utils.
  • Loading branch information
@maximebuyse
maximebuyse committed Jan 14, 2025
1 parent d5f4d3e commit 340fb9a
Show file tree
Hide file tree
Showing 5 changed files with 201 additions and 106 deletions.
6 changes: 4 additions & 2 deletions engine/lib/phases/phase_and_mut_defsite.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -95,12 +95,14 @@ struct
(* visit an expression and replace all `Return e` nodes by `Return (f e)` *)
let map_returns ~(f : expr -> expr) : expr -> expr =
let visitor =
object
object (self)
inherit [_] Visitors.map as super

method! visit_expr' () e =
match e with
| Return { e; witness } -> Return { e = f e; witness }
| Return { e; witness } ->
let e = self#visit_expr () e in
Return { e = f e; witness }
| _ -> super#visit_expr' () e
end
in
Expand Down
4 changes: 2 additions & 2 deletions engine/lib/side_effect_utils.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,9 +42,9 @@ struct
{
details =
"Expected two exact same types, got x="
^ [%show: ty] x
^ (x |> U.LiftToFullAst.ty |> Print_rust.pty_str)
^ " and y="
^ [%show: ty] y;
^ (y |> U.LiftToFullAst.ty |> Print_rust.pty_str);
})
else x
in
Expand Down
123 changes: 74 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 @@ -81,6 +81,31 @@ let test (x y: Core.Option.t_Option i32) : Core.Option.t_Option i32 =
| Core.Option.Option_Some some -> some
| Core.Option.Option_None -> Core.Option.Option_None <: Core.Option.t_Option i32
'''
"Side_effects.Nested_return.fst" = '''
module Side_effects.Nested_return
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
open Core
open FStar.Mul

let other_fun (rng: i8) : (i8 & Core.Result.t_Result Prims.unit Prims.unit) =
let hax_temp_output:Core.Result.t_Result Prims.unit Prims.unit =
Core.Result.Result_Ok (() <: Prims.unit) <: Core.Result.t_Result Prims.unit Prims.unit
in
rng, hax_temp_output <: (i8 & Core.Result.t_Result Prims.unit Prims.unit)

let v_fun (rng: i8) : (i8 & Core.Result.t_Result Prims.unit Prims.unit) =
let tmp0, out:(i8 & Core.Result.t_Result Prims.unit Prims.unit) = other_fun rng in
let rng:i8 = tmp0 in
match out <: Core.Result.t_Result Prims.unit Prims.unit with
| Core.Result.Result_Ok hoist6 ->
rng, (Core.Result.Result_Ok hoist6 <: Core.Result.t_Result Prims.unit Prims.unit)
<:
(i8 & Core.Result.t_Result Prims.unit Prims.unit)
| Core.Result.Result_Err err ->
rng, (Core.Result.Result_Err err <: Core.Result.t_Result Prims.unit Prims.unit)
<:
(i8 & Core.Result.t_Result Prims.unit Prims.unit)
'''
"Side_effects.fst" = '''
module Side_effects
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
Expand Down Expand Up @@ -208,7 +233,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 <: Core.Result.t_Result i8 u16 with
| Core.Result.Result_Ok hoist5 -> Core.Result.Result_Ok hoist5 <: Core.Result.t_Result i8 u32
| Core.Result.Result_Ok hoist10 -> Core.Result.Result_Ok hoist10 <: 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 @@ -224,12 +249,12 @@ let early_returns (x: u32) : u32 =
match true <: bool with
| true -> 34ul
| _ ->
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
let x, hoist14:(u32 & u32) = x, 3ul <: (u32 & u32) in
Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add 123ul hoist14 <: u32) x
else
let x:u32 = x +! 9ul in
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
let x, hoist14:(u32 & u32) = x, x +! 1ul <: (u32 & u32) in
Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add 123ul hoist14 <: u32) x

/// Exercise local mutation with control flow and loops
let local_mutation (x: u32) : u32 =
Expand Down Expand Up @@ -257,7 +282,7 @@ let local_mutation (x: u32) : u32 =
in
Core.Num.impl__u32__wrapping_add x y
else
let (x, y), hoist19:((u32 & u32) & u32) =
let (x, y), hoist24:((u32 & u32) & u32) =
match x <: u32 with
| 12ul ->
let y:u32 = Core.Num.impl__u32__wrapping_add x y in
Expand All @@ -269,47 +294,47 @@ let local_mutation (x: u32) : u32 =
((u32 & u32) & u32)
| _ -> (x, y <: (u32 & u32)), 0ul <: ((u32 & u32) & u32)
in
let x:u32 = hoist19 in
let x:u32 = hoist24 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 hoist20 -> Core.Result.Result_Ok hoist20 <: Core.Result.t_Result t_A t_B
| Core.Result.Result_Ok hoist25 -> Core.Result.Result_Ok hoist25 <: 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 <: Core.Option.t_Option u8 with
| Core.Option.Option_Some hoist26 ->
if hoist26 >. 10uy
| Core.Option.Option_Some hoist31 ->
if hoist31 >. 10uy
then
match x <: Core.Option.t_Option u8 with
| Core.Option.Option_Some hoist28 ->
| Core.Option.Option_Some hoist33 ->
(match
Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist28 3uy)
Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist33 3uy)
<:
Core.Option.t_Option u8
with
| Core.Option.Option_Some hoist34 ->
(match hoist34 <: u8 with
| Core.Option.Option_Some hoist39 ->
(match hoist39 <: u8 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 <: Core.Option.t_Option u8 with
| Core.Option.Option_Some hoist35 ->
| Core.Option.Option_Some hoist40 ->
(match y <: Core.Option.t_Option u8 with
| Core.Option.Option_Some hoist36 ->
| Core.Option.Option_Some hoist41 ->
Core.Option.Option_Some
(Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
hoist35
hoist40
<:
u8)
hoist36)
hoist41)
<:
Core.Option.t_Option u8
| Core.Option.Option_None ->
Expand All @@ -319,18 +344,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 <: Core.Option.t_Option u64 with
| Core.Option.Option_Some hoist23 ->
let v:u8 = 4uy +! (if hoist23 >. 4uL <: bool then 0uy else 3uy) in
| Core.Option.Option_Some hoist28 ->
let v:u8 = 4uy +! (if hoist28 >. 4uL <: bool then 0uy else 3uy) in
(match x <: Core.Option.t_Option u8 with
| Core.Option.Option_Some hoist35 ->
| Core.Option.Option_Some hoist40 ->
(match y <: Core.Option.t_Option u8 with
| Core.Option.Option_Some hoist36 ->
| Core.Option.Option_Some hoist41 ->
Core.Option.Option_Some
(Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
hoist35
hoist40
<:
u8)
hoist36)
hoist41)
<:
Core.Option.t_Option u8
| Core.Option.Option_None ->
Expand All @@ -341,14 +366,14 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
| _ ->
let v:u8 = 12uy in
match x <: Core.Option.t_Option u8 with
| Core.Option.Option_Some hoist35 ->
| Core.Option.Option_Some hoist40 ->
(match y <: Core.Option.t_Option u8 with
| Core.Option.Option_Some hoist36 ->
| Core.Option.Option_Some hoist41 ->
Core.Option.Option_Some
(Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v hoist35
(Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v hoist40
<:
u8)
hoist36)
hoist41)
<:
Core.Option.t_Option u8
| Core.Option.Option_None -> Core.Option.Option_None <: Core.Option.t_Option u8
Expand All @@ -358,30 +383,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 <: Core.Option.t_Option u8 with
| Core.Option.Option_Some hoist31 ->
| Core.Option.Option_Some hoist36 ->
(match y <: Core.Option.t_Option u8 with
| Core.Option.Option_Some hoist30 ->
| Core.Option.Option_Some hoist35 ->
(match
Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist31 hoist30)
Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist36 hoist35)
<:
Core.Option.t_Option u8
with
| Core.Option.Option_Some hoist34 ->
(match hoist34 <: u8 with
| Core.Option.Option_Some hoist39 ->
(match hoist39 <: u8 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 <: Core.Option.t_Option u8 with
| Core.Option.Option_Some hoist35 ->
| Core.Option.Option_Some hoist40 ->
(match y <: Core.Option.t_Option u8 with
| Core.Option.Option_Some hoist36 ->
| Core.Option.Option_Some hoist41 ->
Core.Option.Option_Some
(Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
hoist35
hoist40
<:
u8)
hoist36)
hoist41)
<:
Core.Option.t_Option u8
| Core.Option.Option_None ->
Expand All @@ -392,18 +417,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 <: Core.Option.t_Option u64 with
| Core.Option.Option_Some hoist23 ->
let v:u8 = 4uy +! (if hoist23 >. 4uL <: bool then 0uy else 3uy) in
| Core.Option.Option_Some hoist28 ->
let v:u8 = 4uy +! (if hoist28 >. 4uL <: bool then 0uy else 3uy) in
(match x <: Core.Option.t_Option u8 with
| Core.Option.Option_Some hoist35 ->
| Core.Option.Option_Some hoist40 ->
(match y <: Core.Option.t_Option u8 with
| Core.Option.Option_Some hoist36 ->
| Core.Option.Option_Some hoist41 ->
Core.Option.Option_Some
(Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
hoist35
hoist40
<:
u8)
hoist36)
hoist41)
<:
Core.Option.t_Option u8
| Core.Option.Option_None ->
Expand All @@ -415,15 +440,15 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
| _ ->
let v:u8 = 12uy in
match x <: Core.Option.t_Option u8 with
| Core.Option.Option_Some hoist35 ->
| Core.Option.Option_Some hoist40 ->
(match y <: Core.Option.t_Option u8 with
| Core.Option.Option_Some hoist36 ->
| Core.Option.Option_Some hoist41 ->
Core.Option.Option_Some
(Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v
hoist35
hoist40
<:
u8)
hoist36)
hoist41)
<:
Core.Option.t_Option u8
| Core.Option.Option_None ->
Expand Down Expand Up @@ -463,8 +488,8 @@ let simplifiable_question_mark (c: bool) (x: Core.Option.t_Option i32) : Core.Op
if c
then
match x <: Core.Option.t_Option i32 with
| Core.Option.Option_Some hoist40 ->
let a:i32 = hoist40 +! 10l in
| Core.Option.Option_Some hoist45 ->
let a:i32 = hoist45 +! 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 340fb9a

Please sign in to comment.