ir: add syntactic support for vscale, vscale_range

[artagnon]

In an effort to support checking of programs with scalable vectors, add syntactic support for vscale and vscale_range, making the vscale an smt::expr in State. For the moment, we fail to type-check any program using scalable vectors.

[nunoplopes]

https://discourse.llvm.org/t/please-dont-use-undef-in-tests-part-2/83388

[lukel97]

Apologies for the drive by review, I'd love to see scalable vector support. Is it safe to assume vscale is 1 though? E.g would this mean that an insertelement into a <vscale x 1 x i64> at index 2 would now always be equivalent to poison?

I know very little about alive2 though so I may be completely misunderstanding this!

[artagnon]

Apologies for the drive by review, I'd love to see scalable vector support. Is it safe to assume vscale is 1 though? E.g would this mean that an insertelement into a <vscale x 1 x i64> at index 2 would now always be equivalent to poison?

True, but I'm not sure what else we can do when there is no information about what vscale could be: I was thinking this could be a minimum-first-patch, with the vscale_range function attribute support in a follow-up. vscale can only ever be a power of two, right? I think we have to solve for all powers of two in the vscale range, and report the minimally-refined solution.

[nunoplopes]

This patch needs some work. The type system needs to enumerate concrete vector sizes in, e.g., [min, min + 32]. Alive2 runs the verification for all possible typings.
VectorType::getTypeConstraints() needs to create constraints to make that happen.

Also, there are still a bunch of undefs in the test cases

[nunoplopes]

#923