Remove forked rust dependency

[sskeirik]

This PR removes the forked rust dependency by implementing the following two functions directly in smir_pretty (instead of in a forked rust compiler):

• visited_tys
• visited_alloc_ids

This is done by extending the functionality of LinkNameCollector to also collect Ty and AllocId mappings and renaming the combined collector to InternedValueCollector.

EDIT: When running the panic example on rustc master, there is some weirdness where a static item called:

alloc::alloc::__rust_no_alloc_shim_is_unstable

is generated which has no body. This static item appears to be referenced from several different allocations (can be seen by chasing pointers in allocations provenance table). If this funny static item is findable on other machines, we should document this issue. It may well be that this is an empty type that is never used at runtime, but I haven't gone in to check this yet.

[jberthold]

Going to test the integration with mir-semantics with this PR

[jberthold]

The integration tests in mir-semantics are failing when we use smir_pretty from this PR.

There are some problems with what becomes GlobalAllocs in K (the field allocs in the smir.json)

1. The field has changed structure.
   • Previously it was a list of lists with two elements each, one AllocId (actually a MIRInt) and one GlobalAllocItem
   • Now we are getting a single json object, which has fields keyed by the MIRInts from before, and containing the GlobalAllocItems that were previously paired up
2. The Memory items have changed structure.
   • Previously we had Allocation (see ty.md), an object with fields bytes, provenance, align, mutability
   • Now we have a list with two elements. The second one is again Allocation with the 4 fields, but the first one is another object containing a single field RigidTy (observed values from panic_example are "Str", { "Array": [..] }, { "Ref": [..] } - the latter two argument lists being heterogenous).

There may be other changes in the json, these are the ones making the integration test fail.

[jberthold]

Another issue is this panic in the compiler. Could this be an unresolved issue in master upstream?

jost@freshcode-1:~/work/RV/code/kmir/smir_pretty$ cat tmp/string.rs 
fn main() {
    let a:String = "abcd".to_string();
    assert!(a == "abcd");
}

jost@freshcode-1:~/work/RV/code/kmir/smir_pretty$ ./run.sh tmp/string.rs 
thread 'rustc' panicked at compiler/rustc_middle/src/ty/predicate.rs:533:9:
`<[core::fmt::rt::Argument<'_>] as std::marker::Sized>` has escaping bound vars, so it cannot be wrapped in a dummy binder.
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
[error: 101]--jost@freshcode-1:

Stack trace here:

