viperproject
Prusti performance deteriorates for larger structs that derive `PartialEq`
For the following Rust program:
use prusti_contracts::*;
#[derive(Copy, Clone, PartialEq, Eq)]
pub struct A {
pub field0: usize,
pub field1: isize,
pub field2: u64,
pub field3: i64,
pub field4: [i32; 64],
pub field5: [u32; 64],
pub field6: usize,
pub field7: isize,
pub field8: u64,
pub field9: i64,
pub field10: [i32; 64],
pub field11: [u32; 64],
pub field12: usize,
pub field13: isize,
pub field14: bool,
pub field15: bool,
}
Prusti takes very long to go through the encoding steps:
[2022-04-06T10:55:00Z INFO prusti_viper::encoder::encoder] Encoding: prusti_example::<A as std::clone::Clone>::clone (prusti_example::{impl#1}::clone)
[2022-04-06T10:55:00Z INFO prusti_viper::encoder::encoder] Encoding: prusti_example::<A as std::cmp::PartialEq>::eq (prusti_example::{impl#3}::eq)
[2022-04-06T10:58:32Z INFO prusti_viper::encoder::encoder] Encoding: prusti_example::<A as std::cmp::PartialEq>::ne (prusti_example::{impl#3}::ne)
[2022-04-06T11:01:51Z INFO prusti_viper::encoder::encoder] Encoding: prusti_example::<A as std::cmp::Eq>::assert_receiver_is_total_eq (prusti_example::{impl#5}::assert_receiver_is_total_eq)
Here <A as std::cmp::PartialEq>::eq and <A as std::cmp::PartialEq>::ne take about 3.5 minutes each to be encoded (verification takes 104 seconds for both methods).
Memory usage is normal during the encoding, but CPU usage is at 100%. Probably this is related to issue #854 but the problem of exponential blow-up of the backwards interpretation manifests slightly different here. The expanded derive macro looks like:
#[automatically_derived]
#[allow(unused_qualifications)]
impl ::core::cmp::PartialEq for A {
#[inline]
fn eq(&self, other: &A) -> bool {
match *other {
A {
field0: ref __self_1_0,
field1: ref __self_1_1,
field2: ref __self_1_2,
field3: ref __self_1_3,
field4: ref __self_1_4,
field5: ref __self_1_5,
field6: ref __self_1_6,
field7: ref __self_1_7,
field8: ref __self_1_8,
field9: ref __self_1_9,
field10: ref __self_1_10,
field11: ref __self_1_11,
field12: ref __self_1_12,
field13: ref __self_1_13,
field14: ref __self_1_14,
field15: ref __self_1_15,
} => match *self {
A {
field0: ref __self_0_0,
field1: ref __self_0_1,
field2: ref __self_0_2,
field3: ref __self_0_3,
field4: ref __self_0_4,
field5: ref __self_0_5,
field6: ref __self_0_6,
field7: ref __self_0_7,
field8: ref __self_0_8,
field9: ref __self_0_9,
field10: ref __self_0_10,
field11: ref __self_0_11,
field12: ref __self_0_12,
field13: ref __self_0_13,
field14: ref __self_0_14,
field15: ref __self_0_15,
} => {
(*__self_0_0) == (*__self_1_0)
&& (*__self_0_1) == (*__self_1_1)
&& (*__self_0_2) == (*__self_1_2)
&& (*__self_0_3) == (*__self_1_3)
&& (*__self_0_4) == (*__self_1_4)
&& (*__self_0_5) == (*__self_1_5)
&& (*__self_0_6) == (*__self_1_6)
&& (*__self_0_7) == (*__self_1_7)
&& (*__self_0_8) == (*__self_1_8)
&& (*__self_0_9) == (*__self_1_9)
&& (*__self_0_10) == (*__self_1_10)
&& (*__self_0_11) == (*__self_1_11)
&& (*__self_0_12) == (*__self_1_12)
&& (*__self_0_13) == (*__self_1_13)
&& (*__self_0_14) == (*__self_1_14)
&& (*__self_0_15) == (*__self_1_15)
}
},
}
}
#[inline]
fn ne(&self, other: &A) -> bool {
match *other {
A {
field0: ref __self_1_0,
field1: ref __self_1_1,
field2: ref __self_1_2,
field3: ref __self_1_3,
field4: ref __self_1_4,
field5: ref __self_1_5,
field6: ref __self_1_6,
field7: ref __self_1_7,
field8: ref __self_1_8,
field9: ref __self_1_9,
field10: ref __self_1_10,
field11: ref __self_1_11,
field12: ref __self_1_12,
field13: ref __self_1_13,
field14: ref __self_1_14,
field15: ref __self_1_15,
} => match *self {
A {
field0: ref __self_0_0,
field1: ref __self_0_1,
field2: ref __self_0_2,
field3: ref __self_0_3,
field4: ref __self_0_4,
field5: ref __self_0_5,
field6: ref __self_0_6,
field7: ref __self_0_7,
field8: ref __self_0_8,
field9: ref __self_0_9,
field10: ref __self_0_10,
field11: ref __self_0_11,
field12: ref __self_0_12,
field13: ref __self_0_13,
field14: ref __self_0_14,
field15: ref __self_0_15,
} => {
(*__self_0_0) != (*__self_1_0)
|| (*__self_0_1) != (*__self_1_1)
|| (*__self_0_2) != (*__self_1_2)
|| (*__self_0_3) != (*__self_1_3)
|| (*__self_0_4) != (*__self_1_4)
|| (*__self_0_5) != (*__self_1_5)
|| (*__self_0_6) != (*__self_1_6)
|| (*__self_0_7) != (*__self_1_7)
|| (*__self_0_8) != (*__self_1_8)
|| (*__self_0_9) != (*__self_1_9)
|| (*__self_0_10) != (*__self_1_10)
|| (*__self_0_11) != (*__self_1_11)
|| (*__self_0_12) != (*__self_1_12)
|| (*__self_0_13) != (*__self_1_13)
|| (*__self_0_14) != (*__self_1_14)
|| (*__self_0_15) != (*__self_1_15)
}
},
}
}
}
Since the code is auto-generated by the Derive macro and there are no predicates, the same work-around as in #854 can't be easily applied here, although it might be possible to manually implement the PartialEq trait and mark its methods as #[trusted] or split its implementation into multiple pure functions in order to limit the exponential blow-up.
One important detail I just noticed, is that the encoding problem in this issue only happens when running Prusti in debug mode. In release mode the encoding performance problem is not there, but verification still takes around 90 seconds for each method.
One important detail I just noticed, is that the encoding problem in this issue only happens when running Prusti in debug mode. In release mode the encoding performance problem is not there
Prusti code contains many debug asserts that check the consistency of the state at each encoding step and could be the reason for a significant slowdown.
but verification still takes around 90 seconds for each method.
Verification time is exponential to the number of branches on the MIR level and &&/|| are generating a lot of them.
