Fix: Don't crash when someone uses a macro-rules macro to generate a for loop. (#2763)

Author: parno

source/rust_verify/src/fn_call_to_vir.rs

@@ -2852,6 +2852,14 @@ pub(crate) fn fix_node_substs<'tcx, 'a>(
             let generic_arg1 = GenericArg::from(types.expr_ty_adjusted(&args[0]));
             tcx.mk_args(&[generic_arg0, generic_arg1])
         }
+        Some(RustItem::IntoIterFn) if node_substs.is_empty() => {
+            // A `for` loop produced by a `macro_rules!` expansion is not rewritten
+            // by the `verus!` macro, so it reaches rustc's native for-loop
+            // desugaring, which emits an `IntoIterator::into_iter` call whose
+            // node_substs is empty instead of carrying the Self type argument.
+            let generic_arg = GenericArg::from(types.expr_ty_adjusted(&args[0]));
+            tcx.mk_args(&[generic_arg])
+        }
         _ => node_substs,
     }
 }

source/rust_verify/src/rust_to_vir_expr.rs

@@ -3422,6 +3422,17 @@ pub(crate) fn expr_to_vir_innermost<'tcx>(
                 Ok(ExprOrPlace::Place(p))
             }
         }
+        ExprKind::Loop(_, _, LoopSource::ForLoop, _) => {
+            // The `verus!` macro rewrites `for` loops internally before they
+            // reach rustc's native for-loop desugaring, so a `LoopSource::ForLoop`
+            // only shows up here when the `for` loop was not visited by `verus!`
+            unsupported_err!(
+                expr.span,
+                format!(
+                    "`for` loops produced by a macro expansion (wrap the loop in the macro body with `verus_exec_expr! {{ ... }}`)"
+                )
+            )
+        }
         ExprKind::Loop(..) => unsupported_err!(expr.span, format!("complex loop expressions")),
         ExprKind::Break(..) => unsupported_err!(expr.span, format!("complex break expressions")),
         ExprKind::AssignOp(op, lhs, rhs) => {

source/rust_verify_test/tests/loops.rs

@@ -1946,3 +1946,16 @@ test_verify_one_file! {
         }
     } => Err(err) => assert_fails(err, 1)
 }
+
+test_verify_one_file! {
+    // A `for` loop produced by a `macro_rules!` expansion is not rewritten by the
+    // `verus!` macro, so it reaches rustc's native for-loop desugaring.
+    #[test] macro_rules_for_loop_no_ice_issue2751 verus_code! {
+        fn f() {
+            macro_rules! m {
+                () => { for _ in 0..1 {} };
+            }
+            m!();
+        }
+    } => Err(err) => assert_vir_error_msg(err, "`for` loops produced by a macro expansion")
+}