Handling of compatible structure types under C23 semantics

[jprotopopov-ut]

C23 has relaxed rules for struct type compatibility making the following code snippet legal:

typedef void (*func_t)(void);

struct A {
    func_t f;
};

void test1(struct A {
    func_t f;
} *b) {
    b->f();
}

void dummy() {}

int main() {
    struct A arg = {dummy};
    test1(&arg);
    return 0;
}

Goblint (revision e816b4a) fails to recognize that b->f is initialized to dummy and outputs

[Warning][Unsound][Call] No suitable function to be called at call site. Continuing with state before call

C23 standard (section 6.2.7) specifies:

Moreover, two complete structure, union, or enumerated types declared with the
same tag are compatible if members satisfy the following requirements:
— there shall be a one-to-one correspondence between their members such that each pair of
corresponding members are declared with compatible types;
— if one member of the pair is declared with an alignment specifier, the other is declared with an
equivalent alignment specifier;
— and, if one member of the pair is declared with a name, the other is declared with the same
name

More discussion is also available in the following proposal.

This issue has surfaced when trying to analyze rsync version from AnalyzeThat. The linked code is in fact even more liberal in using pointers to incompatible struct types, as it declares these struct types with different tags (for example, see the type of the first parameter in the call to deflateInit_ from compress2).

[michael-schwarz]

Naively, I would think this might have to be handled on the CIL side? Wdyt @sim642?

[sim642]

It took me a while to understand where the issue even is: there's a new struct type declared within the argument type declaration of the function, instead of just using struct A, right?

I haven't looked at the CIL-ed code, but it seems that there isn't anything CIL is actually doing wrong, I'd expect there just to be an implicit pointer conversion, as required by any version of the standard.
It's just a matter of whether this conversion is defined, but that's out of CIL's hands.

It's probably something that our casting code needs to handle, if that's where the precision is being lost. This might be the place:

analyzer/src/cdomain/value/cdomains/valueDomain.ml

Lines 537 to 554 in bb9722d

	| TComp (ci,_) -> (* struct/union *)
	(* rather clumsy, but our abstract values don't keep their type *)
	let same_struct x = (* check if both have the same parent *)
	match Structs.keys x, ci.cfields with
	| k :: _, f :: _ -> compFullName k.fcomp = compFullName f.fcomp (* compinfo is cyclic, so we only check the name *)
	| _, _ -> false (* can't say if struct is empty *)
	in
	(* 1. casting between structs of different type does not work
	* 2. dereferencing a casted pointer works, but is undefined behavior because of the strict aliasing rule (compiler assumes that pointers of different type can never point to the same location)
	*)
	if ci.cstruct then
	Struct (match v with
	| Struct x when same_struct x -> x
	| Struct x when ci.cfields <> [] ->
	let first = List.hd ci.cfields in
	Structs.(replace (Structs.create (fun fd -> top_value ~varAttr:fd.fattr fd.ftype) ci) first (get x first))
	| _ -> log_top __POS__; Structs.create (fun fd -> top_value ~varAttr:fd.fattr fd.ftype) ci
	)

[jprotopopov-ut]

there's a new struct type declared within the argument type declaration of the function, instead of just using struct A, right?

Yes. Under new C23 rules, all such declarations within the same translation unit are considered compatible, and thus this is valid use of pointers here. Rationale for that was better support for patterns like the following:

#define ERROR(_type) struct Error##_type { bool has_error; _type error; }

ERROR(int) somefn();

void somefn2() {
    ERROR(int) rc = somefn()
}

I am not sure where the notion of type compatibility is handled in goblint, but I believe it should be updated accordingly.

As mentioned, rsync benchmark, as it is now, is even more liberal and assumes type compatibility irrespective of struct tags simply based on the contents.