Merge pull request #567 from Nadrieril/update-hax

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.69"
+let supported_charon_version = "0.1.70"

charon-ml/src/PrintExpressions.ml

@@ -128,6 +128,8 @@ let constant_expr_to_string (env : 'a fmt_env) (cv : constant_expr) : string =
       let trait_ref = trait_ref_to_string env trait_ref in
       trait_ref ^ const_name
   | CFnPtr fn_ptr -> fn_ptr_to_string env fn_ptr
+  | CRawMemory bytes ->
+      "RawMemory([" ^ String.concat ", " (List.map string_of_int bytes) ^ "])"
 
 let operand_to_string (env : 'a fmt_env) (op : operand) : string =
   match op with

charon-ml/src/generated/Generated_Expressions.ml

@@ -254,6 +254,10 @@ and raw_constant_expr =
        *)
   | CVar of const_generic_var_id de_bruijn_var  (** A const generic var *)
   | CFnPtr of fn_ptr  (** Function pointer *)
+  | CRawMemory of int list
+      (** Raw memory value obtained from constant evaluation. Used when a more structured
+          representation isn't possible (e.g. for unions) or just isn't implemented yet.
+       *)
 
 and constant_expr = { value : raw_constant_expr; ty : ty }
 

charon-ml/src/generated/Generated_GAstOfJson.ml

@@ -253,6 +253,9 @@ and raw_constant_expr_of_json (ctx : of_json_ctx) (js : json) :
     | `Assoc [ ("FnPtr", fn_ptr) ] ->
         let* fn_ptr = fn_ptr_of_json ctx fn_ptr in
         Ok (CFnPtr fn_ptr)
+    | `Assoc [ ("RawMemory", raw_memory) ] ->
+        let* raw_memory = list_of_json int_of_json ctx raw_memory in
+        Ok (CRawMemory raw_memory)
     | _ -> Error "")
 
 and constant_expr_of_json (ctx : of_json_ctx) (js : json) :

charon/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.69"
+version = "0.1.70"
 authors = ["Son Ho <[email protected]>"]
 edition = "2021"
 license = "Apache-2.0"

charon/src/ast/expressions.rs

@@ -468,6 +468,10 @@ pub enum RawConstantExpr {
     Var(ConstGenericDbVar),
     /// Function pointer
     FnPtr(FnPtr),
+    /// Raw memory value obtained from constant evaluation. Used when a more structured
+    /// representation isn't possible (e.g. for unions) or just isn't implemented yet.
+    #[drive(skip)]
+    RawMemory(Vec<u8>),
 }
 
 #[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, Drive, DriveMut)]

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

