Verify most of the mid-end#105
Conversation
| // Rebuild the equality sets with the reindex applied, so that the | ||
| // deleted `target` binding is replaced by `replace`. Without this, a | ||
| // deleted binding can linger in the disjoint set (possibly as a set | ||
| // representative), and `equalities()` would later return a reference to | ||
| // a binding that no longer exists. |
There was a problem hiding this comment.
Are there potentially any lingering bugs in the existing verification due to this?
There was a problem hiding this comment.
No observable change in the veri results on other targets, so not that I know of.
| // other compilation units; skip those rather than erroring. | ||
| let Some(term_id) = termenv.get_term_by_name(tyenv, &spec.term) else { | ||
| log::debug!( | ||
| "skipping spec for term {name} not declared in this compilation", |
There was a problem hiding this comment.
I tend to be nervous about silencing warnings like this. The existing warning serves as a good linter, and without it we could end up with stale specs/attrs for terms that have been deleted or renamed.
Is this unavoidable, or could we fix it by rearranging the specs/attrs into a different set of shared files?
| (spec (simplify arg) | ||
| (provide | ||
| (if relax_nan | ||
| (fp_equiv! result arg) | ||
| (= result arg)))) |
There was a problem hiding this comment.
I'm a bit torn here. On one hand this is much simpler than other ways I could think of making this change. On the other hand, I wonder if this sets up a potential future footgun: is it possible that a float-to-int conversion in a rule could end up with relax_nan true causing a fp_equiv! on integer values? If so, is there a way we could prevent that in future?
There was a problem hiding this comment.
Discussed in meeting, adding comment but keeping for now
| Binding::Iterator { source } => { | ||
| // The yielded element has the source term's element type, which we | ||
| // model as its (single) return type. | ||
| let source_binding = lookup_binding(*source); | ||
| binding_type(&source_binding, term_id, prog, lookup_binding) | ||
| } |
There was a problem hiding this comment.
What is the mental model here? We are verifying properties that would hold of any return from a multi term, but not attempting to verify how many returns it has?
There was a problem hiding this comment.
Correct. The one mid-end term that yields an iterator as a multi-term is truthy, which could e.g. match on ineg x and bmask y in the same e-class and trigger a rule firing on both. The correctness condition is for the rewrite to be sound for any return, not the number of returns.
There was a problem hiding this comment.
I'll need more time to look through this, but my first thought is whether some of the helper macros in here belong in the shared spec macros rather than opt.isle.
2 participants
No description provided.