Repository navigation
Conversation
build-sanitizer.sh also builds ./metamath-msan with MemorySanitizer, which reports reads of uninitialized memory. run-cases.sh runs the cases against it too; an open case is checked only against the binary whose sanitizer found it. MemorySanitizer finds a bug that AddressSanitizer misses: parseProof() copies an uninitialized proofString element. It is added as the case open-msan-parseproof-uninit. run-cases.sh and fuzz.py now recognize MemorySanitizer reports: this build exits with status 1, as metamath does on an ordinary error, so the status alone does not show them. Also fix a bug where fuzz.py could not run a binary given by a relative path, as in the README's own example, because each run happens in a temporary directory.
Collaborator
Author
|
@david-a-wheeler can you have a look at this ? It builds on your fuzzing suite, so I think you're the right person to review. Also, PR #209 builds on it (and I have another local branch that builds on #209), so it would be helpful to be able to merge both. |
Member
|
Hi, I'm not dead but I'm on travel. I won't be able to sit down and review seriously for a bit longer, but I will do so. Thanks so much for your work! |
This branch has not been deployed
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
build-sanitizer.sh now also builds fuzz/metamath-msan with MemorySanitizer, which reports reads of uninitialized memory that AddressSanitizer cannot see. It needs clang on Linux or a BSD. run-cases.sh runs the cases against both binaries.
It found a bug: parseProof() copies an uninitialized proofString element on tests/explicit.mm. Added as the case open-msan-parseproof-uninit.
run-cases.sh and fuzz.py now recognize MemorySanitizer reports, which exit with status 1 like an ordinary error. fuzz.py also accepts a relative --binary, as in the README's example.
The FIXED? note for open-assignvar-undeclared-var predates this PR: that case stopped reproducing with #198.
Written with help from Claude code.