Handle initializers for anonymous struct in unions

[michael-schwarz]

Closes #176.

[michael-schwarz]

With these changes the intel-tdx-module benchmarks can be parsed, and the analysis in Goblint starts.

[sim642]

@jprotopopov-ut Didn't you also encounter this issue with the Linux kernel?

[jprotopopov-ut]

@jprotopopov-ut Didn't you also encounter this issue with the Linux kernel?

Yes, I had to implement a fix for that: https://github.com/sws-lab/linux-verification-cil/commit/7da571debf9f895634c0a7820be485d40471297e

[michael-schwarz]

Is the fix the same one as the one I implemented here? (The repo is not public, so I can't compare).

[jprotopopov-ut]

My fix is somewhat ugly (and perhaps incomplete), as I rely on constructing a surrogate designator for anonymous structs/unions. It seems to work for kernel analysis, but you should probably disregard it. At some point, I'll have to sync up my forks, then I'll deal with these changes.

[sim642]

I haven't looked at either fix yet, but looks like we probably can try going with this one first.

The test in the private repository is the following. It would be good to add it here and at least confirm it also works with this implementation.

struct S1 {
    struct {
        int a;
        int x;
    };

    struct {
        int b;
        int y;
    };

    struct {
        int c;
        int z;
    };
} s1 = {
    .a = 1,
    .b = 2,
    .c = 3,
    .x = 100,
    .y = 101,
    .z = 102
};

struct S2 {
    union {
        int a;
        int b;
    };

    union {
        struct {
            int c;
            int d;
        };

        struct {
            int e;
            int f;
        };
    };
} s2 = {
    .b = 100,
    .c = 500,
    .d = 600
};

struct S2 s2_2 = {
    .a = 1,
    .e = 2,
    .f = 3
};

[michael-schwarz]

It was good to add this test. It seems that parsing succeeds for that example, and some (compiling) code is generated, but the generated code is wrong.

[michael-schwarz]

Upon closer inspection, it seems that my approach is somehow flawed as it will always init the entire inner struct. @jprotopopov-ut can you maybe push your commit to a new branch in this repo (I invited you to contribute) so I can have a look?

Would be a shame if we waste effort by developing two solutions that are independent of each other.

[jprotopopov-ut]

Upon closer inspection, it seems that my approach is somehow flawed as it will always init the entire inner struct. @jprotopopov-ut can you maybe push your commit to a new branch in this repo (I invited you to contribute) so I can have a look?

Would be a shame if we waste effort by developing two solutions that are independent of each other.

Pushed it to anon-struct-initializers-1 branch: 113be78

[michael-schwarz]

I now largely went with @jprotopopov-ut's code, with one change to actually filter for anonymous members (the code tried to match on a variable to enforce equality which is a common mistake in OCaml and only creates a new let binding).

I also added an example where one can observe this difference.

Since the history is now polluted with my foibles, we should squash when we merge this.

[sim642]

@michael-schwarz You should do a Goblint PR to also update the pin there. Then we could see in the following nightly if we can do anything at all in intel-tdx-module.