diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index ac689d30f..69bb7c8fa 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -1897,6 +1897,21 @@ let replace_objc_null prop lhs_exp rhs_exp = add_or_replace_exp_attribute prop lhs_exp att | _ -> prop +let rec nullify_exp_with_objc_null prop exp = + match exp with + | Sil.BinOp (op, exp1, exp2) -> + let prop' = nullify_exp_with_objc_null prop exp1 in + nullify_exp_with_objc_null prop' exp2 + | Sil.UnOp (op, exp, _) -> + nullify_exp_with_objc_null prop exp + | Sil.Var name -> + (match get_objc_null_attribute prop exp with + | Some att -> + let prop' = remove_attribute_from_exp att prop exp in + conjoin_eq exp Sil.exp_zero prop' + | _ -> prop) + | _ -> prop + (** Get all the attributes of the prop *) let get_atoms_with_attribute att prop = let atom_remove atom autoreleased_atoms = match atom with diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli index 42080fabb..ff1592d18 100644 --- a/infer/src/backend/prop.mli +++ b/infer/src/backend/prop.mli @@ -312,6 +312,8 @@ val remove_attribute : Sil.attribute -> 'a t -> normal t (** [replace_objc_null lhs rhs]. If rhs has the objc_null attribute, replace the attribute and set the lhs = 0 *) val replace_objc_null : normal t -> exp -> exp -> normal t +val nullify_exp_with_objc_null : normal t -> exp -> normal t + (** Remove an attribute from an exp in the heap *) val remove_attribute_from_exp : Sil.attribute -> 'a t -> exp -> normal t diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index bde99cf23..e2fb415ad 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -953,6 +953,7 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path execute_set pname pdesc tenv lhs_exp typ rhs_exp loc _prop |> ret_old_path | Sil.Prune (cond, loc, true_branch, ik) -> + let _prop = Prop.nullify_exp_with_objc_null _prop cond in let check_condition_always_true_false () = let report_condition_always_true_false i = let skip_loop = match ik with diff --git a/infer/tests/codetoanalyze/objc/errors/npe/ObjCMethodCallInCondition.m b/infer/tests/codetoanalyze/objc/errors/npe/ObjCMethodCallInCondition.m new file mode 100644 index 000000000..69358418f --- /dev/null +++ b/infer/tests/codetoanalyze/objc/errors/npe/ObjCMethodCallInCondition.m @@ -0,0 +1,41 @@ +/* + * Copyright (c) 2015 - 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 +#import + +@interface A : NSObject + +@property (nonatomic) A* child; + +@property (nonatomic) A* url; + +@end + +@implementation A + +- (void)testLength:(NSData *)imageData +{ + unsigned char *pixels = (unsigned char *)[imageData bytes]; + + if (imageData.length > 0) { + pixels[0] = 255; + } +} + +A* testUrl(A* context) +{ + if (context.url) { + A* entityMemObject = context.child; + return entityMemObject->_child; + } + return nil; +} + +@end diff --git a/infer/tests/endtoend/objc/NPEObjCMethodInConditionTest.java b/infer/tests/endtoend/objc/NPEObjCMethodInConditionTest.java new file mode 100644 index 000000000..8a0524146 --- /dev/null +++ b/infer/tests/endtoend/objc/NPEObjCMethodInConditionTest.java @@ -0,0 +1,64 @@ +/* + * Copyright (c) 2013 - 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. + */ + +package endtoend.objc; + +import static org.hamcrest.MatcherAssert.assertThat; +import static utils.matchers.ResultContainsExactly.containsExactly; + +import com.google.common.collect.ImmutableList; + +import org.junit.BeforeClass; +import org.junit.ClassRule; +import org.junit.Test; + +import java.io.IOException; + +import utils.DebuggableTemporaryFolder; +import utils.InferException; +import utils.InferResults; +import utils.InferRunner; + +public class NPEObjCMethodInConditionTest { + + public static final String NPE_FILE = + "infer/tests/codetoanalyze/objc/errors/npe/ObjCMethodCallInCondition.m"; + + private static ImmutableList inferCmdNPD; + + public static final String PARAMETER_NOT_NULL_CHECKED = "PARAMETER_NOT_NULL_CHECKED"; + + @ClassRule + public static DebuggableTemporaryFolder folderNPD = new DebuggableTemporaryFolder(); + + @BeforeClass + public static void runInfer() throws InterruptedException, IOException { + inferCmdNPD = InferRunner.createiOSInferCommandWithMLBuckets( + folderNPD, + NPE_FILE, + "cf", + true); + } + + @Test + public void whenInferRunsOncaptureManagerSessionDidStartThenNoNPEFound() + throws InterruptedException, IOException, InferException { + InferResults inferResults = InferRunner.runInferObjC(inferCmdNPD); + String[] procedures = {}; + assertThat( + "Results should not contain parameter not null checked", + inferResults, + containsExactly( + PARAMETER_NOT_NULL_CHECKED, + NPE_FILE, + procedures + ) + ); + } +}