[pulse] use the disjunctive domain and make it configurable

Summary:
Change join/widen policies to more interesting ones and play around to
find a good tradeoff.

Reviewed By: mbouaziz

Differential Revision: D13432492

fbshipit-source-id: 2c3e498dd

infer/man/man1/infer-full.txt

@@ -1346,6 +1346,13 @@ INTERNAL OPTIONS
        --profiler-samples-reset
            Cancel the effect of --profiler-samples.
 
+       --pulse-max-disjuncts int
+           Under-approximate after int disjunctions in the domain (default:
+           50)
+
+       --pulse-widen-threshold int
+           Under-approximate after int loop iterations (default: 5)
+
        --reactive-capture
            Activates: Compile source files only when required by analyzer
            (clang only) (Conversely: --no-reactive-capture)

infer/src/base/Config.ml

@@ -1800,6 +1800,16 @@ and project_root =
     ~meta:"dir" "Specify the root directory of the project"
 
 
+and pulse_max_disjuncts =
+  CLOpt.mk_int ~long:"pulse-max-disjuncts" ~default:50
+    "Under-approximate after $(i,int) disjunctions in the domain"
+
+
+and pulse_widen_threshold =
+  CLOpt.mk_int ~long:"pulse-widen-threshold" ~default:5
+    "Under-approximate after $(i,int) loop iterations"
+
+
 and quandary_endpoints =
   CLOpt.mk_json ~long:"quandary-endpoints"
     ~in_help:InferCommand.[(Analyze, manual_quandary)]
@@ -2837,6 +2847,10 @@ and project_root = !project_root
 
 and pulse = !pulse
 
+and pulse_max_disjuncts = !pulse_max_disjuncts
+
+and pulse_widen_threshold = !pulse_widen_threshold
+
 and purity = !purity
 
 and quandary = !quandary

infer/src/base/Config.mli

@@ -547,6 +547,10 @@ val progress_bar : [`MultiLine | `Plain | `Quiet]
 
 val pulse : bool
 
+val pulse_max_disjuncts : int
+
+val pulse_widen_threshold : int
+
 val purity : bool
 
 val quandary : bool

infer/src/checkers/Pulse.ml

@@ -141,9 +141,11 @@ module DisjunctiveTransferFunctions =
        (struct
          type domain_t = PulseDomain.t [@@deriving compare]
 
-         let join_policy = `JoinAfter 1
+         let join_policy =
+           match Config.pulse_max_disjuncts with 0 -> `NeverJoin | n -> `UnderApproximateAfter n
 
-         let widen_policy = `UnderApproximateAfterNumIterations 5
+
+         let widen_policy = `UnderApproximateAfterNumIterations Config.pulse_widen_threshold
        end)
 
 module DisjunctiveAnalyzer =