From 0cbe2f9b089a71d0b60938d07d990cc939cffb30 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 8 Dec 2020 10:35:38 -0800 Subject: [PATCH] [pulse] Uninitialized value check in pulse Summary: This diff adds uninitialized value check in pulse. For now, it supports only simple cases, - declared variables with a type of integer, float, void, and pointer - malloced pointer variables that points to integer, float, void, and pointer TODOs: I will add more cases in the following diffs. - declared/malloced array - declared/malloced struct - inter-procedural checking Reviewed By: jvillard Differential Revision: D25269073 fbshipit-source-id: 317df9a85 --- 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 | 5 + infer/src/base/IssueType.mli | 2 + .../src/bufferoverrun/bufferOverrunModels.ml | 23 +-- .../src/bufferoverrun/bufferOverrunModels.mli | 8 + infer/src/pulse/Pulse.ml | 31 +++- infer/src/pulse/PulseAbductiveDomain.ml | 66 ++++++- infer/src/pulse/PulseAbductiveDomain.mli | 16 ++ infer/src/pulse/PulseAttribute.ml | 17 ++ infer/src/pulse/PulseAttribute.mli | 3 + infer/src/pulse/PulseBaseAddressAttributes.ml | 17 ++ .../src/pulse/PulseBaseAddressAttributes.mli | 4 + infer/src/pulse/PulseBaseDomain.ml | 59 +++++-- infer/src/pulse/PulseBaseDomain.mli | 3 + infer/src/pulse/PulseInvalidation.ml | 7 + infer/src/pulse/PulseInvalidation.mli | 1 + infer/src/pulse/PulseModels.ml | 163 +++++++++++------- infer/src/pulse/PulseOperations.ml | 99 +++++++---- infer/src/pulse/PulseOperations.mli | 19 +- infer/tests/codetoanalyze/c/pulse/issues.exp | 4 + infer/tests/codetoanalyze/c/pulse/uninit.c | 85 +++++++++ .../tests/codetoanalyze/cpp/pulse/basics.cpp | 6 +- .../tests/codetoanalyze/objc/pulse/issues.exp | 1 + infer/tests/codetoanalyze/objc/pulse/uninit.m | 43 +++++ 26 files changed, 540 insertions(+), 145 deletions(-) create mode 100644 infer/tests/codetoanalyze/c/pulse/uninit.c create mode 100644 infer/tests/codetoanalyze/objc/pulse/uninit.m diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 52c4451a2..2d3fec0e0 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -502,6 +502,7 @@ OPTIONS PRECONDITION_NOT_FOUND (enabled by default), PRECONDITION_NOT_MET (enabled by default), PREMATURE_NIL_TERMINATION_ARGUMENT (enabled by default), + PULSE_UNINITIALIZED_VALUE (disabled by default), PURE_FUNCTION (enabled by default), QUANDARY_TAINT_ERROR (enabled by default), RESOURCE_LEAK (enabled by default), diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index 8aeb46757..3e9e88d61 100644 --- a/infer/man/man1/infer-report.txt +++ b/infer/man/man1/infer-report.txt @@ -210,6 +210,7 @@ OPTIONS PRECONDITION_NOT_FOUND (enabled by default), PRECONDITION_NOT_MET (enabled by default), PREMATURE_NIL_TERMINATION_ARGUMENT (enabled by default), + PULSE_UNINITIALIZED_VALUE (disabled by default), PURE_FUNCTION (enabled by default), QUANDARY_TAINT_ERROR (enabled by default), RESOURCE_LEAK (enabled by default), diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 1478c3ac7..d37f07295 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -502,6 +502,7 @@ OPTIONS PRECONDITION_NOT_FOUND (enabled by default), PRECONDITION_NOT_MET (enabled by default), PREMATURE_NIL_TERMINATION_ARGUMENT (enabled by default), + PULSE_UNINITIALIZED_VALUE (disabled by default), PURE_FUNCTION (enabled by default), QUANDARY_TAINT_ERROR (enabled by default), RESOURCE_LEAK (enabled by default), diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 20878f76f..58efea28d 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -900,6 +900,11 @@ let uninitialized_value = ~user_documentation:[%blob "../../documentation/issues/UNINITIALIZED_VALUE.md"] +let uninitialized_value_pulse = + register ~enabled:false ~id:"PULSE_UNINITIALIZED_VALUE" Error Pulse ~hum:"Unitialized Value" + ~user_documentation:"See [UNITIALIZED_VALUE](#uninitialized_value). Re-implemented using Pulse." + + let unreachable_code_after = register ~id:"UNREACHABLE_CODE" Error BufferOverrunChecker ~user_documentation:"A program point is unreachable." diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 2eefdcb35..ec10ff64b 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -320,6 +320,8 @@ val topl_pulse_error : t val uninitialized_value : t +val uninitialized_value_pulse : t + val unreachable_code_after : t val use_after_delete : t diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 9c1f3385c..0fb30b44e 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -58,22 +58,23 @@ let eval_binop ~f e1 e2 = {exec; check= no_check} -(* It returns a tuple of: - - type of array element - - stride of the type - - array size - - flexible array size *) -let get_malloc_info : Exp.t -> Typ.t * Int.t option * Exp.t * Exp.t option = function +let get_malloc_info_opt = function | Exp.BinOp (Binop.Mult _, Exp.Sizeof {typ; nbytes}, length) | Exp.BinOp (Binop.Mult _, length, Exp.Sizeof {typ; nbytes}) -> - (typ, nbytes, length, None) + Some (typ, nbytes, length, None) (* In Java all arrays are dynamically allocated *) | Exp.Sizeof {typ; nbytes; dynamic_length= Some arr_length} when Language.curr_language_is Java -> - (typ, nbytes, arr_length, Some arr_length) + Some (typ, nbytes, arr_length, Some arr_length) | Exp.Sizeof {typ; nbytes; dynamic_length} -> - (typ, nbytes, Exp.one, dynamic_length) - | x -> - (Typ.mk (Typ.Tint Typ.IChar), Some 1, x, None) + Some (typ, nbytes, Exp.one, dynamic_length) + | _ -> + None + + +let get_malloc_info : Exp.t -> Typ.t * Int.t option * Exp.t * Exp.t option = + fun x -> + get_malloc_info_opt x + |> IOption.if_none_eval ~f:(fun () -> (Typ.mk (Typ.Tint Typ.IChar), Some 1, x, None)) let check_alloc_size ~can_be_zero size_exp {location; integer_type_widths} mem cond_set = diff --git a/infer/src/bufferoverrun/bufferOverrunModels.mli b/infer/src/bufferoverrun/bufferOverrunModels.mli index 397726234..963591ddf 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.mli +++ b/infer/src/bufferoverrun/bufferOverrunModels.mli @@ -70,3 +70,11 @@ end module Call : sig val dispatch : (Tenv.t, model, unit) ProcnameDispatcher.Call.dispatcher end + +val get_malloc_info_opt : Exp.t -> (Typ.t * Int.t option * Exp.t * Exp.t option) option +(** Return a tuple of malloc information with heuristics: + + - type of array element + - stride of the type + - array size + - flexible array size *) diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index ea16f52ad..a6a451166 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -94,7 +94,9 @@ module PulseTransferFunctions = struct match (exec_state : ExecutionDomain.t) with | ContinueProgram astate -> let gone_out_of_scope = Invalidation.GoneOutOfScope (pvar, typ) in - let* astate, out_of_scope_base = PulseOperations.eval call_loc (Exp.Lvar pvar) astate in + let* astate, out_of_scope_base = + PulseOperations.eval NoAccess call_loc (Exp.Lvar pvar) astate + in (* invalidate [&x] *) PulseOperations.invalidate call_loc gone_out_of_scope out_of_scope_base astate >>| ExecutionDomain.continue @@ -126,8 +128,8 @@ module PulseTransferFunctions = struct match (lhs : Exp.t) with | Lindex (arr, index) -> (let open IResult.Let_syntax in - let* _astate, (aw_array, _history) = PulseOperations.eval loc arr astate in - let+ _astate, (aw_index, _history) = PulseOperations.eval loc index astate in + let* _astate, (aw_array, _history) = PulseOperations.eval Read loc arr astate in + let+ _astate, (aw_index, _history) = PulseOperations.eval Read loc index astate in let topl_event = PulseTopl.ArrayWrite {aw_array; aw_index} in AbductiveDomain.Topl.small_step loc topl_event astate) |> Result.ok (* don't emit Topl event if evals fail *) |> Option.value ~default:astate @@ -135,19 +137,30 @@ module PulseTransferFunctions = struct astate + (* NOTE: At the moment, it conservatively assumes that all reachable addresses from function + arguments are initialized by callee. *) + let conservatively_initialize_args func_args ({AbductiveDomain.post} as astate) = + let arg_values = + List.map func_args ~f:(fun {ProcnameDispatcher.Call.FuncArg.arg_payload= value, _} -> value) + in + let reachable_values = BaseDomain.reachable_addresses_from arg_values (post :> BaseDomain.t) in + AbstractValue.Set.fold AbductiveDomain.initialize reachable_values astate + + let dispatch_call ({InterproceduralAnalysis.tenv} as analysis_data) ret call_exp actuals call_loc flags astate = (* evaluate all actuals *) let* astate, rev_func_args = List.fold_result actuals ~init:(astate, []) ~f:(fun (astate, rev_func_args) (actual_exp, actual_typ) -> - let+ astate, actual_evaled = PulseOperations.eval call_loc actual_exp astate in + let+ astate, actual_evaled = PulseOperations.eval Read call_loc actual_exp astate in ( astate , ProcnameDispatcher.Call.FuncArg. {exp= actual_exp; arg_payload= actual_evaled; typ= actual_typ} :: rev_func_args ) ) in let func_args = List.rev rev_func_args in + let astate = conservatively_initialize_args func_args astate in let callee_pname = proc_name_of_call call_exp in let model = match callee_pname with @@ -278,8 +291,10 @@ module PulseTransferFunctions = struct (* [*lhs_exp := rhs_exp] *) let event = ValueHistory.Assignment loc in let result = - let* astate, (rhs_addr, rhs_history) = PulseOperations.eval loc rhs_exp astate in - let* astate, lhs_addr_hist = PulseOperations.eval loc lhs_exp astate in + let* astate, (rhs_addr, rhs_history) = + PulseOperations.eval NoAccess loc rhs_exp astate + in + let* astate, lhs_addr_hist = PulseOperations.eval Write loc lhs_exp astate in let* astate = PulseOperations.write_deref loc ~ref:lhs_addr_hist ~obj:(rhs_addr, event :: rhs_history) @@ -339,8 +354,8 @@ module PulseTransferFunctions = struct if List.is_empty ret_vars then vars else List.rev_append vars ret_vars in remove_vars vars_to_remove astates - | Metadata (VariableLifetimeBegins (pvar, _, location)) when not (Pvar.is_global pvar) -> - [PulseOperations.realloc_pvar pvar location astate |> Domain.continue] + | Metadata (VariableLifetimeBegins (pvar, typ, location)) when not (Pvar.is_global pvar) -> + [PulseOperations.realloc_pvar pvar typ location astate |> Domain.continue] | Metadata (Abstract _ | VariableLifetimeBegins _ | Nullify _ | Skip) -> [Domain.ContinueProgram astate] ) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index efb8a24f4..42578cad9 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -42,7 +42,11 @@ type base_domain = BaseDomain.t = {heap: BaseMemory.t; stack: BaseStack.t; attrs: BaseAddressAttributes.t} (** represents the post abstract state at each program point *) -module PostDomain : BaseDomainSig = struct +module PostDomain : sig + include BaseDomainSig + + val initialize : AbstractValue.t -> t -> t +end = struct include BaseDomain let update ?stack ?heap ?attrs foot = @@ -70,6 +74,11 @@ module PostDomain : BaseDomainSig = struct BaseAddressAttributes.filter_with_discarded_addrs (fun address _ -> f address) foot.attrs in (update ~heap:heap' ~attrs:attrs' foot, discarded_addresses) + + + let initialize address x = + let attrs = BaseAddressAttributes.initialize address x.attrs in + update ~attrs x end (* NOTE: [PreDomain] and [Domain] theoretically differ in that [PreDomain] should be the inverted lattice of [Domain], but since we never actually join states or check implication the two collapse into one. *) @@ -193,6 +202,11 @@ module AddressAttributes = struct abduce_attribute addr (MustBeValid access_trace) astate + let check_initialized addr astate = + let+ () = BaseAddressAttributes.check_initialized addr (astate.post :> base_domain).attrs in + () + + (** [astate] with [astate.post.attrs = f astate.post.attrs] *) let map_post_attrs ~f astate = let new_post = PostDomain.update astate.post ~attrs:(f (astate.post :> base_domain).attrs) in @@ -299,12 +313,51 @@ module Memory = struct let find_opt address astate = BaseMemory.find_opt address (astate.post :> base_domain).heap end +let set_uninitialized_post src typ location (post : PostDomain.t) = + match typ.Typ.desc with + | Tint _ | Tfloat _ | Tptr _ -> + let {stack; attrs} = (post :> base_domain) in + let stack, addr, history = + match src with + | `LocalDecl (pvar, addr_opt) -> + let history = [ValueHistory.VariableDeclared (pvar, location)] in + let stack, addr = + match addr_opt with + | None -> + let addr = AbstractValue.mk_fresh () in + (BaseStack.add (Var.of_pvar pvar) (addr, history) stack, addr) + | Some addr -> + (stack, addr) + in + (stack, addr, history) + | `Malloc (addr, history) -> + (stack, addr, history) + in + let attrs = + BaseAddressAttributes.add_one addr (Uninitialized (Immediate {location; history})) attrs + in + PostDomain.update ~stack ~attrs post + | Tstruct _ -> + (* TODO: set uninitialized attributes for fields *) + post + | Tarray _ -> + (* TODO: set uninitialized attributes for elements *) + post + | Tvoid | Tfun | TVar _ -> + (* We ignore tricky types to mark uninitialized addresses. *) + post + + +let set_uninitialized src typ location x = + {x with post= set_uninitialized_post src typ location x.post} + + let mk_initial proc_desc = (* HACK: save the formals in the stacks of the pre and the post to remember which local variables correspond to formals *) + let proc_name = Procdesc.get_proc_name proc_desc in + let location = Procdesc.get_loc proc_desc in let formals_and_captured = - let proc_name = Procdesc.get_proc_name proc_desc in - let location = Procdesc.get_loc proc_desc in let init_var mangled = let pvar = Pvar.mk mangled proc_name in (Var.of_pvar pvar, (AbstractValue.mk_fresh (), [ValueHistory.FormalDeclared (pvar, location)])) @@ -328,7 +381,12 @@ let mk_initial proc_desc = in PreDomain.update ~stack:initial_stack ~heap:initial_heap PreDomain.empty in + let locals = Procdesc.get_locals proc_desc in let post = PostDomain.update ~stack:initial_stack PostDomain.empty in + let post = + List.fold locals ~init:post ~f:(fun (acc : PostDomain.t) {ProcAttributes.name; typ} -> + set_uninitialized_post (`LocalDecl (Pvar.mk name proc_name, None)) typ location acc ) + in { pre ; post ; topl= PulseTopl.start () @@ -519,6 +577,8 @@ let get_pre {pre} = (pre :> BaseDomain.t) let get_post {post} = (post :> BaseDomain.t) +let initialize address x = {x with post= PostDomain.initialize address x.post} + (* re-exported for mli *) let incorporate_new_eqs astate (phi, new_eqs) = if PathCondition.is_unsat_cheap phi then phi diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index a2ff20e3d..c35684fad 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -126,6 +126,8 @@ module AddressAttributes : sig val check_valid : Trace.t -> AbstractValue.t -> t -> (t, Invalidation.t * Trace.t) result + val check_initialized : AbstractValue.t -> t -> (unit, Trace.t) result + val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t val allocate : Procname.t -> AbstractValue.t * ValueHistory.t -> Location.t -> t -> t @@ -180,6 +182,20 @@ val incorporate_new_eqs : t -> PathCondition.t * PathCondition.new_eqs -> PathCo and [y] being allocated separately. In those cases, the resulting path condition is {!PathCondition.false_}. *) +val initialize : AbstractValue.t -> t -> t +(** Remove "Uninitialized" attribute of the given address *) + +val set_uninitialized : + [ `LocalDecl of Pvar.t * AbstractValue.t option + (** the second optional parameter is for the address of the variable *) + | `Malloc of AbstractValue.t * ValueHistory.t + (** the address parameter is a newly allocated address *) ] + -> Typ.t + -> Location.t + -> t + -> t +(** Add "Uninitialized" attributes when a variable is declared or a memory is allocated by malloc. *) + module Topl : sig val small_step : Location.t -> PulseTopl.event -> t -> t diff --git a/infer/src/pulse/PulseAttribute.ml b/infer/src/pulse/PulseAttribute.ml index 14e384671..a258e7064 100644 --- a/infer/src/pulse/PulseAttribute.ml +++ b/infer/src/pulse/PulseAttribute.ml @@ -34,6 +34,7 @@ module Attribute = struct | Invalid of Invalidation.t * Trace.t | MustBeValid of Trace.t | StdVectorReserve + | Uninitialized of Trace.t | WrittenTo of Trace.t [@@deriving compare, variants] @@ -70,6 +71,8 @@ module Attribute = struct let end_of_collection_rank = Variants.to_rank EndOfCollection + let uninitialized_rank = Variants.to_rank (Uninitialized dummy_trace) + let pp f attribute = let pp_string_if_debug string fmt = if Config.debug_level_analysis >= 3 then F.pp_print_string fmt string @@ -98,6 +101,10 @@ module Attribute = struct F.fprintf f "MustBeValid %a" (Trace.pp ~pp_immediate:(pp_string_if_debug "access")) trace | StdVectorReserve -> F.pp_print_string f "std::vector::reserve()" + | Uninitialized trace -> + F.fprintf f "Uninitialized %a" + (Trace.pp ~pp_immediate:(pp_string_if_debug "declaration")) + trace | WrittenTo trace -> F.fprintf f "WrittenTo %a" (Trace.pp ~pp_immediate:(pp_string_if_debug "mutation")) trace end @@ -167,6 +174,13 @@ module Attributes = struct typ ) + let get_uninitialized attrs = + Set.find_rank attrs Attribute.uninitialized_rank + |> Option.map ~f:(fun attr -> + let[@warning "-8"] (Attribute.Uninitialized trace) = attr in + trace ) + + include Set end @@ -183,6 +197,7 @@ let is_suitable_for_pre = function | EndOfCollection | Invalid _ | StdVectorReserve + | Uninitialized _ | WrittenTo _ -> false @@ -194,6 +209,8 @@ let map_trace ~f = function Invalid (invalidation, f trace) | MustBeValid trace -> MustBeValid (f trace) + | Uninitialized trace -> + Uninitialized (f trace) | WrittenTo trace -> WrittenTo (f trace) | ( AddressOfCppTemporary _ diff --git a/infer/src/pulse/PulseAttribute.mli b/infer/src/pulse/PulseAttribute.mli index 87998f2b6..df4715635 100644 --- a/infer/src/pulse/PulseAttribute.mli +++ b/infer/src/pulse/PulseAttribute.mli @@ -21,6 +21,7 @@ type t = | Invalid of Invalidation.t * Trace.t | MustBeValid of Trace.t | StdVectorReserve + | Uninitialized of Trace.t | WrittenTo of Trace.t [@@deriving compare] @@ -53,4 +54,6 @@ module Attributes : sig val is_modified : t -> bool val is_std_vector_reserved : t -> bool + + val get_uninitialized : t -> Trace.t option end diff --git a/infer/src/pulse/PulseBaseAddressAttributes.ml b/infer/src/pulse/PulseBaseAddressAttributes.ml index 78d1e5610..8adc58335 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.ml +++ b/infer/src/pulse/PulseBaseAddressAttributes.ml @@ -85,6 +85,15 @@ let check_valid address attrs = Error invalidation +let check_initialized address attrs = + L.d_printfln "Checking if %a is initialized" AbstractValue.pp address ; + match Graph.find_opt address attrs |> Option.bind ~f:Attributes.get_uninitialized with + | Some trace -> + Error trace + | None -> + Ok () + + let get_attribute getter address attrs = let open Option.Monad_infix in Graph.find_opt address attrs >>= getter @@ -98,6 +107,14 @@ let remove_allocation_attr address memory = memory +let initialize address attrs = + match get_attribute Attributes.get_uninitialized address attrs with + | Some trace -> + remove_one address (Attribute.Uninitialized trace) attrs + | None -> + attrs + + let get_closure_proc_name = get_attribute Attributes.get_closure_proc_name let get_must_be_valid = get_attribute Attributes.get_must_be_valid diff --git a/infer/src/pulse/PulseBaseAddressAttributes.mli b/infer/src/pulse/PulseBaseAddressAttributes.mli index eeff97a8c..e040d3b9c 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.mli +++ b/infer/src/pulse/PulseBaseAddressAttributes.mli @@ -31,6 +31,8 @@ val fold : (AbstractValue.t -> Attributes.t -> 'a -> 'a) -> t -> 'a -> 'a val check_valid : AbstractValue.t -> t -> (unit, Invalidation.t * Trace.t) result +val check_initialized : AbstractValue.t -> t -> (unit, Trace.t) result + val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t val get_closure_proc_name : AbstractValue.t -> t -> Procname.t option @@ -48,3 +50,5 @@ val is_end_of_collection : AbstractValue.t -> t -> bool val pp : F.formatter -> t -> unit val remove_allocation_attr : AbstractValue.t -> t -> t + +val initialize : AbstractValue.t -> t -> t diff --git a/infer/src/pulse/PulseBaseDomain.ml b/infer/src/pulse/PulseBaseDomain.ml index c854f2ea3..1782f1a41 100644 --- a/infer/src/pulse/PulseBaseDomain.ml +++ b/infer/src/pulse/PulseBaseDomain.ml @@ -190,9 +190,9 @@ module GraphVisit : sig -> t -> init:'accum -> f: - ( 'accum + ( Var.t + -> 'accum -> AbstractValue.t - -> Var.t -> Memory.Access.t list -> ('accum, 'final) Base.Continue_or_stop.t) -> finish:('accum -> 'final) @@ -202,6 +202,19 @@ module GraphVisit : sig set of addresses that have been visited before [f] returned [Stop] or all reachable addresses were seen. [f] is passed each address together with the variable from which the address was reached and the access path from that variable to the address. *) + + val fold_from_addresses : + AbstractValue.t list + -> t + -> init:'accum + -> f: + ( 'accum + -> AbstractValue.t + -> Memory.Access.t list + -> ('accum, 'final) Base.Continue_or_stop.t) + -> finish:('accum -> 'final) + -> AbstractValue.Set.t * 'final + (** Similar to [fold], but start from given addresses, instead of stack variables. *) end = struct open Base.Continue_or_stop @@ -212,41 +225,53 @@ end = struct `NotAlreadyVisited visited - let rec visit_address orig_var ~f rev_accesses astate address ((visited, accum) as visited_accum) - = + let rec visit_address address ~f rev_accesses astate ((visited, accum) as visited_accum) = match visit address visited with | `AlreadyVisited -> Continue visited_accum | `NotAlreadyVisited visited -> ( - match f accum address orig_var rev_accesses with + match f accum address rev_accesses with | Continue accum -> ( match Memory.find_opt address astate.heap with | None -> Continue (visited, accum) | Some edges -> - visit_edges orig_var ~f rev_accesses astate ~edges (visited, accum) ) + visit_edges edges ~f rev_accesses astate (visited, accum) ) | Stop fin -> Stop (visited, fin) ) - and visit_edges orig_var ~f rev_accesses ~edges astate visited_accum = + and visit_edges edges ~f rev_accesses astate visited_accum = let finish visited_accum = Continue visited_accum in Container.fold_until edges ~fold:Memory.Edges.fold ~finish ~init:visited_accum ~f:(fun visited_accum (access, (address, _trace)) -> - match visit_address orig_var ~f (access :: rev_accesses) astate address visited_accum with + match visit_address address ~f (access :: rev_accesses) astate visited_accum with | Continue _ as cont -> cont | Stop fin -> Stop (Stop fin) ) - let fold ~var_filter astate ~init ~f ~finish = + let visit_address_from_var (orig_var, (address, _loc)) ~f rev_accesses astate visited_accum = + visit_address address ~f:(f orig_var) rev_accesses astate visited_accum + + + let fold_common x astate ~fold ~filter ~visit ~init ~f ~finish = let finish (visited, accum) = (visited, finish accum) in let init = (AbstractValue.Set.empty, init) in - Container.fold_until astate.stack ~fold:(IContainer.fold_of_pervasives_map_fold Stack.fold) - ~init ~finish ~f:(fun visited_accum (var, (address, _loc)) -> - if var_filter var then visit_address var ~f [] astate address visited_accum - else Continue visited_accum ) + Container.fold_until x ~fold ~init ~finish ~f:(fun visited_accum elem -> + if filter elem then visit elem ~f [] astate visited_accum else Continue visited_accum ) + + + let fold ~var_filter astate = + fold_common astate.stack astate + ~fold:(IContainer.fold_of_pervasives_map_fold Stack.fold) + ~filter:(fun (var, _) -> var_filter var) + ~visit:visit_address_from_var + + + let fold_from_addresses from astate = + fold_common from astate ~fold:List.fold ~filter:(fun _ -> true) ~visit:visit_address end include GraphComparison @@ -255,5 +280,11 @@ let reachable_addresses astate = GraphVisit.fold astate ~var_filter:(fun _ -> true) ~init:() ~finish:Fn.id - ~f:(fun () _ _ _ -> Continue ()) + ~f:(fun _ () _ _ -> Continue ()) + |> fst + + +let reachable_addresses_from addresses astate = + GraphVisit.fold_from_addresses addresses astate ~init:() ~finish:Fn.id ~f:(fun () _ _ -> + Continue () ) |> fst diff --git a/infer/src/pulse/PulseBaseDomain.mli b/infer/src/pulse/PulseBaseDomain.mli index fe60e57ea..7c756ecbc 100644 --- a/infer/src/pulse/PulseBaseDomain.mli +++ b/infer/src/pulse/PulseBaseDomain.mli @@ -20,6 +20,9 @@ val reachable_addresses : t -> AbstractValue.Set.t (** compute the set of abstract addresses that are "used" in the abstract state, i.e. reachable from the stack variables *) +val reachable_addresses_from : AbstractValue.t list -> t -> AbstractValue.Set.t +(** compute the set of abstract addresses that are reachable from given abstract addresses *) + type mapping val empty_mapping : mapping diff --git a/infer/src/pulse/PulseInvalidation.ml b/infer/src/pulse/PulseInvalidation.ml index 5cd4c3fce..33edd1558 100644 --- a/infer/src/pulse/PulseInvalidation.ml +++ b/infer/src/pulse/PulseInvalidation.ml @@ -50,6 +50,7 @@ type t = | OptionalEmpty | StdVector of std_vector_function | JavaIterator of java_iterator_function + | Uninitialized [@@deriving compare, equal] let issue_type_of_cause = function @@ -69,6 +70,8 @@ let issue_type_of_cause = function IssueType.optional_empty_access | JavaIterator _ | StdVector _ -> IssueType.vector_invalidation + | Uninitialized -> + IssueType.uninitialized_value_pulse let describe f cause = @@ -96,6 +99,8 @@ let describe f cause = F.fprintf f "was potentially invalidated by `%a()`" pp_std_vector_function std_vector_f | JavaIterator java_iterator_f -> F.fprintf f "was potentially invalidated by `%a()`" pp_java_iterator_function java_iterator_f + | Uninitialized -> + F.pp_print_string f "was uninitialized" let pp f invalidation = @@ -112,3 +117,5 @@ let pp f invalidation = F.fprintf f "StdVector(%a)" describe invalidation | JavaIterator _ -> F.fprintf f "JavaIterator(%a)" describe invalidation + | Uninitialized -> + F.pp_print_string f "Uninitialized" diff --git a/infer/src/pulse/PulseInvalidation.mli b/infer/src/pulse/PulseInvalidation.mli index 8fcdfbb5e..cd0db16ef 100644 --- a/infer/src/pulse/PulseInvalidation.mli +++ b/infer/src/pulse/PulseInvalidation.mli @@ -31,6 +31,7 @@ type t = | OptionalEmpty | StdVector of std_vector_function | JavaIterator of java_iterator_function + | Uninitialized [@@deriving compare, equal] val pp : F.formatter -> t -> unit diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 9fc895093..ff1dcd660 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -36,7 +36,9 @@ module Misc = struct let shallow_copy location event ret_id dest_pointer_hist src_pointer_hist astate = - let* astate, obj = PulseOperations.eval_access location src_pointer_hist Dereference astate in + let* astate, obj = + PulseOperations.eval_access Read location src_pointer_hist Dereference astate + in shallow_copy_value location event ret_id dest_pointer_hist obj astate @@ -133,7 +135,14 @@ end module C = struct let free deleted_access : model = Misc.free_or_delete `Free deleted_access - let malloc _ : model = + let set_uninitialized size_exp_opt location ret_value astate = + Option.value_map size_exp_opt ~default:astate ~f:(fun size_exp -> + BufferOverrunModels.get_malloc_info_opt size_exp + |> Option.value_map ~default:astate ~f:(fun (obj_typ, _, _, _) -> + AbductiveDomain.set_uninitialized (`Malloc ret_value) obj_typ location astate ) ) + + + let malloc_common ~size_exp_opt : model = fun _ ~callee_procname location ~ret:(ret_id, _) astate -> let ret_addr = AbstractValue.mk_fresh () in let ret_value = @@ -143,6 +152,7 @@ module C = struct let astate_alloc = PulseArithmetic.and_positive ret_addr astate |> PulseOperations.allocate callee_procname location ret_value + |> set_uninitialized size_exp_opt location ret_value in let+ astate_null = PulseArithmetic.and_eq_int ret_addr IntLit.zero astate @@ -151,16 +161,28 @@ module C = struct [ExecutionDomain.ContinueProgram astate_alloc; ExecutionDomain.ContinueProgram astate_null] - let malloc_not_null _ : model = + let malloc_not_null_common ~size_exp_opt : model = fun _ ~callee_procname location ~ret:(ret_id, _) astate -> let ret_addr = AbstractValue.mk_fresh () in let ret_value = (ret_addr, [ValueHistory.Allocation {f= Model (Procname.to_string callee_procname); location}]) in let astate = PulseOperations.write_id ret_id ret_value astate in - PulseOperations.allocate callee_procname location ret_value astate - |> PulseArithmetic.and_positive ret_addr - |> ok_continue + let astate = + PulseOperations.allocate callee_procname location ret_value astate + |> PulseArithmetic.and_positive ret_addr + |> set_uninitialized size_exp_opt location ret_value + in + ok_continue astate + + + let malloc size_exp = malloc_common ~size_exp_opt:(Some size_exp) + + let malloc_no_param = malloc_common ~size_exp_opt:None + + let malloc_not_null size_exp = malloc_not_null_common ~size_exp_opt:(Some size_exp) + + let malloc_not_null_no_param = malloc_not_null_common ~size_exp_opt:None end module ObjCCoreFoundation = struct @@ -193,18 +215,18 @@ module Optional = struct let internal_value_access = HilExp.Access.FieldAccess internal_value - let to_internal_value location optional astate = - PulseOperations.eval_access location optional internal_value_access astate + let to_internal_value mode location optional astate = + PulseOperations.eval_access mode location optional internal_value_access astate - let to_internal_value_deref location optional astate = - let* astate, pointer = to_internal_value location optional astate in - PulseOperations.eval_access location pointer Dereference astate + let to_internal_value_deref mode location optional astate = + let* astate, pointer = to_internal_value Read location optional astate in + PulseOperations.eval_access mode location pointer Dereference astate let write_value location this ~value ~desc astate = let event = ValueHistory.Call {f= Model desc; location; in_call= []} in - let* astate, value_field = to_internal_value location this astate in + let* astate, value_field = to_internal_value Read location this astate in let value_hist = (fst value, event :: snd value) in let+ astate = PulseOperations.write_deref location ~ref:value_field ~obj:value_hist astate in (astate, value_hist) @@ -232,7 +254,7 @@ module Optional = struct let assign_optional_value this init ~desc : model = fun _ ~callee_procname:_ location ~ret:_ astate -> - let* astate, value = to_internal_value_deref location init astate in + let* astate, value = to_internal_value_deref Read location init astate in let+ astate, _ = write_value location this ~value ~desc astate in [ExecutionDomain.ContinueProgram astate] @@ -247,10 +269,10 @@ module Optional = struct fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let* astate, ((value_addr, value_hist) as value) = - to_internal_value_deref location optional astate + to_internal_value_deref Write location optional astate in (* Check dereference to show an error at the callsite of `value()` *) - let* astate, _ = PulseOperations.eval_access location value Dereference astate in + let* astate, _ = PulseOperations.eval_access Write location value Dereference astate in PulseOperations.write_id ret_id (value_addr, event :: value_hist) astate |> ok_continue @@ -258,7 +280,7 @@ module Optional = struct fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let ret_addr = AbstractValue.mk_fresh () in let ret_value = (ret_addr, [ValueHistory.Call {f= Model desc; location; in_call= []}]) in - let+ astate, (value_addr, _) = to_internal_value_deref location optional astate in + let+ astate, (value_addr, _) = to_internal_value_deref Read location optional astate in let astate = PulseOperations.write_id ret_id ret_value astate in let astate_non_empty = PulseArithmetic.and_positive value_addr astate in let astate_true = PulseArithmetic.and_positive ret_addr astate_non_empty in @@ -270,7 +292,7 @@ module Optional = struct let get_pointer optional ~desc : model = fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in - let* astate, value_addr = to_internal_value_deref location optional astate in + let* astate, value_addr = to_internal_value_deref Read location optional astate in let value_update_hist = (fst value_addr, event :: snd value_addr) in let astate_value_addr = PulseOperations.write_id ret_id value_update_hist astate @@ -289,15 +311,15 @@ module Optional = struct let value_or optional default ~desc : model = fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in - let* astate, value_addr = to_internal_value_deref location optional astate in + let* astate, value_addr = to_internal_value_deref Read location optional astate in let astate_non_empty = PulseArithmetic.and_positive (fst value_addr) astate in let* astate_non_empty, value = - PulseOperations.eval_access location value_addr Dereference astate_non_empty + PulseOperations.eval_access Read location value_addr Dereference astate_non_empty in let value_update_hist = (fst value, event :: snd value) in let astate_value = PulseOperations.write_id ret_id value_update_hist astate_non_empty in let+ astate, (default_val, default_hist) = - PulseOperations.eval_access location default Dereference astate + PulseOperations.eval_access Read location default Dereference astate in let default_value_hist = (default_val, event :: default_hist) in let astate_empty = PulseArithmetic.and_eq_int (fst value_addr) IntLit.zero astate in @@ -327,11 +349,11 @@ module StdAtomicInteger = struct let load_backing_int location this astate = - let* astate, obj = PulseOperations.eval_access location this Dereference astate in + let* astate, obj = PulseOperations.eval_access Read location this Dereference astate in let* astate, int_addr = - PulseOperations.eval_access location obj (FieldAccess internal_int) astate + PulseOperations.eval_access Read location obj (FieldAccess internal_int) astate in - let+ astate, int_val = PulseOperations.eval_access location int_addr Dereference astate in + let+ astate, int_val = PulseOperations.eval_access Read location int_addr Dereference astate in (astate, int_addr, int_val) @@ -340,7 +362,7 @@ module StdAtomicInteger = struct let event = ValueHistory.Call {f= Model "std::atomic::atomic()"; location; in_call= []} in let this = (AbstractValue.mk_fresh (), [event]) in let* astate, int_field = - PulseOperations.eval_access location this (FieldAccess internal_int) astate + PulseOperations.eval_access Write location this (FieldAccess internal_int) astate in let* astate = PulseOperations.write_deref location ~ref:int_field ~obj:init_value astate in let+ astate = PulseOperations.write_deref location ~ref:this_address ~obj:this astate in @@ -433,9 +455,9 @@ module StdAtomicInteger = struct let operator_t = load_instr "std::atomic::operator_T()" let store_backing_int location this_address new_value astate = - let* astate, this = PulseOperations.eval_access location this_address Dereference astate in + let* astate, this = PulseOperations.eval_access Read location this_address Dereference astate in let* astate, int_field = - PulseOperations.eval_access location this (FieldAccess internal_int) astate + PulseOperations.eval_access Write location this (FieldAccess internal_int) astate in PulseOperations.write_deref location ~ref:int_field ~obj:new_value astate @@ -461,7 +483,9 @@ module JavaObject = struct let clone src_pointer_hist : model = fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model "Object.clone"; location; in_call= []} in - let* astate, obj = PulseOperations.eval_access location src_pointer_hist Dereference astate in + let* astate, obj = + PulseOperations.eval_access Read location src_pointer_hist Dereference astate + in let+ astate, obj_copy = PulseOperations.shallow_copy location obj astate in let astate = PulseOperations.write_id ret_id (fst obj_copy, event :: snd obj_copy) astate in [ExecutionDomain.ContinueProgram astate] @@ -477,7 +501,7 @@ module StdBasicString = struct let internal_string_access = HilExp.Access.FieldAccess internal_string let to_internal_string location bstring astate = - PulseOperations.eval_access location bstring internal_string_access astate + PulseOperations.eval_access Read location bstring internal_string_access astate let data this_hist : model = @@ -485,7 +509,7 @@ module StdBasicString = struct let event = ValueHistory.Call {f= Model "std::basic_string::data()"; location; in_call= []} in let* astate, string_addr_hist = to_internal_string location this_hist astate in let+ astate, (string, hist) = - PulseOperations.eval_access location string_addr_hist Dereference astate + PulseOperations.eval_access Read location string_addr_hist Dereference astate in let astate = PulseOperations.write_id ret_id (string, event :: hist) astate in [ExecutionDomain.ContinueProgram astate] @@ -513,7 +537,7 @@ module StdFunction = struct [PulseOperations.havoc_id ret_id [event] astate] in let* astate, (lambda, _) = - PulseOperations.eval_access location lambda_ptr_hist Dereference astate + PulseOperations.eval_access Read location lambda_ptr_hist Dereference astate in let* astate = PulseOperations.Closures.check_captured_addresses location lambda astate in match AddressAttributes.get_closure_proc_name lambda astate with @@ -560,22 +584,24 @@ module GenericArrayBackedCollection = struct let access = HilExp.Access.FieldAccess field - let eval location collection astate = - PulseOperations.eval_access location collection access astate + let eval mode location collection astate = + PulseOperations.eval_access mode location collection access astate let eval_element location internal_array index astate = - PulseOperations.eval_access location internal_array (ArrayAccess (StdTyp.void, index)) astate + PulseOperations.eval_access Read location internal_array + (ArrayAccess (StdTyp.void, index)) + astate let element location collection index astate = - let* astate, internal_array = eval location collection astate in + let* astate, internal_array = eval Read location collection astate in eval_element location internal_array index astate let eval_pointer_to_last_element location collection astate = let+ astate, pointer = - PulseOperations.eval_access location collection (FieldAccess last_field) astate + PulseOperations.eval_access Write location collection (FieldAccess last_field) astate in let astate = AddressAttributes.mark_as_end_of_collection (fst pointer) astate in (astate, pointer) @@ -586,19 +612,19 @@ module GenericArrayBackedCollectionIterator = struct let internal_pointer_access = HilExp.Access.FieldAccess internal_pointer - let to_internal_pointer location iterator astate = - PulseOperations.eval_access location iterator internal_pointer_access astate + let to_internal_pointer mode location iterator astate = + PulseOperations.eval_access mode location iterator internal_pointer_access astate - let to_internal_pointer_deref location iterator astate = - let* astate, pointer = to_internal_pointer location iterator astate in - let+ astate, index = PulseOperations.eval_access location pointer Dereference astate in + let to_internal_pointer_deref mode location iterator astate = + let* astate, pointer = to_internal_pointer Read location iterator astate in + let+ astate, index = PulseOperations.eval_access mode location pointer Dereference astate in (astate, pointer, index) - let to_elem_pointed_by_iterator ?(step = None) location iterator astate = - let* astate, pointer = to_internal_pointer location iterator astate in - let* astate, index = PulseOperations.eval_access location pointer Dereference astate in + let to_elem_pointed_by_iterator mode ?(step = None) location iterator astate = + let* astate, pointer = to_internal_pointer Read location iterator astate in + let* astate, index = PulseOperations.eval_access mode location pointer Dereference astate in (* Check if not end iterator *) let is_minus_minus = match step with Some `MinusMinus -> true | _ -> false in let* astate = @@ -612,19 +638,21 @@ module GenericArrayBackedCollectionIterator = struct else Ok astate in (* We do not want to create internal array if iterator pointer has an invalid value *) - let* astate = PulseOperations.check_addr_access location index astate in + let* astate = PulseOperations.check_addr_access Read location index astate in let+ astate, elem = GenericArrayBackedCollection.element location iterator (fst index) astate in (astate, pointer, elem) let construct location event ~init ~ref astate = - let* astate, (arr_addr, arr_hist) = GenericArrayBackedCollection.eval location init astate in + let* astate, (arr_addr, arr_hist) = + GenericArrayBackedCollection.eval Read location init astate + in let* astate = PulseOperations.write_field location ~ref GenericArrayBackedCollection.field ~obj:(arr_addr, event :: arr_hist) astate in - let* astate, (p_addr, p_hist) = to_internal_pointer location init astate in + let* astate, (p_addr, p_hist) = to_internal_pointer Read location init astate in PulseOperations.write_field location ~ref internal_pointer ~obj:(p_addr, event :: p_hist) astate @@ -637,8 +665,8 @@ module GenericArrayBackedCollectionIterator = struct let operator_compare comparison ~desc iter_lhs iter_rhs _ ~callee_procname:_ location ~ret:(ret_id, _) astate = let event = ValueHistory.Call {f= Model desc; location; in_call= []} in - let* astate, _, (index_lhs, _) = to_internal_pointer_deref location iter_lhs astate in - let+ astate, _, (index_rhs, _) = to_internal_pointer_deref location iter_rhs astate in + let* astate, _, (index_lhs, _) = to_internal_pointer_deref Read location iter_lhs astate in + let+ astate, _, (index_rhs, _) = to_internal_pointer_deref Read location iter_rhs astate in let ret_val = AbstractValue.mk_fresh () in let astate = PulseOperations.write_id ret_id (ret_val, [event]) astate in let ret_val_equal, ret_val_notequal = @@ -663,7 +691,7 @@ module GenericArrayBackedCollectionIterator = struct let operator_star ~desc iter _ ~callee_procname:_ location ~ret astate = let event = ValueHistory.Call {f= Model desc; location; in_call= []} in - let+ astate, pointer, (elem, _) = to_elem_pointed_by_iterator location iter astate in + let+ astate, pointer, (elem, _) = to_elem_pointed_by_iterator Read location iter astate in let astate = PulseOperations.write_id (fst ret) (elem, event :: snd pointer) astate in [ExecutionDomain.ContinueProgram astate] @@ -671,7 +699,9 @@ module GenericArrayBackedCollectionIterator = struct let operator_step step ~desc iter _ ~callee_procname:_ location ~ret:_ astate = let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let index_new = AbstractValue.mk_fresh () in - let* astate, pointer, _ = to_elem_pointed_by_iterator ~step:(Some step) location iter astate in + let* astate, pointer, _ = + to_elem_pointed_by_iterator Read ~step:(Some step) location iter astate + in PulseOperations.write_deref location ~ref:pointer ~obj:(index_new, event :: snd pointer) astate >>| ExecutionDomain.continue >>| List.return end @@ -691,7 +721,7 @@ module JavaIterator = struct let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let new_index = AbstractValue.mk_fresh () in let* astate, (curr_index, curr_index_hist) = - GenericArrayBackedCollectionIterator.to_internal_pointer location iter astate + GenericArrayBackedCollectionIterator.to_internal_pointer Read location iter astate in let* astate, (curr_elem_val, curr_elem_hist) = GenericArrayBackedCollection.element location iter curr_index astate @@ -713,7 +743,7 @@ module JavaIterator = struct let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let new_index = AbstractValue.mk_fresh () in let* astate, (curr_index, curr_index_hist) = - GenericArrayBackedCollectionIterator.to_internal_pointer location iter astate + GenericArrayBackedCollectionIterator.to_internal_pointer Read location iter astate in let* astate = PulseOperations.write_field location ~ref:iter @@ -722,7 +752,7 @@ module JavaIterator = struct astate in let new_elem = AbstractValue.mk_fresh () in - let* astate, arr = GenericArrayBackedCollection.eval location iter astate in + let* astate, arr = GenericArrayBackedCollection.eval Read location iter astate in let+ astate = PulseOperations.write_arr_index location ~ref:arr ~index:curr_index ~obj:(new_elem, event :: curr_index_hist) @@ -733,7 +763,9 @@ end module StdVector = struct let reallocate_internal_array trace vector vector_f location astate = - let* astate, array_address = GenericArrayBackedCollection.eval location vector astate in + let* astate, array_address = + GenericArrayBackedCollection.eval NoAccess location vector astate + in PulseOperations.invalidate_array_elements location (StdVector vector_f) array_address astate >>= PulseOperations.invalidate_access location (StdVector vector_f) vector GenericArrayBackedCollection.access @@ -781,7 +813,7 @@ module StdVector = struct let index_zero = AbstractValue.mk_fresh () in let astate = PulseArithmetic.and_eq_int index_zero IntLit.zero astate in let* astate, ((arr_addr, _) as arr) = - GenericArrayBackedCollection.eval location vector astate + GenericArrayBackedCollection.eval Read location vector astate in let* astate, _ = GenericArrayBackedCollection.eval_element location arr index_zero astate in PulseOperations.write_field location ~ref:iter GenericArrayBackedCollection.field @@ -795,7 +827,7 @@ module StdVector = struct let vector_end vector iter : model = fun _ ~callee_procname:_ location ~ret:_ astate -> let event = ValueHistory.Call {f= Model "std::vector::end()"; location; in_call= []} in - let* astate, (arr_addr, _) = GenericArrayBackedCollection.eval location vector astate in + let* astate, (arr_addr, _) = GenericArrayBackedCollection.eval Read location vector astate in let* astate, (pointer_addr, _) = GenericArrayBackedCollection.eval_pointer_to_last_element location vector astate in @@ -838,7 +870,7 @@ module JavaCollection = struct let set coll (index, _) (new_elem, new_elem_hist) : model = fun _ ~callee_procname:_ location ~ret astate -> let event = ValueHistory.Call {f= Model "Collection.set"; location; in_call= []} in - let* astate, arr = GenericArrayBackedCollection.eval location coll astate in + let* astate, arr = GenericArrayBackedCollection.eval Read location coll astate in let* astate, (old_addr, old_hist) = GenericArrayBackedCollection.element location coll index astate in @@ -855,7 +887,7 @@ module JavaCollection = struct let add_at coll (index, _) (new_elem, new_elem_hist) : model = fun _ ~callee_procname:_ location ~ret:_ astate -> let event = ValueHistory.Call {f= Model "Collection.add"; location; in_call= []} in - let* astate, arr = GenericArrayBackedCollection.eval location coll astate in + let* astate, arr = GenericArrayBackedCollection.eval Read location coll astate in let+ astate = PulseOperations.write_arr_index location ~ref:arr ~index ~obj:(new_elem, event :: new_elem_hist) @@ -874,7 +906,7 @@ module JavaCollection = struct let remove_at coll (index, _) : model = fun _ ~callee_procname:_ location ~ret:_ astate -> let event = ValueHistory.Call {f= Model "Collection.add"; location; in_call= []} in - let* astate, arr = GenericArrayBackedCollection.eval location coll astate in + let* astate, arr = GenericArrayBackedCollection.eval Read location coll astate in let fresh_elem = AbstractValue.mk_fresh () in let+ astate = PulseOperations.write_arr_index location ~ref:arr ~index @@ -943,7 +975,7 @@ module ProcNameDispatcher = struct make_dispatcher ( transfer_ownership_matchers @ abort_matchers @ return_nonnull_matchers @ [ +match_builtin BuiltinDecl.free <>$ capt_arg_payload $--> C.free - ; +match_builtin BuiltinDecl.malloc <>$ capt_arg_payload $--> C.malloc + ; +match_builtin BuiltinDecl.malloc <>$ capt_exp $--> C.malloc ; +match_builtin BuiltinDecl.__delete <>$ capt_arg_payload $--> Cplusplus.delete ; +match_builtin BuiltinDecl.__new &--> Misc.return_positive ~desc:"new" ; +match_builtin BuiltinDecl.__placement_new &++> Cplusplus.placement_new @@ -1199,10 +1231,13 @@ module ProcNameDispatcher = struct &:: "nextElement" <>$ capt_arg_payload $!--> fun x -> StdVector.at ~desc:"Enumeration.nextElement" x (AbstractValue.mk_fresh (), []) ) - ; +map_context_tenv PatternMatch.ObjectiveC.is_core_graphics_create_or_copy &++> C.malloc - ; +map_context_tenv PatternMatch.ObjectiveC.is_core_foundation_create_or_copy &++> C.malloc - ; +match_builtin BuiltinDecl.malloc_no_fail <>$ capt_arg_payload $--> C.malloc_not_null - ; +map_context_tenv PatternMatch.ObjectiveC.is_modelled_as_alloc &++> C.malloc_not_null + ; +map_context_tenv PatternMatch.ObjectiveC.is_core_graphics_create_or_copy + &--> C.malloc_no_param + ; +map_context_tenv PatternMatch.ObjectiveC.is_core_foundation_create_or_copy + &--> C.malloc_no_param + ; +match_builtin BuiltinDecl.malloc_no_fail <>$ capt_exp $--> C.malloc_not_null + ; +map_context_tenv PatternMatch.ObjectiveC.is_modelled_as_alloc + &--> C.malloc_not_null_no_param ; +map_context_tenv PatternMatch.ObjectiveC.is_core_graphics_release <>$ capt_arg_payload $--> ObjCCoreFoundation.cf_bridging_release ; -"CFRelease" <>$ capt_arg_payload $--> ObjCCoreFoundation.cf_bridging_release diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index f29a1188d..246f898d4 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -14,13 +14,34 @@ type t = AbductiveDomain.t type 'a access_result = 'a PulseReport.access_result -let check_addr_access location (address, history) astate = +type access_mode = Read | Write | NoAccess + +let check_addr_access access_mode location (address, history) astate = let access_trace = Trace.Immediate {location; history} in - AddressAttributes.check_valid access_trace address astate - |> Result.map_error ~f:(fun (invalidation, invalidation_trace) -> - ( Diagnostic.AccessToInvalidAddress - {calling_context= []; invalidation; invalidation_trace; access_trace} - , astate ) ) + let* astate = + AddressAttributes.check_valid access_trace address astate + |> Result.map_error ~f:(fun (invalidation, invalidation_trace) -> + ( Diagnostic.AccessToInvalidAddress + {calling_context= []; invalidation; invalidation_trace; access_trace} + , astate ) ) + in + match access_mode with + | Read -> + let+ () = + AddressAttributes.check_initialized address astate + |> Result.map_error ~f:(fun invalidation_trace -> + ( Diagnostic.AccessToInvalidAddress + { calling_context= [] + ; invalidation= Uninitialized + ; invalidation_trace + ; access_trace } + , astate ) ) + in + astate + | Write -> + Ok (AbductiveDomain.initialize address astate) + | NoAccess -> + Ok astate module Closures = struct @@ -70,7 +91,7 @@ module Closures = struct | Attribute.Closure _ -> IContainer.iter_result ~fold:Memory.Edges.fold edges ~f:(fun (access, addr_trace) -> if is_captured_by_ref_fake_access access then - let+ _ = check_addr_access action addr_trace astate in + let+ _ = check_addr_access Read action addr_trace astate in () else Ok () ) | _ -> @@ -97,35 +118,35 @@ end let eval_var var astate = Stack.eval var astate -let eval_access location addr_hist access astate = - let+ astate = check_addr_access location addr_hist astate in +let eval_access mode location addr_hist access astate = + let+ astate = check_addr_access mode location addr_hist astate in Memory.eval_edge addr_hist access astate -let eval location exp0 astate = - let rec eval exp astate = +let eval mode location exp0 astate = + let rec eval mode exp astate = match (exp : Exp.t) with | Var id -> Ok (eval_var (* error in case of missing history? *) [] (Var.of_id id) astate) | Lvar pvar -> Ok (eval_var [ValueHistory.VariableAccessed (pvar, location)] (Var.of_pvar pvar) astate) | Lfield (exp', field, _) -> - let* astate, addr_hist = eval exp' astate in - eval_access location addr_hist (FieldAccess field) astate + let* astate, addr_hist = eval Read exp' astate in + eval_access mode location addr_hist (FieldAccess field) astate | Lindex (exp', exp_index) -> - let* astate, addr_hist_index = eval exp_index astate in - let* astate, addr_hist = eval exp' astate in - eval_access location addr_hist (ArrayAccess (StdTyp.void, fst addr_hist_index)) astate + let* astate, addr_hist_index = eval Read exp_index astate in + let* astate, addr_hist = eval Read exp' astate in + eval_access mode location addr_hist (ArrayAccess (StdTyp.void, fst addr_hist_index)) astate | Closure {name; captured_vars} -> let+ astate, rev_captured = List.fold_result captured_vars ~init:(astate, []) ~f:(fun (astate, rev_captured) (capt_exp, captured_as, _, mode) -> - let+ astate, addr_trace = eval capt_exp astate in + let+ astate, addr_trace = eval Read capt_exp astate in (astate, (captured_as, addr_trace, mode) :: rev_captured) ) in Closures.record location name (List.rev rev_captured) astate | Cast (_, exp') -> - eval exp' astate + eval mode exp' astate | Const (Cint i) -> let v = AbstractValue.Constants.get_int i in let astate = @@ -136,13 +157,13 @@ let eval location exp0 astate = in Ok (astate, (v, [])) | UnOp (unop, exp, _typ) -> - let+ astate, (addr, hist) = eval exp astate in + let+ astate, (addr, hist) = eval Read exp astate in let unop_addr = AbstractValue.mk_fresh () in (PulseArithmetic.eval_unop unop_addr unop addr astate, (unop_addr, hist)) | BinOp (bop, e_lhs, e_rhs) -> - let* astate, (addr_lhs, hist_lhs) = eval e_lhs astate in + let* astate, (addr_lhs, hist_lhs) = eval Read e_lhs astate in (* NOTE: keeping track of only [hist_lhs] into the binop is not the best *) - let+ astate, (addr_rhs, _hist_rhs) = eval e_rhs astate in + let+ astate, (addr_rhs, _hist_rhs) = eval Read e_rhs astate in let binop_addr = AbstractValue.mk_fresh () in ( PulseArithmetic.eval_binop binop_addr bop (AbstractValueOperand addr_lhs) (AbstractValueOperand addr_rhs) astate @@ -150,15 +171,15 @@ let eval location exp0 astate = | Const _ | Sizeof _ | Exn _ -> Ok (astate, (AbstractValue.mk_fresh (), (* TODO history *) [])) in - eval exp0 astate + eval mode exp0 astate -let eval_to_operand location exp astate = +let eval_to_operand mode location exp astate = match (exp : Exp.t) with | Const (Cint i) -> Ok (astate, PulseArithmetic.LiteralOperand i) | exp -> - let+ astate, (value, _) = eval location exp astate in + let+ astate, (value, _) = eval mode location exp astate in (astate, PulseArithmetic.AbstractValueOperand value) @@ -166,8 +187,8 @@ let prune location ~condition astate = let rec prune_aux ~negated exp astate = match (exp : Exp.t) with | BinOp (bop, exp_lhs, exp_rhs) -> - let* astate, lhs_op = eval_to_operand location exp_lhs astate in - let+ astate, rhs_op = eval_to_operand location exp_rhs astate in + let* astate, lhs_op = eval_to_operand Read location exp_lhs astate in + let+ astate, rhs_op = eval_to_operand Read location exp_rhs astate in PulseArithmetic.prune_binop ~negated bop lhs_op rhs_op astate | UnOp (LNot, exp', _) -> prune_aux ~negated:(not negated) exp' astate @@ -178,15 +199,17 @@ let prune location ~condition astate = let eval_deref location exp astate = - let* astate, addr_hist = eval location exp astate in - let+ astate = check_addr_access location addr_hist astate in + let* astate, addr_hist = eval Read location exp astate in + let+ astate = check_addr_access Read location addr_hist astate in Memory.eval_edge addr_hist Dereference astate -let realloc_pvar pvar location astate = - Stack.add (Var.of_pvar pvar) - (AbstractValue.mk_fresh (), [ValueHistory.VariableDeclared (pvar, location)]) - astate +let realloc_pvar pvar typ location astate = + let addr = AbstractValue.mk_fresh () in + let astate = + Stack.add (Var.of_pvar pvar) (addr, [ValueHistory.VariableDeclared (pvar, location)]) astate + in + AbductiveDomain.set_uninitialized (`LocalDecl (pvar, Some addr)) typ location astate let write_id id new_addr_loc astate = Stack.add (Var.of_id id) new_addr_loc astate @@ -199,7 +222,7 @@ let havoc_id id loc_opt astate = let write_access location addr_trace_ref access addr_trace_obj astate = - check_addr_access location addr_trace_ref astate + check_addr_access Write location addr_trace_ref astate >>| Memory.add_edge addr_trace_ref access addr_trace_obj location @@ -228,7 +251,7 @@ let add_dynamic_type typ address astate = AddressAttributes.add_dynamic_type typ let remove_allocation_attr address astate = AddressAttributes.remove_allocation_attr address astate let invalidate location cause addr_trace astate = - check_addr_access location addr_trace astate + check_addr_access NoAccess location addr_trace astate >>| AddressAttributes.invalidate addr_trace cause location @@ -238,7 +261,7 @@ let invalidate_access location cause ref_addr_hist access astate = let invalidate_array_elements location cause addr_trace astate = - let+ astate = check_addr_access location addr_trace astate in + let+ astate = check_addr_access NoAccess location addr_trace astate in match Memory.find_opt (fst addr_trace) astate with | None -> astate @@ -252,7 +275,7 @@ let invalidate_array_elements location cause addr_trace astate = let shallow_copy location addr_hist astate = - let+ astate = check_addr_access location addr_hist astate in + let+ astate = check_addr_access Read location addr_hist astate in let cell = match AbductiveDomain.find_post_cell_opt (fst addr_hist) astate with | None -> @@ -496,12 +519,12 @@ let apply_callee ~caller_proc_desc callee_pname call_loc callee_exec_state ~ret let get_captured_actuals location ~captured_vars ~actual_closure astate = - let* astate, this_value_addr = eval_access location actual_closure Dereference astate in + let* astate, this_value_addr = eval_access Read location actual_closure Dereference astate in let+ _, astate, captured_vars_with_actuals = List.fold_result captured_vars ~init:(0, astate, []) ~f:(fun (id, astate, captured) (var, mode) -> let+ astate, captured_actual = - eval_access location this_value_addr + eval_access Read location this_value_addr (FieldAccess (Closures.mk_fake_field ~id mode)) astate in diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 6b6febc8f..215b9a207 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -13,7 +13,16 @@ type t = AbductiveDomain.t type 'a access_result = 'a PulseReport.access_result -val check_addr_access : Location.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result +type access_mode = + | Read + | Write + | NoAccess + (** The initialized-ness of the address is not checked when it evaluates a heap address + without actual memory access, for example, when evaluating [&x.f] we need to check + initialized-ness of [x], not that of [x.f]. *) + +val check_addr_access : + access_mode -> Location.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result (** Check that the [address] is not known to be invalid *) module Closures : sig @@ -21,7 +30,8 @@ module Closures : sig (** assert the validity of the addresses captured by the lambda *) end -val eval : Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) access_result +val eval : + access_mode -> Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) access_result (** Use the stack and heap to evaluate the given expression down to an abstract address representing its value. @@ -34,7 +44,8 @@ val eval_deref : Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistor (** Like [eval] but evaluates [*exp]. *) val eval_access : - Location.t + access_mode + -> Location.t -> AbstractValue.t * ValueHistory.t -> BaseMemory.Access.t -> t @@ -52,7 +63,7 @@ val havoc_field : -> t -> t access_result -val realloc_pvar : Pvar.t -> Location.t -> t -> t +val realloc_pvar : Pvar.t -> Typ.t -> Location.t -> t -> t val write_id : Ident.t -> AbstractValue.t * ValueHistory.t -> t -> t diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp index 02709e060..70131dbdc 100644 --- a/infer/tests/codetoanalyze/c/pulse/issues.exp +++ b/infer/tests/codetoanalyze/c/pulse/issues.exp @@ -3,3 +3,7 @@ codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad2, 4, MEMORY_LE codetoanalyze/c/pulse/memory_leak.c, malloc_no_free_bad, 0, 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/nullptr.c, malloc_no_check_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,allocated by call to `malloc` (modelled),is the null pointer,use-after-lifetime part of the trace starts here,allocated by call to `malloc` (modelled),assigned,invalid access occurs here] codetoanalyze/c/pulse/nullptr.c, nullptr_deref_young_bad, 5, 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/c/pulse/uninit.c, call_to_use_and_mayinit_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `x` declared here,was uninitialized,use-after-lifetime part of the trace starts here,variable `x` declared here,invalid access occurs here] +codetoanalyze/c/pulse/uninit.c, dereference_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `p` declared here,was uninitialized,use-after-lifetime part of the trace starts here,variable `p` declared here,invalid access occurs here] +codetoanalyze/c/pulse/uninit.c, malloc_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [invalidation part of the trace starts here,allocated by call to `malloc` (modelled),was uninitialized,use-after-lifetime part of the trace starts here,allocated by call to `malloc` (modelled),assigned,invalid access occurs here] +codetoanalyze/c/pulse/uninit.c, self_assign_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `x` declared here,was uninitialized,use-after-lifetime part of the trace starts here,variable `x` declared here,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/c/pulse/uninit.c b/infer/tests/codetoanalyze/c/pulse/uninit.c new file mode 100644 index 000000000..6bd13eb34 --- /dev/null +++ b/infer/tests/codetoanalyze/c/pulse/uninit.c @@ -0,0 +1,85 @@ +/* + * 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. + */ + +int dereference_bad() { + int* p; + return *p; +} + +void self_assign_bad() { + int x; + x = x; +} + +void use_and_mayinit(int, int*); + +void call_to_use_and_mayinit_bad() { + int x; + use_and_mayinit(x, &x); +} + +void malloc_good() { + int* p = (int*)malloc(sizeof(int)); + if (p) { + *p = 5; + int x = *p; + } + free(p); +} + +void malloc_bad() { + int* p = (int*)malloc(sizeof(int)); + if (p) { + int x = *p; + } + free(p); +} + +void init_int_ref(int* p) { *p = 5; } + +void nop(int* p) {} + +void interprocedural_good() { + int x; + init_int_ref(&x); + int y = x; +} + +void interprocedural_bad_FN() { + int x; + nop(&x); + int y = x; +} + +struct uninit_s { + int f1; + int f2; +}; + +void get_field_address_good() { + struct uninit_s* s = (struct uninit_s*)malloc(2 * sizeof(int)); + if (s) { + int* p = &s->f1; + } + free(s); +} + +void init_f1(struct uninit_s* p) { p->f1 = 5; } + +void interprocedural_struct_bad_FN() { + struct uninit_s s; + init_f1(&s); + int y = s.f2; +} + +void malloc_array_good(int len) { + char* o = (char*)malloc(len); + if (o) { + o[0] = 'a'; + } + free(o); +} diff --git a/infer/tests/codetoanalyze/cpp/pulse/basics.cpp b/infer/tests/codetoanalyze/cpp/pulse/basics.cpp index c64321908..b4aea23a8 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/basics.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/basics.cpp @@ -93,7 +93,7 @@ struct A { A getA(); int struct_inside_loop_ok(std::vector numbers) { - int sum; + int sum = 0; for (auto number : numbers) { A a = getA(); sum += a.f(number); @@ -102,7 +102,7 @@ int struct_inside_loop_ok(std::vector numbers) { } int struct_inside_loop_break_ok(std::vector numbers) { - int sum; + int sum = 0; for (auto number : numbers) { A a = getA(); if (number < 0) { @@ -114,7 +114,7 @@ int struct_inside_loop_break_ok(std::vector numbers) { } int struct_inside_loop_continue_ok(std::vector numbers) { - int sum; + int sum = 0; for (auto number : numbers) { A a = getA(); if (number < 0) { diff --git a/infer/tests/codetoanalyze/objc/pulse/issues.exp b/infer/tests/codetoanalyze/objc/pulse/issues.exp index d8317af99..b0ed542c1 100644 --- a/infer/tests/codetoanalyze/objc/pulse/issues.exp +++ b/infer/tests/codetoanalyze/objc/pulse/issues.exp @@ -10,5 +10,6 @@ codetoanalyze/objc/pulse/MemoryLeaksInBlocks.m, block_captured_var_leak_bad, 6, codetoanalyze/objc/pulse/NPEBlocks.m, Singleton.dispatch_once_no_npe_good_FP, 6, 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/objc/pulse/NPEBlocks.m, captured_npe_bad, 5, 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,when calling `objc_blockcaptured_npe_bad_3` here,parameter `x` of objc_blockcaptured_npe_bad_3,invalid access occurs here] codetoanalyze/objc/pulse/NPEBlocks.m, captured_npe_ok_FP, 6, 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/objc/pulse/uninit.m, Uninit.capture_in_closure_bad, 7, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `x` declared here,was uninitialized,use-after-lifetime part of the trace starts here,variable `x` declared here,invalid access occurs 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] diff --git a/infer/tests/codetoanalyze/objc/pulse/uninit.m b/infer/tests/codetoanalyze/objc/pulse/uninit.m new file mode 100644 index 000000000..68ef90ae3 --- /dev/null +++ b/infer/tests/codetoanalyze/objc/pulse/uninit.m @@ -0,0 +1,43 @@ +/* + * 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. + */ +#import + +@interface Uninit : NSObject +@end + +@implementation Uninit + +- (void)capture_in_closure_ok { + __block BOOL x; + + void (^block)() = ^() { + x = true; + }; +} + +- (BOOL)capture_in_closure_bad { + __block BOOL x; + + void (^block)() = ^() { + x = true; + }; + + return x; +} + +- (BOOL)set_in_closure_ok { + __block BOOL x; + + void (^block)() = ^() { + x = true; + }; + + block(); + return x; +} + +@end