diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 76e276df1248309ee211af152114ef11409d228e..365cbf36d5e5dfec6b09b31ed1089312760095f4 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -20,22 +20,8 @@
(* *)
(**************************************************************************)
-open Cil_types
-open Cil_datatype
open Extlib
-let register r f = r := f
-
-let register_compute name deps r f =
- let name = "!Db." ^ name in
- let compute, self = State_builder.apply_once name deps f in
- r := compute;
- self
-
-let register_guarded_compute is_computed r f =
- let compute () = if not (is_computed ()) then f () in
- r := compute
-
module Main = struct
include Hook.Make()
let play = mk_fun "Main.play"
@@ -47,52 +33,6 @@ module Toplevel = struct
end
-(* ************************************************************************* *)
-(** {2 Others plugins} *)
-(* ************************************************************************* *)
-
-module Security = struct
- let run_whole_analysis = mk_fun "Security.run_whole_analysis"
- let run_ai_analysis = mk_fun "Security.run_ai_analysis"
- let run_slicing_analysis = mk_fun "Security.run_slicing_analysis"
- let self = ref State.dummy
-end
-
-module PostdominatorsTypes = struct
- exception Top
-
- module type Sig = sig
- val compute: (kernel_function -> unit) ref
- val stmt_postdominators:
- (kernel_function -> stmt -> Stmt.Hptset.t) ref
- val is_postdominator:
- (kernel_function -> opening:stmt -> closing:stmt -> bool) ref
- val display: (unit -> unit) ref
- val print_dot : (string -> kernel_function -> unit) ref
- end
-end
-
-
-module Postdominators = struct
- let compute = mk_fun "Postdominators.compute"
- let is_postdominator
- : (kernel_function -> opening:stmt -> closing:stmt -> bool) ref
- = mk_fun "Postdominators.is_postdominator"
- let stmt_postdominators = mk_fun "Postdominators.stmt_postdominators"
- let display = mk_fun "Postdominators.display"
- let print_dot = mk_fun "Postdominators.print_dot"
-end
-
-module PostdominatorsValue = struct
- let compute = mk_fun "PostdominatorsValue.compute"
- let is_postdominator
- : (kernel_function -> opening:stmt -> closing:stmt -> bool) ref
- = mk_fun "PostdominatorsValue.is_postdominator"
- let stmt_postdominators = mk_fun "PostdominatorsValue.stmt_postdominators"
- let display = mk_fun "PostdominatorsValue.display"
- let print_dot = mk_fun "PostdominatorsValue.print_dot"
-end
-
(* ************************************************************************* *)
(** {2 GUI} *)
(* ************************************************************************* *)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index bd5c3f533520ca08101f51ece57e337c88596a0a..e7d04befcc2991a6b84725468d1f43cd09b83286 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -45,27 +45,6 @@
line)
*)
-open Cil_types
-open Cil_datatype
-
-(* ************************************************************************* *)
-(** {2 Registering} *)
-(* ************************************************************************* *)
-
-val register: 'a ref -> 'a -> unit
-(** Plugins must register values with this function. *)
-
-val register_compute:
- string ->
- State.t list ->
- (unit -> unit) ref -> (unit -> unit) -> State.t
-
-val register_guarded_compute:
- (unit -> bool) ->
- (unit -> unit) ref -> (unit -> unit) -> unit
-(** @before 26.0-Iron there was a string parameter (first position) that was
- only used for Journalization, that has been removed. *)
-
(** Frama-C main interface.
@since Lithium-20081201
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
@@ -96,55 +75,6 @@ module Toplevel: sig
end
-(* ************************************************************************* *)
-(** {2 Plugins} *)
-(* ************************************************************************* *)
-
-(** Declarations common to the various postdominators-computing modules *)
-module PostdominatorsTypes: sig
-
- exception Top
- (** Used for postdominators-related functions, when the
- postdominators of a statement cannot be computed. It means that
- there is no path from this statement to the function return. *)
-
- module type Sig = sig
- val compute: (kernel_function -> unit) ref
-
- val stmt_postdominators:
- (kernel_function -> stmt -> Stmt.Hptset.t) ref
- (** @raise Top (see above) *)
-
- val is_postdominator:
- (kernel_function -> opening:stmt -> closing:stmt -> bool) ref
-
- val display: (unit -> unit) ref
-
- val print_dot : (string -> kernel_function -> unit) ref
- (** Print a representation of the postdominators in a dot file
- whose name is [basename.function_name.dot]. *)
- end
-end
-
-module Postdominators: PostdominatorsTypes.Sig
-
-module PostdominatorsValue: PostdominatorsTypes.Sig
-
-module Security : sig
-
- val run_whole_analysis: (unit -> unit) ref
- (** Run all the security analysis. *)
-
- val run_ai_analysis: (unit -> unit) ref
- (** Only run the analysis by abstract interpretation. *)
-
- val run_slicing_analysis: (unit -> Project.t) ref
- (** Only run the security slicing pre-analysis. *)
-
- val self: State.t ref
-
-end
-
(** {3 GUI} *)
(** Registered daemon on progress. *)
diff --git a/src/plugins/eva/domains/taint_domain.ml b/src/plugins/eva/domains/taint_domain.ml
index 4c37d351ce496021ba57d010b0577c792356c66f..d87271e5fc76bf07ad4dbb2de40e9b2b76fa3ec2 100644
--- a/src/plugins/eva/domains/taint_domain.ml
+++ b/src/plugins/eva/domains/taint_domain.ml
@@ -172,7 +172,7 @@ module TransferTaint = struct
let assume_stmts =
Stmt.Set.filter
(fun assume_stmt ->
- not (!Db.Postdominators.is_postdominator kf
+ not (Postdominators.is_postdominator kf
~opening:assume_stmt ~closing:stmt))
state.assume_stmts
in
diff --git a/src/plugins/eva/dune b/src/plugins/eva/dune
index 7023a1e20869441630a0ce257e11798603971a3f..66e75d5fb6c5738a5fac9570a71e8c8c1743dce1 100644
--- a/src/plugins/eva/dune
+++ b/src/plugins/eva/dune
@@ -28,6 +28,7 @@
(echo "EVA:" %{lib-available:frama-c-eva.core} "\n")
(echo " - ppx_deriving.eq:" %{lib-available:ppx_deriving.eq} "\n")
(echo " - ppx_deriving.ord:" %{lib-available:ppx_deriving.ord} "\n")
+ (echo " - Postdominators:" %{lib-available:frama-c-postdominators.core} "\n")
(echo "Numerors:" %{lib-available:frama-c-eva.numerors.core} "\n")
(echo " - MLMPFR:" %{lib-available:mlmpfr} "\n")
(echo "Apron domains:" %{lib-available:frama-c-eva.apron.core} "\n")
@@ -41,7 +42,7 @@
(optional)
(public_name frama-c-eva.core)
(flags -open Frama_c_kernel :standard -w -9)
- (libraries frama-c.kernel frama-c-server.core)
+ (libraries frama-c.kernel frama-c-server.core frama-c-postdominators.core)
(instrumentation (backend landmarks))
(instrumentation (backend bisect_ppx))
(preprocess (staged_pps ppx_deriving.eq ppx_deriving.ord)))
diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index 05546ac6a42726e3760d7bdc5e3d69c6834681f0..af8c23cbca592da73d5a42f76f7275a57d30082f 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -485,7 +485,7 @@ struct
let map' =
ZoneStmtMap.fold
(fun k _v acc_map ->
- if !Db.Postdominators.is_postdominator kf ~opening:k ~closing:s
+ if Postdominators.is_postdominator kf ~opening:k ~closing:s
then ZoneStmtMap.remove k acc_map
else acc_map
) map map
diff --git a/src/plugins/postdominators/compute.ml b/src/plugins/postdominators/compute.ml
index 865519b776cc4c9bfc4ae6d71f83285795c44735..c2e20b2ea2e19d21b45d4ad40ca709c1e53e13cc 100644
--- a/src/plugins/postdominators/compute.ml
+++ b/src/plugins/postdominators/compute.ml
@@ -79,6 +79,8 @@ end
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
+exception Top
+
module type MakePostDomArg = sig
val is_accessible: stmt -> bool
(* Evaluation of an expression which is supposed to be the condition of an
@@ -155,7 +157,7 @@ struct
end
module PostCompute = Dataflow2.Backwards(PostComputer)
- let compute_postdom kf =
+ let compute kf =
let return =
try Kernel_function.find_return kf
with Kernel_function.No_Statement ->
@@ -183,9 +185,9 @@ struct
let get_stmt_postdominators f stmt =
let do_it () = PostDom.find stmt in
try do_it ()
- with Not_found -> compute_postdom f; do_it ()
+ with Not_found -> compute f; do_it ()
- (** @raise Db.PostdominatorsTypes.Top when the statement postdominators
+ (** @raise Top when the statement postdominators
* have not been computed ie neither the return statement is reachable,
* nor the statement is in a natural loop. *)
let stmt_postdominators f stmt =
@@ -194,73 +196,30 @@ struct
Postdominators_parameters.debug ~level:1 "Postdom for %d are %a"
stmt.sid Stmt.Hptset.pretty s;
s
- | DomSet.Top -> raise Db.PostdominatorsTypes.Top
+ | DomSet.Top -> raise Top
let is_postdominator f ~opening ~closing =
let open_postdominators = get_stmt_postdominators f opening in
DomSet.mem closing open_postdominators
- let display_postdom () =
+ let display () =
let disp_all fmt =
PostDom.iter
(fun k v -> Format.fprintf fmt "Stmt:%d -> @[%a@]\n"
k.sid PostComputer.pretty v)
in Postdominators_parameters.result "%t" disp_all
- let print_dot_postdom basename kf =
- let filename = basename ^ "." ^ Kernel_function.get_name kf ^ ".dot" in
- Print.build_dot filename kf;
- Postdominators_parameters.result "dot file generated in %s" filename
-
end
-module PostDomDb(X: MakePostDomArg)(DbPostDom: Db.PostdominatorsTypes.Sig) =
-struct
- include MakePostDom(X)
-
- let () = DbPostDom.compute := compute_postdom
- let () = DbPostDom.is_postdominator := is_postdominator
- let () = DbPostDom.stmt_postdominators := stmt_postdominators
- let () = DbPostDom.display := display_postdom
- let () = DbPostDom.print_dot := print_dot_postdom
-
+module PostDomArg = struct
+ let is_accessible _ = true
+ let dependencies = []
+ let name = "basic"
+ let eval_cond _ _ = true, true
end
-module PostDomBasic =
- PostDomDb(
- struct
- let is_accessible _ = true
- let dependencies = []
- let name = "basic"
- let eval_cond _ _ = true, true
- end)
- (Db.Postdominators)
-
-
-let output () =
- let dot_postdom = Postdominators_parameters.DotPostdomBasename.get () in
- if dot_postdom <> "" then (
- Ast.compute ();
- Globals.Functions.iter (fun kf ->
- if Kernel_function.is_definition kf then
- !Db.Postdominators.print_dot dot_postdom kf)
- )
-
-let output, _ = State_builder.apply_once "Postdominators.Compute.output"
- [PostDomBasic.PostDom.self] output
-
-let () = Db.Main.extend output
-
-
-include
- PostDomDb
- (struct
- let is_accessible = Eva.Results.is_reachable
- let dependencies = [ Eva.Analysis.self ]
- let name = "value"
- let eval_cond stmt _e = Eva.Results.condition_truth_value stmt
- end)
- (Db.PostdominatorsValue)
+include MakePostDom (PostDomArg)
+let self = PostDom.self
(*
Local Variables:
diff --git a/src/plugins/postdominators/compute.mli b/src/plugins/postdominators/compute.mli
index 297da3eb394ab648696630993141f5f678a7b1ef..aa82a20dd8d7fd47b7b3777679c24052daf036bb 100644
--- a/src/plugins/postdominators/compute.mli
+++ b/src/plugins/postdominators/compute.mli
@@ -20,4 +20,22 @@
(* *)
(**************************************************************************)
-(** Register the plugin in the Frama-C kernel. Nothing is exported. *)
+open Cil_types
+
+exception Top
+(** Used for postdominators-related functions, when the
+ postdominators of a statement cannot be computed. It means that
+ there is no path from this statement to the function return. *)
+
+val compute: kernel_function -> unit
+
+val stmt_postdominators:
+ kernel_function -> stmt -> Cil_datatype.Stmt.Hptset.t
+(** @raise Top (see above) *)
+
+val is_postdominator:
+ kernel_function -> opening:stmt -> closing:stmt -> bool
+
+val display: unit -> unit
+
+val self: State.t
diff --git a/src/plugins/postdominators/dune b/src/plugins/postdominators/dune
index 6bcbe0cb1c77ffa55fccff8c6b57d6008edd4550..8a6ab690eab5946a4c1d21bd93e8f2f35eff9df6 100644
--- a/src/plugins/postdominators/dune
+++ b/src/plugins/postdominators/dune
@@ -25,7 +25,6 @@
(deps (universe))
(action (progn
(echo "Postdominators:" %{lib-available:frama-c-postdominators.core} "\n")
- (echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
)
)
)
@@ -35,7 +34,7 @@
(optional)
(public_name frama-c-postdominators.core)
(flags -open Frama_c_kernel :standard -w -9)
- (libraries frama-c.kernel frama-c-eva.core)
+ (libraries frama-c.kernel)
(instrumentation (backend landmarks))
(instrumentation (backend bisect_ppx))
)
diff --git a/src/plugins/postdominators/postdominators.ml b/src/plugins/postdominators/postdominators.ml
new file mode 100644
index 0000000000000000000000000000000000000000..d9273a0790d5e53a0f199245b637d219c8acdfc4
--- /dev/null
+++ b/src/plugins/postdominators/postdominators.ml
@@ -0,0 +1,42 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+include Compute
+
+let print_dot basename kf =
+ let filename = basename ^ "." ^ Kernel_function.get_name kf ^ ".dot" in
+ Print.build_dot filename kf;
+ Postdominators_parameters.result "dot file generated in %s" filename
+
+let output () =
+ let dot_postdom = Postdominators_parameters.DotPostdomBasename.get () in
+ if dot_postdom <> "" then (
+ Ast.compute ();
+ Globals.Functions.iter (fun kf ->
+ if Kernel_function.is_definition kf then
+ print_dot dot_postdom kf)
+ )
+
+let output, _ = State_builder.apply_once "Postdominators.Compute.output"
+ [Compute.self] output
+
+let () = Db.Main.extend output
diff --git a/src/plugins/postdominators/postdominators.mli b/src/plugins/postdominators/postdominators.mli
new file mode 100644
index 0000000000000000000000000000000000000000..8cdf15ad26b4273e437a3d35677270afc3bd37f9
--- /dev/null
+++ b/src/plugins/postdominators/postdominators.mli
@@ -0,0 +1,43 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+exception Top
+(** Used for postdominators-related functions, when the
+ postdominators of a statement cannot be computed. It means that
+ there is no path from this statement to the function return. *)
+
+val compute: kernel_function -> unit
+
+val stmt_postdominators:
+ kernel_function -> stmt -> Cil_datatype.Stmt.Hptset.t
+(** @raise Top (see above) *)
+
+val is_postdominator:
+ kernel_function -> opening:stmt -> closing:stmt -> bool
+
+val display: unit -> unit
+
+val print_dot : string -> kernel_function -> unit
+(** Print a representation of the postdominators in a dot file
+ whose name is [basename.function_name.dot]. *)
diff --git a/src/plugins/postdominators/print.ml b/src/plugins/postdominators/print.ml
index 8c3e12a26545048dfa19c0cf39d3da8ff382d6bb..698fee2b848a3bac44d0fe767a1dbe93ab9b372a 100644
--- a/src/plugins/postdominators/print.ml
+++ b/src/plugins/postdominators/print.ml
@@ -88,14 +88,14 @@ let get_postdom kf graph s =
| Some l -> l
with Not_found ->
try
- let postdom = !Db.Postdominators.stmt_postdominators kf s in
+ let postdom = Compute.stmt_postdominators kf s in
let postdom = Stmt.Hptset.remove s postdom in
Postdominators_parameters.debug "postdom for %d:%a = %a\n"
s.sid pretty_stmt s Stmt.Hptset.pretty postdom;
Kinstr.Hashtbl.add graph (Kstmt s) (Some postdom); postdom
- with Db.PostdominatorsTypes.Top ->
+ with Compute.Top ->
Kinstr.Hashtbl.add graph (Kstmt s) None;
- raise Db.PostdominatorsTypes.Top
+ raise Compute.Top
(** [s_postdom] are [s] postdominators, including [s].
* We don't have to represent the relation between s and s.
@@ -110,7 +110,7 @@ let reduce kf graph s =
let p_postdom = get_postdom kf graph p in
let s_postdom = Stmt.Hptset.diff s_postdom p_postdom
in s_postdom
- with Db.PostdominatorsTypes.Top -> assert false
+ with Compute.Top -> assert false
(* p postdom s -> cannot be top *)
else s_postdom (* p has already been removed from s_postdom *)
in
@@ -120,7 +120,7 @@ let reduce kf graph s =
Postdominators_parameters.debug "new postdom for %d:%a = %a\n"
s.sid pretty_stmt s Stmt.Hptset.pretty postdom;
Kinstr.Hashtbl.replace graph (Kstmt s) (Some postdom)
- with Db.PostdominatorsTypes.Top ->
+ with Compute.Top ->
()
let build_reduced_graph kf graph stmts =