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 { .. } => None,
109            Kind::OcamlEngineErrorPayload { .. } => None,
110        }
111    }
112}
113
114#[derive_group(Serializers)]
115#[derive(Debug, Clone, Hash, Eq, PartialEq, Ord, PartialOrd, JsonSchema)]
116#[repr(u16)]
117pub enum Kind {
118    /// Unsafe code is not supported
119    UnsafeBlock = 0,
120
121    /// A feature is not currently implemented
122    Unimplemented {
123        /// Issue on the GitHub repository
124        issue_id: Option<u32>,
125        details: Option<String>,
126    } = 1,
127
128    /// Unknown error
129    // This is useful when doing sanity checks (i.e. one can yield
130    // this error kind for cases that should never happen)
131    AssertionFailure {
132        details: String,
133    } = 2,
134
135    /// Unallowed mutable reference
136    UnallowedMutRef = 3,
137
138    /// Unsupported macro invokation
139    UnsupportedMacro {
140        id: String,
141    } = 4,
142
143    /// Error parsing a macro invocation to a macro treated specifcially by a backend
144    ErrorParsingMacroInvocation {
145        macro_id: String,
146        details: String,
147    } = 5,
148
149    /// Mutation of bindings living outside a closure scope are not supported
150    ClosureMutatesParentBindings {
151        bindings: Vec<String>,
152    } = 6,
153
154    /// 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.
155    ArbitraryLHS = 7,
156
157    /// A phase explicitely rejected this chunk of code
158    ExplicitRejection {
159        reason: String,
160        issue_id: Option<u32>,
161    } = 8,
162
163    /// A backend doesn't support a tuple size
164    UnsupportedTupleSize {
165        tuple_size: u32,
166        reason: String,
167    } = 9,
168
169    ExpectedMutRef = 10,
170
171    /// &mut inputs should be trivial patterns
172    NonTrivialAndMutFnInput = 11,
173
174    /// An hax attribute (from `hax-lib-macros`) was rejected
175    AttributeRejected {
176        reason: String,
177    } = 12,
178
179    /// A snippet of F* code could not be parsed
180    FStarParseError {
181        fstar_snippet: String,
182        details: String,
183    } = 13,
184
185    /// Internal encoding
186    OcamlEngineErrorPayload(String) = 9999,
187}
188
189impl Kind {
190    // https://doc.rust-lang.org/reference/items/enumerations.html#pointer-casting
191    pub fn discriminant(&self) -> u16 {
192        unsafe { *(self as *const Self as *const u16) }
193    }
194
195    pub fn code(&self) -> String {
196        format!("HAX{:0>4}", self.discriminant())
197    }
198}
hax_types/diagnostics/mod.rs

hax_types/diagnostics/
mod.rs
