Skip to content

[WIP] Update charon submodule to latest HEAD #4254

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

[WIP] Update charon submodule to latest HEAD #4254

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
55 changes: 29 additions & 26 deletions Cargo.lock
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down Expand Up @@ -295,7 +294,7 @@ checksum = "9555578bc9e57714c812a1f84e4fc5b4d21fcb063490c624de019f7464c91268"

[[package]]
name = "charon"
version = "0.1.62"
version = "0.1.122"
dependencies = [
"annotate-snippets",
"anstream",
Expand All @@ -305,23 +304,27 @@ dependencies = [
"colored",
"convert_case",
"derive_generic_visitor",
"either",
"env_logger",
"hashlink",
"index_vec",
"indexmap",
"indoc",
"itertools 0.13.0",
"lazy_static",
"log",
"macros",
"nom",
"nom-supreme",
"num-bigint",
"num-rational",
"petgraph 0.6.5",
"rustc_version",
"serde",
"serde-map-to-array",
"serde_json",
"serde_stacker",
"stacker",
"strip-ansi-escapes",
"take_mut",
"toml",
"tracing",
Expand Down Expand Up @@ -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"
Expand All @@ -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"
Expand Down Expand Up @@ -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]]
Expand Down Expand Up @@ -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",
]
Expand Down Expand Up @@ -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"
Expand Down Expand Up @@ -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"
Expand Down
2 changes: 1 addition & 1 deletion charon
Open in desktop
Submodule charon updated 562 files
13 changes: 7 additions & 6 deletions kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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::{
Expand Down Expand Up @@ -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();
Expand Down Expand Up @@ -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,
Expand All @@ -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() }
}
51 changes: 26 additions & 25 deletions kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand All @@ -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};
Expand All @@ -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};
Expand All @@ -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;
Expand Down Expand Up @@ -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));
Expand Down Expand Up @@ -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),
Expand Down Expand Up @@ -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));
}
}
}
Expand Down Expand Up @@ -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));
}
}
}
Expand Down Expand Up @@ -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));
}
}
}
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -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!(
Expand Down Expand Up @@ -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()),
}
Expand Down Expand Up @@ -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!(),
Expand Down Expand Up @@ -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),
}
}

Expand Down
Loading