Inject pointer validity check when casting raw pointers to references #3221
Conversation
artemagvanian
force-pushed
the
main
branch
7 times, most recently
from
285ac5b
to
5120b02
Compare
|
I'm opposed to adding yet another flag for this adds more cognitive load for users. My understanding of the rationale for this flag is that the extra checks made a single test go out-of-memory in GitHub CI, but that test is exactly the one discussed in #3030: this test already is very close to running OOM and could really go over the limit with about any change, say a toolchain upgrade. My proposal is to disable this one test for the time being and instead independently investigate how to make it cheaper. |
|
That makes sense given the fact that the harness was already close to running OOM. I disabled the test by changing the |
|
Instead of changing the |
There was a problem hiding this comment.
Great work, @artemagvanian!
We need to avoid overriding the files in s2n-quic, as the regression is meant to ensure we don't break our customers' CI.
tests/perf/overlays/s2n-quic/quic/s2n-quic-core/src/inet/checksum.rs
Outdated
Show resolved
Hide resolved
…and str's (#3513) As pointed out in #3498, validity checks for pointer to reference casts (added in #3221) were not instrumented in the case of fat pointers (e.g. array and string slices). This PR extends the instrumentation of validity checks to handle those cases. Resolves #3498 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Celina G. Val <[email protected]>
Resolves #2975
This PR makes Kani able to check if a raw pointer is valid before casting it to a reference.
To check for the pointer validity when casting it to a reference, inject asserting
__CPROVER_r_ok(ptr, sz)into places where a raw pointer is dereferenced and a reference is immediately taken.Since this check seems to cause some of the CIs to run out of memory, it is only enabled under
-Z ptr-to-ref-cast-checksflag.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.