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.

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

Kani cannot handle constant slice with element type different than U8. #1339

Open
celinval opened this issue Jul 6, 2022 · 1 comment
Open
Labels
[C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed

Comments

@celinval
Copy link
Contributor

celinval commented Jul 6, 2022

I tried compiling the std crate after updating the toolchain to 2022-07-05. I got the following error while trying code generation of the std library using the following command line invocation:

./scripts/std-lib-regression.sh

with Kani version: 0.5

I expected to see this happen: Finished Kani codegen for the Rust standard library successfully...

Instead, this happened:

thread 'rustc' panicked at 'not implemented:                                                                                                                                                                
v Slice { data: Allocation { bytes: [0, 1, 3, 5, 5, 6, 6, 2, 7, 6, 8, 7, 9, 17, 10, 28, 11, 25, 12, 26, 13, 16, 14, 13, 15, 4, 16, 3, 18, 18, 19, 9, 22, 1, 23, 4, 24, 1, 25, 3, 26, 7, 27, 1, 28, 2, 31, 22
, 32, 3, 43, 3, 45, 11, 46, 1, 48, 3, 49, 2, 50, 1, 167, 2, 169, 2, 170, 4, 171, 8, 250, 2, 251, 5, 253, 2, 254, 3, 255, 9], relocations: Relocations(SortedMap { data: [] }), init_mask: InitMask { blocks:
 [18446744073709551615, 65535], len: Size(80 bytes) }, align: Align(128 bytes), mutability: Not, extra: () }, start: 0, end: 40 }                                                                           
lit_ty &[(u8, u8)]                                                                                                                                                                                          
span Some(/rustup/toolchains/nightly-2022-07-05-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/unicode/printable.rs:50:22: 50:34 (#0))', kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs:132:9 

[Kani] current codegen item: codegen_function: unicode::printable::is_printable                                                                                                                             
_ZN4core7unicode9printable12is_printable17h26e35c8ac4e6d19aE                                                                                                                                                
[Kani] current codegen location: Loc { file: "/rustup/toolchains/nightly-2022-07-05-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/unicode/printable.rs", func
tion: None, line: 39, col: Some(1) } 
@celinval celinval added the [C] Bug This is a bug. Something isn't working. label Jul 6, 2022
celinval added a commit to celinval/kani-dev that referenced this issue Jul 6, 2022
@danielsn
Copy link
Contributor

danielsn commented Jul 6, 2022

celinval added a commit that referenced this issue Jul 6, 2022
* Update toolchain to 2022-07-05

The updates required were related to the following changes:
  - Simplify memory ordering intrinsics
    - rust-lang/rust#97423
  - once cell renamings
    - rust-lang/rust#98165
  - Rename the ConstS::val field as kind
    - rust-lang/rust#97935
  - Remove the source archive functionality of ArchiveWriter
    - rust-lang/rust#98098
  - Use valtrees as the type-system representation for constant values
    - rust-lang/rust#96591

* Codegen unimplemented for unsupported constant slices

See #1339 for more details.

* Fix copyright check

* Use codegen_option_span instead
@tedinski tedinski added the [F] Crash Kani crashed label Nov 28, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed
Projects
None yet
Development

No branches or pull requests

3 participants