Preparing for WeakTopologicalOrder-based abstract interpreter

Reviewed By: ngorogiannis

Differential Revision: D10069200

fbshipit-source-id: 5d6d5d12c

infer/src/absint/AbstractInterpreter.ml

@@ -17,14 +17,43 @@ type debug =
           When using LowerHil-AI, we're not interested in the underlying SIL instructions,
           it's the only case where want to disable it. *)
 
-type 'a state = {pre: 'a; post: 'a; visit_count: int}
+type exec_node_schedule_result = ReachedFixPoint | DidNotReachFixPoint
+
+module VisitCount : sig
+  type t = private int
+
+  val first_time : t
+
+  val succ : pdesc:Procdesc.t -> t -> t
+end = struct
+  type t = int
+
+  let first_time = 1
+
+  let succ ~pdesc visit_count =
+    let visit_count' = visit_count + 1 in
+    if visit_count' > Config.max_widens then
+      L.(die InternalError)
+        "Exceeded max widening threshold %d while analyzing %a. Please check your widening \
+         operator or increase the threshold"
+        Config.max_widens Typ.Procname.pp (Procdesc.get_proc_name pdesc) ;
+    visit_count'
+end
+
+module State = struct
+  type 'a t = {pre: 'a; post: 'a; visit_count: VisitCount.t}
+
+  let pre {pre} = pre
+
+  let post {post} = post
+end
 
 module type S = sig
   module TransferFunctions : TransferFunctions.SIL
 
   module InvariantMap = TransferFunctions.CFG.Node.IdMap
 
-  type invariant_map = TransferFunctions.Domain.astate state InvariantMap.t
+  type invariant_map = TransferFunctions.Domain.astate State.t InvariantMap.t
 
   val compute_post :
        ?debug:debug
@@ -41,37 +70,30 @@ module type S = sig
   val exec_pdesc :
     TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate -> invariant_map
 
-  val extract_post : InvariantMap.key -> 'a state InvariantMap.t -> 'a option
+  val extract_post : InvariantMap.key -> 'a State.t InvariantMap.t -> 'a option
 
-  val extract_pre : InvariantMap.key -> 'a state InvariantMap.t -> 'a option
+  val extract_pre : InvariantMap.key -> 'a State.t InvariantMap.t -> 'a option
 
   val extract_state : InvariantMap.key -> 'a InvariantMap.t -> 'a option
 end
 
-module MakeNoCFG
+module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = struct
-    (Scheduler : Scheduler.S)
+  module CFG = TransferFunctions.CFG
-    (TransferFunctions : TransferFunctions.SIL with module CFG = Scheduler.CFG) =
-struct
-  module CFG = Scheduler.CFG
   module Node = CFG.Node
   module TransferFunctions = TransferFunctions
   module InvariantMap = TransferFunctions.CFG.Node.IdMap
   module Domain = TransferFunctions.Domain
 
-  type invariant_map = Domain.astate state InvariantMap.t
+  type invariant_map = Domain.astate State.t InvariantMap.t
 
   (** extract the state of node [n] from [inv_map] *)
   let extract_state node_id inv_map = InvariantMap.find_opt node_id inv_map
 
   (** extract the postcondition of node [n] from [inv_map] *)
-  let extract_post node_id inv_map =
+  let extract_post node_id inv_map = extract_state node_id inv_map |> Option.map ~f:State.post
-    match extract_state node_id inv_map with Some state -> Some state.post | None -> None
-
 
   (** extract the precondition of node [n] from [inv_map] *)
-  let extract_pre node_id inv_map =
+  let extract_pre node_id inv_map = extract_state node_id inv_map |> Option.map ~f:State.pre
-    match extract_state node_id inv_map with Some state -> Some state.pre | None -> None
-
 
   let debug_absint_operation op node =
     let pp_name fmt =
@@ -92,44 +114,49 @@ struct
     NodePrinter.finish_session underlying_node
 
 
