Creusot panic

[sarsko]

Could probably be reduced further, but, this code:

struct Heap {
    activity: Vec<f64>,
    heap: Vec<usize>,
    indices: Vec<usize>,
    num_vars: usize,
}

impl Heap {
    pub(crate) fn new(n: usize) -> Self {
        let mut heap = Heap { activity: Vec::new(), heap: Vec::new(), indices: Vec::new(), num_vars: 0 };

        let mut i = 0;
        #[invariant(heap.heap@.len() == i@)]
        while i < n {
            i += 1;
        }

        heap
    }
}

causes the following error. Happens both on current master as well as the one I was on before (5cc6cdd6). Could probably be reduced further. Goes away when the invariant is removed or swapped with something else.

thread 'rustc' panicked at 'called `Option::unwrap()` on a `None` value', creusot/src/cleanup_spec_closures.rs:86:78
stack backtrace:
   0:        0x104bcf103 - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h18ee12cba4ae5e52
   1:        0x104c2a19b - core::fmt::write::hd7e7d467f9d8fe88
   2:        0x104bc43d8 - std::io::Write::write_fmt::hff9bc24f737f0974
   3:        0x104bceefa - std::sys_common::backtrace::print::hedbb71888c21f343
   4:        0x104bd20f5 - std::panicking::default_hook::{{closure}}::h4529dd8014960be5
   5:        0x104bd1eff - std::panicking::default_hook::h47c5a3497bba75bf
   6:        0x1040ae0e4 - <creusot_rustc::ICE_HOOK as core::ops::deref::Deref>::deref::__static_ref_initialize::{{closure}}::h9eb145910f63b926
   7:        0x104bd27ac - std::panicking::rust_panic_with_hook::hf37a639388c6b084
   8:        0x104bd2502 - std::panicking::begin_panic_handler::{{closure}}::h03b7e72620869bd5
   9:        0x104bcf509 - std::sys_common::backtrace::__rust_end_short_backtrace::h7312d0fc382ee9c2
  10:        0x104bd227d - _rust_begin_unwind
  11:        0x104c55423 - core::panicking::panic_fmt::h3ae7848157c0dee2
  12:        0x104c554b7 - core::panicking::panic::hb60615cf3f304a9f
  13:        0x10424f094 - <creusot::cleanup_spec_closures::NoTranslateNoMoves as rustc_middle::mir::visit::MutVisitor>::visit_rvalue::h0cc0ffad7d037bd2
  14:        0x10424ecc3 - <creusot::cleanup_spec_closures::NoTranslateNoMoves as rustc_middle::mir::visit::MutVisitor>::visit_body::hef05e7a958d97306
  15:        0x10424dd32 - creusot::cleanup_spec_closures::cleanup_spec_closures::h8666efe7821d3509
  16:        0x1041cb8a8 - core::ops::function::FnOnce::call_once::h635b6c0a3268ff40
  17:        0x10fd5cd2f - rustc_query_impl[f5d20f126ea0a6a9]::plumbing::__rust_begin_short_backtrace::<rustc_query_impl[f5d20f126ea0a6a9]::query_impl::mir_built::dynamic_query::{closure#2}::{closure#0}, rustc_middle[4dbe5ed0d88c32a7]::query::erase::Erased<[u8; 8usize]>>
  18:        0x10fd16c9c - <rustc_query_impl[f5d20f126ea0a6a9]::query_impl::mir_built::dynamic_query::{closure#2} as core[884b9c30e773de97]::ops::function::FnOnce<(rustc_middle[4dbe5ed0d88c32a7]::ty::context::TyCtxt, rustc_span[3e5a5e309696de3f]::def_id::LocalDefId)>>::call_once
  19:        0x10fc33a63 - rustc_query_system[35918b82e96775f6]::query::plumbing::try_execute_query::<rustc_query_impl[f5d20f126ea0a6a9]::DynamicConfig<rustc_query_system[35918b82e96775f6]::query::caches::VecCache<rustc_span[3e5a5e309696de3f]::def_id::LocalDefId, rustc_middle[4dbe5ed0d88c32a7]::query::erase::Erased<[u8; 8usize]>>, false, false, false>, rustc_query_impl[f5d20f126ea0a6a9]::plumbing::QueryCtxt, true>
  20:        0x10fc5976c - rustc_query_impl[f5d20f126ea0a6a9]::query_impl::mir_built::get_query_incr::__rust_end_short_backtrace
  21:        0x10f7fb2ab - rustc_mir_transform[82d4cc7a1c5e769b]::check_unsafety::unsafety_check_result
  22:        0x10fd5ae9f - rustc_query_impl[f5d20f126ea0a6a9]::plumbing::__rust_begin_short_backtrace::<rustc_query_impl[f5d20f126ea0a6a9]::query_impl::unsafety_check_result::dynamic_query::{closure#2}::{closure#0}, rustc_middle[4dbe5ed0d88c32a7]::query::erase::Erased<[u8; 8usize]>>
  23:        0x10fcafc4c - <rustc_query_impl[f5d20f126ea0a6a9]::query_impl::unsafety_check_result::dynamic_query::{closure#2} as core[884b9c30e773de97]::ops::function::FnOnce<(rustc_middle[4dbe5ed0d88c32a7]::ty::context::TyCtxt, rustc_span[3e5a5e309696de3f]::def_id::LocalDefId)>>::call_once
  24:        0x10fc33a63 - rustc_query_system[35918b82e96775f6]::query::plumbing::try_execute_query::<rustc_query_impl[f5d20f126ea0a6a9]::DynamicConfig<rustc_query_system[35918b82e96775f6]::query::caches::VecCache<rustc_span[3e5a5e309696de3f]::def_id::LocalDefId, rustc_middle[4dbe5ed0d88c32a7]::query::erase::Erased<[u8; 8usize]>>, false, false, false>, rustc_query_impl[f5d20f126ea0a6a9]::plumbing::QueryCtxt, true>
  25:        0x10fc5f23c - rustc_query_impl[f5d20f126ea0a6a9]::query_impl::unsafety_check_result::get_query_incr::__rust_end_short_backtrace
  26:        0x10f744c43 - rustc_mir_transform[82d4cc7a1c5e769b]::mir_const
  27:        0x10fd5cd4f - rustc_query_impl[f5d20f126ea0a6a9]::plumbing::__rust_begin_short_backtrace::<rustc_query_impl[f5d20f126ea0a6a9]::query_impl::mir_const::dynamic_query::{closure#2}::{closure#0}, rustc_middle[4dbe5ed0d88c32a7]::query::erase::Erased<[u8; 8usize]>>
  28:        0x10fdee73c - <rustc_query_impl[f5d20f126ea0a6a9]::query_impl::mir_const::dynamic_query::{closure#2} as core[884b9c30e773de97]::ops::function::FnOnce<(rustc_middle[4dbe5ed0d88c32a7]::ty::context::TyCtxt, rustc_span[3e5a5e309696de3f]::def_id::LocalDefId)>>::call_once
  29:        0x10fc33a63 - rustc_query_system[35918b82e96775f6]::query::plumbing::try_execute_query::<rustc_query_impl[f5d20f126ea0a6a9]::DynamicConfig<rustc_query_system[35918b82e96775f6]::query::caches::VecCache<rustc_span[3e5a5e309696de3f]::def_id::LocalDefId, rustc_middle[4dbe5ed0d88c32a7]::query::erase::Erased<[u8; 8usize]>>, false, false, false>, rustc_query_impl[f5d20f126ea0a6a9]::plumbing::QueryCtxt, true>
  30:        0x10fc5995c - rustc_query_impl[f5d20f126ea0a6a9]::query_impl::mir_const::get_query_incr::__rust_end_short_backtrace
  31:        0x10f74520b - rustc_mir_transform[82d4cc7a1c5e769b]::mir_promoted
  32:        0x10fd58574 - rustc_query_impl[f5d20f126ea0a6a9]::plumbing::__rust_begin_short_backtrace::<rustc_query_impl[f5d20f126ea0a6a9]::query_impl::mir_promoted::dynamic_query::{closure#2}::{closure#0}, rustc_middle[4dbe5ed0d88c32a7]::query::erase::Erased<[u8; 16usize]>>
  33:        0x10fdeb620 - <rustc_query_impl[f5d20f126ea0a6a9]::query_impl::mir_promoted::dynamic_query::{closure#2} as core[884b9c30e773de97]::ops::function::FnOnce<(rustc_middle[4dbe5ed0d88c32a7]::ty::context::TyCtxt, rustc_span[3e5a5e309696de3f]::def_id::LocalDefId)>>::call_once
  34:        0x10fc2c130 - rustc_query_system[35918b82e96775f6]::query::plumbing::try_execute_query::<rustc_query_impl[f5d20f126ea0a6a9]::DynamicConfig<rustc_query_system[35918b82e96775f6]::query::caches::VecCache<rustc_span[3e5a5e309696de3f]::def_id::LocalDefId, rustc_middle[4dbe5ed0d88c32a7]::query::erase::Erased<[u8; 16usize]>>, false, false, false>, rustc_query_impl[f5d20f126ea0a6a9]::plumbing::QueryCtxt, true>
  35:        0x10fc59f7f - rustc_query_impl[f5d20f126ea0a6a9]::query_impl::mir_promoted::get_query_incr::__rust_end_short_backtrace
  36:        0x10e327484 - rustc_borrowck[b352028265e16b60]::consumers::get_body_with_borrowck_facts
  37:        0x1041cb610 - core::ops::function::FnOnce::call_once::h39a0ca28f0c17863
  38:        0x10fd5851f - rustc_query_impl[f5d20f126ea0a6a9]::plumbing::__rust_begin_short_backtrace::<rustc_query_impl[f5d20f126ea0a6a9]::query_impl::mir_borrowck::dynamic_query::{closure#2}::{closure#0}, rustc_middle[4dbe5ed0d88c32a7]::query::erase::Erased<[u8; 8usize]>>
  39:        0x10fcabb8c - <rustc_query_impl[f5d20f126ea0a6a9]::query_impl::mir_borrowck::dynamic_query::{closure#2} as core[884b9c30e773de97]::ops::function::FnOnce<(rustc_middle[4dbe5ed0d88c32a7]::ty::context::TyCtxt, rustc_span[3e5a5e309696de3f]::def_id::LocalDefId)>>::call_once
  40:        0x10fc33a63 - rustc_query_system[35918b82e96775f6]::query::plumbing::try_execute_query::<rustc_query_impl[f5d20f126ea0a6a9]::DynamicConfig<rustc_query_system[35918b82e96775f6]::query::caches::VecCache<rustc_span[3e5a5e309696de3f]::def_id::LocalDefId, rustc_middle[4dbe5ed0d88c32a7]::query::erase::Erased<[u8; 8usize]>>, false, false, false>, rustc_query_impl[f5d20f126ea0a6a9]::plumbing::QueryCtxt, true>
  41:        0x10fc61d7c - rustc_query_impl[f5d20f126ea0a6a9]::query_impl::mir_borrowck::get_query_incr::__rust_end_short_backtrace
  42:        0x1041dacc4 - creusot::callbacks::get_body::he898777d883102c1
  43:        0x10422ad6c - creusot::ctx::TranslationCtx::body_with_facts::he85f03c33c0dfbd0
  44:        0x10428a5f2 - creusot::backend::program::translate_function::h9e405c723936b471
  45:        0x1042d93b0 - creusot::backend::Why3Generator::translate::h050584a187be5d3d
  46:        0x104235488 - creusot::translation::after_analysis::hbd99432799b58a86
  47:        0x10424110a - rustc_middle::ty::context::GlobalCtxt::enter::h68d184efa2661deb
  48:        0x1041daba4 - <creusot::callbacks::ToWhy as rustc_driver_impl::Callbacks>::after_expansion::h6d4d9291fcd8fcea
  49:        0x10e9246fe - <rustc_interface[879a65ad9efb96ec]::interface::Compiler>::enter::<rustc_driver_impl[e78d466f615ba596]::run_compiler::{closure#1}::{closure#2}, core[884b9c30e773de97]::result::Result<core[884b9c30e773de97]::option::Option<rustc_interface[879a65ad9efb96ec]::queries::Linker>, rustc_span[3e5a5e309696de3f]::ErrorGuaranteed>>
  50:        0x10e8c5a9c - rustc_span[3e5a5e309696de3f]::set_source_map::<core[884b9c30e773de97]::result::Result<(), rustc_span[3e5a5e309696de3f]::ErrorGuaranteed>, rustc_interface[879a65ad9efb96ec]::interface::run_compiler<core[884b9c30e773de97]::result::Result<(), rustc_span[3e5a5e309696de3f]::ErrorGuaranteed>, rustc_driver_impl[e78d466f615ba596]::run_compiler::{closure#1}>::{closure#0}::{closure#0}>
  51:        0x10e8d1c0b - <scoped_tls[4af701600c3e4db8]::ScopedKey<rustc_span[3e5a5e309696de3f]::SessionGlobals>>::set::<rustc_interface[879a65ad9efb96ec]::interface::run_compiler<core[884b9c30e773de97]::result::Result<(), rustc_span[3e5a5e309696de3f]::ErrorGuaranteed>, rustc_driver_impl[e78d466f615ba596]::run_compiler::{closure#1}>::{closure#0}, core[884b9c30e773de97]::result::Result<(), rustc_span[3e5a5e309696de3f]::ErrorGuaranteed>>
  52:        0x10e8cadf0 - std[f72bc4faa767410f]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[879a65ad9efb96ec]::util::run_in_thread_pool_with_globals<rustc_interface[879a65ad9efb96ec]::interface::run_compiler<core[884b9c30e773de97]::result::Result<(), rustc_span[3e5a5e309696de3f]::ErrorGuaranteed>, rustc_driver_impl[e78d466f615ba596]::run_compiler::{closure#1}>::{closure#0}, core[884b9c30e773de97]::result::Result<(), rustc_span[3e5a5e309696de3f]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[884b9c30e773de97]::result::Result<(), rustc_span[3e5a5e309696de3f]::ErrorGuaranteed>>
  53:        0x10e8c3d49 - <<std[f72bc4faa767410f]::thread::Builder>::spawn_unchecked_<rustc_interface[879a65ad9efb96ec]::util::run_in_thread_pool_with_globals<rustc_interface[879a65ad9efb96ec]::interface::run_compiler<core[884b9c30e773de97]::result::Result<(), rustc_span[3e5a5e309696de3f]::ErrorGuaranteed>, rustc_driver_impl[e78d466f615ba596]::run_compiler::{closure#1}>::{closure#0}, core[884b9c30e773de97]::result::Result<(), rustc_span[3e5a5e309696de3f]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[884b9c30e773de97]::result::Result<(), rustc_span[3e5a5e309696de3f]::ErrorGuaranteed>>::{closure#1} as core[884b9c30e773de97]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  54:        0x104bdc119 - std::sys::unix::thread::Thread::new::thread_start::ha1eefe3ccfceb164
  55:     0x7ff80d4241d3 - __pthread_start

note: Creusot has panic-ed!
  |
  = note: Oops, that shouldn't have happened, sorry about that.
  = note: Please report this bug over here: https://github.com/xldenis/creusot/issues/new

query stack during panic:
#0 [mir_built] building MIR for `vsids::<impl at Scratch/src/vsids.rs:65:1: 65:10>::new`
#1 [unsafety_check_result] unsafety-checking `vsids::<impl at Scratch/src/vsids.rs:65:1: 65:10>::new`
#2 [mir_const] preparing `vsids::<impl at Scratch/src/vsids.rs:65:1: 65:10>::new` for borrow checking
#3 [mir_promoted] promoting constants in MIR for `vsids::<impl at Scratch/src/vsids.rs:65:1: 65:10>::new`
#4 [mir_borrowck] borrow-checking `vsids::<impl at Scratch/src/vsids.rs:65:1: 65:10>::new`
end of query stack

[xldenis]

I can't reproduce this? the test case above works on the latest master for me.

[sarsko]

Hmm, I updated to most recent master and it is failing for me. I have a src/lib.rs as so:

#![feature(type_ascription)]
#![cfg_attr(not(creusot), feature(stmt_expr_attributes, proc_macro_hygiene))]
#![allow(unused_imports)]
#![allow(unused)]
#![allow(dead_code)]
#![allow(non_snake_case)]
mod test;

and a src/test.rs like so:

extern crate creusot_contracts;
use creusot_contracts::*;

struct Heap {
    activity: Vec<f64>,
    heap: Vec<usize>,
    indices: Vec<usize>,
    num_vars: usize,
}

impl Heap {
    pub(crate) fn new(n: usize) -> Self {
        let mut heap = Heap { activity: Vec::new(), heap: Vec::new(), indices: Vec::new(), num_vars: 0 };

        let mut i = 0;
        #[invariant(heap.heap@.len() == i@)]
        while i < n {
            i += 1;
        }

        heap
    }
}

and a Cargo.toml like so:

[package]
name = "Scratch"
version = "0.1.0"
edition = "2021"

[dependencies]
creusot-contracts = { git = "https://github.com/xldenis/creusot", version = "^0", rev = "e1a80db" }

And then it panics on unwrap when doing: cargo creusot -- -p Scratch