From 019adf7e78bb471ad85f0ddbb9d4f0c06bc345f5 Mon Sep 17 00:00:00 2001 From: Daiva Naudziuniene Date: Mon, 16 Nov 2020 06:24:24 -0800 Subject: [PATCH] [pulse] Model for folly::Optional::get_pointer Summary: Model `folly::Optional::get_pointer` which returns an address to a value if exists or `nullptr` if empty. Reviewed By: jvillard Differential Revision: D24935677 fbshipit-source-id: 9d990fe07 --- infer/src/pulse/PulseModels.ml | 23 ++++++++++++++- .../tests/codetoanalyze/cpp/pulse/issues.exp | 1 + .../codetoanalyze/cpp/pulse/optional.cpp | 28 +++++++++++++++++++ 3 files changed, 51 insertions(+), 1 deletion(-) diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index c285fe72d..520119308 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -252,7 +252,7 @@ module Optional = struct let has_value optional ~desc : model = fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let ret_addr = AbstractValue.mk_fresh () in - let ret_value = (ret_addr, [ValueHistory.Allocation {f= Model desc; location}]) in + let ret_value = (ret_addr, [ValueHistory.Call {f= Model desc; location; in_call= []}]) in let+ astate, (value_addr, _) = to_internal_value_deref location optional astate in let astate = PulseOperations.write_id ret_id ret_value astate in let astate_non_empty = PulseArithmetic.and_positive value_addr astate in @@ -262,6 +262,25 @@ module Optional = struct [ExecutionDomain.ContinueProgram astate_false; ExecutionDomain.ContinueProgram astate_true] + let get_pointer optional ~desc : model = + fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + let event = ValueHistory.Call {f= Model desc; location; in_call= []} in + let* astate, value_addr = to_internal_value_deref location optional astate in + let value_update_hist = (fst value_addr, event :: snd value_addr) in + let astate_value_addr = + PulseOperations.write_id ret_id value_update_hist astate + |> PulseArithmetic.and_positive (fst value_addr) + in + let nullptr = (AbstractValue.mk_fresh (), [event]) in + let+ astate_null = + PulseOperations.write_id ret_id nullptr astate + |> PulseArithmetic.and_eq_int (fst value_addr) IntLit.zero + |> PulseArithmetic.and_eq_int (fst nullptr) IntLit.zero + |> PulseOperations.invalidate location (ConstantDereference IntLit.zero) nullptr + in + [ExecutionDomain.ContinueProgram astate_value_addr; ExecutionDomain.ContinueProgram astate_null] + + let value_or optional default ~desc : model = fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in @@ -969,6 +988,8 @@ module ProcNameDispatcher = struct $+...$--> Optional.assign_none ~desc:"folly::Optional::reset()" ; -"folly" &:: "Optional" &:: "value" <>$ capt_arg_payload $+...$--> Optional.value ~desc:"folly::Optional::value()" + ; -"folly" &:: "Optional" &:: "get_pointer" $ capt_arg_payload + $+...$--> Optional.get_pointer ~desc:"folly::Optional::get_pointer()" ; -"folly" &:: "Optional" &:: "value_or" $ capt_arg_payload $+ capt_arg_payload $+...$--> Optional.value_or ~desc:"folly::Optional::value_or()" (* std::optional *) diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 955a8b14b..dfb97d280 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -50,6 +50,7 @@ codetoanalyze/cpp/pulse/nullptr.cpp, std_false_type_deref_bad, 3, NULLPTR_DEREFE 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/optional.cpp, assign2_bad, 4, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `folly::Optional::operator=` here,passed as argument to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::reset()` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::operator=`,passed as argument to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::operator=`,invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, assign_bad, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),passed as argument to `folly::Optional::operator=`,parameter `other` of folly::Optional::operator=,passed as argument to `folly::Optional::assign(folly::Optional arg)` (modelled),return from call to `folly::Optional::assign(folly::Optional arg)` (modelled),return from call to `folly::Optional::operator=`,invalid access occurs here] +codetoanalyze/cpp/pulse/optional.cpp, get_pointer_no_check_none_check_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::get_pointer()` (modelled),return from call to `folly::Optional::get_pointer()` (modelled),is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::get_pointer()` (modelled),return from call to `folly::Optional::get_pointer()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, none_copy_bad, 3, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),passed as argument to `folly::Optional::Optional(folly::Optional arg)` (modelled),return from call to `folly::Optional::Optional(folly::Optional arg)` (modelled),invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, none_no_check_bad, 2, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, not_none_check_value_ok_FP, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),invalid access occurs here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/optional.cpp b/infer/tests/codetoanalyze/cpp/pulse/optional.cpp index f87f443fc..92288a5bb 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/optional.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/optional.cpp @@ -63,6 +63,8 @@ class Optional { constexpr Value* operator->() { return &value(); } + Value* get_pointer(); + template constexpr Value value_or(U&& dflt) const&; }; @@ -147,6 +149,32 @@ void emplace(folly::Optional state) { void operator_arrow_bad() { emplace(folly::none); } +void get_pointer_check_none_check_ok() { + folly::Optional foo{folly::none}; + if (int* v = foo.get_pointer()) { + *v = 42; + } +} + +void get_pointer_check_value_check_ok() { + folly::Optional foo{5}; + if (int* ptr = foo.get_pointer()) { + *ptr = 42; + } +} + +void get_pointer_no_check_none_check_bad() { + folly::Optional foo{folly::none}; + int* ptr = foo.get_pointer(); + *ptr = 42; +} + +void get_pointer_no_check_value_check_ok() { + folly::Optional foo{5}; + int* ptr = foo.get_pointer(); + *ptr = 42; +} + int value_or_check_empty_ok() { folly::Optional foo{folly::none}; if (foo.value_or(0) > 0) {