From bb2ff197b340feccbd0e6daf34ec477793e75e7b Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Wed, 2 May 2018 07:11:36 -0700 Subject: [PATCH] [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 | 8 +------- infer/src/absint/ProcCfg.ml | 3 +-- .../codetoanalyze/java/quandary/Interprocedural.java | 4 +--- infer/tests/codetoanalyze/java/quandary/issues.exp | 1 + 4 files changed, 4 insertions(+), 12 deletions(-) diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index da61d4be8..db7d1ed85 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/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) diff --git a/infer/src/absint/ProcCfg.ml b/infer/src/absint/ProcCfg.ml index 0bf5ca08b..be7919542 100644 --- a/infer/src/absint/ProcCfg.ml +++ b/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) diff --git a/infer/tests/codetoanalyze/java/quandary/Interprocedural.java b/infer/tests/codetoanalyze/java/quandary/Interprocedural.java index d6237edc5..8a7d68574 100644 --- a/infer/tests/codetoanalyze/java/quandary/Interprocedural.java +++ b/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()); } diff --git a/infer/tests/codetoanalyze/java/quandary/issues.exp b/infer/tests/codetoanalyze/java/quandary/issues.exp index 0e624d348..9bff4fde8 100644 --- a/infer/tests/codetoanalyze/java/quandary/issues.exp +++ b/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]