Skip to content

Commit

Permalink
Upgrade toolchain to 2024-09-12 (model-checking#3524)
Browse files Browse the repository at this point in the history
Relevant upstream PR:

rust-lang/rust@d2309c2a9d Ban non-array SIMD

Resolves model-checking#3521

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
  • Loading branch information
qinheping authored Sep 18, 2024
1 parent f888913 commit d2051b7
Show file tree
Hide file tree
Showing 30 changed files with 184 additions and 184 deletions.
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-09-11"
channel = "nightly-2024-09-12"
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
6 changes: 3 additions & 3 deletions tests/expected/intrinsics/simd-arith-overflows/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,14 +8,14 @@ use std::intrinsics::simd::{simd_add, simd_mul, simd_sub};
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq, Debug)]
pub struct i8x2(i8, i8);
pub struct i8x2([i8; 2]);

#[kani::proof]
fn main() {
let a = kani::any();
let b = kani::any();
let simd_a = i8x2(a, a);
let simd_b = i8x2(b, b);
let simd_a = i8x2([a, a]);
let simd_b = i8x2([b, b]);

unsafe {
let _ = simd_add(simd_a, simd_b);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,26 +9,26 @@ use std::intrinsics::simd::simd_eq;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i64x2(i64, i64);
pub struct i64x2([i64; 2]);

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct u64x2(u64, u64);
pub struct u64x2([u64; 2]);

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct u32x4(u32, u32, u32, u32);
pub struct u32x4([u32; 4]);

#[kani::proof]
fn main() {
let x = u64x2(0, 0);
let y = u64x2(0, 1);
let x = u64x2([0, 0]);
let y = u64x2([0, 1]);

unsafe {
let invalid_simd: u32x4 = simd_eq(x, y);
assert!(invalid_simd == u32x4(u32::MAX, u32::MAX, 0, 0));
assert!(invalid_simd == u32x4([u32::MAX, u32::MAX, 0, 0]));
// ^^^^ The code above fails to type-check in Rust with the error:
// ```
// error[E0511]: invalid monomorphization of `simd_eq` intrinsic: expected
Expand Down
6 changes: 3 additions & 3 deletions tests/expected/intrinsics/simd-div-div-zero/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,13 +8,13 @@ use std::intrinsics::simd::simd_div;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i32x2(i32, i32);
pub struct i32x2([i32; 2]);

#[kani::proof]
fn test_simd_div() {
let dividend = kani::any();
let dividends = i32x2(dividend, dividend);
let dividends = i32x2([dividend, dividend]);
let divisor = 0;
let divisors = i32x2(divisor, divisor);
let divisors = i32x2([divisor, divisor]);
let _ = unsafe { simd_div(dividends, divisors) };
}
4 changes: 2 additions & 2 deletions tests/expected/intrinsics/simd-div-rem-overflow/expected
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
FAILURE\
attempt to compute simd_div which would overflow
UNREACHABLE\
assertion failed: quotients.0 == quotients.1
assertion failed: quotients.0[0] == quotients.0[1]
FAILURE\
attempt to compute simd_rem which would overflow
UNREACHABLE\
assertion failed: remainders.0 == remainders.1
assertion failed: remainders.0[0] == remainders.0[1]
14 changes: 7 additions & 7 deletions tests/expected/intrinsics/simd-div-rem-overflow/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ use std::intrinsics::simd::{simd_div, simd_rem};
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i32x2(i32, i32);
pub struct i32x2([i32; 2]);

unsafe fn do_simd_div(dividends: i32x2, divisors: i32x2) -> i32x2 {
simd_div(dividends, divisors)
Expand All @@ -21,19 +21,19 @@ unsafe fn do_simd_rem(dividends: i32x2, divisors: i32x2) -> i32x2 {
#[kani::proof]
fn test_simd_div_overflow() {
let dividend = i32::MIN;
let dividends = i32x2(dividend, dividend);
let dividends = i32x2([dividend, dividend]);
let divisor = -1;
let divisors = i32x2(divisor, divisor);
let divisors = i32x2([divisor, divisor]);
let quotients = unsafe { do_simd_div(dividends, divisors) };
assert_eq!(quotients.0, quotients.1);
assert_eq!(quotients.0[0], quotients.0[1]);
}

#[kani::proof]
fn test_simd_rem_overflow() {
let dividend = i32::MIN;
let dividends = i32x2(dividend, dividend);
let dividends = i32x2([dividend, dividend]);
let divisor = -1;
let divisors = i32x2(divisor, divisor);
let divisors = i32x2([divisor, divisor]);
let remainders = unsafe { do_simd_rem(dividends, divisors) };
assert_eq!(remainders.0, remainders.1);
assert_eq!(remainders.0[0], remainders.0[1]);
}
4 changes: 2 additions & 2 deletions tests/expected/intrinsics/simd-extract-wrong-type/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,11 +10,11 @@ use std::intrinsics::simd::simd_extract;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i64x2(i64, i64);
pub struct i64x2([i64; 2]);

#[kani::proof]
fn main() {
let y = i64x2(0, 1);
let y = i64x2([0, 1]);
let res: i32 = unsafe { simd_extract(y, 1) };
// ^^^^ The code above fails to type-check in Rust with the error:
// ```
Expand Down
4 changes: 2 additions & 2 deletions tests/expected/intrinsics/simd-insert-wrong-type/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,11 +10,11 @@ use std::intrinsics::simd::simd_insert;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i64x2(i64, i64);
pub struct i64x2([i64; 2]);

#[kani::proof]
fn main() {
let y = i64x2(0, 1);
let y = i64x2([0, 1]);
let _ = unsafe { simd_insert(y, 0, 1) };
// ^^^^ The code above fails to type-check in Rust with the error:
// ```
Expand Down
6 changes: 3 additions & 3 deletions tests/expected/intrinsics/simd-rem-div-zero/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,13 +8,13 @@ use std::intrinsics::simd::simd_rem;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i32x2(i32, i32);
pub struct i32x2([i32; 2]);

#[kani::proof]
fn test_simd_rem() {
let dividend = kani::any();
let dividends = i32x2(dividend, dividend);
let dividends = i32x2([dividend, dividend]);
let divisor = 0;
let divisors = i32x2(divisor, divisor);
let divisors = i32x2([divisor, divisor]);
let _ = unsafe { simd_rem(dividends, divisors) };
}
14 changes: 7 additions & 7 deletions tests/expected/intrinsics/simd-result-type-is-float/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,31 +9,31 @@ use std::intrinsics::simd::simd_eq;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i64x2(i64, i64);
pub struct i64x2([i64; 2]);

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct u64x2(u64, u64);
pub struct u64x2([u64; 2]);

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct u32x4(u32, u32, u32, u32);
pub struct u32x4([u32; 4]);

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq)]
pub struct f32x2(f32, f32);
pub struct f32x2([f32; 2]);

#[kani::proof]
fn main() {
let x = u64x2(0, 0);
let y = u64x2(0, 1);
let x = u64x2([0, 0]);
let y = u64x2([0, 1]);

unsafe {
let invalid_simd: f32x2 = simd_eq(x, y);
assert!(invalid_simd == f32x2(0.0, -1.0));
assert!(invalid_simd == f32x2([0.0, -1.0]));
// ^^^^ The code above fails to type-check in Rust with the error:
// ```
// error[E0511]: invalid monomorphization of `simd_eq` intrinsic: expected return type with integer elements, found `f32x2` with non-integer `f32`
Expand Down
6 changes: 3 additions & 3 deletions tests/expected/intrinsics/simd-shl-shift-negative/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,14 +8,14 @@ use std::intrinsics::simd::simd_shl;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i32x2(i32, i32);
pub struct i32x2([i32; 2]);

#[kani::proof]
fn test_simd_shl() {
let value = kani::any();
let values = i32x2(value, value);
let values = i32x2([value, value]);
let shift = kani::any();
kani::assume(shift < 32);
let shifts = i32x2(shift, shift);
let shifts = i32x2([shift, shift]);
let _result = unsafe { simd_shl(values, shifts) };
}
6 changes: 3 additions & 3 deletions tests/expected/intrinsics/simd-shl-shift-too-large/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,14 +8,14 @@ use std::intrinsics::simd::simd_shl;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i32x2(i32, i32);
pub struct i32x2([i32; 2]);

#[kani::proof]
fn test_simd_shl() {
let value = kani::any();
let values = i32x2(value, value);
let values = i32x2([value, value]);
let shift = kani::any();
kani::assume(shift >= 0);
let shifts = i32x2(shift, shift);
let shifts = i32x2([shift, shift]);
let _result = unsafe { simd_shl(values, shifts) };
}
6 changes: 3 additions & 3 deletions tests/expected/intrinsics/simd-shr-shift-negative/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,14 +8,14 @@ use std::intrinsics::simd::simd_shr;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i32x2(i32, i32);
pub struct i32x2([i32; 2]);

#[kani::proof]
fn test_simd_shr() {
let value = kani::any();
let values = i32x2(value, value);
let values = i32x2([value, value]);
let shift = kani::any();
kani::assume(shift < 32);
let shifts = i32x2(shift, shift);
let shifts = i32x2([shift, shift]);
let _result = unsafe { simd_shr(values, shifts) };
}
6 changes: 3 additions & 3 deletions tests/expected/intrinsics/simd-shr-shift-too-large/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,14 +8,14 @@ use std::intrinsics::simd::simd_shr;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i32x2(i32, i32);
pub struct i32x2([i32; 2]);

#[kani::proof]
fn test_simd_shr() {
let value = kani::any();
let values = i32x2(value, value);
let values = i32x2([value, value]);
let shift = kani::any();
kani::assume(shift >= 0);
let shifts = i32x2(shift, shift);
let shifts = i32x2([shift, shift]);
let _result = unsafe { simd_shr(values, shifts) };
}
6 changes: 3 additions & 3 deletions tests/expected/intrinsics/simd-shuffle-indexes-out/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,12 +9,12 @@ use std::intrinsics::simd::simd_shuffle;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i64x2(i64, i64);
pub struct i64x2([i64; 2]);

#[kani::proof]
fn main() {
let y = i64x2(0, 1);
let z = i64x2(1, 2);
let y = i64x2([0, 1]);
let z = i64x2([1, 2]);
// Only [0, 3] are valid indexes, 4 is out of bounds
const I: [u32; 2] = [1, 4];
let _: i64x2 = unsafe { simd_shuffle(y, z, I) };
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,17 +9,17 @@ use std::intrinsics::simd::simd_shuffle;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i64x2(i64, i64);
pub struct i64x2([i64; 2]);

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq, Eq)]
pub struct i64x4(i64, i64, i64, i64);
pub struct i64x4([i64; 4]);

#[kani::proof]
fn main() {
let y = i64x2(0, 1);
let z = i64x2(1, 2);
let y = i64x2([0, 1]);
let z = i64x2([1, 2]);
const I: [u32; 4] = [1, 2, 1, 2];
let x: i64x2 = unsafe { simd_shuffle(y, z, I) };
// ^^^^ The code above fails to type-check in Rust with the error:
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,17 +9,17 @@ use std::intrinsics::simd::simd_shuffle;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq)]
pub struct i64x2(i64, i64);
pub struct i64x2([i64; 2]);

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq)]
pub struct f64x2(f64, f64);
pub struct f64x2([f64; 2]);

#[kani::proof]
fn main() {
let y = i64x2(0, 1);
let z = i64x2(1, 2);
let y = i64x2([0, 1]);
let z = i64x2([1, 2]);
const I: [u32; 2] = [1, 2];
let x: f64x2 = unsafe { simd_shuffle(y, z, I) };
// ^^^^ The code above fails to type-check in Rust with the error:
Expand Down
34 changes: 17 additions & 17 deletions tests/kani/Intrinsics/SIMD/Compare/float.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,17 +8,17 @@ use std::intrinsics::simd::*;
#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq)]
pub struct f64x2(f64, f64);
pub struct f64x2([f64; 2]);

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq)]
pub struct i64x2(i64, i64);
pub struct i64x2([i64; 2]);

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq)]
pub struct i32x2(i32, i32);
pub struct i32x2([i32; 2]);

macro_rules! assert_cmp {
($res_cmp: ident, $simd_cmp: ident, $x: expr, $y: expr, $($res: expr),+) => {
Expand All @@ -29,21 +29,21 @@ macro_rules! assert_cmp {

#[kani::proof]
fn main() {
let x = f64x2(0.0, 0.0);
let y = f64x2(0.0, 1.0);
let x = f64x2([0.0, 0.0]);
let y = f64x2([0.0, 1.0]);

unsafe {
assert_cmp!(res_eq, simd_eq, x, x, -1, -1);
assert_cmp!(res_eq, simd_eq, x, y, -1, 0);
assert_cmp!(res_ne, simd_ne, x, x, 0, 0);
assert_cmp!(res_ne, simd_ne, x, y, 0, -1);
assert_cmp!(res_lt, simd_lt, x, x, 0, 0);
assert_cmp!(res_lt, simd_lt, x, y, 0, -1);
assert_cmp!(res_le, simd_le, x, x, -1, -1);
assert_cmp!(res_le, simd_le, x, y, -1, -1);
assert_cmp!(res_gt, simd_gt, x, x, 0, 0);
assert_cmp!(res_gt, simd_gt, x, y, 0, 0);
assert_cmp!(res_ge, simd_ge, x, x, -1, -1);
assert_cmp!(res_ge, simd_ge, x, y, -1, 0);
assert_cmp!(res_eq, simd_eq, x, x, [-1, -1]);
assert_cmp!(res_eq, simd_eq, x, y, [-1, 0]);
assert_cmp!(res_ne, simd_ne, x, x, [0, 0]);
assert_cmp!(res_ne, simd_ne, x, y, [0, -1]);
assert_cmp!(res_lt, simd_lt, x, x, [0, 0]);
assert_cmp!(res_lt, simd_lt, x, y, [0, -1]);
assert_cmp!(res_le, simd_le, x, x, [-1, -1]);
assert_cmp!(res_le, simd_le, x, y, [-1, -1]);
assert_cmp!(res_gt, simd_gt, x, x, [0, 0]);
assert_cmp!(res_gt, simd_gt, x, y, [0, 0]);
assert_cmp!(res_ge, simd_ge, x, x, [-1, -1]);
assert_cmp!(res_ge, simd_ge, x, y, [-1, 0]);
}
}
Loading

0 comments on commit d2051b7

Please sign in to comment.