Skip to content

Commit

Permalink
Upgrade toolchain to 2024-05-14 (rust-lang#3183)
Browse files Browse the repository at this point in the history
  • Loading branch information
zhassan-aws authored May 15, 2024
1 parent 997a54c commit 52a5b77
Show file tree
Hide file tree
Showing 35 changed files with 241 additions and 130 deletions.
4 changes: 2 additions & 2 deletions cprover_bindings/src/goto_program/expr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1331,11 +1331,11 @@ impl Expr {
fn unop_return_type(op: UnaryOperator, arg: &Expr) -> Type {
match op {
Bitnot | BitReverse | Bswap | UnaryMinus => arg.typ.clone(),
CountLeadingZeros { .. } | CountTrailingZeros { .. } => arg.typ.clone(),
CountLeadingZeros { .. } | CountTrailingZeros { .. } => Type::unsigned_int(32),
ObjectSize | PointerObject => Type::size_t(),
PointerOffset => Type::ssize_t(),
IsDynamicObject | IsFinite | Not => Type::bool(),
Popcount => arg.typ.clone(),
Popcount => Type::unsigned_int(32),
}
}
/// Private helper function to make unary operators
Expand Down
17 changes: 11 additions & 6 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ use rustc_middle::ty::{List, TypeFoldable};
use rustc_smir::rustc_internal;
use rustc_span::def_id::DefId;
use rustc_target::abi::{
Abi::Vector, FieldIdx, FieldsShape, Integer, LayoutS, Primitive, Size, TagEncoding,
Abi::Vector, FieldIdx, FieldsShape, Float, Integer, LayoutS, Primitive, Size, TagEncoding,
TyAndLayout, VariantIdx, Variants,
};
use stable_mir::abi::{ArgAbi, FnAbi, PassMode};
Expand Down Expand Up @@ -1354,13 +1354,18 @@ impl<'tcx> GotocCtx<'tcx> {
}
}
},
Primitive::Float(f) => self.codegen_float_type(f),
Primitive::Pointer(_) => Ty::new_ptr(self.tcx, self.tcx.types.u8, Mutability::Not),
}
}

Primitive::F32 => self.tcx.types.f32,
Primitive::F64 => self.tcx.types.f64,
pub fn codegen_float_type(&self, f: Float) -> Ty<'tcx> {
match f {
Float::F32 => self.tcx.types.f32,
Float::F64 => self.tcx.types.f64,
// `F16` and `F128` are not yet handled.
// Tracked here: <https://github.com/model-checking/kani/issues/3069>
Primitive::F16 | Primitive::F128 => unimplemented!(),
Primitive::Pointer(_) => Ty::new_ptr(self.tcx, self.tcx.types.u8, Mutability::Not),
Float::F16 | Float::F128 => unimplemented!(),
}
}

