Compute dependencies of file via CIL instead of from .d files generated during pre-processing

[michael-schwarz]

This is an alternative to #535 which it reverts.

Instead of generating .d files during pre-processing and then parsing those in, we use the fact that the desired information is newly exposed by CIL as of goblint/cil#73

The hope is that this simplifies the generation of these dependencies and also makes it less fragile (as observed for #557 and goblint/bench#17).

CC: @karoliineh since this affects GobPie.

[karoliineh]

In #535 implementation the json output files object was something like:

files": {
    "/home/ubuntu/DemoProject/src/subproblems/10-nullpointer-dereference-simple.c": [
      "/home/ubuntu/DemoProject/src/subproblems/10-nullpointer-dereference-simple.h"
    ],
    "/home/ubuntu/DemoProject/src/subproblems/01-assert.c": [
      "/home/ubuntu/goblint/analyzer/_opam/share/goblint/includes/assert.h",
      "/home/ubuntu/DemoProject/src/subproblems/01-assert.h"
    ],
    "/home/ubuntu/goblint/analyzer/_opam/share/goblint/includes/stdlib.c": [],
...

now it has a ton of different stuff in it:

files": {
    "/home/ubuntu/DemoProject/src/subproblems/10-nullpointer-dereference-simple.c": [
      "/usr/include/x86_64-linux-gnu/gnu/stubs.h",
      "/usr/include/x86_64-linux-gnu/bits/types/__FILE.h",
      "/usr/include/x86_64-linux-gnu/bits/typesizes.h",
      "/usr/include/x86_64-linux-gnu/bits/types/__fpos64_t.h",
      "/usr/include/x86_64-linux-gnu/bits/types/FILE.h",
      "/home/ubuntu/DemoProject/src/subproblems/10-nullpointer-dereference-simple.c",
      "/usr/include/x86_64-linux-gnu/bits/wordsize.h",
      "/usr/include/x86_64-linux-gnu/sys/cdefs.h",
      "/usr/include/x86_64-linux-gnu/bits/types/struct_FILE.h",
      "/usr/include/stdc-predef.h", "<command-line>",
      "/usr/include/x86_64-linux-gnu/bits/long-double.h",
 ...

for GopPie, we only need to get back the list of the project files that have been sent for Goblint to be analysed (both .c and .h), so that we could track if any new files have been passed to be analysed since the last analysis. Therefore from the first implementation the ../goblint/analyzer/_opam/share/goblint/includes/stdlib.c files can be removed as well.

[sim642]

Overall, having now seen the actual outputs, I see a bunch of problems:

• Includes <built-in>.
• Includes <command-line>.
• Each file includes itself as dependency!
• System headers cannot be distinguished.

So actually, I think the reasonable thing to do would be the following:

1. Keys of the map are preprocessed files (so no orig). This would be consistent with old Makefile support, because there the preprocessed (i.e. preprocessed and combined) file would be the only key.
2. That automatically solves the self-dependency problem, because then the preprocessed file has the original as its dependency, which is completely true. And again consistent with the old Makefile support, where all the combined original files would be listed as dependencies anyway.
3. CIL should exclude <built-in> and <command-line>.
4. CIL should return (string * bool) list or (string, bool) Hashtbl.t, where the value boolean indicates whether the included file is a system one or not. It can easily know this (just like cpp -MD does) by just looking at the output line markers. The number indicates which one it is: https://gcc.gnu.org/onlinedocs/cpp/Preprocessor-Output.html#Preprocessor-Output. It would be best to rely on cpp doing it for us, rather than using some heuristics in Goblint for this purpose (e.g. guessing based on directories).

[michael-schwarz]

I'll give that a shot tomorrow then.