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

hax_types/diagnostics/
mod.rs
