Add C11 generic support

[sim642]

Part of issue #13.

This PR cherry-picks the generic related commits out of #24, where they have been committed together with unrelated C11 features...

And then it's mostly rewritten according to #24 (review):

1. Generic is removed from CIL and resolved by Cabs2cil, so it's completely transparent downstream (e.g. Goblint).
2. Type compatibility is checked via combineTypes, which seems to be the right thing (it raises on incompatibility).
3. Default case checking is made safer by not abusing void type for it.

[michael-schwarz]

Nice to finally see progress with this! This should probably work in most reasonable cases.
However, I don't think combineTypes does exactly the right thing here.

It simply takes the union of all attributes (we handle qualifiers such as const as attributes too) of both types, but what the C11 standard (6.7.3 Type qualifiers, subsection 10) says is:

For two qualified types to be compatible, both shall have the identically qualified version
of a compatible type; the order of type qualifiers within a list of specifiers or qualifiers
does not affect the specified type.

Also, I think this Lval-Conversion that cppreference mentions also needs to be taken into account.

I added a test that highlights both issues:

cil/test/small1/c11-generic.c

Lines 1 to 27 in 50c02c9

	#include "testharness.h"
	#define type1(x) _Generic((x), char: 1, unsigned int:2, default:0)
	#define type2(x) _Generic((x), char: 1, unsigned int:2, const int:3, default:0)
	// This fails to compile but is perfectly legal, since int and const int are not compatible
	#define type3(x) _Generic((x), int:1, const int:2, default:0)
	int main() {
	unsigned char v_uchar;
	char v_char;
	int v_int;
	const int v_intconst;
	if(type1(v_int) != 0) { E(1); }
	if(type1(v_uchar) != 0) { E(2); }
	if(type1(v_char) != 1) { E(3); }
	if(type2(v_int) != 0) { E(4); } // This fails but should succeed
	if(type2(v_intconst) != 0) { E(5); } // This fails but should succeed
	if(type3(v_int) != 1) { E(6); }
	if(type3(v_intconst) != 1) { E(7); }
	if(type3((const int)v_int) != 1) { E(6); }
	if(type3((const int)v_intconst) != 1) { E(7); }
	SUCCESS;
	}

• Currently, CIL will not compile this because it thinks there are multiple compatible compatible associations in type3.
• When these lines are removed, we will get Error 4 (v_int matching with const int) and Error 5 (v_intconst matching with const int, this is the case where the Lval-Conversion is erroneously disregarded).

GCC (via Godbolt) and Clang (via Godbolt) handle this correctly and output SUCCESS.

[sim642]

However, I don't think combineTypes does exactly the right thing here.

It is the closest thing to compatible types that I found in CIL. Is there anything more correct?

The notion of compatible types is not new with generics, the same exact relation is used for types between different translation units and combineTypes is seems to handle that in CIL. So if there's a problem with it in generics, the same exact problem must also be present with translation unit merging, no?

Thus combineTypes should be fixed to treat const, etc specifiers in attributes specially. And once those specifiers matter, then lvalue conversions aren't really necessary, are they? It's not in the standard, so I'm not sure where cppref is getting it from and there it's just defined to remove const, etc specifiers.

