[absint] fix handling of exceptions

Summary:
The abstract interpreter tried to handle exceptional control-flow by propagating the *pre* of a block that threw an exception rather than the *post*.
This was a half-measure that isn't correct when an exception-throwing instruction isn't in the middle of a block.
The handling of exceptions wasn't actually used anywhere and was leading to further hacks in `ProcCfg`, so let's get rid of it.

Reviewed By: mbouaziz, jvillard

Differential Revision: D7843872

fbshipit-source-id: 2a4a815

infer/src/absint/AbstractInterpreter.ml

@@ -103,14 +103,8 @@ struct
 
   let rec exec_worklist cfg work_queue inv_map proc_data ~debug =
     let compute_pre node inv_map =
-      (* if the [pred] -> [node] transition was normal, use post([pred]) *)
       let extract_post_ pred = extract_post (CFG.id pred) inv_map in
-      let normal_posts = List.map ~f:extract_post_ (CFG.normal_preds cfg node) in
-      (* if the [pred] -> [node] transition was exceptional, use pre([pred]) *)
-      let extract_pre_f acc pred = extract_pre (CFG.id pred) inv_map :: acc in
-      let all_posts =
-        List.fold ~f:extract_pre_f ~init:normal_posts (CFG.exceptional_preds cfg node)
-      in
+      let all_posts = List.map ~f:extract_post_ (CFG.preds cfg node) in
       match List.filter_opt all_posts with
       | post :: posts ->
           Some (List.fold ~f:Domain.join ~init:post posts)

infer/src/absint/ProcCfg.ml

@@ -322,9 +322,8 @@ struct
     else List.map ~f:last_of_node (Base.normal_preds cfg node)
 
 
-  (* HACK: Use first_of_node instead of last_of_node because it is used to get the pre only *)
   let exceptional_preds cfg (node, index) =
-    if index >= 1 then [] else List.map ~f:first_of_node (Base.exceptional_preds cfg node)
+    if index >= 1 then [] else List.map ~f:last_of_node (Base.exceptional_preds cfg node)
 
 
   let preds cfg t = List.rev_append (exceptional_preds cfg t) (normal_preds cfg t)

infer/tests/codetoanalyze/java/quandary/Interprocedural.java

@@ -320,9 +320,7 @@ class Interprocedural {
     for (;;);
   }
 
-  // this fails because the exit block in callSinkThenDiverge is unreachable, so the summary is
-  // empty.
-  public void FN_callSinkThenDivergeBad() {
+  public void callSinkThenDivergeBad() {
     callSinkThenDiverge(InferTaint.inferSecretSource());
   }
 

infer/tests/codetoanalyze/java/quandary/issues.exp

@@ -121,6 +121,7 @@ codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.callSinkO
 codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.callSinkOnLocalBad(), 2, QUANDARY_TAINT_ERROR, ERROR, [Return from Object InferTaint.inferSecretSource(),Call to void Interprocedural.callSinkOnLocal() with tainted index 0,Call to void InferTaint.inferSensitiveSink(Object) with tainted index 0]
 codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.callSinkParam1Bad(), 1, QUANDARY_TAINT_ERROR, ERROR, [Return from Object InferTaint.inferSecretSource(),Call to void Interprocedural.callSinkParam1(Object,Object) with tainted index 0,Call to void InferTaint.inferSensitiveSink(Object) with tainted index 0]
 codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.callSinkParam2Bad(), 1, QUANDARY_TAINT_ERROR, ERROR, [Return from Object InferTaint.inferSecretSource(),Call to void Interprocedural.callSinkParam2(Object,Object) with tainted index 0,Call to void InferTaint.inferSensitiveSink(Object) with tainted index 0]
+codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.callSinkThenDivergeBad(), 1, QUANDARY_TAINT_ERROR, ERROR, [Return from Object InferTaint.inferSecretSource(),Call to void Interprocedural.callSinkThenDiverge(Object) with tainted index 0,Call to void InferTaint.inferSensitiveSink(Object) with tainted index 0]
 codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.callSinkVariadicBad(), 1, QUANDARY_TAINT_ERROR, ERROR, [Return from Object InferTaint.inferSecretSource(),Call to void Interprocedural.callSinkVariadic(java.lang.Object[]) with tainted index 0,Call to void InferTaint.inferSensitiveSink(Object) with tainted index 0]
 codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.doublePassthroughBad(), 4, QUANDARY_TAINT_ERROR, ERROR, [Return from Object InferTaint.inferSecretSource(),Call to void InferTaint.inferSensitiveSink(Object) with tainted index 0]
 codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.getGlobalThenCallSinkBad(), 2, QUANDARY_TAINT_ERROR, ERROR, [Return from Object InferTaint.inferSecretSource(),Call to void Interprocedural.getGlobalThenCallSink() with tainted index 0,Call to void InferTaint.inferSensitiveSink(Object) with tainted index 0]