charon_lib/ast/ullbc_ast.rs
1//! "Unstructured LLBC" ast (ULLBC). This is LLBC before the control-flow
2//! reconstruction. In effect, this is a cleaned up version of MIR.
3pub use crate::ast::*;
4use derive_generic_visitor::{Drive, DriveMut};
5use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName};
6use serde::{Deserialize, Serialize};
7
8// Block identifier. Similar to rust's `BasicBlock`.
9generate_index_type!(BlockId, "Block");
10
11// The entry block of a function is always the block with id 0
12pub static START_BLOCK_ID: BlockId = BlockId::ZERO;
13
14#[charon::rename("Blocks")]
15pub type BodyContents = Vector<BlockId, BlockData>;
16pub type ExprBody = GExprBody<BodyContents>;
17
18/// A raw statement: a statement without meta data.
19#[derive(
20 Debug, Clone, EnumIsA, EnumAsGetters, VariantName, Serialize, Deserialize, Drive, DriveMut,
21)]
22pub enum RawStatement {
23 Assign(Place, Rvalue),
24 /// A call. For now, we don't support dynamic calls (i.e. to a function pointer in memory).
25 SetDiscriminant(Place, VariantId),
26 /// Equivalent to std::intrinsics::copy_nonoverlapping; this is not modelled as a function
27 /// call as it cannot diverge
28 CopyNonOverlapping(Box<CopyNonOverlapping>),
29 /// Indicates that this local should be allocated; if it is already allocated, this frees
30 /// the local and re-allocates it. The return value and arguments do not receive a
31 /// `StorageLive`. We ensure in the micro-pass `insert_storage_lives` that all other locals
32 /// have a `StorageLive` associated with them.
33 StorageLive(LocalId),
34 /// Indicates that this local should be deallocated; if it is already deallocated, this is
35 /// a no-op. A local may not have a `StorageDead` in the function's body, in which case it
36 /// is implicitly deallocated at the end of the function.
37 StorageDead(LocalId),
38 Deinit(Place),
39 Drop(Place),
40 /// A built-in assert, which corresponds to runtime checks that we remove, namely: bounds
41 /// checks, over/underflow checks, div/rem by zero checks, pointer alignement check.
42 Assert(Assert),
43 /// Does nothing. Useful for passes.
44 Nop,
45 #[charon::opaque]
46 #[drive(skip)]
47 Error(String),
48}
49
50#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
51pub struct Statement {
52 pub span: Span,
53 pub content: RawStatement,
54 /// Comments that precede this statement.
55 // This is filled in a late pass after all the control-flow manipulation.
56 #[drive(skip)]
57 pub comments_before: Vec<String>,
58}
59
60#[derive(
61 Debug,
62 Clone,
63 EnumIsA,
64 EnumAsGetters,
65 VariantName,
66 VariantIndexArity,
67 Serialize,
68 Deserialize,
69 Drive,
70 DriveMut,
71)]
72#[charon::rename("Switch")]
73pub enum SwitchTargets {
74 /// Gives the `if` block and the `else` block
75 If(BlockId, BlockId),
76 /// Gives the integer type, a map linking values to switch branches, and the
77 /// otherwise block. Note that matches over enumerations are performed by
78 /// switching over the discriminant, which is an integer.
79 SwitchInt(IntegerTy, Vec<(ScalarValue, BlockId)>, BlockId),
80}
81
82/// A raw terminator: a terminator without meta data.
83#[derive(Debug, Clone, EnumIsA, EnumAsGetters, Serialize, Deserialize, Drive, DriveMut)]
84pub enum RawTerminator {
85 Goto {
86 target: BlockId,
87 },
88 Switch {
89 discr: Operand,
90 targets: SwitchTargets,
91 },
92 Call {
93 call: Call,
94 target: BlockId,
95 on_unwind: BlockId,
96 },
97 /// Handles panics and impossible cases.
98 Abort(AbortKind),
99 Return,
100 UnwindResume,
101}
102
103#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
104pub struct Terminator {
105 pub span: Span,
106 pub content: RawTerminator,
107 /// Comments that precede this terminator.
108 // This is filled in a late pass after all the control-flow manipulation.
109 #[drive(skip)]
110 pub comments_before: Vec<String>,
111}
112
113#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
114#[charon::rename("Block")]
115pub struct BlockData {
116 pub statements: Vec<Statement>,
117 pub terminator: Terminator,
118}