hax_rust_engine/ast/
span.rs

1//! Source positions.
2
3use crate::interning::{Internable, Interned, InterningTable};
4use hax_rust_engine_macros::*;
5use std::sync::{LazyLock, Mutex};
6
7/// Creates a fresh identifier for a span.
8fn fresh_id() -> u32 {
9    use std::sync::atomic::{AtomicU32 as AtomicInt, Ordering};
10    static CURRENT_ID: AtomicInt = AtomicInt::new(0);
11    CURRENT_ID.fetch_add(1, Ordering::Relaxed)
12}
13
14/// Position of a Rust source
15#[derive_group_for_ast]
16struct SpanData {
17    /// A vector of spans as defined by the frontend.
18    /// This is useful for supporting in a trivial way union of spans.
19    data: Vec<hax_frontend_exporter::Span>,
20    /// A reference to the item in which this span lives. This information is
21    /// used for debugging and profiling purposes, e.g. for `cargo hax into
22    /// --stats backend`.
23    owner_hint: Option<Interned<hax_frontend_exporter::DefId>>,
24}
25
26impl SpanData {
27    /// Creates a dummy span.
28    fn dummy() -> Self {
29        let lo: hax_frontend_exporter::Loc = hax_frontend_exporter::Loc { line: 0, col: 0 };
30        let hi = lo.clone();
31        SpanData {
32            data: vec![hax_frontend_exporter::Span {
33                lo,
34                hi,
35                filename: hax_frontend_exporter::FileName::Custom("dumny".into()),
36                rust_span_data: None,
37            }],
38            owner_hint: None,
39        }
40    }
41
42    /// Creates a [`Span`] given information from the hax exporter.
43    fn from_exporter(
44        span: hax_frontend_exporter::Span,
45        owner_hint: Option<&hax_frontend_exporter::DefId>,
46    ) -> Self {
47        Self {
48            data: vec![span],
49            owner_hint: owner_hint.map(Interned::intern),
50        }
51    }
52}
53
54/// Position of a Rust source
55#[derive_group_for_ast]
56#[derive(Copy)]
57pub struct Span {
58    #[serde(flatten)]
59    data: Interned<SpanData>,
60    /// A unique identifier. Since we store spans almost for every node of the
61    /// AST, having a unique identifier for spans gives us a fine-grained way of
62    /// refering to sub-nodes in debugging context. This id is indeed mostly
63    /// used by the web debugger.
64    id: u32,
65}
66
67impl Internable for SpanData {
68    fn interning_table() -> &'static Mutex<InterningTable<Self>> {
69        static TABLE: LazyLock<Mutex<InterningTable<SpanData>>> =
70            LazyLock::new(|| Mutex::new(InterningTable::default()));
71        &TABLE
72    }
73}
74
75impl Span {
76    /// Creates a dummy span.
77    pub fn dummy() -> Self {
78        static DUMMY_SPAN: LazyLock<Span> = LazyLock::new(|| {
79            let data = Interned::intern(&SpanData::dummy());
80            Span {
81                data,
82                id: fresh_id(),
83            }
84        });
85        *DUMMY_SPAN
86    }
87
88    /// Creates a [`Span`] given information from the hax exporter.
89    pub fn from_exporter(
90        span: hax_frontend_exporter::Span,
91        owner_hint: Option<&hax_frontend_exporter::DefId>,
92    ) -> Self {
93        let data = Interned::intern(&SpanData::from_exporter(span, owner_hint));
94        Self {
95            data,
96            id: fresh_id(),
97        }
98    }
99
100    /// Get a vector of frontend spans given a [`Span`].
101    pub fn as_frontend_spans(self) -> &'static [hax_frontend_exporter::Span] {
102        &self.data.get().data
103    }
104}
105
106impl Internable for hax_frontend_exporter::DefId {
107    fn interning_table() -> &'static Mutex<InterningTable<Self>> {
108        static TABLE: LazyLock<Mutex<InterningTable<hax_frontend_exporter::DefId>>> =
109            LazyLock::new(|| Mutex::new(InterningTable::default()));
110        &TABLE
111    }
112}
hax_rust_engine/ast/span.rs

hax_rust_engine/ast/
span.rs
