Fix type inference for enum variants#73
Conversation
mmcloughlin
force-pushed
the
mbm/fix-type-inference-enum-variant
branch
from
bf06d1f to
53ef6f5
Compare
|
Please advise on how to test this PR. |
mmcloughlin
force-pushed
the
mbm/fix-type-inference-enum-variant
branch
from
53ef6f5 to
4443cad
Compare
| /// Lookup term by name. | ||
| pub fn get_term_by_name(&self, tyenv: &TypeEnv, sym: &ast::Ident) -> Option<TermId> { |
There was a problem hiding this comment.
Had to make this public.
Is the intention that some of the verify code would be moved inside this package in future?
There was a problem hiding this comment.
Likely not in the short term, no.
avanhatt
left a comment
avanhatt
left a comment
There was a problem hiding this comment.
Looks good, thanks! Some non-blocking comments inline
| /// Lookup term by name. | ||
| pub fn get_term_by_name(&self, tyenv: &TypeEnv, sym: &ast::Ident) -> Option<TermId> { |
There was a problem hiding this comment.
Likely not in the short term, no.
| #[derive(Clone, Debug)] | ||
| pub struct AnnotationEnv { | ||
| pub annotation_map: HashMap<String, TermAnnotation>, | ||
| pub annotation_map: HashMap<TermId, TermAnnotation>, |
| pub fn spec_to_annotation_bound_var(i: &Ident) -> BoundVar { | ||
| BoundVar { | ||
| name: string_from_ident(env, i), | ||
| name: i.0.clone(), |
|
|
||
| if unresolved_widths.contains(&width_name) { | ||
| // println!("\tResolved width: {}, {}", width_name, width_int); | ||
| println!("\tResolved width: {}, {}", width_name, width_int); |
There was a problem hiding this comment.
For a later change: I (or we, if you get there first) should probably add a --verbose flag so we can toggle these more easily.
There was a problem hiding this comment.
I think we should be using the debug and trace logging macros?
wasmtime/cranelift/codegen/src/opts.rs
Line 66 in bcb8308
|
|
||
| // Print term for debugging | ||
| print!(" {}", t); | ||
| print!(" {}", term_name); |
There was a problem hiding this comment.
We probably don't want this on by default long term, but fine for now.
The integration rule tests exercise this code (including for specific types), so we have some assurance that this doesn't break everything. But feel free to add more unit tests as you go, too. |
Yes, I did rerun the test suite on this PR too. It would be nice to add type-inference specific tests. Perhaps I'll look into that. |
Updates some of the "broken" test cases to ensure they have full enum types.
These were failing with errors such as:
```
---- test_broken_iadd_shift2 stdout ----
Verifying iadd rules in file: ./examples/broken/iadd/broken_shift2.isle
thread '<unnamed>' panicked at 'called `Option::unwrap()` on a `None` value', cranelift/isle/veri/veri_engine/src/annotations.rs:322:85
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
thread 'test_broken_iadd_shift2' panicked at 'called `Result::unwrap()` on an `Err` value: Error { error: "Test thread panicked Any { .. }", total_delay: 0ns, tries: 1 }', cranelift/isle/veri/veri_engine/tests/utils/mod.rs:109:12
```
Following the change in #73, we now error if an enum model does not have a corresponding type declaration. This PR fixes the problem by adding full enum type declarations alongside the models.
Generates the remaining opcodes for `AluRRRR`. Updates #35
2 participants
This PR proposes a fix for the type inference problem that was preventing verification of the Amode lowering with the expression
(Amode.ImmRegRegShift offset x y 0 flags).wasmtime/cranelift/codegen/src/isa/x64/inst.isle
Lines 1130 to 1131 in 6e0a601
The specific problem was a failure to deduce the type for the shift argument (set to the constant 0). I believe the root cause was with
add_isle_constraintswhich was only considering declarations, not enum variants. I saw that the Sema layer in ISLE handles this already, so both declarations and enum variants are merged in the TermEnv. Therefore this PR changesadd_isle_constraintsto operate on Sema Terms rather than AST Decls. This has the (I think) nice side effect that type inference no longer uses any AST types. That also meant that the change had a bit of a larger blast radius, with various function signatures changing etc.