diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateSetNames.java b/liquidjava-example/src/main/java/testSuite/ErrorStateSetNames.java index 144922bc..7a27f3fd 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorStateSetNames.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateSetNames.java @@ -4,7 +4,8 @@ import liquidjava.specification.RefinementPredicate; import liquidjava.specification.StateSet; -// A state set name must be a lowercase identifier that no state, ghost or other state set of the class uses +// A state set name must be a lowercase identifier that no state, ghost or other state set of the class uses, and +// not one of the names given to state sets without a name @StateSet(name = "Door", value = {"closed", "opened"}) // Expect: Error public class ErrorStateSetNames {} @@ -23,3 +24,6 @@ class ErrorStateSetNameOfAnotherSet {} @StateSet(name = "size", value = {"empty", "full"}) // Expect: Error @RefinementPredicate("int size(ErrorStateSetNameOfARefinementPredicate b)") class ErrorStateSetNameOfARefinementPredicate {} + +@StateSet(name = "state2", value = {"closed", "opened"}) // Expect: Error +class ErrorStateSetNameOfAGeneratedName {} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateValueGhostName.java b/liquidjava-example/src/main/java/testSuite/ErrorStateValueGhostName.java new file mode 100644 index 00000000..fbcbc774 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateValueGhostName.java @@ -0,0 +1,21 @@ +package testSuite; + +import liquidjava.specification.Ghost; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// a ghost named like a state of another class is not shown as that state +@Ghost("boolean ready") +public class ErrorStateValueGhostName { + + @StateRefinement(from = "ready(this)") + void use() {} + + static void test() { + ErrorStateValueGhostName sensor = new ErrorStateValueGhostName(); + sensor.use(); // Expect: State Refinement Error + } +} + +@StateSet(name = "phase", value = {"ready", "busy"}) +class ErrorStateValueGhostNameMachine {} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/ErrorMessage.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/ErrorMessage.java index bd6e2153..33c9beaf 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/ErrorMessage.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/ErrorMessage.java @@ -5,6 +5,7 @@ import java.util.ArrayList; import java.util.List; import java.util.function.Predicate; +import java.util.function.UnaryOperator; import liquidjava.diagnostics.TranslationTable; import liquidjava.processor.context.PlacementInCode; @@ -18,10 +19,11 @@ record ErrorMessage(String text, DisplayNames names) { /** * Writes the facts of found about the values expected constrains and expected in frame, or only expected when - * showsFound rejects those facts; path conditions about other values stay in the derivation + * showsFound rejects those facts; path conditions about other values stay in the derivation. The facts are chosen + * on expected and found as given, and written as display rewrites them */ static ErrorMessage of(Expression expected, VCSimplificationResult found, TranslationTable translationTable, - Predicate showsFound, String frame) { + Predicate showsFound, String frame, UnaryOperator display) { Expression shown = linkedToExpected(found.getImplication().toPredicate().getExpression(), expected); // the names of the message first, then those only the original found has, each with the line of its value List message = new ArrayList<>(); @@ -34,9 +36,9 @@ static ErrorMessage of(Expression expected, VCSimplificationResult found, Transl PlacementInCode placement = translationTable == null ? null : translationTable.get(name); return placement == null ? null : placement.getLine(); }); - String expectedText = ExpressionFormatter.format(expected, names); + String expectedText = ExpressionFormatter.format(display.apply(expected), names); String text = showsFound.test(shown) - ? String.format(frame, ExpressionFormatter.format(shown, names), expectedText) + ? String.format(frame, ExpressionFormatter.format(display.apply(shown), names), expectedText) : String.format("expected %s but could not prove it", expectedText); return new ErrorMessage(text, names); } 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 55f5c0a6..775c740b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -7,6 +7,7 @@ import java.util.List; import java.util.Map; import java.util.Set; +import java.util.function.UnaryOperator; import java.util.stream.Collectors; import liquidjava.diagnostics.AliasExpansion; @@ -51,8 +52,10 @@ public class RefinementError extends LJError { public RefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected, VCSimplificationResult found, TranslationTable translationTable, Counterexample counterexample, String customMessage, List aliases) { - super("Refinement Error", ErrorMessage.of(expected.getExpression(), found, translationTable, - shown -> !isTrue(shown), "%s is not a subtype of %s"), position, translationTable, customMessage); + super("Refinement Error", + ErrorMessage.of(expected.getExpression(), found, translationTable, shown -> !isTrue(shown), + "%s is not a subtype of %s", UnaryOperator.identity()), + position, translationTable, customMessage); this.expected = expected; this.found = found; Expression foundExpression = found.getImplication().toPredicate().getExpression(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java index f1e3810a..d1c58ed6 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -3,6 +3,7 @@ import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue; import java.util.List; +import java.util.function.UnaryOperator; import liquidjava.diagnostics.TranslationTable; import liquidjava.diagnostics.categories.ErrorCategory; @@ -26,15 +27,20 @@ public class StateRefinementError extends LJError { private final SourcePosition declarationPosition; private final StateErrorContext context; + /** + * @param display + * rewrites expected and found as the error shows them, here and to the IDE, after the facts to show are + * chosen on them as given + */ public StateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected, VCSimplificationResult found, TranslationTable translationTable, String customMessage, List hints, - ErrorCategory category, StateErrorContext context) { + ErrorCategory category, StateErrorContext context, UnaryOperator display) { super("State Refinement Error", ErrorMessage.of(expected.getExpression(), found, translationTable, - StateRefinementError::appliesGhost, "found %s but expected %s"), position, translationTable, + StateRefinementError::appliesGhost, "found %s but expected %s", display), position, translationTable, customMessage); this.declarationPosition = declarationPosition; - this.expected = expected; - this.found = found; + this.expected = new Predicate(display.apply(expected.getExpression())); + this.found = found.map(display); this.context = context; hints.forEach(this::addHint); setCategory(category); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index 85c0657c..a124092d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -213,7 +213,8 @@ public void registerGhostsAndStateSets(CtElement element) throws LJError { SourcePosition namePosition = nameValue == null ? null : Utils.getAnnotationValuePosition(nameValue); String name = stateSetName(nameValue, namePosition); CtNewArray states = (CtNewArray) ann.getAllValues().get("value"); - GhostFunction g = createStateSet(states, name != null ? name : String.format("state%d", set), element); + GhostFunction g = createStateSet(states, name != null ? name : String.format(Formats.STATE_SET, set), + element); stateSets.put(g, name != null ? namePosition : Utils.getAnnotationValuePosition(states)); checkStatesAreNotInAnotherSet(g, states, setOfState); } @@ -262,6 +263,9 @@ private static String stateSetName(CtExpression nameValue, SourcePosition pos if (!name.matches("[a-z][a-zA-Z0-9_]*") || name.equals(Keys.OLD) || name.equals("true") || name.equals("false")) throw new CustomError(String.format( "State set name '%s' must be an identifier that starts with a lowercase letter", name), position); + if (name.matches(Formats.STATE_SET_NAMES)) + throw new CustomError(String.format("State set name '%s' is kept for state sets without a name", name), + position); return name; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index 7ae0371f..86749010 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java @@ -17,6 +17,7 @@ import liquidjava.processor.VCImplication; import liquidjava.processor.context.*; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.StateValues; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.Ite; import liquidjava.rj_language.ast.Var; @@ -463,7 +464,8 @@ protected void throwStateRefinementError(SourcePosition position, SourcePosition VCSimplificationResult shown = VCSimplification.simplifyOnce(simplified, new VCRelevantFacts(expected.getExpression(), this::ghostFunctionsOf)); throw new StateRefinementError(position, declarationPosition, expected, shown, map, customMessage, hints, - category, context); + category, context, + e -> StateValues.toSetForm(e, this.context.getGhostStates(), this.context.getGhosts())); } /** The ghost functions an invocation name stands for: a state's state set function, or the ghost itself */ diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java index abcc8236..369ac126 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java @@ -16,6 +16,8 @@ import liquidjava.rj_language.ast.FunctionInvocation; import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; +import liquidjava.utils.Utils; +import liquidjava.utils.constants.Formats; /** * Reads a state written as a value of its state set, {@code phase(e) == open}, as the state shorthand {@code open(e)}, @@ -91,6 +93,49 @@ private Optional stateOf(Expression set, Expression name) th return Optional.empty(); } + /** + * {@code expression} with each state of a named set, {@code open(e)}, written as a value of its set, + * {@code phase(e) == open}, and {@code !open(e)} as {@code phase(e) != open}, for display. A state keeps the + * shorthand when its set has a generated name, such as {@code state1}, when sets with different names have a state + * of that name, or when a ghost that is not a state has that name: the name alone does not tell which it is + * + * @param ghosts + * the ghosts that are not states, and the state set functions + */ + public static Expression toSetForm(Expression expression, List states, List ghosts) { + return rewriteToSetForm(expression.clone(), states, ghosts); + } + + private static Expression rewriteToSetForm(Expression e, List states, List ghosts) { + if (e instanceof UnaryExpression u && u.getOp().equals("!")) { + Optional value = setValue(u.getExpression(), "!=", states, ghosts); + if (value.isPresent()) + return value.get(); + } + Optional value = setValue(e, "==", states, ghosts); + if (value.isPresent()) + return value.get(); + for (int i = 0; i < e.getChildren().size(); i++) + e.setChild(i, rewriteToSetForm(e.getChildren().get(i), states, ghosts)); + return e; + } + + /** {@code set(e) op state} when {@code e} is the state {@code state(e)} of a set with one, given name */ + private static Optional setValue(Expression e, String op, List states, + List ghosts) { + if (!(e instanceof FunctionInvocation invocation && invocation.getArgs().size() == 1) + || ghosts.stream().anyMatch(g -> g.matches(invocation.getName())) + || states.stream().anyMatch(s -> s.getParent() == null && s.matches(invocation.getName()))) + return Optional.empty(); + List setNames = states.stream().filter(s -> s.getParent() != null && s.matches(invocation.getName())) + .map(s -> s.getParent().getName()).distinct().toList(); + if (setNames.size() != 1 || setNames.get(0).matches(Formats.STATE_SET_NAMES)) + return Optional.empty(); + FunctionInvocation set = new FunctionInvocation(qualifiedLike(invocation.getName(), setNames.get(0)), + List.of(invocation.getArgs().get(0).clone())); + return Optional.of(new BinaryExpression(set, op, new Var(Utils.getSimpleName(invocation.getName())))); + } + /** The states of {@code set}, or only those named {@code name} when it is not null */ private List statesOf(GhostFunction set, String name) { return states.stream().filter(s -> s.getParent() == set && (name == null || s.getName().equals(name))).toList(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java index b1083f9a..465fedac 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java @@ -2,8 +2,11 @@ import java.util.ArrayList; import java.util.List; +import java.util.function.UnaryOperator; import liquidjava.processor.VCImplication; +import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.Expression; /** * Result of simplifying VC implication chain @@ -65,6 +68,15 @@ public List getBinders() { return binderNames; } + /** This result with each refinement of its chain, and of the chains it was simplified from, rewritten by f */ + public VCSimplificationResult map(UnaryOperator f) { + VCImplication chain = implication.clone(); + for (VCImplication row = chain; row != null; row = row.getNext()) + if (row.getRefinement() != null) + row.setRefinement(new Predicate(f.apply(row.getRefinement().getExpression()))); + return new VCSimplificationResult(chain, origin == null ? null : origin.map(f), simplification); + } + @Override public String toString() { if (origin == null) diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java index f0c63dc0..ba9d2e89 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java @@ -5,4 +5,8 @@ public final class Formats { public static final String THIS = "this#%s"; public static final String RET = "#ret_%d"; public static final String ENUM = "%s.%s"; + /** The name of a state set declared without one, numbered from 1 in the order of the declarations */ + public static final String STATE_SET = "state%d"; + /** The names {@link #STATE_SET} gives, which a state set cannot be given explicitly */ + public static final String STATE_SET_NAMES = "state[1-9][0-9]*"; } \ No newline at end of file diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java index ec988afd..9b6a9c2a 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -343,7 +343,7 @@ void foundOfTheStudysUndoManagerOmitsTheResultsOfOtherCalls() { void foundKeepsANamedStateSetByItsName() { StateRefinementError error = errors("ErrorStateHintMultipleSets.java", 1).get(0); assertEquals( - "found closed(d@26) && locked(d) && doorState(d) == doorState(d@26) but expected closed(d) && unlocked(d)", + "found doorState(d@26) == closed && lockState(d) == locked && doorState(d) == doorState(d@26) but expected doorState(d) == closed && lockState(d) == unlocked", error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", "")); } @@ -354,6 +354,13 @@ void queryWrittenWithItsStateSetIsOfferedAsAGuard() { new Hint(Kind.GUARD, "Guard this call with if (d.isUnlocked()): when it returns true, d is unlocked")); } + @Test + void ghostNamedLikeAStateOfAnotherClassKeepsItsForm() { + StateRefinementError error = errors("ErrorStateValueGhostName.java", 1).get(0); + assertEquals("found ready(sensor) == false but expected ready(sensor)", + error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", "")); + } + @Test void classWithoutStateSetKeepsTheGeneralHint() { assertHints("ErrorUnconstrainedStateRefinement.java", Hint.general( diff --git a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java index aa1d5944..46e51d46 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java @@ -7,6 +7,7 @@ import java.util.Arrays; import java.util.List; +import java.util.function.UnaryOperator; import org.junit.jupiter.api.Test; @@ -143,7 +144,7 @@ void stateMessageKeepsAStateReachingExpectedThroughAnAlias() { new Predicate(RefinementsParser.createAST("full(box)", "")), new VCSimplificationResult( vc("∀b1:Object. empty(b1)", "∀x:int. x > 0", "∀box:Object. box == b1", "true")), - new TranslationTable(), null, List.of(), null, null); + new TranslationTable(), null, List.of(), null, null, UnaryOperator.identity()); assertEquals("found empty(b1) && box == b1 but expected full(box)", error.getMessage()); }