From 060b3dd2c14306a7fcca798fa335a8023e4cc8c3 Mon Sep 17 00:00:00 2001
From: Sungkeun Cho <scho@meta.com>
Date: Thu, 14 Nov 2024 02:33:51 -0800
Subject: [PATCH] [pulse] Simple model for thrift field ref accesses

Summary:
This diff adds a simple model for thrift field refs as the second argument is stored to the first
argument.

Reviewed By: rgrig

Differential Revision: D65833558

fbshipit-source-id: 90206bd0868aee872616ce80dcc22cca479801fc
---
 infer/src/IR/Typ.mli              |  2 ++
 infer/src/pulse/PulseModelsCpp.ml | 15 ++++++++++++++-
 2 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/infer/src/IR/Typ.mli b/infer/src/IR/Typ.mli
index d22d3f4fb6..9b9d433f1b 100644
--- a/infer/src/IR/Typ.mli
+++ b/infer/src/IR/Typ.mli
@@ -354,6 +354,8 @@ val is_shared_pointer : t -> bool
 
 val is_folly_coro : t -> bool
 
+val thrift_field_refs : string list
+
 val is_thrift_field_ref : t -> bool
 
 val is_thrift_field_ref_str : string -> bool
diff --git a/infer/src/pulse/PulseModelsCpp.ml b/infer/src/pulse/PulseModelsCpp.ml
index e167588333..681216bd58 100644
--- a/infer/src/pulse/PulseModelsCpp.ml
+++ b/infer/src/pulse/PulseModelsCpp.ml
@@ -892,6 +892,12 @@ module Pair = struct
       astate
 end
 
+module Thrift = struct
+  let field_ref ~name tgt src : model =
+    let open PulseModelsDSL.Syntax in
+    start_named_model ("apache::thrift::" ^ name) @@ fun () -> store ~ref:tgt src
+end
+
 let folly_co_yield_co_error : model =
   let open PulseModelsDSL.Syntax in
   start_named_model "folly::coro::detail::*::yield_value(folly::coro::co_error)" @@ fun () -> throw
@@ -1093,9 +1099,16 @@ let map_matchers =
   @ folly_concurrent_hash_map_matchers @ folly_coro
 
 
+let thrift_matchers =
+  let open ProcnameDispatcher.Call in
+  List.map Typ.thrift_field_refs ~f:(fun field_ref ->
+      -"apache" &:: "thrift" &:: field_ref &:: field_ref $ capt_arg_payload $+ capt_arg_payload
+      $+...$--> Thrift.field_ref ~name:field_ref )
+
+
 let simple_matchers =
   let open ProcnameDispatcher.Call in
-  map_matchers
+  map_matchers @ thrift_matchers
   @ [ +BuiltinDecl.(match_builtin __builtin_add_overflow)
       <>$ capt_arg_payload $+ capt_arg_payload $+ capt_arg_payload $--> add_overflow
       |> with_non_disj