redesigning abstract interpreter to allow easy composition of analyses

Reviewed By: jberdine

Differential Revision: D3327656

fbshipit-source-id: a5e429f

infer/src/backend/preanal.ml

@@ -118,14 +118,10 @@ module LivenessAnalysis =
   AbstractInterpreter.Make
     (BackwardCfg)
     (Scheduler.ReversePostorder)
-    (Liveness.Domain)
     (Liveness.TransferFunctions)
 
 module VarDomain = AbstractDomain.FiniteSet(Var.Set)
 
-(* (reaching non-nullified vars) * (vars to nullify) *)
-module NullifyDomain = AbstractDomain.Pair (VarDomain) (VarDomain)
-
 (** computes the non-nullified reaching definitions at the end of each node by building on the
     results of a liveness analysis to be precise, what we want to compute is:
     to_nullify := (live_before U non_nullifed_reaching_defs) - live_after
@@ -135,20 +131,29 @@ module NullifyDomain = AbstractDomain.Pair (VarDomain) (VarDomain)
     each pvar in to_nullify afer we finish the analysis. Nullify instructions speed up the analysis
     by enabling it to GC state that will no longer be read. *)
 module NullifyTransferFunctions = struct
-  type astate = NullifyDomain.astate
+  (* (reaching non-nullified vars) * (vars to nullify) *)
+  module Domain = AbstractDomain.Pair (VarDomain) (VarDomain)
+  module CFG = ProcCfg.Exceptional
   type extras = LivenessAnalysis.inv_map
-  type node_id = BackwardCfg.id
 
   let postprocess ((reaching_defs, _) as astate) node_id { ProcData.extras; } =
     match LivenessAnalysis.extract_state node_id extras with
     (* note: because the analysis backward, post and pre are reversed *)
-    | Some { LivenessAnalysis.post = live_before; pre = live_after; } ->
+    | Some { AbstractInterpreter.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)
     | None -> astate
 
-  let exec_instr ((active_defs, to_nullify) as astate) _ = function
+  let is_last_instr_in_node instr node =
+    let rec is_last_instr instr = function
+      | [] -> true
+      | last_instr :: [] -> Sil.instr_compare instr last_instr = 0
+      | _ :: instrs -> is_last_instr instr instrs in
+    is_last_instr instr (CFG.instrs node)
+
+  let exec_instr ((active_defs, to_nullify) as astate) extras node instr =
+    let astate' = match instr with
       | Sil.Letderef (lhs_id, _, _, _) ->
           VarDomain.add (Var.of_id lhs_id) active_defs, to_nullify
       | Sil.Call (lhs_ids, _, _, _, _) ->
@@ -164,14 +169,15 @@ module NullifyTransferFunctions = struct
       | Abstract _ ->
           astate
       | Sil.Nullify _ ->
-        failwith "Should not add nullify instructions before running nullify analysis!"
+          failwith "Should not add nullify instructions before running nullify analysis!" in
+    if is_last_instr_in_node instr node
+    then postprocess astate' (CFG.id node) extras
+    else astate'
 end
 
 module NullifyAnalysis =
-  AbstractInterpreter.Make
-    (ProcCfg.Exceptional)
-    (Scheduler.ReversePostorder)
-    (NullifyDomain)
+  AbstractInterpreter.MakeNoCFG
+    (Scheduler.ReversePostorder (ProcCfg.Exceptional))
     (NullifyTransferFunctions)
 
 let add_nullify_instrs tenv _ pdesc =

infer/src/checkers/abstractInterpreter.ml

@@ -11,18 +11,26 @@ open! Utils
 
 module L = Logging
 
-module Make
-    (CFG : ProcCfg.S)
-    (Sched : Scheduler.S)
-    (A : AbstractDomain.S)
-    (T : TransferFunctions.S with type astate = A.astate and type node_id = CFG.id) = struct
+type 'a state = { pre: 'a; post: 'a; visit_count: int; }
 
-  module S = Sched (CFG)
-  module M = ProcCfg.NodeIdMap (CFG)
+module type S = sig
+  module TF : TransferFunctions.S
+  module M : Map.S with type key = TF.CFG.id
+  type inv_map = TF.Domain.astate state M.t
+
+  val exec_pdesc : TF.extras ProcData.t -> inv_map
+  val compute_post : TF.extras ProcData.t -> TF.Domain.astate option
+end
+
+module MakeNoCFG
+    (Sched : Scheduler.S) (TF : TransferFunctions.S with module CFG = Sched.CFG) = struct
+
+  module CFG = Sched.CFG
+  module M = ProcCfg.NodeIdMap (Sched.CFG)
+  module A = TF.Domain
 
