fix: handle panics for Structural

source/rust_verify/src/fn_call_to_vir.rs

@@ -904,6 +904,12 @@ fn verus_item_to_vir<'tcx, 'a>(
                 }
             }
             ExprItem::StrSliceLen => {
+                if !matches!(bctx.ctxt.cmd_line_args.vstd, Vstd::IsVstd | Vstd::IsCore) {
+                    return err_span(
+                        expr.span,
+                        "verus_builtin::strslice_len is for internal use only and cannot be used directly in user programs",
+                    );
+                }
                 record_spec_fn(bctx, expr);
                 match &expr.kind {
                     ExprKind::Call(_, args) => {
@@ -919,6 +925,12 @@ fn verus_item_to_vir<'tcx, 'a>(
                 }
             }
             ExprItem::StrSliceGetChar => {
+                if !matches!(bctx.ctxt.cmd_line_args.vstd, Vstd::IsVstd | Vstd::IsCore) {
+                    return err_span(
+                        expr.span,
+                        "verus_builtin::strslice_get_char is for internal use only and cannot be used directly in user programs",
+                    );
+                }
                 record_spec_fn(bctx, expr);
                 match &expr.kind {
                     ExprKind::Call(_, args) if args.len() == 2 => {

source/rust_verify/src/rust_to_vir_base.rs

@@ -1737,7 +1737,7 @@ pub(crate) fn try_get_proof_fn_modes<'tcx>(
                 let ret_mode = if let Some(ty) = ret_mode_typ.as_type() {
                     get_proof_fn_one_mode(ctxt, span, &ty)?
                 } else {
-                    panic!("unexpected FnProof argument")
+                    return err_span(span, "unexpected FnProof argument")
                 };
                 let arg_modes = if let Some(ty) = arg_mode_tuple.as_type() {
                     if let TyKind::Tuple(_) = ty.kind() {
@@ -1747,10 +1747,10 @@ pub(crate) fn try_get_proof_fn_modes<'tcx>(
                         }
                         modes
                     } else {
-                        panic!("unexpected FnProof argument")
+                        return err_span(span, "unexpected FnProof argument")
                     }
                 } else {
-                    panic!("unexpected FnProof argument")
+                    return err_span(span, "unexpected FnProof argument")
                 };
                 return Ok(Some((arg_modes, ret_mode)));
             }

source/rust_verify/src/rust_to_vir_impl.rs

@@ -278,7 +278,12 @@ pub(crate) fn translate_impl<'tcx>(
                 // ?
                 let def_id = match impll.self_ty.kind {
                     rustc_hir::TyKind::Path(QPath::Resolved(None, path)) => path.res.def_id(),
-                    _ => panic!("self type of impl is not resolved: {:?}", impll.self_ty.kind),
+                    _ => {
+                        return err_span_vec(
+                            item.span,
+                            "`Structural` can only be implemented for struct or enum types",
+                        )
+                    }
                 };
                 ctxt.tcx.type_of(def_id).skip_binder()
             };
@@ -295,7 +300,10 @@ pub(crate) fn translate_impl<'tcx>(
                     })),
                 )
             } else {
-                panic!("Structural impl for non-adt type");
+                return err_span_vec(
+                    item.span,
+                    "`Structural` can only be implemented for struct or enum types",
+                );
             };
             let ty_applied_never = ctxt.tcx.mk_ty_from_kind(ty_kind_applied_never);
             if !ty_applied_never.is_structural_eq_shallow(ctxt.tcx) {

source/vir/src/triggers_auto.rs

@@ -300,6 +300,21 @@ fn make_score(term: &Term, depth: u64) -> Score {
     }
 }
 
+fn check_no_reachable_internal_auto_trigger_ops(exp: &Exp) -> Result<(), VirErr> {
+    let mut scope_map = air::scope_map::ScopeMap::new();
+    crate::sst_visitor::exp_visitor_check(exp, &mut scope_map, &mut |expr, _scope_map| match &expr.x {
+        ExpX::Unary(UnaryOp::StrLen, _) | ExpX::Binary(BinaryOp::StrGetChar, _, _) => Err(error(
+            &expr.span,
+            "automatic trigger inference does not support internal string operations from verus_builtin",
+        )),
+        ExpX::Unary(UnaryOp::CastToInteger, _) => Err(error(
+            &expr.span,
+            "automatic trigger inference encountered an internal integer cast operation",
+        )),
+        _ => Ok(()),
+    })
+}
+
 fn gather_terms(ctxt: &mut Ctxt, ctx: &Ctx, exp: &Exp, depth: u64) -> (bool, Term) {
     let fail_on_strop = || {
         unreachable!(
@@ -761,6 +776,7 @@ pub(crate) fn build_triggers(
         ctxt.pure_terms_by_var.insert(x.clone(), HashMap::new());
     }
     let mut timer = Timer { span: span.clone(), timeout_countdown: 10000 };
+    check_no_reachable_internal_auto_trigger_ops(exp)?;
     gather_terms(&mut ctxt, ctx, exp, 0);
     /*
     println!();