From b93d5c3bf5fcebb157cf449abbce9e6263bc9a84 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 18 Apr 2024 10:22:52 +0200
Subject: [PATCH] [Sparecode] Renames "select_slice_pragma" into
"select_slice_annot".
As slice pragmas have been replaced by slice ACSL extensions.
---
src/plugins/sparecode/Sparecode.mli | 4 ++--
src/plugins/sparecode/register.ml | 14 +++++++-------
src/plugins/sparecode/register.mli | 4 ++--
src/plugins/sparecode/spare_marks.ml | 11 ++++++-----
src/plugins/sparecode/spare_marks.mli | 2 +-
tests/saveload/load_one.ml | 2 +-
tests/slicing/combine.ml | 2 +-
7 files changed, 20 insertions(+), 19 deletions(-)
diff --git a/src/plugins/sparecode/Sparecode.mli b/src/plugins/sparecode/Sparecode.mli
index 6ed9b48f3a7..2487a7f1405 100644
--- a/src/plugins/sparecode/Sparecode.mli
+++ b/src/plugins/sparecode/Sparecode.mli
@@ -24,10 +24,10 @@
(** Interface for the unused code detection. *)
module Register: sig
- val get: select_annot:bool -> select_slice_pragma:bool -> Project.t
+ val get: select_annot:bool -> select_slice_annot:bool -> Project.t
(** Remove in each function what isn't used to compute its outputs,
or its annotations when [select_annot] is true,
- or its slicing pragmas when [select_slice_pragmas] is true.
+ or its slicing pragmas when [select_slice_annot] is true.
@return a new project where the sparecode has been removed.
*)
diff --git a/src/plugins/sparecode/register.ml b/src/plugins/sparecode/register.ml
index 77ca976d5c5..06889bca2e6 100644
--- a/src/plugins/sparecode/register.ml
+++ b/src/plugins/sparecode/register.ml
@@ -60,13 +60,13 @@ let rm_unused_globals ?new_proj_name ?(project=Project.current ()) () =
P.result "removed unused global declarations in new project '%s'" new_proj_name;
Project.on project Globs.rm_unused_decl new_proj_name
-let run select_annot select_slice_pragma =
+let run select_annot select_slice_annot =
P.feedback "remove unused code...";
(*let initial_file = Ast.get () in*)
let kf_entry, _library = Globals.entry_point () in
let proj =
Spare_marks.select_useful_things
- ~select_annot ~select_slice_pragma kf_entry
+ ~select_annot ~select_slice_annot kf_entry
in
let old_proj_name = Project.get_name (Project.current ()) in
let new_proj_name = (old_proj_name^" without sparecode") in
@@ -81,16 +81,16 @@ let run select_annot select_slice_pragma =
Project.copy ~selection:ctx new_prj;
new_prj
-let get ~select_annot ~select_slice_pragma =
+let get ~select_annot ~select_slice_annot =
Result.memo
- (fun _ -> run select_annot select_slice_pragma)
- (select_annot, select_slice_pragma)
+ (fun _ -> run select_annot select_slice_annot)
+ (select_annot, select_slice_annot)
let main () =
if Sparecode_params.Analysis.get () then begin
let select_annot = Sparecode_params.Annot.get () in
- let select_slice_pragma = true in
- let new_proj = get ~select_annot ~select_slice_pragma in
+ let select_slice_annot = true in
+ let new_proj = get ~select_annot ~select_slice_annot in
File.pretty_ast ~prj:new_proj ()
end
else if Sparecode_params.GlobDecl.get () then begin
diff --git a/src/plugins/sparecode/register.mli b/src/plugins/sparecode/register.mli
index 40470cd52d9..f912136d53e 100644
--- a/src/plugins/sparecode/register.mli
+++ b/src/plugins/sparecode/register.mli
@@ -20,10 +20,10 @@
(* *)
(**************************************************************************)
-val get: select_annot:bool -> select_slice_pragma:bool -> Project.t
+val get: select_annot:bool -> select_slice_annot:bool -> Project.t
(** Remove in each function what isn't used to compute its outputs,
or its annotations when [select_annot] is true,
- or its slicing pragmas when [select_slice_pragmas] is true.
+ or its slicing pragmas when [select_slice_annot] is true.
@return a new project where the sparecode has been removed. *)
val rm_unused_globals : ?new_proj_name:string -> ?project:Project.t -> unit -> Project.t
diff --git a/src/plugins/sparecode/spare_marks.ml b/src/plugins/sparecode/spare_marks.ml
index b37fe42620e..e6a15b273f8 100644
--- a/src/plugins/sparecode/spare_marks.ml
+++ b/src/plugins/sparecode/spare_marks.ml
@@ -321,7 +321,7 @@ class annot_visitor ~filter pdg = object (self)
in Cil.SkipChildren
end
-let select_annotations ~select_annot ~select_slice_pragma proj =
+let select_annotations ~select_annot ~select_slice_annot proj =
let visit_fun kf =
debug 1 "look for annotations in function %a@." Kernel_function.pretty kf;
let pdg = Pdg.Api.get kf in
@@ -329,13 +329,14 @@ let select_annotations ~select_annot ~select_slice_pragma proj =
else if PdgTypes.Pdg.is_bottom pdg
then debug 1 "pdg bottom: skip annotations"
else begin
+ let filter annot =
match annot.Cil_types.annot_content with
| Cil_types.AAssert _-> (* Never select alarms, they are not useful *)
(match Alarms.find annot with
| None -> select_annot
| Some _ -> false)
| AExtended (_, _, ext) when Logic_deps.is_slice_directive ext ->
- select_slice_pragma
+ select_slice_annot
| _ -> select_annot
in
try
@@ -355,7 +356,7 @@ let finalize proj =
process_call_inputs proj;
assert (!call_in_to_check = [])
-let select_useful_things ~select_annot ~select_slice_pragma kf_entry =
+let select_useful_things ~select_annot ~select_slice_annot kf_entry =
let proj = new_project () in
assert (!call_in_to_check = []);
debug 1 "selecting function %a outputs and entry point@."
@@ -368,8 +369,8 @@ let select_useful_things ~select_annot ~select_slice_pragma kf_entry =
else begin
select_entry_point proj kf_entry pdg;
select_all_outputs proj kf_entry pdg;
- if (select_annot || select_slice_pragma) then
- select_annotations ~select_annot ~select_slice_pragma proj;
+ if (select_annot || select_slice_annot) then
+ select_annotations ~select_annot ~select_slice_annot proj;
finalize proj
end;
proj
diff --git a/src/plugins/sparecode/spare_marks.mli b/src/plugins/sparecode/spare_marks.mli
index e0e594a8d22..c75749b2736 100644
--- a/src/plugins/sparecode/spare_marks.mli
+++ b/src/plugins/sparecode/spare_marks.mli
@@ -27,7 +27,7 @@ type proj
type fct
val select_useful_things :
- select_annot:bool -> select_slice_pragma:bool -> kernel_function -> proj
+ select_annot:bool -> select_slice_annot:bool -> kernel_function -> proj
val get_marks : proj -> kernel_function -> fct option
diff --git a/tests/saveload/load_one.ml b/tests/saveload/load_one.ml
index 02186193baa..c631c11a189 100644
--- a/tests/saveload/load_one.ml
+++ b/tests/saveload/load_one.ml
@@ -4,7 +4,7 @@ let () = at_exit (fun _ -> Sys.remove sav_file)
let main () =
let sparecode () =
- Sparecode.Register.get ~select_annot:false ~select_slice_pragma:false
+ Sparecode.Register.get ~select_annot:false ~select_slice_annot:false
in
let fp = Filepath.Normalized.of_string sav_file in
let p = sparecode () in
diff --git a/tests/slicing/combine.ml b/tests/slicing/combine.ml
index 363a5274467..eeda7fecc26 100644
--- a/tests/slicing/combine.ml
+++ b/tests/slicing/combine.ml
@@ -62,7 +62,7 @@ let main _ =
Format.printf "After Constant propagation :@.";
File.pretty_ast ~prj:proj3 ();
- let proj4 = Sparecode.Register.get ~select_annot:true ~select_slice_pragma:true in
+ let proj4 = Sparecode.Register.get ~select_annot:true ~select_slice_annot:true in
Format.printf "After Sparecode :@.";
File.pretty_ast ~prj:proj4 ();;
--
GitLab