diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 649f0b230..1fcf2a519 100644 --- a/infer/src/backend/prop.ml +++ b/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' diff --git a/infer/tests/codetoanalyze/objc/errors/Makefile b/infer/tests/codetoanalyze/objc/errors/Makefile index 761d30adb..020ec78f5 100644 --- a/infer/tests/codetoanalyze/objc/errors/Makefile +++ b/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 \ diff --git a/infer/tests/codetoanalyze/objc/errors/blocks_in_heap/BlockInHeap.m b/infer/tests/codetoanalyze/objc/errors/blocks_in_heap/BlockInHeap.m new file mode 100644 index 000000000..7e6372f67 --- /dev/null +++ b/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 + +@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; + } +} diff --git a/infer/tests/codetoanalyze/objc/errors/issues.exp b/infer/tests/codetoanalyze/objc/errors/issues.exp index 858fde755..a8cc7ee70 100644 --- a/infer/tests/codetoanalyze/objc/errors/issues.exp +++ b/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_blockFreeNoLeakTODO, 3, MEMORY_LEAK, [start of procedure blockFreeNoLeakTODO] +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, 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]