-  type state = { pre: A.astate; post: A.astate; visit_count: int; }
   (* invariant map from node id -> abstract state representing postcondition for node id *)
-  type inv_map = state M.t
+  type inv_map = A.astate state M.t
 
   (** extract the state of node [n] from [inv_map] *)
   let extract_state node_id inv_map =
@@ -52,12 +60,17 @@ module Make
         let exec_instrs astate_acc instr =
           if A.is_bottom astate_acc
           then astate_acc
-          else T.exec_instr astate_acc proc_data instr in
-        let astate_post_instrs = IList.fold_left exec_instrs astate_pre (CFG.instrs node) in
-        T.postprocess astate_post_instrs node_id proc_data in
+          else TF.exec_instr astate_acc proc_data node instr in
+        (* hack to ensure that the transfer functions see every node *)
+        let node_instrs = match CFG.instrs node with
+          | [] ->
+              (* TODO: get rid of Stackop and replace it with Skip *)
+              [Sil.Stackop (Push, Location.dummy)]
+          | instrs -> instrs in
+        IList.fold_left exec_instrs astate_pre node_instrs in
       L.out "Post for node %a is %a@." CFG.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
+      inv_map', Sched.schedule_succs work_queue node in
     if M.mem node_id inv_map then
       let old_state = M.find node_id inv_map in
       let widened_pre =
@@ -90,7 +103,7 @@ module Make
       match IList.flatten_options all_posts with
       | post :: posts -> Some (IList.fold_left A.join post posts)
       | [] -> None in
