From b29d1a2f5faa6dc69cd46a4340e28c70630ee21b Mon Sep 17 00:00:00 2001 From: Dulma Churchill Date: Thu, 9 Apr 2020 02:52:35 -0700 Subject: [PATCH] [pulse] Adding new value history for allocations Reviewed By: jvillard Differential Revision: D20914622 fbshipit-source-id: f32836a95 --- infer/src/pulse/PulseDiagnostic.ml | 4 ++-- infer/src/pulse/PulseModels.ml | 22 ++++++++++--------- infer/src/pulse/PulseValueHistory.ml | 4 ++++ infer/src/pulse/PulseValueHistory.mli | 1 + infer/tests/codetoanalyze/c/pulse/issues.exp | 6 ++--- .../tests/codetoanalyze/cpp/pulse/issues.exp | 2 +- .../tests/codetoanalyze/objc/pulse/issues.exp | 4 ++-- 7 files changed, 25 insertions(+), 18 deletions(-) diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml index 70f227668..181381c98 100644 --- a/infer/src/pulse/PulseDiagnostic.ml +++ b/infer/src/pulse/PulseDiagnostic.ml @@ -113,8 +113,8 @@ let get_trace = function | MemoryLeak {location; allocation_trace} -> let access_start_location = Trace.get_start_location allocation_trace in add_errlog_header ~title:"allocation part of the trace starts here" access_start_location - @@ Trace.add_to_errlog ~nesting:0 - ~pp_immediate:(fun fmt -> F.pp_print_string fmt "allocation occurs here") + @@ Trace.add_to_errlog ~nesting:1 + ~pp_immediate:(fun fmt -> F.pp_print_string fmt "allocation part of the trace ends here") allocation_trace @@ [Errlog.make_trace_element 0 location "memory becomes unreachable here" []] | StackVariableAddressEscape {history; location; _} -> diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 7ec5b6e80..dc97707f7 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -97,21 +97,23 @@ module C = struct let malloc _ : model = fun ~caller_summary:_ ~callee_procname location ~ret:(ret_id, _) astate -> let ret_addr = AbstractValue.mk_fresh () in + let hist = + [ValueHistory.Allocation {f= Model (Procname.to_string callee_procname); location}] + in + let ret_value = (ret_addr, hist) in + let astate = PulseOperations.write_id ret_id ret_value astate in + let immediate_hist = Trace.Immediate {location; history= hist} in let astate_alloc = - PulseOperations.allocate callee_procname location (ret_addr, []) astate - |> PulseOperations.write_id ret_id (ret_addr, []) + PulseOperations.allocate callee_procname location ret_value astate |> AddressAttributes.add_one ret_addr (BoItv Itv.ItvPure.pos) - |> AddressAttributes.add_one ret_addr - (CItv (CItv.ge_to IntLit.one, Immediate {location; history= []})) + |> AddressAttributes.add_one ret_addr (CItv (CItv.ge_to IntLit.one, immediate_hist)) |> PulseExecutionState.continue in let+ astate_null = AddressAttributes.add_one ret_addr (BoItv (Itv.ItvPure.of_int_lit IntLit.zero)) astate - |> AddressAttributes.add_one ret_addr - (CItv (CItv.equal_to IntLit.zero, Immediate {location; history= []})) - |> PulseOperations.write_id ret_id (ret_addr, []) + |> AddressAttributes.add_one ret_addr (CItv (CItv.equal_to IntLit.zero, immediate_hist)) |> PulseOperations.invalidate location (Invalidation.ConstantDereference IntLit.zero) - (ret_addr, []) + ret_value in [astate_alloc; PulseExecutionState.ContinueProgram astate_null] end @@ -277,10 +279,10 @@ module ObjectiveC = struct let alloc _ : model = fun ~caller_summary:_ ~callee_procname location ~ret:(ret_id, _) astate -> let hist = - [ValueHistory.Call {f= Model (Procname.to_string callee_procname); location; in_call= []}] + [ValueHistory.Allocation {f= Model (Procname.to_string callee_procname); location}] in let ret_addr = AbstractValue.mk_fresh () in - let astate = PulseOperations.allocate callee_procname location (ret_addr, []) astate in + let astate = PulseOperations.allocate callee_procname location (ret_addr, hist) astate in PulseOperations.write_id ret_id (ret_addr, hist) astate |> PulseOperations.ok_continue end diff --git a/infer/src/pulse/PulseValueHistory.ml b/infer/src/pulse/PulseValueHistory.ml index 79c9c4e36..b149026c1 100644 --- a/infer/src/pulse/PulseValueHistory.ml +++ b/infer/src/pulse/PulseValueHistory.ml @@ -9,6 +9,7 @@ module F = Format module CallEvent = PulseCallEvent type event = + | Allocation of {f: CallEvent.t; location: Location.t} | Assignment of Location.t | Call of {f: CallEvent.t; location: Location.t; in_call: t} | Capture of {captured_as: Pvar.t; location: Location.t} @@ -30,6 +31,8 @@ let pp_event_no_location fmt event = F.pp_print_string fmt "assigned" | Call {f; location= _} -> F.fprintf fmt "passed as argument to %a" CallEvent.pp f + | Allocation {f} -> + F.fprintf fmt "allocated by call to %a" CallEvent.pp f | Capture {captured_as; location= _} -> F.fprintf fmt "value captured as `%a`" Pvar.pp_value_non_verbose captured_as | Conditional {is_then_branch; if_kind; location= _} -> @@ -50,6 +53,7 @@ let pp_event_no_location fmt event = let location_of_event = function + | Allocation {location} | Assignment location | Call {location} | Capture {location} diff --git a/infer/src/pulse/PulseValueHistory.mli b/infer/src/pulse/PulseValueHistory.mli index 07c937156..d685dbfad 100644 --- a/infer/src/pulse/PulseValueHistory.mli +++ b/infer/src/pulse/PulseValueHistory.mli @@ -9,6 +9,7 @@ module F = Format module CallEvent = PulseCallEvent type event = + | Allocation of {f: CallEvent.t; location: Location.t} | Assignment of Location.t | Call of {f: CallEvent.t; location: Location.t; in_call: t} | Capture of {captured_as: Pvar.t; location: Location.t} diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp index f4adfb381..7877269a5 100644 --- a/infer/tests/codetoanalyze/c/pulse/issues.exp +++ b/infer/tests/codetoanalyze/c/pulse/issues.exp @@ -1,3 +1,3 @@ -codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad, 0, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `create_p` here,allocation occurs here,memory becomes unreachable here] -codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad2, 4, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocation occurs here,memory becomes unreachable here] -codetoanalyze/c/pulse/memory_leak.c, malloc_no_free_bad, 0, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocation occurs here,memory becomes unreachable here] +codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad, 0, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `create_p` here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here] +codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad2, 4, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here] +codetoanalyze/c/pulse/memory_leak.c, malloc_no_free_bad, 0, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 7cdab3118..2524c1849 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -23,7 +23,7 @@ codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_ codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_then_write_bad,when calling `wraps_delete` here,parameter `x` of wraps_delete,when calling `wraps_delete_inner` here,parameter `x` of wraps_delete_inner,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_then_write_bad,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs 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,when calling `may_return_invalid_ptr_ok` here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `may_return_invalid_ptr_ok`,return from call to `may_return_invalid_ptr_ok`,assigned,when calling `call_store` here,parameter `y` of call_store,when calling `store` here,parameter `y` of store,invalid access occurs here] codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_bad,assigned,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_bad,assigned,assigned,assigned,invalid access occurs here] -codetoanalyze/cpp/pulse/memory_leak.cpp, constant_index_no_leak_FP, 3, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocation occurs here,memory becomes unreachable here] +codetoanalyze/cpp/pulse/memory_leak.cpp, constant_index_no_leak_FP, 3, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/cpp/pulse/nullptr.cpp, deref_nullptr_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/nullptr.cpp, no_check_return_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `may_return_nullptr` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `may_return_nullptr`,return from call to `may_return_nullptr`,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/nullptr.cpp, std_false_type_deref_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/objc/pulse/issues.exp b/infer/tests/codetoanalyze/objc/pulse/issues.exp index 314aa2bd3..fad4bd751 100644 --- a/infer/tests/codetoanalyze/objc/pulse/issues.exp +++ b/infer/tests/codetoanalyze/objc/pulse/issues.exp @@ -1,4 +1,4 @@ -codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks::cg_path_create_mutable_leak_bad:, 2, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocation occurs here,memory becomes unreachable here] -codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks::cg_path_create_with_rect_leak_bad, 3, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocation occurs here,memory becomes unreachable here] +codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks::cg_path_create_mutable_leak_bad:, 2, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CGPathCreateMutable` (modelled),allocation part of the trace ends here,memory becomes unreachable here] +codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks::cg_path_create_with_rect_leak_bad, 3, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `CGPathCreateWithRect` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/objc/pulse/use_after_free.m, PulseTest::use_after_free_simple_in_objc_method_bad:, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of PulseTest::use_after_free_simple_in_objc_method_bad:,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of PulseTest::use_after_free_simple_in_objc_method_bad:,invalid access occurs here] codetoanalyze/objc/pulse/use_after_free.m, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of use_after_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of use_after_free_simple_bad,invalid access occurs here]