Added command line option --abstract-pulse-models-for-erlang

Reviewed By: mmarescotti Differential Revision: D50117996 fbshipit-source-id: 7f7ca05adf2e183628a952d58a02204db105abcf
facebook · Oct 13, 2023 · 3a390d9 · 3a390d9
1 parent 9cefdd6
commit 3a390d9
Show file tree

Hide file tree

Showing 4 changed files with 22 additions and 5 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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