[quandary] using exceptional procCFG to explore exceptional control-flow

Reviewed By: dkgi

Differential Revision: D3871621

fbshipit-source-id: e76a274

infer/src/quandary/TaintAnalysis.ml

@@ -351,7 +351,7 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct
   end
 
   module Analyzer = AbstractInterpreter.Make
-      (ProcCfg.Normal)
+      (ProcCfg.Exceptional)
       (Scheduler.ReversePostorder)
       (TransferFunctions)
 

infer/tests/codetoanalyze/java/quandary/Exceptions.java

@@ -0,0 +1,120 @@
+/*
+ * 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.
+ */
+
+package codetoanalyze.java.quandary;
+
+import com.facebook.infer.models.InferTaint;
+
+class Exceptions {
+
+  native static void mayExcept() throws Exception;
+
+  public static void sinkInCatchBad1() {
+    Object source = InferTaint.inferSecretSource();
+    try {
+      mayExcept();
+    } catch (Exception e) {
+      InferTaint.inferSensitiveSink(source);
+    }
+  }
+
+  public static void sinkInCatchBad2() {
+    Object source = null;
+    try {
+      source = InferTaint.inferSecretSource();
+      mayExcept();
+    } catch (Exception e) {
+      InferTaint.inferSensitiveSink(source);
+    }
+  }
+
+  public static void sinkAfterCatchBad() {
+    Object source = InferTaint.inferSecretSource();
+    try {
+      mayExcept();
+      source = null;
+    } catch (Exception e) {
+    }
+    InferTaint.inferSensitiveSink(source);
+  }
+
+  public static void sinkAfterCatchOk() {
+    Object source = InferTaint.inferSecretSource();
+    try {
+      mayExcept();
+      source = null;
+    } catch (Exception e) {
+      source = null;
+    }
+    InferTaint.inferSensitiveSink(source);
+  }
+
+  public static void sinkInFinallyBad1() throws Exception{
+    Object source = InferTaint.inferSecretSource();
+    try {
+      mayExcept();
+    } finally {
+      InferTaint.inferSensitiveSink(source);
+    }
+  }
+
+  public static void sinkInFinallyBad2() throws Exception {
+    Object source = null;
+    try {
+      mayExcept();
+      source = InferTaint.inferSecretSource();
+    } finally {
+      InferTaint.inferSensitiveSink(source);
+    }
+  }
+
+  public static void sinkInFinallyBad3() {
+    Object source = null;
+    try {
+      mayExcept();
+    } catch (Exception e) {
+      source = InferTaint.inferSecretSource();
+    } finally {
+      InferTaint.inferSensitiveSink(source);
+    }
+  }
+
+  public static void sinkAfterFinallyOk1() throws Exception {
+    Object source = InferTaint.inferSecretSource();
+    try {
+      mayExcept();
+    } finally {
+      source = null;
+    }
+    InferTaint.inferSensitiveSink(source);
+  }
+
+  public static void sinkAfterFinallyOk2() {
+    Object source = null;
+    try {
+      mayExcept();
+      source = InferTaint.inferSecretSource();
+    } catch (Exception e) {
+      source = InferTaint.inferSecretSource();
+    } finally {
+      source = null;
+    }
+    InferTaint.inferSensitiveSink(source);
+  }
+
+  public static void callSinkThenThrow(Object param) throws Exception {
+    InferTaint.inferSensitiveSink(param);
+    throw new Exception();
+  }
+
+  public static void callSinkThenThrowBad() throws Exception {
+    callSinkThenThrow(InferTaint.inferSecretSource());
+  }
+
+}

infer/tests/codetoanalyze/java/quandary/Makefile

@@ -13,6 +13,7 @@ INFERPRINT_OPTIONS = --issues-txt
 FILES = \
   Arrays.java \
   Basics.java \
+  Exceptions.java \
   Fields.java \
   Interprocedural.java \
   LoggingPrivateData.java \

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

@@ -22,6 +22,13 @@ Basics.java:142: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.infe
 Basics.java:153: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 150]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 153]) via {  }
 Basics.java:196: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 193]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 196]) via {  }
 Basics.java:205: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 201]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 205]) via {  }
+Exceptions.java:23: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 19]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 23]) via {  }
+Exceptions.java:33: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 30]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 33]) via {  }
+Exceptions.java:44: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 38]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 44]) via {  }
+Exceptions.java:63: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 59]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 63]) via {  }
+Exceptions.java:73: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 71]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 73]) via {  }
+Exceptions.java:84: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 82]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 84]) via {  }
+Exceptions.java:117: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 117]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 112]) via { void Exceptions.callSinkThenThrow(Object) at [line 117] }
 Fields.java:28: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 27]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 28]) via {  }
 Fields.java:33: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 32]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 33]) via {  }
 Fields.java:38: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 37]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 38]) via {  }