charon_lib/ast/meta.rs
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286
//! Meta-information about programs (spans, etc.).
pub use super::meta_utils::*;
use crate::names::Name;
use derive_visitor::{Drive, DriveMut};
use macros::{EnumAsGetters, EnumIsA, EnumToGetters};
use serde::{Deserialize, Serialize};
use std::path::PathBuf;
generate_index_type!(FileId);
#[derive(
Debug,
Copy,
Clone,
PartialEq,
Eq,
PartialOrd,
Ord,
Hash,
Serialize,
Deserialize,
Drive,
DriveMut,
)]
pub struct Loc {
/// The (1-based) line number.
pub line: usize,
/// The (0-based) column offset.
pub col: usize,
}
/// For use when deserializing.
#[cfg(feature = "rustc")]
fn dummy_span_data() -> rustc_span::SpanData {
rustc_span::DUMMY_SP.data()
}
/// Span information
#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
pub struct RawSpan {
pub file_id: FileId,
pub beg: Loc,
pub end: Loc,
/// We keep the rust span so as to be able to leverage Rustc to print
/// error messages (useful in the micro-passes for instance).
/// We use `SpanData` instead of `Span` because `Span` is not `Send` when rustc runs
/// single-threaded (default on older versions). We need this to be `Send` because we pass this
/// data out of the rustc callbacks in charon-driver.
#[cfg(feature = "rustc")]
#[serde(skip)]
#[drive(skip)]
#[serde(default = "dummy_span_data")]
#[charon::opaque]
pub rust_span_data: rustc_span::SpanData,
}
#[cfg(feature = "rustc")]
impl From<RawSpan> for rustc_error_messages::MultiSpan {
fn from(span: RawSpan) -> Self {
span.rust_span_data.span().into()
}
}
/// Meta information about a piece of code (block, statement, etc.)
#[derive(
Debug,
Copy,
Clone,
PartialEq,
Eq,
PartialOrd,
Ord,
Hash,
Serialize,
Deserialize,
Drive,
DriveMut,
)]
pub struct Span {
/// The source code span.
///
/// If this meta information is for a statement/terminator coming from a macro
/// expansion/inlining/etc., this span is (in case of macros) for the macro
/// before expansion (i.e., the location the code where the user wrote the call
/// to the macro).
///
/// Ex:
/// ```text
/// // Below, we consider the spans for the statements inside `test`
///
/// // the statement we consider, which gets inlined in `test`
/// VV
/// macro_rules! macro { ... st ... } // `generated_from_span` refers to this location
///
/// fn test() {
/// macro!(); // <-- `span` refers to this location
/// }
/// ```
pub span: RawSpan,
/// Where the code actually comes from, in case of macro expansion/inlining/etc.
pub generated_from_span: Option<RawSpan>,
}
#[cfg(feature = "rustc")]
impl From<Span> for rustc_span::Span {
fn from(span: Span) -> Self {
span.span.rust_span_data.span()
}
}
#[cfg(feature = "rustc")]
impl From<Span> for rustc_error_messages::MultiSpan {
fn from(span: Span) -> Self {
span.span.into()
}
}
impl Span {
#[cfg(feature = "rustc")]
pub fn rust_span(self) -> rustc_span::Span {
self.span.rust_span_data.span()
}
}
/// `#[inline]` built-in attribute.
#[derive(Debug, Copy, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
pub enum InlineAttr {
/// `#[inline]`
Hint,
/// `#[inline(never)]`
Never,
/// `#[inline(always)]`
Always,
}
/// Attributes (`#[...]`).
#[derive(
Debug,
Clone,
PartialEq,
Eq,
EnumIsA,
EnumAsGetters,
EnumToGetters,
Serialize,
Deserialize,
Drive,
DriveMut,
)]
#[charon::variants_prefix("Attr")]
pub enum Attribute {
/// Do not translate the body of this item.
/// Written `#[charon::opaque]`
Opaque,
/// Provide a new name that consumers of the llbc can use.
/// Written `#[charon::rename("new_name")]`
Rename(String),
/// For enums only: rename the variants by pre-pending their names with the given prefix.
/// Written `#[charon::variants_prefix("prefix_")]`.
VariantsPrefix(String),
/// Same as `VariantsPrefix`, but appends to the name instead of pre-pending.
VariantsSuffix(String),
/// A doc-comment such as `/// ...`.
DocComment(String),
/// A non-charon-specific attribute.
Unknown(RawAttribute),
}
/// A general attribute.
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
pub struct RawAttribute {
pub path: String,
/// The arguments passed to the attribute, if any. We don't distinguish different delimiters or
/// the `path = lit` case.
pub args: Option<String>,
}
/// Information about the attributes and visibility of an item, field or variant..
#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
pub struct AttrInfo {
/// Attributes (`#[...]`).
pub attributes: Vec<Attribute>,
/// Inline hints (on functions only).
pub inline: Option<InlineAttr>,
/// The name computed from `charon::rename` and `charon::variants_prefix` attributes, if any.
/// This provides a custom name that can be used by consumers of llbc. E.g. Aeneas uses this to
/// rename definitions in the extracted code.
pub rename: Option<String>,
/// Whether this item is declared public. Impl blocks and closures don't have visibility
/// modifiers; we arbitrarily set this to `false` for them.
///
/// Note that this is different from being part of the crate's public API: to be part of the
/// public API, an item has to also be reachable from public items in the crate root. For
/// example:
/// ```rust,ignore
/// mod foo {
/// pub struct X;
/// }
/// mod bar {
/// pub fn something(_x: super::foo::X) {}
/// }
/// pub use bar::something; // exposes `X`
/// ```
/// Without the `pub use ...`, neither `X` nor `something` would be part of the crate's public
/// API (this is called "pub-in-priv" items). With or without the `pub use`, we set `public =
/// true`; computing item reachability is harder.
pub public: bool,
}
#[derive(
Debug,
Copy,
Clone,
PartialEq,
Eq,
PartialOrd,
Ord,
Serialize,
Deserialize,
Drive,
DriveMut,
EnumIsA,
)]
pub enum ItemOpacity {
/// Translate the item fully.
Transparent,
/// Translate the item depending on the normal rust visibility of its contents: for types, we
/// translate fully if it is a struct with public fields or an enum; for functions and globals
/// this is equivalent to `Opaque`; for trait decls and impls this is equivalent to
/// `Transparent`.
Foreign,
/// Translate the item name and signature, but not its contents. For function and globals, this
/// means we don't translate the body (the code); for ADTs, this means we don't translate the
/// fields/variants. For traits and trait impls, this doesn't change anything. For modules,
/// this means we don't explore its contents (we still translate any of its items mentioned
/// from somewhere else).
///
/// This can happen either if the item was annotated with `#[charon::opaque]` or if it was
/// declared opaque via a command-line argument.
Opaque,
/// Translate nothing of this item. The corresponding map will not have an entry for the
/// `AnyTransId`. Useful when even the signature of the item causes errors.
Invisible,
}
/// Meta information about an item (function, trait decl, trait impl, type decl, global).
#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
pub struct ItemMeta {
pub name: Name,
pub span: Span,
/// The source code that corresponds to this item.
pub source_text: Option<String>,
/// Attributes and visibility.
pub attr_info: AttrInfo,
/// `true` if the type decl is a local type decl, `false` if it comes from an external crate.
pub is_local: bool,
/// Whether this item is considered opaque. For function and globals, this means we don't
/// translate the body (the code); for ADTs, this means we don't translate the fields/variants.
/// For traits and trait impls, this doesn't change anything. For modules, this means we don't
/// explore its contents (we still translate any of its items mentioned from somewhere else).
///
/// This can happen either if the item was annotated with `#[charon::opaque]` or if it was
/// declared opaque via a command-line argument.
#[charon::opaque]
pub opacity: ItemOpacity,
}
#[derive(Debug, PartialEq, Eq, Clone, Copy, Serialize, Deserialize, Drive, DriveMut)]
pub struct FileInfo {}
/// A filename.
#[derive(
Debug, PartialEq, Eq, Clone, Hash, PartialOrd, Ord, Serialize, Deserialize, Drive, DriveMut,
)]
pub enum FileName {
/// A remapped path (namely paths into stdlib)
#[drive(skip)] // drive is not implemented for `PathBuf`
Virtual(PathBuf),
/// A local path (a file coming from the current crate for instance)
#[drive(skip)] // drive is not implemented for `PathBuf`
Local(PathBuf),
/// A "not real" file name (macro, query, etc.)
#[charon::opaque]
NotReal(String),
}