From 42547d0ac3efed14b183fe4458381a8eca65e201 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Mon, 29 Jul 2019 14:53:08 +0200
Subject: [PATCH] [Kernel] add option -keep-unused-types
---
doc/userman/user-changes.tex | 8 +++++++
doc/userman/user-sources.tex | 4 ++++
man/frama-c.1 | 15 ++++++++++++-
man/frama-c.1.header | 4 ++--
man/frama-c.1.md | 8 +++++++
src/kernel_internals/typing/rmtmps.ml | 5 ++---
src/kernel_internals/typing/rmtmps.mli | 21 +++++++++----------
src/kernel_services/ast_queries/file.ml | 7 +++++--
.../plugin_entry_points/kernel.ml | 9 ++++++++
.../plugin_entry_points/kernel.mli | 5 ++++-
10 files changed, 66 insertions(+), 20 deletions(-)
diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index ed3e8db288f..7c2c49598b8 100644
--- a/doc/userman/user-changes.tex
+++ b/doc/userman/user-changes.tex
@@ -5,6 +5,14 @@ release. First we list changes of the last release.
\section*{\nextframacversion}
+\begin{itemize}
+\item \textbf{Normalizing the Source Code:} added options
+ \texttt{-keep-unused-types} and its opposite,
+ \texttt{-remove-unused-types}.
+\end{itemize}
+
+\section*{18.0 (Argon)}
+
\begin{itemize}
\item \textbf{Feedback Options:} change options governing status of warning categories
\item \textbf{Normalizing the Source Code:} added category \texttt{@inline} to
diff --git a/doc/userman/user-sources.tex b/doc/userman/user-sources.tex
index 1b0cd0706fd..8fc0e1180af 100644
--- a/doc/userman/user-sources.tex
+++ b/doc/userman/user-sources.tex
@@ -249,6 +249,10 @@ a negative value, and choose the smallest rank possible starting from
set by default. So you mostly use the opposite form, namely
\optiondef{-}{remove-unused-specified-functions}.
+\item \optiondef{-}{keep-unused-types} does not remove unused types and
+ enum/struct/union declarations. By default, such types are removed,
+ that is, its opposite option \optiondef{-}{remove-unused-types} is set.
+
\item \texttt{\optiondef{-}{machdep} <machine architecture name>} defines the
target platform. The default value is a \texttt{x86\_32} bits
platform. Analyzers may take into account the \emph{endianness} of the
diff --git a/man/frama-c.1 b/man/frama-c.1
index a9ad49458ae..052066d3bbb 100644
--- a/man/frama-c.1
+++ b/man/frama-c.1
@@ -25,7 +25,7 @@
.\" using pandoc 2.0 or newer. To modify this file, edit the Markdown file
.\" and run `make man/frama-c.1`.
-.TH FRAMA-C 1 2018-01-17
+.TH FRAMA-C 1 2019-07-29
.SH NAME
.PP
frama\-c[.byte] \- a static analyzer for C programs
@@ -403,6 +403,11 @@ see \f[B]\-remove\-unused\-specified\-functions\f[].
.RS
.RE
.TP
+.B \-keep\-unused\-types
+see \f[B]\-remove\-unused\-types\f[].
+.RS
+.RE
+.TP
.B \-kernel\-log \f[I]kind:file\f[]
copies log messages from the Frama\-C's kernel to file.
\f[I]kind\f[] specifies which kinds of messages to be copied (e.g.
@@ -587,6 +592,14 @@ Functions having the attribute \f[B]FRAMAC_BUILTIN\f[] are always kept.
.RS
.RE
.TP
+.B \-remove\-unused\-types
+remove types and struct/union/enum declarations that are not referenced
+anywhere else in the code.
+This is the default.
+Use \f[B]\-keep\-unused\-types\f[] to keep these definitions.
+.RS
+.RE
+.TP
.B \-safe\-arrays
for multidimensional arrays or arrays that are fields inside structs,
assumes that all accesses must be in bound (set by default).
diff --git a/man/frama-c.1.header b/man/frama-c.1.header
index 62f871e6410..e5046fe091c 100644
--- a/man/frama-c.1.header
+++ b/man/frama-c.1.header
@@ -2,7 +2,7 @@
.\"
.\" This file is part of Frama-C.
.\"
-.\" Copyright (C) 2007-2018
+.\" Copyright (C) 2007-2019
.\" CEA (Commissariat à l'énergie atomique et aux énergies
.\" alternatives)
.\"
@@ -25,4 +25,4 @@
.\" using pandoc 2.0 or newer. To modify this file, edit the Markdown file
.\" and run `make man/frama-c.1`.
-.TH FRAMA-C 1 2018-01-17
+.TH FRAMA-C 1 2019-07-29
diff --git a/man/frama-c.1.md b/man/frama-c.1.md
index b4aece519c7..7e21eccfa57 100644
--- a/man/frama-c.1.md
+++ b/man/frama-c.1.md
@@ -242,6 +242,9 @@ Defaults to no.
-keep-unused-specified-functions
: see **-remove-unused-specified-functions**.
+-keep-unused-types
+: see **-remove-unused-types**.
+
-kernel-log *kind:file*
: copies log messages from the Frama-C's kernel to file. *kind* specifies which
kinds of messages to be copied (e.g. **w** for warnings, **e** for errors,
@@ -359,6 +362,11 @@ functions were fully inlined.
in the code. This is the default. Functions having the attribute
**FRAMAC_BUILTIN** are always kept.
+-remove-unused-types
+: remove types and struct/union/enum declarations that are not referenced
+anywhere else in the code. This is the default. Use **-keep-unused-types**
+to keep these definitions.
+
-safe-arrays
: for multidimensional arrays or arrays that are fields inside structs,
assumes that all accesses must be in bound (set by default).
diff --git a/src/kernel_internals/typing/rmtmps.ml b/src/kernel_internals/typing/rmtmps.ml
index 64ada096ee7..49684281806 100644
--- a/src/kernel_internals/typing/rmtmps.ml
+++ b/src/kernel_internals/typing/rmtmps.ml
@@ -71,7 +71,6 @@ module InfoHashtbl = Hashtbl.Make(struct
| Var v -> Cil_datatype.Varinfo.hash v
end)
-(* Used by external plug-ins: *)
let keepUnused = ref false
(* Possibly no longer used: *)
@@ -885,10 +884,10 @@ let removeUnmarked isRoot ast reachable_tbl =
type rootsFilter = global -> bool
-let removeUnusedTemps ?(isRoot : rootsFilter = isExportedRoot) ast =
+let removeUnused ?(isRoot=isExportedRoot) ast =
if not !keepUnused then
begin
- Kernel.debug ~dkey "Removing unused temporaries" ;
+ Kernel.debug ~dkey "Removing unused" ;
(* digest any pragmas that would create additional roots *)
let keepers = categorizePragmas ast in
diff --git a/src/kernel_internals/typing/rmtmps.mli b/src/kernel_internals/typing/rmtmps.mli
index 510a6565b05..015a4f4dff3 100644
--- a/src/kernel_internals/typing/rmtmps.mli
+++ b/src/kernel_internals/typing/rmtmps.mli
@@ -51,18 +51,18 @@
(* Some clients may wish to augment or replace the standard strategy
* for finding the initially reachable roots. The optional
- * "isRoot" argument to Rmtmps.removeUnusedTemps grants this
- * flexibility. If given, it should name a function which will return
- * true if a given global should be treated as a retained root.
+ * "isRoot" argument to Rmtmps.removeUnused grants this
+ * flexibility. It specifies the globals which will serve as roots
+ * to be kept. Starting from these roots, all reachable (used) AST
+ * elements will be kept.
*
- * Function Rmtmps.isDefaultRoot encapsulates the default root
+ * Function [Rmtmps.isExportedRoot] encapsulates the default root
* collection, which consists of those global variables and functions
* which are visible to the linker and runtime loader. A client's
* root filter can use this if the goal is to augment rather than
- * replace the standard logic. Function Rmtmps.isExportedRoot is an
- * alternate name for this same function.
+ * replace the standard logic.
*
- * Function Rmtmps.isCompleteProgramRoot is an example of an alternate
+ * Function [Rmtmps.isCompleteProgramRoot] is an example of an alternate
* root collection. This function assumes that it is operating on a
* complete program rather than just one object file. It treats
* "main()" as a root, as well as any function carrying the
@@ -75,12 +75,11 @@
*)
-type rootsFilter = Cil_types.global -> bool
-val isExportedRoot : rootsFilter
-val isCompleteProgramRoot : rootsFilter
+val isExportedRoot : Cil_types.global -> bool
+val isCompleteProgramRoot : Cil_types.global -> bool
(* process a complete Cil file *)
-val removeUnusedTemps: ?isRoot:rootsFilter -> Cil_types.file -> unit
+val removeUnused: ?isRoot:(Cil_types.global -> bool) -> Cil_types.file -> unit
(** removes unused labels for which [is_removable] is true.
[is_removable] defaults to the negation of boolean flag of [Label]
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 60ee0168a45..356d822f8d2 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -607,8 +607,9 @@ let () =
(** Keep defined entry point even if not defined, and possibly the functions
with only specifications (according to parameter
keep_unused_specified_function). This function is meant to be passed to
- {!Rmtmps.removeUnusedTemps}. *)
+ {!Rmtmps.removeUnused}. *)
let keep_entry_point ?(specs=Kernel.Keep_unused_specified_functions.get ()) g =
+ let keepTypes = Kernel.Keep_unused_types.get () in
Rmtmps.isExportedRoot g ||
match g with
| GFun({svar = v; sspec = spec},_)
@@ -618,6 +619,8 @@ let keep_entry_point ?(specs=Kernel.Keep_unused_specified_functions.get ()) g =
|| (specs && not (is_empty_funspec spec))
(* and the declarations carrying specifications according to the
command line.*)
+ | GType _ | GCompTag _ | GCompTagDecl _ | GEnumTag _ | GEnumTagDecl _ ->
+ keepTypes
| _ -> false
let files_to_cabs_cil files =
@@ -1096,7 +1099,7 @@ let prepare_cil_file ast =
Transform_before_cleanup.apply ast;
(* Remove unused temp variables and globals. *)
Kernel.feedback ~level:2 "cleaning unused parts";
- Rmtmps.removeUnusedTemps ~isRoot:keep_entry_point ast;
+ Rmtmps.removeUnused ~isRoot:keep_entry_point ast;
if Kernel.Check.get () then begin
Filecheck.check_ast ~is_normalized:false ~ast "Removed temp vars"
end;
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index e77d3bf7ff4..02f357e8ebb 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -1131,6 +1131,15 @@ module Keep_unused_specified_functions =
let help = "keep specified-but-unused functions"
end)
+let () = Parameter_customize.set_group normalisation
+let () = Parameter_customize.set_negative_option_name "-remove-unused-types"
+module Keep_unused_types =
+ False(struct
+ let option_name = "-keep-unused-types"
+ let module_name = "Keep_unused_types"
+ let help = "keep unused types (false by default)"
+ end)
+
let () = Parameter_customize.set_group normalisation
module SimplifyTrivialLoops =
True(struct
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index cf9edf9d0fb..7976e6c8667 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -396,7 +396,10 @@ module KeepSwitch: Parameter_sig.Bool
(** Behavior of option "-keep-switch" *)
module Keep_unused_specified_functions: Parameter_sig.Bool
-(** Behavior of option "-keep-unused-specified-function". *)
+(** Behavior of option "-keep-unused-specified-functions". *)
+
+module Keep_unused_types: Parameter_sig.Bool
+(** Behavior of option "-keep-unused-types". *)
module SimplifyTrivialLoops: Parameter_sig.Bool
(** Behavior of option "-simplify-trivial-loops". *)
--
GitLab