From 8913e38dbd6e45ee6c4bdad0e9192dad0caa202a Mon Sep 17 00:00:00 2001
From: Sam Blackshear <shb@fb.com>
Date: Tue, 15 Mar 2016 10:02:35 -0700
Subject: [PATCH] getting rid of bottom

Differential Revision: D3042821

fb-gh-sync-id: 838d948
shipit-source-id: 838d948
---
 infer/src/checkers/abstractDomain.ml       |  3 ---
 infer/src/checkers/abstractInterpreter.ml  | 27 +++++++++++-----------
 infer/src/unit/abstractInterpreterTests.ml |  6 +----
 infer/src/unit/analyzerTester.ml           |  7 +++---
 4 files changed, 17 insertions(+), 26 deletions(-)

diff --git a/infer/src/checkers/abstractDomain.ml b/infer/src/checkers/abstractDomain.ml
index 19b97dafd..338f92aac 100644
--- a/infer/src/checkers/abstractDomain.ml
+++ b/infer/src/checkers/abstractDomain.ml
@@ -13,7 +13,6 @@ module type AbstractDomain = sig
   type astate
 
   val initial : astate
-  val bottom : astate
   val is_bottom : astate -> bool
   val (<=) : lhs:astate -> rhs:astate -> bool (* fst \sqsubseteq snd? *)
   val join : astate -> astate -> astate
@@ -27,8 +26,6 @@ module BottomLiftedAbstractDomain (A : AbstractDomain) : AbstractDomain = struct
     | Bottom
     | NonBottom of A.astate
 
-  let bottom = Bottom
-
   let is_bottom astate =
     astate = Bottom
 
diff --git a/infer/src/checkers/abstractInterpreter.ml b/infer/src/checkers/abstractInterpreter.ml
index 5335d7a69..a221718b3 100644
--- a/infer/src/checkers/abstractInterpreter.ml
+++ b/infer/src/checkers/abstractInterpreter.ml
@@ -26,11 +26,15 @@ module Make
   type inv_map = state M.t
 
   let exec_node node astate_pre work_queue inv_map =
+    let exec_instrs astate_acc instr =
+      if A.is_bottom astate_acc
+      then astate_acc
+      else T.exec_instr astate_acc instr in
     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
+      IList.fold_left exec_instrs 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
@@ -60,12 +64,15 @@ module Make
 
   let rec exec_worklist work_queue inv_map =
     match S.pop work_queue with
-    | Some (node, visited_preds, work_queue') ->
+    | Some (_, [], work_queue') ->
+        exec_worklist work_queue' inv_map
+    | Some (node, visited_pred :: visited_preds, work_queue') ->
+        let get_post pred_id =
+          (M.find pred_id inv_map).post in
         (* 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.bottom visited_preds in
+        let join_pred_posts astate_acc pred_id =
+          A.join (get_post pred_id) astate_acc in
+        let astate_pre = IList.fold_left join_pred_posts (get_post visited_pred) 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
@@ -76,13 +83,5 @@ module Make
     let start_node = C.start_node cfg in
     let inv_map', work_queue' = exec_node start_node A.initial (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
diff --git a/infer/src/unit/abstractInterpreterTests.ml b/infer/src/unit/abstractInterpreterTests.ml
index 3bccb30ab..bc7ed5bf5 100644
--- a/infer/src/unit/abstractInterpreterTests.ml
+++ b/infer/src/unit/abstractInterpreterTests.ml
@@ -25,13 +25,9 @@ module PathCountDomain = struct
     then Top
     else PathCount c
 
-  let bottom = make_path_count 0
-
   let initial = make_path_count 1
 
-  let is_bottom = function
-    | PathCount c -> c = 0
-    | Top -> false
+  let is_bottom _ = false
 
   let (<=) ~lhs ~rhs = match lhs, rhs with
     | PathCount c1, PathCount c2 -> c1 <= c2
diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml
index 183133468..13cf8bbf8 100644
--- a/infer/src/unit/analyzerTester.ml
+++ b/infer/src/unit/analyzerTester.ml
@@ -153,12 +153,11 @@ module Make
     let inv_map = I.exec_pdesc pdesc in
 
     let collect_invariant_mismatches node_id (inv_str, inv_label) error_msgs_acc =
-      let node_id_post =
+      let post_str =
         try
           let state = M.find node_id inv_map in
-          state.post
-        with Not_found -> A.bottom in
-      let post_str = pp_to_string A.pp node_id_post in
+          pp_to_string A.pp state.post
+        with Not_found -> "_|_" in
       if inv_str <> post_str then
         let error_msg =
           F.fprintf F.str_formatter