Correct the logic of dataflow framework. (#3414)

BackwardAnalysis: 1. Add exception block's predecessor exception block to inputs (fix null pointer exception). 2. When running `runAnalysisFor()` with an exception block, pass a copied transfer input to `callTransferFunction()`. ForwardAnalysis: 1. When running `runAnalysisFor()` with an exception block, pass a copied transfer input to `callTransferFunction()`. In the previous dataflow framework (before #3370), we passed a non-copied transfer input (https://github.com/typetools/checker-framework/pull/3370/files#diff-d4108228a0a5407e00c090c2e97d8b6dL401-L402). This seems a bug existing in the old dataflow framework. Resolves #3447.
typetools · Jul 23, 2020 · bc9a120 · bc9a120
1 parent 90cdd5e
commit bc9a120
Show file tree

Hide file tree

Showing 5 changed files with 42 additions and 4 deletions.
diff --git a/build.gradle b/build.gradle
@@ -829,6 +829,7 @@ subprojects {
 
             if (project.name.is('dataflow')) {
                 dependsOn('liveVariableTest')
+                dependsOn('issue3447Test')
             }
         }
 

diff --git a/dataflow/build.gradle b/dataflow/build.gradle
@@ -59,3 +59,21 @@ task liveVariableTest(dependsOn: compileTestJava, group: 'Verification') {
         }
     }
 }
+
+task issue3447Test(dependsOn: compileTestJava, group: 'Verification') {
+    description 'Test issue 3447 test case for backward analysis.'
+    inputs.file('tests/issue3447/Test.java')
+    delete('tests/issue3447/Out.txt')
+    delete('tests/issue3447/Test.class')
+    doLast {
+        javaexec {
+            workingDir = 'tests/issue3447'
+            if (!JavaVersion.current().java9Compatible) {
+                jvmArgs += "-Xbootclasspath/p:${configurations.javacJar.asPath}"
+            }
+            classpath = sourceSets.test.compileClasspath
+            classpath += sourceSets.test.output
+            main = 'livevar.LiveVariable'
+        }
+    }
+}
diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/BackwardAnalysisImpl.java b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/BackwardAnalysisImpl.java
@@ -286,6 +286,7 @@ protected void addStoreAfter(Block pred, @Nullable Node node, S s, boolean addBl
                         (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;
                 }
             }
@@ -344,7 +345,8 @@ public S runAnalysisFor(
                             if (n == node && !before) {
                                 return store.getRegularStore();
                             }
-                            // Copy the store to preserve to change the state in {@link #inputs}
+                            // Copy the store to avoid changing other blocks' transfer inputs in
+                            // {@link #inputs}
                             TransferResult<V, S> transferResult =
                                     callTransferFunction(n, store.copy());
                             if (n == node) {
@@ -370,8 +372,10 @@ public S runAnalysisFor(
                             return transferInput.getRegularStore();
                         }
                         setCurrentNode(node);
+                        // Copy the store to avoid changing other blocks' transfer inputs in {@link
+                        // #inputs}
                         TransferResult<V, S> transferResult =
-                                callTransferFunction(node, transferInput);
+                                callTransferFunction(node, transferInput.copy());
                         // Merge transfer result with the exception store of this exceptional block
                         S exceptionStore = exceptionStores.get(eb);
                         return exceptionStore == null

diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/ForwardAnalysisImpl.java b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/ForwardAnalysisImpl.java
@@ -282,7 +282,8 @@ public S runAnalysisFor(
                             if (cache != null && cache.containsKey(n)) {
                                 transferResult = cache.get(n);
                             } else {
-                                // Copy the store to preserve to change the state in the cache
+                                // Copy the store to avoid changing other blocks' transfer inputs in
+                                // {@link #inputs}
                                 transferResult = callTransferFunction(n, store.copy());
                                 if (cache != null) {
                                     cache.put(n, transferResult);
@@ -312,8 +313,10 @@ public S runAnalysisFor(
                             return transferInput.getRegularStore();
                         }
                         setCurrentNode(node);
+                        // Copy the store to avoid changing other blocks' transfer inputs in {@link
+                        // #inputs}
                         TransferResult<V, S> transferResult =
-                                callTransferFunction(node, transferInput);
+                                callTransferFunction(node, transferInput.copy());
                         return transferResult.getRegularStore();
                     }
                 default:

diff --git a/dataflow/tests/issue3447/Test.java b/dataflow/tests/issue3447/Test.java
@@ -0,0 +1,12 @@
+// Test case for Issue 3447:
+// https://github.com/typetools/checker-framework/issues/3447
+
+public class Test {
+    public void test() throws Exception {
+        try {
+            int[] myNumbers = {1};
+            System.out.println(myNumbers[1]);
+        } catch (Exception e) {
+        }
+    }
+}