From 27ab8bd25309d1086a03fdb9c099fa4a462bff44 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 2 Feb 2021 02:10:40 -0800 Subject: [PATCH] [pulse] Uninitialized check for struct fields Reviewed By: jvillard Differential Revision: D25371929 fbshipit-source-id: 966f333e3 --- infer/src/IR/Fieldname.ml | 6 ++ infer/src/IR/Fieldname.mli | 3 + infer/src/pulse/Pulse.ml | 23 ++--- infer/src/pulse/PulseAbductiveDomain.ml | 92 +++++++++++++------ infer/src/pulse/PulseAbductiveDomain.mli | 5 +- infer/src/pulse/PulseAttribute.ml | 17 ++++ infer/src/pulse/PulseAttribute.mli | 2 + infer/src/pulse/PulseExecutionDomain.ml | 2 +- infer/src/pulse/PulseExecutionDomain.mli | 2 +- infer/src/pulse/PulseModels.ml | 29 +++--- infer/src/pulse/PulseOperations.ml | 44 ++++++--- infer/src/pulse/PulseOperations.mli | 8 +- infer/src/pulse/PulseUninitBlocklist.ml | 21 +++++ infer/src/pulse/PulseUninitBlocklist.mli | 11 +++ infer/src/pulse/PulseValueHistory.ml | 4 + infer/src/pulse/PulseValueHistory.mli | 1 + infer/tests/codetoanalyze/c/pulse/issues.exp | 1 + infer/tests/codetoanalyze/c/pulse/uninit.c | 19 +++- .../codetoanalyze/cpp/pulse/fbstring.cpp | 2 +- .../tests/codetoanalyze/cpp/pulse/issues.exp | 1 + .../tests/codetoanalyze/cpp/pulse/uninit.cpp | 36 ++++++++ 21 files changed, 256 insertions(+), 73 deletions(-) create mode 100644 infer/src/pulse/PulseUninitBlocklist.ml create mode 100644 infer/src/pulse/PulseUninitBlocklist.mli create mode 100644 infer/tests/codetoanalyze/cpp/pulse/uninit.cpp diff --git a/infer/src/IR/Fieldname.ml b/infer/src/IR/Fieldname.ml index 60c26c54c..ac248c773 100644 --- a/infer/src/IR/Fieldname.ml +++ b/infer/src/IR/Fieldname.ml @@ -25,6 +25,12 @@ let is_java {class_name} = Typ.Name.Java.is_class class_name let is_java_synthetic t = is_java t && JConfig.is_synthetic_name (get_field_name t) +let is_internal {field_name} = + String.is_prefix field_name ~prefix:"__" + || (* NOTE: _M_ is internal field of std::thread::id *) + String.is_prefix field_name ~prefix:"_M_" + + module T = struct type nonrec t = t [@@deriving compare] end diff --git a/infer/src/IR/Fieldname.mli b/infer/src/IR/Fieldname.mli index f3b3e4ca6..279dcc21b 100644 --- a/infer/src/IR/Fieldname.mli +++ b/infer/src/IR/Fieldname.mli @@ -26,6 +26,9 @@ val is_java : t -> bool val is_java_synthetic : t -> bool (** Check if the field is autogenerated/synthetic **) +val is_internal : t -> bool +(** Check if the field has the prefix "__" or "_M_" (internal field of std::thread::id) *) + (** Set for fieldnames *) module Set : Caml.Set.S with type elt = t diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 084929e3c..1d985abe4 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -70,14 +70,14 @@ module PulseTransferFunctions = struct AnalysisCallbacks.proc_resolve_attributes pname |> Option.map ~f:ProcAttributes.get_pvar_formals - let interprocedural_call {InterproceduralAnalysis.analyze_dependency; proc_desc} ret callee_pname - call_exp actuals call_loc astate = + let interprocedural_call {InterproceduralAnalysis.analyze_dependency; proc_desc; tenv} ret + callee_pname call_exp actuals call_loc astate = match callee_pname with | Some callee_pname when not Config.pulse_intraprocedural_only -> let formals_opt = get_pvar_formals callee_pname in let callee_data = analyze_dependency callee_pname in - PulseOperations.call ~caller_proc_desc:proc_desc ~callee_data call_loc callee_pname ~ret - ~actuals ~formals_opt astate + PulseOperations.call tenv ~caller_proc_desc:proc_desc ~callee_data call_loc callee_pname + ~ret ~actuals ~formals_opt astate | _ -> L.d_printfln "Skipping indirect call %a@\n" Exp.pp call_exp ; let astate = @@ -86,8 +86,8 @@ module PulseTransferFunctions = struct in [ Ok (ContinueProgram - (PulseOperations.unknown_call call_loc (SkippedUnknownCall call_exp) ~ret ~actuals - ~formals_opt:None astate)) ] + (PulseOperations.unknown_call tenv call_loc (SkippedUnknownCall call_exp) ~ret + ~actuals ~formals_opt:None astate)) ] (** has an object just gone out of scope? *) @@ -289,8 +289,9 @@ module PulseTransferFunctions = struct (astates, ret_vars) - let exec_instr_aux (astate : Domain.t) ({InterproceduralAnalysis.proc_desc} as analysis_data) - _cfg_node (instr : Sil.instr) : Domain.t list = + let exec_instr_aux (astate : Domain.t) + ({InterproceduralAnalysis.proc_desc; tenv} as analysis_data) _cfg_node (instr : Sil.instr) : + Domain.t list = match astate with | ISLLatentMemoryError _ | AbortProgram _ | LatentAbortProgram _ -> (* We can also continue the analysis with the error state here @@ -423,7 +424,7 @@ module PulseTransferFunctions = struct in remove_vars vars_to_remove astates | Metadata (VariableLifetimeBegins (pvar, typ, location)) when not (Pvar.is_global pvar) -> - [PulseOperations.realloc_pvar pvar typ location astate |> Domain.continue] + [PulseOperations.realloc_pvar tenv pvar typ location astate |> Domain.continue] | Metadata (Abstract _ | VariableLifetimeBegins _ | Nullify _ | Skip) -> [ContinueProgram astate] ) @@ -454,9 +455,9 @@ let with_debug_exit_node proc_desc ~f = ~f -let checker ({InterproceduralAnalysis.proc_desc; err_log} as analysis_data) = +let checker ({InterproceduralAnalysis.proc_desc; err_log; tenv} as analysis_data) = AbstractValue.State.reset () ; - let initial = [ExecutionDomain.mk_initial proc_desc] in + let initial = [ExecutionDomain.mk_initial tenv proc_desc] in match DisjunctiveAnalyzer.compute_post analysis_data ~initial proc_desc with | Some posts -> with_debug_exit_node proc_desc ~f:(fun () -> diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 4db8ba346..aa38cff7b 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -13,6 +13,7 @@ module BaseDomain = PulseBaseDomain module BaseStack = PulseBaseStack module BaseMemory = PulseBaseMemory module BaseAddressAttributes = PulseBaseAddressAttributes +module UninitBlocklist = PulseUninitBlocklist (** signature common to the "normal" [Domain], representing the post at the current program point, and the inverted [PreDomain], representing the inferred pre-condition*) @@ -220,12 +221,26 @@ module AddressAttributes = struct (** if [address] is in [pre] then add the attribute [attr] *) let abduce_attribute address attribute astate = - L.d_printfln "Abducing %a:%a" AbstractValue.pp address Attribute.pp attribute ; + let is_must_be_initialized_on_written = + match (attribute : Attribute.t) with + | MustBeInitialized _ -> + BaseAddressAttributes.find_opt address (astate.post :> base_domain).attrs + |> Option.exists ~f:(fun attrs -> Attributes.get_written_to attrs |> Option.is_some) + | _ -> + false + in let new_pre = - if BaseMemory.mem address (astate.pre :> base_domain).heap then - PreDomain.update astate.pre - ~attrs:(BaseAddressAttributes.add_one address attribute (astate.pre :> base_domain).attrs) - else astate.pre + if is_must_be_initialized_on_written then ( + L.d_printfln "No abducing %a:%a, the address has been written" AbstractValue.pp address + Attribute.pp attribute ; + astate.pre ) + else ( + L.d_printfln "Abducing %a:%a" AbstractValue.pp address Attribute.pp attribute ; + if BaseMemory.mem address (astate.pre :> base_domain).heap then + PreDomain.update astate.pre + ~attrs: + (BaseAddressAttributes.add_one address attribute (astate.pre :> base_domain).attrs) + else astate.pre ) in if phys_equal new_pre astate.pre then astate else {astate with pre= new_pre} @@ -312,7 +327,9 @@ module AddressAttributes = struct let astate = if Attribute.is_suitable_for_pre attr then abduce_attribute value attr astate else astate in - let astate = add_one value attr astate in + let astate = + if Attribute.is_suitable_for_post attr then add_one value attr astate else astate + in match attr with Attribute.WrittenTo _ -> initialize value astate | _ -> astate ) @@ -430,28 +447,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) = +let add_edge_on_src src location stack = + match src with + | `LocalDecl (pvar, addr_opt) -> ( + match addr_opt with + | None -> + let addr = AbstractValue.mk_fresh () in + let history = [ValueHistory.VariableDeclared (pvar, location)] in + (BaseStack.add (Var.of_pvar pvar) (addr, history) stack, addr) + | Some addr -> + (stack, addr) ) + | `Malloc addr -> + (stack, addr) + + +let rec set_uninitialized_post tenv src typ location (post : PostDomain.t) = match typ.Typ.desc with | Tint _ | Tfloat _ | Tptr _ -> let {stack; attrs} = (post :> base_domain) in - let stack, addr = - match src with - | `LocalDecl (pvar, addr_opt) -> ( - match addr_opt with - | None -> - let addr = AbstractValue.mk_fresh () in - let history = [ValueHistory.VariableDeclared (pvar, location)] in - (BaseStack.add (Var.of_pvar pvar) (addr, history) stack, addr) - | Some addr -> - (stack, addr) ) - | `Malloc addr -> - (stack, addr) - in + let stack, addr = add_edge_on_src src location stack in let attrs = BaseAddressAttributes.add_one addr Uninitialized attrs in PostDomain.update ~stack ~attrs post - | Tstruct _ -> - (* TODO: set uninitialized attributes for fields *) + | Tstruct typ_name when UninitBlocklist.is_blocklisted_struct typ_name -> post + | Tstruct (CUnion _) | Tstruct (CppClass {is_union= true}) -> + (* Ignore union fields in the uninitialized checker *) + post + | Tstruct _ -> ( + match Typ.name typ |> Option.bind ~f:(Tenv.lookup tenv) with + | None | Some {fields= [_]} -> + (* Ignore single field structs: see D26146578 *) + post + | Some {fields} -> + List.fold fields ~init:post ~f:(fun (acc : PostDomain.t) (field, field_typ, _) -> + if Fieldname.is_internal field then acc + else + let {stack; heap} = (acc :> base_domain) in + let stack, addr = add_edge_on_src src location stack in + let field_addr = AbstractValue.mk_fresh () in + let history = [ValueHistory.StructFieldAddressCreated (field, location)] in + let heap = + BaseMemory.add_edge addr (HilExp.Access.FieldAccess field) (field_addr, history) + heap + in + PostDomain.update ~stack ~heap acc + |> set_uninitialized_post tenv (`Malloc field_addr) field_typ location ) ) | Tarray _ -> (* TODO: set uninitialized attributes for elements *) post @@ -460,11 +500,11 @@ let set_uninitialized_post src typ location (post : PostDomain.t) = post -let set_uninitialized src typ location x = - {x with post= set_uninitialized_post src typ location x.post} +let set_uninitialized tenv src typ location x = + {x with post= set_uninitialized_post tenv src typ location x.post} -let mk_initial proc_desc = +let mk_initial tenv 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 @@ -524,7 +564,7 @@ let mk_initial proc_desc = let locals = Procdesc.get_locals proc_desc 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 ) + set_uninitialized_post tenv (`LocalDecl (Pvar.mk name proc_name, None)) typ location acc ) in { pre ; post diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 7930b8c4b..a861d82cc 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -81,7 +81,7 @@ val pp : Format.formatter -> t -> unit val set_isl_status : isl_status -> t -> t -val mk_initial : Procdesc.t -> t +val mk_initial : Tenv.t -> Procdesc.t -> t val get_pre : t -> BaseDomain.t @@ -212,7 +212,8 @@ val initialize : AbstractValue.t -> t -> t (** Remove "Uninitialized" attribute of the given address *) val set_uninitialized : - [ `LocalDecl of Pvar.t * AbstractValue.t option + Tenv.t + -> [ `LocalDecl of Pvar.t * AbstractValue.t option (** the second optional parameter is for the address of the variable *) | `Malloc of AbstractValue.t (** the address parameter is a newly allocated address *) ] -> Typ.t diff --git a/infer/src/pulse/PulseAttribute.ml b/infer/src/pulse/PulseAttribute.ml index 2b786ced4..61e732b5f 100644 --- a/infer/src/pulse/PulseAttribute.ml +++ b/infer/src/pulse/PulseAttribute.ml @@ -270,6 +270,23 @@ let is_suitable_for_pre = function false +let is_suitable_for_post = function + | MustBeInitialized _ | MustBeValid _ -> + false + | Invalid _ + | Allocated _ + | ISLAbduced _ + | AddressOfCppTemporary _ + | AddressOfStackVariable _ + | Closure _ + | DynamicType _ + | EndOfCollection + | StdVectorReserve + | Uninitialized + | WrittenTo _ -> + true + + let map_trace ~f = function | Allocated (procname, trace) -> Allocated (procname, f trace) diff --git a/infer/src/pulse/PulseAttribute.mli b/infer/src/pulse/PulseAttribute.mli index 309154ed8..3a07088af 100644 --- a/infer/src/pulse/PulseAttribute.mli +++ b/infer/src/pulse/PulseAttribute.mli @@ -31,6 +31,8 @@ val pp : F.formatter -> t -> unit val is_suitable_for_pre : t -> bool +val is_suitable_for_post : t -> bool + val map_trace : f:(Trace.t -> Trace.t) -> t -> t (** applies [f] to the traces found in attributes, leaving attributes without traces intact *) diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml index 7dbba75dd..cd5466a0a 100644 --- a/infer/src/pulse/PulseExecutionDomain.ml +++ b/infer/src/pulse/PulseExecutionDomain.ml @@ -28,7 +28,7 @@ type t = AbductiveDomain.t base_t let continue astate = ContinueProgram astate -let mk_initial pdesc = ContinueProgram (AbductiveDomain.mk_initial pdesc) +let mk_initial tenv pdesc = ContinueProgram (AbductiveDomain.mk_initial tenv pdesc) let leq ~lhs ~rhs = phys_equal lhs rhs diff --git a/infer/src/pulse/PulseExecutionDomain.mli b/infer/src/pulse/PulseExecutionDomain.mli index 972b113a5..20e4218dc 100644 --- a/infer/src/pulse/PulseExecutionDomain.mli +++ b/infer/src/pulse/PulseExecutionDomain.mli @@ -27,7 +27,7 @@ include AbstractDomain.NoJoin with type t := t val continue : AbductiveDomain.t -> t -val mk_initial : Procdesc.t -> t +val mk_initial : Tenv.t -> Procdesc.t -> t val is_unsat_cheap : t -> bool (** see {!PulsePathCondition.is_unsat_cheap} *) diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 3059338d7..e7316135e 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -86,7 +86,7 @@ module Misc = struct don't have the implementation. This triggers a bunch of heuristics, e.g. to havoc arguments we suspect are passed by reference. *) let unknown_call skip_reason args : model = - fun _ ~callee_procname location ~ret astate -> + fun {tenv} ~callee_procname location ~ret astate -> let actuals = List.map args ~f:(fun {ProcnameDispatcher.Call.FuncArg.arg_payload= actual; typ} -> (actual, typ) ) @@ -95,7 +95,7 @@ module Misc = struct AnalysisCallbacks.proc_resolve_attributes callee_procname |> Option.map ~f:ProcAttributes.get_pvar_formals in - PulseOperations.unknown_call location (Model skip_reason) ~ret ~actuals ~formals_opt astate + PulseOperations.unknown_call tenv location (Model skip_reason) ~ret ~actuals ~formals_opt astate |> ok_continue @@ -139,15 +139,15 @@ end module C = struct let free deleted_access : model = Misc.free_or_delete `Free deleted_access - let set_uninitialized size_exp_opt location ret_value astate = + let set_uninitialized tenv 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 ) ) + AbductiveDomain.set_uninitialized tenv (`Malloc ret_value) obj_typ location astate ) ) let malloc_common ~size_exp_opt : model = - fun _ ~callee_procname location ~ret:(ret_id, _) astate -> + fun {tenv} ~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}]) @@ -156,7 +156,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_addr + |> set_uninitialized tenv size_exp_opt location ret_addr in let result_null = let+ astate_null = @@ -169,7 +169,7 @@ module C = struct let malloc_not_null_common ~size_exp_opt : model = - fun _ ~callee_procname location ~ret:(ret_id, _) astate -> + fun {tenv} ~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}]) @@ -178,7 +178,7 @@ module C = struct let astate = PulseOperations.allocate callee_procname location ret_value astate |> PulseArithmetic.and_positive ret_addr - |> set_uninitialized size_exp_opt location ret_addr + |> set_uninitialized tenv size_exp_opt location ret_addr in ok_continue astate @@ -218,7 +218,7 @@ module ObjC = struct let dispatch_sync args : model = - fun {analyze_dependency; proc_desc} ~callee_procname:_ location ~ret astate -> + fun {analyze_dependency; proc_desc; tenv} ~callee_procname:_ location ~ret astate -> match List.last args with | None -> ok_continue astate @@ -230,7 +230,7 @@ module ObjC = struct | None -> ok_continue astate | Some callee_proc_name -> - PulseOperations.call ~caller_proc_desc:proc_desc + PulseOperations.call tenv ~caller_proc_desc:proc_desc ~callee_data:(analyze_dependency callee_proc_name) location callee_proc_name ~ret ~actuals:[] ~formals_opt:None astate ) end @@ -479,6 +479,11 @@ module StdAtomicInteger = struct let store_backing_int location this_address new_value astate = let* astate, this = PulseOperations.eval_access Read location this_address Dereference astate in + let astate = + AddressAttributes.add_one (fst this_address) + (WrittenTo (Trace.Immediate {location; history= []})) + astate + in let* astate, int_field = PulseOperations.eval_access Write location this (FieldAccess internal_int) astate in @@ -551,7 +556,7 @@ end module StdFunction = struct let operator_call ProcnameDispatcher.Call.FuncArg.{arg_payload= lambda_ptr_hist; typ} actuals : model = - fun {analyze_dependency; proc_desc} ~callee_procname:_ location ~ret astate -> + fun {analyze_dependency; proc_desc; tenv} ~callee_procname:_ location ~ret astate -> let havoc_ret (ret_id, _) astate = let event = ValueHistory.Call {f= Model "std::function::operator()"; location; in_call= []} in [PulseOperations.havoc_id ret_id [event] astate] @@ -570,7 +575,7 @@ module StdFunction = struct :: List.map actuals ~f:(fun ProcnameDispatcher.Call.FuncArg.{arg_payload; typ} -> (arg_payload, typ) ) in - PulseOperations.call ~caller_proc_desc:proc_desc + PulseOperations.call tenv ~caller_proc_desc:proc_desc ~callee_data:(analyze_dependency callee_proc_name) location callee_proc_name ~ret ~actuals ~formals_opt:None astate diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index ea5c07dab..b9b966ff0 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -315,12 +315,12 @@ let eval_deref_isl location exp astate = Ok (acc_astates @ [astate_addr]) ) -let realloc_pvar pvar typ location astate = +let realloc_pvar tenv 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 + AbductiveDomain.set_uninitialized tenv (`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 @@ -565,22 +565,36 @@ let is_ptr_to_const formal_typ_opt = match formal_typ.desc with Typ.Tptr (t, _) -> Typ.is_const t.quals | _ -> false ) -let unknown_call call_loc reason ~ret ~actuals ~formals_opt astate = +let unknown_call tenv call_loc reason ~ret ~actuals ~formals_opt astate = let event = ValueHistory.Call {f= reason; location= call_loc; in_call= []} in let havoc_ret (ret, _) astate = havoc_id ret [event] astate in + let rec havoc_fields ((_, history) as addr) typ astate = + match typ.Typ.desc with + | Tstruct struct_name -> ( + match Tenv.lookup tenv struct_name with + | Some {fields} -> + List.fold fields ~init:astate ~f:(fun acc (field, field_typ, _) -> + let fresh_value = AbstractValue.mk_fresh () in + Memory.add_edge addr (FieldAccess field) (fresh_value, [event]) call_loc acc + |> havoc_fields (fresh_value, history) field_typ ) + | None -> + astate ) + | _ -> + astate + in let havoc_actual_if_ptr (actual, actual_typ) formal_typ_opt astate = (* We should not havoc when the corresponding formal is a pointer to const *) - if - (not (Language.curr_language_is Java)) - && Typ.is_pointer actual_typ - && not (is_ptr_to_const formal_typ_opt) - then - (* HACK: write through the pointer even if it is invalid (except in Java). This is to avoid raising issues when - havoc'ing pointer parameters (which normally causes a [check_valid] call. *) - let fresh_value = AbstractValue.mk_fresh () in - Memory.add_edge actual Dereference (fresh_value, [event]) call_loc astate - else astate + match actual_typ.Typ.desc with + | Tptr (typ, _) + when (not (Language.curr_language_is Java)) && not (is_ptr_to_const formal_typ_opt) -> + (* HACK: write through the pointer even if it is invalid (except in Java). This is to avoid raising issues when + havoc'ing pointer parameters (which normally causes a [check_valid] call. *) + let fresh_value = AbstractValue.mk_fresh () in + Memory.add_edge actual Dereference (fresh_value, [event]) call_loc astate + |> havoc_fields actual typ + | _ -> + astate in let add_skipped_proc astate = match reason with @@ -683,7 +697,7 @@ let conservatively_initialize_args arg_values ({AbductiveDomain.post} as astate) AbstractValue.Set.fold AbductiveDomain.initialize reachable_values astate -let call ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.t) option) call_loc +let call tenv ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.t) option) call_loc callee_pname ~ret ~actuals ~formals_opt (astate : AbductiveDomain.t) = let get_arg_values () = List.map actuals ~f:(fun ((value, _), _) -> value) in match callee_data with @@ -743,6 +757,6 @@ let call ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.t) option) L.d_printfln "No spec found for %a@\n" Procname.pp callee_pname ; let astate = conservatively_initialize_args (get_arg_values ()) astate - |> unknown_call call_loc (SkippedKnownCall callee_pname) ~ret ~actuals ~formals_opt + |> unknown_call tenv call_loc (SkippedKnownCall callee_pname) ~ret ~actuals ~formals_opt in [Ok (ContinueProgram astate)] diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index fa3e7216f..b10a665e2 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -102,7 +102,7 @@ val havoc_field : -> t -> t access_result -val realloc_pvar : Pvar.t -> Typ.t -> Location.t -> t -> t +val realloc_pvar : Tenv.t -> Pvar.t -> Typ.t -> Location.t -> t -> t val write_id : Ident.t -> AbstractValue.t * ValueHistory.t -> t -> t @@ -185,7 +185,8 @@ val check_address_escape : Location.t -> Procdesc.t -> AbstractValue.t -> ValueHistory.t -> t -> t access_result val call : - caller_proc_desc:Procdesc.t + Tenv.t + -> caller_proc_desc:Procdesc.t -> callee_data:(Procdesc.t * PulseSummary.t) option -> Location.t -> Procname.t @@ -198,7 +199,8 @@ val call : it exists *) val unknown_call : - Location.t + Tenv.t + -> Location.t -> CallEvent.t -> ret:Ident.t * Typ.t -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list diff --git a/infer/src/pulse/PulseUninitBlocklist.ml b/infer/src/pulse/PulseUninitBlocklist.ml new file mode 100644 index 000000000..7bb54dd66 --- /dev/null +++ b/infer/src/pulse/PulseUninitBlocklist.ml @@ -0,0 +1,21 @@ +(* + * 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. + *) + +open! IStd + +let dispatch : (unit, unit, unit) ProcnameDispatcher.TypName.dispatcher = + let open ProcnameDispatcher.TypName in + make_dispatcher + [ -"folly" &:: "Optional" &::.*--> () + ; -"std" &:: "__wrap_iter" &::.*--> () + ; -"std" &:: "atomic" &::.*--> () + ; -"std" &:: "function" &::.*--> () + ; -"std" &:: "optional" &::.*--> () + ; -"std" &:: "vector" &::.*--> () ] + + +let is_blocklisted_struct typ_name = dispatch () typ_name |> Option.is_some diff --git a/infer/src/pulse/PulseUninitBlocklist.mli b/infer/src/pulse/PulseUninitBlocklist.mli new file mode 100644 index 000000000..519211d22 --- /dev/null +++ b/infer/src/pulse/PulseUninitBlocklist.mli @@ -0,0 +1,11 @@ +(* + * 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. + *) + +open! IStd + +val is_blocklisted_struct : Typ.name -> bool +(** Check if a struct name is in the blocklist for uninit checker. *) diff --git a/infer/src/pulse/PulseValueHistory.ml b/infer/src/pulse/PulseValueHistory.ml index 1f4e18b32..049f526df 100644 --- a/infer/src/pulse/PulseValueHistory.ml +++ b/infer/src/pulse/PulseValueHistory.ml @@ -16,6 +16,7 @@ type event = | Conditional of {is_then_branch: bool; if_kind: Sil.if_kind; location: Location.t} | CppTemporaryCreated of Location.t | FormalDeclared of Pvar.t * Location.t + | StructFieldAddressCreated of Fieldname.t * Location.t | VariableAccessed of Pvar.t * Location.t | VariableDeclared of Pvar.t * Location.t @@ -52,6 +53,8 @@ let pp_event_no_location fmt event = |> Option.iter ~f:(fun proc_name -> F.fprintf fmt " of %a" Procname.pp proc_name) in F.fprintf fmt "parameter `%a`%a" Pvar.pp_value_non_verbose pvar pp_proc pvar + | StructFieldAddressCreated (field_name, _) -> + F.fprintf fmt "struct field address `%a` created" Fieldname.pp field_name | VariableAccessed (pvar, _) -> F.fprintf fmt "%a accessed here" pp_pvar pvar | VariableDeclared (pvar, _) -> @@ -66,6 +69,7 @@ let location_of_event = function | Conditional {location} | CppTemporaryCreated location | FormalDeclared (_, location) + | StructFieldAddressCreated (_, location) | VariableAccessed (_, location) | VariableDeclared (_, location) -> location diff --git a/infer/src/pulse/PulseValueHistory.mli b/infer/src/pulse/PulseValueHistory.mli index 3e9c02103..67abe4b22 100644 --- a/infer/src/pulse/PulseValueHistory.mli +++ b/infer/src/pulse/PulseValueHistory.mli @@ -16,6 +16,7 @@ type event = | Conditional of {is_then_branch: bool; if_kind: Sil.if_kind; location: Location.t} | CppTemporaryCreated of Location.t | FormalDeclared of Pvar.t * Location.t + | StructFieldAddressCreated of Fieldname.t * Location.t | VariableAccessed of Pvar.t * Location.t | VariableDeclared of Pvar.t * Location.t diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp index f27909aef..bc47dfc8f 100644 --- a/infer/tests/codetoanalyze/c/pulse/issues.exp +++ b/infer/tests/codetoanalyze/c/pulse/issues.exp @@ -12,6 +12,7 @@ codetoanalyze/c/pulse/uninit.c, call_to_use_and_mayinit_bad, 2, PULSE_UNINITIALI codetoanalyze/c/pulse/uninit.c, dereference_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `p` declared here,read to uninitialized value occurs here] codetoanalyze/c/pulse/uninit.c, interprocedural_nop_in_callee_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `x` declared here,read to uninitialized value occurs here] codetoanalyze/c/pulse/uninit.c, interprocedural_read_in_callee_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `x` declared here,when calling `read_int_ref` here,parameter `p` of read_int_ref,read to uninitialized value occurs here] +codetoanalyze/c/pulse/uninit.c, interprocedural_struct_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `f2` created,read to uninitialized value occurs here] codetoanalyze/c/pulse/uninit.c, interprocedural_uninit_in_callee_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [passed as argument to `uninit`,return from call to `uninit`,assigned,read to uninitialized value occurs here] codetoanalyze/c/pulse/uninit.c, malloc_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [allocated by call to `malloc` (modelled),assigned,read to uninitialized value occurs here] codetoanalyze/c/pulse/uninit.c, self_assign_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `x` declared here,read to uninitialized value occurs here] diff --git a/infer/tests/codetoanalyze/c/pulse/uninit.c b/infer/tests/codetoanalyze/c/pulse/uninit.c index 83ea6e2b5..f8f26fccf 100644 --- a/infer/tests/codetoanalyze/c/pulse/uninit.c +++ b/infer/tests/codetoanalyze/c/pulse/uninit.c @@ -86,7 +86,13 @@ void get_field_address_good() { void init_f1(struct uninit_s* p) { p->f1 = 5; } -void interprocedural_struct_bad_FN() { +void interprocedural_struct_good() { + struct uninit_s s; + init_f1(&s); + int y = s.f1; +} + +void interprocedural_struct_bad() { struct uninit_s s; init_f1(&s); int y = s.f2; @@ -99,3 +105,14 @@ void malloc_array_good(int len) { } free(o); } + +struct uninit_s unknown_struct(); + +struct uninit_s unknown_wrapper() { + return unknown_struct(); +} + +void havoc_calling_unknown_struct_good() { + struct uninit_s x = unknown_wrapper(); + int y = x.f1; +} diff --git a/infer/tests/codetoanalyze/cpp/pulse/fbstring.cpp b/infer/tests/codetoanalyze/cpp/pulse/fbstring.cpp index dc8f0cc38..34cd2be34 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/fbstring.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/fbstring.cpp @@ -32,7 +32,7 @@ struct LikeFBString { size_t size_; unsigned int* refcount_; - LikeFBString() {} + LikeFBString() { category_ = 0; } LikeFBString(const LikeFBString& src) { category_ = src.category(); diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 3ae733fb2..35a37dece 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -95,6 +95,7 @@ codetoanalyze/cpp/pulse/std_atomics.cpp, atomic_test::load_store_possible_npe_ba codetoanalyze/cpp/pulse/std_atomics.cpp, atomic_test::pre_increment_decrement_test_bad, 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/cpp/pulse/temporaries.cpp, temporaries::call_mk_UniquePtr_A_deref_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `temporaries::mk_UniquePtr_A`,passed as argument to `new` (modelled),return from call to `new` (modelled),passed as argument to `temporaries::UniquePtr::UniquePtr`,parameter `y` of temporaries::UniquePtr::UniquePtr,assigned,return from call to `temporaries::UniquePtr::UniquePtr`,return from call to `temporaries::mk_UniquePtr_A`,when calling `temporaries::UniquePtr::~UniquePtr` here,parameter `this` of temporaries::UniquePtr::~UniquePtr,when calling `temporaries::UniquePtr::__infer_inner_destructor_~UniquePtr` here,parameter `this` of temporaries::UniquePtr::__infer_inner_destructor_~UniquePtr,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `temporaries::mk_UniquePtr_A`,passed as argument to `new` (modelled),return from call to `new` (modelled),passed as argument to `temporaries::UniquePtr::UniquePtr`,parameter `y` of temporaries::UniquePtr::UniquePtr,assigned,return from call to `temporaries::UniquePtr::UniquePtr`,return from call to `temporaries::mk_UniquePtr_A`,passed as argument to `temporaries::UniquePtr::get`,return from call to `temporaries::UniquePtr::get`,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/trace.cpp, trace_free_bad, 4, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of trace_free_bad,passed as argument to `make_alias`,parameter `src` of make_alias,assigned,return from call to `make_alias`,when calling `do_free` here,parameter `x` of do_free,assigned,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of trace_free_bad,invalid access occurs here] +codetoanalyze/cpp/pulse/uninit.cpp, Uninit::call_init_by_store_ok, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `i` created,read to uninitialized value occurs here] codetoanalyze/cpp/pulse/unknown_functions.cpp, call_init_with_pointer_value_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/unknown_functions.cpp, const_no_init_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_latent, 5, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/uninit.cpp b/infer/tests/codetoanalyze/cpp/pulse/uninit.cpp new file mode 100644 index 000000000..bdfb5c1ba --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/pulse/uninit.cpp @@ -0,0 +1,36 @@ +/* + * 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 +#include + +void get_closure(std::function closure); + +class Uninit { + void closure_call_ok() { + auto closure = [this]() { return 5; }; + get_closure(closure); + } + + class MyClass { + public: + int i; + int j; + }; + + void init_by_store(MyClass* x) { + MyClass y{3, 5}; + reinterpret_cast*>(x)->store( + y, std::memory_order_release); + } + + void call_init_by_store_ok() { + MyClass x; + init_by_store(&x); + int y = x.i; + } +};