[rte] Generates alarms on invalid pointer values.

According to the kernel option -warn-invalid-pointer.

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
 

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
 

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 ;
   }
 

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
 

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

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

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;
 ;;

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)

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
 
 (*

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 |||

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] ================================