[pulse] allow models in invalidation traces

Summary: Be more flexible in what type of function calls are allowed in `ViaCall ...` actions to be able to include models. Also get rid of `here here` in traces /o\ As a side-effect, get more precise (=qualified) procedure names in traces (but not in messages so as not to be too verbose). Reviewed By: mbouaziz, ngorogiannis Differential Revision: D16121092 fbshipit-source-id: fb51b02f8
telekom · Jul 15, 2019 · d9aadf5 · d9aadf5
1 parent ba6e6bf
commit d9aadf5
Show file tree

Hide file tree

Showing 8 changed files with 123 additions and 114 deletions.
diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml
@@ -85,7 +85,7 @@ module PulseTransferFunctions = struct
         PulseOperations.call ~caller_summary call_loc callee_pname ~ret ~actuals astate
     | None ->
         L.d_printfln "Indirect call %a@\n" Exp.pp call_exp ;
-        exec_unknown_call (`IndirectCall call_exp) ret call_exp actuals flags call_loc astate
+        exec_unknown_call (SkippedUnknownCall call_exp) ret call_exp actuals flags call_loc astate
         >>| List.return
 
 

diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml
@@ -375,7 +375,7 @@ module PrePost = struct
       history call_state =
     let mk_action action =
       PulseDomain.InterprocAction.ViaCall
-        {action; proc_name= callee_proc_name; location= call_location}
+        {action; f= Call callee_proc_name; location= call_location}
     in
     match visit call_state ~addr_callee:addr_pre ~addr_caller with
     | `AlreadyVisited, call_state ->
@@ -522,7 +522,9 @@ module PrePost = struct
     match (attr : PulseDomain.Attribute.t) with
     | Invalid trace ->
         PulseDomain.Attribute.Invalid
-          { action= PulseDomain.InterprocAction.ViaCall {action= trace.action; proc_name; location}
+          { action=
+              PulseDomain.InterprocAction.ViaCall
+                {action= trace.action; f= Call proc_name; location}
           ; history= trace.history }
     | MustBeValid _ | AddressOfCppTemporary (_, _) | Closure _ | StdVectorReserve ->
         attr
@@ -546,7 +548,7 @@ module PrePost = struct
           let addr_curr, subst = subst_find_or_new subst addr_callee in
           ( subst
           , ( addr_curr
-            , PulseDomain.ValueHistory.Call {f= `Call callee_proc_name; location= call_loc}
+            , PulseDomain.ValueHistory.Call {f= Call callee_proc_name; location= call_loc}
               :: trace_post ) ) )
     in
     let heap =

diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml
@@ -43,23 +43,23 @@ let get_message = function
          Likewise if we don't have "x" in the second part but instead some non-user-visible expression, then
          "`x->f` accesses `x`, which was invalidated at line 42 by `delete`"
       *)
-      let pp_access_trace f (trace : _ PulseDomain.Trace.t) =
+      let pp_access_trace fmt (trace : _ PulseDomain.Trace.t) =
         match trace.action with
         | Immediate {imm= _; _} ->
-            F.fprintf f "accessing memory that "
-        | ViaCall {proc_name; _} ->
-            F.fprintf f "call to `%a` eventually accesses memory that " Typ.Procname.describe
-              proc_name
+            F.fprintf fmt "accessing memory that "
+        | ViaCall {f; _} ->
+            F.fprintf fmt "call to %a eventually accesses memory that "
+              PulseDomain.describe_call_event f
       in
-      let pp_invalidation_trace line f trace =
+      let pp_invalidation_trace line fmt trace =
         match trace.PulseDomain.Trace.action with
         | Immediate {imm= invalidation; _} ->
-            F.fprintf f "%a on line %d" PulseDomain.Invalidation.describe invalidation line
-        | ViaCall {action; proc_name; _} ->
-            F.fprintf f "%a on line %d indirectly during the call to `%a`"
+            F.fprintf fmt "%a on line %d" PulseDomain.Invalidation.describe invalidation line
+        | ViaCall {action; f; _} ->
+            F.fprintf fmt "%a on line %d indirectly during the call to %a"
               PulseDomain.Invalidation.describe
               (PulseDomain.InterprocAction.get_immediate action)
-              line Typ.Procname.describe proc_name
+              line PulseDomain.describe_call_event f
       in
       let line_of_trace trace =
         let {Location.line; _} =
@@ -83,7 +83,7 @@ let get_trace = function
   | AccessToInvalidAddress {accessed_by; invalidated_by} ->
       PulseDomain.Trace.add_to_errlog ~header:"invalidation part of the trace starts here"
         (fun f invalidation ->
-          F.fprintf f "memory %a" PulseDomain.Invalidation.describe invalidation )
+          F.fprintf f "memory %a here" PulseDomain.Invalidation.describe invalidation )
         invalidated_by
       @@ PulseDomain.Trace.add_to_errlog ~header:"use-after-lifetime part of the trace starts here"
            (fun f () -> F.pp_print_string f "invalid access occurs here")

diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml
@@ -10,6 +10,30 @@ module L = Logging
 
 (* {2 Abstract domain description } *)
 
+type call_event =
+  | Call of Typ.Procname.t
+  | Model of string
+  | SkippedKnownCall of Typ.Procname.t
+  | SkippedUnknownCall of Exp.t
+[@@deriving compare]
+
+let pp_call_event_config ~verbose fmt =
+  let pp_proc_name = if verbose then Typ.Procname.pp else Typ.Procname.describe in
+  function
+  | Call proc_name ->
+      F.fprintf fmt "`%a()`" pp_proc_name proc_name
+  | Model model ->
+      F.fprintf fmt "`%s` (modelled)" model
+  | SkippedKnownCall proc_name ->
+      F.fprintf fmt "function `%a` with no summary" pp_proc_name proc_name
+  | SkippedUnknownCall call_exp ->
+      F.fprintf fmt "unresolved call expression `%a`" Exp.pp call_exp
+
+
+let pp_call_event = pp_call_event_config ~verbose:true
+
+let describe_call_event = pp_call_event_config ~verbose:false
+
 module Invalidation = struct
   type std_vector_function =
     | Assign
@@ -101,13 +125,7 @@ module ValueHistory = struct
     | CppTemporaryCreated of Location.t
     | Assignment of {location: Location.t}
     | Capture of {captured_as: Pvar.t; location: Location.t}
-    | Call of
-        { f:
-            [ `Call of Typ.Procname.t
-            | `UnknownCall of Typ.Procname.t
-            | `IndirectCall of Exp.t
-            | `Model of string ]
-        ; location: Location.t }
+    | Call of {f: call_event; location: Location.t}
   [@@deriving compare]
 
   let pp_event_no_location fmt = function
@@ -120,17 +138,7 @@ module ValueHistory = struct
     | Assignment _ ->
         F.pp_print_string fmt "assigned"
     | Call {f; location= _} ->
-        let pp_f fmt = function
-          | `Call proc_name ->
-              F.fprintf fmt "`%a()`" Typ.Procname.pp proc_name
-          | `UnknownCall proc_name ->
-              F.fprintf fmt "unknown function `%a`" Typ.Procname.pp proc_name
-          | `IndirectCall call_exp ->
-              F.fprintf fmt "unresolved expression `%a`" Exp.pp call_exp
-          | `Model model ->
-              F.fprintf fmt "`%s()` (pulse model)" model
-        in
-        F.fprintf fmt "returned from call to %a" pp_f f
+        F.fprintf fmt "returned from call to %a" pp_call_event f
 
 
   let location_of_event = function
@@ -167,7 +175,7 @@ end
 module InterprocAction = struct
   type 'a t =
     | Immediate of {imm: 'a; location: Location.t}
-    | ViaCall of {action: 'a t; proc_name: Typ.Procname.t; location: Location.t}
+    | ViaCall of {action: 'a t; f: call_event; location: Location.t}
   [@@deriving compare]
 
   let rec get_immediate = function
@@ -180,24 +188,23 @@ module InterprocAction = struct
   let pp pp_immediate fmt = function
     | Immediate {imm; _} ->
         pp_immediate fmt imm
-    | ViaCall {proc_name; action; _} ->
-        F.fprintf fmt "%a in call to `%a`" pp_immediate (get_immediate action)
-          Typ.Procname.describe proc_name
+    | ViaCall {f; action; _} ->
+        F.fprintf fmt "%a in call to %a" pp_immediate (get_immediate action) pp_call_event f
 
 
   let add_to_errlog ~nesting pp_immediate action errlog =
     let rec aux ~nesting rev_errlog action =
       match action with
       | Immediate {imm; location} ->
           let rev_errlog =
-            Errlog.make_trace_element nesting location (F.asprintf "%a here" pp_immediate imm) []
+            Errlog.make_trace_element nesting location (F.asprintf "%a" pp_immediate imm) []
             :: rev_errlog
           in
           List.rev_append rev_errlog errlog
-      | ViaCall {action; proc_name; location} ->
+      | ViaCall {action; f; location} ->
           aux ~nesting:(nesting + 1)
             ( Errlog.make_trace_element nesting location
-                (F.asprintf "when calling `%a` here" Typ.Procname.describe proc_name)
+                (F.asprintf "when calling %a here" pp_call_event f)
                 []
             :: rev_errlog )
             action

diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli
@@ -8,6 +8,14 @@
 open! IStd
 module F = Format
 
+type call_event =
+  | Call of Typ.Procname.t  (** known function with summary *)
+  | Model of string  (** hardcoded model *)
+  | SkippedKnownCall of Typ.Procname.t  (** known function without summary *)
+  | SkippedUnknownCall of Exp.t  (** couldn't link the expression to a proc name *)
+
+val describe_call_event : F.formatter -> call_event -> unit
+
 module Invalidation : sig
   type std_vector_function =
     | Assign
@@ -41,13 +49,7 @@ module ValueHistory : sig
     | CppTemporaryCreated of Location.t
     | Assignment of {location: Location.t}
     | Capture of {captured_as: Pvar.t; location: Location.t}
-    | Call of
-        { f:
-            [ `Call of Typ.Procname.t  (** known function with summary *)
-            | `UnknownCall of Typ.Procname.t  (** known function without summary *)
-            | `IndirectCall of Exp.t  (** couldn't link the expression to a proc name *)
-            | `Model of string  (** hardcoded model *) ]
-        ; location: Location.t }
+    | Call of {f: call_event; location: Location.t}
 
   type t = event list [@@deriving compare]
 
@@ -58,7 +60,7 @@ end
 module InterprocAction : sig
   type 'a t =
     | Immediate of {imm: 'a; location: Location.t}
-    | ViaCall of {action: 'a t; proc_name: Typ.Procname.t; location: Location.t}
+    | ViaCall of {action: 'a t; f: call_event; location: Location.t}
   [@@deriving compare]
 
   val get_immediate : 'a t -> 'a

diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml
@@ -20,7 +20,7 @@ type model = exec_fun
 module Misc = struct
   let shallow_copy model_desc : model =
    fun ~caller_summary:_ location ~ret:(ret_id, _) ~actuals astate ->
-    let event = PulseDomain.ValueHistory.Call {f= `Model model_desc; location} in
+    let event = PulseDomain.ValueHistory.Call {f= Model model_desc; location} in
     ( match actuals with
     | [(dest_pointer_hist, _); (src_pointer_hist, _)] ->
         PulseOperations.eval_access location src_pointer_hist Dereference astate
@@ -69,7 +69,7 @@ module Cplusplus = struct
 
   let placement_new : model =
    fun ~caller_summary:_ location ~ret:(ret_id, _) ~actuals astate ->
-    let event = PulseDomain.ValueHistory.Call {f= `Model "<placement new>"; location} in
+    let event = PulseDomain.ValueHistory.Call {f= Model "<placement new>()"; location} in
     match List.rev actuals with
     | ((address, _), _) :: _ ->
         Ok [PulseOperations.write_id ret_id (address, [event]) astate]
@@ -81,9 +81,7 @@ module StdFunction = struct
   let operator_call : model =
    fun ~caller_summary location ~ret ~actuals astate ->
     let havoc_ret (ret_id, _) astate =
-      let event =
-        PulseDomain.ValueHistory.Call {f= `Model "std::function::operator()"; location}
-      in
+      let event = PulseDomain.ValueHistory.Call {f= Model "std::function::operator()"; location} in
       [PulseOperations.havoc_id ret_id [event] astate]
     in
     match actuals with
@@ -141,8 +139,8 @@ module StdVector = struct
         let crumb =
           PulseDomain.ValueHistory.Call
             { f=
-                `Model
-                  (Format.asprintf "%a" PulseDomain.Invalidation.pp_std_vector_function vector_f)
+                Model
+                  (Format.asprintf "%a()" PulseDomain.Invalidation.pp_std_vector_function vector_f)
             ; location }
         in
         reallocate_internal_array [crumb] vector vector_f location astate >>| List.return
@@ -152,7 +150,7 @@ module StdVector = struct
 
   let at : model =
    fun ~caller_summary:_ location ~ret ~actuals astate ->
-    let event = PulseDomain.ValueHistory.Call {f= `Model "std::vector::at"; location} in
+    let event = PulseDomain.ValueHistory.Call {f= Model "std::vector::at()"; location} in
     match actuals with
     | [(vector, _); (index, _)] ->
         element_of_internal_array location vector (fst index) astate
@@ -165,7 +163,7 @@ module StdVector = struct
    fun ~caller_summary:_ location ~ret:_ ~actuals astate ->
     match actuals with
     | [(vector, _); _value] ->
-        let crumb = PulseDomain.ValueHistory.Call {f= `Model "std::vector::reserve"; location} in
+        let crumb = PulseDomain.ValueHistory.Call {f= Model "std::vector::reserve()"; location} in
         reallocate_internal_array [crumb] vector Reserve location astate
         >>| PulseAbductiveDomain.Memory.std_vector_reserve (fst vector)
         >>| List.return
@@ -177,7 +175,7 @@ module StdVector = struct
    fun ~caller_summary:_ location ~ret:_ ~actuals astate ->
     match actuals with
     | [(vector, _); _value] ->
-        let crumb = PulseDomain.ValueHistory.Call {f= `Model "std::vector::push_back"; location} in
+        let crumb = PulseDomain.ValueHistory.Call {f= Model "std::vector::push_back()"; location} in
         if PulseAbductiveDomain.Memory.is_std_vector_reserved (fst vector) astate then
           (* assume that any call to [push_back] is ok after one called [reserve] on the same vector
              (a perfect analysis would also make sure we don't exceed the reserved size) *)

diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml
@@ -317,7 +317,7 @@ let call ~caller_summary call_loc callee_pname ~ret ~actuals astate =
           PulseAbductiveDomain.PrePost.apply callee_pname call_loc pre_post ~formals ~actuals
             astate
           >>| fun (post, return_val_opt) ->
-          let event = ValueHistory.Call {f= `Call callee_pname; location= call_loc} in
+          let event = ValueHistory.Call {f= Call callee_pname; location= call_loc} in
           let post =
             match return_val_opt with
             | Some return_val ->
@@ -329,5 +329,5 @@ let call ~caller_summary call_loc callee_pname ~ret ~actuals astate =
   | None ->
       (* no spec found for some reason (unknown function, ...) *)
       L.d_printfln "No spec found for %a@\n" Typ.Procname.pp callee_pname ;
-      let event = ValueHistory.Call {f= `UnknownCall callee_pname; location= call_loc} in
+      let event = ValueHistory.Call {f= SkippedKnownCall callee_pname; location= call_loc} in
       Ok [havoc_id (fst ret) [event] astate]