From b17861b1c88a4fd5dc22e60aa226dc651c4e4b86 Mon Sep 17 00:00:00 2001 From: Daiva Naudziuniene Date: Fri, 30 Oct 2020 03:56:03 -0700 Subject: [PATCH] [pulse] More precise model for constructing folly::Optional from Value Summary: Before we were creating a fresh internal value when we were constructing `folly::Optional`. This diff models `folly::Optional` constructor more precisely by copying the given value. There was also a missing dereference in the model of `value_or` Reviewed By: jvillard Differential Revision: D24621016 fbshipit-source-id: c86d3c157 --- infer/src/pulse/PulseModels.ml | 35 ++++++++++++++----- .../tests/codetoanalyze/cpp/pulse/issues.exp | 4 +-- .../codetoanalyze/cpp/pulse/optional.cpp | 20 +++++++++++ 3 files changed, 49 insertions(+), 10 deletions(-) diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 4746d76af..10373acf5 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -216,7 +216,15 @@ module FollyOptional = struct [ExecutionDomain.ContinueProgram astate] - let assign_value this init ~desc : model = + let assign_value this value ~desc : model = + fun _ ~callee_procname:_ location ~ret:_ astate -> + let* astate, value_copy = PulseOperations.shallow_copy location value astate in + let+ astate, value_deref = write_value location this ~value:value_copy ~desc astate in + let astate = PulseArithmetic.and_positive (fst value_deref) astate in + [ExecutionDomain.ContinueProgram astate] + + + let assign_optional_value this init ~desc : model = fun _ ~callee_procname:_ location ~ret:_ astate -> let* astate, value = to_internal_value_deref location init astate in let+ astate, _ = write_value location this ~value ~desc astate in @@ -257,15 +265,18 @@ module FollyOptional = struct let value_or optional default : model = fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model "folly::Optional::value_or()"; location; in_call= []} in - let* astate, (value_addr, value_hist) = to_internal_value_deref location optional astate in - let value_hist = (value_addr, event :: value_hist) in - let astate_non_empty = PulseArithmetic.and_positive value_addr astate in - let astate_value = PulseOperations.write_id ret_id value_hist astate_non_empty in + let* astate, value_addr = to_internal_value_deref location optional astate in + let astate_non_empty = PulseArithmetic.and_positive (fst value_addr) astate in + let* astate_non_empty, value = + PulseOperations.eval_access location value_addr Dereference astate_non_empty + in + let value_update_hist = (fst value, event :: snd value) in + let astate_value = PulseOperations.write_id ret_id value_update_hist astate_non_empty in let+ astate, (default_val, default_hist) = PulseOperations.eval_access location default Dereference astate in let default_value_hist = (default_val, event :: default_hist) in - let astate_empty = PulseArithmetic.and_eq_int value_addr IntLit.zero astate in + let astate_empty = PulseArithmetic.and_eq_int (fst value_addr) IntLit.zero astate in let astate_default = PulseOperations.write_id ret_id default_value_hist astate_empty in [ExecutionDomain.ContinueProgram astate_value; ExecutionDomain.ContinueProgram astate_default] end @@ -931,13 +942,21 @@ module ProcNameDispatcher = struct $--> FollyOptional.assign_none ~desc:"folly::Optional::Optional(=None)" ; -"folly" &:: "Optional" &:: "Optional" <>$ capt_arg_payload $--> FollyOptional.assign_none ~desc:"folly::Optional::Optional()" + ; -"folly" &:: "Optional" &:: "Optional" <>$ capt_arg_payload + $+ capt_arg_payload_of_typ (-"folly" &:: "Optional") + $--> FollyOptional.assign_optional_value + ~desc:"folly::Optional::Optional(folly::Optional arg)" ; -"folly" &:: "Optional" &:: "Optional" <>$ capt_arg_payload $+ capt_arg_payload - $+...$--> FollyOptional.assign_value ~desc:"folly::Optional::Optional(arg)" + $+...$--> FollyOptional.assign_value ~desc:"folly::Optional::Optional(Value arg)" ; -"folly" &:: "Optional" &:: "assign" <>$ capt_arg_payload $+ any_arg_of_typ (-"folly" &:: "None") $--> FollyOptional.assign_none ~desc:"folly::Optional::assign(=None)" + ; -"folly" &:: "Optional" &:: "assign" <>$ capt_arg_payload + $+ capt_arg_payload_of_typ (-"folly" &:: "Optional") + $--> FollyOptional.assign_optional_value + ~desc:"folly::Optional::assign(folly::Optional arg)" ; -"folly" &:: "Optional" &:: "assign" <>$ capt_arg_payload $+ capt_arg_payload - $+...$--> FollyOptional.assign_value ~desc:"folly::Optional::assign()" + $+...$--> FollyOptional.assign_value ~desc:"folly::Optional::assign(Value arg)" ; -"folly" &:: "Optional" &:: "emplace<>" $ capt_arg_payload $+...$--> FollyOptional.emplace ; -"folly" &:: "Optional" &:: "emplace" $ capt_arg_payload $+...$--> FollyOptional.emplace ; -"folly" &:: "Optional" &:: "has_value" <>$ capt_arg_payload diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index df3d5f4f3..8cc227a2d 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -47,8 +47,8 @@ codetoanalyze/cpp/pulse/nullptr.cpp, no_check_return_bad, 2, NULLPTR_DEREFERENCE 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/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 folly::None,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=`,passed as argument to `folly::Optional::value()` (modelled),return from call to `folly::Optional::value()` (modelled),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 folly::None,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()` (modelled),return from call to `folly::Optional::assign()` (modelled),return from call to `folly::Optional::operator=`,passed as argument to `folly::Optional::value()` (modelled),return from call to `folly::Optional::value()` (modelled),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 folly::None,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(arg)` (modelled),return from call to `folly::Optional::Optional(arg)` (modelled),passed as argument to `folly::Optional::value()` (modelled),return from call to `folly::Optional::value()` (modelled),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 folly::None,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=`,passed as argument to `folly::Optional::value()` (modelled),return from call to `folly::Optional::value()` (modelled),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 folly::None,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),passed as argument to `folly::Optional::value()` (modelled),return from call to `folly::Optional::value()` (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 folly::None,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::value()` (modelled),return from call to `folly::Optional::value()` (modelled),invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, operator_arrow_bad, 0, 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 folly::None,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),when calling `emplace` here,parameter `state` of emplace,passed as argument to `folly::Optional::operator->`,return from call to `folly::Optional::operator->`,invalid access occurs here] codetoanalyze/cpp/pulse/path.cpp, faulty_call_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [calling context starts here,in call to `only_bad_on_42_latent`,invalidation part of the trace starts here,when calling `may_return_null` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `may_return_null`,return from call to `may_return_null`,assigned,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/optional.cpp b/infer/tests/codetoanalyze/cpp/pulse/optional.cpp index e0520c7c3..d128484ca 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/optional.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/optional.cpp @@ -70,6 +70,16 @@ int not_none_ok() { return foo.value(); } +int not_none_check_value_ok() { + folly::Optional foo{5}; + int x = foo.value(); + if (x != 5) { + folly::Optional foo{folly::none}; + return foo.value(); + } + return x; +} + int none_check_ok() { folly::Optional foo{folly::none}; if (foo) { @@ -139,3 +149,13 @@ int value_or_check_empty_ok() { } return -1; } + +int value_or_check_value_ok() { + folly::Optional foo{5}; + int x = foo.value_or(0); + if (x != 5) { + folly::Optional foo{folly::none}; + return foo.value(); + } + return -1; +}