hax_rust_engine/ast/
span.rs

1//! Source positions.
2
3use hax_rust_engine_macros::*;
4
5/// Creates a fresh identifier for a span.
6fn fresh_id() -> usize {
7    use std::sync::atomic::{AtomicUsize, Ordering};
8    static CURRENT_ID: AtomicUsize = AtomicUsize::new(0);
9    CURRENT_ID.fetch_add(1, Ordering::Relaxed)
10}
11
12/// Identifier used to track the origin Rust item of a span
13#[derive_group_for_ast]
14pub struct OwnerId(usize);
15
16/// Position of a Rust source
17#[derive_group_for_ast]
18pub struct Span {
19    /// A vector of spans as defined by the frontend.
20    /// This is useful for supporting in a trivial way union of spans.
21    pub data: Vec<hax_frontend_exporter::Span>,
22    /// A unique identifier. Since we store spans almost for every node of the
23    /// AST, having a unique identifier for spans gives us a fine-grained way of
24    /// refering to sub-nodes in debugging context. This id is indeed mostly
25    /// used by the web debugger.
26    id: usize,
27    /// A reference to the item in which this span lives. This information is
28    /// used for debugging and profiling purposes, e.g. for `cargo hax into
29    /// --stats backend`.
30    owner_hint: Option<OwnerId>,
31}
32
33impl Span {
34    /// Creates a dummy span.
35    pub fn dummy() -> Self {
36        let lo: hax_frontend_exporter::Loc = hax_frontend_exporter::Loc { line: 0, col: 0 };
37        let hi = lo.clone();
38        Span {
39            data: vec![hax_frontend_exporter::Span {
40                lo,
41                hi,
42                filename: hax_frontend_exporter::FileName::Custom("dumny".into()),
43                rust_span_data: None,
44            }],
45            id: 0,
46            owner_hint: None,
47        }
48    }
49}
50
51impl From<hax_frontend_exporter::Span> for Span {
52    fn from(span: hax_frontend_exporter::Span) -> Self {
53        Self {
54            data: vec![span],
55            id: fresh_id(),
56            owner_hint: None, // TODO: this will be defined properly while addressing issue #1524
57        }
58    }
59}
60
61impl From<&hax_frontend_exporter::Span> for Span {
62    fn from(span: &hax_frontend_exporter::Span) -> Self {
63        span.clone().into()
64    }
65}
hax_rust_engine/ast/span.rs

hax_rust_engine/ast/
span.rs
