adding optional postprocessing step to transfer functions

Reviewed By: jeremydubreil

Differential Revision: D3237864

fb-gh-sync-id: e6e5f92
fbshipit-source-id: e6e5f92

infer/src/checkers/abstractInterpreter.ml

@@ -53,7 +53,8 @@ module Make
           if A.is_bottom astate_acc
           then astate_acc
           else T.exec_instr astate_acc proc_data instr in
-        IList.fold_left exec_instrs astate_pre (C.instrs node) in
+        let astate_post_instrs = IList.fold_left exec_instrs astate_pre (C.instrs node) in
+        T.postprocess astate_post_instrs node_id proc_data in
       L.out "Post for node %a is %a@." Cfg.Node.pp_id node_id A.pp astate_post;
       let inv_map' = M.add node_id { pre=astate_pre; post=astate_post; visit_count; } inv_map in
       inv_map', S.schedule_succs work_queue node in

infer/src/checkers/addressTaken.ml

@@ -21,6 +21,8 @@ module TransferFunctions = struct
   type astate = Domain.astate
   type extras = ProcData.no_extras
 
+  let postprocess = TransferFunctions.no_postprocessing
+
   let rec add_address_taken_pvars exp astate = match exp with
     | Sil.Lvar pvar ->
         Domain.add pvar astate

infer/src/checkers/annotationReachability.ml

@@ -305,6 +305,8 @@ module TransferFunctions = struct
   type astate = Domain.astate
   type extras = ProcData.no_extras
 
+  let postprocess = TransferFunctions.no_postprocessing
+
   (* This is specific to the @NoAllocation and @PerformanceCritical checker
      and the "unlikely" method is used to guard branches that are expected to run sufficiently
      rarely to not affect the performances *)

infer/src/checkers/copyPropagation.ml

@@ -83,6 +83,8 @@ module TransferFunctions = struct
   type astate = Domain.astate
   type extras = ProcData.no_extras
 
+  let postprocess = TransferFunctions.no_postprocessing
+
   let exec_instr astate _ = function
     | Sil.Letderef (lhs_id, Sil.Var rhs_id, _, _) ->
         (* note: logical vars are SSA, don't need to worry about overwriting existing bindings *)

infer/src/checkers/liveness.ml

@@ -22,6 +22,8 @@ module TransferFunctions = struct
   type astate = Domain.astate
   type extras = ProcData.no_extras
 
+  let postprocess = TransferFunctions.no_postprocessing
+
   (* add all of the vars read in [exp] to the live set *)
   let exp_add_live exp astate =
     let (ids, pvars) = Sil.exp_get_vars exp in

infer/src/checkers/transferFunctions.ml

@@ -9,11 +9,16 @@
 
 open! Utils
 
-
 module type S = sig
   type astate (* abstract state to propagate *)
   type extras (* read-only extra state (results of previous analyses, globals, etc.) *)
 
   (* {A} instr {A'}. [caller_pdesc] is the procdesc of the current procedure *)
   val exec_instr : astate -> extras ProcData.t -> Sil.instr -> astate
+
+  (* optional postprocessing step to be performed after executing node [id]. *)
+  val postprocess : astate -> Cfg.Node.id -> extras ProcData.t -> astate
 end
+
+(* default postprocessing: do nothing *)
+let no_postprocessing astate _ _ = astate

infer/src/unit/abstractInterpreterTests.ml

@@ -52,6 +52,8 @@ module PathCountTransferFunctions = struct
   type astate = PathCountDomain.astate
   type extras = ProcData.no_extras
 
+  let postprocess = TransferFunctions.no_postprocessing
+
   (* just propagate the current path count *)
   let exec_instr astate _ _ = astate
 end