"Unified" Type Inference

[mmcloughlin]

I had been working towards a refactor of type inference, but realized the impact would be pervasive and might take too long. Thanks to #90 we now have a workaround so I will pause work on it, but I just wanted to make a note of what the eventual goal might look like.

The problem at the moment is that type inference is split into two phases. The first Rust-based type inference works most of the time, but sometimes cannot deduce all bitvector widths. In this case the solver has to run in a "dynamic widths" mode first. This means that type inference logic is split into two places, and it also complicates the solver. Some of this complexity is inherent in the problem, but it might be cleaner to structure the code differently.

I think the goal would be three phases:

1. Rule Semantics Construction. This would take the AST forms from ISLE and the annotation language and construct RuleSemantics object with veri_ir::Expr types. The logic to do this essentially exists already in type_inference.rs bit it might be cleaner if it's not mixed with type inference logic at the same time. We think it might be possible to entirely remove the annotation_ir layer. This stage might also do "basic type inference" at which we determine whether each expression is integer/boolean/bitvector but not the bitvector width.
2. Type Inference. This stage would be a merging of the existing Rust inference pass and the dynamic widths mode of the solver. We expect it would be simpler to rely on SMT entirely. This pass would be expected to completely resolve types. There's an open question about how best to handle rules that have multiple possible type instantiations. At the moment that's handled with a loop in the solver, but we have discussed that it may be better to insist that type inference has a unique solution and require prior phases to provide enough constraints that this is true (for example type instantiations for intermediate terms).
3. Solver. This would be the same code we have now, but stripped down to only the static mode. The dynamic widths logic would be ported into the separate type inference phase.

---

In case it ends up being useful, I have experimental code that re-implements the solve_constraints Rust part of type inference with an SMT approach.

wasmtime/cranelift/isle/veri/veri_engine/src/type_inference.rs

Line 2034 in 46a7d66

struct TypeSolver {

Commit 46a7d66 is the best place to start from.