setup for creating very simple absint checkers

Reviewed By: cristianoc

Differential Revision: D3734044

fbshipit-source-id: 014b0d9

infer/src/checkers/SimpleChecker.ml

@@ -0,0 +1,108 @@
+(*
+ * 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.
+ *)
+
+open! Utils
+
+module F = Format
+module L = Logging
+
+(** functor that makes it easy to write a basic abstract interpretation checker by lifting
+    a type, comparison function, reporting function, and exec function into an analyzer *)
+
+module type Spec = sig
+  type astate (** what state do you want to propagate? *)
+
+  (** implement the state the analysis should start from here *)
+  val initial : astate
+
+  (** implement how an instruction changes your state here.
+      input is the previous state, current instruction, current node kind, current procedure and
+      type environment.
+  *)
+  val exec_instr : astate -> Sil.instr -> Cfg.Node.nodekind -> Procname.t -> Tenv.t -> astate
+
+  (** log errors here.
+      input is a state, location where the state occurs in the source, and the current procedure.
+  *)
+  val report : astate -> Location.t -> Procname.t -> unit
+
+  val compare : astate -> astate -> int
+end
+
+module type S = sig
+  (** add YourChecker.checker to registerCallbacks.ml to run your checker *)
+  val checker : Callbacks.proc_callback_args -> unit
+end
+
+module Make (Spec : Spec) : S = struct
+
+  (* powerset domain over Spec.astate *)
+  module Domain = struct
+    include
+      AbstractDomain.FiniteSet
+        (PrettyPrintable.MakePPSet(
+          struct
+            type t = Spec.astate
+            let compare = Spec.compare
+            let pp_element _ _ = ()
+          end)
+        )
+
+    let initial = singleton Spec.initial
+
+    let widen ~prev ~next ~num_iters =
+      let iters_befor_timeout = 1000 in
+      (* failsafe for accidental non-finite height domains *)
+      if num_iters >= iters_befor_timeout
+      then
+        failwith
+          ("Stopping analysis after 1000 iterations without convergence." ^
+           "Make sure your domain is finite height.")
+      else widen ~prev ~next ~num_iters
+  end
+
+  module TransferFunctions (CFG : ProcCfg.S) = struct
+    module CFG = CFG
+    module Domain = Domain
+    type extras = ProcData.no_extras
+
+    let exec_instr astate_set proc_data node instr =
+      let node_kind = CFG.kind node in
+      let pname = Cfg.Procdesc.get_proc_name proc_data.ProcData.pdesc in
+      Domain.fold
+        (fun astate acc ->
+           Domain.add (Spec.exec_instr astate instr node_kind pname proc_data.ProcData.tenv) acc)
+        astate_set
+        Domain.empty
+  end
+
+  module Analyzer =
+    AbstractInterpreter.Make
+      (ProcCfg.Exceptional)
+      (Scheduler.ReversePostorder)
+      (TransferFunctions)
+
+  let checker { Callbacks.proc_desc; proc_name; tenv; } =
+    let nodes = Cfg.Procdesc.get_nodes proc_desc in
+    let do_reporting node_id state =
+      let astate_set = state.AbstractInterpreter.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 =
+          IList.find
+            (fun node -> Cfg.Node.id_compare node_id (Cfg.Node.get_id node) = 0)
+            nodes in
+        Domain.iter
+          (fun astate ->
+             Spec.report astate (ProcCfg.Exceptional.loc node) proc_name)
+          astate_set in
+    let inv_map = Analyzer.exec_pdesc (ProcData.make_default proc_desc tenv) in
+    Analyzer.M.iter do_reporting inv_map
+end

infer/src/checkers/procCfg.ml

@@ -23,6 +23,7 @@ module type Node = sig
 
   val kind : t -> Cfg.Node.nodekind
   val id : t -> id
+  val loc : t -> Location.t
   val underlying_id : t -> Cfg.Node.id
   val id_compare : id -> id -> int
   val pp_id : F.formatter -> id -> unit
@@ -34,6 +35,7 @@ module DefaultNode = struct
 
   let kind = Cfg.Node.get_kind
   let id = Cfg.Node.get_id
+  let loc = Cfg.Node.get_loc
   let underlying_id = id
   let id_compare = Cfg.Node.id_compare
   let pp_id = Cfg.Node.pp_id
@@ -49,6 +51,8 @@ module InstrNode = struct
 
   let id t = underlying_id t, Node_index
 
+  let loc t = Cfg.Node.get_loc t
+
   let index_compare index1 index2 = match index1, index2 with
     | Node_index, Node_index -> 0
     | Instr_index i1, Instr_index i2 -> int_compare i1 i2

infer/src/checkers/procCfg.mli

@@ -19,6 +19,7 @@ module type Node = sig
 
   val kind : t -> Cfg.Node.nodekind
   val id : t -> id
+  val loc : t -> Location.t
   val underlying_id : t -> Cfg.Node.id
   val id_compare : id -> id -> int
   val pp_id : Format.formatter -> id -> unit

infer/src/unit/schedulerTests.ml

@@ -22,6 +22,7 @@ module MockNode = struct
   let instr_ids _ = []
   let to_instr_nodes _ = assert false
   let id n = n
+  let loc _ = assert false
   let underlying_id _ = assert false
   let kind _ = Cfg.Node.Stmt_node ""
   let id_compare = int_compare