[backend] Fix consistency of closures after bi-abduction and other executions.

Summary:
The captured variables of a closure are tuples (id, var, typ) with the implicit assumption
that &var -> id holds in the heap. This is true when the closure is created, but is not enforce otherwise.
This becomes a problem when the closure is stored in the heap, goes passed a bi-abduction, and then it's executed
(see new test). This was failing before this diff and now succeeds.

We add the verification of this constraint to the normalization of sigma.

At the moment I expect Precondition_not_met to be removed, but also later, we will be able to compute retain cycles
over the closures, as the correct captured variable info is kept through the execution.

Reviewed By: jvillard

Differential Revision: D6796525

fbshipit-source-id: a8a7655

infer/src/backend/prop.ml

@@ -1415,6 +1415,65 @@ module Normalize = struct
     mk_ptsto tenv exp strexp te
 
 
+  (** Captured variables in the closures consist of expressions and variables, with the implicit
+      assumption that these two values are in the relation &var -> id. However, after bi-abduction, etc. 
+      the constraint may not hold anymore, so this function ensures that it is always kept. 
+      In particular, we have &var -> id iff we also have the pair (id, var) as part of captured variables. *)
+  let make_captured_in_closures_consistent sigma =
+    let open Sil in
+    let find_correct_captured captured =
+      let find_captured_variable_in_the_heap captured' hpred =
+        match hpred with
+        | Hpointsto (Exp.Lvar var, Eexp (Exp.Var id, _), _) ->
+            List.map
+              ~f:(fun ((e_captured, var_captured, t) as captured_item) ->
+                match e_captured with
+                | Exp.Var id_captured ->
+                    if Ident.equal id id_captured && Pvar.equal var var_captured then captured_item
+                    else if Ident.equal id id_captured then (e_captured, var, t)
+                    else if Pvar.equal var var_captured then (Exp.Var id, var_captured, t)
+                    else captured_item
+                | _ ->
+                    captured_item )
+              captured'
+        | _ ->
+            captured'
+      in
+      List.fold_left ~f:find_captured_variable_in_the_heap ~init:captured sigma
+    in
+    let process_closures exp =
+      match exp with
+      | Exp.Closure {name; captured_vars} ->
+          let correct_captured = find_correct_captured captured_vars in
+          if phys_equal captured_vars correct_captured then exp
+          else Exp.Closure {name; captured_vars= correct_captured}
+      | _ ->
+          exp
+    in
+    let rec process_closures_in_se se =
+      match se with
+      | Eexp (exp, inst) ->
+          let new_exp = process_closures exp in
+          if phys_equal exp new_exp then se else Eexp (new_exp, inst)
+      | Estruct (fields, inst) ->
+          let new_fields =
+            List.map ~f:(fun (field, se) -> (field, process_closures_in_se se)) fields
+          in
+          if phys_equal fields new_fields then se else Estruct (new_fields, inst)
+      | _ ->
+          se
+    in
+    let process_closures_in_the_heap hpred =
+      match hpred with
+      | Hpointsto (e, se, inst) ->
+          let new_se = process_closures_in_se se in
+          if phys_equal new_se se then hpred else Hpointsto (e, new_se, inst)
+      | _ ->
+          hpred
+    in
+    List.map ~f:process_closures_in_the_heap sigma
+
+
   let rec hpred_normalize tenv sub (hpred: Sil.hpred) : Sil.hpred =
     let replace_hpred hpred' =
       L.d_strln "found array with sizeof(..) size" ;
@@ -1500,7 +1559,8 @@ module Normalize = struct
 
   let sigma_normalize tenv sub sigma =
     let sigma' =
-      List.stable_sort ~cmp:Sil.compare_hpred (List.map ~f:(hpred_normalize tenv sub) sigma)
+      List.map ~f:(hpred_normalize tenv sub) sigma |> make_captured_in_closures_consistent
+      |> List.stable_sort ~cmp:Sil.compare_hpred
     in
     if equal_sigma sigma sigma' then sigma else sigma'
 

infer/tests/codetoanalyze/objc/errors/Makefile

