Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Panic due to typecheck failure on percent-encoding crate #675

Closed
zhassan-aws opened this issue Dec 2, 2021 · 3 comments
Closed

Panic due to typecheck failure on percent-encoding crate #675

zhassan-aws opened this issue Dec 2, 2021 · 3 comments
Assignees
@celinval
Labels
[C] Bug This is a bug. Something isn't working.

Comments

@zhassan-aws
Copy link
Contributor

Steps to reproduce:

  1. cargo new foo
  2. cd foo
  3. Add percent-encoding to the Cargo.toml dependencies:
[dependencies]
percent-encoding = "2.1.0"
  1. Run:
RUST_BACKTRACE=1 RUSTFLAGS=$(rmc-rustc --rmc-flags) RUSTC=$(rmc-rustc --rmc-path) cargo build --target x86_64-unknown-linux-gnu -j1

with RMC version: 7d0d4cfc6da

I expected to see this happen: Verification Successful

Instead, this happened:

thread 'rustc' panicked at 'BinaryOperation Expression does not typecheck Equal Expr { value: Symbol { identifier: "_ZN16percent_encoding17decode_utf8_lossy17h0e9f786e584e1458E::1::var_21" }, typ: StructTag("tag-_9002246437548051943"), location: None } Expr { value: Symbol { identifier: "_ZN16percent_encoding17decode_utf8_lossy17h0e9f786e584e1458E::1::var_22" }, typ: StructTag("tag-_9002246437548051943"), location: None }', compiler/cbmc/src/goto_program/expr.rs:905:9
stack backtrace:
   0: rust_begin_unwind
             at /home/ubuntu/tools/rmc/library/std/src/panicking.rs:498:5
   1: core::panicking::panic_fmt
             at /home/ubuntu/tools/rmc/library/core/src/panicking.rs:107:14
   2: <cbmc::goto_program::expr::Expr>::binop
             at /home/ubuntu/tools/rmc/compiler/cbmc/src/goto_program/expr.rs:905:9
   3: <cbmc::goto_program::expr::Expr>::eq
             at /home/ubuntu/tools/rmc/compiler/cbmc/src/goto_program/expr.rs:1027:9
   4: <rustc_codegen_rmc::context::goto_ctx::GotocCtx>::codegen_comparison
             at /home/ubuntu/tools/rmc/compiler/rustc_codegen_rmc/src/codegen/rvalue.rs:26:21
   5: <rustc_codegen_rmc::context::goto_ctx::GotocCtx>::codegen_rvalue_binary_op
             at /home/ubuntu/tools/rmc/compiler/rustc_codegen_rmc/src/codegen/rvalue.rs:312:17
   6: <rustc_codegen_rmc::context::goto_ctx::GotocCtx>::codegen_rvalue
             at /home/ubuntu/tools/rmc/compiler/rustc_codegen_rmc/src/codegen/rvalue.rs:380:59
   7: <rustc_codegen_rmc::context::goto_ctx::GotocCtx>::codegen_statement
             at /home/ubuntu/tools/rmc/compiler/rustc_codegen_rmc/src/codegen/statement.rs:555:33
   8: <rustc_codegen_rmc::context::goto_ctx::GotocCtx>::codegen_block
             at /home/ubuntu/tools/rmc/compiler/rustc_codegen_rmc/src/codegen/block.rs:27:32
   9: <rustc_codegen_rmc::context::goto_ctx::GotocCtx>::codegen_function::{closure#1}
             at /home/ubuntu/tools/rmc/compiler/rustc_codegen_rmc/src/codegen/function.rs:95:71
  10: core::iter::traits::iterator::Iterator::for_each::call::<(rustc_middle::mir::BasicBlock, &rustc_middle::mir::BasicBlockData), <rustc_codegen_rmc::context::goto_ctx::GotocCtx>::codegen_function::{closure#1}>::{closure#0}
             at /home/ubuntu/tools/rmc/library/core/src/iter/traits/iterator.rs:733:29
  11: core::iter::adapters::map::map_fold::<(usize, &rustc_middle::mir::BasicBlockData), (rustc_middle::mir::BasicBlock, &rustc_middle::mir::BasicBlockData), (), <rustc_index::vec::IndexVec<rustc_middle::mir::BasicBlock, rustc_middle::mir::BasicBlockData>>::iter_enumerated::{closure#0}, core::iter::traits::iterator::Iterator::for_each::call<(rustc_middle::mir::BasicBlock, &rustc_middle::mir::BasicBlockData), <rustc_codegen_rmc::context::goto_ctx::GotocCtx>::codegen_function::{closure#1}>::{closure#0}>::{closure#0}
             at /home/ubuntu/tools/rmc/library/core/src/iter/adapters/map.rs:84:21
  12: <core::iter::adapters::enumerate::Enumerate<_> as core::iter::traits::iterator::Iterator>::fold::enumerate::<&rustc_middle::mir::BasicBlockData, (), core::iter::adapters::map::map_fold<(usize, &rustc_middle::mir::BasicBlockData), (rustc_middle::mir::BasicBlock, &rustc_middle::mir::BasicBlockData), (), <rustc_index::vec::IndexVec<rustc_middle::mir::BasicBlock, rustc_middle::mir::BasicBlockData>>::iter_enumerated::{closure#0}, core::iter::traits::iterator::Iterator::for_each::call<(rustc_middle::mir::BasicBlock, &rustc_middle::mir::BasicBlockData), <rustc_codegen_rmc::context::goto_ctx::GotocCtx>::codegen_function::{closure#1}>::{closure#0}>::{closure#0}>::{closure#0}
             at /home/ubuntu/tools/rmc/library/core/src/iter/adapters/enumerate.rs:106:27
  13: <core::slice::iter::Iter<rustc_middle::mir::BasicBlockData> as core::iter::traits::iterator::Iterator>::fold::<(), <core::iter::adapters::enumerate::Enumerate<_> as core::iter::traits::iterator::Iterator>::fold::enumerate<&rustc_middle::mir::BasicBlockData, (), core::iter::adapters::map::map_fold<(usize, &rustc_middle::mir::BasicBlockData), (rustc_middle::mir::BasicBlock, &rustc_middle::mir::BasicBlockData), (), <rustc_index::vec::IndexVec<rustc_middle::mir::BasicBlock, rustc_middle::mir::BasicBlockData>>::iter_enumerated::{closure#0}, core::iter::traits::iterator::Iterator::for_each::call<(rustc_middle::mir::BasicBlock, &rustc_middle::mir::BasicBlockData), <rustc_codegen_rmc::context::goto_ctx::GotocCtx>::codegen_function::{closure#1}>::{closure#0}>::{closure#0}>::{closure#0}>
             at /home/ubuntu/tools/rmc/library/core/src/iter/traits/iterator.rs:2171:21
  14: <core::iter::adapters::enumerate::Enumerate<core::slice::iter::Iter<rustc_middle::mir::BasicBlockData>> as core::iter::traits::iterator::Iterator>::fold::<(), core::iter::adapters::map::map_fold<(usize, &rustc_middle::mir::BasicBlockData), (rustc_middle::mir::BasicBlock, &rustc_middle::mir::BasicBlockData), (), <rustc_index::vec::IndexVec<rustc_middle::mir::BasicBlock, rustc_middle::mir::BasicBlockData>>::iter_enumerated::{closure#0}, core::iter::traits::iterator::Iterator::for_each::call<(rustc_middle::mir::BasicBlock, &rustc_middle::mir::BasicBlockData), <rustc_codegen_rmc::context::goto_ctx::GotocCtx>::codegen_function::{closure#1}>::{closure#0}>::{closure#0}>
             at /home/ubuntu/tools/rmc/library/core/src/iter/adapters/enumerate.rs:112:9
  15: <core::iter::adapters::map::Map<core::iter::adapters::enumerate::Enumerate<core::slice::iter::Iter<rustc_middle::mir::BasicBlockData>>, <rustc_index::vec::IndexVec<rustc_middle::mir::BasicBlock, rustc_middle::mir::BasicBlockData>>::iter_enumerated::{closure#0}> as core::iter::traits::iterator::Iterator>::fold::<(), core::iter::traits::iterator::Iterator::for_each::call<(rustc_middle::mir::BasicBlock, &rustc_middle::mir::BasicBlockData), <rustc_codegen_rmc::context::goto_ctx::GotocCtx>::codegen_function::{closure#1}>::{closure#0}>
             at /home/ubuntu/tools/rmc/library/core/src/iter/adapters/map.rs:124:9
  16: <core::iter::adapters::map::Map<core::iter::adapters::enumerate::Enumerate<core::slice::iter::Iter<rustc_middle::mir::BasicBlockData>>, <rustc_index::vec::IndexVec<rustc_middle::mir::BasicBlock, rustc_middle::mir::BasicBlockData>>::iter_enumerated::{closure#0}> as core::iter::traits::iterator::Iterator>::for_each::<<rustc_codegen_rmc::context::goto_ctx::GotocCtx>::codegen_function::{closure#1}>
             at /home/ubuntu/tools/rmc/library/core/src/iter/traits/iterator.rs:736:9
  17: <rustc_codegen_rmc::context::goto_ctx::GotocCtx>::codegen_function
             at /home/ubuntu/tools/rmc/compiler/rustc_codegen_rmc/src/codegen/function.rs:95:13
  18: <rustc_codegen_rmc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::{closure#2}
             at /home/ubuntu/tools/rmc/compiler/rustc_codegen_rmc/src/compiler_interface.rs:109:35
  19: <rustc_codegen_rmc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::<<rustc_codegen_rmc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::{closure#2}>::{closure#0}
             at /home/ubuntu/tools/rmc/compiler/rustc_codegen_rmc/src/utils/debug.rs:87:13
  20: <std::thread::local::LocalKey<core::cell::RefCell<(core::option::Option<alloc::string::String>, core::option::Option<cbmc::goto_program::location::Location>)>>>::try_with::<<rustc_codegen_rmc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info<<rustc_codegen_rmc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::{closure#2}>::{closure#0}, ()>
             at /home/ubuntu/tools/rmc/library/std/src/thread/local.rs:399:16
  21: <std::thread::local::LocalKey<core::cell::RefCell<(core::option::Option<alloc::string::String>, core::option::Option<cbmc::goto_program::location::Location>)>>>::with::<<rustc_codegen_rmc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info<<rustc_codegen_rmc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::{closure#2}>::{closure#0}, ()>
             at /home/ubuntu/tools/rmc/library/std/src/thread/local.rs:375:9
  22: <rustc_codegen_rmc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::<<rustc_codegen_rmc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::{closure#2}>
             at /home/ubuntu/tools/rmc/compiler/rustc_codegen_rmc/src/utils/debug.rs:84:9
  23: <rustc_codegen_rmc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate
             at /home/ubuntu/tools/rmc/compiler/rustc_codegen_rmc/src/compiler_interface.rs:108:25
  24: rustc_interface::passes::start_codegen::{closure#0}
             at /home/ubuntu/tools/rmc/compiler/rustc_interface/src/passes.rs:1077:9
  25: <rustc_data_structures::profiling::VerboseTimingGuard>::run::<alloc::boxed::Box<dyn core::any::Any>, rustc_interface::passes::start_codegen::{closure#0}>
             at /home/ubuntu/tools/rmc/compiler/rustc_data_structures/src/profiling.rs:644:9
  26: <rustc_session::session::Session>::time::<alloc::boxed::Box<dyn core::any::Any>, rustc_interface::passes::start_codegen::{closure#0}>
             at /home/ubuntu/tools/rmc/compiler/rustc_session/src/utils.rs:16:9
  27: rustc_interface::passes::start_codegen
             at /home/ubuntu/tools/rmc/compiler/rustc_interface/src/passes.rs:1076:19
  28: <rustc_interface::queries::Queries>::ongoing_codegen::{closure#0}::{closure#0}
             at /home/ubuntu/tools/rmc/compiler/rustc_interface/src/queries.rs:254:20
  29: <rustc_interface::passes::QueryContext>::enter::<<rustc_interface::queries::Queries>::ongoing_codegen::{closure#0}::{closure#0}, core::result::Result<alloc::boxed::Box<dyn core::any::Any>, rustc_errors::ErrorReported>>::{closure#0}
             at /home/ubuntu/tools/rmc/compiler/rustc_interface/src/passes.rs:805:42
  30: rustc_middle::ty::context::tls::enter_context::<<rustc_interface::passes::QueryContext>::enter<<rustc_interface::queries::Queries>::ongoing_codegen::{closure#0}::{closure#0}, core::result::Result<alloc::boxed::Box<dyn core::any::Any>, rustc_errors::ErrorReported>>::{closure#0}, core::result::Result<alloc::boxed::Box<dyn core::any::Any>, rustc_errors::ErrorReported>>::{closure#0}
             at /home/ubuntu/tools/rmc/compiler/rustc_middle/src/ty/context.rs:1778:50
  31: rustc_middle::ty::context::tls::set_tlv::<rustc_middle::ty::context::tls::enter_context<<rustc_interface::passes::QueryContext>::enter<<rustc_interface::queries::Queries>::ongoing_codegen::{closure#0}::{closure#0}, core::result::Result<alloc::boxed::Box<dyn core::any::Any>, rustc_errors::ErrorReported>>::{closure#0}, core::result::Result<alloc::boxed::Box<dyn core::any::Any>, rustc_errors::ErrorReported>>::{closure#0}, core::result::Result<alloc::boxed::Box<dyn core::any::Any>, rustc_errors::ErrorReported>>
             at /home/ubuntu/tools/rmc/compiler/rustc_middle/src/ty/context.rs:1762:9
  32: rustc_middle::ty::context::tls::enter_context::<<rustc_interface::passes::QueryContext>::enter<<rustc_interface::queries::Queries>::ongoing_codegen::{closure#0}::{closure#0}, core::result::Result<alloc::boxed::Box<dyn core::any::Any>, rustc_errors::ErrorReported>>::{closure#0}, core::result::Result<alloc::boxed::Box<dyn core::any::Any>, rustc_errors::ErrorReported>>
             at /home/ubuntu/tools/rmc/compiler/rustc_middle/src/ty/context.rs:1778:9
  33: <rustc_interface::passes::QueryContext>::enter::<<rustc_interface::queries::Queries>::ongoing_codegen::{closure#0}::{closure#0}, core::result::Result<alloc::boxed::Box<dyn core::any::Any>, rustc_errors::ErrorReported>>
             at /home/ubuntu/tools/rmc/compiler/rustc_interface/src/passes.rs:805:9
  34: <rustc_interface::queries::Queries>::ongoing_codegen::{closure#0}
             at /home/ubuntu/tools/rmc/compiler/rustc_interface/src/queries.rs:245:13
  35: <rustc_interface::queries::Query<alloc::boxed::Box<dyn core::any::Any>>>::compute::<<rustc_interface::queries::Queries>::ongoing_codegen::{closure#0}>
             at /home/ubuntu/tools/rmc/compiler/rustc_interface/src/queries.rs:38:28
  36: rustc_driver::run_compiler::{closure#1}::{closure#2}
             at /home/ubuntu/tools/rmc/compiler/rustc_driver/src/lib.rs:409:13
  37: <rustc_interface::interface::Compiler>::enter::<rustc_driver::run_compiler::{closure#1}::{closure#2}, core::result::Result<core::option::Option<rustc_interface::queries::Linker>, rustc_errors::ErrorReported>>
             at /home/ubuntu/tools/rmc/compiler/rustc_interface/src/queries.rs:394:19
  38: rustc_driver::run_compiler::{closure#1}
             at /home/ubuntu/tools/rmc/compiler/rustc_driver/src/lib.rs:314:22
  39: rustc_interface::interface::create_compiler_and_run::<core::result::Result<(), rustc_errors::ErrorReported>, rustc_driver::run_compiler::{closure#1}>::{closure#1}
             at /home/ubuntu/tools/rmc/compiler/rustc_interface/src/interface.rs:220:13
  40: rustc_span::with_source_map::<core::result::Result<(), rustc_errors::ErrorReported>, rustc_interface::interface::create_compiler_and_run<core::result::Result<(), rustc_errors::ErrorReported>, rustc_driver::run_compiler::{closure#1}>::{closure#1}>
             at /home/ubuntu/tools/rmc/compiler/rustc_span/src/lib.rs:971:5
  41: rustc_interface::interface::create_compiler_and_run::<core::result::Result<(), rustc_errors::ErrorReported>, rustc_driver::run_compiler::{closure#1}>
             at /home/ubuntu/tools/rmc/compiler/rustc_interface/src/interface.rs:214:5
  42: rustc_interface::interface::run_compiler::<core::result::Result<(), rustc_errors::ErrorReported>, rustc_driver::run_compiler::{closure#1}>::{closure#0}
             at /home/ubuntu/tools/rmc/compiler/rustc_interface/src/interface.rs:236:12
  43: rustc_interface::util::setup_callbacks_and_run_in_thread_pool_with_globals::<rustc_interface::interface::run_compiler<core::result::Result<(), rustc_errors::ErrorReported>, rustc_driver::run_compiler::{closure#1}>::{closure#0}, core::result::Result<(), rustc_errors::ErrorReported>>::{closure#0}::{closure#0}
             at /home/ubuntu/tools/rmc/compiler/rustc_interface/src/util.rs:145:13
  44: <scoped_tls::ScopedKey<rustc_span::SessionGlobals>>::set::<rustc_interface::util::setup_callbacks_and_run_in_thread_pool_with_globals<rustc_interface::interface::run_compiler<core::result::Result<(), rustc_errors::ErrorReported>, rustc_driver::run_compiler::{closure#1}>::{closure#0}, core::result::Result<(), rustc_errors::ErrorReported>>::{closure#0}::{closure#0}, core::result::Result<(), rustc_errors::ErrorReported>>
             at /home/ubuntu/.cargo/registry/src/github.com-1ecc6299db9ec823/scoped-tls-1.0.0/src/lib.rs:137:9
  45: rustc_span::create_session_globals_then::<core::result::Result<(), rustc_errors::ErrorReported>, rustc_interface::util::setup_callbacks_and_run_in_thread_pool_with_globals<rustc_interface::interface::run_compiler<core::result::Result<(), rustc_errors::ErrorReported>, rustc_driver::run_compiler::{closure#1}>::{closure#0}, core::result::Result<(), rustc_errors::ErrorReported>>::{closure#0}::{closure#0}>
             at /home/ubuntu/tools/rmc/compiler/rustc_span/src/lib.rs:109:5
  46: rustc_interface::util::setup_callbacks_and_run_in_thread_pool_with_globals::<rustc_interface::interface::run_compiler<core::result::Result<(), rustc_errors::ErrorReported>, rustc_driver::run_compiler::{closure#1}>::{closure#0}, core::result::Result<(), rustc_errors::ErrorReported>>::{closure#0}
             at /home/ubuntu/tools/rmc/compiler/rustc_interface/src/util.rs:143:9
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

error: internal compiler error: unexpected panic

note: the compiler unexpectedly panicked. this is a bug.

note: we would appreciate a bug report: https://github.com/rust-lang/rust/issues/new?labels=C-bug%2C+I-ICE%2C+T-compiler&template=ice.md

note: rustc 1.59.0-dev running on x86_64-unknown-linux-gnu

note: compiler flags: -Z codegen-backend=gotoc -Z trim-diagnostic-paths=no -Z human_readable_cgu_names -C embed-bitcode=no -C debuginfo=2 -C overflow-checks=on --crate-type lib

note: some of the compiler flags provided by cargo are hidden

query stack during panic:
end of query stack

[RMC] current codegen item: codegen_function: decode_utf8_lossy
_ZN16percent_encoding17decode_utf8_lossy17h0e9f786e584e1458E
[RMC] current codegen location: Loc { file: "/home/ubuntu/.cargo/registry/src/github.com-1ecc6299db9ec823/percent-encoding-2.1.0/lib.rs", function: None, line: 427, col: Some(1) }

RMC unexpectedly panicked during code generation.

If you are seeing this message, please file an issue here instead of on the Rust compiler: https://github.com/model-checking/rmc/issues/new?labels=bug&template=bug_report.md
error: could not compile `percent-encoding`
@zhassan-aws zhassan-aws added the [C] Bug This is a bug. Something isn't working. label Dec 2, 2021
@zhassan-aws
Copy link
Contributor Author

The following snippet is sufficient to trigger the same panic:

fn main() {
    let s = "foo";
    let a: *const [u8] = s.as_bytes();
    let arr: [u8; 3] = [1, 2, 3];
    let b = &arr;
    assert!(a == &*b as *const [u8]);
}

@zhassan-aws
Copy link
Contributor Author

Still crashes with the same message with af11d38d93a using cargo kani --only-codegen.

celinval added a commit to celinval/kani-dev that referenced this issue Apr 20, 2022
@celinval
Codegen unimplemented for fat pointer operations for now
ac6ca8e 
This mitigates model-checking#327 and model-checking#675
celinval added a commit to celinval/kani-dev that referenced this issue Apr 20, 2022
@celinval
Add codegen test to model-checking#675
028a2ae 
The verification still fails due to missing std function.
celinval added a commit that referenced this issue Apr 22, 2022
@celinval
Codegen unimplemented for fat pointer operations for now (#1084)
f63d143 
This mitigates #327 and #675
@celinval
Copy link
Contributor

We no longer crash for this crate but we are unable to verify code that includes comparison of fat pointers. We will handle this on the original issue: #327.

I'm closing this one since the error reported has been mitigated.

tedinski pushed a commit that referenced this issue Apr 27, 2022
@celinval @tedinski
Codegen unimplemented for fat pointer operations for now (#1084)
ac2b1de 
This mitigates #327 and #675
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@celinval celinval

Labels
[C] Bug This is a bug. Something isn't working.
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@celinval @zhassan-aws