@@ -9,8 +9,8 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         v: &hax::ConstantLiteral,
     ) -> Result<RawConstantExpr, Error> {
         let lit = match v {
-            hax::ConstantLiteral::ByteStr(bs, _) => Literal::ByteStr(bs.clone()),
-            hax::ConstantLiteral::Str(s, _) => Literal::Str(s.clone()),
+            hax::ConstantLiteral::ByteStr(bs) => Literal::ByteStr(bs.clone()),
+            hax::ConstantLiteral::Str(s) => Literal::Str(s.clone()),
             hax::ConstantLiteral::Char(c) => Literal::Char(*c),
             hax::ConstantLiteral::Bool(b) => Literal::Bool(*b),
             hax::ConstantLiteral::Int(i) => {
@@ -67,7 +67,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
     ) -> Result<ConstantExpr, Error> {
         use hax::ConstantExprKind;
         let ty = &v.ty;
-        let value = match &(*v.contents) {
+        let value = match v.contents.as_ref() {
             ConstantExprKind::Literal(lit) => {
                 self.translate_constant_literal_to_raw_constant_expr(lit)?
             }
@@ -171,6 +171,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                 };
                 RawConstantExpr::FnPtr(fn_id.func)
             }
+            ConstantExprKind::Memory(bytes) => RawConstantExpr::RawMemory(bytes.clone()),
             ConstantExprKind::Todo(msg) => {
                 // Case not yet handled by hax
                 raise_error!(self, span, "Unsupported constant: {:?}", msg)
@@ -194,6 +195,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
             .translate_constant_expr_to_constant_expr(span, v)?
             .value;
         match value {
+            RawConstantExpr::Var(v) => Ok(ConstGeneric::Var(v)),
             RawConstantExpr::Literal(v) => Ok(ConstGeneric::Value(v)),
             RawConstantExpr::Global(global_ref) => {
                 // TODO: handle constant arguments with generics (this can likely only happen with
@@ -202,23 +204,13 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                 Ok(ConstGeneric::Global(global_ref.id))
             }
             RawConstantExpr::Adt(..)
+            | RawConstantExpr::RawMemory { .. }
             | RawConstantExpr::TraitConst { .. }
             | RawConstantExpr::Ref(_)
             | RawConstantExpr::MutPtr(_)
             | RawConstantExpr::FnPtr { .. } => {
                 raise_error!(self, span, "Unexpected constant generic: {:?}", value)
             }
-            RawConstantExpr::Var(v) => Ok(ConstGeneric::Var(v)),
         }
     }
-
-    /// Remark: [hax::ConstantExpr] contains span information, but it is often
-    /// the default span (i.e., it is useless), hence the additional span argument.
-    pub(crate) fn translate_constant_to_constant_expr(
-        &mut self,
-        span: Span,
-        v: &hax::Constant,
-    ) -> Result<ConstantExpr, Error> {
-        self.translate_constant_expr_to_constant_expr(span, &v.const_.constant_kind)
-    }
 }

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

@@ -430,8 +430,9 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                 let ty = p.ty().clone();
                 Ok((Operand::Move(p), ty))
             }
-            hax::Operand::Constant(constant) => {
-                let constant = self.translate_constant_to_constant_expr(span, constant)?;
+            hax::Operand::Constant(const_op) => {
+                let constant =
+                    self.translate_constant_expr_to_constant_expr(span, &const_op.const_)?;
                 let ty = constant.ty.clone();
                 Ok((Operand::Const(constant), ty))
             }

charon/src/pretty/fmt_with_ctx.rs

@@ -793,8 +793,9 @@ impl<C: AstFormatter> FmtWithCtx<C> for RawConstantExpr {
             }
             RawConstantExpr::Var(id) => format!("{}", ctx.format_object(*id)),
             RawConstantExpr::FnPtr(f) => {
-                format!("{}", f.fmt_with_ctx(ctx),)
+                format!("{}", f.fmt_with_ctx(ctx))
             }
+            RawConstantExpr::RawMemory(bytes) => format!("RawMemory({bytes:?})"),
         }
     }
 }

charon/src/transform/simplify_constants.rs

