From 9fa8c901e2fac67afec98ab4e63989f893ca81d6 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Mon, 10 Feb 2025 12:22:41 +0100 Subject: [PATCH] Fix return inside closure. --- engine/lib/side_effect_utils.ml | 7 +- .../toolchain__side-effects into-fstar.snap | 50 +- .../toolchain__side-effects into-ssprove.snap | 478 ++++++++++++++++-- tests/side-effects/src/lib.rs | 12 + 4 files changed, 492 insertions(+), 55 deletions(-) diff --git a/engine/lib/side_effect_utils.ml b/engine/lib/side_effect_utils.ml index 8d3a6b2a6..4f76505d8 100644 --- a/engine/lib/side_effect_utils.ml +++ b/engine/lib/side_effect_utils.ml @@ -481,7 +481,12 @@ struct @@ List.map ~f:U.Reducers.variables_of_pat params in let body = lets_of_bindings lbs body in - let effects = SideEffects.without_rw_vars vars effects in + let effects = + { + (SideEffects.without_rw_vars vars effects) with + return = None; + } + in (body, { lbs = []; effects }) in ({ e with e = Closure { params; body; captures } }, body_effects) 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 b56fb65f0..bcd7f6e77 100644 --- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap @@ -81,6 +81,52 @@ 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.Issue_1300_.fst" = ''' +module Side_effects.Issue_1300_ +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +let v_fun (_: Prims.unit) : Core.Result.t_Result Prims.unit u8 = + match + Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Map.t_Map (Core.Slice.Iter.t_Iter u8) + (u8 -> Core.Result.t_Result (u8 & t_Array u8 (mk_usize 32)) u8)) + #FStar.Tactics.Typeclasses.solve + #(Core.Result.t_Result (Alloc.Vec.t_Vec (u8 & t_Array u8 (mk_usize 32)) Alloc.Alloc.t_Global) + u8) + (Core.Iter.Traits.Iterator.f_map #(Core.Slice.Iter.t_Iter u8) + #FStar.Tactics.Typeclasses.solve + #(Core.Result.t_Result (u8 & t_Array u8 (mk_usize 32)) u8) + (Core.Slice.impl__iter #u8 + (Rust_primitives.Hax.repeat (mk_u8 0) (mk_usize 5) <: t_Slice u8) + <: + Core.Slice.Iter.t_Iter u8) + (fun prev -> + let prev:u8 = prev in + match + Core.Result.Result_Ok + (Rust_primitives.Hax.repeat (mk_u8 0) (mk_usize 32) <: t_Array u8 (mk_usize 32)) + <: + Core.Result.t_Result (t_Array u8 (mk_usize 32)) u8 + with + | Core.Result.Result_Ok hoist45 -> + Core.Result.Result_Ok (prev, hoist45 <: (u8 & t_Array u8 (mk_usize 32))) + <: + Core.Result.t_Result (u8 & t_Array u8 (mk_usize 32)) u8 + | Core.Result.Result_Err err -> + Core.Result.Result_Err err + <: + Core.Result.t_Result (u8 & t_Array u8 (mk_usize 32)) u8) + <: + Core.Iter.Adapters.Map.t_Map (Core.Slice.Iter.t_Iter u8) + (u8 -> Core.Result.t_Result (u8 & t_Array u8 (mk_usize 32)) u8)) + <: + Core.Result.t_Result (Alloc.Vec.t_Vec (u8 & t_Array u8 (mk_usize 32)) Alloc.Alloc.t_Global) u8 + with + | Core.Result.Result_Ok v_val -> + Core.Result.Result_Ok (() <: Prims.unit) <: Core.Result.t_Result Prims.unit u8 + | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result Prims.unit u8 +''' "Side_effects.Nested_return.fst" = ''' module Side_effects.Nested_return #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" @@ -97,8 +143,8 @@ 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 hoist43 -> - rng, (Core.Result.Result_Ok hoist43 <: Core.Result.t_Result Prims.unit Prims.unit) + | Core.Result.Result_Ok hoist41 -> + rng, (Core.Result.Result_Ok hoist41 <: Core.Result.t_Result Prims.unit Prims.unit) <: (i8 & Core.Result.t_Result Prims.unit Prims.unit) | Core.Result.Result_Err err -> 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 4148c9cf8..5776afa9b 100644 --- a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap +++ b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap @@ -66,21 +66,21 @@ Equations fun {L1 : {fset Location}} {I1 : Interface} (rng : both L1 I1 int8) : fun rng := solve_lift (run (letb '(tmp0,out) := other_fun rng in letb _ := assign todo(term) in - letb hoist43 := out in - letb hoist44 := f_branch hoist43 in - letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist45 := matchb hoist44 with + letb hoist41 := out in + letb hoist42 := f_branch hoist41 in + letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist43 := matchb hoist42 with | ControlFlow_Break_case residual => letb residual := ret_both ((residual) : (t_Result t_Infallible 'unit)) in - letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist42 := ControlFlow_Break (prod_b (rng,f_from_residual residual)) in - ControlFlow_Continue (solve_lift (never_to_any hoist42)) + letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist40 := ControlFlow_Break (prod_b (rng,f_from_residual residual)) in + ControlFlow_Continue (solve_lift (never_to_any hoist40)) | ControlFlow_Continue_case val => letb val := ret_both ((val) : ('unit)) in ControlFlow_Continue (solve_lift val) end in - letb hoist46 := Result_Ok hoist45 in - letb hoist47 := prod_b (rng,hoist46) in - letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist48 := ControlFlow_Break hoist47 in - ControlFlow_Continue (letb hax_temp_output := never_to_any hoist48 in + letb hoist44 := Result_Ok hoist43 in + letb hoist45 := prod_b (rng,hoist44) in + letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist46 := ControlFlow_Break hoist45 in + ControlFlow_Continue (letb hax_temp_output := never_to_any hoist46 in prod_b (rng,hax_temp_output)))) : both L1 I1 (int8 × t_Result 'unit 'unit). Fail Next Obligation. @@ -346,14 +346,23 @@ Fail Next Obligation. (*Not implemented yet? todo(item)*) +Equations fun {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 (t_Result 'unit int8) := + fun _ := + letb val := f_collect (f_map (impl__iter (unsize (repeat (ret_both (0 : int8)) (ret_both (5 : uint_size))))) (fun prev => + letb hoist47 := Result_Ok (repeat (ret_both (0 : int8)) (ret_both (32 : uint_size))) in + letb hoist48 := prod_b (prev,hoist47) in + Result_Ok hoist48)) in + Result_Ok (solve_lift (ret_both (tt : 'unit))) : both L1 I1 (t_Result 'unit int8). +Fail Next Obligation. + +(*Not implemented yet? todo(item)*) + 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 hoist40 := fun i => + solve_lift (run (impl__map x (fun i => letm[choice_typeMonad.option_bind_code] hoist38 := y in Option_Some (letb hoist39 := i .+ hoist38 in - Option_Some hoist39) in - letb hoist41 := impl__map x hoist40 in - hoist41)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32). + Option_Some hoist39)))) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32). Fail Next Obligation. ''' "Side_effects_Issue_1083_.v" = ''' @@ -395,21 +404,21 @@ Equations fun {L1 : {fset Location}} {I1 : Interface} (rng : both L1 I1 int8) : fun rng := solve_lift (run (letb '(tmp0,out) := other_fun rng in letb _ := assign todo(term) in - letb hoist43 := out in - letb hoist44 := f_branch hoist43 in - letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist45 := matchb hoist44 with + letb hoist41 := out in + letb hoist42 := f_branch hoist41 in + letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist43 := matchb hoist42 with | ControlFlow_Break_case residual => letb residual := ret_both ((residual) : (t_Result t_Infallible 'unit)) in - letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist42 := ControlFlow_Break (prod_b (rng,f_from_residual residual)) in - ControlFlow_Continue (solve_lift (never_to_any hoist42)) + letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist40 := ControlFlow_Break (prod_b (rng,f_from_residual residual)) in + ControlFlow_Continue (solve_lift (never_to_any hoist40)) | ControlFlow_Continue_case val => letb val := ret_both ((val) : ('unit)) in ControlFlow_Continue (solve_lift val) end in - letb hoist46 := Result_Ok hoist45 in - letb hoist47 := prod_b (rng,hoist46) in - letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist48 := ControlFlow_Break hoist47 in - ControlFlow_Continue (letb hax_temp_output := never_to_any hoist48 in + letb hoist44 := Result_Ok hoist43 in + letb hoist45 := prod_b (rng,hoist44) in + letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist46 := ControlFlow_Break hoist45 in + ControlFlow_Continue (letb hax_temp_output := never_to_any hoist46 in prod_b (rng,hax_temp_output)))) : both L1 I1 (int8 × t_Result 'unit 'unit). Fail Next Obligation. @@ -675,14 +684,23 @@ Fail Next Obligation. (*Not implemented yet? todo(item)*) +Equations fun {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 (t_Result 'unit int8) := + fun _ := + letb val := f_collect (f_map (impl__iter (unsize (repeat (ret_both (0 : int8)) (ret_both (5 : uint_size))))) (fun prev => + letb hoist47 := Result_Ok (repeat (ret_both (0 : int8)) (ret_both (32 : uint_size))) in + letb hoist48 := prod_b (prev,hoist47) in + Result_Ok hoist48)) in + Result_Ok (solve_lift (ret_both (tt : 'unit))) : both L1 I1 (t_Result 'unit int8). +Fail Next Obligation. + +(*Not implemented yet? todo(item)*) + 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 hoist40 := fun i => + solve_lift (run (impl__map x (fun i => letm[choice_typeMonad.option_bind_code] hoist38 := y in Option_Some (letb hoist39 := i .+ hoist38 in - Option_Some hoist39) in - letb hoist41 := impl__map x hoist40 in - hoist41)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32). + Option_Some hoist39)))) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32). Fail Next Obligation. ''' "Side_effects_Issue_1089_.v" = ''' @@ -724,21 +742,21 @@ Equations fun {L1 : {fset Location}} {I1 : Interface} (rng : both L1 I1 int8) : fun rng := solve_lift (run (letb '(tmp0,out) := other_fun rng in letb _ := assign todo(term) in - letb hoist43 := out in - letb hoist44 := f_branch hoist43 in - letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist45 := matchb hoist44 with + letb hoist41 := out in + letb hoist42 := f_branch hoist41 in + letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist43 := matchb hoist42 with | ControlFlow_Break_case residual => letb residual := ret_both ((residual) : (t_Result t_Infallible 'unit)) in - letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist42 := ControlFlow_Break (prod_b (rng,f_from_residual residual)) in - ControlFlow_Continue (solve_lift (never_to_any hoist42)) + letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist40 := ControlFlow_Break (prod_b (rng,f_from_residual residual)) in + ControlFlow_Continue (solve_lift (never_to_any hoist40)) | ControlFlow_Continue_case val => letb val := ret_both ((val) : ('unit)) in ControlFlow_Continue (solve_lift val) end in - letb hoist46 := Result_Ok hoist45 in - letb hoist47 := prod_b (rng,hoist46) in - letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist48 := ControlFlow_Break hoist47 in - ControlFlow_Continue (letb hax_temp_output := never_to_any hoist48 in + letb hoist44 := Result_Ok hoist43 in + letb hoist45 := prod_b (rng,hoist44) in + letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist46 := ControlFlow_Break hoist45 in + ControlFlow_Continue (letb hax_temp_output := never_to_any hoist46 in prod_b (rng,hax_temp_output)))) : both L1 I1 (int8 × t_Result 'unit 'unit). Fail Next Obligation. @@ -1004,14 +1022,361 @@ Fail Next Obligation. (*Not implemented yet? todo(item)*) +Equations fun {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 (t_Result 'unit int8) := + fun _ := + letb val := f_collect (f_map (impl__iter (unsize (repeat (ret_both (0 : int8)) (ret_both (5 : uint_size))))) (fun prev => + letb hoist47 := Result_Ok (repeat (ret_both (0 : int8)) (ret_both (32 : uint_size))) in + letb hoist48 := prod_b (prev,hoist47) in + Result_Ok hoist48)) in + Result_Ok (solve_lift (ret_both (tt : 'unit))) : both L1 I1 (t_Result 'unit int8). +Fail Next Obligation. + +(*Not implemented yet? todo(item)*) + 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 hoist40 := fun i => + solve_lift (run (impl__map x (fun i => letm[choice_typeMonad.option_bind_code] hoist38 := y in Option_Some (letb hoist39 := i .+ hoist38 in - Option_Some hoist39) in - letb hoist41 := impl__map x hoist40 in - hoist41)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32). + Option_Some hoist39)))) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32). +Fail Next Obligation. +''' +"Side_effects_Issue_1300_.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. + +(*Not implemented yet? todo(item)*) + +Equations other_fun {L1 : {fset Location}} {I1 : Interface} (rng : both L1 I1 int8) : both L1 I1 (int8 × t_Result 'unit 'unit) := + other_fun rng := + letb hax_temp_output := Result_Ok (ret_both (tt : 'unit)) in + solve_lift (prod_b (rng,hax_temp_output)) : both L1 I1 (int8 × t_Result 'unit 'unit). +Fail Next Obligation. + +Equations fun {L1 : {fset Location}} {I1 : Interface} (rng : both L1 I1 int8) : both L1 I1 (int8 × t_Result 'unit 'unit) := + fun rng := + solve_lift (run (letb '(tmp0,out) := other_fun rng in + letb _ := assign todo(term) in + letb hoist41 := out in + letb hoist42 := f_branch hoist41 in + letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist43 := matchb hoist42 with + | ControlFlow_Break_case residual => + letb residual := ret_both ((residual) : (t_Result t_Infallible 'unit)) in + letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist40 := ControlFlow_Break (prod_b (rng,f_from_residual residual)) in + ControlFlow_Continue (solve_lift (never_to_any hoist40)) + | ControlFlow_Continue_case val => + letb val := ret_both ((val) : ('unit)) in + ControlFlow_Continue (solve_lift val) + end in + letb hoist44 := Result_Ok hoist43 in + letb hoist45 := prod_b (rng,hoist44) in + letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist46 := ControlFlow_Break hoist45 in + ControlFlow_Continue (letb hax_temp_output := never_to_any hoist46 in + prod_b (rng,hax_temp_output)))) : both L1 I1 (int8 × t_Result 'unit 'unit). +Fail Next Obligation. + +(*Not implemented yet? todo(item)*) + +Class t_MyFrom (Self : choice_type) := { + f_my_from_loc : {fset Location} ; + f_my_from : (forall {L1 I1}, both L1 I1 v_T -> both (L1 :|: f_my_from_loc) I1 v_Self) ; +}. +Hint Unfold f_my_from_loc. + +#[global] Program Instance int16_t_MyFrom : t_MyFrom int16 int8 := + let f_my_from := fun {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) => solve_lift (cast_int (WS2 := _) x) : both (L1 :|: fset []) I1 int16 in + {| f_my_from_loc := (fset [] : {fset Location}); + f_my_from := (@f_my_from)|}. +Fail Next Obligation. +Hint Unfold int16_t_MyFrom. + +Equations f {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result int16 int16) := + f x := + solve_lift (run (letm[choice_typeMonad.result_bind_code int16] _ := impl__map_err (Result_Err (ret_both (1 : int8))) f_from in + Result_Ok (Result_Ok (f_my_from x)))) : both L1 I1 (t_Result int16 int16). +Fail Next Obligation. + +(*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. +Fail Next Obligation. + +Equations local_mutation {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 int32 := + local_mutation x := + letb y loc(y_loc) := ret_both (0 : int32) in + letb _ := assign todo(term) in + letb hoist1 := x >.? (ret_both (3 : int32)) in + solve_lift (ifb hoist1 + then letb _ := assign todo(term) in + letb y loc(y_loc) := x ./ (ret_both (2 : int32)) in + letb _ := assign todo(term) in + letb hoist2 := ret_both (0 : int32) in + letb hoist3 := Build_t_Range (f_start := hoist2) (f_end := ret_both (10 : int32)) in + letb hoist4 := f_into_iter hoist3 in + letb _ := foldi_both_list hoist4 (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 hoist7 := matchb x with + | 12 => + letb _ := assign todo(term) in + solve_lift (ret_both (3 : int32)) + | 13 => + letb hoist6 := x in + letb _ := assign todo(term) in + letb hoist5 := impl_u32__wrapping_add (ret_both (123 : int32)) x in + solve_lift (add3 hoist6 hoist5 x) + | _ => + solve_lift (ret_both (0 : int32)) + end in + letb _ := assign todo(term) in + impl_u32__wrapping_add x y) : both L1 I1 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] hoist8 := ControlFlow_Break (ret_both (0 : int32)) in + ControlFlow_Continue (never_to_any hoist8) + else () in + letb hoist9 := x >.? (ret_both (30 : int32)) in + letm[choice_typeMonad.result_bind_code int32] hoist11 := ifb hoist9 + then matchb ret_both (true : 'bool) with + | true => + letm[choice_typeMonad.result_bind_code int32] hoist10 := ControlFlow_Break (ret_both (34 : int32)) in + ControlFlow_Continue (solve_lift (never_to_any hoist10)) + | _ => + ControlFlow_Continue (solve_lift (ret_both (3 : int32))) + end + else ControlFlow_Continue (letb _ := assign todo(term) in + x .+ (ret_both (1 : int32))) in + letb hoist12 := impl_u32__wrapping_add (ret_both (123 : int32)) hoist11 in + letb hoist13 := impl_u32__wrapping_add hoist12 x in + letm[choice_typeMonad.result_bind_code int32] hoist14 := ControlFlow_Break hoist13 in + ControlFlow_Continue (never_to_any hoist14))) : both L1 I1 int32. +Fail Next Obligation. + +Equations simplifiable_return {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (c1 : both L1 I1 'bool) (c2 : both L2 I2 'bool) (c3 : both L3 I3 'bool) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32 := + simplifiable_return c1 c2 c3 := + solve_lift (run (letb x loc(x_loc) := ret_both (0 : int32) in + letm[choice_typeMonad.result_bind_code int32] _ := ifb c1 + 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] hoist15 := ControlFlow_Break (ret_both (1 : int32)) in + ControlFlow_Continue (never_to_any hoist15) + else () + else () in + ControlFlow_Continue (letb _ := assign todo(term) in + ret_both (tt : 'unit)) + else () in + ControlFlow_Continue x)) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32. +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] hoist16 := x in + Option_Some (hoist16 .+ (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). +Fail Next Obligation. + +Equations direct_result_question_mark {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result 'unit int32)) : both L1 I1 (t_Result int8 int32) := + direct_result_question_mark y := + solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := y in + Result_Ok (Result_Ok (ret_both (0 : int8))))) : both L1 I1 (t_Result int8 int32). +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] hoist17 := impl__map_err y f_from in + Result_Ok (Result_Ok hoist17))) : both L1 I1 (t_Result int8 int32). +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] hoist21 := x in + letb hoist22 := hoist21 >.? (ret_both (10 : int8)) in + letm[choice_typeMonad.option_bind_code] hoist28 := ifb hoist22 + then letm[choice_typeMonad.option_bind_code] hoist23 := x in + Option_Some (letb hoist24 := impl_u8__wrapping_add hoist23 (ret_both (3 : int8)) in + Option_Some hoist24) + else letm[choice_typeMonad.option_bind_code] hoist26 := x in + letm[choice_typeMonad.option_bind_code] hoist25 := y in + Option_Some (letb hoist27 := impl_u8__wrapping_add hoist26 hoist25 in + Option_Some hoist27) in + letm[choice_typeMonad.option_bind_code] hoist29 := hoist28 in + letm[choice_typeMonad.option_bind_code] v := matchb hoist29 with + | 3 => + Option_None + | 4 => + letm[choice_typeMonad.option_bind_code] hoist18 := z in + Option_Some (letb hoist19 := hoist18 >.? (ret_both (4 : int64)) in + letb hoist20 := ifb hoist19 + then ret_both (0 : int8) + else ret_both (3 : int8) in + solve_lift ((ret_both (4 : int8)) .+ hoist20)) + | _ => + Option_Some (solve_lift (ret_both (12 : int8))) + end in + letm[choice_typeMonad.option_bind_code] hoist30 := x in + letb hoist32 := impl_u8__wrapping_add v hoist30 in + letm[choice_typeMonad.option_bind_code] hoist31 := y in + Option_Some (letb hoist33 := impl_u8__wrapping_add hoist32 hoist31 in + Option_Some hoist33))) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8). +Fail Next Obligation. + +Equations question_mark {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 (t_Result int32 int32) := + question_mark x := + solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (40 : int32)) + then letb y loc(y_loc) := ret_both (0 : int32) in + letb _ := assign todo(term) in + letb _ := assign todo(term) in + letb _ := assign todo(term) in + letb hoist34 := x >.? (ret_both (90 : int32)) in + ifb hoist34 + then impl__map_err (Result_Err (ret_both (12 : int8))) f_from + else () + else () in + Result_Ok (Result_Ok (impl_u32__wrapping_add (ret_both (3 : int32)) x)))) : both L1 I1 (t_Result int32 int32). +Fail Next Obligation. + +Definition t_A : choice_type := + 'unit. +Equations Build_t_A : both (fset []) (fset []) (t_A) := + Build_t_A := + solve_lift (ret_both (tt (* Empty tuple *) : (t_A))) : both (fset []) (fset []) (t_A). +Fail Next Obligation. + +Definition t_B : choice_type := + 'unit. +Equations Build_t_B : both (fset []) (fset []) (t_B) := + Build_t_B := + solve_lift (ret_both (tt (* Empty tuple *) : (t_B))) : both (fset []) (fset []) (t_B). +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)] hoist35 := ControlFlow_Continue (Result_Err B) in + letb hoist36 := Result_Ok hoist35 in + letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist37 := ControlFlow_Break hoist36 in + ControlFlow_Continue (never_to_any hoist37) + else ControlFlow_Continue (Result_Ok A))) : both L1 I1 (t_Result t_A t_B). +Fail Next Obligation. + +Definition t_Bar : choice_type := + ('bool × nseq ('bool × 'bool) 6 × 'bool). +Equations f_a {L : {fset Location}} {I : Interface} (s : both L I t_Bar) : both L I 'bool := + f_a s := + bind_both s (fun x => + solve_lift (ret_both (fst x : 'bool))) : both L I 'bool. +Fail Next Obligation. +Equations f_b {L : {fset Location}} {I : Interface} (s : both L I t_Bar) : both L I (nseq ('bool × 'bool) 6 × 'bool) := + f_b s := + bind_both s (fun x => + solve_lift (ret_both (snd x : (nseq ('bool × 'bool) 6 × 'bool)))) : both L I (nseq ('bool × 'bool) 6 × 'bool). +Fail Next Obligation. +Equations Build_t_Bar {L0 : {fset Location}} {L1 : {fset Location}} {I0 : Interface} {I1 : Interface} {f_a : both L0 I0 'bool} {f_b : both L1 I1 (nseq ('bool × 'bool) 6 × 'bool)} : both (L0:|:L1) (I0:|:I1) (t_Bar) := + Build_t_Bar := + bind_both f_b (fun f_b => + bind_both f_a (fun f_a => + solve_lift (ret_both ((f_a,f_b) : (t_Bar))))) : both (L0:|:L1) (I0:|:I1) (t_Bar). +Fail Next Obligation. +Notation "'Build_t_Bar' '[' x ']' '(' 'f_a' ':=' y ')'" := (Build_t_Bar (f_a := y) (f_b := f_b x)). +Notation "'Build_t_Bar' '[' x ']' '(' 'f_b' ':=' y ')'" := (Build_t_Bar (f_a := f_a x) (f_b := y)). + +Definition t_Foo : choice_type := + ('bool × 'bool × t_Vec t_Bar t_Global × nseq t_Bar 6 × t_Bar). +Equations f_x {L : {fset Location}} {I : Interface} (s : both L I t_Foo) : both L I 'bool := + f_x s := + bind_both s (fun x => + solve_lift (ret_both (fst (fst (fst x)) : 'bool))) : both L I 'bool. +Fail Next Obligation. +Equations f_y {L : {fset Location}} {I : Interface} (s : both L I t_Foo) : both L I ('bool × t_Vec t_Bar t_Global) := + f_y s := + bind_both s (fun x => + solve_lift (ret_both (snd (fst (fst x)) : ('bool × t_Vec t_Bar t_Global)))) : both L I ('bool × t_Vec t_Bar t_Global). +Fail Next Obligation. +Equations f_z {L : {fset Location}} {I : Interface} (s : both L I t_Foo) : both L I (nseq t_Bar 6) := + f_z s := + bind_both s (fun x => + solve_lift (ret_both (snd (fst x) : (nseq t_Bar 6)))) : both L I (nseq t_Bar 6). +Fail Next Obligation. +Equations f_bar {L : {fset Location}} {I : Interface} (s : both L I t_Foo) : both L I t_Bar := + f_bar s := + bind_both s (fun x => + solve_lift (ret_both (snd x : t_Bar))) : both L I t_Bar. +Fail Next Obligation. +Equations Build_t_Foo {L0 : {fset Location}} {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I0 : Interface} {I1 : Interface} {I2 : Interface} {I3 : Interface} {f_x : both L0 I0 'bool} {f_y : both L1 I1 ('bool × t_Vec t_Bar t_Global)} {f_z : both L2 I2 (nseq t_Bar 6)} {f_bar : both L3 I3 t_Bar} : both (L0:|:L1:|:L2:|:L3) (I0:|:I1:|:I2:|:I3) (t_Foo) := + Build_t_Foo := + bind_both f_bar (fun f_bar => + bind_both f_z (fun f_z => + bind_both f_y (fun f_y => + bind_both f_x (fun f_x => + solve_lift (ret_both ((f_x,f_y,f_z,f_bar) : (t_Foo))))))) : both (L0:|:L1:|:L2:|:L3) (I0:|:I1:|:I2:|:I3) (t_Foo). +Fail Next Obligation. +Notation "'Build_t_Foo' '[' x ']' '(' 'f_x' ':=' y ')'" := (Build_t_Foo (f_x := y) (f_y := f_y x) (f_z := f_z x) (f_bar := f_bar x)). +Notation "'Build_t_Foo' '[' x ']' '(' 'f_y' ':=' y ')'" := (Build_t_Foo (f_x := f_x x) (f_y := y) (f_z := f_z x) (f_bar := f_bar x)). +Notation "'Build_t_Foo' '[' x ']' '(' 'f_z' ':=' y ')'" := (Build_t_Foo (f_x := f_x x) (f_y := f_y x) (f_z := y) (f_bar := f_bar x)). +Notation "'Build_t_Foo' '[' x ']' '(' 'f_bar' ':=' y ')'" := (Build_t_Foo (f_x := f_x x) (f_y := f_y x) (f_z := f_z x) (f_bar := y)). + +Equations assign_non_trivial_lhs {L1 : {fset Location}} {I1 : Interface} (foo : both L1 I1 t_Foo) : both L1 I1 t_Foo := + assign_non_trivial_lhs foo := + letb _ := assign todo(term) in + letb _ := assign todo(term) in + letb _ := assign todo(term) in + letb _ := assign todo(term) in + letb _ := assign todo(term) in + solve_lift foo : both L1 I1 t_Foo. +Fail Next Obligation. + +(*Not implemented yet? todo(item)*) + +Equations fun {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 (t_Result 'unit int8) := + fun _ := + letb val := f_collect (f_map (impl__iter (unsize (repeat (ret_both (0 : int8)) (ret_both (5 : uint_size))))) (fun prev => + letb hoist47 := Result_Ok (repeat (ret_both (0 : int8)) (ret_both (32 : uint_size))) in + letb hoist48 := prod_b (prev,hoist47) in + Result_Ok hoist48)) in + Result_Ok (solve_lift (ret_both (tt : 'unit))) : both L1 I1 (t_Result 'unit int8). +Fail Next Obligation. + +(*Not implemented yet? todo(item)*) + +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 (impl__map x (fun i => + letm[choice_typeMonad.option_bind_code] hoist38 := y in + Option_Some (letb hoist39 := i .+ hoist38 in + Option_Some hoist39)))) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32). Fail Next Obligation. ''' "Side_effects_Nested_return.v" = ''' @@ -1053,21 +1418,21 @@ Equations fun {L1 : {fset Location}} {I1 : Interface} (rng : both L1 I1 int8) : fun rng := solve_lift (run (letb '(tmp0,out) := other_fun rng in letb _ := assign todo(term) in - letb hoist43 := out in - letb hoist44 := f_branch hoist43 in - letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist45 := matchb hoist44 with + letb hoist41 := out in + letb hoist42 := f_branch hoist41 in + letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist43 := matchb hoist42 with | ControlFlow_Break_case residual => letb residual := ret_both ((residual) : (t_Result t_Infallible 'unit)) in - letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist42 := ControlFlow_Break (prod_b (rng,f_from_residual residual)) in - ControlFlow_Continue (solve_lift (never_to_any hoist42)) + letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist40 := ControlFlow_Break (prod_b (rng,f_from_residual residual)) in + ControlFlow_Continue (solve_lift (never_to_any hoist40)) | ControlFlow_Continue_case val => letb val := ret_both ((val) : ('unit)) in ControlFlow_Continue (solve_lift val) end in - letb hoist46 := Result_Ok hoist45 in - letb hoist47 := prod_b (rng,hoist46) in - letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist48 := ControlFlow_Break hoist47 in - ControlFlow_Continue (letb hax_temp_output := never_to_any hoist48 in + letb hoist44 := Result_Ok hoist43 in + letb hoist45 := prod_b (rng,hoist44) in + letm[choice_typeMonad.result_bind_code (int8 × t_Result 'unit 'unit)] hoist46 := ControlFlow_Break hoist45 in + ControlFlow_Continue (letb hax_temp_output := never_to_any hoist46 in prod_b (rng,hax_temp_output)))) : both L1 I1 (int8 × t_Result 'unit 'unit). Fail Next Obligation. @@ -1333,13 +1698,22 @@ Fail Next Obligation. (*Not implemented yet? todo(item)*) +Equations fun {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 (t_Result 'unit int8) := + fun _ := + letb val := f_collect (f_map (impl__iter (unsize (repeat (ret_both (0 : int8)) (ret_both (5 : uint_size))))) (fun prev => + letb hoist47 := Result_Ok (repeat (ret_both (0 : int8)) (ret_both (32 : uint_size))) in + letb hoist48 := prod_b (prev,hoist47) in + Result_Ok hoist48)) in + Result_Ok (solve_lift (ret_both (tt : 'unit))) : both L1 I1 (t_Result 'unit int8). +Fail Next Obligation. + +(*Not implemented yet? todo(item)*) + 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 hoist40 := fun i => + solve_lift (run (impl__map x (fun i => letm[choice_typeMonad.option_bind_code] hoist38 := y in Option_Some (letb hoist39 := i .+ hoist38 in - Option_Some hoist39) in - letb hoist41 := impl__map x hoist40 in - hoist41)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32). + Option_Some hoist39)))) : 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 feb2eba44..a08b80e58 100644 --- a/tests/side-effects/src/lib.rs +++ b/tests/side-effects/src/lib.rs @@ -190,3 +190,15 @@ mod nested_return { return Ok(other_fun(rng)?); } } + +mod issue_1300 { + fn fun() -> Result<(), u8> { + let val = [0u8; 5] + .iter() + // Removing the inner Result/? below makes this pass + .map(|&prev| Ok::<(u8, [u8; 32]), u8>((prev, Ok::<[u8; 32], u8>([0u8; 32])?))) + // Removing the ? below makes this pass + .collect::, _>>()?; + Ok(()) + } +}