diff --git a/liquidjava-example/src/main/java/testSuite/classes/generated_names_error/Door.java b/liquidjava-example/src/main/java/testSuite/classes/generated_names_error/Door.java new file mode 100644 index 00000000..fb82dc3d --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/generated_names_error/Door.java @@ -0,0 +1,14 @@ +package testSuite.classes.generated_names_error; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"opened", "closed"}) +public class Door { + + @StateRefinement(to = "closed(this)") + public Door() {} + + @StateRefinement(from = "opened(this)", to = "closed(this)") + public void close() {} +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/generated_names_error/GeneratedNames.java b/liquidjava-example/src/main/java/testSuite/classes/generated_names_error/GeneratedNames.java new file mode 100644 index 00000000..6fa47540 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/generated_names_error/GeneratedNames.java @@ -0,0 +1,60 @@ +package testSuite.classes.generated_names_error; + +import liquidjava.specification.Refinement; + +// Each value the verifier introduces is named after what it is, not #fresh (#373) +public class GeneratedNames { + + static void positive(@Refinement("_ > 0") int x) {} + + @Refinement("_ > 0") + static int negate(@Refinement("_ < 0") int x) { + return -x; + } + + static boolean ready(int a) { + return a > 0; + } + + static int read(int key) { + return key; + } + + static void ifCondition(int a) { + if (ready(a)) + positive(a); // Expect: Refinement Error + } + + static void loopCondition(int a) { + while (ready(a)) + positive(a); // Expect: Refinement Error + } + + static int ternaryCondition(int a) { + return ready(a) ? negate(a) : 1; // Expect: Refinement Error + } + + static void tryAndCatchBranches(int a) { + try { + a = read(a); + } catch (IllegalStateException e) { + a = 1; + } catch (RuntimeException e) { + positive(a); // Expect: Refinement Error + } + } + + static void callResult(int key) { + positive(read(key) - 1); // Expect: Refinement Error + } + + static void operationResult(String s) { + boolean isNull = s == null; + if (isNull) + positive(0); // Expect: Refinement Error + } + + static void newObject() { + new Door().close(); // Expect: State 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 47ef1630..1b82977d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -21,9 +21,9 @@ import liquidjava.rj_language.ast.formatter.VariableFormatter; import liquidjava.rj_language.opt.VCSimplificationResult; import liquidjava.smt.Counterexample; +import liquidjava.utils.GeneratedNames; import liquidjava.utils.Pair; import liquidjava.utils.Utils; -import liquidjava.utils.constants.Formats; import spoon.reflect.cu.SourcePosition; import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue; @@ -184,7 +184,7 @@ private List originalBinders() { private static int relevance(String term, List expectedTerms, List foundTerms) { if (expectedTerms.contains(term)) return foundTerms.contains(term) ? 1 : 0; - return term.startsWith(Formats.FRESH_PREFIX) ? 3 : 2; + return GeneratedNames.isGenerated(term) ? 3 : 2; } // Variables and ghost applications of an expression, named as in the SMT model diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 1891a38d..65f5bf19 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -21,6 +21,7 @@ import liquidjava.rj_language.BuiltinFunctionPredicate; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.Enum; +import liquidjava.utils.GeneratedNames; import liquidjava.utils.StaticConstants; import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; @@ -210,7 +211,7 @@ public void visitCtNewArray(CtNewArray newArray) { // TODO only working for 1 dimension for (CtExpression exp : l) { Predicate c = getExpressionRefinements(exp); - String name = String.format(Formats.FRESH, context.getCounter()); + String name = GeneratedNames.of(GeneratedNames.ARRAY_LENGTH, context.getCounter()); if (c.getVariableNames().contains(Keys.WILDCARD)) { c = c.substituteVariable(Keys.WILDCARD, name); } else { @@ -498,7 +499,7 @@ public void visitCtIf(CtIf ifElement) { CtExpression exp = ifElement.getCondition(); Predicate expRefs = getExpressionRefinements(exp); - String pathVarName = String.format(Formats.FRESH, context.getCounter()); + String pathVarName = GeneratedNames.of(GeneratedNames.IF_CONDITION, context.getCounter()); // A value refinement constrains the result of evaluating the expression; it is not // itself the truth value selecting the branch. Calls without a wildcard likewise // provide no information about their boolean result. @@ -610,14 +611,13 @@ private void keepFreshValues(Predicate predicate) { } private void keepFreshValues(Predicate predicate, Set visited) { - String freshPrefix = Formats.FRESH.substring(0, Formats.FRESH.indexOf('%')); for (String name : predicate.getVariableNames()) { if (!visited.add(name)) continue; RefinedVariable value = context.getVariableByName(name); if (value == null) continue; - if (name.startsWith(freshPrefix)) + if (GeneratedNames.isGenerated(name)) context.addInstanceVariable(value); keepFreshValues(value.getMainRefinement(), visited); } @@ -821,7 +821,7 @@ private static void removeCheckMetadata(CtLoop loop) { private void recordExit(LoopTypestates states, CtExpression condition) { if (condition == null) return; - RefinedVariable conditionIsFalse = assumeCondition(condition, false); + RefinedVariable conditionIsFalse = assumeCondition(condition, false, GeneratedNames.LOOP_CONDITION); states.recordExit(); if (conditionIsFalse != null) vcChecker.removePathVariable(conditionIsFalse); @@ -953,22 +953,22 @@ private boolean mayChangeState(CtInvocation invocation) { * the condition of an if, see visitCtIf). Re-assigning a variable in the body drops the conditions on it. */ private void assumeLoopCondition(CtExpression condition) { - assumeCondition(condition, true); + assumeCondition(condition, true, GeneratedNames.LOOP_CONDITION); } /** * Adds a path condition saying that {@code condition} evaluated to {@code holds}, on the values it was evaluated - * on. Returns the path variable, so the caller can remove it where the condition no longer applies, or null when - * nothing is assumed. + * on, in a path variable named after {@code kind}. Returns the path variable, so the caller can remove it where the + * condition no longer applies, or null when nothing is assumed. */ - private RefinedVariable assumeCondition(CtExpression condition, boolean holds) { + private RefinedVariable assumeCondition(CtExpression condition, boolean holds, String kind) { // conditions with side effects (e.g. (n = read()) > 0) are not encoded, so they assume nothing if (condition == null || !condition.getElements(new TypeFilter<>(CtVariableWrite.class)).isEmpty()) return null; Predicate refs = getRefinement(condition); if (isUninformativeCondition(refs, condition)) return null; - String pathVarName = String.format(Formats.FRESH, context.getCounter()); + String pathVarName = GeneratedNames.of(kind, context.getCounter()); boolean valueIsCondition = refs.getVariableNames().contains(Keys.WILDCARD); refs = refs.substituteVariable(Keys.WILDCARD, pathVarName); refs = Predicate.createConjunction(refs, substituteAllVariablesForLastInstance(refs)); @@ -1006,7 +1006,7 @@ public void visitCtConditional(CtConditional conditional) { } private void scanAssuming(CtExpression branch, CtExpression condition, boolean holds) { - RefinedVariable pathVar = assumeCondition(condition, holds); + RefinedVariable pathVar = assumeCondition(condition, holds, GeneratedNames.TERNARY_CONDITION); scan(branch); if (pathVar != null) vcChecker.removePathVariable(pathVar); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TryChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TryChecker.java index 2b6ef116..a20fd2d8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TryChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TryChecker.java @@ -9,6 +9,7 @@ import liquidjava.processor.context.Variable; import liquidjava.processor.context.VariableInstance; import liquidjava.rj_language.Predicate; +import liquidjava.utils.GeneratedNames; import liquidjava.utils.constants.Formats; import spoon.reflect.code.CtCatch; import spoon.reflect.code.CtExpression; @@ -73,7 +74,8 @@ private boolean visitBranches(CtTry tryBlock, int i, Map void getUnaryOpRefinements(CtUnaryOperator operator) throws LJErro operator.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), value)); return; } - String name = Formats.FRESH; + String name = null; Predicate all; if (ex instanceof CtVariableWrite w) { name = w.getVariable().getSimpleName(); @@ -211,9 +212,8 @@ public void getUnaryOpRefinements(CtUnaryOperator operator) throws LJErro type = operator.getFactory().Type().booleanPrimitiveType(); } Predicate metadata = rtc.getRefinement(ex); - String newName = !name.equals(Formats.FRESH) - ? String.format(Formats.INSTANCE, name, rtc.getContext().getCounter()) - : String.format(name, rtc.getContext().getCounter()); + String newName = name != null ? String.format(Formats.INSTANCE, name, rtc.getContext().getCounter()) + : GeneratedNames.valueOf(ex, rtc.getContext().getCounter()); Predicate newMeta = metadata.substituteVariable(Keys.WILDCARD, newName); Predicate unOp = getOperatorFromKind(operator.getKind(), operator); @@ -254,7 +254,7 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab CtExpression element) throws LJError { if (element instanceof CtFieldRead field) { if (field.getVariable().getSimpleName().equals("length")) { - String name = String.format(Formats.FRESH, rtc.getContext().getCounter()); + String name = GeneratedNames.valueOf(field, rtc.getContext().getCounter()); rtc.getContext().addVarToContext(name, element.getType(), rtc.getRefinement(element).substituteVariable(Keys.WILDCARD, name), field); return Predicate.createVar(name); @@ -327,7 +327,7 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), inv); // TODO REVIEW!! // Substitute _ by the variable that we send - String newName = String.format(Formats.FRESH, rtc.getContext().getCounter()); + String newName = GeneratedNames.valueOf(inv, rtc.getContext().getCounter()); innerRefs = innerRefs.substituteVariable(Keys.WILDCARD, newName); rtc.getContext().addVarToContext(newName, fi.getType(), innerRefs, inv); return new Predicate(newName, inv); // Return variable that represents the invocation @@ -341,7 +341,7 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab * method without refinements */ private Predicate getUnconstrainedInvocationVariable(CtInvocation inv) { - String newName = String.format(Formats.FRESH, rtc.getContext().getCounter()); + String newName = GeneratedNames.valueOf(inv, rtc.getContext().getCounter()); rtc.getContext().addVarToContext(newName, inv.getType(), new Predicate(), inv); return new Predicate(newName, inv); } @@ -365,7 +365,7 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation inv) thr Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), inv); // TODO REVIEW!! // Substitute _ by the variable that we send - String newName = String.format(Formats.FRESH, rtc.getContext().getCounter()); + String newName = GeneratedNames.valueOf(inv, rtc.getContext().getCounter()); innerRefs = innerRefs.substituteVariable(Keys.WILDCARD, newName); // change this for the current instance @@ -476,7 +476,7 @@ private Predicate createFreshValue(CtExpression element, Predicate refinement } private Predicate createFreshValue(CtExpression element, CtTypeReference type, Predicate refinement) { - String newName = String.format(Formats.FRESH, rtc.getContext().getCounter()); + String newName = GeneratedNames.valueOf(element, rtc.getContext().getCounter()); Predicate freshRefinement = refinement.substituteVariable(Keys.WILDCARD, newName); rtc.getContext().addVarToContext(newName, type, freshRefinement, element); return Predicate.createVar(newName); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java index f974424f..3200876b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java @@ -98,7 +98,7 @@ static void transferReturnRefinement(RefinedFunction superFunction, RefinedFunct if (functionRef.isBooleanTrue()) function.setRefinement(superRef); else { - String name = String.format(Formats.FRESH, tc.getContext().getCounter()); + String name = String.format(Formats.RET, tc.getContext().getCounter()); tc.getContext().addVarToContext(name, superFunction.getType(), new Predicate(), method); // functionRef might be stronger than superRef // check (superRef <: functionRef) @@ -138,7 +138,7 @@ private static void transferStateRefinements(RefinedFunction superFunction, Refi ObjectState superState = superStates.get(i); ObjectState subState = subStates.get(i); - String thisName = String.format(Formats.FRESH, tc.getContext().getCounter()); + String thisName = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter()); createVariableInContext(thisName, tc, subFunction, superFunction, method); Predicate superConst = matchVariableNames(thisName, superState.getFrom()); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 60349ca1..f1ce3d1c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -23,6 +23,7 @@ import liquidjava.processor.state_machine.StateMachineBuilder; import liquidjava.processor.state_machine.StateSolver; import liquidjava.rj_language.Predicate; +import liquidjava.utils.GeneratedNames; import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; @@ -1090,7 +1091,7 @@ public static String prepareInvocationTarget(TypeChecker tc, CtElement target2, && newCall.getMetadata(Keys.REFINEMENT)instanceof Predicate state) { // `new T(args).method()`: the receiver is a fresh object in the state the constructor gives. Must come // before the TARGET case: a constructor with refined parameters puts its (void) return value in TARGET - String name = String.format(Formats.FRESH, tc.getContext().getCounter()); + String name = GeneratedNames.valueOf(newCall, tc.getContext().getCounter()); RefinedVariable receiver = tc.getContext().addInstanceToContext(name, newCall.getType(), state.substituteVariable(Keys.THIS, name).substituteVariable(Keys.WILDCARD, name), newCall); newCall.putMetadata(Keys.TARGET, receiver); @@ -1105,7 +1106,7 @@ public static String prepareInvocationTarget(TypeChecker tc, CtElement target2, && !isReturnValue(call)) { // `a.get().method()` where get() has no return refinement: the call's TARGET is its own receiver (a), not // the value it returns, so the receiver is a fresh value of the call's type, in a state not known here - String name = String.format(Formats.FRESH, tc.getContext().getCounter()); + String name = GeneratedNames.valueOf(call, tc.getContext().getCounter()); RefinedVariable receiver = tc.getContext().addInstanceToContext(name, call.getType(), new Predicate(), call); call.putMetadata(Keys.RECEIVER, receiver); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java index 7ec4f128..8a1d57fd 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java @@ -28,7 +28,7 @@ public static String format(String name) { String receiver = FieldDisplayNames.writeReceiver(name); if (receiver != null && isField(baseName)) return (receiver.isEmpty() ? "" : receiver + ".") + fieldOf(baseName) + toSuperscript(counter); - String prefix = isSpecialIdentifier(baseName) ? "#" : ""; + String prefix = isReturn(baseName) ? "#" : ""; return prefix + formatField(baseName) + toSuperscript(counter); } @@ -80,8 +80,8 @@ private static String toSuperscript(String number) { return sb.toString(); } - private static boolean isSpecialIdentifier(String id) { - return id.equals("fresh") || id.equals("ret"); + private static boolean isReturn(String id) { + return id.equals("ret"); } private static boolean isApplication(String name) { 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..17aad61d 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 @@ -11,15 +11,13 @@ import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.LiteralBoolean; import liquidjava.rj_language.ast.Var; -import liquidjava.utils.constants.Formats; +import liquidjava.utils.GeneratedNames; /** * Simplifies VCImplication chains by removing vacuous binder implications */ public class VCBinderSimplification implements VCSimplificationPass { - private static final String FRESH_PREFIX = Formats.FRESH_PREFIX; - private final NeededVariables needed; public VCBinderSimplification() { @@ -95,7 +93,7 @@ private boolean isRemovableBinder(VCImplication implication, Set keptTru * Checks for a generated boolean path binder refined exactly by itself */ private boolean isUnusedFreshPathBinder(VCImplication implication) { - if (!implication.hasNext() || !implication.getName().startsWith(FRESH_PREFIX) + if (!implication.hasNext() || !GeneratedNames.isGenerated(implication.getName()) || !"boolean".equals(implication.getType().getQualifiedName())) return false; diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/GeneratedNames.java b/liquidjava-verifier/src/main/java/liquidjava/utils/GeneratedNames.java new file mode 100644 index 00000000..e1633778 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/GeneratedNames.java @@ -0,0 +1,65 @@ +package liquidjava.utils; + +import java.util.regex.Pattern; + +import spoon.reflect.code.CtBinaryOperator; +import spoon.reflect.code.CtConstructorCall; +import spoon.reflect.code.CtExpression; +import spoon.reflect.code.CtFieldRead; +import spoon.reflect.code.CtInvocation; +import spoon.reflect.code.CtUnaryOperator; + +/** + * Names of the values the verifier introduces, such as path conditions and call results. Each is written + * {@code ##_}, so that error messages say what the value stands for. The counter keeps it + * unique, and the second {@code #} keeps it apart from the instances of program variables, + * {@code #_}, as a Java name cannot start with {@code #}. + */ +public final class GeneratedNames { + public static final String IF_CONDITION = "if_condition"; + public static final String LOOP_CONDITION = "loop_condition"; + public static final String TERNARY_CONDITION = "ternary_condition"; + public static final String TRY_BRANCH = "try_branch"; + public static final String CATCH_BRANCH = "catch_branch"; + public static final String ARRAY_LENGTH = "array_length"; + + private static final String RESULT = "_result"; + private static final String VALUE = "_value"; + private static final String NEW = "new_"; + private static final String OPERATION_RESULT = "operation" + RESULT; + private static final String EXPRESSION_VALUE = "expression" + VALUE; + + private static final String PREFIX = "##"; + private static final Pattern NOT_IN_IDENTIFIER = Pattern.compile("[^A-Za-z0-9_]"); + + private GeneratedNames() { + } + + public static String of(String description, int counter) { + return String.format(PREFIX + "%s_%d", NOT_IN_IDENTIFIER.matcher(description).replaceAll("_"), counter); + } + + /** + * Names the value of an expression after what it is: {@code ##size_result_3} for a call to {@code size}, + * {@code ##count_value_3} for a read of field {@code count}, {@code ##new_File_3} for a new {@code File} + */ + public static String valueOf(CtExpression expression, int counter) { + return of(describe(expression), counter); + } + + public static boolean isGenerated(String name) { + return name.startsWith(PREFIX); + } + + private static String describe(CtExpression expression) { + if (expression instanceof CtInvocation invocation) + return invocation.getExecutable().getSimpleName() + RESULT; + if (expression instanceof CtConstructorCall constructorCall) + return NEW + constructorCall.getType().getSimpleName(); + if (expression instanceof CtFieldRead fieldRead) + return fieldRead.getVariable().getSimpleName() + VALUE; + if (expression instanceof CtBinaryOperator || expression instanceof CtUnaryOperator) + return OPERATION_RESULT; + return EXPRESSION_VALUE; + } +} 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 1b6d7acb..f0c63dc0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java @@ -1,8 +1,6 @@ package liquidjava.utils.constants; public final class Formats { - public static final String FRESH_PREFIX = "#fresh_"; - public static final String FRESH = FRESH_PREFIX + "%d"; public static final String INSTANCE = "#%s_%d"; public static final String THIS = "this#%s"; public static final String RET = "#ret_%d"; diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java index 6c6e5568..59bc0501 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestCounterexamples.java @@ -116,7 +116,7 @@ void fieldArgumentKeepsTheField() { @Test void callInsideArgumentKeepsItsResultAfterTheArgument() { RefinementError error = verify("ErrorCounterexampleCallArgument.java"); - assertAssignments(error, assignment("#timeout", "-1"), assignment("#fresh", "0")); + assertAssignments(error, assignment("#timeout", "-1"), assignment("##read_result", "0")); } @Test diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestGeneratedNames.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestGeneratedNames.java new file mode 100644 index 00000000..86e3fc00 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestGeneratedNames.java @@ -0,0 +1,33 @@ +package liquidjava.api.tests; + +import static org.junit.jupiter.api.Assertions.assertEquals; + +import java.util.Map; +import java.util.stream.Collectors; + +import org.junit.jupiter.api.Test; + +import liquidjava.api.CommandLineLauncher; +import liquidjava.diagnostics.Diagnostics; + +/** + * Checks that the messages for {@code classes/generated_names_error} name each value the verifier introduces after what + * it is, without the instance counters that depend on verification order + */ +class TestGeneratedNames { + + @Test + void namesEachGeneratedValueAfterWhatItIs() { + CommandLineLauncher.launch("../liquidjava-example/src/main/java/testSuite/classes/generated_names_error"); + Map messages = Diagnostics.getInstance().getErrors().stream().collect(Collectors.toMap( + error -> error.getPosition().getLine(), error -> error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", ""))); + + assertEquals(Map.of(25, "#if_condition == ready && #if_condition is not a subtype of a > 0", 30, + "#loop_condition == ready && #loop_condition == true is not a subtype of a > 0", 34, + "#ternary_condition == ready && #ternary_condition == true is not a subtype of a < 0", 43, + "!#try_branch && !#catch_branch is not a subtype of a > 0", 48, + "x == #read_result - 1 is not a subtype of x > 0", 54, + "#if_condition == #operation_result && #if_condition && x == 0 is not a subtype of x > 0", 58, + "found closed(#new_Door) but expected opened(#new_Door)"), messages); + } +} 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 5beb4df9..d9930d5d 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java @@ -44,10 +44,11 @@ void keepsFoundConjunctsLinkedThroughAnEqualityChain() { @Test void omitsUnmentionedPathBinderAndListsGeneratedNamesLast() { - RefinementError error = error("t >= 0", vc("∀#fresh_1:int. true", "∀port:int. true", - "∀#fresh_2:boolean. port > 0", "∀t:int. t == #fresh_1 + port", "true"), "#fresh_2=false", "t=-1", - "#fresh_1=-2", "port=1"); - assertEquals(List.of(pair("t", "-1"), pair("port", "1"), pair("#fresh_1", "-2")), + RefinementError error = error("t >= 0", + vc("∀##read_result_1:int. true", "∀port:int. true", "∀##if_condition_2:boolean. port > 0", + "∀t:int. t == ##read_result_1 + port", "true"), + "##if_condition_2=false", "t=-1", "##read_result_1=-2", "port=1"); + assertEquals(List.of(pair("t", "-1"), pair("port", "1"), pair("##read_result_1", "-2")), error.getCounterexample().assignments()); } @@ -90,7 +91,7 @@ void hasNoCounterexampleWhenFoundStatesEveryValue() { void splitsNegatedDisjunctionsSoEachGuardLinksOnlyItsOwnVariables() { RefinementError error = error("t >= 0", vc("∀port:int. true", "∀retries:int. true", "∀t:int. true", - "∀#fresh_1:boolean. !(port < 0 || retries < 0 || t > 100)", "true"), + "∀##if_condition_1:boolean. !(port < 0 || retries < 0 || t > 100)", "true"), "port=0", "retries=0", "t=-1"); assertEquals(List.of(pair("t", "-1")), error.getCounterexample().assignments()); } @@ -99,15 +100,17 @@ void splitsNegatedDisjunctionsSoEachGuardLinksOnlyItsOwnVariables() { void splitsNestedConjunctionsAndDoubleNegations() { RefinementError error = error("t >= 0", vc("∀port:int. true", "∀retries:int. true", "∀backoff:int. true", "∀t:int. true", - "∀#fresh_1:boolean. !(port < 0 || !!(retries > 3 && backoff > 1) || t > 100)", "true"), + "∀##if_condition_1:boolean. !(port < 0 || !!(retries > 3 && backoff > 1) || t > 100)", "true"), "port=0", "retries=0", "backoff=0", "t=-1"); assertEquals(List.of(pair("t", "-1")), error.getCounterexample().assignments()); } @Test void keepsAGuardThatRelatesExpectedToAnotherVariable() { - RefinementError error = error("t >= 0", vc("∀port:int. true", "∀retries:int. true", "∀t:int. true", - "∀#fresh_1:boolean. !(port < 0 || retries > t)", "true"), "port=0", "retries=-2", "t=-1"); + RefinementError error = error("t >= 0", + vc("∀port:int. true", "∀retries:int. true", "∀t:int. true", + "∀##if_condition_1:boolean. !(port < 0 || retries > t)", "true"), + "port=0", "retries=-2", "t=-1"); assertEquals(List.of(pair("t", "-1"), pair("retries", "-2")), error.getCounterexample().assignments()); } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/VariableFormatterTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/VariableFormatterTest.java index 508972c5..2ea3c9d6 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/VariableFormatterTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/VariableFormatterTest.java @@ -16,13 +16,15 @@ void forgetRecordedNames() { void formatsVariables() { assertEquals("x", VariableFormatter.format("x")); assertEquals("x²", VariableFormatter.format("#x_2")); - assertEquals("#fresh¹²", VariableFormatter.format("#fresh_12")); + assertEquals("#if_condition¹²", VariableFormatter.format("##if_condition_12")); + assertEquals("#size_result⁴", VariableFormatter.format("##size_result_4")); + assertEquals("size_result⁴", VariableFormatter.format("#size_result_4")); assertEquals("#ret³", VariableFormatter.format("#ret_3")); assertEquals("this#Class", VariableFormatter.format("this#Class")); // ghost applications assertEquals("size(s²)", VariableFormatter.format("size(#s_2)")); assertEquals("size(bag)", VariableFormatter.format("size(bag)")); - assertEquals("at(list³, #fresh¹²)", VariableFormatter.format("at(#list_3, #fresh_12)")); + assertEquals("at(list³, #get_result¹²)", VariableFormatter.format("at(#list_3, ##get_result_12)")); assertEquals("size(this)", VariableFormatter.format("size(this)")); assertEquals("f(g(a¹, b²), c³)", VariableFormatter.format("f(g(#a_1, #b_2), #c_3)")); assertEquals("f(g(h(a¹)), b)", VariableFormatter.format("f(g(h(#a_1)),b)")); 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..37d74423 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 @@ -30,7 +30,8 @@ void removesTrueBinderWhenVariableIsUnusedDownstream() { @Test void removesFreshPathBinderWhenVariableIsUnusedDownstream() { - assertSimplificationSteps(binderSimplification, vc("∀#fresh_1:boolean. #fresh_1", "y > 0"), step("y > 0")); + assertSimplificationSteps(binderSimplification, vc("∀##if_condition_1:boolean. ##if_condition_1", "y > 0"), + step("y > 0")); } @Test diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCConstraintSimplificationTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCConstraintSimplificationTest.java index d5958e2c..7a7facb4 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCConstraintSimplificationTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCConstraintSimplificationTest.java @@ -43,8 +43,8 @@ void removesConstraintImpliedByEarlierAntecedent() { @Test void removesCoverageConstraintsImpliedByStrongerLaterConstraints() { assertSimplificationSteps(simplification, - vc("∀x:int. x >= 0", "∀#fresh_40:boolean. !(y < 40)", "∀#fresh_60:boolean. !(y < 60)", - "∀#fresh_80:boolean. !(y < 80)", "x + y > 0"), + vc("∀x:int. x >= 0", "∀##if_condition_40:boolean. !(y < 40)", "∀##if_condition_60:boolean. !(y < 60)", + "∀##if_condition_80:boolean. !(y < 80)", "x + y > 0"), step("x >= 0", "!(y < 60)", "!(y < 80)", "x + y > 0"), step("x >= 0", "!(y < 80)", "x + y > 0")); } @@ -74,7 +74,7 @@ void doesNotUseConclusionToSimplifyConstraint() { @Test void simplifiesOnlyFirstImpliedConstraint() { assertSimplificationSteps(simplification, - vc("∀x:int. x > 2", "∀#fresh_1:boolean. x > 1", "∀#fresh_2:boolean. x > 0", "y > 0"), + vc("∀x:int. x > 2", "∀##if_condition_1:boolean. x > 1", "∀##if_condition_2:boolean. x > 0", "y > 0"), step("x > 2", "x > 0", "y > 0"), step("x > 2", "y > 0")); } }