Translate additional unsafe MIR operations

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.36"
+let supported_charon_version = "0.1.37"

charon-ml/src/Expressions.ml

@@ -110,7 +110,7 @@ type field_proj_kind =
     language, we thus merge downcasts and field projections.
  *)
 and projection_elem =
-  | Deref  (** Dereference a shared/mutable reference. *)
+  | Deref  (** Dereference a shared/mutable reference or a raw pointer. *)
   | DerefBox
       (** Dereference a boxed value.
           Note that this doesn't exist in MIR where `Deref` is used both for the
@@ -412,7 +412,12 @@ type operand =
     the field 0, etc.).
  *)
 and aggregate_kind =
-  | AggregatedAdt of type_id * variant_id option * generic_args
+  | AggregatedAdt of
+      type_id * variant_id option * field_id option * generic_args
+      (** A struct, enum or union aggregate. The `VariantId`, if present, indicates this is an enum
+          and the aggregate uses that variant. The `FieldId`, if present, indicates this is a union
+          and the aggregate writes into that field. Otherwise this is a struct.
+       *)
   | AggregatedArray of ty * const_generic
       (** We don't put this with the ADT cas because this is the only built-in type
           with aggregates, and it is a primitive type. In particular, it makes
@@ -467,8 +472,13 @@ and rvalue =
           together with its state.
        *)
   | Global of global_decl_ref
-      (** Not present in MIR: we introduce it when replacing constant variables
-          in operands in [extract_global_assignments.rs].
+      (** Copy the value of the referenced global.
+          Not present in MIR; introduced in [simplify_constants.rs].
+       *)
+  | GlobalRef of global_decl_ref * ref_kind
+      (** Reference the value of the global. This has type `&T` or `*mut T` depending on desired
+          mutability.
+          Not present in MIR; introduced in [simplify_constants.rs].
        *)
   | Len of place * ty * const_generic option
       (** Length of a memory location. The run-time length of e.g. a vector or a slice is

charon-ml/src/GAstOfJson.ml

@@ -1042,11 +1042,12 @@ and operand_of_json (js : json) : (operand, string) result =
 and aggregate_kind_of_json (js : json) : (aggregate_kind, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
-    | `Assoc [ ("Adt", `List [ x_0; x_1; x_2 ]) ] ->
+    | `Assoc [ ("Adt", `List [ x_0; x_1; x_2; x_3 ]) ] ->
         let* x_0 = type_id_of_json x_0 in
         let* x_1 = option_of_json variant_id_of_json x_1 in
-        let* x_2 = generic_args_of_json x_2 in
-        Ok (AggregatedAdt (x_0, x_1, x_2))
+        let* x_2 = option_of_json field_id_of_json x_2 in
+        let* x_3 = generic_args_of_json x_3 in
+        Ok (AggregatedAdt (x_0, x_1, x_2, x_3))
     | `Assoc [ ("Array", `List [ x_0; x_1 ]) ] ->
         let* x_0 = ty_of_json x_0 in
         let* x_1 = const_generic_of_json x_1 in