-    match S.pop work_queue with
+    match Sched.pop work_queue with
     | Some (_, [], work_queue') ->
         exec_worklist cfg work_queue' inv_map proc_data
     | Some (node, _, work_queue') ->
@@ -104,7 +117,8 @@ module Make
   (* compute and return an invariant map for [cfg] *)
   let exec_cfg cfg proc_data =
     let start_node = CFG.start_node cfg in
-    let inv_map', work_queue' = exec_node start_node A.initial (S.empty cfg) M.empty proc_data in
+    let inv_map', work_queue' =
+      exec_node start_node A.initial (Sched.empty cfg) M.empty proc_data in
     exec_worklist cfg work_queue' inv_map' proc_data
 
   (* compute and return an invariant map for [pdesc] *)
@@ -145,3 +159,5 @@ module Make
   end
 end
 
+module Make (C : ProcCfg.S) (S : Scheduler.Make) (T : TransferFunctions.Make) =
+  MakeNoCFG (S (C)) (T (C))

infer/src/checkers/addressTaken.ml

@@ -17,12 +17,10 @@ module PvarSet = PrettyPrintable.MakePPSet(struct
 
 module Domain = AbstractDomain.FiniteSet(PvarSet)
 
-module TransferFunctions = struct
-  type astate = Domain.astate
+module TransferFunctions (CFG : ProcCfg.S) = struct
+  module CFG = CFG
+  module Domain = Domain
   type extras = ProcData.no_extras
-  type node_id = ProcCfg.DefaultNode.id
-
-  let postprocess = TransferFunctions.no_postprocessing
 
   let rec add_address_taken_pvars exp astate = match exp with
     | Sil.Lvar pvar ->
@@ -37,7 +35,7 @@ module TransferFunctions = struct
     | Var _ | Sizeof _ ->
         astate
 
-  let exec_instr astate _ = function
+  let exec_instr astate _ _ = function
     | Sil.Set (_, Tptr _, rhs_exp, _) ->
         add_address_taken_pvars rhs_exp astate
     | Sil.Call (_, _, actuals, _, _) ->
@@ -48,9 +46,8 @@ module TransferFunctions = struct
     | Sil.Set _ | Letderef _ | Prune _ | Nullify _ | Abstract _ | Remove_temps _ | Stackop _
     | Declare_locals _ ->
         astate
-
 end
 
 module Analyzer =
   AbstractInterpreter.Make
-    (ProcCfg.Exceptional) (Scheduler.ReversePostorder) (Domain) (TransferFunctions)
+    (ProcCfg.Exceptional) (Scheduler.ReversePostorder) (TransferFunctions)

infer/src/checkers/annotationReachability.ml

@@ -268,12 +268,10 @@ let report_call_stack end_of_stack lookup_next_calls report pname loc calls =
        loop fst_call_loc Procname.Set.empty (start_trace, "") (fst_callee_pname, fst_call_loc))
     calls
 
-module TransferFunctions = struct
-  type astate = Domain.astate
+module TransferFunctions (CFG : ProcCfg.S) = struct
+  module CFG = CFG
+  module Domain = Domain
   type extras = ProcData.no_extras
-  type node_id = ProcCfg.DefaultNode.id
-
-  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
@@ -327,7 +325,7 @@ module TransferFunctions = struct
            with T *)
         Sil.AnnotMap.fold add_call_for_annot map astate
 
-  let exec_instr astate { ProcData.pdesc; tenv; } = function
+  let exec_instr astate { ProcData.pdesc; tenv; } _ = function
     | Sil.Call ([id], Const (Cfun callee_pname), _, _, _)
       when is_unlikely callee_pname ->
         Domain.add_tracking_var (Var.of_id id) astate
@@ -365,7 +363,6 @@ module Analyzer =
   AbstractInterpreter.Make
     (ProcCfg.Exceptional)
     (Scheduler.ReversePostorder)
-    (Domain)
     (TransferFunctions)
 
 module Interprocedural = struct

infer/src/checkers/copyPropagation.ml

@@ -79,14 +79,12 @@ module Domain = struct
       |> gen lhs_var rhs_var
 end
 
-module TransferFunctions = struct
-  type astate = Domain.astate
+module TransferFunctions (CFG : ProcCfg.S) = struct
+  module CFG = CFG
+  module Domain = Domain
   type extras = ProcData.no_extras
-  type node_id = Cfg.Node.id
 
-  let postprocess = TransferFunctions.no_postprocessing
-
-  let exec_instr astate _ = function
+  let exec_instr astate _ _ = function
     | Sil.Letderef (lhs_id, Sil.Lvar rhs_pvar, _, _) when not (Pvar.is_global rhs_pvar) ->
         Domain.gen (Var.of_id lhs_id) (Var.of_pvar rhs_pvar) astate
     | Sil.Set (Sil.Lvar lhs_pvar, _, Sil.Var rhs_id, _) when not (Pvar.is_global lhs_pvar) ->
@@ -123,7 +121,6 @@ module Analyzer =
   AbstractInterpreter.Make
     (ProcCfg.Exceptional)
     (Scheduler.ReversePostorder)
-    (Domain)
     (TransferFunctions)
 
 let checker { Callbacks.proc_desc; tenv; } =

infer/src/checkers/liveness.ml

@@ -18,12 +18,10 @@ module Domain = AbstractDomain.FiniteSet(Var.Set)
 
 (* compilers 101-style backward transfer functions for liveness analysis. gen a variable when it is
    read, kill the variable when it is assigned *)
-module TransferFunctions = struct
-  type astate = Domain.astate
+module TransferFunctions (CFG : ProcCfg.S) = struct
+  module CFG = CFG
+  module Domain = Domain
   type extras = ProcData.no_extras
-  type node_id = Cfg.Node.id
-
-  let postprocess = TransferFunctions.no_postprocessing
 
   (* add all of the vars read in [exp] to the live set *)
   let exp_add_live exp astate =
@@ -32,7 +30,7 @@ module TransferFunctions = struct
       IList.fold_left (fun astate_acc id -> Domain.add (Var.of_id id) astate_acc) astate ids in
     IList.fold_left (fun astate_acc pvar -> Domain.add (Var.of_pvar pvar) astate_acc) astate' pvars
 
-  let exec_instr astate _ = function
+  let exec_instr astate _ _ = function
     | Sil.Letderef (lhs_id, rhs_exp, _, _) ->
         Domain.remove (Var.of_id lhs_id) astate
         |> exp_add_live rhs_exp
@@ -62,7 +60,6 @@ module Analyzer =
   AbstractInterpreter.Make
     (ProcCfg.Backward(ProcCfg.Exceptional))
     (Scheduler.ReversePostorder)
-    (Domain)
     (TransferFunctions)
 
 let checker { Callbacks.proc_desc; tenv; } =

infer/src/checkers/scheduler.ml

@@ -12,7 +12,8 @@ open! Utils
 module F = Format
 module L = Logging
 
-module type S = functor (CFG : ProcCfg.S) -> sig
+module type S = sig
+  module CFG : ProcCfg.S
   type t
 
   (* schedule the successors of [node] *)
@@ -21,12 +22,16 @@ module type S = functor (CFG : ProcCfg.S) -> sig
      predecessors, and the new schedule *)
   val pop : t -> (CFG.node * CFG.id list * t) option
   val empty : CFG.t -> t
