From e804cb0578c677799ca8f50c1950ae23492c39ff Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 25 Jan 2024 11:15:35 +0100
Subject: [PATCH] [Inout] Changes and documents external API.
---
src/plugins/impact/pdg_aux.ml | 4 +-
src/plugins/inout/Inout.ml | 36 ++++++++++++++++++
src/plugins/inout/Inout.mli | 56 ++++++++++++++++++++++++++++
src/plugins/inout/outputs.mli | 1 +
src/plugins/reduc/collect.ml | 2 +-
src/plugins/scope/datascope.ml | 2 +-
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/reads.ml | 12 +++---
src/plugins/studia/writes.ml | 8 ++--
tests/slicing/simple_intra_slice.ml | 2 +-
15 files changed, 116 insertions(+), 25 deletions(-)
create mode 100644 src/plugins/inout/Inout.ml
create mode 100644 src/plugins/inout/Inout.mli
diff --git a/src/plugins/impact/pdg_aux.ml b/src/plugins/impact/pdg_aux.ml
index a486d6adbac..29097913041 100644
--- a/src/plugins/impact/pdg_aux.ml
+++ b/src/plugins/impact/pdg_aux.ml
@@ -166,9 +166,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 =
- Inout.Operational_inputs.get_internal_precise ~stmt:call_stmt kf_callee
- in
+ let inout = Inout.get_precise_inout ~stmt:call_stmt kf_callee in
inout.Inout_type.over_inputs_if_termination
in
let test_in acc (in_key, in_node) =
diff --git a/src/plugins/inout/Inout.ml b/src/plugins/inout/Inout.ml
new file mode 100644
index 00000000000..9eb53af878a
--- /dev/null
+++ b/src/plugins/inout/Inout.ml
@@ -0,0 +1,36 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+let expr_inputs = Inputs.expr
+let stmt_inputs = Inputs.statement
+let kf_inputs = Inputs.get_internal
+let kf_external_inputs = Inputs.get_external
+
+let stmt_outputs = Outputs.statement
+let kf_outputs = Outputs.get_internal
+let kf_external_outputs = Outputs.get_external
+
+let get_precise_inout = Operational_inputs.get_internal_precise
+
+let states = [ Inputs.self; Outputs.self ]
+let proxy = State_builder.Proxy.(create "inout" Both states)
+let self = State_builder.Proxy.get proxy
diff --git a/src/plugins/inout/Inout.mli b/src/plugins/inout/Inout.mli
new file mode 100644
index 00000000000..90a3cb7230e
--- /dev/null
+++ b/src/plugins/inout/Inout.mli
@@ -0,0 +1,56 @@
+(**************************************************************************)
+(* *)
+(* 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
+
+(** Returns the memory zone needed to evaluate the given expression at the
+ given statement. *)
+val expr_inputs: stmt -> exp -> Locations.Zone.t
+
+(** Returns the memory zone read by the given statement. *)
+val stmt_inputs: stmt -> Locations.Zone.t
+
+(** Returns the memory zone modified by the given statement. *)
+val stmt_outputs: stmt -> Locations.Zone.t
+
+(** Returns the memory zone read by the given function, including its
+ local and formal variables. *)
+val kf_inputs: kernel_function -> Locations.Zone.t
+
+(** Returns the memory zone read by the given function, without its
+ local and formal variables. *)
+val kf_external_inputs: kernel_function -> Locations.Zone.t
+
+(** Returns the memory zone modified by the given function, including its
+ local and formal variables. *)
+val kf_outputs: kernel_function -> Locations.Zone.t
+
+(** Returns the memory zone modified by the given function, without its
+ local and formal variables. *)
+val kf_external_outputs: kernel_function -> Locations.Zone.t
+
+(** Returns the inputs/outputs computed for the given function.
+ If [stmt] is specified and is a possible call to the given function,
+ returns the inputs/outputs for this call specifically. *)
+val get_precise_inout: ?stmt:stmt -> kernel_function -> Inout_type.t
+
+val self: State.t
diff --git a/src/plugins/inout/outputs.mli b/src/plugins/inout/outputs.mli
index 006d55cae5c..192edda7fa5 100644
--- a/src/plugins/inout/outputs.mli
+++ b/src/plugins/inout/outputs.mli
@@ -23,6 +23,7 @@
val self: State.t
val compute: Cil_types.kernel_function -> unit
+val get_internal: Cil_types.kernel_function -> Locations.Zone.t
val get_external: Cil_types.kernel_function -> Locations.Zone.t
val statement: Cil_types.stmt -> Locations.Zone.t
diff --git a/src/plugins/reduc/collect.ml b/src/plugins/reduc/collect.ml
index d19635aa3cd..d2192b5df7a 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 = Inout.Outputs.statement stmt in
+ let out = Inout.stmt_outputs 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 23c2421b339..29708325fc0 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= Inout.Operational_inputs.get_internal_precise ~stmt kf in
+ let inout= Inout.get_precise_inout ~stmt kf in
Locations.Zone.join out inout.Inout_type.over_outputs
in
match stmt.skind with
diff --git a/src/plugins/slicing/fct_slice.ml b/src/plugins/slicing/fct_slice.ml
index 6d09aef97e7..3818ca7685f 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 =
- Inout.Operational_inputs.get_internal_precise ~stmt:call kf in
+ Inout.get_precise_inout ~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 =
- Inout.Operational_inputs.get_internal_precise ~stmt:call kf in
+ Inout.get_precise_inout ~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 637319e1b3d..b5b773dad33 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 = Inout.Outputs.get_external kf in
+ let outputs = Inout.kf_external_outputs 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 (Inout.Outputs.get_external kf) ;
- select_inter_zone select_rd zone_rd_opt (Inout.Inputs.get_external kf)
+ select_inter_zone select_wr zone_wr_opt (Inout.kf_external_outputs kf) ;
+ select_inter_zone select_rd zone_rd_opt (Inout.kf_external_inputs kf)
end
));
!ac
diff --git a/src/plugins/slicing/slicingState.ml b/src/plugins/slicing/slicingState.ml
index bd8abdff686..a95aa8e3435 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; Inout.Inputs.self ; Inout.Outputs.self ])
+ [ Pdg.Api.self; Inout.self ])
let get () =
try P.get ()
diff --git a/src/plugins/sparecode/globs.ml b/src/plugins/sparecode/globs.ml
index dafe82987f4..a55dbb45410 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; Inout.Outputs.self ])
+ [ Pdg.Api.self; Inout.self ])
let rm_unused_decl =
Result.memo
diff --git a/src/plugins/sparecode/register.ml b/src/plugins/sparecode/register.ml
index 8e2d7af9f7e..b413b26e451 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; Inout.Outputs.self ])
+ [ Pdg.Api.self; Inout.self ])
module P = Sparecode_params
diff --git a/src/plugins/sparecode/spare_marks.ml b/src/plugins/sparecode/spare_marks.ml
index 48d1f2884d9..271a330669b 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 = Inout.Outputs.get_external kf in
+ let outputs = Inout.kf_external_outputs 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/reads.ml b/src/plugins/studia/reads.ml
index 457a6a17da9..058691cd35c 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 = Inout.Inputs.statement stmt in
+ let z = Inout.stmt_inputs stmt in
if Zone.intersects z zlval then begin
(* Computes what is read to evaluate [args] and [lvopt] *)
let deps =
- List.map (Inout.Inputs.expr stmt) args
+ List.map (Inout.expr_inputs 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 = Inout.Inputs.get_internal kf in
+ let inputs = Inout.kf_inputs 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 = Inout.Inputs.statement stmt in
+ let z = Inout.stmt_inputs 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 = Inout.Inputs.expr stmt e in
+ let z = Inout.expr_inputs 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 = Inout.Inputs.get_internal kf in
+ let all_in = Inout.kf_inputs 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 65a670198c4..4d566dfcc64 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 = Inout.Operational_inputs.get_internal_precise ~stmt kf in
+ let inout = Inout.get_precise_inout ~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 = Inout.Outputs.statement stmt in
+ let z = Inout.stmt_outputs 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 = Inout.Outputs.statement stmt in
+ let z = Inout.stmt_outputs 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 = Inout.Operational_inputs.get_internal_precise kf in
+ let all_out = Inout.get_precise_inout 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 a5df5c95d1f..e60a1638a7c 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 = Inout.Outputs.get_external fct in
+ let outs = Inout.kf_external_outputs fct in
Format.printf "Sorties de la fonction %s = %a\n"
fct_name Locations.Zone.pretty outs
in
--
GitLab