prusti-dev
prusti-dev copied to clipboard
viperproject
encode_bitvectors not working with generics instantiated to u32
Hi,
I'm trying to verify a piece of code using the volatile crate:
struct Example {
a: Volatile<u32>,
b: Volatile<u32>
}
impl Example {
#[ensures(self.a.read() & 1 == 1)]
fn check(&self) {
while self.a.read() & 1 == 0 {}
}
}
#[extern_spec]
impl<T: Copy> Volatile<T> {
#[pure]
pub fn new(value: T) -> Volatile<T>;
#[pure]
pub fn read(&self) -> T;
pub fn write(&mut self, value: T);
}
The same code without volatile can be verified:
struct Example {
a: u32,
b: u32
}
impl Example {
#[ensures(self.a & 1 == 1)]
fn check(&self) {
while self.a & 1 == 0 {}
}
}
Full Output:
Run verification on /home/ramla/Desktop/prusti-test/src/main.rs...
Preparing verification run #1.
Killing 0 processes.
Run command '/home/ramla/prusti-dev/target/release/cargo-prusti --message-format=json'
Spawned PID: 6728
Output from '/home/ramla/prusti-dev/target/release/cargo-prusti --message-format=json' (6.5s):
┌──── Begin stdout ────┐
{"reason":"compiler-artifact","package_id":"volatile 0.2.7 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/volatile-0.2.7/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"volatile","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/volatile-0.2.7/src/lib.rs","edition":"2015","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":2,"debug_assertions":true,"overflow_checks":true,"test":false},"features":[],"filenames":["/home/ramla/Desktop/prusti-test/target/verify/debug/deps/libvolatile-78762e6d622c4864.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-message","package_id":"prusti-test 0.1.0 (path+file:///home/ramla/Desktop/prusti-test)","manifest_path":"/home/ramla/Desktop/prusti-test/Cargo.toml","target":{"kind":["bin"],"crate_types":["bin"],"name":"prusti-test","src_path":"/home/ramla/Desktop/prusti-test/src/main.rs","edition":"2021","doc":true,"doctest":false,"test":true},"message":{"rendered":"warning: unused variable: `vec1`\n --> src/main.rs:268:9\n |\n268 | let vec1: Vec<u32> = Vec::new();\n | ^^^^ help: if this is intentional, prefix it with an underscore: `_vec1`\n |\n = note: `#[warn(unused_variables)]` on by default\n\n","children":[{"children":[],"code":null,"level":"note","message":"`#[warn(unused_variables)]` on by default","rendered":null,"spans":[]},{"children":[],"code":null,"level":"help","message":"if this is intentional, prefix it with an underscore","rendered":null,"spans":[{"byte_end":6813,"byte_start":6809,"column_end":13,"column_start":9,"expansion":null,"file_name":"src/main.rs","is_primary":true,"label":null,"line_end":268,"line_start":268,"suggested_replacement":"_vec1","suggestion_applicability":"MachineApplicable","text":[{"highlight_end":13,"highlight_start":9,"text":" let vec1: Vec<u32> = Vec::new();"}]}]}],"code":{"code":"unused_variables","explanation":null},"level":"warning","message":"unused variable: `vec1`","spans":[{"byte_end":6813,"byte_start":6809,"column_end":13,"column_start":9,"expansion":null,"file_name":"src/main.rs","is_primary":true,"label":null,"line_end":268,"line_start":268,"suggested_replacement":null,"suggestion_applicability":null,"text":[{"highlight_end":13,"highlight_start":9,"text":" let vec1: Vec<u32> = Vec::new();"}]}]}}
{"reason":"compiler-message","package_id":"prusti-test 0.1.0 (path+file:///home/ramla/Desktop/prusti-test)","manifest_path":"/home/ramla/Desktop/prusti-test/Cargo.toml","target":{"kind":["bin"],"crate_types":["bin"],"name":"prusti-test","src_path":"/home/ramla/Desktop/prusti-test/src/main.rs","edition":"2021","doc":true,"doctest":false,"test":true},"message":{"rendered":"warning: field is never read: `b`\n --> src/main.rs:243:5\n |\n243 | b: Volatile<u32>\n | ^^^^^^^^^^^^^^^^\n |\n = note: `#[warn(dead_code)]` on by default\n\n","children":[{"children":[],"code":null,"level":"note","message":"`#[warn(dead_code)]` on by default","rendered":null,"spans":[]}],"code":{"code":"dead_code","explanation":null},"level":"warning","message":"field is never read: `b`","spans":[{"byte_end":6474,"byte_start":6458,"column_end":21,"column_start":5,"expansion":null,"file_name":"src/main.rs","is_primary":true,"label":null,"line_end":243,"line_start":243,"suggested_replacement":null,"suggestion_applicability":null,"text":[{"highlight_end":21,"highlight_start":5,"text":" b: Volatile<u32>"}]}]}}
{"reason":"compiler-message","package_id":"prusti-test 0.1.0 (path+file:///home/ramla/Desktop/prusti-test)","manifest_path":"/home/ramla/Desktop/prusti-test/Cargo.toml","target":{"kind":["bin"],"crate_types":["bin"],"name":"prusti-test","src_path":"/home/ramla/Desktop/prusti-test/src/main.rs","edition":"2021","doc":true,"doctest":false,"test":true},"message":{"rendered":"warning: associated function is never used: `check`\n --> src/main.rs:248:8\n |\n248 | fn check(&self) {\n | ^^^^^\n\n","children":[],"code":{"code":"dead_code","explanation":null},"level":"warning","message":"associated function is never used: `check`","spans":[{"byte_end":6544,"byte_start":6539,"column_end":13,"column_start":8,"expansion":null,"file_name":"src/main.rs","is_primary":true,"label":null,"line_end":248,"line_start":248,"suggested_replacement":null,"suggestion_applicability":null,"text":[{"highlight_end":13,"highlight_start":8,"text":" fn check(&self) {"}]}]}}
{"reason":"compiler-message","package_id":"prusti-test 0.1.0 (path+file:///home/ramla/Desktop/prusti-test)","manifest_path":"/home/ramla/Desktop/prusti-test/Cargo.toml","target":{"kind":["bin"],"crate_types":["bin"],"name":"prusti-test","src_path":"/home/ramla/Desktop/prusti-test/src/main.rs","edition":"2021","doc":true,"doctest":false,"test":true},"message":{"rendered":"warning: 3 warnings emitted\n\n","children":[],"code":null,"level":"warning","message":"3 warnings emitted","spans":[]}}
{"reason":"build-finished","success":false}
└──── End stdout ──────┘
┌──── Begin stderr ────┐
Checking prusti-test v0.1.0 (/home/ramla/Desktop/prusti-test)
[2022-05-05T20:37:24Z INFO prusti_driver] Prusti version: commit 81366ed155 2022-04-26 16:24:52 UTC, built on 2022-04-27 14:54:02 UTC
[2022-05-05T20:37:24Z INFO prusti_viper::verifier] Received 3 functions to be verified:
[2022-05-05T20:37:24Z INFO prusti_common::stopwatch::log_level] [prusti-viper] Starting: encoding to Viper
[2022-05-05T20:37:24Z INFO prusti_viper::verifier] - main (prusti_test::main)
[2022-05-05T20:37:24Z INFO prusti_viper::verifier] Source: src/main.rs:267:1: 267:10 (#0)
[2022-05-05T20:37:24Z INFO prusti_viper::verifier] - max (prusti_test::max)
[2022-05-05T20:37:24Z INFO prusti_viper::verifier] Source: src/main.rs:228:1: 228:30 (#0)
[2022-05-05T20:37:24Z INFO prusti_viper::verifier] - Example::check (prusti_test::{impl#0}::check)
[2022-05-05T20:37:24Z INFO prusti_viper::verifier] Source: src/main.rs:248:5: 248:20 (#0)
[2022-05-05T20:37:24Z INFO prusti_viper::encoder::encoder] Encoding: prusti_test::main (prusti_test::main)
[2022-05-05T20:37:24Z INFO prusti_viper::encoder::encoder] Encoding: prusti_test::max (prusti_test::max)
[2022-05-05T20:37:24Z INFO prusti_viper::encoder::encoder] Encoding: prusti_test::Example::check (prusti_test::{impl#0}::check)
[2022-05-05T20:37:24Z INFO prusti_common::stopwatch::log_level] [prusti-viper] Completed: encoding to Viper (0.035 seconds)
[2022-05-05T20:37:24Z INFO prusti_common::stopwatch::log_level] [prusti-viper] Starting: optimizing Viper program
[2022-05-05T20:37:24Z INFO prusti_common::stopwatch::log_level] [prusti-viper] Completed: optimizing Viper program (0.001 seconds)
[2022-05-05T20:37:24Z INFO prusti_common::stopwatch::log_level] [prusti-viper] Starting: verifying Viper program
[2022-05-05T20:37:24Z INFO prusti_viper::verifier] Connecting to Prusti server at localhost:37825
thread 'rustc' panicked at 'Verification request of program prusti_test::Example::check failed: reqwest::Error { kind: Request, url: Url { scheme: "http", cannot_be_a_base: false, username: "", password: None, host: Some(Domain("localhost")), port: Some(37825), path: "/bincode/verify/", query: None, fragment: None }, source: hyper::Error(IncompleteMessage) }', prusti-viper/src/verifier.rs:409:17
stack backtrace:
0: rust_begin_unwind
at /rustc/285fa7ecd05dcbfdaf2faaf20400f5f92b39b3c6/library/std/src/panicking.rs:584:5
1: core::panicking::panic_fmt
at /rustc/285fa7ecd05dcbfdaf2faaf20400f5f92b39b3c6/library/core/src/panicking.rs:143:14
2: prusti_viper::verifier::verify_programs::{{closure}}
3: <core::iter::adapters::map::Map<I,F> as core::iter::traits::iterator::Iterator>::fold
4: alloc::vec::source_iter_marker::<impl alloc::vec::spec_from_iter::SpecFromIter<T,I> for alloc::vec::Vec<T>>::from_iter
5: prusti_viper::verifier::Verifier::verify
6: prusti_driver::verifier::verify
7: rustc_interface::passes::QueryContext::enter
8: <prusti_driver::callbacks::PrustiCompilerCalls as rustc_driver::Callbacks>::after_analysis
9: <rustc_interface::interface::Compiler>::enter::<rustc_driver::run_compiler::{closure#1}::{closure#2}, core::result::Result<core::option::Option<rustc_interface::queries::Linker>, rustc_errors::ErrorGuaranteed>>
10: rustc_span::with_source_map::<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_interface::interface::create_compiler_and_run<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_driver::run_compiler::{closure#1}>::{closure#1}>
11: rustc_interface::interface::create_compiler_and_run::<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_driver::run_compiler::{closure#1}>
12: <scoped_tls::ScopedKey<rustc_span::SessionGlobals>>::set::<rustc_interface::interface::run_compiler<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_driver::run_compiler::{closure#1}>::{closure#0}, core::result::Result<(), rustc_errors::ErrorGuaranteed>>
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.
error: internal compiler error: unexpected panic
note: Prusti or the compiler unexpectedly panicked. This is a bug.
note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
note: Prusti version: commit 81366ed155 2022-04-26 16:24:52 UTC, built on 2022-04-27 14:54:02 UTC
query stack during panic:
end of query stack
[2022-05-05T20:37:31Z INFO prusti_common::stopwatch::log_level] [prusti-viper] Completed: verifying Viper program (6.238 seconds)
[2022-05-05T20:37:31Z INFO prusti_common::stopwatch::log_level] [prusti] Completed: main (6.338 seconds)
error: could not compile `prusti-test`; 4 warnings emitted
└──── End stderr ──────┘
Exit code 101, signal null.
Ignored diagnostic message: '3 warnings emitted'
Prusti encountered an unexpected error.
Prusti encountered an unexpected error. We would appreciate a [bug report](https://github.com/viperproject/prusti-dev/issues/new). See the log (View -> Output -> Prusti Assistant) for more details.
Rendering 3 diagnostics at file:///home/ramla/Desktop/prusti-test/src/main.rs
Thank you for the report. From the log it looks like a network transmission error. Could you also include the log of the "Output > Prusti Assistant Server" tab?
[stderr] [2022-05-06T13:49:17Z INFO prusti_common::stopwatch::log_level] [prusti-server] Starting: attach thread to JVM
[stderr] [2022-05-06T13:49:17Z INFO prusti_common::stopwatch::log_level] [prusti-server] Completed: attach thread to JVM (0.000 seconds)
[2022-05-06T13:49:17Z INFO prusti_server::process_verification] Verification request hash: 177752624514423564
[stderr] [2022-05-06T13:49:17Z INFO prusti_common::stopwatch::log_level] [prusti-server] Starting: attach thread to JVM
[stderr] [2022-05-06T13:49:17Z INFO prusti_common::stopwatch::log_level] [prusti-server] Completed: attach thread to JVM (0.000 seconds)
[2022-05-06T13:49:17Z INFO prusti_server::process_verification] Verification request hash: 684624286581388384
[stderr] [2022-05-06T13:49:17Z INFO prusti_common::stopwatch::log_level] [prusti-server] Starting: attach thread to JVM
[stderr] [2022-05-06T13:49:17Z INFO prusti_common::stopwatch::log_level] [prusti-server] Completed: attach thread to JVM (0.000 seconds)
[2022-05-06T13:49:17Z INFO prusti_server::process_verification] Verification request hash: 8165743185970310719
[2022-05-06T13:49:17Z INFO prusti_common::stopwatch::log_level] [prusti-server] Starting: construction of JVM objects
[stderr] thread 'main' panicked at 'internal error: entered unreachable code: illegal binary operation & for type Some(Int)', prusti-common/src/vir/to_viper.rs:535:26
stack backtrace:
0[stderr] : rust_begin_unwind
at /rustc/285fa7ecd05dcbfdaf2faaf20400f5f92b39b3c6/library/std/src/panicking.rs:584:5
1: core::panicking::panic_fmt
at /rustc/285fa7ecd05dcbfdaf2faaf20400f5f92b39b3c6/library/core/src/panicking.rs:143:14
2: prusti_common::vir::to_viper::<impl prusti_common::vir::low_to_viper::ToViper<viper::ast_factory::structs::Expr> for vir::legacy::ast::expr::Expr>::to_viper
3: prusti_common::vir::to_viper::<impl prusti_common::vir::low_to_viper::ToViper<viper::ast_factory::structs::Expr> for vir::legacy::ast::expr::Expr>::to_viper
4: prusti_common::vir::to_viper::<impl prusti_common::vir::low_to_viper::ToViper<viper::ast_factory::structs::Expr> for vir::legacy::ast::expr::Expr>::to_viper
5: prusti_common::vir::to_viper::<impl prusti_common::vir::low_to_viper::ToViper<viper::ast_factory::structs::Expr> for vir::legacy::ast::expr::Expr>::to_viper
6: prusti_common::vir::to_viper::<impl prusti_common::vir::low_to_viper::ToViper<viper::[stderr] ast_factory::structs::Expr> for vir::legacy::ast::expr::Expr>::to_viper
7: prusti_common::vir::to_viper::<impl prusti_common::vir::low_to_viper::ToViper<viper::ast_factory::structs::Stmt> for vir::legacy::ast::stmt::Stmt>::to_viper
8: prusti_common::vir::to_viper::<impl prusti_common::vir::low_to_viper::ToViper<alloc::vec::Vec<viper::ast_factory::structs::Stmt>> for alloc::vec::Vec<vir::legacy::ast::stmt::Stmt>>::to_viper
[stderr] 9: prusti_common::vir::to_viper::block_to_viper
10: prusti_common::vir::to_viper::<impl prusti_common::vir::low_to_viper::ToViper<viper::ast_factory::structs::Method> for &vir::legacy::cfg::method::CfgMethod>::to_viper
[stderr] 11: <alloc::vec::Vec<T> as alloc::vec::spec_from_iter::SpecFromIter<T,I>>::from_iter
12: prusti_common::vir::to_viper::<impl prusti_common::vir::low_to_viper::ToViper<viper::ast_factory::structs::Program[stderr] > for vir::legacy::program::Program>::to_viper
13: prusti_server::process_verification::process_verification_request::{{closure}}
14: viper::ast_utils::AstUtils::with_local_frame
15: prusti_server::process_verification::process_verification_request
[stderr] 16: <F as warp::generic::Func<(T16,)>>::call
17: <warp::filter::or::EitherFuture<T,U> as core::future::future::Future>::poll
[stderr] 18: hyper::proto::h1::dispatch::Dispatcher<D,Bs,I,T>::poll_catch
19: <hyper::server::conn::upgrades::UpgradeableConnection<I,S,E> as core::future::future::Future>::poll
20: <hyper::server::conn::spawn_all::NewSvcTask<I,N,S,E,W> as core::future::future::Future>::poll
21: <core::panic::unwind_safe::AssertUnwindSafe<F> as [stderr] core::ops::function::FnOnce<()>>::call_once
22: tokio::runtime::task::harness::Harness<T,S>::poll
23: tokio::runtime::[stderr] basic_scheduler::BasicScheduler<P>::block_on
24: tokio::runtime::context::enter
25: tokio::runtime::Runtime::block_on
26: prusti_server::server::listen_on_port_with_address_callback
27: prusti_server::server::start_server_on_port
28: prusti_server_driver::main
[stderr] note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.
[2022-05-06T13:49:17Z INFO prusti_common::stopwatch::log_level] [prusti-server] Completed: construction of JVM objects (0.030 seconds)
Thanks! The second log and the updated example are very helpful. It seems to be a bug that is triggered by using bitwise operations with generic types, even when the concrete instantiation of the types is known.
As a workaround, you could try moving self.a.read() to a pure function with an explicit u32 return type. I can't test the code because I don't see the definition of Volatile, but I expect the following to work.
impl Example {
#[pure]
fn a_read(&self) -> u32 {
self.a.read()
}
#[ensures(self.a_read() & 1 == 1)]
fn check(&self) {
while self.a_read() & 1 == 0 {}
}
}
Note, however, that #[pure] on read(&self) -> T means that the result cannot change as long as the program holds a shared reference to Volatile. This is probably not what you want.
Hi, thanks for the quick reply. With the solution, I'm still getting an unexpected error:
Prusti assistant output:
Run verification on /home/ramla/Desktop/prusti-test/src/main.rs...
Preparing verification run #10.
Killing 0 processes.
Run command '/home/ramla/prusti-dev/target/release/cargo-prusti --message-format=json'
Spawned PID: 9534
Output from '/home/ramla/prusti-dev/target/release/cargo-prusti --message-format=json' (0.3s):
┌──── Begin stdout ────┐
{"reason":"compiler-artifact","package_id":"volatile 0.2.7 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/volatile-0.2.7/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"volatile","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/volatile-0.2.7/src/lib.rs","edition":"2015","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":2,"debug_assertions":true,"overflow_checks":true,"test":false},"features":[],"filenames":["/home/ramla/Desktop/prusti-test/target/verify/debug/deps/libvolatile-78762e6d622c4864.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-message","package_id":"prusti-test 0.1.0 (path+file:///home/ramla/Desktop/prusti-test)","manifest_path":"/home/ramla/Desktop/prusti-test/Cargo.toml","target":{"kind":["bin"],"crate_types":["bin"],"name":"prusti-test","src_path":"/home/ramla/Desktop/prusti-test/src/main.rs","edition":"2021","doc":true,"doctest":false,"test":true},"message":{"rendered":"warning: unused variable: `vec1`\n --> src/main.rs:273:9\n |\n273 | let vec1: Vec<u32> = Vec::new();\n | ^^^^ help: if this is intentional, prefix it with an underscore: `_vec1`\n |\n = note: `#[warn(unused_variables)]` on by default\n\n","children":[{"children":[],"code":null,"level":"note","message":"`#[warn(unused_variables)]` on by default","rendered":null,"spans":[]},{"children":[],"code":null,"level":"help","message":"if this is intentional, prefix it with an underscore","rendered":null,"spans":[{"byte_end":6884,"byte_start":6880,"column_end":13,"column_start":9,"expansion":null,"file_name":"src/main.rs","is_primary":true,"label":null,"line_end":273,"line_start":273,"suggested_replacement":"_vec1","suggestion_applicability":"MachineApplicable","text":[{"highlight_end":13,"highlight_start":9,"text":" let vec1: Vec<u32> = Vec::new();"}]}]}],"code":{"code":"unused_variables","explanation":null},"level":"warning","message":"unused variable: `vec1`","spans":[{"byte_end":6884,"byte_start":6880,"column_end":13,"column_start":9,"expansion":null,"file_name":"src/main.rs","is_primary":true,"label":null,"line_end":273,"line_start":273,"suggested_replacement":null,"suggestion_applicability":null,"text":[{"highlight_end":13,"highlight_start":9,"text":" let vec1: Vec<u32> = Vec::new();"}]}]}}
{"reason":"compiler-message","package_id":"prusti-test 0.1.0 (path+file:///home/ramla/Desktop/prusti-test)","manifest_path":"/home/ramla/Desktop/prusti-test/Cargo.toml","target":{"kind":["bin"],"crate_types":["bin"],"name":"prusti-test","src_path":"/home/ramla/Desktop/prusti-test/src/main.rs","edition":"2021","doc":true,"doctest":false,"test":true},"message":{"rendered":"warning: field is never read: `b`\n --> src/main.rs:243:5\n |\n243 | b: Volatile<u32>\n | ^^^^^^^^^^^^^^^^\n |\n = note: `#[warn(dead_code)]` on by default\n\n","children":[{"children":[],"code":null,"level":"note","message":"`#[warn(dead_code)]` on by default","rendered":null,"spans":[]}],"code":{"code":"dead_code","explanation":null},"level":"warning","message":"field is never read: `b`","spans":[{"byte_end":6474,"byte_start":6458,"column_end":21,"column_start":5,"expansion":null,"file_name":"src/main.rs","is_primary":true,"label":null,"line_end":243,"line_start":243,"suggested_replacement":null,"suggestion_applicability":null,"text":[{"highlight_end":21,"highlight_start":5,"text":" b: Volatile<u32>"}]}]}}
{"reason":"compiler-message","package_id":"prusti-test 0.1.0 (path+file:///home/ramla/Desktop/prusti-test)","manifest_path":"/home/ramla/Desktop/prusti-test/Cargo.toml","target":{"kind":["bin"],"crate_types":["bin"],"name":"prusti-test","src_path":"/home/ramla/Desktop/prusti-test/src/main.rs","edition":"2021","doc":true,"doctest":false,"test":true},"message":{"rendered":"warning: associated function is never used: `check`\n --> src/main.rs:253:8\n |\n253 | fn check(&self) {\n | ^^^^^\n\n","children":[],"code":{"code":"dead_code","explanation":null},"level":"warning","message":"associated function is never used: `check`","spans":[{"byte_end":6615,"byte_start":6610,"column_end":13,"column_start":8,"expansion":null,"file_name":"src/main.rs","is_primary":true,"label":null,"line_end":253,"line_start":253,"suggested_replacement":null,"suggestion_applicability":null,"text":[{"highlight_end":13,"highlight_start":8,"text":" fn check(&self) {"}]}]}}
{"reason":"compiler-message","package_id":"prusti-test 0.1.0 (path+file:///home/ramla/Desktop/prusti-test)","manifest_path":"/home/ramla/Desktop/prusti-test/Cargo.toml","target":{"kind":["bin"],"crate_types":["bin"],"name":"prusti-test","src_path":"/home/ramla/Desktop/prusti-test/src/main.rs","edition":"2021","doc":true,"doctest":false,"test":true},"message":{"rendered":"warning: 3 warnings emitted\n\n","children":[],"code":null,"level":"warning","message":"3 warnings emitted","spans":[]}}
{"reason":"build-finished","success":false}
└──── End stdout ──────┘
┌──── Begin stderr ────┐
Checking prusti-test v0.1.0 (/home/ramla/Desktop/prusti-test)
[2022-05-06T14:27:42Z INFO prusti_driver] Prusti version: commit 81366ed155 2022-04-26 16:24:52 UTC, built on 2022-04-27 14:54:02 UTC
[2022-05-06T14:27:42Z INFO prusti_viper::verifier] Received 4 functions to be verified:
[2022-05-06T14:27:42Z INFO prusti_common::stopwatch::log_level] [prusti-viper] Starting: encoding to Viper
[2022-05-06T14:27:42Z INFO prusti_viper::verifier] - main (prusti_test::main)
[2022-05-06T14:27:42Z INFO prusti_viper::verifier] Source: src/main.rs:272:1: 272:10 (#0)
[2022-05-06T14:27:42Z INFO prusti_viper::verifier] - max (prusti_test::max)
[2022-05-06T14:27:42Z INFO prusti_viper::verifier] Source: src/main.rs:228:1: 228:30 (#0)
[2022-05-06T14:27:42Z INFO prusti_viper::verifier] - Example::a_read (prusti_test::{impl#0}::a_read)
[2022-05-06T14:27:42Z INFO prusti_viper::verifier] Source: src/main.rs:248:5: 248:28 (#0)
[2022-05-06T14:27:42Z INFO prusti_viper::verifier] - Example::check (prusti_test::{impl#0}::check)
[2022-05-06T14:27:42Z INFO prusti_viper::verifier] Source: src/main.rs:253:5: 253:20 (#0)
[2022-05-06T14:27:42Z INFO prusti_viper::encoder::encoder] Encoding: prusti_test::main (prusti_test::main)
[2022-05-06T14:27:42Z INFO prusti_viper::encoder::encoder] Encoding: prusti_test::max (prusti_test::max)
[2022-05-06T14:27:42Z INFO prusti_viper::encoder::encoder] Encoding: prusti_test::Example::a_read (prusti_test::{impl#0}::a_read)
[2022-05-06T14:27:42Z INFO prusti_viper::encoder::encoder] Encoding: prusti_test::Example::check (prusti_test::{impl#0}::check)
[2022-05-06T14:27:42Z INFO prusti_common::stopwatch::log_level] [prusti-viper] Completed: encoding to Viper (0.050 seconds)
[2022-05-06T14:27:42Z INFO prusti_common::stopwatch::log_level] [prusti-viper] Starting: optimizing Viper program
[2022-05-06T14:27:42Z INFO prusti_common::stopwatch::log_level] [prusti-viper] Completed: optimizing Viper program (0.002 seconds)
[2022-05-06T14:27:42Z INFO prusti_common::stopwatch::log_level] [prusti-viper] Starting: verifying Viper program
[2022-05-06T14:27:42Z INFO prusti_viper::verifier] Connecting to Prusti server at localhost:33193
thread 'rustc' panicked at 'Verification request of program prusti_test::Example::check failed: reqwest::Error { kind: Request, url: Url { scheme: "http", cannot_be_a_base: false, username: "", password: None, host: Some(Domain("localhost")), port: Some(33193), path: "/bincode/verify/", query: None, fragment: None }, source: hyper::Error(IncompleteMessage) }', prusti-viper/src/verifier.rs:409:17
stack backtrace:
0: rust_begin_unwind
at /rustc/285fa7ecd05dcbfdaf2faaf20400f5f92b39b3c6/library/std/src/panicking.rs:584:5
1: core::panicking::panic_fmt
at /rustc/285fa7ecd05dcbfdaf2faaf20400f5f92b39b3c6/library/core/src/panicking.rs:143:14
2: prusti_viper::verifier::verify_programs::{{closure}}
3: <core::iter::adapters::map::Map<I,F> as core::iter::traits::iterator::Iterator>::fold
4: alloc::vec::source_iter_marker::<impl alloc::vec::spec_from_iter::SpecFromIter<T,I> for alloc::vec::Vec<T>>::from_iter
5: prusti_viper::verifier::Verifier::verify
6: prusti_driver::verifier::verify
7: rustc_interface::passes::QueryContext::enter
8: <prusti_driver::callbacks::PrustiCompilerCalls as rustc_driver::Callbacks>::after_analysis
9: <rustc_interface::interface::Compiler>::enter::<rustc_driver::run_compiler::{closure#1}::{closure#2}, core::result::Result<core::option::Option<rustc_interface::queries::Linker>, rustc_errors::ErrorGuaranteed>>
10: rustc_span::with_source_map::<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_interface::interface::create_compiler_and_run<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_driver::run_compiler::{closure#1}>::{closure#1}>
11: rustc_interface::interface::create_compiler_and_run::<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_driver::run_compiler::{closure#1}>
12: <scoped_tls::ScopedKey<rustc_span::SessionGlobals>>::set::<rustc_interface::interface::run_compiler<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_driver::run_compiler::{closure#1}>::{closure#0}, core::result::Result<(), rustc_errors::ErrorGuaranteed>>
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.
error: internal compiler error: unexpected panic
note: Prusti or the compiler unexpectedly panicked. This is a bug.
note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
note: Prusti version: commit 81366ed155 2022-04-26 16:24:52 UTC, built on 2022-04-27 14:54:02 UTC
query stack during panic:
end of query stack
[2022-05-06T14:27:42Z INFO prusti_common::stopwatch::log_level] [prusti-viper] Completed: verifying Viper program (0.064 seconds)
[2022-05-06T14:27:42Z INFO prusti_common::stopwatch::log_level] [prusti] Completed: main (0.178 seconds)
error: could not compile `prusti-test`; 4 warnings emitted
└──── End stderr ──────┘
Exit code 101, signal null.
Ignored diagnostic message: '3 warnings emitted'
Prusti encountered an unexpected error.
Prusti encountered an unexpected error. We would appreciate a [bug report](https://github.com/viperproject/prusti-dev/issues/new). See the log (View -> Output -> Prusti Assistant) for more details.
Rendering 3 diagnostics at file:///home/ramla/Desktop/prusti-test/src/main.rs
Prusti assistant server output:
[stderr] [2022-05-06T14:27:42Z INFO prusti_common::stopwatch::log_level] [prusti-server] Starting: attach thread to JVM
[stderr] [2022-05-06T14:27:42Z INFO prusti_common::stopwatch::log_level] [prusti-server] Completed: attach thread to JVM (0.000 seconds)
[2022-05-06T14:27:42Z INFO prusti_server::process_verification] Verification request hash: 10267466840255418137
[stderr] [2022-05-06T14:27:42Z INFO prusti_common::stopwatch::log_level] [prusti-server] Starting: attach thread to JVM
[stderr] [2022-05-06T14:27:42Z INFO prusti_common::stopwatch::log_level] [prusti-server] Completed: attach thread to JVM (0.000 seconds)
[2022-05-06T14:27:42Z INFO prusti_server::process_verification] Verification request hash: 16568248359183839258
[stderr] [2022-05-06T14:27:42Z INFO prusti_common::stopwatch::log_level] [prusti-server] Starting: attach thread to JVM
[stderr] [2022-05-06T14:27:42Z INFO prusti_common::stopwatch::log_level] [prusti-server] Completed: attach thread to JVM (0.000 seconds)
[2022-05-06T14:27:42Z INFO prusti_server::process_verification] Verification request hash: 15774060923452460209
[stderr] [2022-05-06T14:27:42Z INFO prusti_common::stopwatch::log_level] [prusti-server] Starting: attach thread to JVM
[stderr] [2022-05-06T14:27:42Z INFO prusti_common::stopwatch::log_level] [prusti-server] Completed: attach thread to JVM (0.000 seconds)
[2022-05-06T14:27:42Z INFO prusti_server::process_verification] Verification request hash: 7625177374903062963
[stderr] [2022-05-06T14:27:42Z INFO prusti_common::stopwatch::log_level] [prusti-server] Starting: construction of JVM objects
[stderr] thread 'main' panicked at 'internal error: entered unreachable code: illegal binary operation & for type Some(Int)', prusti-common/src/vir/to_viper.rs:535:26
stack backtrace:
0: [stderr] rust_begin_unwind
at /rustc/285fa7ecd05dcbfdaf2faaf20400f5f92b39b3c6/library/std/src/panicking.rs:584:5
1: core::panicking::panic_fmt
at /rustc/285fa7ecd05dcbfdaf2faaf20400f5f92b39b3c6/library/core/src/panicking.rs:143:14
2: prusti_common::vir::to_viper::<impl prusti_common::vir::low_to_viper::ToViper<viper::ast_factory::structs::Expr> for vir::legacy::ast::expr::Expr>::to_viper
3: prusti_common::vir::to_viper::<impl prusti_common::vir::low_to_viper::ToViper<viper::ast_factory::structs::Expr> for vir::legacy::ast::expr::Expr>::to_viper
4: prusti_common::vir::to_viper::<impl prusti_common::vir::low_to_viper::ToViper<viper::ast_factory::structs::Expr> for vir::legacy::ast::expr::Expr>::to_viper
5: prusti_common::vir::to_viper::<impl prusti_common::vir::low_to_viper::ToViper<viper::ast_factory::structs::Expr> for vir::legacy::ast::expr::Expr>::to_viper
[stderr] 6: prusti_common::vir::to_viper::<impl prusti_common::vir::low_to_viper::ToViper<viper::ast_factory::structs::Expr> for vir::legacy::ast::expr::Expr>::to_viper
7: prusti_common::vir::to_viper::<impl prusti_common::vir::low_to_viper::ToViper<viper::ast_factory::structs::Stmt> for vir::legacy::ast::stmt::Stmt>::to_viper
8: prusti_common::vir::to_viper::<impl prusti_common[stderr] ::vir::low_to_viper::ToViper<alloc::vec::Vec<viper::ast_factory::structs::Stmt>> for alloc::vec::Vec<vir::legacy::ast::stmt::Stmt>>::to_viper
9: prusti_common::vir::to_viper::block_to_viper
10: prusti_common::vir::to_viper::<impl prusti_common::vir::low_to_viper::ToViper<viper::ast_factory::structs::Method> for &vir::legacy::cfg::method::CfgMethod>::to_viper
11: <alloc::vec::Vec[stderr] <T> as alloc::vec::spec_from_iter::SpecFromIter<T,I>>::from_iter
12: prusti_common::vir::to_viper::<impl prusti_common::vir::low_to_viper::ToViper<viper::ast_factory::structs::Program> for vir::legacy::program::Program>::to_viper
13: prusti_server::process_verification::process_verification_request::{{closure}}
14: [stderr] viper::ast_utils::AstUtils::with_local_frame
15: prusti_server::process_verification::process_verification_request
16: <F as warp::generic::Func<(T16,)>>::call
17: <warp::filter::or::EitherFuture<T,U>[stderr] as core::future::future::Future>::poll
18: hyper::proto::h1::dispatch::Dispatcher<D,Bs,I,T>::poll_catch
[stderr] 19: <hyper::server::conn::upgrades::UpgradeableConnection<I,S,E> as core::future::future::Future>::poll
20: <hyper::server::conn::spawn_all::NewSvcTask<I[stderr] ,N,S,E,W> as core::future::future::Future>::poll
21: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>[stderr] >::call_once
22: tokio::runtime::task::harness::Harness<T,S>::poll
23: tokio::runtime::basic_scheduler::BasicScheduler<P>::block_on
24: tokio::runtime::context::enter
[stderr] 25: tokio::runtime::Runtime::block_on
26: prusti_server::server::listen_on_port_with_address_callback
27: prusti_server::server::start_server_on_port
28: prusti_server_driver::main
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.
[stderr] [2022-05-06T14:27:42Z INFO prusti_common::stopwatch::log_level] [prusti-server] Completed: construction of JVM objects (0.023 seconds)
Then we would need a full example, like a zip of the crate that you are writing.
Trying your code with the workaround I get a proper error:
[Prusti: unsupported feature] bitwise operations on non-boolean types are experimental and disabled by default; use `encode_bitvectors` to enable
Maybe it's because I'm using a recent Prusti version. Can you try switching to the LatestDev channel in the settings of Prusti in the IDE?
ok, I see. I actually have that flag enabled because I wanted to use bitwise operations.
so, is it correct to assume that generic types will not work when we enable bitwise operations?
I ran another very simple test where I creates a Volatile struct just for u32, so generics are out of the picture. Again, this only seems to work without bitwise operations. (see prusti_test_wo_bitwiseop.zip)
I ran a similar test where I added two bitwise operations and enabled the config flag. I get the same unexpected error (see prusti_test_w_bitwiseop.zip)
Prusti assistant output:
Run verification on /home/ramla/Desktop/prusti-test/src/main.rs...
Preparing verification run #2.
Killing 0 processes.
Run command '/home/ramla/prusti-dev/target/release/cargo-prusti --message-format=json'
Spawned PID: 26529
Output from '/home/ramla/prusti-dev/target/release/cargo-prusti --message-format=json' (0.3s):
┌──── Begin stdout ────┐
{"reason":"compiler-artifact","package_id":"volatile 0.2.7 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/volatile-0.2.7/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"volatile","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/volatile-0.2.7/src/lib.rs","edition":"2015","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":2,"debug_assertions":true,"overflow_checks":true,"test":false},"features":[],"filenames":["/home/ramla/Desktop/prusti-test/target/verify/debug/deps/libvolatile-78762e6d622c4864.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-message","package_id":"prusti-test 0.1.0 (path+file:///home/ramla/Desktop/prusti-test)","manifest_path":"/home/ramla/Desktop/prusti-test/Cargo.toml","target":{"kind":["bin"],"crate_types":["bin"],"name":"prusti-test","src_path":"/home/ramla/Desktop/prusti-test/src/main.rs","edition":"2021","doc":true,"doctest":false,"test":true},"message":{"rendered":"warning: unused import: `volatile::Volatile`\n --> src/main.rs:5:5\n |\n5 | use volatile::Volatile;\n | ^^^^^^^^^^^^^^^^^^\n |\n = note: `#[warn(unused_imports)]` on by default\n\n","children":[{"children":[],"code":null,"level":"note","message":"`#[warn(unused_imports)]` on by default","rendered":null,"spans":[]},{"children":[],"code":null,"level":"help","message":"remove the whole `use` item","rendered":null,"spans":[{"byte_end":103,"byte_start":80,"column_end":24,"column_start":1,"expansion":null,"file_name":"src/main.rs","is_primary":true,"label":null,"line_end":5,"line_start":5,"suggested_replacement":"","suggestion_applicability":"MachineApplicable","text":[{"highlight_end":24,"highlight_start":1,"text":"use volatile::Volatile;"}]}]}],"code":{"code":"unused_imports","explanation":null},"level":"warning","message":"unused import: `volatile::Volatile`","spans":[{"byte_end":102,"byte_start":84,"column_end":23,"column_start":5,"expansion":null,"file_name":"src/main.rs","is_primary":true,"label":null,"line_end":5,"line_start":5,"suggested_replacement":null,"suggestion_applicability":null,"text":[{"highlight_end":23,"highlight_start":5,"text":"use volatile::Volatile;"}]}]}}
{"reason":"compiler-message","package_id":"prusti-test 0.1.0 (path+file:///home/ramla/Desktop/prusti-test)","manifest_path":"/home/ramla/Desktop/prusti-test/Cargo.toml","target":{"kind":["bin"],"crate_types":["bin"],"name":"prusti-test","src_path":"/home/ramla/Desktop/prusti-test/src/main.rs","edition":"2021","doc":true,"doctest":false,"test":true},"message":{"rendered":"warning: field is never read: `b`\n --> src/main.rs:10:5\n |\n10 | b: TrustedVolatile\n | ^^^^^^^^^^^^^^^^^^\n |\n = note: `#[warn(dead_code)]` on by default\n\n","children":[{"children":[],"code":null,"level":"note","message":"`#[warn(dead_code)]` on by default","rendered":null,"spans":[]}],"code":{"code":"dead_code","explanation":null},"level":"warning","message":"field is never read: `b`","spans":[{"byte_end":169,"byte_start":151,"column_end":23,"column_start":5,"expansion":null,"file_name":"src/main.rs","is_primary":true,"label":null,"line_end":10,"line_start":10,"suggested_replacement":null,"suggestion_applicability":null,"text":[{"highlight_end":23,"highlight_start":5,"text":" b: TrustedVolatile"}]}]}}
{"reason":"compiler-message","package_id":"prusti-test 0.1.0 (path+file:///home/ramla/Desktop/prusti-test)","manifest_path":"/home/ramla/Desktop/prusti-test/Cargo.toml","target":{"kind":["bin"],"crate_types":["bin"],"name":"prusti-test","src_path":"/home/ramla/Desktop/prusti-test/src/main.rs","edition":"2021","doc":true,"doctest":false,"test":true},"message":{"rendered":"warning: associated function is never used: `check`\n --> src/main.rs:16:8\n |\n16 | fn check(&mut self) {\n | ^^^^^\n\n","children":[],"code":{"code":"dead_code","explanation":null},"level":"warning","message":"associated function is never used: `check`","spans":[{"byte_end":240,"byte_start":235,"column_end":13,"column_start":8,"expansion":null,"file_name":"src/main.rs","is_primary":true,"label":null,"line_end":16,"line_start":16,"suggested_replacement":null,"suggestion_applicability":null,"text":[{"highlight_end":13,"highlight_start":8,"text":" fn check(&mut self) {"}]}]}}
{"reason":"compiler-message","package_id":"prusti-test 0.1.0 (path+file:///home/ramla/Desktop/prusti-test)","manifest_path":"/home/ramla/Desktop/prusti-test/Cargo.toml","target":{"kind":["bin"],"crate_types":["bin"],"name":"prusti-test","src_path":"/home/ramla/Desktop/prusti-test/src/main.rs","edition":"2021","doc":true,"doctest":false,"test":true},"message":{"rendered":"warning: 3 warnings emitted\n\n","children":[],"code":null,"level":"warning","message":"3 warnings emitted","spans":[]}}
{"reason":"build-finished","success":false}
└──── End stdout ──────┘
┌──── Begin stderr ────┐
Checking prusti-test v0.1.0 (/home/ramla/Desktop/prusti-test)
[2022-05-06T18:43:27Z INFO prusti_driver] Prusti version: commit 81366ed155 2022-04-26 16:24:52 UTC, built on 2022-04-27 14:54:02 UTC
[2022-05-06T18:43:27Z INFO prusti_viper::verifier] Received 5 functions to be verified:
[2022-05-06T18:43:27Z INFO prusti_common::stopwatch::log_level] [prusti-viper] Starting: encoding to Viper
[2022-05-06T18:43:27Z INFO prusti_viper::verifier] - main (prusti_test::main)
[2022-05-06T18:43:27Z INFO prusti_viper::verifier] Source: src/main.rs:23:1: 23:10 (#0)
[2022-05-06T18:43:27Z INFO prusti_viper::verifier] - TrustedVolatile::new (prusti_test::{impl#1}::new)
[2022-05-06T18:43:27Z INFO prusti_viper::verifier] Source: src/main.rs:43:5: 43:56 (#0)
[2022-05-06T18:43:27Z INFO prusti_viper::verifier] - Example::check (prusti_test::{impl#0}::check)
[2022-05-06T18:43:27Z INFO prusti_viper::verifier] Source: src/main.rs:16:5: 16:24 (#0)
[2022-05-06T18:43:27Z INFO prusti_viper::verifier] - TrustedVolatile::read (prusti_test::{impl#1}::read)
[2022-05-06T18:43:27Z INFO prusti_viper::verifier] Source: src/main.rs:50:5: 50:30 (#0)
[2022-05-06T18:43:27Z INFO prusti_viper::verifier] - TrustedVolatile::write (prusti_test::{impl#1}::write)
[2022-05-06T18:43:27Z INFO prusti_viper::verifier] Source: src/main.rs:59:5: 59:40 (#0)
[2022-05-06T18:43:27Z INFO prusti_viper::encoder::encoder] Encoding: prusti_test::main (prusti_test::main)
[2022-05-06T18:43:27Z INFO prusti_viper::encoder::encoder] Encoding: prusti_test::TrustedVolatile::new (prusti_test::{impl#1}::new)
[2022-05-06T18:43:27Z INFO prusti_viper::encoder::encoder] Encoding: prusti_test::Example::check (prusti_test::{impl#0}::check)
[2022-05-06T18:43:27Z INFO prusti_viper::encoder::encoder] Encoding: prusti_test::TrustedVolatile::read (prusti_test::{impl#1}::read)
[2022-05-06T18:43:27Z INFO prusti_viper::encoder::encoder] Encoding: prusti_test::TrustedVolatile::write (prusti_test::{impl#1}::write)
[2022-05-06T18:43:27Z INFO prusti_common::stopwatch::log_level] [prusti-viper] Completed: encoding to Viper (0.027 seconds)
[2022-05-06T18:43:27Z INFO prusti_common::stopwatch::log_level] [prusti-viper] Starting: optimizing Viper program
[2022-05-06T18:43:27Z INFO prusti_common::stopwatch::log_level] [prusti-viper] Completed: optimizing Viper program (0.001 seconds)
[2022-05-06T18:43:27Z INFO prusti_common::stopwatch::log_level] [prusti-viper] Starting: verifying Viper program
[2022-05-06T18:43:27Z INFO prusti_viper::verifier] Connecting to Prusti server at localhost:35361
thread 'rustc' panicked at 'Verification request of program prusti_test::Example::check failed: reqwest::Error { kind: Request, url: Url { scheme: "http", cannot_be_a_base: false, username: "", password: None, host: Some(Domain("localhost")), port: Some(35361), path: "/bincode/verify/", query: None, fragment: None }, source: hyper::Error(IncompleteMessage) }', prusti-viper/src/verifier.rs:409:17
stack backtrace:
0: rust_begin_unwind
at /rustc/285fa7ecd05dcbfdaf2faaf20400f5f92b39b3c6/library/std/src/panicking.rs:584:5
1: core::panicking::panic_fmt
at /rustc/285fa7ecd05dcbfdaf2faaf20400f5f92b39b3c6/library/core/src/panicking.rs:143:14
2: prusti_viper::verifier::verify_programs::{{closure}}
3: <core::iter::adapters::map::Map<I,F> as core::iter::traits::iterator::Iterator>::fold
4: alloc::vec::source_iter_marker::<impl alloc::vec::spec_from_iter::SpecFromIter<T,I> for alloc::vec::Vec<T>>::from_iter
5: prusti_viper::verifier::Verifier::verify
6: prusti_driver::verifier::verify
7: rustc_interface::passes::QueryContext::enter
8: <prusti_driver::callbacks::PrustiCompilerCalls as rustc_driver::Callbacks>::after_analysis
9: <rustc_interface::interface::Compiler>::enter::<rustc_driver::run_compiler::{closure#1}::{closure#2}, core::result::Result<core::option::Option<rustc_interface::queries::Linker>, rustc_errors::ErrorGuaranteed>>
10: rustc_span::with_source_map::<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_interface::interface::create_compiler_and_run<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_driver::run_compiler::{closure#1}>::{closure#1}>
11: rustc_interface::interface::create_compiler_and_run::<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_driver::run_compiler::{closure#1}>
12: <scoped_tls::ScopedKey<rustc_span::SessionGlobals>>::set::<rustc_interface::interface::run_compiler<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_driver::run_compiler::{closure#1}>::{closure#0}, core::result::Result<(), rustc_errors::ErrorGuaranteed>>
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.
error: internal compiler error: unexpected panic
note: Prusti or the compiler unexpectedly panicked. This is a bug.
note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
note: Prusti version: commit 81366ed155 2022-04-26 16:24:52 UTC, built on 2022-04-27 14:54:02 UTC
query stack during panic:
end of query stack
[2022-05-06T18:43:27Z INFO prusti_common::stopwatch::log_level] [prusti-viper] Completed: verifying Viper program (0.083 seconds)
[2022-05-06T18:43:27Z INFO prusti_common::stopwatch::log_level] [prusti] Completed: main (0.154 seconds)
error: could not compile `prusti-test`; 4 warnings emitted
└──── End stderr ──────┘
Exit code 101, signal null.
Ignored diagnostic message: '3 warnings emitted'
Prusti encountered an unexpected error.
Prusti encountered an unexpected error. We would appreciate a [bug report](https://github.com/viperproject/prusti-dev/issues/new). See the log (View -> Output -> Prusti Assistant) for more details.
Rendering 3 diagnostics at file:///home/ramla/Desktop/prusti-test/src/main.rs
Prusti assistant server output:
[stderr] [2022-05-06T18:43:27Z INFO prusti_common::stopwatch::log_level] [prusti-server] Starting: attach thread to JVM
[stderr] [2022-05-06T18:43:27Z INFO prusti_common::stopwatch::log_level] [prusti-server] Completed: attach thread to JVM (0.000 seconds)
[2022-05-06T18:43:27Z INFO prusti_server::process_verification] Verification request hash: 10125896359928275422
[stderr] [2022-05-06T18:43:27Z INFO prusti_common::stopwatch::log_level] [prusti-server] Starting: attach thread to JVM
[stderr] [2022-05-06T18:43:27Z INFO prusti_common::stopwatch::log_level] [prusti-server] Completed: attach thread to JVM (0.000 seconds)
[2022-05-06T18:43:27Z INFO prusti_server::process_verification] Verification request hash: 9246711839064512589
[stderr] [2022-05-06T18:43:27Z INFO prusti_common::stopwatch::log_level] [prusti-server] Starting: attach thread to JVM
[stderr] [2022-05-06T18:43:27Z INFO prusti_common::stopwatch::log_level] [prusti-server] Completed: attach thread to JVM (0.000 seconds)
[2022-05-06T18:43:27Z INFO prusti_server::process_verification] Verification request hash: 6106983656618192115
[2022-05-06T18:43:27Z INFO prusti_common::stopwatch::log_level] [prusti-server] Starting: construction of JVM objects
[stderr] thread 'main' panicked at 'internal error: entered unreachable code: illegal binary operation & for type Some(Int)', prusti-common/src/vir/to_viper.rs:535:26
stack backtrace:
[stderr] 0: rust_begin_unwind
at /rustc/285fa7ecd05dcbfdaf2faaf20400f5f92b39b3c6/library/std/src/panicking.rs:584:5
1: core::panicking::panic_fmt
at /rustc/285fa7ecd05dcbfdaf2faaf20400f5f92b39b3c6/library/core/src/panicking.rs:143:14
2: prusti_common::vir::to_viper::<impl prusti_common::vir::low_to_viper::ToViper<viper::ast_factory::structs::Expr> for vir::legacy::ast::expr::Expr>::to_viper
3: prusti_common::vir::to_viper::<impl prusti_common::vir::low_to_viper::ToViper<viper::ast_factory::structs::Expr> for vir::legacy::ast::expr::Expr>::to_viper
4: prusti_common::vir::to_viper::<impl prusti_common::vir::low_to_viper::ToViper<viper::ast_factory::structs::Expr> for vir::legacy::ast::expr::Expr>::to_viper
5: prusti_common::vir::to_viper::<impl prusti_common::vir::low_to_viper::ToViper<viper::ast_factory::structs::Expr> for vir::legacy::ast::expr::Expr>::to_viper
6: prusti_common::vir::to_viper::<impl prusti_common::vir::low_to_viper::ToViper<viper::ast_factory::structs::Expr> for vir::legacy::ast::expr::Expr>::to_viper
7: prusti_common::vir::[stderr] to_viper::<impl prusti_common::vir::low_to_viper::ToViper<viper::ast_factory::structs::Stmt> for vir::legacy::ast::stmt::Stmt>::to_viper
8: prusti_common::vir::to_viper::<impl prusti_common::vir::low_to_viper::ToViper<alloc::vec::Vec<viper::ast_factory::structs::Stmt>> for alloc::vec::Vec<vir::legacy::ast::stmt::Stmt>>::to_viper
9: prusti_common::vir::to_viper::block_to_viper
10: prusti_common::vir::to_viper::<impl prusti_common::vir::low_to_viper::ToViper<viper::ast_factory::structs::Method> for &vir::legacy::cfg::method::CfgMethod>::to_viper
11: <alloc::vec::Vec<T> as alloc::vec::spec_from_iter::SpecFromIter[stderr] <T,I>>::from_iter
12: prusti_common::vir::to_viper::<impl prusti_common::vir::low_to_viper::ToViper<viper::ast_factory::structs::Program> for vir::legacy::program::Program>::to_viper
13: prusti_server::process_verification::process_verification_request::{{closure}}
14: viper::ast_utils::AstUtils::with_local_frame
15: prusti_server::process_verification::process_verification_request
16: <F as warp::generic::Func<(T16,)>>::call
17: <warp::filter::or::EitherFuture<T,U> as core::future::future::Future>::poll
18: hyper::proto::h1::dispatch::Dispatcher<D,Bs,I,T>::poll_catch
19: <hyper::server::conn[stderr] ::upgrades::UpgradeableConnection<I,S,E> as core::future::future::Future>::poll
20: <hyper::server::conn::spawn_all::NewSvcTask<I,N,S,E,W> as core::future::future::Future>::poll
21: <core::panic::unwind_safe::AssertUnwindSafe<F> as core::ops::function::FnOnce<()>>::call_once
22: tokio::runtime::task::harness::Harness<T,S>::poll
23: tokio::runtime::basic_scheduler::BasicScheduler<P>::block_on
24: tokio::runtime::context::enter
25: tokio::runtime::Runtime::block_on
26: prusti_server::server::[stderr] listen_on_port_with_address_callback
27: prusti_server::server::start_server_on_port
28: prusti_server_driver::main
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.
[2022-05-06T18:43:27Z INFO prusti_common::stopwatch::log_level] [prusti-server] Completed: construction of JVM objects (0.037 seconds)
prusti-test_wo_bitwiseop.zip prusti-test_w_bitwiseop.zip
I suppose my question is what are the limitation for using prusti with bitwise operations, since the code I'm aiming to verify uses them a lot.
Thanks, with encode_bitvectors=true I can reproduce the panic. That flag is quite recent and highly experimental, so if you plan to use it a lot you'll probably find more bugs like this. @vakaras should have a better idea of the current status.
The problem is that the bit operation is applied in a specification to a value returned by a function. Here is the minimal example:
// compile-flags: -Pencode_bitvectors=true
use prusti_contracts::*;
#[pure]
fn read() -> u32 {
1
}
#[ensures(read() & 1 == 1)]
fn test() { }
fn main() {}
I doubt that I will be able to fix this any time soon.
