Merge pull request #308 from Nadrieril/bump-hax

AeneasVerif · Aug 14, 2024 · 67ab046 · 67ab046
2 parents f5131f4 + e004019
commit 67ab046
Show file tree

Hide file tree

Showing 35 changed files with 107 additions and 120 deletions.
diff --git a/charon-ml/src/CharonVersion.ml b/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.24"
+let supported_charon_version = "0.1.25"
diff --git a/charon-ml/src/GAstOfJson.ml b/charon-ml/src/GAstOfJson.ml
@@ -537,6 +537,9 @@ and type_decl_kind_of_json (id_to_file : id_to_file_map) (js : json) :
     | `Assoc [ ("Alias", alias) ] ->
         let* alias = ty_of_json alias in
         Ok (Alias alias)
+    | `Assoc [ ("Error", error) ] ->
+        let* error = string_of_json error in
+        Ok (Error error)
     | _ -> Error "")
 
 (* This is written by hand because the corresponding rust type does not exist. *)

diff --git a/charon-ml/src/PrintTypes.ml b/charon-ml/src/PrintTypes.ml
@@ -425,6 +425,7 @@ let type_decl_to_string (env : ('a, 'b) fmt_env) (def : type_decl) : string =
       "enum " ^ name ^ params ^ clauses ^ "\n  =\n" ^ variants
   | Alias ty -> "type " ^ name ^ params ^ clauses ^ " = " ^ ty_to_string env ty
   | Opaque -> "opaque type " ^ name ^ params ^ clauses
+  | Error err -> "error(\"" ^ err ^ "\")"
 
 let adt_variant_to_string (env : ('a, 'b) fmt_env) (def_id : TypeDeclId.id)
     (variant_id : VariantId.id) : string =
@@ -435,7 +436,7 @@ let adt_variant_to_string (env : ('a, 'b) fmt_env) (def_id : TypeDeclId.id)
       ^ variant_id_to_pretty_string variant_id
   | Some def -> (
       match def.kind with
-      | Struct _ | Alias _ | Opaque -> raise (Failure "Unreachable")
+      | Struct _ | Alias _ | Opaque | Error _ -> raise (Failure "Unreachable")
       | Enum variants ->
           let variant = VariantId.nth variants variant_id in
           name_to_string env def.item_meta.name ^ "::" ^ variant.variant_name)

diff --git a/charon-ml/src/Substitute.ml b/charon-ml/src/Substitute.ml
@@ -259,10 +259,10 @@ let type_decl_get_instantiated_variants_fields_types (def : type_decl)
     | Enum variants ->
         List.mapi (fun i v -> (Some (VariantId.of_int i), v.fields)) variants
     | Struct fields -> [ (None, fields) ]
-    | Alias _ | Opaque ->
+    | Alias _ | Opaque | Error _ ->
         raise
           (Failure
-             ("Can't retrieve the variants of an opaque or alias type: "
+             ("Can't retrieve the variants of non-adt type: "
              ^ show_name def.item_meta.name))
   in
   List.map

diff --git a/charon-ml/src/Types.ml b/charon-ml/src/Types.ml
@@ -337,6 +337,9 @@ and ty =
           - assumed types (includes some primitive types, e.g., arrays or slices)
           The information on the nature of the ADT is stored in (`TypeId`)[TypeId].
           The last list is used encode const generics, e.g., the size of an array
+
+          Note: this is incorrectly named: this can refer to any valid `TypeDecl` including extern
+          types.
        *)
   | TVar of type_var_id
   | TLiteral of literal_type
@@ -717,6 +720,10 @@ and type_decl_kind =
       (** An alias to another type. This only shows up in the top-level list of items, as rustc
           inlines uses of type aliases everywhere else.
        *)
