diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 2453bded6360dc01a4109b3724d32b37fb135586..9d0a42e6ebda2f54c326da5882d51ae0154901ce 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -1021,6 +1021,7 @@ module RteGen = struct
let get_pointer_downcast_status = mk_fun "RteGen.get_pointer_downcast_status"
let get_float_to_int_status = mk_fun "RteGen.get_float_to_int_status"
let get_finite_float_status = mk_fun "RteGen.get_finite_float_status"
+ let get_pointer_value_status = mk_fun "RteGen.get_pointer_value_status"
let get_bool_value_status = mk_fun "RteGen.get_bool_value_status"
end
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index a54ae74932d0942ba3df7aa1508675e0dda9c5a8..43b89f26ecf759389eb744dbe06b00e7a871b97f 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -903,6 +903,7 @@ module RteGen : sig
val get_pointer_downcast_status : (unit -> status_accessor) ref
val get_float_to_int_status : (unit -> status_accessor) ref
val get_finite_float_status : (unit -> status_accessor) ref
+ val get_pointer_value_status : (unit -> status_accessor) ref
val get_bool_value_status : (unit -> status_accessor) ref
end
diff --git a/src/plugins/rte/flags.ml b/src/plugins/rte/flags.ml
index 7d17b15a3a9577579b409c2396f89060023f48a8..fea846e8b1989abd969c2b70363767b2379fd136 100644
--- a/src/plugins/rte/flags.ml
+++ b/src/plugins/rte/flags.ml
@@ -40,6 +40,7 @@ type t = {
float_to_int: bool;
finite_float: bool;
pointer_call: bool;
+ pointer_value: bool;
bool_value: bool;
}
@@ -59,6 +60,7 @@ let all = {
float_to_int = true;
finite_float = true;
pointer_call = true;
+ pointer_value = true;
bool_value = true;
}
@@ -78,6 +80,7 @@ let none = {
float_to_int = false;
finite_float = false;
pointer_call = false;
+ pointer_value = false;
bool_value = false;
}
@@ -102,6 +105,7 @@ let default
?float_to_int
?finite_float
?pointer_call
+ ?pointer_value
?bool_value
() =
{
@@ -120,6 +124,7 @@ let default
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 ;
+ pointer_value = option Kernel.InvalidPointer.get pointer_value;
bool_value = option Kernel.InvalidBool.get bool_value ;
}
diff --git a/src/plugins/rte/flags.mli b/src/plugins/rte/flags.mli
index 3ea19d53f367e367c1a0e414871403d5bef54d1b..fc1a7b6f4d7cf274a86954c51a4cf4c900b0e7e5 100644
--- a/src/plugins/rte/flags.mli
+++ b/src/plugins/rte/flags.mli
@@ -42,6 +42,7 @@ type t = {
float_to_int: bool;
finite_float: bool;
pointer_call: bool;
+ pointer_value: bool;
bool_value: bool;
}
@@ -62,6 +63,7 @@ val default :
?float_to_int:bool ->
?finite_float:bool ->
?pointer_call:bool ->
+ ?pointer_value:bool ->
?bool_value:bool ->
unit -> t
diff --git a/src/plugins/rte/generator.ml b/src/plugins/rte/generator.ml
index 8c8e697d4dcf846db06cb7c6062fc9b5fd9847a1..4c84ce9c126543da6535ca91d6b455e1624eb830 100644
--- a/src/plugins/rte/generator.ml
+++ b/src/plugins/rte/generator.ml
@@ -83,6 +83,14 @@ module Mem_access =
let additional_parameters = [ Kernel.SafeArrays.parameter ]
end)
+module Pointer_value =
+ Make
+ (struct
+ let name = "pointer_value"
+ let parameter = Kernel.InvalidPointer.parameter
+ let additional_parameters = []
+ end)
+
module Pointer_call =
Make
(struct
diff --git a/src/plugins/rte/generator.mli b/src/plugins/rte/generator.mli
index 1518a0acc67f22908320d834bb54b1f99c22eec4..0116b9d7698346c6a8811defdb08ceb55039adb7 100644
--- a/src/plugins/rte/generator.mli
+++ b/src/plugins/rte/generator.mli
@@ -30,6 +30,7 @@ end
module Initialized: S
module Mem_access: S
+module Pointer_value: S
module Pointer_call: S
module Div_mod: S
module Shift: S
diff --git a/src/plugins/rte/register.ml b/src/plugins/rte/register.ml
index 8b5afe27c054f83e273da685237efc10d5899d2d..a3f3df56f048d270e2bdb4ede38ae8cac65c1646 100644
--- a/src/plugins/rte/register.ml
+++ b/src/plugins/rte/register.ml
@@ -96,6 +96,7 @@ let () =
nojournal_register get_pointer_downcast_status Pointer_downcast.accessor;
nojournal_register get_float_to_int_status Float_to_int.accessor;
nojournal_register get_finite_float_status Finite_float.accessor;
+ nojournal_register get_pointer_value_status Pointer_value.accessor;
nojournal_register get_bool_value_status Bool_value.accessor ;
nojournal_register get_all_status all_statuses;
;;
diff --git a/src/plugins/rte/rte.ml b/src/plugins/rte/rte.ml
index 467d65f1ffd919d19c5ef4f4784c8cef98e9b490..16845eed8d574889527464bbff6a589dcd4c9b0b 100644
--- a/src/plugins/rte/rte.ml
+++ b/src/plugins/rte/rte.ml
@@ -451,6 +451,24 @@ let finite_float_assertion ~remove_trivial:_ ~on_alarm (fkind, exp) =
let pointer_call ~remove_trivial:_ ~on_alarm (e, args) =
on_alarm ~invalid:false (Alarms.Function_pointer (e, Some args))
+let is_safe_pointer_value = function
+ | Lval (Var vi, offset) ->
+ (* Reading a pointer variable must emit an alarm if an invalid pointer value
+ could have been written without previous alarm, through:
+ - an union type, in which case [offset] is not NoOffset;
+ - an untyped write, in which case the address of [vi] is taken. *)
+ not vi.vaddrof && offset = NoOffset
+ | AddrOf (_, NoOffset) | StartOf (_, NoOffset) -> true
+ | CastE (_typ, e) ->
+ (* 0 can always be converted into a NULL pointer. *)
+ let v = get_expr_val e in
+ Extlib.may_map ~dft:false Integer.(equal zero) v
+ | _ -> false
+
+let pointer_value ~remove_trivial ~on_alarm expr =
+ if not (remove_trivial && is_safe_pointer_value expr.enode)
+ then on_alarm ~invalid:false (Alarms.Invalid_pointer expr)
+
let bool_value ~remove_trivial ~on_alarm lv =
match remove_trivial, lv with
| true, (Var vi, NoOffset)
diff --git a/src/plugins/rte/rte.mli b/src/plugins/rte/rte.mli
index 7c787c279a81d18e1eae71b1683d411036e8874d..c7a292c92cad6f05ceb1b015448c85c4ccbf9e26 100644
--- a/src/plugins/rte/rte.mli
+++ b/src/plugins/rte/rte.mli
@@ -44,6 +44,7 @@ val downcast_assertion: (typ * exp) alarm_gen
val float_to_int_assertion: (typ * exp) alarm_gen
val finite_float_assertion: (fkind * exp) alarm_gen
val pointer_call: (exp * exp list) alarm_gen
+val pointer_value: exp alarm_gen
val bool_value: lval alarm_gen
(*
diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml
index 61dafe98471f4ed4f86338f62319019ef54b5c44..36c092b8a7ca1adc1f69f5179f552820a8e5644d 100644
--- a/src/plugins/rte/visit.ml
+++ b/src/plugins/rte/visit.ml
@@ -99,6 +99,9 @@ class annot_visitor kf flags on_alarm = object (self)
method private do_pointer_call () =
flags.Flags.pointer_call && not (Generator.Pointer_call.is_computed kf)
+ method private do_pointer_value () =
+ flags.Flags.pointer_value && not (Generator.Pointer_value.is_computed kf)
+
method private do_bool_value () =
flags.Flags.bool_value && not (Generator.Bool_value.is_computed kf)
@@ -275,6 +278,9 @@ class annot_visitor kf flags on_alarm = object (self)
self#generate_assertion Rte.finite_float_assertion (fkind,exp)
| _ -> ())
+ | BinOp((PlusPI | MinusPI), _, _, _) when self#do_pointer_value () ->
+ self#generate_assertion Rte.pointer_value exp
+
| UnOp(Neg, exp, ty) ->
(* Note: if unary minus on unsigned integer is to be understood as
"subtracting the promoted value from the largest value
@@ -290,6 +296,8 @@ class annot_visitor kf flags on_alarm = object (self)
| Lval lval ->
(match Cil.(unrollType (typeOfLval lval)) with
+ | TPtr _ when self#do_pointer_value () ->
+ self#generate_assertion Rte.pointer_value exp
| TInt (IBool,_) when self#do_bool_value () ->
self#generate_assertion Rte.bool_value lval
| _ -> ());
@@ -313,6 +321,8 @@ class annot_visitor kf flags on_alarm = object (self)
(* to , from *)
| TInt _, TPtr _ when self#do_pointer_downcast () ->
self#generate_assertion Rte.downcast_assertion (ty, e)
+ | TPtr _, TInt _ when self#do_pointer_value () ->
+ self#generate_assertion Rte.pointer_value exp
| TInt(kind,_), TInt (_, _) ->
let signed = Cil.isSigned kind in
@@ -339,8 +349,9 @@ class annot_visitor kf flags on_alarm = object (self)
| FP_nan ->
self#generate_assertion Rte.finite_float_assertion (fkind,exp)
end
- | StartOf _
- | AddrOf _
+ | StartOf _ | AddrOf _ ->
+ if self#do_pointer_value ()
+ then self#generate_assertion Rte.pointer_value exp
| Info _
| UnOp _
| Const _
@@ -451,6 +462,7 @@ let annotate ?flags kf =
let open Flags in
if comp Initialized.accessor flags.initialized |||
comp Mem_access.accessor flags.mem_access |||
+ comp Pointer_value.accessor flags.pointer_value |||
comp Pointer_call.accessor flags.pointer_call |||
comp Div_mod.accessor flags.div_mod |||
comp Shift.accessor flags.shift |||
diff --git a/tests/rte/oracle/twofunc.res.oracle b/tests/rte/oracle/twofunc.res.oracle
index 5d0a80d5f3847f4511ec8b4104f59014643e42ae..834e89b4e6941e3bb468d33795f53da68909b733 100644
--- a/tests/rte/oracle/twofunc.res.oracle
+++ b/tests/rte/oracle/twofunc.res.oracle
@@ -143,6 +143,7 @@ int main(void)
[kernel] - shift_value_out_of_bounds = true
[kernel] - division_by_zero = true
[kernel] - pointer_call = true
+[kernel] - pointer_value = false
[kernel] - mem_access = true
[kernel] - initialized = false
[kernel] kf = main
@@ -159,6 +160,7 @@ int main(void)
[kernel] - shift_value_out_of_bounds = true
[kernel] - division_by_zero = true
[kernel] - pointer_call = true
+[kernel] - pointer_value = false
[kernel] - mem_access = true
[kernel] - initialized = false
[kernel] ================================
@@ -237,6 +239,7 @@ int main(void)
[kernel] - shift_value_out_of_bounds = true
[kernel] - division_by_zero = true
[kernel] - pointer_call = true
+[kernel] - pointer_value = false
[kernel] - mem_access = true
[kernel] - initialized = false
[kernel] kf = main
@@ -253,6 +256,7 @@ int main(void)
[kernel] - shift_value_out_of_bounds = true
[kernel] - division_by_zero = true
[kernel] - pointer_call = true
+[kernel] - pointer_value = false
[kernel] - mem_access = true
[kernel] - initialized = false
[kernel] ================================