Repository navigation
[9.0 parity 8/8] fix(output): own file for TARGET-REACHED (KLEE state race) - #54
Draft
GuilhermeBn198 wants to merge 1 commit into
Draft
GuilhermeBn198 wants to merge 1 commit into
GuilhermeBn198 wants to merge 1 commit into
Conversation
Under KLEE every state writes the same native map2check_property through external calls, and KLEE switches states between batches of instructions. A state that ended normally renamed its NONE over the violation while the violating state was still writing its aux files, before its abort halted the search, so a reachable target came back UNKNOWN (Map2Check 9.0's integration section 13, a two-step reactive loop; traced with strace). The rename of SD-20 keeps the file whole, not the violation. The other violations already had a file of their own, which no state that ends normally writes. TARGET-REACHED now has map2check_property_target, with the same text; Map2Check reads it before map2check_property. SD-20 and the TARGET-REACHED golden say so (a difference from the C runtime).
GuilhermeBn198
force-pushed
the
port/property-before-abort
branch
from
October 22, 2026 05:00
ebe846a to
82f2014
Compare
GuilhermeBn198
changed the title
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
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.
Found while running Map2Check 9.0's integration regressions on the merged build (hbgit/Map2Check#78 + ports). Not a 9.0 port: a race of this runtime under KLEE that the 9.0 frontend exposes.
What
Under KLEE every state writes the same native
map2check_propertythrough external calls, and KLEE switches states between batches of instructions. Traced with strace: the violating state renamesTARGET-REACHEDinto place, then, while it formats its aux files and before its abort halts the search, a state that ended normally renames its ownNONEover it. The frontend readsNONE→ UNKNOWN on a reachable target. SD-20's temp-file + rename keeps the file whole, not the violation; rewriting the file right before the abort (first attempt) still loses the race.The other violations already have a file of their own (
_deref,_free,_assert,_overflow, ...), which no normally-ending state writes.TARGET-REACHEDnow has one too,map2check_property_target(same text). Map2Check reads it beforemap2check_property(hbgit/Map2Checkport/target-property-file). SD-20 and theTARGET-REACHEDgolden document the difference from the C runtime.Measured
9.0's integration section 13 (
--nondet-generator symex, with and without--slice): UNKNOWN with v1.1.0-rc1 and with #47-#53 (map2check_property=NONE); FAILED with this change and the frontend side, 3/3 (map2check_propertystillNONE,map2check_property_target=TARGET-REACHED).Tests
cargo test(both feature sets) and clippy pass; unit test and golden updated for the extra file.Stack: after #53; merge order #47 → #54, then the Map2Check side. Commits not signed yet (see #47).