Merge pull request #1223 from cryspen/fix-double-return

fix(engine) Attempt to fix double return bug.

engine/lib/phases/phase_and_mut_defsite.ml

@@ -118,9 +118,16 @@ struct
           match e.e with
           | GlobalVar (`TupleCons 0) -> e
           | _ ->
-              let lhs = UB.make_var_pat var e.typ e.span in
               let rhs = e in
-              let body = { e with e = LocalVar var } in
+              let lhs, body =
+                if [%eq: ty] e.typ UB.unit_typ then
+                  (* This case has been added to fix https://github.com/hacspec/hax/issues/720.
+                     It might need a better solution. *)
+                  ( UB.M.pat_PWild ~span:e.span ~typ:e.typ,
+                    UB.M.expr_unit ~span:e.span )
+                else
+                  (UB.make_var_pat var e.typ e.span, { e with e = LocalVar var })
+              in
               { body with e = Let { monadic = None; lhs; rhs; body } }
         in
         UB.map_body_of_nested_lets f e

engine/lib/phases/phase_local_mutation.ml

@@ -267,6 +267,7 @@ struct
           }
       | Loop { body; kind; state; label; witness; _ } ->
           let variables_to_output = s.expr_level in
+          let drop_expr = s.drop_expr in
           (* [adapt]: should we reorder shadowings? *)
           let observable_mutations, adapt =
             let set =
@@ -338,27 +339,32 @@ struct
               span;
             }
           in
-          if adapt && not (List.is_empty variables_to_output) then
-            (* here, we need to introduce the shadowings as bindings *)
-            let out =
-              UB.make_tuple_expr ~span
-              @@ List.map
-                   ~f:(fun (ident, typ) -> B.{ e = LocalVar ident; typ; span })
-                   variables_to_output
-            in
-            let lhs =
-              UB.make_tuple_pat
-              @@ List.map
-                   ~f:(fun (ident, typ) -> UB.make_var_pat ident typ span)
-                   observable_mutations
-            in
-            B.
-              {
-                e = Let { monadic = None; lhs; rhs = loop; body = out };
-                span;
-                typ = out.typ;
-              }
-          else loop
+          let vars =
+            if adapt && not (List.is_empty variables_to_output) then
+              (* here, we need to introduce the shadowings as bindings *)
+              let out =
+                UB.make_tuple_expr ~span
+                @@ List.map
+                     ~f:(fun (ident, typ) ->
+                       B.{ e = LocalVar ident; typ; span })
+                     variables_to_output
+              in
+              let lhs =
+                UB.make_tuple_pat
+                @@ List.map
+                     ~f:(fun (ident, typ) -> UB.make_var_pat ident typ span)
+                     observable_mutations
+              in
+              B.
+                {
+                  e = Let { monadic = None; lhs; rhs = loop; body = out };
+                  span;
+                  typ = out.typ;
+                }
+            else loop
+          in
+          if drop_expr then vars
+          else UB.make_tuple_expr ~span [ vars; UB.unit_expr span ]
       | [%inline_arms
           "dexpr'.*" - Let - Assign - Closure - Loop - If - Match - Break
           - Return] ->

test-harness/src/snapshots/toolchain__attributes into-fstar.snap

@@ -419,7 +419,7 @@ let impl: t_Foo Prims.unit =
     f_i
     =
     fun (x: u8) (y: u8) ->
-      let hax_temp_output:Prims.unit = () <: Prims.unit in
+      let _:Prims.unit = () <: Prims.unit in
       y
   }
 '''

test-harness/src/snapshots/toolchain__loops into-fstar.snap

@@ -27,6 +27,57 @@ stderr = 'Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'
 diagnostics = []
 
 [stdout.files]
+"Loops.And_mut_side_effect_loop.fst" = '''
+module Loops.And_mut_side_effect_loop
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+let looping (array: t_Array u8 (sz 5)) : t_Array u8 (sz 5) =
+  let array:t_Array u8 (sz 5) =
+    Rust_primitives.Hax.Folds.fold_range (sz 0)
+      (Core.Slice.impl__len #u8 (array <: t_Slice u8) <: usize)
+      (fun array temp_1_ ->
+          let array:t_Array u8 (sz 5) = array in
+          let _:usize = temp_1_ in
+          true)
+      array
+      (fun array i ->
+          let array:t_Array u8 (sz 5) = array in
+          let i:usize = i in
+          Rust_primitives.Hax.Monomorphized_update_at.update_at_usize array
+            i
+            (cast (i <: usize) <: u8)
+          <:
+          t_Array u8 (sz 5))
+  in
+  array
+
+let looping_2_ (array: t_Array u8 (sz 5)) : t_Array u8 (sz 5) =
+  let array, result:(t_Array u8 (sz 5) & Prims.unit) =
+    Rust_primitives.Hax.Folds.fold_range (sz 0)
+      (Core.Slice.impl__len #u8 (array <: t_Slice u8) <: usize)
+      (fun array temp_1_ ->
+          let array:t_Array u8 (sz 5) = array in
+          let _:usize = temp_1_ in
+          true)
+      array
+      (fun array i ->
+          let array:t_Array u8 (sz 5) = array in
+          let i:usize = i in
+          Rust_primitives.Hax.Monomorphized_update_at.update_at_usize array
+            i
+            (cast (i <: usize) <: u8)
+          <:
+          t_Array u8 (sz 5)),
+    ()
+    <:
+    (t_Array u8 (sz 5) & Prims.unit)
+  in
+  let _:Prims.unit = admit () (* Panic freedom *) in
+  let _:Prims.unit = result in
+  array
+'''
 "Loops.Control_flow.fst" = '''
 module Loops.Control_flow
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -463,7 +514,7 @@ let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
   in
   acc
 
-let f (_: Prims.unit) : u8 =
+let f (_: Prims.unit) : (u8 & Prims.unit) =
   let acc:u8 = 0uy in
   Rust_primitives.Hax.Folds.fold_range 1uy
     10uy
@@ -477,7 +528,10 @@ let f (_: Prims.unit) : u8 =
         let i:u8 = i in
         let acc:u8 = acc +! i in
         let _:bool = bool_returning i in
-        acc)
+        acc),
+  ()
+  <:
+  (u8 & Prims.unit)
 
 let iterator (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
   let acc:usize = sz 0 in
@@ -653,7 +707,7 @@ 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) : (u64 & Prims.unit) =
   let count:u64 = 0uL in
   Rust_primitives.Hax.Folds.fold_enumerated_chunked_slice (sz 3)
     slice
@@ -666,9 +720,12 @@ let enumerated_chunked_slice (#v_T: Type0) (slice: t_Slice v_T) : u64 =
         let count:u64 = count in
         let i:(usize & t_Slice v_T) = i in
         let count:u64 = count +! 3uL in
-        count)
+        count),
+  ()
+  <:
+  (u64 & Prims.unit)
 
-let enumerated_slice (#v_T: Type0) (slice: t_Slice v_T) : u64 =
+let enumerated_slice (#v_T: Type0) (slice: t_Slice v_T) : (u64 & Prims.unit) =
   let count:u64 = 0uL in
   Rust_primitives.Hax.Folds.fold_enumerated_slice slice
     (fun count i ->
@@ -680,9 +737,12 @@ let enumerated_slice (#v_T: Type0) (slice: t_Slice v_T) : u64 =
         let count:u64 = count in
         let i:(usize & v_T) = i in
         let count:u64 = count +! 2uL in
-        count)
+        count),
+  ()
+  <:
+  (u64 & Prims.unit)
 
-let range (_: Prims.unit) : u64 =
+let range (_: Prims.unit) : (u64 & Prims.unit) =
   let count:u64 = 0uL in
   Rust_primitives.Hax.Folds.fold_range 0uy
     10uy
@@ -695,9 +755,12 @@ let range (_: Prims.unit) : u64 =
         let count:u64 = count in
         let i:u8 = i in
         let count:u64 = count +! 1uL in
-        count)
+        count),
+  ()
+  <:
+  (u64 & Prims.unit)
 
-let range_step_by (_: Prims.unit) : u64 =
+let range_step_by (_: Prims.unit) : (u64 & Prims.unit) =
   let count:u64 = 0uL in
   Rust_primitives.Hax.Folds.fold_range_step_by 0uy
     10uy
@@ -711,7 +774,10 @@ let range_step_by (_: Prims.unit) : u64 =
         let count:u64 = count in
         let i:u8 = i in
         let count:u64 = count +! 1uL in
-        count)
+        count),
+  ()
+  <:
+  (u64 & Prims.unit)
 '''
 "Loops.While_loops.fst" = '''
 module Loops.While_loops

tests/loops/src/lib.rs

@@ -244,3 +244,19 @@ mod control_flow {
         sum
     }
 }
+
+mod and_mut_side_effect_loop {
+    // https://github.com/hacspec/hax/issues/720
+    fn looping(array: &mut [u8; 5]) {
+        for i in 0..array.len() {
+            array[i] = i as u8;
+        }
+    }
+
+    #[hax_lib::fstar::verification_status(panic_free)]
+    fn looping_2(array: &mut [u8; 5]) {
+        for i in 0..array.len() {
+            array[i] = i as u8;
+        }
+    }
+}