charon_lib/ast/meta/
spans.rs

1use derive_generic_visitor::{Drive, DriveMut, DriveTwo};
2use serde::{Deserialize, Serialize};
3use serde_state::{DeserializeState, SerializeState};
4use std::{borrow::Cow, cmp::Ordering, ops::Range, path::PathBuf};
5
6generate_index_type!(FileId);
7
8/// A filename.
9#[derive(
10    Debug,
11    PartialEq,
12    Eq,
13    Clone,
14    Hash,
15    PartialOrd,
16    Ord,
17    Serialize,
18    Deserialize,
19    Drive,
20    DriveMut,
21    DriveTwo,
22)]
23pub enum FileName {
24    /// A remapped path (namely paths into stdlib)
25    #[drive(skip)] // drive is not implemented for `PathBuf`
26    Virtual(PathBuf),
27    /// A local path (a file coming from the current crate for instance)
28    #[drive(skip)] // drive is not implemented for `PathBuf`
29    Local(PathBuf),
30    /// A "not real" file name (macro, query, etc.)
31    NotReal(String),
32}
33
34#[derive(
35    Debug,
36    PartialEq,
37    Eq,
38    Clone,
39    Hash,
40    PartialOrd,
41    Ord,
42    Serialize,
43    Deserialize,
44    Drive,
45    DriveMut,
46    DriveTwo,
47)]
48pub struct File {
49    /// The file identifier.
50    #[cfg_attr(feature = "charon_on_charon", charon::opaque)]
51    pub id: FileId,
52    /// The path to the file.
53    #[drive(skip)]
54    pub name: FileName,
55    /// Name of the crate this file comes from.
56    pub crate_name: String,
57    /// The contents of the source file, as seen by rustc at the time of translation.
58    /// Some files don't have contents.
59    pub contents: Option<String>,
60}
61
62#[derive(
63    Debug,
64    Copy,
65    Clone,
66    PartialEq,
67    Eq,
68    PartialOrd,
69    Ord,
70    Hash,
71    Serialize,
72    Deserialize,
73    Drive,
74    DriveMut,
75    DriveTwo,
76)]
77#[drive(skip)]
78pub struct Loc {
79    /// The (1-based) line number.
80    pub line: usize,
81    /// The (0-based) column offset.
82    pub col: usize,
83}
84
85/// A snippet of source code within a file.
86#[derive(
87    Debug, Copy, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut, DriveTwo,
88)]
89pub struct SpanData {
90    #[cfg_attr(feature = "charon_on_charon", charon::rename("file"))]
91    pub file_id: FileId,
92    #[cfg_attr(feature = "charon_on_charon", charon::rename("beg_loc"))]
93    pub beg: Loc,
94    #[cfg_attr(feature = "charon_on_charon", charon::rename("end_loc"))]
95    pub end: Loc,
96}
97
98/// A snippet of source code within a file.
99#[derive(
100    Debug,
101    Copy,
102    Clone,
103    PartialEq,
104    Eq,
105    PartialOrd,
106    Ord,
107    Hash,
108    Serialize,
109    Deserialize,
110    SerializeState,
111    DeserializeState,
112    Drive,
113    DriveMut,
114    DriveTwo,
115)]
116#[serde_state(stateless)]
117pub struct Span {
118    /// The source code span.
119    ///
120    /// If this meta information is for a statement/terminator coming from a macro
121    /// expansion/inlining/etc., this span is (in case of macros) for the macro
122    /// before expansion (i.e., the location the code where the user wrote the call
123    /// to the macro).
124    ///
125    /// Ex:
126    /// ```text
127    /// // Below, we consider the spans for the statements inside `test`
128    ///
129    /// //   the statement we consider, which gets inlined in `test`
130    ///                          VV
131    /// macro_rules! macro { ... st ... } // `generated_from_span` refers to this location
132    ///
133    /// fn test() {
134    ///     macro!(); // <-- `data` refers to this location
135    /// }
136    /// ```
137    pub data: SpanData,
138    /// Where the code actually comes from, in case of macro expansion/inlining/etc.
139    pub generated_from_span: Option<SpanData>,
140}
141
142/// Given a line number within a source file, get the byte of the start of the line. Obviously not
143/// efficient to do many times, but this is used is diagnostic paths only. The line numer is
144/// expected to be 1-based.
145fn line_to_start_byte(source: &str, line_nbr: usize) -> usize {
146    let mut cur_byte = 0;
147    for (i, line) in source.split_inclusive('\n').enumerate() {
148        if line_nbr == i + 1 {
149            break;
150        }
151        cur_byte += line.len();
152    }
153    cur_byte
154}
155
156impl Loc {
157    fn dummy() -> Self {
158        Loc { line: 0, col: 0 }
159    }
160
161    fn min(l0: &Loc, l1: &Loc) -> Loc {
162        match l0.line.cmp(&l1.line) {
163            Ordering::Equal => Loc {
164                line: l0.line,
165                col: std::cmp::min(l0.col, l1.col),
166            },
167            Ordering::Less => *l0,
168            Ordering::Greater => *l1,
169        }
170    }
171
172    fn max(l0: &Loc, l1: &Loc) -> Loc {
173        match l0.line.cmp(&l1.line) {
174            Ordering::Equal => Loc {
175                line: l0.line,
176                col: std::cmp::max(l0.col, l1.col),
177            },
178            Ordering::Greater => *l0,
179            Ordering::Less => *l1,
180        }
181    }
182
183    pub fn to_byte(self, source: &str) -> usize {
184        line_to_start_byte(source, self.line) + self.col
185    }
186}
187
188impl SpanData {
189    pub fn dummy() -> Self {
190        SpanData {
191            file_id: FileId::from_raw(0),
192            beg: Loc::dummy(),
193            end: Loc::dummy(),
194        }
195    }
196
197    /// Value with which we order `SpanDatas`s.
198    fn sort_key(&self) -> impl Ord {
199        (self.file_id, self.beg, self.end)
200    }
201
202    pub fn to_byte_range(self, source: &str) -> Range<usize> {
203        self.beg.to_byte(source)..self.end.to_byte(source)
204    }
205}
206
207/// Manual impls because `SpanData` is not orderable.
208impl PartialOrd for SpanData {
209    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
210        Some(self.cmp(other))
211    }
212}
213impl Ord for SpanData {
214    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
215        self.sort_key().cmp(&other.sort_key())
216    }
217}
218
219impl Span {
220    pub fn dummy() -> Self {
221        Span {
222            data: SpanData::dummy(),
223            generated_from_span: None,
224        }
225    }
226}
227
228/// Combine some span information (useful when we need to compute the
229/// span-information of, say, a sequence).
230pub fn combine_span(m0: &Span, m1: &Span) -> Span {
231    // Merge the spans
232    if m0.data.file_id == m1.data.file_id {
233        let data = SpanData {
234            file_id: m0.data.file_id,
235            beg: Loc::min(&m0.data.beg, &m1.data.beg),
236            end: Loc::max(&m0.data.end, &m1.data.end),
237        };
238
239        // We don't attempt to merge the "generated from" spans: they might
240        // come from different files, and even if they come from the same files
241        // they might come from different macros, etc.
242        Span {
243            data,
244            generated_from_span: None,
245        }
246    } else {
247        // It happens that the spans don't come from the same file. In this
248        // situation, we just return the first span. TODO: improve this.
249        *m0
250    }
251}
252
253/// Combine all the span information in a slice.
254pub fn combine_span_iter<'a, T: Iterator<Item = &'a Span>>(mut ms: T) -> Span {
255    // The iterator should have a next element
256    let mut mc: Span = ms.next().copied().unwrap_or_default();
257    for m in ms {
258        mc = combine_span(&mc, m);
259    }
260
261    mc
262}
263
264impl FileName {
265    pub fn to_string(&self) -> Cow<'_, str> {
266        match self {
267            FileName::Virtual(path_buf) | FileName::Local(path_buf) => path_buf.to_string_lossy(),
268            FileName::NotReal(path) => Cow::Borrowed(path),
269        }
270    }
271}
272
273impl Default for Span {
274    fn default() -> Self {
275        Self::dummy()
276    }
277}
charon_lib/ast/meta/spans.rs

charon_lib/ast/meta/
spans.rs
