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

Latest kani version breaks CI job #3142

Closed
tcharding opened this issue Apr 15, 2024 · 5 comments
Closed

Latest kani version breaks CI job #3142

tcharding opened this issue Apr 15, 2024 · 5 comments
Labels
[C] Bug This is a bug. Something isn't working.

Comments

@tcharding
Copy link

Thanks for your tool!

We run kani daily in CI and also on each PR we run it with cargo kani --codegen-only.

Today the --codegen-only job broke. It looks like its something to do with the latest release of kani but I'm not sure why its turned up today when the release came out 10 days ago.

The build warning we are seeing is:

error[E0658]: use of unstable library feature 'proc_macro_byte_character'
   --> /home/runner/.cargo/registry/src/index.crates.io-6f17d22bba15001f/proc-macro2-1.0.80/src/wrapper.rs:871:21
    |
871 |                     proc_macro::Literal::byte_character(byte)
    |                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |

I tried using kani v0.48.0 and the job succeeds.

Example of job failing: https://github.com/rust-bitcoin/rust-bitcoin/actions/runs/8682612259/job/23807404841#step:3:288
CI passing after version pinned: rust-bitcoin/rust-bitcoin#2686

And this is how we are running the job:

  Kani:
    runs-on: ubuntu-20.04
    steps:
      - name: 'Checkout your code.'
        uses: actions/checkout@v4

      - name: 'Kani build proofs'
        uses: model-checking/kani-github-action@v1.1
        with:
          args: '--only-codegen'
@tcharding tcharding added the [C] Bug This is a bug. Something isn't working. label Apr 15, 2024
@tcharding tcharding mentioned this issue Apr 15, 2024
Merged
@tatsuya6502 tatsuya6502 mentioned this issue Apr 16, 2024
Closed
@tautschnig
Copy link
Member

Please see #3138 for some initial discussion (including pointers to non-Kani projects that seem to be affected). #3144 will fix this problem via toolchain upgrade.

@tautschnig tautschnig mentioned this issue Apr 16, 2024
Merged
@tcharding
Copy link
Author

Legend, thank you.

This was referenced Apr 16, 2024
Closed
Open
apoelstra added a commit to rust-bitcoin/rust-bitcoin that referenced this issue Apr 16, 2024
@apoelstra
Merge #2686: Fix kani codegen CI job
87b674b 
0f0bd91 kani: Pin version to 0.48.0 (Tobin C. Harding)
5981b15 kani: Rename tests (Tobin C. Harding)
17bacc6 kani: Remove redundant import (Tobin C. Harding)

Pull request description:

  Fix the current failing Kani job on todays PRs.

  FTR our daily `kani` job has been red for ages, perhaps since we created the `units` crate? But today the `--codege-only` job broke (on all PRs). `kani` released a new version 10 days ago, pinning to the previous version seems to resolve the issue. I raised a bug report but did not investigate further.

  - Patch 1: Remove redundant import
  - Patch 2: Rename the tests
  - Patch 3: Pin kani version

  File bug report: model-checking/kani#3142

  PR is CI only, can go in with one ack.

  (Patch 2 is the result of debugging the _real_ kani failure we have at the moment, I'll save the rant for the PR that fixes it.)

ACKs for top commit:
  apoelstra:
    ACK 0f0bd91 though I wonder if we shoud comment out the test in rust.yml and file an issue
  sanket1729:
    utACK 0f0bd91

Tree-SHA512: 1e510dd53f3474dd4891792e312444cec57239c865e4cd7d144932713b3ce2e66806a37b88d55ecaa514292ac936de569cc9126c773048a5a930c6c822faad29
celinval added a commit that referenced this issue Apr 16, 2024
@celinval
Upgrade toolchain to nightly-2024-04-15 (#3144)
b9bd7a8 
Related changes:
  - rust-lang/rust#118310:
    Add `Ord::cmp` for primitives as a `BinOp` in MIR
  - rust-lang/rust#120131:
    Add support to `Pat` pattern type
  - rust-lang/rust#122935:
    Rename CastKind::PointerWithExposedProvenance
  - rust-lang/rust#123097:
    Adapt to changes to local_def_path_hash_to_def_id

Resolves #3130, #3142
celinval added a commit to celinval/kani-dev that referenced this issue Apr 17, 2024
@celinval
Upgrade toolchain to nightly-2024-04-15 (model-checking#3144)
5d962b5 
Related changes:
  - rust-lang/rust#118310:
    Add `Ord::cmp` for primitives as a `BinOp` in MIR
  - rust-lang/rust#120131:
    Add support to `Pat` pattern type
  - rust-lang/rust#122935:
    Rename CastKind::PointerWithExposedProvenance
  - rust-lang/rust#123097:
    Adapt to changes to local_def_path_hash_to_def_id

Resolves model-checking#3130, model-checking#3142
@celinval
Copy link
Contributor

@tcharding were you able to verify that kani-0.50.0 fixes your issue? Thanks!

@tcharding
Copy link
Author

Yep fixed! Thanks a bunch.

@tcharding
Copy link
Author

Verified with rust-bitcoin/rust-bitcoin#2709

zpzigi754 pushed a commit to zpzigi754/kani that referenced this issue May 8, 2024
@celinval @zpzigi754
Upgrade toolchain to nightly-2024-04-15 (model-checking#3144)
6bd7ef8 
Related changes:
  - rust-lang/rust#118310:
    Add `Ord::cmp` for primitives as a `BinOp` in MIR
  - rust-lang/rust#120131:
    Add support to `Pat` pattern type
  - rust-lang/rust#122935:
    Rename CastKind::PointerWithExposedProvenance
  - rust-lang/rust#123097:
    Adapt to changes to local_def_path_hash_to_def_id

Resolves model-checking#3130, model-checking#3142
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
[C] Bug This is a bug. Something isn't working.
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@tautschnig @tcharding @celinval