Crash in cond_with_alloc on small bdd (order dependent)

[dbueno]

If you put this in a project and compile it against rsdd (01a7723) and run:

extern crate rsdd;
use rsdd::builder::bdd::RobddBuilder;
use rsdd::builder::cache::LruIteTable;
use rsdd::builder::BottomUpBuilder;
use rsdd::repr::{BddPtr, VarLabel};

fn main() {
    let builder = RobddBuilder::<LruIteTable<BddPtr>>::new_with_linear_order(0);
    let vars: Vec<VarLabel> = std::iter::repeat_with(|| builder.new_var(true).0)
        .take(15)
        .collect();
    let acc = builder.ite(
        builder.var(vars[8], true),
        builder.var(vars[9], true),
        builder.true_ptr(),
    );
    dbg!(acc);
    let c = (VarLabel::new(8), builder.var(vars[0], true)); // FIRST
    dbg!(c);
    let acc = builder.compose(acc, c.0, c.1);
    dbg!(acc);
    let c = (VarLabel::new(9), builder.var(vars[1], true)); // SECOND
    dbg!(c);
    let acc = builder.compose(acc, c.0, c.1);
    dbg!(acc);
}

It crashes. If you swap lines FIRST and SECOND it doesn't crash.

There is an index into alloc in cond_with_alloc that is out of bounds.

Stack trace:

thread 'main' panicked at /Users/denbuen/.cargo/git/checkouts/rsdd-70c708972b058342/01a7723/src/builder/bdd/robdd.rs:196:34:
index out of bounds: the len is 0 but the index is 0
stack backtrace:
   0:        0x1025ce754 - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::he395ae20fca1ef41
   1:        0x1025dc620 - core::fmt::write::haacaf63c647e4106
   2:        0x1025d02b8 - std::io::Write::write_fmt::hcc90f2571dcb9970
   3:        0x1025ce5a8 - std::sys_common::backtrace::print::ha2445e687f87d0f3
   4:        0x1025cf08c - std::panicking::default_hook::{{closure}}::hc7b880a562e56458
   5:        0x1025cede8 - std::panicking::default_hook::h8fd7f383a85001a1
   6:        0x1025cf804 - std::panicking::rust_panic_with_hook::h99baae440a1a295b
   7:        0x1025cf5cc - std::panicking::begin_panic_handler::{{closure}}::hea77d56975627739
   8:        0x1025ce974 - std::sys_common::backtrace::__rust_end_short_backtrace::h7afafd01e3c2d80e
   9:        0x1025cf344 - _rust_begin_unwind
  10:        0x1025e2d58 - core::panicking::panic_fmt::h5e7349beebf2ad6e
  11:        0x1025e2eb0 - core::panicking::panic_bounds_check::h3de19823c79388aa
  12:        0x10258a214 - <usize as core::slice::index::SliceIndex<[T]>>::index::h73df678068e5c4a5
                               at /private/tmp/nix-build-rustc-1.78.0.drv-0/rustc-1.78.0-src/library/core/src/slice/index.rs:264:10
  13:        0x10258aad8 - core::slice::index::<impl core::ops::index::Index<I> for [T]>::index::h2438b636c7ee056b
                               at /private/tmp/nix-build-rustc-1.78.0.drv-0/rustc-1.78.0-src/library/core/src/slice/index.rs:18:9
  14:        0x10258aad8 - <alloc::vec::Vec<T,A> as core::ops::index::Index<I>>::index::hcd13fd21b7b5374e
                               at /private/tmp/nix-build-rustc-1.78.0.drv-0/rustc-1.78.0-src/library/alloc/src/vec/mod.rs:2829:9
  15:        0x10258e3d4 - rsdd::builder::bdd::robdd::RobddBuilder<T>::cond_with_alloc::he6233a6ad090a152
                               at /Users/denbuen/.cargo/git/checkouts/rsdd-70c708972b058342/01a7723/src/builder/bdd/robdd.rs:196:34
  16:        0x10258e134 - rsdd::builder::bdd::robdd::RobddBuilder<T>::cond_with_alloc::he6233a6ad090a152
                               at /Users/denbuen/.cargo/git/checkouts/rsdd-70c708972b058342/01a7723/src/builder/bdd/robdd.rs:202:25
  17:        0x10258dabc - <rsdd::builder::bdd::robdd::RobddBuilder<T> as rsdd::builder::bdd::builder::BddBuilder>::cond_helper::hdb6771a9ea4823dd
                               at /Users/denbuen/.cargo/git/checkouts/rsdd-70c708972b058342/01a7723/src/builder/bdd/robdd.rs:86:9
  18:        0x10258eb58 - rsdd::builder::bdd::builder::<impl rsdd::builder::BottomUpBuilder<rsdd::repr::bdd::BddPtr> for T>::condition::h7b258a965d65240a
                               at /Users/denbuen/.cargo/git/checkouts/rsdd-70c708972b058342/01a7723/src/builder/bdd/builder.rs:167:17
  19:        0x10258eaa0 - rsdd::builder::bdd::builder::<impl rsdd::builder::BottomUpBuilder<rsdd::repr::bdd::BddPtr> for T>::exists::h1bda9750aeff7d45
                               at /Users/denbuen/.cargo/git/checkouts/rsdd-70c708972b058342/01a7723/src/builder/bdd/builder.rs:161:18
  20:        0x10258decc - rsdd::builder::BottomUpBuilder::compose::h800650db86284d83
                               at /Users/denbuen/.cargo/git/checkouts/rsdd-70c708972b058342/01a7723/src/builder/mod.rs:60:9
  21:        0x10258c60c - mu_calculus_bdd_mc::test_bug::h8b55024bae65aa0a
                               at /Users/denbuen/DontTouch/work/inprogress/proj/src/main.rs:601:15
  22:        0x10258c788 - mu_calculus_bdd_mc::main::hab7bd1394f490286
                               at /Users/denbuen/DontTouch/work/inprogress/proj/src/main.rs:612:5
  23:        0x102588ee0 - core::ops::function::FnOnce::call_once::h9598a2e15e6eeeeb
                               at /private/tmp/nix-build-rustc-1.78.0.drv-0/rustc-1.78.0-src/library/core/src/ops/function.rs:250:5
  24:        0x102596864 - std::sys_common::backtrace::__rust_begin_short_backtrace::ha7dbbf5c76d19971
                               at /private/tmp/nix-build-rustc-1.78.0.drv-0/rustc-1.78.0-src/library/std/src/sys_common/backtrace.rs:155:18
  25:        0x10258bc30 - std::rt::lang_start::{{closure}}::hacd6ff232f341af4
                               at /private/tmp/nix-build-rustc-1.78.0.drv-0/rustc-1.78.0-src/library/std/src/rt.rs:166:18
  26:        0x1025cf21c - std::panicking::try::h930b3e414b1d9cbc
  27:        0x1025c8ca8 - std::rt::lang_start_internal::he9a392d3f16eaee8
  28:        0x10258bbfc - std::rt::lang_start::h4d4d5e1e8f8d49b8
                               at /private/tmp/nix-build-rustc-1.78.0.drv-0/rustc-1.78.0-src/library/std/src/rt.rs:165:17
  29:        0x10258c7b4 - _main

[mattxwang]

Hello @dbueno! I'm just lurking (haven't worked on the project in about a year), but one of the suspect lines looks pretty similar to what someone else ran into on a private project. Do you want to try the (bandaid) fix I made in #182? This looks like it might help?

(also, for the NEU folks I don't mind helping troubleshoot - esp since there's a pretty good chance that I've touched the bug 😅 )