From 6ecf4066e830b277460231ff5c6a72a737a78aab Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Fri, 15 Nov 2019 07:46:40 -0800 Subject: [PATCH] [pulse] model std::integral_constant Summary: cpp_initialization Reviewed By: skcho Differential Revision: D18528537 fbshipit-source-id: ab5f8038a --- infer/src/IR/ProcnameDispatcher.ml | 7 ++++ infer/src/IR/ProcnameDispatcher.mli | 5 +++ infer/src/pulse/PulseModels.ml | 15 ++++++++ .../tests/codetoanalyze/cpp/pulse/issues.exp | 2 ++ .../tests/codetoanalyze/cpp/pulse/nullptr.cpp | 35 +++++++++++++++++++ 5 files changed, 64 insertions(+) diff --git a/infer/src/IR/ProcnameDispatcher.ml b/infer/src/IR/ProcnameDispatcher.ml index da71d7f38..1be9a8a5d 100644 --- a/infer/src/IR/ProcnameDispatcher.ml +++ b/infer/src/IR/ProcnameDispatcher.ml @@ -381,6 +381,11 @@ module type Common = sig -> ('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out) name_matcher (** Ends template arguments and starts a name *) + val ( >::+ ) : + ('a, 'b, 'c, 'd, 'e, 'f, 'g) templ_matcher + -> ('a -> string -> bool) + -> ('a, 'b, 'c, 'd, 'e, 'f) name_matcher + val ( &+...>:: ) : ( 'context , 'f_in @@ -513,6 +518,8 @@ module Common = struct let ( >:: ) templ_matcher name = templ_matcher >! () &::! name + let ( >::+ ) templ_matcher f_name = templ_matcher >! () &::+! f_name + let ( &+...>:: ) templ_matcher name = templ_matcher &+...>! () &::! name let ( &:: ) name_matcher name = name_matcher <...>! () &::! name diff --git a/infer/src/IR/ProcnameDispatcher.mli b/infer/src/IR/ProcnameDispatcher.mli index 393d1d00c..33a8fd493 100644 --- a/infer/src/IR/ProcnameDispatcher.mli +++ b/infer/src/IR/ProcnameDispatcher.mli @@ -155,6 +155,11 @@ module type Common = sig -> ('context, 'f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out) name_matcher (** Ends template arguments and starts a name *) + val ( >::+ ) : + ('a, 'b, 'c, 'd, 'e, 'f, 'g) templ_matcher + -> ('a -> string -> bool) + -> ('a, 'b, 'c, 'd, 'e, 'f) name_matcher + val ( &+...>:: ) : ( 'context , 'f_in diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 4d2b91e20..7a9b58476 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -7,6 +7,7 @@ open! IStd open Result.Monad_infix open PulseBasicInterface +open PulseDomainInterface type exec_fun = caller_summary:Summary.t @@ -38,6 +39,17 @@ module Misc = struct let early_exit : model = fun ~caller_summary:_ _ ~ret:_ ~actuals:_ _ -> Ok [] + let return_int : Int64.t -> model = + fun i64 ~caller_summary:_ location ~ret:(ret_id, _) ~actuals:_ astate -> + let ret_addr = AbstractValue.mk_fresh () in + let astate = + Memory.add_attribute ret_addr + (Arithmetic (Arithmetic.equal_to (IntLit.of_int64 i64), Immediate {location; history= []})) + astate + in + Ok [PulseOperations.write_id ret_id (ret_addr, []) astate] + + let skip : model = fun ~caller_summary:_ _ ~ret:_ ~actuals:_ astate -> Ok [astate] let id_first_arg : model = @@ -243,6 +255,9 @@ module ProcNameDispatcher = struct ; -"std" &:: "basic_string" &:: "~basic_string" &--> StdBasicString.destructor ; -"std" &:: "function" &:: "operator()" &--> StdFunction.operator_call ; -"std" &:: "function" &:: "operator=" &--> Misc.shallow_copy "std::function::operator=" + ; -"std" &:: "integral_constant" < any_typ &+ capt_int + >::+ (fun _ name -> String.is_prefix ~prefix:"operator_" name) + &--> Misc.return_int ; -"std" &:: "vector" &:: "assign" &--> StdVector.invalidate_references Assign ; -"std" &:: "vector" &:: "clear" &--> StdVector.invalidate_references Clear ; -"std" &:: "vector" &:: "emplace" &--> StdVector.invalidate_references Emplace diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 417dc863b..937636716 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -22,6 +22,8 @@ codetoanalyze/cpp/pulse/interprocedural.cpp, feed_invalid_into_access_bad, 2, US 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/nullptr.cpp, std_false_type_deref_bad, 3, 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, std_true_type_deref_bad, 3, 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/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 index d153a9e8d..684647d0d 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/nullptr.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/nullptr.cpp @@ -4,6 +4,9 @@ * This source code is licensed under the MIT license found in the * LICENSE file in the root directory of this source tree. */ + +#include + void assign_zero_ok() { int x[2]; x[1] = 42; @@ -55,3 +58,35 @@ void deref_after_compare_ok(int* x) { compare_to_null(x); *x = 42; } + +bool return_true() { return std::true_type{}; } + +void std_true_type_impossible_deref_ok() { + int* x = nullptr; + if (!return_true()) { + *x = 42; + } +} + +void std_true_type_deref_bad() { + int* x = nullptr; + if (return_true()) { + *x = 42; + } +} + +bool return_false() { return std::false_type{}; } + +void std_false_type_impossible_deref_ok() { + int* x = nullptr; + if (return_false()) { + *x = 42; + } +} + +void std_false_type_deref_bad() { + int* x = nullptr; + if (!return_false()) { + *x = 42; + } +}