[pulse] new option to turn pulse back into an intra-procedural analysis

Summary: To run experiments.

Reviewed By: jberdine

Differential Revision: D19411491

fbshipit-source-id: 9e9490d5e

infer/man/man1/infer-full.txt

@@ -1642,6 +1642,11 @@ INTERNAL OPTIONS
        --profiler-samples-reset
            Cancel the effect of --profiler-samples.
 
+       --pulse-intraprocedural-only
+           Activates: Disable inter-procedural analysis in Pulse. Used for
+           experimentations only. (Conversely:
+           --no-pulse-intraprocedural-only)
+
        --pulse-max-disjuncts int
            Under-approximate after int disjunctions in the domain
 

infer/src/base/Config.ml

@@ -1955,6 +1955,11 @@ and project_root =
     ~meta:"dir" "Specify the root directory of the project"
 
 
+and pulse_intraprocedural_only =
+  CLOpt.mk_bool ~long:"pulse-intraprocedural-only"
+    "Disable inter-procedural analysis in Pulse. Used for experimentations only."
+
+
 and pulse_max_disjuncts =
   CLOpt.mk_int ~long:"pulse-max-disjuncts" ~default:20
     "Under-approximate after $(i,int) disjunctions in the domain"
@@ -3077,6 +3082,8 @@ and project_root = !project_root
 
 and pulse = !pulse
 
+and pulse_intraprocedural_only = !pulse_intraprocedural_only
+
 and pulse_max_disjuncts = !pulse_max_disjuncts
 
 and pulse_widen_threshold = !pulse_widen_threshold

infer/src/base/Config.mli

@@ -550,6 +550,8 @@ val project_root : string
 
 val pulse : bool
 
+val pulse_intraprocedural_only : bool
+
 val pulse_max_disjuncts : int
 
 val pulse_widen_threshold : int

infer/src/pulse/Pulse.ml

@@ -44,10 +44,10 @@ module PulseTransferFunctions = struct
 
   let interprocedural_call caller_summary ret call_exp actuals call_loc get_formals astate =
     match proc_name_of_call call_exp with
-    | Some callee_pname ->
+    | Some callee_pname when not Config.pulse_intraprocedural_only ->
         let formals_opt = get_formals callee_pname in
         PulseOperations.call ~caller_summary call_loc callee_pname ~ret ~actuals ~formals_opt astate
-    | None ->
+    | _ ->
         L.d_printfln "Skipping indirect call %a@\n" Exp.pp call_exp ;
         Ok
           [ PulseOperations.unknown_call call_loc (SkippedUnknownCall call_exp) ~ret ~actuals