From e99295e0e9c8e76c184444c1829aa51f31b8c515 Mon Sep 17 00:00:00 2001 From: Dulma Churchill Date: Thu, 19 Mar 2020 11:05:30 -0700 Subject: [PATCH] [pulse] Memory leak check Summary: First version of a new memory leak check based on Pulse. The idea is to examine unreachable cells in the heap and check that the "Allocated" attribute is available but the "Invalid CFree" isn't. This is done when we remove variables from the state. Currently it only works for malloc, we can extend it to other allocation functions later. Reviewed By: jvillard Differential Revision: D20444097 fbshipit-source-id: 33b6b25a2 --- infer/man/man1/infer-full.txt | 1 + infer/man/man1/infer-report.txt | 1 + infer/man/man1/infer.txt | 1 + infer/src/base/IssueType.ml | 2 ++ infer/src/base/IssueType.mli | 2 ++ infer/src/pulse/Pulse.ml | 3 +- infer/src/pulse/PulseAbductiveDomain.ml | 30 +++++++++++++++---- infer/src/pulse/PulseAbductiveDomain.mli | 7 +++-- infer/src/pulse/PulseBaseAddressAttributes.ml | 2 ++ .../src/pulse/PulseBaseAddressAttributes.mli | 2 ++ infer/src/pulse/PulseDiagnostic.ml | 26 +++++++++++++++- infer/src/pulse/PulseDiagnostic.mli | 1 + infer/src/pulse/PulseOperations.ml | 29 +++++++++++++++++- infer/src/pulse/PulseOperations.mli | 2 +- infer/tests/codetoanalyze/c/pulse/issues.exp | 3 ++ .../tests/codetoanalyze/c/pulse/memory_leak.c | 18 +++++++++-- 16 files changed, 115 insertions(+), 15 deletions(-) diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index cfafd9143..5795200a5 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -470,6 +470,7 @@ OPTIONS PRECONDITION_NOT_FOUND (enabled by default), PRECONDITION_NOT_MET (enabled by default), PREMATURE_NIL_TERMINATION_ARGUMENT (enabled by default), + PULSE_MEMORY_LEAK (disabled by default), PURE_FUNCTION (enabled by default), QUANDARY_TAINT_ERROR (enabled by default), REGISTERED_OBSERVER_BEING_DEALLOCATED (enabled by default), diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index fff901c66..63622fe92 100644 --- a/infer/man/man1/infer-report.txt +++ b/infer/man/man1/infer-report.txt @@ -201,6 +201,7 @@ OPTIONS PRECONDITION_NOT_FOUND (enabled by default), PRECONDITION_NOT_MET (enabled by default), PREMATURE_NIL_TERMINATION_ARGUMENT (enabled by default), + PULSE_MEMORY_LEAK (disabled by default), PURE_FUNCTION (enabled by default), QUANDARY_TAINT_ERROR (enabled by default), REGISTERED_OBSERVER_BEING_DEALLOCATED (enabled by default), diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 52d120802..50e9b761b 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -470,6 +470,7 @@ OPTIONS PRECONDITION_NOT_FOUND (enabled by default), PRECONDITION_NOT_MET (enabled by default), PREMATURE_NIL_TERMINATION_ARGUMENT (enabled by default), + PULSE_MEMORY_LEAK (disabled by default), PURE_FUNCTION (enabled by default), QUANDARY_TAINT_ERROR (enabled by default), REGISTERED_OBSERVER_BEING_DEALLOCATED (enabled by default), diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 09cdccba1..50502748b 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -406,6 +406,8 @@ let precondition_not_met = register_from_string "PRECONDITION_NOT_MET" let premature_nil_termination = register_from_string "PREMATURE_NIL_TERMINATION_ARGUMENT" +let pulse_memory_leak = register_from_string ~enabled:false "PULSE_MEMORY_LEAK" + let pure_function = register_from_string "PURE_FUNCTION" let quandary_taint_error = register_from_string "QUANDARY_TAINT_ERROR" diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index fa07e56e0..286dfb24d 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -264,6 +264,8 @@ val precondition_not_met : t val premature_nil_termination : t +val pulse_memory_leak : t + val pure_function : t val quandary_taint_error : t diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 81cc9ddcb..4059e2126 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -167,7 +167,8 @@ module PulseTransferFunctions = struct dispatch_call tenv summary ret call_exp actuals loc call_flags get_formals astate |> check_error summary | Metadata (ExitScope (vars, location)) -> - [PulseOperations.remove_vars vars location astate] + let astate = PulseOperations.remove_vars vars location astate in + [check_error summary astate] | Metadata (VariableLifetimeBegins (pvar, _, location)) -> [PulseOperations.realloc_pvar pvar location astate] | Metadata (Abstract _ | Nullify _ | Skip) -> diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 6b910a376..073ffdb56 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -27,6 +27,12 @@ module type BaseDomainSig = sig val filter_addr : f:(AbstractValue.t -> bool) -> t -> t (**filter both heap and attrs *) + val partition_addr : + f:(AbstractValue.t -> bool) + -> t + -> (BaseMemory.t * BaseAddressAttributes.t) * (BaseMemory.t * BaseAddressAttributes.t) + (**partition both heap and attrs *) + val pp : F.formatter -> t -> unit end @@ -54,6 +60,14 @@ module BaseDomainCommon = struct let heap' = BaseMemory.filter (fun address _ -> f address) foot.heap in let attrs' = BaseAddressAttributes.filter (fun address _ -> f address) foot.attrs in update ~heap:heap' ~attrs:attrs' foot + + + let partition_addr ~f foot = + let heap_yes, heap_no = BaseMemory.partition (fun address _ -> f address) foot.heap in + let attrs_yes, attrs_no = + BaseAddressAttributes.partition (fun address _ -> f address) foot.attrs + in + ((heap_yes, attrs_yes), (heap_no, attrs_no)) end (** represents the post abstract state at each program point *) @@ -324,11 +338,15 @@ let discard_unreachable ({pre; post} as astate) = in let post_addresses = BaseDomain.reachable_addresses (post :> BaseDomain.t) in let all_addresses = AbstractValue.Set.union pre_addresses post_addresses in - let post_new = - Domain.filter_addr ~f:(fun address -> AbstractValue.Set.mem address all_addresses) post + let (heap_new, attrs_new), (_, attrs_unreachable) = + Domain.partition_addr ~f:(fun address -> AbstractValue.Set.mem address all_addresses) post + in + let post_new = Domain.update ~heap:heap_new ~attrs:attrs_new post in + let astate = + if phys_equal pre_new pre && phys_equal post_new post then astate + else {astate with pre= pre_new; post= post_new} in - if phys_equal pre_new pre && phys_equal post_new post then astate - else {astate with pre= pre_new; post= post_new} + (astate, attrs_unreachable) let is_local var astate = not (Var.is_return var || Stack.is_abducible astate var) @@ -399,7 +417,9 @@ module PrePost = struct let of_post pdesc astate = - filter_for_summary astate |> discard_unreachable |> invalidate_locals pdesc + let domain = filter_for_summary astate in + let domain, _ = discard_unreachable domain in + invalidate_locals pdesc domain (* {2 machinery to apply a pre/post pair corresponding to a function's summary in a function call diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 1a5b0b666..9300b7f88 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -6,6 +6,7 @@ *) open! IStd open PulseBasicInterface +module BaseAddressAttributes = PulseBaseAddressAttributes module BaseDomain = PulseBaseDomain module BaseMemory = PulseBaseMemory module BaseStack = PulseBaseStack @@ -103,9 +104,9 @@ end module SkippedCalls : AbstractDomain.MapS with type key = Procname.t and type value = SkippedTrace.t -val discard_unreachable : t -> t -(** garbage collect unreachable addresses in the state to make it smaller, just for convenience and - keep its size down *) +val discard_unreachable : t -> t * BaseAddressAttributes.t +(** [discard_unreachable astate] garbage collects unreachable addresses in the state to make it + smaller, and retuns the new state and the attributes of discarded addresses *) val add_skipped_calls : Procname.t -> PulseTrace.t -> t -> t diff --git a/infer/src/pulse/PulseBaseAddressAttributes.ml b/infer/src/pulse/PulseBaseAddressAttributes.ml index 8f50e4aae..41f47c923 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.ml +++ b/infer/src/pulse/PulseBaseAddressAttributes.ml @@ -45,6 +45,8 @@ let empty = Graph.empty let filter = Graph.filter +let partition = Graph.partition + let pp = Graph.pp let invalidate (address, history) invalidation location memory = diff --git a/infer/src/pulse/PulseBaseAddressAttributes.mli b/infer/src/pulse/PulseBaseAddressAttributes.mli index 28ff6ef32..c2e8207c9 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.mli +++ b/infer/src/pulse/PulseBaseAddressAttributes.mli @@ -14,6 +14,8 @@ val empty : t val filter : (AbstractValue.t -> Attributes.t -> bool) -> t -> t +val partition : (AbstractValue.t -> Attributes.t -> bool) -> t -> t * t + val find_opt : AbstractValue.t -> t -> Attributes.t option val add_one : AbstractValue.t -> Attribute.t -> t -> t diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml index 724f827bc..307ead84a 100644 --- a/infer/src/pulse/PulseDiagnostic.ml +++ b/infer/src/pulse/PulseDiagnostic.ml @@ -15,12 +15,13 @@ module ValueHistory = PulseValueHistory type t = | AccessToInvalidAddress of {invalidation: Invalidation.t; invalidation_trace: Trace.t; access_trace: Trace.t} + | MemoryLeak of {allocation_trace: Trace.t; location: Location.t} | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t} let get_location = function | AccessToInvalidAddress {access_trace} -> Trace.get_outer_location access_trace - | StackVariableAddressEscape {location} -> + | MemoryLeak {location} | StackVariableAddressEscape {location} -> location @@ -66,6 +67,20 @@ let get_message = function F.asprintf "%a%a" pp_access_trace access_trace (pp_invalidation_trace invalidation_line invalidation) invalidation_trace + | MemoryLeak {location; allocation_trace} -> + let allocation_line = + let {Location.line; _} = Trace.get_outer_location allocation_trace in + line + in + let pp_allocation_trace fmt (trace : Trace.t) = + match trace with + | Immediate _ -> + F.fprintf fmt "by call to `malloc()`" + | ViaCall {f; _} -> + F.fprintf fmt "by call to %a" CallEvent.describe f + in + F.asprintf "memory dynamically allocated at line %d %a, is not reachable after %a" + allocation_line pp_allocation_trace allocation_trace Location.pp location | StackVariableAddressEscape {variable; _} -> let pp_var f var = if Var.is_cpp_temporary var then F.pp_print_string f "C++ temporary" @@ -95,6 +110,13 @@ let get_trace = function ~pp_immediate:(fun fmt -> F.pp_print_string fmt "invalid access occurs here") access_trace @@ [] + | MemoryLeak {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") + allocation_trace + @@ [] | StackVariableAddressEscape {history; location; _} -> ValueHistory.add_to_errlog ~nesting:0 history @@ @@ -105,5 +127,7 @@ let get_trace = function let get_issue_type = function | AccessToInvalidAddress {invalidation; _} -> Invalidation.issue_type_of_cause invalidation + | MemoryLeak _ -> + IssueType.pulse_memory_leak | StackVariableAddressEscape _ -> IssueType.stack_variable_address_escape diff --git a/infer/src/pulse/PulseDiagnostic.mli b/infer/src/pulse/PulseDiagnostic.mli index 3b94721d3..f07ffb7a5 100644 --- a/infer/src/pulse/PulseDiagnostic.mli +++ b/infer/src/pulse/PulseDiagnostic.mli @@ -14,6 +14,7 @@ module ValueHistory = PulseValueHistory type t = | AccessToInvalidAddress of {invalidation: Invalidation.t; invalidation_trace: Trace.t; access_trace: Trace.t} + | MemoryLeak of {allocation_trace: Trace.t; location: Location.t} | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t} val get_message : t -> string diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 2c043eeef..d9bcdff89 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -468,6 +468,29 @@ let mark_address_of_stack_variable history variable location address astate = AddressAttributes.add_one address (AddressOfStackVariable (variable, location, history)) astate +let check_memory_leak_unreachable unreachable_attrs location = + let check_memory_leak _ attributes result = + let allocated_not_freed_opt = + Attributes.fold attributes ~init:(None (* allocation trace *), false (* freed *)) + ~f:(fun acc attr -> + match (attr : Attribute.t) with + | Allocated trace -> + (Some trace, snd acc) + | Invalid (CFree, _) -> + (fst acc, true) + | _ -> + acc ) + in + match allocated_not_freed_opt with + | Some trace, false -> + (* allocated but not freed *) + Error (Diagnostic.MemoryLeak {location; allocation_trace= trace}) + | _ -> + result + in + PulseBaseAddressAttributes.fold check_memory_leak unreachable_attrs (Ok ()) + + let remove_vars vars location astate = let astate = List.fold vars ~init:astate ~f:(fun astate var -> @@ -485,7 +508,11 @@ let remove_vars vars location astate = astate ) in let astate' = Stack.remove_vars vars astate in - if phys_equal astate' astate then astate else AbductiveDomain.discard_unreachable astate' + if phys_equal astate' astate then Ok astate + else + let astate, unreachable_attrs = AbductiveDomain.discard_unreachable astate' in + let+ () = check_memory_leak_unreachable unreachable_attrs location in + astate let is_ptr_to_const formal_typ_opt = diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 2b9603265..b36e1e5d1 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -99,7 +99,7 @@ val shallow_copy : -> (t * (AbstractValue.t * ValueHistory.t)) access_result (** returns the address of a new cell with the same edges as the original *) -val remove_vars : Var.t list -> Location.t -> t -> t +val remove_vars : Var.t list -> Location.t -> t -> t access_result val check_address_escape : Location.t -> Procdesc.t -> AbstractValue.t -> ValueHistory.t -> t -> t access_result diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp index e69de29bb..92634d016 100644 --- a/infer/tests/codetoanalyze/c/pulse/issues.exp +++ b/infer/tests/codetoanalyze/c/pulse/issues.exp @@ -0,0 +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] +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] +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] diff --git a/infer/tests/codetoanalyze/c/pulse/memory_leak.c b/infer/tests/codetoanalyze/c/pulse/memory_leak.c index a93b6b0d6..5b430a8bf 100644 --- a/infer/tests/codetoanalyze/c/pulse/memory_leak.c +++ b/infer/tests/codetoanalyze/c/pulse/memory_leak.c @@ -6,9 +6,7 @@ */ #include -void malloc_no_free_bad() { // TODO implement the check - int* p = malloc(sizeof(p)); -} +void malloc_no_free_bad() { int* p = malloc(sizeof(p)); } int* malloc_returned_ok() { int* p = malloc(sizeof(p)); @@ -20,3 +18,17 @@ void malloc_then_free_ok() { *p = 5; free(p); } + +int* create_p() { + int* p = malloc(sizeof(p)); + return p; +} + +void malloc_interproc_no_free_bad() { int* p = create_p(); } + +void malloc_interproc_no_free_bad2() { + int* p = malloc(sizeof(p)); + int z = 3; + int y = 4; + int* q = p; +}