Fix rustc coverage tests.

Author: maximebuyse

rustc-coverage-tests/run-coverage-tests.py

@@ -135,7 +135,7 @@ def write_summary(results, stability):
 
 def run_tests(config, target, include_negative, check_stability, update_snapshots):
     results = []
-    all_targets = ["coq", "fstar", "fstar-lax", "lean", "lean-tc" "json"]
+    all_targets = ["coq", "fstar", "fstar-lax", "lean", "lean-tc", "json"]
 
     applicable_targets = [target] if target != "all" else all_targets
 

rustc-coverage-tests/snapshots/fstar/Coverage.Color.fst

@@ -4,9 +4,17 @@ open Core
 open FStar.Mul
 
 let main (_: Prims.unit) : (Prims.unit & Prims.unit) =
-  Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
-    "{\n for _i in (core::iter::traits::collect::f_into_iter(core::ops::range::Range {\n f_start: 0,\n f_end: 0,\n })) {\n Tuple0\n }\n }"
-  ,
+  Rust_primitives.Hax.Folds.fold_range (mk_i32 0)
+    (mk_i32 0)
+    (fun temp_0_ temp_1_ ->
+        let _:Prims.unit = temp_0_ in
+        let _:i32 = temp_1_ in
+        true)
+    ()
+    (fun temp_0_ e_i ->
+        let _:Prims.unit = temp_0_ in
+        let e_i:i32 = e_i in
+        ()),
   ()
   <:
   (Prims.unit & Prims.unit)

rustc-coverage-tests/snapshots/fstar/Coverage.If_not.fst

@@ -58,13 +58,29 @@ let if_not (cond: bool) : Prims.unit =
 
 let main (_: Prims.unit) : (Prims.unit & Prims.unit) =
   let _:Prims.unit =
-    Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
-      "{\n for _ in (core::iter::traits::collect::f_into_iter(core::ops::range::Range {\n f_start: 0,\n f_end: 8,\n })) {\n coverage::if_not::if_not(core::hint::black_box::<bool>(true))\n }\n }"
-
+    Rust_primitives.Hax.Folds.fold_range (mk_i32 0)
+      (mk_i32 8)
+      (fun temp_0_ temp_1_ ->
+          let _:Prims.unit = temp_0_ in
+          let _:i32 = temp_1_ in
+          true)
+      ()
+      (fun temp_0_ temp_1_ ->
+          let _:Prims.unit = temp_0_ in
+          let _:i32 = temp_1_ in
+          if_not (Core.Hint.black_box #bool true <: bool) <: Prims.unit)
   in
-  Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
-    "{\n for _ in (core::iter::traits::collect::f_into_iter(core::ops::range::Range {\n f_start: 0,\n f_end: 4,\n })) {\n coverage::if_not::if_not(core::hint::black_box::<bool>(false))\n }\n }"
-  ,
+  Rust_primitives.Hax.Folds.fold_range (mk_i32 0)
+    (mk_i32 4)
+    (fun temp_0_ temp_1_ ->
+        let _:Prims.unit = temp_0_ in
+        let _:i32 = temp_1_ in
+        true)
+    ()
+    (fun temp_0_ temp_1_ ->
+        let _:Prims.unit = temp_0_ in
+        let _:i32 = temp_1_ in
+        if_not (Core.Hint.black_box #bool false <: bool) <: Prims.unit),
   ()
   <:
   (Prims.unit & Prims.unit)

rustc-coverage-tests/snapshots/fstar/Coverage.Inline.fst

@@ -24,9 +24,31 @@ let display
       (xs: t_Slice v_T)
     : Prims.unit =
   let _:Prims.unit =
-    Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
-      "{\n for x in (core::iter::traits::collect::f_into_iter(xs)) {\n {\n let args: [core::fmt::rt::t_Argument; 1] = {\n [core::fmt::rt::impl__new_display::<T>(x)]\n };\n {\n let _: tuple0 = {\n std::io::stdio::e_p..."
-
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(t_Slice v_T)
+          #FStar.Tactics.Typeclasses.solve
+          xs
+        <:
+        Core.Slice.Iter.t_Iter v_T)
+      ()
+      (fun temp_0_ x ->
+          let _:Prims.unit = temp_0_ in
+          let x:v_T = x in
+          let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) =
+            let list = [Core.Fmt.Rt.impl__new_display #v_T x] in
+            FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+            Rust_primitives.Hax.array_of_list 1 list
+          in
+          let _:Prims.unit =
+            Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 1)
+                  (mk_usize 1)
+                  (let list = [""] in
+                    FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+                    Rust_primitives.Hax.array_of_list 1 list)
+                  args
+                <:
+                Core.Fmt.t_Arguments)
+          in
+          ())
   in
   let _:Prims.unit =
     Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1)

