Merge pull request #597 from Nadrieril/update-hax

Update hax

Author: Nadrieril

charon/Cargo.lock

@@ -4,6 +4,7 @@
 #![expect(incomplete_features)]
 #![feature(box_patterns)]
 #![feature(deref_patterns)]
+#![feature(if_let_guard)]
 #![feature(iter_array_chunks)]
 #![feature(iterator_try_collect)]
 #![feature(let_chains)]

charon/src/bin/charon-driver/main.rs

@@ -6,11 +6,16 @@ use hax_frontend_exporter as hax;
 impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
     fn translate_constant_literal_to_raw_constant_expr(
         &mut self,
+        span: Span,
         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::Str(..) => {
+                // This should have been handled in the `&str` case. If we get here, there's a
+                // `str` value not behind a reference.
+                raise_error!(self, span, "found a `str` constants not behind a reference")
+            }
             hax::ConstantLiteral::Char(c) => Literal::Char(*c),
             hax::ConstantLiteral::Bool(b) => Literal::Bool(*b),
             hax::ConstantLiteral::Int(i) => {
@@ -66,15 +71,14 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         v: &hax::ConstantExpr,
     ) -> Result<ConstantExpr, Error> {
         use hax::ConstantExprKind;
-        let ty = &v.ty;
+        let ty = self.translate_ty(span, &v.ty)?;
         let value = match v.contents.as_ref() {
             ConstantExprKind::Literal(lit) => {
-                self.translate_constant_literal_to_raw_constant_expr(lit)?
+                self.translate_constant_literal_to_raw_constant_expr(span, lit)?
             }
             ConstantExprKind::Adt { info, fields } => {
                 let fields: Vec<ConstantExpr> = fields
                     .iter()
-                    // TODO: the user_ty is not always None
                     .map(|f| self.translate_constant_expr_to_constant_expr(span, &f.value))
                     .try_collect()?;
                 use hax::VariantKind;
@@ -85,8 +89,25 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                 };
                 RawConstantExpr::Adt(vid, fields)
             }
-            ConstantExprKind::Array { .. } => {
-                raise_error!(self, span, "array constants are not supported yet")
+            ConstantExprKind::Array { fields } => {
+                let fields: Vec<ConstantExpr> = fields
+                    .iter()
+                    .map(|x| self.translate_constant_expr_to_constant_expr(span, x))
+                    .try_collect()?;
+                if let TyKind::Adt(TypeId::Builtin(BuiltinTy::Array), args) = ty.kind()
+                    && let TyKind::Literal(LiteralTy::Integer(IntegerTy::U8)) = args.types[0].kind()
+                {
+                    RawConstantExpr::Literal(Literal::ByteStr(
+                        fields
+                            .iter()
+                            .map(|konst| konst.value.as_literal().unwrap())
+                            .map(|x| x.as_scalar().unwrap().as_u8().unwrap())
+                            .copied()
+                            .collect(),
+                    ))
+                } else {
+                    raise_error!(self, span, "array constants are not supported yet")
+                }
             }
             ConstantExprKind::Tuple { fields } => {
                 let fields: Vec<ConstantExpr> = fields
@@ -125,9 +146,15 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                     generics,
                 })
             }
-            ConstantExprKind::Borrow(be) => {
-                let be = self.translate_constant_expr_to_constant_expr(span, be)?;
-                RawConstantExpr::Ref(Box::new(be))
+            ConstantExprKind::Borrow(v)
+                if let ConstantExprKind::Literal(hax::ConstantLiteral::Str(s)) =
+                    v.contents.as_ref() =>
+            {
+                RawConstantExpr::Literal(Literal::Str(s.clone()))
+            }
+            ConstantExprKind::Borrow(v) => {
+                let val = self.translate_constant_expr_to_constant_expr(span, v)?;
+                RawConstantExpr::Ref(Box::new(val))
             }
             ConstantExprKind::Cast { .. } => {
                 raise_error!(
@@ -178,7 +205,6 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
             }
         };
 
-        let ty = self.translate_ty(span, ty)?;
         Ok(ConstantExpr { value, ty })
     }
 

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

@@ -432,7 +432,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
             }
             hax::Operand::Constant(const_op) => {
                 let constant =
-                    self.translate_constant_expr_to_constant_expr(span, &const_op.const_)?;
+                    self.translate_constant_expr_to_constant_expr(span, &const_op.evaluated)?;
                 let ty = constant.ty.clone();
                 Ok((Operand::Const(constant), ty))
             }

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

@@ -8,7 +8,7 @@ fn test_crate::two() -> &'static (u32)
     let @3: u32; // anonymous local
     let @4: &'_ (u32); // anonymous local
 
-    @3 := const (RawMemory([2, 0, 0, 0]))
+    @3 := const (2 : u32)
     @4 := &@3
     @2 := move (@4)
     @1 := copy (@2)

charon/tests/ui/simple/promoted-literal-addition.out

@@ -11,7 +11,7 @@ fn test_crate::main()
     let @6: u8; // anonymous local
     let @7: &'_ (u8); // anonymous local
 
-    @6 := const (RawMemory([0]))
+    @6 := const (0 : u8)
     @7 := &@6
     @5 := move (@7)
     @2 := copy (@5)

charon/tests/ui/simple/ptr_to_promoted.out

@@ -43,20 +43,6 @@ error: Item `test_crate::foo` caused errors; ignoring.
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
 
-disabled backtrace
-warning[E9999]: Failed to compute associated type <T as std::marker::DiscriminantKind>::Discriminant
- --> /rustc/86d69c705a552236a622eee3fdea94bf13c5f102/library/core/src/intrinsics.rs:2556:5
-  |
-  = note: ⚠️ This is a bug in Hax's frontend.
-          Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!
-
-disabled backtrace
-warning[E9999]: Failed to compute associated type <Self as std::marker::DiscriminantKind>::Discriminant
- --> /rustc/86d69c705a552236a622eee3fdea94bf13c5f102/library/core/src/marker.rs:823:5
-  |
-  = note: ⚠️ This is a bug in Hax's frontend.
-          Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!
-
-error: aborting due to 1 previous error; 2 warnings emitted
+error: aborting due to 1 previous error
 
 ERROR Code failed to compile