diff --git a/.Makefile.lint b/.Makefile.lint
index 73569bc4b3548ff386b916f43a5bf20c4e81048c..cdddb760969cc6f1075006562db65d2c0cc5af02 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -360,11 +360,6 @@ ML_LINT_KO+=src/plugins/postdominators/compute.ml
ML_LINT_KO+=src/plugins/postdominators/postdominators_parameters.ml
ML_LINT_KO+=src/plugins/postdominators/print.ml
ML_LINT_KO+=src/plugins/print_api/print_interface.ml
-ML_LINT_KO+=src/plugins/rte/generator.ml
-ML_LINT_KO+=src/plugins/rte/options.ml
-ML_LINT_KO+=src/plugins/rte/register.ml
-ML_LINT_KO+=src/plugins/rte/rte.ml
-ML_LINT_KO+=src/plugins/rte/visit.ml
ML_LINT_KO+=src/plugins/scope/Scope.mli
ML_LINT_KO+=src/plugins/scope/datascope.ml
ML_LINT_KO+=src/plugins/scope/defs.ml
diff --git a/Makefile b/Makefile
index 1668a9d2777578fe6d3149774945eaedd101e369..be71d63e14ec90e788cbbf3991707faf9aa956a4 100644
--- a/Makefile
+++ b/Makefile
@@ -957,7 +957,7 @@ $(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
PLUGIN_ENABLE:=$(ENABLE_RTEGEN)
PLUGIN_NAME:=RteGen
PLUGIN_DIR:=src/plugins/rte
-PLUGIN_CMO:= options generator rte visit register
+PLUGIN_CMO:= options generator rte flags visit register
PLUGIN_DISTRIBUTED:=yes
PLUGIN_INTERNAL_TEST:=yes
PLUGIN_TESTS_DIRS:=rte rte_manual
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index dd34d6c7e782c8eb929528844e2b9d94027eb2d7..37041b02d29df294ff1fa3b9326be5b9dd58aaec 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1002,6 +1002,8 @@ src/plugins/report/report_parameters.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/report/scan.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/report/scan.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/rte/RteGen.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/rte/flags.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/rte/flags.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/rte/generator.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/rte/generator.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/rte/options.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/rte/RteGen.mli b/src/plugins/rte/RteGen.mli
index 9926f78e4a0920cb8cc90aa4c4082d8b86e8dad7..aff86d1508f7becc88365eef085f20c05274599c 100644
--- a/src/plugins/rte/RteGen.mli
+++ b/src/plugins/rte/RteGen.mli
@@ -20,4 +20,40 @@
(* *)
(**************************************************************************)
-(** No function is directly exported: they are registered in {!Db.Value}. *)
+(** Consult internal plug-in documentation for more details *)
+
+(** Flags for filtering Alarms *)
+module Flags : module type of Flags
+
+(** RTE Generator Status & Emitters *)
+module Generator : module type of Generator
+
+(** Visitors to iterate over Alarms and/or generate Code-Annotations *)
+module Visit : sig
+ open Cil_types
+
+ 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
+ val iter_lval : lval iterator
+ val iter_exp : exp iterator
+ val iter_instr : instr iterator
+ val iter_stmt : stmt iterator
+ val register :
+ Emitter.t -> kernel_function -> stmt -> invalid:bool -> Alarms.alarm ->
+ code_annotation * bool
+end
diff --git a/src/plugins/rte/flags.ml b/src/plugins/rte/flags.ml
new file mode 100644
index 0000000000000000000000000000000000000000..eed7aa13716ac2e69ce7b4999c1402f04ef5ece8
--- /dev/null
+++ b/src/plugins/rte/flags.ml
@@ -0,0 +1,121 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Fine Tuning Visitors --- *)
+(* -------------------------------------------------------------------------- *)
+
+type t = {
+ remove_trivial: bool;
+ initialized: bool;
+ mem_access: bool;
+ div_mod: bool;
+ shift: bool;
+ left_shift_negative: bool;
+ right_shift_negative: bool;
+ signed_overflow: bool;
+ unsigned_overflow: bool;
+ signed_downcast: bool;
+ unsigned_downcast: bool;
+ float_to_int: bool;
+ finite_float: bool;
+ pointer_call: bool;
+ bool_value: bool;
+}
+
+let all = {
+ remove_trivial = true;
+ initialized = true;
+ mem_access = true;
+ div_mod = true;
+ shift = true;
+ left_shift_negative = true;
+ right_shift_negative = true;
+ signed_overflow = true;
+ unsigned_overflow = true;
+ signed_downcast = true;
+ unsigned_downcast = true;
+ float_to_int = true;
+ finite_float = true;
+ pointer_call = true;
+ bool_value = true;
+}
+
+let none = {
+ remove_trivial = false;
+ initialized = false;
+ mem_access = false;
+ div_mod = false;
+ shift = false;
+ left_shift_negative = false;
+ right_shift_negative = false;
+ signed_overflow = false;
+ unsigned_overflow = false;
+ signed_downcast = false;
+ unsigned_downcast = false;
+ float_to_int = false;
+ finite_float = false;
+ pointer_call = false;
+ bool_value = false;
+}
+
+(* Which annotations should be added,
+ from local options, or deduced from the options of RTE and the kernel *)
+
+let option (get : unit -> bool) = function None -> get () | Some flag -> flag
+
+let default
+ ?remove_trivial
+ ?initialized
+ ?mem_access
+ ?div_mod
+ ?shift
+ ?left_shift_negative
+ ?right_shift_negative
+ ?signed_overflow
+ ?unsigned_overflow
+ ?signed_downcast
+ ?unsigned_downcast
+ ?float_to_int
+ ?finite_float
+ ?pointer_call
+ ?bool_value
+ () =
+ {
+ remove_trivial = option (fun () -> not (Options.Trivial.get ())) remove_trivial ;
+ initialized = option Options.DoInitialized.get initialized ;
+ mem_access = option Options.DoMemAccess.get mem_access ;
+ div_mod = option Options.DoDivMod.get div_mod ;
+ shift = option Options.DoShift.get shift;
+ left_shift_negative = option Kernel.LeftShiftNegative.get left_shift_negative ;
+ right_shift_negative = option Kernel.RightShiftNegative.get right_shift_negative ;
+ signed_overflow = option Kernel.SignedOverflow.get signed_overflow ;
+ unsigned_overflow = option Kernel.UnsignedOverflow.get unsigned_overflow ;
+ signed_downcast = option Kernel.SignedDowncast.get signed_downcast ;
+ unsigned_downcast = option Kernel.UnsignedDowncast.get unsigned_downcast ;
+ float_to_int = option Options.DoFloatToInt.get float_to_int ;
+ finite_float = option (fun () -> Kernel.SpecialFloat.get () <> "none") finite_float ;
+ pointer_call = option Options.DoPointerCall.get pointer_call ;
+ bool_value = option Kernel.InvalidBool.get bool_value ;
+ }
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/rte/flags.mli b/src/plugins/rte/flags.mli
new file mode 100644
index 0000000000000000000000000000000000000000..578ba9ef3088b857eb9fed011be515f5096f90d4
--- /dev/null
+++ b/src/plugins/rte/flags.mli
@@ -0,0 +1,72 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(** Filtering Categories of Alarms *)
+(* -------------------------------------------------------------------------- *)
+
+(** Flags for controling the low-level API. Each flag control whether
+ a category of alarms will be visited or not. *)
+type t = {
+ remove_trivial: bool;
+ initialized: bool;
+ mem_access: bool;
+ div_mod: bool;
+ shift: bool;
+ left_shift_negative: bool;
+ right_shift_negative: bool;
+ signed_overflow: bool;
+ unsigned_overflow: bool;
+ signed_downcast: bool;
+ unsigned_downcast: bool;
+ float_to_int: bool;
+ finite_float: bool;
+ pointer_call: bool;
+ bool_value: bool;
+}
+
+(** Defaults flags are taken from the Kernel and RTE plug-in options. *)
+val default :
+ ?remove_trivial:bool ->
+ ?initialized:bool ->
+ ?mem_access:bool ->
+ ?div_mod:bool ->
+ ?shift:bool ->
+ ?left_shift_negative:bool ->
+ ?right_shift_negative:bool ->
+ ?signed_overflow:bool ->
+ ?unsigned_overflow:bool ->
+ ?signed_downcast:bool ->
+ ?unsigned_downcast:bool ->
+ ?float_to_int:bool ->
+ ?finite_float:bool ->
+ ?pointer_call:bool ->
+ ?bool_value:bool ->
+ unit -> t
+
+(** All flags set to [true]. *)
+val all : t
+
+(** All flags set to [false]. *)
+val none : t
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/rte/generator.ml b/src/plugins/rte/generator.ml
index b6c626b68c4f91251fcdb19397896dc6fec6c40d..2a944b6c6cd35202120b084850912182623afb20 100644
--- a/src/plugins/rte/generator.ml
+++ b/src/plugins/rte/generator.ml
@@ -32,26 +32,26 @@ let states : State.t list ref = ref []
let accessors : Db.RteGen.status_accessor list ref = ref []
module Make
- (M:sig
- val name:string
- val parameter: Typed_parameter.t
- val additional_parameters: Typed_parameter.t list
- end)
- =
+ (M:sig
+ val name:string
+ val parameter: Typed_parameter.t
+ val additional_parameters: Typed_parameter.t list
+ end)
+=
struct
- module H =
+ module H =
Kernel_function.Make_Table
(Datatype.Bool)
(struct
- let name = "RTE.Computed." ^ M.name
- let size = 17
- let dependencies =
+ let name = "RTE.Computed." ^ M.name
+ let size = 17
+ let dependencies =
let extract p = State.get p.Typed_parameter.name in
- Ast.self
- :: Options.Trivial.self
- :: List.map extract (M.parameter :: M.additional_parameters)
- end)
+ Ast.self
+ :: Options.Trivial.self
+ :: List.map extract (M.parameter :: M.additional_parameters)
+ end)
let is_computed =
(* Nothing to do for functions without body. *)
@@ -70,42 +70,42 @@ end
module Initialized =
Make
(struct
- let name = "initialized"
- let parameter = Options.DoInitialized.parameter
- let additional_parameters = [ ]
- end)
+ let name = "initialized"
+ let parameter = Options.DoInitialized.parameter
+ let additional_parameters = [ ]
+ end)
module Mem_access =
Make
(struct
- let name = "mem_access"
- let parameter = Options.DoMemAccess.parameter
- let additional_parameters = [ Kernel.SafeArrays.parameter ]
- end)
+ let name = "mem_access"
+ let parameter = Options.DoMemAccess.parameter
+ let additional_parameters = [ Kernel.SafeArrays.parameter ]
+ end)
module Pointer_call =
Make
(struct
- let name = "pointer_call"
- let parameter = Options.DoPointerCall.parameter
- let additional_parameters = []
- end)
+ let name = "pointer_call"
+ let parameter = Options.DoPointerCall.parameter
+ let additional_parameters = []
+ end)
module Div_mod =
Make
(struct
- let name = "division_by_zero"
- let parameter = Options.DoDivMod.parameter
- let additional_parameters = []
- end)
+ let name = "division_by_zero"
+ let parameter = Options.DoDivMod.parameter
+ let additional_parameters = []
+ end)
module Shift =
Make
(struct
- let name = "shift_value_out_of_bounds"
- let parameter = Options.DoShift.parameter
- let additional_parameters = []
- end)
+ let name = "shift_value_out_of_bounds"
+ let parameter = Options.DoShift.parameter
+ let additional_parameters = []
+ end)
module Left_shift_negative =
Make
@@ -126,51 +126,51 @@ module Right_shift_negative =
module Signed_overflow =
Make
(struct
- let name = "signed_overflow"
- let parameter = Kernel.SignedOverflow.parameter
- let additional_parameters = []
- end)
+ let name = "signed_overflow"
+ let parameter = Kernel.SignedOverflow.parameter
+ let additional_parameters = []
+ end)
module Signed_downcast =
Make
(struct
- let name = "downcast"
- let parameter = Kernel.SignedDowncast.parameter
- let additional_parameters = []
- end)
+ let name = "downcast"
+ let parameter = Kernel.SignedDowncast.parameter
+ let additional_parameters = []
+ end)
module Unsigned_overflow =
Make
(struct
- let name = "unsigned_overflow"
- let parameter = Kernel.UnsignedOverflow.parameter
- let additional_parameters = []
- end)
+ let name = "unsigned_overflow"
+ let parameter = Kernel.UnsignedOverflow.parameter
+ let additional_parameters = []
+ end)
module Unsigned_downcast =
Make
(struct
- let name = "unsigned_downcast"
- let parameter = Kernel.UnsignedDowncast.parameter
- let additional_parameters = []
- end)
+ let name = "unsigned_downcast"
+ let parameter = Kernel.UnsignedDowncast.parameter
+ let additional_parameters = []
+ end)
module Float_to_int =
Make
(struct
- let name = "float_to_int"
- let parameter = Options.DoFloatToInt.parameter
- let additional_parameters = []
- end)
+ let name = "float_to_int"
+ let parameter = Options.DoFloatToInt.parameter
+ let additional_parameters = []
+ end)
module Finite_float =
Make
(struct
- let name = "finite_float"
- let parameter = Kernel.SpecialFloat.parameter
- let additional_parameters = []
- end)
+ let name = "finite_float"
+ let parameter = Kernel.SpecialFloat.parameter
+ let additional_parameters = []
+ end)
module Bool_value =
Make
@@ -191,11 +191,17 @@ let () = Db.RteGen.self := self
let all_statuses = !accessors
let emitter =
- Emitter.create
- "rte"
- [ Emitter.Property_status; Emitter.Alarm ]
- ~correctness:[ Kernel.SafeArrays.parameter ]
- ~tuning:[]
+ Emitter.create
+ "rte"
+ [ Emitter.Property_status; Emitter.Alarm ]
+ ~correctness:[ Kernel.SafeArrays.parameter ]
+ ~tuning:[]
+
+let get_registered_annotations stmt =
+ Annotations.fold_code_annot
+ (fun e a acc -> if Emitter.equal e emitter then a ::acc else acc)
+ stmt
+ []
(*
Local Variables:
diff --git a/src/plugins/rte/generator.mli b/src/plugins/rte/generator.mli
index 2ed6fe38a32711de556d8e0466b224b5050a7655..ae903fb0bc863326a6931efe17bf75d1c75fb9d0 100644
--- a/src/plugins/rte/generator.mli
+++ b/src/plugins/rte/generator.mli
@@ -26,6 +26,8 @@ module type S = sig
val accessor: Db.RteGen.status_accessor
end
+(* No module for Trivial: dependency added for generators below *)
+
module Initialized: S
module Mem_access: S
module Pointer_call: S
@@ -41,9 +43,15 @@ module Float_to_int: S
module Finite_float: S
module Bool_value: S
+val all_statuses: Db.RteGen.status_accessor list
+
+(** The Emitter for Annotations registered by RTE *)
val emitter: Emitter.t
-val all_statuses: Db.RteGen.status_accessor list
+open Cil_types
+
+(** Returns all annotations actually {i registered} by RTE so far *)
+val get_registered_annotations: stmt -> code_annotation list
(*
Local Variables:
diff --git a/src/plugins/rte/options.ml b/src/plugins/rte/options.ml
index 7c646c80c6e977aaf0ae01337b4425641a45e1c1..0b629f7f9941d8f09e6494f4e3c8ca20611539c1 100644
--- a/src/plugins/rte/options.ml
+++ b/src/plugins/rte/options.ml
@@ -21,47 +21,47 @@
(**************************************************************************)
let help_msg = "generates annotations for runtime error checking and \
-preconditions at call sites"
+ preconditions at call sites"
include Plugin.Register
- (struct
- let name = "rtegen"
- let shortname = "rte"
- let help = help_msg
- end)
+ (struct
+ let name = "rtegen"
+ let shortname = "rte"
+ let help = help_msg
+ end)
(* enabling/disabling plugin *)
module Enabled =
False
(struct
- let option_name = "-rte"
- let help = "when on (off by default), " ^ help_msg
- end)
+ let option_name = "-rte"
+ let help = "when on (off by default), " ^ help_msg
+ end)
(* annotates division by zero (undefined behavior) *)
module DoDivMod =
True
(struct
- let option_name = "-rte-div"
- let help = "when on (default), annotate for modulo and division by zero"
- end)
+ let option_name = "-rte-div"
+ let help = "when on (default), annotate for modulo and division by zero"
+ end)
(* annotates left and right shifts (undefined behavior) *)
module DoShift =
True
(struct
- let option_name = "-rte-shift"
- let help = "when on (default), annotate for left and right shifts by a value out of bounds"
- end)
+ let option_name = "-rte-shift"
+ let help = "when on (default), annotate for left and right shifts by a value out of bounds"
+ end)
(* annotates casts from floating-point to integer (undefined behavior) *)
module DoFloatToInt =
True
(struct
- let option_name = "-rte-float-to-int"
- let help = "when on (default), annotate casts from floating-point to \
- integer"
- end)
+ let option_name = "-rte-float-to-int"
+ let help = "when on (default), annotate casts from floating-point to \
+ integer"
+ end)
(* annotates local variables and pointers read (aside from globals) initialization *)
module DoInitialized =
@@ -76,52 +76,52 @@ module DoInitialized =
module DoMemAccess =
True
(struct
- let option_name = "-rte-mem"
- let help = "when on (default), annotate for valid pointer or \
-array access"
- end)
+ let option_name = "-rte-mem"
+ let help = "when on (default), annotate for valid pointer or \
+ array access"
+ end)
(* annotates calls through pointers *)
module DoPointerCall =
True
(struct
- let option_name = "-rte-pointer-call"
- let help = "when on, annotate functions calls through pointers"
- end)
+ let option_name = "-rte-pointer-call"
+ let help = "when on, annotate functions calls through pointers"
+ end)
(* uses results of basic constant propagation in order to check
validity / invalidity of generated assertions, emitting a status if possible
- *)
+*)
module Trivial =
False
(struct
- let option_name = "-rte-trivial-annotations"
- let help = "generate annotations for constant expressions, even when \
-they trivially hold"
- (* if on, evaluates constants in order to check if assertions
- are trivially true / false *)
- end)
+ let option_name = "-rte-trivial-annotations"
+ let help = "generate annotations for constant expressions, even when \
+ they trivially hold"
+ (* if on, evaluates constants in order to check if assertions
+ are trivially true / false *)
+ end)
-(* emits a warning when an assertion generated by rte is clearly invalid
+(* emits a warning when an assertion generated by rte is clearly invalid
(using constant folding, see ConstFold *)
module Warn =
True
(struct
- let option_name = "-rte-warn"
- let help = "when on (default), emits warning on broken asserts"
- end)
+ let option_name = "-rte-warn"
+ let help = "when on (default), emits warning on broken asserts"
+ end)
(* this option allows the user to select a set of functions on which
- the plug-in performs its jobs (and only those).
+ the plug-in performs its jobs (and only those).
By default all functions are annotated *)
module FunctionSelection =
Kernel_function_set
(struct
- let option_name = "-rte-select"
- let arg_name = "fun"
- let help = "select <fun> for analysis (default all functions)"
- end)
-
+ let option_name = "-rte-select"
+ let arg_name = "fun"
+ let help = "select <fun> for analysis (default all functions)"
+ end)
+
let warn ?source fmt = warning ?source ~current:true ~once:true fmt
(*
diff --git a/src/plugins/rte/register.ml b/src/plugins/rte/register.ml
index 5a7a9ba4af947ea862faa59e349c55e4b3cb1805..ab0d3111c0a0da3d7e9c6b7e1777e17659c14c57 100644
--- a/src/plugins/rte/register.ml
+++ b/src/plugins/rte/register.ml
@@ -20,7 +20,46 @@
(* *)
(**************************************************************************)
-let journal_register ?comment is_dyn name ty_arg fctref fct =
+(* -------------------------------------------------------------------------- *)
+(* dedicated computations *)
+(* -------------------------------------------------------------------------- *)
+
+(* annotate for all rte + unsigned overflows (which are not rte), for a given
+ function *)
+let do_all_rte kf =
+ let flags =
+ { Flags.all with
+ Flags.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
+ Flags.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;
if is_dyn then
@@ -29,22 +68,21 @@ let journal_register ?comment is_dyn name ty_arg fctref fct =
in
()
-let nojournal_register fctref fct =
+let nojournal_register fctref fct =
Db.register Db.Journalization_not_required fctref (fun () -> fct)
-let () =
+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;
+ given function."
+ "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;
+ in the given function."
+ "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;
@@ -76,36 +114,36 @@ let _ =
let _ =
Dynamic.register
~comment:"Get the list of annotations previously emitted by RTE for the \
-given statement."
+ given statement."
~plugin:"RteGen"
"get_rte_annotations"
(Datatype.func
Cil_datatype.Stmt.ty
(let module L = Datatype.List(Cil_datatype.Code_annotation) in L.ty))
~journalize:true
- Visit.rte_annotations
+ Generator.get_registered_annotations
let _ =
Dynamic.register
~comment:"Generate RTE annotations corresponding to the given stmt of \
-the given function."
+ the given function."
~plugin:"RteGen"
"stmt_annotations"
(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
~comment:"Generate RTE annotations corresponding to the given exp \
-of the given stmt in the given function."
+ of the given stmt in the given function."
~plugin:"RteGen"
"exp_annotations"
- (Datatype.func3 Kernel_function.ty Cil_datatype.Stmt.ty Cil_datatype.Exp.ty
+ (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/rte.ml b/src/plugins/rte/rte.ml
index 855e2b4e729349a97a695626041ebe7d19df816c..b1f2b7ffaec2b3a980a1816314f0756e902e471e 100644
--- a/src/plugins/rte/rte.ml
+++ b/src/plugins/rte/rte.ml
@@ -24,9 +24,7 @@ open Cil_types
type 'a alarm_gen =
remove_trivial:bool ->
- on_alarm:(?status:Property_status.emitted_status ->
- Alarms.alarm ->
- unit) ->
+ on_alarm:(invalid:bool -> Alarms.alarm -> unit) ->
'a -> unit
type bound_kind = Alarms.bound_kind = Lower_bound | Upper_bound
@@ -45,7 +43,7 @@ let valid_index ~remove_trivial ~on_alarm e size =
in
(* Do not create upper-bound check on GNU zero-length arrays *)
if not (bk == Upper_bound && Cil.isZero size) then begin
- on_alarm ?status:None (Alarms.Index_out_of_bound(e, b))
+ on_alarm ~invalid:false (Alarms.Index_out_of_bound(e, b))
end
in
if remove_trivial then begin
@@ -54,7 +52,7 @@ let valid_index ~remove_trivial ~on_alarm e size =
let v_e = get_expr_val e in
let v_size = get_expr_val size in
let neg_ok =
- Extlib.may_map ~dft:false (Integer.le Integer.zero) v_e
+ Extlib.may_map ~dft:false (Integer.le Integer.zero) v_e
|| Cil.isUnsignedInteger (Cil.typeOf e)
in
if not neg_ok then alarm Lower_bound;
@@ -76,11 +74,11 @@ let valid_index ~remove_trivial ~on_alarm e size =
let lval_assertion ~read_only ~remove_trivial ~on_alarm lv =
(* For accesses to known arrays we generate an assertions that constrains
the index. This is simpler than the [\valid] assertion *)
- let rec check_array_access default off typ in_struct =
+ let rec check_array_access default off typ in_struct =
match off with
- | NoOffset ->
- if default then
- on_alarm ?status:None (Alarms.Memory_access(lv, read_only))
+ | NoOffset ->
+ if default then
+ on_alarm ~invalid:false (Alarms.Memory_access(lv, read_only))
| Field (fi, off) ->
(* Mark that we went through a struct field, then recurse *)
check_array_access default off fi.ftype true
@@ -108,10 +106,10 @@ let lval_assertion ~read_only ~remove_trivial ~on_alarm lv =
(* assertion for lvalue initialization *)
let lval_initialized_assertion ~remove_trivial:_ ~on_alarm lv =
- let rec check_array_initialized default off typ in_struct l =
+ let rec check_array_initialized default off typ in_struct l =
match off with
- | NoOffset ->
- begin
+ | NoOffset ->
+ begin
match typ with
| TComp({cstruct = false; cfields} ,_,_) ->
(match cfields with
@@ -123,11 +121,11 @@ let lval_initialized_assertion ~remove_trivial:_ ~on_alarm lv =
(fun fi -> Cil.addOffsetLval (Field (fi, NoOffset)) lv)
cfields
in
- if default then
- on_alarm ?status:None (Alarms.Uninitialized_union llv))
- | _ ->
- if default then
- on_alarm ?status:None (Alarms.Uninitialized lv)
+ if default then
+ on_alarm ~invalid:false (Alarms.Uninitialized_union llv))
+ | _ ->
+ if default then
+ on_alarm ~invalid:false (Alarms.Uninitialized lv)
end
| Field (fi, off) ->
(* Mark that we went through a struct field, then recurse *)
@@ -158,17 +156,17 @@ let uminus_assertion ~remove_trivial ~on_alarm exp =
let min_ty = Cil.min_signed_number size in
(* alarm is bound <= exp, hence bound must be MIN_INT+1 *)
let bound = Integer.add Integer.one min_ty in
- let alarm ?status () =
+ let alarm ?(invalid=false) () =
let a = Alarms.Overflow(Alarms.Signed, exp, bound, Lower_bound) in
- on_alarm ?status a
+ on_alarm ~invalid a
in
if remove_trivial then begin
match get_expr_val exp with
| None -> alarm ()
- | Some a64 ->
+ | Some a64 ->
(* constant operand *)
if Integer.equal a64 min_ty then
- alarm ~status:Property_status.False_if_reachable ()
+ alarm ~invalid:true ()
end
else alarm ()
@@ -179,17 +177,17 @@ let mult_sub_add_assertion ~signed ~remove_trivial ~on_alarm (exp,op,lexp,rexp)
is strictly more than [max_ty] or strictly less than [min_ty] *)
let t = Cil.unrollType (Cil.typeOf exp) in
let size = Cil.bitsSizeOf t in
- let min_ty, max_ty =
+ let min_ty, max_ty =
if signed then Cil.min_signed_number size, Cil.max_signed_number size
- else Integer.zero, Cil.max_unsigned_number size
+ else Integer.zero, Cil.max_unsigned_number size
in
- let alarm ?status bk =
+ let alarm ?(invalid=false) bk =
let bound = match bk with
| Upper_bound -> max_ty
| Lower_bound -> min_ty
in
let signed = if signed then Alarms.Signed else Alarms.Unsigned in
- on_alarm ?status (Alarms.Overflow (signed, exp, bound, bk));
+ on_alarm ~invalid (Alarms.Overflow (signed, exp, bound, bk));
in
let alarms () =
alarm Lower_bound;
@@ -199,7 +197,7 @@ let mult_sub_add_assertion ~signed ~remove_trivial ~on_alarm (exp,op,lexp,rexp)
match get_expr_val lexp, get_expr_val rexp, op with
| Some l, Some r, _ -> (* both operands are constant *)
let warn r =
- let warn bk = alarm ~status:Property_status.False_if_reachable bk in
+ let warn bk = alarm ~invalid:true bk in
if Integer.gt r max_ty then warn Upper_bound
else if Integer.lt r min_ty then warn Lower_bound
in
@@ -228,7 +226,7 @@ let mult_sub_add_assertion ~signed ~remove_trivial ~on_alarm (exp,op,lexp,rexp)
(* Only negative overflows are possible, since r is positive. (TODO:
nothing can happen on [max_int]. *)
alarm Lower_bound
- end
+ end
| Some v, None, Mult | None, Some v, Mult
when Integer.is_zero v || Integer.is_one v -> ()
@@ -240,8 +238,8 @@ let mult_sub_add_assertion ~signed ~remove_trivial ~on_alarm (exp,op,lexp,rexp)
(* assertions for division and modulo (divisor is 0) *)
let divmod_assertion ~remove_trivial ~on_alarm divisor =
(* division or modulo: overflow occurs when divisor is equal to zero *)
- let alarm ?status () =
- on_alarm ?status (Alarms.Division_by_zero divisor);
+ let alarm ?(invalid=false) () =
+ on_alarm ~invalid (Alarms.Division_by_zero divisor);
in
if remove_trivial then begin
match get_expr_val divisor with
@@ -250,7 +248,7 @@ let divmod_assertion ~remove_trivial ~on_alarm divisor =
| Some v64 ->
if Integer.equal v64 Integer.zero then
(* divide by 0 *)
- alarm ~status:Property_status.False_if_reachable ()
+ alarm ~invalid:true ()
(* else divide by constant which is not 0: nothing to assert *)
end
else alarm ()
@@ -270,9 +268,9 @@ let signed_div_assertion ~remove_trivial ~on_alarm (exp, lexp, rexp) =
(* check dividend_expr / divisor_expr : if constants ... *)
(* compute smallest representable "size bits" (signed) integer *)
let max_ty = Cil.max_signed_number size in
- let alarm ?status () =
+ let alarm ?(invalid=false) () =
let a = Alarms.Overflow(Alarms.Signed, exp, max_ty, Alarms.Upper_bound) in
- on_alarm ?status a;
+ on_alarm ~invalid a;
in
if remove_trivial then begin
let min = Cil.min_signed_number size in
@@ -285,8 +283,8 @@ let signed_div_assertion ~remove_trivial ~on_alarm (exp, lexp, rexp) =
()
| Some _, Some _ ->
(* invalid constant division *)
- alarm ~status:Property_status.False_if_reachable ()
- | None, Some _ | Some _, None | None, None ->
+ alarm ~invalid:true ()
+ | None, Some _ | Some _, None | None, None ->
(* at least one is not constant: cannot conclude *)
alarm ()
end
@@ -294,9 +292,9 @@ let signed_div_assertion ~remove_trivial ~on_alarm (exp, lexp, rexp) =
(* Assertions for the left and right operands of left and right shift. *)
let shift_assertion ~remove_trivial ~on_alarm (exp, upper_bound) =
- let alarm ?status () =
+ let alarm ?(invalid=false) () =
let a = Alarms.Invalid_shift(exp, upper_bound) in
- on_alarm ?status a;
+ on_alarm ~invalid a ;
in
if remove_trivial then begin
match get_expr_val exp with
@@ -310,7 +308,7 @@ let shift_assertion ~remove_trivial ~on_alarm (exp, upper_bound) =
| Some u -> Integer.lt c64 (Integer.of_int u)
in
if not (Integer.ge c64 Integer.zero && upper_bound_ok) then
- alarm ~status:Property_status.False_if_reachable ()
+ alarm ~invalid:true ()
end
else alarm ()
@@ -340,22 +338,22 @@ let shift_overflow_assertion ~signed ~remove_trivial ~on_alarm (exp, op, lexp, r
then Cil.max_signed_number size
else Cil.max_unsigned_number size
in
- let overflow_alarm ?status () =
+ let overflow_alarm ?(invalid=false) () =
let signed = if signed then Alarms.Signed else Alarms.Unsigned in
let a = Alarms.Overflow (signed, exp, maxValResult, Alarms.Upper_bound) in
- on_alarm ?status a;
+ on_alarm ~invalid a;
in
if remove_trivial then begin
match get_expr_val lexp, get_expr_val rexp with
- | None,_ | _, None ->
+ | None,_ | _, None ->
overflow_alarm ()
| Some lval64, Some rval64 ->
(* both operands are constant: check result is representable in
result type *)
- if Integer.ge rval64 Integer.zero
+ if Integer.ge rval64 Integer.zero
&& Integer.gt (Integer.shift_left lval64 rval64) maxValResult
then
- overflow_alarm ~status:Property_status.False_if_reachable ()
+ overflow_alarm ~invalid:true ()
end
else overflow_alarm ()
@@ -375,16 +373,16 @@ let unsigned_downcast_assertion ~remove_trivial ~on_alarm (ty, exp) =
ok is same bit size ;
if target is <, requires <= max target *)
let max_ty = Cil.max_unsigned_number szTo in
- let alarm ?status bk =
+ let alarm ?(invalid=false) bk =
let b = match bk with
| Lower_bound -> Integer.zero
| Upper_bound -> max_ty
in
let a = Alarms.Overflow (Alarms.Unsigned_downcast, exp, b, bk) in
- on_alarm ?status a;
+ on_alarm ~invalid a;
in
let alarms () =
- if Cil.isSigned kind then begin (* signed to unsigned *)
+ if Cil.isSigned kind then begin (* signed to unsigned *)
alarm Upper_bound;
alarm Lower_bound;
end else (* unsigned to unsigned; cannot overflow in the negative *)
@@ -395,11 +393,9 @@ let unsigned_downcast_assertion ~remove_trivial ~on_alarm (ty, exp) =
| None -> alarms ()
| Some a64 ->
if Integer.lt a64 Integer.zero then
- alarm ~status:Property_status.False_if_reachable
- Lower_bound
+ alarm ~invalid:true Lower_bound
else if Integer.gt a64 max_ty then
- alarm ~status:Property_status.False_if_reachable
- Upper_bound
+ alarm ~invalid:true Upper_bound
end
else alarms ())
| _ -> ()
@@ -416,13 +412,13 @@ let signed_downcast_assertion ~remove_trivial ~on_alarm (ty, exp) =
(* downcast: the expression result should fit on szTo bits *)
let min_ty = Cil.min_signed_number szTo in
let max_ty = Cil.max_signed_number szTo in
- let alarm ?status bk =
+ let alarm ?(invalid=false) bk =
let b = match bk with
| Lower_bound -> min_ty
| Upper_bound -> max_ty
in
let a = Alarms.Overflow (Alarms.Signed_downcast, exp, b, bk) in
- on_alarm ?status a;
+ on_alarm ~invalid a;
in
let alarms () =
if Cil.isSigned kind then begin
@@ -437,9 +433,9 @@ let signed_downcast_assertion ~remove_trivial ~on_alarm (ty, exp) =
| None -> alarms ()
| Some a64 ->
(if Integer.lt a64 min_ty then
- alarm ~status:Property_status.False_if_reachable Lower_bound
+ alarm ~invalid:true Lower_bound
else if Integer.gt a64 max_ty then
- alarm ~status:Property_status.False_if_reachable Upper_bound)
+ alarm ~invalid:true Upper_bound)
end
else alarms ())
| _ -> ()
@@ -456,12 +452,12 @@ let float_to_int_assertion ~remove_trivial ~on_alarm (ty, exp) =
else
Integer.zero, Cil.max_unsigned_number szTo
in
- let alarm ?status bk =
+ let alarm ?(invalid=false) bk =
let b = match bk with
| Lower_bound -> min_ty
| Upper_bound -> max_ty
in
- on_alarm ?status (Alarms.Float_to_int (exp, b, bk))
+ on_alarm ~invalid (Alarms.Float_to_int (exp, b, bk))
in
let f = match exp.enode with
| Const (CReal (f, _, _)) -> Some f
@@ -474,9 +470,9 @@ let float_to_int_assertion ~remove_trivial ~on_alarm (ty, exp) =
try
let fint = Floating_point.truncate_to_integer f in
if Integer.lt fint min_ty then
- alarm ~status:Property_status.False_if_reachable Lower_bound
+ alarm ~invalid:true Lower_bound
else if Integer.gt fint max_ty then
- alarm ~status:Property_status.False_if_reachable Upper_bound
+ alarm ~invalid:true Upper_bound
with Floating_point.Float_Non_representable_as_Int64 sign ->
match sign with
| Floating_point.Neg -> alarm Lower_bound
@@ -490,19 +486,19 @@ let float_to_int_assertion ~remove_trivial ~on_alarm (ty, exp) =
(* assertion for checking only finite float are used *)
let finite_float_assertion ~remove_trivial:_ ~on_alarm (fkind, exp) =
- let status = None in
+ let invalid = false in
match Kernel.SpecialFloat.get () with
| "none" -> ()
- | "nan" -> on_alarm ?status (Alarms.Is_nan (exp, fkind))
- | "non-finite" -> on_alarm ?status (Alarms.Is_nan_or_infinite (exp, fkind))
+ | "nan" -> on_alarm ~invalid (Alarms.Is_nan (exp, fkind))
+ | "non-finite" -> on_alarm ~invalid (Alarms.Is_nan_or_infinite (exp, fkind))
| _ -> assert false
(* assertion for a pointer call [( *e )(args)]. *)
let pointer_call ~remove_trivial:_ ~on_alarm (e, args) =
- on_alarm ?status:None (Alarms.Function_pointer (e, Some args))
+ on_alarm ~invalid:false (Alarms.Function_pointer (e, Some args))
let bool_value ~remove_trivial:_ ~on_alarm lv =
- on_alarm ?status:None (Alarms.Invalid_bool lv)
+ on_alarm ~invalid:false (Alarms.Invalid_bool lv)
(*
Local Variables:
diff --git a/src/plugins/rte/rte.mli b/src/plugins/rte/rte.mli
index 0b1d55a21e304b9ccec0cb61b1c270fe232f69a9..6d194a63109c9b13466d45139ea283f3a8b18ee9 100644
--- a/src/plugins/rte/rte.mli
+++ b/src/plugins/rte/rte.mli
@@ -24,9 +24,7 @@ open Cil_types
type 'a alarm_gen =
remove_trivial:bool ->
- on_alarm:(?status:Property_status.emitted_status ->
- Alarms.alarm ->
- unit) ->
+ on_alarm:(invalid:bool -> Alarms.alarm -> unit) ->
'a -> unit
(** ['a alarm_gen] is an abstraction over the process of generating a certain
kind of RTEs over something of type ['a].
diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml
index c8091e90c750efa7277e1caec1f71c0451f8906e..41f597a4fc075a37c252d2f6f2634c8d1842b0e6 100644
--- a/src/plugins/rte/visit.ml
+++ b/src/plugins/rte/visit.ml
@@ -27,88 +27,10 @@ open Cil_datatype
(* AST inplace visitor for runtime annotation generation *)
-(* module for bypassing categories of annotation generation for certain
- expression ids ;
- useful in a case such as
-
- signed char cx,cy,cz;
- cz = cx * cy;
-
- which translates to
-
- cz = (signed char) ((int) cx * (int) cz) ;
-
- which would in this case be annotated both by
-
- assert
- (((int )cx+(int )cy <= 2147483647) and
- ((int )cx+(int )cy >= (-0x7FFFFFFF-1)));
-
- and
-
- assert (((int )cx+(int )cy <= 127) and ((int )cx+(int )cy >= -128));
-
- while we only want to keep the second assert (comes from the cast,
- and is stronger)
-*)
-
-type to_annotate = {
- initialized: bool;
- mem_access: bool;
- div_mod: bool;
- shift: bool;
- left_shift_negative: bool;
- right_shift_negative: bool;
- signed_ov: bool;
- unsigned_ov: bool;
- signed_downcast: bool;
- unsigned_downcast: bool;
- float_to_int: bool;
- finite_float: bool;
- pointer_call: bool;
- bool_value: bool;
-}
-
-let annotate_all = {
- initialized = true;
- mem_access = true;
- div_mod = true;
- shift = true;
- left_shift_negative = true;
- right_shift_negative = true;
- signed_ov = true;
- unsigned_ov = true;
- signed_downcast = true;
- unsigned_downcast = true;
- float_to_int = true;
- finite_float = true;
- pointer_call = true;
- bool_value = true;
-}
-
-(** Which annotations should be added, deduced from the options of RTE and
- the kernel itself. *)
-let annotate_from_options () = {
- initialized = Options.DoInitialized.get ();
- mem_access = Options.DoMemAccess.get ();
- div_mod = Options.DoDivMod.get ();
- shift = Options.DoShift.get ();
- left_shift_negative = Kernel.LeftShiftNegative.get ();
- right_shift_negative = Kernel.RightShiftNegative.get ();
- signed_ov = Kernel.SignedOverflow.get ();
- unsigned_ov = Kernel.UnsignedOverflow.get ();
- signed_downcast = Kernel.SignedDowncast.get ();
- unsigned_downcast = Kernel.UnsignedDowncast.get ();
- float_to_int = Options.DoFloatToInt.get ();
- finite_float = Kernel.SpecialFloat.get () <> "none";
- pointer_call = Options.DoPointerCall.get ();
- bool_value = Kernel.InvalidBool.get ();
-}
-
(** [kf]: function to annotate
- [to_annot]: which RTE to generate.
+ [flags]: which RTE to generate.
[register]: the action to perform on each RTE alarm *)
-class annot_visitor kf to_annot on_alarm = object (self)
+class annot_visitor kf flags on_alarm = object (self)
inherit Visitor.frama_c_inplace
@@ -129,81 +51,84 @@ class annot_visitor kf to_annot on_alarm = object (self)
r
method private do_initialized () =
- to_annot.initialized && not (Generator.Initialized.is_computed kf)
+ flags.Flags.initialized && not (Generator.Initialized.is_computed kf)
method private do_mem_access () =
- to_annot.mem_access && not (Generator.Mem_access.is_computed kf)
+ flags.Flags.mem_access && not (Generator.Mem_access.is_computed kf)
method private do_div_mod () =
- to_annot.div_mod && not (Generator.Div_mod.is_computed kf)
+ flags.Flags.div_mod && not (Generator.Div_mod.is_computed kf)
method private do_shift () =
- to_annot.shift && not (Generator.Shift.is_computed kf)
+ flags.Flags.shift && not (Generator.Shift.is_computed kf)
method private do_left_shift_negative () =
- to_annot.left_shift_negative
+ flags.Flags.left_shift_negative
&& not (Generator.Left_shift_negative.is_computed kf)
method private do_right_shift_negative () =
- to_annot.right_shift_negative
+ flags.Flags.right_shift_negative
&& not (Generator.Right_shift_negative.is_computed kf)
method private do_signed_overflow () =
- to_annot.signed_ov && not (Generator.Signed_overflow.is_computed kf)
+ flags.Flags.signed_overflow
+ && not (Generator.Signed_overflow.is_computed kf)
method private do_unsigned_overflow () =
- to_annot.unsigned_ov && not (Generator.Unsigned_overflow.is_computed kf)
+ flags.Flags.unsigned_overflow
+ && not (Generator.Unsigned_overflow.is_computed kf)
method private do_signed_downcast () =
- to_annot.signed_downcast && not (Generator.Signed_downcast.is_computed kf)
+ flags.Flags.signed_downcast
+ && not (Generator.Signed_downcast.is_computed kf)
method private do_unsigned_downcast () =
- to_annot.unsigned_downcast &&
- not (Generator.Unsigned_downcast.is_computed kf)
+ flags.Flags.unsigned_downcast
+ && not (Generator.Unsigned_downcast.is_computed kf)
method private do_float_to_int () =
- to_annot.float_to_int && not (Generator.Float_to_int.is_computed kf)
+ flags.Flags.float_to_int && not (Generator.Float_to_int.is_computed kf)
method private do_finite_float () =
- to_annot.finite_float && not (Generator.Finite_float.is_computed kf)
+ flags.Flags.finite_float && not (Generator.Finite_float.is_computed kf)
method private do_pointer_call () =
- to_annot.pointer_call && not (Generator.Pointer_call.is_computed kf)
+ flags.Flags.pointer_call && not (Generator.Pointer_call.is_computed kf)
method private do_bool_value () =
- to_annot.bool_value && not (Generator.Bool_value.is_computed kf)
+ flags.Flags.bool_value && not (Generator.Bool_value.is_computed kf)
method private queue_stmt_spec spec =
let stmt = Extlib.the (self#current_stmt) in
Queue.add
(fun () ->
- let annot = Logic_const.new_code_annotation (AStmtSpec ([], spec)) in
- Annotations.add_code_annot Generator.emitter ~kf stmt annot)
+ let annot = Logic_const.new_code_annotation (AStmtSpec ([], spec)) in
+ Annotations.add_code_annot Generator.emitter ~kf stmt annot)
self#get_filling_actions
method private generate_assertion: 'a. 'a Rte.alarm_gen -> 'a -> unit =
- let remove_trivial = not (Options.Trivial.get ()) in
fun fgen ->
- let on_alarm ?status a = on_alarm self#current_kinstr ?status a in
- fgen ~remove_trivial ~on_alarm
+ let stmt = Extlib.the (self#current_stmt) in
+ let on_alarm ~invalid a = on_alarm stmt ~invalid a in
+ fgen ~remove_trivial:flags.Flags.remove_trivial ~on_alarm
method! vstmt s = match s.skind with
- | UnspecifiedSequence l ->
- (* UnspecifiedSequences may contain lvals for side-effects, that
- give rise to spurious assertions *)
- let no_lval = List.map (fun (s, _, _, _, sref) -> s, [], [], [], sref) l in
- let s' = { s with skind = UnspecifiedSequence no_lval } in
- Cil.ChangeDoChildrenPost (s', fun _ -> s)
- | _ -> Cil.DoChildren
+ | UnspecifiedSequence l ->
+ (* UnspecifiedSequences may contain lvals for side-effects, that
+ give rise to spurious assertions *)
+ let no_lval = List.map (fun (s, _, _, _, sref) -> s, [], [], [], sref) l in
+ let s' = { s with skind = UnspecifiedSequence no_lval } in
+ Cil.ChangeDoChildrenPost (s', fun _ -> s)
+ | _ -> Cil.DoChildren
method private treat_call ret_opt =
match ret_opt, self#do_mem_access () with
| None, _ | Some _, false -> ()
- | Some ret, true ->
+ | Some ret, true ->
Options.debug "lval %a: validity of potential mem access checked\n"
- Printer.pp_lval ret;
- self#generate_assertion
- (Rte.lval_assertion ~read_only:Alarms.For_writing) ret
+ Printer.pp_lval ret;
+ self#generate_assertion
+ (Rte.lval_assertion ~read_only:Alarms.For_writing) ret
method private check_uchar_assign dest src =
@@ -215,59 +140,59 @@ class annot_visitor kf to_annot on_alarm = object (self)
dest
end;
begin match src.enode with
- | Lval src_lv ->
- let typ1 = Cil.typeOfLval src_lv in
- let typ2 = Cil.typeOfLval dest in
- let isUChar t = Cil.isUnsignedInteger t && Cil.isAnyCharType t in
- if isUChar typ1 && isUChar typ2 then
- self#mark_to_skip_initialized src_lv
- | _ -> ()
+ | Lval src_lv ->
+ let typ1 = Cil.typeOfLval src_lv in
+ let typ2 = Cil.typeOfLval dest in
+ let isUChar t = Cil.isUnsignedInteger t && Cil.isAnyCharType t in
+ if isUChar typ1 && isUChar typ2 then
+ self#mark_to_skip_initialized src_lv
+ | _ -> ()
end ;
Cil.DoChildren
(* assigned left values are checked for valid access *)
method! vinst = function
- | Set (lval,exp,_) -> self#check_uchar_assign lval exp
- | Call (ret_opt,funcexp,argl,_) ->
- (* Do not emit alarms on Eva builtins such as Frama_C_show_each, that should
- have no effect on analyses. *)
- let is_builtin, is_va_start =
- match funcexp.enode with
- | Lval (Var vinfo, NoOffset) ->
- let kf = Globals.Functions.get vinfo in
- let frama_b = Ast_info.is_frama_c_builtin (Kernel_function.get_name kf)
- in
- let va_start = Kernel_function.get_name kf = "__builtin_va_start" in
- (frama_b, va_start)
- | _ -> (false, false)
- in
- if is_va_start then begin
- match (List.nth argl 0).enode with
+ | Set (lval,exp,_) -> self#check_uchar_assign lval exp
+ | Call (ret_opt,funcexp,argl,_) ->
+ (* Do not emit alarms on Eva builtins such as Frama_C_show_each, that should
+ have no effect on analyses. *)
+ let is_builtin, is_va_start =
+ match funcexp.enode with
+ | Lval (Var vinfo, NoOffset) ->
+ let kf = Globals.Functions.get vinfo in
+ let frama_b = Ast_info.is_frama_c_builtin (Kernel_function.get_name kf)
+ in
+ let va_start = Kernel_function.get_name kf = "__builtin_va_start" in
+ (frama_b, va_start)
+ | _ -> (false, false)
+ in
+ if is_va_start then begin
+ match (List.nth argl 0).enode with
| Lval lv -> self#mark_to_skip_initialized lv
| _ -> ()
- end ;
- if is_builtin
- then Cil.SkipChildren
- else begin
- self#treat_call ret_opt;
- (* Alarm if the call is through a pointer. Done in DoChildrenPost to get a
- more pleasant ordering of annotations. *)
- let do_ptr () =
- if self#do_pointer_call () then
- match funcexp.enode with
- | Lval (Mem e, _) -> self#generate_assertion Rte.pointer_call (e, argl)
- | _ -> ()
- in
- Cil.DoChildrenPost (fun res -> do_ptr (); res)
- end
- | Local_init (v,ConsInit(f,args,kind),loc) ->
- let do_call lv _e _args _loc = self#treat_call lv in
- Cil.treat_constructor_as_func do_call v f args kind loc;
- Cil.DoChildren
- | Local_init (v,AssignInit (SingleInit exp),_) ->
- self#check_uchar_assign (Cil.var v) exp
- | Local_init (_,AssignInit _,_)
- | Asm _ | Skip _ | Code_annot _ -> Cil.DoChildren
+ end ;
+ if is_builtin
+ then Cil.SkipChildren
+ else begin
+ self#treat_call ret_opt;
+ (* Alarm if the call is through a pointer. Done in DoChildrenPost to get a
+ more pleasant ordering of annotations. *)
+ let do_ptr () =
+ if self#do_pointer_call () then
+ match funcexp.enode with
+ | Lval (Mem e, _) -> self#generate_assertion Rte.pointer_call (e, argl)
+ | _ -> ()
+ in
+ Cil.DoChildrenPost (fun res -> do_ptr (); res)
+ end
+ | Local_init (v,ConsInit(f,args,kind),loc) ->
+ let do_call lv _e _args _loc = self#treat_call lv in
+ Cil.treat_constructor_as_func do_call v f args kind loc;
+ Cil.DoChildren
+ | Local_init (v,AssignInit (SingleInit exp),_) ->
+ self#check_uchar_assign (Cil.var v) exp
+ | Local_init (_,AssignInit _,_)
+ | Asm _ | Skip _ | Code_annot _ -> Cil.DoChildren
method! vexpr exp =
Options.debug "considering exp %a\n" Printer.pp_exp exp;
@@ -281,12 +206,12 @@ class annot_visitor kf to_annot on_alarm = object (self)
let generate () =
match exp.enode with
| BinOp((Div | Mod) as op, lexp, rexp, ty) ->
- (match Cil.unrollType ty with
- | TInt(kind,_) ->
+ (match Cil.unrollType ty with
+ | TInt(kind,_) ->
(* add assertion "divisor not zero" *)
if self#do_div_mod () then
self#generate_assertion Rte.divmod_assertion rexp;
- if self#do_signed_overflow () && op = Div && Cil.isSigned kind then
+ if self#do_signed_overflow () && op = Div && Cil.isSigned kind then
(* treat the special case of signed division overflow
(no signed modulo overflow) *)
self#generate_assertion Rte.signed_div_assertion (exp, lexp, rexp)
@@ -295,7 +220,7 @@ class annot_visitor kf to_annot on_alarm = object (self)
| _ -> ())
| BinOp((Shiftlt | Shiftrt) as op, lexp, rexp,ttype ) ->
- (match Cil.unrollType ttype with
+ (match Cil.unrollType ttype with
| TInt(kind,_) ->
(* 0 <= rexp <= width *)
if self#do_shift () then begin
@@ -320,13 +245,13 @@ class annot_visitor kf to_annot on_alarm = object (self)
| BinOp((PlusA |MinusA | Mult) as op, lexp, rexp, ttype) ->
(* may be skipped if the enclosing expression is a downcast to a signed
type *)
- (match Cil.unrollType ttype with
- | TInt(kind,_) when Cil.isSigned kind ->
+ (match Cil.unrollType ttype with
+ | TInt(kind,_) when Cil.isSigned kind ->
if self#do_signed_overflow () && not (self#must_skip exp) then
self#generate_assertion
(Rte.mult_sub_add_assertion ~signed:true)
(exp, op, lexp, rexp)
- | TInt(kind,_) when not (Cil.isSigned kind) ->
+ | TInt(kind,_) when not (Cil.isSigned kind) ->
if self#do_unsigned_overflow () then
self#generate_assertion
(Rte.mult_sub_add_assertion ~signed:false)
@@ -340,8 +265,8 @@ class annot_visitor kf to_annot on_alarm = object (self)
"subtracting the promoted value from the largest value
of the promoted type and adding one",
the result is always representable: so no overflow *)
- (match Cil.unrollType ty with
- | TInt(kind,_) when Cil.isSigned kind ->
+ (match Cil.unrollType ty with
+ | TInt(kind,_) when Cil.isSigned kind ->
if self#do_signed_overflow () then
self#generate_assertion Rte.uminus_assertion exp;
| TFloat(fkind,_) when self#do_finite_float () ->
@@ -356,9 +281,9 @@ class annot_visitor kf to_annot on_alarm = object (self)
(* left values are checked for valid access *)
if self#do_mem_access () then begin
Options.debug
- "exp %a is an lval: validity of potential mem access checked"
+ "exp %a is an lval: validity of potential mem access checked"
Printer.pp_exp exp;
- self#generate_assertion
+ self#generate_assertion
(Rte.lval_assertion ~read_only:Alarms.For_reading) lval
end;
if self#do_initialized () && not (self#must_skip_initialized lval) then begin
@@ -391,12 +316,12 @@ class annot_visitor kf to_annot on_alarm = object (self)
| _ -> ());
| Const (CReal(f,fkind,_)) when self#do_finite_float () ->
begin match Pervasives.classify_float f with
- | FP_normal
- | FP_subnormal
- | FP_zero -> ()
- | FP_infinite
- | FP_nan ->
- self#generate_assertion Rte.finite_float_assertion (fkind,exp)
+ | FP_normal
+ | FP_subnormal
+ | FP_zero -> ()
+ | FP_infinite
+ | FP_nan ->
+ self#generate_assertion Rte.finite_float_assertion (fkind,exp)
end
| StartOf _
| AddrOf _
@@ -416,41 +341,78 @@ class annot_visitor kf to_annot on_alarm = object (self)
end
-let rte_annotations stmt =
- Annotations.fold_code_annot
- (fun e a acc -> if Emitter.equal e Generator.emitter then a ::acc else acc)
- stmt
- []
-
-
-(** {2 List of all RTEs on a given Cil object} *)
-
-let get_annotations from kf stmt x =
- let to_annot = annotate_from_options () in
- (* Accumulator containing all the code_annots corresponding to an alarm
- emitted so far. *)
- let code_annots = ref [] in
- let on_alarm ki ?status:_ alarm =
- let ca, _ = Alarms.to_annot ki alarm in
- code_annots := ca :: !code_annots;
- in
- let o = object (self)
- inherit annot_visitor kf to_annot on_alarm
+(** {2 Iterate over Alarms on Cil elements} *)
+
+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 visitor = object (self)
+ inherit annot_visitor kf (filter flags) (on_alarm kf)
+ initializer self#push_stmt stmt
+ end in
+ ignore (visit (visitor :> Cil.cilVisitor) element)
+
+type 'a iterator =
+ ?flags:Flags.t -> on_alarm ->
+ Kernel_function.t -> Cil_types.stmt -> 'a -> unit
+
+let iter_lval : lval iterator = iter_alarms Cil.visitCilLval
+let iter_exp : exp iterator = iter_alarms Cil.visitCilExpr
+let iter_instr : instr iterator = iter_alarms Cil.visitCilInstr
+let iter_stmt : stmt iterator = iter_alarms Cil.visitCilStmt
+
+(** {2 Regitration} *)
+
+let status ~invalid =
+ if invalid then Some Property_status.False_if_reachable else None
+
+let register emitter kf stmt ~invalid alarm =
+ let status = status ~invalid in
+ Alarms.register emitter ~kf (Kstmt stmt) ?status alarm
+
+(* -------------------------------------------------------------------------- *)
+(* --- List Code Annotations --- *)
+(* -------------------------------------------------------------------------- *)
+
+let collector () =
+ let pool = ref [] in
+ let on_alarm stmt ~invalid:_ alarm =
+ let ca, _ = Alarms.to_annot (Kstmt stmt) alarm in
+ 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 [to_annot] *)
-let annotate_kf_aux to_annot kf =
+(* generates annotation for function kf on the basis of [flags] *)
+let annotate ?flags kf =
+ let flags = filter flags in
Options.debug "annotating function %a" Kernel_function.pretty kf;
match kf.fundec with
| Declaration _ -> ()
@@ -470,72 +432,35 @@ let annotate_kf_aux to_annot kf =
(* Strict version of ||, because [comp] has side-effects *)
let (|||) a b = a || b in
let open Generator in
- if comp Initialized.accessor to_annot.initialized |||
- comp Mem_access.accessor to_annot.mem_access |||
- comp Pointer_call.accessor to_annot.pointer_call |||
- comp Div_mod.accessor to_annot.div_mod |||
- comp Shift.accessor to_annot.shift |||
- comp Left_shift_negative.accessor to_annot.left_shift_negative |||
- comp Right_shift_negative.accessor to_annot.right_shift_negative |||
- comp Signed_overflow.accessor to_annot.signed_ov |||
- comp Signed_downcast.accessor to_annot.signed_downcast |||
- comp Unsigned_overflow.accessor to_annot.unsigned_ov |||
- comp Unsigned_downcast.accessor to_annot.unsigned_downcast |||
- comp Float_to_int.accessor to_annot.float_to_int |||
- comp Finite_float.accessor to_annot.finite_float
+ let open Flags in
+ if comp Initialized.accessor flags.initialized |||
+ comp Mem_access.accessor flags.mem_access |||
+ comp Pointer_call.accessor flags.pointer_call |||
+ comp Div_mod.accessor flags.div_mod |||
+ comp Shift.accessor flags.shift |||
+ comp Left_shift_negative.accessor flags.left_shift_negative |||
+ comp Right_shift_negative.accessor flags.right_shift_negative |||
+ comp Signed_overflow.accessor flags.signed_overflow |||
+ comp Signed_downcast.accessor flags.signed_downcast |||
+ comp Unsigned_overflow.accessor flags.unsigned_overflow |||
+ comp Unsigned_downcast.accessor flags.unsigned_downcast |||
+ comp Float_to_int.accessor flags.float_to_int |||
+ comp Finite_float.accessor flags.finite_float
then begin
Options.feedback "annotating function %a" Kernel_function.pretty kf;
let warn = Options.Warn.get () in
- let on_alarm ki ?status alarm =
- let ca, _ = Alarms.register Generator.emitter ~kf ki ?status alarm in
- match warn, status with
- | true, Some Property_status.False_if_reachable ->
+ let on_alarm stmt ~invalid alarm =
+ let ca, _ = register Generator.emitter kf stmt ~invalid alarm in
+ if warn && invalid then
Options.warn "@[guaranteed RTE:@ %a@]"
Printer.pp_code_annotation ca
- | _ -> ()
in
- let vis = new annot_visitor kf to_annot on_alarm in
+ let vis = new annot_visitor kf flags on_alarm in
let nkf = Visitor.visitFramacFunction vis f in
assert(nkf == f);
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 (annotate_from_options ()) kf
-
-(* annotate for all rte + unsigned overflows (which are not rte), for a given
- function *)
-let do_all_rte kf =
- let to_annot =
- { annotate_all with
- signed_downcast = false;
- unsigned_downcast = false; }
- in
- annotate_kf_aux to_annot kf
-
-(* annotate for rte only (not unsigned overflows and downcasts) for a given
- function *)
-let do_rte kf =
- let to_annot =
- { annotate_all with
- unsigned_ov = false;
- signed_downcast = false;
- unsigned_downcast = false; }
- in
- annotate_kf_aux to_annot 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 1413e3b8f7bf3411f312dd1401f8664fa1c4d521..3fe997f0057f61ac8eae273f29fa88a649f41308 100644
--- a/src/plugins/rte/visit.mli
+++ b/src/plugins/rte/visit.mli
@@ -20,28 +20,76 @@
(* *)
(**************************************************************************)
+(* --- Synchronized with RteGen.mli --- *)
+
open Cil_types
-(** 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
+(** {2 RTE Generator API} *)
+
+(** Annotate kernel-function with respect to options
+ and current generator status. *)
+val annotate: ?flags:Flags.t -> 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 rte_annotations: stmt -> code_annotation list
-val do_stmt_annotations: kernel_function -> stmt -> code_annotation list
-val do_exp_annotations: kernel_function -> stmt -> exp -> code_annotation list
+(** Returns annotations associated to alarms {i without} registering them. *)
+val get_annotations_lval:
+ ?flags:Flags.t -> kernel_function -> stmt -> lval -> 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.
+(** {2 Low-Level RTE Iterators}
+
+ RTE Iterators allow to traverse a Cil AST fragment (stmt, expr, l-value)
+ and reveal its potential Alarms. Each alarm will be presented to a callback
+ with type [on_alarm], that you can use in turn to generate an annotation
+ or perform any other treatment.
+
+ Flags can be used to select which alarm categories to visit, with
+ defaults derived from Kernel and RTE plug-in parameters.
*)
-val compute: unit -> unit
+
+(** Alarm callback.
+
+ The [on_alarm kf stmt ~invalid alarm] callback is invoked on each
+ alarm visited by an RTE iterator, provided it fits the selected categories.
+ The [kf] and [stmt] designates the statement originating the alarm,
+ while [~invalid:true] is set when the alarm trivially evaluates to false.
+ In this later case, the corresponding annotation shall be assigned
+ the status [False_if_reachable].
+
+*)
+type on_alarm = kernel_function -> stmt -> invalid:bool -> Alarms.alarm -> unit
+
+(** Type of low-level iterators visiting an element ['a] of the AST *)
+type 'a iterator = ?flags:Flags.t -> on_alarm ->
+ Kernel_function.t -> Cil_types.stmt -> 'a -> unit
+
+val iter_lval : lval iterator
+val iter_exp : exp iterator
+val iter_instr : instr iterator
+val iter_stmt : stmt iterator
+
+(** {2 Alarm Helpers} *)
+
+(** Returns a [False_if_reachable] status when invalid. *)
+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. Simple wrapper over [Alarms.register]. *)
+val register :
+ Emitter.t ->
+ kernel_function -> stmt -> invalid:bool -> Alarms.alarm ->
+ code_annotation * bool
(*
Local Variables: