Skip to content

kani autoharness with --harness panics in determine_targets on debug builds #4939

Open

Description

@ivmat

The issue can be reproduced with this code:

fn add(a: u8, b: u8) -> u8 {
    a.wrapping_add(b)
}

#[kani::proof]
fn manual() {
    assert!(add(1, 1) == 2);
}

and the following command line invocation:
kani autoharness -Z autoharness repro.rs --harness manual
Kani version: 0.68.0, a debug build (cargo build-dev) of main at b1bdd18. The code involved is unchanged on current main.

Expected behavior: manual and the automatic harness for add are verified, as without --harness. kani autoharness -Z autoharness repro.rs (no filter) verifies both and exits 0.

Actual behavior: the driver panics before verification (exit code 101). The same happens with a filter that matches nothing (--harness nomatch):

thread 'main' panicked at kani-driver/src/metadata.rs:108:13:

assertion `left == right` failed
  left: [HarnessMetadata { pretty_name: "manual", .. }, HarnessMetadata { pretty_name: "add", .., is_automatically_generated: true, .. }]
 right: [HarnessMetadata { pretty_name: "manual", .. }]

stack backtrace:

...
   4: <kani_driver::session::KaniSession>::determine_targets
             at ./kani-driver/src/metadata.rs:108:13
   5: kani_driver::verify_project
             at ./kani-driver/src/main.rs:177:29
   6: kani_driver::autoharness::postprocess_project
             at ./kani-driver/src/autoharness/mod.rs:117:52
   7: kani_driver::autoharness::autoharness_standalone
             at ./kani-driver/src/autoharness/mod.rs:52:5
   8: kani_driver::standalone_main
             at ./kani-driver/src/main.rs:141:20
   9: kani_driver::main
             at ./kani-driver/src/main.rs:68:39

The debug-only check in determine_targets compares the compiler's filtered list with a re-filter through find_proof_harnesses. The compiler keeps every automatic harness, but find_proof_harnesses skips automatic harnesses (kani_metadata/src/harness.rs), so the two lists differ whenever autoharness generates at least one harness and a --harness filter is given. Release builds skip this check.

The issue was found during the development of #4771 and was left out of that PR's scope.

Activity

  1. added
    [C] BugThis is a bug. Something isn't working.
    on Oct 1, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    [C] BugThis is a bug. Something isn't working.

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions