Make analysis/test miri-compatible and add a miri test for it
#686
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
kkysen
changed the title
analysis/test miri-compatible and add a miri test for it
aneksteind
suggested changes
Sep 27, 2022
Merged
kkysen
added a commit
that referenced
this pull request
Sep 28, 2022
Fixes #680. See the commits for the individual fixes. The fixes are: * 2 use after frees: 429962d, 95e483d * 2 uninitialized reads: 50b1bb4, f6e5bce * 2 nullptr derefs: f96bcb2, 69de3c3 Now `cd analysis/test && cargo miri run` reports no UB. However, `miri` can't run variadic functions like `printf`, so running this requires the monomorphic `printf` shim in #686.
aneksteind
approved these changes
Sep 29, 2022
kkysen
force-pushed
the
kkysen/analysis-test-miri-compat
branch
from
c02f3e4 to
8c42e54
Compare
…so that it works with `miri`. This works in `analysis/test` because all `printf`s are monomorphic.
…rintf` shim is defined instead.
…i run --features miri`.
…at it's used to test `analysis/test`.
… running `miri` (which installs `xargo`) in CI. The test can still be manually run with `cargo test -p c2rust-pdg -- --ignored analysis_test_miri`.
kkysen
force-pushed
the
kkysen/analysis-test-miri-compat
branch
from
8c42e54 to
4152d34
Compare
|
There are issues with running |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Fixes #685.
This makes
analysis/testmiri-compatible when running with--features miri. This is done by using a monomorphicprintfshim, sincemirican't handle variadic functions likeprintf. Since all uses ofprintfinanalysis/testare monomorphic (they all have the same format string), we can substitute afn printfthat is non-extern "C", non-variadic (and thusmiri-compatible), and that still has the same behavior for its call sites.Then we add a test in
c2rust-pdgthat runsmirionanalysis/testto ensure it stays UB-free.However, we don't yet run this test by default (it's
#[ignore]d for now) as there are issues with runningmiriin CI (it installsxargoevery time and I'm getting a permission denied error (not sure from quite what exactly), and it'd be better to installxargoupfront, not on every run). Thus, I'm#[ignore]ing it for now in 4152d34. We can get it to run in CI correctly later in another PR, but I want to merge this now and avoid over-complicating it here. The test can still be manually run withcargo test -p c2rust-pdg -- --ignored analysis_test_miri. See #698 for the tracking issue to re-enable this test by default.The new test passing is blocked on:
analysis/test#683 (f ixes Fix UB inanalysis/test#680)analysis/test#684 (f ixes Fix non-intentional memory leaks inanalysis/test#681)It would also be nice to f ix #682, but that's not completely necessary for this (though it would create a much less noisy output).