getting rid of bottom

Differential Revision: D3042821

fb-gh-sync-id: 838d948
shipit-source-id: 838d948

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
 

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 join_pred_posts astate_acc pred_id =
-          let pred_state = M.find pred_id inv_map in
+          A.join (get_post pred_id) astate_acc in
-          A.join pred_state.post astate_acc in
+        let astate_pre = IList.fold_left join_pred_posts (get_post visited_pred) visited_preds in
-        let astate_pre = IList.fold_left join_pred A.bottom 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

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
+  let is_bottom _ = false
-    | PathCount c -> c = 0
-    | Top -> false
 
   let (<=) ~lhs ~rhs = match lhs, rhs with
     | PathCount c1, PathCount c2 -> c1 <= c2

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
+          pp_to_string A.pp state.post
-        with Not_found -> A.bottom in
+        with Not_found -> "_|_" in
-      let post_str = pp_to_string A.pp node_id_post in
       if inv_str <> post_str then
         let error_msg =
           F.fprintf F.str_formatter