[CIL] Issue Tracker for porting SRK CIL's fixes to Goblint CIL

[difcsi]

I've looked through all the commits on our CIL fork since diverging from upstream, to see what needs to be ported to retain all of our functionality when using goblint CIL.

Importantly, the comparison branch is my fork of Peter's fork Tom's fork of Goblint-CIL, which already has some changes, that are not listed here

This really should live in our CIL's repo, but there is no issue tracker there

There are some more complex features added that warrant more explanation than their original commit message.

Support for ISO/IEC 'interchange and extended' floating-point types.

This needs to be reimplemented at Goblint CIL's version, which is based on their int128 and complexes. Fairly straightforward

• [ x ] caab1d2ed2aef322f807e3c1b60c62c23ddf94e2

Extern Inline

There is a lot of work in our branch to handle inlining better.

• Extern inline handling needs to be ported

Commits

Feat:

• d5b9293
• bf49a98
• 3a61d45
• 44f03ad
• 2c9fcf4
• e563c01
• d711287
• bb71350d56d9ae7f76a9296009dee1af7a1012bc
• 3d36c277185a056822aa79c8b88da5183d9109bf
• d7b3171295884c781c45ba90b21f716aba7f59c1

Documentation:

• 3c7ad39

Test case:

• a9f7012

Alias handling

Previously, CIL's handling of gcc's alias attribute was broken. It would
Create a new function, rather than a linker alias, and it would not work
for varargs functions or any kind of variable.

In Goblint, alias-attributed declarations are represented as GVarDecl (a declaration/prototype node) with the alias attribute preserved on the varinfo — rather than generating a new GFun (a full function definition). See the test:

goblint / cil / test / small1 / typeof1.c

Porting variadic aliases is needed, though, which lives in two commits:

• 49662e7
• 6a29ca6

Minor Things

This subsection is a sink of one-commit fixes that are yet to be ported. Most should be cherry-pickable

• 3c37b44
• 5cf9f2d
• b5f0728
• bacc20b
• 0b2fbce
• a7627ce Goblint CIL has conflicting work
• c90a760
• 229e5fc
• 0670a0a
• 42c35a2
• 8127b45
• bf1b61e
• 0abff3fa96b2b87842003ef8787c08c4aa7c94f9
• 4985d444980a78c6c8233655b323f5d5ab3ea42b
• 31bad1a1adf78921f1f32f4403e94668d73d0ee7

Wontfix

• d41c601e407eba9317d913569c7765ff3ec32d66 Goblint Conflict potential
  • This was added to support static assert but goblint already does that
• 8de3105
  • This commit is merely a log output change
• 6dc5bcf7875cad35961721a67b9dc265bfe7278f
  • Turns out this was fixed by goblint already after all
• a570678157a198dec97f25beecd28d5be633e9b0
  5e430e83e2ca8707070838a1a2993d221d82855b

[difcsi]

There is a commit pushing this test case:

https://www.humprog.org/~stephen/blog/devel/understanding-c99-inlines.html

All commits try to make that pass

[difcsi]

Please see
difcsi/cil#3

[difcsi]

@stephenrkell Could you please make a branch on your CIL by pushing the contents of https://github.com/goblint/cil 's develop branch (much like your goblint-extinlinefix (we can't use that one as doing so will mess up the pending PR you made to goblint) ) ?

I'll then make a pull request identical to (difcsi/cil#3) that will bring our fixes to a repository owned by you. @mbyzhang then could redirect the submodule link in the PR #183 to use that branch

[mbyzhang]

@difcsi Do you think you should rebase your changes onto my newer clang-support branch: https://github.com/mbyzhangAlt/cil/commits/clang-support/ ? This branch contains dynamic compiler model detection commits (which may or may not be liked by Goblint), plus everything in my dev branch rebased.

Thanks!

[difcsi]

@mbyzhang Hmm, my branch diverges from Goblint at a later date than yours. Can you rebase your branch on mine instead? I'll then pull your commits into my branch. I've tried rebasing, but there are some conflicts in areas where you are certainly more familiar with code than me

[difcsi]

On second thought, probably the clang stuff should live separately. These are mostly bugfixes, so should be upstreamable to Goblint without any trouble. Though liballocs should use that branch as it needs to. Rebasing your branch on mine would be the best solution I think.

