[RFC] Typing of ite

[cdonovick]

Currently the typing of ite is a mess and inconsistent with magma.
Now before you all go looking at the mess I want you all to consider the following code snippets and tell me which of the following should be allowable syntax (otherwise you will never understand why ite is such a mess).

Assume the following for all snippets:

BV = BitVector

class SBV(BV): pass
class TBV(BV): pass
class WrappedInt:
    def __init__(self, i):
        self.i = i
    
    def __int__(self):
        return self.i
        
bv1 = BV[8](4) # values here don't really matter
bv2 = BV[8](5)
sbv = SBV[8](4) 
tbv = TBV[8](4)
wi = WrappedInt(4)
b = Bit(0) # again the value here is arbitrary 

Also keep in mind the following property:

res = bv1 & 4
assert isinstance(res, BV[8])
assert res == BV[8](4) == 4

res = bv1 & sbv # Note: sbv & tbv is an error
assert isinstance(res, BV[8])
assert res == BV[8](4) == 4

res = bv1 & wi
assert isinstance(res, BV[8])
assert res == BV[8](4) == 4 

# The preceding may surprise you but would it make sense for it
# to fail and the following to succeed?

res = bv1 & (0 + wi)
res = bv1 & BV[8](wi)

Okay on to the code snippets

b.ite(bv1, 0)                 # 1
b.ite(bv1, wi)                # 2 (Note I consider this to be the same case as 1)
b.ite(bv1, sbv)               # 3

b.ite((bv1, sbv), (bv1, sbv)) # 4
b.ite((bv1, sbv), (sbv, sbv)) # 5

# 6
@ssa # this could be ast_tools or magma combinational
def foo(cond: Bit) -> (BV, BV):
    if cond:
        return bv1, bv2
    else:
        return bv2, bv1        
# 7
@ssa
def bar(cond: Bit) -> (BV, BV):
    if cond:
        r_val = bv1, bv2
    else:
        return bv2, bv1
    return r_val
   
# 8
@ssa
def foobar(cond: Bit) -> (BV, BV):
    if cond:
        r_val = bv1, bv2
    else:
        r_val = bv2, bv1
    return r_val

