Add Compilation Database support

src/analyses/contain.ml

@@ -79,7 +79,7 @@ struct
       Hashtbl.replace htbl cn xs
     in (*read CXX.json; FIXME: use mangled names including namespaces*)
     let json=
-      match List.filter (fun x -> Str.string_match (Str.regexp ".*CXX\\.json$") x 0) !Goblintutil.jsonFiles with
+      match List.filter (fun x -> Filename.check_suffix x "CXX.json") !Goblintutil.arg_files with
       | [] -> failwith "Containment analysis needs a CXX.json file."
       | f :: _ ->
         begin
@@ -100,7 +100,7 @@ struct
         end
     in (*read in SAFE.json, suppress warnings for safe funs/vars*)
     json;
-    match List.filter (fun x -> Str.string_match (Str.regexp ".*SAFE\\.json$") x 0) !Goblintutil.jsonFiles with
+    match List.filter (fun x -> Filename.check_suffix x "SAFE.json") !Goblintutil.arg_files with
     | [] -> ()
     | f :: _ ->
       try

src/incremental/makefileUtil.ml

@@ -27,10 +27,6 @@ let exec_command ?path (command: string) =
     Sys.chdir current_dir;
     (exit_code, output)
 
-let string_of_process_status = function
-  | WEXITED n -> "terminated with exit code " ^ string_of_int n
-  | WSIGNALED n -> "was killed by signal " ^ string_of_int n
-  | WSTOPPED n -> "was stopped by signal " ^ string_of_int n
 
 (* BFS for a file with a given suffix in a directory or any subdirectoy *)
 let find_file_by_suffix (dir: string) (file_name_suffix: string) =
@@ -47,23 +43,49 @@ let find_file_by_suffix (dir: string) (file_name_suffix: string) =
   in
   search dir (list_files dir)
 
+(* Delete all *_comb.c files in the directory *)
+let remove_comb_files path =
+  try
+    while true do
+      let comb = find_file_by_suffix path comb_suffix in
+      if GobConfig.get_bool "dbg.verbose" then print_endline ("deleting " ^ comb);
+      Sys.remove comb;
+    done
+  with Failure e -> ()
+
 let run_cilly (path: string) =
   if Sys.file_exists path && Sys.is_directory path then (
     (* We need to `make clean` if `make` was run manually, otherwise it would say there is nothing to do and cilly would not be run and no combined C file would be created. *)
     let _ = exec_command ~path "make clean" in
-    (try
-       while true do
-         let comb = find_file_by_suffix path comb_suffix in
-         if GobConfig.get_bool "dbg.verbose" then print_endline ("deleting " ^ comb);
-         Sys.remove comb;
-       done
-     with Failure e -> ()); (* Deleted all *_comb.c files in the directory *)
+    remove_comb_files path;
     (* Combine source files with make using cilly as compiler *)
     let gcc_path = GobConfig.get_string "exp.gcc_path" in
     let (exit_code, output) = exec_command ~path ("make CC=\"cilly --gcc=" ^ gcc_path ^ " --merge --keepmerged\" " ^
                                                   "LD=\"cilly --gcc=" ^ gcc_path ^ " --merge --keepmerged\"") in
     print_string output;
     (* fail if make failed *)
     if exit_code <> WEXITED 0 then
-      failwith ("Failed combining files. Make " ^ (string_of_process_status exit_code) ^ ".")
+      failwith ("Failed combining files. Make was " ^ (GobUnix.string_of_process_status exit_code) ^ ".")
   )
+
+let generate_and_combine makefile =
+  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! Try to generate it.");
+    let configure = ("configure", "./configure", Filename.concat path "configure") in
+    let autogen = ("autogen", "sh autogen.sh && ./configure", Filename.concat path "autogen.sh") in
+    let exception MakefileNotGenerated in
+    let generate_makefile_with (name, command, file) = if Sys.file_exists file then (
+        print_endline ("Trying to run " ^ name ^ " to generate Makefile");
+        let exit_code, output = exec_command ~path command in
+        print_endline (command ^ GobUnix.string_of_process_status exit_code ^ ". Output: " ^ output);
+        if not (Sys.file_exists makefile) then raise MakefileNotGenerated
+      ); raise MakefileNotGenerated in
+    try generate_makefile_with configure
+    with MakefileNotGenerated ->
+    try generate_makefile_with autogen
+    with MakefileNotGenerated -> failwith ("Could neither find given " ^ makefile ^ " nor generate it - abort!");
+  );
+  run_cilly path;
+  find_file_by_suffix path comb_suffix

src/maingoblint.ml

