From f240214b3567244ac8b7fd115380eb417431f757 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 24 Jan 2024 15:03:11 +0100
Subject: [PATCH] [kernel] remove Inout from Db
---
src/kernel_services/plugin_entry_points/db.ml | 110 ------------------
.../plugin_entry_points/db.mli | 85 --------------
.../eva/domains/cvalue/cvalue_domain.ml | 2 +-
src/plugins/eva/engine/transfer_stmt.ml | 2 +-
src/plugins/eva/gui/register_gui.ml | 8 +-
src/plugins/eva/utils/inout.ml | 48 ++++++++
src/plugins/eva/utils/inout.mli | 51 ++++++++
src/plugins/eva/utils/private.ml | 1 +
src/plugins/eva/utils/private.mli | 1 +
src/plugins/impact/pdg_aux.ml | 2 +-
src/plugins/inout/derefs.ml | 9 --
src/plugins/inout/inputs.ml | 18 +--
src/plugins/inout/inputs.mli | 8 ++
src/plugins/inout/operational_inputs.ml | 37 +++---
src/plugins/inout/operational_inputs.mli | 6 +
src/plugins/inout/outputs.ml | 15 ++-
src/plugins/inout/outputs.mli | 6 +
src/plugins/reduc/collect.ml | 2 +-
src/plugins/scope/datascope.ml | 2 +-
src/plugins/slicing/dune | 3 +-
src/plugins/slicing/fct_slice.ml | 4 +-
src/plugins/slicing/slicingCmds.ml | 6 +-
src/plugins/slicing/slicingState.ml | 2 +-
src/plugins/sparecode/globs.ml | 2 +-
src/plugins/sparecode/register.ml | 2 +-
src/plugins/sparecode/spare_marks.ml | 2 +-
src/plugins/studia/dune | 3 +-
src/plugins/studia/reads.ml | 12 +-
src/plugins/studia/writes.ml | 8 +-
tests/slicing/simple_intra_slice.ml | 2 +-
30 files changed, 190 insertions(+), 269 deletions(-)
create mode 100644 src/plugins/eva/utils/inout.ml
create mode 100644 src/plugins/eva/utils/inout.mli
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 76c8222d724..f323723913f 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -47,116 +47,6 @@ module Toplevel = struct
end
-(* ************************************************************************* *)
-(** {2 Inouts} *)
-(* ************************************************************************* *)
-
-module type INOUTKF = sig
- type t
- val self_internal: State.t ref
- val self_external: State.t ref
- val compute : (kernel_function -> unit) ref
-
- val get_internal : (kernel_function -> t) ref
- val get_external : (kernel_function -> t) ref
-
- val display : (Format.formatter -> kernel_function -> unit) ref
- val pretty : Format.formatter -> t -> unit
-end
-module type INOUT = sig
- include INOUTKF
- val statement : (stmt -> t) ref
- val kinstr : kinstr -> t option
-end
-
-(** State_builder.of outputs
- - over-approximation of zones written by each function. *)
-module Outputs = struct
- type t = Locations.Zone.t
- let self_internal = ref State.dummy
- let self_external = ref State.dummy
- let compute = mk_fun "Out.compute"
- let display = mk_fun "Out.display"
- let display_external = mk_fun "Out.display_external"
- let get_internal = mk_fun "Out.get_internal"
- let get_external = mk_fun "Out.get_external"
- let statement = mk_fun "Out.statement"
- let kinstr ki = match ki with
- | Kstmt s -> Some (!statement s)
- | Kglobal -> None
-
- let pretty = Locations.Zone.pretty
-end
-
-(** State_builder.of read inputs
- - over-approximation of locations read by each function. *)
-module Inputs = struct
- (* What about [Inputs.statement] ? *)
- type t = Locations.Zone.t
- let self_internal = ref State.dummy
- let self_external = ref State.dummy
- let self_with_formals = ref State.dummy
- let compute = mk_fun "Inputs.compute"
- let display = mk_fun "Inputs.display"
- let display_with_formals = mk_fun "Inputs.display_with_formals"
- let get_internal = mk_fun "Inputs.get_internal"
- let get_external = mk_fun "Inputs.get_external"
- let get_with_formals = mk_fun "Inputs.get_with_formals"
- let statement = mk_fun "Inputs.statement"
- let expr = mk_fun "Inputs.expr"
- let kinstr ki = match ki with
- | Kstmt s -> Some (!statement s)
- | Kglobal -> None
-
- let pretty = Locations.Zone.pretty
-end
-
-(** State_builder.of operational inputs
- - over-approximation of zones whose input values are read by each function,
- State_builder.of sure outputs
- - under-approximation of zones written by each function. *)
-module Operational_inputs = struct
- type t = Inout_type.t
- let self_internal = ref State.dummy
- let self_external = ref State.dummy
- let compute = mk_fun "Operational_inputs.compute"
- let display = mk_fun "Operational_inputs.display"
- let get_internal = mk_fun "Operational_inputs.get_internal"
- let get_internal_precise = ref (fun ?stmt:_ _ ->
- failwith ("Db.Operational_inputs.get_internal_precise not implemented"))
- let get_external = mk_fun "Operational_inputs.get_external"
-
- module Record_Inout_Callbacks = Hook.Build (struct type t = Inout_type.t end)
-
- let pretty fmt x =
- Format.fprintf fmt "@[<v>";
- Format.fprintf fmt "@[<v 2>Operational inputs:@ @[<hov>%a@]@]@ "
- Locations.Zone.pretty (x.Inout_type.over_inputs);
- Format.fprintf fmt "@[<v 2>Operational inputs on termination:@ @[<hov>%a@]@]@ "
- Locations.Zone.pretty (x.Inout_type.over_inputs_if_termination);
- Format.fprintf fmt "@[<v 2>Sure outputs:@ @[<hov>%a@]@]"
- Locations.Zone.pretty (x.Inout_type.under_outputs_if_termination);
- Format.fprintf fmt "@]";
-
-end
-
-(** Derefs computations *)
-module Derefs = struct
- type t = Locations.Zone.t
- let self_internal = ref State.dummy
- let self_external = ref State.dummy
- let compute = mk_fun "Derefs.compute"
- let display = mk_fun "Derefs.display"
- let get_internal = mk_fun "Derefs.get_internal"
- let get_external = mk_fun "Derefs.get_external"
- let statement = mk_fun "Derefs.statement"
- let kinstr ki = match ki with
- | Kstmt s -> Some (!statement s)
- | Kglobal -> None
-
- let pretty = Locations.Zone.pretty
-end
-
(* ************************************************************************* *)
(** {2 Others plugins} *)
(* ************************************************************************* *)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index e191d7d2f3a..65434ec1c10 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -145,91 +145,6 @@ module Security : sig
end
-(** Signature common to some Inout plugin options. The results of
- the computations are available on a per function basis. *)
-module type INOUTKF = sig
-
- type t
-
- val self_internal: State.t ref
- val self_external: State.t ref
-
- val compute : (kernel_function -> unit) ref
-
- val get_internal : (kernel_function -> t) ref
- (** Inputs/Outputs with local and formal variables *)
-
- val get_external : (kernel_function -> t) ref
- (** Inputs/Outputs without either local or formal variables *)
-
- (** {3 Pretty printing} *)
-
- val display : (Format.formatter -> kernel_function -> unit) ref
- val pretty : Format.formatter -> t -> unit
-
-end
-
-(** Signature common to inputs and outputs computations. The results
- are also available on a per-statement basis. *)
-module type INOUT = sig
- include INOUTKF
-
- val statement : (stmt -> t) ref
- val kinstr : kinstr -> t option
-end
-
-(** State_builder.of read inputs.
- That is over-approximation of zones read by each function.
- @see <../inout/Inputs.html> internal documentation. *)
-module Inputs : sig
-
- include INOUT with type t = Locations.Zone.t
-
- val expr : (stmt -> exp -> t) ref
-
- val self_with_formals: State.t ref
-
- val get_with_formals : (kernel_function -> t) ref
- (** Inputs with formals and without local variables *)
-
- val display_with_formals: (Format.formatter -> kernel_function -> unit) ref
-
-end
-
-(** State_builder.of outputs.
- That is over-approximation of zones written by each function.
- @see <../inout/Outputs.html> internal documentation. *)
-module Outputs : sig
- include INOUT with type t = Locations.Zone.t
- val display_external : (Format.formatter -> kernel_function -> unit) ref
-end
-
-(** State_builder.of operational inputs.
- That is:
- - over-approximation of zones whose input values are read by each function,
- State_builder.of sure outputs
- - under-approximation of zones written by each function.
- @see <../inout/Context.html> internal documentation. *)
-module Operational_inputs : sig
- include INOUTKF with type t = Inout_type.t
- val get_internal_precise: (?stmt:stmt -> kernel_function -> Inout_type.t) ref
- (** More precise version of [get_internal] function. If [stmt] is
- specified, and is a possible call to the given kernel_function,
- returns the operational inputs for this call. *)
-
- (**/**)
- (* Internal use *)
- module Record_Inout_Callbacks: Hook.Iter_hook with type param = Inout_type.t
- (**/**)
-end
-
-
-(**/**)
-(** Do not use yet.
- @see <../inout/Derefs.html> internal documentation. *)
-module Derefs : INOUT with type t = Locations.Zone.t
-(**/**)
-
(** {3 GUI} *)
(** This function should be called from time to time by all analysers taking
diff --git a/src/plugins/eva/domains/cvalue/cvalue_domain.ml b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
index 132a3c72d5f..39ec5355a64 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
@@ -411,7 +411,7 @@ module State = struct
then Cvalue.Model.cardinal_estimate values
else Cvalue.CardinalEstimate.one
in
- let outs = !Db.Outputs.get_internal kf in
+ let outs = Inout.Outputs.get_internal kf in
let outs = Locations.Zone.filter_base filter_generated_and_locals outs in
let header fmt =
Format.fprintf fmt "Values at end of function %a:%t"
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index 165dbf57cdd..710cda5a2cf 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -56,7 +56,7 @@ module InOutCallback =
end)
let register_callback () =
- Db.Operational_inputs.Record_Inout_Callbacks.extend_once InOutCallback.set
+ Inout.Operational_inputs.Record_Inout_Callbacks.extend_once InOutCallback.set
let () = Cmdline.run_after_configuring_stage register_callback
diff --git a/src/plugins/eva/gui/register_gui.ml b/src/plugins/eva/gui/register_gui.ml
index a24c62d362d..66a19c086f5 100644
--- a/src/plugins/eva/gui/register_gui.ml
+++ b/src/plugins/eva/gui/register_gui.ml
@@ -46,8 +46,8 @@ let used_var = UsedVarState.memo
Function_calls.partial_results () ||
try
let f = fst (Globals.entry_point ()) in
- let inputs = !Db.Inputs.get_external f in
- let outputs = !Db.Outputs.get_external f in
+ let inputs = Inout.Inputs.get_external f in
+ let outputs = Inout.Outputs.get_external f in
let b = Base.of_varinfo var in
Locations.Zone.mem_base b inputs || Locations.Zone.mem_base b outputs
with e ->
@@ -227,7 +227,7 @@ let gui_compute_values (main_ui:main_ui) =
then main_ui#launcher ()
let cleaned_outputs kf s =
- let outs = Db.Outputs.kinstr (Kstmt s) in
+ let outs = Inout.Outputs.kinstr (Kstmt s) in
let accept = Logic_inout.accept_base ~formals:true ~locals:true kf in
let filter = Locations.Zone.filter_base accept in
Option.map filter outs
@@ -251,7 +251,7 @@ let pretty_stmt_info (main_ui:main_ui) kf stmt =
match outs with
| Some outs ->
main_ui#pretty_information
- "Modifies @[<hov>%a@]@." Db.Outputs.pretty outs
+ "Modifies @[<hov>%a@]@." Locations.Zone.pretty outs
| _ -> ()
end
else main_ui#pretty_information "This code is dead@."
diff --git a/src/plugins/eva/utils/inout.ml b/src/plugins/eva/utils/inout.ml
new file mode 100644
index 00000000000..399e26b1c5c
--- /dev/null
+++ b/src/plugins/eva/utils/inout.ml
@@ -0,0 +1,48 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+module Outputs = struct
+ let ref_statement = ref (fun _ -> assert false)
+ let ref_get_external = ref (fun _ -> assert false)
+ let ref_get_internal = ref (fun _ -> assert false)
+
+ let kinstr = function
+ | Cil_types.Kstmt s -> Some (!ref_statement s)
+ | Kglobal -> None
+
+ let get_external kf = !ref_get_external kf
+ let get_internal kf = !ref_get_internal kf
+end
+
+module Inputs = struct
+ let ref_get_external = ref (fun _ -> assert false)
+
+ let get_external kf = !ref_get_external kf
+end
+
+(** State_builder.of operational inputs
+ - over-approximation of zones whose input values are read by each function,
+ State_builder.of sure outputs
+ - under-approximation of zones written by each function. *)
+module Operational_inputs = struct
+ module Record_Inout_Callbacks = Hook.Build (struct type t = Inout_type.t end)
+end
diff --git a/src/plugins/eva/utils/inout.mli b/src/plugins/eva/utils/inout.mli
new file mode 100644
index 00000000000..087dd364341
--- /dev/null
+++ b/src/plugins/eva/utils/inout.mli
@@ -0,0 +1,51 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+module Outputs :
+sig
+ val ref_statement : (Cil_types.stmt -> Locations.Zone.t) ref
+ val ref_get_external : (Cil_types.kernel_function -> Locations.Zone.t) ref
+ val ref_get_internal : (Cil_types.kernel_function -> Locations.Zone.t) ref
+
+ val kinstr : Cil_types.kinstr -> Locations.Zone.t option
+ val get_external : Cil_types.kernel_function -> Locations.Zone.t
+ val get_internal : Cil_types.kernel_function -> Locations.Zone.t
+end
+
+module Inputs :
+sig
+ val ref_get_external : (Cil_types.kernel_function -> Locations.Zone.t) ref
+ val get_external : Cil_types.kernel_function -> Locations.Zone.t
+end
+
+(** State_builder.of operational inputs.
+ That is:
+ - over-approximation of zones whose input values are read by each function,
+ State_builder.of sure outputs
+ - under-approximation of zones written by each function.
+ @see <../inout/Context.html> internal documentation. *)
+module Operational_inputs : sig
+ (**/**)
+ (* Internal use *)
+ module Record_Inout_Callbacks: Hook.Iter_hook with type param = Inout_type.t
+ (**/**)
+end
diff --git a/src/plugins/eva/utils/private.ml b/src/plugins/eva/utils/private.ml
index e4a368655a9..15a046d096a 100644
--- a/src/plugins/eva/utils/private.ml
+++ b/src/plugins/eva/utils/private.ml
@@ -41,6 +41,7 @@ module Eval_op = Eval_op
module Eval_terms = Eval_terms
module Eval_typ = Eval_typ
module Function_calls = Function_calls
+module Inout = Inout
module Logic_inout = Logic_inout
module Main_locations = Main_locations
module Main_values = Main_values
diff --git a/src/plugins/eva/utils/private.mli b/src/plugins/eva/utils/private.mli
index f7037715286..6386a914cd8 100644
--- a/src/plugins/eva/utils/private.mli
+++ b/src/plugins/eva/utils/private.mli
@@ -45,6 +45,7 @@ module Eval_op = Eval_op
module Eval_terms = Eval_terms
module Eval_typ = Eval_typ
module Function_calls = Function_calls
+module Inout = Inout
module Logic_inout = Logic_inout
module Main_locations = Main_locations
module Main_values = Main_values
diff --git a/src/plugins/impact/pdg_aux.ml b/src/plugins/impact/pdg_aux.ml
index c6ecfcf8c6e..a486d6adbac 100644
--- a/src/plugins/impact/pdg_aux.ml
+++ b/src/plugins/impact/pdg_aux.ml
@@ -167,7 +167,7 @@ let find_call_input_nodes pdg_caller call_stmt ?(z=Locations.Zone.top) in_key =
let all_call_input_nodes ~caller:pdg_caller ~callee:(kf_callee, pdg_callee) call_stmt =
let real_inputs =
let inout =
- !Db.Operational_inputs.get_internal_precise ~stmt:call_stmt kf_callee
+ Inout.Operational_inputs.get_internal_precise ~stmt:call_stmt kf_callee
in
inout.Inout_type.over_inputs_if_termination
in
diff --git a/src/plugins/inout/derefs.ml b/src/plugins/inout/derefs.ml
index f7115d4022a..0a1d04589e8 100644
--- a/src/plugins/inout/derefs.ml
+++ b/src/plugins/inout/derefs.ml
@@ -108,12 +108,3 @@ let pretty_external fmt kf =
Format.fprintf fmt "@[Derefs for function %a:@\n@[<hov 2> %a@]@]@\n"
Kernel_function.pretty kf
Zone.pretty (get_external kf)
-
-let () =
- Db.Derefs.self_internal := Analysis.Memo.self;
- Db.Derefs.self_external := Externals.self;
- Db.Derefs.get_internal := get_internal;
- Db.Derefs.get_external := get_external;
- Db.Derefs.compute := compute_external;
- Db.Derefs.display := pretty_external;
- Db.Derefs.statement := Analysis.statement
diff --git a/src/plugins/inout/inputs.ml b/src/plugins/inout/inputs.ml
index 1de8961fa3e..b99014f2018 100644
--- a/src/plugins/inout/inputs.ml
+++ b/src/plugins/inout/inputs.ml
@@ -163,7 +163,7 @@ let get_with_formals kf =
(Eva.Logic_inout.accept_base ~formals:true ~locals:false kf)
(get_internal kf)
-let compute_external kf = ignore (get_external kf)
+let compute kf = ignore (get_external kf)
let pretty_external fmt kf =
Format.fprintf fmt "@[Inputs for function %a:@\n@[<hov 2> %a@]@]@\n"
@@ -175,18 +175,12 @@ let pretty_with_formals fmt kf =
Kernel_function.pretty kf
Zone.pretty (get_with_formals kf)
+let self = Externals.self
+let statement = Analysis.statement
+let expr = Analysis.expr
+
let () =
- Db.Inputs.self_internal := Analysis.Memo.self;
- Db.Inputs.self_external := Externals.self;
- Db.Inputs.self_with_formals := Analysis.Memo.self;
- Db.Inputs.get_internal := get_internal;
- Db.Inputs.get_external := get_external;
- Db.Inputs.get_with_formals := get_with_formals;
- Db.Inputs.compute := compute_external;
- Db.Inputs.display := pretty_external;
- Db.Inputs.display_with_formals := pretty_with_formals;
- Db.Inputs.statement := Analysis.statement;
- Db.Inputs.expr := Analysis.expr
+ Eva__Private.Inout.Inputs.ref_get_external := get_external
(*
Local Variables:
diff --git a/src/plugins/inout/inputs.mli b/src/plugins/inout/inputs.mli
index 593785adddf..93148f6a94e 100644
--- a/src/plugins/inout/inputs.mli
+++ b/src/plugins/inout/inputs.mli
@@ -20,5 +20,13 @@
(* *)
(**************************************************************************)
+val self: State.t
+
+val compute: Cil_types.kernel_function -> unit
+val get_external: Cil_types.kernel_function -> Locations.Zone.t
+val get_internal: Cil_types.kernel_function -> Locations.Zone.t
+val statement: Cil_types.stmt -> Locations.Zone.t
+val expr: Cil_types.stmt -> Cil_types.exp -> Locations.Zone.t
+
val pretty_external: Format.formatter -> Cil_types.kernel_function -> unit
val pretty_with_formals: Format.formatter -> Cil_types.kernel_function -> unit
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index 8f658d124e1..227ac8101eb 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -486,19 +486,23 @@ let compute_externals_using_prototype ?stmt kf =
let internals = compute_using_prototype ?stmt kf in
externalize ~with_formals:false kf internals
+let ref_get_internal = ref (fun _kf : t -> assert false)
+
let get_internal_aux ?stmt kf =
match stmt with
- | None -> !Db.Operational_inputs.get_internal kf
+ | None -> !ref_get_internal kf
| Some stmt ->
try CallwiseResults.find (kf, Kstmt stmt)
with Not_found ->
if Eva.Analysis.use_spec_instead_of_definition kf then
compute_using_prototype ~stmt kf
- else !Db.Operational_inputs.get_internal kf
+ else !ref_get_internal kf
+
+let ref_get_external = ref (fun _kf : t -> assert false)
let get_external_aux ?stmt kf =
match stmt with
- | None -> !Db.Operational_inputs.get_external kf
+ | None -> !ref_get_external kf
| Some stmt ->
try
let internals = CallwiseResults.find (kf, Kstmt stmt) in
@@ -508,7 +512,7 @@ let get_external_aux ?stmt kf =
let r = compute_externals_using_prototype ~stmt kf in
CallwiseResults.add (kf, Kstmt stmt) r;
r
- else !Db.Operational_inputs.get_external kf
+ else !ref_get_external kf
let extract_inout_from_froms froms =
let open Function_Froms in
@@ -580,7 +584,7 @@ module Callwise = struct
| [] -> Inout_parameters.fatal "callwise: internal stack is empty"
let end_record callstack kf inout =
- Db.Operational_inputs.Record_Inout_Callbacks.apply inout;
+ Eva__Private.Inout.Operational_inputs.Record_Inout_Callbacks.apply inout;
let callsite = Eva.Callstack.top_callsite callstack in
match callsite, !call_inout_stack with
| Kstmt _, (_caller, table) :: _ ->
@@ -765,7 +769,7 @@ module Externals =
let size = 17
end)
let get_external = Externals.memo (raw_externals ~with_formals:false)
-let compute_external kf = ignore (get_external kf)
+let compute kf = ignore (get_external kf)
@@ -795,17 +799,22 @@ let pretty_operational_inputs_external_with_formals fmt kf =
Kernel_function.pretty kf
Inout_type.pretty_operational_inputs (get_external_with_formals kf)
+let pretty fmt x =
+ Format.fprintf fmt "@[<v>";
+ Format.fprintf fmt "@[<v 2>Operational inputs:@ @[<hov>%a@]@]@ "
+ Locations.Zone.pretty (x.Inout_type.over_inputs);
+ Format.fprintf fmt "@[<v 2>Operational inputs on termination:@ @[<hov>%a@]@]@ "
+ Locations.Zone.pretty (x.Inout_type.over_inputs_if_termination);
+ Format.fprintf fmt "@[<v 2>Sure outputs:@ @[<hov>%a@]@]"
+ Locations.Zone.pretty (x.Inout_type.under_outputs_if_termination);
+ Format.fprintf fmt "@]"
+let get_internal_precise = get_internal_aux
-let () =
- Db.Operational_inputs.self_internal := Internals.self;
- Db.Operational_inputs.self_external := Externals.self;
- Db.Operational_inputs.get_internal := get_internal;
- Db.Operational_inputs.get_external := get_external;
- Db.Operational_inputs.get_internal_precise := get_internal_aux;
- Db.Operational_inputs.compute := compute_external;
- Db.Operational_inputs.display := pretty_operational_inputs_internal
+let () =
+ ref_get_internal := get_internal;
+ ref_get_external := get_external
(*
Local Variables:
diff --git a/src/plugins/inout/operational_inputs.mli b/src/plugins/inout/operational_inputs.mli
index 3c54c51db8c..2a545e374ea 100644
--- a/src/plugins/inout/operational_inputs.mli
+++ b/src/plugins/inout/operational_inputs.mli
@@ -22,12 +22,18 @@
open Cil_types
+val compute: kernel_function -> unit
+
val get_external: kernel_function -> Inout_type.t
val get_external_aux: ?stmt:stmt -> kernel_function -> Inout_type.t
+val get_internal_precise: ?stmt:stmt -> kernel_function -> Inout_type.t
+
val pretty_operational_inputs_internal:
Format.formatter -> kernel_function -> unit
val pretty_operational_inputs_external:
Format.formatter -> kernel_function -> unit
val pretty_operational_inputs_external_with_formals:
Format.formatter -> kernel_function -> unit
+
+val pretty: Format.formatter -> Inout_type.t -> unit
diff --git a/src/plugins/inout/outputs.ml b/src/plugins/inout/outputs.ml
index 14c8ee4b6bf..1caf9f4d01b 100644
--- a/src/plugins/inout/outputs.ml
+++ b/src/plugins/inout/outputs.ml
@@ -171,15 +171,14 @@ let pretty_external fmt kf =
with Not_found ->
()
+let self = Externals.self
+let compute kf = ignore (get_internal kf)
+let statement = Analysis.statement
+
let () =
- Db.Outputs.self_internal := Analysis.Memo.self;
- Db.Outputs.self_external := Externals.self;
- Db.Outputs.get_internal := get_internal;
- Db.Outputs.get_external := get_external;
- Db.Outputs.compute := (fun kf -> ignore (get_internal kf));
- Db.Outputs.display := pretty_internal;
- Db.Outputs.display_external := pretty_external;
- Db.Outputs.statement := Analysis.statement
+ Eva__Private.Inout.Outputs.ref_statement := Analysis.statement ;
+ Eva__Private.Inout.Outputs.ref_get_external := get_external ;
+ Eva__Private.Inout.Outputs.ref_get_internal := get_internal
(*
Local Variables:
diff --git a/src/plugins/inout/outputs.mli b/src/plugins/inout/outputs.mli
index 4fe03b173c6..006d55cae5c 100644
--- a/src/plugins/inout/outputs.mli
+++ b/src/plugins/inout/outputs.mli
@@ -20,5 +20,11 @@
(* *)
(**************************************************************************)
+val self: State.t
+
+val compute: Cil_types.kernel_function -> unit
+val get_external: Cil_types.kernel_function -> Locations.Zone.t
+val statement: Cil_types.stmt -> Locations.Zone.t
+
val pretty_external: Format.formatter -> Cil_types.kernel_function -> unit
val pretty_internal: Format.formatter -> Cil_types.kernel_function -> unit
diff --git a/src/plugins/reduc/collect.ml b/src/plugins/reduc/collect.ml
index ad7b55351d3..d19635aa3cd 100644
--- a/src/plugins/reduc/collect.ml
+++ b/src/plugins/reduc/collect.ml
@@ -122,7 +122,7 @@ class inout_vis
with Kernel_function.No_Statement -> assert false
method !vstmt stmt =
- let out = !Db.Outputs.statement stmt in
+ let out = Inout.Outputs.statement stmt in
let filter_out vi =
let open Locations in
let zone = enumerate_bits (loc_of_varinfo vi) in
diff --git a/src/plugins/scope/datascope.ml b/src/plugins/scope/datascope.ml
index f992fda8da2..23c2421b339 100644
--- a/src/plugins/scope/datascope.ml
+++ b/src/plugins/scope/datascope.ml
@@ -87,7 +87,7 @@ let get_writes stmt lval =
let register_modified_zones lmap stmt =
let register lmap zone = InitSid.add_zone lmap zone stmt in
let aux_out out kf =
- let inout= !Db.Operational_inputs.get_internal_precise ~stmt kf in
+ let inout= Inout.Operational_inputs.get_internal_precise ~stmt kf in
Locations.Zone.join out inout.Inout_type.over_outputs
in
match stmt.skind with
diff --git a/src/plugins/slicing/dune b/src/plugins/slicing/dune
index 23df7d7c78f..fda67cdea22 100644
--- a/src/plugins/slicing/dune
+++ b/src/plugins/slicing/dune
@@ -27,6 +27,7 @@
(echo "Slicing:" %{lib-available:frama-c-slicing.core} "\n")
(echo " - Pdg:" %{lib-available:frama-c-pdg.core} "\n")
(echo " - Sparecode:" %{lib-available:frama-c-sparecode.core} "\n")
+ (echo " - Inout" %{lib-available:frama-c-inout.core} "\n")
)
)
)
@@ -36,7 +37,7 @@
(optional)
(public_name frama-c-slicing.core)
(flags -open Frama_c_kernel :standard -w -9)
- (libraries frama-c.kernel frama-c-pdg.core frama-c-sparecode.core)
+ (libraries frama-c.kernel frama-c-inout.core frama-c-pdg.core frama-c-sparecode.core)
(instrumentation (backend landmarks))
(instrumentation (backend bisect_ppx))
)
diff --git a/src/plugins/slicing/fct_slice.ml b/src/plugins/slicing/fct_slice.ml
index 7611cece658..6d09aef97e7 100644
--- a/src/plugins/slicing/fct_slice.ml
+++ b/src/plugins/slicing/fct_slice.ml
@@ -424,7 +424,7 @@ end = struct
let add_mark =
let kf = fi_to_call.SlicingInternals.fi_kf in
let op_inputs =
- !Db.Operational_inputs.get_internal_precise ~stmt:call kf in
+ Inout.Operational_inputs.get_internal_precise ~stmt:call kf in
let z = op_inputs.Inout_type.over_inputs in
match s with
| PdgMarks.SelNode (_, None) -> true
@@ -1308,7 +1308,7 @@ let apply_change_call ff call f_to_call =
try
let kf = ff_to_call.SlicingInternals.ff_fct.SlicingInternals.fi_kf in
let op_inputs =
- !Db.Operational_inputs.get_internal_precise ~stmt:call kf in
+ Inout.Operational_inputs.get_internal_precise ~stmt:call kf in
let z = op_inputs.Inout_type.over_inputs in
(*Format.printf "##Call at %a,@ kf %a,@ @[Z %a@]@."
Cil.d_loc (Cil_datatype.Stmt.loc call)
diff --git a/src/plugins/slicing/slicingCmds.ml b/src/plugins/slicing/slicingCmds.ml
index 38c151c53b0..637319e1b3d 100644
--- a/src/plugins/slicing/slicingCmds.ml
+++ b/src/plugins/slicing/slicingCmds.ml
@@ -247,7 +247,7 @@ let select_func_calls_to set ~spare kf =
SlicingMarks.mk_user_mark ~data:nspare ~addr:nspare ~ctrl:nspare
in
assert (Eva.Analysis.is_computed ());
- let outputs = !Db.Outputs.get_external kf in
+ let outputs = Inout.Outputs.get_external kf in
select_entry_point_and_some_inputs_outputs set ~mark kf
~return:true
~outputs
@@ -407,8 +407,8 @@ let select_lval_rw set mark ~rd ~wr ~eval kf ki_opt=
in
assert (Eva.Results.is_called kf) ; (* otherwise [!Db.Outputs.get_external kf] gives weird results *)
- select_inter_zone select_wr zone_wr_opt (!Db.Outputs.get_external kf) ;
- select_inter_zone select_rd zone_rd_opt (!Db.Inputs.get_external kf)
+ select_inter_zone select_wr zone_wr_opt (Inout.Outputs.get_external kf) ;
+ select_inter_zone select_rd zone_rd_opt (Inout.Inputs.get_external kf)
end
));
!ac
diff --git a/src/plugins/slicing/slicingState.ml b/src/plugins/slicing/slicingState.ml
index 082deff8194..bd8abdff686 100644
--- a/src/plugins/slicing/slicingState.ml
+++ b/src/plugins/slicing/slicingState.ml
@@ -34,7 +34,7 @@ let () =
(fun () ->
State_dependency_graph.add_codependencies
~onto:self
- [ Pdg.Api.self; !Db.Inputs.self_external; !Db.Outputs.self_external ])
+ [ Pdg.Api.self; Inout.Inputs.self ; Inout.Outputs.self ])
let get () =
try P.get ()
diff --git a/src/plugins/sparecode/globs.ml b/src/plugins/sparecode/globs.ml
index 08f1df99b3b..dafe82987f4 100644
--- a/src/plugins/sparecode/globs.ml
+++ b/src/plugins/sparecode/globs.ml
@@ -160,7 +160,7 @@ let () =
(fun () ->
State_dependency_graph.add_codependencies
~onto:Result.self
- [ Pdg.Api.self; !Db.Outputs.self_external ])
+ [ Pdg.Api.self; Inout.Outputs.self ])
let rm_unused_decl =
Result.memo
diff --git a/src/plugins/sparecode/register.ml b/src/plugins/sparecode/register.ml
index 0a90bf35987..8e2d7af9f7e 100644
--- a/src/plugins/sparecode/register.ml
+++ b/src/plugins/sparecode/register.ml
@@ -43,7 +43,7 @@ let () =
(fun () ->
State_dependency_graph.add_codependencies
~onto:Result.self
- [ Pdg.Api.self; !Db.Outputs.self_external ])
+ [ Pdg.Api.self; Inout.Outputs.self ])
module P = Sparecode_params
diff --git a/src/plugins/sparecode/spare_marks.ml b/src/plugins/sparecode/spare_marks.ml
index e41b498caea..48d1f2884d9 100644
--- a/src/plugins/sparecode/spare_marks.ml
+++ b/src/plugins/sparecode/spare_marks.ml
@@ -280,7 +280,7 @@ let select_entry_point proj _kf pdg =
select_pdg_elements proj pdg to_select
let select_all_outputs proj kf pdg =
- let outputs = !Db.Outputs.get_external kf in
+ let outputs = Inout.Outputs.get_external kf in
debug 1 "@[selecting output zones %a@]" Locations.Zone.pretty outputs;
try
let nodes, undef = Pdg.Api.find_location_nodes_at_end pdg outputs in
diff --git a/src/plugins/studia/dune b/src/plugins/studia/dune
index cb4cc468ce9..daf095129ec 100644
--- a/src/plugins/studia/dune
+++ b/src/plugins/studia/dune
@@ -26,6 +26,7 @@
(action (progn
(echo "Studia:" %{lib-available:frama-c-studia.core} "\n")
(echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
+ (echo " - Inout:" %{lib-available:frama-c-inout.core} "\n")
)
)
)
@@ -35,7 +36,7 @@
(optional)
(public_name frama-c-studia.core)
(flags -open Frama_c_kernel :standard)
- (libraries frama-c.kernel frama-c-eva.core)
+ (libraries frama-c.kernel frama-c-eva.core frama-c-inout.core)
(instrumentation (backend landmarks))
(instrumentation (backend bisect_ppx))
)
diff --git a/src/plugins/studia/reads.ml b/src/plugins/studia/reads.ml
index 3bebf797fa3..457a6a17da9 100644
--- a/src/plugins/studia/reads.ml
+++ b/src/plugins/studia/reads.ml
@@ -37,11 +37,11 @@ class find_read zlval = object
method! vstmt_aux stmt =
let aux_call lvopt _kf args _loc =
- let z = !Db.Inputs.statement stmt in
+ let z = Inout.Inputs.statement stmt in
if Zone.intersects z zlval then begin
(* Computes what is read to evaluate [args] and [lvopt] *)
let deps =
- List.map (!Db.Inputs.expr stmt) args
+ List.map (Inout.Inputs.expr stmt) args
in
let deps = List.fold_left Zone.join Zone.bottom deps in
let deps = match lvopt with
@@ -54,7 +54,7 @@ class find_read zlval = object
(* now determine if the functions called at [stmt] read directly or
indirectly [zlval] *)
let aux_kf (direct, indirect) kf =
- let inputs = !Db.Inputs.get_internal kf in
+ let inputs = Inout.Inputs.get_internal kf in
(* TODO: change to this once we can get "full" inputs through Inout.
Currently, non operational inputs disappear, and this function
is not suitable.
@@ -85,13 +85,13 @@ class find_read zlval = object
Cil.treat_constructor_as_func aux_call v f args k l;
Cil.SkipChildren
| Instr _ ->
- let z = !Db.Inputs.statement stmt in
+ let z = Inout.Inputs.statement stmt in
if Zone.intersects z zlval then begin
res <- Direct stmt :: res
end;
Cil.SkipChildren
| If (e, _, _, _) | Switch (e, _, _, _) | Return (Some e, _) ->
- let z = !Db.Inputs.expr stmt e in
+ let z = Inout.Inputs.expr stmt e in
if Zone.intersects z zlval then begin
res <- Direct stmt :: res
end;
@@ -104,7 +104,7 @@ end
let compute z =
let vis = new find_read z in
let aux_kf_fundec kf =
- let all_in = !Db.Inputs.get_internal kf in
+ let all_in = Inout.Inputs.get_internal kf in
if Zone.intersects all_in z then begin
let fundec = Kernel_function.get_definition kf in
ignore
diff --git a/src/plugins/studia/writes.ml b/src/plugins/studia/writes.ml
index d5a2f6b0584..65a670198c4 100644
--- a/src/plugins/studia/writes.ml
+++ b/src/plugins/studia/writes.ml
@@ -65,7 +65,7 @@ let compare w1 w2 =
(** Does the functions called at [stmt] modify directly or indirectly [zlval] *)
let effects_of_call stmt zlval effects =
let aux_kf (direct, indirect) kf =
- let inout = !Db.Operational_inputs.get_internal_precise ~stmt kf in
+ let inout = Inout.Operational_inputs.get_internal_precise ~stmt kf in
let out = inout.Inout_type.over_outputs in
if Zone.intersects out zlval then
if Eva.Analysis.use_spec_instead_of_definition kf then
@@ -89,7 +89,7 @@ class find_write_insts zlval = object (self)
let aux_call lvopt _kf _args _loc =
(* Direct effect through the writing of [lvopt], or indirect inside
the call. *)
- let z = !Db.Outputs.statement stmt in
+ let z = Inout.Outputs.statement stmt in
if Zone.intersects z zlval then
let direct = match lvopt with
| None -> false
@@ -106,7 +106,7 @@ class find_write_insts zlval = object (self)
match i with
| Set _ | Local_init(_, AssignInit _, _) ->
(* Effect only throuh the written l-value *)
- let z = !Db.Outputs.statement stmt in
+ let z = Inout.Outputs.statement stmt in
if Zone.intersects z zlval then begin
res <- Assign stmt :: res
end
@@ -123,7 +123,7 @@ end
let inst_writes z =
let vis = new find_write_insts z in
let aux_kf_fundec kf =
- let all_out = !Db.Operational_inputs.get_internal_precise kf in
+ let all_out = Inout.Operational_inputs.get_internal_precise kf in
let zout = all_out.Inout_type.over_outputs in
if Zone.intersects zout z then begin
let fundec = Kernel_function.get_definition kf in
diff --git a/tests/slicing/simple_intra_slice.ml b/tests/slicing/simple_intra_slice.ml
index 7a7e189a1c9..a5df5c95d1f 100644
--- a/tests/slicing/simple_intra_slice.ml
+++ b/tests/slicing/simple_intra_slice.ml
@@ -47,7 +47,7 @@ let main _ =
in
let print_outputs fct_name =
let fct = Globals.Functions.find_by_name fct_name in
- let outs = !Db.Outputs.get_external fct in
+ let outs = Inout.Outputs.get_external fct in
Format.printf "Sorties de la fonction %s = %a\n"
fct_name Locations.Zone.pretty outs
in
--
GitLab