Expand Down Expand Up @@ -1672,7 +1677,7 @@ pub fn pointee_type(mir_type: Ty) -> Option<Ty> {
/// Extracts the pointee type if the given mir type is either a known smart pointer (Box, Rc, ..)
/// or a regular pointer.
pub fn std_pointee_type(mir_type: Ty) -> Option<Ty> {
mir_type.builtin_deref(true).map(|tm| tm.ty)
mir_type.builtin_deref(true)
}

/// This is a place holder function that should normalize the given type.
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/kani_middle/coercion.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,8 +16,8 @@
use rustc_hir::lang_items::LangItem;
use rustc_middle::traits::{ImplSource, ImplSourceUserDefinedData};
use rustc_middle::ty::adjustment::CustomCoerceUnsized;
use rustc_middle::ty::TraitRef;
use rustc_middle::ty::{ParamEnv, Ty, TyCtxt};
use rustc_middle::ty::{TraitRef, TypeAndMut};
use rustc_smir::rustc_internal;
use stable_mir::ty::{RigidTy, Ty as TyStable, TyKind};
use stable_mir::Symbol;
Expand Down Expand Up @@ -263,5 +263,5 @@ fn custom_coerce_unsize_info<'tcx>(

/// Extract pointee type from builtin pointer types.
fn extract_pointee(tcx: TyCtxt<'_>, typ: TyStable) -> Option<Ty<'_>> {
rustc_internal::internal(tcx, typ).builtin_deref(true).map(|TypeAndMut { ty, .. }| ty)
rustc_internal::internal(tcx, typ).builtin_deref(true)
}
7 changes: 7 additions & 0 deletions library/kani_macros/build.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT

fn main() {
// Make sure `kani_sysroot` is a recognized config
println!("cargo::rustc-check-cfg=cfg(kani_sysroot)");
}
2 changes: 1 addition & 1 deletion rust-toolchain.toml
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT

[toolchain]
channel = "nightly-2024-04-22"
channel = "nightly-2024-05-14"
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
11 changes: 7 additions & 4 deletions tests/expected/coroutines/as_parameter/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,11 @@ where

#[kani::proof]
fn main() {
foo(|| {
yield 1;
return 2;
});
foo(
#[coroutine]
|| {
yield 1;
return 2;
},
);
}
4 changes: 3 additions & 1 deletion tests/expected/coroutines/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
// SPDX-License-Identifier: Apache-2.0 OR MIT

#![feature(coroutines, coroutine_trait)]
#![feature(stmt_expr_attributes)]

use std::ops::{Coroutine, CoroutineState};
use std::pin::Pin;
Expand All @@ -10,7 +11,8 @@ use std::pin::Pin;
#[kani::unwind(2)]
fn main() {
let val: bool = kani::any();
let mut coroutine = move || {
let mut coroutine = #[coroutine]
move || {
let x = val;
yield x;
return !x;
Expand Down
4 changes: 3 additions & 1 deletion tests/expected/coroutines/pin/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,13 +5,15 @@
// from https://github.com/model-checking/kani/issues/416

#![feature(coroutines, coroutine_trait)]
#![feature(stmt_expr_attributes)]

use std::ops::{Coroutine, CoroutineState};
use std::pin::Pin;

#[kani::proof]
fn main() {
let mut coroutine = || {
let mut coroutine = #[coroutine]
|| {
yield 1;
return true;
};
Expand Down
14 changes: 0 additions & 14 deletions tests/expected/intrinsics/ctpop-ice/ctpop_ice.rs

This file was deleted.

6 changes: 0 additions & 6 deletions tests/expected/intrinsics/ctpop-ice/expected

This file was deleted.

4 changes: 3 additions & 1 deletion tests/kani/Coroutines/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,14 +4,16 @@
// This tests that coroutines work, even with a non-() resume type.

#![feature(coroutines, coroutine_trait)]
#![feature(stmt_expr_attributes)]

use std::ops::{Coroutine, CoroutineState};
use std::pin::Pin;

#[kani::proof]
#[kani::unwind(3)]
fn main() {
let mut add_one = |mut resume: u8| {
let mut add_one = #[coroutine]
|mut resume: u8| {
loop {
resume = yield resume.saturating_add(1);
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@
//[nomiropt]compile-flags: -Z mir-opt-level=0

#![feature(coroutines, coroutine_trait)]
#![feature(stmt_expr_attributes)]

use std::ops::Coroutine;
use std::pin::Pin;
Expand Down Expand Up @@ -41,7 +42,8 @@ fn main() {
}

fn t1() {
let mut a = || {
let mut a = #[coroutine]
|| {
let b = B;
if test() {
drop(b);
Expand All @@ -57,7 +59,8 @@ fn t1() {
}

fn t2() {
let mut a = || {
let mut a = #[coroutine]
|| {
let b = B;
if test2() {
drop(b);
Expand Down
76 changes: 48 additions & 28 deletions tests/kani/Coroutines/rustc-coroutine-tests/control-flow.rs
Original file line number Diff line number Diff line change
Expand Up @@ -35,32 +35,52 @@ where
#[kani::proof]
#[kani::unwind(16)]
fn main() {
finish(1, || yield);
finish(8, || {
for _ in 0..8 {
yield;
}
});
finish(1, || {
if true {
yield;
} else {
}
});
finish(1, || {
if false {
} else {
yield;
}
});
finish(2, || {
if {
yield;
false
} {
yield;
panic!()
}
yield
});
finish(
1,
#[coroutine]
|| yield,
);
finish(
8,
#[coroutine]
|| {
for _ in 0..8 {
yield;
}
},
);
finish(
1,
#[coroutine]
|| {
if true {
yield;
} else {
}
},
);
finish(
1,
#[coroutine]
|| {
if false {
} else {
yield;
}
},
);
finish(
2,
#[coroutine]
|| {
if {
yield;
false
} {
yield;
panic!()
}
yield
},
);
}
10 changes: 7 additions & 3 deletions tests/kani/Coroutines/rustc-coroutine-tests/env-drop.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@
//[nomiropt]compile-flags: -Z mir-opt-level=0

#![feature(coroutines, coroutine_trait)]
#![feature(stmt_expr_attributes)]

use std::ops::Coroutine;
use std::pin::Pin;
Expand All @@ -36,7 +37,8 @@ fn main() {

fn t1() {
let b = B;
let mut foo = || {
let mut foo = #[coroutine]
|| {
yield;
drop(b);
};
Expand All @@ -50,7 +52,8 @@ fn t1() {

fn t2() {
let b = B;
let mut foo = || {
let mut foo = #[coroutine]
|| {
yield b;
};

Expand All @@ -63,7 +66,8 @@ fn t2() {

fn t3() {
let b = B;
let foo = || {
let foo = #[coroutine]
|| {
yield;
drop(b);
};
Expand Down
2 changes: 2 additions & 0 deletions tests/kani/Coroutines/rustc-coroutine-tests/iterator-count.rs
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@ impl<T: Coroutine<(), Return = ()> + Unpin> Iterator for W<T> {
}

fn test() -> impl Coroutine<(), Return = (), Yield = u8> + Unpin {
#[coroutine]
|| {
for i in 1..6 {
yield i
Expand All @@ -43,6 +44,7 @@ fn main() {
let end = 11;

let closure_test = |start| {
#[coroutine]
move || {
for i in start..end {
yield i
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,14 +9,16 @@
// run-pass

#![feature(coroutines, coroutine_trait)]
#![feature(stmt_expr_attributes)]

use std::ops::Coroutine;
use std::pin::Pin;

#[kani::proof]
fn main() {
let b = |_| 3;
let mut a = || {
let mut a = #[coroutine]
|| {
b(yield);
};
Pin::new(&mut a).resume(());
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,7 @@ impl Drop for Foo {
}

fn move_before_yield() -> impl Coroutine<Yield = (), Return = ()> {
#[coroutine]
static || {
let first = Foo([0; FOO_SIZE]);
let _second = first;
Expand All @@ -52,6 +53,7 @@ fn move_before_yield() -> impl Coroutine<Yield = (), Return = ()> {
fn noop() {}

fn move_before_yield_with_noop() -> impl Coroutine<Yield = (), Return = ()> {
#[coroutine]
static || {
let first = Foo([0; FOO_SIZE]);
noop();
Expand All @@ -64,6 +66,7 @@ fn move_before_yield_with_noop() -> impl Coroutine<Yield = (), Return = ()> {
// Today we don't have NRVO (we allocate space for both `first` and `second`,)
// but we can overlap `first` with `_third`.
fn overlap_move_points() -> impl Coroutine<Yield = (), Return = ()> {
#[coroutine]
static || {
let first = Foo([0; FOO_SIZE]);
yield;
Expand All @@ -75,6 +78,7 @@ fn overlap_move_points() -> impl Coroutine<Yield = (), Return = ()> {
}

fn overlap_x_and_y() -> impl Coroutine<Yield = (), Return = ()> {
#[coroutine]
static || {
let x = Foo([0; FOO_SIZE]);
yield;
Expand Down
Loading

0 comments on commit 52a5b77

Please sign in to comment.