Partial support for subslice projection (rust-lang#452)

* Partial support for subslice pattern

* Added two tests for sub-slices

* Added fixme to broken test

* Add copyright notice in tests

* Add comments linking to full support issue

* Remove `dbg` macros

* Use `ssize_t` for index

Co-authored-by: Zyad Hassan <zyadh@amazon.com>

Author: 2 people

Diff for: compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/place.rs

@@ -6,10 +6,12 @@
 //! in [codegen_place] below.
 
 use crate::gotoc::cbmc::goto_program::{Expr, Type};
+use crate::gotoc::mir_to_goto::utils::slice_fat_ptr;
 use crate::gotoc::mir_to_goto::GotocCtx;
+use rustc_hir::Mutability;
 use rustc_middle::{
     mir::{Field, Local, Place, ProjectionElem},
-    ty::{self, Ty, TyS, VariantDef},
+    ty::{self, Ty, TyS, TypeAndMut, VariantDef},
 };
 use rustc_target::abi::{LayoutOf, TagEncoding, Variants};
 use tracing::{debug, warn};
@@ -357,7 +359,46 @@ impl<'tcx> GotocCtx<'tcx> {
             ProjectionElem::ConstantIndex { offset, min_length, from_end } => {
                 self.codegen_constant_index(before, offset, min_length, from_end)
             }
-            ProjectionElem::Subslice { .. } => unimplemented!(),
+            // Best effort to codegen subslice projection.
+            // This is known to fail with a CBMC invariant violation
+            // in some cases. Full support to be added in
+            // https://github.com/model-checking/rmc/issues/357
+            ProjectionElem::Subslice { from, to, from_end } => {
+                // https://rust-lang.github.io/rfcs/2359-subslice-pattern-syntax.html
+                match before.mir_typ().kind() {
+                    ty::Array(..) => unimplemented!(),
+                    ty::Slice(elemt) => {
+                        let len = if from_end {
+                            let olen = before
+                                .fat_ptr_goto_expr
+                                .clone()
+                                .unwrap()
+                                .member("len", &self.symbol_table);
+                            let sum = Expr::int_constant(to + from, Type::size_t());
+                            olen.sub(sum) // olen - (to + from) = olen - to - from
+                        } else {
+                            Expr::int_constant(to - from, Type::size_t())
+                        };
+                        let typ = self.tcx.mk_slice(elemt);
+                        let typ_and_mut = TypeAndMut { ty: typ, mutbl: Mutability::Mut };
+                        let ptr_typ = self.tcx.mk_ptr(typ_and_mut);
+                        let goto_type = self.codegen_ty(ptr_typ);
+
+                        let index = Expr::int_constant(from, Type::ssize_t());
+                        let from_elem = before.goto_expr.index(index);
+                        let data = from_elem.address_of();
+                        let fat_ptr = slice_fat_ptr(goto_type, data, len, &self.symbol_table);
+                        ProjectedPlace::new(
+                            fat_ptr.clone(),
+                            TypeOrVariant::Type(ptr_typ),
+                            Some(fat_ptr),
+                            Some(ptr_typ),
+                            self,
+                        )
+                    }
+                    _ => unreachable!("must be array or slice"),
+                }
+            }
             ProjectionElem::Downcast(_, idx) => {
                 // downcast converts a variable of an enum type to one of its discriminated cases
                 let t = before.mir_typ();

Diff for: compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/rvalue.rs

@@ -109,6 +109,11 @@ impl<'tcx> GotocCtx<'tcx> {
          * Construct a fat pointer to the value of this place
          */
 
+        // skip constructing a fat ptr if this place is already one
+        if place_goto_expr.typ().is_rust_fat_ptr(&self.symbol_table) {
+            return place_goto_expr;
+        }
+
         // In the sequence of projections leading to this place, we dereferenced
         // this fat pointer.
         let intermediate_fat_pointer = projection.fat_ptr_goto_expr.unwrap();

Diff for: src/test/cbmc/SubSlice/subslice1.rs

@@ -0,0 +1,9 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+fn main() {
+    let arr = [1, 2, 3];
+    // s is a slice (&[i32])
+    let [s @ ..] = &arr[..];
+    assert!(s[0] == 1);
+    assert!(s[1] == 2);
+}

Diff for: src/test/cbmc/SubSlice/subslice2_fixme.rs

@@ -0,0 +1,39 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// At present, this test fails with a CBMC invariant violation:
+//
+// Invariant check failed
+// File: ../src/solvers/flattening/boolbv_add_sub.cpp:68 function: convert_add_sub
+// Condition: it->type() == type
+// Reason: add/sub with mixed types:
+// +
+//   * type: signedbv
+//       * width: 64
+//       * #c_type: signed_long_int
+//   0: constant
+//       * type: signedbv
+//           * width: 64
+//           * #c_type: signed_long_int
+//       * value: 1
+//   1: constant
+//       * type: unsignedbv
+//           * #source_location:
+//             * file: <built-in-additions>
+//             * line: 1
+//             * working_directory: /home/ubuntu/rmc-rebase
+//           * width: 64
+//           * #typedef: __CPROVER_size_t
+//           * #c_type: unsigned_long_int
+//       * value: 1
+//
+// Full support for subslice projection to be added in
+// https://github.com/model-checking/rmc/issues/357
+
+fn main() {
+    let arr = [1, 2, 3];
+    // s is a slice (&[i32])
+    let [s @ ..] = &arr[1..];
+    assert!(s[0] == 2);
+    assert!(s[1] == 3);
+}