From 84533c79c93100b36f4eb6e365eef0ebb537be35 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 23 Sep 2020 23:01:52 +0200
Subject: [PATCH] [Metrics] split 'undef functions' into 'spec-only' and
'unspec and undef'
---
src/plugins/metrics/metrics_cilast.ml | 36 ++++++++++++---
src/plugins/metrics/metrics_cilast.mli | 4 +-
tests/libc/oracle/fc_libc.0.res.oracle | 46 +++++++++++--------
tests/metrics/oracle/cyclo_comp5.res.oracle | 8 +++-
tests/metrics/oracle/func_ptr.0.res.oracle | 8 +++-
tests/metrics/oracle/func_ptr.1.res.oracle | 8 +++-
tests/metrics/oracle/libc.0.res.oracle | 8 +++-
tests/metrics/oracle/libc.1.res.oracle | 8 +++-
tests/metrics/oracle/reach.res.oracle | 8 +++-
tests/metrics/oracle/unreachable.res.oracle | 8 +++-
.../variadic-stdlib-generated.res.oracle | 8 +++-
11 files changed, 107 insertions(+), 43 deletions(-)
diff --git a/src/plugins/metrics/metrics_cilast.ml b/src/plugins/metrics/metrics_cilast.ml
index e719e52e683..387c97650ec 100644
--- a/src/plugins/metrics/metrics_cilast.ml
+++ b/src/plugins/metrics/metrics_cilast.ml
@@ -27,8 +27,9 @@ open Metrics_base
;;
type cilast_metrics = {
- fundecl_calls: int Metrics_base.VInfoMap.t;
- fundef_calls: int Metrics_base.VInfoMap.t;
+ fundecl_calls: int Metrics_base.VInfoMap.t; (* undefined and unspecified *)
+ funspec_calls: int Metrics_base.VInfoMap.t; (* undefined, but with spec *)
+ fundef_calls: int Metrics_base.VInfoMap.t; (* defined *)
extern_global_vars: Metrics_base.VInfoSet.t;
basic_global_metrics: BasicMetrics.t
}
@@ -43,9 +44,10 @@ class type sloc_visitor = object
inherit Visitor.generic_frama_c_visitor
(* Get the number of times a function has been called if it has been
- defined (fundef) or not (fundecl).
+ defined (fundef), specified (funspec), or just declared (fundecl).
*)
method fundecl_calls: int Metrics_base.VInfoMap.t
+ method funspec_calls: int Metrics_base.VInfoMap.t
method fundef_calls: int Metrics_base.VInfoMap.t
(* Global variables with 'Extern' storage *)
method extern_global_vars: Metrics_base.VInfoSet.t
@@ -92,11 +94,13 @@ class slocVisitor ~libc : sloc_visitor = object(self)
val mutable seen_vars = Varinfo.Set.empty;
val fundecl_calls: int VInfoMap.t ref = ref VInfoMap.empty;
+ val funspec_calls: int VInfoMap.t ref = ref VInfoMap.empty;
val fundef_calls: int VInfoMap.t ref = ref VInfoMap.empty;
val extern_global_vars = ref VInfoSet.empty
(* Getters/setters *)
method fundecl_calls = !fundecl_calls
+ method funspec_calls = !funspec_calls
method fundef_calls = !fundef_calls
method extern_global_vars = !extern_global_vars
method get_global_metrics = !global_metrics
@@ -339,8 +343,16 @@ class slocVisitor ~libc : sloc_visitor = object(self)
in
if vinfo.vdefined
then update_call_map fundef_calls
- else update_call_map fundecl_calls
-
+ else
+ let has_spec =
+ try
+ let spec = Annotations.funspec ~populate:false (Globals.Functions.get vinfo) in
+ spec <> Cil.empty_funspec ()
+ with Annotations.No_funspec _ ->
+ false
+ in
+ if has_spec then update_call_map funspec_calls
+ else update_call_map fundecl_calls
method! vinst i =
begin match i with
@@ -575,7 +587,9 @@ let dump_html fmt cil_visitor =
@{<h2>Synthetic results@}@ <br/>@ \
@{<span>Defined function(s)@} (%d): <br/>@ \
@[ %a@]@ <br/>@ <br/>@ \
- @{<span>Undefined function(s)@} (%d):@ <br/>@ \
+ @{<span>Specified-only function(s)@} (%d):@ <br/>@ \
+ @[ %a@]@ <br>@ <br/>@ \
+ @{<span>Undefined and unspecified function(s)@} (%d):@ <br/>@ \
@[ %a@]@ <br>@ <br/>@ \
@{<span>'Extern' global variable(s)@} (%d):@ <br/>@ \
@[ %a@]@ <br>@ <br/>@ \
@@ -584,6 +598,8 @@ let dump_html fmt cil_visitor =
@}@]"
(VInfoMap.cardinal cil_visitor#fundef_calls)
Metrics_base.pretty_set cil_visitor#fundef_calls
+ (VInfoMap.cardinal cil_visitor#funspec_calls)
+ Metrics_base.pretty_set cil_visitor#funspec_calls
(VInfoMap.cardinal cil_visitor#fundecl_calls)
Metrics_base.pretty_set cil_visitor#fundecl_calls
(VInfoSet.cardinal cil_visitor#extern_global_vars)
@@ -625,21 +641,26 @@ let dump_html fmt cil_visitor =
let pp_funinfo fmt vis =
let nfundef = VInfoMap.cardinal vis#fundef_calls in
+ let nfunspec = VInfoMap.cardinal vis#funspec_calls in
let nfundecl = VInfoMap.cardinal vis#fundecl_calls in
let nextern = VInfoSet.cardinal vis#extern_global_vars in
let fundef_hdr = Format.sprintf "Defined functions (%d)" nfundef
- and fundecl_hdr = Format.sprintf "Undefined functions (%d)" nfundecl
+ and funspec_hdr = Format.sprintf "Specified-only functions (%d)" nfunspec
+ and fundecl_hdr = Format.sprintf "Undefined and unspecified functions (%d)" nfundecl
and extern_hdr = Format.sprintf "'Extern' global variables (%d)" nextern
and entry_pts_hdr = Format.sprintf "Potential entry points (%d)"
(Metrics_base.number_entry_points vis#fundef_calls) in
Format.fprintf fmt
"@[<v 0>@[<v 1>%a@ @[%a@]@]@ @ \
+ @[<v 1>%a@ @[%a@]@]@ @ \
@[<v 1>%a@ @[%a@]@]@ @ \
@[<v 1>%a@ @[%a@]@]@ @ \
@[<v 1>%a@ @[%a@]@]@ \
@]"
(Metrics_base.mk_hdr 1) fundef_hdr
Metrics_base.pretty_set vis#fundef_calls
+ (Metrics_base.mk_hdr 1) funspec_hdr
+ Metrics_base.pretty_set vis#funspec_calls
(Metrics_base.mk_hdr 1) fundecl_hdr
Metrics_base.pretty_set vis#fundecl_calls
(Metrics_base.mk_hdr 1) extern_hdr
@@ -680,6 +701,7 @@ let get_cilast_metrics ~libc =
(cil_visitor:>Visitor.frama_c_visitor) file;
{
fundecl_calls = cil_visitor#fundecl_calls;
+ funspec_calls = cil_visitor#funspec_calls;
fundef_calls = cil_visitor#fundef_calls;
extern_global_vars = cil_visitor#extern_global_vars;
basic_global_metrics = cil_visitor#get_global_metrics;
diff --git a/src/plugins/metrics/metrics_cilast.mli b/src/plugins/metrics/metrics_cilast.mli
index 2da3fbdf04b..e7dcd86abb5 100644
--- a/src/plugins/metrics/metrics_cilast.mli
+++ b/src/plugins/metrics/metrics_cilast.mli
@@ -31,9 +31,10 @@ class type sloc_visitor = object
inherit Visitor.generic_frama_c_visitor
(* Get the number of times a function has been called if it has been
- defined (fundef) or not (fundecl).
+ defined (fundef), specified (funspec), or just declared (fundecl).
*)
method fundecl_calls: int Metrics_base.VInfoMap.t
+ method funspec_calls: int Metrics_base.VInfoMap.t
method fundef_calls: int Metrics_base.VInfoMap.t
method extern_global_vars: Metrics_base.VInfoSet.t
@@ -64,6 +65,7 @@ val get_global_metrics : libc:bool -> Metrics_base.BasicMetrics.t ;;
type cilast_metrics = {
fundecl_calls: int Metrics_base.VInfoMap.t;
+ funspec_calls: int Metrics_base.VInfoMap.t;
fundef_calls: int Metrics_base.VInfoMap.t;
extern_global_vars: Metrics_base.VInfoSet.t;
basic_global_metrics: Metrics_base.BasicMetrics.t
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 137fa979193..21143ee8813 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -41,8 +41,8 @@
wcscpy (0 call); wcslen (2 calls); wcsncat (0 call); wcsncpy (0 call);
wmemcpy (0 call); wmemset (0 call);
- Undefined functions (412)
- =========================
+ Specified-only functions (411)
+ ==============================
FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
Frama_C_long_long_interval (0 call);
@@ -52,21 +52,21 @@
Frama_C_unsigned_long_interval (0 call);
Frama_C_unsigned_long_long_interval (0 call);
Frama_C_unsigned_short_interval (0 call); _Exit (0 call);
- __builtin_abort (1 call); __builtin_clz (0 call); __builtin_clzl (0 call);
- __builtin_clzll (0 call); __builtin_ctz (0 call); __builtin_ctzl (0 call);
- __builtin_ctzll (0 call); __builtin_popcount (0 call);
- __builtin_popcountl (0 call); __builtin_popcountll (0 call);
- __builtin_sadd_overflow (0 call); __builtin_saddl_overflow (0 call);
- __builtin_saddll_overflow (0 call); __builtin_smul_overflow (0 call);
- __builtin_smull_overflow (0 call); __builtin_smulll_overflow (0 call);
- __builtin_ssub_overflow (0 call); __builtin_ssubl_overflow (0 call);
- __builtin_ssubll_overflow (0 call); __builtin_uadd_overflow (0 call);
- __builtin_uaddl_overflow (0 call); __builtin_uaddll_overflow (0 call);
- __builtin_umul_overflow (0 call); __builtin_umull_overflow (0 call);
- __builtin_umulll_overflow (0 call); __builtin_usub_overflow (0 call);
- __builtin_usubl_overflow (0 call); __builtin_usubll_overflow (0 call);
- __fc_fpclassify (0 call); __fc_fpclassifyf (0 call); __fc_infinity (0 call);
- __fc_nan (0 call); __va_fcntl_flock (0 call); __va_fcntl_int (0 call);
+ __builtin_clz (0 call); __builtin_clzl (0 call); __builtin_clzll (0 call);
+ __builtin_ctz (0 call); __builtin_ctzl (0 call); __builtin_ctzll (0 call);
+ __builtin_popcount (0 call); __builtin_popcountl (0 call);
+ __builtin_popcountll (0 call); __builtin_sadd_overflow (0 call);
+ __builtin_saddl_overflow (0 call); __builtin_saddll_overflow (0 call);
+ __builtin_smul_overflow (0 call); __builtin_smull_overflow (0 call);
+ __builtin_smulll_overflow (0 call); __builtin_ssub_overflow (0 call);
+ __builtin_ssubl_overflow (0 call); __builtin_ssubll_overflow (0 call);
+ __builtin_uadd_overflow (0 call); __builtin_uaddl_overflow (0 call);
+ __builtin_uaddll_overflow (0 call); __builtin_umul_overflow (0 call);
+ __builtin_umull_overflow (0 call); __builtin_umulll_overflow (0 call);
+ __builtin_usub_overflow (0 call); __builtin_usubl_overflow (0 call);
+ __builtin_usubll_overflow (0 call); __fc_fpclassify (0 call);
+ __fc_fpclassifyf (0 call); __fc_infinity (0 call); __fc_nan (0 call);
+ __va_fcntl_flock (0 call); __va_fcntl_int (0 call);
__va_fcntl_void (0 call); __va_ioctl_int (0 call); __va_ioctl_ptr (0 call);
__va_ioctl_void (0 call); __va_open_mode_t (0 call);
__va_open_void (0 call); __va_openat_mode_t (0 call);
@@ -166,6 +166,10 @@
wcsstr (0 call); wcstombs (0 call); wctomb (0 call); wmemchr (0 call);
wmemcmp (0 call); wmemmove (0 call); write (0 call);
+ Undefined and unspecified functions (1)
+ =======================================
+ __builtin_abort (1 call);
+
'Extern' global variables (16)
==============================
__fc_basename; __fc_dirname; __fc_getpwuid_pw_dir; __fc_getpwuid_pw_name;
@@ -280,8 +284,12 @@ void main(void)
=====================
main (0 call);
- Undefined functions (0)
- =======================
+ Specified-only functions (0)
+ ============================
+
+
+ Undefined and unspecified functions (0)
+ =======================================
'Extern' global variables (0)
diff --git a/tests/metrics/oracle/cyclo_comp5.res.oracle b/tests/metrics/oracle/cyclo_comp5.res.oracle
index 835739a7ac6..18ec0102d58 100644
--- a/tests/metrics/oracle/cyclo_comp5.res.oracle
+++ b/tests/metrics/oracle/cyclo_comp5.res.oracle
@@ -3,8 +3,12 @@
=====================
complexity5 (1 call); main (0 call);
- Undefined functions (1)
- =======================
+ Specified-only functions (0)
+ ============================
+
+
+ Undefined and unspecified functions (1)
+ =======================================
printf (4 calls);
'Extern' global variables (0)
diff --git a/tests/metrics/oracle/func_ptr.0.res.oracle b/tests/metrics/oracle/func_ptr.0.res.oracle
index 0a380c92321..c9313069f70 100644
--- a/tests/metrics/oracle/func_ptr.0.res.oracle
+++ b/tests/metrics/oracle/func_ptr.0.res.oracle
@@ -6,8 +6,12 @@
baz (address taken) (0 call); foo (address taken) (0 call); foobar (0 call);
main (0 call);
- Undefined functions (1)
- =======================
+ Specified-only functions (0)
+ ============================
+
+
+ Undefined and unspecified functions (1)
+ =======================================
exit (1 call);
'Extern' global variables (1)
diff --git a/tests/metrics/oracle/func_ptr.1.res.oracle b/tests/metrics/oracle/func_ptr.1.res.oracle
index b44df54a2fe..740bbb61a1c 100644
--- a/tests/metrics/oracle/func_ptr.1.res.oracle
+++ b/tests/metrics/oracle/func_ptr.1.res.oracle
@@ -6,8 +6,12 @@
baz (address taken) (0 call); foo (address taken) (0 call); foobar (0 call);
main (0 call);
- Undefined functions (1)
- =======================
+ Specified-only functions (0)
+ ============================
+
+
+ Undefined and unspecified functions (1)
+ =======================================
exit (1 call);
'Extern' global variables (1)
diff --git a/tests/metrics/oracle/libc.0.res.oracle b/tests/metrics/oracle/libc.0.res.oracle
index c3bb5a741d5..1742799970d 100644
--- a/tests/metrics/oracle/libc.0.res.oracle
+++ b/tests/metrics/oracle/libc.0.res.oracle
@@ -4,8 +4,12 @@
bar (0 call); f (0 call); foo (0 call); g (address taken) (0 call);
main (0 call);
- Undefined functions (0)
- =======================
+ Specified-only functions (0)
+ ============================
+
+
+ Undefined and unspecified functions (0)
+ =======================================
'Extern' global variables (0)
diff --git a/tests/metrics/oracle/libc.1.res.oracle b/tests/metrics/oracle/libc.1.res.oracle
index b00598fd71a..690ea20f9c4 100644
--- a/tests/metrics/oracle/libc.1.res.oracle
+++ b/tests/metrics/oracle/libc.1.res.oracle
@@ -4,8 +4,8 @@
bar (1 call); f (0 call); foo (1 call); g (address taken) (0 call);
getopt (1 call); main (0 call);
- Undefined functions (122)
- =========================
+ Specified-only functions (122)
+ ==============================
_exit (0 call); access (0 call); chdir (0 call); chown (0 call);
chroot (0 call); clearerr (0 call); clearerr_unlocked (0 call);
close (0 call); dup (0 call); dup2 (0 call); execl (0 call);
@@ -40,6 +40,10 @@
vprintf (0 call); vscanf (0 call); vsnprintf (0 call); vsprintf (0 call);
write (0 call);
+ Undefined and unspecified functions (0)
+ =======================================
+
+
'Extern' global variables (10)
==============================
Frama_C_entropy_source; __fc_errno; __fc_hostname; __fc_stdin; __fc_stdout;
diff --git a/tests/metrics/oracle/reach.res.oracle b/tests/metrics/oracle/reach.res.oracle
index 76558191cce..f033a695ab9 100644
--- a/tests/metrics/oracle/reach.res.oracle
+++ b/tests/metrics/oracle/reach.res.oracle
@@ -49,8 +49,12 @@
=====================
baz (address taken) (0 call); foo (address taken) (0 call); main (0 call);
- Undefined functions (0)
- =======================
+ Specified-only functions (0)
+ ============================
+
+
+ Undefined and unspecified functions (0)
+ =======================================
'Extern' global variables (0)
diff --git a/tests/metrics/oracle/unreachable.res.oracle b/tests/metrics/oracle/unreachable.res.oracle
index 38770a200d1..f3507cf43c9 100644
--- a/tests/metrics/oracle/unreachable.res.oracle
+++ b/tests/metrics/oracle/unreachable.res.oracle
@@ -3,8 +3,12 @@
=====================
foo (1 call); main (0 call);
- Undefined functions (0)
- =======================
+ Specified-only functions (0)
+ ============================
+
+
+ Undefined and unspecified functions (0)
+ =======================================
'Extern' global variables (0)
diff --git a/tests/metrics/oracle/variadic-stdlib-generated.res.oracle b/tests/metrics/oracle/variadic-stdlib-generated.res.oracle
index e79acc9295d..edae7ad63d8 100644
--- a/tests/metrics/oracle/variadic-stdlib-generated.res.oracle
+++ b/tests/metrics/oracle/variadic-stdlib-generated.res.oracle
@@ -3,8 +3,12 @@
=====================
main (0 call); my_printf (1 call);
- Undefined functions (1)
- =======================
+ Specified-only functions (0)
+ ============================
+
+
+ Undefined and unspecified functions (1)
+ =======================================
rand (1 call);
'Extern' global variables (0)
--
GitLab