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.
To put the hypotheses of an /EXPLICIT proof back in order, parseProof() copied the whole proof string at every step with hypotheses, although only the steps up to the current one were built. In the first proof the others are uninitialized memory, so this read indeterminate values: undefined behaviour, which MemorySanitizer reports. Copy only the steps built so far, which are all the rearrangement uses. The values read never reached the result, since only steps before the current one are copied back. Skipping the copies also makes verifying /EXPLICIT proofs slightly faster. The case open-msan-parseproof-uninit is now fixed: rename it parseproof-uninit.
benjub
changed the title
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
1 participant
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.
Depends on #208; first commit is 083ed66
parseProof()copied the entire arrayproofStringat every proof step with hypotheses, although only steps 0 tostepare built. In the first proof the rest is uninitialized memory, so copying them is UB (as reported by MemorySanitizer). Copy only the built steps.Results are unchanged, since only steps before
stepare copied back. Verifying/EXPLICITproofs gets slightly faster.The case
open-msan-parseproof-uninitadded in #208 now passes, so this renames itparseproof-uninitand marks it fixed.Written with help from Claude code.