Leave a guard's arguments for the caller and name parameters that conditions mention

A guard is written as if (l.tryLock(...)), with the declaration tryLock(long timeout)
to fill in, since the callee's parameter names are not in scope where the call is made.
Argument conditions and deciding arguments show the parameters' names too, so
"with lo < hi" says which argument is which. The path search ranks paths that need no
argument conditions first before capping the paths to each set of states.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Author: CatarinaGamboa

liquidjava-example/src/main/java/testSuite/ErrorStateHintGuards.java

@@ -13,7 +13,7 @@ static void negated() {
         c.send(); // Expect: State Refinement Error
     }
 
-    // known state with no sequence of calls to the needed state: the check, with its parameter
+    // known state with no sequence of calls to the needed state: the check, with its parameters for the caller to fill in
     static void withParameter() {
         GuardLock l = new GuardLock();
         l.unlock(); // Expect: State Refinement Error

liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java

@@ -84,8 +84,10 @@ public static List<Hint> forCall(StateMachine machine, RefinedFunction call, Set
     /** The earlier call whose arguments decided the receiver's state, and values that would allow the call */
     public static Hint decidingArgument(DecidingArgument deciding, String receiver) {
         RefinedFunction function = deciding.call().function();
-        String call = CtExecutableReference.CONSTRUCTOR_NAME.equals(function.getName()) ? constructor(function)
-                : receiver + "." + signature(function);
+        // the values name the parameters, so the call shows their names
+        String call = CtExecutableReference.CONSTRUCTOR_NAME.equals(function.getName())
+                ? "new " + Utils.getSimpleName(function.getTargetClass()) + namedParameters(function)
+                : receiver + "." + declaration(function);
         String values = deciding.values().isEmpty() ? "other arguments" : deciding.values().entrySet().stream()
                 .map(e -> e.getKey() + " == " + e.getValue()).collect(Collectors.joining(" and "));
         return new Hint(Kind.DECIDING_ARGUMENT,
@@ -152,9 +154,11 @@ private List<Hint> guard(Set<State> current, RefinedFunction call) {
             return List.of();
         CallVariant guard = guards.get(0);
         boolean negated = guard.negatedResult();
-        String check = (negated ? "!" : "") + invocation(guard.method());
-        String message = String.format("Guard this call with if (%s): when it returns %s, %s is %s", check, !negated,
-                receiver, needed());
+        String check = (negated ? "!" : "") + guardCall(guard.method());
+        String arguments = guard.method().getArguments().isEmpty() ? ""
+                : ", filling in the arguments of " + declaration(guard.method());
+        String message = String.format("Guard this call with if (%s)%s: when it returns %s, %s is %s", check, arguments,
+                !negated, receiver, needed());
         return List.of(new Hint(Kind.GUARD, message));
     }
 
@@ -208,20 +212,32 @@ private String call(RefinedFunction method) {
         return receiver + "." + signature(method);
     }
 
-    /** A call as written in code, with the parameters' names as its arguments, e.g. {@code l.tryLock(timeout)} */
-    private String invocation(RefinedFunction method) {
-        return receiver + "." + Utils.getSimpleName(method.getName())
-                + method.getArguments().stream().map(Variable::getName).collect(Collectors.joining(", ", "(", ")"));
+    /**
+     * A call as written in code, with {@code ...} for arguments the caller must supply, e.g. {@code l.tryLock(...)}:
+     * the parameters' names are not in scope where the call is made
+     */
+    private String guardCall(RefinedFunction method) {
+        String arguments = method.getArguments().isEmpty() ? "()" : "(...)";
+        return receiver + "." + Utils.getSimpleName(method.getName()) + arguments;
+    }
+
+    /**
+     * A method with its parameters' types and names, e.g. {@code tryLock(long timeout)}, for hints that mention the
+     * parameters by name
+     */
+    private static String declaration(RefinedFunction method) {
+        return Utils.getSimpleName(method.getName()) + namedParameters(method);
     }
 
     /**
      * A step of a sequence, with the condition on its arguments if it has one, e.g.
-     * {@code p.setMode(int) with mode == 2}
+     * {@code p.setMode(int mode) with mode == 2}
      */
     private String call(CallVariant step) {
-        String condition = step.kind() == CallVariant.Kind.ARGUMENTS
-                ? " with " + step.condition().getExpression().toDisplayString() : "";
-        return call(step.method()) + condition;
+        if (step.kind() != CallVariant.Kind.ARGUMENTS)
+            return call(step.method());
+        return receiver + "." + declaration(step.method()) + " with "
+                + step.condition().getExpression().toDisplayString();
     }
 
     /** A method as shown in hints, e.g. {@code open(int)} */
@@ -233,6 +249,11 @@ private static String constructor(RefinedFunction constructor) {
         return "new " + Utils.getSimpleName(constructor.getTargetClass()) + parameters(constructor);
     }
 
+    private static String namedParameters(RefinedFunction function) {
+        return function.getArguments().stream().map(v -> v.getType().getSimpleName() + " " + v.getName())
+                .collect(Collectors.joining(", ", "(", ")"));
+    }
+
     private static String parameters(RefinedFunction function) {
         return function.getArguments().stream().map(Variable::getType).map(CtTypeReference::getSimpleName)
                 .collect(Collectors.joining(", ", "(", ")"));

liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/DecidingArgument.java

@@ -99,8 +99,7 @@ private static Optional<Map<String, String>> valuesAllowing(TypeChecker tc, Stat
             for (Variable parameter : function.getArguments())
                 to = leaveFree(context, to, parameter.getName(), parameter.getType(), parameter.getName(), free, types,
                         invocation);
-            boolean returnsValue = function.getType() != null && !"void".equals(function.getType().toString());
-            to = returnsValue
+            to = StateMachineBuilder.returnsValue(function)
                     ? leaveFree(context, to, Keys.WILDCARD, function.getType(), RESULT, free, types, invocation)
                     : to.substituteVariable(Keys.WILDCARD, OBJECT);
 

liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/SolverEffects.java

@@ -124,17 +124,16 @@ public Set<State> after(int index, State state) {
 
     private Optional<Set<State>> computeAfter(int index, State state, Set<State> candidates) {
         return withScope(() -> {
-            State s = state;
             if (query != null) {
-                Predicate known = Predicate.createConjunction(before(s),
+                Predicate known = Predicate.createConjunction(before(state),
                         Predicate.createConjunction(query.substituteVariable(Keys.THIS, BEFORE), condition));
-                return possibleStates(Set.of(s), known, BEFORE);
+                return possibleStates(Set.of(state), known, BEFORE);
             }
             ObjectState change = changes.get(index);
             if (!change.hasTo())
-                return Set.of(s);
+                return Set.of(state);
             Predicate to = change.getTo().substituteVariable(Keys.THIS, AFTER).changeOldMentions(BEFORE, AFTER);
-            Predicate known = Predicate.createConjunction(before(s), to);
+            Predicate known = Predicate.createConjunction(before(state), to);
             if (onResult)
                 known = Predicate.createConjunction(known, condition);
             Set<State> next = possibleStates(candidates, known, AFTER);

liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java

@@ -2,6 +2,7 @@
 
 import java.util.ArrayList;
 import java.util.Collection;
+import java.util.Comparator;
 import java.util.Collections;
 import java.util.HashSet;
 import java.util.LinkedHashMap;
@@ -197,15 +198,16 @@ public Optional<List<List<CallVariant>>> shortestPaths(Set<State> current, Refin
                     if (visited.contains(reached))
                         continue;
                     List<List<CallVariant>> reachedPaths = next.computeIfAbsent(reached, k -> new ArrayList<>());
-                    paths.stream().limit(limit - reachedPaths.size()).map(path -> append(path, step))
-                            .forEach(reachedPaths::add);
+                    paths.stream().map(path -> append(path, step)).forEach(reachedPaths::add);
                 }
             });
+            // capped only once every path to a set is known, so that paths needing no arguments are the ones kept
+            next.replaceAll((states, paths) -> paths.stream().sorted(Comparator.comparingLong(StateMachine::conditions))
+                    .limit(limit).toList());
             List<List<CallVariant>> found = next.entrySet().stream().filter(e -> allows(e.getKey(), call))
                     .flatMap(e -> e.getValue().stream()).toList();
             if (!found.isEmpty()) {
-                List<List<CallVariant>> unconditioned = found.stream()
-                        .filter(p -> p.stream().noneMatch(v -> v.kind() == CallVariant.Kind.ARGUMENTS)).toList();
+                List<List<CallVariant>> unconditioned = found.stream().filter(p -> conditions(p) == 0).toList();
                 return Optional.of((unconditioned.isEmpty() ? found : unconditioned).stream().limit(limit).toList());
             }
             visited.addAll(next.keySet());
@@ -260,6 +262,11 @@ private Optional<Transition> transition(State from, RefinedFunction method) {
         return transitions.stream().filter(t -> t.from().equals(from) && t.method().equals(method)).findFirst();
     }
 
+    /** The steps of {@code path} that need arguments meeting a condition */
+    private static long conditions(List<CallVariant> path) {
+        return path.stream().filter(v -> v.kind() == CallVariant.Kind.ARGUMENTS).count();
+    }
+
     private static List<CallVariant> append(List<CallVariant> path, CallVariant method) {
         List<CallVariant> extended = new ArrayList<>(path);
         extended.add(method);

liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java

@@ -400,7 +400,7 @@ private static boolean returnsBoolean(RefinedFunction function) {
         return function.getType() != null && Types.BOOLEAN.equals(function.getType().toString());
     }
 
-    private static boolean returnsValue(RefinedFunction function) {
+    static boolean returnsValue(RefinedFunction function) {
         return function.getType() != null && !"void".equals(function.getType().toString());
     }
 

liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java

@@ -55,7 +55,7 @@ void finalStateSuggestsCreatingANewObject() {
     @Test
     void transitionDependingOnArgumentsIsSuggestedWithItsConditionButPreventsClaimingStateIsFinal() {
         assertHints("ErrorStateHintIncomplete.java", new Hint(Kind.CALL_SEQUENCE,
-                "Call f.reopen(int) with attempts > 0 before this call to move f from closed to open"));
+                "Call f.reopen(int attempts) with attempts > 0 before this call to move f from closed to open"));
     }
 
     @Test
@@ -244,13 +244,13 @@ void onlyPublicInheritedMethodsAreSuggested() {
     @Test
     void argumentThatDecidedTheStateIsShownWithAValueThatWouldWork() {
         assertHints("ErrorArgumentPicksTheState.java", new Hint(Kind.DECIDING_ARGUMENT,
-                "buffer.reset(boolean) on line 20 decides the state of buffer: with keep == true, this call would be allowed"));
+                "buffer.reset(boolean keep) on line 20 decides the state of buffer: with keep == true, this call would be allowed"));
     }
 
     @Test
     void deciderIsTheLastCallThatChangedTheCheckedStateSet() {
         assertHints("ErrorArgumentPicksTheStateEarlier.java", new Hint(Kind.DECIDING_ARGUMENT,
-                "param.setTilingMode(int) on line 25 decides the state of param: with mode == 2, this call would be allowed"));
+                "param.setTilingMode(int mode) on line 25 decides the state of param: with mode == 2, this call would be allowed"));
     }
 
     @Test
@@ -262,7 +262,8 @@ void checksAreSuggestedOnlyWhenTheRefinementsProveThem() {
                                 + "Objects created with new GuardChannel() start in such a state"),
                 new Hint(Kind.GUARD, "Guard this call with if (!c.isClosed()): when it returns false, c is open"));
         assertHints(errors.get(1),
-                new Hint(Kind.GUARD, "Guard this call with if (l.tryLock(timeout)): when it returns true, l is locked"),
+                new Hint(Kind.GUARD, "Guard this call with if (l.tryLock(...)), "
+                        + "filling in the arguments of tryLock(long timeout): when it returns true, l is locked"),
                 new Hint(Kind.AVAILABLE_CALLS, "In state unlocked, l can call: tryLock(long) (and possibly others)"));
         assertHints(errors.get(2),
                 new Hint(Kind.NEEDED_STATE, "The state of p is unknown here, and this call needs it to be ready"));
@@ -291,14 +292,13 @@ void argumentConditionsAreSuggestedOnlyWhenEveryArgumentMeetingThemWorks() {
         List<StateRefinementError> errors = errors("ErrorStateHintArgumentConditions.java", 7);
         assertHints(errors.get(0),
                 new Hint(Kind.CALL_SEQUENCE,
-                        "Call r.set(int, int) with lo < hi before this call to move r from low to high"),
+                        "Call r.set(int lo, int hi) with lo < hi before this call to move r from low to high"),
                 new Hint(Kind.AVAILABLE_CALLS, "In state low, r can call: set(int, int) (and possibly others)"));
         assertHints(errors.get(1), new Hint(Kind.CALL_SEQUENCE,
-                "Call chain.pick(int) with k == 1, then chain.next() before this call to move chain from a to c"),
+                "Call chain.pick(int k) with k == 1, then chain.next() before this call to move chain from a to c"),
                 new Hint(Kind.AVAILABLE_CALLS, "In state a, chain can call: pick(int) (and possibly others)"));
-        assertHints(errors.get(2),
-                new Hint(Kind.CALL_SEQUENCE,
-                        "Call l.setLimit(int) with limit <= 0 before this call to move l from bounded to unbounded"),
+        assertHints(errors.get(2), new Hint(Kind.CALL_SEQUENCE,
+                "Call l.setLimit(int limit) with limit <= 0 before this call to move l from bounded to unbounded"),
                 new Hint(Kind.AVAILABLE_CALLS, "In state bounded, l can call: setLimit(int) (and possibly others)"));
         // no condition, and no value of the earlier call's argument, is claimed to allow the call
         for (StateRefinementError error : errors.subList(3, 5))
@@ -313,7 +313,7 @@ void argumentConditionsAreSuggestedOnlyWhenEveryArgumentMeetingThemWorks() {
     @Test
     void callWhoseStateDependsOnItsArgumentIsSuggestedWithTheCondition() {
         assertHints("classes/state_hint_compression_mode_error", new Hint(Kind.CALL_SEQUENCE,
-                "Call wParam.setCompressionMode(int) with mode == 2 before this call to move wParam from startCompression to compressionExplicit"),
+                "Call wParam.setCompressionMode(int mode) with mode == 2 before this call to move wParam from startCompression to compressionExplicit"),
                 new Hint(Kind.AVAILABLE_CALLS,
                         "In state startCompression, wParam can call: setCompressionMode(int) (and possibly others)"));
     }