+  | Error of string
+      (** Used if an error happened during the extraction, and we don't panic
+          on error.
+       *)
 
 (** A type declaration.
 

diff --git a/charon/Cargo.lock b/charon/Cargo.lock
diff --git a/charon/Cargo.toml b/charon/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.24"
+version = "0.1.25"
 authors = ["Son Ho <[email protected]>"]
 edition = "2021"
 
@@ -70,6 +70,7 @@ tracing = { version = "0.1", features = [ "max_level_trace", "release_max_level_
 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 = { path = "../../hax/frontend/exporter", optional = true }
 macros = { path = "./macros" }
 

diff --git a/charon/src/ast/types.rs b/charon/src/ast/types.rs
@@ -433,7 +433,6 @@ pub enum TypeDeclKind {
     Alias(Ty),
     /// Used if an error happened during the extraction, and we don't panic
     /// on error.
-    #[charon::opaque]
     Error(String),
 }
 
@@ -631,6 +630,9 @@ pub enum Ty {
     /// - assumed types (includes some primitive types, e.g., arrays or slices)
     /// The information on the nature of the ADT is stored in (`TypeId`)[TypeId].
     /// The last list is used encode const generics, e.g., the size of an array
+    ///
+    /// Note: this is incorrectly named: this can refer to any valid `TypeDecl` including extern
+    /// types.
     Adt(TypeId, GenericArgs),
     #[charon::rename("TVar")]
     TypeVar(TypeVarId),

diff --git a/charon/src/bin/charon-driver/main.rs b/charon/src/bin/charon-driver/main.rs
@@ -7,7 +7,6 @@
 #![feature(iter_array_chunks)]
 #![feature(iterator_try_collect)]
 #![feature(let_chains)]
-#![feature(lint_reasons)]
 
 extern crate rustc_ast;
 extern crate rustc_ast_pretty;

diff --git a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs
@@ -1162,17 +1162,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                     target,
                 }
             }
-            TerminatorKind::Yield {
-                value: _,
-                resume: _,
-                resume_arg: _,
-                drop: _,
-            } => {
-                error_or_panic!(self, rustc_span, "Unsupported terminator: yield");
-            }
-            TerminatorKind::CoroutineDrop => {
-                error_or_panic!(self, rustc_span, "Unsupported terminator: coroutine drop");
-            }
             TerminatorKind::FalseEdge {
                 real_target,
                 imaginary_target,
@@ -1203,6 +1192,15 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
             TerminatorKind::InlineAsm { .. } => {
                 error_or_panic!(self, rustc_span, "Inline assembly is not supported");
             }
+            TerminatorKind::CoroutineDrop
+            | TerminatorKind::TailCall { .. }
+            | TerminatorKind::Yield { .. } => {
+                error_or_panic!(
+                    self,
+                    rustc_span,
+                    format!("Unsupported terminator: {:?}", terminator.kind)
+                );
+            }
         };
 
         // Add the span information

diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs
@@ -341,13 +341,10 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 }
             }
 
-            hax::Ty::Foreign(id) => {
+            hax::Ty::Foreign(def_id) => {
                 trace!("Foreign");
-                error_or_panic!(
-                    self,
-                    span,
-                    format!("Unsupported type: foreign type: {:?}", DefId::from(id))
-                )
+                let def_id = self.translate_type_id(span, def_id)?;
+                Ok(Ty::Adt(def_id, GenericArgs::empty()))
             }
             hax::Ty::Infer(_) => {
                 trace!("Infer");

diff --git a/charon/src/lib.rs b/charon/src/lib.rs
@@ -19,7 +19,6 @@
 #![feature(impl_trait_in_assoc_type)]
 #![feature(iterator_try_collect)]
 #![feature(let_chains)]
-#![feature(lint_reasons)]
 #![feature(trait_alias)]
 #![feature(register_tool)]
 // For when we use charon on itself :3

diff --git a/charon/tests/crate_data.rs b/charon/tests/crate_data.rs
@@ -1,5 +1,4 @@
 #![feature(rustc_private)]
-#![feature(lint_reasons)]
 
 use assert_cmd::prelude::{CommandCargoExt, OutputAssertExt};
 use itertools::Itertools;

diff --git a/charon/tests/ui/external.out b/charon/tests/ui/external.out
@@ -52,7 +52,7 @@ impl core::clone::impls::{impl core::clone::Clone for u32}#8 : core::clone::Clon
     fn clone = core::clone::impls::{impl core::clone::Clone for u32}#8::clone
 }
 
-impl core::marker::{impl core::marker::Copy for u32}#41 : core::marker::Copy<u32>
+impl core::marker::{impl core::marker::Copy for u32}#40 : core::marker::Copy<u32>
 {
     parent_clause0 = core::clone::impls::{impl core::clone::Clone for u32}#8
 }
@@ -75,7 +75,7 @@ impl core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzer
 
 impl core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for u32}#20 : core::num::nonzero::ZeroablePrimitive<u32>
 {
-    parent_clause0 = core::marker::{impl core::marker::Copy for u32}#41
+    parent_clause0 = core::marker::{impl core::marker::Copy for u32}#40
     parent_clause1 = core::num::nonzero::{impl core::num::nonzero::private::Sealed for u32}#19
     parent_clause2 = core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroU32Inner}#12
     parent_clause3 = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroU32Inner}#11
