This PR does a bit of refactoring of the rules for binary (arithmetic) operators on integers. This will probably be useful to @paulzhu, and I needed this first step for the handling of right shifts. The changes are the following:
- Define a function
arith_op_resultthat, given the two operands and the op computes the result.
- Define a predicate
arith_op_sidecondthat gives the side conditions for a given op.
- Use the above functions in the rule
type_arith_op_int_int, and factor in the rules for
- Give more precise side conditions for the right and left shift operators (this is the goal of this PR). Note that the standard leaves it as implementation-define what is the result of right-shifting a negative number. I thing we should consider that UB.
Some further factoring of code is possible with the operational semantics, but we can do that as a second step.