diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 785a8324..6e717e80 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -7,27 +7,40 @@ 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: +This script recompiles `liquidjava-api` and `liquidjava-verifier` when local sources or Maven files have changed. + +## Testing + +To run all tests, run: ```bash -./liquidjava path/to/File.java +mvn test ``` -The launcher recompiles `liquidjava-api` and `liquidjava-verifier` only when local sources or Maven files have changed. -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 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..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 @@ -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,43 +136,35 @@ private static Expression lookup(Expression exp, Map map, Se * * @param exp * @param name + * @param value + * @param topLevel * * @return true if used, false otherwise */ - private static boolean hasUsage(Expression exp, String name, Expression value) { - // exclude own definitions - if (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()) { - for (Expression child : exp.getChildren()) - if (hasUsage(child, name, value)) - return true; - } - - // usage not found + for (Expression child : exp.getChildren()) + if (hasUsage(child, name, value, false)) + return true; return false; } 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..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 @@ -658,4 +658,53 @@ 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()); + } + + @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 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))"); + 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 f85aacc4..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 @@ -99,6 +99,61 @@ 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 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 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");