rustc-coverage-tests/snapshots/fstar/Coverage.Let_else_loop.fst

@@ -7,7 +7,7 @@ let loopy (cond: bool) : Prims.unit =
   match cond <: bool with
   | true -> ()
   | _ ->
-    Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
+    Rust_primitives.Hax.failure "something is not implemented yet.\nUnhandled loop kind\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/933.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
       "{\n loop {\n Tuple0\n }\n }",
     ()
     <:
@@ -16,15 +16,15 @@ let loopy (cond: bool) : Prims.unit =
 let e_loop_either_way (cond: bool) : Prims.unit =
   match cond <: bool with
   | true ->
-    Rust_primitives.Hax.never_to_any ((Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
+    Rust_primitives.Hax.never_to_any ((Rust_primitives.Hax.failure "something is not implemented yet.\nUnhandled loop kind\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/933.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
             "{\n loop {\n Tuple0\n }\n }"
           <:
           Prims.unit),
         ()
         <:
         (Prims.unit & Prims.unit))
   | _ ->
-    Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
+    Rust_primitives.Hax.failure "something is not implemented yet.\nUnhandled loop kind\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/933.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
       "{\n loop {\n Tuple0\n }\n }",
     ()
     <:
@@ -33,15 +33,15 @@ let e_loop_either_way (cond: bool) : Prims.unit =
 let e_if (cond: bool) : Prims.unit =
   if cond
   then
-    Rust_primitives.Hax.never_to_any ((Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
+    Rust_primitives.Hax.never_to_any ((Rust_primitives.Hax.failure "something is not implemented yet.\nUnhandled loop kind\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/933.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
             "{\n loop {\n Tuple0\n }\n }"
           <:
           Prims.unit),
         ()
         <:
         (Prims.unit & Prims.unit))
   else
-    Rust_primitives.Hax.never_to_any ((Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
+    Rust_primitives.Hax.never_to_any ((Rust_primitives.Hax.failure "something is not implemented yet.\nUnhandled loop kind\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/933.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
             "{\n loop {\n Tuple0\n }\n }"
           <:
           Prims.unit),

rustc-coverage-tests/snapshots/fstar/Coverage.Loop_break.fst

@@ -4,7 +4,7 @@ open Core
 open FStar.Mul
 
 let main (_: Prims.unit) : (Prims.unit & Prims.unit) =
-  Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
+  Rust_primitives.Hax.failure "something is not implemented yet.\nUnhandled loop kind\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/933.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
     "{\n loop {\n (if core::hint::black_box::<bool>(true) {\n core::ops::control_flow::ControlFlow_Break(Tuple2(Tuple0, Tuple0()))\n } else {\n core::ops::control_flow::ControlFlow_Continue(Tuple0)\n })\n }\n }"
   ,
   ()

rustc-coverage-tests/snapshots/fstar/Coverage.Loop_break_value.fst

@@ -5,7 +5,7 @@ open FStar.Mul
 
 let main (_: Prims.unit) : Prims.unit =
   let result:i32 =
-    Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
+    Rust_primitives.Hax.failure "something is not implemented yet.\nUnhandled loop kind\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/933.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
       "{\n loop {\n core::ops::control_flow::ControlFlow_Break(Tuple2(10, Tuple0()))\n }\n }",
     ()
     <: