analyzer icon indicating copy to clipboard operation
analyzer copied to clipboard

Crash with `pre.compdb.original-path`

Open sim642 opened this issue 3 years ago • 0 comments

In the chrony interactive story, compile_commands.json would normally be in the chrony-4.2 git submodule, making it impossible to version the compilation database in our bench repository for better reproducibility. Compilation databases are annoying in that regard: they're not meant to be moved between systems and use absolute paths. At some point I added the pre.compdb.original-path option to try to hack around that limitation while reading the database in.

I now tried moving the compilation database on my machine from

/home/simmo/dev/goblint/sv-comp/goblint-bench/gobpie-demos/chrony/chrony-4.2/compile_commands.json

to (up one directory)

/home/simmo/dev/goblint/sv-comp/goblint-bench/gobpie-demos/chrony/compile_commands.json

Passing the first path for pre.compdb.original-path while analyzing the compilation database at the second path crashes in the path rerooting code.

Issues

There seem to be multiple issues on top of each other:

  • [ ] In #642 I screwed up replacing my custom chop_common_suffix function with rem_find_prefix based on the fpath library: https://github.com/goblint/analyzer/pull/642/commits/c555984e7753cfb76ed7d47ad54b3b704c43dff9#diff-116f7b65666b150610ed8ad3daad6e25e7b45c8972bc1e8fda2230cf395bcf48R28-R29. Other places used chop_common_prefix, so I probably didn't notice the prefix vs suffix distinction in this code.
  • [ ] Working around the first issue using
    let old_root = original_database_dir in
    let new_root = database_dir in
    
    (which would be the intended paths in this particular case anyway) leads to another problem: if both old_root and p are the same (or at least on some combination of them ending with an additional /), Fpath.relativize returns a weird ../chrony-4.2 path, which appended to the rest doesn't give a valid path.
  • [ ] The second issue seems workable around with Fpath.rem_empty_seg to normalize the trailing slashes, but there we just hit a dead end: the compilation database I have from bear 3.0.8 still has relative paths for the gcc command arguments as the files in chrony are all right in the repository root. The compilation database rerooting logic cannot really do anything about relative paths.

sim642 avatar May 06 '22 20:05 sim642