Section 12.5 BITWISE_DIFFERENT_BITWIDTHS question

[eryjus]

I have a question about the definition of BITWISE_DIFFERENT_BITWIDTHS and where that definition is used. I am not certain this is a real issue or not. I appreciate the dialogue.

I see the definition in the prose and the formal definition, but no other rule explicitly uses this definition.

I can read that any operation on bitvectors can only operate literals of the same size. However, this is only weakly implied in the definitions.

If this is called out somewhere else I have missed, please let me know. However, I believe it might be clearer if that rule was explicitly called out when it is relevant.

Am I missing something here?

[Roman-Manevich]

This is definitely not an issue for user-given expressions that are part of statements, as we have this rule to check against applying operations to bitvectors of different widths:

The only case where this might be triggered (I'm not entirely sure though) is when static evaluation attempts to evaluate an expression reachable from an integer constraint. This is probably impossible, but I can't prove it beyond doubt right now.

I'm not sure what you mean by "but no other rule explicitly uses this definition". This is a possible case every time binop_literals is called. The way to call it is to pass two bitvectors, which happens every time a binary expression is evaluated via eval_binop.

Does this make sense? Please feel free to continue the discussion.