Correct handling of exception edges in backward analysis

dataflow/src/main/java/org/checkerframework/dataflow/analysis/BackwardAnalysisImpl.java

@@ -4,6 +4,7 @@
 import java.util.List;
 import java.util.ListIterator;
 import java.util.Map;
+import java.util.Set;
 import org.checkerframework.checker.interning.qual.FindDistinct;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.checker.nullness.qual.RequiresNonNull;
@@ -253,25 +254,19 @@ protected void propagateStoresTo(
   protected void addStoreAfter(Block pred, @Nullable Node node, S s, boolean addBlockToWorklist) {
     // If the block pred is an exception block, decide whether the block of passing node is an
     // exceptional successor of the block pred
-    if (pred instanceof ExceptionBlock
-        && ((ExceptionBlock) pred).getSuccessor() != null
-        && node != null) {
-      @Nullable Block succBlock = ((ExceptionBlock) pred).getSuccessor();
-      @Nullable Block block = node.getBlock();
-      if (succBlock != null && block != null && succBlock.getUid() == block.getUid()) {
-        // If the block of passing node is an exceptional successor of Block pred, propagate
-        // store to the exceptionStores. Currently it doesn't track the label of an
-        // exceptional edge from exception block to its exceptional successors in backward
-        // direction. Instead, all exception stores of exceptional successors of an
-        // exception block will merge to one exception store at the exception block
-        ExceptionBlock ebPred = (ExceptionBlock) pred;
-        S exceptionStore = exceptionStores.get(ebPred);
-        S newExceptionStore = (exceptionStore != null) ? exceptionStore.leastUpperBound(s) : s;
-        if (!newExceptionStore.equals(exceptionStore)) {
-          exceptionStores.put(ebPred, newExceptionStore);
-          inputs.put(ebPred, new TransferInput<V, S>(node, this, newExceptionStore));
-          addBlockToWorklist = true;
-        }
+    if (isExceptionalSucc(pred, node)) {
+      // If the block of passing node is an exceptional successor of Block pred, propagate
+      // store to the exceptionStores. Currently it doesn't track the label of an
+      // exceptional edge from exception block to its exceptional successors in backward
+      // direction. Instead, all exception stores of exceptional successors of an
+      // exception block will merge to one exception store at the exception block
+      ExceptionBlock ebPred = (ExceptionBlock) pred;
+      S exceptionStore = exceptionStores.get(ebPred);
+      S newExceptionStore = (exceptionStore != null) ? exceptionStore.leastUpperBound(s) : s;
+      if (!newExceptionStore.equals(exceptionStore)) {
+        exceptionStores.put(ebPred, newExceptionStore);
+        inputs.put(ebPred, new TransferInput<V, S>(node, this, newExceptionStore));
+        addBlockToWorklist = true;
       }
     } else {
       S predOutStore = getStoreAfter(pred);
@@ -287,6 +282,31 @@ protected void addStoreAfter(Block pred, @Nullable Node node, S s, boolean addBl
     }
   }
 
+  /**
+   * Checks if the block for a node is an exceptional successor of a predecessor block.
+   *
+   * @param pred the predecessor block
+   * @param node the successor node
+   * @return {@code true} if {@code pred} is an {@link ExceptionBlock} and the block for {@code
+   *     node} is an exceptional successor of {@code pred}, false otherwise
+   */
+  private boolean isExceptionalSucc(Block pred, @Nullable Node node) {
+    if (pred instanceof ExceptionBlock && node != null) {
+      Block block = node.getBlock();
+      if (block != null) {
+        for (Set<Block> excSuccBlocks :
+            ((ExceptionBlock) pred).getExceptionalSuccessors().values()) {
+          for (Block excSuccBlock : excSuccBlocks) {
+            if (excSuccBlock.getUid() == block.getUid()) {
+              return true;
+            }
+          }
+        }
+      }
+    }
+    return false;
+  }
+
   /**
    * Returns the store corresponding to the location right after the basic block {@code b}.
    *

dataflow/tests/live-variable/Expected.txt

@@ -4,7 +4,12 @@
 4 -> 10 ELSE_TO_BOTH
 8 -> 11 EACH_TO_EACH
 10 -> 11 EACH_TO_EACH
-11 -> 0 EACH_TO_EACH
+11 -> 12 EACH_TO_EACH
+12 -> 13 EACH_TO_EACH
+12 -> 15 ArithmeticException
+13 -> 17 EACH_TO_EACH
+15 -> 17 EACH_TO_EACH
+17 -> 0 EACH_TO_EACH
 
 2:
 Process order: 1
@@ -31,7 +36,7 @@ a   [ LocalVariable ]
 0   [ IntegerLiteral ]
 (a > 0)   [ GreaterThan ]
 ~~~~~~~~~
-TransferInput#22
+TransferInput#49
 After:   live variables = a, b, c
 
 4:
@@ -52,7 +57,7 @@ c   [ LocalVariable ]
 (a + c)   [ NumericalAddition ]
 d = (a + c)   [ Assignment ]
 ~~~~~~~~~
-TransferInput#6
+TransferInput#33
 After:   live variables = a
 
 10:
@@ -66,23 +71,75 @@ b   [ LocalVariable ]
 (a + b)   [ NumericalAddition ]
 e = (a + b)   [ Assignment ]
 ~~~~~~~~~
-TransferInput#5
+TransferInput#32
 After:   live variables = a
 
 11:
 Process order: 6
 AnalysisResult#11
 Before:   live variables = a
 ~~~~~~~~~
+f   [ VariableDeclaration ]
+b   [ LocalVariable ]
+0   [ IntegerLiteral ]
+b = 0   [ Assignment ]
+marker (start of try statement #0)   [ Marker ]
+marker (start of try block #0)   [ Marker ]
+f   [ LocalVariable ]
+1   [ IntegerLiteral ]
+a   [ LocalVariable ]
+~~~~~~~~~
+TransferInput#21
+After:   live variables = a, b
+
+12:
+Process order: 7
+AnalysisResult#13
+Before:   live variables = a
+~~~~~~~~~
+(1 / a)   [ IntegerDivision ]
+
+13:
+Process order: 8
+AnalysisResult#15
+Before:   live variables = a
+~~~~~~~~~
+(1 / a)   [ IntegerDivision ]
+f = (1 / a)   [ Assignment ]
+marker (end of try block #0)   [ Marker ]
+~~~~~~~~~
+TransferInput#5
+After:   live variables = a
+
+15:
+Process order: 9
+AnalysisResult#17
+Before:   live variables = a, b
+~~~~~~~~~
+marker (start of catch block for ArithmeticException #0)   [ Marker ]
+e   [ VariableDeclaration ]
+f   [ LocalVariable ]
+b   [ LocalVariable ]
+f = b   [ Assignment ]
+marker (end of catch block for ArithmeticException #0)   [ Marker ]
+~~~~~~~~~
+TransferInput#6
+After:   live variables = a
+
+17:
+Process order: 10
+AnalysisResult#19
+Before:   live variables = a
+~~~~~~~~~
 a   [ LocalVariable ]
 return a   [ Return ]
 ~~~~~~~~~
 TransferInput#1
 After:   live variables = none
 
 0:
-Process order: 7
-AnalysisResult#13
+Process order: 11
+AnalysisResult#21
 Before:   live variables = none
 ~~~~~~~~~
 <exit>

dataflow/tests/live-variable/Test.java

@@ -7,6 +7,13 @@ public int test() {
     } else {
       int e = a + b;
     }
+    int f;
+    b = 0;
+    try {
+      f = 1 / a;
+    } catch (ArithmeticException e) {
+      f = b;
+    }
     return a;
   }
 }