Missed Optimization: memcpy(a,b,sizeof(*a)) is slower than *a = *b

[danielsn]

In branch https://github.com/danielsn/rmc/tree/test-use-memcpy-in-hook

cd tests/kani/Refs 
kani main.rs

If you run with the HEAD of the branch, the test is very slow; if you run with one commit before HEAD, its fast. The only change is to emit memcpy(a,b,sizeof(*a)) vs*a = *b.

[danielsn]

Branch read-ptr-hook shows what we are actually trying to achieve, (i.e. how Rust actually does it).

[tautschnig]

A bunch of questions/comments:

1. Where can one find documentation on PtrRead to understand "how Rust actually does it?"
2. Do you really have to use memcpy for what you're trying to achieve?
3. Optimising within memcpy seems non-trivial as a lot of information is lost at that point.
4. I'll try to investigate nonetheless why the resulting byte extracts result in slowdown? (When yo say "very slow," what exactly do you mean?)

[danielsn]

Sorry for the scanty feature request.

1. To give some context: PtrRead is a Rust core library function

pub unsafe fn read<T>(src: [*const T](https://doc.rust-lang.org/std/primitive.pointer.html)) -> T

It implements the logical operation

result = *src;

However, under the hood, it is implemented as memcpy (or copy_nonoverlapping as it's called in rust). This is likely because the function is generic: making it a memcpy over a set of bytes is the easiest way to support the generic operation.
https://doc.rust-lang.org/src/core/ptr/mod.rs.html#685

When Kani was first written, we didn't have support for Rust intrinsics, so we used a hook mechanism to override the standard library functions that used the intrinsics. Now that we have support, we want to remove the hooks and use the actual standard library code. But, this means we end up using the copy_nonoverlapping intrinsic, which turns into memcpy, which gives us the performance issue.

[danielsn]

2. We can consider special casing the copy_nonoverlapping intrinsic and doing the optimization ourselves at that point. But given that

• this may also occur in C code,
• the optimization may require doing constant propagation
  it seemed to make sense to make this a CBMC optimization

3. The optimization should probably happen before the call to memcpy, rather than in the body of memcpy
4. By very slow, several Kani benchmarks that used to finish in seconds now do not complete in minutes

[tautschnig]

Studying the example mentioned at the top, I am not entirely convinced that memcpy is what is giving us grief: The changes in model-checking/kani@92ce4729518d appear to be introducing a loop that CBMC is unable to determine an unwinding bound for. (CBMC's memcpy does not use a loop.) Running CBMC on that "slower" code with --unwind 2 --unwinding-assertions yields 1) no failing unwinding assertions and 2) a modest increase in execution time from 0.45 seconds to 2.83 seconds. The following loop unwinding reports are new, and do not appear when running on the prior commit:

Unwinding loop _RNvMsl_NtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree8navigateINtNtB7_4node7NodeRefNtNtB10_6marker5DyingReuNtB1k_14LeafOrInternalE15first_leaf_edgeCs4DoytuIVp26_4main.0 iteration 1 file /home/ubuntu/.rustup/toolchains/nightly-2022-03-23-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 605 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<BorrowType, K, V, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionRINtNtNtB5_3ptr8non_null7NonNullINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node12InternalNodeReuEEE3mapINtB1h_6HandleINtB1h_7NodeRefNtNtB1h_6marker5DyingB2j_uNtB2Y_8InternalENtB2Y_4EdgeENCNvMse_B1h_IB2I_B2W_B2j_uNtB2Y_14LeafOrInternalE6ascend0ECs4DoytuIVp26_4main.0 iteration 1  thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionRINtNtNtB5_3ptr8non_null7NonNullINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node12InternalNodeReuEEE3mapINtB1h_6HandleINtB1h_7NodeRefNtNtB1h_6marker5DyingB2j_uNtB2Y_8InternalENtB2Y_4EdgeENCNvMse_B1h_IB2I_B2W_B2j_uNtB2Y_14LeafOrInternalE6ascend0ECs4DoytuIVp26_4main.1 iteration 1  thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node6HandleINtBL_7NodeRefNtNtBL_6marker5DyingReuNtB1W_8InternalENtB1W_4EdgeEE5ok_orIB1H_B1U_B2e_uNtB1W_14LeafOrInternalEECs4DoytuIVp26_4main.0 iteration 1  thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node6HandleINtBL_7NodeRefNtNtBL_6marker5DyingReuNtB1W_8InternalENtB1W_4EdgeEE5ok_orIB1H_B1U_B2e_uNtB1W_14LeafOrInternalEECs4DoytuIVp26_4main.1 iteration 1  thread 0
Unwinding loop _RNvMsh_NtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree8navigateINtNtB7_4node6HandleINtB10_7NodeRefNtNtB10_6marker5DyingReuNtB1y_4LeafENtB1y_4EdgeE16deallocating_endCs4DoytuIVp26_4main.0 iteration 1 file /home/ubuntu/.rustup/toolchains/nightly-2022-03-23-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 497 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Dying, K, V, alloc::collections::btree::node::marker::Leaf>, alloc::collections::btree::node::marker::Edge>>::deallocating_end thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionRINtNtNtB5_3ptr8non_null7NonNullINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node12InternalNodeReuEEE3mapINtB1h_6HandleINtB1h_7NodeRefNtNtB1h_6marker5DyingB2j_uNtB2Y_8InternalENtB2Y_4EdgeENCNvMse_B1h_IB2I_B2W_B2j_uNtB2Y_14LeafOrInternalE6ascend0ECs4DoytuIVp26_4main.0 iteration 1  thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionRINtNtNtB5_3ptr8non_null7NonNullINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node12InternalNodeReuEEE3mapINtB1h_6HandleINtB1h_7NodeRefNtNtB1h_6marker5DyingB2j_uNtB2Y_8InternalENtB2Y_4EdgeENCNvMse_B1h_IB2I_B2W_B2j_uNtB2Y_14LeafOrInternalE6ascend0ECs4DoytuIVp26_4main.1 iteration 1  thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node6HandleINtBL_7NodeRefNtNtBL_6marker5DyingReuNtB1W_8InternalENtB1W_4EdgeEE5ok_orIB1H_B1U_B2e_uNtB1W_14LeafOrInternalEECs4DoytuIVp26_4main.0 iteration 1  thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node6HandleINtBL_7NodeRefNtNtBL_6marker5DyingReuNtB1W_8InternalENtB1W_4EdgeEE5ok_orIB1H_B1U_B2e_uNtB1W_14LeafOrInternalEECs4DoytuIVp26_4main.1 iteration 1  thread 0
Unwinding loop _RNvMsl_NtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree8navigateINtNtB7_4node7NodeRefNtNtB10_6marker5DyingReuNtB1k_14LeafOrInternalE15first_leaf_edgeCs4DoytuIVp26_4main.0 iteration 1 file /home/ubuntu/.rustup/toolchains/nightly-2022-03-23-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 605 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<BorrowType, K, V, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
Unwinding loop _RNvMsl_NtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree8navigateINtNtB7_4node7NodeRefNtNtB10_6marker5DyingReuNtB1k_14LeafOrInternalE15first_leaf_edgeCs4DoytuIVp26_4main.0 iteration 1 file /home/ubuntu/.rustup/toolchains/nightly-2022-03-23-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 605 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<BorrowType, K, V, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionRINtNtNtB5_3ptr8non_null7NonNullINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node12InternalNodeReuEEE3mapINtB1h_6HandleINtB1h_7NodeRefNtNtB1h_6marker5DyingB2j_uNtB2Y_8InternalENtB2Y_4EdgeENCNvMse_B1h_IB2I_B2W_B2j_uNtB2Y_14LeafOrInternalE6ascend0ECs4DoytuIVp26_4main.0 iteration 1  thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionRINtNtNtB5_3ptr8non_null7NonNullINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node12InternalNodeReuEEE3mapINtB1h_6HandleINtB1h_7NodeRefNtNtB1h_6marker5DyingB2j_uNtB2Y_8InternalENtB2Y_4EdgeENCNvMse_B1h_IB2I_B2W_B2j_uNtB2Y_14LeafOrInternalE6ascend0ECs4DoytuIVp26_4main.1 iteration 1  thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node6HandleINtBL_7NodeRefNtNtBL_6marker5DyingReuNtB1W_8InternalENtB1W_4EdgeEE5ok_orIB1H_B1U_B2e_uNtB1W_14LeafOrInternalEECs4DoytuIVp26_4main.0 iteration 1  thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node6HandleINtBL_7NodeRefNtNtBL_6marker5DyingReuNtB1W_8InternalENtB1W_4EdgeEE5ok_orIB1H_B1U_B2e_uNtB1W_14LeafOrInternalEECs4DoytuIVp26_4main.1 iteration 1  thread 0
Unwinding loop _RNvMsh_NtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree8navigateINtNtB7_4node6HandleINtB10_7NodeRefNtNtB10_6marker5DyingReuNtB1y_4LeafENtB1y_4EdgeE17deallocating_nextCs4DoytuIVp26_4main.0 iteration 1 file /home/ubuntu/.rustup/toolchains/nightly-2022-03-23-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 449 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Dying, K, V, alloc::collections::btree::node::marker::Leaf>, alloc::collections::btree::node::marker::Edge>>::deallocating_next thread 0
Unwinding loop _RNvMsl_NtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree8navigateINtNtB7_4node7NodeRefNtNtB10_6marker5DyingReuNtB1k_14LeafOrInternalE15first_leaf_edgeCs4DoytuIVp26_4main.0 iteration 1 file /home/ubuntu/.rustup/toolchains/nightly-2022-03-23-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 605 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<BorrowType, K, V, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionRINtNtNtB5_3ptr8non_null7NonNullINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node12InternalNodeReuEEE3mapINtB1h_6HandleINtB1h_7NodeRefNtNtB1h_6marker5DyingB2j_uNtB2Y_8InternalENtB2Y_4EdgeENCNvMse_B1h_IB2I_B2W_B2j_uNtB2Y_14LeafOrInternalE6ascend0ECs4DoytuIVp26_4main.0 iteration 1  thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionRINtNtNtB5_3ptr8non_null7NonNullINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node12InternalNodeReuEEE3mapINtB1h_6HandleINtB1h_7NodeRefNtNtB1h_6marker5DyingB2j_uNtB2Y_8InternalENtB2Y_4EdgeENCNvMse_B1h_IB2I_B2W_B2j_uNtB2Y_14LeafOrInternalE6ascend0ECs4DoytuIVp26_4main.1 iteration 1  thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node6HandleINtBL_7NodeRefNtNtBL_6marker5DyingReuNtB1W_8InternalENtB1W_4EdgeEE5ok_orIB1H_B1U_B2e_uNtB1W_14LeafOrInternalEECs4DoytuIVp26_4main.0 iteration 1  thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node6HandleINtBL_7NodeRefNtNtBL_6marker5DyingReuNtB1W_8InternalENtB1W_4EdgeEE5ok_orIB1H_B1U_B2e_uNtB1W_14LeafOrInternalEECs4DoytuIVp26_4main.1 iteration 1  thread 0
Unwinding loop _RNvXsq_NtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree3mapINtB5_8IntoIterReuENtNtNtCsfBSZGGNiBQi_4core3ops4drop4Drop4dropCs4DoytuIVp26_4main.0 iteration 1 file /home/ubuntu/.rustup/toolchains/nightly-2022-03-23-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/map.rs line 1501 column 9 function <std::collections::btree_map::IntoIter<K, V> as std::ops::Drop>::drop thread 0
Unwinding loop _RNvMsl_NtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree8navigateINtNtB7_4node7NodeRefNtNtB10_6marker5DyingReuNtB1k_14LeafOrInternalE15first_leaf_edgeCs4DoytuIVp26_4main.0 iteration 1 file /home/ubuntu/.rustup/toolchains/nightly-2022-03-23-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 605 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<BorrowType, K, V, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionRINtNtNtB5_3ptr8non_null7NonNullINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node12InternalNodeReuEEE3mapINtB1h_6HandleINtB1h_7NodeRefNtNtB1h_6marker5DyingB2j_uNtB2Y_8InternalENtB2Y_4EdgeENCNvMse_B1h_IB2I_B2W_B2j_uNtB2Y_14LeafOrInternalE6ascend0ECs4DoytuIVp26_4main.0 iteration 1  thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionRINtNtNtB5_3ptr8non_null7NonNullINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node12InternalNodeReuEEE3mapINtB1h_6HandleINtB1h_7NodeRefNtNtB1h_6marker5DyingB2j_uNtB2Y_8InternalENtB2Y_4EdgeENCNvMse_B1h_IB2I_B2W_B2j_uNtB2Y_14LeafOrInternalE6ascend0ECs4DoytuIVp26_4main.1 iteration 1  thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node6HandleINtBL_7NodeRefNtNtBL_6marker5DyingReuNtB1W_8InternalENtB1W_4EdgeEE5ok_orIB1H_B1U_B2e_uNtB1W_14LeafOrInternalEECs4DoytuIVp26_4main.0 iteration 1  thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node6HandleINtBL_7NodeRefNtNtBL_6marker5DyingReuNtB1W_8InternalENtB1W_4EdgeEE5ok_orIB1H_B1U_B2e_uNtB1W_14LeafOrInternalEECs4DoytuIVp26_4main.1 iteration 1  thread 0
Unwinding loop _RNvMsh_NtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree8navigateINtNtB7_4node6HandleINtB10_7NodeRefNtNtB10_6marker5DyingReuNtB1y_4LeafENtB1y_4EdgeE16deallocating_endCs4DoytuIVp26_4main.0 iteration 1 file /home/ubuntu/.rustup/toolchains/nightly-2022-03-23-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 497 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Dying, K, V, alloc::collections::btree::node::marker::Leaf>, alloc::collections::btree::node::marker::Edge>>::deallocating_end thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionRINtNtNtB5_3ptr8non_null7NonNullINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node12InternalNodeReuEEE3mapINtB1h_6HandleINtB1h_7NodeRefNtNtB1h_6marker5DyingB2j_uNtB2Y_8InternalENtB2Y_4EdgeENCNvMse_B1h_IB2I_B2W_B2j_uNtB2Y_14LeafOrInternalE6ascend0ECs4DoytuIVp26_4main.0 iteration 1  thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionRINtNtNtB5_3ptr8non_null7NonNullINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node12InternalNodeReuEEE3mapINtB1h_6HandleINtB1h_7NodeRefNtNtB1h_6marker5DyingB2j_uNtB2Y_8InternalENtB2Y_4EdgeENCNvMse_B1h_IB2I_B2W_B2j_uNtB2Y_14LeafOrInternalE6ascend0ECs4DoytuIVp26_4main.1 iteration 1  thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node6HandleINtBL_7NodeRefNtNtBL_6marker5DyingReuNtB1W_8InternalENtB1W_4EdgeEE5ok_orIB1H_B1U_B2e_uNtB1W_14LeafOrInternalEECs4DoytuIVp26_4main.0 iteration 1  thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node6HandleINtBL_7NodeRefNtNtBL_6marker5DyingReuNtB1W_8InternalENtB1W_4EdgeEE5ok_orIB1H_B1U_B2e_uNtB1W_14LeafOrInternalEECs4DoytuIVp26_4main.1 iteration 1  thread 0
Unwinding loop _RNvMsl_NtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree8navigateINtNtB7_4node7NodeRefNtNtB10_6marker5DyingReuNtB1k_14LeafOrInternalE15first_leaf_edgeCs4DoytuIVp26_4main.0 iteration 1 file /home/ubuntu/.rustup/toolchains/nightly-2022-03-23-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 605 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<BorrowType, K, V, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
Unwinding loop _RNvMsl_NtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree8navigateINtNtB7_4node7NodeRefNtNtB10_6marker5DyingReuNtB1k_14LeafOrInternalE15first_leaf_edgeCs4DoytuIVp26_4main.0 iteration 1 file /home/ubuntu/.rustup/toolchains/nightly-2022-03-23-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 605 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<BorrowType, K, V, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionRINtNtNtB5_3ptr8non_null7NonNullINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node12InternalNodeReuEEE3mapINtB1h_6HandleINtB1h_7NodeRefNtNtB1h_6marker5DyingB2j_uNtB2Y_8InternalENtB2Y_4EdgeENCNvMse_B1h_IB2I_B2W_B2j_uNtB2Y_14LeafOrInternalE6ascend0ECs4DoytuIVp26_4main.0 iteration 1  thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionRINtNtNtB5_3ptr8non_null7NonNullINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node12InternalNodeReuEEE3mapINtB1h_6HandleINtB1h_7NodeRefNtNtB1h_6marker5DyingB2j_uNtB2Y_8InternalENtB2Y_4EdgeENCNvMse_B1h_IB2I_B2W_B2j_uNtB2Y_14LeafOrInternalE6ascend0ECs4DoytuIVp26_4main.1 iteration 1  thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node6HandleINtBL_7NodeRefNtNtBL_6marker5DyingReuNtB1W_8InternalENtB1W_4EdgeEE5ok_orIB1H_B1U_B2e_uNtB1W_14LeafOrInternalEECs4DoytuIVp26_4main.0 iteration 1  thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node6HandleINtBL_7NodeRefNtNtBL_6marker5DyingReuNtB1W_8InternalENtB1W_4EdgeEE5ok_orIB1H_B1U_B2e_uNtB1W_14LeafOrInternalEECs4DoytuIVp26_4main.1 iteration 1  thread 0
Unwinding loop _RNvMsh_NtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree8navigateINtNtB7_4node6HandleINtB10_7NodeRefNtNtB10_6marker5DyingReuNtB1y_4LeafENtB1y_4EdgeE17deallocating_nextCs4DoytuIVp26_4main.0 iteration 1 file /home/ubuntu/.rustup/toolchains/nightly-2022-03-23-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 449 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::Handle<alloc::collections::btree::node::NodeRef<alloc::collections::btree::node::marker::Dying, K, V, alloc::collections::btree::node::marker::Leaf>, alloc::collections::btree::node::marker::Edge>>::deallocating_next thread 0
Unwinding loop _RNvMsl_NtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree8navigateINtNtB7_4node7NodeRefNtNtB10_6marker5DyingReuNtB1k_14LeafOrInternalE15first_leaf_edgeCs4DoytuIVp26_4main.0 iteration 1 file /home/ubuntu/.rustup/toolchains/nightly-2022-03-23-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/collections/btree/navigate.rs line 605 column 9 function alloc::collections::btree::navigate::<impl alloc::collections::btree::node::NodeRef<BorrowType, K, V, alloc::collections::btree::node::marker::LeafOrInternal>>::first_leaf_edge thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionRINtNtNtB5_3ptr8non_null7NonNullINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node12InternalNodeReuEEE3mapINtB1h_6HandleINtB1h_7NodeRefNtNtB1h_6marker5DyingB2j_uNtB2Y_8InternalENtB2Y_4EdgeENCNvMse_B1h_IB2I_B2W_B2j_uNtB2Y_14LeafOrInternalE6ascend0ECs4DoytuIVp26_4main.0 iteration 1  thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionRINtNtNtB5_3ptr8non_null7NonNullINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node12InternalNodeReuEEE3mapINtB1h_6HandleINtB1h_7NodeRefNtNtB1h_6marker5DyingB2j_uNtB2Y_8InternalENtB2Y_4EdgeENCNvMse_B1h_IB2I_B2W_B2j_uNtB2Y_14LeafOrInternalE6ascend0ECs4DoytuIVp26_4main.1 iteration 1  thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node6HandleINtBL_7NodeRefNtNtBL_6marker5DyingReuNtB1W_8InternalENtB1W_4EdgeEE5ok_orIB1H_B1U_B2e_uNtB1W_14LeafOrInternalEECs4DoytuIVp26_4main.0 iteration 1  thread 0
Unwinding loop _RINvMNtCsfBSZGGNiBQi_4core6optionINtB3_6OptionINtNtNtNtCs5Ucdn1vYc9q_5alloc11collections5btree4node6HandleINtBL_7NodeRefNtNtBL_6marker5DyingReuNtB1W_8InternalENtB1W_4EdgeEE5ok_orIB1H_B1U_B2e_uNtB1W_14LeafOrInternalEECs4DoytuIVp26_4main.1 iteration 1  thread 0

[tautschnig]

Further investigation suggests that the root cause of those additional loops being triggered is constant propagation no longer taking place. This, in turn, is caused by thememcpy operation entailing byte extracts (this is expected) over a struct where only some members are constants. Therefore, at least at present, the entire expression is no longer a constant, and propagation through that byte extract operation is lost.

I will try to come up with a small example and will then try to implement additional simplification rules that make constant propagation possible again.

[tautschnig]

#6856 improves the constant propagation, and makes the Kani test case complete without having to specify unwinding constraints.