creusot icon indicating copy to clipboard operation
creusot copied to clipboard

Add support for upcasting of integer types

Open sarsko opened this issue 1 year ago • 2 comments

Upcasting an integer causes a "violent" panic.

For instance:

fn test(inp: u8) {
    let bing = inp as usize;
}

results in the following backtrace:

thread 'rustc' panicked at 'not implemented', creusot/src/translation/function/statement.rs:293:23
stack backtrace:
   0:     0x7f1b7469e02d - std::backtrace_rs::backtrace::libunwind::trace::h7a926b2032699775
                               at /rustc/5750a6aa2777382bf421b726f234da23f990a953/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5
   1:     0x7f1b7469e02d - std::backtrace_rs::backtrace::trace_unsynchronized::h2d3d408762c23e47
                               at /rustc/5750a6aa2777382bf421b726f234da23f990a953/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x7f1b7469e02d - std::sys_common::backtrace::_print_fmt::h24dd014972ee0b6e
                               at /rustc/5750a6aa2777382bf421b726f234da23f990a953/library/std/src/sys_common/backtrace.rs:66:5
   3:     0x7f1b7469e02d - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h566854fd172f06bc
                               at /rustc/5750a6aa2777382bf421b726f234da23f990a953/library/std/src/sys_common/backtrace.rs:45:22
   4:     0x7f1b746f9dec - core::fmt::write::h56c1eb76bd5c87c8
                               at /rustc/5750a6aa2777382bf421b726f234da23f990a953/library/core/src/fmt/mod.rs:1196:17
   5:     0x7f1b7468f741 - std::io::Write::write_fmt::hc13fd41e7e0921d4
                               at /rustc/5750a6aa2777382bf421b726f234da23f990a953/library/std/src/io/mod.rs:1672:15
   6:     0x7f1b746a0cf5 - std::sys_common::backtrace::_print::hc7d36740cfaf072f
                               at /rustc/5750a6aa2777382bf421b726f234da23f990a953/library/std/src/sys_common/backtrace.rs:48:5
   7:     0x7f1b746a0cf5 - std::sys_common::backtrace::print::h33a30c8305581751
                               at /rustc/5750a6aa2777382bf421b726f234da23f990a953/library/std/src/sys_common/backtrace.rs:35:9
   8:     0x7f1b746a0cf5 - std::panicking::default_hook::{{closure}}::hb07a10016924ba07
                               at /rustc/5750a6aa2777382bf421b726f234da23f990a953/library/std/src/panicking.rs:295:22
   9:     0x7f1b746a0a16 - std::panicking::default_hook::h4dbb3420eca4773d
                               at /rustc/5750a6aa2777382bf421b726f234da23f990a953/library/std/src/panicking.rs:314:9
  10:     0x560dd8b5f5a4 - creusot_rustc::report_panic::hd26bd7e1b5cf5c67
  11:     0x7f1b5f2db7e3 - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::h62717ff274ce2f1a
                               at /rustc/5750a6aa2777382bf421b726f234da23f990a953/library/alloc/src/boxed.rs:1965:9
  12:     0x7f1b5f2597ad - proc_macro::bridge::client::<impl proc_macro::bridge::Bridge>::enter::{{closure}}::{{closure}}::heb1e553301785037
                               at /rustc/5750a6aa2777382bf421b726f234da23f990a953/library/proc_macro/src/bridge/client.rs:328:21
  13:     0x7f1b746a13ca - std::panicking::rust_panic_with_hook::h11d9659c53a62795
                               at /rustc/5750a6aa2777382bf421b726f234da23f990a953/library/std/src/panicking.rs:702:17
  14:     0x7f1b746a11c9 - std::panicking::begin_panic_handler::{{closure}}::hc90f9b2ac4aba546
                               at /rustc/5750a6aa2777382bf421b726f234da23f990a953/library/std/src/panicking.rs:586:13
  15:     0x7f1b7469e4e4 - std::sys_common::backtrace::__rust_end_short_backtrace::h1fb1308c3e524aae
                               at /rustc/5750a6aa2777382bf421b726f234da23f990a953/library/std/src/sys_common/backtrace.rs:138:18
  16:     0x7f1b746a0f39 - rust_begin_unwind
                               at /rustc/5750a6aa2777382bf421b726f234da23f990a953/library/std/src/panicking.rs:584:5
  17:     0x7f1b74666103 - core::panicking::panic_fmt::h1eab4c4b36474163
                               at /rustc/5750a6aa2777382bf421b726f234da23f990a953/library/core/src/panicking.rs:142:14
  18:     0x7f1b74665fcd - core::panicking::panic::hf14553acd83284c1
                               at /rustc/5750a6aa2777382bf421b726f234da23f990a953/library/core/src/panicking.rs:48:5
  19:     0x560dd8d39222 - creusot::translation::function::statement::uint_to_int::h08e5d135c1588144
  20:     0x560dd8cff950 - creusot::translation::function::BodyTranslator::translate_body::hd6318372f3b4d362
  21:     0x560dd8cfab61 - creusot::translation::function::translate_function::h2d7fc273e123af74
  22:     0x560dd8c92c8b - creusot::ctx::TranslationCtx::translate_function::h9188b80757b81a92
  23:     0x560dd8c918c4 - creusot::ctx::TranslationCtx::translate::h11e8daaf38f136e6
  24:     0x560dd8d3c119 - creusot::translation::after_analysis::h7d483e27310e5bc4
  25:     0x560dd8d08067 - rustc_interface::passes::QueryContext::enter::haad0e490ae1935ba
  26:     0x560dd8c1a912 - <creusot::callbacks::ToWhy as rustc_driver::Callbacks>::after_expansion::h0c9fe6d0360f7980
  27:     0x7f1b770a6f65 - <rustc_interface[341dd5f2483eca50]::interface::Compiler>::enter::<rustc_driver[a8f804d3c049a324]::run_compiler::{closure#1}::{closure#2}, core[1c0d46d4499c473b]::result::Result<core[1c0d46d4499c473b]::option::Option<rustc_interface[341dd5f2483eca50]::queries::Linker>, rustc_errors[c8f8689a602b606d]::ErrorGuaranteed>>
  28:     0x7f1b770cb4cf - rustc_span[220bbbfb33dac20d]::with_source_map::<core[1c0d46d4499c473b]::result::Result<(), rustc_errors[c8f8689a602b606d]::ErrorGuaranteed>, rustc_interface[341dd5f2483eca50]::interface::create_compiler_and_run<core[1c0d46d4499c473b]::result::Result<(), rustc_errors[c8f8689a602b606d]::ErrorGuaranteed>, rustc_driver[a8f804d3c049a324]::run_compiler::{closure#1}>::{closure#1}>
  29:     0x7f1b770a7ed2 - <scoped_tls[641400cc490278fe]::ScopedKey<rustc_span[220bbbfb33dac20d]::SessionGlobals>>::set::<rustc_interface[341dd5f2483eca50]::interface::run_compiler<core[1c0d46d4499c473b]::result::Result<(), rustc_errors[c8f8689a602b606d]::ErrorGuaranteed>, rustc_driver[a8f804d3c049a324]::run_compiler::{closure#1}>::{closure#0}, core[1c0d46d4499c473b]::result::Result<(), rustc_errors[c8f8689a602b606d]::ErrorGuaranteed>>
  30:     0x7f1b770bd48f - std[b2b29a4a916e13c6]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[341dd5f2483eca50]::util::run_in_thread_pool_with_globals<rustc_interface[341dd5f2483eca50]::interface::run_compiler<core[1c0d46d4499c473b]::result::Result<(), rustc_errors[c8f8689a602b606d]::ErrorGuaranteed>, rustc_driver[a8f804d3c049a324]::run_compiler::{closure#1}>::{closure#0}, core[1c0d46d4499c473b]::result::Result<(), rustc_errors[c8f8689a602b606d]::ErrorGuaranteed>>::{closure#0}, core[1c0d46d4499c473b]::result::Result<(), rustc_errors[c8f8689a602b606d]::ErrorGuaranteed>>
  31:     0x7f1b770bd5c9 - <<std[b2b29a4a916e13c6]::thread::Builder>::spawn_unchecked_<rustc_interface[341dd5f2483eca50]::util::run_in_thread_pool_with_globals<rustc_interface[341dd5f2483eca50]::interface::run_compiler<core[1c0d46d4499c473b]::result::Result<(), rustc_errors[c8f8689a602b606d]::ErrorGuaranteed>, rustc_driver[a8f804d3c049a324]::run_compiler::{closure#1}>::{closure#0}, core[1c0d46d4499c473b]::result::Result<(), rustc_errors[c8f8689a602b606d]::ErrorGuaranteed>>::{closure#0}, core[1c0d46d4499c473b]::result::Result<(), rustc_errors[c8f8689a602b606d]::ErrorGuaranteed>>::{closure#1} as core[1c0d46d4499c473b]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  32:     0x7f1b746ab303 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::he7c258be890a1644
                               at /rustc/5750a6aa2777382bf421b726f234da23f990a953/library/alloc/src/boxed.rs:1951:9
  33:     0x7f1b746ab303 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h20b4ca040d24e40b
                               at /rustc/5750a6aa2777382bf421b726f234da23f990a953/library/alloc/src/boxed.rs:1951:9
  34:     0x7f1b746ab303 - std::sys::unix::thread::Thread::new::thread_start::ha415642a774b6db6
                               at /rustc/5750a6aa2777382bf421b726f234da23f990a953/library/std/src/sys/unix/thread.rs:108:17
  35:     0x7f1b7448054d - <unknown>
  36:     0x7f1b74505874 - clone
  37:                0x0 - <unknown>

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:
end of query stack

sarsko avatar Aug 01 '22 23:08 sarsko

pub fn uint_to_int(uty: &UintTy) -> Exp {
    match uty {
        UintTy::Usize => Exp::impure_qvar(QName::from_string("UIntSize.to_int").unwrap()),
        UintTy::U8 => unimplemented!(),
        UintTy::U16 => unimplemented!(),
        UintTy::U32 => Exp::impure_qvar(QName::from_string("UInt32.to_int").unwrap()),
        UintTy::U64 => Exp::impure_qvar(QName::from_string("UInt64.to_int").unwrap()),
        UintTy::U128 => unimplemented!(),
    }
}

....

xldenis avatar Aug 02 '22 20:08 xldenis

that'll be a trivial fix

xldenis avatar Aug 02 '22 20:08 xldenis