+end
 
+module type Make = functor (CFG : ProcCfg.S) -> sig
+  include (S with module CFG = CFG)
 end
 
 (* simple scheduler that visits CFG nodes in reverse postorder. fast/precise for straightline code
    and conditionals; not as good for loops (may visit nodes after a loop multiple times). *)
-module ReversePostorder : S = functor (CFG : ProcCfg.S) -> struct
+module ReversePostorder (CFG : ProcCfg.S) = struct
+  module CFG = CFG
   module M = ProcCfg.NodeIdMap (CFG)
 
   module WorkUnit = struct

infer/src/checkers/transferFunctions.ml

@@ -9,17 +9,18 @@
 
 open! Utils
 
+(** Transfer functions that push abstract states across instructions. A typical client should
+    implement the Make signature to allow the transfer functions to be used with any kind of CFG. *)
+
 module type S = sig
-  type astate (* abstract state to propagate *)
+  module CFG : ProcCfg.S
+  module Domain : AbstractDomain.S (* abstract domain whose state we propagate *)
   type extras (* read-only extra state (results of previous analyses, globals, etc.) *)
-  type node_id
-
-  (* {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 -> node_id -> extras ProcData.t -> astate
+  (* {A} instr {A'}. [node] is the node of the current instruction *)
+  val exec_instr : Domain.astate -> extras ProcData.t -> CFG.node -> Sil.instr -> Domain.astate
 end
 
-(* default postprocessing: do nothing *)
-let no_postprocessing astate _ _ = astate
+module type Make = functor (C : ProcCfg.S) -> sig
+  include (S with module CFG = C)
+end

infer/src/checkers/transferFunctions.mli

@@ -0,0 +1,24 @@
+(*
+ * Copyright (c) 2016 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+(** Transfer functions that push abstract states across instructions. A typical client should
+    implement the Make signature to allow the transfer functions to be used with any kind of CFG. *)
+
+module type S = sig
+  module CFG : ProcCfg.S
+  module Domain : AbstractDomain.S (* abstract domain whose state we propagate *)
+  type extras (* read-only extra state (results of previous analyses, globals, etc.) *)
+
+  (* {A} instr {A'}. [node] is the node of the current instruction *)
+  val exec_instr : Domain.astate -> extras ProcData.t -> CFG.node -> Sil.instr -> Domain.astate
+end
+
+module type Make = functor (C : ProcCfg.S) -> sig
+  include (S with module CFG = C)
+end

infer/src/unit/abstractInterpreterTests.ml

@@ -48,28 +48,24 @@ module PathCountDomain = struct
 
 end
 
-module PathCountTransferFunctions = struct
-  type astate = PathCountDomain.astate
+module PathCountTransferFunctions (CFG : ProcCfg.S) = struct
+  module CFG = CFG
+  module Domain = PathCountDomain
   type extras = ProcData.no_extras
-  type node_id = Cfg.Node.id
-
-  let postprocess = TransferFunctions.no_postprocessing
 
   (* just propagate the current path count *)
-  let exec_instr astate _ _ = astate
+  let exec_instr astate _ _ _ = astate
 end
 
 
 module NormalTestInterpreter = AnalyzerTester.Make
     (ProcCfg.Normal)
     (Scheduler.ReversePostorder)
-    (PathCountDomain)
     (PathCountTransferFunctions)
 
 module ExceptionalTestInterpreter = AnalyzerTester.Make
     (ProcCfg.Exceptional)
     (Scheduler.ReversePostorder)
-    (PathCountDomain)
     (PathCountTransferFunctions)
 
 let tests =
@@ -186,7 +182,7 @@ let tests =
       );
       invariant "1"
     ];
-  ] |> NormalTestInterpreter.create_tests in
+  ] |> NormalTestInterpreter.create_tests ProcData.empty_extras in
   let exceptional_test_list = [
     "try1",
     [
@@ -222,5 +218,5 @@ let tests =
       );
       invariant "3"
     ];
-  ] |> ExceptionalTestInterpreter.create_tests in
+  ] |> ExceptionalTestInterpreter.create_tests ProcData.empty_extras in
   "analyzer_tests_suite">:::(normal_test_list @ exceptional_test_list)

infer/src/unit/addressTakenTests.ml

@@ -14,7 +14,6 @@ module F = Format
 module TestInterpreter = AnalyzerTester.Make
     (ProcCfg.Exceptional)
     (Scheduler.ReversePostorder)
-    (AddressTaken.Domain)
     (AddressTaken.TransferFunctions)
 
 let tests =
@@ -99,5 +98,5 @@ let tests =
       var_assign_var ~rhs_typ:int_ptr_typ "e" "f";
       invariant "{ &b, &d, &f }"
     ];