-  let exec_node node astate_pre work_queue inv_map ({ProcData.pdesc} as proc_data) ~debug =
+  let exec_instrs ~debug proc_data node node_id ~visit_count pre inv_map =
-    let node_id = Node.id node in
+    let on_instrs instrs =
-    let update_inv_map pre ~visit_count =
+      if Config.write_html && debug <> DefaultNoExecInstr_UseFromLowerHilAbstractInterpreterOnly
-      let exec_instrs instrs =
+      then
-        if Config.write_html && debug <> DefaultNoExecInstr_UseFromLowerHilAbstractInterpreterOnly
+        NodePrinter.start_session
-        then
+          ~pp_name:(TransferFunctions.pp_session_name node)
-          NodePrinter.start_session
+          (Node.underlying_node node) ;
-            ~pp_name:(TransferFunctions.pp_session_name node)
+      let astate_post =
-            (Node.underlying_node node) ;
+        let compute_post pre instr =
-        let astate_post =
+          try TransferFunctions.exec_instr pre proc_data node instr with exn ->
-          let compute_post pre instr =
+            IExn.reraise_after exn ~f:(fun () ->
-            try TransferFunctions.exec_instr pre proc_data node instr with exn ->
+                L.internal_error "In instruction %a@\n" (Sil.pp_instr Pp.text) instr )
-              IExn.reraise_after exn ~f:(fun () ->
-                  L.internal_error "In instruction %a@\n" (Sil.pp_instr Pp.text) instr )
-          in
-          Instrs.fold ~f:compute_post ~init:pre instrs
         in