@@ -119,18 +119,14 @@ let option_spec_list =
   ; "--osekids"            , Arg.Set_string OilUtil.osek_ids, ""
   ]
 
-(** List of C files to consider. *)
-let cFileNames = ref []
 
-(** Parse arguments and fill [cFileNames] and [jsonFiles]. Print help if needed. *)
+(** Parse arguments and fill [arg_files]. Print help if needed. *)
 let parse_arguments () =
-  let jsonRegex = Str.regexp ".+\\.json$" in
-  let recordFile fname =
-    if Str.string_match jsonRegex fname 0
-    then Goblintutil.jsonFiles := fname :: !Goblintutil.jsonFiles
-    else cFileNames := fname :: !cFileNames
+  let anon_arg filename =
+    arg_files := filename :: !arg_files
   in
-  Arg.parse option_spec_list recordFile "Look up options using 'goblint --help'.";
+  Arg.parse option_spec_list anon_arg "Look up options using 'goblint --help'.";
+  arg_files := List.rev !arg_files; (* reverse files to get given order *)
   if !writeconffile <> "" then (GobConfig.write_file !writeconffile; raise Exit)
 
 (** Initialize some globals in other modules. *)
@@ -151,15 +147,15 @@ let handle_flags () =
     set_string "outfile" ""
 
 (** Use gcc to preprocess a file. Returns the path to the preprocessed file. *)
-let preprocess_one_file cppflags fname =
+let basic_preprocess ~all_cppflags fname =
   (* The actual filename of the preprocessed sourcefile *)
   let nname =  Filename.concat !Goblintutil.tempDirName (Filename.basename fname) in
   if Sys.file_exists (get_string "tempDir") then
     nname
   else
     (* Preprocess using cpp. *)
     (* ?? what is __BLOCKS__? is it ok to just undef? this? http://en.wikipedia.org/wiki/Blocks_(C_language_extension) *)
-    let command = Config.cpp ^ " --undef __BLOCKS__ " ^ cppflags ^ " \"" ^ fname ^ "\" -o \"" ^ nname ^ "\"" in
+    let command = Config.cpp ^ " --undef __BLOCKS__ " ^ String.join " " (List.map Filename.quote all_cppflags) ^ " \"" ^ fname ^ "\" -o \"" ^ nname ^ "\"" in
     if get_bool "dbg.verbose" then print_endline command;
 
     (* if something goes wrong, we need to clean up and exit *)
@@ -173,7 +169,7 @@ let preprocess_one_file cppflags fname =
 (** Preprocess all files. Return list of preprocessed files and the temp directory name. *)
 let preprocess_files () =
   (* Preprocessor flags *)
-  let cppflags = ref (get_string "cppflags") in
+  let cppflags = ref (get_string_list "cppflags") in
 
   (* the base include directory *)
   let custom_include_dirs =
@@ -213,37 +209,6 @@ let preprocess_files () =
 
   include_dirs := custom_include_dirs @ !include_dirs;
 
-  (* reverse the files again *)
-  cFileNames := List.rev !cFileNames;
-
-  (* If the first file given is a Makefile, we use it to combine files *)
-  if !cFileNames <> [] 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);
-    );
-  );
-
-  cFileNames := find_custom_include "stdlib.c" :: !cFileNames;
-
-  if get_bool "ana.sv-comp.functions" then
-    cFileNames := find_custom_include "sv-comp.c" :: !cFileNames;
-
   (* If we analyze a kernel module, some special includes are needed. *)
   if get_bool "kernel" then (
     let kernel_roots = [
@@ -261,7 +226,7 @@ let preprocess_files () =
 
     let preconf = find_custom_include "linux/goblint_preconf.h" in
     let autoconf = Filename.concat kernel_dir "linux/kconfig.h" in
-    cppflags := "-D__KERNEL__ -U__i386__ -D__x86_64__ " ^ !cppflags;
+    cppflags := "-D__KERNEL__" :: "-U__i386__" :: "-D__x86_64__" :: !cppflags;
     include_files := preconf :: autoconf :: !include_files;
     (* These are not just random permutations of directories, but based on USERINCLUDE from the
      * Linux kernel Makefile (in the root directory of the kernel distribution). *)
@@ -271,17 +236,48 @@ let preprocess_files () =
       ]
   );
 
-  let includes =
-    String.join " " (List.map (fun include_dir -> "-I " ^ include_dir) !include_dirs) ^
-    " " ^
-    String.join " " (List.map (fun include_file -> "-include " ^ include_file) !include_files)
+  let include_args =
+    List.flatten (List.map (fun include_dir -> ["-I"; include_dir]) !include_dirs) @
+    List.flatten (List.map (fun include_file -> ["-include"; include_file]) !include_files)
   in
 
