Adds small helpers in llbcastutils and document raw_statement a bit

charon-ml/src/CharonVersion.ml

@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.20"
+let supported_charon_version = "0.1.21"

charon-ml/src/LlbcAstUtils.ml

@@ -1,6 +1,18 @@
 include GAstUtils
 open LlbcAst
 open Utils
+open Collections
+
+let fun_decl_list_from_crate (crate : crate) : fun_decl list =
+  snd (List.split (FunDeclId.Map.bindings crate.fun_decls))
+
+let get_fun_args (fun_decl : fun_decl) : var list =
+  match fun_decl.body with
+  | Some body ->
+      let input_number = body.arg_count in
+      let input_list = snd (List.split_at body.locals 1) in
+      fst (List.split_at input_list input_number)
+  | None -> []
 
 (** Check if a {!type:Charon.LlbcAst.statement} contains loops *)
 let statement_has_loops (st : statement) : bool =

charon/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.20"
+version = "0.1.21"
 authors = ["Son Ho <hosonmarc@gmail.com>"]
 edition = "2021"
 

charon/src/ast/llbc_ast.rs

@@ -27,8 +27,14 @@ pub struct Assert {
     Debug, Clone, EnumIsA, EnumToGetters, EnumAsGetters, Serialize, Deserialize, Drive, DriveMut,
 )]
 pub enum RawStatement {
+    /// Assigns an `Rvalue` to a `Place`. e.g. `let y = x` becomes
+    /// `y := copy x` which looks like
+    /// `"Assign":(("var_id":2,"projection":[]),("Use":("Copy":("var_id":1,
+    /// "projection":[]))))` in llbc
     Assign(Place, Rvalue),
+    /// Only used for borrow-checking
     FakeRead(Place),
+    /// Not used today because we take MIR built.
     SetDiscriminant(Place, VariantId),
     Drop(Place),
     Assert(Assert),
@@ -53,6 +59,10 @@ pub enum RawStatement {
     Nop,
     /// The contained statements must NOT be sequences. To ensure that, use [Sequence::then] to
     /// build sequences.
+    /// Note that on the ml side, sequences will be in the shape of
+    /// `Sequence of statement * statement` where the second `statement` might
+    ///  be a sequence if needed, but not the first one, e.g. `Sequence [a, b,
+    ///  c]` becomes `Sequence (a, Sequence (b, c))`
     Sequence(Vec<Statement>),
     Switch(Switch),
     Loop(Box<Statement>),
@@ -79,7 +89,10 @@ pub struct Statement {
     VariantIndexArity,
 )]
 pub enum Switch {
-    /// Gives the `if` block and the `else` block
+    /// Gives the `if` block and the `else` block. The `Operand` is the "body" of the `if`, e.g. `if (y == 0)` becomes
+    /// `v@3 := copy y^1;
+    ///  v@2 := move v@3 == (0: u32 : u32);
+    ///  if (move v@2) {`
     If(Operand, Box<Statement>, Box<Statement>),
     /// Gives the integer type, a map linking values to switch branches, and the
     /// otherwise block. Note that matches over enumerations are performed by