Re: [Libguestfs] [PATCH nbdkit 2/2] common/include/checked-overflow.h: Provide fallback
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