Skip to content

Commit 4578a6a

Browse files
tautschnigtautschnig
authored
Incrementally update charon submodule with LLBC backend adaptations (#4445)
The commits in this PR change the git submodule through incremental updates. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent 201661c commit 4578a6a

File tree

5 files changed

+49
-41
lines changed

5 files changed

+49
-41
lines changed

‎Cargo.lock‎

Lines changed: 6 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -265,7 +265,7 @@ checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801"
265265

266266
[[package]]
267267
name = "charon"
268-
version = "0.1.62"
268+
version = "0.1.65"
269269
dependencies = [
270270
"annotate-snippets",
271271
"anstream",
@@ -276,15 +276,17 @@ dependencies = [
276276
"convert_case",
277277
"derive_generic_visitor",
278278
"env_logger",
279-
"hashlink",
280279
"index_vec",
280+
"indexmap",
281281
"indoc",
282282
"itertools 0.13.0",
283283
"lazy_static",
284284
"log",
285285
"macros",
286286
"nom",
287287
"nom-supreme",
288+
"num-bigint",
289+
"num-rational",
288290
"petgraph 0.6.5",
289291
"rustc_version",
290292
"serde",
@@ -805,15 +807,6 @@ dependencies = [
805807
"petgraph 0.8.3",
806808
]
807809

808-
[[package]]
809-
name = "hashbrown"
810-
version = "0.14.5"
811-
source = "registry+https://github.com/rust-lang/crates.io-index"
812-
checksum = "e5274423e17b7c9fc20b6e7e208532f9b19825d82dfd615708b70edd83df41f1"
813-
dependencies = [
814-
"ahash",
815-
]
816-
817810
[[package]]
818811
name = "hashbrown"
819812
version = "0.15.5"
@@ -829,16 +822,6 @@ version = "0.16.0"
829822
source = "registry+https://github.com/rust-lang/crates.io-index"
830823
checksum = "5419bdc4f6a9207fbeba6d11b604d481addf78ecd10c11ad51e76c2f6482748d"
831824

832-
[[package]]
833-
name = "hashlink"
834-
version = "0.9.1"
835-
source = "registry+https://github.com/rust-lang/crates.io-index"
836-
checksum = "6ba4ff7128dee98c7dc9794b6a411377e1404dba1c97deb8d1a55297bd25d8af"
837-
dependencies = [
838-
"hashbrown 0.14.5",
839-
"serde",
840-
]
841-
842825
[[package]]
843826
name = "heck"
844827
version = "0.5.0"
@@ -1009,6 +992,8 @@ checksum = "6717a8d2a5a929a1a2eb43a12812498ed141a0bcfb7e8f7844fbdbe4303bba9f"
1009992
dependencies = [
1010993
"equivalent",
1011994
"hashbrown 0.16.0",
995+
"serde",
996+
"serde_core",
1012997
]
1013998

1014999
[[package]]

‎charon‎

Submodule charon updated 120 files

‎kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs‎

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,6 @@ use crate::kani_middle::transform::{BodyTransformation, GlobalPasses};
1414
use crate::kani_queries::QueryDb;
1515
use charon_lib::ast::{AnyTransId, TranslatedCrate, meta::ItemOpacity::*, meta::Span};
1616
use charon_lib::errors::ErrorCtx;
17-
use charon_lib::errors::error_or_panic;
1817
use charon_lib::name_matcher::NamePattern;
1918
use charon_lib::transform::TransformCtx;
2019
use charon_lib::transform::ctx::{TransformOptions, TransformPass};
@@ -41,6 +40,7 @@ use rustc_session::Session;
4140
use rustc_session::config::{CrateType, OutputFilenames, OutputType};
4241
use rustc_session::output::out_filename;
4342
use std::any::Any;
43+
use std::cell::RefCell;
4444
use std::fs::File;
4545
use std::path::Path;
4646
use std::sync::{Arc, Mutex};
@@ -115,12 +115,13 @@ impl LlbcCodegenBackend {
115115
debug!("Translating: {item:?}");
116116
match item {
117117
MonoItem::Fn(instance) => {
118+
let mut errors_borrow = ccx.errors.borrow_mut();
118119
let mut fcx = Context::new(
119120
tcx,
120121
*instance,
121122
&mut ccx.translated,
122123
&mut id_map,
123-
&mut ccx.errors,
124+
&mut *errors_borrow,
124125
);
125126
let _ = fcx.translate();
126127
}
@@ -167,7 +168,7 @@ impl LlbcCodegenBackend {
167168
}
168169

169170
// TODO: display an error report about the external dependencies, if necessary
170-
if ccx.errors.error_count > 0 {
171+
if ccx.errors.borrow().error_count > 0 {
171172
todo!()
172173
}
173174

@@ -400,7 +401,7 @@ fn get_transform_options(tcx: &TranslatedCrate, error_ctx: &mut ErrorCtx) -> Tra
400401
Ok(p) => Ok(p),
401402
Err(e) => {
402403
let msg = format!("failed to parse pattern `{s}` ({e})");
403-
error_or_panic!(error_ctx, &TranslatedCrate::default(), Span::dummy(), msg)
404+
Err(error_ctx.span_err(&TranslatedCrate::default(), Span::dummy(), &msg))
404405
}
405406
};
406407
let options = tcx.options.clone();
@@ -443,6 +444,7 @@ fn get_transform_options(tcx: &TranslatedCrate, error_ctx: &mut ErrorCtx) -> Tra
443444
no_merge_goto_chains: false,
444445
item_opacities,
445446
print_built_llbc: true,
447+
remove_associated_types: Vec::new(),
446448
}
447449
}
448450

@@ -451,5 +453,5 @@ fn create_charon_transformation_context(tcx: TyCtxt) -> TransformCtx {
451453
let translated = TranslatedCrate { crate_name, ..TranslatedCrate::default() };
452454
let mut errors = ErrorCtx::new(true, false);
453455
let options = get_transform_options(&translated, &mut errors);
454-
TransformCtx { options, translated, errors }
456+
TransformCtx { options, translated, errors: std::cell::RefCell::new(errors) }
455457
}

‎kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs‎

Lines changed: 21 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ use charon_lib::ullbc_ast::{
5252
RawTerminator as CharonRawTerminator, Statement as CharonStatement,
5353
SwitchTargets as CharonSwitchTargets, Terminator as CharonTerminator,
5454
};
55-
use charon_lib::{error_assert, error_or_panic};
55+
use charon_lib::{error_assert, raise_error, register_error};
5656
use core::panic;
5757
use rustc_data_structures::fx::FxHashMap;
5858
use rustc_middle::ty::{TyCtxt, TypingEnv};
@@ -114,8 +114,8 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
114114
self.tcx
115115
}
116116

117-
fn span_err(&mut self, span: CharonSpan, msg: &str) {
118-
self.errors.span_err(self.translated, span, msg);
117+
fn span_err(&mut self, span: CharonSpan, msg: &str) -> CharonError {
118+
self.errors.span_err(self.translated, span, msg)
119119
}
120120

121121
fn continue_on_failure(&self) -> bool {
@@ -442,7 +442,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
442442
trait_clauses: CharonVector::new(),
443443
regions_outlive: Vec::new(),
444444
types_outlive: Vec::new(),
445-
trait_type_constraints: Vec::new(),
445+
trait_type_constraints: CharonVector::new(),
446446
}
447447
}
448448

@@ -523,7 +523,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
523523
trait_clauses,
524524
regions_outlive: Vec::new(),
525525
types_outlive: Vec::new(),
526-
trait_type_constraints: Vec::new(),
526+
trait_type_constraints: CharonVector::new(),
527527
}
528528
}
529529

@@ -595,7 +595,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
595595
trait_clauses,
596596
regions_outlive: Vec::new(),
597597
types_outlive: Vec::new(),
598-
trait_type_constraints: Vec::new(),
598+
trait_type_constraints: CharonVector::new(),
599599
}
600600
}
601601

@@ -857,7 +857,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
857857
// block.
858858
}
859859
_ => {
860-
error_or_panic!(self, span, format!("Unexpected DefPathData: {:?}", data));
860+
raise_error!(self, span, "Unexpected DefPathData: {:?}", data);
861861
}
862862
}
863863
}
@@ -1000,7 +1000,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
10001000
// block.
10011001
}
10021002
_ => {
1003-
error_or_panic!(self, span, format!("Unexpected DefPathData: {:?}", data));
1003+
raise_error!(self, span, "Unexpected DefPathData: {:?}", data);
10041004
}
10051005
}
10061006
}
@@ -1106,7 +1106,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
11061106
// block.
11071107
}
11081108
_ => {
1109-
error_or_panic!(self, span, format!("Unexpected DefPathData: {:?}", data));
1109+
raise_error!(self, span, "Unexpected DefPathData: {:?}", data);
11101110
}
11111111
}
11121112
}
@@ -1253,7 +1253,11 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
12531253
},
12541254
};
12551255
let subs_traitref = CharonTraitRef {
1256-
kind: CharonTraitRefKind::BuiltinOrAuto(subs_traitdeclref.clone()),
1256+
kind: CharonTraitRefKind::BuiltinOrAuto {
1257+
trait_decl_ref: subs_traitdeclref.clone(),
1258+
parent_trait_refs: CharonVector::new(),
1259+
types: Vec::new(),
1260+
},
12571261
trait_decl_ref: subs_traitdeclref,
12581262
};
12591263
trait_refs.push(subs_traitref);
@@ -1488,7 +1492,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
14881492
};
14891493
if let Some(content) = content {
14901494
let span = self.translate_span(stmt.span);
1491-
return Some(CharonStatement { span, content });
1495+
return Some(CharonStatement { span, content, comments_before: Vec::new() });
14921496
};
14931497
None
14941498
}
@@ -1559,8 +1563,12 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
15591563
_ => todo!(),
15601564
};
15611565
(
1562-
statement.map(|statement| CharonStatement { span, content: statement }),
1563-
CharonTerminator { span, content: terminator },
1566+
statement.map(|statement| CharonStatement {
1567+
span,
1568+
content: statement,
1569+
comments_before: Vec::new(),
1570+
}),
1571+
CharonTerminator { span, content: terminator, comments_before: Vec::new() },
15641572
)
15651573
}
15661574

