Skip to content
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

Closed
vecchiot-aws opened this issue Aug 20, 2021 · 3 comments
Closed

Fix code generation for SIMD types #444

vecchiot-aws opened this issue Aug 20, 2021 · 3 comments

Comments

@vecchiot-aws
Copy link
Contributor

vecchiot-aws commented Aug 20, 2021

I'm not sure where in the translation process this should happen, but consider the following program:

#![feature(repr_simd)]

#[repr(simd)]
#[derive(PartialEq, Eq)]
pub struct A(i64, i64);

fn main() {
    let x = A(1, 2);
    let y = A(3, 4);
    assert!(x != y);
}

The generated C code from --gen-c does comparison like this:

_Bool _RNvXs_Csb7rQPrKk64Y_4mainNtB4_1ANtNtCs75dudyTCRYy_4core3cmp9PartialEq2neB4_(long int __attribute__((vector_size (2*sizeof(long int)))) *self, long int __attribute__((vector_size (2*sizeof(long int)))) *other)
{
  // ...
  long int *__self_1_0;
  long int *__self_1_1;
  long int *__self_0_0;
  long int *__self_0_1;
  // ...
  __self_1_0 = *other;
  __self_1_1 = &(*other)[1];
  __self_0_0 = *self;
  __self_0_1 = &(*self)[1];
  var_8 = *__self_0_0;
  var_9 = *__self_1_0;
  var_7 = var_8 != var_9;
  // ...
}

There are two main issues:

  1. __self_1_0 = *other;: the value *other is a vector type, while __self_1_0 is a long int*
  2. __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.

@tedinski
Copy link
Contributor

@adpaco-aws This is probably getting fixed now?

@adpaco-aws
Copy link
Contributor

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.

@celinval celinval changed the title Get CBMC to fix how SIMD vectors are codegenned. Fix code generation for SIMD types Nov 23, 2022
@celinval
Copy link
Contributor

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 --gen-c will have the following code:

// 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;                                                                                                                                                    
}  

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

4 participants