diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStaticFinalConstantName.java b/liquidjava-example/src/main/java/testSuite/ErrorStaticFinalConstantName.java new file mode 100644 index 00000000..cba965d5 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStaticFinalConstantName.java @@ -0,0 +1,21 @@ +package testSuite; + +import javax.imageio.ImageWriteParam; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +public class ErrorStaticFinalConstantName { + + static void setProgressiveMode(@Refinement("_ != ImageWriteParam.MODE_EXPLICIT") int mode) { + } + + static void direct() { + setProgressiveMode(ImageWriteParam.MODE_EXPLICIT); // Expect: Refinement Error + } + + static void throughLocal() { + int mode = ImageWriteParam.MODE_EXPLICIT; + setProgressiveMode(mode); // Expect: Refinement Error + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index 22e275b8..47f4226a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -187,8 +187,11 @@ private static boolean isKnown(Pair assignment, List || states(binary.getSecondOperand(), binary.getFirstOperand(), assignment))); } - // An enum constant is written Format.JPG in found, either as such or as a variable, and JPG in the model + // An enum constant is written Format.JPG in found, either as such or as a variable, and JPG in the model; a static + // final constant keeps its name in found and is its value in the model private static boolean states(Expression term, Expression value, Pair assignment) { + if (value instanceof Enum constant && constant.getResolvedLiteral() != null) + value = constant.getResolvedLiteral(); String valueName = value instanceof Enum constant ? constant.getConstName() : value instanceof Var var ? Utils.getSimpleName(var.getName()) : value.toString(); return assignment.first().equals(termName(term)) && assignment.second().equals(valueName); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java index 54b6bff7..363c0d2f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java @@ -23,9 +23,6 @@ protected Expression simplify(Expression expression, Void context) { * Folds the first foldable expression found */ private Expression fold(Expression expression) { - // enum constant -> literal - if (expression instanceof Enum en && en.getResolvedLiteral() != null) - return en.getResolvedLiteral().clone(); if (expression instanceof BinaryExpression binary) return foldBinary(binary); if (expression instanceof UnaryExpression unary) @@ -51,7 +48,7 @@ private Expression foldBinary(BinaryExpression binary) { String op = binary.getOperator(); - Expression foldedBinary = foldLiteralBinary(left, right, op); + Expression foldedBinary = foldLiteralBinary(valueOf(left), valueOf(right), op); if (foldedBinary != null) return foldedBinary; @@ -72,17 +69,18 @@ private Expression foldUnary(UnaryExpression unary) { return new UnaryExpression(unary.getOp(), foldedOperand); String op = unary.getOp(); + Expression value = valueOf(operand); // !true -> false // !false -> true - if ("!".equals(op) && operand instanceof LiteralBoolean literal) + if ("!".equals(op) && value instanceof LiteralBoolean literal) return new LiteralBoolean(!literal.isBooleanTrue()); if ("-".equals(op)) { // -(x) -> -x - if (operand instanceof LiteralInt literal) + if (value instanceof LiteralInt literal) return new LiteralInt(-literal.getValue()); - if (operand instanceof LiteralReal literal) + if (value instanceof LiteralReal literal) return new LiteralReal(-literal.getValue()); } @@ -97,7 +95,7 @@ private Expression foldIte(Ite ite) { // true ? x : y -> x // false ? x : y -> y - if (condition instanceof LiteralBoolean literal) + if (valueOf(condition)instanceof LiteralBoolean literal) return literal.isBooleanTrue() ? ite.getThen().clone() : ite.getElse().clone(); Expression foldedCondition = fold(condition); @@ -121,6 +119,14 @@ private Expression foldIte(Ite ite) { return new Ite(condition, thenExpression, elseExpression); } + /** + * The value of a static final constant, which only replaces its name when the expression around it folds, so a + * constant compared with a variable keeps the name the code or the spec wrote + */ + private Expression valueOf(Expression expression) { + return expression instanceof Enum en && en.getResolvedLiteral() != null ? en.getResolvedLiteral() : expression; + } + /** * Folds a binary expression whose operands are both literals */ diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStaticConstantNames.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStaticConstantNames.java new file mode 100644 index 00000000..c5aaaf92 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStaticConstantNames.java @@ -0,0 +1,43 @@ +package liquidjava.api.tests; + +import static org.junit.jupiter.api.Assertions.*; + +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.RefinementError; + +/** Checks that a static final constant the code passes is shown by its name, as the spec writes it */ +class TestStaticConstantNames { + + private static final Map ERRORS = new TreeMap<>(); + + @BeforeAll + static void verify() { + CommandLineLauncher.launch("../liquidjava-example/src/main/java/testSuite/ErrorStaticFinalConstantName.java"); + for (LJError error : Diagnostics.getInstance().getErrors()) + ERRORS.put(error.getPosition().getLine(), assertInstanceOf(RefinementError.class, error)); + } + + @Test + void constantPassedDirectlyKeepsItsName() { + assertShowsName(ERRORS.get(14)); + } + + @Test + void constantPassedThroughLocalKeepsItsName() { + assertShowsName(ERRORS.get(19)); + } + + private static void assertShowsName(RefinementError error) { + assertEquals("mode == ImageWriteParam.MODE_EXPLICIT is not a subtype of mode != ImageWriteParam.MODE_EXPLICIT", + error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", "")); + assertTrue(error.getCounterexample().isEmpty()); + } +} diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java index 0c23c4f1..9c2924ab 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java @@ -6,6 +6,7 @@ import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Enum; import liquidjava.rj_language.ast.LiteralInt; +import liquidjava.rj_language.ast.Var; import org.junit.jupiter.api.Test; class VCFoldingTest { @@ -120,7 +121,7 @@ void foldsResolvedEnumLiterals() { VCImplication implication = new VCImplication( new Predicate(new BinaryExpression(limit, "==", new LiteralInt(3)))); - assertSimplificationSteps(folding, implication, step("3 == 3"), step("true")); + assertSimplificationSteps(folding, implication, step("true")); } @Test @@ -131,6 +132,15 @@ void foldsResolvedEnumLiteralsInsideLargerExpression() { VCImplication implication = new VCImplication( new Predicate(new BinaryExpression(arithmetic, "==", new LiteralInt(5)))); - assertSimplificationSteps(folding, implication, step("3 + 2 == 5"), step("5 == 5"), step("true")); + assertSimplificationSteps(folding, implication, step("5 == 5"), step("true")); + } + + @Test + void keepsResolvedEnumNameWhenNothingFolds() { + Enum mode = new Enum("ImageWriteParam", "MODE_EXPLICIT"); + mode.setResolvedLiteral(new LiteralInt(2)); + VCImplication implication = new VCImplication(new Predicate(new BinaryExpression(new Var("x"), "==", mode))); + + assertSimplificationSteps(folding, implication, step("x == ImageWriteParam.MODE_EXPLICIT")); } }