Merge pull request #610 from goblint/pre-refactor

Refactor preprocessing

.github/workflows/unlocked.yml

@@ -217,8 +217,8 @@ jobs:
       - name: Symlink installed goblint to repository # because tests want to use locally built one
         run: ln -s $(opam exec -- which goblint) goblint
 
-      - name: Set gobopt with kernel-root # because linux-headers are not installed
-        run: echo "gobopt=--set kernel-root $PWD/linux-headers" >> $GITHUB_ENV
+      - name: Set gobopt with pre.kernel-root # because linux-headers are not installed
+        run: echo "gobopt=--set pre.kernel-root $PWD/linux-headers" >> $GITHUB_ENV
 
       - name: Test regression
         run: ./make.sh headers testci

.gitignore

@@ -28,7 +28,7 @@ tests/regression/16-relinv/flags.json
 tests/regression/*/goblint_temp
 linux-headers
 
-.goblint/*
+.goblint*/
 goblint_temp_*/
 
 src/spec/graph

scripts/update_suite.rb

@@ -357,7 +357,7 @@ def run_testset (testset, cmd, starttime)
 
   def run
     filename = File.basename(@path)
-    cmd = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --enable dbg.print_dead_code 2>#{@testset.statsfile}"
+    cmd = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --enable dbg.print_dead_code --set goblint-dir .goblint-#{@id.sub('/','-')} 2>#{@testset.statsfile}"
     starttime = Time.now
     run_testset(@testset, cmd, starttime)
   end
@@ -418,8 +418,8 @@ def create_test_set(lines)
 
   def run
     filename = File.basename(@path)
-    cmd = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --enable dbg.print_dead_code --enable incremental.save 2>#{@testset.statsfile}"
-    cmd_incr = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset_incr.warnfile} --set printstats true --enable dbg.print_dead_code --enable incremental.load 2>#{@testset_incr.statsfile}"
+    cmd = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --enable dbg.print_dead_code --enable incremental.save --set goblint-dir .goblint-#{@id.sub('/','-')}-incr-save 2>#{@testset.statsfile}"
+    cmd_incr = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset_incr.warnfile} --set printstats true --enable dbg.print_dead_code --enable incremental.load --set goblint-dir .goblint-#{@id.sub('/','-')}-incr-load 2>#{@testset_incr.statsfile}"
     starttime = Time.now
     run_testset(@testset_incr, cmd, starttime)
     # apply patch
@@ -462,8 +462,8 @@ def create_test_set(lines)
   end
   def run ()
     filename = File.basename(@path)
-    cmd1 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --enable dbg.print_dead_code --set save_run run  2>#{@testset.statsfile}"
-    cmd2 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --enable dbg.print_dead_code --conf run/config.json --set save_run '' --set load_run run  2>#{@testset.statsfile}"
+    cmd1 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --enable dbg.print_dead_code --set save_run run --set goblint-dir .goblint-#{@id.sub('/','-')}-run-save 2>#{@testset.statsfile}"
+    cmd2 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --enable dbg.print_dead_code --conf run/config.json --set save_run '' --set load_run run --set goblint-dir .goblint-#{@id.sub('/','-')}-run-load 2>#{@testset.statsfile}"
     starttime = Time.now
     run_testset(@testset, cmd1, starttime)
     run_testset(@testset, cmd2, starttime)

src/framework/control.ml

@@ -472,7 +472,7 @@ struct
             if get_bool "dbg.verbose" then (
               print_endline ("Saving the current configuration to " ^ config ^ ", meta-data about this run to " ^ meta ^ ", and solver statistics to " ^ solver_stats);
             );
-            ignore @@ GU.create_dir (save_run); (* ensure the directory exists *)
+            GobSys.mkdir_or_exists save_run;
             GobConfig.write_file config;
             let module Meta = struct
                 type t = { command : string; version: string; timestamp : float; localtime : string } [@@deriving to_yojson]

src/goblint.ml

@@ -17,13 +17,13 @@ let main () =
     Cilfacade.init ();
 
     handle_extraspecials ();
-    create_temp_dir ();
+    GoblintDir.init ();
     handle_flags ();
     if get_bool "dbg.verbose" then (
       print_endline (localtime ());
       print_endline command;
     );
