Closed Ekleog closed 6 months ago
Hmmm seems like the tests are failing due to kani
on MacOS…? Unfortunately I know literally nothing about kani, do you have any idea what this could be due to?
error: internal compiler error: Kani unexpectedly panicked at panicked at cprover_bindings/src/goto_program/stmt.rs:170:9:
thread 'rustc' panicked at cprover_bindings/src/goto_program/stmt.rs:170:9:
assertion `left == right` failed: Error: assign statement with unequal types lhs Pointer { typ: StructTag("tag-_98053125857340468998566196306834697786") } rhs CInteger(SSizeT)
assertion `left == right` failed: Error: assign statement with unequal types lhs Pointer { typ: StructTag("tag-_98053125857340468998566196306834697786") } rhs CInteger(SSizeT)
left: Pointer { typ: StructTag("tag-_98053125857340468998566196306834697786") }
right: CInteger(SSizeT)
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::sync::atomic::atomic_sub::<*mut std::sys::pal::unix::locks::queue_rwlock::Node>
_ZN4core4sync6atomic10atomic_sub17h64afa658122eff2eE
[Kani] current codegen location: Loc { file: "/Users/runner/.rustup/toolchains/nightly-2024-02-14-x86_64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs", function: None, start_line: 3352, start_col: Some(1), end_line: 3352, end_col: Some(73) }
left: Pointer { typ: StructTag("tag-_98053125857340468998566196306834697786") }
right: CInteger(SSizeT).
error: could not compile `basic` (lib test)
error: Failed to compile `basic` due to an internal compiler error.: error: internal compiler error: Kani unexpectedly panicked at panicked at cprover_bindings/src/goto_program/stmt.rs:170:9:
assertion `left == right` failed: Error: assign statement with unequal types lhs Pointer { typ: StructTag("tag-_98053125857340468998566196306834697786") } rhs CInteger(SSizeT)
left: Pointer { typ: StructTag("tag-_98053125857340468998566196306834697786") }
right: CInteger(SSizeT).
error: getting status result from command "cargo" "kani" "--tests" "--harness" "tests::add_test": process exited with status 1
Hmm none of the changes you've made here should interact with Kani, so I'm assuming it's failing even outside of these changes. I will open a PR up with them; it should never encounter an internal compiler error.
Thank you! :D When do you think you could release? I'm thinking this would be a very useful change to pull in on my end (in a soon-to-be-published crate, so it's hard to just patch), so that I could replace my current batch of with_iterations(20)
that take hours due to running the whole corpus anyway :)
I won't be able to release it until next Monday (I'm on vacation with no computer 😁). But I can add you to the crate owners if you're wanting it sooner. Just let me know which GitHub handle you'd like me to add, if so.
Of course, no hurry and have a good vacation! I'll be mostly away from computer until next Tuesday anyway, I was just asking to know if there's anything else that you wanted to do before release, like last time :)
As for the multiple github handles, basically Ekleog-NEAR is the account I use on my work machine and Ekleog on my personal machine, hence the two accounts. (but soon we're going to switch back to individually-administrated work machines so I'll probably just ditch Ekleog-NEAR then)
I've noticed that some of my bolero tests are very unbelievably slow to run. This is because bolero runs through the whole local corpus on each run, and my tests are fundamentally slow (~10 execs / second, with a multi-thousand corpus).
My solution up to now was to have another corpus directory, but it means that I cannot use the base bolero commands, etc.
Instead, here is an idea: what if we replaced
with_iterations
withwith_test_time
? What's important for the user is the time taken by the test anyway, considering that the tests are random anyway. And computers can have vastly different speeds.In addition, doing things this way allows setting a reasonable default test duration (1s) that's independent of how slow the tests themselves are, and that test duration will stop the tests even if they're still in the process of going through the corpus.
WDYT? :)