Stream: git-wasmtime

Topic: wasmtime / issue #5686 ISLE: disallow non-partial express...

Wasmtime GitHub notifications bot (Feb 01 2023 at 20:41):

fitzgen opened issue #5686:

It's a footgun: they will always succeed (should be using if-let to match on the result of the value, not if on whether anything is matchable).

See #5684 where this bit us (me) in practice.

Wasmtime GitHub notifications bot (Feb 01 2023 at 20:41):

fitzgen labeled issue #5686:

It's a footgun: they will always succeed (should be using if-let to match on the result of the value, not if on whether anything is matchable).

See #5684 where this bit us (me) in practice.

Wasmtime GitHub notifications bot (Feb 01 2023 at 21:55):

jameysharp commented on issue #5686:

I thought this would be something I could hack together between meetings, but it's trickier than I thought.

First off, I believe we can't do this during parsing/AST construction. We don't necessarily know whether a term is partial at that point since we may not have parsed its declaration yet.

During semantic analysis, we've already rewritten (if foo) into (if-let _ foo), so we can't reject total terms only when they're inside an if construct. That's not a bad thing though, because really we shouldn't allow infallible if-let either.

An infallible if-let occurs if both the left-hand pattern and the right-hand expression are infallible/non-partial. That's not completely trivial to determine, in that we can't just check the top-level of either. We have to recurse through the whole subtree and reason about how, for example, and-patterns or let-binding expressions interact with match failures. Not a huge deal, but not "hack together between meetings" material.

There are some complicated cases. For one, (if-let x (...)) may be infallible, in which case it's almost equivalent to a let-binding expression. However that might be useful as the only way to let-bind an expression for use in multiple if-lets. And (if-let (extractor x) (...)) is the only way to call an extractor on an arbitrary expression, so even if the extractor is infallible this pattern could be necessary.

We could add a (let) construct for the left-hand side of a rule: functionally it would be identical to if-let but would suppress this infallible-if check and capture the rule-author's intent better.

I wondered if this would be any easier to check on the trie_again representation, after semantic analysis. This bug would show up as an unused binding-site. However, right now we generate unused binding sites in other ways that are harmless. Also, this is a property of a single rule, but we only build that representation on the combined set of all rules for a term, so determining where a binding site is "used" is non-trivial. So I think this is best done in semantic analysis.

Independent of this current issue, we should also consider checking for unused variable bindings, and checking that let-bindings only bind _ for impure expressions.

Last updated: Dec 23 2024 at 12:05 UTC