@@ -1095,6 +1096,10 @@ and rvalue_of_json (js : json) : (rvalue, string) result =
     | `Assoc [ ("Global", global) ] ->
         let* global = global_decl_ref_of_json global in
         Ok (Global global)
+    | `Assoc [ ("GlobalRef", `List [ x_0; x_1 ]) ] ->
+        let* x_0 = global_decl_ref_of_json x_0 in
+        let* x_1 = ref_kind_of_json x_1 in
+        Ok (GlobalRef (x_0, x_1))
     | `Assoc [ ("Len", `List [ x_0; x_1; x_2 ]) ] ->
         let* x_0 = place_of_json x_0 in
         let* x_1 = ty_of_json x_1 in

charon-ml/src/PrintExpressions.ml

@@ -178,10 +178,18 @@ 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
+  | GlobalRef (global_ref, RShared) ->
+      let generics = generic_args_to_string env global_ref.global_generics in
+      "&global " ^ global_decl_id_to_string env global_ref.global_id ^ generics
+  | GlobalRef (global_ref, RMut) ->
+      let generics = generic_args_to_string env global_ref.global_generics in
+      "&raw mut global "
+      ^ global_decl_id_to_string env global_ref.global_id
+      ^ generics
   | Aggregate (akind, ops) -> (
       let ops = List.map (operand_to_string env) ops in
       match akind with
-      | AggregatedAdt (type_id, opt_variant_id, _generics) -> (
+      | AggregatedAdt (type_id, opt_variant_id, opt_field_id, _generics) -> (
           match type_id with
           | TTuple -> "(" ^ String.concat ", " ops ^ ")"
           | TAdtId def_id ->
@@ -197,6 +205,13 @@ let rvalue_to_string (env : ('a, 'b) fmt_env) (rv : rvalue) : string =
                 match adt_field_names env def_id opt_variant_id with
                 | None -> "(" ^ String.concat ", " ops ^ ")"
                 | Some field_names ->
+                    let field_names =
+                      match opt_field_id with
+                      | None -> field_names
+                      (* Only keep the selected field *)
+                      | Some field_id ->
+                          [ List.nth field_names (FieldId.to_int field_id) ]
+                    in
                     let fields = List.combine field_names ops in
                     let fields =
                       List.map

charon-ml/src/PrintUllbcAst.ml

@@ -31,6 +31,7 @@ module Ast = struct
     | StorageDead var_id ->
         indent ^ "storage_dead " ^ var_id_to_string env var_id
     | Deinit p -> indent ^ "deinit " ^ place_to_string env p
+    | StAssert a -> assertion_to_string env indent a
 
   let switch_to_string (indent : string) (tgt : switch) : string =
     match tgt with

charon-ml/src/UllbcAst.ml

@@ -36,6 +36,7 @@ and raw_statement =
       (** We translate this to [crate::llbc_ast::RawStatement::Drop] in LLBC *)
   | Deinit of place
       (** We translate this to [crate::llbc_ast::RawStatement::Drop] in LLBC *)
+  | StAssert of assertion
 [@@deriving
   show,
     visitors

charon-ml/src/UllbcOfJson.ml

@@ -43,6 +43,9 @@ and raw_statement_of_json (js : json) : (raw_statement, string) result =
     | `Assoc [ ("Deinit", deinit) ] ->
         let* deinit = place_of_json deinit in
         Ok (Deinit deinit)
+    | `Assoc [ ("Assert", assert_) ] ->
+        let* assert_ = assertion_of_json assert_ in
+        Ok (StAssert assert_)
     | _ -> Error "")
 
 and switch_of_json (js : json) : (switch, string) result =

charon/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.36"
+version = "0.1.37"
 authors = ["Son Ho <hosonmarc@gmail.com>"]
 edition = "2021"
 license = "Apache-2.0"
@@ -74,8 +74,8 @@ tracing-tree = { git = "https://github.com/Nadrieril/tracing-tree", features = [
 tracing = { version = "0.1", features = [ "max_level_trace", "release_max_level_warn" ] }
 which = "6.0.1"
 
-hax-frontend-exporter = { git = "https://github.com/hacspec/hax", branch = "main", optional = true }
-# hax-frontend-exporter = { git = "https://github.com/Nadrieril/hax", branch = "update-rustc", optional = true }
+# hax-frontend-exporter = { git = "https://github.com/hacspec/hax", branch = "main", optional = true }
+hax-frontend-exporter = { git = "https://github.com/Nadrieril/hax", branch = "charon", optional = true }
 # hax-frontend-exporter = { path = "../../hax/frontend/exporter", optional = true }
 macros = { path = "./macros" }
 

charon/src/ast/expressions.rs

@@ -40,7 +40,7 @@ pub type Projection = Vec<ProjectionElem>;
     DriveMut,
 )]
 pub enum ProjectionElem {
-    /// Dereference a shared/mutable reference.
+    /// Dereference a shared/mutable reference or a raw pointer.
     Deref,
     /// Dereference a boxed value.
     /// Note that this doesn't exist in MIR where `Deref` is used both for the
@@ -49,12 +49,6 @@ pub enum ProjectionElem {
     /// during the translation.
     /// In rust, this comes from the `*` operator applied on boxes.
     DerefBox,
-    /// Dereference a raw pointer. See the comments for [crate::types::Ty::RawPtr].
-    /// TODO: remove those (we would also need: `DerefPtrUnique`, `DerefPtrNonNull`, etc.)
-    /// and only keep a single `Deref` variant?
-    /// Or if we keep them, change to: `Deref(DerefKind)`?
-    #[charon::opaque]
-    DerefRawPtr,
     /// Projection from ADTs (variants, structures).
     /// We allow projections to be used as left-values and right-values.
     /// We should never have projections to fields of symbolic variants (they
@@ -419,8 +413,7 @@ pub enum RawConstantExpr {
     /// We eliminate this case in a micro-pass.
     #[charon::opaque]
     Adt(Option<VariantId>, Vec<ConstantExpr>),
-    ///
-    /// The value is a top-level value.
+    /// The value is a top-level constant/static.
     ///
     /// We eliminate this case in a micro-pass.
     ///
@@ -453,12 +446,16 @@ pub enum RawConstantExpr {
     /// Remark: trait constants can not be used in types, they are necessarily
     /// values.
     TraitConst(TraitRef, TraitItemName),
-    ///
-    /// A shared reference to a constant value
+    /// A shared reference to a constant value.
     ///
     /// We eliminate this case in a micro-pass.
     #[charon::opaque]
     Ref(Box<ConstantExpr>),
+    /// A mutable pointer to a mutable static.
+    ///
+    /// We eliminate this case in a micro-pass.
+    #[charon::opaque]
+    MutPtr(Box<ConstantExpr>),
     /// A const generic var
     Var(ConstGenericVarId),
     /// Function pointer
@@ -518,9 +515,13 @@ pub enum Rvalue {
     /// Remark: in case of closures, the aggregated value groups the closure id
     /// together with its state.
     Aggregate(AggregateKind, Vec<Operand>),
-    /// Not present in MIR: we introduce it when replacing constant variables
-    /// in operands in [extract_global_assignments.rs].
+    /// Copy the value of the referenced global.
+    /// Not present in MIR; introduced in [simplify_constants.rs].
     Global(GlobalDeclRef),
+    /// Reference the value of the global. This has type `&T` or `*mut T` depending on desired
+    /// mutability.
+    /// Not present in MIR; introduced in [simplify_constants.rs].
+    GlobalRef(GlobalDeclRef, RefKind),
     /// Length of a memory location. The run-time length of e.g. a vector or a slice is
     /// represented differently (but pretty-prints the same, FIXME).
     /// Should be seen as a function of signature:
@@ -579,7 +580,10 @@ pub enum Rvalue {
 #[derive(Debug, Clone, VariantIndexArity, Serialize, Deserialize, Drive, DriveMut)]
 #[charon::variants_prefix("Aggregated")]
 pub enum AggregateKind {
-    Adt(TypeId, Option<VariantId>, GenericArgs),
+    /// A struct, enum or union aggregate. The `VariantId`, if present, indicates this is an enum
+    /// and the aggregate uses that variant. The `FieldId`, if present, indicates this is a union
+    /// and the aggregate writes into that field. Otherwise this is a struct.
+    Adt(TypeId, Option<VariantId>, Option<FieldId>, GenericArgs),
     /// We don't put this with the ADT cas because this is the only built-in type
     /// with aggregates, and it is a primitive type. In particular, it makes
     /// sense to treat it differently because it has a variable number of fields.

charon/src/ast/ullbc_ast.rs

@@ -29,6 +29,8 @@ pub enum RawStatement {
     StorageDead(VarId),
     /// We translate this to [crate::llbc_ast::RawStatement::Drop] in LLBC
     Deinit(Place),
+    #[charon::rename("StAssert")]
+    Assert(Assert),
     #[charon::opaque]
     Error(String),
 }

charon/src/bin/charon-driver/translate/translate_constants.rs

@@ -126,6 +126,10 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 let be = self.translate_constant_expr_to_constant_expr(span, be)?;
                 RawConstantExpr::Ref(Box::new(be))
             }
+            ConstantExprKind::MutPtr(be) => {
+                let be = self.translate_constant_expr_to_constant_expr(span, be)?;
+                RawConstantExpr::MutPtr(Box::new(be))
+            }
             ConstantExprKind::ConstRef { id } => {
                 let var_id = self.const_generic_vars_map.get(&id.index);
                 if let Some(var_id) = var_id {
@@ -196,6 +200,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
             RawConstantExpr::Adt(..)
             | RawConstantExpr::TraitConst { .. }
             | RawConstantExpr::Ref(_)
+            | RawConstantExpr::MutPtr(_)
             | RawConstantExpr::FnPtr { .. } => {
                 error_or_panic!(
                     self,