[pulse] use WTO scheduler

Summary:
I hear that this scheduler is better. I want the best scheduler
possible. Also pulse's join is a bit complex so it might matter one day.

whydididothis

Reviewed By: mbouaziz

Differential Revision: D12958131

fbshipit-source-id: 3bd77ccba

infer/src/absint/LowerHil.ml

@@ -93,11 +93,12 @@ struct
 end
 
 module MakeAbstractInterpreterWithConfig
+    (MakeAbstractInterpreter : AbstractInterpreter.Make)
     (HilConfig : HilConfig)
     (CFG : ProcCfg.S)
     (MakeTransferFunctions : TransferFunctions.MakeHIL) =
 struct
-  module Interpreter = AbstractInterpreter.MakeRPO (Make (MakeTransferFunctions) (HilConfig) (CFG))
+  module Interpreter = MakeAbstractInterpreter (Make (MakeTransferFunctions) (HilConfig) (CFG))
 
   let compute_post ({ProcData.pdesc; tenv} as proc_data) ~initial =
     Preanal.do_preanalysis pdesc tenv ;
@@ -116,4 +117,5 @@ struct
     Interpreter.compute_post ~pp_instr proc_data ~initial:initial' |> Option.map ~f:fst
 end
 
-module MakeAbstractInterpreter = MakeAbstractInterpreterWithConfig (DefaultConfig)
+module MakeAbstractInterpreter =
+  MakeAbstractInterpreterWithConfig (AbstractInterpreter.MakeRPO) (DefaultConfig)

infer/src/absint/LowerHil.mli

@@ -35,6 +35,7 @@ end
 
 (** Wrapper around Interpreter to prevent clients from having to deal with IdAccessPathMapDomain *)
 module MakeAbstractInterpreterWithConfig
+    (MakeAbstractInterpreter : AbstractInterpreter.Make)
     (HilConfig : HilConfig)
     (CFG : ProcCfg.S)
     (MakeTransferFunctions : TransferFunctions.MakeHIL) : sig
@@ -54,5 +55,6 @@ module MakeAbstractInterpreter
     (CFG : ProcCfg.S)
     (MakeTransferFunctions : TransferFunctions.MakeHIL) : sig
   include module type of
-    MakeAbstractInterpreterWithConfig (DefaultConfig) (CFG) (MakeTransferFunctions)
+    MakeAbstractInterpreterWithConfig (AbstractInterpreter.MakeRPO) (DefaultConfig) (CFG)
+      (MakeTransferFunctions)
 end

infer/src/checkers/Pulse.ml

@@ -125,7 +125,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   let pp_session_name _node fmt = F.pp_print_string fmt "Pulse"
 end
 
-module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Exceptional) (TransferFunctions)
+module Analyzer =
+  LowerHil.MakeAbstractInterpreterWithConfig (AbstractInterpreter.MakeWTO) (LowerHil.DefaultConfig)
+    (ProcCfg.Exceptional)
+    (TransferFunctions)
 
 let checker {Callbacks.proc_desc; tenv; summary} =
   let proc_data = ProcData.make proc_desc tenv summary in

infer/src/quandary/TaintAnalysis.ml

@@ -744,7 +744,8 @@ module Make (TaintSpecification : TaintSpec.S) = struct
   end
 
   module Analyzer =
-    LowerHil.MakeAbstractInterpreterWithConfig (HilConfig) (ProcCfg.Exceptional)
+    LowerHil.MakeAbstractInterpreterWithConfig (AbstractInterpreter.MakeRPO) (HilConfig)
+      (ProcCfg.Exceptional)
       (TransferFunctions)
 
   (* sanity checks for summaries. should only be used in developer mode *)

infer/tests/codetoanalyze/cpp/pulse/issues.exp

@@ -1,5 +1,5 @@
 codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 58, column 5 here,accessed `*(ptr)` here]
-codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 8, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 68, column 7 here,accessed `*(ptr)` here]
+codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 68, column 7 here,accessed `ptr` here]
 codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete result` at line 21, column 5 here,accessed `*(result)` here]
 codetoanalyze/cpp/pulse/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete x` at line 112, column 3 here,accessed `x` here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 57, column 5 here,accessed `s` here]