AbsInt / CompCert

The CompCert formally-verified C compiler
https://compcert.org
Other
1.85k stars 225 forks source link

possible other miscompilation error of variable arguments builtins on arm(hf) #474

Closed monniaux closed 1 year ago

monniaux commented 1 year ago

reduced version of gcc test va-arg-21.c

#include <stdarg.h>
#include <stdlib.h>
void a(char *b, ...) {
  va_list *c[3], **d = c;
  c[0] = malloc(sizeof(va_list));
  c[1] = NULL;
  c[2] = c[0];
  va_start(*c[0], b);
  va_end(**d++);
  d++;
  if (*d == 0)
    abort();
}
int main() { a(""); }

It seems to me that this program should not abort. Examination of the RTL shows that for some reason the pointer d is incremented only once.

This program is equivalent to the following one, which does not abort:

#include <stdarg.h>
#include <stdlib.h>
void a(char *b, ...) {
  va_list *c[3], **d = c;
  c[0] = malloc(sizeof(va_list));
  c[1] = (void*) 0;
  c[2] = c[0];
  va_start(*c[0], b);
  va_end(**d);
  d++;
  d++;
  if (*d == 0)
    abort();
}
int main() { a(""); }
m-schmidt commented 1 year ago

The problem is in C2C.ml, function convertExpr:

  | C.ECall({edesc = C.EVar {name = "__builtin_va_end"}}, _) ->
      Ecast (ezero, Tvoid)

Arguments to va_end (with possible side effects) are ignored and the whole expression replaced with zero.

m-schmidt commented 1 year ago

Potential fix:

| C.ECall({edesc = C.EVar {name = "__builtin_va_end"}}, [arg]) ->
    Ecast (convertExpr env arg, Tvoid)