creusot
creusot copied to clipboard
Add support for upcasting of integer types
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
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!(),
}
}
....
that'll be a trivial fix