diff --git a/Cargo.lock b/Cargo.lock index 82abb43fd069..defc75960dcf 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -63,8 +63,7 @@ dependencies = [ [[package]] name = "annotate-snippets" version = "0.11.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "710e8eae58854cdc1790fcb56cca04d712a17be849eeb81da2a724bf4bae2bc4" +source = "git+https://github.com/rust-lang/annotate-snippets-rs#d6c6bbde10b3c08f72317dd9607a98183d467f6d" dependencies = [ "anstyle", "unicode-width", @@ -295,7 +294,7 @@ checksum = "9555578bc9e57714c812a1f84e4fc5b4d21fcb063490c624de019f7464c91268" [[package]] name = "charon" -version = "0.1.62" +version = "0.1.122" dependencies = [ "annotate-snippets", "anstream", @@ -305,9 +304,10 @@ dependencies = [ "colored", "convert_case", "derive_generic_visitor", + "either", "env_logger", - "hashlink", "index_vec", + "indexmap", "indoc", "itertools 0.13.0", "lazy_static", @@ -315,6 +315,8 @@ dependencies = [ "macros", "nom", "nom-supreme", + "num-bigint", + "num-rational", "petgraph 0.6.5", "rustc_version", "serde", @@ -322,6 +324,7 @@ dependencies = [ "serde_json", "serde_stacker", "stacker", + "strip-ansi-escapes", "take_mut", "toml", "tracing", @@ -794,15 +797,6 @@ dependencies = [ "petgraph 0.8.2", ] -[[package]] -name = "hashbrown" -version = "0.14.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e5274423e17b7c9fc20b6e7e208532f9b19825d82dfd615708b70edd83df41f1" -dependencies = [ - "ahash", -] - [[package]] name = "hashbrown" version = "0.15.4" @@ -814,16 +808,6 @@ dependencies = [ "foldhash", ] -[[package]] -name = "hashlink" -version = "0.9.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6ba4ff7128dee98c7dc9794b6a411377e1404dba1c97deb8d1a55297bd25d8af" -dependencies = [ - "hashbrown 0.14.5", - "serde", -] - [[package]] name = "heck" version = "0.5.0" @@ -998,7 +982,8 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "fe4cd85333e22411419a0bcae1297d25e58c9443848b11dc6a86fefe8c78a661" dependencies = [ "equivalent", - "hashbrown 0.15.4", + "hashbrown", + "serde", ] [[package]] @@ -1543,7 +1528,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "54acf3a685220b533e437e264e4d932cfbdc4cc7ec0cd232ed73c08d03b8a7ca" dependencies = [ "fixedbitset 0.5.7", - "hashbrown 0.15.4", + "hashbrown", "indexmap", "serde", ] @@ -2028,10 +2013,19 @@ version = "0.19.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "23de088478b31c349c9ba67816fa55d9355232d63c3afea8bf513e31f0f1d2c0" dependencies = [ - "hashbrown 0.15.4", + "hashbrown", "serde", ] +[[package]] +name = "strip-ansi-escapes" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2a8f8038e7e7969abb3f1b7c2a811225e9296da208539e0f79c5251d6cac0025" +dependencies = [ + "vte", +] + [[package]] name = "strsim" version = "0.11.1" @@ -2462,6 +2456,15 @@ version = "0.9.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" +[[package]] +name = "vte" +version = "0.14.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "231fdcd7ef3037e8330d8e17e61011a2c244126acc0a982f4040ac3f9f0bc077" +dependencies = [ + "memchr", +] + [[package]] name = "wait-timeout" version = "0.2.1" diff --git a/charon b/charon index df3b7fd4c127..e6ad3f7969ab 160000 --- a/charon +++ b/charon @@ -1 +1 @@ -Subproject commit df3b7fd4c1277827c92b4a2cb84347f1f54d92a6 +Subproject commit e6ad3f7969ab802a0f6a06d612ea24358c11e274 diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index 6a8137e1c744..9a2e7a81058b 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -14,10 +14,11 @@ use crate::kani_middle::transform::{BodyTransformation, GlobalPasses}; use crate::kani_queries::QueryDb; 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::errors::{raise_error, register_error}; use charon_lib::name_matcher::NamePattern; +use charon_lib::options::TranslateOptions; use charon_lib::transform::TransformCtx; -use charon_lib::transform::ctx::{TransformOptions, TransformPass}; +use charon_lib::transform::ctx::TransformPass; use kani_metadata::ArtifactType; use kani_metadata::{AssignsContract, CompilerArtifactStub}; use rustc_codegen_ssa::back::archive::{ @@ -382,12 +383,12 @@ where ret } -fn get_transform_options(tcx: &TranslatedCrate, error_ctx: &mut ErrorCtx) -> TransformOptions { +fn get_transform_options(tcx: &TranslatedCrate, error_ctx: &mut ErrorCtx) -> TranslateOptions { 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) + raise_error!(error_ctx, &TranslatedCrate::default(), Span::dummy(), "{}", msg) } }; let options = tcx.options.clone(); @@ -424,7 +425,7 @@ fn get_transform_options(tcx: &TranslatedCrate, error_ctx: &mut ErrorCtx) -> Tra .filter_map(|(s, opacity)| parse_pattern(&s).ok().map(|pat| (pat, opacity))) .collect() }; - TransformOptions { + TranslateOptions { no_code_duplication: false, hide_marker_traits: true, no_merge_goto_chains: false, @@ -438,5 +439,5 @@ fn create_charon_transformation_context(tcx: TyCtxt) -> TransformCtx { 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 } + TransformCtx { options, translated, errors: errors.into() } } 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 index c9a980b25f22..dc88934c22a2 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs @@ -26,7 +26,7 @@ use charon_lib::ast::{ 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, + GlobalDeclRef as CharonGlobalDeclRef, IntTy as CharonIntTy, 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, @@ -41,7 +41,7 @@ use charon_lib::ast::{ TraitRef as CharonTraitRef, TraitRefKind as CharonTraitRefKind, TranslatedCrate as CharonTranslatedCrate, TypeDecl as CharonTypeDecl, TypeDeclKind as CharonTypeDeclKind, TypeId as CharonTypeId, TypeVar as CharonTypeVar, - TypeVarId as CharonTypeVarId, UnOp as CharonUnOp, Var as CharonVar, VarId as CharonVarId, + TypeVarId as CharonTypeVarId, UnOp as CharonUnOp, Local as CharonVar, LocalId as CharonVarId, Variant as CharonVariant, VariantId as CharonVariantId, }; use charon_lib::errors::{Error as CharonError, ErrorCtx as CharonErrorCtx}; @@ -52,7 +52,7 @@ use charon_lib::ullbc_ast::{ RawTerminator as CharonRawTerminator, Statement as CharonStatement, SwitchTargets as CharonSwitchTargets, Terminator as CharonTerminator, }; -use charon_lib::{error_assert, error_or_panic}; +use charon_lib::{error_assert, raise_error, register_error}; use core::panic; use rustc_data_structures::fx::FxHashMap; use rustc_middle::ty::{TyCtxt, TypingEnv}; @@ -69,6 +69,7 @@ use rustc_public::ty::{ Ty, TyConst, TyConstKind, TyKind, UintTy, }; use rustc_public::{CrateDef, CrateDefType, DefId}; +use rustc_public_bridge::IndexedVal; use std::collections::HashMap; use std::iter::zip; use std::path::PathBuf; @@ -186,7 +187,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { regions: CharonVector::new(), skip_binder: CharonTraitDeclRef { trait_id: c_traitdecl_id, - generics: c_genarg.clone(), + generics: Box::new(c_genarg), }, }; let debr = CharonDeBruijnVar::free(CharonTraitClauseId::from_usize(i)); @@ -226,7 +227,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { .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 }, + skip_binder: CharonTraitDeclRef { trait_id: c_traitdecl_id, generics: Box::new(c_genarg) }, }; let c_traitclause = CharonTraitClause { clause_id: CharonTraitClauseId::from_usize(i), @@ -856,7 +857,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { // block. } _ => { - error_or_panic!(self, span, format!("Unexpected DefPathData: {:?}", data)); + raise_error!(self, span, "{}", format!("Unexpected DefPathData: {:?}", data)); } } } @@ -999,7 +1000,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { // block. } _ => { - error_or_panic!(self, span, format!("Unexpected DefPathData: {:?}", data)); + raise_error!(self, span, "{}", format!("Unexpected DefPathData: {:?}", data)); } } } @@ -1106,7 +1107,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { // block. } _ => { - error_or_panic!(self, span, format!("Unexpected DefPathData: {:?}", data)); + raise_error!(self, span, "{}", format!("Unexpected DefPathData: {:?}", data)); } } } @@ -1249,7 +1250,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { regions: trait_ref.trait_decl_ref.regions.clone(), skip_binder: CharonTraitDeclRef { trait_id: traitdecl_id, - generics: generics.clone(), + generics: Box::new(generics), }, }; let subs_traitref = CharonTraitRef { @@ -1528,7 +1529,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { }; let funcid = CharonFunIdOrTraitMethodRef::Fun(CharonFunId::Regular(fid)); let generics = self.translate_generic_args(genarg_resolve, def_id); - CharonFnPtr { func: funcid, generics } + CharonFnPtr { func: Box::new(funcid), Box::new(generics) } } TyKind::RigidTy(RigidTy::FnPtr(..)) => todo!(), x => unreachable!( @@ -1619,8 +1620,8 @@ impl<'a, 'tcx> Context<'a, 'tcx> { let ty = self.place_ty(place); let c_ty = self.translate_ty(ty); match c_ty.kind() { - CharonTyKind::Adt(CharonTypeId::Adt(c_typedeclid), _) => { - CharonRvalue::Discriminant(c_place, *c_typedeclid) + CharonTyKind::Adt(CharonTypeId::Adt(_), _) => { + CharonRvalue::Discriminant(c_place) } _ => todo!("Not yet implemented:{:?}", c_ty.kind()), } @@ -1724,7 +1725,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { let c_genarg = self.translate_generic_args(uc.args.clone(), defid); CharonRawConstantExpr::Global(CharonGlobalDeclRef { id: c_defid, - generics: c_genarg, + generics: Box::new(c_genarg), }) } ConstantKind::Param(_) => todo!(), @@ -1927,25 +1928,25 @@ impl<'a, 'tcx> Context<'a, 'tcx> { fn translate_int_ty(int_ty: IntTy) -> CharonIntegerTy { match int_ty { - IntTy::I8 => CharonIntegerTy::I8, - IntTy::I16 => CharonIntegerTy::I16, - IntTy::I32 => CharonIntegerTy::I32, - IntTy::I64 => CharonIntegerTy::I64, - IntTy::I128 => CharonIntegerTy::I128, + IntTy::I8 => CharonIntegerTy::Signed(CharonIntTy::I8), + IntTy::I16 => CharonIntegerTy::Signed(CharonIntTy::I16), + IntTy::I32 => CharonIntegerTy::Signed(CharonIntTy::I32), + IntTy::I64 => CharonIntegerTy::Signed(CharonIntTy::I64), + IntTy::I128 => CharonIntegerTy::Signed(CharonIntTy::I128), // TODO: assumes 64-bit platform - IntTy::Isize => CharonIntegerTy::Isize, + IntTy::Isize => CharonIntegerTy::Signed(CharonIntTy::Isize), } } fn translate_uint_ty(uint_ty: UintTy) -> CharonIntegerTy { match uint_ty { - UintTy::U8 => CharonIntegerTy::U8, - UintTy::U16 => CharonIntegerTy::U16, - UintTy::U32 => CharonIntegerTy::U32, - UintTy::U64 => CharonIntegerTy::U64, - UintTy::U128 => CharonIntegerTy::U128, + UintTy::U8 => CharonIntegerTy::Unsigned(CharonIntTy::U8), + UintTy::U16 => CharonIntegerTy::Unsigned(CharonIntTy::U16), + UintTy::U32 => CharonIntegerTy::Unsigned(CharonIntTy::U32), + UintTy::U64 => CharonIntegerTy::Unsigned(CharonIntTy::U64), + UintTy::U128 => CharonIntegerTy::Unsigned(CharonIntTy::U128), // TODO: assumes 64-bit platform - UintTy::Usize => CharonIntegerTy::Usize, + UintTy::Usize => CharonIntegerTy::Unsigned(CharonIntTy::Usize), } }