From 28d8ffd55c9ae3da7756d198f1d209c398bc25c6 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Tue, 5 Nov 2024 15:15:09 +0100 Subject: [PATCH] Drop return/break/continue inside closures. --- .../phase_drop_return_break_continue.ml | 15 +- .../toolchain__side-effects into-fstar.snap | 119 ++++++++------ .../toolchain__side-effects into-ssprove.snap | 145 +++++++++++------- tests/side-effects/src/lib.rs | 6 + 4 files changed, 182 insertions(+), 103 deletions(-) diff --git a/engine/lib/phases/phase_drop_return_break_continue.ml b/engine/lib/phases/phase_drop_return_break_continue.ml index 3be7e8b1f..937bfeb69 100644 --- a/engine/lib/phases/phase_drop_return_break_continue.ml +++ b/engine/lib/phases/phase_drop_return_break_continue.ml @@ -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' = @@ -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 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 e03cc7117..a2038278d 100644 --- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap @@ -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" @@ -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) <: @@ -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 = @@ -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 @@ -246,7 +267,7 @@ 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 @@ -254,39 +275,39 @@ 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 -> @@ -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 -> @@ -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 @@ -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 -> @@ -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 -> @@ -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 -> @@ -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 diff --git a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap index 80a576172..2f2304adb 100644 --- a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap +++ b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap @@ -128,6 +128,8 @@ Notation "'Build_t_Foo' '[' x ']' '(' 'f_bar' ':=' y ')'" := (Build_t_Foo (f_x : (*Not implemented yet? todo(item)*) +(*Not implemented yet? todo(item)*) + Equations add3 {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (x : both L1 I1 int32) (y : both L2 I2 int32) (z : both L3 I3 int32) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32 := add3 x y z := solve_lift (impl__u32__wrapping_add (impl__u32__wrapping_add x y) z) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32. @@ -151,31 +153,31 @@ Fail Next Obligation. Equations direct_result_question_mark_coercion {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result int8 int16)) : both L1 I1 (t_Result int8 int32) := direct_result_question_mark_coercion y := - solve_lift (run (letm[choice_typeMonad.result_bind_code int32] hoist1 := impl__map_err y f_from in - Result_Ok (Result_Ok hoist1))) : both L1 I1 (t_Result int8 int32). + solve_lift (run (letm[choice_typeMonad.result_bind_code int32] hoist5 := impl__map_err y f_from in + Result_Ok (Result_Ok hoist5))) : both L1 I1 (t_Result int8 int32). Fail Next Obligation. Equations early_returns {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 int32 := early_returns x := solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (3 : int32)) - then letm[choice_typeMonad.result_bind_code int32] hoist2 := ControlFlow_Break (ret_both (0 : int32)) in - ControlFlow_Continue (never_to_any hoist2) + then letm[choice_typeMonad.result_bind_code int32] hoist6 := ControlFlow_Break (ret_both (0 : int32)) in + ControlFlow_Continue (never_to_any hoist6) else () in - letb hoist3 := x >.? (ret_both (30 : int32)) in - letm[choice_typeMonad.result_bind_code int32] hoist5 := ifb hoist3 + letb hoist7 := x >.? (ret_both (30 : int32)) in + letm[choice_typeMonad.result_bind_code int32] hoist9 := ifb hoist7 then matchb ret_both (true : 'bool) with | true => - letm[choice_typeMonad.result_bind_code int32] hoist4 := ControlFlow_Break (ret_both (34 : int32)) in - ControlFlow_Continue (solve_lift (never_to_any hoist4)) + letm[choice_typeMonad.result_bind_code int32] hoist8 := ControlFlow_Break (ret_both (34 : int32)) in + ControlFlow_Continue (solve_lift (never_to_any hoist8)) | _ => ControlFlow_Continue (solve_lift (ret_both (3 : int32))) end else ControlFlow_Continue (letb _ := assign todo(term) in x .+ (ret_both (1 : int32))) in - letb hoist6 := impl__u32__wrapping_add (ret_both (123 : int32)) hoist5 in - letb hoist7 := impl__u32__wrapping_add hoist6 x in - letm[choice_typeMonad.result_bind_code int32] hoist8 := ControlFlow_Break hoist7 in - ControlFlow_Continue (never_to_any hoist8))) : both L1 I1 int32. + letb hoist10 := impl__u32__wrapping_add (ret_both (123 : int32)) hoist9 in + letb hoist11 := impl__u32__wrapping_add hoist10 x in + letm[choice_typeMonad.result_bind_code int32] hoist12 := ControlFlow_Break hoist11 in + ControlFlow_Continue (never_to_any hoist12))) : both L1 I1 int32. Fail Next Obligation. Definition y_loc : Location := @@ -186,27 +188,27 @@ Equations local_mutation {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 local_mutation x := letb y loc(y_loc) := ret_both (0 : int32) in letb _ := assign todo(term) in - letb hoist9 := x >.? (ret_both (3 : int32)) in - solve_lift (ifb hoist9 + letb hoist13 := x >.? (ret_both (3 : int32)) in + solve_lift (ifb hoist13 then letb _ := assign todo(term) in letb y loc(y_loc) := x ./ (ret_both (2 : int32)) in letb _ := assign todo(term) in - letb hoist10 := ret_both (0 : int32) in - letb hoist11 := Build_t_Range (f_start := hoist10) (f_end := ret_both (10 : int32)) in - letb hoist12 := f_into_iter hoist11 in - letb _ := foldi_both_list hoist12 (fun i => + letb hoist14 := ret_both (0 : int32) in + letb hoist15 := Build_t_Range (f_start := hoist14) (f_end := ret_both (10 : int32)) in + letb hoist16 := f_into_iter hoist15 in + letb _ := foldi_both_list hoist16 (fun i => ssp (fun _ => assign todo(term) : (both (*0*)(L1:|:fset []) (I1) 'unit))) (ret_both (tt : 'unit)) in impl__u32__wrapping_add x y - else letb hoist15 := matchb x with + else letb hoist19 := matchb x with | 12 => letb _ := assign todo(term) in solve_lift (ret_both (3 : int32)) | 13 => - letb hoist14 := x in + letb hoist18 := x in letb _ := assign todo(term) in - letb hoist13 := impl__u32__wrapping_add (ret_both (123 : int32)) x in - solve_lift (add3 hoist14 hoist13 x) + letb hoist17 := impl__u32__wrapping_add (ret_both (123 : int32)) x in + solve_lift (add3 hoist18 hoist17 x) | _ => solve_lift (ret_both (0 : int32)) end in @@ -217,44 +219,44 @@ Fail Next Obligation. Equations monad_lifting {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result t_A t_B) := monad_lifting x := solve_lift (run (ifb x >.? (ret_both (123 : int8)) - then letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist16 := ControlFlow_Continue (Result_Err B) in - letb hoist17 := Result_Ok hoist16 in - letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist18 := ControlFlow_Break hoist17 in - ControlFlow_Continue (never_to_any hoist18) + then letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist20 := ControlFlow_Continue (Result_Err B) in + letb hoist21 := Result_Ok hoist20 in + letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist22 := ControlFlow_Break hoist21 in + ControlFlow_Continue (never_to_any hoist22) else ControlFlow_Continue (Result_Ok A))) : both L1 I1 (t_Result t_A t_B). Fail Next Obligation. Equations options {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (x : both L1 I1 (t_Option int8)) (y : both L2 I2 (t_Option int8)) (z : both L3 I3 (t_Option int64)) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8) := options x y z := - solve_lift (run (letm[choice_typeMonad.option_bind_code] hoist22 := x in - letb hoist23 := hoist22 >.? (ret_both (10 : int8)) in - letm[choice_typeMonad.option_bind_code] hoist29 := ifb hoist23 - then letm[choice_typeMonad.option_bind_code] hoist24 := x in - Option_Some (letb hoist25 := impl__u8__wrapping_add hoist24 (ret_both (3 : int8)) in - Option_Some hoist25) - else letm[choice_typeMonad.option_bind_code] hoist27 := x in - letm[choice_typeMonad.option_bind_code] hoist26 := y in - Option_Some (letb hoist28 := impl__u8__wrapping_add hoist27 hoist26 in - Option_Some hoist28) in - letm[choice_typeMonad.option_bind_code] hoist30 := hoist29 in - letm[choice_typeMonad.option_bind_code] v := matchb hoist30 with + solve_lift (run (letm[choice_typeMonad.option_bind_code] hoist26 := x in + letb hoist27 := hoist26 >.? (ret_both (10 : int8)) in + letm[choice_typeMonad.option_bind_code] hoist33 := ifb hoist27 + then letm[choice_typeMonad.option_bind_code] hoist28 := x in + Option_Some (letb hoist29 := impl__u8__wrapping_add hoist28 (ret_both (3 : int8)) in + Option_Some hoist29) + else letm[choice_typeMonad.option_bind_code] hoist31 := x in + letm[choice_typeMonad.option_bind_code] hoist30 := y in + Option_Some (letb hoist32 := impl__u8__wrapping_add hoist31 hoist30 in + Option_Some hoist32) in + letm[choice_typeMonad.option_bind_code] hoist34 := hoist33 in + letm[choice_typeMonad.option_bind_code] v := matchb hoist34 with | 3 => Option_None | 4 => - letm[choice_typeMonad.option_bind_code] hoist19 := z in - Option_Some (letb hoist20 := hoist19 >.? (ret_both (4 : int64)) in - letb hoist21 := ifb hoist20 + letm[choice_typeMonad.option_bind_code] hoist23 := z in + Option_Some (letb hoist24 := hoist23 >.? (ret_both (4 : int64)) in + letb hoist25 := ifb hoist24 then ret_both (0 : int8) else ret_both (3 : int8) in - solve_lift ((ret_both (4 : int8)) .+ hoist21)) + solve_lift ((ret_both (4 : int8)) .+ hoist25)) | _ => Option_Some (solve_lift (ret_both (12 : int8))) end in - letm[choice_typeMonad.option_bind_code] hoist31 := x in - letb hoist33 := impl__u8__wrapping_add v hoist31 in - letm[choice_typeMonad.option_bind_code] hoist32 := y in - Option_Some (letb hoist34 := impl__u8__wrapping_add hoist33 hoist32 in - Option_Some hoist34))) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8). + letm[choice_typeMonad.option_bind_code] hoist35 := x in + letb hoist37 := impl__u8__wrapping_add v hoist35 in + letm[choice_typeMonad.option_bind_code] hoist36 := y in + Option_Some (letb hoist38 := impl__u8__wrapping_add hoist37 hoist36 in + Option_Some hoist38))) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8). Fail Next Obligation. Definition y_loc : Location := @@ -266,8 +268,8 @@ Equations question_mark {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 letb _ := assign todo(term) in letb _ := assign todo(term) in letb _ := assign todo(term) in - letb hoist35 := x >.? (ret_both (90 : int32)) in - ifb hoist35 + letb hoist39 := x >.? (ret_both (90 : int32)) in + ifb hoist39 then impl__map_err (Result_Err (ret_both (12 : int8))) f_from else () else () in @@ -277,8 +279,8 @@ Fail Next Obligation. Equations simplifiable_question_mark {L1 : {fset Location}} {L2 : {fset Location}} {I1 : Interface} {I2 : Interface} (c : both L1 I1 'bool) (x : both L2 I2 (t_Option int32)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32) := simplifiable_question_mark c x := solve_lift (run (letm[choice_typeMonad.option_bind_code] a := ifb c - then letm[choice_typeMonad.option_bind_code] hoist36 := x in - Option_Some (hoist36 .+ (ret_both (10 : int32))) + then letm[choice_typeMonad.option_bind_code] hoist40 := x in + Option_Some (hoist40 .+ (ret_both (10 : int32))) else Option_Some (ret_both (0 : int32)) in Option_Some (letb b := ret_both (20 : int32) in Option_Some (a .+ b)))) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32). @@ -293,8 +295,8 @@ Equations simplifiable_return {L1 : {fset Location}} {L2 : {fset Location}} {L3 then letm[choice_typeMonad.result_bind_code int32] _ := ifb c2 then letb _ := assign todo(term) in ifb c3 - then letm[choice_typeMonad.result_bind_code int32] hoist37 := ControlFlow_Break (ret_both (1 : int32)) in - ControlFlow_Continue (never_to_any hoist37) + then letm[choice_typeMonad.result_bind_code int32] hoist41 := ControlFlow_Break (ret_both (1 : int32)) in + ControlFlow_Continue (never_to_any hoist41) else () else () in ControlFlow_Continue (letb _ := assign todo(term) in @@ -349,3 +351,40 @@ Equations f {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both Result_Ok (Result_Ok (f_my_from x)))) : both L1 I1 (t_Result int16 int16). Fail Next Obligation. ''' +"Side_effects_Issue_1089_.v" = ''' +(* File automatically generated by Hacspec *) +Set Warnings "-notation-overridden,-ambiguous-paths". +From Crypt Require Import choice_type Package Prelude. +Import PackageNotation. +From extructures Require Import ord fset. +From mathcomp Require Import word_ssrZ word. +From Jasmin Require Import word. + +From Coq Require Import ZArith. +From Coq Require Import Strings.String. +Import List.ListNotations. +Open Scope list_scope. +Open Scope Z_scope. +Open Scope bool_scope. + +From Hacspec Require Import ChoiceEquality. +From Hacspec Require Import LocationUtility. +From Hacspec Require Import Hacspec_Lib_Comparable. +From Hacspec Require Import Hacspec_Lib_Pre. +From Hacspec Require Import Hacspec_Lib. + +Open Scope hacspec_scope. +Import choice.Choice.Exports. + +Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations. + +Equations test {L1 : {fset Location}} {L2 : {fset Location}} {I1 : Interface} {I2 : Interface} (x : both L1 I1 (t_Option int32)) (y : both L2 I2 (t_Option int32)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32) := + test x y := + solve_lift (run (letb hoist3 := fun i => + letm[choice_typeMonad.option_bind_code] hoist1 := y in + Option_Some (letb hoist2 := i .+ hoist1 in + Option_Some hoist2) in + letb hoist4 := impl__map x hoist3 in + hoist4)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32). +Fail Next Obligation. +''' diff --git a/tests/side-effects/src/lib.rs b/tests/side-effects/src/lib.rs index c7db53f22..6c8f45a19 100644 --- a/tests/side-effects/src/lib.rs +++ b/tests/side-effects/src/lib.rs @@ -173,3 +173,9 @@ mod issue_1083 { Ok(u16::my_from(x)) } } + +mod issue_1089 { + fn test(x: Option, y: Option) -> Option { + x.map(|i| Some(i + y?))? + } +}