So today I (re-?) discovered that substitutions are not type-preserving in C.
int x[1];
int *px = x;
int **ppx = &px;
substituting px away breaks typing:
int x[1];
int **ppx = &x;
does not work, because &x has type (int*)[1]. In other words, the intermediary declaration px forces array decay, which otherwise does not happen (because array decay is in function argument position, or assignment position). This makes sense: &x represents only a single level of indirection, not two.
The C compiler will flag this and reject the program. But of course we don't want to generate C code that doesn't compile, so rather than introduce a cast, we simply refuse to substitute away variables that force array decay.
This was only triggered by Eurydice, because due to a fortuitous scheduling of compilation passes, this was not exercised with the Low frontend (& is only introduced very late as a cosmetic optimization when the frontend is Low, and this happens after substitution of temporary variables).
So today I (re-?) discovered that substitutions are not type-preserving in C.
substituting px away breaks typing:
does not work, because
&xhas type(int*)[1]. In other words, the intermediary declarationpxforces array decay, which otherwise does not happen (because array decay is in function argument position, or assignment position). This makes sense:&xrepresents only a single level of indirection, not two.The C compiler will flag this and reject the program. But of course we don't want to generate C code that doesn't compile, so rather than introduce a cast, we simply refuse to substitute away variables that force array decay.
This was only triggered by Eurydice, because due to a fortuitous scheduling of compilation passes, this was not exercised with the Low frontend (& is only introduced very late as a cosmetic optimization when the frontend is Low, and this happens after substitution of temporary variables).
This has no impact on HACL*.