diff --git a/prusti-tests/tests/verify/fail/issues/issue960-1.rs b/prusti-tests/tests/verify/fail/issues/issue960-1.rs new file mode 100644 index 00000000000..aa8f1f70253 --- /dev/null +++ b/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() {} \ No newline at end of file diff --git a/prusti-tests/tests/verify_overflow/pass/issues/issue-709-12.rs b/prusti-tests/tests/verify_overflow/fail/issues/issue-709-12.rs similarity index 83% rename from prusti-tests/tests/verify_overflow/pass/issues/issue-709-12.rs rename to prusti-tests/tests/verify_overflow/fail/issues/issue-709-12.rs index 99064bb9111..e7b9a02384b 100644 --- a/prusti-tests/tests/verify_overflow/pass/issues/issue-709-12.rs +++ b/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 } } diff --git a/prusti-viper/src/encoder/errors/error_manager.rs b/prusti-viper/src/encoder/errors/error_manager.rs index 78564fbbf90..350054a9ecf 100644 --- a/prusti-viper/src/encoder/errors/error_manager.rs +++ b/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), diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index 25f0b4c8fcd..e914e6e9f92 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/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> { 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] }]