From ddbed917265f84a833062a3d5eab3df5784dec88 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 20 Feb 2019 18:08:10 +0100
Subject: [PATCH] [rte] refactor high level API
---
src/plugins/rte/RteGen.mli | 24 ++++++----
src/plugins/rte/register.ml | 54 ++++++++++++++++++---
src/plugins/rte/visit.ml | 95 ++++++++++++++-----------------------
src/plugins/rte/visit.mli | 45 ++++++++----------
4 files changed, 118 insertions(+), 100 deletions(-)
diff --git a/src/plugins/rte/RteGen.mli b/src/plugins/rte/RteGen.mli
index 37f64d20dc0..aff86d1508f 100644
--- a/src/plugins/rte/RteGen.mli
+++ b/src/plugins/rte/RteGen.mli
@@ -31,12 +31,21 @@ module Generator : module type of Generator
(** Visitors to iterate over Alarms and/or generate Code-Annotations *)
module Visit : sig
open Cil_types
- val annotate_kf: kernel_function -> unit
- val do_all_rte: kernel_function -> unit
- val do_rte: kernel_function -> unit
- val do_stmt_annotations: kernel_function -> stmt -> code_annotation list
- val do_exp_annotations: kernel_function -> stmt -> exp -> code_annotation list
- val compute: unit -> unit
+
+ val annotate: ?flags:Flags.t -> kernel_function -> unit
+
+ val get_annotations_kf:
+ ?flags:Flags.t -> kernel_function -> code_annotation list
+
+ val get_annotations_stmt:
+ ?flags:Flags.t -> kernel_function -> stmt -> code_annotation list
+
+ val get_annotations_exp:
+ ?flags:Flags.t -> kernel_function -> stmt -> exp -> code_annotation list
+
+ val get_annotations_lval:
+ ?flags:Flags.t -> kernel_function -> stmt -> lval -> code_annotation list
+
type on_alarm = kernel_function -> stmt -> invalid:bool -> Alarms.alarm -> unit
type 'a iterator = ?flags:Flags.t -> on_alarm ->
Kernel_function.t -> Cil_types.stmt -> 'a -> unit
@@ -44,8 +53,7 @@ module Visit : sig
val iter_exp : exp iterator
val iter_instr : instr iterator
val iter_stmt : stmt iterator
- val annotation :
+ val register :
Emitter.t -> kernel_function -> stmt -> invalid:bool -> Alarms.alarm ->
code_annotation * bool
- val register : Emitter.t -> on_alarm
end
diff --git a/src/plugins/rte/register.ml b/src/plugins/rte/register.ml
index e5b0281e856..87386ea7f8b 100644
--- a/src/plugins/rte/register.ml
+++ b/src/plugins/rte/register.ml
@@ -20,6 +20,47 @@
(* *)
(**************************************************************************)
+(* -------------------------------------------------------------------------- *)
+(* dedicated computations *)
+(* -------------------------------------------------------------------------- *)
+
+open Flags
+
+(* annotate for all rte + unsigned overflows (which are not rte), for a given
+ function *)
+let do_all_rte kf =
+ let flags =
+ { Flags.all with
+ signed_downcast = false;
+ unsigned_downcast = false; }
+ in
+ Visit.annotate ~flags kf
+
+(* annotate for rte only (not unsigned overflows and downcasts) for a given
+ function *)
+let do_rte kf =
+ let flags =
+ { Flags.all with
+ unsigned_overflow = false;
+ signed_downcast = false;
+ unsigned_downcast = false; }
+ in
+ Visit.annotate ~flags kf
+
+let compute () =
+ (* compute RTE annotations, whether Enabled is set or not *)
+ Ast.compute () ;
+ let include_function kf =
+ let fsel = Options.FunctionSelection.get () in
+ Kernel_function.Set.is_empty fsel
+ || Kernel_function.Set.mem kf fsel
+ in
+ Globals.Functions.iter
+ (fun kf -> if include_function kf then !Db.RteGen.annotate_kf kf)
+
+
+(* journal utilities *)
+
let journal_register ?comment is_dyn name ty_arg fctref fct =
let ty = Datatype.func ty_arg Datatype.unit in
Db.register (Db.Journalize("RteGen." ^ name, ty)) fctref fct;
@@ -34,17 +75,16 @@ let nojournal_register fctref fct =
let () =
journal_register false
- "annotate_kf" Kernel_function.ty Db.RteGen.annotate_kf Visit.annotate_kf;
- journal_register false "compute" Datatype.unit Db.RteGen.compute
- Visit.compute;
+ "annotate_kf" Kernel_function.ty Db.RteGen.annotate_kf Visit.annotate;
+ journal_register false "compute" Datatype.unit Db.RteGen.compute compute;
journal_register true
~comment:"Generate all RTE annotations in the \
given function."
- "do_all_rte" Kernel_function.ty Db.RteGen.do_all_rte Visit.do_all_rte;
+ "do_all_rte" Kernel_function.ty Db.RteGen.do_all_rte do_all_rte;
journal_register false
~comment:"Generate all RTE annotations except pre-conditions \
in the given function."
- "do_rte" Kernel_function.ty Db.RteGen.do_rte Visit.do_rte;
+ "do_rte" Kernel_function.ty Db.RteGen.do_rte do_rte;
let open Generator in
let open Db.RteGen in
nojournal_register get_signedOv_status Signed_overflow.accessor;
@@ -94,7 +134,7 @@ let _ =
(Datatype.func2 Kernel_function.ty Cil_datatype.Stmt.ty
(let module L = Datatype.List(Cil_datatype.Code_annotation) in L.ty))
~journalize:false
- Visit.do_stmt_annotations
+ Visit.get_annotations_stmt
let _ =
Dynamic.register
@@ -105,7 +145,7 @@ let _ =
(Datatype.func3 Kernel_function.ty Cil_datatype.Stmt.ty Cil_datatype.Exp.ty
(let module L = Datatype.List(Cil_datatype.Code_annotation) in L.ty))
~journalize:false
- Visit.do_exp_annotations
+ Visit.get_annotations_exp
let main () =
(* reset "rte generated"/"called precond generated" properties for all
diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml
index 4487c5bdfff..9bd7ee4f39b 100644
--- a/src/plugins/rte/visit.ml
+++ b/src/plugins/rte/visit.ml
@@ -343,12 +343,11 @@ end
type on_alarm = kernel_function -> stmt -> invalid:bool -> Alarms.alarm -> unit
+let filter = function None -> Flags.default () | Some flags -> flags
+
let iter_alarms visit ?flags (on_alarm:on_alarm) kf stmt element =
- let flags = match flags with
- | None -> default ()
- | Some opt -> opt in
let visitor = object (self)
- inherit annot_visitor kf flags (on_alarm kf)
+ inherit annot_visitor kf (filter flags) (on_alarm kf)
initializer self#push_stmt stmt
end in
ignore (visit (visitor :> Cil.cilVisitor) element)
@@ -367,40 +366,51 @@ let iter_stmt : stmt iterator = iter_alarms Cil.visitCilStmt
let status ~invalid =
if invalid then Some Property_status.False_if_reachable else None
-let annotation emitter kf stmt ~invalid alarm =
+let register emitter kf stmt ~invalid alarm =
let status = status ~invalid in
Alarms.register emitter ~kf (Kstmt stmt) ?status alarm
-let register emitter kf stmt ~invalid alarm =
- ignore (annotation emitter kf stmt ~invalid alarm)
-
-(** {2 List of all RTEs on a given Cil object} *)
+(* -------------------------------------------------------------------------- *)
+(* --- List Code Annotations --- *)
+(* -------------------------------------------------------------------------- *)
-let get_annotations from kf stmt x =
- let flags = default () in
- (* Accumulator containing all the code_annots corresponding to an alarm
- emitted so far. *)
- let code_annots = ref [] in
+let collector () =
+ let pool = ref [] in
let on_alarm stmt ~invalid:_ alarm =
let ca, _ = Alarms.to_annot (Kstmt stmt) alarm in
- code_annots := ca :: !code_annots;
- in
- let o = object (self)
- inherit annot_visitor kf flags on_alarm
+ pool := ca :: !pool ;
+ in pool , on_alarm
+
+let get_annotations_kf ?flags kf =
+ match kf.fundec with
+ | Declaration _ -> []
+ | Definition(f, _) ->
+ let pool,on_alarm = collector () in
+ let visitor = new annot_visitor kf (filter flags) on_alarm in
+ ignore (Visitor.visitFramacFunction visitor f) ; !pool
+
+let collect from flags kf stmt elt =
+ let pool,on_alarm = collector () in
+ let visitor = object (self)
+ inherit annot_visitor kf (filter flags) on_alarm
initializer self#push_stmt stmt
end in
- ignore (from (o :> Cil.cilVisitor) x);
- !code_annots
+ ignore (from (visitor :> Cil.cilVisitor) elt); !pool
-let do_stmt_annotations kf stmt =
- get_annotations Cil.visitCilStmt kf stmt stmt
+let get_annotations_stmt ?flags kf stmt =
+ collect Cil.visitCilStmt flags kf stmt stmt
-let do_exp_annotations = get_annotations Cil.visitCilExpr
+let get_annotations_exp ?flags kf stmt exp =
+ collect Cil.visitCilExpr flags kf stmt exp
+
+let get_annotations_lval ?flags kf stmt lv =
+ collect Cil.visitCilLval flags kf stmt lv
(** {2 Annotations of kernel_functions for a given type of RTE} *)
(* generates annotation for function kf on the basis of [flags] *)
-let annotate_kf_aux flags kf =
+let annotate ?flags kf =
+ let flags = filter flags in
Options.debug "annotating function %a" Kernel_function.pretty kf;
match kf.fundec with
| Declaration _ -> ()
@@ -437,7 +447,7 @@ let annotate_kf_aux flags kf =
Options.feedback "annotating function %a" Kernel_function.pretty kf;
let warn = Options.Warn.get () in
let on_alarm stmt ~invalid alarm =
- let ca, _ = annotation Generator.emitter kf stmt ~invalid alarm in
+ let ca, _ = register Generator.emitter kf stmt ~invalid alarm in
if warn && invalid then
Options.warn "@[guaranteed RTE:@ %a@]"
Printer.pp_code_annotation ca
@@ -448,41 +458,6 @@ let annotate_kf_aux flags kf =
List.iter (fun f -> f ()) !to_update;
end
-(* generates annotation for function kf on the basis of command-line options *)
-let annotate_kf kf = annotate_kf_aux (default ()) kf
-
-(* annotate for all rte + unsigned overflows (which are not rte), for a given
- function *)
-let do_all_rte kf =
- let flags =
- { Flags.all with
- signed_downcast = false;
- unsigned_downcast = false; }
- in
- annotate_kf_aux flags kf
-
-(* annotate for rte only (not unsigned overflows and downcasts) for a given
- function *)
-let do_rte kf =
- let flags =
- { Flags.all with
- unsigned_overflow = false;
- signed_downcast = false;
- unsigned_downcast = false; }
- in
- annotate_kf_aux flags kf
-
-let compute () =
- (* compute RTE annotations, whether Enabled is set or not *)
- Ast.compute () ;
- let include_function kf =
- let fsel = Options.FunctionSelection.get () in
- Kernel_function.Set.is_empty fsel
- || Kernel_function.Set.mem kf fsel
- in
- Globals.Functions.iter
- (fun kf -> if include_function kf then !Db.RteGen.annotate_kf kf)
-
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/plugins/rte/visit.mli b/src/plugins/rte/visit.mli
index 9c909a5706c..3fe997f0057 100644
--- a/src/plugins/rte/visit.mli
+++ b/src/plugins/rte/visit.mli
@@ -24,30 +24,27 @@
open Cil_types
-(** {2 RTE Generator API}
+(** {2 RTE Generator API} *)
- The all-in-one entry points of the RTE plugin.
-*)
+(** Annotate kernel-function with respect to options
+ and current generator status. *)
+val annotate: ?flags:Flags.t -> kernel_function -> unit
-(** Generates RTE for a single function. Uses the status of the various
- RTE options do decide which kinds of annotations must be generated.
-*)
-val annotate_kf: kernel_function -> unit
+(** Returns annotations associated to alarms {i without} registering them. *)
+val get_annotations_kf:
+ ?flags:Flags.t -> kernel_function -> code_annotation list
-(** Generates all RTEs for a given function. *)
-val do_all_rte: kernel_function -> unit
+(** Returns annotations associated to alarms {i without} registering them. *)
+val get_annotations_stmt:
+ ?flags:Flags.t -> kernel_function -> stmt -> code_annotation list
-(** Generates all RTEs except preconditions for a given function. *)
-val do_rte: kernel_function -> unit
+(** Returns annotations associated to alarms {i without} registering them. *)
+val get_annotations_exp:
+ ?flags:Flags.t -> kernel_function -> stmt -> exp -> code_annotation list
-val do_stmt_annotations: kernel_function -> stmt -> code_annotation list
-val do_exp_annotations: kernel_function -> stmt -> exp -> code_annotation list
-
-(** Main entry point of the plug-in, used by [-rte] option: computes
- RTE on the whole AST. Which kind of RTE is generated depends on the
- options given on the command line.
-*)
-val compute: unit -> unit
+(** Returns annotations associated to alarms {i without} registering them. *)
+val get_annotations_lval:
+ ?flags:Flags.t -> kernel_function -> stmt -> lval -> code_annotation list
(** {2 Low-Level RTE Iterators}
@@ -88,14 +85,12 @@ val status : invalid:bool -> Property_status.emitted_status option
(** Registers and returns the annotation associated with the alarm,
and a boolean flag indicating whether it has been freshly generated
- or not. *)
-val annotation :
- Emitter.t -> kernel_function -> stmt -> invalid:bool -> Alarms.alarm ->
+ or not. Simple wrapper over [Alarms.register]. *)
+val register :
+ Emitter.t ->
+ kernel_function -> stmt -> invalid:bool -> Alarms.alarm ->
code_annotation * bool
-(** A callback that simply register the annotation associated with the alarm. *)
-val register : Emitter.t -> on_alarm
-
(*
Local Variables:
compile-command: "make -C ../../.."
--
GitLab