adapt CFInferenceTest

Author: d367wang

testdata/ostrusted-unsat-test/Unsat.java …ata/ostrusted-inferrable-test/Unsat.javatestdata/ostrusted-unsat-test/Unsat.java renamed to testdata/ostrusted-inferrable-test/Unsat.java testdata/ostrusted-unsat-test/Unsat.java renamed to testdata/ostrusted-inferrable-test/Unsat.java

@@ -1,6 +1,7 @@
 package checkers.inference;
 
 import checkers.inference.solver.MaxSat2TypeSolver;
+import checkers.inference.solver.SolverEngine;
 import checkers.inference.test.CFInferenceTest;
 import org.checkerframework.framework.test.TestUtilities;
 import org.checkerframework.javacutil.Pair;
@@ -19,7 +20,7 @@ public OsTrustedTest(File testFile) {
 
     @Override
     public Pair<String, List<String>> getSolverNameAndOptions() {
-        return Pair.<String, List<String>>of(MaxSat2TypeSolver.class.getCanonicalName(), new ArrayList<String>());
+        return Pair.<String, List<String>>of(SolverEngine.class.getCanonicalName(), new ArrayList<String>());
     }
 
     @Parameters

tests/checkers/inference/OsTrustedTest.java

@@ -1,7 +1,11 @@
 package checkers.inference.test;
 
 import org.checkerframework.framework.test.CheckerFrameworkPerFileTest;
+import org.checkerframework.framework.test.TestConfiguration;
 import org.checkerframework.framework.test.TestUtilities;
+import org.checkerframework.framework.test.diagnostics.DiagnosticKind;
+import org.checkerframework.framework.test.diagnostics.JavaDiagnosticReader;
+import org.checkerframework.framework.test.diagnostics.TestDiagnostic;
 import org.checkerframework.javacutil.Pair;
 import org.checkerframework.javacutil.SystemUtil;
 
@@ -11,6 +15,7 @@
 
 import javax.annotation.processing.AbstractProcessor;
 
+import org.junit.Assert;
 import org.junit.Test;
 
 public abstract class CFInferenceTest extends CheckerFrameworkPerFileTest {
@@ -57,15 +62,19 @@ testFile, testDataDir, checkerName, checkerOptions, getAdditionalInferenceOption
                 solverArgs.second, useHacks(), shouldEmitDebugInfo, getPathToAfuScripts(), getPathToInferenceScript());
 
         InferenceTestResult testResult = new InferenceTestExecutor().runTest(config);
-        postProcessResult(testResult);
-    }
 
-    /**
-     * Report a summary of the failed test based on the {@link InferenceTestResult}.
-     *
-     * @param testResult the test result returned by {@code InferenceTestExecutor}
-     */
-    protected void postProcessResult(InferenceTestResult testResult) {
-        InferenceTestUtilities.assertResultsAreValid(testResult);
+        // If the test file contains any hard error, then the test should fail at inference phase and not proceed.
+        // i.e. the last phase is inference.
+        TestConfiguration typecheckConfig = config.getInitialTypecheckConfig();
+        List<TestDiagnostic> expectedDiagnostics = JavaDiagnosticReader.readJavaSourceFiles(typecheckConfig.getTestSourceFiles());
+        InferenceTestPhase expectedLastPhase = InferenceTestPhase.FINAL_TYPECHECK;
+        for (TestDiagnostic diagnostic : expectedDiagnostics) {
+            if (!diagnostic.isFixable()) {
+                expectedLastPhase = InferenceTestPhase.INFER;
+                break;
+            }
+        }
+        InferenceTestUtilities.assertResultsAreValid(testResult, expectedLastPhase);
     }
+
 }

tests/checkers/inference/OsTrustedUnsatTest.java

@@ -14,6 +14,7 @@
 import java.util.regex.Matcher;
 import java.util.regex.Pattern;
 
+import org.checkerframework.javacutil.SystemUtil;
 import org.junit.Assert;
 
 /**
@@ -96,7 +97,7 @@ public static void assertFail(InferenceTestPhase lastPhase, String summary) {
         Assert.fail(message);
     }
 
-    public static void assertResultsAreValid(InferenceTestResult testResult) {
+    public static void assertResultsAreValid(InferenceTestResult testResult, InferenceTestPhase expectedLastPhase) {
         final InferenceTestPhase lastPhaseRun = testResult.getLastPhaseRun();
 
         switch (lastPhaseRun) {
@@ -105,14 +106,23 @@ public static void assertResultsAreValid(InferenceTestResult testResult) {
                 break;
 
             case INFER:
-                assertFail(InferenceTestPhase.INFER, testResult.getInferenceResult().summarize());
+                if (expectedLastPhase != InferenceTestPhase.INFER) {
+                    assertFail(InferenceTestPhase.INFER, testResult.getInferenceResult().summarize());
+                }
                 break;
 
             case INSERT:
                 assertFail(InferenceTestPhase.INSERT, testResult.getInsertionResult().summarize());
                 break;
 
             case FINAL_TYPECHECK:
+                if (expectedLastPhase == InferenceTestPhase.INFER) {
+                    String summary = "Inference is expected to fail, but succeeded on the source file: \n"
+                            + SystemUtil.join("\n", testResult.getConfiguration().getInitialTypecheckConfig().getTestSourceFiles()) + "\n\n";
+
+                    assertFail(InferenceTestPhase.INFER, summary);
+                }
+
                 TypecheckResult finalTypecheckResult = testResult.getFinalTypecheckResult();
                 if (finalTypecheckResult.didTestFail()) {
                     assertFail(InferenceTestPhase.FINAL_TYPECHECK, finalTypecheckResult.summarize());