TrustInSoft / tis-interpreter

An interpreter for finding subtle bugs in programs written in standard C
565 stars 28 forks source link

strict aliasing not checked #125

Open albertnetymk opened 8 years ago

albertnetymk commented 8 years ago
int f(int *x, long *y)
{
  *x = 0;
  *y = 1;
  return *x;
}

int main() {
  long x = 0;
  printf("%d\n", f((int*)&x, &x));
  return 0;
}

Was reading this, and if I understand it correctly, the above program should get a warning.

pascal-cuoq commented 8 years ago

A sequel of sorts to John's post (that he wrote while on sabbatical and contributing to tis-interpreter) is this one. The bug report is here. The total lack of reaction to the bug report makes me doubt whether there is more than punctual interest in such an analysis, but for now we continue to tune it and fix bugs. We'll investigate at least the situation with struct sockaddr before deciding what to do with such an analysis.

(“We” is @Aaylor and I. Unfortunately John's sabbatical has ended and he is only following what happens with it from a distance as one of the thousand fascinating projects he is involved in.)

dubiousjim commented 6 years ago

I've installed the tis-kernel package and am running its tis-interpreter script. Am I right that that package is based on this one? All the bug reporting activity seems to be taking place in this repository instead of that one.

When I run tis-interpreter -sa alias.c on the following file:

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <stdint.h>

union u1 {
    int i;
    float f;
};

float foo( void ) {
    int i = 1;
    float *fp = (float *)&i; // invalid
    union u1 u;
    u.i = 2;
    float g1 = u.f; // should be OK
    float g2 = *(&u.f); // invalid?
    float g3 = ((union u1 *)(&u.i))->f; // invalid?
    float g4 = ((union u1 *)(&u.f))->f; // invalid?
    float g5 = (&u)->f; // invalid?
    return (g1+g2+g3+g4+g5+ *fp) > 0;
}

int main() {
    float f = foo();
    printf("res: %g\n", f);
    return 0;
}

only the assignment that's definitely marked "invalid" (with no "?") is flagged. Actually, it's not until I try to dereference fp at the end of foo that the analyzer complains.

From reading the GCC docs, it looks like some or all of the lines marked "invalid?" should also fail. But tis-interpreter doesn't catch them. And neither does GCC complain, when run with -fstrict-aliasing -Wstrict-aliasing.

dubiousjim commented 6 years ago

The lines with g3 and g4 give a warning when I run with -Wstrict-aliasing=2 but not -Wstrict-aliasing (which is the same as -Wstrict-aliasing=3, and is supposed to be most accurate). Also if I separate the assignment and dereference, like this:

    union u1 *g3p = (union u1 *)&u.i;
    float g3 = g3p->f;

I'll get a warning only with -Wstrict-aliasing=2. Not sure whether this is really safe behavior, though. The last example in the GCC docs linked above seems to be of the same form, and there it's said to have undefined behavior.

pascal-cuoq commented 6 years ago

I've installed the tis-kernel package and am running its tis-interpreter script. Am I right that that package is based on this one? All the bug reporting activity seems to be taking place in this repository instead of that one.

The release of tis-interpreter predates that of tis-kernel. tis-kernel almost entirely subsumes tis-interpreter. The tis-interpreter repo was where all the initial bugs were reported, and it was advertised more because it was new and not just a new package for something that was already available before, but the tis-kernel repo is where this kind of discussion should take place now.

If you have not seen it, it would be a shame you didn't take a look at the article that sets the goals for and summarizes the design of the strict aliasing analysis. Re-reading it, I agree that I would expect at least some examples in g2, …, g5 to cause warnings, because GCC's documentation hints that it may optimize in these cases but even more so because Clang has been observed to optimize in very similar cases.

dubiousjim commented 6 years ago

OK, thanks for the explanation about the repos. I'm in the middle of reading that article. I'll follow up on the other repo, and/or on StackOverflow.