Kani does not support fat pointer comparison

[avanhatt]

RMC crashes on the core Rust test (src/test/ui/raw-fat-ptr.rs).

After minimizing:

trait a {}
fn main() {
  let b : &mut[ *const a] = &mut[];
  b.sort_by(| c, d | c.cmp(d))
}

thread 'rustc' panicked at 'BinaryOperation Expression does not typecheck Equal Expr { value: Symbol { identifier: "_RNvXs0_NtNtCsgWci0eQkB8o_4core3ptr9const_ptrPDNtCs8ZdcvQGSn7l_4test1aEL_NtNtB9_3cmp9PartialEq2eqBK_::1::var_3" }, typ: StructTag("tag-dyn a"), location: None } Expr { value: Symbol { identifier: "_RNvXs0_NtNtCsgWci0eQkB8o_4core3ptr9const_ptrPDNtCs8ZdcvQGSn7l_4test1aEL_NtNtB9_3cmp9PartialEq2eqBK_::1::var_4" }, typ: StructTag("tag-dyn a"), location: None }', compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs:863:9
stack backtrace:
   0: rust_begin_unwind
             at ./library/std/src/panicking.rs:517:5
   1: std::panicking::begin_panic_fmt
             at ./library/std/src/panicking.rs:460:5
   2: rustc_codegen_llvm::gotoc::cbmc::goto_program::expr::Expr::binop
             at ./compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs:863:9
   3: rustc_codegen_llvm::gotoc::cbmc::goto_program::expr::Expr::eq
             at ./compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs:985:9
   4: rustc_codegen_llvm::gotoc::rvalue::<impl rustc_codegen_llvm::gotoc::metadata::GotocCtx>::codegen_comparison
             at ./compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs:24:21
   5: rustc_codegen_llvm::gotoc::rvalue::<impl rustc_codegen_llvm::gotoc::metadata::GotocCtx>::codegen_rvalue_binary_op
             at ./compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs:305:17
   6: rustc_codegen_llvm::gotoc::rvalue::<impl rustc_codegen_llvm::gotoc::metadata::GotocCtx>::codegen_rvalue
             at ./compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs:373:59
   7: rustc_codegen_llvm::gotoc::statement::<impl rustc_codegen_llvm::gotoc::metadata::GotocCtx>::codegen_statement
             at ./compiler/rustc_codegen_llvm/src/gotoc/statement.rs:482:33
   8: rustc_codegen_llvm::gotoc::<impl rustc_codegen_llvm::gotoc::metadata::GotocCtx>::codegen_block
             at ./compiler/rustc_codegen_llvm/src/gotoc/mod.rs:124:32
   9: rustc_codegen_llvm::gotoc::<impl rustc_codegen_llvm::gotoc::metadata::GotocCtx>::codegen_function::{{closure}}
             at ./compiler/rustc_codegen_llvm/src/gotoc/mod.rs:295:71
  10: core::iter::traits::iterator::Iterator::for_each::call::{{closure}}
             at ./library/core/src/iter/traits/iterator.rs:730:29
  11: core::iter::adapters::map::map_fold::{{closure}}
             at ./library/core/src/iter/adapters/map.rs:84:21
  12: <core::iter::adapters::enumerate::Enumerate<I> as core::iter::traits::iterator::Iterator>::fold::enumerate::{{closure}}
             at ./library/core/src/iter/adapters/enumerate.rs:106:27
  13: core::iter::traits::iterator::Iterator::fold
             at ./library/core/src/iter/traits/iterator.rs:2170:21
  14: <core::iter::adapters::enumerate::Enumerate<I> as core::iter::traits::iterator::Iterator>::fold
             at ./library/core/src/iter/adapters/enumerate.rs:112:9
  15: <core::iter::adapters::map::Map<I,F> as core::iter::traits::iterator::Iterator>::fold
             at ./library/core/src/iter/adapters/map.rs:124:9
  16: core::iter::traits::iterator::Iterator::for_each
             at ./library/core/src/iter/traits/iterator.rs:733:9
  17: rustc_codegen_llvm::gotoc::<impl rustc_codegen_llvm::gotoc::metadata::GotocCtx>::codegen_function
             at ./compiler/rustc_codegen_llvm/src/gotoc/mod.rs:295:13
  18: <rustc_codegen_llvm::gotoc::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::{{closure}}
             at ./compiler/rustc_codegen_llvm/src/gotoc/mod.rs:479:35
  19: rustc_codegen_llvm::gotoc::<impl rustc_codegen_llvm::gotoc::metadata::GotocCtx>::call_with_panic_debug_info::{{closure}}
             at ./compiler/rustc_codegen_llvm/src/gotoc/mod.rs:103:13
  20: std::thread::local::LocalKey<T>::try_with
             at ./library/std/src/thread/local.rs:399:16
  21: std::thread::local::LocalKey<T>::with
             at ./library/std/src/thread/local.rs:375:9
  22: rustc_codegen_llvm::gotoc::<impl rustc_codegen_llvm::gotoc::metadata::GotocCtx>::call_with_panic_debug_info
             at ./compiler/rustc_codegen_llvm/src/gotoc/mod.rs:101:9
  23: <rustc_codegen_llvm::gotoc::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate
             at ./compiler/rustc_codegen_llvm/src/gotoc/mod.rs:478:25
  24: rustc_interface::passes::start_codegen::{{closure}}
             at ./compiler/rustc_interface/src/passes.rs:1056:9
  25: rustc_data_structures::profiling::VerboseTimingGuard::run
             at ./compiler/rustc_data_structures/src/profiling.rs:611:9
  26: rustc_session::utils::<impl rustc_session::session::Session>::time
             at ./compiler/rustc_session/src/utils.rs:16:9
  27: rustc_interface::passes::start_codegen
             at ./compiler/rustc_interface/src/passes.rs:1055:19
  28: rustc_interface::queries::Queries::ongoing_codegen::{{closure}}::{{closure}}
             at ./compiler/rustc_interface/src/queries.rs:254:20
  29: rustc_interface::passes::QueryContext::enter::{{closure}}
             at ./compiler/rustc_interface/src/passes.rs:780:42
  30: rustc_middle::ty::context::tls::enter_context::{{closure}}
             at ./compiler/rustc_middle/src/ty/context.rs:1784:50
  31: rustc_middle::ty::context::tls::set_tlv
             at ./compiler/rustc_middle/src/ty/context.rs:1768:9
  32: rustc_middle::ty::context::tls::enter_context
             at ./compiler/rustc_middle/src/ty/context.rs:1784:9
  33: rustc_interface::passes::QueryContext::enter
             at ./compiler/rustc_interface/src/passes.rs:780:9
  34: rustc_interface::queries::Queries::ongoing_codegen::{{closure}}
             at ./compiler/rustc_interface/src/queries.rs:245:13
  35: rustc_interface::queries::Query<T>::compute
             at ./compiler/rustc_interface/src/queries.rs:38:28
  36: rustc_interface::queries::Queries::ongoing_codegen
             at ./compiler/rustc_interface/src/queries.rs:243:9
  37: rustc_driver::run_compiler::{{closure}}::{{closure}}
             at ./compiler/rustc_driver/src/lib.rs:407:13
  38: rustc_interface::queries::<impl rustc_interface::interface::Compiler>::enter
             at ./compiler/rustc_interface/src/queries.rs:394:19
  39: rustc_driver::run_compiler::{{closure}}
             at ./compiler/rustc_driver/src/lib.rs:312:22
  40: rustc_interface::interface::create_compiler_and_run::{{closure}}
             at ./compiler/rustc_interface/src/interface.rs:209:13
  41: rustc_span::with_source_map
             at ./compiler/rustc_span/src/lib.rs:911:5
  42: rustc_interface::interface::create_compiler_and_run
             at ./compiler/rustc_interface/src/interface.rs:203:5
  43: rustc_interface::interface::run_compiler::{{closure}}
             at ./compiler/rustc_interface/src/interface.rs:225:12
  44: rustc_interface::util::setup_callbacks_and_run_in_thread_pool_with_globals::{{closure}}::{{closure}}
             at ./compiler/rustc_interface/src/util.rs:157:13
  45: scoped_tls::ScopedKey<T>::set
             at /home/ubuntu/.cargo/registry/src/github.com-1ecc6299db9ec823/scoped-tls-1.0.0/src/lib.rs:137:9
  46: rustc_span::create_session_globals_then
             at ./compiler/rustc_span/src/lib.rs:105:5
  47: rustc_interface::util::setup_callbacks_and_run_in_thread_pool_with_globals::{{closure}}
             at ./compiler/rustc_interface/src/util.rs:155:9
  48: rustc_interface::util::scoped_thread::{{closure}}
             at ./compiler/rustc_interface/src/util.rs:130:24
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.56.0-dev running on x86_64-unknown-linux-gnu