-        if Config.write_html && debug <> DefaultNoExecInstr_UseFromLowerHilAbstractInterpreterOnly
+        Instrs.fold ~f:compute_post ~init:pre instrs
-        then (
-          L.d_strln
-            ( Format.asprintf "@[PRE: %a@]@\n@[INSTRS: %a@]@[POST: %a@]@." Domain.pp pre
-                (Instrs.pp Pp.text) instrs Domain.pp astate_post
-            |> Escape.escape_xml ) ;
-          NodePrinter.finish_session (Node.underlying_node node) ) ;
-        let inv_map' = InvariantMap.add node_id {pre; post= astate_post; visit_count} inv_map in
-        (inv_map', Scheduler.schedule_succs work_queue node)
       in
+      if Config.write_html && debug <> DefaultNoExecInstr_UseFromLowerHilAbstractInterpreterOnly
+      then (
+        L.d_strln
+          ( Format.asprintf "@[PRE: %a@]@\n@[INSTRS: %a@]@[POST: %a@]@." Domain.pp pre
+              (Instrs.pp Pp.text) instrs Domain.pp astate_post
+          |> Escape.escape_xml ) ;
+        NodePrinter.finish_session (Node.underlying_node node) ) ;
+      InvariantMap.add node_id {State.pre; post= astate_post; visit_count} inv_map
+    in
+    let instrs = CFG.instrs node in
+    if Instrs.is_empty instrs then
       (* hack to ensure that we call `exec_instr` on a node even if it has no instructions *)
-      let instrs = CFG.instrs node in
+      on_instrs (Instrs.singleton Sil.skip_instr)
-      if Instrs.is_empty instrs then exec_instrs (Instrs.singleton Sil.skip_instr)
+    else on_instrs instrs
-      else exec_instrs instrs
+
+
+  let exec_node ~debug ({ProcData.pdesc} as proc_data) node ~is_loop_head astate_pre inv_map =
+    let node_id = Node.id node in
+    let update_inv_map pre ~visit_count =
+      let inv_map' = exec_instrs ~debug proc_data node node_id ~visit_count pre inv_map in
+      (inv_map', DidNotReachFixPoint)
     in
-    if InvariantMap.mem node_id inv_map then (
+    if InvariantMap.mem node_id inv_map then
       let old_state = InvariantMap.find node_id inv_map in
       let widened_pre =
-        if CFG.is_loop_head pdesc node then (
+        if is_loop_head then (
-          let num_iters = old_state.visit_count in
+          let num_iters = (old_state.State.visit_count :> int) in
-          let prev = old_state.pre in
+          let prev = old_state.State.pre in
           let next = astate_pre in
           let res = Domain.widen ~prev ~next ~num_iters in
           if Config.write_html then
@@ -137,48 +164,69 @@ struct
           res )
         else astate_pre
       in
-      if Domain.( <= ) ~lhs:widened_pre ~rhs:old_state.pre then (inv_map, work_queue)
+      if Domain.( <= ) ~lhs:widened_pre ~rhs:old_state.State.pre then (inv_map, ReachedFixPoint)
       else
-        let visit_count' = old_state.visit_count + 1 in
+        let visit_count' = VisitCount.succ ~pdesc old_state.State.visit_count in
-        if visit_count' > Config.max_widens then
+        update_inv_map widened_pre ~visit_count:visit_count'
-          L.(die InternalError)
+    else
-            "Exceeded max widening threshold %d while analyzing %a. Please check your widening \
+      (* first time visiting this node *)
-             operator or increase the threshold"
+      update_inv_map astate_pre ~visit_count:VisitCount.first_time
-            Config.max_widens Typ.Procname.pp (Procdesc.get_proc_name pdesc) ;
+
-        update_inv_map widened_pre ~visit_count:visit_count' )
+
-    else (* first time visiting this node *)
+  let compute_pre cfg node inv_map =
-      update_inv_map astate_pre ~visit_count:1
+    let extract_post_ pred = extract_post (Node.id pred) inv_map in
-
+    CFG.fold_preds cfg node ~init:None ~f:(fun joined_post_opt pred ->
-
+        match extract_post_ pred with
-  let rec exec_worklist cfg work_queue inv_map proc_data ~debug =
+        | None ->
-    let compute_pre node inv_map =
+            joined_post_opt
-      let extract_post_ pred = extract_post (Node.id pred) inv_map in
+        | Some post as some_post -> (
-      CFG.fold_preds cfg node ~init:None ~f:(fun joined_post_opt pred ->
+          match joined_post_opt with
-          match extract_post_ pred with
           | None ->
-              joined_post_opt
+              some_post
-          | Some post as some_post -> (
+          | Some joined_post ->
-            match joined_post_opt with
+              let res = Domain.join joined_post post in
-            | None ->
+              if Config.write_html then
-                some_post
+                debug_absint_operation (`Join (joined_post, post, res)) node ;
-            | Some joined_post ->
+              Some res ) )
-                let res = Domain.join joined_post post in
+
-                if Config.write_html then
+
-                  debug_absint_operation (`Join (joined_post, post, res)) node ;
+  (** compute and return an invariant map for [pdesc] *)
-                Some res ) )
+  let make_exec_pdesc ~exec_cfg_internal ({ProcData.pdesc} as proc_data) ~initial =
-    in
+    exec_cfg_internal ~debug:Default (CFG.from_pdesc pdesc) proc_data ~initial
+
+
+  (** compute and return the postcondition of [pdesc] *)
+  let make_compute_post ~exec_cfg_internal ?(debug = Default) ({ProcData.pdesc} as proc_data)
+      ~initial =
+    let cfg = CFG.from_pdesc pdesc in
+    let inv_map = exec_cfg_internal ~debug cfg proc_data ~initial in
+    extract_post (Node.id (CFG.exit_node cfg)) inv_map
+end
+
+module MakeWithScheduler
+    (Scheduler : Scheduler.S)
+    (TransferFunctions : TransferFunctions.SIL with module CFG = Scheduler.CFG) =
+struct
+  include AbstractInterpreterCommon (TransferFunctions)
+
+  let rec exec_worklist ~debug cfg ({ProcData.pdesc} as proc_data) work_queue inv_map =
     match Scheduler.pop work_queue with
     | Some (_, [], work_queue') ->
-        exec_worklist cfg work_queue' inv_map proc_data ~debug
+        exec_worklist ~debug cfg proc_data work_queue' inv_map
     | Some (node, _, work_queue') ->
         let inv_map_post, work_queue_post =
-          match compute_pre node inv_map with
+          match compute_pre cfg node inv_map with
-          | Some astate_pre ->
+          | Some astate_pre -> (
-              exec_node node astate_pre work_queue' inv_map proc_data ~debug
+              let is_loop_head = CFG.is_loop_head pdesc node in
+              match exec_node ~debug proc_data node ~is_loop_head astate_pre inv_map with
+              | inv_map, ReachedFixPoint ->
+                  (inv_map, work_queue')
+              | inv_map, DidNotReachFixPoint ->
+                  (inv_map, Scheduler.schedule_succs work_queue' node) )
           | None ->
               (inv_map, work_queue')
         in
-        exec_worklist cfg work_queue_post inv_map_post proc_data ~debug
+        exec_worklist ~debug cfg proc_data work_queue_post inv_map_post
     | None ->
         inv_map
 
@@ -186,25 +234,22 @@ struct
   (* compute and return an invariant map for [cfg] *)
   let exec_cfg_internal ~debug cfg proc_data ~initial =
     let start_node = CFG.start_node cfg in
-    let inv_map', work_queue' =
+    let inv_map, _did_not_reach_fix_point =
-      exec_node start_node initial (Scheduler.empty cfg) InvariantMap.empty proc_data ~debug
+      exec_node ~debug proc_data start_node ~is_loop_head:false initial InvariantMap.empty
     in
-    exec_worklist cfg work_queue' inv_map' proc_data ~debug
+    let work_queue = Scheduler.schedule_succs (Scheduler.empty cfg) start_node in
+    exec_worklist ~debug cfg proc_data work_queue inv_map
 
 
   let exec_cfg = exec_cfg_internal ~debug:Default
 
-  (* compute and return an invariant map for [pdesc] *)
+  let exec_pdesc = make_exec_pdesc ~exec_cfg_internal
-  let exec_pdesc ({ProcData.pdesc} as proc_data) = exec_cfg (CFG.from_pdesc pdesc) proc_data
 
-  (* compute and return the postcondition of [pdesc] *)
+  let compute_post = make_compute_post ~exec_cfg_internal
-  let compute_post ?(debug = Default) ({ProcData.pdesc} as proc_data) ~initial =
-    let cfg = CFG.from_pdesc pdesc in
-    let inv_map = exec_cfg_internal cfg proc_data ~initial ~debug in
-    extract_post (Node.id (CFG.exit_node cfg)) inv_map
 end
 
-module MakeWithScheduler (C : ProcCfg.S) (S : Scheduler.Make) (T : TransferFunctions.MakeSIL) =
+module type Make = functor (TransferFunctions : TransferFunctions.SIL) -> S
-  MakeNoCFG (S (C)) (T (C))
+                                                                          with module TransferFunctions = TransferFunctions
-module Make (C : ProcCfg.S) (T : TransferFunctions.MakeSIL) =
+
-  MakeWithScheduler (C) (Scheduler.ReversePostorder) (T)
+module MakeRPO (T : TransferFunctions.SIL) =
+  MakeWithScheduler (Scheduler.ReversePostorder (T.CFG)) (T)

infer/src/absint/AbstractInterpreter.mli

@@ -9,7 +9,13 @@ open! IStd
 
 type debug = Default | DefaultNoExecInstr_UseFromLowerHilAbstractInterpreterOnly
 
-type 'a state = {pre: 'a; post: 'a; visit_count: int}
+module VisitCount : sig
+  type t
+end
+
+module State : sig
+  type 'a t = {pre: 'a; post: 'a; visit_count: VisitCount.t}
+end
 
 (** type of an intraprocedural abstract interpreter *)
 module type S = sig
@@ -18,7 +24,7 @@ module type S = sig
   module InvariantMap = TransferFunctions.CFG.Node.IdMap
 
   (** invariant map from node id -> state representing postcondition for node id *)
-  type invariant_map = TransferFunctions.Domain.astate state InvariantMap.t
+  type invariant_map = TransferFunctions.Domain.astate State.t InvariantMap.t
 
   val compute_post :
        ?debug:debug
@@ -38,23 +44,18 @@ module type S = sig
     TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate -> invariant_map
   (** compute and return invariant map for the given procedure starting from [initial] *)
 
-  val extract_post : InvariantMap.key -> 'a state InvariantMap.t -> 'a option
+  val extract_post : InvariantMap.key -> 'a State.t InvariantMap.t -> 'a option
   (** extract the postcondition for a node id from the given invariant map *)
 
-  val extract_pre : InvariantMap.key -> 'a state InvariantMap.t -> 'a option
+  val extract_pre : InvariantMap.key -> 'a State.t InvariantMap.t -> 'a option
   (** extract the precondition for a node id from the given invariant map *)
 
   val extract_state : InvariantMap.key -> 'a InvariantMap.t -> 'a option
   (** extract the state for a node id from the given invariant map *)
 end
 
-(** create an intraprocedural abstract interpreter from a scheduler and transfer functions *)
+module type Make = functor (TransferFunctions : TransferFunctions.SIL) -> S
-module MakeNoCFG
+                                                                          with module TransferFunctions = TransferFunctions
-    (Scheduler : Scheduler.S)
-    (TransferFunctions : TransferFunctions.SIL with module CFG = Scheduler.CFG) :
-  S with module TransferFunctions = TransferFunctions
 
-(** create an intraprocedural abstract interpreter from a CFG and functors for creating a scheduler/
+(** create an intraprocedural abstract interpreter from transfer functions using the reverse post-order scheduler *)
-    transfer functions from a CFG *)
+module MakeRPO : Make
-module Make (CFG : ProcCfg.S) (MakeTransferFunctions : TransferFunctions.MakeSIL) :
-  S with module TransferFunctions = MakeTransferFunctions(CFG)

infer/src/absint/LowerHil.ml

@@ -90,7 +90,7 @@ module MakeAbstractInterpreterWithConfig
     (CFG : ProcCfg.S)
     (MakeTransferFunctions : TransferFunctions.MakeHIL) =
 struct
-  module Interpreter = AbstractInterpreter.Make (CFG) (Make (MakeTransferFunctions) (HilConfig))
+  module Interpreter = AbstractInterpreter.MakeRPO (Make (MakeTransferFunctions) (HilConfig) (CFG))
 
   let debug = AbstractInterpreter.DefaultNoExecInstr_UseFromLowerHilAbstractInterpreterOnly
 

infer/src/absint/LowerHil.mli

@@ -39,7 +39,7 @@ module MakeAbstractInterpreterWithConfig
     (CFG : ProcCfg.S)
     (MakeTransferFunctions : TransferFunctions.MakeHIL) : sig
   module Interpreter :
-      module type of AbstractInterpreter.Make (CFG) (Make (MakeTransferFunctions) (HilConfig))
+      module type of AbstractInterpreter.MakeRPO (Make (MakeTransferFunctions) (HilConfig) (CFG))
 
   val compute_post :
        Interpreter.TransferFunctions.extras ProcData.t

infer/src/backend/preanal.ml

@@ -35,7 +35,7 @@ let add_abstraction_instructions pdesc =
 
 
 module BackwardCfg = ProcCfg.Backward (ProcCfg.Exceptional)
-module LivenessAnalysis = AbstractInterpreter.Make (BackwardCfg) (Liveness.TransferFunctions)
+module LivenessAnalysis = AbstractInterpreter.MakeRPO (Liveness.TransferFunctions (BackwardCfg))
 module VarDomain = Liveness.Domain
 
 (** computes the non-nullified reaching definitions at the end of each node by building on the
@@ -57,7 +57,7 @@ module NullifyTransferFunctions = struct
     let node_id = Procdesc.Node.get_id (CFG.Node.underlying_node node) in
     match LivenessAnalysis.extract_state node_id extras with
     (* note: because the analysis is backward, post and pre are reversed *)
-    | Some {AbstractInterpreter.post= live_before; pre= live_after} ->
+    | Some {AbstractInterpreter.State.post= live_before; pre= live_after} ->
         let to_nullify = VarDomain.diff (VarDomain.union live_before reaching_defs) live_after in
         let reaching_defs' = VarDomain.diff reaching_defs to_nullify in
         (reaching_defs', to_nullify)
@@ -105,9 +105,7 @@ module NullifyTransferFunctions = struct
   let pp_session_name _node fmt = Format.pp_print_string fmt "nullify"
 end
 
-module NullifyAnalysis =
+module NullifyAnalysis = AbstractInterpreter.MakeRPO (NullifyTransferFunctions)
-  AbstractInterpreter.MakeNoCFG
-    (Scheduler.ReversePostorder (ProcCfg.Exceptional)) (NullifyTransferFunctions)
 
 let add_nullify_instrs pdesc tenv liveness_inv_map =
   let address_taken_vars =

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -239,7 +239,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 end
 
 module CFG = ProcCfg.NormalOneInstrPerNode
-module Analyzer = AbstractInterpreter.Make (CFG) (TransferFunctions)
+module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions (CFG))
 
 type invariant_map = Analyzer.invariant_map
 
@@ -572,16 +572,16 @@ module Report = struct
       -> CFG.t
       -> CFG.Node.t
       -> Instrs.not_reversed_t
-      -> Dom.Mem.astate AbstractInterpreter.state
+      -> Dom.Mem.astate AbstractInterpreter.State.t
       -> PO.ConditionSet.t
       -> PO.ConditionSet.t =
    fun summary pdesc tenv symbol_table cfg node instrs state cond_set ->
     match state with
     | _ when Instrs.is_empty instrs ->
         cond_set
-    | {AbstractInterpreter.pre= Bottom} ->
+    | {AbstractInterpreter.State.pre= Bottom} ->
         cond_set
-    | {AbstractInterpreter.pre= NonBottom _ as pre; post} ->
+    | {AbstractInterpreter.State.pre= NonBottom _ as pre; post} ->
         if Instrs.nth_exists instrs 1 then
           L.(die InternalError) "Did not expect several instructions" ;
         let instr = Instrs.nth_exn instrs 0 in

infer/src/checkers/BoundedCallTree.ml

@@ -139,7 +139,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   let pp_session_name _node fmt = F.pp_print_string fmt "crashcontext"
 end
 
-module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (TransferFunctions)
+module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions (ProcCfg.Exceptional))
 
 let loaded_stacktraces =
   (* Load all stacktraces defined in either Config.stacktrace or

infer/src/checkers/NullabilityPreanalysis.ml

@@ -62,7 +62,7 @@ end
 
 (* Tracks when block variables of ObjC classes have been assigned to in constructors *)
 module FieldsAssignedInConstructorsChecker =
-  AbstractInterpreter.Make (ProcCfg.Normal) (TransferFunctions)
+  AbstractInterpreter.MakeRPO (TransferFunctions (ProcCfg.Normal))
 
 let add_annot annot annot_name = ({Annot.class_name= annot_name; parameters= []}, true) :: annot
 

infer/src/checkers/SimpleChecker.ml

@@ -78,13 +78,13 @@ module Make (Spec : Spec) : S = struct
     let pp_session_name _node fmt = F.pp_print_string fmt "simple checker"
   end
 
-  module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (TransferFunctions)
+  module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions (ProcCfg.Exceptional))
 
   let checker {Callbacks.proc_desc; tenv; summary} : Summary.t =
     let proc_name = Procdesc.get_proc_name proc_desc in
     let nodes = Procdesc.get_nodes proc_desc in
     let do_reporting node_id state =
-      let astate_set = state.AbstractInterpreter.post in
+      let astate_set = state.AbstractInterpreter.State.post in
       if not (Domain.is_empty astate_set) then
         (* should never fail since keys in the invariant map should always be real node id's *)
         let node =

infer/src/checkers/Siof.ml

@@ -209,7 +209,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   let pp_session_name _node fmt = F.pp_print_string fmt "siof"
 end
 
-module Analyzer = AbstractInterpreter.Make (ProcCfg.Normal) (TransferFunctions)
+module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions (ProcCfg.Normal))
 
 let is_foreign current_tu v =
   match Pvar.get_translation_unit v with

infer/src/checkers/addressTaken.ml

@@ -53,4 +53,4 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   let pp_session_name _node fmt = Format.pp_print_string fmt "address taken"
 end
 
-module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (TransferFunctions)
+module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions (ProcCfg.Exceptional))

infer/src/checkers/annotationReachability.ml

@@ -432,7 +432,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   let pp_session_name _node fmt = F.pp_print_string fmt "annotation reachability"
 end
 
-module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (TransferFunctions)
+module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions (ProcCfg.Exceptional))
 
 let checker ({Callbacks.proc_desc; tenv; summary} as callback) : Summary.t =
   let initial = (AnnotReachabilityDomain.empty, NonBottom Domain.TrackingVar.empty) in

infer/src/checkers/control.ml

@@ -9,7 +9,7 @@ open! IStd
 module F = Format
 module L = Logging
 (* forward dependency analysis for computing set of variables that
-   affect the looping behavior of the program 
+   affect the looping behavior of the program
 
    1. perform a control flow dependency analysis by getting all the
    variables that appear in the guards of the loops.
@@ -17,7 +17,7 @@ module L = Logging
    2. for each control dependency per node, find its respective data
    dependency
 
-   3. remove invariant vars in the loop from control vars 
+   3. remove invariant vars in the loop from control vars
  *)
 
 module VarSet = AbstractDomain.FiniteSet (Var)
@@ -147,7 +147,7 @@ module TransferFunctionsControlDeps (CFG : ProcCfg.S) = struct
     F.fprintf fmt "control dependency analysis %a" CFG.Node.pp_id (CFG.Node.id node)
 end
 
-module ControlDepAnalyzer = AbstractInterpreter.Make (CFG) (TransferFunctionsControlDeps)
+module ControlDepAnalyzer = AbstractInterpreter.MakeRPO (TransferFunctionsControlDeps (CFG))
 
 (* Filter CVs which are invariant in the loop where the CV originated from *)
 let remove_invariant_vars control_vars loop_inv_map =

infer/src/checkers/cost.ml

@@ -26,7 +26,6 @@ let expensive_threshold = BasicCost.of_int_exn 200
 (* CFG modules used in several other modules  *)
 module InstrCFG = ProcCfg.NormalOneInstrPerNode
 module NodeCFG = ProcCfg.Normal
-module InstrCFGScheduler = Scheduler.ReversePostorder (InstrCFG)
 module Node = ProcCfg.DefaultNode
 
 (* Compute a map (node,instruction) -> basic_cost, where basic_cost is the
@@ -99,8 +98,7 @@ module TransferFunctionsNodesBasicCost = struct
   let pp_session_name node fmt = F.fprintf fmt "cost(basic) %a" CFG.Node.pp_id (CFG.Node.id node)
 end
 
-module AnalyzerNodesBasicCost =
+module AnalyzerNodesBasicCost = AbstractInterpreter.MakeRPO (TransferFunctionsNodesBasicCost)
-  AbstractInterpreter.MakeNoCFG (InstrCFGScheduler) (TransferFunctionsNodesBasicCost)
 
 (* Map associating to each node a bound on the number of times it can be executed.
    This bound is computed using environments (map: val -> values), using the following
@@ -720,7 +718,7 @@ module TransferFunctionsWCET = struct
   let pp_session_name _node fmt = F.pp_print_string fmt "cost(wcet)"
 end
 
-module AnalyzerWCET = AbstractInterpreter.MakeNoCFG (InstrCFGScheduler) (TransferFunctionsWCET)
+module AnalyzerWCET = AbstractInterpreter.MakeRPO (TransferFunctionsWCET)
 
 let check_and_report_top_and_bottom cost proc_desc summary =
   let report issue suffix =

infer/src/checkers/liveness.ml

@@ -75,7 +75,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 end
 
 module CFG = ProcCfg.OneInstrPerNode (ProcCfg.Backward (ProcCfg.Exceptional))
-module Analyzer = AbstractInterpreter.Make (CFG) (TransferFunctions)
+module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions (CFG))
 
 (* It's fine to have a dead store on a type that uses the "scope guard" pattern. These types
    are only read in their destructors, and this is expected/ok.
@@ -118,7 +118,7 @@ module CapturedByRefTransferFunctions (CFG : ProcCfg.S) = struct
 end
 
 module CapturedByRefAnalyzer =
-  AbstractInterpreter.Make (ProcCfg.Exceptional) (CapturedByRefTransferFunctions)
+  AbstractInterpreter.MakeRPO (CapturedByRefTransferFunctions (ProcCfg.Exceptional))
 
 let get_captured_by_ref_invariant_map proc_desc proc_data =
   let cfg = ProcCfg.Exceptional.from_pdesc proc_desc in

infer/src/checkers/reachingDefs.ml

@@ -64,4 +64,4 @@ let init_reaching_defs_with_formals pdesc =
          ReachingDefsMap.add (Var.of_pvar pvar) start_node_defs acc )
 
 
-module Analyzer = AbstractInterpreter.Make (ProcCfg.Normal) (TransferFunctionsReachingDefs)
+module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctionsReachingDefs (ProcCfg.Normal))

infer/src/unit/analyzerTester.ml

@@ -147,10 +147,13 @@ module StructuredSil = struct
     make_call ?return args
 end
 
-module Make (CFG : ProcCfg.S with type Node.t = Procdesc.Node.t) (T : TransferFunctions.MakeSIL) =
+module MakeMake
+    (MakeAbstractInterpreter : AbstractInterpreter.Make)
+    (CFG : ProcCfg.S with type Node.t = Procdesc.Node.t)
+    (T : TransferFunctions.MakeSIL) =
 struct
   open StructuredSil
-  module I = AbstractInterpreter.Make (CFG) (T)
+  module I = MakeAbstractInterpreter (T (CFG))
   module M = I.InvariantMap
 
   let structured_program_to_cfg program test_pname =
@@ -239,15 +242,15 @@ struct
     (pdesc, assert_map)
 
 
-  let create_test test_program extras pp_opt ~initial test_pname _ =
+  let create_test test_program extras ~initial pp_opt test_pname _ =
     let pp_state = Option.value ~default:I.TransferFunctions.Domain.pp pp_opt in
     let pdesc, assert_map = structured_program_to_cfg test_program test_pname in
     let inv_map = I.exec_pdesc (ProcData.make pdesc (Tenv.create ()) extras) ~initial in
     let collect_invariant_mismatches node_id (inv_str, inv_label) error_msgs_acc =
       let post_str =
         try
-          let state = M.find node_id inv_map in
+          let {AbstractInterpreter.State.post} = M.find node_id inv_map in
-          F.asprintf "%a" pp_state state.post
+          F.asprintf "%a" pp_state post
         with Caml.Not_found -> "_|_"
       in
       if inv_str <> post_str then
@@ -273,12 +276,20 @@ struct
           |> F.flush_str_formatter
         in
         OUnit2.assert_failure assert_fail_message
+end
+
+module Make (CFG : ProcCfg.S with type Node.t = Procdesc.Node.t) (T : TransferFunctions.MakeSIL) =
+struct
+  module AI_RPO = MakeMake (AbstractInterpreter.MakeRPO) (CFG) (T)
 
+  let ai_list = [("ai_rpo", AI_RPO.create_test)]
 
   let create_tests ?(test_pname = Typ.Procname.empty_block) ~initial ?pp_opt extras tests =
     let open OUnit2 in
-    List.map
+    List.concat_map
       ~f:(fun (name, test_program) ->
-        name >:: create_test test_program extras ~initial pp_opt test_pname )
+        List.map ai_list ~f:(fun (ai_name, create_test) ->
+            name ^ "_" ^ ai_name >:: create_test test_program extras ~initial pp_opt test_pname )
+        )
       tests
 end

infer/src/unit/inferunit.ml

@@ -31,19 +31,19 @@ let () =
         ; AccessTreeTests.tests
         ; AddressTakenTests.tests
         ; BoundedCallTreeTests.tests
-        ; DifferentialTests.tests
         ; DifferentialFiltersTests.tests
+        ; DifferentialTests.tests
         ; FileDiffTests.tests
         ; IListTests.tests
         ; JavaProfilerSamplesTest.tests
+        ; LivenessTests.tests
         ; PerfProfilerATDParserTest.tests
         ; ProcCfgTests.tests
-        ; LivenessTests.tests
         ; SchedulerTests.tests
+        ; SeverityTests.tests
         ; StacktraceTests.tests
         ; TaintTests.tests
-        ; TraceTests.tests
+        ; TraceTests.tests ]
-        ; SeverityTests.tests ]
       @ ClangTests.tests )
   in
   let test_suite = "all" >::: tests in

infer/src/unit/schedulerTests.ml

@@ -84,8 +84,7 @@ module MockProcCfg = struct
 
   let from_adjacency_list t = t
 
-  (* not called by the scheduler *)
+  let start_node _ = 1
-  let start_node _ = assert false
 
   let exit_node _ = assert false
 
@@ -117,21 +116,24 @@ let create_test test_graph expected_result _ =
   OUnit2.assert_equal ~pp_diff result expected_result
 
 
+let inputs =
+  [ ("straightline", [(1, [2]); (2, [3]); (3, [4])], [1; 2; 3; 4])
+  ; ("if_then_else", [(1, [2; 3]); (2, [4]); (3, [4]); (4, [5])], [1; 2; 3; 4; 5])
+  ; ("if_then", [(1, [2; 4]); (2, [3]); (3, [4]); (4, [5])], [1; 2; 3; 4; 5])
+  ; ( "diamond"
+    , [(1, [2; 3]); (2, [4]); (3, [4]); (4, [5; 6]); (5, [7]); (6, [7]); (7, [8])]
+    , [1; 2; 3; 4; 5; 6; 7; 8] )
+  ; ( "switch"
+    , [(1, [2; 3; 4; 5]); (2, [6]); (3, [6]); (4, [6]); (5, [6]); (6, [7])]
+    , [1; 2; 3; 4; 5; 6; 7] )
+  ; ( "nums_order_irrelevant"
+    , [(11, [10]); (1, [7; 2]); (2, [3; 11]); (7, [11]); (3, [7])]
+    , [1; 2; 3; 7; 11; 10] ) ]
+
+
 let tests =
   let open OUnit2 in
   let test_list =
-    [ ("straightline", [(1, [2]); (2, [3]); (3, [4])], [1; 2; 3; 4])
+    inputs |> List.map ~f:(fun (name, test, expected) -> name >:: create_test test expected)
-    ; ("if_then_else", [(1, [2; 3]); (2, [4]); (3, [4]); (4, [5])], [1; 2; 3; 4; 5])
-    ; ("if_then", [(1, [2; 4]); (2, [3]); (3, [4]); (4, [5])], [1; 2; 3; 4; 5])
-    ; ( "diamond"
-      , [(1, [2; 3]); (2, [4]); (3, [4]); (4, [5; 6]); (5, [7]); (6, [7]); (7, [8])]
-      , [1; 2; 3; 4; 5; 6; 7; 8] )
-    ; ( "switch"
-      , [(1, [2; 3; 4; 5]); (2, [6]); (3, [6]); (4, [6]); (5, [6]); (6, [7])]
-      , [1; 2; 3; 4; 5; 6; 7] )
-    ; ( "nums_order_irrelevant"
-      , [(11, [10]); (1, [7; 2]); (2, [3; 11]); (7, [11]); (3, [7])]
-      , [1; 2; 3; 7; 11; 10] ) ]
-    |> List.map ~f:(fun (name, test, expected) -> name >:: create_test test expected)
   in
   "scheduler_suite" >::: test_list