Oversize leaq operand in stack chaining MacOS x86_64

[AndrewTolmach]

If a stack frame size exceeds 2^32, e.g. due to large local arrays, the offset link is set incorrectly, because its value is calculated using an leaq using the frame size as an offset, but such offsets are restricted to 32-bit (signed) ints.
(The relevant code is generated at x86/Asmexpand.ml line 574).

The assembler should reject such invalid offset arguments, but unfortunately, MacOS as
(at least as of Apple LLVM version 10.0.0) does not do so. (Although gas on a recent debian linux does.)
Instead, it just silently throws away the high-order bits, in this case leading to a negative offset.

OK, so perhaps these large stack frames are officially undefined behavior (max 65K bytes per object and 512 declarations per block), and certainly a noisy failure would be fine here, but a silent one seems unfortunate.

Demonstrated by the following code, which should print 7 but prints 0:

#include <stdio.h>

char f(char x1, char x2, char x3, char x4, char x5, char x6, char x7) {
  char b[0x100000000];
  return x7;
}

int main() {
  char c = f(1,2,3,4,5,6,7);
  printf("%d\n",c);
}

[xavierleroy]

Well spotted, thanks for the report. This will be fixed shortly (with a proper compile-time error).

[xavierleroy]

Tentative fix in #407. Instead of failing at compile-time when lea overflows, it generates alternate code (mov + add immediate) that should be correct for any stack frame size. Let me know if it doesn't work for you.

[AndrewTolmach]

Works for me; thanks!

This does raise another question, though. I actually happened on this problem while trying to construct an exploit that uses a giant local array to evade the stack guard page and corrupt static memory. I didn't expect CompCert to prevent this (in fact, I used CompCert precisely to avoid the hassle of trying to turn off all the stack protections now found in gcc and clang), and indeed, the code quoted below has the desired bad effect.

Of course this is outside of the verified part anyhow, but does CompCert have an official policy, or even any unofficial guidance, about which programs will be considered as having undefined behavior due to excessive frame size (which does seem to be indirectly mentioned in the standard) or stack overflow (which does not seem to appear in the standard AFAICT) ?

#include <stdio.h>

char a[0x10000];

void g(int x) {
  printf("g &x = %lx\n", &x);
}

void f(int x) {
  char b[0x7ffeefbff6b8 - 0x100008000];
  printf("f &x = %lx\n", &x);
  printf("&a = %lx\n", a);
  printf("&b = %lx\n", b);
  b[0] = 43;
  printf("b[0] = %d\n",b[0]);
}


int main() {
  a[0] = 42;
  printf("a[0] = %d\n",a[0]);
  printf("&a = %lx\n", a); 
  g(1);
  f(1);
  printf("a[0] = %d\n",a[0]);
}

Compiling with -Wl,-no_pie,-no_compact_unwind yields this output on my MacOS platform:

a[0] = 42
&a = 100008000
g &x = 7ffeefbff6a8
f &x = 100007ff8
&a = 100008000
&b = 100008000
b[0] = 43
a[0] = 43

[xavierleroy]

Thanks for the feedback.

Regarding the question: no, CompCert doesn't try to put limits on the size of stack frames, except when absolutely necessary for the proof (i.e. the size must fit into a platform-sized signed integer). I'm not sure how such checks would prevent exploits: the effect of a large stack frame can be achieved by many recursive calls to a function with a small stack frame, right?

Concerning stack overflow: the CompCert semantics make no provisions for stack overflow and assume an infinite stack. See Stack-aware CompCert for a nice way to handle stack usage in semantics and code transformations.