Migrate to Goblint CIL

[mbyzhang]

No description provided.

[mbyzhang]

WIP: currently the CI fails (perhaps due to CIL/OCaml dependencies not correctly specified). I'll try to fix later today.

[mbyzhang]

@stephenrkell I can't reproduce the CI failure locally. Any ideas?

In my local run

$ cd tests && make checkrun-lib-test
Initially CFLAGS is  and CPPFLAGS is -I/home/peter/liballocs/contrib/liballocstool/contrib/dwarfidl/contrib/libantlr3c/include -I/home/peter/liballocs/contrib/liballocstool/contrib/dwarfidl/contrib/libantlr3c/
CIL_INSTALL is /home/peter/liballocs/contrib/../lib/ocaml/lib/goblint-cil/
appending -I/home/peter/liballocs/contrib/libsystrap/contrib/librunt/include -I/home/peter/liballocs/contrib/libmallochooks/include -I/home/peter/liballocs/contrib/liballocstool/include
lib-test            		expected: exit-zero 	PASS

[difcsi]

I think the makefile should mkdir -p instead

[difcsi]

Thanks for the PR! This would be really nice to have, indeed. I believe we all run into relatively frequent CIL errors.
Couldn't reproduce the error locally, will ask Stephen to rerun CI as the logs are now lost!

One thing with the PR, though: Wouldn't setting up an opam env be easier to maintain? There is no need to rely on aptitude for oOCamlpackages (which is quite unreliable), and we could more easily pin OCaml versions if we build CIL in an opam switch env. The dune submodule is also droppable that way!

I already built liballocs that way on my local, happy to send a PR to your PR to add that instead. Though there may be a reason for the current approach I am unaware of, so please let me know your thoughts!

[mbyzhang]

Thanks for the PR! This would be really nice to have, indeed. I believe we all run into relatively frequent CIL errors. Couldn't reproduce the error locally, will ask Stephen to rerun CI as the logs are now lost!

One thing with the PR, though: Wouldn't setting up an opam env be easier to maintain? There is no need to rely on aptitude for oOCamlpackages (which is quite unreliable), and we could more easily pin OCaml versions if we build CIL in an opam switch env. The dune submodule is also droppable that way!

I already built liballocs that way on my local, happy to send a PR to your PR to add that instead. Though there may be a reason for the current approach I am unaware of, so please let me know your thoughts!

Thanks for your comment! I agree that setting up an opam env would be a good idea (plus it makes installing language servers easier which facilitates development), so PRs are welcome!

I had the same discussion with Stephen earlier and he is also open to switching to opam if we can make it clean.

[difcsi]

Thanks for the PR! This would be really nice to have, indeed. I believe we all run into relatively frequent CIL errors. Couldn't reproduce the error locally, will ask Stephen to rerun CI as the logs are now lost!
One thing with the PR, though: Wouldn't setting up an opam env be easier to maintain? There is no need to rely on aptitude for oOCamlpackages (which is quite unreliable), and we could more easily pin OCaml versions if we build CIL in an opam switch env. The dune submodule is also droppable that way!
I already built liballocs that way on my local, happy to send a PR to your PR to add that instead. Though there may be a reason for the current approach I am unaware of, so please let me know your thoughts!

Thanks for your comment! I agree that setting up an opam env would be a good idea (plus it makes installing language servers easier which facilitates development), so PRs are welcome!

I had the same discussion with Stephen earlier and he is also open to switching to opam if we can make it clean.

Great! Will send a PR to your PR, once I finish working with #179

[difcsi]

I think we should rather have opam init as a build step, and only have dune build within the project make path. See:
https://github.com/difcsi/liballocs/blob/master/.github/workflows/ci.yml

[mbyzhang]

This would require non-CI users of liballocs to run opam init first, and their opam config might have unintended effects on Goblint CIL build?

[mbyzhang]

Unfortunately the latest changes in upstream liballocs master branch (about switching from gcc-10 to gcc-13) broke most of the test cases.

The reason is that CIL has trouble handling duplicated extern function declarations, which is used in gcc-13’s stdlib.h.

The following code (found in gcc-13's stdlib.h after preprocessing)

extern void *reallocarray (void *__ptr, size_t __nmemb, size_t __size)
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__warn_unused_result__))
     __attribute__ ((__alloc_size__ (2, 3)))
    __attribute__ ((__malloc__ (__builtin_free, 1)));


extern void *reallocarray (void *__ptr, size_t __nmemb, size_t __size)
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__ (reallocarray, 1)));

is transformed by CIL to

extern  __attribute__((__nothrow__)) void *( __attribute__((__warn_unused_result__,
__leaf__)) reallocarray)(void *__ptr , size_t __nmemb , size_t __size )  __attribute__((__malloc__(__builtin_free,1),
__malloc__(reallocarray,1), __alloc_size__(2,3))) ;

Then GCC is complaining about reallocarray in __malloc__(reallocarray,1) is not declared.

It seems like this issue doesn't exist in SRK CIL. It seems to be fixed by stephenrkell/cil@e563c01

[stephenrkell]

I think we may just need to cherry-pick something from my CIL. In issue #101 I think I found that I had fixed this in my CIL (and then forgotten all about it).

[difcsi]

I am working on porting this to Goblint at the moment, see #190