From 4b2ac79a89f03d5d557c70bde35d28ddbe7112d9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 25 Jan 2019 13:52:34 +0100
Subject: [PATCH] [rte] low-level visitor API
---
src/plugins/rte/RteGen.mli | 50 +++++++++++++++++++++++++++++++++++++-
src/plugins/rte/visit.ml | 43 ++++++++++++++++++++++++++++++++
src/plugins/rte/visit.mli | 41 +++++++++++++++++++++++++++++++
3 files changed, 133 insertions(+), 1 deletion(-)
diff --git a/src/plugins/rte/RteGen.mli b/src/plugins/rte/RteGen.mli
index 9926f78e4a0..bd2f3ac38d5 100644
--- a/src/plugins/rte/RteGen.mli
+++ b/src/plugins/rte/RteGen.mli
@@ -20,4 +20,52 @@
(* *)
(**************************************************************************)
-(** No function is directly exported: they are registered in {!Db.Value}. *)
+(** Some functions are also registered in {!Db.Value}. *)
+
+open Cil_types
+
+module Visit :
+sig
+
+ (** Low-level iterator
+
+ [generator ~options:... on_alarm kf stmt element] iterates over
+ potential alarms for Cil element, located in the given
+ kernel_function and stmt.
+
+ The [on_alarm ki ?status alarm] callback is invoked with
+ the k-instruction originating the alarm and the already known status,
+ if any.
+
+ Potential alarms can be specified by the provided options,
+ with defaults generated from the Kernel options and the RTE plug-in
+ options.
+ *)
+ type 'a generator =
+ ?remove_trivial:bool ->
+ ?initialized:Options.DoInitialized.t ->
+ ?mem_access:Options.DoMemAccess.t ->
+ ?div_mod:Options.DoDivMod.t ->
+ ?shift:Options.DoShift.t ->
+ ?left_shift_negative:Kernel.LeftShiftNegative.t ->
+ ?right_shift_negative:Kernel.RightShiftNegative.t ->
+ ?signed_overflow:Kernel.SignedOverflow.t ->
+ ?unsigned_overflow:Kernel.UnsignedOverflow.t ->
+ ?signed_downcast:Kernel.SignedDowncast.t ->
+ ?unsigned_downcast:Kernel.UnsignedDowncast.t ->
+ ?float_to_int:Options.DoFloatToInt.t ->
+ ?finite_float:bool ->
+ ?pointer_call:Options.DoPointerCall.t ->
+ ?bool_value:Kernel.InvalidBool.t ->
+ (Cil_types.kinstr ->
+ ?status:Property_status.emitted_status -> Alarms.alarm -> unit) ->
+ Kernel_function.t ->
+ Cil_types.stmt ->
+ 'a -> unit
+
+ val iter_lval : lval generator
+ val iter_exp : exp generator
+ val iter_instr : instr generator
+ val iter_stmt : stmt generator
+
+end
diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml
index 869f5788986..7b28afc6cd8 100644
--- a/src/plugins/rte/visit.ml
+++ b/src/plugins/rte/visit.ml
@@ -445,6 +445,49 @@ let rte_annotations stmt =
stmt
[]
+(** {2 Iterate over Alarms on Cil elements} *)
+
+type 'a generator =
+ ?remove_trivial:bool ->
+ ?initialized:Options.DoInitialized.t ->
+ ?mem_access:Options.DoMemAccess.t ->
+ ?div_mod:Options.DoDivMod.t ->
+ ?shift:Options.DoShift.t ->
+ ?left_shift_negative:Kernel.LeftShiftNegative.t ->
+ ?right_shift_negative:Kernel.RightShiftNegative.t ->
+ ?signed_overflow:Kernel.SignedOverflow.t ->
+ ?unsigned_overflow:Kernel.UnsignedOverflow.t ->
+ ?signed_downcast:Kernel.SignedDowncast.t ->
+ ?unsigned_downcast:Kernel.UnsignedDowncast.t ->
+ ?float_to_int:Options.DoFloatToInt.t ->
+ ?finite_float:bool ->
+ ?pointer_call:Options.DoPointerCall.t ->
+ ?bool_value:Kernel.InvalidBool.t ->
+ (Cil_types.kinstr ->
+ ?status:Property_status.emitted_status -> Alarms.alarm -> unit) ->
+ Kernel_function.t ->
+ Cil_types.stmt ->
+ 'a -> unit
+
+let iter_alarms visit to_annot on_alarm kf stmt element =
+ let visitor = object (self)
+ inherit annot_visitor kf to_annot on_alarm
+ initializer self#push_stmt stmt
+ end in
+ ignore (visit (visitor :> Cil.cilVisitor) element)
+
+let iter_lval : lval generator =
+ annotate_from_options (iter_alarms Cil.visitCilLval)
+
+let iter_exp : exp generator =
+ annotate_from_options (iter_alarms Cil.visitCilExpr)
+
+let iter_instr : instr generator =
+ annotate_from_options (iter_alarms Cil.visitCilInstr)
+
+let iter_stmt : stmt generator =
+ annotate_from_options (iter_alarms Cil.visitCilStmt)
+
(** {2 List of all RTEs on a given Cil object} *)
let get_annotations from kf stmt x =
diff --git a/src/plugins/rte/visit.mli b/src/plugins/rte/visit.mli
index 1413e3b8f7b..4dc723cc58c 100644
--- a/src/plugins/rte/visit.mli
+++ b/src/plugins/rte/visit.mli
@@ -22,6 +22,47 @@
open Cil_types
+(** Low-level iterator
+
+ [generator ~options:... on_alarm kf stmt element] iterates over
+ potential alarms for Cil element, located in the given
+ kernel_function and stmt.
+
+ The [on_alarm ki ?status alarm] callback is invoked with
+ the k-instruction originating the alarm and the already known status,
+ if any.
+
+ Potential alarms can be specified by the provided options,
+ with defaults generated from the Kernel options and the RTE plug-in
+ options.
+*)
+type 'a generator =
+ ?remove_trivial:bool ->
+ ?initialized:Options.DoInitialized.t ->
+ ?mem_access:Options.DoMemAccess.t ->
+ ?div_mod:Options.DoDivMod.t ->
+ ?shift:Options.DoShift.t ->
+ ?left_shift_negative:Kernel.LeftShiftNegative.t ->
+ ?right_shift_negative:Kernel.RightShiftNegative.t ->
+ ?signed_overflow:Kernel.SignedOverflow.t ->
+ ?unsigned_overflow:Kernel.UnsignedOverflow.t ->
+ ?signed_downcast:Kernel.SignedDowncast.t ->
+ ?unsigned_downcast:Kernel.UnsignedDowncast.t ->
+ ?float_to_int:Options.DoFloatToInt.t ->
+ ?finite_float:bool ->
+ ?pointer_call:Options.DoPointerCall.t ->
+ ?bool_value:Kernel.InvalidBool.t ->
+ (Cil_types.kinstr ->
+ ?status:Property_status.emitted_status -> Alarms.alarm -> unit) ->
+ Kernel_function.t ->
+ Cil_types.stmt ->
+ 'a -> unit
+
+val iter_lval : lval generator
+val iter_exp : exp generator
+val iter_instr : instr generator
+val iter_stmt : stmt generator
+
(** Generates RTE for a single function. Uses the status of the various
RTE options do decide which kinds of annotations must be generated.
*)
--
GitLab