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.

cil/src/frontc/cabs2cil.ml

Lines 3499 to 3514 in f5ee39b

	let findField (n: string) (fidlist: fieldinfo list) : offset =
	(* Depth first search for the field. This appears to be what GCC does. *)
	let rec search = function
	[] -> NoOffset (* Did not find *)
	| fid :: rest when fid.fname = n -> Field(fid, NoOffset)
	| fid :: rest when prefix annonCompFieldName fid.fname -> begin
	match unrollType fid.ftype with
	TComp (ci, _) ->
	let off = search ci.cfields in
	if off = NoOffset then
	search rest (* Continue searching *)
	else
	Field (fid, off)
	| _ -> E.s (bug "unnamed field type is not a struct/union")
	end
	| _ :: rest -> search rest

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:

cil/src/frontc/cabs2cil.ml

Lines 5524 to 5551 in f5ee39b

	(* We have a designator that tells us to select the matching union field.
	This is to support a GCC extension *)
	| TComp(ci, _) as targ, [(A.NEXT_INIT,
	A.COMPOUND_INIT [(A.INFIELD_INIT ("___matching_field",
	A.NEXT_INIT),
	A.SINGLE_INIT oneinit)])]
	when not ci.cstruct ->
	(* Do the expression to find its type *)
	let _, _, t' = doExp isconst oneinit (AExp None) in
	let tsig = typeSigNoAttrs t' in
	let rec findField = function
	[] -> E.s (error "Cannot find matching union field in cast")
	| fi :: rest
	when Util.equals (typeSigNoAttrs fi.ftype) tsig
	-> fi
	| _ :: rest -> findField rest
	in
	(* If this is a cast from union X to union X *)
	if Util.equals tsig (typeSigNoAttrs targ)
	then
	doInit isconst setone so acc [(A.NEXT_INIT, A.SINGLE_INIT oneinit)]
	else
	(* If this is a GNU extension with field-to-union cast find the field *)
	let fi = findField ci.cfields in
	let _ = ignore (E.log "REDO" ) in
	(* Change the designator and redo *)
	doInit isconst setone so acc [(A.INFIELD_INIT (fi.fname, A.NEXT_INIT),
	A.SINGLE_INIT oneinit)]

There's some Cabs hackery with a special ___matching_field field name.

The code in the initial issue prints these REDOs.