feature request: Support getting compile flags from compile_commands.json

[archigup]

Clang-based linting tooling, such as clangd, often use the compile_commands.json file for determining what compilation flags to use. Its also used by editors like vscode for linting files.

This file is generated by build systems like CMake or by tools like Bear. Information/rationale on the format is here: https://clang.llvm.org/docs/JSONCompilationDatabase.html

CBMC tooling could use a compilation database to determine the flags needed for goto-cc.

For example, the iwyu include linter provides a wrapper that pulls flags from compile_commands.json, given an argument pointing to the build dir. The same approach could be used here by providing a goto-cc wrapper.

For the user experience for this, assuming the user has a project where they are already using a compile_commands.json for other tooling, this would let them type something like goto-cc-compdb -b build src/test.c which would look up src/test.c in build/compile_commands.json and use the relevant flags from there to call goto-cc, placing the result in a default location derived from the compilation db. The option to pass specific source files to use is needed to test one file at a time or to skip files from dependencies.

If not passed a source file, this could build each source files in the compilation db.

If passed an output path (maybe like goto-cc-compdb -b build -o merged.goto), it could perform the link of all the inputs' resulting goto files into the combined goto file for use with goto-instrument or cmbc.

Additionally, it should either add a -D__CPROVER__=1 flag or allow adding additional defines.

Here is a snippet of one of my compile_commands.json from aws-greengrass-sdk-lite:

{
  "directory": "/home/ANT.AMAZON.COM/archigup/projects/ggl/aws-greengrass-sdk-lite/build",
  "command": "/nix/store/f0m6caffiykyvsjim9376a3hx2yj2ghj-gcc-wrapper-14.2.1.20250322/bin/gcc -DGGL_LOG_LEVEL=GGL_LOG_TRACE -DGGL_MODULE=\"(\\\"ggl-sdk\\\")\" -D_GNU_SOURCE -I/home/ANT.AMAZON.COM/archigup/projects/ggl/aws-greengrass-sdk-lite/include -I/home/ANT.AMAZON.COM/archigup/projects/ggl/aws-greengrass-sdk-lite/priv_include -fdiagnostics-color=always -O0 -ggdb3 -pthread -fno-strict-aliasing -std=gnu11 -fvisibility=hidden -fno-semantic-interposition -fno-common -fno-unwind-tables -fno-asynchronous-unwind-tables -fstrict-flex-arrays=3 -fmacro-prefix-map=/home/ANT.AMAZON.COM/archigup/projects/ggl/aws-greengrass-sdk-lite/= -fno-omit-frame-pointer -ftrivial-auto-var-init=pattern -Werror -Wall -Wextra -Wwrite-strings -Wno-missing-braces -Wvla -Wshadow -Wformat -Wformat=2 -Wmissing-prototypes -Wstrict-prototypes -Wold-style-definition -Wunused -Wundef -Wconversion -Wsign-conversion -Wimplicit-fallthrough -Wredundant-decls -Wdate-time -Wstack-protector -Wenum-int-mismatch -Wtrampolines -Wbidi-chars=any,ucn -Werror=format-security -Werror=implicit -Werror=incompatible-pointer-types -Werror=int-conversion -frandom-seed=/home/ANT.AMAZON.COM/archigup/projects/ggl/aws-greengrass-sdk-lite/src/arena.c -o CMakeFiles/ggl-sdk.dir/src/arena.c.o -c /home/ANT.AMAZON.COM/archigup/projects/ggl/aws-greengrass-sdk-lite/src/arena.c",
  "file": "/home/ANT.AMAZON.COM/archigup/projects/ggl/aws-greengrass-sdk-lite/src/arena.c",
  "output": "CMakeFiles/ggl-sdk.dir/src/arena.c.o"
},

With a compilation db with the above entry, and keeping all the flags, the goto-cc command would be:

goto-cc -DGGL_LOG_LEVEL=GGL_LOG_TRACE -DGGL_MODULE="(\"ggl-sdk\")" -D_GNU_SOURCE -I/home/ANT.AMAZON.COM/archigup/projects/ggl/aws-greengrass-sdk-lite/include -I/home/ANT.AMAZON.COM/archigup/projects/ggl/aws-greengrass-sdk-lite/priv_include -fdiagnostics-color=always -O0 -ggdb3 -pthread -fno-strict-aliasing -std=gnu11 -fvisibility=hidden -fno-semantic-interposition -fno-common -fno-unwind-tables -fno-asynchronous-unwind-tables -fstrict-flex-arrays=3 -fmacro-prefix-map=/home/ANT.AMAZON.COM/archigup/projects/ggl/aws-greengrass-sdk-lite/= -fno-omit-frame-pointer -ftrivial-auto-var-init=pattern -Werror -Wall -Wextra -Wwrite-strings -Wno-missing-braces -Wvla -Wshadow -Wformat -Wformat=2 -Wmissing-prototypes -Wstrict-prototypes -Wold-style-definition -Wunused -Wundef -Wconversion -Wsign-conversion -Wimplicit-fallthrough -Wredundant-decls -Wdate-time -Wstack-protector -Wenum-int-mismatch -Wtrampolines -Wbidi-chars=any,ucn -Werror=format-security -Werror=implicit -Werror=incompatible-pointer-types -Werror=int-conversion -frandom-seed=/home/ANT.AMAZON.COM/archigup/projects/ggl/aws-greengrass-sdk-lite/src/arena.c -o CMakeFiles/ggl-sdk.dir/src/arena.c.goto -c /home/ANT.AMAZON.COM/archigup/projects/ggl/aws-greengrass-sdk-lite/src/arena.c

Of course, only the flags used by goto-cc could be retained if preferred, resulting in:

goto-cc -DGGL_LOG_LEVEL=GGL_LOG_TRACE -DGGL_MODULE="(\"ggl-sdk\")" -D_GNU_SOURCE -I/home/ANT.AMAZON.COM/archigup/projects/ggl/aws-greengrass-sdk-lite/include -I/home/ANT.AMAZON.COM/archigup/projects/ggl/aws-greengrass-sdk-lite/priv_include -pthread -std=gnu11-o CMakeFiles/ggl-sdk.dir/src/arena.c.goto -c /home/ANT.AMAZON.COM/archigup/projects/ggl/aws-greengrass-sdk-lite/src/arena.c

From here, the user could link their desired goto binaries, if not already linked, and then run goto-instrument or whatever else they need (for aws-greengrass-sdk-lite, I plan to take each individual c file's goto, link just it alone, and instrument a copy for each contract with a function body available in order to check each contract).

[archigup]

Possibly also useful for #8640?