Change a polymorphic variant type to a regular variant

Summary: Polymorphic variant types are prone to type errors when largely present. Change this one to a regular variant type.

Reviewed By: skcho

Differential Revision: D49458271

fbshipit-source-id: d335ee2f2d7b6d338e029d53d6e49c4bf018804d

infer/src/absint/AbstractInterpreter.ml

@@ -208,7 +208,9 @@ struct
 
   type analysis_data = T.analysis_data
 
-  let (`UnderApproximateAfter disjunct_limit) = DConfig.join_policy
+  let disjunct_limit =
+    match DConfig.join_policy with UnderApproximateAfter max_states -> max_states
+
 
   let has_geq_disj ~leq ~than:disj disjs =
     List.exists disjs ~f:(fun disj' -> leq ~lhs:disj ~rhs:disj')
@@ -291,7 +293,9 @@ struct
 
 
     let widen ~prev ~next ~num_iters =
-      let (`UnderApproximateAfterNumIterations max_iter) = DConfig.widen_policy in
+      let max_iter =
+        match DConfig.widen_policy with UnderApproximateAfterNumIterations max_iter -> max_iter
+      in
       if phys_equal prev next then prev
       else if num_iters > max_iter then (
         L.d_printfln "Iteration %d is greater than max iter %d, stopping." num_iters max_iter ;

infer/src/absint/TransferFunctions.ml

@@ -34,10 +34,14 @@ module type MakeHIL = functor (C : ProcCfg.S) -> sig
   include HIL with module CFG = C
 end
 
+type join_policy_t = UnderApproximateAfter of int
+
+type widen_policy_t = UnderApproximateAfterNumIterations of int
+
 module type DisjunctiveConfig = sig
-  val join_policy : [`UnderApproximateAfter of int]
+  val join_policy : join_policy_t
 
-  val widen_policy : [`UnderApproximateAfterNumIterations of int]
+  val widen_policy : widen_policy_t
 end
 
 module type DisjReady = sig

infer/src/absint/TransferFunctions.mli

@@ -42,14 +42,16 @@ module type HIL = sig
   include S with type instr := HilInstr.t
 end
 
+(** When the set of disjuncts gets bigger than [n] then just stop adding new states to it, drop any
+    further states on the floor. This corresponds to an under-approximation/bounded approach. *)
+type join_policy_t = UnderApproximateAfter of int
+
+type widen_policy_t = UnderApproximateAfterNumIterations of int
+
 module type DisjunctiveConfig = sig
-  val join_policy :
-    [ `UnderApproximateAfter of int
-      (** When the set of disjuncts gets bigger than [n] then just stop adding new states to it,
-          drop any further states on the floor. This corresponds to an under-approximation/bounded
-          approach. *) ]
+  val join_policy : join_policy_t
 
-  val widen_policy : [`UnderApproximateAfterNumIterations of int]
+  val widen_policy : widen_policy_t
 end
 
 module type DisjReady = sig

infer/src/checkers/DisjunctiveDemo.ml

@@ -37,7 +37,7 @@ end
 
 module NonDisjDomain = AbstractDomain.BottomTopLifted (AbstractDomain.Empty)
 
-module TransferFunctions = struct
+module DisjunctiveAnalyzerTransferFunctions = struct
   module CFG = ProcCfg.Normal
   module DisjDomain = DisjDomain
   module NonDisjDomain = NonDisjDomain
@@ -71,13 +71,13 @@ end
 
 module DisjunctiveAnalyzer =
   AbstractInterpreter.MakeDisjunctive
-    (TransferFunctions)
+    (DisjunctiveAnalyzerTransferFunctions)
     (struct
       (* re-use pulse options to avoid complicating the command-line interface just for testing *)
-      let join_policy = `UnderApproximateAfter Config.pulse_max_disjuncts
+      let join_policy = TransferFunctions.UnderApproximateAfter Config.pulse_max_disjuncts
 
       (* just 2 for now, we may want to parameterize this in the future *)
-      let widen_policy = `UnderApproximateAfterNumIterations 2
+      let widen_policy = TransferFunctions.UnderApproximateAfterNumIterations 2
     end)
 
 type domain = DisjunctiveAnalyzer.TransferFunctions.Domain.t

infer/src/pulse/Pulse.ml

@@ -1431,9 +1431,10 @@ module DisjunctiveAnalyzer =
   AbstractInterpreter.MakeDisjunctive
     (PulseTransferFunctions)
     (struct
-      let join_policy = `UnderApproximateAfter Config.pulse_max_disjuncts
+      let join_policy = TransferFunctions.UnderApproximateAfter Config.pulse_max_disjuncts
 
-      let widen_policy = `UnderApproximateAfterNumIterations Config.pulse_widen_threshold
+      let widen_policy =
+        TransferFunctions.UnderApproximateAfterNumIterations Config.pulse_widen_threshold
     end)
 
 let with_html_debug_node node ~desc ~f =