AstraVer Toolset » Deductive Verification Tools for Linux Kernel

I revealed this issue one more time, but now I built up a simple example:

int main(int argc, char *argv[])
{
    int res;

    res = (argc > 1 ? ({ (void)1; }) : (void)2, (int)3);

    return res;
}

You can compile this code and check that function main always returns 3, while CIL fails to parse it with the error as in the issue description. It looks like the internal compound statement "({ ... })" confuses CIL. If you will replace it with, say, "(void)1" it will work.

This is example is artificial. The original issue comes from substitution of macro r1(), say, in https://elixir.bootlin.com/linux/v5.5.19/source/drivers/block/paride/friq.c#L58. Hopefully there are just several drivers that do this.

Ultimately reverted the framac|34aba90f and pushed an entirely different fix framac|8caa89de. Basically, instead of disabling the workaround in this case, now the solution is to actually reproduce the work-around even in case of a GNU-body ({ ...; (void) e; }), where the what = ADrop cannot be passed from the caller and so the special handling is added in yet another place (GNU-body handling). The possible side-effect is translating some extra code in the ignored GNU bodies that previously were entirely dropped, which potentially can expose some more bugs

Pushed framac|5b8e240a. It just refines treatment of some void expressions within GNU_BODY and in the arguments of the ?: operator. Inside the body we seek to avoid creating temp vars if the result is dropped; inside the ?: operator we allow `void` expressions in either side if the result is dropped. The attached test cases now pass, however, in general the semantics of the fixes is quite lax. In particular, epia.c has a call to __udelay and (void) 0 as arguments to ?:, which makes calculating the resulting type of the operation dubious: it can be either naively treated as `void` (which is wrong if the expression is later used in some larger context, as a temporary of type void is prohibited) or (void) 0 can be heuristically treated as plain 0 of type int (as in the heuristic discussed earlier, which is wrong since an implicit conversion between `int` and `void` is also prohibited). Technically, it seems there should be no expressions of type void in C, but the GNU {...; statement } allows for such possibility, hence all the issues

Partially reverted previous fixes in favor of a minimal change: framac|93c99dbf. Allowing an implicit cast between `void` and any type in case of an ignored result covers all the cases. I finally (after attempting many manual tests with GCC, LLVM and Frama-C) vaguely understand the logic behind all those cases: if the final result is ultimately dropped, a sub-expression of type void is treated as if it is of type int with all the corresponding implicit conversions or even as an expression of any type. However, the notion of "ultimately" is not very consistent: Frama-C accepted a computation (int)(x ? f() : (char *)0); (f is void) even before the patch, while GCC and LLVM failed on that, but a simpler x ? f() : (char *)0 is accepted by all of them. Also, x ? f() : (struct s) {.f = 0 } is accepted by LLVM and GCC, but not Frama-C (even after the minimal fix since the ignored call is treated as (int)0 elsewhere). The problem here is properly propagating the static approximation of the dropped flag, which is already different in Frama-C vs. GCC and LLVM. A really thorough fix would require consistently changing it everywhere, which is a lot of places in the entire expression translation function (about 2000 lines of code)

After more tests: Actually, the behavior of GCC and LLVM can be explained simpler: the result of a conditional conversion between void and any other type is simply void. Then the value of type void must be ignored (other conversions and operations don't allow it). No dropped flags needed anywhere. However, in Frama-C there are many places implicitly treating ignored expressions as int (the dummy value 0): at least in function calls, in casts, in statement expressions. In general this still requires a thorough revamp of the overall approach in the entire Frama-C translation procedure (the ubiquitous what argument is probably just a generally wrong optimization)