some additional comments: On 11/18/21 13:39, Laszlo Ersek wrote:
The usual way to prove "equivalence" between two logical formulae is to prove "implication" in both directions. That is, assuming "b" is nonzero, let's prove both of the following implications between C-language expressions:
(a <= max / b) IMPLIES (a * b <= max) [1]
(a * b <= max) IMPLIES (a <= max / b) [2]
- We can call [1] "correctness": wherever our reformulated condition works, we're sure to avoid overflow. I.e., our reworked formula isn't "too lax" (= a security issue). - We can call [2] "completeness": wherever our original condition can be satisfied, our reformulated condition will evaluate to "true" as well. In other words, our reworked formula isn't "too strict" (= a needless limit). - In both [1] and [2], it is understood (as I posited initially) that the multiplication operation "a * b" does not overflow. We posit that for the sake of argument; after the (proven) rearrangements, we'll only use multiplication if it indeed does not overflow. So perhaps it would be more precise to call [1] and [2] mathematical expressions already (not C expressions), just redefine "/" to be the C-style division (but let * have infinite precision).
/* This macro does not evaluate any one of its arguments, unless the argument * has variably modified type. */ #define HAVE_SAME_UINT_TYPES(a, b) \ ((typeof (a))1 / 2 == 0 && \ (typeof (b))1 / 2 == 0 && \ (typeof (a))-1 > 0 && \ (typeof (b))-1 > 0 && \ (typeof (a))-1 == (typeof (b))-1 && \ sizeof a == sizeof b)
Sorry, forgot the parens around (a) and (b) in the sizeof operands -- normally they are not needed, but here "a" and "b" are macro arguments, so the parents are needed. Thanks, Laszlo