Support almost all MIR rvalues

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.31"
+let supported_charon_version = "0.1.32"

charon-ml/src/Expressions.ml

@@ -259,6 +259,7 @@ type cast_kind =
       (** Conversion between types in {Integer, Bool}
           Remark: for now we don't support conversions with Char.
        *)
+  | CastRawPtr of ty * ty
   | CastFnPtr of ty * ty
   | CastUnsize of ty * ty
       (** [Unsize coercion](https://doc.rust-lang.org/std/ops/trait.CoerceUnsized.html). This is
@@ -267,6 +268,7 @@ type cast_kind =
 
           The special case of `&[T; N]` -> `&[T]` coercion is caught by `UnOp::ArrayToSlice`.
        *)
+  | CastTransmute of ty * ty
 
 (** Unary operation *)
 and unop =
@@ -279,6 +281,9 @@ and unop =
   | Cast of cast_kind
       (** Casts are rvalues in MIR, but we treat them as unops. *)
 
+(** Nullary operation *)
+and nullop = SizeOf | AlignOf | OffsetOf of (int * field_id) list | UbChecks
+
 (** A constant expression.
 
     Only the [Literal] and [Var] cases are left in the final LLBC.
@@ -428,11 +433,16 @@ and aggregate_kind =
     TODO: we should prefix the type variants with "R" or "Rv", this would avoid collisions
  *)
 and rvalue =
-  | Use of operand
-  | RvRef of place * borrow_kind
-  | UnaryOp of unop * operand  (** Unary operation (not, neg) *)
+  | Use of operand  (** Returns the operand unchanged. *)
+  | RvRef of place * borrow_kind  (** Takes a reference to the given place. *)
+  | RawPtr of place * ref_kind
+      (** Takes a raw pointer with the given mutability to the given place. This is generated by
+          pointer casts like `&v as *const _` or raw borrow expressions like `&raw const v.`
+       *)
   | BinaryOp of binop * operand * operand
       (** Binary operations (note that we merge "checked" and "unchecked" binops) *)
+  | UnaryOp of unop * operand  (** Unary operation (e.g. not, neg) *)
+  | NullaryOp of nullop * ty  (** Nullary operation (e.g. `size_of`) *)
   | Discriminant of place * type_decl_id
       (** Discriminant (for enumerations).
           Note that discriminant values have type isize. We also store the identifier
@@ -488,6 +498,8 @@ and rvalue =
           rustc introduces a check that the length of the slice is exactly equal
           to 1 and that we preserve.
        *)
+  | ShallowInitBox of operand * ty
+      (** Transmutes a `*mut u8` (obtained from `malloc`) into shallow-initialized `Box<T>`. *)
 [@@deriving
   show,
     visitors

charon-ml/src/GAstOfJson.ml

@@ -807,6 +807,10 @@ and cast_kind_of_json (js : json) : (cast_kind, string) result =
         let* x_0 = literal_type_of_json x_0 in
         let* x_1 = literal_type_of_json x_1 in
         Ok (CastScalar (x_0, x_1))
+    | `Assoc [ ("RawPtr", `List [ x_0; x_1 ]) ] ->
+        let* x_0 = ty_of_json x_0 in
+        let* x_1 = ty_of_json x_1 in
+        Ok (CastRawPtr (x_0, x_1))
     | `Assoc [ ("FnPtr", `List [ x_0; x_1 ]) ] ->
         let* x_0 = ty_of_json x_0 in
         let* x_1 = ty_of_json x_1 in
@@ -815,6 +819,10 @@ and cast_kind_of_json (js : json) : (cast_kind, string) result =
         let* x_0 = ty_of_json x_0 in
         let* x_1 = ty_of_json x_1 in
         Ok (CastUnsize (x_0, x_1))
+    | `Assoc [ ("Transmute", `List [ x_0; x_1 ]) ] ->
+        let* x_0 = ty_of_json x_0 in
+        let* x_1 = ty_of_json x_1 in
+        Ok (CastTransmute (x_0, x_1))
     | _ -> Error "")
 
 and abort_kind_of_json (id_to_file : id_to_file_map) (js : json) :
@@ -836,6 +844,19 @@ and assertion_of_json (js : json) : (assertion, string) result =
         Ok ({ cond; expected } : assertion)
     | _ -> Error "")
 
