Improve symbolic execution performance when running against concrete values #2363
Comments
celinval
added
[E] Performance
|
Here is one such example: #[kani::proof]
#[kani::unwind(7)]
#[kani::solver(cadical)]
fn main() {
let s = "Mary had a little lamb";
let v: Vec<&str> = s.split(' ').collect();
assert_eq!(v, ["Mary", "had", "a", "little", "lamb"]);
}This takes ~77 seconds with ~150 seconds with and ~635 seconds with minisat: MIRI takes 0.2 seconds on this example. |
|
Given we seem to manage to do ~27.5k (complex) instructions per second, which is certainly not below what we usually see. But: we can and should still seek to improve on that, so I'll happily take up that challenge. (Also, the number of instructions does not seem excessive: |
|
@tautschnig do you know why this is invoking the SAT solver? I don't know much about the symbolic execution engine, but I was hoping that it would be able to solve these cases on its own. |
That's a good point that needs digging in a bit more: I believe that Kani's reachability assertions will mean we invoke the solver in some way, but then all the queries should be trivial (because the path conditions for those assertions should trivially be TRUE or FALSE, and the solver should have no clauses in the input formula). |
|
I tried it without reachability checks as well, and it was slightly faster. It also performed a single SAT query: |
|
Disabling all CBMC checks cuts the time in half: |
|
We need to look into overriding |
This hook intercepts calls to `std::ptr::align_offset<T>` as CBMC's memory model has no concept of alignment of allocations, so we would have to non-deterministically choose an alignment of the base pointer, add the pointer's offset to it, and then do the math that is done in `library/core/src/ptr/mod.rs`. Instead, we choose to always return `usize::MAX`, per `align_offset`'s documentation, which states: "It is permissible for the implementation to always return usize::MAX. Only your algorithm’s performance can depend on getting a usable offset here, not its correctness." Fixes: model-checking#2363
|
Another example from #2235: fn main() {
let x = String::new().repeat(1);
assert!(x.chars().nth(1).is_none());
}This runs for |
|
Another case is #2517. |
Requested feature: When running Kani assess, many unit tests take a long time to run. Since these tests run with concrete inputs, I would expect the performance to be somewhat similar to MIRI.
Use case: Running tests to find undefined behavior + potential improvement to harnesses.
Link to relevant documentation (Rust reference, Nomicon, RFC):
Test case:
// TODOThe text was updated successfully, but these errors were encountered: