Incorporate charon changes to the frontend

CHANGELOG.md

@@ -15,6 +15,8 @@ Changes to the Rust Engine:
    lift monadic computations into values) (#1746)
 
 Changes to the frontend:
+ - Update the pin of rustc (#1765)
+ - Miscellaneous changes related to Charon (#1765)
 
 Change to cargo-hax:
 

cli/driver/src/exporter.rs

@@ -72,9 +72,10 @@ impl From<ExtractionCallbacks> for hax_frontend_exporter_options::Options {
         hax_frontend_exporter_options::Options {
             inline_anon_consts: true,
             bounds_options: hax_frontend_exporter_options::BoundsOptions {
-                resolve_drop: false,
+                resolve_destruct: false,
                 prune_sized: true,
             },
+            item_ref_use_concrete_impl: false,
         }
     }
 }

engine/backends/fstar/fstar_backend.ml

@@ -587,6 +587,12 @@ struct
           ]
         in
         F.term @@ F.AST.QExists (binders, ([], []), phi)
+    | App
+        {
+          f = { e = GlobalVar (`Projector (`TupleField (_, 1))) };
+          args = [ arg ];
+        } ->
+        pexpr arg
     | App
         {
           f = { e = GlobalVar (`Projector (`TupleField (n, len))) };

engine/lib/concrete_ident/thir_simple_types.ml

@@ -58,22 +58,29 @@ let to_string ~(namespace : View.ModPath.t) :
     | Uint U128 -> Some "u128"
     | Float F32 -> Some "f32"
     | Float F64 -> Some "f64"
-    | Tuple [] -> Some "unit"
+    | Tuple { value = { generic_args = []; _ }; _ } -> Some "unit"
     | Adt { value = { def_id; generic_args = []; _ }; _ } ->
         Option.map ~f:escape (adt def_id)
     | _ -> None
   in
   let apply left right = left ^ "_of_" ^ right in
   let rec arity1 (ty : Types.node_for__ty_kind) =
     match ty.value with
-    | Slice sub -> arity1 sub |> Option.map ~f:(apply "slice")
+    | Slice { value = { generic_args = [ Type sub ]; _ }; _ } ->
+        arity1 sub |> Option.map ~f:(apply "slice")
     | Ref (_, sub, _) -> arity1 sub |> Option.map ~f:(apply "ref")
     | Adt { value = { def_id; generic_args = [ Type arg ]; _ }; _ } ->
         let* adt = adt def_id in
         let* arg = arity1 arg in
         Some (apply adt arg)
-    | Tuple l ->
-        let* l = List.map ~f:arity0 l |> Option.all in
+    | Tuple { value = { generic_args; _ }; _ } ->
+        let* l =
+          List.map
+            ~f:(fun (arg : Types.generic_arg) ->
+              match arg with Type ty -> arity0 ty | _ -> None)
+            generic_args
+          |> Option.all
+        in
         Some ("tuple_" ^ String.concat ~sep:"_" l)
     | _ -> arity0 ty
   in

engine/lib/import_thir.ml

@@ -100,8 +100,8 @@ let c_borrow_kind span : Thir.borrow_kind -> borrow_kind = function
 
 let c_binding_mode : Thir.by_ref -> binding_mode = function
   | No -> ByValue
-  | Yes true -> ByRef (Mut W.mutable_reference, W.reference)
-  | Yes false -> ByRef (Shared, W.reference)
+  | Yes (_, true) -> ByRef (Mut W.mutable_reference, W.reference)
+  | Yes (_, false) -> ByRef (Shared, W.reference)
 
 let unit_typ : ty = TApp { ident = `TupleType 0; args = [] }
 
@@ -663,11 +663,14 @@ end) : EXPR = struct
             }
       | TupleField { lhs; field } ->
           (* TODO: refactor *)
+          let lhs = c_expr lhs in
           let tuple_len =
-            0
-            (* todo, lookup type *)
+            match lhs.typ with
+            | TApp { ident = `TupleType len; _ } -> len
+            | _ ->
+                assertion_failure [ e.span ]
+                  "LHS of tuple field projection is not typed as a tuple."
           in
-          let lhs = c_expr lhs in
           let projector =
             GlobalVar
               (`Projector (`TupleField (Int.of_string field, tuple_len)))
@@ -906,7 +909,7 @@ end) : EXPR = struct
             "constant_lit_to_lit: TraitConst | FnPtr | RawBorrow | Cast | \
              Memory"
       | Todo _ -> assertion_failure [ span ] "ConstantExpr::Todo"
-    and constant_lit_to_lit (l : Thir.constant_literal) _span :
+    and constant_lit_to_lit (l : Thir.constant_literal) span :
         Thir.lit_kind * bool =
       match l with
       | Bool v -> (Bool v, false)
@@ -922,6 +925,8 @@ end) : EXPR = struct
           | None -> (Float (v, Suffixed ty), false))
       | Str v -> (Str (v, Cooked), false)
       | ByteStr v -> (ByteStr (v, Cooked), false)
+      | PtrNoProvenance _ ->
+          assertion_failure [ span ] "constant_lit_to_lit: PtrNoProvenance"
     and constant_field_expr ({ field; value } : Thir.constant_field_expr) :
         Thir.field_expr =
       { field; value = constant_expr_to_expr value }
@@ -1080,9 +1085,25 @@ end) : EXPR = struct
         TApp { ident; args }
     | Foreign _ -> unimplemented ~issue_id:928 [ span ] "Foreign"
     | Str -> TStr
-    | Array (ty, len) ->
+    | Array item_ref ->
+        let ty, len =
+          match item_ref.value.generic_args with
+          | [ Type ty; Const len ] -> (ty, len)
+          | _ ->
+              assertion_failure [ span ]
+                "Wrong generics for array: expected a type and a constant. See \
+                 synthetic_items in hax frontend."
+        in
         TArray { typ = c_ty span ty; length = c_constant_expr len }
-    | Slice ty ->
+    | Slice item_ref ->
+        let ty =
+          match item_ref.value.generic_args with
+          | [ Type ty ] -> ty
+          | _ ->
+              assertion_failure [ span ]
+                "Wrong generics for slice: expected a type. See \
+                 synthetic_items in hax frontend."
+        in
         let ty = c_ty span ty in
         TSlice { ty; witness = W.slice }
     | RawPtr _ -> TRawPointer { witness = W.raw_pointer }
@@ -1091,7 +1112,17 @@ end) : EXPR = struct
         let mut = c_mutability W.mutable_reference mut in
         TRef { witness = W.reference; region = "todo"; typ; mut }
     | Never -> U.never_typ
