From 2f90b05c2a79545a8b18f2a7b698a4745c178fa9 Mon Sep 17 00:00:00 2001 From: Dulma Churchill Date: Wed, 11 Mar 2020 03:44:31 -0700 Subject: [PATCH] [pulse] Add model for malloc Summary: Adding a model for malloc: we add an attribute "Allocated". This can be used for implementing memory leaks: whenever the variables get out of scope, we can check that if the variable has an attribute Allocated, it also has an attribute Invalid CFree. Possibly we will need more details in the Allocated attribute, to know if it's malloc, or other allocation function, but we can add that later when we know how it should look like. Reviewed By: jvillard Differential Revision: D20364541 fbshipit-source-id: 5e667a8c3 --- Makefile | 1 + infer/src/pulse/PulseAbductiveDomain.ml | 7 ++++++ infer/src/pulse/PulseAbductiveDomain.mli | 2 ++ infer/src/pulse/PulseAttribute.ml | 4 ++++ infer/src/pulse/PulseAttribute.mli | 1 + infer/src/pulse/PulseBaseAddressAttributes.ml | 4 ++++ .../src/pulse/PulseBaseAddressAttributes.mli | 2 ++ infer/src/pulse/PulseModels.ml | 7 ++++++ infer/src/pulse/PulseOperations.ml | 2 ++ infer/src/pulse/PulseOperations.mli | 2 ++ infer/tests/codetoanalyze/c/pulse/Makefile | 15 +++++++++++++ infer/tests/codetoanalyze/c/pulse/issues.exp | 0 .../tests/codetoanalyze/c/pulse/memory_leak.c | 22 +++++++++++++++++++ 13 files changed, 69 insertions(+) create mode 100644 infer/tests/codetoanalyze/c/pulse/Makefile create mode 100644 infer/tests/codetoanalyze/c/pulse/issues.exp create mode 100644 infer/tests/codetoanalyze/c/pulse/memory_leak.c diff --git a/Makefile b/Makefile index dbf28927e..ee74af76d 100644 --- a/Makefile +++ b/Makefile @@ -55,6 +55,7 @@ DIRECT_TESTS += \ c_errors \ c_frontend \ c_performance \ + c_pulse \ c_purity \ c_uninit \ cpp_annotation-reachability \ diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 77b7a678f..d3446d458 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -203,6 +203,10 @@ module AddressAttributes = struct map_post_attrs astate ~f:(BaseAddressAttributes.invalidate address invalidation location) + let allocate address location astate = + map_post_attrs astate ~f:(BaseAddressAttributes.allocate address location) + + let add_one address attributes astate = map_post_attrs astate ~f:(BaseAddressAttributes.add_one address attributes) @@ -662,6 +666,7 @@ module PrePost = struct ) | AddressOfCppTemporary _ | AddressOfStackVariable _ + | Allocated _ | Closure _ | Invalid _ | MustBeValid _ @@ -681,6 +686,8 @@ module PrePost = struct | Arithmetic (arith, trace) -> Attribute.Arithmetic (arith, add_call_to_trace proc_name call_location caller_history trace) + | Allocated trace -> + Attribute.Allocated (add_call_to_trace proc_name call_location caller_history trace) | AddressOfCppTemporary _ | AddressOfStackVariable _ | BoItv _ diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 0ec3674b3..0f985d8f5 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -76,6 +76,8 @@ module AddressAttributes : sig val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t + val allocate : AbstractValue.t * ValueHistory.t -> Location.t -> t -> t + val get_closure_proc_name : AbstractValue.t -> t -> Procname.t option val is_std_vector_reserved : AbstractValue.t -> t -> bool diff --git a/infer/src/pulse/PulseAttribute.ml b/infer/src/pulse/PulseAttribute.ml index 5fb510ec1..adf8415de 100644 --- a/infer/src/pulse/PulseAttribute.ml +++ b/infer/src/pulse/PulseAttribute.ml @@ -28,6 +28,7 @@ module Attribute = struct type t = | AddressOfCppTemporary of Var.t * ValueHistory.t | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t + | Allocated of Trace.t | Arithmetic of Arithmetic.t * Trace.t | BoItv of Itv.ItvPure.t | Closure of Procname.t @@ -75,6 +76,8 @@ module Attribute = struct F.fprintf f "t&%a (%a)" Var.pp var ValueHistory.pp history | AddressOfStackVariable (var, location, history) -> F.fprintf f "s&%a (%a) at %a" Var.pp var ValueHistory.pp history Location.pp location + | Allocated trace -> + F.fprintf f "Allocated %a" (Trace.pp ~pp_immediate:(pp_string_if_debug "allocation")) trace | BoItv bo_itv -> F.fprintf f "BoItv (%a)" Itv.ItvPure.pp bo_itv | Closure pname -> @@ -164,6 +167,7 @@ let is_suitable_for_pre = function true | AddressOfCppTemporary _ | AddressOfStackVariable _ + | Allocated _ | Closure _ | Invalid _ | StdVectorReserve diff --git a/infer/src/pulse/PulseAttribute.mli b/infer/src/pulse/PulseAttribute.mli index dd8c8d6f8..6a56ad007 100644 --- a/infer/src/pulse/PulseAttribute.mli +++ b/infer/src/pulse/PulseAttribute.mli @@ -14,6 +14,7 @@ module ValueHistory = PulseValueHistory type t = | AddressOfCppTemporary of Var.t * ValueHistory.t | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t + | Allocated of Trace.t | Arithmetic of Arithmetic.t * Trace.t | BoItv of Itv.ItvPure.t | Closure of Procname.t diff --git a/infer/src/pulse/PulseBaseAddressAttributes.ml b/infer/src/pulse/PulseBaseAddressAttributes.ml index d0c0f8538..67fb3b83e 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.ml +++ b/infer/src/pulse/PulseBaseAddressAttributes.ml @@ -51,6 +51,10 @@ let invalidate (address, history) invalidation location memory = add_one address (Attribute.Invalid (invalidation, Immediate {location; history})) memory +let allocate (address, history) location memory = + add_one address (Attribute.Allocated (Immediate {location; history})) memory + + let check_valid address attrs = L.d_printfln "Checking validity of %a" AbstractValue.pp address ; match Graph.find_opt address attrs |> Option.bind ~f:Attributes.get_invalid with diff --git a/infer/src/pulse/PulseBaseAddressAttributes.mli b/infer/src/pulse/PulseBaseAddressAttributes.mli index 140e4fd6a..a510ac6ed 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.mli +++ b/infer/src/pulse/PulseBaseAddressAttributes.mli @@ -20,6 +20,8 @@ val add_one : AbstractValue.t -> Attribute.t -> t -> t val add : AbstractValue.t -> Attributes.t -> t -> t +val allocate : AbstractValue.t * ValueHistory.t -> Location.t -> t -> t + val fold : (AbstractValue.t -> Attributes.t -> 'a -> 'a) -> t -> 'a -> 'a val check_valid : AbstractValue.t -> t -> (unit, Invalidation.t * Trace.t) result diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 654761212..7e904bc50 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -87,6 +87,12 @@ module C = struct else let+ astate = PulseOperations.invalidate location Invalidation.CFree deleted_access astate in [astate] + + + let malloc access : model = + fun ~caller_summary:_ location ~ret:(ret_id, _) astate -> + let astate = PulseOperations.allocate location access astate in + Ok [PulseOperations.write_id ret_id access astate] end module Cplusplus = struct @@ -397,6 +403,7 @@ module ProcNameDispatcher = struct let pushback_modeled = StringSet.of_list ["add"; "put"; "addAll"; "putAll"; "remove"] in make_dispatcher [ +match_builtin BuiltinDecl.free <>$ capt_arg_payload $--> C.free + ; +match_builtin BuiltinDecl.malloc <>$ capt_arg_payload $--> C.malloc ; +match_builtin BuiltinDecl.__delete <>$ capt_arg_payload $--> Cplusplus.delete ; +match_builtin BuiltinDecl.__placement_new &++> Cplusplus.placement_new ; +match_builtin BuiltinDecl.objc_cpp_throw <>--> Misc.early_exit diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 86baa234e..5bfeace1f 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -376,6 +376,8 @@ let havoc_field location addr_trace field trace_obj astate = write_field location addr_trace field (AbstractValue.mk_fresh (), trace_obj) astate +let allocate location addr_trace astate = AddressAttributes.allocate addr_trace location astate + let invalidate location cause addr_trace astate = check_addr_access location addr_trace astate >>| AddressAttributes.invalidate addr_trace cause location diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index f2e827a48..2b9603265 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -82,6 +82,8 @@ val invalidate : Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result (** record that the address is invalid *) +val allocate : Location.t -> AbstractValue.t * ValueHistory.t -> t -> t + val invalidate_deref : Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result (** record that what the address points to is invalid *) diff --git a/infer/tests/codetoanalyze/c/pulse/Makefile b/infer/tests/codetoanalyze/c/pulse/Makefile new file mode 100644 index 000000000..4b936314b --- /dev/null +++ b/infer/tests/codetoanalyze/c/pulse/Makefile @@ -0,0 +1,15 @@ +# Copyright (c) Facebook, Inc. and its affiliates. +# +# This source code is licensed under the MIT license found in the +# LICENSE file in the root directory of this source tree. + +TESTS_DIR = ../../.. + +CLANG_OPTIONS = -c +INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR) + +INFERPRINT_OPTIONS = --issues-tests + +SOURCES = $(wildcard *.c) + +include $(TESTS_DIR)/clang.make diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp new file mode 100644 index 000000000..e69de29bb diff --git a/infer/tests/codetoanalyze/c/pulse/memory_leak.c b/infer/tests/codetoanalyze/c/pulse/memory_leak.c new file mode 100644 index 000000000..a93b6b0d6 --- /dev/null +++ b/infer/tests/codetoanalyze/c/pulse/memory_leak.c @@ -0,0 +1,22 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +#include + +void malloc_no_free_bad() { // TODO implement the check + int* p = malloc(sizeof(p)); +} + +int* malloc_returned_ok() { + int* p = malloc(sizeof(p)); + return p; +} + +void malloc_then_free_ok() { + int* p = malloc(sizeof(p)); + *p = 5; + free(p); +}