-    let file = Fun.protect ~finally:remove_temp_dir preprocess_and_merge in
+    let file = Fun.protect ~finally:GoblintDir.finalize preprocess_and_merge in
     if get_bool "server.enabled" then Server.start file else (
       let changeInfo = if GobConfig.get_bool "incremental.load" || GobConfig.get_bool "incremental.save" then diff_and_rename file else Analyses.empty_increment_data file in
       file|> do_analyze changeInfo;

src/incremental/serialize.ml

@@ -65,9 +65,9 @@ let store_data (data : 'a) (data_type : incremental_data_kind) =
     | AnalysisData -> server_analysis_data := Some (Obj.repr data)
     | _ -> ()
   else (
-    ignore @@ Goblintutil.create_dir (gob_directory ());
+    GobSys.mkdir_or_exists (gob_directory ());
     let d = gob_results_tmp_dir () in
-    ignore @@ Goblintutil.create_dir d;
+    GobSys.mkdir_or_exists d;
     let p = Filename.concat d (type_to_file_name data_type) in
     marshal data p)
 

src/maingoblint.ml

@@ -76,8 +76,8 @@ let option_spec_list =
   [ "-o"                   , Arg.String (set_string "outfile"), ""
   ; "-v"                   , Arg.Unit (fun () -> set_bool "dbg.verbose" true; set_bool "printstats" true), ""
   ; "-j"                   , Arg.Int (set_int "jobs"), ""
-  ; "-I"                   , Arg.String (set_string "includes[+]"), ""
-  ; "-IK"                  , Arg.String (set_string "kernel_includes[+]"), ""
+  ; "-I"                   , Arg.String (set_string "pre.includes[+]"), ""
+  ; "-IK"                  , Arg.String (set_string "pre.kernel_includes[+]"), ""
   ; "--set"                , Arg.Tuple [Arg.Set_string tmp_arg; Arg.String (fun x -> set_auto !tmp_arg x)], ""
   ; "--sets"               , Arg.Tuple [Arg.Set_string tmp_arg; Arg.String (fun x -> prerr_endline "--sets is deprecated, use --set instead."; set_string !tmp_arg x)], ""
   ; "--enable"             , Arg.String (fun x -> set_bool x true), ""
@@ -139,26 +139,24 @@ let handle_flags () =
 (** Use gcc to preprocess a file. Returns the path to the preprocessed file. *)
 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, None)
-  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 = (Preprocessor.get_cpp ()) ^ " --undef __BLOCKS__ " ^ String.join " " (List.map Filename.quote all_cppflags) ^ " \"" ^ fname ^ "\" -o \"" ^ nname ^ "\"" in
-    if get_bool "dbg.verbose" then print_endline command;
-    (nname, Some {ProcessPool.command; cwd = None})
+  let nname =  Filename.concat (GoblintDir.preprocessed ()) (Filename.chop_extension (Filename.basename fname) ^ ".i") in
+  (* Preprocess using cpp. *)
+  (* ?? what is __BLOCKS__? is it ok to just undef? this? http://en.wikipedia.org/wiki/Blocks_(C_language_extension) *)
+  let arguments = "--undef" :: "__BLOCKS__" :: all_cppflags @ fname :: "-o" :: nname :: [] in
+  let command = Filename.quote_command (Preprocessor.get_cpp ()) arguments in
+  if get_bool "dbg.verbose" then print_endline command;
+  (nname, Some {ProcessPool.command; cwd = None})
 
 (** Preprocess all files. Return list of preprocessed files and the temp directory name. *)
 let preprocess_files () =
   Hashtbl.clear Preprocessor.dependencies; (* clear for server mode *)
 
   (* Preprocessor flags *)
-  let cppflags = ref (get_string_list "cppflags") in
+  let cppflags = ref (get_string_list "pre.cppflags") in
 
   (* the base include directory *)
   let custom_include_dirs =
-    get_string_list "custom_includes" @
+    get_string_list "pre.custom_includes" @
     Filename.concat exe_dir "includes" ::
     Goblint_sites.includes
   in
@@ -188,16 +186,16 @@ let preprocess_files () =
 
   (* fill include flags *)
   let one_include_f f x = include_dirs := f x :: !include_dirs in
-  if get_string "ana.osek.oil" <> "" then include_files := Filename.concat !Goblintutil.tempDirName OilUtil.header :: !include_files;
+  if get_string "ana.osek.oil" <> "" then include_files := Filename.concat (GoblintDir.preprocessed ()) OilUtil.header :: !include_files;
   (* if get_string "ana.osek.tramp" <> "" then include_files := get_string "ana.osek.tramp" :: !include_files; *)
-  get_string_list "includes" |> List.iter (one_include_f identity);
+  get_string_list "pre.includes" |> List.iter (one_include_f identity);
 
   include_dirs := custom_include_dirs @ !include_dirs;
 
   (* If we analyze a kernel module, some special includes are needed. *)
   if get_bool "kernel" then (
     let kernel_roots = [
-      get_string "kernel-root";
+      get_string "pre.kernel-root";
       Filename.concat exe_dir "linux-headers";
       (* linux-headers not installed with goblint package *)
     ]
@@ -207,7 +205,7 @@ let preprocess_files () =
     let kernel_dir = kernel_root ^ "/include" in
     let arch_dir = kernel_root ^ "/arch/x86/include" in (* TODO add arm64: https://github.com/goblint/analyzer/issues/312 *)
 
-    get_string_list "kernel_includes" |> List.iter (Filename.concat kernel_root |> one_include_f);
+    get_string_list "pre.kernel_includes" |> List.iter (Filename.concat kernel_root |> one_include_f);
 
     let preconf = find_custom_include "linux/goblint_preconf.h" in
     let autoconf = Filename.concat kernel_dir "linux/kconfig.h" in
@@ -264,12 +262,14 @@ let preprocess_files () =
     extra_arg_files := find_custom_include "sv-comp.c" :: !extra_arg_files;
 
   let preprocessed = List.concat_map preprocess_arg_file (!extra_arg_files @ !arg_files) in
-  let preprocess_tasks = List.filter_map snd preprocessed in
-  let terminated task = function
-    | Unix.WEXITED 0 -> ()
-    | process_status -> failwith (GobUnix.string_of_process_status process_status)
-  in
-  ProcessPool.run ~jobs:(Goblintutil.jobs ()) ~terminated preprocess_tasks;
+  if not (get_bool "pre.exist") then (
+    let preprocess_tasks = List.filter_map snd preprocessed in
+    let terminated task = function
+      | Unix.WEXITED 0 -> ()
+      | process_status -> failwith (GobUnix.string_of_process_status process_status)
+    in
+    ProcessPool.run ~jobs:(Goblintutil.jobs ()) ~terminated preprocess_tasks
+  );
   List.map fst preprocessed
 
 (** Possibly merge all postprocessed files *)

src/solvers/generic.ml

@@ -107,7 +107,7 @@ struct
   let stats_csv =
     let save_run = GobConfig.get_string "save_run" in
     if save_run <> "" then (
-      ignore @@ Goblintutil.create_dir save_run;
+      GobSys.mkdir_or_exists save_run;
       save_run ^ Filename.dir_sep ^ "solver_stats.csv" |> open_out |> Option.some
     ) else None
   let write_csv xs oc = output_string oc @@ String.concat ",\t" xs ^ "\n"

src/solvers/postSolver.ml

@@ -126,7 +126,7 @@ module SaveRun: F =
       let solver = Filename.concat save_run solver_file in
       if get_bool "dbg.verbose" then
         print_endline ("Saving the solver result to " ^ solver);
-      ignore @@ GU.create_dir save_run; (* ensure the directory exists *)
+      GobSys.mkdir_or_exists save_run;
       Serialize.marshal vh solver
   end
 

src/util/compilationDatabase.ml

@@ -33,9 +33,7 @@ let load_and_preprocess ~all_cppflags filename =
     else
       Fun.id
   in
-  (* TODO: generalize .goblint for everything *)
-  ignore (Goblintutil.create_dir ".goblint");
-  let preprocessed_dir = Goblintutil.create_dir (Filename.concat ".goblint" "preprocessed") in
+  let preprocessed_dir = GobFilename.absolute (GoblintDir.preprocessed ()) in (* absolute due to cwd changes *)
   let preprocess obj =
     let file = obj.file in
     let extension = Filename.extension file in

src/util/gobSys.ml

@@ -6,3 +6,15 @@ let rec mkdir_parents filename =
     mkdir_parents dirname;
     Unix.mkdir dirname 0o770; (* TODO: what permissions? *)
   )
+
+let mkdir_or_exists dirname =
+  try
+    Unix.mkdir dirname 0o770 (* TODO: what permissions? *)
+  with Unix.Unix_error (Unix.EEXIST, _, _) ->
+    assert (Sys.is_directory dirname) (* may exist, but as a file *)
+
+let rmdir_if_empty dirname =
+  try
+    Unix.rmdir dirname
+  with Unix.Unix_error (Unix.ENOTEMPTY, _, _) ->
+    ()

src/util/goblintDir.ml

@@ -0,0 +1,15 @@
+open GobConfig
+
+let root () = get_string "goblint-dir"
+
+let preprocessed () = Filename.concat (root ()) "preprocessed"
+
+let init () =
+  (* TODO: generalize .goblint for everything *)
+  GobSys.mkdir_or_exists (root ());
+  GobSys.mkdir_or_exists (preprocessed ())
+
+let finalize () =
+  if not (get_bool "pre.keep") then
+    ignore (Goblintutil.rm_rf (preprocessed ()));
+  GobSys.rmdir_if_empty (root ())

src/util/goblintutil.ml

@@ -23,9 +23,6 @@ let inthack = Int64.of_int (-19012009) (* TODO do we still need this? *)
 (** The file where everything is output *)
 let out = ref stdout
 
-(** Temp directory, set by create_temp_dir, but used by the OSEK analysis. *)
-let tempDirName = ref "goblint_temp"
-
 (** Command for assigning an id to a varinfo. All varinfos directly created by Goblint should be modified by this method *)
 let create_var (var: varinfo) =
   (* TODO Hack: this offset should preempt conflicts with ids generated by CIL *)
@@ -67,20 +64,8 @@ let escape = XmlUtil.escape (* TODO: inline everywhere *)
 
 (** Creates a directory and returns the absolute path **)
 let create_dir name =
-  let dirName = if Filename.is_relative name then Filename.concat (Unix.getcwd ()) name else name in
-  (* The directory should be writable to group and user *)
-  let dirPerm = 0o770 in
-  let _ =
-    try
-      Unix.mkdir dirName dirPerm
-    with Unix.Unix_error(err, ctx1, ctx) as ex ->
-      (* We can discared the EEXIST, we are happy to use the existing directory *)
-      if err != Unix.EEXIST then begin
-        (* Hopefully will be friendly enough :) *)
-        print_endline ("Error, " ^ (Unix.error_message err));
-        raise ex
-      end
-  in
+  let dirName = GobFilename.absolute name in
+  GobSys.mkdir_or_exists dirName;
   dirName
 
 (** Remove directory and its content, as "rm -rf" would do. *)
@@ -95,20 +80,6 @@ let rm_rf path =
   in
   f path
 
-(* The temp directory for preprocessing the input files *)
-let create_temp_dir () =
-  if Sys.file_exists (get_string "tempDir") then
-    tempDirName := get_string "tempDir"
-  else
-    (* Using the stdlib to create a free tmp file name. *)
-    let tmpDirRel = Filename.temp_file ~temp_dir:"" "goblint_temp_" "" in
-    (* ... and then delete it to create a directory instead. *)
-    Sys.remove tmpDirRel;
-    let tmpDirName = create_dir tmpDirRel in
-    tempDirName := tmpDirName
-
-let remove_temp_dir () =
-  if not (get_bool "keepcpp") then ignore (rm_rf !tempDirName)
 
 exception Timeout
 

src/util/oilUtil.ml

@@ -99,7 +99,7 @@ let is_starting f = (List.mem f !concurrent_tasks) || (List.mem f !starting_task
 
 (*print id header *)
 let generate_header () =
-  let f = open_out (Filename.concat !Goblintutil.tempDirName header) in
+  let f = open_out (Filename.concat (GoblintDir.preprocessed ()) header) in
   let print_resources id value = if not(is_task_res id) then output_string f ("int " ^ id ^ ";\n") else () in
   let print_events id value 	 = output_string f ("int " ^ id           ^ ";\n") in
   let print_tasks id value     = output_string f ("int " ^ trim_task id ^ ";\n") in