Skip to content

Refactor rule for arithmetic operators.

Rodolphe Lepigre requested to merge ci/refactor_arith_ops into master

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_result that, given the two operands and the op computes the result.
  • Define a predicate arith_op_sidecond that 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 / and %.
  • 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.

Merge request reports