Skip to content

Commit 6ccf625

Browse files
remi-delmas-3000remi-delmas-3000
authored
Merge branch 'main' into bump-cbmc-viewer-3.10
2 parents 0e0014b + 0dc09a7 commit 6ccf625

File tree

16 files changed

+779
-135
lines changed

16 files changed

+779
-135
lines changed

‎Cargo.lock‎

Lines changed: 37 additions & 58 deletions
Original file line numberDiff line numberDiff line change
@@ -145,18 +145,15 @@ dependencies = [
145145

146146
[[package]]
147147
name = "bitflags"
148-
version = "2.6.0"
148+
version = "1.3.2"
149149
source = "registry+https://github.com/rust-lang/crates.io-index"
150-
checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de"
150+
checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a"
151151

152152
[[package]]
153-
name = "bitmaps"
154-
version = "2.1.0"
153+
name = "bitflags"
154+
version = "2.6.0"
155155
source = "registry+https://github.com/rust-lang/crates.io-index"
156-
checksum = "031043d04099746d8db04daf1fa424b2bc8bd69d92b25962dcde24da39ab64a2"
157-
dependencies = [
158-
"typenum",
159-
]
156+
checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de"
160157

161158
[[package]]
162159
name = "brownstone"
@@ -249,7 +246,7 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
249246

250247
[[package]]
251248
name = "charon"
252-
version = "0.1.36"
249+
version = "0.1.45"
253250
dependencies = [
254251
"anyhow",
255252
"assert_cmd",
@@ -260,7 +257,6 @@ dependencies = [
260257
"derive-visitor",
261258
"env_logger",
262259
"hashlink",
263-
"im",
264260
"index_vec",
265261
"indoc",
266262
"itertools 0.13.0",
@@ -272,6 +268,7 @@ dependencies = [
272268
"petgraph",
273269
"pretty",
274270
"regex",
271+
"rustc_apfloat",
275272
"rustc_version",
276273
"serde",
277274
"serde-map-to-array",
@@ -282,7 +279,7 @@ dependencies = [
282279
"toml",
283280
"tracing",
284281
"tracing-subscriber",
285-
"tracing-tree 0.3.1",
282+
"tracing-tree 0.4.0 (git+https://github.com/Nadrieril/tracing-tree)",
286283
"which",
287284
]
288285

@@ -454,7 +451,7 @@ version = "0.27.0"
454451
source = "registry+https://github.com/rust-lang/crates.io-index"
455452
checksum = "f476fe445d41c9e991fd07515a6f463074b782242ccf4a5b7b1d1012e70824df"
456453
dependencies = [
457-
"bitflags",
454+
"bitflags 2.6.0",
458455
"crossterm_winapi",
459456
"libc",
460457
"parking_lot",
@@ -703,20 +700,6 @@ version = "2.1.0"
703700
source = "registry+https://github.com/rust-lang/crates.io-index"
704701
checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4"
705702

706-
[[package]]
707-
name = "im"
708-
version = "15.1.0"
709-
source = "registry+https://github.com/rust-lang/crates.io-index"
710-
checksum = "d0acd33ff0285af998aaf9b57342af478078f53492322fafc47450e09397e0e9"
711-
dependencies = [
712-
"bitmaps",
713-
"rand_core",
714-
"rand_xoshiro",
715-
"sized-chunks",
716-
"typenum",
717-
"version_check",
718-
]
719-
720703
[[package]]
721704
name = "indent_write"
722705
version = "2.2.0"
@@ -814,7 +797,7 @@ dependencies = [
814797
"syn 2.0.87",
815798
"tracing",
816799
"tracing-subscriber",
817-
"tracing-tree 0.4.0",
800+
"tracing-tree 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)",
818801
]
819802

820803
[[package]]
@@ -1121,6 +1104,15 @@ dependencies = [
11211104
"autocfg",
11221105
]
11231106

1107+
[[package]]
1108+
name = "num_threads"
1109+
version = "0.1.7"
1110+
source = "registry+https://github.com/rust-lang/crates.io-index"
1111+
checksum = "5c7398b9c8b70908f6371f47ed36737907c87c52af34c268fed0bf0ceb92ead9"
1112+
dependencies = [
1113+
"libc",
1114+
]
1115+
11241116
[[package]]
11251117
name = "object"
11261118
version = "0.36.5"
@@ -1329,15 +1321,6 @@ dependencies = [
13291321
"getrandom",
13301322
]
13311323

1332-
[[package]]
1333-
name = "rand_xoshiro"
1334-
version = "0.6.0"
1335-
source = "registry+https://github.com/rust-lang/crates.io-index"
1336-
checksum = "6f97cdb2a36ed4183de61b2f824cc45c9f1037f28afe0a322e9fff4c108b5aaa"
1337-
dependencies = [
1338-
"rand_core",
1339-
]
1340-
13411324
[[package]]
13421325
name = "rayon"
13431326
version = "1.10.0"
@@ -1364,7 +1347,7 @@ version = "0.5.7"
13641347
source = "registry+https://github.com/rust-lang/crates.io-index"
13651348
checksum = "9b6dfecf2c74bce2466cabf93f6664d6998a69eb21e39f4207930065b27b771f"
13661349
dependencies = [
1367-
"bitflags",
1350+
"bitflags 2.6.0",
13681351
]
13691352

13701353
[[package]]
@@ -1417,6 +1400,16 @@ version = "0.1.24"
14171400
source = "registry+https://github.com/rust-lang/crates.io-index"
14181401
checksum = "719b953e2095829ee67db738b3bfa9fa368c94900df327b3f07fe6e794d2fe1f"
14191402

1403+
[[package]]
1404+
name = "rustc_apfloat"
1405+
version = "0.2.1+llvm-462a31f5a5ab"
1406+
source = "registry+https://github.com/rust-lang/crates.io-index"
1407+
checksum = "886d94c63c812a8037c4faca2607453a0fa4cf82f734665266876b022244543f"
1408+
dependencies = [
1409+
"bitflags 1.3.2",
1410+
"smallvec",
1411+
]
1412+
14201413
[[package]]
14211414
name = "rustc_version"
14221415
version = "0.4.1"
@@ -1432,7 +1425,7 @@ version = "0.38.38"
14321425
source = "registry+https://github.com/rust-lang/crates.io-index"
14331426
checksum = "aa260229e6538e52293eeb577aabd09945a09d6d9cc0fc550ed7529056c2e32a"
14341427
dependencies = [
1435-
"bitflags",
1428+
"bitflags 2.6.0",
14361429
"errno",
14371430
"libc",
14381431
"linux-raw-sys",
@@ -1600,16 +1593,6 @@ dependencies = [
16001593
"libc",
16011594
]
16021595

1603-
[[package]]
1604-
name = "sized-chunks"
1605-
version = "0.6.5"
1606-
source = "registry+https://github.com/rust-lang/crates.io-index"
1607-
checksum = "16d69225bde7a69b235da73377861095455d298f2b970996eec25ddbb42b3d1e"
1608-
dependencies = [
1609-
"bitmaps",
1610-
"typenum",
1611-
]
1612-
16131596
[[package]]
16141597
name = "smallvec"
16151598
version = "1.13.2"
@@ -1757,7 +1740,9 @@ checksum = "5dfd88e563464686c916c7e46e623e520ddc6d79fa6641390f2e3fa86e83e885"
17571740
dependencies = [
17581741
"deranged",
17591742
"itoa",
1743+
"libc",
17601744
"num-conv",
1745+
"num_threads",
17611746
"powerfmt",
17621747
"serde",
17631748
"time-core",
@@ -1906,9 +1891,9 @@ dependencies = [
19061891

19071892
[[package]]
19081893
name = "tracing-tree"
1909-
version = "0.3.1"
1894+
version = "0.4.0"
19101895
source = "registry+https://github.com/rust-lang/crates.io-index"
1911-
checksum = "b56c62d2c80033cb36fae448730a2f2ef99410fe3ecbffc916681a32f6807dbe"
1896+
checksum = "f459ca79f1b0d5f71c54ddfde6debfc59c8b6eeb46808ae492077f739dc7b49c"
19121897
dependencies = [
19131898
"nu-ansi-term 0.50.1",
19141899
"tracing-core",
@@ -1919,10 +1904,10 @@ dependencies = [
19191904
[[package]]
19201905
name = "tracing-tree"
19211906
version = "0.4.0"
1922-
source = "registry+https://github.com/rust-lang/crates.io-index"
1923-
checksum = "f459ca79f1b0d5f71c54ddfde6debfc59c8b6eeb46808ae492077f739dc7b49c"
1907+
source = "git+https://github.com/Nadrieril/tracing-tree#841286bfffd3c2200810244506cd127013dbeff9"
19241908
dependencies = [
19251909
"nu-ansi-term 0.50.1",
1910+
"time",
19261911
"tracing-core",
19271912
"tracing-log",
19281913
"tracing-subscriber",
@@ -1962,12 +1947,6 @@ version = "2.0.2"
19621947
source = "registry+https://github.com/rust-lang/crates.io-index"
19631948
checksum = "6af6ae20167a9ece4bcb41af5b80f8a1f1df981f6391189ce00fd257af04126a"
19641949

1965-
[[package]]
1966-
name = "typenum"
1967-
version = "1.17.0"
1968-
source = "registry+https://github.com/rust-lang/crates.io-index"
1969-
checksum = "42ff0bf0c66b8238c6f3b578df37d0b7848e55df8577b3f74f92a69acceeb825"
1970-
19711950
[[package]]
19721951
name = "unicode-ident"
19731952
version = "1.0.13"

‎charon‎

Submodule charon updated 238 files

‎deny.toml‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ confidence-threshold = 0.8
2323
# All these exceptions should probably appear in: tools/build-kani/license-notes.txt
2424
exceptions = [
2525
{ name = "unicode-ident", allow=["Unicode-DFS-2016"] },
26+
{ name = "rustc_apfloat", allow=["Apache-2.0 WITH LLVM-exception"] },
2627
]
2728

2829
[licenses.private]
@@ -42,3 +43,4 @@ wildcards = "allow"
4243
unknown-registry = "deny"
4344
unknown-git = "deny"
4445
allow-registry = ["https://github.com/rust-lang/crates.io-index"]
46+
allow-git = ["https://github.com/Nadrieril/tracing-tree"]

‎docs/src/rust-feature-support/intrinsics.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -156,7 +156,7 @@ fabsf32 | Yes | |
156156
fabsf64 | Yes | |
157157
fadd_fast | Yes | |
158158
fdiv_fast | Partial | [#809](https://github.com/model-checking/kani/issues/809) |
159-
float_to_int_unchecked | No | |
159+
float_to_int_unchecked | Partial | [#3629](https://github.com/model-checking/kani/issues/3629) |
160160
floorf32 | Yes | |
161161
floorf64 | Yes | |
162162
fmaf32 | Partial | Results are overapproximated |

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

Lines changed: 22 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ use crate::kani_middle::provide;
1212
use crate::kani_middle::reachability::{collect_reachable_items, filter_crate_items};
1313
use crate::kani_middle::transform::{BodyTransformation, GlobalPasses};
1414
use crate::kani_queries::QueryDb;
15-
use charon_lib::ast::TranslatedCrate;
15+
use charon_lib::ast::{AnyTransId, TranslatedCrate};
1616
use charon_lib::errors::ErrorCtx;
1717
use charon_lib::transform::TransformCtx;
1818
use charon_lib::transform::ctx::TransformOptions;
@@ -24,7 +24,7 @@ use rustc_codegen_ssa::back::archive::{
2424
use rustc_codegen_ssa::back::link::link_binary;
2525
use rustc_codegen_ssa::traits::CodegenBackend;
2626
use rustc_codegen_ssa::{CodegenResults, CrateInfo};
27-
use rustc_data_structures::fx::FxIndexMap;
27+
use rustc_data_structures::fx::{FxHashMap, FxIndexMap};
2828
use rustc_errors::{DEFAULT_LOCALE_RESOURCE, ErrorGuaranteed};
2929
use rustc_hir::def_id::{DefId as InternalDefId, LOCAL_CRATE};
3030
use rustc_metadata::EncodedMetadata;
@@ -106,13 +106,19 @@ impl LlbcCodegenBackend {
106106

107107
// Create a Charon transformation context that will be populated with translation results
108108
let mut ccx = create_charon_transformation_context(tcx);
109+
let mut id_map: FxHashMap<DefId, AnyTransId> = FxHashMap::default();
109110

110111
// Translate all the items
111112
for item in &items {
112113
match item {
113114
MonoItem::Fn(instance) => {
114-
let mut fcx =
115-
Context::new(tcx, *instance, &mut ccx.translated, &mut ccx.errors);
115+
let mut fcx = Context::new(
116+
tcx,
117+
*instance,
118+
&mut ccx.translated,
119+
&mut id_map,
120+
&mut ccx.errors,
121+
);
116122
let _ = fcx.translate();
117123
}
118124
MonoItem::Static(_def) => todo!(),
@@ -140,7 +146,7 @@ impl LlbcCodegenBackend {
140146

141147
// Run the micro-passes that clean up bodies.
142148
for pass in charon_lib::transform::ULLBC_PASSES.iter() {
143-
pass.transform_ctx(&mut ccx)
149+
pass.run(&mut ccx)
144150
}
145151

146152
// # Go from ULLBC to LLBC (Low-Level Borrow Calculus) by reconstructing
@@ -151,7 +157,7 @@ impl LlbcCodegenBackend {
151157

152158
// Run the micro-passes that clean up bodies.
153159
for pass in charon_lib::transform::LLBC_PASSES.iter() {
154-
pass.transform_ctx(&mut ccx)
160+
pass.run(&mut ccx)
155161
}
156162

157163
// Print the LLBC if requested. This is useful for expected tests.
@@ -161,8 +167,10 @@ impl LlbcCodegenBackend {
161167
debug!("# Final LLBC before serialization:\n\n{}\n", ccx);
162168
}
163169

164-
// Display an error report about the external dependencies, if necessary
165-
ccx.errors.report_external_deps_errors();
170+
// TODO: display an error report about the external dependencies, if necessary
171+
if ccx.errors.error_count > 0 {
172+
todo!()
173+
}
166174

167175
let crate_data: charon_lib::export::CrateData = charon_lib::export::CrateData::new(&ccx);
168176

@@ -393,18 +401,20 @@ fn create_charon_transformation_context(tcx: TyCtxt) -> TransformCtx {
393401
let options = TransformOptions {
394402
no_code_duplication: false,
395403
hide_marker_traits: false,
404+
no_merge_goto_chains: false,
396405
item_opacities: Vec::new(),
397406
};
398407
let crate_name = tcx.crate_name(LOCAL_CRATE).as_str().into();
399408
let translated = TranslatedCrate { crate_name, ..TranslatedCrate::default() };
400409
let errors = ErrorCtx {
401410
continue_on_failure: true,
402-
errors_as_warnings: false,
403-
dcx: tcx.dcx(),
404-
decls_with_errors: HashSet::new(),
411+
error_on_warnings: false,
412+
dcx: &(),
413+
external_decls_with_errors: HashSet::new(),
405414
ignored_failed_decls: HashSet::new(),
406-
dep_sources: HashMap::new(),
415+
external_dep_sources: HashMap::new(),
407416
def_id: None,
417+
def_id_is_local: true,
408418
error_count: 0,
409419
};
410420
TransformCtx { options, translated, errors }

0 commit comments

Comments
 (0)