diff --git a/engine/lib/side_effect_utils.ml b/engine/lib/side_effect_utils.ml index 801a3b268..a479c389b 100644 --- a/engine/lib/side_effect_utils.ml +++ b/engine/lib/side_effect_utils.ml @@ -503,6 +503,61 @@ struct collect_and_hoist_effects_object#visit_expr CollectContext.empty e in (lets_of_bindings lbs e, effects) + + let has_side_effect = + object + inherit [_] Visitors.reduce as super + method zero = false + method plus l r = l || r + + method! visit_expr' () = + function + | Assign _ | Return _ | Break _ | Continue _ -> true + | e -> super#visit_expr' () e + end + + (* This visitor binds in `let_ = e in ()` all expressions + of type unit that are not already in a let binding. + This ensures that all side effects happen in the rhs of a let binding. *) + let bind_unit_return_position = + object (self) + inherit [_] Visitors.map as super + + method! visit_expr in_let e = + match e.e with + | Let { monadic; rhs; lhs; body } -> + { + e with + e = + Let + { + monadic; + rhs = self#visit_expr true rhs; + lhs = self#visit_pat false lhs; + body = self#visit_expr false body; + }; + } + | _ -> + let span = e.span in + if [%eq: expr'] e.e (U.unit_expr span).e then e + else if + [%eq: ty] e.typ U.unit_typ + && (not in_let) + && has_side_effect#visit_expr () e + then + { + e with + e = + Let + { + monadic = None; + rhs = self#visit_expr true e; + lhs = U.M.pat_PWild ~span ~typ:e.typ; + body = U.unit_expr span; + }; + } + else super#visit_expr false e + end end end @@ -538,7 +593,10 @@ struct open ID let dexpr (expr : A.expr) : B.expr = - Hoist.collect_and_hoist_effects expr |> fst |> dexpr + Hoist.collect_and_hoist_effects expr + |> fst + |> Hoist.bind_unit_return_position#visit_expr false + |> dexpr [%%inline_defs "Item.*"] diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap index 26fe6fce5..56deae445 100644 --- a/test-harness/src/snapshots/toolchain__generics into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__generics into-fstar.snap @@ -153,7 +153,8 @@ let foo (v_LEN: usize) (arr: t_Array usize v_LEN) : usize = (fun acc i -> let acc:usize = acc in let i:usize = i in - acc +! (arr.[ i ] <: usize) <: usize) + let acc:usize = acc +! (arr.[ i ] <: usize) in + acc) in acc diff --git a/test-harness/src/snapshots/toolchain__loops into-fstar.snap b/test-harness/src/snapshots/toolchain__loops into-fstar.snap index 75dc6849a..3da01bbff 100644 --- a/test-harness/src/snapshots/toolchain__loops into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__loops into-fstar.snap @@ -157,7 +157,8 @@ let double_sum2 (_: Prims.unit) : i32 = Core.Ops.Control_flow.t_ControlFlow (Prims.unit & (i32 & i32)) (i32 & i32) else let sum:i32 = sum +! i in - Core.Ops.Control_flow.ControlFlow_Continue (sum, sum2 +! i <: (i32 & i32)) + let sum2:i32 = sum2 +! i in + Core.Ops.Control_flow.ControlFlow_Continue (sum, sum2 <: (i32 & i32)) <: Core.Ops.Control_flow.t_ControlFlow (Prims.unit & (i32 & i32)) (i32 & i32)) in @@ -187,7 +188,8 @@ let double_sum2_return (v: t_Slice i32) : i32 = (Core.Ops.Control_flow.t_ControlFlow i32 (Prims.unit & (i32 & i32))) (i32 & i32) else let sum:i32 = sum +! i in - Core.Ops.Control_flow.ControlFlow_Continue (sum, sum2 +! i <: (i32 & i32)) + let sum2:i32 = sum2 +! i in + Core.Ops.Control_flow.ControlFlow_Continue (sum, sum2 <: (i32 & i32)) <: Core.Ops.Control_flow.t_ControlFlow (Core.Ops.Control_flow.t_ControlFlow i32 (Prims.unit & (i32 & i32))) (i32 & i32)) @@ -372,7 +374,8 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global (fun mean item -> let mean:usize = mean in let item:usize = item in - mean +! item <: usize) + let mean:usize = mean +! item in + mean) in let acc:usize = acc +! (mean /! v_CHUNK_LEN <: usize) in acc) @@ -387,7 +390,8 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global (fun acc item -> let acc:usize = acc in let item:usize = item in - acc -! item <: usize) + let acc:usize = acc -! item in + acc) in acc @@ -419,7 +423,8 @@ let composed_range (n: usize) : usize = (fun acc i -> let acc:usize = acc in let i:usize = i in - (acc +! i <: usize) +! sz 1 <: usize) + let acc:usize = (acc +! i <: usize) +! sz 1 in + acc) in acc @@ -448,36 +453,41 @@ let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = (fun acc temp_1_ -> let acc:usize = acc in let i, chunk:(usize & t_Slice usize) = temp_1_ in - Rust_primitives.Hax.Folds.fold_enumerated_slice chunk - (fun acc temp_1_ -> - let acc:usize = acc in - let _:usize = temp_1_ in - true) - acc - (fun acc temp_1_ -> - let acc:usize = acc in - let j, x:(usize & usize) = temp_1_ in - (i +! j <: usize) +! x <: usize) - <: - usize) + let acc:usize = + Rust_primitives.Hax.Folds.fold_enumerated_slice chunk + (fun acc temp_1_ -> + let acc:usize = acc in + let _:usize = temp_1_ in + true) + acc + (fun acc temp_1_ -> + let acc:usize = acc in + let j, x:(usize & usize) = temp_1_ in + let acc:usize = (i +! j <: usize) +! x in + acc) + in + acc) in acc -let f (_: Prims.unit) : u8 = +let f (_: Prims.unit) : Prims.unit = let acc:u8 = 0uy in - Rust_primitives.Hax.Folds.fold_range 1uy - 10uy - (fun acc temp_1_ -> - let acc:u8 = acc in - let _:u8 = temp_1_ in - true) - acc - (fun acc i -> - let acc:u8 = acc in - let i:u8 = i in - let acc:u8 = acc +! i in - let _:bool = bool_returning i in - acc) + let acc:u8 = + Rust_primitives.Hax.Folds.fold_range 1uy + 10uy + (fun acc temp_1_ -> + let acc:u8 = acc in + let _:u8 = temp_1_ in + true) + acc + (fun acc i -> + let acc:u8 = acc in + let i:u8 = i in + let acc:u8 = acc +! i in + let _:bool = bool_returning i in + acc) + in + () let iterator (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = let acc:usize = sz 0 in @@ -499,7 +509,8 @@ let iterator (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = (fun acc item -> let acc:usize = acc in let item:usize = item in - acc +! item <: usize) + let acc:usize = acc +! item in + acc) in acc @@ -523,53 +534,61 @@ let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = (fun acc item -> let acc:usize = acc in let item:usize = item in - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Rev.t_Rev - (Core.Ops.Range.t_Range usize)) - #FStar.Tactics.Typeclasses.solve - (Core.Iter.Traits.Iterator.f_rev #(Core.Ops.Range.t_Range usize) - #FStar.Tactics.Typeclasses.solve - ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = item } - <: - Core.Ops.Range.t_Range usize) - <: - Core.Iter.Adapters.Rev.t_Rev (Core.Ops.Range.t_Range usize)) - <: - Core.Iter.Adapters.Rev.t_Rev (Core.Ops.Range.t_Range usize)) - acc - (fun acc i -> - let acc:usize = acc in - let i:usize = i in - let acc:usize = acc +! sz 1 in - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Zip.t_Zip - (Core.Slice.Iter.t_Iter usize) (Core.Ops.Range.t_Range usize)) + let acc:usize = + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Rev.t_Rev + (Core.Ops.Range.t_Range usize)) + #FStar.Tactics.Typeclasses.solve + (Core.Iter.Traits.Iterator.f_rev #(Core.Ops.Range.t_Range usize) #FStar.Tactics.Typeclasses.solve - (Core.Iter.Traits.Iterator.f_zip #(Core.Slice.Iter.t_Iter usize) + ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = item } + <: + Core.Ops.Range.t_Range usize) + <: + Core.Iter.Adapters.Rev.t_Rev (Core.Ops.Range.t_Range usize)) + <: + Core.Iter.Adapters.Rev.t_Rev (Core.Ops.Range.t_Range usize)) + acc + (fun acc i -> + let acc:usize = acc in + let i:usize = i in + let acc:usize = acc +! sz 1 in + let acc:usize = + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Zip.t_Zip + (Core.Slice.Iter.t_Iter usize) (Core.Ops.Range.t_Range usize)) #FStar.Tactics.Typeclasses.solve - #(Core.Ops.Range.t_Range usize) - (Core.Slice.impl__iter #usize - (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) - #FStar.Tactics.Typeclasses.solve - arr + (Core.Iter.Traits.Iterator.f_zip #(Core.Slice.Iter.t_Iter usize) + #FStar.Tactics.Typeclasses.solve + #(Core.Ops.Range.t_Range usize) + (Core.Slice.impl__iter #usize + (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize + Alloc.Alloc.t_Global) + #FStar.Tactics.Typeclasses.solve + arr + <: + t_Slice usize) <: - t_Slice usize) - <: - Core.Slice.Iter.t_Iter usize) - ({ Core.Ops.Range.f_start = sz 4; Core.Ops.Range.f_end = i } + Core.Slice.Iter.t_Iter usize) + ({ Core.Ops.Range.f_start = sz 4; Core.Ops.Range.f_end = i } + <: + Core.Ops.Range.t_Range usize) <: - Core.Ops.Range.t_Range usize) + Core.Iter.Adapters.Zip.t_Zip (Core.Slice.Iter.t_Iter usize) + (Core.Ops.Range.t_Range usize)) <: Core.Iter.Adapters.Zip.t_Zip (Core.Slice.Iter.t_Iter usize) (Core.Ops.Range.t_Range usize)) - <: - Core.Iter.Adapters.Zip.t_Zip (Core.Slice.Iter.t_Iter usize) - (Core.Ops.Range.t_Range usize)) - acc - (fun acc j -> - let acc:usize = acc in - let j:(usize & usize) = j in - (((acc +! item <: usize) +! i <: usize) +! j._1 <: usize) +! j._2 <: usize)) - <: - usize) + acc + (fun acc j -> + let acc:usize = acc in + let j:(usize & usize) = j in + let acc:usize = + (((acc +! item <: usize) +! i <: usize) +! j._1 <: usize) +! j._2 + in + acc) + in + acc) + in + acc) in acc @@ -586,7 +605,8 @@ let pattern (arr: Alloc.Vec.t_Vec (usize & usize) Alloc.Alloc.t_Global) : usize (fun acc temp_1_ -> let acc:usize = acc in let x, y:(usize & usize) = temp_1_ in - acc +! (x *! y <: usize) <: usize) + let acc:usize = acc +! (x *! y <: usize) in + acc) in acc @@ -603,7 +623,8 @@ let range1 (_: Prims.unit) : usize = (fun acc i -> let acc:usize = acc in let i:usize = i in - acc +! i <: usize) + let acc:usize = acc +! i in + acc) in acc @@ -620,7 +641,8 @@ let range2 (n: usize) : usize = (fun acc i -> let acc:usize = acc in let i:usize = i in - (acc +! i <: usize) +! sz 1 <: usize) + let acc:usize = (acc +! i <: usize) +! sz 1 in + acc) in acc @@ -643,7 +665,8 @@ let rev_range (n: usize) : usize = (fun acc i -> let acc:usize = acc in let i:usize = i in - (acc +! i <: usize) +! sz 1 <: usize) + let acc:usize = (acc +! i <: usize) +! sz 1 in + acc) in acc ''' @@ -653,65 +676,77 @@ module Loops.Recognized_loops open Core open FStar.Mul -let enumerated_chunked_slice (#v_T: Type0) (slice: t_Slice v_T) : u64 = +let enumerated_chunked_slice (#v_T: Type0) (slice: t_Slice v_T) : Prims.unit = let count:u64 = 0uL in - Rust_primitives.Hax.Folds.fold_enumerated_chunked_slice (sz 3) - slice - (fun count i -> - let count:u64 = count in - let i:usize = i in - i <= Core.Slice.impl__len #v_T slice <: usize) - count - (fun count i -> - let count:u64 = count in - let i:(usize & t_Slice v_T) = i in - let count:u64 = count +! 3uL in - count) + let count:u64 = + Rust_primitives.Hax.Folds.fold_enumerated_chunked_slice (sz 3) + slice + (fun count i -> + let count:u64 = count in + let i:usize = i in + i <= Core.Slice.impl__len #v_T slice <: usize) + count + (fun count i -> + let count:u64 = count in + let i:(usize & t_Slice v_T) = i in + let count:u64 = count +! 3uL in + count) + in + () -let enumerated_slice (#v_T: Type0) (slice: t_Slice v_T) : u64 = +let enumerated_slice (#v_T: Type0) (slice: t_Slice v_T) : Prims.unit = let count:u64 = 0uL in - Rust_primitives.Hax.Folds.fold_enumerated_slice slice - (fun count i -> - let count:u64 = count in - let i:usize = i in - i <=. sz 10 <: bool) - count - (fun count i -> - let count:u64 = count in - let i:(usize & v_T) = i in - let count:u64 = count +! 2uL in - count) + let count:u64 = + Rust_primitives.Hax.Folds.fold_enumerated_slice slice + (fun count i -> + let count:u64 = count in + let i:usize = i in + i <=. sz 10 <: bool) + count + (fun count i -> + let count:u64 = count in + let i:(usize & v_T) = i in + let count:u64 = count +! 2uL in + count) + in + () -let range (_: Prims.unit) : u64 = +let range (_: Prims.unit) : Prims.unit = let count:u64 = 0uL in - Rust_primitives.Hax.Folds.fold_range 0uy - 10uy - (fun count i -> - let count:u64 = count in - let i:u8 = i in - i <=. 10uy <: bool) - count - (fun count i -> - let count:u64 = count in - let i:u8 = i in - let count:u64 = count +! 1uL in - count) + let count:u64 = + Rust_primitives.Hax.Folds.fold_range 0uy + 10uy + (fun count i -> + let count:u64 = count in + let i:u8 = i in + i <=. 10uy <: bool) + count + (fun count i -> + let count:u64 = count in + let i:u8 = i in + let count:u64 = count +! 1uL in + count) + in + () -let range_step_by (_: Prims.unit) : u64 = +let range_step_by (_: Prims.unit) : Prims.unit = let count:u64 = 0uL in - Rust_primitives.Hax.Folds.fold_range_step_by 0uy - 10uy - (sz 2) - (fun count i -> - let count:u64 = count in - let i:u8 = i in - i <=. 10uy <: bool) - count - (fun count i -> - let count:u64 = count in - let i:u8 = i in - let count:u64 = count +! 1uL in - count) + let count:u64 = + Rust_primitives.Hax.Folds.fold_range_step_by 0uy + 10uy + (sz 2) + (fun count i -> + let count:u64 = count in + let i:u8 = i in + i <=. 10uy <: bool) + count + (fun count i -> + let count:u64 = count in + let i:u8 = i in + let count:u64 = count +! 1uL in + count) + in + () ''' "Loops.While_loops.fst" = ''' module Loops.While_loops diff --git a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap index fee5eaadb..9c1120523 100644 --- a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap @@ -140,18 +140,19 @@ let foo (lhs rhs: t_S) : t_S = (fun lhs i -> let lhs:t_S = lhs in let i:usize = i in - { - lhs with - f_b - = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize lhs.f_b - i - ((lhs.f_b.[ i ] <: u8) +! (rhs.f_b.[ i ] <: u8) <: u8) + let lhs:t_S = + { + lhs with + f_b + = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize lhs.f_b + i + ((lhs.f_b.[ i ] <: u8) +! (rhs.f_b.[ i ] <: u8) <: u8) + } <: - t_Array u8 (sz 5) - } - <: - t_S) + t_S + in + lhs) in lhs @@ -169,16 +170,12 @@ let g (x: t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) (fun x i -> let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = x in let i:u8 = i in - { - x with - f_a - = - Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global x.f_a i + let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = + { x with f_a = Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global x.f_a i } <: - Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global - } - <: - t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) + t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) + in + x) in let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = { x with f_a = Core.Slice.impl__swap #u8 x.f_a (sz 0) (sz 1) } 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 66c41f5fa..ca91a36c2 100644 --- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap @@ -49,7 +49,8 @@ let impl: t_MyFrom u16 u8 = let f (x: u8) : Core.Result.t_Result u16 u16 = match Core.Result.Result_Err 1uy <: Core.Result.t_Result Prims.unit u8 with - | Core.Result.Result_Ok _ -> + | Core.Result.Result_Ok ok -> + let _:Prims.unit = ok in Core.Result.Result_Ok (f_my_from #u16 #u8 #FStar.Tactics.Typeclasses.solve x) <: Core.Result.t_Result u16 u16 @@ -201,7 +202,9 @@ let assign_non_trivial_lhs (foo: t_Foo) : t_Foo = let direct_result_question_mark (y: Core.Result.t_Result Prims.unit u32) : Core.Result.t_Result i8 u32 = match y <: Core.Result.t_Result Prims.unit u32 with - | Core.Result.Result_Ok _ -> Core.Result.Result_Ok 0y <: Core.Result.t_Result i8 u32 + | Core.Result.Result_Ok ok -> + let _:Prims.unit = ok in + Core.Result.Result_Ok 0y <: Core.Result.t_Result i8 u32 | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result i8 u32 /// Question mark with an error coercion @@ -253,7 +256,8 @@ let local_mutation (x: u32) : u32 = (fun y i -> let y:u32 = y in let i:u32 = i in - Core.Num.impl__u32__wrapping_add x i <: u32) + let y:u32 = Core.Num.impl__u32__wrapping_add x i in + y) in Core.Num.impl__u32__wrapping_add x y else @@ -447,6 +451,7 @@ let question_mark (x: u32) : Core.Result.t_Result u32 u32 = then match Core.Result.Result_Err 12uy <: Core.Result.t_Result Prims.unit u8 with | Core.Result.Result_Ok ok -> + let _:Prims.unit = ok in Core.Result.Result_Ok (Core.Num.impl__u32__wrapping_add 3ul x) <: Core.Result.t_Result u32 u32 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 2f2304adb..b3a535f34 100644 --- a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap +++ b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap @@ -198,7 +198,8 @@ Equations local_mutation {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 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 + letb _ := assign todo(term) in + solve_lift (ret_both (tt : 'unit)) : (both (*0*)(L1:|:fset []) (I1) 'unit))) (ret_both (tt : 'unit)) in impl__u32__wrapping_add x y else letb hoist19 := matchb x with | 12 => @@ -294,10 +295,11 @@ Equations simplifiable_return {L1 : {fset Location}} {L2 : {fset Location}} {L3 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 + letm[choice_typeMonad.result_bind_code int32] _ := ifb c3 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 (ret_both (tt : 'unit)) else () in ControlFlow_Continue (letb _ := assign todo(term) in ret_both (tt : 'unit))