mirage/mir/
charon_llbc.rs

1//! Charon LLBC JSON representation
2//!
3//! Based on AeneasVerif/charon's exported JSON format for Low-Level Borrow Calculus (LLBC).
4
5use serde::{Deserialize, Serialize};
6
7/// Top-level structure for a Charon exported crate
8#[derive(Debug, Clone, Serialize, Deserialize)]
9pub struct Crate {
10    pub crate_name: String,
11    pub files: Vec<File>,
12    pub fun_decls: Vec<FunDecl>,
13}
14
15#[derive(Debug, Clone, Serialize, Deserialize)]
16pub struct File {
17    pub path: String,
18    pub contents: Option<String>,
19}
20
21#[derive(Debug, Clone, Serialize, Deserialize)]
22pub struct FunDecl {
23    pub def_id: u32,
24    pub name: Vec<String>,
25    pub meta: Meta,
26    pub signature: FunSignature,
27    pub body: Option<Body>,
28}
29
30#[derive(Debug, Clone, Serialize, Deserialize)]
31pub struct Meta {
32    pub span: Span,
33}
34
35#[derive(Debug, Clone, Serialize, Deserialize)]
36pub struct Span {
37    pub file_id: u32,
38    pub beg: Loc,
39    pub end: Loc,
40}
41
42#[derive(Debug, Clone, Serialize, Deserialize)]
43pub struct Loc {
44    pub line: u32,
45    pub col: u32,
46}
47
48#[derive(Debug, Clone, Serialize, Deserialize)]
49pub struct FunSignature {
50    pub inputs: Vec<Ty>,
51    pub output: Ty,
52}
53
54#[derive(Debug, Clone, Serialize, Deserialize)]
55#[serde(rename_all = "PascalCase")]
56pub enum Ty {
57    Adt { id: String, generics: Generics },
58    Bool,
59    Char,
60    Integer(IntegerTy),
61    Str,
62    Array(Box<Ty>, usize),
63    Slice(Box<Ty>),
64    Ref(Box<Ty>, RefKind),
65    Never,
66}
67
68#[derive(Debug, Clone, Serialize, Deserialize)]
69pub enum IntegerTy {
70    Isize,
71    I8,
72    I16,
73    I32,
74    I64,
75    I128,
76    Usize,
77    U8,
78    U16,
79    U32,
80    U64,
81    U128,
82}
83
84#[derive(Debug, Clone, Serialize, Deserialize)]
85pub enum RefKind {
86    Mut,
87    Shared,
88}
89
90#[derive(Debug, Clone, Serialize, Deserialize)]
91pub struct Generics {
92    pub types: Vec<String>,
93}
94
95#[derive(Debug, Clone, Serialize, Deserialize)]
96pub struct Body {
97    pub arg_count: usize,
98    pub locals: Vec<Local>,
99    #[serde(rename = "unstructured_body")]
100    pub unstructured: Option<UllbcBody>,
101}
102
103#[derive(Debug, Clone, Serialize, Deserialize)]
104pub struct Local {
105    pub name: Option<String>,
106    pub ty: Ty,
107}
108
109#[derive(Debug, Clone, Serialize, Deserialize)]
110pub struct UllbcBody {
111    pub blocks: Vec<BlockData>,
112}
113
114#[derive(Debug, Clone, Serialize, Deserialize)]
115pub struct BlockData {
116    pub id: u32,
117    pub statements: Vec<Statement>,
118    pub terminator: Terminator,
119}
120
121#[derive(Debug, Clone, Serialize, Deserialize)]
122#[serde(rename_all = "PascalCase")]
123pub enum Statement {
124    Assign(Place, Rvalue),
125    FakeRead(Place),
126}
127
128#[derive(Debug, Clone, Serialize, Deserialize)]
129#[serde(rename_all = "PascalCase")]
130pub enum Terminator {
131    Goto(u32),
132    #[serde(rename_all = "camelCase")]
133    SwitchInt {
134        discr: Operand,
135        targets: Vec<SwitchTarget>,
136        otherwise: u32,
137    },
138    Return,
139    Panic,
140    #[serde(rename_all = "camelCase")]
141    Call {
142        func: FnPtr,
143        args: Vec<Operand>,
144        dest: Place,
145        yield_target: Option<u32>,
146        target: Option<u32>,
147    },
148    #[serde(rename_all = "camelCase")]
149    Assert {
150        cond: Operand,
151        expected: bool,
152        target: u32,
153    },
154    #[serde(rename_all = "camelCase")]
155    Drop {
156        place: Place,
157        target: u32,
158    },
159}
160
161#[derive(Debug, Clone, Serialize, Deserialize)]
162#[serde(rename_all = "PascalCase")]
163pub enum FnPtr {
164    Regular { id: u32, generics: Generics },
165    // Add other variants if needed
166}
167
168#[derive(Debug, Clone, Serialize, Deserialize)]
169pub struct SwitchTarget {
170    pub value: String,
171    pub target: u32,
172}
173
174#[derive(Debug, Clone, Serialize, Deserialize)]
175#[serde(rename_all = "PascalCase")]
176pub enum Place {
177    Local(u32),
178}
179
180#[derive(Debug, Clone, Serialize, Deserialize)]
181#[serde(rename_all = "PascalCase")]
182pub enum Rvalue {
183    BinaryOp(BinOp, Operand, Operand),
184    UnaryOp(UnOp, Operand),
185    Use(Operand),
186    Constant(String),
187}
188
189#[derive(Debug, Clone, Serialize, Deserialize)]
190pub enum UnOp {
191    Not,
192    Neg,
193}
194
195#[derive(Debug, Clone, Serialize, Deserialize)]
196pub enum BinOp {
197    Add,
198    Sub,
199    Mul,
200    Div,
201    Rem,
202    BitAnd,
203    BitOr,
204    BitXor,
205    Shl,
206    Shr,
207    Eq,
208    Ne,
209    Lt,
210    Le,
211    Gt,
212    Ge,
213}
214
215#[derive(Debug, Clone, Serialize, Deserialize)]
216#[serde(rename_all = "PascalCase")]
217pub enum Operand {
218    Copy(Place),
219    Move(Place),
220    Constant(String),
221}
mirage/mir/charon_llbc.rs

mirage/mir/
charon_llbc.rs
