goblint / goblint/analyzer

Crash with `pre.compdb.original-path`

Open
#730 0 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

preprocessing
Dominant language
OCaml
Stars
252
Forks
90
Avg merge
4d 1m
Merged PRs (30d)
19

Description

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.

Contributor guide

No contributing guide indexed for this repository

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Research direction

Start by locating the handling of pre.compdb.original-path and the path rerooting code, then compare it with the #642 rem_find_prefix change. Reproduce the two database locations and inspect Fpath.relativize and Fpath.rem_empty_seg; done means rerooting no longer crashes or produces invalid paths, with the relative command-argument limitation understood.

Written by the indexing model from the issue text.

Assessment

Tech stack
c, ocaml
Domain
build-system, tooling
Issue type
Bug
Difficulty
4/5
Estimated time
3-5 days
Activity status
Stale
Clarity
Mostly clear
Newbie friendliness
35/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.