Update Charon submodule (#3823)

Update Charon submodule to df3b7fd4c1277827c92b4a2cb84347f1f54d92a6 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Zyad Hassan <[email protected]>
model-checking · Jan 14, 2025 · 441cde0 · 441cde0
1 parent 5efd8b6
commit 441cde0
Show file tree

Hide file tree

Showing 4 changed files with 98 additions and 59 deletions.
diff --git a/Cargo.lock b/Cargo.lock
@@ -244,7 +244,7 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
 
 [[package]]
 name = "charon"
-version = "0.1.58"
+version = "0.1.62"
 dependencies = [
  "annotate-snippets",
  "anstream",

diff --git a/charon b/charon
diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs
@@ -12,10 +12,12 @@ use crate::kani_middle::provide;
 use crate::kani_middle::reachability::{collect_reachable_items, filter_crate_items};
 use crate::kani_middle::transform::{BodyTransformation, GlobalPasses};
 use crate::kani_queries::QueryDb;
-use charon_lib::ast::{AnyTransId, TranslatedCrate};
+use charon_lib::ast::{AnyTransId, TranslatedCrate, meta::ItemOpacity::*, meta::Span};
 use charon_lib::errors::ErrorCtx;
+use charon_lib::errors::error_or_panic;
+use charon_lib::name_matcher::NamePattern;
 use charon_lib::transform::TransformCtx;
-use charon_lib::transform::ctx::TransformOptions;
+use charon_lib::transform::ctx::{TransformOptions, TransformPass};
 use kani_metadata::ArtifactType;
 use kani_metadata::{AssignsContract, CompilerArtifactStub};
 use rustc_codegen_ssa::back::archive::{
@@ -133,8 +135,8 @@ impl LlbcCodegenBackend {
         // - compute the order in which to extract the definitions
         // - find the recursive definitions
         // - group the mutually recursive definitions
-        let reordered_decls = charon_lib::reorder_decls::compute_reordered_decls(&ccx);
-        ccx.translated.ordered_decls = Some(reordered_decls);
+        let reordered_decls = charon_lib::transform::reorder_decls::Transform {};
+        reordered_decls.transform_ctx(&mut ccx);
 
         //
         // =================
@@ -151,10 +153,6 @@ impl LlbcCodegenBackend {
 
         // # Go from ULLBC to LLBC (Low-Level Borrow Calculus) by reconstructing
         // the control flow.
-        charon_lib::ullbc_to_llbc::translate_functions(&mut ccx);
-
-        trace!("# LLBC resulting from control-flow reconstruction:\n\n{}\n", ccx);
-
         // Run the micro-passes that clean up bodies.
         for pass in charon_lib::transform::LLBC_PASSES.iter() {
             pass.run(&mut ccx)
@@ -385,17 +383,61 @@ where
     ret
 }
 
-fn create_charon_transformation_context(tcx: TyCtxt) -> TransformCtx {
-    let options = TransformOptions {
+fn get_transform_options(tcx: &TranslatedCrate, error_ctx: &mut ErrorCtx) -> TransformOptions {
+    let mut parse_pattern = |s: &str| match NamePattern::parse(s) {
+        Ok(p) => Ok(p),
+        Err(e) => {
+            let msg = format!("failed to parse pattern `{s}` ({e})");
+            error_or_panic!(error_ctx, &TranslatedCrate::default(), Span::dummy(), msg)
+        }
+    };
+    let options = tcx.options.clone();
+    let item_opacities = {
+        let mut opacities = vec![];
+
+        // This is how to treat items that don't match any other pattern.
+        if options.extract_opaque_bodies {
+            opacities.push(("_".to_string(), Transparent));
+        } else {
+            opacities.push(("_".to_string(), Foreign));
+        }
+
+        // We always include the items from the crate.
+        opacities.push(("crate".to_owned(), Transparent));
+
+        for pat in options.include.iter() {
+            opacities.push((pat.to_string(), Transparent));
+        }
+        for pat in options.opaque.iter() {
+            opacities.push((pat.to_string(), Opaque));
+        }
+        for pat in options.exclude.iter() {
+            opacities.push((pat.to_string(), Invisible));
+        }
+
+        // We always hide this trait.
+        opacities.push(("core::alloc::Allocator".to_string(), Invisible));
+        opacities
+            .push(("alloc::alloc::{{impl core::alloc::Allocator for _}}".to_string(), Invisible));
+
+        opacities
+            .into_iter()
+            .filter_map(|(s, opacity)| parse_pattern(&s).ok().map(|pat| (pat, opacity)))
+            .collect()
+    };
+    TransformOptions {
         no_code_duplication: false,
         hide_marker_traits: true,
         no_merge_goto_chains: false,
-        item_opacities: Vec::new(),
-    };
+        item_opacities,
+        print_built_llbc: true,
+    }
+}
+
+fn create_charon_transformation_context(tcx: TyCtxt) -> TransformCtx {
     let crate_name = tcx.crate_name(LOCAL_CRATE).as_str().into();
-    let mut translated = TranslatedCrate { crate_name, ..TranslatedCrate::default() };
-    //This option setting is for Aeneas compatibility
-    translated.options.hide_marker_traits = true;
-    let errors = ErrorCtx::new(true, false);
+    let translated = TranslatedCrate { crate_name, ..TranslatedCrate::default() };
+    let mut errors = ErrorCtx::new(true, false);
+    let options = get_transform_options(&translated, &mut errors);
     TransformCtx { options, translated, errors }
 }
diff --git a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs
@@ -14,23 +14,23 @@ use charon_lib::ast::types::{Ty as CharonTy, TyKind as CharonTyKind};
 use charon_lib::ast::{
     AbortKind as CharonAbortKind, AggregateKind as CharonAggregateKind,
     AnyTransId as CharonAnyTransId, Assert as CharonAssert, BinOp as CharonBinOp,
-    Body as CharonBody, BodyId as CharonBodyId, BorrowKind as CharonBorrowKind,
-    BuiltinTy as CharonBuiltinTy, Call as CharonCall, CastKind as CharonCastKind,
-    ConstGeneric as CharonConstGeneric, ConstGenericVar as CharonConstGenericVar,
-    ConstGenericVarId as CharonConstGenericVarId, ConstantExpr as CharonConstantExpr,
-    DeBruijnId as CharonDeBruijnId, DeBruijnVar as CharonDeBruijnVar,
-    Disambiguator as CharonDisambiguator, ExistentialPredicate as CharonExistentialPredicate,
-    Field as CharonField, FieldId as CharonFieldId, FieldProjKind as CharonFieldProjKind,
-    File as CharonFile, FileId as CharonFileId, FileName as CharonFileName,
-    FnOperand as CharonFnOperand, FnPtr as CharonFnPtr, FunDecl as CharonFunDecl,
-    FunDeclId as CharonFunDeclId, FunId as CharonFunId,
-    FunIdOrTraitMethodRef as CharonFunIdOrTraitMethodRef, FunSig as CharonFunSig,
-    GenericArgs as CharonGenericArgs, GenericParams as CharonGenericParams,
-    GlobalDeclId as CharonGlobalDeclId, GlobalDeclRef as CharonGlobalDeclRef,
-    IntegerTy as CharonIntegerTy, ItemKind as CharonItemKind, ItemMeta as CharonItemMeta,
-    ItemOpacity as CharonItemOpacity, Literal as CharonLiteral, LiteralTy as CharonLiteralTy,
-    Locals as CharonLocals, Name as CharonName, Opaque as CharonOpaque, Operand as CharonOperand,
-    PathElem as CharonPathElem, Place as CharonPlace, PolyTraitDeclRef as CharonPolyTraitDeclRef,
+    Body as CharonBody, BorrowKind as CharonBorrowKind, BuiltinTy as CharonBuiltinTy,
+    Call as CharonCall, CastKind as CharonCastKind, ConstGeneric as CharonConstGeneric,
+    ConstGenericVar as CharonConstGenericVar, ConstGenericVarId as CharonConstGenericVarId,
+    ConstantExpr as CharonConstantExpr, DeBruijnId as CharonDeBruijnId,
+    DeBruijnVar as CharonDeBruijnVar, Disambiguator as CharonDisambiguator,
+    ExistentialPredicate as CharonExistentialPredicate, Field as CharonField,
+    FieldId as CharonFieldId, FieldProjKind as CharonFieldProjKind, File as CharonFile,
+    FileId as CharonFileId, FileName as CharonFileName, FnOperand as CharonFnOperand,
+    FnPtr as CharonFnPtr, FunDecl as CharonFunDecl, FunDeclId as CharonFunDeclId,
+    FunId as CharonFunId, FunIdOrTraitMethodRef as CharonFunIdOrTraitMethodRef,
+    FunSig as CharonFunSig, GenericArgs as CharonGenericArgs, GenericParams as CharonGenericParams,
+    GenericsSource as CharonGenericsSource, GlobalDeclId as CharonGlobalDeclId,
+    GlobalDeclRef as CharonGlobalDeclRef, IntegerTy as CharonIntegerTy, ItemKind as CharonItemKind,
+    ItemMeta as CharonItemMeta, ItemOpacity as CharonItemOpacity, Literal as CharonLiteral,
+    LiteralTy as CharonLiteralTy, Locals as CharonLocals, Name as CharonName,
+    Opaque as CharonOpaque, Operand as CharonOperand, PathElem as CharonPathElem,
+    Place as CharonPlace, PolyTraitDeclRef as CharonPolyTraitDeclRef,
     PredicateOrigin as CharonPredicateOrigin, ProjectionElem as CharonProjectionElem,
     RawConstantExpr as CharonRawConstantExpr, RefKind as CharonRefKind, Region as CharonRegion,
     RegionBinder as CharonRegionBinder, RegionId as CharonRegionId, RegionVar as CharonRegionVar,
@@ -180,7 +180,8 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                 continue;
             };
             let c_traitdecl_id = self.translate_traitdecl(trait_def);
-            let c_genarg = self.translate_generic_args_without_trait(trait_ref.args().clone());
+            let c_genarg = self
+                .translate_generic_args_without_trait(trait_ref.args().clone(), trait_def.def_id());
             let c_polytrait = CharonPolyTraitDeclRef {
                 regions: CharonVector::new(),
                 skip_binder: CharonTraitDeclRef {
@@ -221,7 +222,8 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                 continue;
             };
             let c_traitdecl_id = self.translate_traitdecl(trait_def);
-            let c_genarg = self.translate_generic_args_without_trait(trait_ref.args().clone());
+            let c_genarg = self
+                .translate_generic_args_without_trait(trait_ref.args().clone(), trait_def.def_id());
             let c_polytrait = CharonPolyTraitDeclRef {
                 regions: CharonVector::new(),
                 skip_binder: CharonTraitDeclRef { trait_id: c_traitdecl_id, generics: c_genarg },
@@ -1167,19 +1169,14 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         }
     }
 
-    fn translate_function_body(
-        &mut self,
-        instance: Instance,
-    ) -> Result<CharonBodyId, CharonOpaque> {
+    fn translate_function_body(&mut self, instance: Instance) -> Result<CharonBody, CharonOpaque> {
         let fndef = match instance.ty().kind() {
             TyKind::RigidTy(RigidTy::FnDef(fndef, _)) => fndef,
             _ => panic!("Expected a function type"),
         };
         let mir_body = fndef.body().unwrap();
-        let body_id = self.translated.bodies.reserve_slot();
         let body = self.translate_body(mir_body);
-        self.translated.bodies.set_slot(body_id, body);
-        Ok(body_id)
+        Ok(body)
     }
 
     fn translate_body(&mut self, mir_body: Body) -> CharonBody {
@@ -1195,6 +1192,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
     }
 
     fn translate_generic_args(&mut self, ga: GenericArgs, defid: DefId) -> CharonGenericArgs {
+        let target = CharonGenericsSource::Item(*self.id_map.get(&defid).unwrap());
         let genvec = ga.0;
         let mut c_regions: CharonVector<CharonRegionId, CharonRegion> = CharonVector::new();
         let mut c_types: CharonVector<CharonTypeVarId, CharonTy> = CharonVector::new();
@@ -1244,6 +1242,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                 types: t_types,
                 const_generics: t_const_generics,
                 trait_refs: trait_ref.trait_decl_ref.skip_binder.generics.trait_refs.clone(),
+                target: target.clone(),
             };
             let traitdecl_id = trait_ref.trait_decl_ref.skip_binder.trait_id;
             let subs_traitdeclref = CharonPolyTraitDeclRef {
@@ -1264,10 +1263,16 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             types: c_types,
             const_generics: c_const_generics,
             trait_refs,
+            target,
         }
     }
 
-    fn translate_generic_args_without_trait(&mut self, ga: GenericArgs) -> CharonGenericArgs {
+    fn translate_generic_args_without_trait(
+        &mut self,
+        ga: GenericArgs,
+        defid: DefId,
+    ) -> CharonGenericArgs {
+        let target = CharonGenericsSource::Item(*self.id_map.get(&defid).unwrap());
         let genvec = ga.0;
         let mut c_regions: CharonVector<CharonRegionId, CharonRegion> = CharonVector::new();
         let mut c_types: CharonVector<CharonTypeVarId, CharonTy> = CharonVector::new();
@@ -1295,6 +1300,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             types: c_types,
             const_generics: c_const_generics,
             trait_refs: CharonVector::new(),
+            target,
         }
     }
 
@@ -1345,12 +1351,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                 CharonTypeId::Builtin(CharonBuiltinTy::Str),
                 // TODO: find out whether any of the information below should be
                 // populated for strings
-                CharonGenericArgs {
-                    regions: CharonVector::new(),
-                    types: CharonVector::new(),
-                    const_generics: CharonVector::new(),
-                    trait_refs: CharonVector::new(),
-                },
+                CharonGenericArgs::empty(CharonGenericsSource::Builtin),
             )),
             RigidTy::Array(ty, tyconst) => {
                 let c_ty = self.translate_ty(ty);
@@ -1366,6 +1367,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                         types: c_types,
                         const_generics: c_const_generics,
                         trait_refs: CharonVector::new(),
+                        target: CharonGenericsSource::Builtin,
                     },
                 ))
             }
@@ -1380,12 +1382,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             RigidTy::Tuple(ty) => {
                 let types = ty.iter().map(|ty| self.translate_ty(*ty)).collect();
                 // TODO: find out if any of the information below is needed
-                let generic_args = CharonGenericArgs {
-                    regions: CharonVector::new(),
-                    types,
-                    const_generics: CharonVector::new(),
-                    trait_refs: CharonVector::new(),
-                };
+                let generic_args = CharonGenericArgs::new_for_builtin(types);
                 CharonTy::new(CharonTyKind::Adt(CharonTypeId::Tuple, generic_args))
             }
             RigidTy::FnDef(def_id, _args) => {
@@ -1414,7 +1411,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                 c_types.push(c_ty);
                 CharonTy::new(CharonTyKind::Adt(
                     CharonTypeId::Builtin(CharonBuiltinTy::Slice),
-                    CharonGenericArgs::new_from_types(c_types),
+                    CharonGenericArgs::new_for_builtin(c_types),
                 ))
             }
             RigidTy::RawPtr(ty, mutability) => {
@@ -1672,7 +1669,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                             CharonTypeId::Tuple,
                             None,
                             None,
-                            CharonGenericArgs::empty(),
+                            CharonGenericArgs::empty(CharonGenericsSource::Builtin),
                         ),
                         c_operands,
                     ),