-  ] |> TestInterpreter.create_tests in
+  ] |> TestInterpreter.create_tests ProcData.empty_extras in
   "address_taken_suite">:::test_list

infer/src/unit/analyzerTester.ml

@@ -139,16 +139,13 @@ end
 
 module Make
     (CFG : ProcCfg.S with type node = Cfg.Node.t)
-    (S : Scheduler.S)
-    (A : AbstractDomain.S)
-    (T : TransferFunctions.S
-     with type astate = A.astate and type extras = ProcData.no_extras
-                                 and type node_id = CFG.id) = struct
+    (S : Scheduler.Make)
+    (T : TransferFunctions.Make) = struct
 
   open StructuredSil
 
-  module I = AbstractInterpreter.Make (CFG) (S) (A) (T)
-  module M = ProcCfg.NodeIdMap (CFG)
+  module I = AbstractInterpreter.Make (CFG) (S) (T)
+  module M = I.M
 
   type assert_map = string M.t
 
@@ -229,15 +226,15 @@ module Make
     Cfg.Procdesc.set_exit_node pdesc exit_node;
     pdesc, assert_map
 
-  let create_test test_program _ =
+  let create_test test_program extras _ =
     let pdesc, assert_map = structured_program_to_cfg test_program in
-    let inv_map = I.exec_pdesc (ProcData.make_default pdesc (Tenv.create ())) in
+    let inv_map = I.exec_pdesc (ProcData.make pdesc (Tenv.create ()) extras) 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
-          pp_to_string A.pp state.post
+          pp_to_string I.A.pp state.post
         with Not_found -> "_|_" in
       if inv_str <> post_str then
         let error_msg =
@@ -262,8 +259,8 @@ module Make
           |> F.flush_str_formatter in
         OUnit2.assert_failure assert_fail_message
 
-  let create_tests tests =
+  let create_tests extras tests =
     let open OUnit2 in
-    IList.map (fun (name, test_program) -> name>::create_test test_program) tests
+    IList.map (fun (name, test_program) -> name>::create_test test_program extras) tests
 
 end

infer/src/unit/copyPropagationTests.ml

@@ -14,7 +14,6 @@ module F = Format
 module TestInterpreter = AnalyzerTester.Make
     (ProcCfg.Exceptional)
     (Scheduler.ReversePostorder)
-    (CopyPropagation.Domain)
     (CopyPropagation.TransferFunctions)
 
 let tests =
@@ -192,5 +191,5 @@ let tests =
       var_assign_var "c" "b";
       invariant "{ &b -> &a, &c -> &b }"
     ];
-  ] |> TestInterpreter.create_tests in
+  ] |> TestInterpreter.create_tests ProcData.empty_extras in
   "copy_propagation_test_suite">:::test_list

infer/src/unit/livenessTests.ml

@@ -14,7 +14,6 @@ module F = Format
 module TestInterpreter = AnalyzerTester.Make
     (ProcCfg.Backward(ProcCfg.Normal))
     (Scheduler.ReversePostorder)
-    (Liveness.Domain)
     (Liveness.TransferFunctions)
 
 let tests =
@@ -192,5 +191,5 @@ let tests =
       invariant "{ &b }";
       var_assign_var "a" "b"
     ];
-  ] |> TestInterpreter.create_tests in
+  ] |> TestInterpreter.create_tests ProcData.empty_extras in
   "liveness_test_suite">:::test_list