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

Stack Assertions, kind of a hack #2

Closed
kevin-montrose opened this Issue Feb 13, 2013 · 1 comment

Comments

Projects
None yet
1 participant
@kevin-montrose
Copy link
Owner

kevin-montrose commented Feb 13, 2013

Ideally assertions would just be there for peace of mind, rather than actually being required in some cases.

This is solvable, but a lot of how types on the stack are tracked needs to be cleaned up and refactored.

10,000 foot view:

  • Stack state at every op needs to be available
  • When in an "unbased" (like after a Br) state, underflowing the stack should produce wildcards
  • When types pushed to the stack are technically "constrained"
    • When we're not "unbased" everything's constrained to a single type
    • When "unbased" things are constrained to some subset (possibly the wildcard)
  • When we loop back to an "unbased" point, we propagate constraints "forward" through the op stream
  • If at any point a type is constrained to the null set, the op at that state is unverifiable

Such a flow gives us exactly when (in the stream) a bad op happened, and let's us throw exactly when (in the emitting code) it became provable as such.

But yeah, lots of infrastructure to build and rebuild so this feels like a 1.3 or 2.0 (depending on how far reaching interfaces changes are) feature.

@ghost ghost assigned kevin-montrose Feb 13, 2013

@kevin-montrose

This comment has been minimized.

Copy link
Owner

kevin-montrose commented Feb 24, 2013

The new verifier added afteer 1.2.9 fixes this, stack assertions are no longer necessary.

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