From 7a656f2959b69d3eb88584e3826a5f475e22c420 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 4 Nov 2026 16:52:47 +0000 Subject: [PATCH 1/3] Drop the bare true row left when the last binder is dropped When the binder simplification drops the last binder of a Found chain, it left a bare `true` row after the path conditions, which reads as if the value above were true. A suffix that becomes just `true` is now left out; a Found that simplifies away entirely still shows `true`. Co-Authored-By: Claude Opus 5.5 --- .../ImageWriteParamRefinements.java | 21 +++++++ .../found_true_rows_error/Recoder.java | 34 +++++++++++ .../opt/VCBinderSimplification.java | 19 +++++- .../java/liquidjava/api/tests/FoundRows.java | 31 ++++++++++ .../api/tests/TestFoundBinders.java | 19 +----- .../api/tests/TestFoundTrueRows.java | 60 +++++++++++++++++++ .../opt/VCBinderSimplificationTest.java | 16 +++++ 7 files changed, 182 insertions(+), 18 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/found_true_rows_error/ImageWriteParamRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/found_true_rows_error/Recoder.java create mode 100644 liquidjava-verifier/src/test/java/liquidjava/api/tests/FoundRows.java create mode 100644 liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundTrueRows.java diff --git a/liquidjava-example/src/main/java/testSuite/classes/found_true_rows_error/ImageWriteParamRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/found_true_rows_error/ImageWriteParamRefinements.java new file mode 100644 index 00000000..0f57e3c4 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/found_true_rows_error/ImageWriteParamRefinements.java @@ -0,0 +1,21 @@ +package testSuite.classes.found_true_rows_error; + +import java.util.Locale; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// The call that reaches the state setCompressionType needs depends on its argument +@ExternalRefinementsFor("javax.imageio.ImageWriteParam") +@StateSet({"startCompression", "compressionExplicit", "compressionSet"}) +public interface ImageWriteParamRefinements { + @StateRefinement(to = "startCompression(this)") + void ImageWriteParam(Locale locale); + + @StateRefinement(to = "mode == 2 ? compressionExplicit(this) : startCompression(this)") + void setCompressionMode(int mode); + + @StateRefinement(from = "compressionExplicit(this)", to = "compressionSet(this)") + void setCompressionType(String compressionType); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/found_true_rows_error/Recoder.java b/liquidjava-example/src/main/java/testSuite/classes/found_true_rows_error/Recoder.java new file mode 100644 index 00000000..e8d3774b --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/found_true_rows_error/Recoder.java @@ -0,0 +1,34 @@ +package testSuite.classes.found_true_rows_error; + +import java.util.Locale; + +import javax.imageio.ImageWriteParam; + +// Study case A1_01 (dcm4che SlideRecoder, #375): Found showed the path conditions followed by a bare true row +public class Recoder { + + static void unknownState(ImageWriteParam wParam) { + wParam.setCompressionType("JPEG"); // Expect: State Refinement Error + } + + static void unknownStateInBranch(ImageWriteParam wParam, boolean baseline, boolean extended) { + if (baseline || extended) { + wParam.setCompressionType("JPEG"); // Expect: State Refinement Error + } + } + + static void unknownStateInNestedBranch(ImageWriteParam wParam, boolean lossless, boolean extended) { + if (lossless) { + if (!extended) { + wParam.setCompressionType("JPEG"); // Expect: State Refinement Error + } + } + } + + static void knownStateInBranch(boolean baseline) { + ImageWriteParam wParam = new ImageWriteParam(Locale.ROOT); + if (baseline) { + wParam.setCompressionType("JPEG"); // Expect: State Refinement Error + } + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCBinderSimplification.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCBinderSimplification.java index 3a2c4251..8f6c4fd3 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCBinderSimplification.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCBinderSimplification.java @@ -57,8 +57,17 @@ private VCImplication simplify(VCImplication implication, Set keptTrueBi if (next == null) return null; + return withNext(implication, next); + } + + /** + * Copies a VC node followed by its simplified suffix, leaving out a suffix that became just true + */ + private VCImplication withNext(VCImplication implication, VCImplication next) { VCImplication result = copyWithRefinement(implication, implication.getRefinement().clone()); - result.setNext(next); + // P => true -> P, so a trailing true row does not read as the value of the row above + if (!isPlainTrue(next)) + result.setNext(next); return result; } @@ -119,6 +128,14 @@ private boolean isTrueBinder(VCImplication implication) { return implication.hasBinder() && isTrue(implication.getRefinement().getExpression()); } + /** + * Checks whether a VC node is a last implication without binder refined with true + */ + private boolean isPlainTrue(VCImplication implication) { + return !implication.hasBinder() && !implication.hasNext() + && isTrue(implication.getRefinement().getExpression()); + } + /** * Checks whether a VC node is a binder refined with false */ diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/FoundRows.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/FoundRows.java new file mode 100644 index 00000000..af2cc6ab --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/FoundRows.java @@ -0,0 +1,31 @@ +package liquidjava.api.tests; + +import java.util.ArrayList; +import java.util.List; + +import liquidjava.processor.VCImplication; +import liquidjava.rj_language.ast.formatter.VariableFormatter; + +/** + * The rows of Found as the IDE writes them, without the instance counters that depend on verification order + */ +final class FoundRows { + + private FoundRows() { + } + + // binder name, then its refinement + static List rows(VCImplication found) { + List rows = new ArrayList<>(); + for (VCImplication current = found; current != null; current = current.getNext()) { + String refinement = current.getRefinement().getExpression().toDisplayString(); + rows.add(plain(current.hasBinder() ? "∀" + VariableFormatter.format(current.getName()) + " " + refinement + : refinement)); + } + return rows; + } + + static String plain(String text) { + return text.replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", ""); + } +} diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java index 6f5d44ff..3d86ad05 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java @@ -1,5 +1,7 @@ package liquidjava.api.tests; +import static liquidjava.api.tests.FoundRows.plain; +import static liquidjava.api.tests.FoundRows.rows; import static org.junit.jupiter.api.Assertions.*; import java.util.ArrayList; @@ -14,8 +16,6 @@ import liquidjava.diagnostics.Diagnostics; import liquidjava.diagnostics.errors.LJError; import liquidjava.diagnostics.errors.RefinementError; -import liquidjava.processor.VCImplication; -import liquidjava.rj_language.ast.formatter.VariableFormatter; import liquidjava.rj_language.opt.VCSimplificationResult; /** @@ -99,19 +99,4 @@ void writeToAnotherObjectsFieldIsNamedAfterThatObject() { assertEquals(List.of("∀this.level this.level >= 0", "∀other.level other.level == this.level - 1"), ERRORS.get(48).rows()); } - - // the rows of Found as the IDE writes them: binder name, then its refinement - private static List rows(VCImplication found) { - List rows = new ArrayList<>(); - for (VCImplication current = found; current != null; current = current.getNext()) { - String refinement = current.getRefinement().getExpression().toDisplayString(); - rows.add(plain(current.hasBinder() ? "∀" + VariableFormatter.format(current.getName()) + " " + refinement - : refinement)); - } - return rows; - } - - private static String plain(String text) { - return text.replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", ""); - } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundTrueRows.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundTrueRows.java new file mode 100644 index 00000000..05fc4c9a --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundTrueRows.java @@ -0,0 +1,60 @@ +package liquidjava.api.tests; + +import static liquidjava.api.tests.FoundRows.plain; +import static liquidjava.api.tests.FoundRows.rows; +import static org.junit.jupiter.api.Assertions.*; + +import java.util.List; +import java.util.Map; +import java.util.TreeMap; + +import org.junit.jupiter.api.BeforeAll; +import org.junit.jupiter.api.Test; + +import liquidjava.api.CommandLineLauncher; +import liquidjava.diagnostics.Diagnostics; +import liquidjava.diagnostics.errors.LJError; +import liquidjava.diagnostics.errors.StateRefinementError; + +/** + * Checks that Found for the errors of {@code classes/found_true_rows_error} ends with no bare true row once the binders + * that state nothing are dropped + */ +class TestFoundTrueRows { + + private static final Map ERRORS = new TreeMap<>(); + + @BeforeAll + static void verify() { + CommandLineLauncher.launch("../liquidjava-example/src/main/java/testSuite/classes/found_true_rows_error"); + for (LJError error : Diagnostics.getInstance().getErrors()) + ERRORS.put(error.getPosition().getLine(), assertInstanceOf(StateRefinementError.class, error)); + } + + private static List rowsAt(int line) { + return rows(ERRORS.get(line).getFoundSimplification().getImplication()); + } + + @Test + void foundThatSimplifiesAwayIsTrue() { + assertEquals(List.of("true"), rowsAt(11)); + assertEquals("found true but expected compressionExplicit(wParam)", plain(ERRORS.get(11).getMessage())); + } + + @Test + void pathConditionIsNotFollowedByTrue() { + assertEquals(List.of("∀#fresh baseline || extended"), rowsAt(16)); + assertEquals("found baseline || extended but expected compressionExplicit(wParam)", + plain(ERRORS.get(16).getMessage())); + } + + @Test + void nestedPathConditionsAreNotFollowedByTrue() { + assertEquals(List.of("∀#fresh #fresh == lossless && #fresh", "∀#fresh !extended"), rowsAt(23)); + } + + @Test + void knownStateStaysAfterThePathCondition() { + assertEquals(List.of("∀#fresh #fresh == baseline && #fresh", "∀wParam startCompression(wParam)"), rowsAt(31)); + } +} diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCBinderSimplificationTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCBinderSimplificationTest.java index 417fe864..1705c53e 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCBinderSimplificationTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCBinderSimplificationTest.java @@ -104,6 +104,22 @@ void ignoresNonBinderBooleanLiterals() { assertSimplificationSteps(binderSimplification, vc("true", "false"), step("true", "false")); } + @Test + void removesLastTrueBinderWithoutLeavingTrue() { + assertSimplificationSteps(binderSimplification, vc("∀p:boolean. p || q", "∀x:Object. true"), step("p || q")); + } + + @Test + void removesLastTrueBinderAfterNestedConditionsWithoutLeavingTrue() { + assertSimplificationSteps(binderSimplification, vc("∀p:boolean. p", "∀q:boolean. !q", "∀x:Object. true"), + step("p", "!q")); + } + + @Test + void collapsedFalseBinderLeavesNoTrueAfterAnotherRow() { + assertSimplificationSteps(binderSimplification, vc("∀x:int. x > 0", "∀y:int. false", "z > 0"), step("x > 0")); + } + @Test void trueBinderWithoutSuffixBecomesPlainTrue() { assertSimplificationSteps(binderSimplification, vc("∀x:int. true"), step("true")); From 6c948cb6ecc6074f843416eb3c94796703e8291c Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 4 Nov 2026 17:10:13 +0000 Subject: [PATCH 2/3] Explain the trailing true rule as a conjunction Co-Authored-By: Claude Opus 5.5 --- .../java/liquidjava/rj_language/opt/VCBinderSimplification.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCBinderSimplification.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCBinderSimplification.java index 8f6c4fd3..8e90ee18 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCBinderSimplification.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCBinderSimplification.java @@ -65,7 +65,7 @@ private VCImplication simplify(VCImplication implication, Set keptTrueBi */ private VCImplication withNext(VCImplication implication, VCImplication next) { VCImplication result = copyWithRefinement(implication, implication.getRefinement().clone()); - // P => true -> P, so a trailing true row does not read as the value of the row above + // Found reads its rows as a conjunction, so P && true -> P: a trailing true row only reads as the value above if (!isPlainTrue(next)) result.setNext(next); return result; From 25ed98791dc94da38114e3814f6a731a61abe1fa Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 4 Nov 2026 18:20:46 +0000 Subject: [PATCH 3/3] Keep only the unit tests for the trailing true row Co-Authored-By: Claude Opus 5.5 --- .../ImageWriteParamRefinements.java | 21 ------- .../found_true_rows_error/Recoder.java | 34 ----------- .../java/liquidjava/api/tests/FoundRows.java | 31 ---------- .../api/tests/TestFoundBinders.java | 19 +++++- .../api/tests/TestFoundTrueRows.java | 60 ------------------- 5 files changed, 17 insertions(+), 148 deletions(-) delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/found_true_rows_error/ImageWriteParamRefinements.java delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/found_true_rows_error/Recoder.java delete mode 100644 liquidjava-verifier/src/test/java/liquidjava/api/tests/FoundRows.java delete mode 100644 liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundTrueRows.java diff --git a/liquidjava-example/src/main/java/testSuite/classes/found_true_rows_error/ImageWriteParamRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/found_true_rows_error/ImageWriteParamRefinements.java deleted file mode 100644 index 0f57e3c4..00000000 --- a/liquidjava-example/src/main/java/testSuite/classes/found_true_rows_error/ImageWriteParamRefinements.java +++ /dev/null @@ -1,21 +0,0 @@ -package testSuite.classes.found_true_rows_error; - -import java.util.Locale; - -import liquidjava.specification.ExternalRefinementsFor; -import liquidjava.specification.StateRefinement; -import liquidjava.specification.StateSet; - -// The call that reaches the state setCompressionType needs depends on its argument -@ExternalRefinementsFor("javax.imageio.ImageWriteParam") -@StateSet({"startCompression", "compressionExplicit", "compressionSet"}) -public interface ImageWriteParamRefinements { - @StateRefinement(to = "startCompression(this)") - void ImageWriteParam(Locale locale); - - @StateRefinement(to = "mode == 2 ? compressionExplicit(this) : startCompression(this)") - void setCompressionMode(int mode); - - @StateRefinement(from = "compressionExplicit(this)", to = "compressionSet(this)") - void setCompressionType(String compressionType); -} diff --git a/liquidjava-example/src/main/java/testSuite/classes/found_true_rows_error/Recoder.java b/liquidjava-example/src/main/java/testSuite/classes/found_true_rows_error/Recoder.java deleted file mode 100644 index e8d3774b..00000000 --- a/liquidjava-example/src/main/java/testSuite/classes/found_true_rows_error/Recoder.java +++ /dev/null @@ -1,34 +0,0 @@ -package testSuite.classes.found_true_rows_error; - -import java.util.Locale; - -import javax.imageio.ImageWriteParam; - -// Study case A1_01 (dcm4che SlideRecoder, #375): Found showed the path conditions followed by a bare true row -public class Recoder { - - static void unknownState(ImageWriteParam wParam) { - wParam.setCompressionType("JPEG"); // Expect: State Refinement Error - } - - static void unknownStateInBranch(ImageWriteParam wParam, boolean baseline, boolean extended) { - if (baseline || extended) { - wParam.setCompressionType("JPEG"); // Expect: State Refinement Error - } - } - - static void unknownStateInNestedBranch(ImageWriteParam wParam, boolean lossless, boolean extended) { - if (lossless) { - if (!extended) { - wParam.setCompressionType("JPEG"); // Expect: State Refinement Error - } - } - } - - static void knownStateInBranch(boolean baseline) { - ImageWriteParam wParam = new ImageWriteParam(Locale.ROOT); - if (baseline) { - wParam.setCompressionType("JPEG"); // Expect: State Refinement Error - } - } -} diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/FoundRows.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/FoundRows.java deleted file mode 100644 index af2cc6ab..00000000 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/FoundRows.java +++ /dev/null @@ -1,31 +0,0 @@ -package liquidjava.api.tests; - -import java.util.ArrayList; -import java.util.List; - -import liquidjava.processor.VCImplication; -import liquidjava.rj_language.ast.formatter.VariableFormatter; - -/** - * The rows of Found as the IDE writes them, without the instance counters that depend on verification order - */ -final class FoundRows { - - private FoundRows() { - } - - // binder name, then its refinement - static List rows(VCImplication found) { - List rows = new ArrayList<>(); - for (VCImplication current = found; current != null; current = current.getNext()) { - String refinement = current.getRefinement().getExpression().toDisplayString(); - rows.add(plain(current.hasBinder() ? "∀" + VariableFormatter.format(current.getName()) + " " + refinement - : refinement)); - } - return rows; - } - - static String plain(String text) { - return text.replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", ""); - } -} diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java index 3d86ad05..6f5d44ff 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java @@ -1,7 +1,5 @@ package liquidjava.api.tests; -import static liquidjava.api.tests.FoundRows.plain; -import static liquidjava.api.tests.FoundRows.rows; import static org.junit.jupiter.api.Assertions.*; import java.util.ArrayList; @@ -16,6 +14,8 @@ import liquidjava.diagnostics.Diagnostics; import liquidjava.diagnostics.errors.LJError; import liquidjava.diagnostics.errors.RefinementError; +import liquidjava.processor.VCImplication; +import liquidjava.rj_language.ast.formatter.VariableFormatter; import liquidjava.rj_language.opt.VCSimplificationResult; /** @@ -99,4 +99,19 @@ void writeToAnotherObjectsFieldIsNamedAfterThatObject() { assertEquals(List.of("∀this.level this.level >= 0", "∀other.level other.level == this.level - 1"), ERRORS.get(48).rows()); } + + // the rows of Found as the IDE writes them: binder name, then its refinement + private static List rows(VCImplication found) { + List rows = new ArrayList<>(); + for (VCImplication current = found; current != null; current = current.getNext()) { + String refinement = current.getRefinement().getExpression().toDisplayString(); + rows.add(plain(current.hasBinder() ? "∀" + VariableFormatter.format(current.getName()) + " " + refinement + : refinement)); + } + return rows; + } + + private static String plain(String text) { + return text.replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", ""); + } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundTrueRows.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundTrueRows.java deleted file mode 100644 index 05fc4c9a..00000000 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundTrueRows.java +++ /dev/null @@ -1,60 +0,0 @@ -package liquidjava.api.tests; - -import static liquidjava.api.tests.FoundRows.plain; -import static liquidjava.api.tests.FoundRows.rows; -import static org.junit.jupiter.api.Assertions.*; - -import java.util.List; -import java.util.Map; -import java.util.TreeMap; - -import org.junit.jupiter.api.BeforeAll; -import org.junit.jupiter.api.Test; - -import liquidjava.api.CommandLineLauncher; -import liquidjava.diagnostics.Diagnostics; -import liquidjava.diagnostics.errors.LJError; -import liquidjava.diagnostics.errors.StateRefinementError; - -/** - * Checks that Found for the errors of {@code classes/found_true_rows_error} ends with no bare true row once the binders - * that state nothing are dropped - */ -class TestFoundTrueRows { - - private static final Map ERRORS = new TreeMap<>(); - - @BeforeAll - static void verify() { - CommandLineLauncher.launch("../liquidjava-example/src/main/java/testSuite/classes/found_true_rows_error"); - for (LJError error : Diagnostics.getInstance().getErrors()) - ERRORS.put(error.getPosition().getLine(), assertInstanceOf(StateRefinementError.class, error)); - } - - private static List rowsAt(int line) { - return rows(ERRORS.get(line).getFoundSimplification().getImplication()); - } - - @Test - void foundThatSimplifiesAwayIsTrue() { - assertEquals(List.of("true"), rowsAt(11)); - assertEquals("found true but expected compressionExplicit(wParam)", plain(ERRORS.get(11).getMessage())); - } - - @Test - void pathConditionIsNotFollowedByTrue() { - assertEquals(List.of("∀#fresh baseline || extended"), rowsAt(16)); - assertEquals("found baseline || extended but expected compressionExplicit(wParam)", - plain(ERRORS.get(16).getMessage())); - } - - @Test - void nestedPathConditionsAreNotFollowedByTrue() { - assertEquals(List.of("∀#fresh #fresh == lossless && #fresh", "∀#fresh !extended"), rowsAt(23)); - } - - @Test - void knownStateStaysAfterThePathCondition() { - assertEquals(List.of("∀#fresh #fresh == baseline && #fresh", "∀wParam startCompression(wParam)"), rowsAt(31)); - } -}