CHC: add command-line option to control the status of system includes

Author: sipma

CodeHawk/CHC/cchanalyze/cCHGenerateAndCheck.ml

@@ -35,6 +35,7 @@ open CHPretty
 
 (* chutil *)
 open CHLogger
+open CHTiming
 open CHTimingLog
 
 (* cchlib *)
@@ -160,6 +161,7 @@ let make_invariant_generation_spec t =
 
 
 let process_function gspecs fname =
+  let cfilename = system_settings#get_cfilename in
   try
     if !function_to_be_analyzed = fname || !function_to_be_analyzed = "" then
       let _ = log_info "analyze function %s [%s:%d]" fname __FILE__ __LINE__ in
@@ -180,6 +182,10 @@ let process_function gspecs fname =
           (List.length openpos)
           __FILE__ __LINE__ in
       if (List.length openpos) > 0 then
+        let _ =
+          pr_timing [
+              STR cfilename; STR ": ===analyze function=== "; STR fname;
+              STR " with "; INT (List.length openpos); STR " open pos"] in
         let callcount = proof_scaffolding#get_call_count fname in
         let _ =
           List.iter
@@ -209,6 +215,10 @@ let process_function gspecs fname =
                   begin
 	            gspec.ig_invariant_extractor env invio invariants;
                     record_postconditions fname env invio;
+                    pr_timing [
+                        STR cfilename; STR ":"; STR fname;
+                        STR ": Finished analyzing with domain ";
+                        STR gspec.ig_domain]
                   end
 	        with
 	        | CCHFailure p | CHFailure p ->
@@ -342,6 +352,7 @@ let process_function gspecs fname =
 let generate_and_check_process_file (domains: string list) =
   let gspecs = List.map make_invariant_generation_spec domains in
   try
+    let cfilename = system_settings#get_cfilename in
     let _ = read_cfile_dictionary () in
     let cfile = read_cfile () in
     let _ = fenv#initialize cfile in
@@ -352,7 +363,14 @@ let generate_and_check_process_file (domains: string list) =
     let _ = read_cfile_contract () in
     let _ = file_contract#collect_file_attributes in
     let _ = log_info "Read file-level xml files [%s:%d]" __FILE__ __LINE__ in
+    let _ = pr_timing [STR cfilename; STR ": finished loading files"] in
     let functions = fenv#get_application_functions in
+    let _ =
+      pr_timing [
+          STR cfilename;
+          STR ": Analyzing ";
+          INT (List.length functions);
+          STR " functions"] in
     let _ =
       log_info "Processing %d functions [%s:%d]"
         (List.length functions) __FILE__ __LINE__ in
@@ -363,6 +381,7 @@ let generate_and_check_process_file (domains: string list) =
     let _ = save_cfile_interface_dictionary () in
     let _ = save_cfile_predicate_dictionary () in
     let _ = log_info "Saved file-level xml files [%s:%d]" __FILE__ __LINE__ in
+    let _ = pr_timing [STR cfilename; STR ": finished saving files"] in
     ()
   with
   | CHXmlReader.IllFormed ->

CodeHawk/CHC/cchcil/cCHXParseFile.ml

@@ -52,7 +52,7 @@ open CHCilWriteXml
 let projectpath = ref ""
 let targetdirectory = ref ""
 let filename = ref ""
-let filterfiles = ref true
+let keep_system_includes = ref false
 let keepUnused = ref false
 
 let version = "CP1.1"
@@ -70,8 +70,8 @@ let speclist = [
      "path to the project base directory");
     ("-targetdirectory", Arg.String set_targetdirectory,
      "directory to store the generated xml files");
-    ("-nofilter", Arg.Unit (fun () -> filterfiles := false),
-     "don't filter out functions in files starting with slash");
+    ("-keep_system_includes", Arg.Unit (fun () -> keep_system_includes := true),
+     "don't filter out functions in files with an absolute path name");
     ("-keepUnused",
      Arg.Set keepUnused, "keep unused type and function definitions")]
 
@@ -241,11 +241,12 @@ let save_xml_file f =
           match g with
           | GFun (fdec, _loc) -> fdec :: a | _ -> a) [] f.globals in
     let fns =
-      if !filterfiles then
-        List.filter (fun fdec ->
-            not ((String.get fdec.svar.vdecl.file 0) = '/')) fns
+      if !keep_system_includes then
+        fns
       else
-        fns in
+        (* filter out functions with an absolute path names *)
+        List.filter (fun fdec ->
+            not ((String.get fdec.svar.vdecl.file 0) = '/')) fns in
     let fnsTarget = Filename.concat (Filename.dirname absoluteTarget) "functions" in
     begin
       List.iter (fun f -> cil_function_to_file target f fnsTarget) fns;

CodeHawk/CHC/cchcmdline/cCHXCAnalyzer.ml

@@ -33,6 +33,7 @@ open CHPretty
 (* chutil *)
 open CHGc
 open CHLogger
+open CHTiming
 open CHTimingLog
 open CHXmlDocument
 
@@ -128,14 +129,15 @@ let speclist = [
    "print status on proof obligations and invariants");
   ("-projectname", Arg.String system_settings#set_projectname,
    "name of the project (determines name of results directory)");
