Fix code generation for SIMD types

[vecchiot-aws]

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]

@adpaco-aws This is probably getting fixed now?

[adpaco-aws]

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]

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