Skip to content

Commit 9be3d1f

Browse files
celinvalcelinval
committed
Regression now passes
- Use internal to go around is_foreign_item() issue - Update tests after an issue: rust-lang/rust#116915 - Update the toolchain
1 parent fa92da2 commit 9be3d1f

File tree

5 files changed

+16
-69
lines changed

5 files changed

+16
-69
lines changed

‎kani-compiler/src/kani_middle/reachability.rs

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -153,7 +153,11 @@ impl<'tcx> MonoItemsCollector<'tcx> {
153153
/// instruction looking for the items that should be included in the compilation.
154154
fn reachable_items(&mut self) {
155155
while let Some(to_visit) = self.queue.pop() {
156-
if !self.collected.contains(&to_visit) {
156+
// TODO: This should only check is_foreign_item() or even `has_body()`.
157+
// We need https://github.com/rust-lang/rust/pull/118681 to land first.
158+
if !self.collected.contains(&to_visit)
159+
&& !self.tcx.is_foreign_item(rustc_internal::internal(to_visit.clone()).def_id())
160+
{
157161
self.collected.insert(to_visit.clone());
158162
let next_items = match &to_visit {
159163
MonoItem::Fn(instance) => self.visit_fn(*instance),
@@ -485,10 +489,7 @@ fn to_fingerprint(tcx: TyCtxt, item: &InternalMonoItem) -> Fingerprint {
485489

486490
/// Return whether we should include the item into codegen.
487491
fn should_codegen_locally(instance: &Instance) -> bool {
488-
// TODO: This should only check is_foreign_item() or even `has_body()`.
489-
// We need https://github.com/rust-lang/rust/pull/118681 to land first.
490-
//!instance.is_foreign_item()
491-
instance.body().is_some()
492+
!instance.is_foreign_item()
492493
}
493494

494495
fn collect_alloc_items(alloc_id: AllocId) -> Vec<MonoItem> {

‎kani-compiler/src/kani_middle/stubbing/mod.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,7 @@ pub fn harness_stub_map(
4646
pub fn validate_instance(tcx: TyCtxt, instance: Instance) -> bool {
4747
let internal_instance = rustc_internal::internal(instance);
4848
if get_stub(tcx, internal_instance.def_id()).is_some() {
49+
debug!(?instance, "validate_instance");
4950
let item = CrateItem::try_from(instance).unwrap();
5051
let mut checker = StubConstChecker::new(tcx, internal_instance, item);
5152
checker.visit_body(&item.body());

‎rust-toolchain.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@
22
# SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
[toolchain]
5-
channel = "nightly-2023-12-03"
5+
channel = "nightly-2023-12-07"
66
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

‎tests/expected/any_vec/exact_length.expected

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
Checking harness check_access_length_17...
22

3-
Failed Checks: dereference failure: pointer outside object bounds\
4-
in check_access_length_17
3+
Failed Checks: assumption failed\
4+
in <usize as std::slice::SliceIndex<[Dummy]>>::get_unchecked
55

66
Checking harness check_access_length_zero...
77

8-
Failed Checks: dereference failure: pointer outside object bounds\
9-
in check_access_length_zero
8+
Failed Checks: assumption failed\
9+
in <usize as std::slice::SliceIndex<[u8]>>::get_unchecked
1010

1111
Verification failed for - check_access_length_17
1212
Verification failed for - check_access_length_zero

‎tests/expected/any_vec/out_bounds.expected

Lines changed: 4 additions & 59 deletions
Original file line numberDiff line numberDiff line change
@@ -1,61 +1,6 @@
1-
check_always_out_bounds::check_0.pointer_dereference\
2-
Status: FAILURE\
3-
Description: "dereference failure: pointer NULL"\
4-
function check_always_out_bounds::check_0
5-
6-
check_always_out_bounds::check_0.pointer_dereference\
7-
Status: FAILURE\
8-
Description: "dereference failure: pointer outside object bounds"\
9-
function check_always_out_bounds::check_0
10-
11-
check_always_out_bounds::check_0.pointer_dereference\
12-
Status: FAILURE\
13-
Description: "dereference failure: invalid integer address"\
14-
function check_always_out_bounds::check_0
15-
16-
check_always_out_bounds::check_1.pointer_dereference\
17-
Status: FAILURE\
18-
Description: "dereference failure: pointer outside object bounds"\
19-
function check_always_out_bounds::check_1
20-
21-
check_always_out_bounds::check_2.pointer_dereference\
22-
Status: FAILURE\
23-
Description: "dereference failure: pointer outside object bounds"\
24-
function check_always_out_bounds::check_2
25-
26-
check_always_out_bounds::check_3.pointer_dereference\
27-
Status: FAILURE\
28-
Description: "dereference failure: pointer outside object bounds"\
29-
function check_always_out_bounds::check_3
30-
31-
check_always_out_bounds::check_4.pointer_dereference\
32-
Status: FAILURE\
33-
Description: "dereference failure: pointer outside object bounds"\
34-
function check_always_out_bounds::check_4
35-
36-
check_always_out_bounds::check_5.pointer_dereference\
37-
Status: FAILURE\
38-
Description: "dereference failure: pointer outside object bounds"\
39-
function check_always_out_bounds::check_5
40-
41-
check_always_out_bounds::check_6.pointer_dereference\
42-
Status: FAILURE\
43-
Description: "dereference failure: pointer outside object bounds"\
44-
function check_always_out_bounds::check_6
45-
46-
check_always_out_bounds::check_7.pointer_dereference\
47-
Status: FAILURE\
48-
Description: "dereference failure: pointer outside object bounds"\
49-
function check_always_out_bounds::check_7
50-
51-
check_always_out_bounds::check_8.pointer_dereference\
52-
Status: FAILURE\
53-
Description: "dereference failure: pointer outside object bounds"\
54-
function check_always_out_bounds::check_8
55-
56-
check_always_out_bounds::check_9.cover\
57-
Status: UNREACHABLE\
58-
Description: "cover condition: *val == 0"\
59-
function check_always_out_bounds::check_9
1+
Checking harness check_always_out_bounds...
602

3+
Failed Checks: assumption failed
4+
in <usize as std::slice::SliceIndex<[u8]>>::get_unchecked
615

6+
Verification failed for - check_always_out_bounds

0 commit comments

Comments
 (0)