Fix handling of empty type

[ThomasHaas]

This fixes a bug introduced in #770.

EDIT: I renamed the PR and added more fixes, mostly related to handling the empty type (+ one fix for alignments computation of arrays).

[hernanponcedeleon]

I noticed this regression when running the svcomp benchmarks. The fix restores the previous behavior.

@natgavrilenko can you please review?

[ThomasHaas]

There is nothing to review really. The empty struct is 1-aligned but #776 changed the behaviour to throw an error instead.

[natgavrilenko]

I don't see why it would change the behavior. The getAlignment method is called either from computeDefaultOffsets or from getMemorySizeInBytes. Both caller methods check if the AggregateType is empty.

How can reproduce the problem?

[hernanponcedeleon]

Try this file. It should be reproducible with all memory models.

[ThomasHaas]

I just noticed that the commit message of this PR is wrong (it seems I accidentally took the one from #775). Not sure how that happened.

[ThomasHaas]

Btw. I think this part of the alignment computation is wrong (*) as well:

        if (type instanceof ArrayType arrayType) {
            return getMemorySizeInBytes(arrayType.getElementType());
        }

The array should be aligned according to the alignment of its elements, not their size.

(*) This might technically not wrong because we simply overalign. But it does not match the usually expected alignment.

[ThomasHaas]

Actually, there are more issues.

(1) The behaviour of TypeFactory.getAggregateType(List<Type>) and TypeFactory.getAggregateType(List<Type>, List<Integer>) differ in that the former allows for empty members but the latter does not.

(2) In C, empty structs are undefined behavior, at least in theory!!! The SVCOMP benchmark is thus problematic. GCC allows empty structs as a custom extension and gives them size 0, and since Clang tries to be compatible with GCC, it shows the same behaviour.
Interestingly, in C++ empty structs are allowed but their size is 1 as to disallow different objects occupying the same memory location.
This begs the question: what should we do? Since we do only C for now, the choice of size 0 for the empty struct is probably the best (maybe we need to support a flag in the future like input.language=c++). However, we then inherit the awkward situation of having different objects at the same memory location, i.e., unions.
So the preconditions on TypeFactory.getAggregateType need to get relaxed.

EDIT: I fixed the above mentioned issues.

[hernanponcedeleon]

the choice of size 0 for the empty struct is probably the best

If empty structures are undefined behavior, we should report this and throw an exception when verifying C code.

@natgavrilenko what does the spirv standard say about empty structures? Can we have "This is UB" as a general solution?

[natgavrilenko]

Try this file. It should be reproducible with all memory models.

Thanks, now I see what is the problem.

[natgavrilenko]

the choice of size 0 for the empty struct is probably the best

If empty structures are undefined behavior, we should report this and throw an exception when verifying C code.

@natgavrilenko what does the spirv standard say about empty structures? Can we have "This is UB" as a general solution?

Yes, it works fine for spirv with empty structures. @ThomasHaas could you add this case to AggregateTypeTest?

[ThomasHaas]

If empty structures are undefined behavior, we should report this and throw an exception when verifying C code.

I think this solution is not practically viable because its a feature that is expected to work since GCC/Clang support it. One might say it is more implementation-defined in practice rather than undefined. On top of that you have the issue that we are technically parsing LLVM and not C directly, and so it makes sense to take LLVM semantics into account. For LLVM, empty structs are not an issue it seems.

[ThomasHaas]

[...] @ThomasHaas could you add this case to AggregateTypeTest?

will do.