Fix slice with range encoding

prusti-tests/tests/verify/fail/issues/issue960-1.rs

@@ -0,0 +1,24 @@
+use prusti_contracts::*;
+
+
+#[requires(end <= slice.len())]
+fn foo(slice: &[i32], start: usize, end: usize) {
+    let subslice = &slice[start..end]; //~ ERROR the range end may be smaller than the start when slicing
+}
+
+#[requires(start <= end)]
+fn bar(slice: &[i32], start: usize, end: usize) {
+    let subslice = &slice[start..end]; //~ ERROR the range end value may be out of bounds when slicing
+}
+
+#[requires(end <= slice.len())]
+fn foo_mut(slice: &mut [i32], start: usize, end: usize) {
+    let subslice = &mut slice[start..end]; //~ ERROR mutably slicing is not fully supported yet
+}
+
+#[requires(start <= end)]
+fn bar_mut(slice: &mut [i32], start: usize, end: usize) {
+    let subslice = &mut slice[start..end]; //~ ERROR mutably slicing is not fully supported yet
+}
+
+fn main() {}

prusti-tests/tests/verify_overflow/pass/issues/issue-709-12.rs → prusti-tests/tests/verify_overflow/fail/issues/issue-709-12.rs

@@ -12,7 +12,7 @@ impl B {
     #[requires(index <= self.0.len())]
     #[ensures(result.len() == index)]
     pub fn get_mut(&mut self, index: usize) -> &mut [A] {
-        &mut self.0[0..index]
+        &mut self.0[0..index] //~ ERROR mutably slicing is not fully supported yet
     }
 }
 

prusti-viper/src/encoder/errors/error_manager.rs

@@ -73,6 +73,9 @@ pub enum ErrorCtxt {
     AssertTerminator(String),
     /// A Viper `assert false` in the context of a bounds check
     BoundsCheckAssert,
+    /// A Viper `assert false` in the context of a hardcoded bounds check (e.g. when we hardcode a `index`)
+    /// TODO: remove this in favor of extern_spec for e.g. the stdlib `fn index(...)`
+    SliceRangeBoundsCheckAssert(String),
     /// A Viper `assert false` that encodes an `abort` Rust terminator
     AbortTerminator,
     /// A Viper `assert false` that encodes an `unreachable` Rust terminator
@@ -591,6 +594,14 @@ impl<'tcx> ErrorManager<'tcx> {
                 ).set_failing_assertion(opt_cause_span)
             }
 
+            ("assert.failed:assertion.false", ErrorCtxt::SliceRangeBoundsCheckAssert(s)) |
+            ("application.precondition:assertion.false", ErrorCtxt::SliceRangeBoundsCheckAssert(s)) => {
+                PrustiError::verification(
+                    s,
+                    error_span,
+                ).set_failing_assertion(opt_cause_span)
+            }
+
             ("assert.failed:assertion.false", ErrorCtxt::Unsupported(ref reason)) => {
                 PrustiError::unsupported(
                     format!("an unsupported Rust feature might be reachable: {}.", reason),

prusti-viper/src/encoder/procedure_encoder.rs

@@ -2446,8 +2446,15 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                             ));
                         }
 
+                        // TODO: use extern_spec
                         "core::ops::IndexMut::index_mut" |
-                        "std::ops::IndexMut::index_mut" |
+                        "std::ops::IndexMut::index_mut" => {
+                            return Err(SpannedEncodingError::unsupported(
+                                "mutably slicing is not fully supported yet",
+                                term.source_info.span,
+                            ));
+                        }
+
                         "core::ops::Index::index" |
                         "std::ops::Index::index" => {
                             debug!("Encoding call of array/slice index call");
@@ -2456,6 +2463,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                                     destination,
                                     args,
                                     location,
+                                    term.source_info.span,
                                 ).with_span(span)?
                             );
                         }