‎scripts/charon-patch.diff‎

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ index 20f8a9df..a1bf1ee6 100644
44
+++ b/charon/Cargo.toml
55
@@ -2,7 +2,7 @@
66
name = "charon"
7-
version = "0.1.62"
7+
version = "0.1.65"
88
authors = ["Son Ho <[email protected]>"]
99
-edition = "2021"
1010
+edition = "2024"
@@ -24,3 +24,16 @@ index 59f7eaab..21508e19 100644
2424
self.vector.indices()
2525
}
2626

27+
diff --git a/charon/src/transform/expand_associated_types.rs b/charon/src/transform/expand_associated_types.rs
28+
index 19978d56..c98c8e0e 100644
29+
--- a/charon/src/transform/expand_associated_types.rs
30+
+++ b/charon/src/transform/expand_associated_types.rs
31+
@@ -761,7 +761,7 @@ impl<'a> ComputeItemModifications<'a> {
32+
&'b mut self,
33+
clause: &TraitClause,
34+
clause_to_path: F,
35+
- ) -> impl Iterator<Item = AssocTypePath> + use<'b, F>
36+
+ ) -> impl Iterator<Item = AssocTypePath> + use<'a, 'b, F>
37+
where
38+
F: Fn(TraitClauseId) -> TraitRefPath,
39+
{

0 commit comments

Comments
 (0)