adding generic abstract interpreter

Reviewed By: dkgi

Differential Revision: D2997068

fb-gh-sync-id: 265c0b9
shipit-source-id: 265c0b9

infer/src/checkers/abstractDomain.ml

@@ -15,14 +15,14 @@ module type AbstractDomain = sig
   val init : astate (* the initial state *)
   val bot : astate
   val is_bot : astate -> bool
-  val lteq : astate -> astate -> bool (* fst \sqsubseteq snd? *)
+  val lteq : lhs:astate -> rhs:astate -> bool (* fst \sqsubseteq snd? *)
   val join : astate -> astate -> astate
-  val widen : astate -> astate -> astate
+  val widen : prev:astate -> next:astate -> num_iters:int -> astate
   val pp : F.formatter -> astate -> unit
 
 end
 
-module BotLiftedAbstractDomain (A : AbstractDomain) = struct
+module BotLiftedAbstractDomain (A : AbstractDomain) : AbstractDomain = struct
   type astate =
     | Bot
     | NonBot of A.astate
@@ -34,10 +34,10 @@ module BotLiftedAbstractDomain (A : AbstractDomain) = struct
 
   let init = NonBot A.init
 
-  let lteq astate1 astate2 = match astate1, astate2 with
+  let lteq ~lhs ~rhs = match lhs, rhs with
     | Bot, _ -> true
     | _ , Bot -> false
-    | NonBot a1, NonBot a2 -> A.lteq a1 a2
+    | NonBot lhs, NonBot rhs -> A.lteq ~lhs ~rhs
 
   let join astate1 astate2 =
     match astate1, astate2 with
@@ -45,11 +45,11 @@ module BotLiftedAbstractDomain (A : AbstractDomain) = struct
     | _, Bot -> astate1
     | NonBot a1, NonBot a2 -> NonBot (A.join a1 a2)
 
-  let widen astate1 astate2 =
-    match astate1, astate2 with
-    | Bot, _ -> astate2
-    | _, Bot -> astate1
-    | NonBot a1, NonBot a2 -> NonBot (A.widen a1 a2)
+  let widen ~prev ~next ~num_iters =
+    match prev, next with
+    | Bot, _ -> next
+    | _, Bot -> prev
+    | NonBot prev, NonBot next -> NonBot (A.widen ~prev ~next ~num_iters)
 
   let pp fmt = function
     | Bot -> F.fprintf fmt "_|_"

infer/src/checkers/abstractInterpreter.ml

