From 6df4fb6a9bfe4a48052090e2fc3f54e4967e678b Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Fri, 15 Nov 2019 07:46:36 -0800 Subject: [PATCH] [pulse] report dereference of NULL and constants Summary: Note: Disabled by default. Having some support for values, we can report when a null or constant value is being dereferenced. The particularity here is that we don't report when 0 is a possible value for the address, or even if we know that the value of the address can only be 0 in that branch! Instead, we allow ourselves to report only when we the address has been *set* to NULL (or any constant). This is in line with how pulse deals with other issues: only report when 1. we see an address become invalid, and 2. we see the same address be used later on Reviewed By: skcho Differential Revision: D17665468 fbshipit-source-id: f1ccf94cf --- infer/man/man1/infer-full.txt | 2 + infer/man/man1/infer-report.txt | 2 + infer/man/man1/infer.txt | 2 + infer/src/base/IssueType.ml | 6 ++ infer/src/base/IssueType.mli | 4 ++ infer/src/pulse/PulseAttribute.ml | 4 +- infer/src/pulse/PulseBaseMemory.ml | 4 +- infer/src/pulse/PulseInvalidation.ml | 18 +++--- infer/src/pulse/PulseInvalidation.mli | 2 +- infer/src/pulse/PulseOperations.ml | 3 + .../tests/codetoanalyze/cpp/pulse/issues.exp | 2 + .../tests/codetoanalyze/cpp/pulse/nullptr.cpp | 57 +++++++++++++++++++ 12 files changed, 95 insertions(+), 11 deletions(-) create mode 100644 infer/tests/codetoanalyze/cpp/pulse/nullptr.cpp diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 93961a8c1..e2e9f40c6 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -373,6 +373,7 @@ OPTIONS COMPONENT_WITH_UNCONVENTIONAL_SUPERCLASS (enabled by default), CONDITION_ALWAYS_FALSE (disabled by default), CONDITION_ALWAYS_TRUE (disabled by default), + CONSTANT_ADDRESS_DEREFERENCE (disabled by default), CREATE_INTENT_FROM_URI (enabled by default), CROSS_SITE_SCRIPTING (enabled by default), Cannot_star (enabled by default), @@ -448,6 +449,7 @@ OPTIONS MIXED_SELF_WEAKSELF (enabled by default), MUTABLE_LOCAL_VARIABLE_IN_COMPONENT_FILE (enabled by default), Missing_fld (enabled by default), + NULLPTR_DEREFERENCE (disabled by default), NULLSAFE_FIELD_NOT_NULLABLE (enabled by default), NULLSAFE_NULLABLE_DEREFERENCE (enabled by default), NULL_DEREFERENCE (enabled by default), diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index ae20cc1cb..cd353c489 100644 --- a/infer/man/man1/infer-report.txt +++ b/infer/man/man1/infer-report.txt @@ -115,6 +115,7 @@ OPTIONS COMPONENT_WITH_UNCONVENTIONAL_SUPERCLASS (enabled by default), CONDITION_ALWAYS_FALSE (disabled by default), CONDITION_ALWAYS_TRUE (disabled by default), + CONSTANT_ADDRESS_DEREFERENCE (disabled by default), CREATE_INTENT_FROM_URI (enabled by default), CROSS_SITE_SCRIPTING (enabled by default), Cannot_star (enabled by default), @@ -190,6 +191,7 @@ OPTIONS MIXED_SELF_WEAKSELF (enabled by default), MUTABLE_LOCAL_VARIABLE_IN_COMPONENT_FILE (enabled by default), Missing_fld (enabled by default), + NULLPTR_DEREFERENCE (disabled by default), NULLSAFE_FIELD_NOT_NULLABLE (enabled by default), NULLSAFE_NULLABLE_DEREFERENCE (enabled by default), NULL_DEREFERENCE (enabled by default), diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 3dc0c52aa..8f5e0dbd7 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -373,6 +373,7 @@ OPTIONS COMPONENT_WITH_UNCONVENTIONAL_SUPERCLASS (enabled by default), CONDITION_ALWAYS_FALSE (disabled by default), CONDITION_ALWAYS_TRUE (disabled by default), + CONSTANT_ADDRESS_DEREFERENCE (disabled by default), CREATE_INTENT_FROM_URI (enabled by default), CROSS_SITE_SCRIPTING (enabled by default), Cannot_star (enabled by default), @@ -448,6 +449,7 @@ OPTIONS MIXED_SELF_WEAKSELF (enabled by default), MUTABLE_LOCAL_VARIABLE_IN_COMPONENT_FILE (enabled by default), Missing_fld (enabled by default), + NULLPTR_DEREFERENCE (disabled by default), NULLSAFE_FIELD_NOT_NULLABLE (enabled by default), NULLSAFE_NULLABLE_DEREFERENCE (enabled by default), NULL_DEREFERENCE (enabled by default), diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index aa55ed446..58c2ac909 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -197,6 +197,10 @@ let condition_always_false = register_from_string ~enabled:false "CONDITION_ALWA let condition_always_true = register_from_string ~enabled:false "CONDITION_ALWAYS_TRUE" +let constant_address_dereference = + register_from_string ~enabled:false "CONSTANT_ADDRESS_DEREFERENCE" + + let create_intent_from_uri = register_from_string "CREATE_INTENT_FROM_URI" let cross_site_scripting = register_from_string "CROSS_SITE_SCRIPTING" @@ -355,6 +359,8 @@ let null_dereference = register_from_string "NULL_DEREFERENCE" let null_test_after_dereference = register_from_string ~enabled:false "NULL_TEST_AFTER_DEREFERENCE" +let nullptr_dereference = register_from_string ~enabled:false "NULLPTR_DEREFERENCE" + let nullsafe_field_not_nullable = register_from_string "NULLSAFE_FIELD_NOT_NULLABLE" ~hum:"Field Not Nullable" diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 07ca4c44a..5cc5bd7e7 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -119,6 +119,8 @@ val condition_always_false : t val condition_always_true : t +val constant_address_dereference : t + val create_intent_from_uri : t val cross_site_scripting : t @@ -238,6 +240,8 @@ val null_dereference : t val null_test_after_dereference : t +val nullptr_dereference : t + val nullsafe_field_not_nullable : t val nullsafe_nullable_dereference : t diff --git a/infer/src/pulse/PulseAttribute.ml b/infer/src/pulse/PulseAttribute.ml index c26594b9c..cf57bb15d 100644 --- a/infer/src/pulse/PulseAttribute.ml +++ b/infer/src/pulse/PulseAttribute.ml @@ -54,7 +54,9 @@ module Attribute = struct Variants.to_rank (AddressOfStackVariable (var, location, [])) - let invalid_rank = Variants.to_rank (Invalid (Invalidation.Nullptr, dummy_trace)) + let invalid_rank = + Variants.to_rank (Invalid (Invalidation.ConstantDereference IntLit.zero, dummy_trace)) + let must_be_valid_rank = Variants.to_rank (MustBeValid dummy_trace) diff --git a/infer/src/pulse/PulseBaseMemory.ml b/infer/src/pulse/PulseBaseMemory.ml index 980bf1207..9b099838d 100644 --- a/infer/src/pulse/PulseBaseMemory.ml +++ b/infer/src/pulse/PulseBaseMemory.ml @@ -75,10 +75,10 @@ let invalidate (address, history) invalidation location memory = let check_valid address memory = L.d_printfln "Checking validity of %a" AbstractValue.pp address ; match Graph.find_opt address (snd memory) |> Option.bind ~f:Attributes.get_invalid with - | Some invalidation -> - Error invalidation | None -> Ok () + | Some invalidation -> + Error invalidation let get_attribute getter address memory = diff --git a/infer/src/pulse/PulseInvalidation.ml b/infer/src/pulse/PulseInvalidation.ml index 2fa3441bc..1cff9abd8 100644 --- a/infer/src/pulse/PulseInvalidation.ml +++ b/infer/src/pulse/PulseInvalidation.ml @@ -39,21 +39,23 @@ let pp_std_vector_function f = function type t = | CFree + | ConstantDereference of IntLit.t | CppDelete | GoneOutOfScope of Pvar.t * Typ.t - | Nullptr | StdVector of std_vector_function [@@deriving compare] let issue_type_of_cause = function | CFree -> IssueType.use_after_free + | ConstantDereference i when IntLit.iszero i -> + IssueType.nullptr_dereference + | ConstantDereference _ -> + IssueType.constant_address_dereference | CppDelete -> IssueType.use_after_delete | GoneOutOfScope _ -> IssueType.use_after_lifetime - | Nullptr -> - IssueType.null_dereference | StdVector _ -> IssueType.vector_invalidation @@ -62,6 +64,10 @@ let describe f cause = match cause with | CFree -> F.pp_print_string f "was invalidated by call to `free()`" + | ConstantDereference i when IntLit.iszero i -> + F.pp_print_string f "is the null pointer" + | ConstantDereference i -> + F.fprintf f "is the constant %a" IntLit.pp i | CppDelete -> F.pp_print_string f "was invalidated by `delete`" | GoneOutOfScope (pvar, typ) -> @@ -71,8 +77,6 @@ let describe f cause = else F.fprintf f "is the address of a stack variable `%a`" Pvar.pp_value pvar in F.fprintf f "%a whose lifetime has ended" pp_var pvar - | Nullptr -> - F.pp_print_string f "is the null pointer" | StdVector std_vector_f -> F.fprintf f "was potentially invalidated by `%a()`" pp_std_vector_function std_vector_f @@ -81,11 +85,11 @@ let pp f invalidation = match invalidation with | CFree -> F.fprintf f "CFree(%a)" describe invalidation + | ConstantDereference _ -> + F.fprintf f "ConstantDereference(%a)" describe invalidation | CppDelete -> F.fprintf f "CppDelete(%a)" describe invalidation | GoneOutOfScope _ -> describe f invalidation - | Nullptr -> - describe f invalidation | StdVector _ -> F.fprintf f "StdVector(%a)" describe invalidation diff --git a/infer/src/pulse/PulseInvalidation.mli b/infer/src/pulse/PulseInvalidation.mli index 76eadb842..b15e7b8ed 100644 --- a/infer/src/pulse/PulseInvalidation.mli +++ b/infer/src/pulse/PulseInvalidation.mli @@ -23,9 +23,9 @@ val pp_std_vector_function : F.formatter -> std_vector_function -> unit type t = | CFree + | ConstantDereference of IntLit.t | CppDelete | GoneOutOfScope of Pvar.t * Typ.t - | Nullptr | StdVector of std_vector_function [@@deriving compare] diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index dd46437fa..57d330954 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -137,6 +137,9 @@ let eval location exp0 astate = Memory.add_attribute addr (Arithmetic (Arithmetic.equal_to i, Immediate {location; history= []})) astate + |> Memory.invalidate + (addr, [ValueHistory.Assignment location]) + (ConstantDereference i) location in Ok (astate, (addr, [])) | Const _ | Sizeof _ | UnOp _ | BinOp _ | Exn _ -> diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index da9c130d1..417dc863b 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -20,6 +20,8 @@ codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_ codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_then_write_bad,when calling `wraps_delete` here,parameter `x` of wraps_delete,when calling `wraps_delete_inner` here,parameter `x` of wraps_delete_inner,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_then_write_bad,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here] codetoanalyze/cpp/pulse/interprocedural.cpp, feed_invalid_into_access_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `may_return_invalid_ptr_ok` here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `may_return_invalid_ptr_ok`,return from call to `may_return_invalid_ptr_ok`,assigned,when calling `call_store` here,parameter `y` of call_store,when calling `store` here,parameter `y` of store,invalid access occurs here] codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_bad,assigned,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_bad,assigned,assigned,assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/nullptr.cpp, deref_nullptr_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/nullptr.cpp, no_check_return_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `may_return_nullptr` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `may_return_nullptr`,return from call to `may_return_nullptr`,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_heap_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `rw` declared here,when calling `getwrapperHeap` here,variable `a` declared here,passed as argument to `WrapsB::WrapsB`,assigned,return from call to `WrapsB::WrapsB`,when calling `WrapsB::~WrapsB` here,parameter `this` of WrapsB::~WrapsB,when calling `WrapsB::__infer_inner_destructor_~WrapsB` here,parameter `this` of WrapsB::__infer_inner_destructor_~WrapsB,was invalidated by `delete`,use-after-lifetime part of the trace starts here,variable `rw` declared here,passed as argument to `getwrapperHeap`,variable `a` declared here,passed as argument to `WrapsB::WrapsB`,assigned,return from call to `WrapsB::WrapsB`,passed as argument to `ReferenceWrapperHeap::ReferenceWrapperHeap`,parameter `a` of ReferenceWrapperHeap::ReferenceWrapperHeap,passed as argument to `WrapsB::getb`,return from call to `WrapsB::getb`,assigned,return from call to `ReferenceWrapperHeap::ReferenceWrapperHeap`,return from call to `getwrapperHeap`,invalid access occurs here] codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_stack_bad, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `rw` declared here,when calling `getwrapperStack` here,variable `b` declared here,is the address of a stack variable `b` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `rw` declared here,passed as argument to `getwrapperStack`,variable `b` declared here,passed as argument to `ReferenceWrapperStack::ReferenceWrapperStack`,parameter `bref` of ReferenceWrapperStack::ReferenceWrapperStack,assigned,return from call to `ReferenceWrapperStack::ReferenceWrapperStack`,return from call to `getwrapperStack`,invalid access occurs here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_literal_stack_reference_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable `C++ temporary` declared here,returned here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/nullptr.cpp b/infer/tests/codetoanalyze/cpp/pulse/nullptr.cpp new file mode 100644 index 000000000..d153a9e8d --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/pulse/nullptr.cpp @@ -0,0 +1,57 @@ +/* + * 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. + */ +void assign_zero_ok() { + int x[2]; + x[1] = 42; +} + +void deref_nullptr_bad() { + int* p = nullptr; + *p = 42; +} + +void guarded_nullptr_ok() { + int* p = nullptr; + if (p != nullptr) { + *p = 42; + } +} + +struct X { + void foo(); +}; + +bool choice(); + +X* may_return_nullptr() { + if (choice) { + return nullptr; + } + return new X(); +} + +void no_check_return_bad() { + X* x = may_return_nullptr(); + x->foo(); +} + +void check_return_ok() { + X* x = may_return_nullptr(); + if (x != nullptr) { + x->foo(); + } +} + +void compare_to_null(void* x) { + if (x) { + } +} + +void deref_after_compare_ok(int* x) { + compare_to_null(x); + *x = 42; +}