charon_driver/hax/utils/
error_macros.rs

1macro_rules! format_with_context {
2    ($format_str:expr $(,$arg:expr)* $(; {$($x:expr),*})?) => {
3        format!(
4            concat!(
5                $format_str
6                $(, "\n\nContext:\n", $(concat!(" - ", stringify!($x), ": "), "{:#?}", "\n",)*)?
7            ),
8            $($arg,)*
9            $($($x,)*)?
10        )
11    };
12    ($($tt:tt)*) => {format!($($tt)*)};
13}
14
15mod internal_helpers {
16    macro_rules! _verb {
17        (fatal, $o:expr, $message:expr) => {
18            $o.struct_fatal($message)
19        };
20        (error, $o:expr, $message:expr) => {
21            $o.struct_err($message)
22        };
23        (warn, $o:expr, $message:expr) => {
24            $o.struct_warn($message)
25        };
26    }
27    macro_rules! _span_verb_base {
28        ($verb:ident, $s:ident, $span:expr, $message:expr) => {{
29            let backtrace = std::backtrace::Backtrace::capture();
30            eprintln!("{}", backtrace);
31            let mut builder = $crate::hax::utils::_verb!($verb, $s.base().tcx.dcx(), $message);
32            if let Some(span) = $span {
33                builder.span(span.clone());
34            }
35            builder.code(rustc_errors::codes::ErrCode::MAX);
36            builder.emit()
37        }};
38    }
39
40    pub(crate) use _span_verb_base;
41    pub(crate) use _verb;
42}
43
44macro_rules! report {
45    ($verb:ident, $s:ident [$span:expr], $($tt:tt)*) => {
46        $crate::hax::utils::_span_verb_base!($verb, $s, Some($span), $crate::hax::utils::format_with_context!($($tt)*))
47    };
48    ($verb:ident, $s:ident, $($tt:tt)*) => {
49        $crate::hax::utils::_span_verb_base!(
50            $verb,
51            $s,
52            $s.base().opt_def_id.map(|did| $s.base().tcx.def_span(did)),
53            $crate::hax::utils::format_with_context!($($tt)*)
54        )
55    };
56}
57
58#[allow(unused_macros)]
59macro_rules! warning { ($($tt:tt)*) => {$crate::hax::utils::report!(warn, $($tt)*)} }
60macro_rules! fatal { ($($tt:tt)*) => {$crate::hax::utils::report!(fatal, $($tt)*)} }
61
62pub(crate) use format_with_context;
63pub(crate) use internal_helpers::_span_verb_base;
64pub(crate) use internal_helpers::_verb;
65pub(crate) use report;
66
67macro_rules! supposely_unreachable_message {
68    ($label:literal) => {
69        concat!(
70            "Supposely unreachable place in the Rust AST. The label is ",
71            stringify!($label),
72            ".\nThis error report happend because some assumption about the Rust AST was broken."
73        )
74    };
75}
76
77macro_rules! supposely_unreachable_fatal {
78    ($s:ident $([$span:expr])?, $label:literal $($tt:tt)*) => {
79        $crate::hax::utils::fatal!($s$([$span])?, $crate::hax::utils::supposely_unreachable_message!($label) $($tt)+)
80    };
81}
82
83pub(crate) use fatal;
84pub(crate) use supposely_unreachable_fatal;
85pub(crate) use supposely_unreachable_message;
86#[allow(unused_imports)]
87pub(crate) use warning;
88
89pub trait SExpect: Sized {
90    type Output;
91    fn s_expect<'tcx, S: crate::hax::BaseState<'tcx>>(self, s: &S, message: &str) -> Self::Output;
92
93    fn s_unwrap<'tcx, S: crate::hax::BaseState<'tcx>>(self, s: &S) -> Self::Output {
94        self.s_expect(s, "")
95    }
96}
97
98mod s_expect_impls {
99    use super::*;
100    struct Dummy;
101    impl std::fmt::Debug for Dummy {
102        fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
103            write!(f, "...")
104        }
105    }
106
107    fn s_expect_error<'tcx>(
108        s: &impl crate::hax::BaseState<'tcx>,
109        expected: impl std::fmt::Debug,
110        got: impl std::fmt::Debug,
111        message: &str,
112    ) -> ! {
113        fatal!(
114            s,
115            "s_expect: expected {:?}, got {:?}. {}",
116            expected,
117            got,
118            message
119        )
120    }
121
122    impl<T: std::fmt::Debug> SExpect for Option<T> {
123        type Output = T;
124        fn s_expect<'tcx, S: crate::hax::BaseState<'tcx>>(
125            self,
126            s: &S,
127            message: &str,
128        ) -> Self::Output {
129            self.unwrap_or_else(|| s_expect_error(s, Some(Dummy), None::<()>, message))
130        }
131    }
132
133    impl<T: std::fmt::Debug, E: std::fmt::Debug> SExpect for Result<T, E> {
134        type Output = T;
135        fn s_expect<'tcx, S: crate::hax::BaseState<'tcx>>(
136            self,
137            s: &S,
138            message: &str,
139        ) -> Self::Output {
140            self.unwrap_or_else(|e| s_expect_error(s, Ok::<_, ()>(Dummy), Err::<(), _>(e), message))
141        }
142    }
143}
charon_driver/hax/utils/error_macros.rs

charon_driver/hax/utils/
error_macros.rs