note: compiler flags: -Z codegen-backend=gotoc -Z symbol-mangling-version=v0 -Z symbol_table_passes=

query stack during panic:
end of query stack

[RMC] current codegen item: codegen_function: std::ptr::const_ptr::<impl std::cmp::PartialEq for *const T>::eq

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
warning: 2 warnings emitted

[celinval]

Note to myself: We need to compare the data field and, potentially, the metadata. Need to double check the latter.

[celinval]

https://doc.rust-lang.org/std/ptr/fn.eq.html

[celinval]

Lowering the priority since this has been mitigated.

[celinval]

I'm looking into this issue right now, but it is still not clear to me what the actual semantics of pointer comparison is for Rust. Even for thin pointers it isn't clear.

Interesting enough, the standard library does support Eq and Ord of raw pointers and the compiler behavior is somewhat deterministic (not clear if the LLVM portion is though). I'll keep digging.

Here are some interesting references:

• What are the exact semantics of pointer comparison? rust-lang/unsafe-code-guidelines#239
• Implement raw fat pointer comparisons rust-lang/rfcs#1135
• https://rust-lang.github.io/rfcs/1135-raw-pointer-comparisons.html

[celinval]

From this discussion in the zulip tlang channel, it seems that pointers with the same provenance, we should be able to do the following:

• Compare concrete address for data pointers and thin pointers.
• Compare metadata for fat pointers (i.e.: length or vtable pointer).

However, the vtable pointer has a few caveats.

1. It will only have the same provenance if they point to the same vtable.
2. In theory, vtable may have different addresses even if they represent the same type. That may happen when each pointer is created in a different compilation units (see this issue for more details).

So I propose the following solution.

1. For now, we add support to fat pointers that represent slice and fail for vtable pointers.
2. We create an issue to implement vtable pointer comparison but only implement that if there is a real need, since this operation is not stable, users should probably avoid them.
   . If we do want to implement vtable comparison, we should use their concrete address and add non-determinism via uninterpreted functions (See http://www.cprover.org/cprover-manual/modeling/nondeterminism/).

We should also defer implementing comparison between pointers with different provenance. This behavior is also not well defined.