@@ -0,0 +1,88 @@
+(*
+ * 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.
+ *)
+
+module L = Logging
+
+open AbstractDomain
+open TransferFunctions
+
+module Make
+    (C : ProcCfg.Wrapper)
+    (Sched : Scheduler.S)
+    (A : AbstractDomain)
+    (T : TransferFunctions with type astate = A.astate) = struct
+
+  module S = Sched (C)
+  module M = ProcCfg.NodeIdMap (C)
+
+  type state = { post: A.astate; visit_count: int; }
+  (* invariant map from node id -> abstract state representing postcondition for node id *)
+  type inv_map = state M.t
+
+  let exec_node node astate_pre work_queue inv_map =
+    let node_id = C.node_id node in
+    L.out "Doing analysis of node %a from pre %a@." C.pp_node_id node_id A.pp astate_pre;
+    let instrs = C.instrs node in
+    let astate_post =
+      IList.fold_left (fun astate_acc instr -> T.exec_instr astate_acc instr) astate_pre instrs in
+    L.out "Post for node %a is %a@." C.pp_node_id node_id A.pp astate_post;
+    if M.mem node_id inv_map then
+      let old_state = M.find node_id inv_map in
+      let widened_post =
+        A.widen ~prev:old_state.post ~next:astate_post ~num_iters:old_state.visit_count in
+      if A.lteq ~lhs:widened_post ~rhs:old_state.post
+      then
+        begin
+          L.out "Old state contains new, not adding succs@.";
+          inv_map, work_queue
+        end
+      else
+        begin
+          L.out "Widening: %a <widen> %a = %a@."
+            A.pp astate_post A.pp old_state.post A.pp widened_post;
+          let inv_map' =
+            let visit_count = old_state.visit_count + 1 in
+            M.add node_id { post=widened_post; visit_count; } inv_map in
+          inv_map', S.schedule_succs work_queue node
+        end
+    else
+      (* first time visiting this node *)
+      let inv_map' =
+        let visit_count = 0 in
+        M.add node_id { post=astate_post; visit_count; } inv_map in
+      inv_map', S.schedule_succs work_queue node
+
+  let rec exec_worklist work_queue inv_map =
+    match S.pop work_queue with
+    | Some (node, visited_preds, work_queue') ->
+        (* compute the precondition for node by joining post of all visited preds *)
+        let join_pred astate_acc pred_id =
+          let pred_state = M.find pred_id inv_map in
+          A.join pred_state.post astate_acc in
+        let astate_pre = IList.fold_left join_pred A.bot visited_preds in
+        let inv_map', work_queue'' = exec_node node astate_pre work_queue' inv_map in
+        exec_worklist work_queue'' inv_map'
+    | None -> inv_map
+
+  let exec_pdesc pdesc =
+    L.out "Starting analysis of %a@." Procname.pp (Cfg.Procdesc.get_proc_name pdesc);
+    let cfg = C.from_pdesc pdesc in
+    let start_node = C.start_node cfg in
+    let inv_map', work_queue' = exec_node start_node A.init (S.empty cfg) M.empty in
+    exec_worklist work_queue' inv_map'
+
+end
+
+module UnitTests = struct
+
+  let tests =
+    let open OUnit2 in
+    "abstract_interpreter_suite">:::[]
+
+end

infer/src/checkers/scheduler.ml

@@ -17,18 +17,15 @@ module type S = functor (C : ProcCfg.Base) -> sig
   val schedule_succs : t -> C.node -> t
   (* remove and return the node with the highest priority, the ids of its visited
      predecessors, and the new schedule *)
-  val pop : t -> C.node * C.node_id list * t
+  val pop : t -> (C.node * C.node_id list * t) option
   val empty : C.t -> t
 
-  exception Empty
-
 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 (C : ProcCfg.Base) -> struct
   module M = ProcCfg.NodeIdMap (C)
-  exception Empty
 
   module WorkUnit = struct
     module IdSet = ProcCfg.NodeIdSet(C)
@@ -82,10 +79,10 @@ module ReversePostorder : S = functor (C : ProcCfg.Base) -> struct
   (* TODO: could do this slightly more efficiently by keeping a list of priority zero nodes for
      quick popping, and do a linear search only when this list is empty *)
   let pop t =
-    let max_priority_id, _ =
     try
       let init_id, init_work = M.choose t.worklist in
       let init_priority = WorkUnit.priority init_work in
+      let max_priority_id, _ =
         M.fold
           (fun id work (lowest_id, lowest_priority) ->
              let priority = WorkUnit.priority work in
@@ -93,12 +90,12 @@ module ReversePostorder : S = functor (C : ProcCfg.Base) -> struct
              then id, priority
              else lowest_id, lowest_priority)
           t.worklist
-          (init_id, init_priority)
-      with Not_found -> raise Empty in
+          (init_id, init_priority) in
       let max_priority_work = M.find max_priority_id t.worklist in
       let node = WorkUnit.node max_priority_work in
       let t' = { t with worklist = M.remove (C.node_id node) t.worklist } in
-    node, WorkUnit.visited_preds max_priority_work, t'
+      Some (node, WorkUnit.visited_preds max_priority_work, t')
+    with Not_found -> None
 
   let empty cfg = { worklist = M.empty; cfg; }
 

infer/src/unit/inferunit.ml

@@ -9,10 +9,11 @@
 
 (** module for running OCaml unit tests *)
 
-module L = Logging
-
 let () =
   let open OUnit2 in
-  let tests = [SchedulerTests.tests] in
+  let tests = [
+    SchedulerTests.tests;
+    AbstractInterpreter.UnitTests.tests;
+  ] in
   let test_suite = "all" >::: tests in
   OUnit2.run_test_tt_main test_suite

infer/src/unit/schedulerTests.ml

@@ -42,10 +42,10 @@ module S = Scheduler.ReversePostorder (MockProcCfg)
 let create_test test_graph expected_result _ =
   (* keep popping and scheduling until the queue is empty, record the results *)
   let rec pop_schedule_record q visited_acc =
-    try
-      let n, _, q' = S.pop q in
+    match S.pop q with
+    | Some (n, _, q') ->
         pop_schedule_record (S.schedule_succs q' n) (n :: visited_acc)
-    with S.Empty -> IList.rev visited_acc in
+    | None -> IList.rev visited_acc in
   let pp_diff fmt (exp, actual) =
     let pp_sched fmt l =
       F.pp_print_list ~pp_sep:F.pp_print_space (fun fmt i -> F.fprintf fmt "%d" i) fmt l in