Currently, hwtypes with ast_tools rewrites* accepts all of these (if it doesn't there is a bug).

It would not be hard to convince me to drop 1 and 2, they are coercions. While it is consistent with other methods to coerce I am fine not coercing in ite and continuing to coerce in other methods (I would rather have no coercion at all)

I feel very strongly that 3 is correct sbv is a BV[8] so there is no reason it shouldn't work

4 and 5 are (partly) the cause of current mess but I feel strongly that if 4 is valid and 3 is valid then logically so must be 5.

Finally, the last 3 cases are the reason why hwtypes accepts tuples. Currently magma combinational will work with 6 and 7 but not 8. This is because magma is quite clever about unpacking return values before it muxes (by using the returns annotation to determine if a return value is a tuple), it however cannot support the arbitrary muxing of tuples which is why 8 does not work. Hence to support 8 we must support 4**.

I find allowing 6 and 7 but not 8 to be pretty unintuitive and hence undesirable.

Now these requirements leads to the really messy typing rules for ITE. See:
https://github.com/leonardt/hwtypes/blob/master/hwtypes/bit_vector.py#L82
https://github.com/leonardt/hwtypes/blob/master/hwtypes/smt_bit_vector.py#L137
https://github.com/leonardt/hwtypes/blob/master/hwtypes/bit_vector_util.py

*

@end_rewrite()
@if_to_phi(Bit.ite)
@bool_to_bit()
@ssa()
@begin_rewrite()

**
I tried to come up with an ast transformation that could robustly perform the necessary unpacking of tuples. However, all the solutions I came up with either required type annotations on ALL assignments (r_val: (BV, BV) = ...) or a static type inference engine (which would give us those annotations). Note as we a have dependent type system we cannot easily hack mypy (or any other static type checking tool that I am aware of) to generate annotations for us.

[leonardt]

I think allowing 8 seems reasonable from a purely user facing perspective, it looks like natural code to write.

From what I understand, the reason 6 and 7 work are an artifact of how magma handles muxing return values (on the individual components, rather than muxing the tuple itself).

Supporting 8 would simply require magma to support muxing Python tuples, which itself doesn't seem to be the issue (this should be straightforward to add). I think the issue you're raising is the the typing rules are pretty unwieldy (specifically this: https://github.com/leonardt/hwtypes/blob/master/hwtypes/bit_vector_util.py#L12-L58)

I think having the user annotate the tuple type (i.e. r_val: (BV, BV) = ...), would be essentially the same as asking them to use a Tuple instead of a native Python tuple (e.g. r_val = Tuple[BV, BV](...)) which would be another option, but possibly worse because it's more verbose and unnatural.

I'll ponder this some more, but I can't think of anything useful off the top of my head. Perhaps we can abstract the type coercion logic into the types themselves? Given two sides of ite, would determining the resulting logic be the same as the result of a binary operator? If so, could we just abstract that into a reusable function that resolves the type given to two compatible types? Not sure if that really helps, because that's essentially just the same code that's been written.

[cdonovick]

Supporting 8 would simply require magma to support muxing Python tuples, which itself doesn't seem to be the issue (this should be straightforward to add). I think the issue you're raising is the the typing rules are pretty unwieldy (specifically this: https://github.com/leonardt/hwtypes/blob/master/hwtypes/bit_vector_util.py#L12-L58)

You are correct.

Given two sides of ite, would determining the resulting logic be the same as the result of a binary operator?

No, even ignoring the tuple case we still have the problem that ite is different from all other operators because of an issue I didn't even raise. No only does it mux BitVector (and tuples of BitVector) it also supports Bit. So the coercion logic is recursively do the following: coerce it like its a binary bit operator. If that fails coerce it like its a binary bit vector operator.

[phanrahan]

I vote for allowing muxing any magma type including tuples.

I also vote for requiring the two types in the then and else clauses to be the same. That is, no coercion. Particular, no coercion of fields in a tuple. I also think all the if-then-else statement blocks should be consistent with ite.

My queasiness for coercion is due to value preservation. If the types were a lattice, then parent types can hold all the values possible in the value types. And the semantics of the types would be the same.

When you have a class hierarchy, you may not preserve values. Although uint is-a bitvector, uint has different semantics than bitvector.

This leads to unpredicable behavior, for example bv & uint is a bv,. But what is bv + uint. If it is a bv, that seems weird because + is only technically defined on integers. And if it returned an uint because + is an operator on uint, then we need to convert bv to uint which seems dangerous.

I am ok with coercing an integer constant to a type in our language. That seems more like type inference to me. But I was always happy to do it explicitly; we just got lots of complaints about that.

I hope I understood the nuances here. Maybe we should talk in person.

[cdonovick]

I vote for allowing muxing any magma type including tuples.

Do you mean including python tuples? Just need to disambiguate that term.

My queasiness for coercion is due to value preservation. If the types were a lattice, then parent types can hold all the values possible in the value types. And the semantics of the types would be the same.

I am ok with coercing an integer constant to a type in our language. That seems more like type inference to me. But I was always happy to do it explicitly; we just got lots of complaints about that.

I would prefer to have no coercion as well but have been told that people complain if they are not allowed to write: bv + 1

What I don't want to do is special case int outside the constructor. My coercion logic simply trys to call the constructor on non BV types, if that fails it raise an error or returns NotImplemented depending on the context.

This leads to unpredicable behavior, for example bv & uint is a bv,. But what is bv + uint. If it is a bv, that seems weird because + is only technically defined on integers. And if it returned an uint because + is an operator on uint, then we need to convert bv to uint which seems dangerous.

Technically no __operators__ are defined by the abstract classes (this could be changed). However AbstractBitVector does define bvadd . And the python and smt implementations do define __add__ as bvadd. This was based on the code I inherited when I took over bitvector.

I would be happy to accept a PR which defined __operators__ on the abstract classes and removed them from the concrete ones.

[cdonovick]

@phanrahan
Not that this relevant to this issue but as a little experiment to test how common the use of __add__ on BitVector is I removed it (just __add__ not other arithmetic operators). It broke the tests of the following repos:
magma
mantle
fault
lassen
peak

So any PR removing arithmetic operators from BitVector will need to update at least those repos. I did not check gemstone / garnet / canal. But I suspect they would break too. I should also say the breaking does not all flow from some common internal call but rather from the tests themselves expecting + to work on bitvectors.

[phanrahan]

Comments.

• I wasn't referring to python tuples.

• The int() approach seems reasonable to me.

• Let's review one more time the type conversion rules for all the operators. And then update all the tests to be consistent.

[cdonovick]

Just to be clear @phanrahan excluding python tuple means excluding:

# 8
@ssa
def foobar(cond: Bit) -> (BV, BV):
    if cond:
        r_val = bv1, bv2
    else:
        r_val = bv2, bv1
    return r_val

[phanrahan]

I'd be ok with coercing python tuples to magma tuples. My only worry is this issue is that it will start getting out of control. For example, are we going to continually be adding conversions that are less and less well-defined.

[cdonovick]

Okay here is my issue with support through coercion into Tuple inside of Bit.ite

T = Tuple[BV[4], BV[4]]
S = Tuple[SBV[4], BV[4]]

# This could be False, which would fix my issue partially 
# However the implementation would be pretty tricky
assert not issubclass(S, T)

def foo(cond: Bit):
    if cond:
        r_val = bv1, bv2
    else:
        r_val = sbv, bv1
    return r_val

gets transformed approximately to:

def foo(cond: Bit):
    r_val = cond.ite((bv1, bv2), (sbv, bv1))
    # ite infers type T form (bv1, bv2)
    # ite infers type S from (sbv, bv1)
    # there is no way to unify the types so a TypeError will be raised
    # but if we did resolve S a sublclass of T it would return a T
    return r_val

However:

def bar(cond: Bit):
    if cond:
        r_val_0 = bv1
        r_val_1 = bv2
    else:
        r_val_0 = sbv
        r_val_1 = bv1
    
    return r_val_0, r_val_1

get transformed approximately to:

def bar(cond: Bit):
    r_val_0 = cond.ite(bv1, sbv) # type is BV[4]
    r_val_1 = cond.ite(bv2, bv1) # type is BV[4]
    return r_val_0, r_val_1 # returns python tuple

[cdonovick]

I want consistent and clear rules for user code. Either we allow python tuples or we don't. If we do you shouldn't have to use stupid code structuring tricks (like Bar above) to get it the code to type check.

I think the rules become the most sane if we remove the coercion from ite and use the following type unification algorithm (this effectively what is implement but the implementation is slightly expanded to give better error messages and because of the coercion logic):

def unify_types(true_branch, false_branch):
    if (isinstance(true_branch, tuple)
        and isinstance(false_branch, tuple)
        and len(true_branch) == len(false_branch):
        return tuple(unify_types(t, f) for t, f in zip(true_branch, false_branch))
    elif isinstance(false_branch, type(true_branch)):
        return type(true_branch)
    elif isinstance(true_branch, type(false_branch)):
        return type(false_branch)
    else:
        raise TypeError()

Otherwise I think we should forbid the use of python tuples completely.