-   ("-nofilter", Arg.Unit (fun () -> system_settings#set_filterabspathfiles false),
-    "do not filter out functions in files with absolute path names");
-   ("-unreachability", Arg.Unit (fun () -> system_settings#set_use_unreachability),
-    "use unreachability as a justification for discharging proof obligations");
-   ("-wordsize", Arg.Int system_settings#set_wordsize,
-    "set word size (e.g., 16, 32, or 64)");
-   ("-contractpath", Arg.String system_settings#set_contractpath,
-    "path to contract files")
+  ("-keep_system_includes",
+   Arg.Unit (fun () -> system_settings#set_keep_system_includes true),
+   "do not filter out functions in files with absolute path names");
+  ("-unreachability", Arg.Unit (fun () -> system_settings#set_use_unreachability),
+   "use unreachability as a justification for discharging proof obligations");
+  ("-wordsize", Arg.Int system_settings#set_wordsize,
+   "set word size (e.g., 16, 32, or 64)");
+  ("-contractpath", Arg.String system_settings#set_contractpath,
+   "path to contract files")
 ]
 
 let usage_msg = "chc_analyze <options> <path to analysis directory>"
@@ -153,10 +155,11 @@ let save_log_files (contenttype:string) =
 
 let main () =
   try
-    let _ = set_log_level "DEBUG" in
+    let _ = set_log_level "WARNING" in
     let _ = read_args () in
     let _ = chlog#set_max_entry_size 1000 in
     let _ = log_info "AIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAIAI" in
+    let cfilename = system_settings#get_cfilename in
     if !cmd = "version" then
       begin
 	pr_debug [version#toPretty; NL];
@@ -201,13 +204,15 @@ let main () =
     else if !cmd = "generate_and_check" then
       begin
         generate_and_check_process_file (List.rev !domains);
+        pr_timing [STR cfilename; STR ": finished generate_and_check"];
         log_info
           "Invariants generated and proof obligations checked [%s:%d]"
           __FILE__ __LINE__;
         save_log_files "gencheck";
         log_info
           "Invariant generation and proof obligation check log files saved [%s:%d]"
-          __FILE__ __LINE__
+          __FILE__ __LINE__;
+        pr_timing [STR cfilename; STR ": finished saving log files"]
       end
 
     else

CodeHawk/CHC/cchlib/cCHFileEnvironment.ml

@@ -98,10 +98,11 @@ object (self)
   method initialize (f:file) =
     let _ = self#reset in
     let is_application_function (v:varinfo) =
-      if system_settings#filterabspathfiles then
-        not ((String.get v.vdecl.file 0) = '/')
+      if system_settings#keep_system_includes then
+        true
       else
-        true in
+        (* filter out functions originating from files from system path *)
+        not ((String.get v.vdecl.file 0) = '/') in
     begin
       List.iter (fun g ->
           match g with

CodeHawk/CHC/cchlib/cCHLibTypes.mli

@@ -872,8 +872,13 @@ class type system_settings_int =
     method set_verbose: bool -> unit
     method verbose: bool
 
-    method set_filterabspathfiles: bool -> unit
-    method filterabspathfiles: bool
+    (* The [keep_system_includes] is set to false by default. If set to [true]
+       (by command-line option), it assumes that functions from system includes
+       (specifically, functions from include files whose path starts with '/')
+       have been parsed by CIL and are to be included in the analysis.
+     *)
+    method set_keep_system_includes: bool -> unit
+    method keep_system_includes: bool
 
     method set_wordsize: int -> unit
     method get_wordsize: int

CodeHawk/CHC/cchlib/cCHSettings.ml

@@ -46,7 +46,7 @@ object
   val mutable contractpath = ""
 
   val mutable verbose = false
-  val mutable filterabspathfiles = true
+  val mutable keep_system_includes = false
   val mutable wordsize = Some 32
   val mutable use_unreachability = false
   val mutable analysis_level = ImplementationDefinedBehavior
@@ -78,7 +78,8 @@ object
 
   method set_verbose (v:bool) = verbose <- v
 
-  method set_filterabspathfiles (v:bool) = filterabspathfiles <- v
+  method set_keep_system_includes (v:bool) = keep_system_includes <- v
+  method keep_system_includes = keep_system_includes
 
   method set_wordsize (v:int) = wordsize <- Some v
 
@@ -98,7 +99,7 @@ object
 
   method use_unreachability = use_unreachability
   method verbose = verbose
-  method filterabspathfiles = filterabspathfiles
+
   method has_wordsize = match wordsize with Some _ -> true | _ -> false
 
 

CodeHawk/CHC/cchpre/cCHCreatePrimaryProofObligations.ml

@@ -93,6 +93,7 @@ let process_function (fname:string) =
 
 let primary_process_file () =
   try
+    let cfilename = system_settings#get_cfilename in
     let _ = read_cfile_dictionary () in
     let _ = read_cfile_interface_dictionary () in
     let cfile = read_cfile () in
@@ -101,8 +102,8 @@ let primary_process_file () =
     let functions = fenv#get_application_functions in
     let _ =
       log_info
-        "Cfile initialized with %d functions [%s:%d]"
-        (List.length functions)
+        "Cfile %s initialized with %d functions [%s:%d]"
+        cfilename (List.length functions)
         __FILE__ __LINE__ in
     let _ = read_cfile_contract () in
     let _ = file_contract#collect_file_attributes in