charon_lib/ast/gast.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 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341
//! Definitions common to [crate::ullbc_ast] and [crate::llbc_ast]
pub use super::gast_utils::*;
use crate::expressions::*;
use crate::generate_index_type;
use crate::ids::Vector;
use crate::llbc_ast;
use crate::meta::{ItemMeta, Span};
use crate::names::Name;
use crate::types::*;
use crate::ullbc_ast;
use crate::values::*;
use derive_visitor::{Drive, DriveMut, Event, Visitor, VisitorMut};
use macros::EnumIsA;
use macros::EnumToGetters;
use serde::{Deserialize, Serialize};
use std::collections::HashMap;
generate_index_type!(FunDeclId, "Fun");
generate_index_type!(BodyId, "Body");
/// A variable
#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
pub struct Var {
/// Unique index identifying the variable
pub index: VarId,
/// Variable name - may be `None` if the variable was introduced by Rust
/// through desugaring.
pub name: Option<String>,
/// The variable type
#[charon::rename("var_ty")]
pub ty: Ty,
}
/// Marker to indicate that a declaration is opaque (i.e. we don't inspect its body).
#[derive(Debug, Copy, Clone, Serialize, Deserialize, Drive, DriveMut)]
pub struct Opaque;
/// An expression body.
/// TODO: arg_count should be stored in GFunDecl below. But then,
/// the print is obfuscated and Aeneas may need some refactoring.
#[derive(Debug, Clone, Serialize, Deserialize)]
#[charon::rename("GexprBody")]
pub struct GExprBody<T> {
pub span: Span,
/// The number of local variables used for the input arguments.
pub arg_count: usize,
/// The local variables.
/// We always have, in the following order:
/// - the local used for the return value (index 0)
/// - the input arguments
/// - the remaining locals, used for the intermediate computations
pub locals: Vector<VarId, Var>,
/// For each line inside the body, we record any whole-line `//` comments found before it. They
/// are added to statements in the late `recover_body_comments` pass.
#[charon::opaque]
pub comments: Vec<(usize, Vec<String>)>,
pub body: T,
}
// The derive macro doesn't handle generics well.
impl<T: Drive> Drive for GExprBody<T> {
fn drive<V: Visitor>(&self, visitor: &mut V) {
visitor.visit(self, Event::Enter);
self.span.drive(visitor);
self.arg_count.drive(visitor);
self.locals.drive(visitor);
self.body.drive(visitor);
visitor.visit(self, Event::Exit);
}
}
impl<T: DriveMut> DriveMut for GExprBody<T> {
fn drive_mut<V: VisitorMut>(&mut self, visitor: &mut V) {
visitor.visit(self, Event::Enter);
self.span.drive_mut(visitor);
self.arg_count.drive_mut(visitor);
self.locals.drive_mut(visitor);
self.body.drive_mut(visitor);
visitor.visit(self, Event::Exit);
}
}
/// The body of a function or a constant.
#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut, EnumIsA, EnumToGetters)]
pub enum Body {
/// Body represented as a CFG. This is what ullbc is made of, and what we get after translating MIR.
Unstructured(ullbc_ast::ExprBody),
/// Body represented with structured control flow. This is what llbc is made of. We restructure
/// the control flow in `ullbc_to_llbc`.
Structured(llbc_ast::ExprBody),
}
/// Item kind: whether this function/const is part of a trait declaration, trait implementation, or
/// neither.
///
/// Example:
/// ```text
/// trait Foo {
/// fn bar(x : u32) -> u32; // trait item decl without default
///
/// fn baz(x : bool) -> bool { x } // trait item decl with default
/// }
///
/// impl Foo for ... {
/// fn bar(x : u32) -> u32 { x } // trait item implementation
/// }
///
/// fn test(...) { ... } // regular
///
/// impl Type {
/// fn test(...) { ... } // regular
/// }
/// ```
#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut, PartialEq, Eq)]
#[charon::variants_suffix("Item")]
pub enum ItemKind {
/// A function/const at the top level or in an inherent impl block.
Regular,
/// Function/const that is part of a trait declaration. It has a body if and only if the trait
/// provided a default implementation.
TraitDecl {
/// The trait declaration this item belongs to.
trait_id: TraitDeclId,
/// The name of the item.
item_name: TraitItemName,
/// Whether the trait declaration provides a default implementation.
has_default: bool,
},
/// Function/const that is part of a trait implementation.
TraitImpl {
/// The trait implementation the method belongs to
impl_id: TraitImplId,
/// The trait declaration this item belongs to.
trait_id: TraitDeclId,
/// The name of the item
item_name: TraitItemName,
/// True if the trait decl had a default implementation for this function/const and this
/// item is a copy of the default item.
reuses_default: bool,
},
}
/// A function definition
#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
pub struct FunDecl {
#[drive(skip)]
pub def_id: FunDeclId,
/// The meta data associated with the declaration.
pub item_meta: ItemMeta,
/// The signature contains the inputs/output types *with* non-erased regions.
/// It also contains the list of region and type parameters.
pub signature: FunSig,
/// The function kind: "regular" function, trait method declaration, etc.
pub kind: ItemKind,
/// The function body, unless the function is opaque.
/// Opaque functions are: external functions, or local functions tagged
/// as opaque.
pub body: Result<BodyId, Opaque>,
}
/// A global variable definition
#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
pub struct GlobalDecl {
#[drive(skip)]
pub def_id: GlobalDeclId,
/// The meta data associated with the declaration.
pub item_meta: ItemMeta,
pub generics: GenericParams,
pub ty: Ty,
/// The global kind: "regular" function, trait const declaration, etc.
pub kind: ItemKind,
pub body: Result<BodyId, Opaque>,
}
/// Reference to a global declaration.
#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash, Drive, DriveMut)]
pub struct GlobalDeclRef {
#[charon::rename("global_id")]
pub id: GlobalDeclId,
#[charon::rename("global_generics")]
pub generics: GenericArgs,
}
#[derive(
Debug, Clone, Serialize, Deserialize, Drive, DriveMut, PartialEq, Eq, Hash, PartialOrd, Ord,
)]
pub struct TraitItemName(pub String);
/// A trait **declaration**.
///
/// For instance:
/// ```text
/// trait Foo {
/// type Bar;
///
/// fn baz(...); // required method (see below)
///
/// fn test() -> bool { true } // provided method (see below)
/// }
/// ```
///
/// In case of a trait declaration, we don't include the provided methods (the methods
/// with a default implementation): they will be translated on a per-need basis. This is
/// important for two reasons:
/// - this makes the trait definitions a lot smaller (the Iterator trait
/// has *one* declared function and more than 70 provided functions)
/// - this is important for the external traits, whose provided methods
/// often use features we don't support yet
///
/// Remark:
/// In Aeneas, we still translate the provided methods on an individual basis,
/// and in such a way thay they take as input a trait instance. This means that
/// we can use default methods *but*:
/// - implementations of required methods shoudln't call default methods
/// - trait implementations shouldn't redefine required methods
/// The use case we have in mind is [std::iter::Iterator]: it declares one required
/// method (`next`) that should be implemented for every iterator, and defines many
/// helpers like `all`, `map`, etc. that shouldn't be re-implemented.
/// Of course, this forbids other useful use cases such as visitors implemented
/// by means of traits.
#[allow(clippy::type_complexity)]
#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
pub struct TraitDecl {
#[drive(skip)]
pub def_id: TraitDeclId,
pub item_meta: ItemMeta,
pub generics: GenericParams,
/// The "parent" clauses: the supertraits.
///
/// Supertraits are actually regular where clauses, but we decided to have
/// a custom treatment.
/// ```text
/// trait Foo : Bar {
/// ^^^
/// supertrait, that we treat as a parent predicate
/// }
/// ```
/// TODO: actually, as of today, we consider that all trait clauses of
/// trait declarations are parent clauses.
pub parent_clauses: Vector<TraitClauseId, TraitClause>,
/// The associated constants declared in the trait, along with their type.
pub consts: Vec<(TraitItemName, Ty)>,
/// Records associated constants that have a default value.
#[charon::opaque]
pub const_defaults: HashMap<TraitItemName, GlobalDeclRef>,
/// The associated types declared in the trait.
pub types: Vec<TraitItemName>,
/// Records associated types that have a default value.
#[charon::opaque]
pub type_defaults: HashMap<TraitItemName, Ty>,
/// List of trait clauses that apply to each associated type. This is used during translation,
/// but the `lift_associated_item_clauses` pass moves them to be parent clauses later. Hence
/// this is empty after that pass.
/// TODO: Do this as we translate to avoid the need to store this vector.
#[charon::opaque]
pub type_clauses: Vec<(TraitItemName, Vector<TraitClauseId, TraitClause>)>,
/// The *required* methods.
///
/// The required methods are the methods declared by the trait but with no default
/// implementation. The corresponding `FunDecl`s don't have a body.
pub required_methods: Vec<(TraitItemName, FunDeclId)>,
/// The *provided* methods.
///
/// The provided methods are the methods with a default implementation. The corresponding
/// `FunDecl`s may have a body, according to the usual rules for extracting function bodies.
pub provided_methods: Vec<(TraitItemName, FunDeclId)>,
}
/// A trait **implementation**.
///
/// For instance:
/// ```text
/// impl Foo for List {
/// type Bar = ...
///
/// fn baz(...) { ... }
/// }
/// ```
#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
pub struct TraitImpl {
#[drive(skip)]
pub def_id: TraitImplId,
pub item_meta: ItemMeta,
/// The information about the implemented trait.
/// Note that this contains the instantiation of the "parent"
/// clauses.
pub impl_trait: TraitDeclRef,
pub generics: GenericParams,
/// The trait references for the parent clauses (see [TraitDecl]).
pub parent_trait_refs: Vector<TraitClauseId, TraitRef>,
/// The associated constants declared in the trait.
pub consts: Vec<(TraitItemName, GlobalDeclRef)>,
/// The associated types declared in the trait.
pub types: Vec<(TraitItemName, Ty)>,
/// The `Vec` corresponds to the same `Vector` in `TraitDecl`. In the same way, this is
/// empty after the `lift_associated_item_clauses` pass.
#[charon::opaque]
pub type_clauses: Vec<(TraitItemName, Vector<TraitClauseId, TraitRef>)>,
/// The implemented required methods
pub required_methods: Vec<(TraitItemName, FunDeclId)>,
/// The re-implemented provided methods
pub provided_methods: Vec<(TraitItemName, FunDeclId)>,
}
/// A function operand is used in function calls.
/// It either designates a top-level function, or a place in case
/// we are using function pointers stored in local variables.
#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
#[charon::variants_prefix("FnOp")]
pub enum FnOperand {
/// Regular case: call to a top-level function, trait method, etc.
Regular(FnPtr),
/// Use of a function pointer stored in a local variable
Move(Place),
}
#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
pub struct Call {
pub func: FnOperand,
pub args: Vec<Operand>,
pub dest: Place,
}
#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
pub enum AbortKind {
/// A built-in panicking function.
Panic(Name),
/// A MIR `Unreachable` terminator corresponds to undefined behavior in the rust abstract
/// machine.
UndefinedBehavior,
}
/// Asserts are special constructs introduced by Rust to perform dynamic
/// checks, to detect out-of-bounds accesses or divisions by zero for
/// instance. We eliminate the assertions in [crate::remove_dynamic_checks],
/// then introduce other dynamic checks in [crate::reconstruct_asserts].
#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
#[charon::rename("Assertion")]
pub struct Assert {
pub cond: Operand,
pub expected: bool,
}