From 575c31928780fce3ae96dc06c090c6df07ad1423 Mon Sep 17 00:00:00 2001 From: Johannes Schilling Date: Mon, 3 May 2021 12:57:19 +0200 Subject: [PATCH 1/3] Update to nightly-2021-05-03 --- Cargo.lock | 8 ++++---- rust-toolchain | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 5a4201152fa..c6ee51cac7f 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2108,9 +2108,9 @@ dependencies = [ [[package]] name = "regex" -version = "1.5.2" +version = "1.5.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1efb2352a0f4d4b128f734b5c44c79ff80117351138733f12f982fe3e2b13343" +checksum = "ce5f1ceb7f74abbce32601642fcf8e8508a8a8991e0621c7d750295b9095702b" dependencies = [ "aho-corasick", "memchr", @@ -2128,9 +2128,9 @@ dependencies = [ [[package]] name = "regex-syntax" -version = "0.6.24" +version = "0.6.25" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "00efb87459ba4f6fb2169d20f68565555688e1250ee6825cdf6254f8b48fafb2" +checksum = "f497285884f3fcff424ffc933e56d7cbca511def0c9831a7f9b5f6153e3cc89b" [[package]] name = "remove_dir_all" diff --git a/rust-toolchain b/rust-toolchain index 1ea10b4745a..9ad01c49ede 100644 --- a/rust-toolchain +++ b/rust-toolchain @@ -1,4 +1,4 @@ [toolchain] -channel = "nightly-2021-05-01" +channel = "nightly-2021-05-03" components = [ "rustc-dev", "llvm-tools-preview" ] profile = "minimal" From b27f307174e9117bc1cd0c603d33dfd0433bdf14 Mon Sep 17 00:00:00 2001 From: Johannes Schilling Date: Mon, 3 May 2021 12:38:29 +0200 Subject: [PATCH 2/3] Use AssertKind::fmt_assert_args now that it's pub See https://github.com/viperproject/prusti-dev/pull/467 and https://github.com/rust-lang/rust/pull/84392 for context. --- prusti-viper/src/encoder/procedure_encoder.rs | 10 ++-------- prusti-viper/src/encoder/pure_function_encoder.rs | 11 +++-------- 2 files changed, 5 insertions(+), 16 deletions(-) diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index bceb6bc06b1..2dfade294fb 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -2158,14 +2158,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { }; // Check or assume the assertion - let assert_msg = if let AssertKind::BoundsCheck{ .. } = msg { - // Use the debug impl for BoundsCheck, as it is supposed to be handled before - // calling display() according to the docs - // TODO: use fmt_assert_args once https://github.com/rust-lang/rust/pull/84392 is merged - format!("{:?}", msg) - } else { - msg.description().to_string() - }; + let mut assert_msg = String::new(); + msg.fmt_assert_args(&mut assert_msg).unwrap(); stmts.push(vir::Stmt::comment(format!("Rust assertion: {}", assert_msg))); if self.check_panics { diff --git a/prusti-viper/src/encoder/pure_function_encoder.rs b/prusti-viper/src/encoder/pure_function_encoder.rs index 12ddcf21b9d..ddde6fe8f06 100644 --- a/prusti-viper/src/encoder/pure_function_encoder.rs +++ b/prusti-viper/src/encoder/pure_function_encoder.rs @@ -948,14 +948,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx> vir::Expr::not(cond_val) }; - let assert_msg = if let mir::AssertKind::BoundsCheck{ .. } = msg { - // Use the debug impl for BoundsCheck, as it is supposed to be handled before - // calling display() according to the docs - // TODO: use fmt_assert_args once https://github.com/rust-lang/rust/pull/84392 is merged - format!("{:?}", msg) - } else { - msg.description().to_string() - }; + let mut assert_msg = String::new(); + msg.fmt_assert_args(&mut assert_msg).unwrap(); + let pos = self.encoder.error_manager().register( term.source_info.span, ErrorCtxt::PureFunctionAssertTerminator(assert_msg), From 3bea86ec3fd2283707a9f58e32a9c53ec0684514 Mon Sep 17 00:00:00 2001 From: Johannes Schilling Date: Mon, 3 May 2021 14:51:00 +0200 Subject: [PATCH 3/3] Only use fmt_assert_msg for BoundsCheck The `description` method still gives nicer errors for everything else. --- prusti-viper/src/encoder/procedure_encoder.rs | 9 +++++++-- prusti-viper/src/encoder/pure_function_encoder.rs | 9 +++++++-- 2 files changed, 14 insertions(+), 4 deletions(-) diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index 2dfade294fb..adf7192ba41 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -2158,8 +2158,13 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { }; // Check or assume the assertion - let mut assert_msg = String::new(); - msg.fmt_assert_args(&mut assert_msg).unwrap(); + let assert_msg = if let mir::AssertKind::BoundsCheck { .. } = msg { + let mut s = String::new(); + msg.fmt_assert_args(&mut s).unwrap(); + s + } else { + msg.description().to_string() + }; stmts.push(vir::Stmt::comment(format!("Rust assertion: {}", assert_msg))); if self.check_panics { diff --git a/prusti-viper/src/encoder/pure_function_encoder.rs b/prusti-viper/src/encoder/pure_function_encoder.rs index ddde6fe8f06..db33409be74 100644 --- a/prusti-viper/src/encoder/pure_function_encoder.rs +++ b/prusti-viper/src/encoder/pure_function_encoder.rs @@ -948,8 +948,13 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx> vir::Expr::not(cond_val) }; - let mut assert_msg = String::new(); - msg.fmt_assert_args(&mut assert_msg).unwrap(); + let assert_msg = if let mir::AssertKind::BoundsCheck { .. } = msg { + let mut s = String::new(); + msg.fmt_assert_args(&mut s).unwrap(); + s + } else { + msg.description().to_string() + }; let pos = self.encoder.error_manager().register( term.source_info.span,