Compilation Database support

[sim642]

From an old Slack message:

Regarding this build systems stuff, I remembered a feature CLion added at one point: compilation database. It's some generic JSON format for C/C++ compilations to list the compiled files etc from a number of different build systems. So maybe this is what we should focus on by just assuming the user has created a compilation database and let magpie extract the list of files from that. Or maybe even make Goblint directly parse compilation databases.

• CLion documentation about it: https://www.jetbrains.com/help/clion/compilation-database.html
  • CMake has the ability to output that
  • Makefiles can also somehow be converted to it with compiledb-generator directly or the cilly-like interception tool Bear: https://github.com/rizsotto/Bear
• Clang documentation about it: https://clang.llvm.org/docs/JSONCompilationDatabase.html
• Some other overview of it (lists other analysis tools that can use it): https://sarcasm.github.io/notes/dev/compilation-database.html

[sim642]

A few hints for the implementation:

• The handling of a compilation database argument should go here, like the handling of Makefile:

  analyzer/src/maingoblint.ml

  Lines 203 to 224 in e7353f7

  	(* If the first file given is a Makefile, we use it to combine files *)
  	if List.length !cFileNames >= 1 then (
  	let firstFile = List.first !cFileNames in
  	if Filename.basename firstFile = "Makefile" then (
  	let makefile = firstFile in
  	let path = Filename.dirname makefile in
  	(* make sure the Makefile exists or try to generate it *)
  	if not (Sys.file_exists makefile) then (
  	print_endline ("Given " ^ makefile ^ " does not exist!");
  	let configure = Filename.concat path "configure" in
  	if Sys.file_exists configure then (
  	print_endline ("Trying to run " ^ configure ^ " to generate Makefile");
  	let exit_code, output = MakefileUtil.exec_command ~path "./configure" in
  	print_endline (configure ^ MakefileUtil.string_of_process_status exit_code ^ ". Output: " ^ output);
  	if not (Sys.file_exists makefile) then failwith ("Running " ^ configure ^ " did not generate a Makefile - abort!")
  	) else failwith ("Could neither find given " ^ makefile ^ " nor " ^ configure ^ " - abort!")
  	);
  	let _ = MakefileUtil.run_cilly path in
  	let file = MakefileUtil.(find_file_by_suffix path comb_suffix) in
  	cFileNames := file :: (List.drop 1 !cFileNames);
  	);
  	);

• The parsing of compilation databases hopefully can all be done by just defining appropriate record types with [@@deriving of_yojson].

[stilscher]

I looked into the compilation databases, but I'm not sure whether adding support for them is very helpful in our case. The compilation databases contain so called command objects. Each specifies a command, and as far as I found, the commands do not fulfill any further requirements. When generating this compilation database with CMake, a command is usually a call to the compiler used by CMake.
For the preprocessing, parsing to CIL, compilation and so on, we use cilly which behaves like a compiler and is also used to merge all relevant files. For supporting a compilation database, it would require that cilly was specified as compiler when generating it. One would need to find a way to generate the cilly-specific compilation databases with different build tools or transform one into a cilly-based one.
So one could maybe instead just try to directly generate the Makefile which we already support (CMake can generate Makefiles in general, but I 'm still trying to get it to work with cilly). Also, adding support in Goblint for projects build with autotools seems to be rather simple.

[sim642]

We don't have to use the commands though, but just get the list of all files in the project into the cFileNames list for preprocessing and merging inside Goblint. That's already there, but one just has to manually list all the files as arguments, which is nonsense.

[sim642]

Although getting just the list of files to be analyzed together is the basic case, which might not be enough for most real-world projects, which pass preprocessing options as arguments to the compiler.

When generating this compilation database with CMake, a command is usually a call to the compiler used by CMake.

Therefore we would probably want to use these commands (calls to gcc, we don't support other compilers anyway) and add the -E argument to just preprocess (just like the project wants) instead of fully compiling. This preprocessing would be to temporary files (just like it already happens in Goblint) and those would be merged with the Mergecil module (just like it already happens in Goblint).

So I don't see any need for cilly here, since it's just an outdated pretend compiler for collecting the list of files, preprocessing them and merging them — all the same stuff. If we keep cilly as a central part of analyzing real-world projects, this won't get us any further than we already are, as far as I understand, because cilly supposedly cannot handle almost all real-world projects.

The hope for compilation databases would be to get rid of this unmaintained pseudo-compiler hack that's holding us back and switch to a modern better-supported mechanism that's specially designed for external tooling to work with the complexity C projects.