Repository: cryspen/hax (language: rust)

Issue:
`error[E9999]: scalar_int_to_constant_literal: the type *mut libc::c_void is not a literal`
When running `cargo hax json` for `getrandom`, I get:
```
Compiling libc v0.2.161
   Compiling cfg-if v1.0.0
   Compiling getrandom v0.2.15 (/home/maxime/test/getrandom)
disabled backtrace
error[E9999]: scalar_int_to_constant_literal: the type *mut libc::c_void is not a literal
   --> src/util_libc.rs:111:5
    |
111 |     pub fn ptr(&self) -> Option<NonNull<c_void>> {
    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
    = 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: could not compile `getrandom` (lib) due to 1 previous error
warning: hax: running `cargo build` was not successful, continuing anyway.
```

## Other crates having this issue:
 <details><summary>Crate `getrandom@0.2.15`</summary>
  
  
```
error[E9999]: scalar_int_to_constant_literal: the type *mut libc::c_void is not a literal
   --> src/util_libc.rs:111:5
    |
111 |     pub fn ptr(&self) -> Option<NonNull<c_void>> {
    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
    = 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)!


```
</details>

<details><summary>Crate `rustix@0.38.37`</summary>
  
  
```
error[E9999]: scalar_int_to_constant_literal: the type *mut std::ffi::c_void is not a literal
  --> src/weak.rs:67:5
   |
67 |     pub(crate) fn get(&self) -> Option<F> {
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |
   = 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)!


```
</details>

<details><summary>Crate `region@3.0.2`</summary>
  
  
```
error[E9999]: scalar_int_to_constant_literal: the type *mut libc::c_void is not a literal
  --> src/os/unix.rs:10:1
   |
10 | pub unsafe fn alloc(base: *const (), size: usize, protection: Protection) -> Result<*const ()> {
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |
   = 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)!


```
</details>




Discussion / hints:
Minimification:

```rust
const NULL: *mut () = std::ptr::null_mut();

unsafe fn f(x: *mut ()) -> () {
    match x {
        NULL => (),
        _ => (),
    }
}
```
[Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar/7cf8c4885c/gist=1e3ba1c7432f28ad430ca4a447c1521a)


Fix patch:
diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
index 7af3249f8..0fc1dd2de 100644
--- a/engine/lib/import_thir.ml
+++ b/engine/lib/import_thir.ml
@@ -837,7 +837,7 @@ end) : EXPR = struct
       | Borrow arg ->
           Borrow { arg = constant_expr_to_expr arg; borrow_kind = Thir.Shared }
       | ConstRef { id } -> ConstRef { id }
-      | MutPtr _ | TraitConst _ | FnPtr _ ->
+      | Cast _ | RawBorrow _ | TraitConst _ | FnPtr _ ->
           assertion_failure [ span ]
             "constant_lit_to_lit: TraitConst | FnPtr | MutPtr"
       | Todo _ -> assertion_failure [ span ] "ConstantExpr::Todo"
diff --git a/frontend/exporter/src/constant_utils.rs b/frontend/exporter/src/constant_utils.rs
index acaa7d0d7..ede21a233 100644
--- a/frontend/exporter/src/constant_utils.rs
+++ b/frontend/exporter/src/constant_utils.rs
@@ -78,8 +78,18 @@ pub enum ConstantExprKind {
     },
     /// A shared reference to a static variable.
     Borrow(ConstantExpr),
-    /// A `*mut` pointer to a static mutable variable.
-    MutPtr(ConstantExpr),
+    /// A raw borrow (`*const` or `*mut`).
+    RawBorrow {
+        mutability: Mutability,
+        arg: ConstantExpr,
+    },
+    /// A cast `<source> as <type>`, `<type>` is stored as the type of
+    /// the current constant expression. Currently, this is only used
+    /// to represent `lit as *mut T` or `lit as *const T`, where `lit`
+    /// is a `usize` literal.
+    Cast {
+        source: ConstantExpr,
+    },
     ConstRef {
         id: ParamConst,
     },