@@ -30,6 +30,7 @@ fn transform_constant_expr<F: FnMut(Ty) -> Place>(
     match val.value {
         RawConstantExpr::Literal(_)
         | RawConstantExpr::Var(_)
+        | RawConstantExpr::RawMemory(..)
         | RawConstantExpr::TraitConst(..)
         | RawConstantExpr::FnPtr(..) => {
             // Nothing to do

charon/tests/ui/associated-types.out

@@ -21,7 +21,7 @@ where
     parent_clause1 : [@TraitClause1]: core::marker::Sized<Self_Item>
     parent_clause2 : [@TraitClause2]: core::clone::Clone<Self_Item>
     fn use_item_required = test_crate::Foo::use_item_required<'a, Self, Self_Item>
-    fn use_item_provided<Clause0_Item, [@TraitClause0]: test_crate::Foo<'_, Self_Item, Clause0_Item>> = test_crate::Foo::use_item_provided<'a, Self, Clause0_Item, Self_Item>[@TraitClause0_0]
+    fn use_item_provided<Clause0_Item, [@TraitClause0]: test_crate::Foo<'a, Self_Item, Clause0_Item>> = test_crate::Foo::use_item_provided<'a, Self, Clause0_Item, Self_Item>[@TraitClause0_0]
 }
 
 enum core::option::Option<T>
@@ -73,7 +73,7 @@ where
 fn test_crate::{impl test_crate::Foo<'a, core::option::Option<&'a (T)>[core::marker::Sized<&'_ (T)>]> for &'a (T)}::use_item_provided<'a, T, Clause1_Item>(@1: core::option::Option<&'a (T)>[core::marker::Sized<&'_ (T)>]) -> core::option::Option<&'a (T)>[core::marker::Sized<&'_ (T)>]
 where
     [@TraitClause0]: core::marker::Sized<T>,
-    [@TraitClause1]: test_crate::Foo<'_, core::option::Option<&'a (T)>[core::marker::Sized<&'_ (T)>], Clause1_Item>,
+    [@TraitClause1]: test_crate::Foo<'a, core::option::Option<&'a (T)>[core::marker::Sized<&'_ (T)>], Clause1_Item>,
 {
     let @0: core::option::Option<&'a (T)>[core::marker::Sized<&'_ (T)>]; // return
     let x@1: core::option::Option<&'a (T)>[core::marker::Sized<&'_ (T)>]; // arg #1
@@ -90,7 +90,7 @@ where
     parent_clause1 = core::marker::Sized<core::option::Option<&'_ (T)>[core::marker::Sized<&'_ (T)>]>
     parent_clause2 = core::option::{impl core::clone::Clone for core::option::Option<T>[@TraitClause0]}#5<&'_ (T)>[core::marker::Sized<&'_ (T)>, core::clone::impls::{impl core::clone::Clone for &'_0 (T)}#3<'_, T>]
     fn use_item_required = test_crate::{impl test_crate::Foo<'a, core::option::Option<&'a (T)>[core::marker::Sized<&'_ (T)>]> for &'a (T)}::use_item_required<'a, T>[@TraitClause0]
-    fn use_item_provided<Clause0_Item, [@TraitClause0]: test_crate::Foo<'_, core::option::Option<&'a (T)>[core::marker::Sized<&'_ (T)>], Clause0_Item>> = test_crate::{impl test_crate::Foo<'a, core::option::Option<&'a (T)>[core::marker::Sized<&'_ (T)>]> for &'a (T)}::use_item_provided<'a, T, Clause0_Item>[@TraitClause0, @TraitClause0_0]
+    fn use_item_provided<Clause0_Item, [@TraitClause0]: test_crate::Foo<'a, core::option::Option<&'a (T)>[core::marker::Sized<&'_ (T)>], Clause0_Item>> = test_crate::{impl test_crate::Foo<'a, core::option::Option<&'a (T)>[core::marker::Sized<&'_ (T)>]> for &'a (T)}::use_item_provided<'a, T, Clause0_Item>[@TraitClause0, @TraitClause0_0]
 }
 
 impl<T> core::option::{impl core::marker::Copy for core::option::Option<T>[@TraitClause0]}#44<T> : core::marker::Copy<core::option::Option<T>[@TraitClause0]>
@@ -118,7 +118,7 @@ fn test_crate::{impl test_crate::Foo<'a, T> for core::option::Option<T>[@TraitCl
 where
     [@TraitClause0]: core::marker::Sized<T>,
     [@TraitClause1]: core::marker::Copy<T>,
-    [@TraitClause2]: test_crate::Foo<'_, T, Clause2_Item>,
+    [@TraitClause2]: test_crate::Foo<'a, T, Clause2_Item>,
     T : 'a,
 {
     let @0: T; // return
@@ -138,12 +138,12 @@ where
     parent_clause1 = @TraitClause0
     parent_clause2 = @TraitClause1::parent_clause0
     fn use_item_required = test_crate::{impl test_crate::Foo<'a, T> for core::option::Option<T>[@TraitClause0]}#1::use_item_required<'a, T>[@TraitClause0, @TraitClause1]
-    fn use_item_provided<Clause0_Item, [@TraitClause0]: test_crate::Foo<'_, T, Clause0_Item>> = test_crate::{impl test_crate::Foo<'a, T> for core::option::Option<T>[@TraitClause0]}#1::use_item_provided<'a, T, Clause0_Item>[@TraitClause0, @TraitClause1, @TraitClause0_0]
+    fn use_item_provided<Clause0_Item, [@TraitClause0]: test_crate::Foo<'a, T, Clause0_Item>> = test_crate::{impl test_crate::Foo<'a, T> for core::option::Option<T>[@TraitClause0]}#1::use_item_provided<'a, T, Clause0_Item>[@TraitClause0, @TraitClause1, @TraitClause0_0]
 }
 
 fn test_crate::Foo::use_item_provided<'a, Self, Clause0_Item, Self_Item>(@1: Self_Item) -> Self_Item
 where
-    [@TraitClause0]: test_crate::Foo<'_, Self_Item, Clause0_Item>,
+    [@TraitClause0]: test_crate::Foo<'a, Self_Item, Clause0_Item>,
 {
     let @0: Self_Item; // return
     let x@1: Self_Item; // arg #1
@@ -157,8 +157,8 @@ fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self
 fn test_crate::external_use_item<'a, T, Clause1_Item, Clause2_Item>(@1: Clause1_Item) -> Clause1_Item
 where
     [@TraitClause0]: core::marker::Sized<T>,
-    [@TraitClause1]: test_crate::Foo<'_, T, Clause1_Item>,
-    [@TraitClause2]: test_crate::Foo<'_, Clause1_Item, Clause2_Item>,
+    [@TraitClause1]: test_crate::Foo<'a, T, Clause1_Item>,
+    [@TraitClause2]: test_crate::Foo<'a, Clause1_Item, Clause2_Item>,
 {
     let @0: Clause1_Item; // return
     let x@1: Clause1_Item; // arg #1
@@ -196,8 +196,8 @@ fn test_crate::type_equality<'a, I, J, Clause2_Item>(@1: Clause2_Item) -> Clause
 where
     [@TraitClause0]: core::marker::Sized<I>,
     [@TraitClause1]: core::marker::Sized<J>,
-    [@TraitClause2]: test_crate::Foo<'_, I, Clause2_Item>,
-    [@TraitClause3]: test_crate::Foo<'_, J, Clause2_Item>,
+    [@TraitClause2]: test_crate::Foo<'a, I, Clause2_Item>,
+    [@TraitClause3]: test_crate::Foo<'a, J, Clause2_Item>,
 {
     let @0: Clause2_Item; // return
     let x@1: Clause2_Item; // arg #1
@@ -276,8 +276,8 @@ trait test_crate::loopy_with_generics::Foo<'b, Self, T>
 {
     parent_clause0 : [@TraitClause0]: core::marker::Sized<T>
     parent_clause1 : [@TraitClause1]: core::marker::Sized<Self::FooTy>
-    parent_clause2 : [@TraitClause2]: test_crate::loopy_with_generics::Foo<'_, Self::FooTy, T>
-    parent_clause3 : [@TraitClause3]: test_crate::loopy_with_generics::Bar<'_, Self::FooTy, u8, core::option::Option<T>[Self::parent_clause0], Self::Self_Clause3_BarTy>
+    parent_clause2 : [@TraitClause2]: test_crate::loopy_with_generics::Foo<'b, Self::FooTy, T>
+    parent_clause3 : [@TraitClause3]: test_crate::loopy_with_generics::Bar<'b, Self::FooTy, u8, core::option::Option<T>[Self::parent_clause0], Self::Self_Clause3_BarTy>
     type FooTy
     type Self_Clause3_BarTy
 }

charon/tests/ui/closures.out

@@ -292,7 +292,7 @@ trait test_crate::Trait<'a, Self>
 fn test_crate::test_closure_ref_early_bound::closure<'a, '_1, '_2, T>(@1: &'_2 (()), @2: &'_1 (T)) -> &'_1 (T)
 where
     [@TraitClause0]: core::marker::Sized<T>,
-    [@TraitClause1]: test_crate::Trait<'_, T>,
+    [@TraitClause1]: test_crate::Trait<'a, T>,
 {
     let @0: &'_ (T); // return
     let state@1: &'_2 (()); // arg #1
@@ -305,7 +305,7 @@ where
 fn test_crate::test_closure_ref_early_bound<'a, T>(@1: &'a (T)) -> &'a (T)
 where
     [@TraitClause0]: core::marker::Sized<T>,
-    [@TraitClause1]: test_crate::Trait<'_, T>,
+    [@TraitClause1]: test_crate::Trait<'a, T>,
 {
     let @0: &'_ (T); // return
     let x@1: &'_ (T); // arg #1

charon/tests/ui/issue-372-type-param-out-of-range.out

@@ -48,7 +48,7 @@ fn test_crate::{test_crate::S<'a, K>[@TraitClause0]}::g<'a, K, F>()
 where
     [@TraitClause0]: core::marker::Sized<K>,
     [@TraitClause1]: core::marker::Sized<F>,
-    [@TraitClause2]: for<'_0> core::ops::function::FnMut<F, (&'_0_0 (u32))>,
+    [@TraitClause2]: for<'b> core::ops::function::FnMut<F, (&'b (u32))>,
     for<'b> @TraitClause2::parent_clause0::Output = (),
 {
     let @0: (); // return