From e4c42c1574fb4e2efe3fe852b44c586e216bb1ea Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 14 May 2026 15:50:00 +0100 Subject: [PATCH 1/5] Fix Usage Detection for Repeated Equalities --- .../liquidjava/rj_language/opt/VariableResolver.java | 12 ++++++++---- .../rj_language/opt/ExpressionSimplifierTest.java | 8 ++++++++ .../rj_language/opt/VariableResolverTest.java | 9 +++++++++ 3 files changed, 25 insertions(+), 4 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java index f19f2f8a..637020f1 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java @@ -27,7 +27,7 @@ public static Map resolve(Expression exp) { resolveRecursive(exp, map); // remove variables that were not used in the expression - map.entrySet().removeIf(entry -> !hasUsage(exp, entry.getKey(), entry.getValue())); + map.entrySet().removeIf(entry -> !hasUsage(exp, entry.getKey(), entry.getValue(), true)); // transitively resolve variables return resolveTransitive(map); @@ -136,12 +136,14 @@ private static Expression lookup(Expression exp, Map map, Se * * @param exp * @param name + * @param value + * @param canExcludeDefinition * * @return true if used, false otherwise */ - private static boolean hasUsage(Expression exp, String name, Expression value) { + private static boolean hasUsage(Expression exp, String name, Expression value, boolean canExcludeDefinition) { // exclude own definitions - if (exp instanceof BinaryExpression binary && "==".equals(binary.getOperator())) { + if (canExcludeDefinition && exp instanceof BinaryExpression binary && "==".equals(binary.getOperator())) { Expression left = binary.getFirstOperand(); Expression right = binary.getSecondOperand(); if (left instanceof Var v && v.getName().equals(name) && right.equals(value) @@ -167,8 +169,10 @@ && isConstant(left)) // recurse children if (exp.hasChildren()) { + boolean childCanExcludeDefinition = exp instanceof BinaryExpression binary + && "&&".equals(binary.getOperator()); for (Expression child : exp.getChildren()) - if (hasUsage(child, name, value)) + if (hasUsage(child, name, value, childCanExcludeDefinition)) return true; } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java index f243835f..67ecff69 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java @@ -658,4 +658,12 @@ void testEnumConstantsPropagateIntoTernaryCondition() { assertEquals("start(param)", result.getValue().toString()); } + + @Test + void testRepeatedEqualDefinitionPropagatesIntoTernaryCondition() { + Expression expression = parse("mode == 2 && (mode == 2 ? explicit(param) : start(param))"); + ValDerivationNode result = ExpressionSimplifier.simplify(expression); + + assertEquals("explicit(param)", result.getValue().toString()); + } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java index f85aacc4..10e217d6 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java @@ -99,6 +99,15 @@ void testDifferentEqualityInIteConditionCountsAsUsage() { assertEquals("1", result.get("mode").toString()); } + @Test + void testRepeatedEqualDefinitionCountsAsUsage() { + Expression expression = parse("mode == 2 && (mode == 2 ? explicit(param) : start(param))"); + Map result = VariableResolver.resolve(expression); + + assertEquals(1, result.size(), "Repeated equalities should keep one definition and treat the other as usage"); + assertEquals("2", result.get("mode").toString()); + } + @Test void testReturnVariableIsNotSubstituted() { Expression expression = parse("x > 0 && #ret_1 == x"); From 3153855f2a6f42e8b1efe53a8357d287463ec13f Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 15 May 2026 16:12:29 +0100 Subject: [PATCH 2/5] Refactor `hasUsage` --- .../rj_language/opt/VariableResolver.java | 50 +++++++------------ 1 file changed, 19 insertions(+), 31 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java index 637020f1..32170c79 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java @@ -137,46 +137,34 @@ private static Expression lookup(Expression exp, Map map, Se * @param exp * @param name * @param value - * @param canExcludeDefinition + * @param topLevel * * @return true if used, false otherwise */ - private static boolean hasUsage(Expression exp, String name, Expression value, boolean canExcludeDefinition) { - // exclude own definitions - if (canExcludeDefinition && exp instanceof BinaryExpression binary && "==".equals(binary.getOperator())) { + private static boolean hasUsage(Expression exp, String name, Expression value, boolean topLevel) { + if (topLevel && exp instanceof BinaryExpression binary && "&&".equals(binary.getOperator())) { + return hasUsage(binary.getFirstOperand(), name, value, true) + || hasUsage(binary.getSecondOperand(), name, value, true); + } + + if (topLevel && exp instanceof BinaryExpression binary && "==".equals(binary.getOperator())) { Expression left = binary.getFirstOperand(); Expression right = binary.getSecondOperand(); - if (left instanceof Var v && v.getName().equals(name) && right.equals(value) - && (isConstant(right) || (!(right instanceof Var) && canSubstitute(v, right)))) - return false; - if (left instanceof FunctionInvocation && left.toString().equals(name) && right.equals(value) - && (isConstant(right) || (!(right instanceof Var) && !containsExpression(right, left)))) - return false; - if (right instanceof Var v && v.getName().equals(name) && left.equals(value) && isConstant(left)) - return false; - if (right instanceof FunctionInvocation && right.toString().equals(name) && left.equals(value) - && isConstant(left)) + boolean leftDefinition = name.equals(substitutionKey(left)) && right.equals(value) + && (isConstant(right) + || (left instanceof Var v && !(right instanceof Var) && canSubstitute(v, right)) + || (left instanceof FunctionInvocation && !(right instanceof Var) + && !containsExpression(right, left))); + boolean rightDefinition = name.equals(substitutionKey(right)) && left.equals(value) && isConstant(left); + if (leftDefinition || rightDefinition) return false; } - // usage found - if (exp instanceof Var var && var.getName().equals(name)) { - return true; - } - if (exp instanceof FunctionInvocation && exp.toString().equals(name)) { + if (name.equals(substitutionKey(exp))) return true; - } - - // recurse children - if (exp.hasChildren()) { - boolean childCanExcludeDefinition = exp instanceof BinaryExpression binary - && "&&".equals(binary.getOperator()); - for (Expression child : exp.getChildren()) - if (hasUsage(child, name, value, childCanExcludeDefinition)) - return true; - } - - // usage not found + for (Expression child : exp.getChildren()) + if (hasUsage(child, name, value, false)) + return true; return false; } From 8d46af232330a3d7de5c8cc5697e230d0033cdb5 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 15 May 2026 16:12:51 +0100 Subject: [PATCH 3/5] Add More Tests --- .../opt/ExpressionSimplifierTest.java | 33 +++++++++++++++++++ .../rj_language/opt/VariableResolverTest.java | 20 +++++++++++ 2 files changed, 53 insertions(+) diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java index 67ecff69..b14d3db5 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java @@ -666,4 +666,37 @@ void testRepeatedEqualDefinitionPropagatesIntoTernaryCondition() { assertEquals("explicit(param)", result.getValue().toString()); } + + @Test + void testRepeatedEqualDefinitionsPropagateIntoCompoundTernaryCondition() { + Expression expression = parse( + "mode == 2 && other == 5 && ((mode == 2 && other == 5) ? explicit(param) : start(param))"); + ValDerivationNode result = ExpressionSimplifier.simplify(expression); + + assertEquals("explicit(param)", result.getValue().toString()); + } + + @Test + void testRepeatedEqualDefinitionPropagatesWhenUsageComesFirst() { + Expression expression = parse("(mode == 2 ? explicit(param) : start(param)) && mode == 2"); + ValDerivationNode result = ExpressionSimplifier.simplify(expression); + + assertEquals("explicit(param)", result.getValue().toString()); + } + + @Test + void testRepeatedEqualDefinitionsPropagateIntoNestedTernaryConditions() { + Expression expression = parse("mode == 2 && other == 3 && (mode == 2 ? (other == 3 ? a(p) : b(p)) : c(p))"); + ValDerivationNode result = ExpressionSimplifier.simplify(expression); + + assertEquals("a(p)", result.getValue().toString()); + } + + @Test + void testRepeatedEqualDefinitionsPropagateIntoNestedTernaryElseBranch() { + Expression expression = parse("mode == 2 && other == 4 && (mode == 2 ? (other == 3 ? a(p) : b(p)) : c(p))"); + ValDerivationNode result = ExpressionSimplifier.simplify(expression); + + assertEquals("b(p)", result.getValue().toString()); + } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java index 10e217d6..289a6655 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java @@ -108,6 +108,26 @@ void testRepeatedEqualDefinitionCountsAsUsage() { assertEquals("2", result.get("mode").toString()); } + @Test + void testRepeatedEqualDefinitionsInCompoundIteConditionCountAsUsage() { + Expression expression = parse( + "mode == 2 && other == 5 && ((mode == 2 && other == 5) ? explicit(param) : start(param))"); + Map result = VariableResolver.resolve(expression); + + assertEquals(2, result.size(), "Compound ternary condition should count as a use of both variables"); + assertEquals("2", result.get("mode").toString()); + assertEquals("5", result.get("other").toString()); + } + + @Test + void testRepeatedEqualDefinitionCountsAsUsageBeforeDefinitionConjunct() { + Expression expression = parse("(mode == 2 ? explicit(param) : start(param)) && mode == 2"); + Map result = VariableResolver.resolve(expression); + + assertEquals(1, result.size(), "Conjunct order should not affect repeated equality usage detection"); + assertEquals("2", result.get("mode").toString()); + } + @Test void testReturnVariableIsNotSubstituted() { Expression expression = parse("x > 0 && #ret_1 == x"); From 684b19ead065e503f3bebd032f9d486a5dd319e4 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 15 May 2026 16:19:38 +0100 Subject: [PATCH 4/5] Add More Tests --- .../opt/ExpressionSimplifierTest.java | 8 ++++++ .../rj_language/opt/VariableResolverTest.java | 26 +++++++++++++++++++ 2 files changed, 34 insertions(+) diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java index b14d3db5..31051546 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java @@ -684,6 +684,14 @@ void testRepeatedEqualDefinitionPropagatesWhenUsageComesFirst() { assertEquals("explicit(param)", result.getValue().toString()); } + @Test + void testRepeatedFunctionInvocationDefinitionPropagatesIntoTernaryCondition() { + Expression expression = parse("modeOf(param) == 2 && (modeOf(param) == 2 ? explicit(param) : start(param))"); + ValDerivationNode result = ExpressionSimplifier.simplify(expression); + + assertEquals("explicit(param)", result.getValue().toString()); + } + @Test void testRepeatedEqualDefinitionsPropagateIntoNestedTernaryConditions() { Expression expression = parse("mode == 2 && other == 3 && (mode == 2 ? (other == 3 ? a(p) : b(p)) : c(p))"); diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java index 289a6655..136af9e2 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java @@ -128,6 +128,32 @@ void testRepeatedEqualDefinitionCountsAsUsageBeforeDefinitionConjunct() { assertEquals("2", result.get("mode").toString()); } + @Test + void testRepeatedFunctionInvocationDefinitionCountsAsUsage() { + Expression expression = parse("modeOf(param) == 2 && (modeOf(param) == 2 ? explicit(param) : start(param))"); + Map result = VariableResolver.resolve(expression); + + assertEquals(1, result.size(), "Function invocation definition should count repeated nested equality as usage"); + assertEquals("2", result.get("modeOf(param)").toString()); + } + + @Test + void testRepeatedExpressionDefinitionCountsAsUsage() { + Expression expression = parse("limit == max - 1 && (limit == max - 1 ? a(p) : b(p))"); + Map result = VariableResolver.resolve(expression); + + assertEquals(1, result.size(), "Expression definition should count repeated nested equality as usage"); + assertEquals("max - 1", result.get("limit").toString()); + } + + @Test + void testRepeatedTopLevelDefinitionsOnlyDoNotCountAsUsage() { + Expression expression = parse("mode == 2 && mode == 2"); + Map result = VariableResolver.resolve(expression); + + assertTrue(result.isEmpty(), "Repeated top-level definitions alone should not count as usage"); + } + @Test void testReturnVariableIsNotSubstituted() { Expression expression = parse("x > 0 && #ret_1 == x"); From 7177e4984d877075d6d03883b78b81716bd83e64 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 15 May 2026 16:32:12 +0100 Subject: [PATCH 5/5] Update CONTRIBUTING --- CONTRIBUTING.md | 28 ++++++++++++++++++++-------- 1 file changed, 20 insertions(+), 8 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 6fb8cb1a..84d5eec2 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -7,26 +7,38 @@ Thanks for your interest in contributing! This guide covers the essentials. - Java 20+ - Maven 3.6+ -## Build & test +## Build and Run + +To build the project, run: ```bash -mvn clean install # build everything -mvn test # run the test suite +mvn clean install ``` -Run a single test: +Code formatting runs automatically via `formatter-maven-plugin` during the `validate` phase. + +To verify a single file from the CLI, run: ```bash -mvn -pl liquidjava-verifier -Dtest=TestExamples#testMultiplePaths test +./liquidjava path/to/File.java ``` -Verify a single file from the CLI: +## Testing + +To run all tests, run: ```bash -./liquidjava path/to/File.java +mvn test ``` -Code formatting runs automatically via `formatter-maven-plugin` during the `validate` phase. +To run specific tests, run: + +```bash +mvn -pl liquidjava-verifier -Dtest=ExpressionFormatterTest test +mvn -pl liquidjava-verifier -Dtest=ExpressionSimplifierTest test +mvn -pl liquidjava-verifier -Dtest=RefinementsParserTest test +mvn -pl liquidjava-verifier -Dtest=VariableResolverTest test +``` ## Release