@@ -86,6 +86,7 @@ SOURCES_BUCKET_ALL = \
 
 SOURCES_ARC = \
   field_superclass/SubtypingExample.m \
+	blocks_in_heap/BlockInHeap.m \
   initialization/struct_initlistexpr.c \
 	memory_leaks_benchmark/RetainCycleExampleWeak.m \
   memory_leaks_benchmark/RetainReleaseExampleBucketingArc.m \

infer/tests/codetoanalyze/objc/errors/blocks_in_heap/BlockInHeap.m

@@ -0,0 +1,47 @@
+/*
+ * Copyright (c) 2018 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+#import <Foundation/NSObject.h>
+
+@interface BlockInHeap : NSObject
+
+typedef void (^BlockInHeapHandler)(BlockInHeap* name);
+
+@property(nonatomic, strong) BlockInHeapHandler handler;
+
+@property(nonatomic, strong) BlockInHeap* child;
+
+@end
+
+@implementation BlockInHeap
+
+- (void)assign_block_to_ivar {
+  self.handler = ^(BlockInHeap* b) {
+    self->_child = b;
+  };
+}
+
+@end
+
+int block_in_heap_executed_after_bi_abduction_ok() {
+  BlockInHeap* c = [[BlockInHeap alloc] init];
+  [c assign_block_to_ivar];
+  BlockInHeap* b = [[BlockInHeap alloc] init];
+  c.handler(b);
+  return 5;
+}
+
+int block_in_heap_executed_after_bi_abduction_ok_test() {
+  if (block_in_heap_executed_after_bi_abduction_ok() == 5) {
+    int* p = 0;
+    return *p;
+  } else {
+    int* p = 0;
+    return *p;
+  }
+}

infer/tests/codetoanalyze/objc/errors/issues.exp

@@ -19,9 +19,10 @@ codetoanalyze/objc/shared/block/BlockVar.m, BlockVar_capturedNullDeref, 5, NULL_
 codetoanalyze/objc/shared/block/BlockVar.m, BlockVar_navigateToURLInBackground, 8, NULL_DEREFERENCE, [start of procedure navigateToURLInBackground,start of procedure block,start of procedure test,return from a call to BlockVar_test,return from a call to objc_blockBlockVar_navigateToURLInBackground_1,Condition is true]
 codetoanalyze/objc/shared/block/block.m, main1, 31, DIVIDE_BY_ZERO, [start of procedure main1(),start of procedure block,start of procedure block,return from a call to objc_blockobjc_blockmain1_2_3,return from a call to objc_blockmain1_2,start of procedure block,return from a call to objc_blockmain1_1]
 codetoanalyze/objc/shared/block/block_no_args.m, My_manager_m, 10, NULL_DEREFERENCE, [start of procedure m,start of procedure block,return from a call to objc_blockMy_manager_m_1,Condition is true]
-codetoanalyze/objc/shared/block/block_release.m, My_manager_blockReleaseTODO, 5, MEMORY_LEAK, [start of procedure blockReleaseTODO]
+codetoanalyze/objc/shared/block/block_release.m, My_manager_blockReleaseTODO, 9, MEMORY_LEAK, [start of procedure blockReleaseTODO]
 codetoanalyze/objc/shared/category_procdesc/main.c, CategoryProcdescMain, 3, MEMORY_LEAK, [start of procedure CategoryProcdescMain(),Skipping performDaysWork: function or method not found]
 codetoanalyze/objc/shared/field_superclass/SuperExample.m, ASuper_init, 2, NULL_DEREFERENCE, [start of procedure init,start of procedure init,return from a call to BSuper_init]
+codetoanalyze/objc/errors/blocks_in_heap/BlockInHeap.m, block_in_heap_executed_after_bi_abduction_ok_test, 3, NULL_DEREFERENCE, [start of procedure block_in_heap_executed_after_bi_abduction_ok_test(),start of procedure block_in_heap_executed_after_bi_abduction_ok(),start of procedure assign_block_to_ivar,return from a call to BlockInHeap_assign_block_to_ivar,start of procedure block,return from a call to objc_blockBlockInHeap_assign_block_to_ivar_1,return from a call to block_in_heap_executed_after_bi_abduction_ok,Condition is true]
 codetoanalyze/objc/errors/field_superclass/SubtypingExample.m, Employee_initWithName:andAge:andEducation:, 3, NULL_TEST_AFTER_DEREFERENCE, [start of procedure initWithName:andAge:andEducation:,start of procedure initWithName:andAge:,return from a call to Person_initWithName:andAge:,Condition is false]
 codetoanalyze/objc/errors/field_superclass/SubtypingExample.m, Employee_initWithName:andAge:andEducation:, 6, DIVIDE_BY_ZERO, [start of procedure initWithName:andAge:andEducation:,start of procedure initWithName:andAge:,return from a call to Person_initWithName:andAge:,Condition is true]
 codetoanalyze/objc/errors/field_superclass/SubtypingExample.m, subtyping_test, 0, DIVIDE_BY_ZERO, [start of procedure subtyping_test(),start of procedure testFields(),start of procedure setEmployeeEducation:,return from a call to Employee_setEmployeeEducation:,start of procedure setAge:,return from a call to Person_setAge:,start of procedure setEmployeeEducation:,return from a call to Employee_setEmployeeEducation:,start of procedure getAge,return from a call to Person_getAge,return from a call to testFields]
@@ -86,8 +87,8 @@ codetoanalyze/objc/shared/annotations/nullable_annotations.m, User_otherUserName
 codetoanalyze/objc/shared/annotations/nullable_annotations.m, npe_property_nullable, 3, NULL_DEREFERENCE, [start of procedure npe_property_nullable(),Skipping child: function or method not found]
 codetoanalyze/objc/shared/annotations/nullable_annotations_fields.m, A_nullable_field, 3, NULL_DEREFERENCE, [start of procedure nullable_field,Skipping getA(): function or method not found]
 codetoanalyze/objc/shared/block/dispatch.m, DispatchA_dispatch_a_block_variable_from_macro_delivers_initialised_object, 3, DIVIDE_BY_ZERO, [start of procedure dispatch_a_block_variable_from_macro_delivers_initialised_object,start of procedure dispatch_a_block_variable_from_macro,Skipping _dispatch_once(): function or method not found,return from a call to DispatchA_dispatch_a_block_variable_from_macro]
-codetoanalyze/objc/shared/memory_leaks_benchmark/MemoryLeakExample.m, MemoryLeakExample_blockCapturedVarLeak, 3, MEMORY_LEAK, [start of procedure blockCapturedVarLeak]
+codetoanalyze/objc/shared/memory_leaks_benchmark/MemoryLeakExample.m, MemoryLeakExample_blockCapturedVarLeak, 6, MEMORY_LEAK, [start of procedure blockCapturedVarLeak,start of procedure block,return from a call to objc_blockMemoryLeakExample_blockCapturedVarLeak_1]
-codetoanalyze/objc/shared/memory_leaks_benchmark/MemoryLeakExample.m, MemoryLeakExample_blockFreeNoLeakTODO, 3, MEMORY_LEAK, [start of procedure blockFreeNoLeakTODO]
+codetoanalyze/objc/shared/memory_leaks_benchmark/MemoryLeakExample.m, MemoryLeakExample_blockFreeNoLeakTODO, 8, MEMORY_LEAK, [start of procedure blockFreeNoLeakTODO,start of procedure block,return from a call to objc_blockMemoryLeakExample_blockFreeNoLeakTODO_2]
 codetoanalyze/objc/shared/memory_leaks_benchmark/MemoryLeakExample.m, MemoryLeakExample_createCloseCrossGlyph:, 2, MEMORY_LEAK, [start of procedure createCloseCrossGlyph:,Skipping CGRectGetHeight(): function or method not found]
 codetoanalyze/objc/shared/memory_leaks_benchmark/MemoryLeakExample.m, MemoryLeakExample_measureFrameSizeForText, 1, MEMORY_LEAK, [start of procedure measureFrameSizeForText]
 codetoanalyze/objc/shared/memory_leaks_benchmark/MemoryLeakExample.m, MemoryLeakExample_regularLeak, 3, MEMORY_LEAK, [start of procedure regularLeak]