fix: three Mythos-discovered bugs (parser + range lowering)#132
Merged
Conversation
Regression from PR #130. When property_expression was split into an outer binary-op wrapper + an inner _primary for #127, the PLUS/MINUS arm in the primary kept recursing into the outer wrapper. The outer's binary-op loop then greedily consumed the following `+`/`-`/`*` operators into the signed operand — so `-1 + 2` parsed as `-(1+2)` instead of `(-1)+2`, silently inverting the sign of every additive tail downstream. AS-5506B §11.2.5 defines `numeric_term ::= [sign] numeric_literal` — the sign is atomic with the literal, not a prefix over the additive expression. Fix: one-line change at properties.rs:251, recurse into `property_expression_primary` in the signed-numeric arm. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
AS-5506B §4.5 (component_type) and §5.1 (component_implementation)
grammar uses `?` on each section clause — `features`, `modes`,
`properties`, `subcomponents`, `connections`, `prototypes`, `calls`,
`flows`, `internal features`, `processor features`. Before this fix the
`loop { match }` section dispatcher had no seen-tracking, so a
component with two `features` blocks parsed cleanly. Lowering then
silently dropped the duplicate because `item_tree/lower.rs` walks the
CST with `.find(|c| c.kind() == FEATURE_SECTION)` — first match wins —
so a reviewer who saw ports in both sections ended up with ONLY the
first set in the instance model.
Adds a `SeenSections` guard consulted before each arm. On a repeat we
emit `p.error("duplicate `<label>` section")` and still consume the
section so the parser recovers cleanly. Annex subclauses are
intentionally exempt — real models routinely stack EMV2 and Behavior
Annex on the same component.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…ent 0 `lower_range_from_tokens` had `parse_aadl_integer(&num_text).unwrap_or(0) * min_sign`. On a literal larger than i64::MAX, `parse_aadl_integer` returns None, `unwrap_or(0)` substitutes 0, and the RANGE_VALUE was lowered as `Integer(0, _)` with zero diagnostic. Downstream analyses (scheduling, latency, resource budgets) would then consume a forged bound of `0` in place of the author's actual literal — a silent HIR drift. Replace with `and_then(.checked_mul).unwrap_or(Opaque(<original-text>))` so overflow falls back to preserving the original literal as Opaque text, letting property-typed analyses detect the overflow rather than silently using a fake value. The sibling helper at line 1688 already used `?` — this site was the outlier. Maps to hazard H-5 (HIR drift); UCA-4 (Lowering assigns wrong property value). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Codecov Report❌ Patch coverage is
📢 Thoughts on this report? Let us know! |
`thin-vec 0.2.14` has a Use-After-Free / Double Free in `IntoIter::drop` and `ThinVec::clear` when an element's Drop panics, reachable from safe Rust (confirmed via Miri / AddressSanitizer per the RustSec advisory). 0.2.16 ships the fix; bumping via `cargo update -p thin-vec` is a patch-level bump through salsa's indirect dependency. Unblocks `Cargo Deny` + `Security Audit (RustSec)` CI checks. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Match the Cargo.lock bump in the previous commit. cargo-vet was failing Supply Chain because the exemption still pointed at the pre-RUSTSEC-2026-0103 version.
avrabe
added a commit
that referenced
this pull request
Apr 22, 2026
* docs: Mythos-style bug-hunt pipeline + spar ranking Ships the four-prompt bug-hunt pipeline modeled on Anthropic's Claude Mythos (red.anthropic.com, April 2026) adapted for spar. The architecture: let an agent reason freely about code but require a machine-checkable oracle (Kani harness + PoC test) for every reported bug so hallucinations don't ship. Contents: - HOWTO.md — pipeline overview, prerequisites, worked example - rank.md — tier-1-through-5 rubric specific to spar's pipeline (parser/syntax/hir-def/annex = tier 5; analysis/solver = tier 4; …) - discover.md — Mythos-verbatim discovery prompt + spar context + AADL-specific hypothesis priors (parser edge cases, HIR drift, proof-code drift from the 180 Kani harnesses) - validate.md — fresh-session validator enforcing both oracle halves - emit.md — converts a confirmed finding into a draft STPA artifact entry under safety/stpa/*.yaml - rank.json — ranking of 144 spar source files produced by running rank.md (tier 5: 43 files; tier 4: 51; tier 3: 35; tier 2: 14; tier 1: 1). Kept as evidence the pipeline works end-to-end. First parallel run on the top-5 tier-5 files surfaced three shipped bugs (fixed in PR #132) and two confirmed-but-no-uca findings that were filtered by validation. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * chore(deps): bump thin-vec to 0.2.16 to clear RUSTSEC-2026-0103 Same patch as fix/mythos-batch-1 — `thin-vec 0.2.14` has a UAF/Double Free in `IntoIter::drop` reachable from safe Rust (RustSec 2026-0103), 0.2.16 ships the fix. Indirect through salsa. Unblocks `Cargo Deny` + `Security Audit (RustSec)` CI checks on this branch too. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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.
Summary
Three correctness bugs surfaced by the first Mythos discover pass (
scripts/mythos/) on tier-5 files, all with both Kani-harness and PoC-test oracles, validated by fresh-session Mythos validators.Fixes
1. Unary sign regression from PR #130 (
parser/grammar/properties.rs:251)When
property_expressionwas split into an outer binary-op wrapper + inner_primaryfor issue #127, thePLUS/MINUSarm in the primary kept recursing into the outer wrapper. The outer's binary-op loop then greedily consumed the following+/-/*operators into the signed operand, so-1 + 2parsed as-(1+2)instead of(-1)+2— silently inverting the sign of every additive tail. AS-5506B §11.2.5:numeric_term ::= [sign] numeric_literal— the sign is atomic with the literal.Fix: one-line change to recurse into
property_expression_primaryin the PLUS/MINUS arm.2. Duplicate component sections silently accepted (
parser/grammar/components.rs)component_type_sectionsandcomponent_impl_sectionsusedloop { match }with no seen-tracking. AS-5506B §4.5 / §5.1 grammar uses?(zero-or-one) on each clause —features,modes,properties,subcomponents,connections,prototypes,calls,flows. Worse, lowering used.find(|c| c.kind() == FEATURE_SECTION)(first match only), silently dropping the duplicate section — so a reviewer who saw twofeaturesblocks ended up with only the first set in the instance model.Fix: adds a
SeenSectionsguard consulted before each arm. On repeat, emitsp.error("duplicate <label> section")and still consumes the section so the parser recovers. Annex subclauses are intentionally exempt (EMV2 + BA commonly co-exist on one component).3. Overflowing range-min silently lowers to 0 (
hir-def/item_tree/lower.rs:1989)lower_range_from_tokenshadparse_aadl_integer(&num_text).unwrap_or(0) * min_sign. On a literal larger than i64::MAX,parse_aadl_integerreturns None,unwrap_or(0)substitutes 0, and the range was lowered asInteger(0, _)— a forged bound consumed by scheduling / latency / resource-budget analyses. The sibling helper at line 1688 already used?.Fix:
and_then(.checked_mul).unwrap_or(Opaque(<original-text>))— overflow falls back to preserving the original literal, letting property-typed analyses detect overflow rather than consume a fake value.Hazards mitigated
Test plan
cargo test --workspace→ 2,464 passed, 0 failedrustup run nightly cargo clippy --workspace --all-targets -- -D warnings→ cleanrustup run nightly cargo fmt --check→ cleancrates/spar-syntax/tests/parser_tests.rs—unary_sign_binds_to_literal_only_not_to_additive_tail,test_data_property_value_signed_arithmetic, 3×duplicate_*_section_is_rejected,multiple_annex_subclauses_are_allowedtest-data/parser/property_value_signed_arithmetic.aadl— leading-sign arithmetic fixturecrates/spar-hir-def/src/item_tree/lower.rs—range_lowering_tests::overflowing_range_min_does_not_silently_become_zero,range_lowering_tests::in_range_positive_min_lowers_correctlyNot in this PR
Two findings from the same pass were validated as
confirmed-but-no-ucaand are deferred:applies to fwunresolved — spar's parser doesn't yet accept[n]selectors, so this is a missing-feature gap, not a resolver bug.PropertyMap::get()returning.first()vs+=>append — AS-5506B §11.3 makes+=>append (not override), cited call-sites read scalars, and the corpus uses+=>in one file. The real defect is a misleading docstring, not unsoundness. Doc-only fix will be separate.🤖 Generated with Claude Code