From ef4e9f619b2a0f2cafa579b85b23fd1ad0b44abf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 20 Oct 2021 15:14:36 +0200
Subject: [PATCH] [Eva] Summary and analysis coverage: fixes the count of
analyzed functions.
Only the functions whose body is analyzed are counted as covered by the
analysis. The functions reached by the analysis but for which a builtin or the
specification is used are not considered analyzed anymore.
Summary: computes statistics only for analyzed function. Returns [None] for
other functions.
---
.../bts/oracle/issue-eacsl-145.res.oracle | 4 +-
src/plugins/server/kernel_ast.ml | 13 ++++++
src/plugins/server/kernel_ast.mli | 1 +
src/plugins/value/api/general_requests.ml | 6 +--
src/plugins/value/engine/compute_functions.ml | 4 +-
src/plugins/value/utils/summary.ml | 43 ++++++++++---------
src/plugins/value/utils/summary.mli | 10 ++---
.../oracle/generalized_check.0.res.oracle | 4 +-
8 files changed, 50 insertions(+), 35 deletions(-)
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-145.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-145.res.oracle
index 6136cebc45e..8d646242f63 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-145.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-145.res.oracle
@@ -26,8 +26,8 @@
[eva] ====== VALUES COMPUTED ======
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 5 functions analyzed (out of 5): 100% coverage.
- In these functions, 27 statements reached (out of 27): 100% coverage.
+ 3 functions analyzed (out of 5): 60% coverage.
+ In these functions, 23 statements reached (out of 23): 100% coverage.
----------------------------------------------------------------------------
No errors or warnings raised during the analysis.
----------------------------------------------------------------------------
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 7ce9dd03cc6..d130f00bdd8 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -375,6 +375,19 @@ struct
with Not_found -> Data.failure "Undefined function '%s'" key
end
+module Fundec =
+struct
+ type t = fundec
+ let jtype = Pkg.Jkey "fundec"
+ let to_json fundec =
+ `String fundec.svar.vname
+ let of_json js =
+ let key = Js.to_string js in
+ try Kernel_function.get_definition (Globals.Functions.find_by_name key)
+ with Not_found | Kernel_function.No_Definition ->
+ Data.failure "Undefined function definition '%s'" key
+end
+
module KfMarker = struct
type record
let record : record Record.signature = Record.signature ()
diff --git a/src/plugins/server/kernel_ast.mli b/src/plugins/server/kernel_ast.mli
index d85697dec67..e0cc3e7007d 100644
--- a/src/plugins/server/kernel_ast.mli
+++ b/src/plugins/server/kernel_ast.mli
@@ -30,6 +30,7 @@ open Cil_types
module Position : Data.S with type t = Filepath.position
module Kf : Data.S with type t = kernel_function
+module Fundec : Data.S with type t = fundec
module Ki : Data.S with type t = kinstr
module Stmt : Data.S with type t = stmt
module Lval : Data.S with type t = kinstr * lval
diff --git a/src/plugins/value/api/general_requests.ml b/src/plugins/value/api/general_requests.ml
index 2a225d40834..1b226d8e8d2 100644
--- a/src/plugins/value/api/general_requests.ml
+++ b/src/plugins/value/api/general_requests.ml
@@ -428,9 +428,9 @@ let _array =
~name:"functionStats"
~descr:(Markdown.plain
"Statistics about the last Eva analysis for each function")
- ~key:(fun (kf,_stats) -> Kernel_function.get_name kf)
- ~keyType:Kernel_ast.Kf.jtype
- ~iter:(fun f -> FunctionStats.iter (fun kf s -> f (kf,s)))
+ ~key:(fun (fundec,_stats) -> fundec.svar.vname)
+ ~keyType:Kernel_ast.Fundec.jtype
+ ~iter:(fun f -> FunctionStats.iter (fun fundec s -> f (fundec,s)))
~add_update_hook:FunctionStats.register_hook
model
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index a382c2266d9..5d0cf41b0ba 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -201,10 +201,10 @@ module Make (Abstract: Abstractions.Eva) = struct
Library_functions.warn_unsupported_spec vi.vorig_name;
Spec.compute_using_specification ~warn:true call_kinstr call spec state,
Eval.Cacheable
- | `Def _fundec ->
+ | `Def fundec ->
Db.Value.Call_Type_Value_Callbacks.apply (`Def, cvalue_state, call_stack);
let result = Computer.compute kf call_kinstr state in
- Summary.FunctionStats.recompute kf;
+ Summary.FunctionStats.recompute fundec;
result
in
if pp then
diff --git a/src/plugins/value/utils/summary.ml b/src/plugins/value/utils/summary.ml
index b9f8b34078b..1429c0262b3 100644
--- a/src/plugins/value/utils/summary.ml
+++ b/src/plugins/value/utils/summary.ml
@@ -157,11 +157,12 @@ let get_status ip =
in
Property_status.fold_on_statuses aux_status ip None
-let compute_fun_stats kf =
+let compute_fun_stats fundec =
let alarms = AlarmsStats.create 13
and coverage = Coverage.make ()
and statuses = Statuses.make ()
in
+ let kf = Globals.Functions.get fundec.Cil_types.svar in
let do_status alarm ip =
match get_status ip with
| None -> ()
@@ -183,11 +184,7 @@ let compute_fun_stats kf =
Coverage.incr coverage ~reachable;
Annotations.iter_code_annot (do_annot stmt) stmt
in
- begin match kf.Cil_types.fundec with
- | Declaration _ -> ()
- | Definition (fundec,_loc) ->
- List.iter do_stmt fundec.Cil_types.sallstmts
- end;
+ List.iter do_stmt fundec.Cil_types.sallstmts;
{ fun_coverage = coverage;
fun_alarm_count = AlarmsStats.to_list alarms;
fun_alarm_statuses = statuses; }
@@ -196,7 +193,7 @@ let compute_fun_stats kf =
module FunctionStats_Type = Datatype.Make (struct
include Datatype.Serializable_undefined
type t = fun_stats
- let name = "Eva.Value_results.FunctionStats_Type"
+ let name = "Eva.Summary.FunctionStats_Type"
let reprs = [{
fun_coverage = Coverage.make ();
fun_alarm_count = [];
@@ -205,23 +202,26 @@ module FunctionStats_Type = Datatype.Make (struct
end)
module FunctionStats = struct
- include Kernel_function.Make_Table
+ include State_builder.Hashtbl
+ (Cil_datatype.Fundec.Hashtbl)
(FunctionStats_Type)
(struct
- let name = "Eva.Value_results.FunctionStats"
+ let name = "Eva.Summary.FunctionStats"
let dependencies = [ Db.Value.self ]
let size = 17
end)
module Hook = Hook.Build (struct
- type t = Cil_types.kernel_function * fun_stats
+ type t = Cil_types.fundec * fun_stats
end)
let compute kf =
let stats = compute_fun_stats kf in
Hook.apply (kf,stats);
stats
- let get = memo compute
+ let get kf =
+ try Some (find kf)
+ with Not_found -> None
let recompute kf = replace kf (compute kf)
let register_hook = Hook.extend
end
@@ -289,19 +289,20 @@ let compute_stats () =
and prog_stmt_coverage = Coverage.make ()
and prog_alarms = AlarmsStats.create 131
in
- let do_fun kf =
- let reachable = Value_results.is_called kf in
- let consider = consider_function (Kernel_function.get_vi kf) in
- if consider then
- Coverage.incr prog_fun_coverage ~reachable;
- if reachable then begin
- let fun_stats = FunctionStats.get kf in
+ let do_fun fundec =
+ let consider = consider_function fundec.Cil_types.svar in
+ match FunctionStats.get fundec with
+ | Some fun_stats ->
AlarmsStats.add_list prog_alarms fun_stats.fun_alarm_count;
if consider then
- Coverage.add prog_stmt_coverage fun_stats.fun_coverage;
- end
+ begin
+ Coverage.incr prog_fun_coverage ~reachable:true;
+ Coverage.add prog_stmt_coverage fun_stats.fun_coverage;
+ end
+ | None ->
+ if consider then Coverage.incr prog_fun_coverage ~reachable:false;
in
- Globals.Functions.iter do_fun;
+ Globals.Functions.iter_on_fundecs do_fun;
let alarms_statuses, assertions_statuses, preconds_statuses =
compute_statuses ()
and eva_events, kernel_events = compute_events () in
diff --git a/src/plugins/value/utils/summary.mli b/src/plugins/value/utils/summary.mli
index 9bfbc90e4c6..a0e912834d7 100644
--- a/src/plugins/value/utils/summary.mli
+++ b/src/plugins/value/utils/summary.mli
@@ -66,16 +66,16 @@ type program_stats =
module FunctionStats : sig
(** Get the current analysis statistics for a function *)
- val get: Cil_types.kernel_function -> fun_stats
+ val get: Cil_types.fundec -> fun_stats option
- (** Iterate on every function statistices *)
- val iter: (Cil_types.kernel_function -> fun_stats -> unit) -> unit
+ (** Iterate on every function statistics *)
+ val iter: (Cil_types.fundec -> fun_stats -> unit) -> unit
(** Trigger the recomputation of function stats *)
- val recompute: Cil_types.kernel_function -> unit
+ val recompute: Cil_types.fundec -> unit
(** Set a hook on function statistics computation *)
- val register_hook: (Cil_types.kernel_function * fun_stats -> unit) -> unit
+ val register_hook: (Cil_types.fundec * fun_stats -> unit) -> unit
end
(** Compute analysis statistics. *)
diff --git a/tests/spec/oracle/generalized_check.0.res.oracle b/tests/spec/oracle/generalized_check.0.res.oracle
index f93e7228b40..4fc947aed52 100644
--- a/tests/spec/oracle/generalized_check.0.res.oracle
+++ b/tests/spec/oracle/generalized_check.0.res.oracle
@@ -30,8 +30,8 @@
__retres ∈ {0}
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
- 3 functions analyzed (out of 3): 100% coverage.
- In these functions, 25 statements reached (out of 28): 89% coverage.
+ 2 functions analyzed (out of 3): 66% coverage.
+ In these functions, 25 statements reached (out of 25): 100% coverage.
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis:
by the Eva analyzer: 0 errors 1 warning
--
GitLab