From f15d9915a0737793087d4130234ef8ef9fe786ca Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 26 Jun 2019 10:27:31 -0700 Subject: [PATCH] [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 | 4 ++-- infer/src/pulse/PulseAbductiveDomain.ml | 3 +-- infer/src/pulse/PulseDomain.ml | 14 +++++++++----- infer/src/pulse/PulseDomain.mli | 6 +++++- infer/tests/codetoanalyze/cpp/pulse/issues.exp | 12 ++++++------ 5 files changed, 23 insertions(+), 16 deletions(-) diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 01a161e01..20d37e325 100644 --- a/infer/src/pulse/Pulse.ml +++ b/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) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 565383988..b3926100b 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/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 - {f= `Call (Const (Cfun callee_proc_name)); location= call_loc} + , PulseDomain.ValueHistory.Call {f= `Call callee_proc_name; location= call_loc} :: trace_post ) ) ) in let caller_post = diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml index cd4756666..ecc48ef1a 100644 --- a/infer/src/pulse/PulseDomain.ml +++ b/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 -> - F.fprintf fmt "`%a()`" Exp.pp call_exp - | `UnknownCall call_exp -> - F.fprintf fmt "unknown function `%a`" Exp.pp call_exp + | `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 -> diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli index 89c4fc4ef..7246742fa 100644 --- a/infer/src/pulse/PulseDomain.mli +++ b/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] diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 6f20c31f2..4e38d1651 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/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_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_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 `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::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::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 `()` (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::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::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 `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]