Devirtualization ignores functions incompatible with call sites.

[michael-emmi]

The following program is apparently not well defined by the C standard due to the type-unsafe call. However, real compilers end up actually calling foo and thus lead to an assertion violation. Currently our devirtualization pass does not consider the call to foo since its signature is incompatible with the call site.

#include <stdio.h>
#include <smack.h>

void foo(int x, int y, int z) {
  printf("Hello there %d, %d, %d!\n", x, y, z);
  assert(0);
}

int x;

int main(void) {
  void (*f)(void);
  f = (void (*)(void)) (x ? &foo : &foo);
  f();
  return 0;
}

Should devirtualization continue to ignore incompatible functions?

[shaobo-he]

I think we shouldn't ignore them because I think we'd like to make the handling of undefined behaviors consistent (i.e., respect the common-sense compiler). For strict-aliasing violations, we simply assume aliasing as the C compilers do. We shouldn't make an exception for type-unsafe calls.

[zvonimir]

Does seadsa handle devirtualization much more precisely than DSA?

There is a good reason for matching types - it allows us to prune many potential targets, thereby leading to much smaller switch-case, thereby often greatly improving performance. So there is a soundness vs performance trade-off here. I would be ok to improve soundness (by dropping type matching) if that will not lead to a major performance penalty.

Of course, we could always introduce a command line option that controls this behavior, which might be a nice middle ground.