From e8613b20f49067a08d8214d385f12c2e546399cc Mon Sep 17 00:00:00 2001 From: d367wang Date: Tue, 6 Jul 2021 18:54:30 -0400 Subject: [PATCH 01/11] add unsat verification to test infrastructure --- testdata/ostrusted-unsat-test/Unsat.java | 16 ++++++++ .../inference/OsTrustedUnsatTest.java | 31 +++++++++++++++ .../inference/test/CFInferenceUnsatTest.java | 38 +++++++++++++++++++ 3 files changed, 85 insertions(+) create mode 100644 testdata/ostrusted-unsat-test/Unsat.java create mode 100644 tests/checkers/inference/OsTrustedUnsatTest.java create mode 100644 tests/checkers/inference/test/CFInferenceUnsatTest.java diff --git a/testdata/ostrusted-unsat-test/Unsat.java b/testdata/ostrusted-unsat-test/Unsat.java new file mode 100644 index 000000000..f9d95f570 --- /dev/null +++ b/testdata/ostrusted-unsat-test/Unsat.java @@ -0,0 +1,16 @@ +import ostrusted.qual.OsUntrusted; +import ostrusted.qual.OsTrusted; + +class Unsat { + + void foo(@OsTrusted String s) {} + + @OsUntrusted + String bar() { return ""; } + + void m() { + String s = bar(); + // :: error: (argument.type.incompatible) + foo(s); + } +} diff --git a/tests/checkers/inference/OsTrustedUnsatTest.java b/tests/checkers/inference/OsTrustedUnsatTest.java new file mode 100644 index 000000000..22c744a27 --- /dev/null +++ b/tests/checkers/inference/OsTrustedUnsatTest.java @@ -0,0 +1,31 @@ +package checkers.inference; + +import checkers.inference.solver.SolverEngine; +import checkers.inference.test.CFInferenceUnsatTest; +import org.checkerframework.framework.test.TestUtilities; +import org.checkerframework.javacutil.Pair; +import org.junit.runners.Parameterized; + +import java.io.File; +import java.util.ArrayList; +import java.util.List; + +public class OsTrustedUnsatTest extends CFInferenceUnsatTest { + + public OsTrustedUnsatTest(File testFile) { + super(testFile, ostrusted.OsTrustedChecker.class, "ostrusted", + "-Anomsgtext", "-Astubs=src/ostrusted/jdk.astub", "-d", "tests/build/outputdir"); + } + + @Override + public Pair> getSolverNameAndOptions() { + return Pair.>of(SolverEngine.class.getCanonicalName(), new ArrayList()); + } + + @Parameterized.Parameters + public static List getTestFiles(){ + List testfiles = new ArrayList<>();//InferenceTestUtilities.findAllSystemTests(); + testfiles.addAll(TestUtilities.findRelativeNestedJavaFiles("testdata", "ostrusted-unsat-test")); + return testfiles; + } +} diff --git a/tests/checkers/inference/test/CFInferenceUnsatTest.java b/tests/checkers/inference/test/CFInferenceUnsatTest.java new file mode 100644 index 000000000..75f419ead --- /dev/null +++ b/tests/checkers/inference/test/CFInferenceUnsatTest.java @@ -0,0 +1,38 @@ +package checkers.inference.test; + +import org.checkerframework.framework.test.TestUtilities; +import org.checkerframework.javacutil.Pair; +import org.checkerframework.javacutil.SystemUtil; +import org.junit.Test; + +import javax.annotation.processing.AbstractProcessor; +import java.io.File; +import java.util.List; + +public abstract class CFInferenceUnsatTest extends CFInferenceTest{ + public CFInferenceUnsatTest(File testFile, Class checker, + String testDir, String... checkerOptions) { + super(testFile, checker, testDir, checkerOptions); + } + + @Override + @Test + public void run() { + boolean shouldEmitDebugInfo = TestUtilities.getShouldEmitDebugInfo(); + Pair> solverArgs = getSolverNameAndOptions(); + + final File testDataDir = new File("testdata"); + + InferenceTestConfiguration config = InferenceTestConfigurationBuilder.buildDefaultConfiguration(testDir, + testFile, testDataDir, checkerName, checkerOptions, getAdditionalInferenceOptions(), solverArgs.first, + solverArgs.second, useHacks(), shouldEmitDebugInfo, getPathToAfuScripts(), getPathToInferenceScript()); + + InferenceTestResult testResult = new InferenceTestExecutor().runTest(config); + final InferenceTestPhase lastPhaseRun = testResult.getLastPhaseRun(); + if (lastPhaseRun != InferenceTestPhase.INFER) { + String summary = "Inference is expected to fail, but succeeded on source files: \n" + + SystemUtil.join("\n", testResult.getConfiguration().getInitialTypecheckConfig().getTestSourceFiles()) + "\n\n"; + InferenceTestUtilities.assertFail(InferenceTestPhase.INFER, summary); + } + } +} From 6bf6317fcdbefedb38fee653ced5a11811f450b8 Mon Sep 17 00:00:00 2001 From: d367wang Date: Thu, 8 Jul 2021 08:47:20 -0400 Subject: [PATCH 02/11] update error messages for different kinds of failure --- tests/checkers/inference/test/CFInferenceUnsatTest.java | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/tests/checkers/inference/test/CFInferenceUnsatTest.java b/tests/checkers/inference/test/CFInferenceUnsatTest.java index 75f419ead..36f705b4b 100644 --- a/tests/checkers/inference/test/CFInferenceUnsatTest.java +++ b/tests/checkers/inference/test/CFInferenceUnsatTest.java @@ -29,7 +29,10 @@ testFile, testDataDir, checkerName, checkerOptions, getAdditionalInferenceOption InferenceTestResult testResult = new InferenceTestExecutor().runTest(config); final InferenceTestPhase lastPhaseRun = testResult.getLastPhaseRun(); - if (lastPhaseRun != InferenceTestPhase.INFER) { + if (lastPhaseRun == InferenceTestPhase.INITIAL_TYPECHECK) { + InferenceTestUtilities.assertResultsAreValid(testResult); + + } else if (lastPhaseRun == InferenceTestPhase.FINAL_TYPECHECK) { String summary = "Inference is expected to fail, but succeeded on source files: \n" + SystemUtil.join("\n", testResult.getConfiguration().getInitialTypecheckConfig().getTestSourceFiles()) + "\n\n"; InferenceTestUtilities.assertFail(InferenceTestPhase.INFER, summary); From 5209dc4424538fd2df75e289819a7ba33fe89842 Mon Sep 17 00:00:00 2001 From: d367wang Date: Tue, 13 Jul 2021 14:38:57 -0400 Subject: [PATCH 03/11] refactor --- .../inference/test/CFInferenceTest.java | 4 ++++ .../inference/test/CFInferenceUnsatTest.java | 24 +++++++------------ 2 files changed, 12 insertions(+), 16 deletions(-) diff --git a/tests/checkers/inference/test/CFInferenceTest.java b/tests/checkers/inference/test/CFInferenceTest.java index 34fbf60d3..aed50b6fb 100644 --- a/tests/checkers/inference/test/CFInferenceTest.java +++ b/tests/checkers/inference/test/CFInferenceTest.java @@ -57,6 +57,10 @@ testFile, testDataDir, checkerName, checkerOptions, getAdditionalInferenceOption solverArgs.second, useHacks(), shouldEmitDebugInfo, getPathToAfuScripts(), getPathToInferenceScript()); InferenceTestResult testResult = new InferenceTestExecutor().runTest(config); + postProcessResult(testResult); + } + + protected void postProcessResult(InferenceTestResult testResult) { InferenceTestUtilities.assertResultsAreValid(testResult); } } diff --git a/tests/checkers/inference/test/CFInferenceUnsatTest.java b/tests/checkers/inference/test/CFInferenceUnsatTest.java index 36f705b4b..a73078f38 100644 --- a/tests/checkers/inference/test/CFInferenceUnsatTest.java +++ b/tests/checkers/inference/test/CFInferenceUnsatTest.java @@ -1,14 +1,17 @@ package checkers.inference.test; -import org.checkerframework.framework.test.TestUtilities; -import org.checkerframework.javacutil.Pair; import org.checkerframework.javacutil.SystemUtil; -import org.junit.Test; import javax.annotation.processing.AbstractProcessor; import java.io.File; -import java.util.List; +/** + * This test suite runs inference individually on target files that are unsatisfiable. This means each + * test case is expected to pass the initial check phase while fail at the inference phase and terminate. + * + * The use of this class is the same as {@link CFInferenceTest}. Note that the target directory of the test + * cases can only contain unsatisfiable cases. + */ public abstract class CFInferenceUnsatTest extends CFInferenceTest{ public CFInferenceUnsatTest(File testFile, Class checker, String testDir, String... checkerOptions) { @@ -16,18 +19,7 @@ public CFInferenceUnsatTest(File testFile, Class ch } @Override - @Test - public void run() { - boolean shouldEmitDebugInfo = TestUtilities.getShouldEmitDebugInfo(); - Pair> solverArgs = getSolverNameAndOptions(); - - final File testDataDir = new File("testdata"); - - InferenceTestConfiguration config = InferenceTestConfigurationBuilder.buildDefaultConfiguration(testDir, - testFile, testDataDir, checkerName, checkerOptions, getAdditionalInferenceOptions(), solverArgs.first, - solverArgs.second, useHacks(), shouldEmitDebugInfo, getPathToAfuScripts(), getPathToInferenceScript()); - - InferenceTestResult testResult = new InferenceTestExecutor().runTest(config); + protected void postProcessResult(InferenceTestResult testResult) { final InferenceTestPhase lastPhaseRun = testResult.getLastPhaseRun(); if (lastPhaseRun == InferenceTestPhase.INITIAL_TYPECHECK) { InferenceTestUtilities.assertResultsAreValid(testResult); From d5a96722bb74aa55f448d29ae38483af472ac999 Mon Sep 17 00:00:00 2001 From: d367wang <55197967+d367wang@users.noreply.github.com> Date: Tue, 13 Jul 2021 21:42:37 -0400 Subject: [PATCH 04/11] Apply suggestions from code review Co-authored-by: Werner Dietl --- testdata/ostrusted-unsat-test/Unsat.java | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/testdata/ostrusted-unsat-test/Unsat.java b/testdata/ostrusted-unsat-test/Unsat.java index f9d95f570..96b3758bc 100644 --- a/testdata/ostrusted-unsat-test/Unsat.java +++ b/testdata/ostrusted-unsat-test/Unsat.java @@ -5,8 +5,7 @@ class Unsat { void foo(@OsTrusted String s) {} - @OsUntrusted - String bar() { return ""; } + @OsUntrusted String bar() { return ""; } void m() { String s = bar(); From 5c2182858cc007f878bb831a66c14cc9d71b1b7a Mon Sep 17 00:00:00 2001 From: d367wang Date: Wed, 14 Jul 2021 00:18:59 -0400 Subject: [PATCH 05/11] add comments --- testdata/ostrusted-unsat-test/Unsat.java | 7 +++++++ tests/checkers/inference/test/CFInferenceTest.java | 5 +++++ tests/checkers/inference/test/CFInferenceUnsatTest.java | 5 +++-- 3 files changed, 15 insertions(+), 2 deletions(-) diff --git a/testdata/ostrusted-unsat-test/Unsat.java b/testdata/ostrusted-unsat-test/Unsat.java index 96b3758bc..84032cd1b 100644 --- a/testdata/ostrusted-unsat-test/Unsat.java +++ b/testdata/ostrusted-unsat-test/Unsat.java @@ -1,6 +1,13 @@ import ostrusted.qual.OsUntrusted; import ostrusted.qual.OsTrusted; +/** + * This case is unsatisfiable, because in method {@code m()}, + *

(1) at line 18, the local variable {@code s} is refined by the return type of {@code bar()}. + * Denote the refinement variable as @1, then @1 == @OsUntrusted. + *

(2) at line 20, {@code s} is passed to method {@code foo} as the argument, therefore @1 <: @OsTrusted + * since @OsTrusted is bottom, @1 == @OsTrusted. + */ class Unsat { void foo(@OsTrusted String s) {} diff --git a/tests/checkers/inference/test/CFInferenceTest.java b/tests/checkers/inference/test/CFInferenceTest.java index aed50b6fb..4f04e3398 100644 --- a/tests/checkers/inference/test/CFInferenceTest.java +++ b/tests/checkers/inference/test/CFInferenceTest.java @@ -60,6 +60,11 @@ testFile, testDataDir, checkerName, checkerOptions, getAdditionalInferenceOption 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); } diff --git a/tests/checkers/inference/test/CFInferenceUnsatTest.java b/tests/checkers/inference/test/CFInferenceUnsatTest.java index a73078f38..02d5a11cd 100644 --- a/tests/checkers/inference/test/CFInferenceUnsatTest.java +++ b/tests/checkers/inference/test/CFInferenceUnsatTest.java @@ -6,8 +6,9 @@ import java.io.File; /** - * This test suite runs inference individually on target files that are unsatisfiable. This means each - * test case is expected to pass the initial check phase while fail at the inference phase and terminate. + * This test suite runs inference individually on target files that are unsatisfiable. A test case passes + * when it passes the initial check phase (i.e. outputs expected errors/warnings and none unexpected ones), + * while fails at the inference phase and then terminates. * * The use of this class is the same as {@link CFInferenceTest}. Note that the target directory of the test * cases can only contain unsatisfiable cases. From 576d9b489ce33c0d8395480558c6e5bbace5e3ad Mon Sep 17 00:00:00 2001 From: d367wang Date: Thu, 15 Jul 2021 02:41:05 -0400 Subject: [PATCH 06/11] adapt CFInferenceTest --- .../Unsat.java | 0 tests/checkers/inference/OsTrustedTest.java | 3 +- .../inference/OsTrustedUnsatTest.java | 31 ----------------- .../inference/test/CFInferenceTest.java | 27 ++++++++++----- .../inference/test/CFInferenceUnsatTest.java | 34 ------------------- .../test/InferenceTestUtilities.java | 14 ++++++-- 6 files changed, 32 insertions(+), 77 deletions(-) rename testdata/{ostrusted-unsat-test => ostrusted-inferrable-test}/Unsat.java (100%) delete mode 100644 tests/checkers/inference/OsTrustedUnsatTest.java delete mode 100644 tests/checkers/inference/test/CFInferenceUnsatTest.java diff --git a/testdata/ostrusted-unsat-test/Unsat.java b/testdata/ostrusted-inferrable-test/Unsat.java similarity index 100% rename from testdata/ostrusted-unsat-test/Unsat.java rename to testdata/ostrusted-inferrable-test/Unsat.java diff --git a/tests/checkers/inference/OsTrustedTest.java b/tests/checkers/inference/OsTrustedTest.java index 5551acaed..be6aaf06e 100644 --- a/tests/checkers/inference/OsTrustedTest.java +++ b/tests/checkers/inference/OsTrustedTest.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> getSolverNameAndOptions() { - return Pair.>of(MaxSat2TypeSolver.class.getCanonicalName(), new ArrayList()); + return Pair.>of(SolverEngine.class.getCanonicalName(), new ArrayList()); } @Parameters diff --git a/tests/checkers/inference/OsTrustedUnsatTest.java b/tests/checkers/inference/OsTrustedUnsatTest.java deleted file mode 100644 index 22c744a27..000000000 --- a/tests/checkers/inference/OsTrustedUnsatTest.java +++ /dev/null @@ -1,31 +0,0 @@ -package checkers.inference; - -import checkers.inference.solver.SolverEngine; -import checkers.inference.test.CFInferenceUnsatTest; -import org.checkerframework.framework.test.TestUtilities; -import org.checkerframework.javacutil.Pair; -import org.junit.runners.Parameterized; - -import java.io.File; -import java.util.ArrayList; -import java.util.List; - -public class OsTrustedUnsatTest extends CFInferenceUnsatTest { - - public OsTrustedUnsatTest(File testFile) { - super(testFile, ostrusted.OsTrustedChecker.class, "ostrusted", - "-Anomsgtext", "-Astubs=src/ostrusted/jdk.astub", "-d", "tests/build/outputdir"); - } - - @Override - public Pair> getSolverNameAndOptions() { - return Pair.>of(SolverEngine.class.getCanonicalName(), new ArrayList()); - } - - @Parameterized.Parameters - public static List getTestFiles(){ - List testfiles = new ArrayList<>();//InferenceTestUtilities.findAllSystemTests(); - testfiles.addAll(TestUtilities.findRelativeNestedJavaFiles("testdata", "ostrusted-unsat-test")); - return testfiles; - } -} diff --git a/tests/checkers/inference/test/CFInferenceTest.java b/tests/checkers/inference/test/CFInferenceTest.java index 4f04e3398..17a3aa1fb 100644 --- a/tests/checkers/inference/test/CFInferenceTest.java +++ b/tests/checkers/inference/test/CFInferenceTest.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 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); } + } diff --git a/tests/checkers/inference/test/CFInferenceUnsatTest.java b/tests/checkers/inference/test/CFInferenceUnsatTest.java deleted file mode 100644 index 02d5a11cd..000000000 --- a/tests/checkers/inference/test/CFInferenceUnsatTest.java +++ /dev/null @@ -1,34 +0,0 @@ -package checkers.inference.test; - -import org.checkerframework.javacutil.SystemUtil; - -import javax.annotation.processing.AbstractProcessor; -import java.io.File; - -/** - * This test suite runs inference individually on target files that are unsatisfiable. A test case passes - * when it passes the initial check phase (i.e. outputs expected errors/warnings and none unexpected ones), - * while fails at the inference phase and then terminates. - * - * The use of this class is the same as {@link CFInferenceTest}. Note that the target directory of the test - * cases can only contain unsatisfiable cases. - */ -public abstract class CFInferenceUnsatTest extends CFInferenceTest{ - public CFInferenceUnsatTest(File testFile, Class checker, - String testDir, String... checkerOptions) { - super(testFile, checker, testDir, checkerOptions); - } - - @Override - protected void postProcessResult(InferenceTestResult testResult) { - final InferenceTestPhase lastPhaseRun = testResult.getLastPhaseRun(); - if (lastPhaseRun == InferenceTestPhase.INITIAL_TYPECHECK) { - InferenceTestUtilities.assertResultsAreValid(testResult); - - } else if (lastPhaseRun == InferenceTestPhase.FINAL_TYPECHECK) { - String summary = "Inference is expected to fail, but succeeded on source files: \n" - + SystemUtil.join("\n", testResult.getConfiguration().getInitialTypecheckConfig().getTestSourceFiles()) + "\n\n"; - InferenceTestUtilities.assertFail(InferenceTestPhase.INFER, summary); - } - } -} diff --git a/tests/checkers/inference/test/InferenceTestUtilities.java b/tests/checkers/inference/test/InferenceTestUtilities.java index c55606bfa..d62c877df 100644 --- a/tests/checkers/inference/test/InferenceTestUtilities.java +++ b/tests/checkers/inference/test/InferenceTestUtilities.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,7 +106,9 @@ 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: @@ -113,6 +116,13 @@ public static void assertResultsAreValid(InferenceTestResult testResult) { 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()); From fad7c628a7df32368e51b2f12de623057487c62a Mon Sep 17 00:00:00 2001 From: d367wang Date: Thu, 15 Jul 2021 13:12:35 -0400 Subject: [PATCH 07/11] change back to max2type solver --- tests/checkers/inference/OsTrustedTest.java | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/tests/checkers/inference/OsTrustedTest.java b/tests/checkers/inference/OsTrustedTest.java index be6aaf06e..5551acaed 100644 --- a/tests/checkers/inference/OsTrustedTest.java +++ b/tests/checkers/inference/OsTrustedTest.java @@ -1,7 +1,6 @@ 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; @@ -20,7 +19,7 @@ public OsTrustedTest(File testFile) { @Override public Pair> getSolverNameAndOptions() { - return Pair.>of(SolverEngine.class.getCanonicalName(), new ArrayList()); + return Pair.>of(MaxSat2TypeSolver.class.getCanonicalName(), new ArrayList()); } @Parameters From 49c3cf5acc80ae1d927948d1d62d81713edb5769 Mon Sep 17 00:00:00 2001 From: d367wang Date: Fri, 27 Aug 2021 07:31:11 -0400 Subject: [PATCH 08/11] tweaks --- tests/checkers/inference/test/InferenceTestUtilities.java | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/tests/checkers/inference/test/InferenceTestUtilities.java b/tests/checkers/inference/test/InferenceTestUtilities.java index d62c877df..37d7c34fa 100644 --- a/tests/checkers/inference/test/InferenceTestUtilities.java +++ b/tests/checkers/inference/test/InferenceTestUtilities.java @@ -14,9 +14,10 @@ import java.util.regex.Matcher; import java.util.regex.Pattern; -import org.checkerframework.javacutil.SystemUtil; import org.junit.Assert; +import org.plumelib.util.StringsPlume; + /** * Created by jburke on 7/7/15. */ @@ -118,7 +119,7 @@ public static void assertResultsAreValid(InferenceTestResult testResult, Inferen 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"; + + StringsPlume.join("\n", testResult.getConfiguration().getInitialTypecheckConfig().getTestSourceFiles()) + "\n\n"; assertFail(InferenceTestPhase.INFER, summary); } From 5f840ed4d42cc1cd08921afd10a0f053be4a9fec Mon Sep 17 00:00:00 2001 From: d367wang Date: Tue, 31 Aug 2021 14:59:15 -0400 Subject: [PATCH 09/11] remove -Awarn flag --- src/checkers/inference/InferenceMain.java | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/checkers/inference/InferenceMain.java b/src/checkers/inference/InferenceMain.java index e7d167ac2..1345e875d 100644 --- a/src/checkers/inference/InferenceMain.java +++ b/src/checkers/inference/InferenceMain.java @@ -160,8 +160,7 @@ private void startCheckerFramework() { "-processor", "checkers.inference.InferenceChecker", "-Xmaxwarns", "1000", "-Xmaxerrs", "1000", - "-XDignore.symbol.file", - "-Awarns")); + "-XDignore.symbol.file")); if (SystemUtil.getJreVersion() == 8) { checkerFrameworkArgs.addAll(Arrays.asList("-source", "8", "-target", "8")); From 10fe1b262682cab45ddaf5ffc3fb9c6b4cc0e756 Mon Sep 17 00:00:00 2001 From: d367wang Date: Fri, 17 Dec 2021 12:24:29 -0500 Subject: [PATCH 10/11] enable -Awarn --- src/checkers/inference/InferenceMain.java | 6 +++++- testdata/ostrusted-inferrable-test/Unsat.java | 5 ++--- .../inference/test/CFInferenceTest.java | 20 +------------------ .../test/InferenceTestUtilities.java | 15 ++------------ 4 files changed, 10 insertions(+), 36 deletions(-) diff --git a/src/checkers/inference/InferenceMain.java b/src/checkers/inference/InferenceMain.java index 1345e875d..9971dfcf2 100644 --- a/src/checkers/inference/InferenceMain.java +++ b/src/checkers/inference/InferenceMain.java @@ -160,7 +160,8 @@ private void startCheckerFramework() { "-processor", "checkers.inference.InferenceChecker", "-Xmaxwarns", "1000", "-Xmaxerrs", "1000", - "-XDignore.symbol.file")); + "-XDignore.symbol.file", + "-Awarns")); if (SystemUtil.getJreVersion() == 8) { checkerFrameworkArgs.addAll(Arrays.asList("-source", "8", "-target", "8")); @@ -452,6 +453,9 @@ public DefaultResultHandler(Logger logger) { @Override public void handleCompilerResult(boolean success, String javacOutStr) { + if (!javacOutStr.isEmpty()) { + logger.severe(javacOutStr); + } if (!success) { logger.severe("Error return code from javac! Quitting."); logger.info(javacOutStr); diff --git a/testdata/ostrusted-inferrable-test/Unsat.java b/testdata/ostrusted-inferrable-test/Unsat.java index 84032cd1b..6c7e40b4e 100644 --- a/testdata/ostrusted-inferrable-test/Unsat.java +++ b/testdata/ostrusted-inferrable-test/Unsat.java @@ -15,8 +15,7 @@ void foo(@OsTrusted String s) {} @OsUntrusted String bar() { return ""; } void m() { - String s = bar(); - // :: error: (argument.type.incompatible) - foo(s); + // :: error: (assignment.type.incompatible) + @OsTrusted String s = bar(); } } diff --git a/tests/checkers/inference/test/CFInferenceTest.java b/tests/checkers/inference/test/CFInferenceTest.java index 148c72650..50ab7bda5 100644 --- a/tests/checkers/inference/test/CFInferenceTest.java +++ b/tests/checkers/inference/test/CFInferenceTest.java @@ -1,11 +1,7 @@ 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; @@ -15,7 +11,6 @@ import javax.annotation.processing.AbstractProcessor; -import org.junit.Assert; import org.junit.Test; public abstract class CFInferenceTest extends CheckerFrameworkPerFileTest { @@ -62,19 +57,6 @@ testFile, testDataDir, checker, checkerOptions, getAdditionalInferenceOptions(), solverArgs.second, useHacks(), shouldEmitDebugInfo, getPathToAfuScripts(), getPathToInferenceScript()); InferenceTestResult testResult = new InferenceTestExecutor().runTest(config); - - // 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 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); + InferenceTestUtilities.assertResultsAreValid(testResult); } - } diff --git a/tests/checkers/inference/test/InferenceTestUtilities.java b/tests/checkers/inference/test/InferenceTestUtilities.java index 37d7c34fa..c55606bfa 100644 --- a/tests/checkers/inference/test/InferenceTestUtilities.java +++ b/tests/checkers/inference/test/InferenceTestUtilities.java @@ -16,8 +16,6 @@ import org.junit.Assert; -import org.plumelib.util.StringsPlume; - /** * Created by jburke on 7/7/15. */ @@ -98,7 +96,7 @@ public static void assertFail(InferenceTestPhase lastPhase, String summary) { Assert.fail(message); } - public static void assertResultsAreValid(InferenceTestResult testResult, InferenceTestPhase expectedLastPhase) { + public static void assertResultsAreValid(InferenceTestResult testResult) { final InferenceTestPhase lastPhaseRun = testResult.getLastPhaseRun(); switch (lastPhaseRun) { @@ -107,9 +105,7 @@ public static void assertResultsAreValid(InferenceTestResult testResult, Inferen break; case INFER: - if (expectedLastPhase != InferenceTestPhase.INFER) { - assertFail(InferenceTestPhase.INFER, testResult.getInferenceResult().summarize()); - } + assertFail(InferenceTestPhase.INFER, testResult.getInferenceResult().summarize()); break; case INSERT: @@ -117,13 +113,6 @@ public static void assertResultsAreValid(InferenceTestResult testResult, Inferen break; case FINAL_TYPECHECK: - if (expectedLastPhase == InferenceTestPhase.INFER) { - String summary = "Inference is expected to fail, but succeeded on the source file: \n" - + StringsPlume.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()); From 64ab80098749c7a1e9df0969b5a451df40b6b832 Mon Sep 17 00:00:00 2001 From: d367wang <55197967+d367wang@users.noreply.github.com> Date: Fri, 17 Dec 2021 12:27:25 -0500 Subject: [PATCH 11/11] Update Unsat.java --- testdata/ostrusted-inferrable-test/Unsat.java | 9 --------- 1 file changed, 9 deletions(-) diff --git a/testdata/ostrusted-inferrable-test/Unsat.java b/testdata/ostrusted-inferrable-test/Unsat.java index 6c7e40b4e..66cbdab08 100644 --- a/testdata/ostrusted-inferrable-test/Unsat.java +++ b/testdata/ostrusted-inferrable-test/Unsat.java @@ -1,17 +1,8 @@ import ostrusted.qual.OsUntrusted; import ostrusted.qual.OsTrusted; -/** - * This case is unsatisfiable, because in method {@code m()}, - *

(1) at line 18, the local variable {@code s} is refined by the return type of {@code bar()}. - * Denote the refinement variable as @1, then @1 == @OsUntrusted. - *

(2) at line 20, {@code s} is passed to method {@code foo} as the argument, therefore @1 <: @OsTrusted - * since @OsTrusted is bottom, @1 == @OsTrusted. - */ class Unsat { - void foo(@OsTrusted String s) {} - @OsUntrusted String bar() { return ""; } void m() {