diff --git a/infer/src/pulse/PulseJoin.ml b/infer/src/pulse/PulseJoin.ml index a07fc23659..89e4d1d537 100644 --- a/infer/src/pulse/PulseJoin.ml +++ b/infer/src/pulse/PulseJoin.ml @@ -200,7 +200,59 @@ let join_stacks astate_lhs astate_rhs = (join_state, (stack_pre_join, heap_pre_join), (stack_post_join, heap_post_join)) -let join_one_sided_attribute _attr = (* TODO: weaken the given attribute in most cases *) None +let join_one_sided_attribute (attr : Attribute.t) = + let weaken attr = + (* TODO: add weaker versions of some of the attributes so that we can distinguish when we have + lost precision on attributes or not (eg the pointer is null in all branches vs null in some + branches only. For now let's just pretend we always have the strong version. *) + attr + in + match attr with + | AlwaysReachable + (* maybe we want to be more forgiving, at least we get a closure to call even if it comes from + just one branch? *) + | Closure _ + | CSharpResourceReleased + | DictContainConstKeys + | HackConstinitCalled + | Initialized + | JavaResourceReleased + (* could move these two to the "keep if one sided" case if this creates too many FPs *) + | ReturnedFromUnknown _ + | UnknownEffect _ + (* could be more forgiving about one-sided [StaticType] too *) + | StaticType _ + | StdVectorReserve + (* harsh, but biased towards reporting more taint errors *) + | TaintSanitized _ + | UnreachableAt _ -> + None + | Allocated _ + | AwaitedAwaitable + | CopiedInto _ + | CopiedReturn _ + | InReportedRetainCycle + | LastLookup _ + | SourceOriginOfCopy _ + | StdMoved + | UsedAsBranchCond _ + | WrittenTo _ -> + Some attr + | AddressOfCppTemporary _ + | AddressOfStackVariable _ + | ConfigUsage _ + | DictReadConstKeys _ + | EndOfCollection + | HackBuilder _ + | Invalid _ + | MustBeInitialized _ + | MustBeValid _ + | MustNotBeTainted _ + | PropagateTaintFrom _ + | Tainted _ + | Uninitialized _ -> + Some (weaken attr) + let join_two_sided_attribute join_state (attr1 : Attribute.t) (attr2 : Attribute.t) : Attribute.t option = diff --git a/infer/tests/codetoanalyze/c/pulse-join/attributes.c b/infer/tests/codetoanalyze/c/pulse-join/attributes.c new file mode 100644 index 0000000000..140e1fafa1 --- /dev/null +++ b/infer/tests/codetoanalyze/c/pulse-join/attributes.c @@ -0,0 +1,64 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +// best run with --pulse-max-disjuncts 0 --pulse-over-approximate-reasoning + +#include + +int init_one_branch_only_bad() { + int x; + if (random()) { + x = 42; + } + return x; +} + +void FN_free_one_branch_only_bad() { + int* p = (int*)malloc(sizeof(int)); + if (random()) { + // FN because Invalid is used to represent freed locations and are kept by + // joining + free(p); + } +} + +// FN-ish: suppressed for now because we don't join histories properly +void FNsuppressed_invalid_one_branch_only_bad() { + int* p = NULL; + int x = 42; + if (random()) { + p = &x; + } + *p = 11; +} + +int* get_maybe_invalid_pointer(int a) { + if (a > 0) { + int* p = (int*)malloc(sizeof(int)); + while (!p) { + } + return p; + } + return NULL; +} + +void maybe_deref_pointer(int a, int* p) { + if (a > 0) { + *p = 42; + } +} + +// no interproc yet +void FN_interproc_joined_invalid_deref_bad() { + int* p = get_maybe_invalid_pointer(random()); + maybe_deref_pointer(random(), p); +} + +void interproc_path_sensitive_valid_deref_ok() { + int* p = get_maybe_invalid_pointer(10); + maybe_deref_pointer(10, p); +} diff --git a/infer/tests/codetoanalyze/c/pulse-join/issues.exp b/infer/tests/codetoanalyze/c/pulse-join/issues.exp index 1cd2d9f8ef..f0a7e78e25 100644 --- a/infer/tests/codetoanalyze/c/pulse-join/issues.exp +++ b/infer/tests/codetoanalyze/c/pulse-join/issues.exp @@ -1,3 +1,5 @@ +codetoanalyze/c/pulse-join/attributes.c, init_one_branch_only_bad, 5, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `x` declared here,read to uninitialized value occurs here] +codetoanalyze/c/pulse-join/attributes.c, FNsuppressed_invalid_one_branch_only_bad, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** SUPPRESSED ***,source of the null value part of the trace starts here,assigned,is assigned to the null pointer,null pointer dereference part of the trace starts here,invalid access occurs here] codetoanalyze/c/pulse-join/formula.c, FP_same_facts_different_branches_ok, 19, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse-join/formula.c, FP_same_facts_different_branches_ok, 23, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is assigned to the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse-join/join.c, join_valid_invalid_pointers, 1, NULLPTR_DEREFERENCE_LATENT, no_bucket, ERROR, [*** SUPPRESSED ***,source of the null value part of the trace starts here,is assigned to the null pointer,null pointer dereference part of the trace starts here,parameter `p` of join_valid_invalid_pointers,invalid access occurs here]