[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 (c47911359a), 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

@@ -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}

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

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

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

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. *)

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
+        ()
     | _ ->
         () )
   | _ ->

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)])

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

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, []

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]