diff --git a/src/plugins/metrics/metrics_acsl.ml b/src/plugins/metrics/metrics_acsl.ml index 6e8cc4b68f7771060214537bbe16865d7ea0904f..68210ab38d896d6da3b75e0dc1ddca83914a44fd 100644 --- a/src/plugins/metrics/metrics_acsl.ml +++ b/src/plugins/metrics/metrics_acsl.ml @@ -315,7 +315,10 @@ let dump () = let fmt = Format.formatter_of_out_channel chan in (match Metrics_base.get_file_type out with | Metrics_base.Html -> dump_acsl_stats_html fmt - | Metrics_base.Text -> dump_acsl_stats fmt); + | Metrics_base.Text -> dump_acsl_stats fmt + | Metrics_base.Json -> + raise (Log.FeatureRequest ("Metrics", "JSON format for ACSL metrics")) + ); close_out chan with Sys_error s -> Metrics_parameters.abort "Cannot open file %s (%s)" out s diff --git a/src/plugins/metrics/metrics_base.ml b/src/plugins/metrics/metrics_base.ml index baf2ca5fd2b43f6e3bb9a1f82b6e8621948e722e..f39592a07eb42ec3a47de75bc6ac63ee797cdebc 100644 --- a/src/plugins/metrics/metrics_base.ml +++ b/src/plugins/metrics/metrics_base.ml @@ -248,6 +248,7 @@ let get_suffix filename = type output_type = | Html | Text + | Json ;; let get_file_type filename = @@ -255,6 +256,7 @@ let get_file_type filename = match get_suffix filename with | "html" | "htm" -> Html | "txt" | "text" -> Text + | "json" -> Json | s -> Metrics_parameters.abort "Unknown file extension %s. Cannot produce output.@." s @@ -285,6 +287,16 @@ let pretty_set fmt s = s; Format.fprintf fmt "@]" +let json_of_varinfo_map m = + let elems = VInfoMap.fold (fun f n acc -> + let calls = ("calls", `Int n) in + let address_taken = ("address_taken", `Bool f.vaddrof) in + let elem = `Assoc [(f.vname, `Assoc ([calls; address_taken]))] in + elem :: acc + ) m [] + in + `List (List.rev elems) + let pretty_extern_vars fmt s = Pretty_utils.pp_iter ~pre:"@[" ~suf:"@]" ~sep:";@ " VInfoSet.iter Printer.pp_varinfo fmt s @@ -312,6 +324,16 @@ let pretty_entry_points fmt fs = Format.fprintf fmt "@[<hov 1>%a@]" print fs; ;; +let json_of_entry_points m = + `List + (List.rev + (VInfoMap.fold + (fun vi n acc -> + if is_entry_point vi n then `String vi.vname :: acc + else acc) + m []) + ) + (* Utilities for CIL ASTs *) let file_of_vinfodef fvinfo = diff --git a/src/plugins/metrics/metrics_base.mli b/src/plugins/metrics/metrics_base.mli index bd8b85522c181da835fdfc7c4e1fc0d628978db6..1b209bbd078e665182942b0bba4e0c18d96e3e21 100644 --- a/src/plugins/metrics/metrics_base.mli +++ b/src/plugins/metrics/metrics_base.mli @@ -108,6 +108,10 @@ val pretty_set : Format.formatter -> int VInfoMap.t -> unit val pretty_extern_vars: Format.formatter -> VInfoSet.t -> unit +(** Build a JSON list with the varinfos in [m], each as a JSON object with + the varinfo name as key and additional attributes as values. *) +val json_of_varinfo_map : int VInfoMap.t -> Yojson.t + (** Handling entry points informations *) val number_entry_points : int VInfoMap.t -> int ;; @@ -116,6 +120,8 @@ val pretty_entry_points : Format.formatter -> int VInfoMap.t -> unit ;; +val json_of_entry_points : int VInfoMap.t -> Yojson.t + (** Get the filename where the definition of a varinfo occurs *) val file_of_vinfodef: Cil_types.varinfo -> Datatype.Filepath.t;; @@ -133,6 +139,7 @@ val get_filename: Cabs.definition -> Datatype.Filepath.t;; type output_type = | Html | Text + | Json ;; (** get_file_type [extension] sets the output type according to [extension]. diff --git a/src/plugins/metrics/metrics_cilast.ml b/src/plugins/metrics/metrics_cilast.ml index 88dc82d6538964a15a5d664d9bbb345c55e59d4d..8c737e2c13e7a7f25666c6870d107b7433be8568 100644 --- a/src/plugins/metrics/metrics_cilast.ml +++ b/src/plugins/metrics/metrics_cilast.ml @@ -662,6 +662,28 @@ let pp_funinfo fmt vis = Metrics_base.pretty_entry_points vis#fundef_calls ;; +let json_of_funinfo vis = + let fundef = + ("defined-functions", json_of_varinfo_map vis#fundef_calls) + in + let funspec = + ("specified-only-functions", json_of_varinfo_map vis#funspec_calls) + in + let fundecl = + ("undefined-functions", json_of_varinfo_map vis#fundecl_calls) + in + let extern_vars = + VInfoSet.fold (fun vi acc -> `String vi.vname :: acc) + vis#extern_global_vars [] + in + let extern = + ("extern-global-vars", `List (List.rev extern_vars)) + in + let entry_points = + ("entry-points", json_of_entry_points vis#fundef_calls) + in + `Assoc [fundef; funspec; fundecl; extern; entry_points] + let pp_with_funinfo fmt cil_visitor = Format.fprintf fmt "@[<v 0>%a@ %a@]" pp_funinfo cil_visitor @@ -721,6 +743,9 @@ let compute_on_cilast ~libc = (match Metrics_base.get_file_type out_fname with | Html -> dump_html fmt cil_visitor | Text -> pp_with_funinfo fmt cil_visitor + | Json -> + let json = json_of_funinfo cil_visitor in + Yojson.pretty_print fmt json ); close_out oc; with Sys_error _ -> diff --git a/src/plugins/metrics/metrics_parameters.ml b/src/plugins/metrics/metrics_parameters.ml index 9d9127573bcc5b44b29f991cfc1417418c0af55b..ca410edbb5e529bfee912a5d8ed37aaa4ff31718 100644 --- a/src/plugins/metrics/metrics_parameters.ml +++ b/src/plugins/metrics/metrics_parameters.ml @@ -49,7 +49,9 @@ module OutputFile = let option_name = "-metrics-output" let arg_name = "filename" let help = "print some metrics into the specified file; \ - the output format is recognized through the extension." + the output format is recognized through the extension. \ + If the filename is only the extension (txt, html, json), \ + print to stdout but in the specified format." end) module ValueCoverage = diff --git a/tests/metrics/libc.c b/tests/metrics/libc.c index c9c41a18762157b7fe04cf2289fd0ee154a0fb75..15e0328f762aa57887caa863f9459c63ed2a15c1 100644 --- a/tests/metrics/libc.c +++ b/tests/metrics/libc.c @@ -1,6 +1,8 @@ /* run.config STDOPT: #"-metrics-no-libc -metrics-eva-cover" STDOPT: #"-metrics-libc -metrics-eva-cover" + STDOPT: #"-metrics-libc -metrics-output @PTEST_DIR@/oracle/libc.json" + LOG: @PTEST_DIR@/oracle/libc.json */ #include <ctype.h> #include <stdio.h> // defines external variables diff --git a/tests/metrics/oracle/libc.2.res.oracle b/tests/metrics/oracle/libc.2.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..eeb5977dbc5fef0789c0e314ec2e68f5834bd8d2 --- /dev/null +++ b/tests/metrics/oracle/libc.2.res.oracle @@ -0,0 +1 @@ +[kernel] Parsing tests/metrics/libc.c (with preprocessing) diff --git a/tests/metrics/oracle/libc.json b/tests/metrics/oracle/libc.json new file mode 100644 index 0000000000000000000000000000000000000000..bf512214d4c9e47568c1b43de29a9545b6267d3e --- /dev/null +++ b/tests/metrics/oracle/libc.json @@ -0,0 +1,140 @@ +{ + "defined-functions": [ + { "bar": { "calls": 1, "address_taken": false } }, + { "f": { "calls": 0, "address_taken": false } }, + { "foo": { "calls": 1, "address_taken": false } }, + { "g": { "calls": 0, "address_taken": true } }, + { "getopt": { "calls": 1, "address_taken": false } }, + { "main": { "calls": 0, "address_taken": false } } + ], + "specified-only-functions": [ + { "_exit": { "calls": 0, "address_taken": false } }, + { "access": { "calls": 0, "address_taken": false } }, + { "chdir": { "calls": 0, "address_taken": false } }, + { "chown": { "calls": 0, "address_taken": false } }, + { "chroot": { "calls": 0, "address_taken": false } }, + { "clearerr": { "calls": 0, "address_taken": false } }, + { "clearerr_unlocked": { "calls": 0, "address_taken": false } }, + { "close": { "calls": 0, "address_taken": false } }, + { "dup": { "calls": 0, "address_taken": false } }, + { "dup2": { "calls": 0, "address_taken": false } }, + { "execl": { "calls": 0, "address_taken": false } }, + { "execle": { "calls": 0, "address_taken": false } }, + { "execlp": { "calls": 0, "address_taken": false } }, + { "execv": { "calls": 0, "address_taken": false } }, + { "execve": { "calls": 0, "address_taken": false } }, + { "execvp": { "calls": 0, "address_taken": false } }, + { "fclose": { "calls": 0, "address_taken": false } }, + { "fdopen": { "calls": 0, "address_taken": false } }, + { "feof": { "calls": 0, "address_taken": false } }, + { "feof_unlocked": { "calls": 0, "address_taken": false } }, + { "ferror": { "calls": 0, "address_taken": false } }, + { "ferror_unlocked": { "calls": 0, "address_taken": false } }, + { "fflush": { "calls": 0, "address_taken": false } }, + { "fgetc": { "calls": 0, "address_taken": false } }, + { "fgetpos": { "calls": 0, "address_taken": false } }, + { "fgets": { "calls": 0, "address_taken": false } }, + { "fileno": { "calls": 0, "address_taken": false } }, + { "fileno_unlocked": { "calls": 0, "address_taken": false } }, + { "flockfile": { "calls": 0, "address_taken": false } }, + { "fopen": { "calls": 0, "address_taken": false } }, + { "fork": { "calls": 0, "address_taken": false } }, + { "fputc": { "calls": 0, "address_taken": false } }, + { "fputs": { "calls": 0, "address_taken": false } }, + { "fread": { "calls": 0, "address_taken": false } }, + { "freopen": { "calls": 0, "address_taken": false } }, + { "fseek": { "calls": 0, "address_taken": false } }, + { "fseeko": { "calls": 0, "address_taken": false } }, + { "fsetpos": { "calls": 0, "address_taken": false } }, + { "ftell": { "calls": 0, "address_taken": false } }, + { "ftello": { "calls": 0, "address_taken": false } }, + { "ftrylockfile": { "calls": 0, "address_taken": false } }, + { "funlockfile": { "calls": 0, "address_taken": false } }, + { "fwrite": { "calls": 0, "address_taken": false } }, + { "getc": { "calls": 0, "address_taken": false } }, + { "getc_unlocked": { "calls": 0, "address_taken": false } }, + { "getchar": { "calls": 1, "address_taken": false } }, + { "getchar_unlocked": { "calls": 0, "address_taken": false } }, + { "getcwd": { "calls": 0, "address_taken": false } }, + { "getegid": { "calls": 0, "address_taken": false } }, + { "geteuid": { "calls": 0, "address_taken": false } }, + { "getgid": { "calls": 0, "address_taken": false } }, + { "gethostname": { "calls": 0, "address_taken": false } }, + { "getopt_long": { "calls": 0, "address_taken": false } }, + { "getopt_long_only": { "calls": 0, "address_taken": false } }, + { "getpgid": { "calls": 0, "address_taken": false } }, + { "getpgrp": { "calls": 0, "address_taken": false } }, + { "getpid": { "calls": 0, "address_taken": false } }, + { "getppid": { "calls": 0, "address_taken": false } }, + { "getresgid": { "calls": 0, "address_taken": false } }, + { "getresuid": { "calls": 0, "address_taken": false } }, + { "gets": { "calls": 0, "address_taken": false } }, + { "getsid": { "calls": 0, "address_taken": false } }, + { "getuid": { "calls": 0, "address_taken": false } }, + { "isalnum": { "calls": 0, "address_taken": false } }, + { "isalpha": { "calls": 1, "address_taken": false } }, + { "isascii": { "calls": 0, "address_taken": false } }, + { "isatty": { "calls": 0, "address_taken": false } }, + { "isblank": { "calls": 1, "address_taken": false } }, + { "iscntrl": { "calls": 0, "address_taken": false } }, + { "isdigit": { "calls": 0, "address_taken": false } }, + { "isgraph": { "calls": 0, "address_taken": false } }, + { "islower": { "calls": 0, "address_taken": false } }, + { "isprint": { "calls": 0, "address_taken": false } }, + { "ispunct": { "calls": 0, "address_taken": false } }, + { "isspace": { "calls": 0, "address_taken": false } }, + { "isupper": { "calls": 0, "address_taken": false } }, + { "isxdigit": { "calls": 0, "address_taken": false } }, + { "lseek": { "calls": 0, "address_taken": false } }, + { "pathconf": { "calls": 0, "address_taken": false } }, + { "pclose": { "calls": 0, "address_taken": false } }, + { "perror": { "calls": 0, "address_taken": false } }, + { "pipe": { "calls": 0, "address_taken": false } }, + { "popen": { "calls": 0, "address_taken": false } }, + { "putc": { "calls": 0, "address_taken": false } }, + { "putc_unlocked": { "calls": 0, "address_taken": false } }, + { "putchar": { "calls": 0, "address_taken": false } }, + { "putchar_unlocked": { "calls": 0, "address_taken": false } }, + { "puts": { "calls": 0, "address_taken": false } }, + { "read": { "calls": 0, "address_taken": false } }, + { "remove": { "calls": 0, "address_taken": false } }, + { "rename": { "calls": 0, "address_taken": false } }, + { "rewind": { "calls": 0, "address_taken": false } }, + { "setbuf": { "calls": 0, "address_taken": false } }, + { "setegid": { "calls": 0, "address_taken": false } }, + { "seteuid": { "calls": 0, "address_taken": false } }, + { "setgid": { "calls": 0, "address_taken": false } }, + { "sethostname": { "calls": 0, "address_taken": false } }, + { "setpgid": { "calls": 0, "address_taken": false } }, + { "setregid": { "calls": 0, "address_taken": false } }, + { "setresgid": { "calls": 0, "address_taken": false } }, + { "setresuid": { "calls": 0, "address_taken": false } }, + { "setreuid": { "calls": 0, "address_taken": false } }, + { "setsid": { "calls": 0, "address_taken": false } }, + { "setuid": { "calls": 0, "address_taken": false } }, + { "setvbuf": { "calls": 0, "address_taken": false } }, + { "sync": { "calls": 0, "address_taken": false } }, + { "sysconf": { "calls": 0, "address_taken": false } }, + { "tmpfile": { "calls": 0, "address_taken": false } }, + { "tmpnam": { "calls": 0, "address_taken": false } }, + { "tolower": { "calls": 0, "address_taken": false } }, + { "toupper": { "calls": 0, "address_taken": false } }, + { "ttyname": { "calls": 0, "address_taken": false } }, + { "ungetc": { "calls": 0, "address_taken": false } }, + { "unlink": { "calls": 0, "address_taken": false } }, + { "usleep": { "calls": 0, "address_taken": false } }, + { "vfprintf": { "calls": 0, "address_taken": false } }, + { "vfscanf": { "calls": 0, "address_taken": false } }, + { "vprintf": { "calls": 0, "address_taken": false } }, + { "vscanf": { "calls": 0, "address_taken": false } }, + { "vsnprintf": { "calls": 0, "address_taken": false } }, + { "vsprintf": { "calls": 0, "address_taken": false } }, + { "write": { "calls": 0, "address_taken": false } } + ], + "undefined-functions": [], + "extern-global-vars": [ + "Frama_C_entropy_source", "__fc_errno", "__fc_hostname", "__fc_stdin", + "__fc_stdout", "__fc_ttyname", "optarg", "opterr", "optind", "optopt" + ], + "entry-points": [ "f", "main" ] +} \ No newline at end of file