From 059c0f24a2c782e47707ee14338e2d805029ae60 Mon Sep 17 00:00:00 2001
From: Daiva Naudziuniene <daivan@fb.com>
Date: Tue, 27 Oct 2020 02:17:03 -0700
Subject: [PATCH] [pulse] Model Optional value_or

Summary: Model `folly::Optional::value_or(default)` to return value if not-empty and `default` if empty.

Reviewed By: jvillard

Differential Revision: D24539456

fbshipit-source-id: cc9e176cc
---
 infer/src/pulse/PulseModels.ml                 | 18 ++++++++++++++++++
 .../tests/codetoanalyze/cpp/pulse/optional.cpp | 11 +++++++++++
 2 files changed, 29 insertions(+)

diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml
index e1159e6b2..4746d76af 100644
--- a/infer/src/pulse/PulseModels.ml
+++ b/infer/src/pulse/PulseModels.ml
@@ -252,6 +252,22 @@ module FollyOptional = struct
     let astate_empty = PulseArithmetic.and_eq_int value_addr IntLit.zero astate in
     let astate_false = PulseArithmetic.and_eq_int ret_addr IntLit.zero astate_empty in
     [ExecutionDomain.ContinueProgram astate_false; ExecutionDomain.ContinueProgram astate_true]
+
+
+  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, (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_default = PulseOperations.write_id ret_id default_value_hist astate_empty in
+    [ExecutionDomain.ContinueProgram astate_value; ExecutionDomain.ContinueProgram astate_default]
 end
 
 module Cplusplus = struct
@@ -929,6 +945,8 @@ module ProcNameDispatcher = struct
         ; -"folly" &:: "Optional" &:: "reset" <>$ capt_arg_payload
           $+...$--> FollyOptional.assign_none ~desc:"folly::Optional::reset()"
         ; -"folly" &:: "Optional" &:: "value" <>$ capt_arg_payload $+...$--> FollyOptional.value
+        ; -"folly" &:: "Optional" &:: "value_or" $ capt_arg_payload $+ capt_arg_payload
+          $+...$--> FollyOptional.value_or
         ; -"std" &:: "basic_string" &:: "data" <>$ capt_arg_payload $--> StdBasicString.data
         ; -"std" &:: "basic_string" &:: "~basic_string" <>$ capt_arg_payload
           $--> StdBasicString.destructor
diff --git a/infer/tests/codetoanalyze/cpp/pulse/optional.cpp b/infer/tests/codetoanalyze/cpp/pulse/optional.cpp
index b3de9e68c..e0520c7c3 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/optional.cpp
+++ b/infer/tests/codetoanalyze/cpp/pulse/optional.cpp
@@ -59,6 +59,9 @@ class Optional {
   constexpr const Value* operator->() const { return &value(); }
 
   constexpr Value* operator->() { return &value(); }
+
+  template <class U>
+  constexpr Value value_or(U&& dflt) const&;
 };
 } // namespace folly
 
@@ -128,3 +131,11 @@ void emplace(folly::Optional<State> state) {
 }
 
 void operator_arrow_bad() { emplace(folly::none); }
+
+int value_or_check_empty_ok() {
+  folly::Optional<int> foo{folly::none};
+  if (foo.value_or(0) > 0) {
+    return foo.value();
+  }
+  return -1;
+}