I'm working on fixing the inlining stuff, which is your blocker right now. I think I had enough of it for today, but I'll try to get it done by EOW. See the branch goblint-inlining on my branch, unfortunately there is some regression with tests I still need to sort out

[mbyzhang]

On second thought, probably the clang stuff should live separately. These are mostly bugfixes, so should be upstreamable to Goblint without any trouble. Though liballocs should use that branch as it needs to. Rebasing your branch on mine would be the best solution I think.

Actually, your goblint dev branch is already basing on my older commits from my dev branch, starting from difcsi/cil@1ebc093. My commits in newer clang-support should replace these commits. I can definitely help with that, if that sounds good to you?

BTW, my clang-support has commits that supersede SRK's difcsi/cil@7ff39f1, so this should not be included after the rebase.

I'm working on fixing the inlining stuff, which is your blocker right now. I think I had enough of it for today, but I'll try to get it done by EOW. See the branch goblint-inlining on my branch, unfortunately there is some regression with tests I still need to sort out

Thanks! I don't need them urgently so there is no need to hurry at all.

[mbyzhang]

I've fixed issues with CI and rebased your goblint branch (before your wip commit: difcsi/cil@caa986a) onto my clang-support: check out https://github.com/mbyzhangAlt/cil/tree/zoltan-port-over-clang-support

I see that your wip commit tries to add a new _Float128x type. Should I try to rebase that as well? If you want to do that, have a look at mbyzhangAlt/cil@30397ff for reference on adding new types with the new dynamic compiler model mechanism.

Thanks

[difcsi]

Hi,

Thanks for the rebase! I'll rebase my inlining work on that shortly.

My WiP commit is a port of stephenrkell/cil@caab1d2

Though I see no point in porting that if you are reworking how the types are handled! I'll skip that for now, pull your rebase into my branch and work on the inlining. It would be great could please take a look at supporting float[16,32,64,128][_,x], as these are the two things SRK CIL did that goblint doesn't, or at least does it differently.

W.R.T the self referential attributes that are blocking you, I'm happy to expedite that and fix just that. But given that inlining is somewhat broken too (although not as much as original CIL), I presently have these fixes together (still haven't looked much into the gnu89 regression, but on it)

[mbyzhang]

Hi,

It seems like features introduced in stephenrkell/cil@caab1d2 are already supported by the upstream, except for the short float and _Float128x types. short float is non-standard C and no mainstream compilers (GCC and Clang) seem to support it, and _Float128x is not supported on today's hardware: "GCC does not currently support _Float128x on any systems." [1] So there is not much point supporting them today.

Note that the Goblint upstream handles _Float{32,64}{x,} differently from stephenrkell/cil@caab1d2. The upstream tries match and replace them with conventional floating types [2], whereas stephenrkell/cil@caab1d2 emits _Float{32,64}{x,} as is. This can be problematic when _Float{32,64}x are distinct types, e.g. on 32-bit x86, _Float64x is a unique 80-bit extended-precision format [3]. I think fixing this is left for future work, as 32-bit x86 is pretty much obsolete.

So I think the conclusion here is to drop stephenrkell/cil@caab1d2 completely. Let me know if you have any thoughts.

Thanks.

[1] https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
[2] mbyzhangAlt/cil@4436237#diff-ded244e1032a1d7ef47ebce532dadfa1f0c07727e2d3e70e678af36fef96299b
[3] https://en.wikipedia.org/wiki/Extended_precision#x86_extended-precision_format

[mbyzhang]

Regarding to my rebase, the drop of difcsi/cil@7ff39f1 is intentional -- it is already implemented (in a different way) in one of my nomachdep commits.

[stephenrkell]

Thanks both for the progress on this. @difcsi I am not sure if I'm too late, but there is now a goblint-develop branch of my CIL repo.

@mbyzhang I am fine with dropping stephenrkell/cil@caab1d2 but it sounds like your conclusion was actually that it was a better approach than goblint's? It is fine to defer fixing this though. I do sometimes build some stuff for 32-bit but the floating-point aspects are pretty niche.

[difcsi]

I think fixing this is left for future work, as 32-bit x86 is pretty much obsolete.

@stephenrkell: we want to keep support for it, but not urgent, so can be future work