Make fe magnitude implied statically

[real-or-random]

See the discussion starting here: #943 (comment)

[roconnor-blockstream]

To be clear, all the instances of magnitude are currently statically implied because all those "variables" that are dynamic are currently only ever passed integer literal values.

[peterdettman]

@roconnor-blockstream Surely not, e.g. what about _fe_cmov?

[roconnor-blockstream]

I wasn't aware of that one. (I'm less familiar with the non-verification related code.)

Make sense to patch that case by always setting the magnitude to the max of the two values?

[peterdettman]

Yes, which was already done, then patched out, so this time with more comments I think!

[real-or-random]

@peterdettman Can you elaborate a little bit more on the reasoning behind this suggestion?

I fully agree it's conceptually nicer. But as long as we don't have automated checks that prove that the magnitude is always low enough, does it really matter?

[roconnor-blockstream]

The whole point of the magnitude field is to have a check that the tested code paths would not overflow even if different values were used. It is a poor man's abstract interpretation.

But when we, say, set the magnitude of the output of cmov, based on the flag value, and the value of that flag value is dependent on the specific initial value we are testing, then our "abstract interpretation" ends up being limited to only those value that would produce the same flag value at that call site.

I respect that our poor man's abstract interpretation is imperfect. There are places were we explicitly branch on data (especially in the _var functions). But we can at least strive to make our abstraction as abstract as reasonably possible.

(For illustration: the opposite course of action would be to make the magnitude based more and more on concrete values, but there is no point in doing that. We already have a prefect measure of the a concrete magnitude: using the actual value itself!).

[peterdettman]

I thought of the magnitude verification AS the automated checks. It's inherently worst-case, basically a static bounds check. That plus code coverage of all branches (and careful analysis of the very few loops) means there's no overflows in the field arithmetic. Without that property you need to be sure you have test cases that exercise every code path at the maximum possible magnitude, which is just a harder-to-prove/understand version of the same thing.

[peterdettman]

We already have a prefect measure of the a concrete magnitude: using the actual value itself!

Bingo.

[real-or-random]

I thought of the magnitude verification AS the automated checks. It's inherently worst-case, basically a static bounds check.

Oh sure, I missed this part!

(My thinking was: "it's only dynamic analysis anyway". But if the values are statically determined, then that's indeed all we need...)

[peterdettman]

It sure would be nice to have a way of restricting a function argument to be a literal. Both to allow the obvious implementation for _mul_int, but also to restrict _fe_negate to specifying a literal for its 'm' (magnitude) argument.

[roconnor-blockstream]

I'm moderately sure there is some horrible way to enforce this with macros. The specific solution I came across uses compound literals, but I suspect there are C89 ways too.

But I'm not sure that we really want to go down the horrible-macro route.

Edit: Maybe just casting through a one dimensional array somehow I'm not sure.

#define foo(i) foo_do_not_call_directly((int[1+0*i])(int)(i)[0])

[real-or-random]

@roconnor-blockstream What about just appending u in the macro? That's valid only for literals, and magnitude is anyway not negative.

[roconnor-blockstream]

appending u also works for the expression i + 1.

[real-or-random]

Oh indeed.

What about this?

#define foo(i) foo_do_not_call_directly(sizeof(char[i]))?

edit: that doesn't give an error in GCC. It just gives a warning, and you need -pedantic to trigger the warning (variable-length arrays are a GCC extension)

Here's a better one:

#define foo(i) do { switch (i) {  case i: foo_do_not_call(i) }} while (0)

(suggested by @roconnor-blockstream again)

Another way of doing it is to define a force_const macro like:

#define force_const(i) (sizeof(struct{int a:i;}), i)

That only works up to the bitwidth of int, which is at least 16, so that's enough for this particular purpose...

https://port70.net/~nsz/c/c89/c89-draft.html#45 is pretty useful here.

There's also in https://gcc.gnu.org/onlinedocs/gcc/Other-Builtins.html#index-_005f_005fbuiltin_005fconstant_005fp in gcc.