viperproject
Consistency error in postcondition when calling pure function that returns a slice
The following Rust program:
use prusti_contracts::*;
#[derive(Copy, Clone)]
pub struct A {
inner: usize,
}
impl A {
#[pure]
pub const fn get(&self) -> usize {
self.inner
}
}
pub struct B {
a: A,
}
impl B {
#[pure]
#[trusted]
pub fn foo(&self, a: usize, b: usize) -> &[u8] {
unimplemented!()
}
#[pure]
#[ensures(result == self.foo(a.get(), b))]
pub fn bar(&self, a: A, b: usize) -> &[u8] {
self.foo(a.get(), b)
}
#[pure]
pub fn baz(&self) -> &[u8] {
self.bar(self.a, 1)
}
}
Generates the following for error message for the Viper program of B::baz:
error: [Prusti internal error] Prusti encountered an unexpected internal error
|
= note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
= note: Details: consistency error in prusti_example::B::baz: Consistency error: Local variable _4 not found. (@96.15)
This is due to the pure function encoding of B::bar:
function m_B$$bar__$TY$__(_1: Snap$struct$m_B, _2: Snap$struct$m_A, _3: Int): Snap$Slice$u8
requires 0 <= _3
requires _3 <= 18446744073709551615
requires true
requires true
ensures snap$__$TY$__Snap$Slice$u8$(_4.val_ref) == m_B$$foo__$TY$__(_1, m_A$$get__$TY$__(_2), _3)
ensures [result == mirror_simple$m_B$$bar__$TY$__(_1, _2, _3), true]
{
m_B$$foo__$TY$__(_1, m_A$$get__$TY$__(_2), _3)
}
Here we can see that in the post-condition it mentions snap$__$TY$__Snap$Slice$u8$(_4.val_ref), while it should mention result instead. The MIR for B::bar is:
It seems that the expression replacement in fn inline_spec_item fails here:
https://github.com/viperproject/prusti-dev/blob/7a5c782d52c92a7e7ce208786efad64fb2cb7836/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs#L100-L102
Here it tries to replace the expression for _4:
Field(
FieldExpr {
base: Local(
Local {
variable: _4: Ref(ref$Slice$u8),
position: Position {
line: 0,
column: 0,
id: 0,
},
},
),
field: val_ref: Ref(Slice$u8),
position: Position {
line: 0,
column: 0,
id: 0,
},
},
),
with:
Local(
Local {
variable: _0: Snapshot(Slice$u8),
position: Position {
line: 0,
column: 0,
id: 0,
},
},
),
However, the expression to be replaced is not present in the pure expression. Instead the pure expression holds a:
SnapApp(
SnapApp {
base: Local(
Local {
variable: _4: Ref(ref$Slice$u8),
position: Position {
line: 96,
column: 15,
id: 81,
},
},
),
position: Position {
line: 96,
column: 15,
id: 62,
},
},
),
I think this is due to that the method Encoder::encode_value_expr does not have a case that handles (references to) slices:
https://github.com/viperproject/prusti-dev/blob/7a5c782d52c92a7e7ce208786efad64fb2cb7836/prusti-viper/src/encoder/encoder.rs#L297-L315
which is called from here:
https://github.com/viperproject/prusti-dev/blob/7a5c782d52c92a7e7ce208786efad64fb2cb7836/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs#L85-L89
Does this extra replacement we added in #980 to encoder_poly fix this?
https://github.com/viperproject/prusti-dev/blob/7d25c73cb63cc0f985b48e5d3d91a7e50264c152/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs#L56-L63
Looks like the extra code from #980 doesn't fix it, but this custom fix does seem to work:
https://github.com/viperproject/prusti-dev/compare/master...Pointerbender:issue-1006?expand=1#diff-2bae12bf0e8545aac8fbb34fd81324fbf8bf69d6178b4084a790ab14ad106bdb
The only problem with it is that it triggers a panic in the new encoder when this line is enabled:
https://github.com/viperproject/prusti-dev/blob/7a5c782d52c92a7e7ce208786efad64fb2cb7836/prusti-viper/src/encoder/mir/pure/pure_functions/interface.rs#L295-L301
The error is:
[2022-05-17T13:16:09Z INFO prusti_viper::encoder::encoder] Encoding: prusti_example::B::baz (prusti_example::{impl#1}::baz)
thread 'rustc' panicked at 'assertion failed: self.pure_function_encoder_state.function_constructors.borrow_mut().insert(function_identifier,\n constructor).is_none()', prusti-viper/src/encoder/mir/pure/pure_functions/interface.rs:540:9
stack backtrace:
0: rust_begin_unwind
at /rustc/e7575f9670f3c837def3d186ae09366c75c7632e/library/std/src/panicking.rs:584:5
1: core::panicking::panic_fmt
at /rustc/e7575f9670f3c837def3d186ae09366c75c7632e/library/core/src/panicking.rs:142:14
2: core::panicking::panic
at /rustc/e7575f9670f3c837def3d186ae09366c75c7632e/library/core/src/panicking.rs:48:5
3: <prusti_viper::encoder::encoder::Encoder as prusti_viper::encoder::mir::pure::pure_functions::interface::PureFunctionEncoderInterface>::register_function_constructor_mir
at ~/git/rust/pointerbender/prusti-dev/prusti-viper/src/encoder/mir/pure/pure_functions/interface.rs:540:9
4: <prusti_viper::encoder::encoder::Encoder as prusti_viper::encoder::high::builtin_functions::interface::HighBuiltinFunctionEncoderInterfacePrivate>::encode_builtin_function_def_high
at ~/git/rust/pointerbender/prusti-dev/prusti-viper/src/encoder/high/builtin_functions/interface.rs:125:13
5: <prusti_viper::encoder::encoder::Encoder as prusti_viper::encoder::high::builtin_functions::interface::HighBuiltinFunctionEncoderInterface>::encode_builtin_function_use_high
at ~/git/rust/pointerbender/prusti-dev/prusti-viper/src/encoder/high/builtin_functions/interface.rs:191:13
6: prusti_viper::encoder::mir::pure::interpreter::ExpressionBackwardInterpreter::unreachable_expr
at ~/git/rust/pointerbender/prusti-dev/prusti-viper/src/encoder/mir/pure/interpreter/mod.rs:730:47
7: <prusti_viper::encoder::mir::pure::interpreter::ExpressionBackwardInterpreter as prusti_viper::encoder::mir_interpreter::BackwardMirInterpreter>::apply_terminator
at ~/git/rust/pointerbender/prusti-dev/prusti-viper/src/encoder/mir/pure/interpreter/mod.rs:800:21
8: prusti_viper::encoder::mir_interpreter::run_backward_interpretation
at ~/git/rust/pointerbender/prusti-dev/prusti-viper/src/encoder/mir_interpreter.rs:69:30
9: prusti_viper::encoder::mir::pure::pure_functions::new_encoder::PureEncoder::encode_function_decl
at ~/git/rust/pointerbender/prusti-dev/prusti-viper/src/encoder/mir/pure/pure_functions/new_encoder.rs:217:25
10: prusti_viper::encoder::mir::pure::pure_functions::new_encoder::encode_function_decl
at ~/git/rust/pointerbender/prusti-dev/prusti-viper/src/encoder/mir/pure/pure_functions/new_encoder.rs:40:25
11: <prusti_viper::encoder::encoder::Encoder as prusti_viper::encoder::mir::pure::pure_functions::interface::PureFunctionEncoderInterface>::encode_pure_function_def::{{closure}}
at ~/git/rust/pointerbender/prusti-dev/prusti-viper/src/encoder/mir/pure/pure_functions/interface.rs:296:37
12: <prusti_viper::encoder::encoder::Encoder as prusti_viper::encoder::mir::pure::pure_functions::interface::PureFunctionEncoderInterface>::encode_pure_function_def
at ~/git/rust/pointerbender/prusti-dev/prusti-viper/src/encoder/mir/pure/pure_functions/interface.rs:278:89
13: prusti_viper::encoder::encoder::Encoder::process_encoding_queue
at ~/git/rust/pointerbender/prusti-dev/prusti-viper/src/encoder/encoder.rs:746:37
14: prusti_viper::verifier::Verifier::verify
at ~/git/rust/pointerbender/prusti-dev/prusti-viper/src/verifier.rs:247:9
15: prusti_driver::verifier::verify
at ~/git/rust/pointerbender/prusti-dev/prusti/src/verifier.rs:51:39
16: <prusti_driver::callbacks::PrustiCompilerCalls as rustc_driver::Callbacks>::after_analysis::{{closure}}
at ~/git/rust/pointerbender/prusti-dev/prusti/src/callbacks.rs:116:17
17: rustc_interface::passes::QueryContext::enter::{{closure}}
at /rustc/e7575f9670f3c837def3d186ae09366c75c7632e/compiler/rustc_interface/src/passes.rs:815:42
18: rustc_middle::ty::context::tls::enter_context::{{closure}}
at /rustc/e7575f9670f3c837def3d186ae09366c75c7632e/compiler/rustc_middle/src/ty/context.rs:1786:50
19: rustc_middle::ty::context::tls::set_tlv
at /rustc/e7575f9670f3c837def3d186ae09366c75c7632e/compiler/rustc_middle/src/ty/context.rs:1770:9
20: rustc_middle::ty::context::tls::enter_context
at /rustc/e7575f9670f3c837def3d186ae09366c75c7632e/compiler/rustc_middle/src/ty/context.rs:1786:9
21: rustc_interface::passes::QueryContext::enter
at /rustc/e7575f9670f3c837def3d186ae09366c75c7632e/compiler/rustc_interface/src/passes.rs:815:9
22: <prusti_driver::callbacks::PrustiCompilerCalls as rustc_driver::Callbacks>::after_analysis
at ~/git/rust/pointerbender/prusti-dev/prusti/src/callbacks.rs:71:9
23: <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>>
24: 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}>
25: <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 7a5c782d52 2022-05-13 15:04:27 UTC, built on 2022-05-14 20:22:53 UTC
query stack during panic:
end of query stack
[2022-05-17T13:16:09Z INFO prusti_common::stopwatch::log_level] [prusti-viper] Completed: encoding to Viper (0.788 seconds)
[2022-05-17T13:16:09Z INFO prusti_common::stopwatch::log_level] [prusti] Completed: main (1.243 seconds)
which is triggered from here:
https://github.com/viperproject/prusti-dev/blob/7a5c782d52c92a7e7ce208786efad64fb2cb7836/prusti-viper/src/encoder/mir/pure/pure_functions/interface.rs#L532-L544
Would it be acceptable to put the new encoder behind a configuration flag for now? I have it disabled in a local build since a few weeks because the pure function handling is not fully implemented yet :) Then I can create a PR for the fix for this Github issue.
(#729 is another known issue for which I have the new encoder temporarily disabled on my local build, btw)
Would it be acceptable to put the new encoder behind a configuration flag for now?
Yes, as long as it is enabled when running the tests (to avoid introducing regressions). Thanks!
Cool! I'll set the flag to globally enabled by default and selectively disable it for the regression test for this Github issue and #729 (together with a FIXME for when the pure function logic is fully implemented in the new encoder). This should help spot any further gaps which we can then document with regression tests to assist the refactoring :)
I created PR #1008 to fix the bug from this issue, but perhaps it's best to leave this issue open until the regression test also passes under the new encoder in the long run?