(Unsurprisingly CIL contains two implementations for combineTypes with slightly different usage, which doesn't help this mess.)

[michael-schwarz]

So if there's a problem with it in generics, the same exact problem must also be present with translation unit merging, no?

Maybe there is. But what CIL (and we in Goblint) try here is not exactly implement the C11 standard, but we are (very often) more relaxed in order to handle pre C11 code (C99, or ANSI) or allow things that are GCCism even if they are not in accordance to the standard; So it may very well be that - despite not doing exactly what the standard requires - the implementation does the correct things in all the places where it was used before we added support for generics?

And once those specifiers matter, then lvalue conversions aren't really necessary, are they?

So, if we look at the example above, compliant behavior is to match int even when the type supplied in the control expression at first glance is int const.

#define type3(x) _Generic((x), int:1, const int:2, default:0) 
if(type3(v_intconst) != 1) { E(7); } 

If CIL does insert such a cast to int for the control expression (as the type of the Cil.Lval will come from the varinfo, so include the qualifier), we don't need to do anything.
But I am not sure whether it will do this automatically. We'll see as soon as we fix the first bug.

The relevant definition for lvalue conversions btw is in 6.3.2.1:

Except when it is the operand of the sizeof operator, the unary & operator, the ++
operator, the -- operator, or the left operand of the . operator or an assignment operator,
an lvalue that does not have array type is converted to the value stored in the designated
object (and is no longer an lvalue); this is called lvalue conversion. If the lvalue has
qualified type, the value has the unqualified version of the type of the lvalue; (...)

So the way I would read this, this includes usage in the control expression of a generic expression, no?

[sim642]

I looked at the other uses of combineTypes and there are two which explicitly use it to check for compatible types via exception, so it intends to do this check:

cil/src/frontc/cabs2cil.ml

Lines 1669 to 1670 in 041c7cf

	(* Make sure the types are compatible *)
	ignore (combineTypes CombineOther oldf.ftype f.ftype);

cil/src/frontc/cabs2cil.ml

Lines 4568 to 4570 in 041c7cf

	let compatible =
	try ignore(combineTypes CombineOther t1 t2); true
	with Failure _ -> false

And the type returned by combineTypes is actually what is called composite type in the standard and can only be constructed from two compatible types.

But you're probably right that the existing process is too forgiving for type qualifiers. C11 6.2.7.2 just says:

All declarations that refer to the same object or function shall have compatible type;
otherwise, the behavior is undefined.

So CIL is allowing some of this undefined behavior. But the way it currently is implemented (union of attributes, which contain qualifiers) is nonsense: if one translation unit specifies a global as const int and the other one just as int, then in the combined file it should definitely not be const int (which the union would currently give).

I'll try to add some extra type qualifier attribute checks to combineTypes to make generics work right at least. In other aspect this should only forbid a bit more undefined behavior in CIL.

[sim642]

@michael-schwarz How is one supposed to run the tests locally? If I use dune runtest then it prints tons of output for each test (stdout, timings, etc) making it impossible to find out what's actually wrong. Including error output like:

Starting test 401/410 on Mon Sep 13 12:14:18 2021: testrungcc/enum3c
enum3c.c:3: Error: Constant initializer 22 << 34 not an integer
Error on A.ONLYTYPEDEF (Errormsg.Error)
enum3c.c:11: Error: Cannot resolve variable LARGE.
enum3c.c:11: Error: global initializer
error in createGlobal(magic2: enum3c.c:11): Errormsg.Errorenum3c.c:17: Error: Cannot resolve variable TINY.
Error: Cabs2cil had some errors
Fatal error: exception Errormsg.Error
make[1]: *** [Makefile:203: testrungcc/enum3c] Error 2

which actually is an expected failure (?). The exact same command on CI somehow only prints concise output: https://github.com/goblint/cil/runs/3567221712#step:11:538 and none of this confusing crap.

EDIT: I figured it out. If any test fails, then make test outputs the raw output for all tests (including those which succeeded or failed as expected). And this output was so long that the original overview was far out of my terminal history. And dune runtest didn't work properly under less.

I made a small change to not dump the whole raw log by default like that.

[michael-schwarz]

@michael-schwarz How is one supposed to run the tests locally?

If you are interested in only one specific tests you can also (provided you have done the Makefile based build) run just that one.
E.g.:

cd test
make testrunc11/c11-generic

[sim642]

I'm not sure what CIL does with this const info though, I don't think it itself really cares anywhere. I guess the recursive const removal is just necessary for things like --enable justcil of Goblint to still compile.

I tried to fix this final issue and it turned out to be much harder than I thought.

First, I thought I could just introduce a global mutable CIL option, which controls whether to strip const attribute from local variables or not, but this fails tests either way:

1. if it's enabled, then the generic test fails.
2. If it's disabled, then many tests fail because of assignments to const variables, which have been split from local initializers.

Second, I tried something very naive: keep the const internally to make generics work correctly, but never print them when writing the CIL AST back into a C file. That sounds like it should fix both problems, but hell no. The whole testing framework of CIL is built on the pipeline "CIL parse" -> "CIL print" -> "GCC compile" -> "execute". Removing all const makes the parsed and printed programs not equivalent to the originals in terms of whether they compile or not, so many tests didn't fail when they should've (unexpected success).

Third and (hopefully) final, I came up with the idea of separating the const attribute from whether const should be printed when outputting. I added a second pconst attribute which controls whether const is printed, while the const attribute is used for all the type-based stuff internally, thus fixing generics. The stripping of const from local variables still happens, but it only strips the pconst attribute to make printed programs still compile as well.
Of course this is complete mayhem, but at least the tests pass like this.

[michael-schwarz]

Is removing this necessary?

[michael-schwarz]

Ok, looks like this is an MSVC thing, which we will no longer support anyway.

[sim642]

I think it was actually supposed to be a GCC thing, but it didn't even match the typing behavior of GCC: #48 (comment).

[michael-schwarz]

Is this TODO resolved now?

[sim642]

I suspect not, but I don't know what it's precedence is even supposed to be because it's not even listed here: https://en.cppreference.com/w/c/language/operator_precedence.

Also, I'm not sure the rest are right either. Most of the additions have been copy-pasted all with precedence 16, but that doesn't match at all with the precedence table comment above or the table on cppref.

[michael-schwarz]

Probably after merging develop, we should be good to go here, right? Might not cover 100% of usages of generic and not 100% of C11, but still seems worth having :)