We are not changing the typing rules of BIL or Core Theory, but providing a well-defined behavior for application of binary operations on bitvectors with unequal lengths. Before that, the behavior was undefined and the precondition of the function was clearly specifying that the inputs should be of equal lengths.
The new behavior is to promote words to the equal length, (much like in C, which implicitly coerces the narrow type to the wider type).
The motivation is simple. It is hard to ensure this precondition in general. Yes, our lifters produce well-typed code, so there are no issues when we interpret code from the lifters. But we also have a lot of different interpreters, extensible via primitives. And those interpreters sometimes don't have any means (or at least efficient means) to ensure that all binary operations have matching widths. A concrete example of such interpreter is Veri that is used for bi-interpretation of traces and BIL programs for verification. Sometimes, the tracers organically produce ill-typed code, as they rely on their own typing rules. For example, qemu-based tracer just represent every register (including flags) and every number (including bools) with a word-sized bitvector. We still want to be able to perform calculations on such inputs and, to be honest, the results are quite well-defined, no hacks required. In other words, this change tries to follow the robustness principle, i.e., "be conservative in what you do, be liberal in what you accept from others". Our lifters, i.e., the code that we produce, are still much conservative, but our interpreters tend to be more liberal and understand even the ill-typed code, especially if this code has clear semantics.
We are not changing the typing rules of BIL or Core Theory, but providing a well-defined behavior for application of binary operations on bitvectors with unequal lengths. Before that, the behavior was undefined and the precondition of the function was clearly specifying that the inputs should be of equal lengths.
The new behavior is to promote words to the equal length, (much like in C, which implicitly coerces the narrow type to the wider type).
The motivation is simple. It is hard to ensure this precondition in general. Yes, our lifters produce well-typed code, so there are no issues when we interpret code from the lifters. But we also have a lot of different interpreters, extensible via primitives. And those interpreters sometimes don't have any means (or at least efficient means) to ensure that all binary operations have matching widths. A concrete example of such interpreter is Veri that is used for bi-interpretation of traces and BIL programs for verification. Sometimes, the tracers organically produce ill-typed code, as they rely on their own typing rules. For example, qemu-based tracer just represent every register (including flags) and every number (including bools) with a word-sized bitvector. We still want to be able to perform calculations on such inputs and, to be honest, the results are quite well-defined, no hacks required. In other words, this change tries to follow the robustness principle, i.e., "be conservative in what you do, be liberal in what you accept from others". Our lifters, i.e., the code that we produce, are still much conservative, but our interpreters tend to be more liberal and understand even the ill-typed code, especially if this code has clear semantics.