Skip to content

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

Merged
michael-schwarz merged 12 commits intomasterfrom
deps_from_cil
Feb 10, 2022
Merged

Compute dependencies of file via CIL instead of from .d files generated during pre-processing#587
michael-schwarz merged 12 commits intomasterfrom
deps_from_cil

Conversation

@michael-schwarz
Copy link
Copy Markdown
Member

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.

@michael-schwarz michael-schwarz added the cleanup Refactoring, clean-up label Feb 3, 2022
@karoliineh
Copy link
Copy Markdown
Member

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
Copy link
Copy Markdown
Member

sim642 commented Feb 3, 2022

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
Copy link
Copy Markdown
Member Author

I'll give that a shot tomorrow then.

@michael-schwarz michael-schwarz merged commit e1d65b2 into master Feb 10, 2022
@michael-schwarz michael-schwarz deleted the deps_from_cil branch February 10, 2022 15:31
@sim642 sim642 added this to the v2.0.0 milestone Aug 12, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

cleanup Refactoring, clean-up

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants