Merge pull request #222 from Nadrieril/bump-hax

charon/Cargo.toml

@@ -56,8 +56,8 @@ which = "6.0.1"
 
 hax-frontend-exporter = { git = "https://github.com/hacspec/hax", branch = "main" }
 hax-frontend-exporter-options = { git = "https://github.com/hacspec/hax", branch = "main" }
-# hax-frontend-exporter = { path = "../../hacspec-v2/frontend/exporter" }
-# hax-frontend-exporter-options = { path = "../../hacspec-v2/frontend/exporter/options" }
+# hax-frontend-exporter = { path = "../../hax/frontend/exporter" }
+# hax-frontend-exporter-options = { path = "../../hax/frontend/exporter/options" }
 macros = { path = "./macros" }
 
 [dev-dependencies]

charon/src/ast/names_utils.rs

@@ -313,27 +313,27 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
         let def_id = item.owner_id.to_def_id();
 
         let name = match &item.kind {
-            ItemKind::OpaqueTy(_) => unimplemented!(),
-            ItemKind::Union(_, _) => unimplemented!(),
-            ItemKind::ExternCrate(_) => {
+            ItemKind::OpaqueTy(..) => unimplemented!(),
+            ItemKind::Union(..) => unimplemented!(),
+            ItemKind::ExternCrate(..) => {
                 // We ignore this -
                 // TODO: investigate when extern crates appear, and why
                 Option::None
             }
-            ItemKind::Use(_, _) => Option::None,
-            ItemKind::TyAlias(_, _) => {
+            ItemKind::Use(..) => Option::None,
+            ItemKind::TyAlias(..) => {
                 // We ignore the type aliases - it seems they are inlined
                 Option::None
             }
-            ItemKind::Enum(_, _)
-            | ItemKind::Struct(_, _)
-            | ItemKind::Fn(_, _, _)
-            | ItemKind::Impl(_)
-            | ItemKind::Mod(_)
+            ItemKind::Enum(..)
+            | ItemKind::Struct(..)
+            | ItemKind::Fn(..)
+            | ItemKind::Impl(..)
+            | ItemKind::Mod(..)
             | ItemKind::ForeignMod { .. }
-            | ItemKind::Const(_, _)
-            | ItemKind::Static(_, _, _)
-            | ItemKind::Macro(_, _)
+            | ItemKind::Const(..)
+            | ItemKind::Static(..)
+            | ItemKind::Macro(..)
             | ItemKind::Trait(..) => Option::Some(self.def_id_to_name(def_id)?),
             _ => {
                 unimplemented!("{:?}", item.kind);

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

@@ -101,7 +101,11 @@ impl Callbacks for CharonCallbacks {
     /// For this reason, and as we may want to plug ourselves at different
     /// phases of the compilation process, we query the context as early as
     /// possible (i.e., after parsing). See [charon_lib::get_mir].
-    fn after_parsing<'tcx>(&mut self, c: &Compiler, queries: &'tcx Queries<'tcx>) -> Compilation {
+    fn after_crate_root_parsing<'tcx>(
+        &mut self,
+        c: &Compiler,
+        queries: &'tcx Queries<'tcx>,
+    ) -> Compilation {
         // Set up our own `DefId` debug routine.
         rustc_hir::def_id::DEF_ID_DEBUG
             .swap(&(def_id_debug as fn(_, &mut fmt::Formatter<'_>) -> _));

charon/src/export.rs

@@ -89,7 +89,7 @@ impl<FD: Serialize + Clone, GD: Serialize + Clone> GCrateData<FD, GD> {
         };
 
         // Create the file.
-        let std::io::Result::Ok(outfile) = File::create(target_filename.clone()) else {
+        let std::io::Result::Ok(outfile) = File::create(target_filename) else {
             error!("Could not open: {:?}", target_filename);
             return Err(());
         };

charon/src/translate/translate_ctx.rs

@@ -587,7 +587,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
             | Struct
             | Trait
             | TraitAlias
-            | TyAlias
+            | TyAlias { .. }
             | Union
             | Use => Some(self.tcx.visibility(id).is_public()),
             // These kinds don't have visibility modifiers (which would cause `visibility` to panic).

charon/src/translate/translate_functions_to_ullbc.rs

@@ -67,18 +67,16 @@ fn translate_unaryop_kind(binop: hax::UnOp) -> UnOp {
 /// Small utility
 pub(crate) fn check_impl_item(impl_item: &rustc_hir::Impl<'_>) {
     // TODO: make proper error messages
-    use rustc_hir::{Constness, Defaultness, ImplPolarity, Unsafety};
+    use rustc_hir::{Defaultness, ImplPolarity, Unsafety};
     assert!(impl_item.unsafety == Unsafety::Normal);
     // About polarity:
     // [https://doc.rust-lang.org/beta/unstable-book/language-features/negative-impls.html]
     // Not sure about what I should do about it. Should I do anything, actually?
     // This seems useful to enforce some discipline on the user-side, but not
     // necessary for analysis purposes.
     assert!(impl_item.polarity == ImplPolarity::Positive);
-    // Note sure what this is about
+    // Not sure what this is about
     assert!(impl_item.defaultness == Defaultness::Final);
-    // Note sure what this is about
-    assert!(impl_item.constness == Constness::NotConst);
 }
 
 impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
@@ -552,7 +550,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         span: rustc_span::Span,
         rvalue: &hax::Rvalue,
     ) -> Result<Rvalue, Error> {
-        use std::ops::Deref;
         let erase_regions = true;
         match rvalue {
             hax::Rvalue::Use(operand) => Ok(Rvalue::Use(self.translate_operand(span, operand)?)),
@@ -697,15 +694,12 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                     }
                 }
             }
-            hax::Rvalue::BinaryOp(binop, operands) => {
-                let (left, right) = operands.deref();
-                Ok(Rvalue::BinaryOp(
-                    self.t_ctx.translate_binaryop_kind(span, *binop)?,
-                    self.translate_operand(span, left)?,
-                    self.translate_operand(span, right)?,
-                ))
-            }
-            hax::Rvalue::CheckedBinaryOp(binop, operands) => {
+            hax::Rvalue::BinaryOp(binop, (left, right)) => Ok(Rvalue::BinaryOp(
+                self.t_ctx.translate_binaryop_kind(span, *binop)?,
+                self.translate_operand(span, left)?,
+                self.translate_operand(span, right)?,
+            )),
+            hax::Rvalue::CheckedBinaryOp(binop, (left, right)) => {
                 let binop = match binop {
                     hax::BinOp::Add => BinOp::CheckedAdd,
                     hax::BinOp::Sub => BinOp::CheckedSub,
@@ -714,7 +708,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                         error_or_panic!(self, span, "Only Add, Sub and Mul are supported as checked binary operations, found {binop:?}");
                     }
                 };
-                let (left, right) = operands.deref();
                 Ok(Rvalue::BinaryOp(
                     binop,
                     self.translate_operand(span, left)?,
@@ -767,7 +760,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                     .map(|op| self.translate_operand(span, op))
                     .try_collect()?;
 
-                match aggregate_kind.deref() {
+                match aggregate_kind {
                     hax::AggregateKind::Array(ty) => {
                         let t_ty = self.translate_ty(span, erase_regions, ty)?;
                         let cg = ConstGeneric::Value(Literal::Scalar(ScalarValue::Usize(
@@ -1082,12 +1075,9 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         trace!("About to translate statement (MIR) {:?}", statement);
         let span = statement.source_info.span.rust_span_data.unwrap().span();
 
-        use std::ops::Deref;
-
         use hax::StatementKind;
         let t_statement: Option<RawStatement> = match &*statement.kind {
-            StatementKind::Assign(assign) => {
-                let (place, rvalue) = assign.deref();
+            StatementKind::Assign((place, rvalue)) => {
                 let t_place = self.translate_place(span, place)?;
                 let t_rvalue = self.translate_rvalue(
                     statement.source_info.span.rust_span_data.unwrap().span(),
@@ -1096,8 +1086,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
 
                 Some(RawStatement::Assign(t_place, t_rvalue))
             }
-            StatementKind::FakeRead(info) => {
-                let (_read_cause, place) = info.deref();
+            StatementKind::FakeRead((_read_cause, place)) => {
                 let t_place = self.translate_place(span, place)?;
 
                 Some(RawStatement::FakeRead(t_place))
@@ -1203,14 +1192,16 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
 
                 RawTerminator::Switch { discr, targets }
             }
-            TerminatorKind::Resume => {
+            TerminatorKind::UnwindResume => {
                 // This is used to correctly unwind. We shouldn't get there: if
                 // we panic, the state gets stuck.
-                error_or_panic!(self, rustc_span, "Unexpected terminator: resume");
+                error_or_panic!(self, rustc_span, "Unexpected terminator: UnwindResume");
+            }
+            TerminatorKind::UnwindTerminate { .. } => {
+                error_or_panic!(self, rustc_span, "Unexpected terminator: UnwindTerminate")
             }
             TerminatorKind::Return => RawTerminator::Return,
             TerminatorKind::Unreachable => RawTerminator::Unreachable,
-            TerminatorKind::Terminate => unimplemented!(),
             TerminatorKind::Drop {
                 place,
                 target,
@@ -1574,7 +1565,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         let (substs, signature, closure_info): (
             Vec<hax::GenericArg>,
             rustc_middle::ty::Binder<'tcx, rustc_middle::ty::FnSig<'tcx>>,
-            Option<(ClosureKind, Vec<rustc_middle::ty::Ty<'tcx>>)>,
+            Option<(ClosureKind, &ty::List<rustc_middle::ty::Ty<'tcx>>)>,
         ) = if is_closure {
             // Closures have a peculiar handling in Rust: we can't call
             // `TyCtxt::fn_sig`.
@@ -1604,8 +1595,8 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 rustc_middle::ty::ClosureKind::FnOnce => ClosureKind::FnOnce,
             };
 
-            // Retrieve the type of the captured stated
-            let state: Vec<rustc_middle::ty::Ty<'tcx>> = closure.upvar_tys().collect();
+            // Retrieve the type of the captured state
+            let state: &ty::List<rustc_middle::ty::Ty<'tcx>> = closure.upvar_tys();
 
             let substs = substs.sinto(&self.hax_state);
 

charon/src/translate/translate_traits.rs

@@ -166,8 +166,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         // the parent and item predicates.
         let trait_pred = rustc_middle::ty::TraitPredicate {
             trait_ref,
-            // Not really necessary (dummy value)
-            constness: rustc_middle::ty::BoundConstness::NotConst,
             // Not really necessary
             polarity: rustc_middle::ty::ImplPolarity::Positive,
         };

charon/tests/cargo/dependencies.out

@@ -75,18 +75,17 @@ fn test_cargo_dependencies::main()
     let left_val@10: &'_ (u32); // local
     let right_val@11: &'_ (u32); // local
     let @12: bool; // anonymous local
-    let @13: bool; // anonymous local
+    let @13: u32; // anonymous local
     let @14: u32; // anonymous local
-    let @15: u32; // anonymous local
-    let kind@16: core::panicking::AssertKind; // local
-    let @17: core::panicking::AssertKind; // anonymous local
+    let kind@15: core::panicking::AssertKind; // local
+    let @16: core::panicking::AssertKind; // anonymous local
+    let @17: &'_ (u32); // anonymous local
     let @18: &'_ (u32); // anonymous local
     let @19: &'_ (u32); // anonymous local
     let @20: &'_ (u32); // anonymous local
-    let @21: &'_ (u32); // anonymous local
-    let @22: core::option::Option<core::fmt::Arguments<'_>>; // anonymous local
+    let @21: core::option::Option<core::fmt::Arguments<'_>>; // anonymous local
+    let @22: (); // anonymous local
     let @23: (); // anonymous local
-    let @24: (); // anonymous local
 
     x@1 := const (0 : u32)
     @fake_read(x@1)
@@ -105,40 +104,40 @@ fn test_cargo_dependencies::main()
     @fake_read(@6)
     left_val@10 := copy ((@6).0)
     right_val@11 := copy ((@6).1)
-    @14 := copy (*(left_val@10))
-    @15 := copy (*(right_val@11))
-    @13 := move (@14) == move (@15)
-    drop @15
-    drop @14
-    @12 := ~(move (@13))
-    drop @13
+    @13 := copy (*(left_val@10))
+    @14 := copy (*(right_val@11))
+    @12 := move (@13) == move (@14)
     if move (@12) {
         nop
     }
     else {
-        @23 := ()
-        @5 := move (@23)
-        drop @12
-        drop right_val@11
-        drop left_val@10
-        drop @9
-        drop @6
-        drop @5
-        @24 := ()
-        @0 := move (@24)
-        drop x@1
-        @0 := ()
-        return
+        drop @14
+        drop @13
+        kind@15 := core::panicking::AssertKind::Eq {  }
+        @fake_read(kind@15)
+        @16 := move (kind@15)
+        @18 := &*(left_val@10)
+        @17 := &*(@18)
+        @20 := &*(right_val@11)
+        @19 := &*(@20)
+        @21 := core::option::Option::None {  }
+        panic
     }
-    kind@16 := core::panicking::AssertKind::Eq {  }
-    @fake_read(kind@16)
-    @17 := move (kind@16)
-    @19 := &*(left_val@10)
-    @18 := &*(@19)
-    @21 := &*(right_val@11)
-    @20 := &*(@21)
-    @22 := core::option::Option::None {  }
-    panic
+    drop @14
+    drop @13
+    @22 := ()
+    @5 := move (@22)
+    drop @12
+    drop right_val@11
+    drop left_val@10
+    drop @9
+    drop @6
+    drop @5
+    @23 := ()
+    @0 := move (@23)
+    drop x@1
+    @0 := ()
+    return
 }
 
 fn core::ops::function::FnOnce::call_once<Self, Args>(@1: Self, @2: Args) -> Self::Output