Skip to content

Add an XSD schema for SDF#430

Closed
vjackson725 wants to merge 4 commits intoseL4:mainfrom
vjackson725:xsd
Closed

Add an XSD schema for SDF#430
vjackson725 wants to merge 4 commits intoseL4:mainfrom
vjackson725:xsd

Conversation

@vjackson725
Copy link

I have updated @podhrmic's XSD to account for the changes in the SDF format since that pull request was made. This resolves pull request #77.

This should probably live somewhere else, and not in the root of the project; but I'm not sure where to put it.

Also, someone who's worked on the SDF Rust parser should look through this to make sure I didn't overlook something obvious. I wrote this out only with reference to @podhrmic's previous version and the SDF documentation.

podhrmic and others added 3 commits March 10, 2026 13:10
Signed-off-by: Michal Podhradsky <mpodhradsky@galois.com>
Signed-off-by: Vincent Jackson <v.jackson@unsw.edu.au>
Signed-off-by: Vincent Jackson <v.jackson@unsw.edu.au>
Signed-off-by: Vincent Jackson <v.jackson@unsw.edu.au>
@vjackson725
Copy link
Author

vjackson725 commented Mar 12, 2026

So, after investigating some more, it appears that XSD 1.0 is not sufficient to describe the SDF format with any specificity. In particular, it can't describe unordered collections of elements with bounds other than 0, 1, or unbounded. @podhrmic tried to get around this by nesting <choice> in a <sequence>:

<xs:sequence>
  ...
  <xs:choice minOccurs="0" maxOccurs="unbounded">
    <xs:element name="setvar">...</xs:element>
    <xs:element name="irq" minOccurs="0" maxOccurs="63">...</xs:element>
     ...
  </xs:choice>                               
  ...

which is sufficient when the numerosity constraint is on the number of children alone, without reference to the type of element. But it does not have the correct semantics when particular elements types have a fixed bound, such as for irq.

There are very few open source parsers that support XSD 1.1, which is powerful enough to express such constraints. I am currently investigating RelaxNG, a different schema format, that xmllint also supports. It appears to have better support for unordered child elements.

But, for the time being, this schema should not be merged.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants