sv-benchmarks intel-tdx-module parsing errors

[sim642]

SV-COMP has a new SoftwareSystems subcategory where we cannot parse any of the programs. For example:

$ ./goblint --conf conf/svcomp25.json --sets ana.specification ../sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 64bit ../sv-benchmarks/c
/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i
[Warning] --sets is deprecated, use --set instead.
[Warning] --sets is deprecated, use --set instead.
REDOREDOREDOREDO../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:6002: Error: Cannot find designated field leaf
error in createGlobal(cpuid_lookup: ../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:6002): GoblintCil__Errormsg.Error../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:6450: Error: Cannot find designated field leaf
error in createGlobal(cpuid_configurable: ../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:6450): GoblintCil__Errormsg.Error../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:6542: Error: Cannot find designated field vmm_rd_mask
error in createGlobal(global_sys_lookup: ../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:6542): GoblintCil__Errormsg.Error../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:7139: Error: Cannot find designated field prod_rd_mask
error in createGlobal(td_l2_vmcs_lookup: ../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:7139): GoblintCil__Errormsg.Error../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:8725: Error: Cannot find designated field prod_rd_mask
error in createGlobal(td_vmcs_lookup: ../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:8725): GoblintCil__Errormsg.Error../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:10167: Error: Cannot find designated field prod_rd_mask
error in createGlobal(tdr_tdcs_lookup: ../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:10167): GoblintCil__Errormsg.Error../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:11104: Error: Cannot find designated field prod_rd_mask
error in createGlobal(tdvps_lookup: ../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i:11104): GoblintCil__Errormsg.ErrorREDOREDOREDOREDOError: There were parsing errors in ../sv-benchmarks/c/intel-tdx-module/tdg_servtd_wr__cover__success_havoc_memory.i
Fatal error: exception Goblint_lib__Maingoblint.FrontendError("Errormsg.Error")

[sim642]

The first error also happens on this minimized program:

typedef unsigned int uint32_t;
typedef unsigned long long int uint64_t;
typedef union
{
    struct
    {
        uint32_t leaf;
        uint32_t subleaf;
    };
    uint64_t raw;
} cpuid_config_leaf_subleaf_t;
typedef struct
{
    cpuid_config_leaf_subleaf_t leaf_subleaf;
} cpuid_lookup_t;
extern const cpuid_lookup_t cpuid_lookup[68];
const cpuid_lookup_t cpuid_lookup[68] = {
 [10] = { .leaf_subleaf = {.leaf = 0x0, .subleaf = 0xffffffff}}
};

[michael-schwarz]

After further simplification, it seems that to trigger the problem it suffices to initialize a union with a struct.

typedef union
{
    struct
    {
        short leaf;
    };
    int raw;
} un;


un v = { .leaf = 0 };

[michael-schwarz]

It seems that the code to generate initializers does not handle anonymous members properly. For normal accesses CIL properly translates this.

For example

    un v;
    v.leaf = 8;

becomes

  un v ;
  v.__annonCompField1.leaf = (short)8;

Notice the nice spelling mistake 🤣

[sim642]

I vaguely recall from looking at it that referencing the inner leaf field like that in the initializer is problematic. In particular, CIL has to find the field from somewhere and construct the intermediate layers (anonymous struct). The ability to do this is perhaps GNU-specific? I think I couldn't really find any description on how/what exactly is allowed to be omitted like this. In particular, what if multiple intermediates are omitted?

[michael-schwarz]

In other cases CIL seems to perform a DFS which also seems to be the morally correct thing to do. As these anonymous things behave "as if" their members were members of the original struct, this should be non-ambigous.

https://github.com/goblint/cil/blob/f5ee39bd344dc74e2a10e407d877e0ddf73c9c6f/src/frontc/cabs2cil.ml#L3499-L3514

It supposedly was supported as a GCC extension but has since become part of the standard (C11). For a rather superficial treatment see, e.g., here https://www.geeksforgeeks.org/g-fact-38-anonymous-union-and-structure/.

[sim642]

If I'm not mistaken, the initializer case is instead handled here: https://github.com/goblint/cil/blob/f5ee39bd344dc74e2a10e407d877e0ddf73c9c6f/src/frontc/cabs2cil.ml#L5524-L5551 There's some Cabs hackery with a special ___matching_field field name.

The code in the initial issue prints these REDOs.