From 4987edbc0b17d283f3aba87d853ffe6cfae4f3bb Mon Sep 17 00:00:00 2001 From: Jonas Date: Fri, 22 Apr 2022 16:13:01 +0200 Subject: [PATCH 1/5] Fix slice encoding --- .../tests/verify/fail/issues/issue960-1.rs | 24 +++++++++ .../src/encoder/errors/error_manager.rs | 11 ++++ prusti-viper/src/encoder/procedure_encoder.rs | 53 +++++++++++++++---- 3 files changed, 79 insertions(+), 9 deletions(-) create mode 100644 prusti-tests/tests/verify/fail/issues/issue960-1.rs 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-viper/src/encoder/errors/error_manager.rs b/prusti-viper/src/encoder/errors/error_manager.rs index a228f82d012..83b30edf319 100644 --- a/prusti-viper/src/encoder/errors/error_manager.rs +++ b/prusti-viper/src/encoder/errors/error_manager.rs @@ -69,6 +69,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(...)` + HardcodedBoundsCheckAssert(String), /// A Viper `assert false` that encodes an `abort` Rust terminator AbortTerminator, /// A Viper `assert false` that encodes an `unreachable` Rust terminator @@ -565,6 +568,14 @@ impl<'tcx> ErrorManager<'tcx> { ).set_failing_assertion(opt_cause_span) } + ("assert.failed:assertion.false", ErrorCtxt::HardcodedBoundsCheckAssert(s)) | + ("application.precondition:assertion.false", ErrorCtxt::HardcodedBoundsCheckAssert(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 71fe16a9a6c..0dba6450410 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -2203,8 +2203,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"); @@ -2213,6 +2220,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { destination, args, location, + term.source_info.span, ).with_span(span)? ); } @@ -2406,6 +2414,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 @@ -2477,14 +2486,23 @@ 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)?; + // 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::HardcodedBoundsCheckAssert("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... @@ -2498,19 +2516,30 @@ 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)?; + // 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::HardcodedBoundsCheckAssert("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)] }; + // 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::HardcodedBoundsCheckAssert("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) }; @@ -2521,6 +2550,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { // length let length = vir_expr!{ [end] - [start] }; + // start must be leq than end + stmts.push(vir::Stmt::Assert( vir::Assert { + expr: vir_expr!{ [start] <= [end] }, + position: self.register_error(error_span, ErrorCtxt::HardcodedBoundsCheckAssert("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] }] From b23b42606fd62b46ea2a6f32346635bf978e605a Mon Sep 17 00:00:00 2001 From: Jonas Date: Fri, 22 Apr 2022 18:51:12 +0200 Subject: [PATCH 2/5] Mark test case as unsupported --- .../tests/verify_overflow/{pass => fail}/issues/issue-709-12.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) rename prusti-tests/tests/verify_overflow/{pass => fail}/issues/issue-709-12.rs (83%) 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 } } From 7ada33494d90e4d1ae54913dcaebc5f192778d69 Mon Sep 17 00:00:00 2001 From: Jonas Date: Tue, 26 Apr 2022 16:19:30 +0200 Subject: [PATCH 3/5] Review change --- prusti-viper/src/encoder/errors/error_manager.rs | 6 +++--- prusti-viper/src/encoder/procedure_encoder.rs | 8 ++++---- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/prusti-viper/src/encoder/errors/error_manager.rs b/prusti-viper/src/encoder/errors/error_manager.rs index 83b30edf319..b4b344c945a 100644 --- a/prusti-viper/src/encoder/errors/error_manager.rs +++ b/prusti-viper/src/encoder/errors/error_manager.rs @@ -71,7 +71,7 @@ pub enum ErrorCtxt { 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(...)` - HardcodedBoundsCheckAssert(String), + SliceRangeBoundsCheckAssert(String), /// A Viper `assert false` that encodes an `abort` Rust terminator AbortTerminator, /// A Viper `assert false` that encodes an `unreachable` Rust terminator @@ -568,8 +568,8 @@ impl<'tcx> ErrorManager<'tcx> { ).set_failing_assertion(opt_cause_span) } - ("assert.failed:assertion.false", ErrorCtxt::HardcodedBoundsCheckAssert(s)) | - ("application.precondition:assertion.false", ErrorCtxt::HardcodedBoundsCheckAssert(s)) => { + ("assert.failed:assertion.false", ErrorCtxt::SliceRangeBoundsCheckAssert(s)) | + ("application.precondition:assertion.false", ErrorCtxt::SliceRangeBoundsCheckAssert(s)) => { PrustiError::verification( s, error_span, diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index 0dba6450410..e124f378d6c 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -2499,7 +2499,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { // 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::HardcodedBoundsCheckAssert("the range start value may be smaller than 0 when slicing".to_string())), + position: self.register_error(error_span, ErrorCtxt::SliceRangeBoundsCheckAssert("the range start value may be smaller than 0 when slicing".to_string())), })); start_expr } @@ -2521,7 +2521,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { // 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::HardcodedBoundsCheckAssert("the range end value may be out of bounds when slicing".to_string())), + position: self.register_error(error_span, ErrorCtxt::SliceRangeBoundsCheckAssert("the range end value may be out of bounds when slicing".to_string())), })); end_expr } @@ -2534,7 +2534,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { // 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::HardcodedBoundsCheckAssert("the range end value may be out of bounds when slicing".to_string())), + position: self.register_error(error_span, ErrorCtxt::SliceRangeBoundsCheckAssert("the range end value may be out of bounds when slicing".to_string())), })); end_expr } @@ -2553,7 +2553,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { // start must be leq than end stmts.push(vir::Stmt::Assert( vir::Assert { expr: vir_expr!{ [start] <= [end] }, - position: self.register_error(error_span, ErrorCtxt::HardcodedBoundsCheckAssert("the range end may be smaller than the start when slicing".to_string())), + 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()); From 9efd402600eb05331dd517e4e9a55eeb59bc4d33 Mon Sep 17 00:00:00 2001 From: Jonas Date: Thu, 28 Apr 2022 17:13:47 +0200 Subject: [PATCH 4/5] Avoid check when full range --- prusti-viper/src/encoder/procedure_encoder.rs | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index e124f378d6c..d15498c6b7f 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -2551,10 +2551,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { // length let length = vir_expr!{ [end] - [start] }; // start must be leq than end - 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())), - })); + 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!{ From 3f6d4c8be1df121ce350941409114647eb6dd923 Mon Sep 17 00:00:00 2001 From: Jonas Date: Fri, 27 May 2022 12:30:11 +0200 Subject: [PATCH 5/5] Only check slicing bounds when check_panics enabled --- prusti-viper/src/encoder/procedure_encoder.rs | 50 +++++++++++-------- 1 file changed, 29 insertions(+), 21 deletions(-) diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index 5efbd0f746e..e914e6e9f92 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -2737,11 +2737,13 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { "std::ops::Range" | "core::ops::Range" | "std::ops::RangeFrom" | "core::ops::RangeFrom" => { let start_expr = self.encoder.encode_struct_field_value(encoded_idx.clone(), "start", usize_ty)?; - // 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())), - })); + 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 @@ -2759,11 +2761,13 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { "std::ops::Range" | "core::ops::Range" | "std::ops::RangeTo" | "core::ops::RangeTo" => { let end_expr = self.encoder.encode_struct_field_value(encoded_idx, "end", usize_ty)?; - // 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())), - })); + 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( @@ -2772,11 +2776,13 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { "std::ops::RangeToInclusive" | "core::ops::RangeToInclusive" => { let end_expr = self.encoder.encode_struct_field_value(encoded_idx, "end", usize_ty)?; let end_expr = vir_expr!{ [end_expr] + [vir::Expr::from(1usize)] }; - // 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())), - })); + 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" | @@ -2791,12 +2797,14 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { // length let length = vir_expr!{ [end] - [start] }; - // 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())), - })); + 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());