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

Initial implementation of resource type validation #192

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

Conversation

pl-semiotics
Copy link
Collaborator

@pl-semiotics pl-semiotics commented Apr 27, 2023

This adds a relatively direct OCaml implementation of the current formalisation (essentially that given in #101), focusing on the rules around how resource types are treated as creating quantified component types.

It is designed to layer cleanly around the Core WebAssembly reference interpreter, but presently requires minor changes to expose certain parsing-related information and entrypoints.

@pl-semiotics pl-semiotics requested a review from lukewagner April 27, 2023 07:29
@lukewagner
Copy link
Member

Sorry for the slow reply, but excited to check this out! Could you perhaps add a README.md to the interpreter/ directory giving step-by-step instructions (for Linux and MacOS, ideally) to go from "I've checked out this repo" to "I'm running the test suite"?

@lukewagner
Copy link
Member

One other thing that would be super-useful is to see if this reference interpreter can run the tests in wasm-tools/tests/local/component-model and wasmtime/tests/misc-testsuite/component-model. The error strings won't match of course, so we can start by ignoring error string equality. But once the reference interpreter agrees, we'll get a bunch of coverage from importing them into the reference test suite.

Copy link
Member

@lukewagner lukewagner left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Lots of great tests in there! Just a few nits and a question.

(type $t (resource (rep i32)))
(component
(alias outer $C $t (type))))
"Cannot export type containing bare resource type")
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Might be nice to distinguish this case in the error string (e.g. "Cannot outer alias resource types across components" or something)

Comment on lines +107 to +113
)

(component
(instance $deftype (instantiate $dt))
(instance (instantiate $use2c
(with "deftype" (instance $deftype))
(with "two" (component $use1)))))
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seems like this test is missing a final part that, e.g., requires one and two to have the same function type.

(component
(instance (instantiate $needs_dt2i_backwards
(with "deftype" (component $dt2)))))
"Type variable u0.0 is not u0.1")
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Perhaps also add an invalid testcase that tries to import one and two with the same resource type?

(instance $ii (instantiate $in))
(alias export $ii "t" (type $t))
(export "t" (type $t)))
"Component type may not refer to non-imported uvar")
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would think that the problem here was the lack of ascribed type, but if you did ascribe a (sub resource) type, it would be valid, and thus the error of "may not refer to non-imported uvar" doesn't make sense to me.

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