Monica Pardeshi (Jun 22 2022 at 03:22): Monica Pardeshi (Jun 22 2022 at 03:22):What are the semantics of uextend? How does ISLE know how much to extend the input value?
On a related note, we're currently trying to verify uextend and are having trouble because we don't know the size of Inst. Is there a way to enforce a bit width on Inst for some terms? Does it even make sense to think about Inst having a size?
fitzgen (he/him) (Jun 22 2022 at 17:58):How does ISLE know how much to extend the input value?
The bit width of the result value and of the input value should determine the extend that is happening. For example, see the usage of the has_type and value_type extractors here: https://github.com/bytecodealliance/wasmtime/blob/25a588c35f52a7005d7f455facc15e9e35273497/cranelift/codegen/src/isa/x64/lower.isle#L2150-L2152
Does it even make sense to think about
Insthaving a size?
Not really. Instead it makes sense to talk about the size of values, and an Inst can produce zero or more values, each of which have an associated size.
Monica Pardeshi (Jun 23 2022 at 04:06):How does ISLE know how much to extend the input value?
for a rule like
(rule (lower (has_type (fits_in_64 out) (uextend x @ (value_type in))))
(extend x $false (ty_bits in) (ty_bits out)))
are we saying that in could have any width, and we extend it to 8, 16, 32, or 64 bytes?
Does it even make sense to think about Inst having a size?
Ah, yes, that makes more sense. So for certain instructions we should think about constraining the size of Value?
fitzgen (he/him) (Jun 24 2022 at 15:58):are we saying that in could have any width, and we extend it to 8, 16, 32, or 64 bytes?
pretty much, although there is a little more in the extend term and also just what is implicitly valid or not for CLIF (dest must be wider than source; checked when the clif validator is enabled)
fitzgen (he/him) (Jun 24 2022 at 15:58):So for certain instructions we should think about constraining the size of Value?
Yes, that sounds right.
Monica Pardeshi (Jul 04 2022 at 03:50):We're having some trouble mapping isle types to our internal ir types. Specifically, we want Value to be constrained in different ways depending on which rule it's being used in (in the below example we want Value to be a bv64).
(decl extend (Reg bool u8 u8) Reg)
(rule (extend rn signed from_bits to_bits)
(let ((dst WritableReg (temp_writable_reg $I64))
(_ Unit (emit (MInst.Extend dst rn signed from_bits to_bits))))
dst))
(rule (lower (has_type (fits_in_64 out) (uextend x @ (value_type in))))
(extend x $false (ty_bits in) (ty_bits out)))
In other rules, we don't necessarily want this constraint. Do you have any advice on how to map the same type name to different ir types?
Monica Pardeshi (Jul 04 2022 at 04:05):Does isle type-checking have any way to differentiate Value in different rules? How does it distinguish a Value that represents a u8 from one that represents a u64?
Chris Fallin (Jul 04 2022 at 04:54):hi @Monica Pardeshi -- the short answer is that in ISLE those cases aren't different types; there's an abstraction-levels sort of issue going on here, where the type at the "compiler implementation" abstraction level is Value (an SSA value) but the type at the "IR value" level is u8 or u64. (In other words, type of compiler SSA identifier vs. type of value it identifies.)
If we want to encode u8 vs u64 somehow, that gets into dependent-type territory; but I would question: do we really need it?
In my mind the approach y'all have been aiming for has always been: map Values to a bitvector big enough for the biggest value; then make assertions about its bits. A u8 is stored in the low 8 bits, so we only have assertions about the low 8 bits; the upper bits are undef / "don't-cares". One could think of this sort of like having an abstract machine model where Value gets stored in a "register" of some width. Does that make sense? Or is there some reason the SMT-solver-level bitvector width has to be narrower?
Last updated: Nov 22 2024 at 16:03 UTC