Kani crashes when an intrinsic call using ZST is invalid

[celinval]

I tried this code:

#![feature(core_intrinsics)]
use std::intrinsics::ctpop;

// These shouldn't compile.
#[kani::proof]
pub fn check_zst_ctpop() {
    let n = ctpop(());
    assert!(n == ());
}

and also this code:

#![feature(core_intrinsics)]
use std::intrinsics::sub_with_overflow;

#[kani::proof]
pub fn check_zst_sub_with_overflow() {
    let n = sub_with_overflow((), ());
    assert!(!n.1);
}

using the following command line invocation:

kani ice.rs

with Kani version:

I expected to see this happen: Kani should fail with a compilation error similar to running rustc ice.rs

Instead, this happened: Kani crashes.

thread '<unnamed>' panicked at 'BinaryOperation Expression does not typecheck OverflowResultMinus Expr { value: Symbol { identifier: "arithmetic_zst_fixme::check_zst_sub_with_overflow::1::var_2" }, typ: StructTag("tag-Unit"), loc
ation: None } Expr { value: Symbol { identifier: "arithmetic_zst_fixme::check_zst_sub_with_overflow::1::var_3" }, typ: StructTag("tag-Unit"), location: None }', cprover_bindings/src/goto_program/expr.rs:1000:9                    
stack backtrace:                                                                                                                                                                                                                     
   0: rust_begin_unwind                                                                                           
             at /rustc/c5d82ed7a4ad94a538bb87e5016e7d5ce0bd434b/library/std/src/panicking.rs:575:5                
   1: core::panicking::panic_fmt                                                                                  
             at /rustc/c5d82ed7a4ad94a538bb87e5016e7d5ce0bd434b/library/core/src/panicking.rs:65:14                                                                                                                                  
   2: cprover_bindings::goto_program::expr::Expr::binop                                                                                                                                                                              
             at /kani/cprover_bindings/src/goto_program/expr.rs:1000:9
   3: cprover_bindings::goto_program::expr::Expr::sub_overflow_result                                             
             at /kani/cprover_bindings/src/goto_program/expr.rs:1468:9                                                                                                           
   4: kani_compiler::codegen_cprover_gotoc::codegen::intrinsic::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_intrinsic                                                                          
             at /kani/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs:631:36                                       
   5: kani_compiler::codegen_cprover_gotoc::codegen::intrinsic::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_funcall_of_intrinsic                                                               
             at /kani/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs:74:21                                                                                         
   6: kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_funcall                                                                            
             at /kani/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs:513:20
   7: kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_terminator                                                                         
             at /kani/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs:209:17
   8: kani_compiler::codegen_cprover_gotoc::codegen::block::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_block
             at /kani/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs:22:29                      
   9: kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function::{{closure}}                                                               
             at /kani/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs:90:69                                                                                          
  10: core::iter::traits::iterator::Iterator::for_each::call::{{closure}}                                                                                                                                                            
             at /rustc/c5d82ed7a4ad94a538bb87e5016e7d5ce0bd434b/library/core/src/iter/traits/iterator.rs:828:29
  11: core::iter::adapters::map::map_fold::{{closure}}                                                                                                                                                                               
             at /rustc/c5d82ed7a4ad94a538bb87e5016e7d5ce0bd434b/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 /rustc/c5d82ed7a4ad94a538bb87e5016e7d5ce0bd434b/library/core/src/iter/adapters/enumerate.rs:106:27 
  13: core::iter::traits::iterator::Iterator::fold
             at /rustc/c5d82ed7a4ad94a538bb87e5016e7d5ce0bd434b/library/core/src/iter/traits/iterator.rs:2414:21
  14: <core::iter::adapters::enumerate::Enumerate<I> as core::iter::traits::iterator::Iterator>::fold
             at /rustc/c5d82ed7a4ad94a538bb87e5016e7d5ce0bd434b/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 /rustc/c5d82ed7a4ad94a538bb87e5016e7d5ce0bd434b/library/core/src/iter/adapters/map.rs:124:9
  16: core::iter::traits::iterator::Iterator::for_each                                                            
             at /rustc/c5d82ed7a4ad94a538bb87e5016e7d5ce0bd434b/library/core/src/iter/traits/iterator.rs:831:9
  17: kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function
             at /kani/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs:90:13
  18: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::{{closure}}::{{closure}}
             at /kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:130:39
  19: kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::{{closure}}
             at /kani/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs:68:13
  20: std::thread::local::LocalKey<T>::try_with
             at /rustc/c5d82ed7a4ad94a538bb87e5016e7d5ce0bd434b/library/std/src/thread/local.rs:446:16
  21: std::thread::local::LocalKey<T>::with
             at /rustc/c5d82ed7a4ad94a538bb87e5016e7d5ce0bd434b/library/std/src/thread/local.rs:422:9
  22: kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info
             at /kani/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs:65:9
  23: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::{{closure}}
             at /kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:129:29
  24: kani_compiler::codegen_cprover_gotoc::compiler_interface::with_timer
             at /kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:518:15
  25: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate
             at /kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:99:9
  26: <rustc_session::session::Session>::time::<alloc::boxed::Box<dyn core::any::Any>, rustc_interface::passes::start_codegen::{closure#0}>
  27: rustc_interface::passes::start_codegen
  28: <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::ErrorGuaranteed>>
  29: <rustc_interface::queries::Queries>::ongoing_codegen
  30: <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::ErrorGuaranteed>>
  31: rustc_span::with_source_map::<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_interface::interface::run_compiler<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_driver::run_compiler::{closure#1
}>::{closure#0}::{closure#1}>

[matthiaskrgr]

Might be related:

#![feature(core_intrinsics, generators, generator_trait, is_sorted)]

#[cfg(target_arch = "x86_64")]
use std::arch::x86_64::*;

#[kani::proof]
fn main() {}


#[cfg(target_arch = "x86_64")]
#[target_feature(enable = "sse2")]
#[kani::proof]
unsafe fn test_mm_add_pd() {
    let a = _mm_setr_pd(1.0, 2.0);
    let b = _mm_setr_pd(5.0, 10.0);
    let r = _mm_add_pd(a, b);
}

[JustusAdam]

I added basic logic to catch the ctpop case before it gets to the backend. It now generates this error message:

error: Type Check Failure: Expected integer type for call to `ctpop`, found StructTag("tag-Unit")
  --> fixme_ctpop_ice.rs:12:13
   |
12 |     let n = ctpop(());
   |             ^^^^^^^^^

error: aborting due to previous error

error: /Users/justbldr/research/kani/target/kani/bin/kani-compiler exited with status exit status: 1

However there are several open questions wrt. a comprehensive fix.

• At the moment I essentially perform the same type check that cprover_bindings does but earlier, when we have access to the rustc session and can gracefully emit errors. The clean thing to do here is to only perform this type check in one place. Probably cleanest to have functions that perform type checks (such as Expr::popcont) return Result so that it propagates the error gracefully and then turn it into a rustc error. That's a bigger change though that I could use feedback on. Specifically if it is appropriate to change the signature of e.g. Expr::popcount to reeturn Result, or if instead we want to keep them for backward compatibility and add an opt_* suite of functions with graceful errors or if we shouldn't make any changes to cprover_bindings?
  The Result approach would also make it easier to expand this fix to any other, similar cases as they are then obvious from the change in type.
• I used the Debug printing of the internal Type struct here, since that's what's available at that point and because it does not implement Display, but this won't mean much to the user so I'll have to revisit this to make it more meaningful. Would it be better to implement Display, propagate the error even further so we have access to the rust type or is there already a pretty-printing function I just didn't see?
• Emitting errors via tcx.sess does not immediately abort the compilation (unlike assert!). This means I need to emit a no-op Stmt to make codegen_intrinsic's type happy. Depending on the statement used and when exactly the compiler aborts this could (possibly) cause weird error downstream. I'm using Stmt::skip but that may not be the right choice.

Obviously the fixes for the other examples are missing as well, but they sort of depend on answers to the questions raised above.

[celinval]

I added basic logic to catch the ctpop case before it gets to the backend. It now generates this error message:

Where exactly did you add this logic?

error: Type Check Failure: Expected integer type for call to `ctpop`, found StructTag("tag-Unit")
  --> fixme_ctpop_ice.rs:12:13
   |
12 |     let n = ctpop(());
   |             ^^^^^^^^^

error: aborting due to previous error

error: /Users/justbldr/research/kani/target/kani/bin/kani-compiler exited with status exit status: 1

However there are several open questions wrt. a comprehensive fix.

• At the moment I essentially perform the same type check that cprover_bindings does but earlier, when we have access to the rustc session and can gracefully emit errors. The clean thing to do here is to only perform this type check in one place. Probably cleanest to have functions that perform type checks (such as Expr::popcont) return Result so that it propagates the error gracefully and then turn it into a rustc error. That's a bigger change though that I could use feedback on. Specifically if it is appropriate to change the signature of e.g. Expr::popcount to reeturn Result, or if instead we want to keep them for backward compatibility and add an opt_* suite of functions with graceful errors or if we shouldn't make any changes to cprover_bindings?
  The Result approach would also make it easier to expand this fix to any other, similar cases as they are then obvious from the change in type.

Most of our codegen functions just assume that types have been checked before, and incompatible types are handled as bugs. The main exception to this rule is intrinsics. Some of them have a rather generic declaration, and type checking is deferred to the backend. Thus, we add extra checks as part of intrinsics handling. You can see an example on how this is handled here:

kani/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

Lines 1249 to 1257 in dfa0e5b

	_ => {
	let err_msg = format!(
	"simd_shuffle index must be an array of `u32`, got `{}`",
	farg_types[2]
	);
	self.tcx.sess.span_err(span.unwrap(), err_msg);
	// Return a dummy value
	u64::MIN
	}

• I used the Debug printing of the internal Type struct here, since that's what's available at that point and because it does not implement Display, but this won't mean much to the user so I'll have to revisit this to make it more meaningful. Would it be better to implement Display, propagate the error even further so we have access to the rust type or is there already a pretty-printing function I just didn't see?

The cprover_bindings crate was designed to reflect the goto-program language, and it might be hard to retrieve the exact Rust type after it has been translated. I would suggest that you use Ty instead.

• Emitting errors via tcx.sess does not immediately abort the compilation (unlike assert!). This means I need to emit a no-op Stmt to make codegen_intrinsic's type happy. Depending on the statement used and when exactly the compiler aborts this could (possibly) cause weird error downstream. I'm using Stmt::skip but that may not be the right choice.

You got the right idea. We do want to abort at that point. If you look at the function I pointed above, you will notice that at the end of the validation we invoke abort_if_errors() to stop the compilation.

kani/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

Line 1269 in dfa0e5b

self.tcx.sess.abort_if_errors();

Obviously the fixes for the other examples are missing as well, but they sort of depend on answers to the questions raised above.

Thanks for taking a look at it.

[JustusAdam]

@matthiaskrgr I was not able to reproduce your issue on 522616980eeac0130803838549a4c3a884e75773. What is the error you encountered?

[matthiaskrgr]

with kani 0.29.0 I get

warning: unused variable: `r`
  --> kani.rs:16:9
   |
16 |     let r = _mm_add_pd(a, b);
   |         ^ help: if this is intentional, prefix it with an underscore: `_r`
   |
   = note: `#[warn(unused_variables)]` on by default

thread 'rustc' panicked at 'BinaryOperation Expression does not typecheck OverflowPlus Expr { value: Index { array: Expr { value: Symbol { identifier: "_RNvNtNtNtCsg38raRqfonS_4core9core_arch3x864sse210__mm_add_pdCsdqAnRMfZsQO_4kani::1::var_1::a" }, typ: Vector { typ: Double, size: 2 }, location: None, size_of_annotation: None }, index: Expr { value: IntConstant(0), typ: CInteger(SSizeT), location: None, size_of_annotation: None } }, typ: Double, location: None, size_of_annotation: None } Expr { value: Index { array: Expr { value: Symbol { identifier: "_RNvNtNtNtCsg38raRqfonS_4core9core_arch3x864sse210__mm_add_pdCsdqAnRMfZsQO_4kani::1::var_2::b" }, typ: Vector { typ: Double, size: 2 }, location: None, size_of_annotation: None }, index: Expr { value: IntConstant(0), typ: CInteger(SSizeT), location: None, size_of_annotation: None } }, typ: Double, location: None, size_of_annotation: None }', cprover_bindings/src/goto_program/expr.rs:1033:9
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Kani unexpectedly panicked during compilation.
Please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md

[Kani] current codegen item: codegen_function: std::arch::x86_64::_mm_add_pd
_RNvNtNtNtCsg38raRqfonS_4core9core_arch3x864sse210__mm_add_pdCsdqAnRMfZsQO_4kani
[Kani] current codegen location: Loc { file: "/github/home/.rustup/toolchains/nightly-2023-04-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/../../stdarch/crates/core_arch/src/x86/sse2.rs", function: None, start_line: 1600, start_col: Some(1), end_line: 1600, end_col: Some(60) }
warning: 1 warning emitted

error: /home/matthias/.kani/kani-0.29.0/bin/kani-compiler exited with status exit status: 101

[JustusAdam]

Oh my fault, I am running on arm so all the interesting code is not even included.

[zhassan-aws]

As of #3183 (which includes rust-lang/rust#124003), the test including ctpop now produces a compiler error:

$ kani ctpop_ice.rs 
Kani Rust Verifier 0.51.0 (standalone)
warning: the feature `core_intrinsics` is internal to the compiler or standard library
 --> ctpop_ice.rs:6:12
  |
6 | #![feature(core_intrinsics)]
  |            ^^^^^^^^^^^^^^^
  |
  = note: using it is strongly discouraged
  = note: `#[warn(internal_features)]` on by default

error[E0308]: mismatched types
  --> ctpop_ice.rs:13:18
   |
13 |     assert!(n == ());
   |             -    ^^ expected `u32`, found `()`
   |             |
   |             expected because this is `u32`

error: aborting due to 1 previous error; 1 warning emitted

For more information about this error, try `rustc --explain E0308`.
error: /home/ubuntu/git/kani/target/kani/bin/kani-compiler exited with status exit status: 1

Closing this issue.