diff --git a/infer/src/IR/HilExp.mli b/infer/src/IR/HilExp.mli index 04f9b6c7a..bba7be2a8 100644 --- a/infer/src/IR/HilExp.mli +++ b/infer/src/IR/HilExp.mli @@ -54,6 +54,8 @@ module AccessExpression : sig [@@warning "-32"] (** address_of doesn't always make sense, eg [address_of (Dereference t)] is [None] *) + val address_of_base : AccessPath.base -> access_expression + val to_accesses_fold : access_expression -> init:'accum diff --git a/infer/src/IR/Var.ml b/infer/src/IR/Var.ml index 2235f3e36..4acc69131 100644 --- a/infer/src/IR/Var.ml +++ b/infer/src/IR/Var.ml @@ -40,8 +40,6 @@ let is_global = function ProgramVar pvar -> Pvar.is_global pvar | LogicalVar _ - let is_return = function ProgramVar pvar -> Pvar.is_return pvar | LogicalVar _ -> false -let is_this = function ProgramVar pvar -> Pvar.is_this pvar | LogicalVar _ -> false - let is_footprint = function ProgramVar _ -> false | LogicalVar id -> Ident.is_footprint id let is_none = function LogicalVar id -> Ident.is_none id | _ -> false diff --git a/infer/src/IR/Var.mli b/infer/src/IR/Var.mli index e67203378..3f975d26b 100644 --- a/infer/src/IR/Var.mli +++ b/infer/src/IR/Var.mli @@ -37,9 +37,6 @@ val is_local_to_procedure : Typ.Procname.t -> t -> bool val is_return : t -> bool -val is_this : t -> bool -(** return whether the var is the special "this" var *) - val is_footprint : t -> bool val is_none : t -> bool diff --git a/infer/src/backend/Payloads.ml b/infer/src/backend/Payloads.ml index 42c8abcec..b0ae3e3b4 100644 --- a/infer/src/backend/Payloads.ml +++ b/infer/src/backend/Payloads.ml @@ -17,6 +17,7 @@ type t = ; cost: CostDomain.summary option ; lab_resource_leaks: ResourceLeakDomain.summary option ; litho: LithoDomain.t option + ; pulse: PulseSummary.t option ; purity: PurityDomain.summary option ; quandary: QuandarySummary.t option ; racerd: RacerDDomain.summary option @@ -34,6 +35,7 @@ let pp pe fmt ; cost ; lab_resource_leaks ; litho + ; pulse ; purity ; quandary ; racerd @@ -47,7 +49,7 @@ let pp pe fmt | None -> () in - F.fprintf fmt "%a%a%a%a%a%a%a%a%a%a%a%a%a%a%a@\n" + F.fprintf fmt "%a%a%a%a%a%a%a%a%a%a%a%a%a%a%a%a@\n" (pp_opt "AnnotationReachability" AnnotReachabilityDomain.pp) annot_map (pp_opt "Biabduction" (BiabductionSummary.pp pe)) @@ -59,7 +61,7 @@ let pp pe fmt (pp_opt "ClassLoads" ClassLoadsDomain.pp_summary) class_loads (pp_opt "Cost" CostDomain.pp_summary) - cost (pp_opt "Litho" LithoDomain.pp) litho + cost (pp_opt "Litho" LithoDomain.pp) litho (pp_opt "Pulse" PulseSummary.pp) pulse (pp_opt "Purity" PurityDomain.pp_summary) purity (pp_opt "Quandary" QuandarySummary.pp) @@ -85,6 +87,7 @@ let empty = ; cost= None ; lab_resource_leaks= None ; litho= None + ; pulse= None ; purity= None ; quandary= None ; racerd= None diff --git a/infer/src/backend/Payloads.mli b/infer/src/backend/Payloads.mli index c3d70258c..2e52c85e5 100644 --- a/infer/src/backend/Payloads.mli +++ b/infer/src/backend/Payloads.mli @@ -17,6 +17,7 @@ type t = ; cost: CostDomain.summary option ; lab_resource_leaks: ResourceLeakDomain.summary option ; litho: LithoDomain.t option + ; pulse: PulseSummary.t option ; purity: PurityDomain.summary option ; quandary: QuandarySummary.t option ; racerd: RacerDDomain.summary option diff --git a/infer/src/istd/IList.ml b/infer/src/istd/IList.ml index dd9ed16f8..74ebdb1ff 100644 --- a/infer/src/istd/IList.ml +++ b/infer/src/istd/IList.ml @@ -194,3 +194,8 @@ let pp_print_list ~max ?(pp_sep = Format.pp_print_cut) pp_v ppf = aux (n + 1) rest ) in function [] -> () | [v] -> pp_v ppf v | v :: rest -> pp_v ppf v ; aux 1 rest + + +let fold2_result ~init ~f l1 l2 = + List.fold2 l1 l2 ~init:(Ok init) ~f:(fun result x1 x2 -> + Result.bind result ~f:(fun acc -> f acc x1 x2) ) diff --git a/infer/src/istd/IList.mli b/infer/src/istd/IList.mli index 4419325d2..61d519ac1 100644 --- a/infer/src/istd/IList.mli +++ b/infer/src/istd/IList.mli @@ -53,3 +53,10 @@ val pp_print_list : -> Format.formatter -> 'a list -> unit + +val fold2_result : + init:'acc + -> f:('acc -> 'a -> 'b -> ('acc, 'err) result) + -> 'a list + -> 'b list + -> ('acc, 'err) result Base.List.Or_unequal_lengths.t diff --git a/infer/src/istd/Pp.ml b/infer/src/istd/Pp.ml index 9722602e6..4070df03c 100644 --- a/infer/src/istd/Pp.ml +++ b/infer/src/istd/Pp.ml @@ -173,3 +173,5 @@ let cli_args fmt args = let pair ~fst ~snd fmt (a, b) = F.fprintf fmt "(%a,@,%a)" fst a snd b + +let in_backticks pp fmt x = F.fprintf fmt "`%a`" pp x diff --git a/infer/src/istd/Pp.mli b/infer/src/istd/Pp.mli index 5b8edcf99..ceadd3ff3 100644 --- a/infer/src/istd/Pp.mli +++ b/infer/src/istd/Pp.mli @@ -100,3 +100,5 @@ val pair : -> F.formatter -> 'a * 'b -> unit + +val in_backticks : (F.formatter -> 'a -> unit) -> F.formatter -> 'a -> unit diff --git a/infer/src/istd/PrettyPrintable.ml b/infer/src/istd/PrettyPrintable.ml index fa2aa14b8..31ef71864 100644 --- a/infer/src/istd/PrettyPrintable.ml +++ b/infer/src/istd/PrettyPrintable.ml @@ -119,6 +119,8 @@ end module type PPMap = sig include Caml.Map.S + val fold_map : 'a t -> init:'b -> f:('b -> 'a -> 'b * 'c) -> 'b * 'c t + val is_singleton_or_more : 'a t -> (key * 'a) IContainer.singleton_or_more val pp_key : F.formatter -> key -> unit @@ -147,6 +149,19 @@ end module MakePPMap (Ord : PrintableOrderedType) = struct include Caml.Map.Make (Ord) + let fold_map m ~init ~f = + let acc = ref init in + let new_map = + map + (fun value -> + let acc', res = f !acc value in + acc := acc' ; + res ) + m + in + (!acc, new_map) + + let is_singleton_or_more m = if is_empty m then IContainer.Empty else diff --git a/infer/src/istd/PrettyPrintable.mli b/infer/src/istd/PrettyPrintable.mli index 83e283783..40bfc6831 100644 --- a/infer/src/istd/PrettyPrintable.mli +++ b/infer/src/istd/PrettyPrintable.mli @@ -121,6 +121,8 @@ end module type PPMap = sig include Caml.Map.S + val fold_map : 'a t -> init:'b -> f:('b -> 'a -> 'b * 'c) -> 'b * 'c t + val is_singleton_or_more : 'a t -> (key * 'a) IContainer.singleton_or_more val pp_key : F.formatter -> key -> unit diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 60db49ec5..bd8c2e614 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -37,6 +37,14 @@ let check_error summary = function raise_notrace AbstractDomain.Stop_analysis +module Payload = SummaryPayload.Make (struct + type t = PulseSummary.t + + let update_payloads astate (payloads : Payloads.t) = {payloads with pulse= Some astate} + + let of_payloads (payloads : Payloads.t) = payloads.pulse +end) + module PulseTransferFunctions = struct module CFG = ProcCfg.Exceptional module Domain = PulseAbductiveDomain @@ -80,25 +88,13 @@ module PulseTransferFunctions = struct >>= PulseOperations.havoc [crumb] loc lhs_access - let exec_call summary _ret (call : HilInstr.call) (actuals : HilExp.t list) _flags call_loc - astate = + let exec_unknown_call summary _ret (call : HilInstr.call) (actuals : HilExp.t list) _flags + call_loc astate = let read_all args astate = PulseOperations.read_all call_loc (List.concat_map args ~f:HilExp.get_access_exprs) astate in let crumb = PulseTrace.Call {f= `HilCall call; actuals; location= call_loc} in match call with - | Direct callee_pname when is_destructor callee_pname -> ( - match actuals with - | [AccessExpression (Base (destroyed_var, _))] when Var.is_this destroyed_var -> - (* do not invalidate [this] when it is destroyed by calls to [this->~Obj()] *) - Ok astate - | [AccessExpression destroyed_access] -> - let destroyed_object = HilExp.AccessExpression.dereference destroyed_access in - PulseOperations.invalidate - (CppDestructor (callee_pname, destroyed_object, call_loc)) - call_loc destroyed_object astate - | _ -> - Ok astate ) | Direct callee_pname when Typ.Procname.is_constructor callee_pname -> ( L.d_printfln "constructor call detected@." ; match actuals with @@ -129,6 +125,54 @@ module PulseTransferFunctions = struct read_all actuals astate + let interprocedural_call caller_summary ret (call : HilInstr.call) (actuals : HilExp.t list) + flags call_loc astate = + let unknown_function () = + exec_unknown_call caller_summary ret call actuals flags call_loc astate >>| List.return + in + match call with + | Direct callee_pname -> ( + match Payload.read_full caller_summary.Summary.proc_desc callee_pname with + | Some (callee_proc_desc, preposts) -> + let formals = + Procdesc.get_formals callee_proc_desc + |> List.map ~f:(fun (mangled, _) -> Pvar.mk mangled callee_pname |> Var.of_pvar) + in + PulseOperations.Interproc.call callee_pname ~formals ~ret ~actuals flags call_loc astate + preposts + | None -> + (* no spec found for some reason (unknown function, ...) *) + L.d_printfln "No spec found for %a@\n" Typ.Procname.pp callee_pname ; + unknown_function () ) + | Indirect access_expression -> + L.d_printfln "Indirect call %a@\n" HilExp.AccessExpression.pp access_expression ; + unknown_function () + + + (** has an object just gone out of scope? *) + let get_destructed_object (call : HilInstr.call) (actuals : HilExp.t list) (flags : CallFlags.t) + = + (* injected destructors are precisely inserted where an object goes out of scope *) + if flags.cf_injected_destructor then + match (call, actuals) with + | Direct callee_pname, [AccessExpression destroyed_access] when is_destructor callee_pname -> + Some (callee_pname, destroyed_access) + | _ -> + None + else None + + + (** [destroyed_access_expr] has just gone out of scope and in now invalid *) + let destruct_object callee_pname call_loc destroyed_access_expr astate = + let destroyed_object = HilExp.AccessExpression.dereference destroyed_access_expr in + (* TODO: need an [OutOfScope] invalidation reason instead of [CppDestructor]? *) + PulseOperations.invalidate + (PulseTrace.Immediate + { imm= PulseInvalidation.CppDestructor (callee_pname, destroyed_object, call_loc) + ; location= call_loc }) + call_loc destroyed_object astate + + let dispatch_call summary ret (call : HilInstr.call) (actuals : HilExp.t list) flags call_loc astate = let model = @@ -140,13 +184,23 @@ module PulseTransferFunctions = struct PulseModels.dispatch callee_pname flags in match model with - | None -> - exec_call summary ret call actuals flags call_loc astate - >>| PulseOperations.havoc_var - [PulseTrace.Call {f= `HilCall call; actuals; location= call_loc}] - (fst ret) | Some model -> - model call_loc ~ret ~actuals astate + model call_loc ~ret ~actuals astate >>| fun post -> [post] + | None -> ( + (* do interprocedural call then destroy objects going out of scope *) + PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse interproc call" ())) ; + let posts = interprocedural_call summary ret call actuals flags call_loc astate in + PerfEvent.(log (fun logger -> log_end_event logger ())) ; + match get_destructed_object call actuals flags with + | Some (destructor_pname, access_expr) -> + L.d_printfln "%a is going out of scope" HilExp.AccessExpression.pp access_expr ; + posts + >>= fun posts -> + List.map posts ~f:(fun astate -> + destruct_object destructor_pname call_loc access_expr astate ) + |> Result.all + | None -> + posts ) let exec_instr (astate : Domain.t) {ProcData.extras= summary} _cfg_node (instr : HilInstr.t) = @@ -161,10 +215,10 @@ module PulseTransferFunctions = struct in [post] | Call (ret, call, actuals, flags, loc) -> - let post = + let posts = dispatch_call summary ret call actuals flags loc astate |> check_error summary in - [post] + posts | Metadata (ExitScope (vars, _)) -> let post = PulseOperations.remove_vars vars astate in [post] @@ -202,9 +256,15 @@ module DisjunctiveAnalyzer = let checker {Callbacks.proc_desc; tenv; summary} = let proc_data = ProcData.make proc_desc tenv summary in AbstractAddress.init () ; - ( try - ignore - (DisjunctiveAnalyzer.compute_post proc_data - ~initial:(DisjunctiveTransferFunctions.Disjuncts.singleton PulseAbductiveDomain.empty)) - with AbstractDomain.Stop_analysis -> () ) ; - summary + match + DisjunctiveAnalyzer.compute_post proc_data + ~initial:(DisjunctiveTransferFunctions.Disjuncts.singleton PulseAbductiveDomain.empty) + with + | Some posts -> + Payload.update_summary + (PulseSummary.of_posts (DisjunctiveTransferFunctions.Disjuncts.elements posts)) + summary + | None -> + summary + | exception AbstractDomain.Stop_analysis -> + summary diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 7637a0c2f..f532fb50c 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -6,6 +6,7 @@ *) open! IStd module F = Format +module L = Logging module AbstractAddress = PulseDomain.AbstractAddress module Attributes = PulseDomain.Attributes module BaseStack = PulseDomain.Stack @@ -140,20 +141,20 @@ module Memory = struct (** if [address] is in [pre] and it should be valid then that fact goes in the precondition *) - let record_must_be_valid actor address (pre : InvertedDomain.t) = + let record_must_be_valid action address (pre : InvertedDomain.t) = if BaseMemory.mem_edges address (pre :> base_domain).heap then InvertedDomain.update pre ~heap: (BaseMemory.add_attributes address - (Attributes.singleton (MustBeValid actor)) + (Attributes.singleton (MustBeValid action)) (pre :> base_domain).heap) else pre - let check_valid actor addr ({post; pre} as astate) = + let check_valid action addr ({post; pre} as astate) = BaseMemory.check_valid addr (post :> base_domain).heap >>| fun () -> - let new_pre = record_must_be_valid actor addr pre in + let new_pre = record_must_be_valid action addr pre in if phys_equal new_pre pre then astate else {astate with pre= new_pre} @@ -188,8 +189,8 @@ module Memory = struct , addr_trace' ) - let invalidate address actor astate = - map_post_heap astate ~f:(fun heap -> BaseMemory.invalidate address actor heap) + let invalidate address action astate = + map_post_heap astate ~f:(fun heap -> BaseMemory.invalidate address action heap) let add_attributes address attributes astate = @@ -235,3 +236,396 @@ let discard_unreachable ({pre; post} as astate) = else { pre= InvertedDomain.make (pre :> PulseDomain.t).stack pre_new_heap ; post= Domain.make (post :> PulseDomain.t).stack post_new_heap } + + +module PrePost = struct + type domain_t = t + + type t = domain_t + + let of_post astate = discard_unreachable astate + + (* machinery to apply a pre/post pair corresponding to a function's summary in a function call to + the current state *) + + module AddressSet = PulseDomain.AbstractAddressSet + module AddressMap = PulseDomain.AbstractAddressMap + + (** raised when the pre/post pair and the current state disagree on the aliasing, i.e. some + addresses that are distinct in the pre/post are aliased in the current state. Typically raised + when calling [foo(z,z)] where the spec for [foo(x,y)] says that [x] and [y] are disjoint. *) + exception Aliasing + + (** stuff we carry around when computing the result of applying one pre/post pair *) + type call_state = + { astate: t (** caller's abstract state computed so far *) + ; subst: AbstractAddress.t AddressMap.t + (** translation from callee addresses to caller addresses *) + ; rev_subst: AbstractAddress.t AddressMap.t + (** the inverse translation from [subst] from caller addresses to callee addresses *) + ; visited: AddressSet.t + (** set of callee addresses that have been visited already + + NOTE: this is not always equal to the domain of [rev_subst]: when applying the post + we visit each subgraph from each formal independently so we reset [visited] between + the visit of each formal *) + } + + let pp_call_state fmt {astate; subst; rev_subst; visited} = + F.fprintf fmt + "@[{ astate=@[%a@];@, subst=@[%a@];@, rev_subst=@[%a@];@, \ + visited=@[%a@]@, }@]" + pp astate + (AddressMap.pp ~pp_value:AbstractAddress.pp) + subst + (AddressMap.pp ~pp_value:AbstractAddress.pp) + rev_subst AddressSet.pp visited + + + let visit call_state ~addr_callee ~addr_caller = + ( match AddressMap.find_opt addr_caller call_state.rev_subst with + | Some addr_callee' when not (AbstractAddress.equal addr_callee addr_callee') -> + L.d_printfln "Huho, address %a in post already bound to %a, not %a@\nState=%a" + AbstractAddress.pp addr_caller AbstractAddress.pp addr_callee' AbstractAddress.pp + addr_callee pp_call_state call_state ; + raise Aliasing + | _ -> + () ) ; + if AddressSet.mem addr_callee call_state.visited then (`AlreadyVisited, call_state) + else + ( `NotAlreadyVisited + , { call_state with + visited= AddressSet.add addr_callee call_state.visited + ; subst= AddressMap.add addr_callee addr_caller call_state.subst + ; rev_subst= AddressMap.add addr_caller addr_callee call_state.rev_subst } ) + + + let pp f {pre; post} = + F.fprintf f "PRE:@\n @[%a@]@\n" PulseDomain.pp (pre :> PulseDomain.t) ; + F.fprintf f "POST:@\n @[%a@]@\n" PulseDomain.pp (post :> PulseDomain.t) + + + (* reading the pre from the current state *) + + (** Materialize the (abstract memory) subgraph of [pre] reachable from [addr_pre] in + [call_state.astate] starting from address [addr_caller]. Report an error if some invalid + addresses are traversed in the process. *) + let rec materialize_pre_from_address callee_proc_name call_location ~pre ~addr_pre ~addr_caller + trace call_state = + let mk_action action = + PulseTrace.ViaCall {action; proc_name= callee_proc_name; location= call_location} + in + match visit call_state ~addr_callee:addr_pre ~addr_caller with + | `AlreadyVisited, call_state -> + Ok call_state + | `NotAlreadyVisited, call_state -> ( + (let open Option.Monad_infix in + PulseDomain.Memory.find_opt addr_pre pre.PulseDomain.heap + >>= fun (edges_pre, attrs_pre) -> + PulseDomain.Attributes.get_must_be_valid attrs_pre + >>| fun callee_action -> + let action = mk_action callee_action in + match Memory.check_valid action addr_caller call_state.astate with + | Error invalidated_by -> + Error + (PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= action; trace}) + | Ok astate -> + let call_state = {call_state with astate} in + Container.fold_result + ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold) + ~init:call_state edges_pre ~f:(fun call_state (access, (addr_pre_dest, _)) -> + let astate, (addr_caller_dest, _) = + Memory.materialize_edge addr_caller access call_state.astate + in + let call_state = {call_state with astate} in + materialize_pre_from_address callee_proc_name call_location ~pre + ~addr_pre:addr_pre_dest ~addr_caller:addr_caller_dest trace call_state )) + |> function Some result -> result | None -> Ok call_state ) + + + (** materialize subgraph of [pre] rooted at the address represented by a [formal] parameter that + has been instantiated with the corresponding [actual] into the current state + [call_state.astate] *) + let materialize_pre_from_actual callee_proc_name call_location ~pre ~formal ~actual call_state = + L.d_printfln "Materializing PRE from [%a <- %a]" Var.pp formal (Pp.option AbstractAddress.pp) + (Option.map ~f:fst actual) ; + match actual with + | None -> + (* the expression representing the actual couldn't be evaluated down to an abstract address + *) + Ok call_state + | Some (addr_caller, trace) -> ( + (let open Option.Monad_infix in + PulseDomain.Stack.find_opt formal pre.PulseDomain.stack + >>= fun (addr_formal_pre, _) -> + PulseDomain.Memory.find_edge_opt addr_formal_pre Dereference pre.PulseDomain.heap + >>| fun (formal_pre, _) -> + materialize_pre_from_address callee_proc_name call_location ~pre ~addr_pre:formal_pre + ~addr_caller trace call_state) + |> function Some result -> result | None -> Ok call_state ) + + + let is_cell_read_only ~cell_pre_opt ~cell_post:(edges_post, attrs_post) = + match cell_pre_opt with + | None -> + false + | Some (edges_pre, _) -> + Attributes.is_empty attrs_post + && PulseDomain.Memory.Edges.equal + (fun (addr_dest_pre, _) (addr_dest_post, _) -> + (* NOTE: ignores traces + + TODO: can the traces be leveraged here? maybe easy to detect writes by looking at + the post trace *) + AbstractAddress.equal addr_dest_pre addr_dest_post ) + edges_pre edges_post + + + let materialize_pre callee_proc_name call_location pre_post ~formals ~actuals call_state = + (* For each [(formal, actual)] pair, resolve them to addresses in their respective states then + call [materialize_pre_from] on them. Give up if calling the function introduces aliasing. + *) + match + PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call pre" ())) ; + let r = + IList.fold2_result formals actuals ~init:call_state ~f:(fun call_state formal actual -> + materialize_pre_from_actual callee_proc_name call_location + ~pre:(pre_post.pre :> PulseDomain.t) + ~formal ~actual call_state ) + in + PerfEvent.(log (fun logger -> log_end_event logger ())) ; + r + with + | Ok result -> + Some result + | Unequal_lengths -> + L.d_printfln "ERROR: formals have length %d but actuals have length %d" + (List.length formals) (List.length actuals) ; + None + | exception Aliasing -> + (* can't make sense of the pre-condition in the current context: give up on that particular + pre/post pair *) + None + + + (* applying the post to the current state *) + + let subst_find_or_new subst addr_callee = + match AddressMap.find_opt addr_callee subst with + | None -> + let addr_fresh = AbstractAddress.mk_fresh () in + (addr_fresh, AddressMap.add addr_callee addr_fresh subst) + | Some addr_caller -> + (addr_caller, subst) + + + let call_state_subst_find_or_new call_state addr_callee = + let addr_caller, new_subst = subst_find_or_new call_state.subst addr_callee in + if phys_equal new_subst call_state.subst then (call_state, addr_caller) + else ({call_state with subst= new_subst}, addr_caller) + + + let delete_edges_in_callee_pre_from_caller ~addr_callee:_ ~cell_pre_opt ~addr_caller call_state = + match + PulseDomain.Memory.find_edges_opt addr_caller (call_state.astate.post :> base_domain).heap + with + | None -> + PulseDomain.Memory.Edges.empty + | Some old_post_edges -> ( + match cell_pre_opt with + | None -> + old_post_edges + | Some (edges_pre, _) -> + PulseDomain.Memory.Edges.merge + (fun _access old_opt pre_opt -> + (* TODO: should apply [call_state.subst] to [_access]! Actually, should rewrite the + whole [cell_pre] beforehand so that [Edges.merge] makes sense. *) + if Option.is_some pre_opt then + (* delete edge if some edge for the same access exists in the pre *) + None + else (* keep old edge if it exists *) old_opt ) + old_post_edges edges_pre ) + + + let add_call_to_attr proc_name location attr = + match (attr : PulseDomain.Attribute.t) with + | Invalid action -> + PulseDomain.Attribute.Invalid (PulseTrace.ViaCall {action; proc_name; location}) + | MustBeValid _ | AddressOfCppTemporary (_, _) | Closure _ | StdVectorReserve -> + attr + + + let rec record_post_for_address callee_proc_name call_loc ({pre; post} as pre_post) ~addr_callee + ~addr_caller call_state = + L.d_printfln "%a<->%a@\n" AbstractAddress.pp addr_callee AbstractAddress.pp addr_caller ; + match visit call_state ~addr_callee ~addr_caller with + | `AlreadyVisited, call_state -> + call_state + | `NotAlreadyVisited, call_state -> ( + match PulseDomain.Memory.find_opt addr_callee (post :> PulseDomain.t).PulseDomain.heap with + | None -> + call_state + | Some ((edges_post, _attrs_post) as cell_post) -> + let cell_pre_opt = + PulseDomain.Memory.find_opt addr_callee (pre :> PulseDomain.t).PulseDomain.heap + in + let call_state_after_post = + if is_cell_read_only ~cell_pre_opt ~cell_post then call_state + else + record_post_cell callee_proc_name call_loc ~addr_callee ~cell_pre_opt ~addr_caller + ~cell_post call_state + in + IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold + ~init:call_state_after_post edges_post + ~f:(fun call_state (_access, (addr_callee_dest, _)) -> + let call_state, addr_curr_dest = + call_state_subst_find_or_new call_state addr_callee_dest + in + record_post_for_address callee_proc_name call_loc pre_post + ~addr_callee:addr_callee_dest ~addr_caller:addr_curr_dest call_state ) ) + + + and record_post_cell callee_proc_name call_loc ~addr_callee ~cell_pre_opt + ~cell_post:(edges_post, attrs_post) ~addr_caller call_state = + let post_edges_minus_pre = + delete_edges_in_callee_pre_from_caller ~addr_callee ~cell_pre_opt ~addr_caller call_state + in + let new_attrs = + let attrs_post = Attributes.map (add_call_to_attr callee_proc_name call_loc) attrs_post in + match + PulseDomain.Memory.find_attrs_opt addr_caller (call_state.astate.post :> base_domain).heap + with + | None -> + attrs_post + | Some old_attrs_post -> + Attributes.union old_attrs_post attrs_post + in + let subst, translated_post_edges = + PulseDomain.Memory.Edges.fold_map ~init:call_state.subst edges_post + ~f:(fun subst (addr_callee, trace_post) -> + let addr_curr, subst = subst_find_or_new subst addr_callee in + ( subst + , ( addr_curr + , PulseTrace.Call + {f= `HilCall (Direct callee_proc_name); actuals= [ (* TODO *) ]; location= call_loc} + :: trace_post ) ) ) + in + let caller_post = + let new_edges = + PulseDomain.Memory.Edges.union + (fun _ _ post_cell -> Some post_cell) + post_edges_minus_pre translated_post_edges + in + Domain.make (call_state.astate.post :> base_domain).stack + (PulseDomain.Memory.set_cell addr_caller (new_edges, new_attrs) + (call_state.astate.post :> base_domain).heap) + in + {call_state with subst; astate= {call_state.astate with post= caller_post}} + + + let record_post_for_actual callee_proc_name call_loc pre_post ~formal ~actual call_state = + L.d_printfln_escaped "Recording POST from [%a] <-> %a" Var.pp formal + (Pp.option AbstractAddress.pp) (Option.map ~f:fst actual) ; + match actual with + | None -> + call_state + | Some (addr_caller, _trace) -> ( + let open Option.Monad_infix in + match + PulseDomain.Stack.find_opt formal (pre_post.pre :> PulseDomain.t).PulseDomain.stack + >>= fun (addr_formal_pre, _) -> + PulseDomain.Memory.find_edge_opt addr_formal_pre Dereference + (pre_post.pre :> PulseDomain.t).PulseDomain.heap + >>| fun (formal_pre, _) -> + record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:formal_pre + ~addr_caller call_state + with + | Some call_state -> + call_state + | None -> + call_state ) + + + let record_post_for_return callee_proc_name call_loc pre_post ~ret call_state = + let return_var = Var.of_pvar (Pvar.get_ret_pvar callee_proc_name) in + match + PulseDomain.Stack.find_opt return_var (pre_post.pre :> PulseDomain.t).PulseDomain.stack + with + | Some (addr_return, _) -> + record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:addr_return + ~addr_caller:(fst ret) call_state + | None -> + call_state + + + let apply_post callee_proc_name call_location pre_post ~formals ~ret ~actuals call_state = + (* reset [visited] *) + let call_state_pre = {call_state with visited= AddressSet.empty} in + (* for each [(formal_i, actual_i)] pair, do [post_i = post union subst(graph reachable from + formal_i in post)], deleting previous info when comparing pre and post shows a difference + (TODO: record in the pre when a location is written to instead of just comparing values + between pre and post since it's unreliable, eg replace value read in pre with same value in + post but nuke other fields in the meantime? is that possible?). *) + match + PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call post" ())) ; + let r = + List.fold2 formals actuals ~init:call_state_pre ~f:(fun call_state formal actual -> + record_post_for_actual callee_proc_name call_location pre_post ~formal ~actual + call_state ) + in + PerfEvent.(log (fun logger -> log_end_event logger ())) ; + r + with + | Ok call_state -> + record_post_for_return callee_proc_name call_location pre_post ~ret call_state + |> fun {astate} -> Some astate + | exception Aliasing -> + None + | Unequal_lengths -> + (* should have been checked before by [materialize_pre] *) + assert false + + + (* - read all the pre, assert validity of addresses and materializes *everything* (to throw stuff + in the *current* pre as appropriate so that callers of the current procedure will also know + about the deeper reads) + + - for each actual, write the post for that actual + + - if aliasing is introduced at any time then give up + + questions: + + - what if some preconditions raise lifetime issues but others don't? Have to be careful with + the noise that this will introduce since we don't care about values. For instance, if the pre + is for a path where [formal != 0] and we pass [0] then it will be an FP. Maybe the solution is + to bake in some value analysis. *) + let apply callee_proc_name call_location pre_post ~formals ~ret ~actuals astate = + L.d_printfln "Applying pre/post for %a(%a):@\n%a" Typ.Procname.pp callee_proc_name + (Pp.seq ~sep:"," Var.pp) formals pp pre_post ; + let empty_call_state = + {astate; subst= AddressMap.empty; rev_subst= AddressMap.empty; visited= AddressSet.empty} + in + (* read the precondition *) + match + materialize_pre callee_proc_name call_location pre_post ~formals ~actuals empty_call_state + with + | None -> + (* couldn't apply the pre for some technical reason (as in: not by the fault of the + programmer as far as we know) *) + Ok astate + | Some (Error _ as error) -> + (* error: the function call requires to read some state known to be invalid *) + error + | Some (Ok call_state) -> ( + (* apply the postcondition *) + match + apply_post callee_proc_name call_location pre_post ~formals ~ret ~actuals call_state + with + | None -> + (* same as when trying to apply the pre: give up for that pre/post pair and return the + original state *) + Ok astate + | Some astate_post -> + Ok astate_post ) +end diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 8f1a33a0b..d73d3bb50 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -46,13 +46,16 @@ module Memory : sig AbstractAddress.t -> Access.t -> PulseDomain.AddrTracePair.t -> t -> t val check_valid : - PulseDiagnostic.actor -> AbstractAddress.t -> t -> (t, PulseInvalidation.t) result + HilExp.AccessExpression.t PulseTrace.action + -> AbstractAddress.t + -> t + -> (t, PulseInvalidation.t PulseTrace.action) result val find_opt : AbstractAddress.t -> t -> PulseDomain.Memory.cell option val set_cell : AbstractAddress.t -> PulseDomain.Memory.cell -> t -> t - val invalidate : AbstractAddress.t -> PulseInvalidation.t -> t -> t + val invalidate : AbstractAddress.t -> PulseInvalidation.t PulseTrace.action -> t -> t val is_std_vector_reserved : AbstractAddress.t -> t -> bool @@ -61,6 +64,26 @@ module Memory : sig val materialize_edge : AbstractAddress.t -> Access.t -> t -> t * PulseDomain.AddrTracePair.t end +module PrePost : sig + type domain_t = t + + type t = private domain_t + + val pp : Format.formatter -> t -> unit + + val of_post : domain_t -> t + + val apply : + Typ.Procname.t + -> Location.t + -> t + -> formals:Var.t list + -> ret:AbstractAddress.t * PulseTrace.t + -> actuals:(AbstractAddress.t * PulseTrace.t) option list + -> domain_t + -> (domain_t, PulseDiagnostic.t) result +end + val discard_unreachable : t -> t (** garbage collect unreachable addresses in the state to make it smaller, just for convenience and - keep its size down *) + keep its size down *) diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml index bdaa2dff0..a1a86bb63 100644 --- a/infer/src/pulse/PulseDiagnostic.ml +++ b/infer/src/pulse/PulseDiagnostic.ml @@ -8,25 +8,28 @@ open! IStd module F = Format -type actor = {access_expr: HilExp.AccessExpression.t; location: Location.t} [@@deriving compare] - type t = | AccessToInvalidAddress of - { invalidated_by: PulseInvalidation.t - ; accessed_by: actor + { invalidated_by: PulseInvalidation.t PulseTrace.action + ; accessed_by: HilExp.AccessExpression.t PulseTrace.action ; trace: PulseTrace.t } | StackVariableAddressEscape of {variable: Var.t; location: Location.t} +let pp_access = PulseTrace.pp_action HilExp.AccessExpression.pp + +let pp_invalidation = PulseTrace.pp_action PulseInvalidation.pp + let get_location = function - | AccessToInvalidAddress {accessed_by= {location}} | StackVariableAddressEscape {location} -> + | AccessToInvalidAddress {accessed_by} -> + PulseTrace.outer_location_of_action accessed_by + | StackVariableAddressEscape {location} -> location let get_message = function | AccessToInvalidAddress {accessed_by; invalidated_by; trace} -> - F.asprintf "`%a` accesses address %a%a past its lifetime" HilExp.AccessExpression.pp - accessed_by.access_expr PulseTrace.pp_interesting_events trace PulseInvalidation.pp - invalidated_by + F.asprintf "%a accesses address %a%a past its lifetime" pp_access accessed_by + PulseTrace.pp_interesting_events trace pp_invalidation invalidated_by | StackVariableAddressEscape {variable} -> let pp_var f var = if Var.is_cpp_temporary var then F.pp_print_string f "C++ temporary" @@ -37,25 +40,17 @@ let get_message = function let get_trace = function | AccessToInvalidAddress {accessed_by; invalidated_by; trace} -> - let invalidated_by_trace = - PulseInvalidation.get_location invalidated_by - |> Option.map ~f:(fun location -> - Errlog.make_trace_element 0 location - (F.asprintf "%a here" PulseInvalidation.pp invalidated_by) - [] ) - |> Option.to_list - in PulseTrace.make_errlog_trace ~depth:0 trace - @ invalidated_by_trace - @ [ Errlog.make_trace_element 0 accessed_by.location - (F.asprintf "accessed `%a` here" HilExp.AccessExpression.pp accessed_by.access_expr) - [] ] + @ PulseTrace.trace_of_action ~action_name:"invalidated" PulseInvalidation.pp invalidated_by + @ PulseTrace.trace_of_action ~action_name:"accessed" + (Pp.in_backticks HilExp.AccessExpression.pp) + accessed_by | StackVariableAddressEscape _ -> [] let get_issue_type = function | AccessToInvalidAddress {invalidated_by} -> - PulseInvalidation.issue_type_of_cause invalidated_by + PulseTrace.immediate_of_action invalidated_by |> PulseInvalidation.issue_type_of_cause | StackVariableAddressEscape _ -> IssueType.stack_variable_address_escape diff --git a/infer/src/pulse/PulseDiagnostic.mli b/infer/src/pulse/PulseDiagnostic.mli index 380adc139..1b5c1bd31 100644 --- a/infer/src/pulse/PulseDiagnostic.mli +++ b/infer/src/pulse/PulseDiagnostic.mli @@ -7,12 +7,10 @@ open! IStd -type actor = {access_expr: HilExp.AccessExpression.t; location: Location.t} [@@deriving compare] - type t = | AccessToInvalidAddress of - { invalidated_by: PulseInvalidation.t - ; accessed_by: actor + { invalidated_by: PulseInvalidation.t PulseTrace.action + ; accessed_by: HilExp.AccessExpression.t PulseTrace.action ; trace: PulseTrace.t } | StackVariableAddressEscape of {variable: Var.t; location: Location.t} diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml index 759ba4da7..bf359103f 100644 --- a/infer/src/pulse/PulseDomain.ml +++ b/infer/src/pulse/PulseDomain.ml @@ -19,8 +19,8 @@ module Attribute = struct address is invalid) *) type t = (* DO NOT MOVE, see toplevel comment *) - | Invalid of Invalidation.t - | MustBeValid of PulseDiagnostic.actor + | Invalid of Invalidation.t PulseTrace.action + | MustBeValid of HilExp.AccessExpression.t PulseTrace.action | AddressOfCppTemporary of Var.t * Location.t option | Closure of Typ.Procname.t | StdVectorReserve @@ -28,10 +28,12 @@ module Attribute = struct let pp f = function | Invalid invalidation -> - Invalidation.pp f invalidation - | MustBeValid actor -> - F.fprintf f "MustBeValid (read by %a @ %a)" HilExp.AccessExpression.pp actor.access_expr - Location.pp actor.location + (PulseTrace.pp_action Invalidation.pp) f invalidation + | MustBeValid action -> + F.fprintf f "MustBeValid (read by %a @ %a)" + (PulseTrace.pp_action HilExp.AccessExpression.pp) + action Location.pp + (PulseTrace.outer_location_of_action action) | AddressOfCppTemporary (var, location_opt) -> F.fprintf f "&%a (%a)" Var.pp var (Pp.option Location.pp) location_opt | Closure pname -> @@ -48,6 +50,13 @@ module Attributes = struct [Invalid _] attributes are the smallest we can simply look at the first element to decide if an address is invalid or not. *) match min_elt_opt attrs with Some (Invalid invalidation) -> Some invalidation | _ -> None + + + let get_must_be_valid attrs = + find_first_opt (function MustBeValid _ -> true | _ -> false) attrs + |> Option.map ~f:(fun attr -> + let[@warning "-8"] (Attribute.MustBeValid action) = attr in + action ) end (** An abstract address in memory. *) @@ -91,6 +100,7 @@ end = struct end module AbstractAddressSet = PrettyPrintable.MakePPSet (AbstractAddress) +module AbstractAddressMap = PrettyPrintable.MakePPMap (AbstractAddress) (* {3 Heap domain } *) @@ -126,6 +136,10 @@ module Memory : sig val set_cell : AbstractAddress.t -> cell -> t -> t + val find_attrs_opt : AbstractAddress.t -> t -> Attributes.t option + + val find_edges_opt : AbstractAddress.t -> t -> edges option + val mem_edges : AbstractAddress.t -> t -> bool val pp : F.formatter -> t -> unit @@ -140,9 +154,9 @@ module Memory : sig val add_attributes : AbstractAddress.t -> Attributes.t -> t -> t - val invalidate : AbstractAddress.t -> Invalidation.t -> t -> t + val invalidate : AbstractAddress.t -> Invalidation.t PulseTrace.action -> t -> t - val check_valid : AbstractAddress.t -> t -> (unit, Invalidation.t) result + val check_valid : AbstractAddress.t -> t -> (unit, Invalidation.t PulseTrace.action) result val std_vector_reserve : AbstractAddress.t -> t -> t @@ -245,8 +259,12 @@ end = struct let empty = (Graph.empty, Graph.empty) + let find_edges_opt addr memory = Graph.find_opt addr (fst memory) + + let find_attrs_opt addr memory = Graph.find_opt addr (snd memory) + let find_opt addr memory = - match (Graph.find_opt addr (fst memory), Graph.find_opt addr (snd memory)) with + match (find_edges_opt addr memory, find_attrs_opt addr memory) with | None, None -> None | edges_opt, attrs_opt -> diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli index bc9317ef7..e34182c10 100644 --- a/infer/src/pulse/PulseDomain.mli +++ b/infer/src/pulse/PulseDomain.mli @@ -10,15 +10,19 @@ module F = Format module Attribute : sig type t = - | Invalid of PulseInvalidation.t - | MustBeValid of PulseDiagnostic.actor + | Invalid of PulseInvalidation.t PulseTrace.action + | MustBeValid of HilExp.AccessExpression.t PulseTrace.action | AddressOfCppTemporary of Var.t * Location.t option | Closure of Typ.Procname.t | StdVectorReserve [@@deriving compare] end -module Attributes : PrettyPrintable.PPSet with type elt = Attribute.t +module Attributes : sig + include PrettyPrintable.PPSet with type elt = Attribute.t + + val get_must_be_valid : t -> HilExp.AccessExpression.t PulseTrace.action option +end module AbstractAddress : sig type t = private int [@@deriving compare] @@ -40,6 +44,8 @@ end module AbstractAddressSet : PrettyPrintable.PPSet with type elt = AbstractAddress.t +module AbstractAddressMap : PrettyPrintable.PPMap with type key = AbstractAddress.t + module Stack : sig include PrettyPrintable.MonoMap @@ -73,6 +79,10 @@ module Memory : sig val set_cell : AbstractAddress.t -> cell -> t -> t + val find_attrs_opt : AbstractAddress.t -> t -> Attributes.t option + + val find_edges_opt : AbstractAddress.t -> t -> edges option + val mem_edges : AbstractAddress.t -> t -> bool val register_address : AbstractAddress.t -> t -> t @@ -85,9 +95,9 @@ module Memory : sig val add_attributes : AbstractAddress.t -> Attributes.t -> t -> t - val invalidate : AbstractAddress.t -> PulseInvalidation.t -> t -> t + val invalidate : AbstractAddress.t -> PulseInvalidation.t PulseTrace.action -> t -> t - val check_valid : AbstractAddress.t -> t -> (unit, PulseInvalidation.t) result + val check_valid : AbstractAddress.t -> t -> (unit, PulseInvalidation.t PulseTrace.action) result val std_vector_reserve : AbstractAddress.t -> t -> t diff --git a/infer/src/pulse/PulseInvalidation.ml b/infer/src/pulse/PulseInvalidation.ml index 56e7e3c5b..5df74cfad 100644 --- a/infer/src/pulse/PulseInvalidation.ml +++ b/infer/src/pulse/PulseInvalidation.ml @@ -58,28 +58,16 @@ let issue_type_of_cause = function IssueType.vector_invalidation -let get_location = function - | CFree (_, location) - | CppDelete (_, location) - | CppDestructor (_, _, location) - | StdVector (_, _, location) -> - Some location - | Nullptr -> - None - - let pp f = function - | CFree (access_expr, location) -> - F.fprintf f "invalidated by call to `free(%a)` at %a" HilExp.AccessExpression.pp access_expr - Location.pp_line location - | CppDelete (access_expr, location) -> - F.fprintf f "invalidated by call to `delete %a` at %a" HilExp.AccessExpression.pp access_expr - Location.pp_line location - | CppDestructor (proc_name, access_expr, location) -> - F.fprintf f "invalidated by destructor call `%a(%a)` at %a" Typ.Procname.pp proc_name - HilExp.AccessExpression.pp access_expr Location.pp_line location + | CFree (access_expr, _) -> + F.fprintf f "by call to `free()` on `%a`" HilExp.AccessExpression.pp access_expr + | CppDelete (access_expr, _) -> + F.fprintf f "by `delete` on `%a`" HilExp.AccessExpression.pp access_expr + | CppDestructor (proc_name, access_expr, _) -> + F.fprintf f "by destructor call `%a()` on `%a`" Typ.Procname.pp proc_name + HilExp.AccessExpression.pp access_expr | Nullptr -> F.fprintf f "null pointer" - | StdVector (std_vector_f, access_expr, location) -> - F.fprintf f "potentially invalidated by call to `%a(%a, ..)` at %a" pp_std_vector_function - std_vector_f HilExp.AccessExpression.pp access_expr Location.pp_line location + | StdVector (std_vector_f, access_expr, _) -> + F.fprintf f "potentially invalidated by call to `%a()` on `%a`" pp_std_vector_function + std_vector_f HilExp.AccessExpression.pp access_expr diff --git a/infer/src/pulse/PulseInvalidation.mli b/infer/src/pulse/PulseInvalidation.mli index 252ea3a28..ce6508900 100644 --- a/infer/src/pulse/PulseInvalidation.mli +++ b/infer/src/pulse/PulseInvalidation.mli @@ -29,6 +29,4 @@ type t = val issue_type_of_cause : t -> IssueType.t -val get_location : t -> Location.t option - val pp : Format.formatter -> t -> unit diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index bb7555da2..2319a6b2b 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -26,7 +26,7 @@ module C = struct match actuals with | [AccessExpression deleted_access] -> PulseOperations.invalidate - (CFree (deleted_access, location)) + (PulseTrace.Immediate {imm= PulseInvalidation.CFree (deleted_access, location); location}) location deleted_access astate | _ -> Ok astate @@ -40,7 +40,8 @@ module Cplusplus = struct match actuals with | [AccessExpression deleted_access] -> PulseOperations.invalidate - (CppDelete (deleted_access, location)) + (PulseTrace.Immediate + {imm= PulseInvalidation.CppDelete (deleted_access, location); location}) location deleted_access astate | _ -> Ok astate @@ -76,7 +77,7 @@ module Cplusplus = struct |> read_all other_actuals | _ :: other_actuals -> read_all other_actuals astate >>| PulseOperations.havoc_var [crumb] ret_var - | _ -> + | [] -> Ok (PulseOperations.havoc_var [crumb] ret_var astate) end @@ -100,7 +101,9 @@ module StdVector = struct let reallocate_internal_array trace vector vector_f location astate = let array_address = to_internal_array vector in let array = deref_internal_array vector in - let invalidation = PulseInvalidation.StdVector (vector_f, vector, location) in + let invalidation = + PulseTrace.Immediate {imm= PulseInvalidation.StdVector (vector_f, vector, location); location} + in PulseOperations.invalidate_array_elements invalidation location array astate >>= PulseOperations.invalidate invalidation location array >>= PulseOperations.havoc trace location array_address diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index d233a5fe6..b931fcfef 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -26,23 +26,23 @@ type t = PulseAbductiveDomain.t type 'a access_result = ('a, PulseDiagnostic.t) result (** Check that the address is not known to be invalid *) -let check_addr_access actor (address, trace) astate = - Memory.check_valid actor address astate +let check_addr_access action (address, trace) astate = + Memory.check_valid action address astate |> Result.map_error ~f:(fun invalidated_by -> - PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= actor; trace} ) + PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= action; trace} ) (** Walk the heap starting from [addr] and following [path]. Stop either at the element before last and return [new_addr] if [overwrite_last] is [Some new_addr], or go until the end of the path if it is [None]. Create more addresses into the heap as needed to follow the [path]. Check that each address reached is valid. *) -let rec walk ~dereference_to_ignore actor ~on_last addr_trace path astate = - let check_addr_access_optional actor addr_trace astate = +let rec walk ~dereference_to_ignore action ~on_last addr_trace path astate = + let check_addr_access_optional action addr_trace astate = match dereference_to_ignore with | Some 0 -> Ok astate | _ -> - check_addr_access actor addr_trace astate + check_addr_access action addr_trace astate in match (path, on_last) with | [], `Access -> @@ -50,18 +50,18 @@ let rec walk ~dereference_to_ignore actor ~on_last addr_trace path astate = | [], `Overwrite _ -> L.die InternalError "Cannot overwrite last address in empty path" | [a], `Overwrite new_addr_trace -> - check_addr_access_optional actor addr_trace astate + check_addr_access_optional action addr_trace astate >>| fun astate -> let astate = Memory.add_edge_and_back_edge (fst addr_trace) a new_addr_trace astate in (astate, new_addr_trace) | a :: path, _ -> - check_addr_access_optional actor addr_trace astate + check_addr_access_optional action addr_trace astate >>= fun astate -> let dereference_to_ignore = Option.map ~f:(fun index -> max 0 (index - 1)) dereference_to_ignore in let astate, addr_trace' = Memory.materialize_edge (fst addr_trace) a astate in - walk ~dereference_to_ignore actor ~on_last addr_trace' path astate + walk ~dereference_to_ignore action ~on_last addr_trace' path astate let write_var var new_addr_trace astate = @@ -130,8 +130,8 @@ and walk_access_expr ~on_last astate access_expr location = | [HilExp.Access.TakeAddress] -> Ok (astate, base_addr_trace) | _ -> - let actor = {PulseDiagnostic.access_expr; location} in - walk ~dereference_to_ignore actor ~on_last base_addr_trace + let action = PulseTrace.Immediate {imm= access_expr; location} in + walk ~dereference_to_ignore action ~on_last base_addr_trace (HilExp.Access.Dereference :: access_list) astate ) @@ -143,12 +143,7 @@ and walk_access_expr ~on_last astate access_expr location = known to be invalid. *) and materialize_address astate access_expr = walk_access_expr ~on_last:`Access astate access_expr -and read location access_expr astate = - materialize_address astate access_expr location - >>= fun (astate, addr_trace) -> - let actor = {PulseDiagnostic.access_expr; location} in - check_addr_access actor addr_trace astate >>| fun astate -> (astate, addr_trace) - +and read location access_expr astate = materialize_address astate access_expr location and read_all location access_exprs astate = List.fold_result access_exprs ~init:astate ~f:(fun astate access_expr -> @@ -174,7 +169,7 @@ let overwrite_address astate access_expr new_addr_trace = (** Add the given address to the set of know invalid addresses. *) -let mark_invalid actor address astate = Memory.invalidate address actor astate +let mark_invalid action address astate = Memory.invalidate address action astate let havoc_var trace var astate = write_var var (AbstractAddress.mk_fresh (), trace) astate @@ -189,14 +184,14 @@ let write location access_expr addr astate = let invalidate cause location access_expr astate = materialize_address astate access_expr location >>= fun (astate, addr_trace) -> - check_addr_access {access_expr; location} addr_trace astate + check_addr_access (Immediate {imm= access_expr; location}) addr_trace astate >>| mark_invalid cause (fst addr_trace) let invalidate_array_elements cause location access_expr astate = materialize_address astate access_expr location >>= fun (astate, addr_trace) -> - check_addr_access {access_expr; location} addr_trace astate + check_addr_access (Immediate {imm= access_expr; location}) addr_trace astate >>| fun astate -> match Memory.find_opt (fst addr_trace) astate with | None -> @@ -319,7 +314,7 @@ module Closures = struct ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold) edges ~f:(fun (access, addr_trace) -> if is_captured_fake_access access then - check_addr_access {access_expr= lambda; location} addr_trace astate + check_addr_access (Immediate {imm= lambda; location}) addr_trace astate >>| fun _ -> () else Ok () ) | _ -> @@ -367,3 +362,28 @@ module StdVector = struct read location vector_access_expr astate >>| fun (astate, (addr, _)) -> Memory.std_vector_reserve addr astate end + +module Interproc = struct + open Result.Monad_infix + + (* compute addresses for actuals and then call {!PulseAbductiveDomain.PrePost.apply} on each + pre/post pair in the summary. *) + let call callee_pname ~formals ~ret ~actuals _flags call_loc astate pre_posts = + L.d_printfln "PulseOperations.call" ; + List.fold_result actuals ~init:(astate, []) ~f:(fun (astate, rev_actual_addresses) actual -> + match actual with + | HilExp.AccessExpression access_expr -> + read call_loc access_expr astate + >>| fun (astate, (addr, trace)) -> (astate, Some (addr, trace) :: rev_actual_addresses) + | _ -> + Ok (astate, None :: rev_actual_addresses) ) + >>= fun (astate, rev_actual_addresses) -> + let actuals = List.rev rev_actual_addresses in + read call_loc HilExp.AccessExpression.(address_of_base ret) astate + >>= fun (astate, ret) -> + List.fold_result pre_posts ~init:[] ~f:(fun posts pre_post -> + (* apply all pre/post specs *) + PulseAbductiveDomain.PrePost.apply callee_pname call_loc pre_post ~formals ~ret ~actuals + astate + >>| fun post -> post :: posts ) +end diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index f658bcb4b..3406678c5 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -59,10 +59,18 @@ val write : -> t access_result val invalidate : - PulseInvalidation.t -> Location.t -> HilExp.AccessExpression.t -> t -> t access_result + PulseInvalidation.t PulseTrace.action + -> Location.t + -> HilExp.AccessExpression.t + -> t + -> t access_result val invalidate_array_elements : - PulseInvalidation.t -> Location.t -> HilExp.AccessExpression.t -> t -> t access_result + PulseInvalidation.t PulseTrace.action + -> Location.t + -> HilExp.AccessExpression.t + -> t + -> t access_result val record_var_decl_location : Location.t -> Var.t -> t -> t @@ -70,3 +78,16 @@ val remove_vars : Var.t list -> t -> t (* TODO: better name and pass location to report where we returned *) val check_address_of_local_variable : Procdesc.t -> AbstractAddress.t -> t -> t access_result + +module Interproc : sig + val call : + Typ.Procname.t + -> formals:Var.t list + -> ret:AccessPath.base + -> actuals:HilExp.t list + -> CallFlags.t + -> Location.t + -> t + -> PulseSummary.t + -> PulseAbductiveDomain.t list access_result +end diff --git a/infer/src/pulse/PulseSummary.ml b/infer/src/pulse/PulseSummary.ml new file mode 100644 index 000000000..464cd25f2 --- /dev/null +++ b/infer/src/pulse/PulseSummary.ml @@ -0,0 +1,14 @@ +(* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) +open! IStd + +type t = PulseAbductiveDomain.PrePost.t list + +let of_posts posts = List.map posts ~f:PulseAbductiveDomain.PrePost.of_post + +let pp fmt summary = + PrettyPrintable.pp_collection ~pp_item:PulseAbductiveDomain.PrePost.pp fmt summary diff --git a/infer/src/pulse/PulseSummary.mli b/infer/src/pulse/PulseSummary.mli new file mode 100644 index 000000000..beb5c7e27 --- /dev/null +++ b/infer/src/pulse/PulseSummary.mli @@ -0,0 +1,13 @@ +(* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) +open! IStd + +type t = PulseAbductiveDomain.PrePost.t list + +val of_posts : PulseAbductiveDomain.t list -> t + +val pp : Format.formatter -> t -> unit diff --git a/infer/src/pulse/PulseTrace.ml b/infer/src/pulse/PulseTrace.ml index 5013b4c31..6c8c9f160 100644 --- a/infer/src/pulse/PulseTrace.ml +++ b/infer/src/pulse/PulseTrace.ml @@ -70,3 +70,44 @@ let pp_last_event f = function let pp_interesting_events f trace = pp_last_event f trace + +type 'a action = + | Immediate of {imm: 'a; location: Location.t} + | ViaCall of {action: 'a action; proc_name: Typ.Procname.t; location: Location.t} +[@@deriving compare] + +let pp_action pp_immediate fmt = function + | Immediate {imm; _} -> + F.fprintf fmt "`%a`" pp_immediate imm + | ViaCall {proc_name; _} -> + F.fprintf fmt "call to `%a`" Typ.Procname.pp proc_name + + +let rec immediate_of_action = function + | Immediate {imm; _} -> + imm + | ViaCall {action; _} -> + immediate_of_action action + + +let trace_of_action ~action_name pp_immediate action = + let rec aux ~nesting rev_trace action = + match action with + | Immediate {imm; location} -> + Errlog.make_trace_element nesting location + (F.asprintf "%s %a here" action_name pp_immediate imm) + [] + :: rev_trace + |> List.rev + | ViaCall {action; proc_name; location} -> + aux ~nesting:(nesting + 1) + ( Errlog.make_trace_element nesting location + (F.asprintf "%s during call to `%a` here" action_name Typ.Procname.pp proc_name) + [] + :: rev_trace ) + action + in + aux ~nesting:0 [] action + + +let outer_location_of_action = function Immediate {location} | ViaCall {location} -> location diff --git a/infer/src/pulse/PulseTrace.mli b/infer/src/pulse/PulseTrace.mli index 424a64e34..2378ad57c 100644 --- a/infer/src/pulse/PulseTrace.mli +++ b/infer/src/pulse/PulseTrace.mli @@ -6,6 +6,7 @@ *) open! IStd +module F = Format type breadcrumb = | VariableDeclaration of Location.t @@ -21,8 +22,22 @@ type breadcrumb = type t = breadcrumb list [@@deriving compare] -val pp : Format.formatter -> t -> unit +val pp : F.formatter -> t -> unit val make_errlog_trace : depth:int -> t -> Errlog.loc_trace -val pp_interesting_events : Format.formatter -> t -> unit +val pp_interesting_events : F.formatter -> t -> unit + +type 'a action = + | Immediate of {imm: 'a; location: Location.t} + | ViaCall of {action: 'a action; proc_name: Typ.Procname.t; location: Location.t} +[@@deriving compare] + +val pp_action : (F.formatter -> 'a -> unit) -> F.formatter -> 'a action -> unit + +val immediate_of_action : 'a action -> 'a + +val outer_location_of_action : 'a action -> Location.t + +val trace_of_action : + action_name:string -> (F.formatter -> 'a -> unit) -> 'a action -> Errlog.loc_trace_elem sexp_list diff --git a/infer/tests/codetoanalyze/cpp/pulse/closures.cpp b/infer/tests/codetoanalyze/cpp/pulse/closures.cpp index 429b448cd..30f98729e 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/closures.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/closures.cpp @@ -31,7 +31,6 @@ int implicit_ref_capture_destroy_invoke_bad() { return f(); } -// need to understand copy constructor int FN_reassign_lambda_capture_destroy_invoke_bad() { std::function f; { @@ -97,8 +96,12 @@ std::function ref_capture_read_lambda_ok() { f; // reading (but not invoking) the lambda doesn't use its captured vars } -void delete_lambda_then_call_bad() { +int FN_delete_lambda_then_call_bad() { std::function lambda = [] { return 1; }; + // std::function<_>_~function() has no implementation so the call is + // skipped and we don't apply the logic for marking the object as + // destructed because it's an explicit call (as opposed to a call + // injected by the frontend) lambda.~function(); return lambda(); } @@ -125,7 +128,7 @@ int ref_capture_return_local_lambda_ok() { return f().f; } -S& FN_ref_capture_return_local_lambda_bad() { +S& ref_capture_return_local_lambda_bad() { S x; auto f = [&x](void) -> S& { // no way to know if ok here diff --git a/infer/tests/codetoanalyze/cpp/pulse/interprocedural.cpp b/infer/tests/codetoanalyze/cpp/pulse/interprocedural.cpp index 17398b07c..ada9ebff2 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/interprocedural.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/interprocedural.cpp @@ -23,12 +23,12 @@ void wraps_delete_inner(struct X* x) { delete x; } void wraps_delete(struct X* x) { wraps_delete_inner(x); } -void FP_delete_then_skip_ok(struct X& x) { +void delete_then_skip_ok(struct X& x) { delete (&x); skip(x); } -void FP_delete_then_skip_ptr_ok(struct X* x) { +void delete_then_skip_ptr_ok(struct X* x) { delete x; skip_ptr(x); } @@ -38,12 +38,12 @@ void delete_then_read_bad(struct X& x) { wraps_read(x); } -void FN_delete_then_write_bad(struct X& x) { +void delete_then_write_bad(struct X& x) { wraps_delete(&x); wraps_read(x); } -void FN_delete_inner_then_write_bad(struct X& x) { +void delete_inner_then_write_bad(struct X& x) { wraps_delete_inner(&x); wraps_read(x); } @@ -75,7 +75,7 @@ void call_store(struct Y* y) { extern bool nondet_choice(); -struct Y* FP_may_return_invalid_ptr_ok() { +struct Y* may_return_invalid_ptr_ok() { struct Y* y = new Y(); if (nondet_choice()) { delete y; @@ -83,7 +83,7 @@ struct Y* FP_may_return_invalid_ptr_ok() { return y; } -void FN_feed_invalid_into_access_bad() { - struct Y* y = FP_may_return_invalid_ptr_ok(); +void feed_invalid_into_access_bad() { + struct Y* y = may_return_invalid_ptr_ok(); call_store(y); } diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index f2124f66e..1583bf25c 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,43 +1,42 @@ -codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 58 here,accessed `*(ptr)` here] -codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 68 here,accessed `ptr` here] -codetoanalyze/cpp/pulse/closures.cpp, delete_lambda_then_call_bad, 3, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `std::function<_fn_>::function(&(lambda),&(0$?%__sil_tmpSIL_materialize_temp__n$8))`,invalidated by destructor call `std::function<_fn_>::~function(lambda)` at line 102 here,accessed `lambda` here] -codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `S::S(&(s),&(0$?%__sil_tmpSIL_materialize_temp__n$11))`,`&(s)` captured as `s`,invalidated by destructor call `S::~S(s)` at line 30 here,accessed `&(f)` here] -codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `S::S(&(s))`,`&(s)` captured as `s`,invalidated by destructor call `S::~S(s)` at line 21 here,accessed `&(f)` here] -codetoanalyze/cpp/pulse/interprocedural.cpp, FP_delete_then_skip_ok, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete x` at line 27 here,accessed `x` here] -codetoanalyze/cpp/pulse/interprocedural.cpp, FP_delete_then_skip_ptr_ok, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete x` at line 32 here,accessed `x` here] -codetoanalyze/cpp/pulse/interprocedural.cpp, FP_may_return_invalid_ptr_ok, 5, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Y))`,assigned to `y`,invalidated by call to `delete y` at line 81 here,accessed `y` here] -codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete x` at line 37 here,accessed `x` here] -codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `result`,invalidated by call to `delete result` at line 30 here,accessed `*(result)` here] -codetoanalyze/cpp/pulse/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(int))`,assigned to `x`,invalidated by call to `delete x` at line 112 here,accessed `x` here] +codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by `delete` on `ptr` here,accessed `*(ptr)` here] +codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by `delete` on `ptr` here,accessed `ptr` here] +codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [variable declared,`&(s)` captured as `s`,invalidated by destructor call `S::~S()` on `s` here,accessed `&(f)` here] +codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [variable declared,`&(s)` captured as `s`,invalidated by destructor call `S::~S()` on `s` here,accessed `&(f)` here] +codetoanalyze/cpp/pulse/interprocedural.cpp, delete_inner_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated during call to `wraps_delete_inner` here,invalidated by `delete` on `x` here,accessed during call to `wraps_read` here,accessed during call to `wraps_read_inner` here,accessed `x->f` here] +codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by `delete` on `x` here,accessed during call to `wraps_read` here,accessed during call to `wraps_read_inner` here,accessed `x->f` here] +codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated during call to `wraps_delete` here,invalidated during call to `wraps_delete_inner` here,invalidated by `delete` on `x` here,accessed during call to `wraps_read` here,accessed during call to `wraps_read_inner` here,accessed `x->f` here] +codetoanalyze/cpp/pulse/interprocedural.cpp, feed_invalid_into_access_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `y`,assigned to `return`,returned from call to `may_return_invalid_ptr_ok()`,assigned to `y`,invalidated during call to `may_return_invalid_ptr_ok` here,invalidated by `delete` on `y` here,accessed during call to `call_store` here,accessed during call to `store` here,accessed `y->p` here] +codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `result`,invalidated by `delete` on `result` here,accessed `*(result)` here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_literal_stack_reference_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [] codetoanalyze/cpp/pulse/returns.cpp, returns::return_stack_pointer_bad, 1, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [] codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference1_bad, 1, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [] codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference2_bad, 1, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [] -codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 57 here,accessed `s->f` here] -codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 82 here,accessed `s` here] -codetoanalyze/cpp/pulse/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 18 here,accessed `s` here] -codetoanalyze/cpp/pulse/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 50 here,accessed `s` here] -codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 37 here,accessed `s->f` here] -codetoanalyze/cpp/pulse/use_after_delete.cpp, return_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 24 here,accessed `s` here] -codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 73 here,accessed `s` here] -codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 102 here,accessed `s->f` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::double_destructor_bad, 5, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `use_after_destructor::S::S(&(s),1)`,invalidated by destructor call `use_after_destructor::S::~S(s)` at line 65 here,accessed `s` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,invalidated by call to `delete alias` at line 149 here,accessed `s` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,returned from call to `(sizeof(use_after_destructor::S),s)`,assigned to `alias`,invalidated by call to `delete s` at line 157 here,accessed `alias` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing3_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,assigned to `alias`,invalidated by call to `delete s` at line 166 here,accessed `alias` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_destructor_bad, 3, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `use_after_destructor::S::S(&(s),1)`,invalidated by destructor call `use_after_destructor::S::~S(s)` at line 72 here,accessed `*(s.f)` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `use_after_destructor::C::C(&(c),3)`,invalidated by destructor call `use_after_destructor::C::~C(c)` at line 211 here,accessed `pc->f` here] -codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free(x)` at line 15 here,accessed `x` here] -codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free(x)` at line 10 here,accessed `*(x)` here] -codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(&(vec),(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 65 here,accessed `*(elt)` here] -codetoanalyze/cpp/pulse/vector.cpp, VectorA::FP_push_back_value_field_ok, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 134 here,accessed `&(this->x)` here] -codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::assign(vec, ..)` at line 93 here,accessed `*(elt)` here] -codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::clear(vec, ..)` at line 87 here,accessed `*(elt)` here] -codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(&(vec),(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 20 here,accessed `*(elt)` here] -codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,assigned to `y`,potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 13 here,accessed `*(y)` here] -codetoanalyze/cpp/pulse/vector.cpp, emplace_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::emplace_back(vec, ..)` at line 117 here,accessed `*(elt)` here] -codetoanalyze/cpp/pulse/vector.cpp, emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::emplace(vec, ..)` at line 111 here,accessed `*(elt)` here] -codetoanalyze/cpp/pulse/vector.cpp, insert_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::insert(vec, ..)` at line 105 here,accessed `*(elt)` here] -codetoanalyze/cpp/pulse/vector.cpp, push_back_loop_bad, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(&(vec),(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 74 here,accessed `*(elt)` here] -codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::reserve(vec, ..)` at line 81 here,accessed `*(elt)` here] -codetoanalyze/cpp/pulse/vector.cpp, shrink_to_fit_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::shrink_to_fit(vec, ..)` at line 99 here,accessed `*(elt)` here] +codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `s`,invalidated by `delete` on `s` here,accessed `s->f` here] +codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `s`,invalidated by `delete` on `s` here,accessed `s` here] +codetoanalyze/cpp/pulse/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `s`,invalidated by `delete` on `s` here,accessed during call to `Simple::Simple` here,accessed `__param_0->f` here] +codetoanalyze/cpp/pulse/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `s`,invalidated by `delete` on `s` here,accessed `s` here] +codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `s`,invalidated by `delete` on `s` here,accessed `s->f` here] +codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `s`,invalidated by `delete` on `s` here,accessed during call to `Simple::Simple` here,accessed `__param_0->f` here] +codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `s`,invalidated by `delete` on `s` here,accessed `s->f` here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::FP_destruct_pointer_contents_then_placement_new2_ok, 2, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `(sizeof(use_after_destructor::S),&(s->f))`,invalidated during call to `use_after_destructor::S::~S` here,invalidated during call to `use_after_destructor::S::__infer_inner_destructor_~S` here,invalidated by `delete` on `this->f` here,accessed during call to `use_after_destructor::S::S` here,accessed `this->f` here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::double_destructor_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [variable declared,invalidated during call to `use_after_destructor::S::~S` here,invalidated during call to `use_after_destructor::S::__infer_inner_destructor_~S` here,invalidated by `delete` on `this->f` here,accessed during call to `use_after_destructor::S::~S` here,accessed during call to `use_after_destructor::S::__infer_inner_destructor_~S` here,accessed `this->f` here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `s`,invalidated by `delete` on `alias` here,accessed `s->f` here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `s`,returned from call to `(sizeof(use_after_destructor::S),s)`,assigned to `alias`,invalidated by `delete` on `s` here,accessed `alias->f` here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing3_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `s`,assigned to `alias`,invalidated by `delete` on `s` here,accessed `alias->f` here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::reinit_after_explicit_destructor2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [variable declared,invalidated during call to `use_after_destructor::S::~S` here,invalidated during call to `use_after_destructor::S::__infer_inner_destructor_~S` here,invalidated by `delete` on `this->f` here,accessed during call to `use_after_destructor::S::~S` here,accessed during call to `use_after_destructor::S::__infer_inner_destructor_~S` here,accessed `this->f` here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_destructor_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `this->f`,returned from call to `use_after_destructor::S::S()`,invalidated during call to `use_after_destructor::S::~S` here,invalidated during call to `use_after_destructor::S::__infer_inner_destructor_~S` here,invalidated by `delete` on `this->f` here,accessed `*(s.f)` here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope1_bad, 7, USE_AFTER_DELETE, no_bucket, ERROR, [variable declared,invalidated during call to `use_after_destructor::S::~S` here,invalidated during call to `use_after_destructor::S::__infer_inner_destructor_~S` here,invalidated by `delete` on `this->f` here,accessed during call to `use_after_destructor::S::~S` here,accessed during call to `use_after_destructor::S::__infer_inner_destructor_~S` here,accessed `this->f` here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [variable declared,invalidated by destructor call `use_after_destructor::C::~C()` on `c` here,accessed `pc->f` here] +codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free()` on `x` here,accessed `x` here] +codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free()` on `x` here,accessed `*(x)` here] +codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(&(vec),(unsigned long) 1)`,assigned to `elt`,invalidated potentially invalidated by call to `std::vector::push_back()` on `&(vec)` here,accessed `*(elt)` here] +codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalidated potentially invalidated by call to `std::vector::assign()` on `vec` here,accessed `*(elt)` here] +codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalidated potentially invalidated by call to `std::vector::clear()` on `vec` here,accessed `*(elt)` here] +codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(&(vec),(unsigned long) 1)`,assigned to `elt`,invalidated potentially invalidated by call to `std::vector::push_back()` on `&(vec)` here,accessed `*(elt)` here] +codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,assigned to `y`,invalidated potentially invalidated by call to `std::vector::push_back()` on `vec` here,accessed `*(y)` here] +codetoanalyze/cpp/pulse/vector.cpp, emplace_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalidated potentially invalidated by call to `std::vector::emplace_back()` on `vec` here,accessed `*(elt)` here] +codetoanalyze/cpp/pulse/vector.cpp, emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalidated potentially invalidated by call to `std::vector::emplace()` on `vec` here,accessed `*(elt)` here] +codetoanalyze/cpp/pulse/vector.cpp, insert_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalidated potentially invalidated by call to `std::vector::insert()` on `vec` here,accessed `*(elt)` here] +codetoanalyze/cpp/pulse/vector.cpp, push_back_loop_bad, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(&(vec),(unsigned long) 1)`,assigned to `elt`,invalidated potentially invalidated by call to `std::vector::push_back()` on `&(vec)` here,accessed `*(elt)` here] +codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalidated potentially invalidated by call to `std::vector::reserve()` on `vec` here,accessed `*(elt)` here] +codetoanalyze/cpp/pulse/vector.cpp, shrink_to_fit_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalidated potentially invalidated by call to `std::vector::shrink_to_fit()` on `vec` here,accessed `*(elt)` here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/returns.cpp b/infer/tests/codetoanalyze/cpp/pulse/returns.cpp index 16eb24053..b77f3d97b 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/returns.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/returns.cpp @@ -106,7 +106,8 @@ S* return_static_local_inner_scope_ok(bool b) { int* return_formal_pointer_ok(int* formal) { return formal; } -int* return_deleted_bad() { +// this *could* be ok depending on what the caller does +int* return_deleted_ok() { int* x = new int; *x = 2; delete x; diff --git a/infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp b/infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp index 4842d2c31..fbf1d52b5 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp @@ -19,7 +19,8 @@ void deref_deleted_bad() { Simple tmp = *s; } -Simple* return_deleted_bad() { +// could be ok depending on what the caller does +Simple* return_deleted_ok() { auto s = new Simple{1}; delete s; return s; diff --git a/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp b/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp index 49a14af9f..3d7aad3bb 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp @@ -75,9 +75,8 @@ int use_after_destructor_bad() { return ret; } -// can't get this yet because we assume operator= copies resources correctly -// (but this isn't true for S) -void FN_use_after_scope1_bad() { +// S::operator= doesn't copy resources correctly +void use_after_scope1_bad() { S s(1); { S tmp(2); @@ -130,41 +129,41 @@ void basic_placement_new_ok() { delete[] ptr; } -S* destruct_pointer_contents_then_placement_new1_ok(S* s) { +int* destruct_pointer_contents_then_placement_new1_ok(S* s) { s->~S(); new (s) S(1); - return s; + return s->f; } -S* destruct_pointer_contents_then_placement_new2_ok(S* s) { +int* FP_destruct_pointer_contents_then_placement_new2_ok(S* s) { s->~S(); new (&(s->f)) S(1); - return s; + return s->f; } -S* placement_new_aliasing1_bad() { +int* placement_new_aliasing1_bad() { S* s = new S(1); s->~S(); auto alias = new (s) S(2); delete alias; // this deletes s too - return s; // bad, returning freed memory + return s->f; // bad, accessing freed memory } -S* placement_new_aliasing2_bad() { +int* placement_new_aliasing2_bad() { S* s = new S(1); s->~S(); auto alias = new (s) S(2); delete s; // this deletes alias too - return alias; // bad, returning freed memory + return alias->f; // bad, accessing freed memory } -S* placement_new_aliasing3_bad() { +int* placement_new_aliasing3_bad() { S* s = new S(1); s->~S(); S* alias = s; auto alias_placement = new (s) S(2); delete s; // this deletes alias too - return alias; // bad, returning freed memory + return alias->f; // bad, accessing freed memory } void placement_new_non_var_ok() { diff --git a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp index 91e405314..ec6147041 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp @@ -129,7 +129,7 @@ void push_back_value_ok(std::vector& vec) { struct VectorA { int x; - void FP_push_back_value_field_ok(std::vector& vec) { + void push_back_value_field_ok(std::vector& vec) { x = vec[0]; vec.push_back(7); f(x);