-  let cppflags = !cppflags ^ " " ^ includes in
+  let all_cppflags = !cppflags @ include_args in
 
   (* preprocess all the files *)
   if get_bool "dbg.verbose" then print_endline "Preprocessing files.";
-  List.rev_map (preprocess_one_file cppflags) !cFileNames
+
+  let rec preprocess_arg_file = function
+    | filename when Filename.basename filename = "Makefile" ->
+      let comb_file = MakefileUtil.generate_and_combine filename in
+      [basic_preprocess ~all_cppflags comb_file]
+
+    | filename when Filename.basename filename = CompilationDatabase.basename ->
+      CompilationDatabase.load_and_preprocess ~all_cppflags filename
+
+    | filename when Sys.is_directory filename ->
+      let dir_files = Sys.readdir filename in
+      if Array.mem CompilationDatabase.basename dir_files then (* prefer compilation database to Makefile in case both exist, because compilation database is more robust *)
+        preprocess_arg_file (Filename.concat filename CompilationDatabase.basename)
+      else if Array.mem "Makefile" dir_files then
+        preprocess_arg_file (Filename.concat filename "Makefile")
+      else
+        [] (* don't recurse for anything else *)
+
+    | filename when Filename.extension filename = ".json" ->
+      [] (* ignore other JSON files for contain analysis *)
+
+    | filename ->
+      [basic_preprocess ~all_cppflags filename]
+  in
+
+  let extra_arg_files = ref [] in
+
+  extra_arg_files := find_custom_include "stdlib.c" :: !extra_arg_files;
+
+  if get_bool "ana.sv-comp.functions" then
+    extra_arg_files := find_custom_include "sv-comp.c" :: !extra_arg_files;
+
+  List.flatten (List.map preprocess_arg_file (!extra_arg_files @ !arg_files))
 
 (** Possibly merge all postprocessed files *)
 let merge_preprocessed cpp_file_names =

src/util/compilationDatabase.ml

@@ -0,0 +1,74 @@
+open Prelude
+
+let basename = "compile_commands.json"
+
+type command_object = {
+  directory: string;
+  file: string;
+  command: string option [@default None];
+  arguments: string list option [@default None];
+  output: string option [@default None];
+} [@@deriving yojson]
+
+type t = command_object list [@@deriving yojson]
+
+let parse_file filename =
+  Result.get_ok (of_yojson (Yojson.Safe.from_file filename))
+
+let command_o_regexp = Str.regexp "-o +[^ ]+"
+let command_program_regexp = Str.regexp "^ *\\([^ ]+\\)"
+
+let system ~cwd command =
+  let old_cwd = Sys.getcwd () in
+  Fun.protect ~finally:(fun () ->
+      Sys.chdir old_cwd
+    ) (fun () ->
+      Sys.chdir cwd;
+      match Unix.system command with
+      | WEXITED 0 -> ()
+      | process_status -> failwith (GobUnix.string_of_process_status process_status)
+    )
+
+let load_and_preprocess ~all_cppflags filename =
+  let database_dir = Filename.dirname (GobFilename.absolute filename) in (* absolute before dirname to avoid . *)
+  (* TODO: generalize .goblint for everything *)
+  ignore (Goblintutil.create_dir ".goblint");
+  let preprocessed_dir = Goblintutil.create_dir (Filename.concat ".goblint" "preprocessed") in
+  let preprocess obj =
+    let file = obj.file in
+    let preprocessed_file = Filename.concat preprocessed_dir (Filename.chop_extension (GobFilename.chop_common_prefix database_dir file) ^ ".i") in
+    GobSys.mkdir_parents preprocessed_file;
+    let preprocess_command = match obj.command, obj.arguments with
+      | Some command, None ->
+        (* TODO: extract o_file *)
+        let preprocess_command = Str.replace_first command_program_regexp ("\\1 " ^ String.join " " (List.map Filename.quote all_cppflags) ^ " -E") command in
+        let preprocess_command = Str.replace_first command_o_regexp ("-o " ^ preprocessed_file) preprocess_command in
+        if preprocess_command = command then (* easier way to check if match was found (and replaced) *)
+          failwith "CompilationDatabase.preprocess: no -o argument found for " ^ file
+        else
+          preprocess_command
+      | None, Some arguments ->
+        begin match List.findi (fun i e -> e = "-o") arguments with
+          | (o_i, _) ->
+            begin match List.split_at o_i arguments with
+              | (arguments_program :: arguments_init, _ :: o_file :: arguments_tl) ->
+                let preprocess_arguments = arguments_program :: all_cppflags @ "-E" :: arguments_init @ "-o" :: preprocessed_file :: arguments_tl in
+                String.join " " (List.map Filename.quote preprocess_arguments) (* TODO: use quote_command after OCaml 4.10 *)
+              | _ ->
+                failwith "CompilationDatabase.preprocess: no -o argument value found for " ^ file
+            end
+          | exception Not_found ->
+            failwith "CompilationDatabase.preprocess: no -o argument found for " ^ file
+        end
+      | Some _, Some _ ->
+        failwith "CompilationDatabase.preprocess: both command and arguments specified for " ^ file
+      | None, None ->
+        failwith "CompilationDatabase.preprocess: neither command nor arguments specified for " ^ file
+    in
+    if GobConfig.get_bool "dbg.verbose" then
+      Printf.printf "Preprocessing %s\n  to %s\n  using %s\n  in %s\n" file preprocessed_file preprocess_command obj.directory;
+    system ~cwd:obj.directory preprocess_command; (* command/arguments might have paths relative to directory *)
+    preprocessed_file
+  in
+  parse_file filename
+  |> List.map preprocess

src/util/defaults.ml

@@ -73,7 +73,7 @@ let _ = ()
       ; reg Std "allglobs"        "false"        "Prints access information about all globals, not just races."
       ; reg Std "keepcpp"         "false"        "Keep the intermediate output of running the C preprocessor."
       ; reg Std "tempDir"         "''"           "Reuse temporary directory for preprocessed files."
-      ; reg Std "cppflags"        "''"           "Pre-processing parameters."
+      ; reg Std "cppflags"        "[]"           "Pre-processing parameters."
       ; reg Std "kernel"          "false"        "For analyzing Linux Device Drivers."
       ; reg Std "dump_globs"      "false"        "Print out the global invariant."
       ; reg Std "result"          "'none'"       "Result style: none, fast_xml, json, mongo, pretty, json-messages."

src/util/gobFilename.ml

@@ -0,0 +1,40 @@
+open Prelude
+
+(** Make path absolute, if relative. *)
+let absolute filename =
+  if Filename.is_relative filename then
+    Filename.concat (Unix.getcwd ()) filename
+  else
+    filename
+
+let chop_prefix ~prefix filename =
+  let prefix =
+    if String.ends_with prefix Filename.dir_sep then
+      prefix
+    else
+      prefix ^ Filename.dir_sep
+  in
+  if String.starts_with filename prefix then
+    String.lchop ~n:(String.length prefix) filename
+  else
+    raise (Invalid_argument "GobFilename.chop_prefix: doesn't start with given prefix")
+
+let common_prefix filename1 filename2 =
+  let common_prefix_length s1 s2 =
+    let l1 = String.length s1 in
+    let l2 = String.length s2 in
+    let rec common_prefix_length' i =
+      if i >= l1 || i >= l2 then
+        i
+      else if s1.[i] = s2.[i] then
+        common_prefix_length' (i + 1)
+      else
+        i
+    in
+    common_prefix_length' 0
+  in
+  String.left filename1 (common_prefix_length filename1 filename2)
+
+let chop_common_prefix filename1 filename2 =
+  let filename2 = absolute filename2 in
+  chop_prefix ~prefix:(common_prefix (absolute filename1) filename2) filename2

src/util/gobSys.ml

@@ -0,0 +1,8 @@
+open Prelude
+
+let rec mkdir_parents filename =
+  let dirname = Filename.dirname filename in
+  if not (Sys.file_exists dirname) then (
+    mkdir_parents dirname;
+    Unix.mkdir dirname 0o770; (* TODO: what permissions? *)
+  )

src/util/gobUnix.ml

@@ -0,0 +1,7 @@
+open Prelude
+open Unix
+
+let string_of_process_status = function
+  | WEXITED n -> "terminated with exit code " ^ string_of_int n
+  | WSIGNALED n -> "killed by signal " ^ string_of_int n
+  | WSTOPPED n -> "stopped by signal " ^ string_of_int n

src/util/goblintutil.ml

@@ -7,8 +7,8 @@ open GobConfig
 (** Outputs information about what the goblin is doing *)
 (* let verbose = ref false *)
 
-(** Json files that are given as arguments *)
-let jsonFiles : string list ref = ref []
+(** Files given as arguments. *)
+let arg_files : string list ref = ref []
 
 (** If this is true we output messages and collect accesses.
     This is set to true in control.ml before we verify the result (or already before solving if warn = 'early') *)