pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[pulse] More precise model for constructing folly::Optional<Value> from Value

Browse Source 
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
master
Daiva Naudziuniene 4 years ago committed by Facebook GitHub Bot
parent b6eb480597
commit b17861b1c8
3 changed files with 49 additions and 10 deletions
Show Stats Download Patch File Download Diff File

35
infer/src/pulse/PulseModels.ml
Unescape View File

@ -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<Value> 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<Value> 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

4
infer/tests/codetoanalyze/cpp/pulse/issues.exp
Unescape View File

@ -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<int>::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<int>::operator=`,passed as argument to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::reset()` (modelled),return from call to `folly::Optional<int>::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<int>::operator=`,parameter `other` of folly::Optional<int>::operator=,passed as argument to `folly::Optional::assign()` (modelled),return from call to `folly::Optional::assign()` (modelled),return from call to `folly::Optional<int>::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<int>::operator=`,parameter `other` of folly::Optional<int>::operator=,passed as argument to `folly::Optional::assign(folly::Optional<Value> arg)` (modelled),return from call to `folly::Optional::assign(folly::Optional<Value> arg)` (modelled),return from call to `folly::Optional<int>::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<Value> arg)` (modelled),return from call to `folly::Optional::Optional(folly::Optional<Value> 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<State>::operator->`,return from call to `folly::Optional<State>::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]

20
infer/tests/codetoanalyze/cpp/pulse/optional.cpp
Unescape View File

@ -70,6 +70,16 @@ int not_none_ok() {
return foo.value();
}
int not_none_check_value_ok() {
folly::Optional<int> foo{5};
int x = foo.value();
if (x != 5) {
folly::Optional<int> foo{folly::none};
return foo.value();
}
return x;
}
int none_check_ok() {
folly::Optional<int> 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<int> foo{5};
int x = foo.value_or(0);
if (x != 5) {
folly::Optional<int> foo{folly::none};
return foo.value();
}
return -1;
}

Write Preview
Loading…
Cancel
Save