+and nullop_of_json (js : json) : (nullop, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | `String "SizeOf" -> Ok SizeOf
+    | `String "AlignOf" -> Ok AlignOf
+    | `Assoc [ ("OffsetOf", offset_of) ] ->
+        let* offset_of =
+          list_of_json (pair_of_json int_of_json field_id_of_json) offset_of
+        in
+        Ok (OffsetOf offset_of)
+    | `String "UbChecks" -> Ok UbChecks
+    | _ -> Error "")
+
 and unop_of_json (js : json) : (unop, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
@@ -1018,15 +1039,23 @@ and rvalue_of_json (js : json) : (rvalue, string) result =
         let* x_0 = place_of_json x_0 in
         let* x_1 = borrow_kind_of_json x_1 in
         Ok (RvRef (x_0, x_1))
-    | `Assoc [ ("UnaryOp", `List [ x_0; x_1 ]) ] ->
-        let* x_0 = unop_of_json x_0 in
-        let* x_1 = operand_of_json x_1 in
-        Ok (UnaryOp (x_0, x_1))
+    | `Assoc [ ("RawPtr", `List [ x_0; x_1 ]) ] ->
+        let* x_0 = place_of_json x_0 in
+        let* x_1 = ref_kind_of_json x_1 in
+        Ok (RawPtr (x_0, x_1))
     | `Assoc [ ("BinaryOp", `List [ x_0; x_1; x_2 ]) ] ->
         let* x_0 = binop_of_json x_0 in
         let* x_1 = operand_of_json x_1 in
         let* x_2 = operand_of_json x_2 in
         Ok (BinaryOp (x_0, x_1, x_2))
+    | `Assoc [ ("UnaryOp", `List [ x_0; x_1 ]) ] ->
+        let* x_0 = unop_of_json x_0 in
+        let* x_1 = operand_of_json x_1 in
+        Ok (UnaryOp (x_0, x_1))
+    | `Assoc [ ("NullaryOp", `List [ x_0; x_1 ]) ] ->
+        let* x_0 = nullop_of_json x_0 in
+        let* x_1 = ty_of_json x_1 in
+        Ok (NullaryOp (x_0, x_1))
     | `Assoc [ ("Discriminant", `List [ x_0; x_1 ]) ] ->
         let* x_0 = place_of_json x_0 in
         let* x_1 = type_decl_id_of_json x_1 in
@@ -1043,6 +1072,10 @@ and rvalue_of_json (js : json) : (rvalue, string) result =
         let* x_1 = ty_of_json x_1 in
         let* x_2 = option_of_json const_generic_of_json x_2 in
         Ok (Len (x_0, x_1, x_2))
+    | `Assoc [ ("ShallowInitBox", `List [ x_0; x_1 ]) ] ->
+        let* x_0 = operand_of_json x_0 in
+        let* x_1 = ty_of_json x_1 in
+        Ok (ShallowInitBox (x_0, x_1))
     | _ -> Error "")
 
 and params_info_of_json (js : json) : (params_info, string) result =

charon-ml/src/PrintExpressions.ml

@@ -57,11 +57,18 @@ let cast_kind_to_string (env : ('a, 'b) fmt_env) (cast : cast_kind) : string =
   | CastScalar (src, tgt) ->
       "cast<" ^ literal_type_to_string src ^ "," ^ literal_type_to_string tgt
       ^ ">"
-  | CastFnPtr (src, tgt) ->
+  | CastFnPtr (src, tgt) | CastRawPtr (src, tgt) | CastTransmute (src, tgt) ->
       "cast<" ^ ty_to_string env src ^ "," ^ ty_to_string env tgt ^ ">"
   | CastUnsize (src, tgt) ->
       "unsize<" ^ ty_to_string env src ^ "," ^ ty_to_string env tgt ^ ">"
 
+let nullop_to_string (env : ('a, 'b) fmt_env) (op : nullop) : string =
+  match op with
+  | SizeOf -> "size_of"
+  | AlignOf -> "align_of"
+  | OffsetOf _ -> "offset_of(?)"
+  | UbChecks -> "ub_checks"
+
 let unop_to_string (env : ('a, 'b) fmt_env) (unop : unop) : string =
   match unop with
   | Not -> "¬"
