Add comment + improve tests

model-checking · Jul 29, 2023 · bc70aa5 · bc70aa5
1 parent f794fe5
commit bc70aa5
Show file tree

Hide file tree

Showing 3 changed files with 27 additions and 15 deletions.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
@@ -235,6 +235,11 @@ impl<'tcx> TypeOrVariant<'tcx> {
 }
 
 impl<'tcx> GotocCtx<'tcx> {
+    /// Codegen field access for types that allow direct field projection.
+    ///
+    /// I.e.: Algebraic data types, closures, and generators.
+    ///
+    /// Other composite types such as array only support index projection.
     fn codegen_field(
         &mut self,
         parent_expr: Expr,
@@ -255,13 +260,14 @@ impl<'tcx> GotocCtx<'tcx> {
                     | ty::Never
                     | ty::FnDef(..)
                     | ty::GeneratorWitness(..)
+                    | ty::GeneratorWitnessMIR(..)
                     | ty::Foreign(..)
                     | ty::Dynamic(..)
                     | ty::Bound(..)
                     | ty::Placeholder(..)
                     | ty::Param(_)
                     | ty::Infer(_)
-                    | ty::Error(_) => unreachable!("type {:?} does not have a field", parent_ty),
+                    | ty::Error(_) => unreachable!("type {parent_ty:?} does not have a field"),
                     ty::Tuple(_) => Ok(parent_expr
                         .member(&Self::tuple_fld_name(field.index()), &self.symbol_table)),
                     ty::Adt(def, _) if def.repr().simd() => Ok(self.codegen_simd_field(
@@ -283,7 +289,11 @@ impl<'tcx> GotocCtx<'tcx> {
                             .member("direct_fields", &self.symbol_table)
                             .member(field_name, &self.symbol_table))
                     }
-                    _ => unimplemented!(),
+                    ty::Str | ty::Array(_, _) | ty::Slice(_) | ty::RawPtr(_) | ty::Ref(_, _, _) => {
+                        unreachable!(
+                            "element of {parent_ty:?} is not accessed via field projection"
+                        )
+                    }
                 }
             }
             // if we fall here, then we are handling an enum

diff --git a/tests/kani/SIMD/array_simd_repr.rs b/tests/kani/SIMD/array_simd_repr.rs
@@ -1,12 +1,12 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-//! Verify that Kani can properly handle SIMD declared using array syntax.
+//! Verify that Kani can properly handle SIMD declaration and field access using array syntax.
 
 #![allow(non_camel_case_types)]
 #![feature(repr_simd)]
 
 #[repr(simd)]
-#[derive(PartialEq, Eq, kani::Arbitrary)]
+#[derive(Clone, PartialEq, Eq, PartialOrd, kani::Arbitrary)]
 pub struct i64x2([i64; 2]);
 
 #[kani::proof]
@@ -17,11 +17,11 @@ fn check_diff() {
 }
 
 #[kani::proof]
-fn check_nondet() {
+fn check_ge() {
     let x: i64x2 = kani::any();
-    let y: i64x2 = kani::any();
-    kani::cover!(x != y);
-    kani::cover!(x == y);
+    kani::assume(x.0[0] > 0);
+    kani::assume(x.0[1] > 0);
+    assert!(x > i64x2([0, 0]));
 }
 
 #[derive(Clone, Debug)]
@@ -30,5 +30,7 @@ struct CustomSimd<T, const LANES: usize>([T; LANES]);
 
 #[kani::proof]
 fn simd_vec() {
-    std::hint::black_box(CustomSimd([0u8; 10]));
+    let simd = CustomSimd([0u8; 10]);
+    let idx: usize = kani::any_where(|x: &usize| *x < 10);
+    assert_eq!(simd.0[idx], 0);
 }
diff --git a/tests/kani/SIMD/multi_field_simd.rs b/tests/kani/SIMD/multi_field_simd.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-//! Verify that Kani can properly handle SIMD declared using multi-field syntax.
+//! Verify that Kani can properly handle SIMD declaration and field access using multi-field syntax.
 //! Note: Multi-field SIMD is actually being deprecated, but until it's removed, we might
 //! as well keep supporting it.
 //! See <https://github.com/rust-lang/compiler-team/issues/621> for more details.
@@ -9,7 +9,7 @@
 #![feature(repr_simd)]
 
 #[repr(simd)]
-#[derive(PartialEq, Eq, kani::Arbitrary)]
+#[derive(PartialEq, Eq, PartialOrd, kani::Arbitrary)]
 pub struct i64x2(i64, i64);
 
 #[kani::proof]
@@ -20,9 +20,9 @@ fn check_diff() {
 }
 
 #[kani::proof]
-fn check_nondet() {
+fn check_ge() {
     let x: i64x2 = kani::any();
-    let y: i64x2 = kani::any();
-    kani::cover!(x != y);
-    kani::cover!(x == y);
+    kani::assume(x.0 > 0);
+    kani::assume(x.1 > 0);
+    assert!(x > i64x2(0, 0));
 }