[Kernel/Eva] add audit options and checks

src/kernel_services/ast_queries/file.ml

@@ -46,6 +46,11 @@ type file =
   | External of Filepath.Normalized.t * string
   (* file * name of plug-in that handles it *)
 
+let filepath_of_file = function
+  | NeedCPP (fp, _, _)
+  | NoCPP fp
+  | External (fp, _) -> fp
+
 module D =
   Datatype.Make
     (struct
@@ -1605,6 +1610,121 @@ let init_cil () =
   Logic_env.Builtins.apply ();
   Logic_env.prepare_tables ()
 
+let re_included_file = Str.regexp "^[.]+ \\(.*\\)$"
+
+let file_hash file =
+  Digest.to_hex (Digest.file file)
+
+let add_source_if_new tbl (fp : Filepath.Normalized.t) =
+  if not (Hashtbl.mem tbl fp) then
+    Hashtbl.replace tbl fp (file_hash (fp:>string))
+
+(* Inserts, into the hashtbl of (Filepath.Normalized.t, Digest.t), [tbl],
+   the included sources listed in [file],
+   which contains the output of 'gcc -H -MM'. *)
+let add_included_sources tbl file =
+  let ic = open_in file in
+  try
+    while true; do
+      let line = input_line ic in
+      if Str.string_match re_included_file line 0 then
+        let f = Str.matched_group 1 line in
+        add_source_if_new tbl (Filepath.Normalized.of_string f)
+    done;
+    assert false
+  with End_of_file ->
+    close_in ic
+
+let print_all_sources out all_sources_tbl =
+  let elems =
+    Hashtbl.fold (fun f hash acc ->
+        (Filepath.Normalized.to_pretty_string f, hash) :: acc)
+      all_sources_tbl []
+  in
+  let sorted_elems =
+    List.sort (fun (f1, _) (f2, _) -> Extlib.compare_ignore_case f1 f2) elems
+  in
+  if Filepath.Normalized.is_special_stdout out then begin
+    (* text format, to stdout *)
+    Kernel.feedback "Audit: all used sources, with md5 hashes:@\n%a"
+      (Pretty_utils.pp_list ~sep:"@\n"
+         (Pretty_utils.pp_pair ~sep:": "
+            Format.pp_print_string Format.pp_print_string)) sorted_elems
+  end else begin
+    (* json format, into file [out] *)
+    let json =
+      `Assoc
+        [("sources",
+          `Assoc (List.map (fun (f, hash) -> f, `String hash) sorted_elems)
+         )]
+    in
+    Json.merge_object out json
+  end
+
+let compute_sources_table cpp_commands =
+  let all_sources_tbl = Hashtbl.create 7 in
+  List.iter (fun (f, cmd_opt) ->
+      let fp = filepath_of_file f in
+      match cmd_opt with
+      | None ->
+        add_source_if_new all_sources_tbl fp
+      | Some (cpp_cmd, _ppf, _sl) ->
+        let audit_sources_tmpfile =
+          try
+            Datatype.Filepath.of_string
+              (Extlib.temp_file_cleanup_at_exit
+                 "audit_produce_sources" ".txt")
+          with Extlib.Temp_file_error s ->
+            Kernel.abort "cannot create temporary file: %s" s
+        in
+        let cmd_for_sources =
+          cpp_cmd ^ " -H -MM >/dev/null 2>" ^ (audit_sources_tmpfile:>string)
+        in
+        let exit_code = Sys.command cmd_for_sources in
+        if exit_code <> 0 then begin
+          let cause_frama_c_compliant =
+            if not (Kernel.CppGnuLike.get ()) then
+              Kernel.abort "\nPlease ensure preprocessor is Frama-C-compliant \
+                            (see option %s)"
+                Kernel.CppGnuLike.option_name
+            else ""
+          in
+          Kernel.abort "error running command to obtain included sources \
+                        (exit code %d):@\n%s%s"
+            exit_code cmd_for_sources
+            cause_frama_c_compliant;
+        end else begin
+          add_included_sources all_sources_tbl (audit_sources_tmpfile:>string);
+          add_source_if_new all_sources_tbl fp;
+        end;
+    ) cpp_commands;
+  all_sources_tbl
+
+let source_hashes_of_json path =
+  try
+    let json = Json.from_file path in
+    let open Yojson.Basic.Util in
+    json |> member "sources" |> to_assoc |>
+    List.map (fun (k, h) -> k, to_string h)
+  with
+  | Yojson.Json_error msg ->
+    Kernel.abort "error reading %a: %s"
+      Filepath.Normalized.pretty path msg
+  | Yojson.Basic.Util.Type_error (msg, v) ->
+    Kernel.abort "error reading %a: %s - %s"
+      Filepath.Normalized.pretty path msg
+      (Yojson.Basic.pretty_to_string v)
+
+let check_source_hashes expected actual_table =
+  Hashtbl.iter (fun fp hash ->
+      let fp = Filepath.Normalized.to_pretty_string fp in
+      let expected_hash = List.assoc_opt fp expected in
+      if Some hash <> expected_hash then
+        Kernel.warning ~wkey:Kernel.wkey_audit
+          "different hashes for %s: got %s, expected %s"
+          fp hash (Option.value ~default:("<none> (not in list)") expected_hash)
+    ) actual_table
+
 let prepare_from_c_files () =
   init_cil ();
   let files = Files.get () in (* Allow pre-registration of prolog files *)
@@ -1619,6 +1739,19 @@ let prepare_from_c_files () =
       ) cpp_commands;
     raise Cmdline.Exit
   end;
+  let audit_check_path = Kernel.AuditCheck.get () in
+  if not (Filepath.Normalized.is_unknown audit_check_path) then begin
+    let all_sources_tbl = compute_sources_table cpp_commands in
+    let expected_hashes = source_hashes_of_json audit_check_path in
+    check_source_hashes expected_hashes all_sources_tbl
+  end;
+  let audit_path = Kernel.AuditPrepare.get () in
+  if not (Filepath.Normalized.is_unknown audit_path) then begin
+    let all_sources_tbl = compute_sources_table cpp_commands in
+    print_all_sources audit_path all_sources_tbl;
+    Kernel.feedback "Audit: sources list written to: %a@."
+      Filepath.Normalized.pretty audit_path;
+  end;
   let cil, cabs_files = files_to_cabs_cil files cpp_commands in
   prepare_cil_file cil;
   (* prepare_cil_file may call syntactic transformers, that will ultimately

src/kernel_services/plugin_entry_points/kernel.ml

@@ -194,6 +194,8 @@ let wkey_acsl_extension = register_warn_category "acsl-extension"
 
 let wkey_cmdline = register_warn_category "cmdline"
 
+let wkey_audit = register_warn_category "audit"
+
 (* ************************************************************************* *)
 (** {2 Specialised functors for building kernel parameters} *)
 (* ************************************************************************* *)
@@ -1040,6 +1042,41 @@ module PrintCppCommands =
                   and exits."
     end)
 
+let () = Parameter_customize.set_group parsing
+let () = Parameter_customize.do_not_reset_on_copy ()
+module AuditPrepare =
+  P.Filepath
+    (struct
+      let option_name = "-audit-prepare"
+      let arg_name = "path"
+      let existence = Filepath.Indifferent
+      let file_kind = "json"
+      let help = "produces audit-related information, such as the list of all \
+                  source files used during parsing (including those in include \
+                  directives) with checksums. Some plug-ins may produce \
+                  additional audit-related information. \
+                  Prints the information as JSON to the specified file, or \
+                  if the file is '-', prints as text to the standard output. \
+                  Requires -cpp-frama-c-compliant."
+    end)
+
+let () = Parameter_customize.set_group parsing
+let () = Parameter_customize.do_not_reset_on_copy ()
+module AuditCheck =
+  P.Filepath
+    (struct
+      let option_name = "-audit-check"
+      let arg_name = "path"
+      let existence = Filepath.Must_exist
+      let file_kind = "json"
+      let help = "reads an audit JSON file (produced by -audit-prepare) and \
+                  checks compliance w.r.t. to it; e.g., if the source files \
+                  were declared and have the expected checksum. \
+                  Raises a warning (with warning key 'audit') in case of \
+                  failed checks. \
+                  Requires -cpp-frama-c-compliant."
+    end)
+
 let () = Parameter_customize.set_group parsing
 let () = Parameter_customize.do_not_reset_on_copy ()
 module FramaCStdLib =

src/kernel_services/plugin_entry_points/kernel.mli

@@ -186,6 +186,9 @@ val wkey_acsl_extension: warn_category
 val wkey_cmdline: warn_category
 (** Command-line related warning, e.g. for invalid options given by the user *)
 
+val wkey_audit: warn_category
+(** Warning related to options '-audit-*'. *)
+
 (* ************************************************************************* *)
 (** {2 Functors for late option registration}                                *)
 (** Kernel_function-related options cannot be registered in this module:
@@ -414,6 +417,12 @@ module CppGnuLike: Parameter_sig.Bool
 module PrintCppCommands: Parameter_sig.Bool
 (** Behavior of option "-print-cpp-commands" *)
 
+module AuditPrepare: Parameter_sig.Filepath
+(** Behavior of option "-audit-prepare" *)
+
+module AuditCheck: Parameter_sig.Filepath
+(** Behavior of option "-audit-check" *)
+
 module FramaCStdLib: Parameter_sig.Bool
 (** Behavior of option "-frama-c-stdlib" *)
 

src/plugins/value/engine/analysis.ml

@@ -173,7 +173,10 @@ let reset_analyzer () =
 let force_compute () =
   Ast.compute ();
   Value_parameters.configure_precision ();
-  Value_parameters.print_configuration ();
+  if not (Filepath.Normalized.is_unknown (Kernel.AuditCheck.get ()))
+  then Value_parameters.check_configuration (Kernel.AuditCheck.get ());
+  if not (Filepath.Normalized.is_unknown (Kernel.AuditPrepare.get ()))
+  then Value_parameters.print_configuration (Kernel.AuditPrepare.get ());
   let kf, lib_entry = Globals.entry_point () in
   reset_analyzer ();
   let module Analyzer = (val snd !ref_analyzer) in

src/plugins/value/value_parameters.ml

@@ -61,6 +61,8 @@ let add_precision_dep p =
 
 let () = List.iter add_correctness_dep kernel_parameters_correctness
 
+module Fc_filepath = Filepath
+
 module Eva =
   Plugin.Register
     (struct
@@ -84,7 +86,6 @@ let dkey_incompatible_states = register_category "incompatible-states"
 let dkey_iterator = register_category "iterator"
 let dkey_callbacks = register_category "callbacks"
 let dkey_widening = register_category "widening"
-let dkey_config = register_category "config"
 
 let () =
   let activate dkey = add_debug_keys dkey in
@@ -1427,17 +1428,69 @@ let parameters_correctness =
 let parameters_tuning =
   Typed_parameter.Set.elements !parameters_tuning
 
-let print_correctness_parameters () =
-  feedback ~dkey:dkey_config
-    "Correctness parameters of the analysis:";
-  let print param =
+let json_of_parameters parms =
+  let pair param =
     let name = param.Typed_parameter.name in
     let value = Typed_parameter.get_value param in
-    printf "  %s: %s" name value
+    (name, `String value)
   in
-  List.iter print parameters_correctness
-
-let print_warning_status name (module Plugin: Log.Messages) =
+  let parms_json = List.map pair parms in
+  `Assoc [("correctness-parameters", `Assoc parms_json)]
+
+let parameters_of_json parms_json =
+  try
+    let open Yojson.Basic.Util in
+    let parms = parms_json |> member "correctness-parameters" |> to_assoc in
+    List.map (fun (key, value) -> (key, value |> to_string)) parms
+  with
+  | Yojson.Json_error msg ->
+    Kernel.abort "error reading JSON file: %s" msg
+  | Yojson.Basic.Util.Type_error (msg, v) ->
+    Kernel.abort "error reading JSON file: %s - %s" msg
+      (Yojson.Basic.pretty_to_string v)
+
+let print_correctness_parameters path =
+  if Fc_filepath.Normalized.is_special_stdout path then begin
+    feedback "Correctness parameters of the analysis:";
+    let print param =
+      let name = param.Typed_parameter.name in
+      let value = Typed_parameter.get_value param in
+      printf "  %s: %s" name value
+    in
+    List.iter print parameters_correctness
+  end else begin
+    let json = `Assoc [("eva", json_of_parameters parameters_correctness)] in
+    Json.merge_object path json
+  end
+
+let check_correctness_parameters json =
+  let get param =
+    let name = param.Typed_parameter.name in
+    let value = Typed_parameter.get_value param in
+    (name, value)
+  in
+  let parameters = List.map get parameters_correctness in
+  let expected_parameters =
+    parameters_of_json (json |> Yojson.Basic.Util.member "eva")
+  in
+  let sort = List.sort (fun (p1, _) (p2, _) -> Stdlib.String.compare p1 p2) in
+  let expected_parameters = sort expected_parameters in
+  let parameters = sort parameters in
+  (* Note: we could simply compare lengths and use a two-list iterator,
+     but in case of divergence, the error messages would be less clear. *)
+  List.iter (fun (exp_p, exp_v) ->
+      try
+        let v = List.assoc exp_p parameters in
+        if exp_v <> v then
+          Kernel.warning ~wkey:Kernel.wkey_audit
+            "correctness parameter %s: expected value %s, but got %s" exp_p
+            exp_v v
+      with Not_found ->
+        Kernel.warning ~wkey:Kernel.wkey_audit
+          "expected correctness parameter %s, but not found" exp_p
+    ) expected_parameters
+
+let compute_warning_status (module Plugin: Log.Messages) =
   let warning_categories = Plugin.get_all_warn_categories_status () in
   let is_active = function
     | Log.Winactive | Wfeedback_once | Wfeedback -> false
@@ -1445,20 +1498,83 @@ let print_warning_status name (module Plugin: Log.Messages) =
   in
   let is_enabled (_key, status) = is_active status in
   let enabled, disabled = List.partition is_enabled warning_categories in
-  let pp_categories = Pretty_utils.pp_list ~sep:",@ " Plugin.pp_warn_category in
-  feedback ~dkey:dkey_config "%s warning categories:" name;
-  printf "  Enabled: @[%a@]" pp_categories (List.map fst enabled);
-  printf "  Disabled: @[%a@]" pp_categories (List.map fst disabled)
-
-let print_configuration () =
-  if is_debug_key_enabled dkey_config
-  then
+  let pp_fst = List.map (fun (c, s) -> Plugin.wkey_name c, s) in
+  (pp_fst enabled, pp_fst disabled)
+
+let json_of_warning_statuses wkeys key_name =
+  let json_of_wkey = List.map (fun (c, _) -> `String c) in
+  (key_name, `List (json_of_wkey wkeys))
+
+let warning_statuses_of_json json =
+  try
+    let open Yojson.Basic.Util in
+    json |> to_list |> filter_string
+  with
+  | Yojson.Json_error msg ->
+    Kernel.abort "error reading JSON file: %s" msg
+  | Yojson.Basic.Util.Type_error (msg, v) ->
+    Kernel.abort "error reading JSON file: %s - %s" msg
+      (Yojson.Basic.pretty_to_string v)
+
+let print_warning_status path name (module Plugin: Log.Messages) =
+  let enabled, disabled = compute_warning_status (module Plugin) in
+  if Fc_filepath.Normalized.is_special_stdout path then
     begin
-      print_correctness_parameters ();
-      print_warning_status "Kernel" (module Kernel);
-      print_warning_status "Eva" (module Eva);
+      let pp_categories =
+        Pretty_utils.pp_list ~sep:",@ " Format.pp_print_string
+      in
+      feedback "Audit: %s warning categories:" name;
+      printf "  Enabled: @[%a@]" pp_categories (List.map fst enabled);
+      printf "  Disabled: @[%a@]" pp_categories (List.map fst disabled)
     end
-
+  else begin
+    let enabled_json =
+      json_of_warning_statuses enabled "enabled"
+    in
+    let disabled_json =
+      json_of_warning_statuses disabled "disabled"
+    in
+    let json = `Assoc [(Stdlib.String.lowercase_ascii name,
+                        `Assoc [("warning-categories",
+                                 `Assoc [enabled_json; disabled_json])])]
+    in
+    Json.merge_object path json
+  end
+
+let check_warning_status json name (module Plugin: Log.Messages) =
+  let lower_name = Stdlib.String.lowercase_ascii name in
+  let enabled, _disabled = compute_warning_status (module Plugin) in
+  let enabled = List.map fst enabled in
+  let (expected_enabled : string list) =
+    try
+      let open Yojson.Basic.Util in
+      json |> member lower_name |> member "warning-categories" |>
+      member "enabled" |> to_list |> filter_string
+    with
+    | Yojson.Json_error msg ->
+      Kernel.abort "error reading JSON file: %s" msg
+    | Yojson.Basic.Util.Type_error (msg, v) ->
+      Kernel.abort "error reading JSON file: %s - %s" msg
+        (Yojson.Basic.pretty_to_string v)
+  in
+  let diff l1 l2 = List.filter (fun k -> not (List.mem k l2)) l1 in
+  let should_be_enabled = diff expected_enabled enabled in
+  if should_be_enabled <> [] then
+    Kernel.warning ~wkey:Kernel.wkey_audit
+      "the following warning categories were expected to be enabled,@ \
+       but were disabled: %a"
+      (Pretty_utils.pp_list ~sep:", " Format.pp_print_string) should_be_enabled
+
+let check_configuration path =
+  let json = Json.from_file path in
+  check_correctness_parameters json;
+  check_warning_status json "Kernel" (module Kernel);
+  check_warning_status json "Eva" (module Eva)
+
+let print_configuration path =
+  print_correctness_parameters path;
+  print_warning_status path "Kernel" (module Kernel);
+  print_warning_status path "Eva" (module Eva)
 
 (*
 Local Variables:

src/plugins/value/value_parameters.mli

@@ -20,6 +20,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+module Fc_filepath = Filepath
+
 include Plugin.General_services
 
 module ForceValues: Parameter_sig.With_output
@@ -153,7 +155,8 @@ val configure_precision: unit -> unit
 val parameters_correctness: Typed_parameter.t list
 val parameters_tuning: Typed_parameter.t list
 
-val print_configuration: unit -> unit
+val check_configuration: Fc_filepath.Normalized.t -> unit
+val print_configuration: Fc_filepath.Normalized.t -> unit
 
 (** Debug categories responsible for printing initial and final states of Value.
     Enabled by default, but can be disabled via the command-line: