Merge branch 'feature/kernel/remove-db' into 'master'

[kernel] Removes module Postdominators and Security from Db.

See merge request frama-c/frama-c!4466

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} *)
 (* ************************************************************************* *)

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. *)

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

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)))

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

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:

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

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))
 )

src/plugins/postdominators/postdominators.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  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

src/plugins/postdominators/postdominators.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  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]. *)

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 =