hax_types/diagnostics/
mod.rs

1use crate::prelude::*;
2use colored::Colorize;
3
4pub mod message;
5pub mod report;
6
7#[derive_group(Serializers)]
8#[derive(Debug, Clone, JsonSchema, Eq, PartialEq, Hash)]
9pub struct Diagnostics {
10    pub kind: Kind,
11    pub span: Vec<hax_frontend_exporter::Span>,
12    pub context: String,
13    pub owner_id: Option<hax_frontend_exporter::DefId>,
14}
15
16impl std::fmt::Display for Diagnostics {
17    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
18        match &self.kind {
19            Kind::Unimplemented { issue_id:_, details } => write!(
20                f,
21                "something is not implemented yet.\n{}",
22                match details {
23                    Some(details) => format!("{}", details),
24                    _ => "".to_string(),
25                },
26            ),
27            Kind::UnsupportedMacro { id } => write!(
28                f,
29                "The unexpanded macro {} is not supported by this backend.\nPlease verify the argument you passed to the {} (or {}) option.",
30                id.bold(),
31                "--inline-macro-call".bold(), "-i".bold()
32            ),
33            Kind::UnsafeBlock => write!(f, "Unsafe blocks are not allowed."),
34            Kind::AssertionFailure {details} => write!(
35                f,
36                "Fatal error: something we considered as impossible occurred! {}\nDetails: {}",
37                "Please report this by submitting an issue on GitHub!".bold(),
38                details
39            ),
40            Kind::UnallowedMutRef => write!(
41                f,
42                "The mutation of this {} is not allowed here.",
43                "&mut".bold()
44            ),
45            Kind::ExpectedMutRef => write!(
46                f,
47                "At this position, Hax was expecting an expression of the shape `&mut _`.\nHax forbids `f(x)` (where `f` expects a mutable reference as input) when `x` is not a {}{} or when it is a dereference expression.
48
49{}",
50                "place expression".bold(),
51                "[1]".bright_black(),
52                "[1]: https://doc.rust-lang.org/reference/expressions.html#place-expressions-and-value-expressions"
53            ),
54            Kind::ClosureMutatesParentBindings {bindings} => write!(
55                f,
56                "The bindings {:?} cannot be mutated here: they don't belong to the closure scope, and this is not allowed.",
57                bindings
58            ),
59            Kind::ArbitraryLHS => write!(f, "Assignation of an arbitrary left-hand side is not supported.\n`lhs = e` is fine only when `lhs` is a combination of local identifiers, field accessors and index accessors."),
60
61            Kind::AttributeRejected {reason} => write!(f, "Here, this attribute cannot be used: {reason}."),
62
63            Kind::NonTrivialAndMutFnInput => write!(f, "The support in hax of function with one or more inputs of type `&mut _` is limited.\nOnly trivial patterns are allowed there: `fn f(x: &mut (T, U)) ...` is allowed while `f((x, y): &mut (T, U))` is rejected."),
64
65            Kind::FStarParseError { fstar_snippet, details: _ } => write!(f, "The following code snippet could not be parsed as valid F*:\n```\n{fstar_snippet}\n```"),
66
67            Kind::ExplicitRejection { reason , .. } => write!(f, "Explicit rejection by a phase in the Hax engine:\n{}", reason),
68
69            _ => write!(f, "{:?}", self.kind),
70        }?;
71        write!(f, "\n\n")?;
72        if let Some(issue) = self.kind.issue_number() {
73            write!(
74                f,
75                "This is discussed in issue https://github.com/hacspec/hax/issues/{issue}.\nPlease upvote or comment this issue if you see this error message.\n"
76            )?;
77        }
78        write!(
79            f,
80            "{}",
81            format!(
82                "Note: the error was labeled with context `{}`.\n",
83                self.context
84            )
85            .bright_black()
86        )?;
87        Ok(())
88    }
89}
90
91impl Kind {
92    fn issue_number(&self) -> Option<u32> {
93        match self {
94            Kind::UnsafeBlock => None,
95            Kind::ExplicitRejection { issue_id, .. } | Kind::Unimplemented { issue_id, .. } => {
96                issue_id.clone()
97            }
98            Kind::AssertionFailure { .. } => None,
99            Kind::UnallowedMutRef => Some(420),
100            Kind::UnsupportedMacro { .. } => None,
101            Kind::ErrorParsingMacroInvocation { .. } => None,
102            Kind::ClosureMutatesParentBindings { .. } => Some(1060),
103            Kind::ArbitraryLHS => None,
104            Kind::UnsupportedTupleSize { .. } => None,
105            Kind::ExpectedMutRef => Some(420),
106            Kind::NonTrivialAndMutFnInput => Some(1405),
107            Kind::AttributeRejected { .. } => None,
108            Kind::FStarParseError { .. } => todo!(),
109        }
110    }
111}
112
113#[derive_group(Serializers)]
114#[derive(Debug, Clone, Hash, Eq, PartialEq, Ord, PartialOrd, JsonSchema)]
115#[repr(u16)]
116pub enum Kind {
117    /// Unsafe code is not supported
118    UnsafeBlock = 0,
119
120    /// A feature is not currently implemented
121    Unimplemented {
122        /// Issue on the GitHub repository
123        issue_id: Option<u32>,
124        details: Option<String>,
125    } = 1,
126
127    /// Unknown error
128    // This is useful when doing sanity checks (i.e. one can yield
129    // this error kind for cases that should never happen)
130    AssertionFailure {
131        details: String,
132    } = 2,
133
134    /// Unallowed mutable reference
135    UnallowedMutRef = 3,
136
137    /// Unsupported macro invokation
138    UnsupportedMacro {
139        id: String,
140    } = 4,
141
142    /// Error parsing a macro invocation to a macro treated specifcially by a backend
143    ErrorParsingMacroInvocation {
144        macro_id: String,
145        details: String,
146    } = 5,
147
148    /// Mutation of bindings living outside a closure scope are not supported
149    ClosureMutatesParentBindings {
150        bindings: Vec<String>,
151    } = 6,
152
153    /// Assignation of an arbitrary left-hand side is not supported. `lhs = e` is fine only when `lhs` is a combination of local identifiers, field accessors and index accessors.
154    ArbitraryLHS = 7,
155
156    /// A phase explicitely rejected this chunk of code
157    ExplicitRejection {
158        reason: String,
159        issue_id: Option<u32>,
160    } = 8,
161
162    /// A backend doesn't support a tuple size
163    UnsupportedTupleSize {
164        tuple_size: u32,
165        reason: String,
166    } = 9,
167
168    ExpectedMutRef = 10,
169
170    /// &mut inputs should be trivial patterns
171    NonTrivialAndMutFnInput = 11,
172
173    /// An hax attribute (from `hax-lib-macros`) was rejected
174    AttributeRejected {
175        reason: String,
176    } = 12,
177
178    /// A snippet of F* code could not be parsed
179    FStarParseError {
180        fstar_snippet: String,
181        details: String,
182    } = 13,
183}
184
185impl Kind {
186    // https://doc.rust-lang.org/reference/items/enumerations.html#pointer-casting
187    pub fn discriminant(&self) -> u16 {
188        unsafe { *(self as *const Self as *const u16) }
189    }
190
191    pub fn code(&self) -> String {
192        format!("HAX{:0>4}", self.discriminant())
193    }
194}
hax_types/diagnostics/mod.rs

hax_types/diagnostics/
mod.rs