@@ -191,9 +201,9 @@ mod rustc {
                     borrow_kind: BorrowKind::Shared,
                     arg: e.into(),
                 },
-                MutPtr(e) => ExprKind::RawBorrow {
-                    mutability: true,
-                    arg: e.into(),
+                RawBorrow { mutability, arg } => ExprKind::RawBorrow {
+                    mutability,
+                    arg: arg.into(),
                 },
                 ConstRef { id } => ExprKind::ConstRef { id },
                 Array { fields } => ExprKind::Array {
@@ -202,6 +212,9 @@ mod rustc {
                 Tuple { fields } => ExprKind::Tuple {
                     fields: fields.into_iter().map(|field| field.into()).collect(),
                 },
+                Cast { source } => ExprKind::Cast {
+                    source: source.into(),
+                },
                 kind @ (FnPtr { .. } | TraitConst { .. }) => {
                     // SH: I see the `Closure` kind, but it's not the same as function pointer?
                     ExprKind::Todo(format!("FnPtr or TraitConst. kind={:#?}", kind))
@@ -215,10 +228,11 @@ mod rustc {
         }
     }
 
+    #[tracing::instrument(level = "trace", skip(s))]
     pub(crate) fn scalar_int_to_constant_literal<'tcx, S: UnderOwnerState<'tcx>>(
         s: &S,
         x: rustc_middle::ty::ScalarInt,
-        ty: rustc_middle::ty::Ty,
+        ty: rustc_middle::ty::Ty<'tcx>,
     ) -> ConstantLiteral {
         match ty.kind() {
             ty::Char => ConstantLiteral::Char(
@@ -236,14 +250,19 @@ mod rustc {
                 let v = x.to_uint(x.size());
                 ConstantLiteral::Int(ConstantInt::Uint(v, kind.sinto(s)))
             }
-            _ => fatal!(
-                s,
-                "scalar_int_to_constant_literal: the type {:?} is not a literal",
-                ty
-            ),
+            // https://github.com/rust-lang/rust/pull/116930
+            _ => {
+                let ty_sinto: Ty = ty.sinto(s);
+                supposely_unreachable_fatal!(
+                    s,
+                    "scalar_int_to_constant_literal_ExpectedLiteralType";
+                    { ty, ty_sinto, x }
+                )
+            }
         }
     }
 
+    #[tracing::instrument(level = "trace", skip(s))]
     pub(crate) fn scalar_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>(
         s: &S,
         ty: rustc_middle::ty::Ty<'tcx>,
@@ -317,7 +336,10 @@ mod rustc {
                 let contents = contents.decorate(inner_ty.sinto(s), cspan.clone());
                 match ty.kind() {
                     ty::Ref(..) => ConstantExprKind::Borrow(contents),
-                    ty::RawPtr(..) => ConstantExprKind::MutPtr(contents),
+                    ty::RawPtr(_, mutability) => ConstantExprKind::RawBorrow {
+                        arg: contents,
+                        mutability: mutability.sinto(s),
+                    },
                     _ => unreachable!(),
                 }
             }
@@ -373,6 +395,7 @@ mod rustc {
         )
     }
 
+    #[tracing::instrument(level = "trace", skip(s))]
     fn trait_const_to_constant_expr_kind<'tcx, S: BaseState<'tcx> + HasOwnerId>(
         s: &S,
         _const_def_id: rustc_hir::def_id::DefId,
@@ -486,6 +509,7 @@ mod rustc {
         }
     }
     impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ConstantExpr> for ty::Const<'tcx> {
+        #[tracing::instrument(level = "trace", skip(s))]
         fn sinto(&self, s: &S) -> ConstantExpr {
             use rustc_middle::query::Key;
             let span = self.default_span(s.base().tcx);
@@ -515,7 +539,7 @@ mod rustc {
         }
     }
 
-    // #[tracing::instrument(skip(s))]
+    #[tracing::instrument(level = "trace", skip(s))]
     pub(crate) fn valtree_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>(
         s: &S,
         valtree: rustc_middle::ty::ValTree<'tcx>,
@@ -523,59 +547,69 @@ mod rustc {
         span: rustc_span::Span,
     ) -> ConstantExpr {
         let kind = match (valtree, ty.kind()) {
-        (_, ty::Ref(_, inner_ty, _)) => {
-            ConstantExprKind::Borrow(valtree_to_constant_expr(s, valtree, *inner_ty, span))
-        }
-        (ty::ValTree::Branch(valtrees), ty::Str) => ConstantExprKind::Literal(
-            ConstantLiteral::byte_str(valtrees.iter().map(|x| match x {
-                ty::ValTree::Leaf(leaf) => leaf.to_u8(),
-                _ => fatal!(s[span], "Expected a flat list of leaves while translating a str literal, got a arbitrary valtree.")
-            }).collect(), StrStyle::Cooked))
-        ,
-        (ty::ValTree::Branch(_), ty::Array(..) | ty::Tuple(..) | ty::Adt(..)) => {
-            let contents: rustc_middle::ty::DestructuredConst = s
-                .base().tcx
-                .destructure_const(ty::Const::new_value(s.base().tcx, valtree, ty));
-            let fields = contents.fields.iter().copied();
-            match ty.kind() {
-                ty::Array(_, _) => ConstantExprKind::Array {
-                    fields: fields
-                        .map(|field| field.sinto(s))
-                        .collect(),
-                },
-                ty::Tuple(_) => ConstantExprKind::Tuple {
-                    fields: fields
-                        .map(|field| field.sinto(s))
-                        .collect(),
-                },
-                ty::Adt(def, _) => {
-                    let variant_idx = contents
-                        .variant
-                        .s_expect(s, "destructed const of adt without variant idx");
-                    let variant_def = &def.variant(variant_idx);
-
-                    ConstantExprKind::Adt{
-                        info: get_variant_information(def, variant_idx, s),
-                        fields: fields.into_iter()
-                            .zip(&variant_def.fields)
-                            .map(|(value, field)| ConstantFieldExpr {
-                                field: field.did.sinto(s),
-                                value: value.sinto(s),
-                            })
-                        .collect(),
+            (_, ty::Ref(_, inner_ty, _)) => {
+                ConstantExprKind::Borrow(valtree_to_constant_expr(s, valtree, *inner_ty, span))
+            }
+            (ty::ValTree::Branch(valtrees), ty::Str) => ConstantExprKind::Literal(
+                ConstantLiteral::byte_str(valtrees.iter().map(|x| match x {
+                    ty::ValTree::Leaf(leaf) => leaf.to_u8(),
+                    _ => fatal!(s[span], "Expected a flat list of leaves while translating a str literal, got a arbitrary valtree.")
+                }).collect(), StrStyle::Cooked))
+                ,
+            (ty::ValTree::Branch(_), ty::Array(..) | ty::Tuple(..) | ty::Adt(..)) => {
+                let contents: rustc_middle::ty::DestructuredConst = s
+                    .base().tcx
+                    .destructure_const(ty::Const::new_value(s.base().tcx, valtree, ty));
+                let fields = contents.fields.iter().copied();
+                match ty.kind() {
+                    ty::Array(_, _) => ConstantExprKind::Array {
+                        fields: fields
+                            .map(|field| field.sinto(s))
+                            .collect(),
+                    },
+                    ty::Tuple(_) => ConstantExprKind::Tuple {
+                        fields: fields
+                            .map(|field| field.sinto(s))
+                            .collect(),
+                    },
+                    ty::Adt(def, _) => {
+                        let variant_idx = contents
+                            .variant
+                            .s_expect(s, "destructed const of adt without variant idx");
+                        let variant_def = &def.variant(variant_idx);
+
+                        ConstantExprKind::Adt{
+                            info: get_variant_information(def, variant_idx, s),
+                            fields: fields.into_iter()
+                                .zip(&variant_def.fields)
+                                .map(|(value, field)| ConstantFieldExpr {
+                                    field: field.did.sinto(s),
+                                    value: value.sinto(s),
+                                })
+                                .collect(),
+                        }
                     }
+                    _ => unreachable!(),
                 }
-                _ => unreachable!(),
             }
-        }
-        (ty::ValTree::Leaf(x), _) => ConstantExprKind::Literal (
-            scalar_int_to_constant_literal(s, x, ty)
-        ),
-        _ => supposely_unreachable_fatal!(
-            s[span], "valtree_to_expr";
-            {valtree, ty}
-        ),
-    };
+            (ty::ValTree::Leaf(x), ty::RawPtr(_, _)) => {
+                use crate::rustc_type_ir::inherent::Ty;
+                let raw_address = x.to_bits_unchecked();
+                let uint_ty = UintTy::Usize;
+                let usize_ty = rustc_middle::ty::Ty::new_usize(s.base().tcx).sinto(s);
+                let lit = ConstantLiteral::Int(ConstantInt::Uint(raw_address, uint_ty));
+                ConstantExprKind::Cast {
+                    source: ConstantExprKind::Literal(lit).decorate(usize_ty, span.sinto(s))
+                }
+            }
+            (ty::ValTree::Leaf(x), _) => ConstantExprKind::Literal (
+                scalar_int_to_constant_literal(s, x, ty)
+            ),
+            _ => supposely_unreachable_fatal!(
+                s[span], "valtree_to_expr";
+                {valtree, ty}
+            ),
+        };
         kind.decorate(ty.sinto(s), span.sinto(s))
     }
 


Test patch:
diff --git a/test-harness/src/snapshots/toolchain__functions into-coq.snap b/test-harness/src/snapshots/toolchain__functions into-coq.snap
index 56ca87c28..29fe45a24 100644
--- a/test-harness/src/snapshots/toolchain__functions into-coq.snap
+++ b/test-harness/src/snapshots/toolchain__functions into-coq.snap
@@ -20,10 +20,12 @@ info:
     include_flag: ~
     backend_options: ~
 ---
-exit = 0
-
-[stdout]
-diagnostics = []
+exit = 1
+[[stdout.diagnostics]]
+message = '''
+(Coq backend) something is not implemented yet.
+[ty] node typ'''
+spans = ['Span { lo: Loc { line: 11, col: 4 }, hi: Loc { line: 17, col: 5 }, filename: Real(LocalPath("functions/src/lib.rs")), rust_span_data: None }']
 
 [stdout.files]
 "Functions.v" = '''
@@ -36,6 +38,8 @@ Open Scope bool_scope.
 
 (*Not implemented yet? todo(item)*)
 
+(*Not implemented yet? todo(item)*)
+
 Definition calling_function_pointer__f (_ : unit) : unit :=
   tt.
 
@@ -44,3 +48,19 @@ Definition calling_function_pointer (_ : unit) : unit :=
   let _ := calling_function_pointer__f tt : unit in
   tt.
 '''
+"Functions_Issue_1048_.v" = '''
+(* File automatically generated by Hacspec *)
+From Hacspec Require Import Hacspec_Lib MachineIntegers.
+From Coq Require Import ZArith.
+Import List.ListNotations.
+Open Scope Z_scope.
+Open Scope bool_scope.
+
+Record t_CallableViaDeref : Type := {
+}.
+
+(*item error backend*)
+
+Definition call_via_deref (_ : unit) : bool :=
+  f_deref CallableViaDereft_CallableViaDeref_t tt.
+'''
diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap
index 4aaf4ea2f..3ada99292 100644
--- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap
@@ -387,11 +387,11 @@ let method_caller
   ()
 
 class t_SubTrait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_8779313392680198588:t_Trait v_Self
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_11748868061750783190:t_Trait v_Self
     v_TypeArg
     v_ConstArg;
   f_AssocType:Type0;
-  f_AssocType_6369404467997533198:t_Trait f_AssocType v_TypeArg v_ConstArg
+  f_AssocType_10469511598065652520:t_Trait f_AssocType v_TypeArg v_ConstArg
 }
 '''
 "Traits.Interlaced_consts_types.fst" = '''