From c80b80d0d71137401fbf94c71cb229b90ab1cb5e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Wed, 18 Nov 2020 00:40:27 -0800 Subject: [PATCH] [preanalysis] Handle closure substitution in conditionals Summary: Specialized closure substitution was broken for conditionals: ``` void foo(dispatch_block_t block1){ if (x){ block1(); // not replaced with specialized implementation } } ``` The problem was that when substituting function calls, it only used memory state at the exit node, rather than at each program point. We could solve this by - reverting the domain change in D24418560 (https://github.com/facebook/infer/commit/c47911359ac9a207aa376f6641915fccca5b150e), i.e. collecting all possible mappings conservatively (e.g. switch the domain back to `Map`) - pass the `invariant_map` for substitutions at each program point. We go with the second option here. The closure substitution is still somewhat broken as exemplified by the following example: ``` void foo(dispatch_block_t block1){ dispatch_block_t local_block = block1; local_block(); // we don't substitute the call here } ``` Reviewed By: skcho Differential Revision: D24993962 fbshipit-source-id: ebadddb58 --- infer/src/IR/Ident.ml | 2 +- infer/src/IR/Instrs.ml | 29 ++++++++- infer/src/IR/Instrs.mli | 8 ++- infer/src/IR/Procdesc.ml | 18 ++++++ infer/src/IR/Procdesc.mli | 9 +++ .../backend/ClosureSubstSpecializedMethod.ml | 63 ++++++++++++------- infer/src/biabduction/interproc.ml | 14 +---- .../objc/autoreleasepool/arc_block.m | 33 ++++++++++ .../objc/autoreleasepool/cost-issues.exp | 8 +++ .../objc/autoreleasepool/issues.exp | 2 + 10 files changed, 144 insertions(+), 42 deletions(-) diff --git a/infer/src/IR/Ident.ml b/infer/src/IR/Ident.ml index 20a1304d9..f58379a76 100644 --- a/infer/src/IR/Ident.ml +++ b/infer/src/IR/Ident.ml @@ -164,7 +164,7 @@ let standard_name kind = else Name.Primed -(** Every identifier with a given stamp should unltimately be created using this function *) +(** Every identifier with a given stamp should ultimately be created using this function *) let create_with_stamp kind name stamp = NameGenerator.update_name_hash name stamp ; {kind; name; stamp} diff --git a/infer/src/IR/Instrs.ml b/infer/src/IR/Instrs.ml index d2a1fafa6..e38d277ca 100644 --- a/infer/src/IR/Instrs.ml +++ b/infer/src/IR/Instrs.ml @@ -116,9 +116,7 @@ let map (t : not_reversed t) ~f = map_and_fold t ~f ~init:() -let concat_map t ~f = - let instrs = get_underlying_not_reversed t in - let instrs' = Array.concat_map ~f instrs in +let check_instr_equality t instrs instrs' = if Int.equal (Array.length instrs) (Array.length instrs') && Array.for_all2_exn ~f:phys_equal instrs instrs' @@ -126,6 +124,19 @@ let concat_map t ~f = else NotReversed instrs' +let concat_map t ~f = + let instrs = get_underlying_not_reversed t in + let instrs' = Array.concat_map ~f instrs in + check_instr_equality t instrs instrs' + + +let concat_map_and_fold t ~f ~init = + let cm ~f ~init t = Array.concat (Array.to_list (Array.folding_map ~init ~f t)) in + let instrs = get_underlying_not_reversed t in + let instrs' = cm ~init ~f instrs in + check_instr_equality t instrs instrs' + + let reverse_order t = let instrs = get_underlying_not_reversed t in Reversed (RevArray.of_rev_array instrs) @@ -205,3 +216,15 @@ let find_map t ~f = Container.find_map ~iter t ~f let pp pe fmt t = iter t ~f:(fun instr -> F.fprintf fmt "%a;@\n" (Sil.pp_instr ~print_types:false pe) instr) + + +(** Return the list of normal ids occurring in the instructions *) +let instrs_get_normal_vars instrs = + let do_instr res instr = + Sil.exps_of_instr instr + |> List.fold_left ~init:res ~f:(fun res e -> + Exp.free_vars e + |> Sequence.filter ~f:Ident.is_normal + |> Ident.hashqueue_of_sequence ~init:res ) + in + fold ~init:(Ident.HashQueue.create ()) ~f:do_instr instrs |> Ident.HashQueue.keys diff --git a/infer/src/IR/Instrs.mli b/infer/src/IR/Instrs.mli index d06830261..46f73fe31 100644 --- a/infer/src/IR/Instrs.mli +++ b/infer/src/IR/Instrs.mli @@ -34,11 +34,15 @@ val map : not_reversed t -> f:(Sil.instr -> Sil.instr) -> not_reversed t val map_and_fold : not_reversed t -> f:('a -> Sil.instr -> 'a * Sil.instr) -> init:'a -> not_reversed t - [@@warning "-32"] (** replace every instruction [instr] with [snd (f context instr)]. The context is computed by folding [f] on [init] and previous instructions (before [instr]) in the collection. Preserve physical equality. **) +val concat_map_and_fold : + not_reversed t -> f:('a -> Sil.instr -> 'a * Sil.instr array) -> init:'a -> not_reversed t +(** Like [map_and_fold] but replace every instruction [instr] with the list [snd (f context instr)] + by threading an accumulator. Preserve physical equality. **) + val concat_map : not_reversed t -> f:(Sil.instr -> Sil.instr array) -> not_reversed t (** replace every instruction [instr] with the list [f instr]. Preserve physical equality. **) @@ -67,3 +71,5 @@ val fold : (_ t, Sil.instr, 'a) Container.fold val iter : (_ t, Sil.instr) Container.iter val get_underlying_not_reversed : not_reversed t -> Sil.instr array + +val instrs_get_normal_vars : not_reversed t -> Ident.t list diff --git a/infer/src/IR/Procdesc.ml b/infer/src/IR/Procdesc.ml index a0cb04e7b..2e70ddca9 100644 --- a/infer/src/IR/Procdesc.ml +++ b/infer/src/IR/Procdesc.ml @@ -269,6 +269,16 @@ module Node = struct true ) + (** Concat map and replace the instructions to be executed using a context *) + let replace_instrs_by_using_context node ~f ~update_context ~context_at_node = + let f node context instr = (update_context context instr, f node context instr) in + let instrs' = Instrs.concat_map_and_fold node.instrs ~f:(f node) ~init:context_at_node in + if phys_equal instrs' node.instrs then false + else ( + node.instrs <- instrs' ; + true ) + + (** Like [replace_instrs], but 1 instr gets replaced by 0, 1, or more instructions. *) let replace_instrs_by node ~f = let instrs' = Instrs.concat_map node.instrs ~f:(f node) in @@ -594,6 +604,14 @@ let replace_instrs_using_context pdesc ~f ~update_context ~context_at_node = update_nodes pdesc ~update +let replace_instrs_by_using_context pdesc ~f ~update_context ~context_at_node = + let update node = + Node.replace_instrs_by_using_context ~f ~update_context ~context_at_node:(context_at_node node) + node + in + update_nodes pdesc ~update + + let replace_instrs_by pdesc ~f = let update node = Node.replace_instrs_by ~f node in update_nodes pdesc ~update diff --git a/infer/src/IR/Procdesc.mli b/infer/src/IR/Procdesc.mli index b9c83fda5..abdc1698e 100644 --- a/infer/src/IR/Procdesc.mli +++ b/infer/src/IR/Procdesc.mli @@ -293,6 +293,15 @@ val replace_instrs_using_context : (** Map and replace the instructions to be executed using a context that we built with previous instructions in the node. Returns true if at least one substitution occured. *) +val replace_instrs_by_using_context : + t + -> f:(Node.t -> 'a -> Sil.instr -> Sil.instr array) + -> update_context:('a -> Sil.instr -> 'a) + -> context_at_node:(Node.t -> 'a) + -> bool +(** Like [replace_instrs_using_context], but slower, and each instruction may be replaced by 0, 1, + or more instructions. *) + val replace_instrs_by : t -> f:(Node.t -> Sil.instr -> Sil.instr array) -> bool (** Like [replace_instrs], but slower, and each instruction may be replaced by 0, 1, or more instructions. *) diff --git a/infer/src/backend/ClosureSubstSpecializedMethod.ml b/infer/src/backend/ClosureSubstSpecializedMethod.ml index e70cbd66d..b2287ad73 100644 --- a/infer/src/backend/ClosureSubstSpecializedMethod.ml +++ b/infer/src/backend/ClosureSubstSpecializedMethod.ml @@ -6,6 +6,7 @@ *) open! IStd module CFG = ProcCfg.Normal +module L = Logging module PPPVar = struct type t = Pvar.t [@@deriving compare, equal] @@ -16,24 +17,26 @@ end module VDom = AbstractDomain.Flat (PPPVar) module Domain = AbstractDomain.SafeInvertedMap (Ident) (VDom) +let eval_instr astate instr = + let open Sil in + match instr with + | Load {id; e= Exp.Lvar pvar} -> + Domain.add id (VDom.v pvar) astate + | Load {id} -> + Domain.add id VDom.top astate + | Call ((id, _), _, _, _, _) -> + Domain.add id VDom.top astate + | _ -> + astate + + module TransferFunctions = struct module CFG = CFG module Domain = Domain type analysis_data = unit - let exec_instr astate _analysis_data _node instr = - let open Sil in - match instr with - | Load {id; e= Exp.Lvar pvar} -> - Domain.add id (VDom.v pvar) astate - | Load {id} -> - Domain.add id VDom.top astate - | Call ((id, _), _, _, _, _) -> - Domain.add id VDom.top astate - | _ -> - astate - + let exec_instr astate _ _node instr = eval_instr astate instr let pp_session_name node fmt = Format.fprintf fmt "Closure Subst Specialized Method %a" CFG.Node.pp_id (CFG.Node.id node) @@ -41,7 +44,7 @@ end module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions) -let exec_instr domain proc_name formals_to_blocks_map _node instr = +let exec_instr proc_name formals_to_blocks_map domain instr = let open Sil in let res = let exec_exp exp = @@ -71,6 +74,7 @@ let exec_instr domain proc_name formals_to_blocks_map _node instr = extra_formals |> List.unzip in + L.debug Capture Verbose "substituting specialized method@\n" ; load_instrs @ [ Call (ret_id_typ, Const (Cfun procname), extra_args @ converted_args, loc, call_flags) @@ -88,6 +92,14 @@ let exec_instr domain proc_name formals_to_blocks_map _node instr = Array.of_list res +let analyze_at_node (map : Analyzer.invariant_map) node : Domain.t = + match Analyzer.InvariantMap.find_opt (Procdesc.Node.get_id node) map with + | Some abstate -> + abstate.pre + | None -> + Domain.top + + let process summary = let pdesc = Summary.get_proc_desc summary in let proc_name = Procdesc.get_proc_name pdesc in @@ -95,19 +107,22 @@ let process summary = match proc_attributes.ProcAttributes.specialized_with_blocks_info with | Some spec_with_blocks_info -> ( match AnalysisCallbacks.get_proc_desc spec_with_blocks_info.orig_proc with - | Some orig_proc_desc -> ( + | Some orig_proc_desc -> let formals_to_blocks_map = spec_with_blocks_info.formals_to_procs_and_new_formals in Procdesc.shallow_copy_code_from_pdesc ~orig_pdesc:orig_proc_desc ~dest_pdesc:pdesc ; - let analysis_data = () in - match Analyzer.compute_post ~initial:Domain.empty analysis_data pdesc with - | Some domain -> - let used_ids = Domain.bindings domain |> List.map ~f:fst in - Ident.update_name_generator used_ids ; - Procdesc.replace_instrs_by pdesc ~f:(exec_instr domain proc_name formals_to_blocks_map) - |> ignore ; - () - | None -> - () ) + let node_cfg = CFG.from_pdesc pdesc in + let invariant_map = Analyzer.exec_cfg node_cfg () ~initial:Domain.empty in + let update_context = eval_instr in + CFG.fold_nodes node_cfg ~init:() ~f:(fun _ node -> + let used_ids = Instrs.instrs_get_normal_vars (CFG.instrs node) in + Ident.update_name_generator used_ids ) ; + let replace_instr _node = exec_instr proc_name formals_to_blocks_map in + let context_at_node node = analyze_at_node invariant_map node in + let _has_changed : bool = + Procdesc.replace_instrs_by_using_context pdesc ~f:replace_instr ~update_context + ~context_at_node + in + () | _ -> () ) | _ -> diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml index 4f0454405..92dc7daef 100644 --- a/infer/src/biabduction/interproc.ml +++ b/infer/src/biabduction/interproc.ml @@ -354,25 +354,13 @@ exception RE_EXE_ERROR let pp_name fmt = F.pp_print_string fmt "biabduction" -(** Return the list of normal ids occurring in the instructions *) -let instrs_get_normal_vars instrs = - let do_instr res instr = - Sil.exps_of_instr instr - |> List.fold_left ~init:res ~f:(fun res e -> - Exp.free_vars e - |> Sequence.filter ~f:Ident.is_normal - |> Ident.hashqueue_of_sequence ~init:res ) - in - Instrs.fold ~init:(Ident.HashQueue.create ()) ~f:do_instr instrs |> Ident.HashQueue.keys - - (** Perform symbolic execution for a node starting from an initial prop *) let do_symbolic_execution ({InterproceduralAnalysis.tenv; _} as analysis_data) proc_cfg handle_exn (node : ProcCfg.Exceptional.Node.t) (prop : Prop.normal Prop.t) (path : Paths.Path.t) = State.mark_execution_start node ; let instrs = ProcCfg.Exceptional.instrs node in (* fresh normal vars must be fresh w.r.t. instructions *) - Ident.update_name_generator (instrs_get_normal_vars instrs) ; + Ident.update_name_generator (Instrs.instrs_get_normal_vars instrs) ; let pset = SymExec.node handle_exn analysis_data proc_cfg node (Paths.PathSet.from_renamed_list [(prop, path)]) diff --git a/infer/tests/codetoanalyze/objc/autoreleasepool/arc_block.m b/infer/tests/codetoanalyze/objc/autoreleasepool/arc_block.m index 222a619cc..d623daf43 100644 --- a/infer/tests/codetoanalyze/objc/autoreleasepool/arc_block.m +++ b/infer/tests/codetoanalyze/objc/autoreleasepool/arc_block.m @@ -29,4 +29,37 @@ int i = [x indexOfObjectPassingTest:b]; } +BOOL x; + +- (void)conditionalRunBlock:(dispatch_block_t)block { + if (x) { + block(); + } +} + +- (void)call_ConditionalRunBlock_linear:(int)k { + int i = 0; + while (i < k) { + [self conditionalRunBlock:^{ + NoArcCallee* o = [NoArcCallee giveMeObject]; + }]; + i++; + } +} + +- (void)callBlock:(dispatch_block_t)block { + dispatch_block_t local_block = block; + local_block(); // pre-analysis can't specialize here and we drop the trace +} + +- (void)call_CallBlock_linear:(int)k { + int i = 0; + while (i < k) { + [self callBlock:^{ + NoArcCallee* o = [NoArcCallee giveMeObject]; + }]; + i++; + } +} + @end diff --git a/infer/tests/codetoanalyze/objc/autoreleasepool/cost-issues.exp b/infer/tests/codetoanalyze/objc/autoreleasepool/cost-issues.exp index a60d54d66..328f79a8b 100644 --- a/infer/tests/codetoanalyze/objc/autoreleasepool/cost-issues.exp +++ b/infer/tests/codetoanalyze/objc/autoreleasepool/cost-issues.exp @@ -1,10 +1,18 @@ ${XCODE_ISYSROOT}/System/Library/Frameworks/Foundation.framework/Headers/NSArray.h, NSArray.indexOfObjectPassingTest:[objc_blockArcBlock.callIndexOfObjectPassingTest_linear:_1], 0, OnUIThread:false, [] ${XCODE_ISYSROOT}/System/Library/Frameworks/Foundation.framework/Headers/NSArray.h, NSArray.indexOfObjectPassingTest:[objc_blockArcBlock.callIndexOfObjectPassingTest_param_linear:_2], 0, OnUIThread:false, [] +codetoanalyze/objc/autoreleasepool/arc_block.m, ArcBlock.callBlock:, |block|, OnUIThread:false, [] +codetoanalyze/objc/autoreleasepool/arc_block.m, ArcBlock.callBlock:[objc_blockArcBlock.call_CallBlock_linear:_4], |block|, OnUIThread:false, [] codetoanalyze/objc/autoreleasepool/arc_block.m, ArcBlock.callIndexOfObjectPassingTest_linear:, x->elements.length.ub, OnUIThread:false, [{x->elements.length.ub},Modeled call to indexOfObjectPassingTest:,autorelease,Call to NoArcCallee.giveMeObject,Modeled call to NSObject.autorelease] codetoanalyze/objc/autoreleasepool/arc_block.m, ArcBlock.callIndexOfObjectPassingTest_param_linear:, x->elements.length.ub, OnUIThread:false, [{x->elements.length.ub},Modeled call to indexOfObjectPassingTest:,autorelease,Call to NoArcCallee.giveMeObject,Modeled call to NSObject.autorelease] +codetoanalyze/objc/autoreleasepool/arc_block.m, ArcBlock.call_CallBlock_linear:, k, OnUIThread:false, [{k},Loop] +codetoanalyze/objc/autoreleasepool/arc_block.m, ArcBlock.call_ConditionalRunBlock_linear:, k, OnUIThread:false, [{k},Loop,autorelease,Call to ArcBlock.conditionalRunBlock:[objc_blockArcBlock.call_ConditionalRunBlock_linear:_3],Call to objc_blockArcBlock.call_ConditionalRunBlock_linear:_3,Call to NoArcCallee.giveMeObject,Modeled call to NSObject.autorelease] +codetoanalyze/objc/autoreleasepool/arc_block.m, ArcBlock.conditionalRunBlock:, |block|, OnUIThread:false, [] +codetoanalyze/objc/autoreleasepool/arc_block.m, ArcBlock.conditionalRunBlock:[objc_blockArcBlock.call_ConditionalRunBlock_linear:_3], 1, OnUIThread:false, [autorelease,Call to objc_blockArcBlock.call_ConditionalRunBlock_linear:_3,Call to NoArcCallee.giveMeObject,Modeled call to NSObject.autorelease] codetoanalyze/objc/autoreleasepool/arc_block.m, ArcBlock.dealloc, 0, OnUIThread:false, [] codetoanalyze/objc/autoreleasepool/arc_block.m, objc_blockArcBlock.callIndexOfObjectPassingTest_linear:_1, 1, OnUIThread:false, [autorelease,Call to NoArcCallee.giveMeObject,Modeled call to NSObject.autorelease] codetoanalyze/objc/autoreleasepool/arc_block.m, objc_blockArcBlock.callIndexOfObjectPassingTest_param_linear:_2, 1, OnUIThread:false, [autorelease,Call to NoArcCallee.giveMeObject,Modeled call to NSObject.autorelease] +codetoanalyze/objc/autoreleasepool/arc_block.m, objc_blockArcBlock.call_CallBlock_linear:_4, 1, OnUIThread:false, [autorelease,Call to NoArcCallee.giveMeObject,Modeled call to NSObject.autorelease] +codetoanalyze/objc/autoreleasepool/arc_block.m, objc_blockArcBlock.call_ConditionalRunBlock_linear:_3, 1, OnUIThread:false, [autorelease,Call to NoArcCallee.giveMeObject,Modeled call to NSObject.autorelease] codetoanalyze/objc/autoreleasepool/arc_callee.m, ArcCallee.allocObject, 0, OnUIThread:false, [] codetoanalyze/objc/autoreleasepool/arc_callee.m, ArcCallee.copyObject:, 0, OnUIThread:false, [] codetoanalyze/objc/autoreleasepool/arc_callee.m, ArcCallee.dealloc, 0, OnUIThread:false, [] diff --git a/infer/tests/codetoanalyze/objc/autoreleasepool/issues.exp b/infer/tests/codetoanalyze/objc/autoreleasepool/issues.exp index 75a04ebb0..64a28eaa6 100644 --- a/infer/tests/codetoanalyze/objc/autoreleasepool/issues.exp +++ b/infer/tests/codetoanalyze/objc/autoreleasepool/issues.exp @@ -1,5 +1,7 @@ codetoanalyze/objc/autoreleasepool/arc_block.m, ArcBlock.callIndexOfObjectPassingTest_linear:, 0, EXPENSIVE_AUTORELEASEPOOL_SIZE, no_bucket, ERROR, [{x->elements.length.ub},Modeled call to indexOfObjectPassingTest:,autorelease,Call to NoArcCallee.giveMeObject,Modeled call to NSObject.autorelease] codetoanalyze/objc/autoreleasepool/arc_block.m, ArcBlock.callIndexOfObjectPassingTest_param_linear:, 0, EXPENSIVE_AUTORELEASEPOOL_SIZE, no_bucket, ERROR, [{x->elements.length.ub},Modeled call to indexOfObjectPassingTest:,autorelease,Call to NoArcCallee.giveMeObject,Modeled call to NSObject.autorelease] +codetoanalyze/objc/autoreleasepool/arc_block.m, ArcBlock.call_CallBlock_linear:, 0, EXPENSIVE_AUTORELEASEPOOL_SIZE, no_bucket, ERROR, [{k},Loop] +codetoanalyze/objc/autoreleasepool/arc_block.m, ArcBlock.call_ConditionalRunBlock_linear:, 0, EXPENSIVE_AUTORELEASEPOOL_SIZE, no_bucket, ERROR, [{k},Loop,autorelease,Call to ArcBlock.conditionalRunBlock:[objc_blockArcBlock.call_ConditionalRunBlock_linear:_3],Call to objc_blockArcBlock.call_ConditionalRunBlock_linear:_3,Call to NoArcCallee.giveMeObject,Modeled call to NSObject.autorelease] codetoanalyze/objc/autoreleasepool/arc_caller.m, ArcCaller.callGiveMeObject_linear:, 0, EXPENSIVE_AUTORELEASEPOOL_SIZE, no_bucket, ERROR, [{n},Loop,autorelease,Call to NoArcCallee.giveMeObject,Modeled call to NSObject.autorelease] codetoanalyze/objc/autoreleasepool/arc_enumerator.m, ArcEnumerator.callMyEnumerator_linear_FP:, 0, EXPENSIVE_AUTORELEASEPOOL_SIZE, no_bucket, ERROR, [{x->elements.length.ub + 1},Call to MyEnumerator.nextObject,Loop,{x->elements.length.ub + 1},Call to MyEnumerator.nextObject,Loop,{x->elements.length.ub + 1},Loop] codetoanalyze/objc/autoreleasepool/arc_enumerator.m, ArcEnumerator.callMyEnumerator_nextObject_linear:, 0, EXPENSIVE_AUTORELEASEPOOL_SIZE, no_bucket, ERROR, [{x->elements.length.ub + 1},Call to MyEnumerator.nextObject,Loop]