fix(schema): saturate effectively-unbounded content-model counters (#192, partial)
The counted content-model automaton represents its active set as (state, counter-vector) configurations bounded by states times the product of the per-counter saturation caps. An unbounded counter already saturates at its minimum (every higher count is matching-equivalent). A finite maximum the input cannot reach is equivalent: the active set increments a counter at most to its cap, the cap is at most inputLength+1, so when maximum > inputLength+1 the value can never reach maximum, belowMaximum is always satisfied, and every value at or above the minimum is indistinguishable. Saturate such a counter at its minimum too, so a huge but finite maxOccurs on a nested counter no longer multiplies the active set by an inputLength factor per nesting level. A document that did not terminate within a minute against the Z035 worst case (nested sequences/choices with maxOccurs up to 1e11) now validates in linear time. No accept/reject decision changes: the full XSTS suite holds at 0/35/0/26, and an adversarial no-caps reference-matcher differential found no false positive or false negative, including the nullable-body case (where the builder makes canExit unconditional, so the counter value is matching-irrelevant) and the occurrence boundary. Guarded by ContentMatcherWorstCaseTests. Partial: a model with several moderate (input-reachable) maxOccurs nested deeply still enumerates a large active set; the general polynomial bound (a position- indexed DP over the counting automaton) remains under #192.
This commit is contained in:
parent
7a126a9b0a
commit
fa3552876a
14
CHANGELOG.md
14
CHANGELOG.md
@ -38,6 +38,20 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
|
||||
|
||||
### Fixed
|
||||
|
||||
- The content-model matcher no longer blows up on a nested model group with a huge but
|
||||
finite `maxOccurs` (#192, partial). The counted-automaton active set is bounded by the
|
||||
product of the per-counter saturation caps; a finite `maximum` the input cannot reach
|
||||
(`maximum > inputLength + 1`) is now saturated at its minimum, exactly as an unbounded
|
||||
counter is, because the value can never reach that maximum under any continuation (the
|
||||
cap is at most `inputLength + 1`), so `belowMaximum` always holds and every value at or
|
||||
above the minimum is matching-equivalent. A document that did not terminate within a
|
||||
minute against such a model (the Z035 worst case) now validates in linear time, with no
|
||||
change to any accept/reject decision (full XSTS suite still 0/35/0/26; an adversarial
|
||||
no-caps reference-matcher differential confirms no verdict changed, including nullable
|
||||
bodies and the occurrence boundary). Guarded by `ContentMatcherWorstCaseTests`. A model
|
||||
with several *moderate* (input-reachable) `maxOccurs` nested deeply still enumerates a
|
||||
large active set and is tracked under #192.
|
||||
|
||||
- A reference to a model group whose content is an `all` group must have `maxOccurs`
|
||||
of 1 and `minOccurs` of 0 or 1 (XSD 1.0 cos-all-limited, #158). A `<group ref>` that
|
||||
resolves to an `<xs:all>` group with `maxOccurs="2"` is now rejected (corpus
|
||||
|
||||
@ -245,19 +245,32 @@ extension PureXML.Schema {
|
||||
|
||||
/// The per-counter saturation point for the active-set representation.
|
||||
///
|
||||
/// An occurrence counter only needs distinct values up to what its own
|
||||
/// bound and the available input make observable. A bounded counter
|
||||
/// saturates at `min(maximum, inputLength + 1)`. An unbounded counter
|
||||
/// saturates at its `minimum`: once the minimum is reached every higher
|
||||
/// count is matching-equivalent (`canExit` stays satisfied and
|
||||
/// `belowMaximum` is vacuous), so collapsing them is exact. Clamping each
|
||||
/// counter independently bounds the active-configuration set by the content
|
||||
/// model instead of by `inputLength` raised to the counter count, so a long
|
||||
/// run of one repeated element no longer makes the closure blow up.
|
||||
/// An occurrence counter only needs distinct values up to what its own bound
|
||||
/// and the available input make observable. An unbounded counter saturates at
|
||||
/// its `minimum`: once the minimum is reached every higher count is
|
||||
/// matching-equivalent (`canExit` stays satisfied and `belowMaximum` is
|
||||
/// vacuous), so collapsing them is exact.
|
||||
///
|
||||
/// A finite `maximum` the input cannot reach is matching-equivalent to
|
||||
/// unbounded and saturates the same way. The active set increments a counter
|
||||
/// at most to its cap, and the cap is at most `inputLength + 1`; so when
|
||||
/// `maximum > inputLength + 1` the value can never reach `maximum` under any
|
||||
/// continuation, `belowMaximum` is always satisfied, and every value `>= min`
|
||||
/// is indistinguishable. Saturating such a counter at its minimum (rather than
|
||||
/// at `min(maximum, inputLength + 1)`) is therefore exact, and it keeps a huge
|
||||
/// but finite `maxOccurs` on a nested counter from multiplying the
|
||||
/// active-configuration set by an `inputLength` factor per nesting level (the
|
||||
/// Z035 worst case). Only a `maximum` the input can actually reach
|
||||
/// (`<= inputLength + 1`) still needs its values tracked up to that maximum.
|
||||
private func counterCaps(for inputLength: Int) -> [Int] {
|
||||
let reachable = inputLength == Int.max ? Int.max : inputLength + 1
|
||||
return counters.map { scope in
|
||||
scope.range.maximum.clamped(to: reachable) ?? scope.range.minimum.clamped(to: reachable)
|
||||
guard let maximumCap = scope.range.maximum.clamped(to: reachable),
|
||||
!scope.range.maximum.isGreaterThan(reachable)
|
||||
else {
|
||||
return scope.range.minimum.clamped(to: reachable)
|
||||
}
|
||||
return maximumCap
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
41
Tests/ContentMatcherWorstCaseTests.swift
Normal file
41
Tests/ContentMatcherWorstCaseTests.swift
Normal file
@ -0,0 +1,41 @@
|
||||
import Testing
|
||||
@testable import PureXML
|
||||
|
||||
/// #192 worst-case guard. A content model with nested huge-`maxOccurs` counters (the
|
||||
/// Z035-class adversarial shape) must validate a large document in bounded work, not
|
||||
/// blow up the active-configuration set. Before effectively-unbounded finite counters
|
||||
/// were saturated at their minimum, an 800-child document against this model did not
|
||||
/// terminate within a minute (the active set grew like `inputLength` raised to the
|
||||
/// nesting depth); it is now linear. The time limit turns a regression back to the
|
||||
/// super-linear blowup into a test failure rather than a silent interactive hang.
|
||||
///
|
||||
/// This covers the huge-`maxOccurs` case (a maximum the input cannot reach). A model
|
||||
/// with several MODERATE `maxOccurs` (reachable by the document) nested deeply is not
|
||||
/// yet bounded to a small constant and remains tracked in #192.
|
||||
@Suite("XSD content-matcher worst case (#192)")
|
||||
struct ContentMatcherWorstCaseTests {
|
||||
private let hugeMaxOccursModel = """
|
||||
<xs:schema xmlns:xs="http://www.w3.org/2001/XMLSchema">
|
||||
<xs:element name="root"><xs:complexType>
|
||||
<xs:sequence maxOccurs="100000"><xs:sequence maxOccurs="100000">
|
||||
<xs:choice maxOccurs="100000"><xs:element name="a" type="xs:string" maxOccurs="100000"/></xs:choice>
|
||||
</xs:sequence></xs:sequence>
|
||||
</xs:complexType></xs:element>
|
||||
</xs:schema>
|
||||
"""
|
||||
|
||||
#if os(WASI)
|
||||
@Test("a huge-maxOccurs nested content model validates a large document in bounded work")
|
||||
#else
|
||||
@Test("a huge-maxOccurs nested content model validates a large document in bounded work", .timeLimit(.minutes(1)))
|
||||
#endif
|
||||
func test_hugeMaxOccursBounded() throws {
|
||||
let document = try PureXML.Schema.Document(hugeMaxOccursModel)
|
||||
let valid = "<root>" + String(repeating: "<a>x</a>", count: 10000) + "</root>"
|
||||
#expect(try document.validate(valid).isEmpty)
|
||||
// A child the model does not admit is still correctly rejected (the saturation
|
||||
// does not widen what is accepted), and that decision is also bounded.
|
||||
let invalid = "<root>" + String(repeating: "<a>x</a>", count: 5000) + "<b/></root>"
|
||||
#expect(try !document.validate(invalid).isEmpty)
|
||||
}
|
||||
}
|
||||
Loading…
Reference in New Issue
Block a user