-
Notifications
You must be signed in to change notification settings - Fork 105
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Fix code generation for SIMD types #444
Comments
@adpaco-aws This is probably getting fixed now? |
This isn't related to adding support for SIMD intrinsics, but I agree it should be fixed. However, it's not clear to me what "should be fixed at the CBMC level" means here, this appears to be an issue with how codegen SIMD types. I haven't seen "address of vector element requested" show up in our tests, but I've seen other pointer-related properties. |
I just double checked, and everything seems correct. For this code: #![allow(non_camel_case_types)]
#![feature(repr_simd)]
#[repr(simd)]
#[derive(PartialEq, Eq, kani::Arbitrary)]
pub struct i64x2(i64, i64);
#[kani::proof]
fn check_diff() {
let x = i64x2(1, 2);
let y = i64x2(3, 4);
assert!(x != y);
} Kani verification result is correct, and the // check_diff
// file /home/ANT.AMAZON.COM/celinval/workspace/kani-project/kani/tests/kani/SIMD/multi_field_simd.rs line 18 column 1 function check_diff
struct () check_diff(void)
{
struct () var_0;
long int __attribute__((vector_size (2*sizeof(long int)))) x;
long int __attribute__((vector_size (2*sizeof(long int)))) y;
struct () var_3;
_Bool var_4;
_Bool var_5;
_Bool var_6;
long int __attribute__((vector_size (2*sizeof(long int)))) *var_7;
long int __attribute__((vector_size (2*sizeof(long int)))) *var_8;
bb0:
;
x = (long int __attribute__((vector_size (2*sizeof(long int))))){ 1, 2 };
y = (long int __attribute__((vector_size (2*sizeof(long int))))){ 3, 4 };
var_7 = &x;
var_8 = &y;
var_6=<i64x2 as std::cmp::PartialEq>::ne(var_7, var_8);
bb1:
;
var_5 = !(var_6 != 0);
var_4 = !(var_5 != 0);
/* KANI_CHECK_ID_multi_field_simd.974260c9fb978643::multi_field_simd_0 */
assert(0);
__CPROVER_bool temp_0=var_4 != 0;
/* [KANI_CHECK_ID_multi_field_simd.974260c9fb978643::multi_field_simd_0] assertion failed: x != y */
assert(temp_0);
__CPROVER_assume(temp_0);
goto bb2;
bb2:
;
return Void();
}
// <i64x2 as std::cmp::PartialEq>::ne
// file /home/ANT.AMAZON.COM/celinval/.rustup/toolchains/nightly-2023-06-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs line 226 column 5 function <i64x2 as std::cmp::PartialEq>::ne
_Bool <i64x2 as std::cmp::PartialEq>::ne(long int __attribute__((vector_size (2*sizeof(long int)))) *self, long int __attribute__((vector_size (2*sizeof(long int))
)) *other)
{
_Bool var_0;
bb0:
;
_Bool var_3=<i64x2 as std::cmp::PartialEq>::eq(self, other);
bb1:
;
var_0 = !(var_3 != 0);
return var_0;
}
// <i64x2 as std::cmp::PartialEq>::eq
// file /home/ANT.AMAZON.COM/celinval/workspace/kani-project/kani/tests/kani/SIMD/multi_field_simd.rs line 14 column 10 function <i64x2 as std::cmp::PartialEq>::eq
_Bool <i64x2 as std::cmp::PartialEq>::eq(long int __attribute__((vector_size (2*sizeof(long int)))) *self, long int __attribute__((vector_size (2*sizeof(long int))
)) *other)
{
_Bool var_0;
_Bool var_3;
long int var_4;
long int var_5;
_Bool var_6;
long int var_7;
long int var_8;
bb0:
;
var_4 = (*self)[0];
var_5 = (*other)[0];
var_3 = var_4 == var_5;
if(!(var_3 == 0))
goto bb2;
bb1:
;
var_0 = 0;
goto bb3;
bb2:
;
var_7 = (*self)[1];
var_8 = (*other)[1];
var_6 = var_7 == var_8;
var_0 = var_6;
bb3:
;
return var_0;
} |
I'm not sure where in the translation process this should happen, but consider the following program:
The generated C code from
--gen-c
does comparison like this:There are two main issues:
__self_1_0 = *other;
: the value*other
is a vector type, while__self_1_0
is along int*
__self_1_1 = &(*other)[1];
: this leads to "address of vector element requested"; you cannot take reference to a vector element in C.No longer relevant:
The--gen-c-runnable
transformation handles this by casting the vector to a raw pointer and using array indexing, but long-term this should be fixed at the CBMC level.The text was updated successfully, but these errors were encountered: