graphalgs icon indicating copy to clipboard operation
graphalgs copied to clipboard

Check `count_spanning_trees` on UB

Open starovoid opened this issue 1 year ago • 0 comments

MIRI finds UB in the safe API of the nalgebra crate.

Need to check if there really is an UB error, or it is a MIRI bug.

pub fn count_spanning_trees<G>(graph: G, root: G::NodeId) -> usize
where
    G: IntoEdges + IntoNodeIdentifiers + NodeCount + NodeIndexable + GraphProp,
{
    let mut mtrx = laplacian_matrix(graph, |_| 1.0f32);
    mtrx = mtrx.remove_row(graph.to_index(root)); // <==== HERE
    mtrx = mtrx.remove_column(graph.to_index(root));
    mtrx.determinant() as usize
}

Trace

test spec::st::test::test_count_spanning_trees ... error: Undefined Behavior: attempting a read access using <96507504> at alloc44255162[0x4], but that tag does not exist in the borrow stack for this location
    --> /home/starovoid/.cargo/registry/src/index.crates.io-6f17d22bba15001f/nalgebra-0.33.2/src/base/edition.rs:1114:9
     |
1114 | /         ptr::copy(
1115 | |             ptr_in.add(curr_i + (k + 1) * nremove),
1116 | |             ptr_out.add(curr_i),
1117 | |             new_nrows,
1118 | |         );
     | |         ^
     | |         |
     | |_________attempting a read access using <96507504> at alloc44255162[0x4], but that tag does not exist in the borrow stack for this location
     |           this error occurs as part of an access at alloc44255162[0x4..0x8]
     |
     = help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
     = help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
help: <96507504> was created by a SharedReadOnly retag at offsets [0x0..0x10]
    --> src/spec/st.rs:84:12
     |
84   |     mtrx = mtrx.remove_row(graph.to_index(root));
     |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
help: <96507504> was later invalidated at offsets [0x0..0x10] by a Unique function-entry retag inside this call
    --> src/spec/st.rs:84:12
     |
84   |     mtrx = mtrx.remove_row(graph.to_index(root));
     |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
     = note: BACKTRACE (of the first span) on thread `spec::st::test:`:
     = note: inside `nalgebra::base::edition::compress_rows::<f32>` at /home/starovoid/.cargo/registry/src/index.crates.io-6f17d22bba15001f/nalgebra-0.33.2/src/base/edition.rs:1114:9: 1118:10
     = note: inside `nalgebra::base::edition::<impl nalgebra::Matrix<f32, nalgebra::Dyn, nalgebra::Dyn, nalgebra::VecStorage<f32, nalgebra::Dyn, nalgebra::Dyn>>>::remove_rows_generic::<nalgebra::Const<1>>` at /home/starovoid/.cargo/registry/src/index.crates.io-6f17d22bba15001f/nalgebra-0.33.2/src/base/edition.rs:600:17: 606:18
     = note: inside `nalgebra::base::edition::<impl nalgebra::Matrix<f32, nalgebra::Dyn, nalgebra::Dyn, nalgebra::VecStorage<f32, nalgebra::Dyn, nalgebra::Dyn>>>::remove_fixed_rows::<1>` at /home/starovoid/.cargo/registry/src/index.crates.io-6f17d22bba15001f/nalgebra-0.33.2/src/base/edition.rs:566:9: 566:48
     = note: inside `nalgebra::base::edition::<impl nalgebra::Matrix<f32, nalgebra::Dyn, nalgebra::Dyn, nalgebra::VecStorage<f32, nalgebra::Dyn, nalgebra::Dyn>>>::remove_row` at /home/starovoid/.cargo/registry/src/index.crates.io-6f17d22bba15001f/nalgebra-0.33.2/src/base/edition.rs:556:9: 556:39
note: inside `spec::st::count_spanning_trees::<&petgraph::Graph<u32, f32, petgraph::Undirected>>`
    --> src/spec/st.rs:84:12
     |
84   |     mtrx = mtrx.remove_row(graph.to_index(root));
     |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
note: inside `spec::st::test::test_count_spanning_trees`
    --> src/spec/st.rs:99:20
     |
99   |         assert_eq!(count_spanning_trees(&graph, n0), 0);
     |                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
note: inside closure
    --> src/spec/st.rs:94:35
     |
93   |     #[test]
     |     ------- in this procedural macro expansion
94   |     fn test_count_spanning_trees() {
     |                                   ^
     = note: this error originates in the attribute macro `test` (in Nightly builds, run with -Z macro-backtrace for more info)

note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace

error: aborting due to 1 previous error

error: test failed, to rerun pass `--lib`

starovoid avatar Dec 18 '24 19:12 starovoid