From 3a390d9ab7008829b58dade25d94156dc3a63434 Mon Sep 17 00:00:00 2001
From: Dino Distefano <ddino@meta.com>
Date: Fri, 13 Oct 2023 06:41:50 -0700
Subject: [PATCH] Added command line option --abstract-pulse-models-for-erlang

Reviewed By: mmarescotti

Differential Revision: D50117996

fbshipit-source-id: 7f7ca05adf2e183628a952d58a02204db105abcf
---
 infer/man/man1/infer-full.txt        |  5 +++++
 infer/src/base/Config.ml             | 15 +++++++++++----
 infer/src/base/Config.mli            |  2 ++
 infer/src/pulse/PulseModelsErlang.ml |  5 ++++-
 4 files changed, 22 insertions(+), 5 deletions(-)

diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt
index 7cf1f8b107d..c6c4804109a 100644
--- a/infer/man/man1/infer-full.txt
+++ b/infer/man/man1/infer-full.txt
@@ -1966,6 +1966,11 @@ OPTIONS
 INTERNAL OPTIONS
        Use at your own risk.
 
+       --no-abstract-pulse-models-for-erlang
+           Deactivates: Applies abstraction of the pulse models passed by
+           --pulse-models-for-erlang (Conversely:
+           --abstract-pulse-models-for-erlang)
+
        --analysis-schedule-file-reset
            Cancel the effect of --analysis-schedule-file.
 
diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml
index 911a1e0d37a..17a464d1149 100644
--- a/infer/src/base/Config.ml
+++ b/infer/src/base/Config.ml
@@ -595,7 +595,12 @@ let () =
   ()
 
 
-let analysis_schedule_file =
+let abstract_pulse_models_for_erlang =
+  CLOpt.mk_bool ~long:"abstract-pulse-models-for-erlang"
+    "Applies abstraction of the pulse models passed by --pulse-models-for-erlang" ~default:true
+
+
+and analysis_schedule_file =
   CLOpt.mk_path_opt ~long:"analysis-schedule-file"
     ~in_help:InferCommand.[(Analyze, manual_scheduler)]
     ( "The file where an analysis schedule is stored. The default is "
@@ -3631,6 +3636,8 @@ let command =
 
 let rest = !rest
 
+and dynamic_dispatch_json_file_path = !dynamic_dispatch_json_file_path
+
 and analysis_schedule_file = !analysis_schedule_file
 
 and biabduction_abs_struct = !biabduction_abs_struct
@@ -3894,7 +3901,7 @@ and dump_duplicate_symbols = !dump_duplicate_symbols
 
 and dump_textual = !dump_textual
 
-and dynamic_dispatch_json_file_path = !dynamic_dispatch_json_file_path
+and abstract_pulse_models_for_erlang = !abstract_pulse_models_for_erlang
 
 and eradicate_condition_redundant = !eradicate_condition_redundant
 
@@ -4075,6 +4082,8 @@ and never_returning_null = match never_returning_null with k, r -> (k, !r)
 
 and no_censor_report = RevList.rev_map !no_censor_report ~f:Str.regexp
 
+and no_translate_libs = not !headers
+
 and nullable_annotation = !nullable_annotation
 
 and nullsafe_annotation_graph = !nullsafe_annotation_graph
@@ -4095,8 +4104,6 @@ and nullsafe_third_party_location_for_messaging_only =
 
 and nullsafe_strict_containers = !nullsafe_strict_containers
 
-and no_translate_libs = not !headers
-
 and oom_threshold = !oom_threshold
 
 and only_cheap_debug = !only_cheap_debug
diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli
index 2278e17ba8f..2218c3730f4 100644
--- a/infer/src/base/Config.mli
+++ b/infer/src/base/Config.mli
@@ -123,6 +123,8 @@ val wrappers_dir : string
 
 (** {2 Configuration values specified by command-line options} *)
 
+val abstract_pulse_models_for_erlang : bool
+
 val analysis_schedule_file : string option
 
 val annotation_reachability_cxx : Yojson.Basic.t
diff --git a/infer/src/pulse/PulseModelsErlang.ml b/infer/src/pulse/PulseModelsErlang.ml
index 4b9bb8032cf..b2d3093ece9 100644
--- a/infer/src/pulse/PulseModelsErlang.ml
+++ b/infer/src/pulse/PulseModelsErlang.ml
@@ -1489,7 +1489,10 @@ module Custom = struct
               let behavior_json = Sqlite3.column_text stmt 0 in
               match behavior_of_yojson (Yojson.Safe.from_string behavior_json) with
               | behavior ->
-                  let abs_behavior = abstract_behavior mfa behavior in
+                  let abs_behavior =
+                    if Config.abstract_pulse_models_for_erlang then abstract_behavior mfa behavior
+                    else behavior
+                  in
                   L.debug Analysis Quiet "Function '%s' ABS BEHAVIOR:[  %a ] @\n@\n" mfa pp_behavior
                     abs_behavior ;
                   let model_abs_behavior = make_model abs_behavior in