[error: 101]--jost@freshcode-1:~/work/RV/code/kmir//smir_pretty$ RUST_BACKTRACE=1 ./run.sh tmp/string.rs 
thread 'rustc' panicked at compiler/rustc_middle/src/ty/predicate.rs:533:9:
`<[core::fmt::rt::Argument<'_>] as std::marker::Sized>` has escaping bound vars, so it cannot be wrapped in a dummy binder.
stack backtrace:
   0: rust_begin_unwind
   1: core::panicking::panic_fmt
   2: <rustc_middle::ty::predicate::Predicate as rustc_type_ir::upcast::UpcastFrom<rustc_middle::ty::context::TyCtxt, rustc_type_ir::predicate::TraitRef<rustc_middle::ty::context::TyCtxt>>>::upcast_from
   3: rustc_trait_selection::traits::type_known_to_meet_bound_modulo_regions
   4: rustc_ty_utils::common_traits::is_item_raw
      [... omitted 2 frames ...]
   5: rustc_middle::query::plumbing::query_get_at::<rustc_query_system::query::caches::DefaultCache<rustc_middle::ty::ParamEnvAnd<rustc_middle::ty::Ty>, rustc_middle::query::erase::Erased<[u8; 1]>>>
   6: <rustc_middle::ty::Ty>::is_sized
   7: rustc_ty_utils::layout::layout_of_uncached
   8: rustc_ty_utils::layout::layout_of
      [... omitted 2 frames ...]
   9: <rustc_middle::ty::layout::LayoutCx as rustc_middle::ty::layout::LayoutOf>::spanned_layout_of
  10: core::iter::adapters::try_process::<core::iter::adapters::by_ref_sized::ByRefSized<core::iter::adapters::map::Map<core::slice::iter::Iter<rustc_middle::ty::FieldDef>, rustc_ty_utils::layout::layout_of_uncached::{closure#13}::{closure#0}>>, rustc_abi::layout::ty::TyAndLayout<rustc_middle::ty::Ty>, core::result::Result<core::convert::Infallible, &rustc_middle::ty::layout::LayoutError>, <core::iter::adapters::map::Map<core::slice::iter::Iter<rustc_middle::ty::FieldDef>, rustc_ty_utils::layout::layout_of_uncached::{closure#13}::{closure#0}> as core::iter::traits::iterator::Iterator>::try_collect<rustc_index::vec::IndexVec<rustc_abi::layout::ty::FieldIdx, rustc_abi::layout::ty::TyAndLayout<rustc_middle::ty::Ty>>>::{closure#0}, rustc_index::vec::IndexVec<rustc_abi::layout::ty::FieldIdx, rustc_abi::layout::ty::TyAndLayout<rustc_middle::ty::Ty>>>
  11: core::iter::adapters::try_process::<core::iter::adapters::by_ref_sized::ByRefSized<core::iter::adapters::map::Map<core::slice::iter::Iter<rustc_middle::ty::VariantDef>, rustc_ty_utils::layout::layout_of_uncached::{closure#13}>>, rustc_index::vec::IndexVec<rustc_abi::layout::ty::FieldIdx, rustc_abi::layout::ty::TyAndLayout<rustc_middle::ty::Ty>>, core::result::Result<core::convert::Infallible, &rustc_middle::ty::layout::LayoutError>, <core::iter::adapters::map::Map<core::slice::iter::Iter<rustc_middle::ty::VariantDef>, rustc_ty_utils::layout::layout_of_uncached::{closure#13}> as core::iter::traits::iterator::Iterator>::try_collect<rustc_index::vec::IndexVec<rustc_abi::layout::ty::VariantIdx, rustc_index::vec::IndexVec<rustc_abi::layout::ty::FieldIdx, rustc_abi::layout::ty::TyAndLayout<rustc_middle::ty::Ty>>>>::{closure#0}, rustc_index::vec::IndexVec<rustc_abi::layout::ty::VariantIdx, rustc_index::vec::IndexVec<rustc_abi::layout::ty::FieldIdx, rustc_abi::layout::ty::TyAndLayout<rustc_middle::ty::Ty>>>>
  12: rustc_ty_utils::layout::layout_of_uncached
  13: rustc_ty_utils::layout::layout_of
      [... omitted 2 frames ...]
  14: rustc_middle::query::plumbing::query_get_at::<rustc_query_system::query::caches::DefaultCache<rustc_middle::ty::ParamEnvAnd<rustc_middle::ty::Ty>, rustc_middle::query::erase::Erased<[u8; 16]>>>
  15: <rustc_smir::rustc_smir::context::TablesWrapper as stable_mir::compiler_interface::Context>::ty_layout
  16: <stable_mir::ty::Ty>::layout
  17: smir_pretty::printer::collect_ty
             at ./src/printer.rs:468:65
  18: smir_pretty::printer::collect_vec_tys::{{closure}}
             at ./src/printer.rs:449:35
  19: core::iter::traits::iterator::Iterator::for_each::call::{{closure}}
             at ./deps/rust/src/library/core/src/iter/traits/iterator.rs:797:29
  20: <alloc::vec::into_iter::IntoIter<T,A> as core::iter::traits::iterator::Iterator>::fold
             at ./deps/rust/src/library/alloc/src/vec/into_iter.rs:318:25
  21: core::iter::traits::iterator::Iterator::for_each
             at ./deps/rust/src/library/core/src/iter/traits/iterator.rs:800:9
  22: smir_pretty::printer::collect_vec_tys
             at ./src/printer.rs:449:5
  23: smir_pretty::printer::collect_ty
             at ./src/printer.rs:485:17
  24: <smir_pretty::printer::InternedValueCollector as stable_mir::mir::visit::MirVisitor>::visit_ty
             at ./src/printer.rs:550:6
  25: stable_mir::mir::visit::MirVisitor::super_mir_const
             at ./deps/rust/src/compiler/stable_mir/src/mir/visit.rs:381:9
  26: <smir_pretty::printer::InternedValueCollector as stable_mir::mir::visit::MirVisitor>::visit_mir_const
             at ./src/printer.rs:546:5
  27: stable_mir::mir::visit::MirVisitor::super_const_operand
             at ./deps/rust/src/compiler/stable_mir/src/mir/visit.rs:376:9
  28: stable_mir::mir::visit::MirVisitor::visit_const_operand
             at ./deps/rust/src/compiler/stable_mir/src/mir/visit.rs:112:9
  29: stable_mir::mir::visit::MirVisitor::super_operand
             at ./deps/rust/src/compiler/stable_mir/src/mir/visit.rs:359:17
  30: stable_mir::mir::visit::MirVisitor::visit_operand
             at ./deps/rust/src/compiler/stable_mir/src/mir/visit.rs:99:9
  31: stable_mir::mir::visit::MirVisitor::super_terminator
             at ./deps/rust/src/compiler/stable_mir/src/mir/visit.rs:247:17
  32: <smir_pretty::printer::InternedValueCollector as stable_mir::mir::visit::MirVisitor>::visit_terminator
             at ./src/printer.rs:516:5
  33: stable_mir::mir::visit::MirVisitor::super_basic_block
             at ./deps/rust/src/compiler/stable_mir/src/mir/visit.rs:172:9
  34: stable_mir::mir::visit::MirVisitor::visit_basic_block
             at ./deps/rust/src/compiler/stable_mir/src/mir/visit.rs:48:9
  35: stable_mir::mir::visit::MirVisitor::super_body
             at ./deps/rust/src/compiler/stable_mir/src/mir/visit.rs:146:13
  36: stable_mir::mir::visit::MirVisitor::visit_body
             at ./deps/rust/src/compiler/stable_mir/src/mir/visit.rs:44:9
  37: smir_pretty::printer::collect_interned_values
             at ./src/printer.rs:569:12
  38: smir_pretty::printer::emit_smir_internal
             at ./src/printer.rs:693:50
  39: smir_pretty::printer::emit_smir
             at ./src/printer.rs:738:9
  40: <smir_pretty::driver::StableMirCallbacks as rustc_driver_impl::Callbacks>::after_analysis::{{closure}}::{{closure}}
             at ./src/driver.rs:46:53
  41: rustc_smir::rustc_internal::init::{{closure}}
             at ./deps/rust/src/compiler/rustc_smir/src/rustc_internal/mod.rs:192:33
  42: scoped_tls::ScopedKey<T>::set
             at /home/jost/.cargo/registry/src/index.crates.io-6f17d22bba15001f/scoped-tls-1.0.1/src/lib.rs:137:9
  43: rustc_smir::rustc_internal::init
             at ./deps/rust/src/compiler/rustc_smir/src/rustc_internal/mod.rs:192:5
  44: rustc_smir::rustc_internal::run::{{closure}}
             at ./deps/rust/src/compiler/rustc_smir/src/rustc_internal/mod.rs:223:53
  45: stable_mir::compiler_interface::run::{{closure}}
             at ./deps/rust/src/compiler/stable_mir/src/compiler_interface.rs:265:40
  46: scoped_tls::ScopedKey<T>::set
             at /home/jost/.cargo/registry/src/index.crates.io-6f17d22bba15001f/scoped-tls-1.0.1/src/lib.rs:137:9
  47: stable_mir::compiler_interface::run
             at ./deps/rust/src/compiler/stable_mir/src/compiler_interface.rs:265:9
  48: rustc_smir::rustc_internal::run
             at ./deps/rust/src/compiler/rustc_smir/src/rustc_internal/mod.rs:223:5
  49: <smir_pretty::driver::StableMirCallbacks as rustc_driver_impl::Callbacks>::after_analysis::{{closure}}
             at ./src/driver.rs:46:25
  50: rustc_middle::ty::context::GlobalCtxt::enter::{{closure}}
             at ./deps/rust/src/compiler/rustc_middle/src/ty/context.rs:1365:37
  51: rustc_middle::ty::context::tls::enter_context::{{closure}}
             at ./deps/rust/src/compiler/rustc_middle/src/ty/context/tls.rs:82:9
  52: std::thread::local::LocalKey<T>::try_with
             at ./deps/rust/src/library/std/src/thread/local.rs:283:12
  53: std::thread::local::LocalKey<T>::with
             at ./deps/rust/src/library/std/src/thread/local.rs:260:9
  54: rustc_middle::ty::context::tls::enter_context
             at ./deps/rust/src/compiler/rustc_middle/src/ty/context/tls.rs:79:9
  55: rustc_middle::ty::context::GlobalCtxt::enter
             at ./deps/rust/src/compiler/rustc_middle/src/ty/context.rs:1365:9
  56: <smir_pretty::driver::StableMirCallbacks as rustc_driver_impl::Callbacks>::after_analysis
             at ./src/driver.rs:41:18
  57: <rustc_interface::interface::Compiler>::enter::<rustc_driver_impl::run_compiler::{closure#0}::{closure#1}, core::result::Result<core::option::Option<rustc_interface::queries::Linker>, rustc_span::ErrorGuaranteed>>
  58: rustc_span::create_session_globals_then::<core::result::Result<(), rustc_span::ErrorGuaranteed>, rustc_interface::util::run_in_thread_with_globals<rustc_interface::util::run_in_thread_pool_with_globals<rustc_interface::interface::run_compiler<core::result::Result<(), rustc_span::ErrorGuaranteed>, rustc_driver_impl::run_compiler::{closure#0}>::{closure#1}, core::result::Result<(), rustc_span::ErrorGuaranteed>>::{closure#0}, core::result::Result<(), rustc_span::ErrorGuaranteed>>::{closure#0}::{closure#0}::{closure#0}>
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

This happens with two different programs from the integration tests in `mir-semantics`:

https://github.com/runtimeverification/mir-semantics/blob/master/kmir/src/tests/integration/data/run-rs/traits/defined-trait.rs

https://github.com/runtimeverification/mir-semantics/blob/master/kmir/src/tests/integration/data/run-rs/strings-chars/std-to-string.rs

The call to to_string() for a literal might be the problem since it occurs in both.

[sskeirik]

Things are pretty fragile the moment. Sorry for that. For context, there were several competing forces that contributed to the current state of affairs:

1. a push to try and get an MVP working: "we'll nail things down and write proper tests afterwards"
2. a lot of moving parts (including parts of the rust compiler that we found as we went along)
3. the size of emitted JSON is pretty big, even on tiny examples, so it's hard to manually check things when updates are made

Regarding the JSON output format breaking, it should be possible to the massage the output to what we had before --- I am not sure I will have time for that though.

The second issue about the compiler error --- the bug is likely in our code --- many of these compiler queries (in this case, the misbehaving query is layout() on line 468) have invariants which are only checked at runtime. I thought it would be the case that after type-checking, borrow-checking, and monomorphization, nothing could go wrong with these queries --- but it may be that some additional setup is required to call these functions safely. EDIT: for now, the offending call can be removed.

I hope this is helpful.

[dkcumming]

This is helpful @sskeirik. @jberthold I will look into it when I can with you and we will figure out what we need to get mir-semantics accepting the current state, and document what needs to be improved of course