[pulse] better types to avoid `_fun_` prefix to proc names in bug traces

Summary:
Printing `Exp.Const (Cfun proc_name)` adds `_fun_` in front of the
procedure name, eg `_fun_foo` instead of `foo`. This showed up in pulse
traces.

Reviewed By: mbouaziz

Differential Revision: D16004606

fbshipit-source-id: 72ac6866f

infer/src/pulse/Pulse.ml

@@ -103,7 +103,7 @@ module PulseTransferFunctions = struct
               PulseAbductiveDomain.PrePost.apply callee_pname call_loc pre_post ~formals ~actuals
                 astate
               >>| fun (post, return_val_opt) ->
-              let event = ValueHistory.Call {f= `Call call_exp; 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 ->
@@ -115,7 +115,7 @@ module PulseTransferFunctions = struct
       | None ->
           (* no spec found for some reason (unknown function, ...) *)
           L.d_printfln "No spec found for %a@\n" Typ.Procname.pp callee_pname ;
-          unknown_function (`UnknownCall call_exp) )
+          unknown_function (`UnknownCall callee_pname) )
     | None ->
         L.d_printfln "Indirect call %a@\n" Exp.pp call_exp ;
         unknown_function (`IndirectCall call_exp)

infer/src/pulse/PulseAbductiveDomain.ml

@@ -577,8 +577,7 @@ module PrePost = struct
           let addr_curr, subst = subst_find_or_new subst addr_callee in
           ( subst
           , ( addr_curr
-            , PulseDomain.ValueHistory.Call
+            , PulseDomain.ValueHistory.Call {f= `Call callee_proc_name; location= call_loc}
-                {f= `Call (Const (Cfun callee_proc_name)); location= call_loc}
               :: trace_post ) ) )
     in
     let caller_post =

infer/src/pulse/PulseDomain.ml

@@ -102,7 +102,11 @@ module ValueHistory = struct
     | Assignment of {location: Location.t}
     | Capture of {captured_as: Pvar.t; location: Location.t}
     | Call of
-        { f: [`Call of Exp.t | `UnknownCall of Exp.t | `IndirectCall of Exp.t | `Model of string]
+        { f:
+            [ `Call of Typ.Procname.t
+            | `UnknownCall of Typ.Procname.t
+            | `IndirectCall of Exp.t
+            | `Model of string ]
         ; location: Location.t }
   [@@deriving compare]
 
@@ -117,10 +121,10 @@ module ValueHistory = struct
         F.pp_print_string fmt "assigned"
     | Call {f; location= _} ->
         let pp_f fmt = function
-          | `Call call_exp ->
+          | `Call proc_name ->
-              F.fprintf fmt "`%a()`" Exp.pp call_exp
+              F.fprintf fmt "`%a()`" Typ.Procname.pp proc_name
-          | `UnknownCall call_exp ->
+          | `UnknownCall proc_name ->
-              F.fprintf fmt "unknown function `%a`" Exp.pp call_exp
+              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 ->

infer/src/pulse/PulseDomain.mli

@@ -42,7 +42,11 @@ module ValueHistory : sig
     | Assignment of {location: Location.t}
     | Capture of {captured_as: Pvar.t; location: Location.t}
     | Call of
-        { f: [`Call of Exp.t | `UnknownCall of Exp.t | `IndirectCall of Exp.t | `Model of string]
+        { 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 }
 
   type t = event list [@@deriving compare]

infer/tests/codetoanalyze/cpp/pulse/issues.exp

@@ -9,15 +9,15 @@ codetoanalyze/cpp/pulse/interprocedural.cpp, delete_aliased_then_read_bad, 4, US
 codetoanalyze/cpp/pulse/interprocedural.cpp, delete_inner_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `wraps_delete_inner()` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access occurs here here]
 codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access occurs here here]
 codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `wraps_delete()` here,when calling `wraps_delete_inner()` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access occurs here here]
-codetoanalyze/cpp/pulse/interprocedural.cpp, feed_invalid_into_access_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,when calling `may_return_invalid_ptr_ok()` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,returned from call to `_fun_may_return_invalid_ptr_ok()`,assigned,when calling `call_store()` here,when calling `store()` here,invalid access occurs here here]
+codetoanalyze/cpp/pulse/interprocedural.cpp, feed_invalid_into_access_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,when calling `may_return_invalid_ptr_ok()` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,returned from call to `may_return_invalid_ptr_ok()`,assigned,when calling `call_store()` here,when calling `store()` here,invalid access occurs here here]
 codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here here]
-codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_heap_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `getwrapperHeap()` here,when calling `~WrapsB` here,when calling `__infer_inner_destructor_~WrapsB` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,returned from call to `_fun_ReferenceWrapperHeap::ReferenceWrapperHeap()`,invalid access occurs here here]
+codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_heap_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `getwrapperHeap()` here,when calling `~WrapsB` here,when calling `__infer_inner_destructor_~WrapsB` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,returned from call to `ReferenceWrapperHeap::ReferenceWrapperHeap()`,invalid access occurs here here]
-codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_stack_bad, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,when calling `getwrapperStack()` here,memory is the address of a stack variable `b` whose lifetime has ended here,use-after-lifetime part of the trace starts here,assigned,returned from call to `_fun_ReferenceWrapperStack::ReferenceWrapperStack()`,invalid access occurs here here]
+codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_stack_bad, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,when calling `getwrapperStack()` here,memory is the address of a stack variable `b` whose lifetime has ended here,use-after-lifetime part of the trace starts here,assigned,returned from call to `ReferenceWrapperStack::ReferenceWrapperStack()`,invalid access occurs here here]
 codetoanalyze/cpp/pulse/returns.cpp, returns::return_literal_stack_reference_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable declared,returned here]
 codetoanalyze/cpp/pulse/returns.cpp, returns::return_stack_pointer_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable declared,returned here]
 codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference1_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable declared,assigned,returned here]
 codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference2_bad, 3, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable declared,assigned,assigned,returned here]
-codetoanalyze/cpp/pulse/temporaries.cpp, temporaries::call_mk_UniquePtr_A_deref_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~UniquePtr` here,when calling `__infer_inner_destructor_~UniquePtr` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,returned from call to `_fun_temporaries::UniquePtr<temporaries::A>::get()`,assigned,invalid access occurs here here]
+codetoanalyze/cpp/pulse/temporaries.cpp, temporaries::call_mk_UniquePtr_A_deref_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~UniquePtr` here,when calling `__infer_inner_destructor_~UniquePtr` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,returned from call to `temporaries::UniquePtr<temporaries::A>::get()`,assigned,invalid access occurs here here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `Simple` here,invalid access occurs here here]
@@ -30,8 +30,8 @@ codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placemen
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,returned from call to `<placement new>()` (pulse model),assigned,invalid access occurs here here]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing3_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,assigned,invalid access occurs here here]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::reinit_after_explicit_destructor2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access occurs here here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::reinit_after_explicit_destructor_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,returned from call to `_fun_use_after_destructor::S::operator=()`,invalid access occurs here here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::reinit_after_explicit_destructor_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,returned from call to `use_after_destructor::S::operator=()`,invalid access occurs here here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_destructor_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,returned from call to `_fun_use_after_destructor::S::S()`,invalid access occurs here here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_destructor_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,returned from call to `use_after_destructor::S::S()`,invalid access occurs here here]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope1_bad, 7, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access occurs here here]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope2_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access occurs here here]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,memory is the address of a stack variable `c` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable declared,assigned,invalid access occurs here here]