Open cdonovick opened 5 years ago
FWIW, in magma we distinguish Bits from UInt based on the definition of arithmetic/comparison operators (i.e. raw bits just have logical element wise operators and equality, uint adds a notion of addition, less then, etc... since these only hav meaning if you're interpreting the bits in a certain way). However, it seems like this is inconsistent with the SMT bitvector theory? (which defines all the operators on bitvectors)
@leonardt
Theory bitvectors doesn't have a notion of signedness just defines functions (e.g. bvslt
, bvult
) and none of those functions are of the form __[^_].*[^_]__
(no dunders). So it would be completely consistent to remove all operators and ext
from BitVector
and have them only defined on Unsigned
/ Signed
In https://github.com/phanrahan/magma/issues/457 @jameshegarty requested type checking on signedness.
One way we could approach the role of Unsigned is simply for type checking.
Currently, both modifiers and signed / unsigned is ignored by all BitVector operations and coerces to the lhs to the type of rhs.
bv + bv -> bv
bv + unsigned -> bv
unsigned + signed -> unsigned
...
This is convenient as the code doesn't need to be littered with casts. One approach we could use to both have type safety is require the lhs be subclass of the rhs. So
bv + bv -> bv
bv + unsigned -> bv
unsigned + signed -> NotImplemented
unsigned + bv -> NotImplemented
Now the the final error conditions is probably not desirable so we could add the __r*__
operators (which is probably a good idea anyway so that int + bv
stops being an error),
bv + bv -> bv
bv + unsigned -> bv
unsigned + signed -> NotImplemented
unsigned + bv -> bv # dispatches to bv.__radd___(unsigned)
It should be noted that such a change will undoubtedly break a lot of code. @jameshegarty would a warning be sufficient? Adding that would not be hard. Another option would be to add a flag to turn strict type checking on.
hwtypes.STRICT = true
hwtypes.SIntVector[8](0) + hwtypes.UIntVector[8](0) -> Error
However, people who extend hwtypes (read: magma.Bits
) would need to be sure to also check this flag.
I don't have much context for this discussion but maybe I can add some issues I've run into. IMO It's realllly hard to automatically figure out the type conversions for math ops (eg to cast unsigned to signed without losing precision, you need to add an extra bit, but you also may not want this a lot of the time!). Not saying it's impossible, but without spending a lot of time on this, IMO I would prefer to err on the side of just making everything explicit, at least for a hardware language. The extra casts don't bother me, personally. I would also caution against adding warnings. These are usually ignored, and don't actually enforce any behavior in the language. This is certainly the case with Verilog. I would be ok with having a way to disable checks as a temporary backwards compatibility mode though.
btw I think my request was related to Magma in general (ie including arrays, handshakes, whatever). I don't fully understand how this repo relates to that effort.
@jameshegarty
I would also caution against adding warnings. These are usually ignored, and don't actually enforce any behavior in the language.
This is 100% true. Won't stop me from raising warnings though.
I would be ok with having a way to disable checks as a temporary backwards compatibility mode though.
For it to be backwards compatible it would needs to be explicit enable instead of explicit disable.
btw I think my request was related to Magma in general (ie including arrays, handshakes, whatever). I don't fully understand how this repo relates to that effort.
This repo defines (or will define in the future) the interfaces to these types and provides python functional models.
I wanted to comment on how I thought the code was suppose to work. Sadly, no guarantees.
All operators should be strictly typed. For example, you can add two unsigned or two signed, but not a signed and an unsigned. The result should be the same type as the operands.
Also, recall the type hierarchy.
Bits < Arrays UInt < Bits SInt < Bits
This means that array access are inplemented on Bits, UInt, and Sint.
Bits implement bitwise operators. Current, SInt and UInt also inherit these operators. One could argue with this decision.
Arithmetic and relational operators only work on Uint and SInt.
Finally, type checking should also be done at the level of functions.
For add(a,b) is equivalent to a+b.
We are encouraging people to use <= for assignment This works because the rhs must be an output and the lhs must be an input (which differentiates this operator from less than or equal). We could do strict typing on assignment.
I agree with that, I think that makes sense! My understanding is then, you could send a UInt[8] into a port that expects Bits[8], but could not send a SInt[8] into a UInt[8] port. And I would advocate for having the same behavior on the <= assignment as well, and the other various ways of doing wiring.
All operators should be strictly typed. For example, you can add two unsigned or two signed, but not a signed and an unsigned. The result should be the same type as the operands.
As I mentioned above this is not this case and will break things if it is. I am fine with making things strict if we can get people to update downstream tools...
Bits implement bitwise operators. Current, SInt and UInt also inherit these operators. One could argue with this decision. Arithmetic and relational operators only work on Uint and SInt.
We need to unify the Bits
and BitVector
interfaces which means either Bits
is going to gain arithmetic / comparison operators or BitVector
is going to lose them. As removing operators from BitVector
will break just about everything that's out of the question. Hence Bits
/BitVector
is basically going to become an alias for UInt
accept it can be coerced to SInt
. However it still isn't clear to me what the rules will be. If people could list there expected output type / error status for the following expressions it would help me.
bv + sint
uint + bv
uint + sint
Addendum:
It is isn't technically necessary for Bits
to have arithmetic operators as they are not part of the AbstractBitVector
interface. However, people use AbstractBitVector
with the assumption that operators will be defined.
What about implementing all the operators as methods in BitVector, but only overload the operators in python in the way I described.
I do agree in general with James that we should be stricter on typing.
What about implementing all the operators as methods in BitVector, but only overload the operators in python in the way I described.
This is currently the case AbstractBitVector
requires all the bvop
methods but no operators. My concern is that people use AbstractBitVector
expecting them to behave like BitVector
.
@phanrahan Also I still want to know the expected return types of the following expressions
bv + sint
uint + bv
uint + sint
I agree that it may be confusing to not overload the operators in BitVector. We could create a new class Bits, but let me think about it.
The following
bv + sint
uint + bv
uint + sint
would all be errors, since it would be an error to do an implicit cast.
uint + uint
sint + sint
would work.
@phanrahan so this should be an error as well then?
class Tagged(UInt): pass
tagged = Tagged[8](0)
uint = Uint[8](0)
tagged + uint
Also what about
uint + 7
uint + <type that supports __int__>
I personally am not really a user of hwtypes so have very little stake in the decision. However, I want to be clear about all the cases and ramifications of requiring an explicit type match.
@leonardt and I discussed this case in the past
uint + 7
sint + 7
We thought that this should be allowed, with a type check that the python int
fits within the uint or sint. It would not be legal to do uint + (-1)
, for example. I could imagine this would be a good choice for any python type that supports __int__
.
Generally, we would support inheritance on magma types. So, Tagged would be considered a uint
. I think that is what the programmer intended if he wrote class Tagged(Uint)
.
By this reasoning, uint
and sint
inherit all the bitwise operators.
There is a question of what should be the type of the result when inheriting an operator. Should the result be the type which implements the operator, or the instance that was being called with the operator. I think it should be the type of the instance.
uint & 1
should return an uint
.
My 2c.
I somewhat disagree with your stance on uint + (-1)
. UInt(-1)
is legal and in my opinion should remain legal, it's a super useful way to construct masks. It would seem uninitiative to me to then block arithmetic operators using it.
But even without that, the rules you are describing are becoming a bit convoluted.
def type_check(self, operand):
# Allow tagged_uint to work with uint but prevent uint from working with bv
if isinstance(operand, type(self)) and isinstance(self, (AbstractUnsigned, AbstractSigned)):
return True
# Allow tagged_bv to work with bv but prevent uint from working with bv
elif isinstance(operand, type(self)) and not isinstance(operand, (AbstractUnsigned, AbstractSigned)):
return True
# Allow int
elif isinstance(operand, int):
return True
# Allow types that support __int__ but not bitvector types
elif hasattr(operand, '__int__') and not isinstance(operand, AbstractBitVector):
return True
else:
return False
If I have misinterpreted your goals please correct me.
I was thinking that bitwise operators would be part of uint and sint, since these are subclasses of bits.
Thinking about it some more, I am worried that checking for int is too general.
My code would probable be simpler.
def type_check_operator(self, operand):
is isinstance(operand, int):
return True
elif type(self) == type(operand)
return True
else:
return False
And then make sure the operators return type(self).
Your code excludes tagged + uint
.
I would only allow tagged + tagged
.
@rdaly525 @rsetaluri @leonardt What are all your opinions on this? You guys actually use hwtypes.
As far I am concerned I would think the following is the most intuitive rule:
def type_check(self, operand):
if isinstance(operand, int):
return True
elif isinstance(operand, type(self)):
return True
else:
return False
But again I am not really a user so don't have a lot of stake in this.
I agree that is more precise.
Yes, it would be good to get other comments on this, including @jameshegarty.
My default model for numeric types these days is Rust, which does not implicit type conversion and requires types to match on numeric operators.
I am fine with that typechecking rule
I am a fan of stricter rules, requiring the user to do conversion where necessary.
I think the difference between the two most recent proposed rules by @cdonovick and @phanrahan is that @cdonovick uses isinstance(operand, type(self))
whereas @phanrahan uses type(self) == type(operand)
.
In @cdonovick's scheme, it would be okay to do something like bits + uint
, since uint
is a subclass of bits
so an instance of uint
would be an instance of bits
. If we use this rule, I think we'll need to check both directions to be consistent (so bits + uint
and uint + bits
). Another issue here is what the return type would be uint
or bits
. I think one idea is that returning a bits
makes sense, since there's no implicit downcast, but then this brings an issue as to whether this makes sense w.r.t. to +
being defined on bits
. Perhaps there's some scheme where if the operator is defined on the subtype, then the result is of the subtype, otherwise the result is upcasted to the supertype, but this is starting to get into more complex territory.
@phanrahan requires strict type checking (no implicit up/down cast), which is less convenient for the user but easy to understand.
Can we define a clear set of rules for up/down casting w.r.t. to operators and sub/super types?
I switched my vote from type(self) == type(operand)
to isinstance(operand, type(self))
. My reasoning is that if we are going to use inheritance, we should inherit operators from the parent class.
The following would be legal.
bits & unit
Since uint
is a bits
. The uint would be cast to a bit
, the bitwise &
would be performaned, and a bits
would be returned. The length of the uint
would need to be the same as the length of the bits
.
The following would be lilegal.
uint + bits
Okay, it seems that actually works with Caleb's rule, basically operator would be defined on uint, so it would fail an isinstance check with a bits (but the other way around would work for a bits operator).
So the summary seems to be implicit upcasting (casting to the super type) is allowed.
My only additional comment is that the type work properly for commutative operators.
bits & uint
uint & bits
I'm also generally in favor of allowing this implicit casting to super type and defining the ops on the the "oldest" member in the type hierarchy.
Not sure if I should start a new issue for this, but magma has to extend the Tuple/Product types for various reasons, so I would vote to add Tuple/Product (and Sum, etc...) to be part of the family if possible.
@phanrahan we can have bits & unit
and uint & bits
both return bits
by defining __r*__
operators and returning not implemented
def __operator__(self, other):
# Note BV[8] is not a subclass of BV[16] so this ensures a size match
if isinstance(other, type(self)):
return operator(self, other)
elif isinstance(other, int):
return operator(self, type(self)(other))
else:
return NotImplemented
def __roperator__(self, other):
if isinstance(other, type(self)):
return operator(other, self)
elif isinstance(other, int):
return operator(type(self)(other), self)
else:
return NotImplemented
The following would be lilegal.
uint + bits
Again I think we should add arithmetic operators to bits so that its inline with bitvector.
@leonardt In my mind there is no reason you should have to subclass the ADT types. Maybe we meet to discuss what your needs are.
And in any event I am strongly opposed to adding them to the family. They are not dependent on or related to BitVector types in any way.
I'm happy with stricter rules, no implicit conversion but inheritance operators work as https://github.com/leonardt/hwtypes/issues/98#issuecomment-544651967
My question is, what is explicit conversion in magma? is uint()
explicit?
Currently,
uint(SInt_value) -> Error
Because uint
has the rule (sint
has a typo though https://github.com/phanrahan/magma/pull/525 ). Even if uint
is explicit, still it makes sense if explicit conversion only allows upcast and downcast (Bits
-> SInt
, SInt
-> Bits
for example)
But downcast doesn't work now.
bits(SInt_value) -> SInt_value
array(SInt_value) -> SInt_value
Python doesn't have downcast, so it may still make sense, in terms of Python type.
Most convenient way to convert SInt from UInt now is,
uint(concat(SInt)) -> UInt
concat(SInt_value) -> Array[8, Out(Bit)]_value
uint(Array[8, Out(Bit)]_value) -> UInt_value
Type families are a hack. I would like to make them more elegant.
I want to define a class
Family
which expects that inheriting classes will have inner classesBit
andBitVector
, then automatically generatesSigned
/Unsigned
for those classes.expands to
Where
Now currently
Unsigned
is pointless as it is basically just an alias ofBitVector
. So I think we should do one of two things: drop it or remove signed dependent operators and functions fromBitVector
and require the use ofUnsigned
. Now changing the interface ofBitVector
would break a lot of code so I would lean towards just removingUnsigned
as it is basically unused.