@@ -153,7 +153,7 @@ fn test_crate::use_get<'_0>(@1: &'_0 (core::cell::Cell<u32>)) -> u32
     let @2: &'_ (core::cell::Cell<u32>); // anonymous local
 
     @2 := &*(rc@1)
-    @0 := core::cell::{core::cell::Cell<T>}#10::get<u32>[core::marker::{impl core::marker::Copy for u32}#41](move (@2))
+    @0 := core::cell::{core::cell::Cell<T>}#10::get<u32>[core::marker::{impl core::marker::Copy for u32}#40](move (@2))
     drop @2
     return
 }

diff --git a/charon/tests/ui/generic-associated-types.out b/charon/tests/ui/generic-associated-types.out
@@ -16,7 +16,7 @@ error: Ignoring the following item due to an error: test_crate::{impl#0}
 10 | impl<'a, T> LendingIterator for Option<&'a T> {
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-thread 'rustc' panicked at /rustc/6b0f4b5ec3aa707ecaa78230722117324a4ce23c/compiler/rustc_type_ir/src/binder.rs:785:9:
+thread 'rustc' panicked at /rustc/730d5d4095a264ef5f7c0a0781eea68c15431d45/compiler/rustc_type_ir/src/binder.rs:783:9:
 const parameter `'a/#1` ('a/#1/1) out of range when instantiating args=[Self/#0]
 note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
 error: Thread panicked when extracting item `test_crate::LendingIterator::next`.
@@ -38,9 +38,10 @@ warning[E9999]: Hax frontend found a projected type with escaping bound vars. Pl
                  - alias_ty: AliasTy {
                     args: [
                         impl for<'a> FnMut(I::Item<'a>)/#1,
-                        (Alias(Projection, AliasTy { args: [I/#0, '^0.Named(test_crate::for_each::'a, "'a")], def_id: test_crate::LendingIterator::Item }),),
+                        (Alias(Projection, AliasTy { args: [I/#0, '^0.Named(test_crate::for_each::'a, "'a")], def_id: test_crate::LendingIterator::Item, .. }),),
                     ],
                     def_id: core::ops::function::FnOnce::Output,
+                    ..
                 }
                  - alias_kind: Projection
                  - trait_ref: <impl for<'a> FnMut(I::Item<'a>) as std::ops::FnOnce<(<I as LendingIterator>::Item<'a>,)>>
@@ -50,17 +51,17 @@ warning[E9999]: Hax frontend found a projected type with escaping bound vars. Pl
                 )
                  - rebased_generics: [
                     impl for<'a> FnMut(I::Item<'a>)/#1,
-                    (Alias(Projection, AliasTy { args: [I/#0, '^0.Named(test_crate::for_each::'a, "'a")], def_id: test_crate::LendingIterator::Item }),),
-                    (Alias(Projection, AliasTy { args: [I/#0, '^0.Named(test_crate::for_each::'a, "'a")], def_id: test_crate::LendingIterator::Item }),),
+                    (Alias(Projection, AliasTy { args: [I/#0, '^0.Named(test_crate::for_each::'a, "'a")], def_id: test_crate::LendingIterator::Item, .. }),),
+                    (Alias(Projection, AliasTy { args: [I/#0, '^0.Named(test_crate::for_each::'a, "'a")], def_id: test_crate::LendingIterator::Item, .. }),),
                 ]
                  - norm_rebased_generics: Err(
                     Type(
-                        (Alias(Projection, AliasTy { args: [impl for<'a> FnMut(I::Item<'a>)/#1, '^0.Named(test_crate::for_each::'a, "'a")], def_id: test_crate::LendingIterator::Item }),),
+                        (Alias(Projection, AliasTy { args: [impl for<'a> FnMut(I::Item<'a>)/#1, '^0.Named(test_crate::for_each::'a, "'a")], def_id: test_crate::LendingIterator::Item, .. }),),
                     ),
                 )
                  - norm_generics: Err(
                     Type(
-                        (Alias(Projection, AliasTy { args: [impl for<'a> FnMut(I::Item<'a>)/#1, '^0.Named(test_crate::for_each::'a, "'a")], def_id: test_crate::LendingIterator::Item }),),
+                        (Alias(Projection, AliasTy { args: [impl for<'a> FnMut(I::Item<'a>)/#1, '^0.Named(test_crate::for_each::'a, "'a")], def_id: test_crate::LendingIterator::Item, .. }),),
                     ),
                 )
                  - early_binder_generics: Ok(
@@ -73,7 +74,7 @@ warning[E9999]: Hax frontend found a projected type with escaping bound vars. Pl
   = 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)!
 
-thread 'rustc' panicked at /rustc/6b0f4b5ec3aa707ecaa78230722117324a4ce23c/compiler/rustc_type_ir/src/binder.rs:785:9:
+thread 'rustc' panicked at /rustc/730d5d4095a264ef5f7c0a0781eea68c15431d45/compiler/rustc_type_ir/src/binder.rs:783:9:
 const parameter `'a/#1` ('a/#1/1) out of range when instantiating args=[I/#0]
 error: Thread panicked when extracting item `test_crate::for_each`.
   --> tests/ui/generic-associated-types.rs:24:1
@@ -97,5 +98,4 @@ warning: unused variable: `x`
 
 error: aborting due to 6 previous errors; 2 warnings emitted
 
-[ERROR charon_driver:249] Compilation encountered 6 errors
-Error: Charon driver exited with code 1
+Error: Charon driver exited with code 101
diff --git a/charon/tests/ui/issue-4-slice-try-into-array.out b/charon/tests/ui/issue-4-slice-try-into-array.out
@@ -63,7 +63,7 @@ impl core::clone::impls::{impl core::clone::Clone for u8}#6 : core::clone::Clone
     fn clone = core::clone::impls::{impl core::clone::Clone for u8}#6::clone
 }
 
-impl core::marker::{impl core::marker::Copy for u8}#39 : core::marker::Copy<u8>
+impl core::marker::{impl core::marker::Copy for u8}#38 : core::marker::Copy<u8>
 {
     parent_clause0 = core::clone::impls::{impl core::clone::Clone for u8}#6
 }
@@ -102,7 +102,7 @@ fn test_crate::trait_error<'_0>(@1: &'_0 (Slice<u8>))
     let @5: (); // anonymous local
 
     @4 := &*(s@1)
-    @3 := core::convert::{impl core::convert::TryInto<U> for T}#6<&'_ (Slice<u8>), Array<u8, 4 : usize>>[core::array::{impl core::convert::TryFrom<&'_0 (Slice<T>)> for Array<T, const N : usize>}#7<'_, u8, 4 : usize>[core::marker::{impl core::marker::Copy for u8}#39]]::try_into(move (@4))
+    @3 := core::convert::{impl core::convert::TryInto<U> for T}#6<&'_ (Slice<u8>), Array<u8, 4 : usize>>[core::array::{impl core::convert::TryFrom<&'_0 (Slice<T>)> for Array<T, const N : usize>}#7<'_, u8, 4 : usize>[core::marker::{impl core::marker::Copy for u8}#38]]::try_into(move (@4))
     drop @4
     _array@2 := core::result::{core::result::Result<T, E>}::unwrap<Array<u8, 4 : usize>, core::array::TryFromSliceError>[core::array::{impl core::fmt::Debug for core::array::TryFromSliceError}#26](move (@3))
     drop @3

diff --git a/charon/tests/ui/issue-4-traits.out b/charon/tests/ui/issue-4-traits.out
@@ -63,7 +63,7 @@ impl core::clone::impls::{impl core::clone::Clone for u8}#6 : core::clone::Clone
     fn clone = core::clone::impls::{impl core::clone::Clone for u8}#6::clone
 }
 
-impl core::marker::{impl core::marker::Copy for u8}#39 : core::marker::Copy<u8>
+impl core::marker::{impl core::marker::Copy for u8}#38 : core::marker::Copy<u8>
 {
     parent_clause0 = core::clone::impls::{impl core::clone::Clone for u8}#6
 }
@@ -102,7 +102,7 @@ fn test_crate::trait_error<'_0>(@1: &'_0 (Slice<u8>))
     let @5: (); // anonymous local
 
     @4 := &*(s@1)
-    @3 := core::convert::{impl core::convert::TryInto<U> for T}#6<&'_ (Slice<u8>), Array<u8, 4 : usize>>[core::array::{impl core::convert::TryFrom<&'_0 (Slice<T>)> for Array<T, const N : usize>}#7<'_, u8, 4 : usize>[core::marker::{impl core::marker::Copy for u8}#39]]::try_into(move (@4))
+    @3 := core::convert::{impl core::convert::TryInto<U> for T}#6<&'_ (Slice<u8>), Array<u8, 4 : usize>>[core::array::{impl core::convert::TryFrom<&'_0 (Slice<T>)> for Array<T, const N : usize>}#7<'_, u8, 4 : usize>[core::marker::{impl core::marker::Copy for u8}#38]]::try_into(move (@4))
     drop @4
     _array@2 := core::result::{core::result::Result<T, E>}::unwrap<Array<u8, 4 : usize>, core::array::TryFromSliceError>[core::array::{impl core::fmt::Debug for core::array::TryFromSliceError}#26](move (@3))
     drop @3

diff --git a/charon/tests/ui/issue-45-misc.out b/charon/tests/ui/issue-45-misc.out
@@ -301,7 +301,7 @@ impl core::clone::impls::{impl core::clone::Clone for usize}#5 : core::clone::Cl
     fn clone = core::clone::impls::{impl core::clone::Clone for usize}#5::clone
 }
 
-impl core::marker::{impl core::marker::Copy for usize}#38 : core::marker::Copy<usize>
+impl core::marker::{impl core::marker::Copy for usize}#37 : core::marker::Copy<usize>
 {
     parent_clause0 = core::clone::impls::{impl core::clone::Clone for usize}#5
 }
@@ -324,7 +324,7 @@ impl core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzer
 
 impl core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26 : core::num::nonzero::ZeroablePrimitive<usize>
 {
-    parent_clause0 = core::marker::{impl core::marker::Copy for usize}#38
+    parent_clause0 = core::marker::{impl core::marker::Copy for usize}#37
     parent_clause1 = core::num::nonzero::{impl core::num::nonzero::private::Sealed for usize}#25
     parent_clause2 = core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner}#27
     parent_clause3 = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner}#26

diff --git a/charon/tests/ui/issue-73-extern.out b/charon/tests/ui/issue-73-extern.out
@@ -6,5 +6,17 @@ global test_crate::CONST
 
 opaque type test_crate::Type
 
+fn test_crate::use_type<'_0>(@1: &'_0 (test_crate::Type))
+{
+    let @0: (); // return
+    let _x@1: &'_ (test_crate::Type); // arg #1
+    let @2: (); // anonymous local
+
+    @2 := ()
+    @0 := move (@2)
+    @0 := ()
+    return
+}
+
 
 
diff --git a/charon/tests/ui/issue-73-extern.rs b/charon/tests/ui/issue-73-extern.rs
@@ -4,3 +4,5 @@ extern "C" {
     static CONST: u8;
     type Type;
 }
+
+fn use_type(_x: &Type) {}
diff --git a/charon/tests/ui/issue-91-enum-to-discriminant-cast.out b/charon/tests/ui/issue-91-enum-to-discriminant-cast.out
@@ -6,5 +6,4 @@ error: Unsupported statement kind: intrinsic
 
 error: aborting due to 1 previous error
 
-[ERROR charon_driver:249] Compilation encountered 1 errors
-Error: Charon driver exited with code 1
+Error: Charon driver exited with code 101
diff --git a/charon/tests/ui/loops.out b/charon/tests/ui/loops.out
@@ -1030,7 +1030,7 @@ impl core::clone::impls::{impl core::clone::Clone for usize}#5 : core::clone::Cl
     fn clone = core::clone::impls::{impl core::clone::Clone for usize}#5::clone
 }
 
-impl core::marker::{impl core::marker::Copy for usize}#38 : core::marker::Copy<usize>
+impl core::marker::{impl core::marker::Copy for usize}#37 : core::marker::Copy<usize>
 {
     parent_clause0 = core::clone::impls::{impl core::clone::Clone for usize}#5
 }
@@ -1053,7 +1053,7 @@ impl core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzer
 
 impl core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}#26 : core::num::nonzero::ZeroablePrimitive<usize>
 {
-    parent_clause0 = core::marker::{impl core::marker::Copy for usize}#38
+    parent_clause0 = core::marker::{impl core::marker::Copy for usize}#37
     parent_clause1 = core::num::nonzero::{impl core::num::nonzero::private::Sealed for usize}#25
     parent_clause2 = core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner}#27
     parent_clause3 = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner}#26