Share PBT runtime reliability fixes with Calls - #413
Open
CaelmBleidd wants to merge 3 commits into
Open
CaelmBleidd wants to merge 3 commits into
CaelmBleidd wants to merge 3 commits into
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
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.
PBT contains several runtime fixes that also apply to Calls and the shared FastCheck backend. This PR extracts those fixes on top of #412 without importing PBT campaign/search protocols.
finitenumber tags against their actual IEEE-754 bits in Node and reuse one Kotlin validator for examples, manifests and decoding. NaN/infinity bits cannot bypass input checks with afinitetag.toJSONmethods. An analyzed predicate can no longer replace or break the response by changing an inherited serializer.ErrororTypeErrorusing the existing Calls runtime-type storage. Both new assertions failed withstringbefore this fix. Keep the Calls constructor/storage models and existing fallback for other object exceptions.The three commits separate protocol/numbers, process/coverage, and frontend/error integration. Review order: #391 → #410 → #394 → #409 → #412 → this PR.
Local validation with published JacoDB
86b07fc9fband JDK 21::usvm-ts-fast-check:check :usvm-ts-pbt:check: 196 Kotlin tests and 77 Node tests passed.git diff --checkpassed.main(53dce8f3, including [TS PBT] Align property execution semantics #386). The merge was conflict-free, and PBT/FastCheck checks plus Detekt passed: 207 Kotlin tests and 88 Node tests. That validation merge was then discarded; no merge commit was published.Remote CI for
b1c0c7df: https://github.com/UnitTestBot/usvm/actions/runs/36860002257 (running).Sources include PBT commits
3011a138,ee0ff619,de1298c3,a416726b,1895c251,8c29d1ff,48c5e169, and the narrow thrown-type part of3ad57381. Campaign deadlines/outcomes, generated-observation lifecycle, candidate reduction and unfinished feature work remain in PBT. No campaign, corpus or manuscript result is changed. JacoDB #366 remains a separate open catch-binding fix and is not in the current dependency pin.