From 793b7f20e05d92347468268d92d994ce63e44ec4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 14 Jan 2022 22:23:51 +0100
Subject: [PATCH] [Eva] Uses the plugins callgraph, rtegen and scope via the
dynamic API.
The new file eva_dynamic contains all accesses via the dynamic API.
---
Makefile | 2 +-
headers/header_spec.txt | 2 +
.../value/domains/cvalue/cvalue_domain.ml | 2 +-
src/plugins/value/engine/compute_functions.ml | 4 +-
src/plugins/value/gui_files/register_gui.ml | 4 +-
src/plugins/value/legacy/eval_annots.ml | 5 --
src/plugins/value/legacy/eval_annots.mli | 1 -
src/plugins/value/utils/eva_dynamic.ml | 67 +++++++++++++++++++
src/plugins/value/utils/eva_dynamic.mli | 43 ++++++++++++
9 files changed, 117 insertions(+), 13 deletions(-)
create mode 100644 src/plugins/value/utils/eva_dynamic.ml
create mode 100644 src/plugins/value/utils/eva_dynamic.mli
diff --git a/Makefile b/Makefile
index 9fa91830176..75ce964f267 100644
--- a/Makefile
+++ b/Makefile
@@ -856,7 +856,7 @@ endif
# - try to keep the legacy Value before Eva
PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
utils/eva_audit utils/value_perf utils/eva_annotations \
- utils/value_util utils/red_statuses \
+ utils/eva_dynamic utils/value_util utils/red_statuses \
utils/mark_noresults \
utils/widen_hints_ext utils/widen \
partitioning/split_return \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 081be10cddc..40c2cc32fa2 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1483,6 +1483,8 @@ src/plugins/value/utils/eva_annotations.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/eva_annotations.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/eva_audit.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/eva_audit.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/eva_dynamic.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/eva_dynamic.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/structure.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/structure.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/summary.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index 80abee069dd..57dd8ab350c 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -559,7 +559,7 @@ module State = struct
let display_results () =
Value_parameters.result "====== VALUES COMPUTED ======";
- Callgraph.Uses.iter_in_rev_order display;
+ Eva_dynamic.Callgraph.iter_in_rev_order display;
Value_parameters.result "%t" Value_perf.display
let post_analysis _state =
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index 718da24a529..e294447de66 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -108,10 +108,10 @@ let post_analysis () =
(* Try to refine the 'Unknown' statuses that have been emitted during
this analysis. *)
Eval_annots.mark_green_and_red ();
- Eval_annots.mark_rte ();
+ Eva_dynamic.RteGen.mark_generated_rte ();
post_analysis_cleanup ~aborted:false;
(* Remove redundant alarms *)
- if Value_parameters.RmAssert.get () then !Db.Value.rm_asserts ()
+ if Value_parameters.RmAssert.get () then Eva_dynamic.Scope.rm_asserts ()
(* Registers signal handlers for SIGUSR1 and SIGINT to cleanly abort the Eva
analysis. Returns a function that restores previous signal behaviors after
diff --git a/src/plugins/value/gui_files/register_gui.ml b/src/plugins/value/gui_files/register_gui.ml
index 5adf217e9f9..3587497948d 100644
--- a/src/plugins/value/gui_files/register_gui.ml
+++ b/src/plugins/value/gui_files/register_gui.ml
@@ -227,9 +227,7 @@ let gui_compute_values (main_ui:main_ui) =
let cleaned_outputs kf s =
let outs = Db.Outputs.kinstr (Kstmt s) in
- let accept =
- Callgraph.Uses.accept_base ~with_formals:true ~with_locals:true kf
- in
+ let accept = Eva_dynamic.Callgraph.accept_base kf in
let filter = Locations.Zone.filter_base accept in
Option.map filter outs
diff --git a/src/plugins/value/legacy/eval_annots.ml b/src/plugins/value/legacy/eval_annots.ml
index 7e3434b351b..68aed0aadab 100644
--- a/src/plugins/value/legacy/eval_annots.ml
+++ b/src/plugins/value/legacy/eval_annots.ml
@@ -102,11 +102,6 @@ let mark_unreachable () =
Annotations.iter_all_code_annot do_code_annot;
Visitor.visitFramacFile unreach (Ast.get ())
-let mark_rte () =
- let list = !Db.RteGen.get_all_status () in
- let mark kf = List.iter (fun (_kind, set, _get) -> set kf true) list in
- Globals.Functions.iter (fun kf -> if !Db.Value.is_called kf then mark kf)
-
let c_labels kf cs =
if !Db.Value.use_spec_instead_of_definition kf then
Cil_datatype.Logic_label.Map.empty
diff --git a/src/plugins/value/legacy/eval_annots.mli b/src/plugins/value/legacy/eval_annots.mli
index 03fbb8c5154..ba43b7aa2f9 100644
--- a/src/plugins/value/legacy/eval_annots.mli
+++ b/src/plugins/value/legacy/eval_annots.mli
@@ -26,5 +26,4 @@ val has_requires: spec -> bool
val mark_invalid_initializers: unit -> unit
val mark_unreachable: unit -> unit
val mark_green_and_red: unit -> unit
-val mark_rte: unit -> unit
val c_labels: kernel_function -> Value_types.callstack -> Eval_terms.labels_states
diff --git a/src/plugins/value/utils/eva_dynamic.ml b/src/plugins/value/utils/eva_dynamic.ml
new file mode 100644
index 00000000000..b62a8ec73cb
--- /dev/null
+++ b/src/plugins/value/utils/eva_dynamic.ml
@@ -0,0 +1,67 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+let get ~plugin name typ ~fallback =
+ try Dynamic.get ~plugin name typ
+ with Failure _ | Dynamic.(Unbound_value _ | Incompatible_type _) -> fallback
+
+module Callgraph = struct
+ let plugin = "callgraph"
+
+ let iter_in_rev_order f =
+ let fallback = Globals.Functions.iter in
+ let typ = Datatype.(func (func Kernel_function.ty unit) unit) in
+ get ~plugin "iter_in_rev_order" typ ~fallback f
+
+ let accept_base kf v =
+ let fallback _ _ = true in
+ let typ = Datatype.(func2 Kernel_function.ty Base.ty bool) in
+ get ~plugin "accept_base" typ ~fallback kf v
+end
+
+module Scope = struct
+ let plugin = "scope"
+
+ let rm_asserts () =
+ let fallback () =
+ Value_parameters.warning
+ "The scope plugin is missing: cannot remove redundant alarms."
+ in
+ let typ = Datatype.(func unit unit) in
+ get ~plugin "rm_asserts" typ ~fallback ()
+end
+
+module RteGen = struct
+ let plugin = "RteGen"
+
+ let all_statuses () =
+ let kf = Kernel_function.ty in
+ let typ =
+ Datatype.(list (triple string (func2 kf bool unit) (func kf bool)))
+ in
+ get ~plugin "all_statuses" typ ~fallback:[]
+
+ let mark_generated_rte () =
+ let list = all_statuses () in
+ let mark kf = List.iter (fun (_kind, set, _get) -> set kf true) list in
+ Globals.Functions.iter (fun kf -> if !Db.Value.is_called kf then mark kf)
+end
diff --git a/src/plugins/value/utils/eva_dynamic.mli b/src/plugins/value/utils/eva_dynamic.mli
new file mode 100644
index 00000000000..85648b91530
--- /dev/null
+++ b/src/plugins/value/utils/eva_dynamic.mli
@@ -0,0 +1,43 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Access to other plugins API via {Dynamic.get}. *)
+
+module Callgraph: sig
+ (** Iterates over all functions in the callgraph in reverse order, i.e. from
+ callees to callers. If callgraph is missing, the order is unspecified. *)
+ val iter_in_rev_order: (Kernel_function.t -> unit) -> unit
+
+ (** Returns [true] if [base] is a global, or a formal or local of either [kf]
+ or one of its callers. If callgraph is missing, always returns true. *)
+ val accept_base: Kernel_function.t -> Base.t -> bool
+end
+
+module Scope: sig
+ (** Removes redundant assertions. Warns if the scope plugin is missing. *)
+ val rm_asserts: unit -> unit
+end
+
+module RteGen: sig
+ (** Marks all RTE as generated. Does nothing if the rte plugin is missing. *)
+ val mark_generated_rte: unit -> unit
+end
--
GitLab