@@ -138,13 +145,20 @@ let operand_to_string (env : ('a, 'b) fmt_env) (op : operand) : string =
 let rvalue_to_string (env : ('a, 'b) fmt_env) (rv : rvalue) : string =
   match rv with
   | Use op -> operand_to_string env op
-  | RvRef (p, bk) -> (
+  | RvRef (p, bk) -> begin
       let p = place_to_string env p in
       match bk with
       | BShared -> "&" ^ p
       | BMut -> "&mut " ^ p
       | BTwoPhaseMut -> "&two-phase " ^ p
-      | BShallow -> "&shallow " ^ p)
+      | BShallow -> "&shallow " ^ p
+    end
+  | RawPtr (p, pk) -> begin
+      let p = place_to_string env p in
+      match pk with RShared -> "&raw const " ^ p | RMut -> "&raw mut " ^ p
+    end
+  | NullaryOp (op, ty) ->
+      nullop_to_string env op ^ "<" ^ ty_to_string env ty ^ ">"
   | UnaryOp (unop, op) ->
       unop_to_string env unop ^ " " ^ operand_to_string env op
   | BinaryOp (binop, op1, op2) ->
@@ -163,6 +177,9 @@ let rvalue_to_string (env : ('a, 'b) fmt_env) (rv : rvalue) : string =
   | Global global_ref ->
       let generics = generic_args_to_string env global_ref.global_generics in
       "global " ^ global_decl_id_to_string env global_ref.global_id ^ generics
+  | ShallowInitBox (op, ty) ->
+      "shallow_init_box<" ^ ty_to_string env ty ^ ">("
+      ^ operand_to_string env op ^ ")"
   | Aggregate (akind, ops) -> (
       let ops = List.map (operand_to_string env) ops in
       match akind with

charon/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.31"
+version = "0.1.32"
 authors = ["Son Ho <hosonmarc@gmail.com>"]
 edition = "2021"
 license = "Apache-2.0"

charon/src/ast/expressions.rs

@@ -149,6 +149,18 @@ pub enum UnOp {
     ArrayToSlice(RefKind, Ty, ConstGeneric),
 }
 
+/// Nullary operation
+#[derive(
+    Debug, PartialEq, Eq, Clone, EnumIsA, VariantName, Serialize, Deserialize, Drive, DriveMut,
+)]
+#[charon::rename("Nullop")]
+pub enum NullOp {
+    SizeOf,
+    AlignOf,
+    OffsetOf(Vec<(usize, FieldId)>),
+    UbChecks,
+}
+
 /// For all the variants: the first type gives the source type, the second one gives
 /// the destination type.
 #[derive(
@@ -159,13 +171,15 @@ pub enum CastKind {
     /// Conversion between types in {Integer, Bool}
     /// Remark: for now we don't support conversions with Char.
     Scalar(LiteralTy, LiteralTy),
+    RawPtr(Ty, Ty),
     FnPtr(Ty, Ty),
     /// [Unsize coercion](https://doc.rust-lang.org/std/ops/trait.CoerceUnsized.html). This is
     /// either `[T; N]` -> `[T]` or `T: Trait` -> `dyn Trait` coercions, behind a pointer
     /// (reference, `Box`, or other type that implements `CoerceUnsized`).
     ///
     /// The special case of `&[T; N]` -> `&[T]` coercion is caught by `UnOp::ArrayToSlice`.
     Unsize(Ty, Ty),
+    Transmute(Ty, Ty),
 }
 
 /// Binary operations.
