Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Added XSD and a validation script #77

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Conversation

podhrmic
Copy link

Partially resolves #70

TL;DR; I added an XSD schema for validating the system XMLs. You are currently using numbers with underscores, such as period="100_000" which is not a valid XML number. I parse these as strings, which is fine as long as you trust your build tool to resolve these correctly.

The long story
I asked ChatGPT to generate XSD schema from the few Microkit examples that are out there, and it did pretty well. I manually edited the XSD in a few places, and it certainly can be improved further, but IMHO it is good enough as it is. I recommend validating all .system files in a CI.

Signed-off-by: Michal Podhradsky <mpodhradsky@galois.com>
@Ivan-Velickovic
Copy link
Collaborator

Thanks for doing this @podhrmic. I'm not familiar with XSD, do you know if there's more sanitisation we can do, such as a minimum and maximum value for the period/budget for example?

For #70 I was hoping for some kind of specification that would be the input for the Microkit tool as well as any other tools that generate or consume the system description. One thing to consider is that with this XSD file, there is a possibility for the tool to be out-of-sync with the XSD or vice-versa. Something to look into would be whether we can consume the XSD file in Microkit to avoid that, or do you know of anything else in the XML space that would achieve this?

@Ivan-Velickovic
Copy link
Collaborator

And sorry for taking so long to review the PR.

@podhrmic
Copy link
Author

No worries, I figured you were busy!

You can certainly set min/max for any integer attribute, similar to what I have done for the priority values here. It just requires the budget etc. to be treated as integers, not strings (see my initial comment).

You can certainly generate datatypes from XSD, (xmlschema, xsdata, xml-schema, xgen, ... ). Perhaps a good start is to explicitly write the requirements for the .system format, implement them in XSD and then use the XSD to generate code for Microkit tools.

If this is interesting to you, I can look into it further!

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.

Syntax/Semantics for the system manifest
2 participants