-    | Tuple types ->
+    | Tuple item_ref ->
+        let types =
+          List.map
+            ~f:(function Types.Type ty -> Some ty | _ -> None)
+            item_ref.value.generic_args
+          |> Option.all
+          |> Option.value_or_thunk ~default:(fun _ ->
+                 assertion_failure [ span ]
+                   "Wrong generics for slice: expected a type. See \
+                    synthetic_items in hax frontend.")
+        in
         let types = List.map ~f:(fun ty -> GType (c_ty span ty)) types in
         TApp { ident = `TupleType (List.length types); args = types }
     | Alias { kind = Projection { assoc_item = _; impl_expr }; def_id; _ } ->

engine/names/extract/build.rs

@@ -73,6 +73,8 @@ fn def_path_item_to_str(path_item: DefPathItem) -> String {
         DefPathItem::AnonAssocTy(..) => "AnonAssocTy".into(),
         DefPathItem::SyntheticCoroutineBody => "SyntheticCoroutineBody".into(),
         DefPathItem::NestedStatic => "NestedStatic".into(),
+        DefPathItem::LateAnonConst => "LateAnonConst".into(),
+        DefPathItem::DesugaredAnonymousLifetime => "DesugaredAnonymousLifetime".into(),
     }
 }
 
@@ -130,6 +132,11 @@ fn is_macro(did: &DefId) -> bool {
     matches!(last.data, DefPathItem::MacroNs { .. })
 }
 
+/// Checks wether a def id refers to a syntactic item (see `syntactic_item.rs` in hax' exporter)
+fn is_synthetic(did: &DefId) -> bool {
+    &did.contents.value.krate == hax_frontend_exporter_def_id::SYNTHETIC_CRATE_NAME
+}
+
 fn reader_to_str(s: String) -> String {
     let json: Value = match serde_json::from_str(&s) {
         Ok(v) => v,
@@ -141,6 +148,7 @@ fn reader_to_str(s: String) -> String {
     let def_ids = def_ids
         .into_iter()
         .filter(|did| !is_macro(did))
+        .filter(|did| !is_synthetic(did))
         .map(|did| {
             let (json, krate_name) = def_id_to_str(&did);
             (serde_json::to_string(&json).unwrap(), krate_name)

frontend/exporter/options/src/lib.rs

@@ -103,13 +103,15 @@ pub struct Options {
     pub inline_anon_consts: bool,
     /// Options related to bounds.
     pub bounds_options: BoundsOptions,
+    /// Resolve definition identifiers to their concrete impl counterpart when possible in `ItemRef::translate`.
+    pub item_ref_use_concrete_impl: bool,
 }
 
 #[derive(Debug, Clone, Copy)]
 pub struct BoundsOptions {
-    /// Add `T: Drop` bounds to every type generic, so that we can build `ImplExpr`s to know what
-    /// code is run on drop.
-    pub resolve_drop: bool,
+    /// Add `T: Destruct` bounds to every type generic, so that we can build `ImplExpr`s to know
+    /// what code is run on drop.
+    pub resolve_destruct: bool,
     /// Prune `T: Sized` and `T: MetaSized` predicates.
     pub prune_sized: bool,
 }

frontend/exporter/src/constant_utils.rs

@@ -24,6 +24,7 @@ pub enum ConstantLiteral {
     Char(char),
     Float(String, FloatTy),
     Int(ConstantInt),
+    PtrNoProvenance(u128),
     Str(String),
     ByteStr(Vec<u8>),
 }
@@ -146,6 +147,7 @@ impl From<ConstantExpr> for Expr {
                         }
                     }
                     Float(f, ty) => LitKind::Float(f, LitFloatType::Suffixed(ty)),
+                    PtrNoProvenance(p) => LitKind::Int(p, LitIntType::Unsigned(UintTy::Usize)),
                     ByteStr(raw) => LitKind::ByteStr(raw, StrStyle::Cooked),
                     Str(raw) => LitKind::Str(raw, StrStyle::Cooked),
                 };

frontend/exporter/src/constant_utils/uneval.rs

@@ -111,8 +111,10 @@ pub fn translate_constant_reference<'tcx>(
         .try_normalize_erasing_regions(typing_env, ty)
         .unwrap_or(ty);
     let kind = if let Some(assoc) = s.base().tcx.opt_associated_item(ucv.def)
-        && (assoc.trait_item_def_id.is_some() || assoc.container == ty::AssocItemContainer::Trait)
-    {
+        && matches!(
+            assoc.container,
+            ty::AssocContainer::Trait | ty::AssocContainer::TraitImpl(..)
+        ) {
         // This is an associated constant in a trait.
         let name = assoc.name().to_string();
         let impl_expr = self_clause_for_item(s, ucv.def, ucv.args).unwrap();
@@ -128,11 +130,22 @@ pub fn translate_constant_reference<'tcx>(
 /// Evaluate a `ty::Const`.
 pub fn eval_ty_constant<'tcx, S: UnderOwnerState<'tcx>>(
     s: &S,
-    c: ty::Const<'tcx>,
+    uv: rustc_middle::ty::UnevaluatedConst<'tcx>,
 ) -> Option<ty::Const<'tcx>> {
+    use ty::TypeVisitableExt;
     let tcx = s.base().tcx;
-    let evaluated = tcx.try_normalize_erasing_regions(s.typing_env(), c).ok()?;
-    (evaluated != c).then_some(evaluated)
+    let typing_env = s.typing_env();
+    if uv.has_non_region_param() {
+        return None;
+    }
+    let span = tcx.def_span(uv.def);
+    let erased_uv = tcx.erase_and_anonymize_regions(uv);
+    let val = tcx
+        .const_eval_resolve_for_typeck(typing_env, erased_uv, span)
+        .ok()?
+        .ok()?;
+    let ty = tcx.type_of(uv.def).instantiate(tcx, uv.args);
+    Some(ty::Const::new_value(tcx, val, ty))
 }
 
 /// Evaluate a `mir::Const`.
@@ -164,7 +177,7 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ConstantExpr> for ty::Const<'tcx>
 
             ty::ConstKind::Unevaluated(ucv) => match translate_constant_reference(s, span, ucv) {
                 Some(val) => val,
-                None => match eval_ty_constant(s, *self) {
+                None => match eval_ty_constant(s, ucv) {
                     Some(val) => val.sinto(s),
                     // TODO: This is triggered when compiling using `generic_const_exprs`
                     None => supposely_unreachable_fatal!(s, "TranslateUneval"; {self, ucv}),
@@ -183,6 +196,13 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ConstantExpr> for ty::Const<'tcx>
     }
 }
 
+impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, ConstantExpr> for ty::Value<'tcx> {
+    #[tracing::instrument(level = "trace", skip(s))]
+    fn sinto(&self, s: &S) -> ConstantExpr {
+        valtree_to_constant_expr(s, self.valtree, self.ty, rustc_span::DUMMY_SP)
+    }
+}
+
 #[tracing::instrument(level = "trace", skip(s))]
 pub(crate) fn valtree_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>(
     s: &S,
@@ -369,15 +389,24 @@ fn op_to_const<'tcx, S: UnderOwnerState<'tcx>>(
             ConstantExprKind::FnPtr(item)
         }
         ty::RawPtr(..) | ty::Ref(..) => {
-            let op = ecx.deref_pointer(&op)?;
-            let val = op_to_const(s, span, ecx, op.into())?;
-            match ty.kind() {
-                ty::Ref(..) => ConstantExprKind::Borrow(val),
-                ty::RawPtr(.., mutability) => ConstantExprKind::RawBorrow {
-                    arg: val,
-                    mutability: mutability.sinto(s),
-                },
-                _ => unreachable!(),
+            if let Some(op) = ecx.deref_pointer(&op).discard_err() {
+                // Valid pointer case
+                let val = op_to_const(s, span, ecx, op.into())?;
+                match ty.kind() {
+                    ty::Ref(..) => ConstantExprKind::Borrow(val),
+                    ty::RawPtr(.., mutability) => ConstantExprKind::RawBorrow {
+                        arg: val,
+                        mutability: mutability.sinto(s),
+                    },
+                    _ => unreachable!(),
+                }
+            } else {
+                // Invalid pointer; try reading it as a raw address
+                let scalar = ecx.read_scalar(&op)?;
+                let scalar_int = scalar.try_to_scalar_int().unwrap();
+                let v = scalar_int.to_uint(scalar_int.size());
+                let lit = ConstantLiteral::PtrNoProvenance(v);
+                ConstantExprKind::Literal(lit)
             }
         }
         ty::FnPtr(..)
@@ -402,7 +431,7 @@ fn op_to_const<'tcx, S: UnderOwnerState<'tcx>>(
 pub fn const_value_to_constant_expr<'tcx, S: UnderOwnerState<'tcx>>(
     s: &S,
     ty: rustc_middle::ty::Ty<'tcx>,
-    val: mir::ConstValue<'tcx>,
+    val: mir::ConstValue,
     span: rustc_span::Span,
 ) -> InterpResult<'tcx, ConstantExpr> {
     let tcx = s.base().tcx;

frontend/exporter/src/lib.rs

@@ -23,7 +23,6 @@ cfg_feature_rustc! {
     extern crate rustc_abi;
     extern crate rustc_ast;
     extern crate rustc_ast_pretty;
-    extern crate rustc_attr_data_structures;
     extern crate rustc_apfloat;
     extern crate rustc_const_eval;
     extern crate rustc_data_structures;