@@ -451,13 +465,20 @@ pub struct ConstantExpr {
     Debug, Clone, EnumToGetters, EnumAsGetters, EnumIsA, Serialize, Deserialize, Drive, DriveMut,
 )]
 pub enum Rvalue {
+    /// Returns the operand unchanged.
     Use(Operand),
+    /// Takes a reference to the given place.
     #[charon::rename("RvRef")]
     Ref(Place, BorrowKind),
-    /// Unary operation (not, neg)
-    UnaryOp(UnOp, Operand),
+    /// Takes a raw pointer with the given mutability to the given place. This is generated by
+    /// pointer casts like `&v as *const _` or raw borrow expressions like `&raw const v.`
+    RawPtr(Place, RefKind),
     /// Binary operations (note that we merge "checked" and "unchecked" binops)
     BinaryOp(BinOp, Operand, Operand),
+    /// Unary operation (e.g. not, neg)
+    UnaryOp(UnOp, Operand),
+    /// Nullary operation (e.g. `size_of`)
+    NullaryOp(NullOp, Ty),
     /// Discriminant (for enumerations).
     /// Note that discriminant values have type isize. We also store the identifier
     /// of the type from which we read the discriminant.
@@ -511,9 +532,11 @@ pub enum Rvalue {
     Len(Place, Ty, Option<ConstGeneric>),
     /// [Repeat(x, n)] creates an array where [x] is copied [n] times.
     ///
-    /// We desugar this to a function call.
+    /// We translate this to a function call.
     #[charon::opaque]
     Repeat(Operand, Ty, ConstGeneric),
+    /// Transmutes a `*mut u8` (obtained from `malloc`) into shallow-initialized `Box<T>`.
+    ShallowInitBox(Operand, Ty),
 }
 
 /// An aggregated ADT.

charon/src/ast/ullbc_ast_utils.rs

@@ -2,6 +2,7 @@
 use crate::ids::Vector;
 use crate::meta::Span;
 use crate::ullbc_ast::*;
+use derive_visitor::{visitor_enter_fn_mut, DriveMut};
 use take_mut::take;
 
 impl SwitchTargets {
@@ -35,35 +36,6 @@ impl Terminator {
 }
 
 impl BlockData {
-    /// Visit the operands in an rvalue and generate statements.
-    /// Used below in [BlockData::transform_operands].
-    /// TODO: use visitors
-    fn transform_rvalue_operands<F: FnMut(&Span, &mut Vec<Statement>, &mut Operand)>(
-        span: &Span,
-        nst: &mut Vec<Statement>,
-        rval: &mut Rvalue,
-        f: &mut F,
-    ) {
-        match rval {
-            Rvalue::Use(op) | Rvalue::UnaryOp(_, op) => f(span, nst, op),
-            Rvalue::BinaryOp(_, o1, o2) => {
-                f(span, nst, o1);
-                f(span, nst, o2);
-            }
-            Rvalue::Aggregate(_, ops) => {
-                for op in ops {
-                    f(span, nst, op);
-                }
-            }
-            Rvalue::Repeat(op, _, _) => {
-                f(span, nst, op);
-            }
-            Rvalue::Global(..) | Rvalue::Discriminant(..) | Rvalue::Ref(_, _) | Rvalue::Len(..) => {
-                // No operands: nothing to do
-            }
-        }
-    }
-
     /// See [body_transform_operands]
     pub fn transform_operands<F: FnMut(&Span, &mut Vec<Statement>, &mut Operand)>(
         mut self,
@@ -74,44 +46,20 @@ impl BlockData {
 
         // Explore the operands in the statements
         for mut st in self.statements {
-            let span = &st.span;
-            match &mut st.content {
-                RawStatement::Assign(_, rvalue) => {
-                    BlockData::transform_rvalue_operands(span, &mut nst, rvalue, f);
-                }
-                RawStatement::FakeRead(_)
-                | RawStatement::SetDiscriminant(_, _)
-                | RawStatement::StorageDead(_)
-                | RawStatement::Deinit(_)
-                | RawStatement::Error(_) => {
-                    // No operands: nothing to do
-                }
-            }
+            st.content
+                .drive_mut(&mut visitor_enter_fn_mut(|op: &mut Operand| {
+                    f(&st.span, &mut nst, op)
+                }));
             // Add the statement to the vector of statements
             nst.push(st)
         }
 
         // Explore the terminator
-        let span = &self.terminator.span;
-        match &mut self.terminator.content {
-            RawTerminator::Switch { discr, targets: _ } => {
-                f(span, &mut nst, discr);
-            }
-            RawTerminator::Call { call, target: _ } => {
-                for arg in &mut call.args {
-                    f(span, &mut nst, arg);
-                }
-            }
-            RawTerminator::Assert { assert, .. } => {
-                f(span, &mut nst, &mut assert.cond);
-            }
-            RawTerminator::Abort(..)
-            | RawTerminator::Return
-            | RawTerminator::Goto { .. }
-            | RawTerminator::Drop { .. } => {
-                // Nothing to do
-            }
-        };
+        self.terminator
+            .content
+            .drive_mut(&mut visitor_enter_fn_mut(|op: &mut Operand| {
+                f(&self.terminator.span, &mut nst, op)
+            }));
 
         // Update the vector of statements
         self.statements = nst;