@@ -2649,6 +2657,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         destination: &Option<(mir::Place<'tcx>, BasicBlockIndex)>,
         args: &[mir::Operand<'tcx>],
         location: mir::Location,
+        error_span: Span
     ) -> EncodingResult<Vec<vir::Stmt>> {
         trace!("encode_sequence_index_call(destination={:?}, args={:?})", destination, args);
         // args[0] is the base array/slice, args[1] is the index
@@ -2718,14 +2727,25 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
 
         self.slice_created_at.insert(location, encoded_lhs);
 
+        let original_len = enc_sequence_types.len(self.encoder, base_seq_expr);
+
         // TODO: there's fields like _5.f$start.val_int on `encoded_idx`, it just feels hacky to
         // manually re-do and hardcode them here when we probably just encoded the type
         // and the construction of the fields.
         let usize_ty = self.encoder.env().tcx().mk_ty(ty::TyKind::Uint(ty::UintTy::Usize));
         let start = match &*idx_ident {
             "std::ops::Range" | "core::ops::Range" |
-            "std::ops::RangeFrom" | "core::ops::RangeFrom" =>
-                self.encoder.encode_struct_field_value(encoded_idx.clone(), "start", usize_ty)?,
+            "std::ops::RangeFrom" | "core::ops::RangeFrom" => {
+                let start_expr = self.encoder.encode_struct_field_value(encoded_idx.clone(), "start", usize_ty)?;
+                if self.check_panics {
+                    // Check indexing in bounds
+                    stmts.push(vir::Stmt::Assert( vir::Assert {
+                        expr: vir_expr!{ [start_expr] >= [vir::Expr::from(0usize)] },
+                        position: self.register_error(error_span, ErrorCtxt::SliceRangeBoundsCheckAssert("the range start value may be smaller than 0 when slicing".to_string())),
+                    }));
+                }
+                start_expr
+            }
             // RangeInclusive is wierdly differnet to all of the other Range*s in that the struct fields are private
             // and it is created with a new() fn and start/end are accessed with getter fns
             // See https://github.com/rust-lang/rust/issues/67371 for why this is the case...
@@ -2739,19 +2759,34 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
         };
         let end = match &*idx_ident {
             "std::ops::Range" | "core::ops::Range" |
-            "std::ops::RangeTo" | "core::ops::RangeTo" =>
-                self.encoder.encode_struct_field_value(encoded_idx, "end", usize_ty)?,
+            "std::ops::RangeTo" | "core::ops::RangeTo" => {
+                let end_expr = self.encoder.encode_struct_field_value(encoded_idx, "end", usize_ty)?;
+                if self.check_panics {
+                    // Check indexing in bounds
+                    stmts.push(vir::Stmt::Assert( vir::Assert {
+                        expr: vir_expr!{ [end_expr] <= [original_len] },
+                        position: self.register_error(error_span, ErrorCtxt::SliceRangeBoundsCheckAssert("the range end value may be out of bounds when slicing".to_string())),
+                    }));
+                }
+                end_expr
+            }
             "std::ops::RangeInclusive" | "core::ops::RangeInclusive" => return Err(
                 EncodingError::unsupported("slicing with RangeInclusive (e.g. [x..=y]) currently not supported".to_string())
             ),
             "std::ops::RangeToInclusive" | "core::ops::RangeToInclusive" => {
                 let end_expr = self.encoder.encode_struct_field_value(encoded_idx, "end", usize_ty)?;
-                vir_expr!{ [end_expr] + [vir::Expr::from(1usize)] }
+                let end_expr = vir_expr!{ [end_expr] + [vir::Expr::from(1usize)] };
+                if self.check_panics {
+                    // Check indexing in bounds
+                    stmts.push(vir::Stmt::Assert( vir::Assert {
+                        expr: vir_expr!{ [end_expr] <= [original_len] },
+                        position: self.register_error(error_span, ErrorCtxt::SliceRangeBoundsCheckAssert("the range end value may be out of bounds when slicing".to_string())),
+                    }));
+                }
+                end_expr
             }
             "std::ops::RangeFrom" | "core::ops::RangeFrom" |
-            "std::ops::RangeFull" | "core::ops::RangeFull" => {
-                enc_sequence_types.len(self.encoder, base_seq_expr)
-            }
+            "std::ops::RangeFull" | "core::ops::RangeFull" => original_len,
             _ => unreachable!("{}", idx_ident)
         };
 
@@ -2762,6 +2797,16 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
 
         // length
         let length = vir_expr!{ [end] - [start] };
+        if self.check_panics {
+            // start must be leq than end
+            if idx_ident != "std::ops::RangeFull" && idx_ident != "core::ops::RangeFull" {
+                stmts.push(vir::Stmt::Assert( vir::Assert {
+                    expr: vir_expr!{ [start] <= [end] },
+                    position: self.register_error(error_span, ErrorCtxt::SliceRangeBoundsCheckAssert("the range end may be smaller than the start when slicing".to_string())),
+                }));
+            }
+        }
+
         let slice_len_call = slice_types_lhs.len(self.encoder, lhs_slice_expr.clone());
         stmts.push(vir_stmt!{
             inhale [vir_expr!{ [slice_len_call] == [length] }]