From 8a79ec2eab6bc7ce6361eea6b8c0d5ff0a6c9ce6 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 4 Nov 2026 00:07:20 +0000 Subject: [PATCH 1/2] Suggest result checks and argument conditions in state hints Methods whose state refinements mention their parameters or result were left out of the state machine, so the hints could not suggest checking canRedo() before redo(), or calling setCompressionMode(int) with mode == 2. They are now kept as call variants: with any arguments, with arguments meeting each condition the refinement tests, and, for a boolean result, with the result checked. Boolean methods whose return refinement relates the result to the state are kept as checks too. The solver works out what a variant does only when a hint needs it. A check is suggested only if the verifier allows it in every state the receiver can be in, its result can have the value checked, and the failing call is then allowed; if several checks would do, none is suggested. An argument condition is suggested only if every argument meeting it leads to a state that allows the call, and the value shown for an earlier call's argument is now checked the same way. Co-Authored-By: Claude Opus 5.5 --- .../testSuite/CorrectStateHintGuards.java | 109 +++++++++ .../ErrorStateHintArgumentConditions.java | 129 +++++++++++ .../java/testSuite/ErrorStateHintGuards.java | 218 ++++++++++++++++++ .../ImageWriteParamRefinements.java | 21 ++ .../Recoder.java | 22 ++ .../EditCommand.java | 48 ++++ .../UndoManagerRefinementsExpert.java | 98 ++++++++ .../EditCommand.java | 56 +++++ .../UndoManagerRefinementsExpert.java | 98 ++++++++ .../UndoManagerRefinements.java | 2 +- .../liquidjava/diagnostics/hints/Hint.java | 4 +- .../diagnostics/hints/StateHints.java | 59 ++++- .../object_checkers/AuxStateHandler.java | 12 +- .../processor/state_machine/CallVariant.java | 67 ++++++ .../state_machine/DecidingArgument.java | 44 +++- .../state_machine/SolverEffects.java | 200 ++++++++++++++++ .../processor/state_machine/StateMachine.java | 141 +++++++++-- .../state_machine/StateMachineBuilder.java | 194 +++++++++++++++- .../liquidjava/api/tests/TestStateHints.java | 112 ++++++++- .../state_machine/StateMachineTest.java | 81 +++++++ 20 files changed, 1658 insertions(+), 57 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectStateHintGuards.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintArgumentConditions.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintGuards.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_compression_mode_error/ImageWriteParamRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_compression_mode_error/Recoder.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_correct/EditCommand.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_correct/UndoManagerRefinementsExpert.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_error/EditCommand.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_error/UndoManagerRefinementsExpert.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/CallVariant.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/SolverEffects.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectStateHintGuards.java b/liquidjava-example/src/main/java/testSuite/CorrectStateHintGuards.java new file mode 100644 index 00000000..2571f828 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectStateHintGuards.java @@ -0,0 +1,109 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// The programs of ErrorStateHintGuards and ErrorStateHintArgumentConditions with their hints followed +public class CorrectStateHintGuards { + + static void negated() { + FixedChannel c = FixedChannel.make(); + if (!c.isClosed()) + c.send(); + } + + static void withParameter() { + FixedLock l = new FixedLock(); + if (l.tryLock(10)) + l.unlock(); + } + + static void checkAllowed() { + FixedWriter w = new FixedWriter(); + if (w.canWrite()) + w.write(); + } + + static void twoParameters() { + FixedRange r = new FixedRange(); + r.set(1, 2); + r.scan(); + } + + static void thenAnotherCall() { + FixedChain chain = new FixedChain(); + chain.pick(1); + chain.next(); + chain.done(); + } +} + +@StateSet({"open", "closed"}) +class FixedChannel { + @StateRefinement(to = "open(this)") + public FixedChannel() {} + + @StateRefinement(to = "return ? closed(this) : open(this)") + public boolean isClosed() { return false; } + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} + + @StateRefinement(from = "open(this)") + public void send() {} + + static FixedChannel make() { return new FixedChannel(); } +} + +@StateSet({"unlocked", "locked"}) +class FixedLock { + @StateRefinement(to = "unlocked(this)") + public FixedLock() {} + + @StateRefinement(from = "unlocked(this)", to = "return ? locked(this) : unlocked(this)") + public boolean tryLock(long timeout) { return true; } + + @StateRefinement(from = "locked(this)", to = "unlocked(this)") + public void unlock() {} +} + +@StateSet({"start", "accept"}) +class FixedWriter { + @StateRefinement(to = "start(this)") + public FixedWriter() {} + + @StateRefinement(from = "start(this)", to = "return ? accept(this) : start(this)") + public boolean canWrite() { return true; } + + @StateRefinement(from = "accept(this)") + public void write() {} + + static FixedWriter make() { return new FixedWriter(); } +} + +@StateSet({"low", "high"}) +class FixedRange { + @StateRefinement(to = "low(this)") + public FixedRange() {} + + @StateRefinement(to = "lo < hi ? high(this) : low(this)") + public void set(int lo, int hi) {} + + @StateRefinement(from = "high(this)") + public void scan() {} +} + +@StateSet({"a", "b", "c"}) +class FixedChain { + @StateRefinement(to = "a(this)") + public FixedChain() {} + + @StateRefinement(from = "a(this)", to = "k == 1 ? b(this) : a(this)") + public void pick(int k) {} + + @StateRefinement(from = "b(this)", to = "c(this)") + public void next() {} + + @StateRefinement(from = "c(this)") + public void done() {} +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintArgumentConditions.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintArgumentConditions.java new file mode 100644 index 00000000..07dd6e3f --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintArgumentConditions.java @@ -0,0 +1,129 @@ +package testSuite; + +import liquidjava.specification.Ghost; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// A call whose state after depends on its arguments is suggested with the condition its refinement tests, only when +// every argument that meets the condition leads to a state that allows the failing call +public class ErrorStateHintArgumentConditions { + + // a condition on two parameters + static void twoParameters() { + ConditionRange r = new ConditionRange(); + r.scan(); // Expect: State Refinement Error + } + + // a condition, then a call that needs no condition + static void thenAnotherCall() { + ConditionChain chain = new ConditionChain(); + chain.done(); // Expect: State Refinement Error + } + + // the negation of the condition the refinement tests + static void negatedCondition() { + ConditionLimit l = new ConditionLimit(); + l.stream(); // Expect: State Refinement Error + } + + // the condition does not decide the state + static void undecided() { + ConditionLoose l = new ConditionLoose(); + l.go(); // Expect: State Refinement Error + } + + // nor does an argument value that meets it: no value is suggested for the earlier call + static void undecidedValue() { + ConditionLoose l = new ConditionLoose(); + l.set(1); + l.go(); // Expect: State Refinement Error + } + + // the condition mentions a ghost of this, and then of another parameter: not a condition on the arguments alone + static void ghostOfThis() { + ConditionSized s = new ConditionSized(); + s.shrink(); // Expect: State Refinement Error + } + + static void ghostOfParameter() { + ConditionBin b = new ConditionBin(); + b.dump(); // Expect: State Refinement Error + } +} + +@StateSet({"low", "high"}) +class ConditionRange { + @StateRefinement(to = "low(this)") + public ConditionRange() {} + + @StateRefinement(to = "lo < hi ? high(this) : low(this)") + public void set(int lo, int hi) {} + + @StateRefinement(from = "high(this)") + public void scan() {} +} + +@StateSet({"a", "b", "c"}) +class ConditionChain { + @StateRefinement(to = "a(this)") + public ConditionChain() {} + + @StateRefinement(from = "a(this)", to = "k == 1 ? b(this) : a(this)") + public void pick(int k) {} + + @StateRefinement(from = "b(this)", to = "c(this)") + public void next() {} + + @StateRefinement(from = "c(this)") + public void done() {} +} + +@StateSet({"bounded", "unbounded"}) +class ConditionLimit { + @StateRefinement(to = "bounded(this)") + public ConditionLimit() {} + + @StateRefinement(to = "limit > 0 ? bounded(this) : unbounded(this)") + public void setLimit(int limit) {} + + @StateRefinement(from = "unbounded(this)") + public void stream() {} +} + +@StateSet({"a", "b"}) +class ConditionLoose { + @StateRefinement(to = "b(this)") + public ConditionLoose() {} + + @StateRefinement(to = "mode == 2 ? (a(this) || b(this)) : b(this)") + public void set(int mode) {} + + @StateRefinement(from = "a(this)") + public void go() {} +} + +@Ghost("int size") +@StateSet({"small", "big"}) +class ConditionSized { + @StateRefinement(to = "small(this) && size(this) == 0") + public ConditionSized() {} + + @StateRefinement(to = "n > size(old(this)) ? big(this) : small(this)") + public void grow(int n) {} + + @StateRefinement(from = "big(this)") + public void shrink() {} +} + +@Ghost("int capacity") +@StateSet({"empty", "full"}) +class ConditionBin { + @StateRefinement(to = "empty(this)") + public ConditionBin() {} + + @StateRefinement(from = "empty(this)", to = "capacity(other) > 3 ? full(this) : empty(this)") + public void fill(ConditionBin other) {} + + @StateRefinement(from = "full(this)") + public void dump() {} +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintGuards.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintGuards.java new file mode 100644 index 00000000..3bab50b6 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintGuards.java @@ -0,0 +1,218 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// A boolean method whose result decides a state that the failing call needs is suggested as a check, only when the +// refinements prove that checking it allows the call +public class ErrorStateHintGuards { + + // false decides the state: the check is negated + static void negated() { + GuardChannel c = GuardChannel.make(); + c.send(); // Expect: State Refinement Error + } + + // known state with no sequence of calls to the needed state: the check, with its parameter + static void withParameter() { + GuardLock l = new GuardLock(); + l.unlock(); // Expect: State Refinement Error + } + + // a true result does not decide the state + static void undecided() { + GuardPoll p = GuardPoll.make(); + p.use(); // Expect: State Refinement Error + } + + // the check needs a state that is just as unknown, but is allowed once the state is known + static void checkNeedsAState() { + GuardWriter w = GuardWriter.make(); + w.write(); // Expect: State Refinement Error + } + + static void checkAllowed() { + GuardWriter w = new GuardWriter(); + w.write(); // Expect: State Refinement Error + } + + // the check decides the state set it tests but resets another one the call needs + static void resetsAnotherSet() { + GuardBoth b = GuardBoth.make(); + b.both(); // Expect: State Refinement Error + } + + // the result decides the state only for some arguments + static void dependsOnArguments() { + GuardProbe p = GuardProbe.make(); + p.fire(); // Expect: State Refinement Error + } + + // in some states the refinement applied is not the one that tests the result + static void otherRefinement() { + GuardSteps m = GuardSteps.make(); + m.act(); // Expect: State Refinement Error + } + + // the state changes whatever the result + static void notACheck() { + GuardToken t = GuardToken.make(); + t.peek(); // Expect: State Refinement Error + } + + // a result that is not boolean is not suggested as a check + static void notBoolean() { + GuardReader r = new GuardReader(); + r.finish(); // Expect: State Refinement Error + } + + // several checks would do, so the refinements do not tell which one the call needs + static void severalChecks() { + GuardCoarse g = GuardCoarse.make(); + g.run(); // Expect: State Refinement Error + } +} + +@StateSet({"open", "closed"}) +class GuardChannel { + @StateRefinement(to = "open(this)") + public GuardChannel() {} + + @StateRefinement(to = "return ? closed(this) : open(this)") + public boolean isClosed() { return false; } + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} + + @StateRefinement(from = "open(this)") + public void send() {} + + static GuardChannel make() { return new GuardChannel(); } +} + +@StateSet({"unlocked", "locked"}) +class GuardLock { + @StateRefinement(to = "unlocked(this)") + public GuardLock() {} + + @StateRefinement(from = "unlocked(this)", to = "return ? locked(this) : unlocked(this)") + public boolean tryLock(long timeout) { return true; } + + @StateRefinement(from = "locked(this)", to = "unlocked(this)") + public void unlock() {} +} + +@StateSet({"ready", "busy"}) +class GuardPoll { + @StateRefinement(to = "busy(this)") + public GuardPoll() {} + + @StateRefinement(to = "return ? (ready(this) || busy(this)) : busy(this)") + public boolean poll() { return true; } + + @StateRefinement(from = "ready(this)") + public void use() {} + + static GuardPoll make() { return new GuardPoll(); } +} + +@StateSet({"start", "accept"}) +class GuardWriter { + @StateRefinement(to = "start(this)") + public GuardWriter() {} + + @StateRefinement(from = "start(this)", to = "return ? accept(this) : start(this)") + public boolean canWrite() { return true; } + + @StateRefinement(from = "accept(this)") + public void write() {} + + static GuardWriter make() { return new GuardWriter(); } +} + +@StateSet({"undoable", "notUndoable"}) +@StateSet({"redoable", "notRedoable"}) +class GuardBoth { + @StateRefinement(to = "notUndoable(this) && notRedoable(this)") + public GuardBoth() {} + + @StateRefinement(to = "return ? redoable(this) && notUndoable(this) : notRedoable(this)") + public boolean canRedo() { return true; } + + @StateRefinement(from = "redoable(this) && undoable(this)") + public void both() {} + + static GuardBoth make() { return new GuardBoth(); } +} + +@StateSet({"idle", "armed"}) +class GuardProbe { + @StateRefinement(to = "idle(this)") + public GuardProbe() {} + + @StateRefinement(to = "(n > 0 && return) ? armed(this) : idle(this)") + public boolean check(int n) { return true; } + + @StateRefinement(from = "armed(this)") + public void fire() {} + + static GuardProbe make() { return new GuardProbe(); } +} + +@StateSet({"s0", "s1", "s2"}) +class GuardSteps { + @StateRefinement(to = "s0(this)") + public GuardSteps() {} + + @StateRefinement(from = "s0(this)", to = "return ? s1(this) : s0(this)") + @StateRefinement(from = "s2(this)", to = "s2(this)") + public boolean step() { return true; } + + @StateRefinement(from = "s1(this)") + public void act() {} + + static GuardSteps make() { return new GuardSteps(); } +} + +@StateSet({"fresh", "used"}) +class GuardToken { + @StateRefinement(to = "fresh(this)") + public GuardToken() {} + + @StateRefinement(from = "fresh(this)", to = "used(this)") + public boolean consume() { return true; } + + @StateRefinement(from = "fresh(this)") + public void peek() {} + + static GuardToken make() { return new GuardToken(); } +} + +@StateSet({"start", "running"}) +class GuardCoarse { + @StateRefinement(to = "start(this)") + public GuardCoarse() {} + + @StateRefinement(to = "return ? running(this) : true") + public boolean canRun() { return true; } + + @StateRefinement(to = "return ? running(this) : true") + public boolean canStop() { return true; } + + @StateRefinement(from = "running(this)") + public void run() {} + + static GuardCoarse make() { return new GuardCoarse(); } +} + +@StateSet({"live", "eof"}) +class GuardReader { + @StateRefinement(to = "live(this)") + public GuardReader() {} + + @StateRefinement(from = "live(this)", to = "return == -1 ? eof(this) : live(this)") + public int read() { return 0; } + + @StateRefinement(from = "eof(this)") + public void finish() {} +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_compression_mode_error/ImageWriteParamRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_compression_mode_error/ImageWriteParamRefinements.java new file mode 100644 index 00000000..2a43a600 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_compression_mode_error/ImageWriteParamRefinements.java @@ -0,0 +1,21 @@ +package testSuite.classes.state_hint_compression_mode_error; + +import java.util.Locale; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// The call that reaches the state setCompressionType needs depends on its argument +@ExternalRefinementsFor("javax.imageio.ImageWriteParam") +@StateSet({"startCompression", "compressionExplicit", "compressionSet"}) +public interface ImageWriteParamRefinements { + @StateRefinement(to = "startCompression(this)") + void ImageWriteParam(Locale locale); + + @StateRefinement(to = "mode == 2 ? compressionExplicit(this) : startCompression(this)") + void setCompressionMode(int mode); + + @StateRefinement(from = "compressionExplicit(this)", to = "compressionSet(this)") + void setCompressionType(String compressionType); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_compression_mode_error/Recoder.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_compression_mode_error/Recoder.java new file mode 100644 index 00000000..f1ee8314 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_compression_mode_error/Recoder.java @@ -0,0 +1,22 @@ +package testSuite.classes.state_hint_compression_mode_error; + +import java.util.Locale; + +import javax.imageio.ImageWriteParam; + +// Study case A1_01 (dcm4che Transcoder): the compression type is set without setting the compression mode first +public class Recoder { + static ImageWriteParam params() { + ImageWriteParam wParam = new ImageWriteParam(Locale.ROOT); + wParam.setCompressionType("JPEG"); // Expect: State Refinement Error + return wParam; + } + + // the hint followed + static ImageWriteParam explicitParams() { + ImageWriteParam wParam = new ImageWriteParam(Locale.ROOT); + wParam.setCompressionMode(ImageWriteParam.MODE_EXPLICIT); + wParam.setCompressionType("JPEG"); + return wParam; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_correct/EditCommand.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_correct/EditCommand.java new file mode 100644 index 00000000..cadcced5 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_correct/EditCommand.java @@ -0,0 +1,48 @@ +package testSuite.classes.state_hint_study_undo_manager_correct; + +import javax.swing.undo.UndoManager; + +// Study case A1_56 (JabRef EditCommand) with both calls checked, as the hints say +public class EditCommand { + private final JabRefFrame frame; + private final StandardActions action; + + public EditCommand(StandardActions action, JabRefFrame frame) { + this.action = action; + this.frame = frame; + } + + public void execute() { + CountingUndoManager undoManager = frame.getUndoManager(); + switch (action) { + case REDO -> { + if (undoManager.canRedo()) + undoManager.redo(); + } + case UNDO -> { + if (undoManager.canUndo()) + undoManager.undo(); + } + default -> { } + } + } +} + +enum StandardActions { + COPY, UNDO, REDO +} + +class CountingUndoManager extends UndoManager { +} + +class JabRefFrame { + private final CountingUndoManager undoManager; + + JabRefFrame(CountingUndoManager undoManager) { + this.undoManager = undoManager; + } + + CountingUndoManager getUndoManager() { + return undoManager; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_correct/UndoManagerRefinementsExpert.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_correct/UndoManagerRefinementsExpert.java new file mode 100644 index 00000000..7015d9d7 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_correct/UndoManagerRefinementsExpert.java @@ -0,0 +1,98 @@ +package testSuite.classes.state_hint_study_undo_manager_correct; + +import javax.swing.event.UndoableEditEvent; +import javax.swing.undo.UndoableEdit; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// specs-v2: three orthogonal state sets. +// Phase: whether the manager still collects edits (start -> canEdit -> end). It decides addEdit, +// setLimit and discardAllEdits. end() is irreversible: inProgress never becomes true again. +// Undo / Redo: whether undo() / redo() would succeed right now, which is exactly what canUndo() / +// canRedo() answer, in every phase. "notUndoable" means "not known to be undoable": the verifier +// does not count edits, so after an undo() while editing there may or may not be more to undo. +// JDK 21: after end() the manager is one CompoundEdit, and undo/redo alternate over all edits at +// once (AbstractUndoableEdit.hasBeenDone), so end() makes it undoable and not redoable. +@ExternalRefinementsFor("javax.swing.undo.UndoManager") +@StateSet({"start", "canEdit", "end"}) +@StateSet({"undoable", "notUndoable"}) +@StateSet({"redoable", "notRedoable"}) +public interface UndoManagerRefinementsExpert { + + @StateRefinement(to="start(this) && notUndoable(this) && notRedoable(this)") + void UndoManager(); + + // A new edit can be undone, and it trims everything that could have been redone. + @StateRefinement(from="start(this)", to="canEdit(this) && undoable(this) && notRedoable(this)") + @StateRefinement(from="canEdit(this)", to="canEdit(this) && undoable(this) && notRedoable(this)") + boolean addEdit(UndoableEdit anEdit); + + @StateRefinement(from="canEdit(this)", to="canEdit(this) && notUndoable(this) && notRedoable(this)") + void discardAllEdits(); + + // end() drops the edits that were undone, and hasBeenDone is true; ending again changes nothing. + @StateRefinement(from="start(this)", to="end(this) && undoable(this) && notRedoable(this)") + @StateRefinement(from="canEdit(this)", to="end(this) && undoable(this) && notRedoable(this)") + @StateRefinement(from="end(this)") + void end(); + + @StateRefinement(from="canEdit(this)") + @StateRefinement(from="end(this)") + String getRedoPresentationName(); + + @StateRefinement(from="canEdit(this)") + @StateRefinement(from="end(this)") + String getUndoOrRedoPresentationName(); + + @StateRefinement(from="canEdit(this)") + @StateRefinement(from="end(this)") + String getUndoPresentationName(); + + // While editing, what was just redone can be undone, and there may be more to redo; after end() + // it is exact. + @StateRefinement(from="redoable(this)", to="undoable(this) && notRedoable(this)") + void redo(); + + // A smaller limit trims edits on both sides of the current position (all of them for 0). + @StateRefinement(from="start(this)") + @StateRefinement(from="canEdit(this)", to="canEdit(this) && notUndoable(this) && notRedoable(this)") + void setLimit(int l); + + @StateRefinement(from="undoable(this)", to="notUndoable(this) && redoable(this)") + void undo(); + + @StateRefinement(from="start(this)", to="canEdit(this) && undoable(this) && notRedoable(this)") + @StateRefinement(from="canEdit(this)", to="canEdit(this) && undoable(this) && notRedoable(this)") + @StateRefinement(from="end(this)") + void undoableEditHappened(UndoableEditEvent e); + + // undoOrRedo() undoes at the top of the stack and redoes below it, so either is enough; which one + // ran is unknown afterwards. + @StateRefinement(from="undoable(this)", to="notUndoable(this) && notRedoable(this)") + @StateRefinement(from="redoable(this)", to="notUndoable(this) && notRedoable(this)") + void undoOrRedo(); + + + + // int getLimit(); //any + + // Queries: they never change the manager, they tell the verifier which state it is in. When it is + // already known to be undoable / redoable the answer is true; otherwise (not known, or a field whose + // state is unknown) the answer decides. + @StateRefinement(from="undoable(this)", to="return && undoable(this)") + @StateRefinement(to="return ? undoable(this) : notUndoable(this)") + boolean canUndo(); + + @StateRefinement(from="redoable(this)", to="return && redoable(this)") + @StateRefinement(to="return ? redoable(this) : notRedoable(this)") + boolean canRedo(); + + // In start nothing was ever added. + @StateRefinement(from="start(this)", to="!return && start(this)") + @StateRefinement(from="canEdit(this)") + @StateRefinement(from="end(this)") + boolean canUndoOrRedo(); + +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_error/EditCommand.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_error/EditCommand.java new file mode 100644 index 00000000..4ee21785 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_error/EditCommand.java @@ -0,0 +1,56 @@ +package testSuite.classes.state_hint_study_undo_manager_error; + +import javax.swing.undo.UndoManager; + +// Study case A1_56 (JabRef EditCommand), trimmed to the calls on the undo manager: it comes from the frame, so its +// state is unknown, and canRedo() and canUndo() are the checks that decide it +public class EditCommand { + private final JabRefFrame frame; + private final StandardActions action; + + public EditCommand(StandardActions action, JabRefFrame frame) { + this.action = action; + this.frame = frame; + } + + public void execute() { + CountingUndoManager undoManager = frame.getUndoManager(); + switch (action) { + case REDO -> undoManager.redo(); // Expect: State Refinement Error + case UNDO -> undoManager.undo(); + default -> { } + } + } + + // redo() checked as the first hint says: undo() needs the other check + public void executeRedoChecked() { + CountingUndoManager undoManager = frame.getUndoManager(); + switch (action) { + case REDO -> { + if (undoManager.canRedo()) + undoManager.redo(); + } + case UNDO -> undoManager.undo(); // Expect: State Refinement Error + default -> { } + } + } +} + +enum StandardActions { + COPY, UNDO, REDO +} + +class CountingUndoManager extends UndoManager { +} + +class JabRefFrame { + private final CountingUndoManager undoManager; + + JabRefFrame(CountingUndoManager undoManager) { + this.undoManager = undoManager; + } + + CountingUndoManager getUndoManager() { + return undoManager; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_error/UndoManagerRefinementsExpert.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_error/UndoManagerRefinementsExpert.java new file mode 100644 index 00000000..c2e8e3a8 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_study_undo_manager_error/UndoManagerRefinementsExpert.java @@ -0,0 +1,98 @@ +package testSuite.classes.state_hint_study_undo_manager_error; + +import javax.swing.event.UndoableEditEvent; +import javax.swing.undo.UndoableEdit; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// specs-v2: three orthogonal state sets. +// Phase: whether the manager still collects edits (start -> canEdit -> end). It decides addEdit, +// setLimit and discardAllEdits. end() is irreversible: inProgress never becomes true again. +// Undo / Redo: whether undo() / redo() would succeed right now, which is exactly what canUndo() / +// canRedo() answer, in every phase. "notUndoable" means "not known to be undoable": the verifier +// does not count edits, so after an undo() while editing there may or may not be more to undo. +// JDK 21: after end() the manager is one CompoundEdit, and undo/redo alternate over all edits at +// once (AbstractUndoableEdit.hasBeenDone), so end() makes it undoable and not redoable. +@ExternalRefinementsFor("javax.swing.undo.UndoManager") +@StateSet({"start", "canEdit", "end"}) +@StateSet({"undoable", "notUndoable"}) +@StateSet({"redoable", "notRedoable"}) +public interface UndoManagerRefinementsExpert { + + @StateRefinement(to="start(this) && notUndoable(this) && notRedoable(this)") + void UndoManager(); + + // A new edit can be undone, and it trims everything that could have been redone. + @StateRefinement(from="start(this)", to="canEdit(this) && undoable(this) && notRedoable(this)") + @StateRefinement(from="canEdit(this)", to="canEdit(this) && undoable(this) && notRedoable(this)") + boolean addEdit(UndoableEdit anEdit); + + @StateRefinement(from="canEdit(this)", to="canEdit(this) && notUndoable(this) && notRedoable(this)") + void discardAllEdits(); + + // end() drops the edits that were undone, and hasBeenDone is true; ending again changes nothing. + @StateRefinement(from="start(this)", to="end(this) && undoable(this) && notRedoable(this)") + @StateRefinement(from="canEdit(this)", to="end(this) && undoable(this) && notRedoable(this)") + @StateRefinement(from="end(this)") + void end(); + + @StateRefinement(from="canEdit(this)") + @StateRefinement(from="end(this)") + String getRedoPresentationName(); + + @StateRefinement(from="canEdit(this)") + @StateRefinement(from="end(this)") + String getUndoOrRedoPresentationName(); + + @StateRefinement(from="canEdit(this)") + @StateRefinement(from="end(this)") + String getUndoPresentationName(); + + // While editing, what was just redone can be undone, and there may be more to redo; after end() + // it is exact. + @StateRefinement(from="redoable(this)", to="undoable(this) && notRedoable(this)") + void redo(); + + // A smaller limit trims edits on both sides of the current position (all of them for 0). + @StateRefinement(from="start(this)") + @StateRefinement(from="canEdit(this)", to="canEdit(this) && notUndoable(this) && notRedoable(this)") + void setLimit(int l); + + @StateRefinement(from="undoable(this)", to="notUndoable(this) && redoable(this)") + void undo(); + + @StateRefinement(from="start(this)", to="canEdit(this) && undoable(this) && notRedoable(this)") + @StateRefinement(from="canEdit(this)", to="canEdit(this) && undoable(this) && notRedoable(this)") + @StateRefinement(from="end(this)") + void undoableEditHappened(UndoableEditEvent e); + + // undoOrRedo() undoes at the top of the stack and redoes below it, so either is enough; which one + // ran is unknown afterwards. + @StateRefinement(from="undoable(this)", to="notUndoable(this) && notRedoable(this)") + @StateRefinement(from="redoable(this)", to="notUndoable(this) && notRedoable(this)") + void undoOrRedo(); + + + + // int getLimit(); //any + + // Queries: they never change the manager, they tell the verifier which state it is in. When it is + // already known to be undoable / redoable the answer is true; otherwise (not known, or a field whose + // state is unknown) the answer decides. + @StateRefinement(from="undoable(this)", to="return && undoable(this)") + @StateRefinement(to="return ? undoable(this) : notUndoable(this)") + boolean canUndo(); + + @StateRefinement(from="redoable(this)", to="return && redoable(this)") + @StateRefinement(to="return ? redoable(this) : notRedoable(this)") + boolean canRedo(); + + // In start nothing was ever added. + @StateRefinement(from="start(this)", to="!return && start(this)") + @StateRefinement(from="canEdit(this)") + @StateRefinement(from="end(this)") + boolean canUndoOrRedo(); + +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_hint_undo_manager_error/UndoManagerRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_hint_undo_manager_error/UndoManagerRefinements.java index 8bee5cd1..b08f7f4e 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/state_hint_undo_manager_error/UndoManagerRefinements.java +++ b/liquidjava-example/src/main/java/testSuite/classes/state_hint_undo_manager_error/UndoManagerRefinements.java @@ -5,7 +5,7 @@ import liquidjava.specification.StateSet; // Issue #454: with an unknown state, redo() needs redoable, and the only call that leads there, undo(), needs -// undoable, which is just as unknown +// undoable, which is just as unknown; canRedo() is the check that decides it @ExternalRefinementsFor("javax.swing.undo.UndoManager") @StateSet({"undoable", "notUndoable"}) @StateSet({"redoable", "notRedoable"}) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java index 4ce0e7ac..9098f6ba 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java @@ -26,7 +26,9 @@ public enum Kind { /** The object is in a state where no call with a state refinement is allowed */ FINAL_STATE, /** The object can be in any state: the state the failing call needs, and the constructors that create it */ - NEEDED_STATE + NEEDED_STATE, + /** A call whose result, checked right before the failing call, puts the object in a state that allows it */ + GUARD } public static Hint general(String message) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java index 899f0d13..48fd7d52 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java @@ -14,6 +14,7 @@ import liquidjava.diagnostics.hints.Hint.Kind; import liquidjava.processor.context.RefinedFunction; import liquidjava.processor.context.Variable; +import liquidjava.processor.state_machine.CallVariant; import liquidjava.processor.state_machine.DecidingArgument; import liquidjava.processor.state_machine.State; import liquidjava.processor.state_machine.StateMachine; @@ -25,7 +26,7 @@ /** * Hints for a call made in a state that does not allow it, read from the class's {@link StateMachine}. The error's * category decides which kinds of hints are given, and each hint only states what the machine proves, so a suggested - * sequence of calls always makes the failing call verify. + * sequence of calls, or check of a call's result, always makes the failing call verify. */ public final class StateHints { @@ -74,7 +75,10 @@ public static List forCall(StateMachine machine, RefinedFunction call, Set boolean pathDependent = category == ErrorCategory.PATH_DEPENDENT_STATE; List sequences = hints.howToReach(current, call, hints.namesHere(current), () -> machine.complete() ? List.of(hints.unreachable(current, call, pathDependent)) : List.of()); - return Stream.concat(sequences.stream(), hints.allowedCalls(current).stream()).toList(); + // in a known state, a check is suggested only when no sequence of calls reaches a state that allows the call + boolean reachable = sequences.stream().anyMatch(h -> h.kind() == Kind.CALL_SEQUENCE); + List guards = reachable && current.size() == 1 ? List.of() : hints.guard(current, call); + return Stream.of(sequences, guards, hints.allowedCalls(current)).flatMap(List::stream).toList(); } /** The earlier call whose arguments decided the receiver's state, and values that would allow the call */ @@ -90,9 +94,9 @@ public static Hint decidingArgument(DecidingArgument deciding, String receiver) } /** - * The receiver can be in any state: name the state {@code call} needs and the calls that get there from any state. - * A call allowed in only some states is never suggested, since whether it is allowed is just as unknown. Calls that - * only tell which state the object is in are not in the machine, so no hint suggests checking one first. + * The receiver can be in any state: name the state {@code call} needs, the call whose result tells whether the + * receiver is in it, and the calls that get there from any state. A call allowed in only some states is never + * suggested, since whether it is allowed is just as unknown. * * @param checkedElsewhere * whether the state was checked, though the check did not decide it @@ -104,6 +108,7 @@ private List anyState(Set current, RefinedFunction call, boolean ch message += newObjects(call).map(c -> ". Objects created with " + c + " start in such a state").orElse(""); List hints = new ArrayList<>(); hints.add(new Hint(Kind.NEEDED_STATE, message)); + hints.addAll(guard(current, call)); hints.addAll(howToReach(current, call, "any state", List::of)); return hints; } @@ -118,10 +123,10 @@ private List anyState(Set current, RefinedFunction call, boolean ch */ private List howToReach(Set current, RefinedFunction call, String from, Supplier> unreachable) { - Optional>> search = machine.shortestPaths(current, call, MAX_SEQUENCES); + Optional>> search = machine.shortestPaths(current, call, MAX_SEQUENCES); if (search.isEmpty()) return List.of(); - List> sequences = search.get(); + List> sequences = search.get(); if (sequences.isEmpty()) return unreachable.get(); if (sequences.get(0).size() > MAX_SEQUENCE_LENGTH) @@ -129,10 +134,34 @@ private List howToReach(Set current, RefinedFunction call, String f return sequences.stream().map(sequence -> callSequence(current, sequence, from)).toList(); } - private Hint callSequence(Set current, List sequence, String from) { + /** + * The call whose result, checked right before {@code call}, puts the receiver in a state that allows it: one the + * verifier allows in every state of {@code current}, whose result can have the value checked. If several calls + * would do, none is suggested, since the refinements do not tell them apart. + */ + private List guard(Set current, RefinedFunction call) { + List guards = new ArrayList<>(); + for (CallVariant guard : machine.guards()) { + if (!machine.allows(current, guard)) + continue; + Set reached = machine.after(current, guard); + if (!reached.isEmpty() && machine.allows(reached, call)) + guards.add(guard); + } + if (guards.size() != 1) + return List.of(); + CallVariant guard = guards.get(0); + boolean negated = guard.negatedResult(); + String check = (negated ? "!" : "") + call(guard.method()); + String message = String.format("Guard this call with if (%s): when it returns %s, %s is %s", check, !negated, + receiver, needed()); + return List.of(new Hint(Kind.GUARD, message)); + } + + private Hint callSequence(Set current, List sequence, String from) { Set reached = current; - for (RefinedFunction method : sequence) - reached = machine.after(reached, method); + for (CallVariant step : sequence) + reached = machine.after(reached, step); String calls = sequence.stream().map(this::call).collect(Collectors.joining(", then ")); return new Hint(Kind.CALL_SEQUENCE, String.format("Call %s before this call to move %s from %s to %s", calls, receiver, from, names(reached))); @@ -179,6 +208,16 @@ private String call(RefinedFunction method) { return receiver + "." + signature(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} + */ + private String call(CallVariant step) { + String condition = step.kind() == CallVariant.Kind.ARGUMENTS + ? " with " + step.condition().getExpression().toDisplayString() : ""; + return call(step.method()) + condition; + } + /** A method as shown in hints, e.g. {@code open(int)} */ public static String signature(RefinedFunction method) { return Utils.getSimpleName(method.getName()) + parameters(method); 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 978e005a..60349ca1 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 @@ -876,13 +876,21 @@ private static Optional decidingArgument(TypeChecker tc, Varia } } - /** Hints on how to fix a call to {@code function} made in a state that does not allow it */ + /** + * Hints on how to fix a call to {@code function} made in a state that does not allow it. Best effort, like + * {@link #receiverStates}: the machine asks the solver about some calls only when a hint needs them + */ private static List stateHints(ReceiverStates states, RefinedFunction function, ErrorCategory category, boolean checked, CtElement invocation) { Optional receiver = receiverOf(invocation); if (receiver.isEmpty() || !StateMachineBuilder.canModel(function)) return List.of(); - return StateHints.forCall(states.machine(), function, states.current(), receiver.get(), category, checked); + try { + return StateHints.forCall(states.machine(), function, states.current(), receiver.get(), category, checked); + } catch (RuntimeException e) { + DebugLog.warn("Could not compute the state hints: " + e.getMessage()); + return List.of(); + } } /** diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/CallVariant.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/CallVariant.java new file mode 100644 index 00000000..a54ce0a6 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/CallVariant.java @@ -0,0 +1,67 @@ +package liquidjava.processor.state_machine; + +import java.util.Set; + +import liquidjava.processor.context.RefinedFunction; +import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.UnaryExpression; + +/** + * A way to call a method whose state refinements depend on more than the state of this: with any arguments, with + * arguments that meet a condition its refinements test, or followed by a check of its boolean result + * + * @param method + * the method called + * @param kind + * what {@code condition} is about + * @param condition + * the condition, in the names of the refinement: its parameter names, and {@code _} for the result + * @param effects + * what each state refinement of the method does when the call meets {@code condition}, or null for a call of + * a method whose transitions the {@link StateMachine} has + */ +public record CallVariant(RefinedFunction method, Kind kind, Predicate condition, Effects effects) { + + public enum Kind { + /** Any arguments and any result */ + ANY, + /** Arguments that meet the condition */ + ARGUMENTS, + /** A result that meets the condition, checked right after the call */ + RESULT + } + + /** Whether the {@code from} of a state refinement holds in a state */ + public enum Entry { + HOLDS, FAILS, + /** It may or may not hold, or the solver could not tell */ + UNDECIDED + } + + /** + * What the state refinements of a method do in each state, in the order they are declared, for calls that meet a + * variant's condition + */ + public interface Effects { + + int refinements(); + + /** Whether the state refinement at {@code index} has a {@code to} */ + boolean changesState(int index); + + Entry entry(int index, State state); + + /** + * The states the object can be in after a call made in {@code state}, whose {@code from} must hold for the + * refinement at {@code index}, or null if the solver could not tell + */ + Set after(int index, State state); + } + + /** + * Whether the condition is on the result and holds when the result is {@code false}, as in {@code !x.isClosed()} + */ + public boolean negatedResult() { + return kind == Kind.RESULT && condition.getExpression() instanceof UnaryExpression; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/DecidingArgument.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/DecidingArgument.java index 134cbb0d..da0c9970 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/DecidingArgument.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/DecidingArgument.java @@ -26,7 +26,7 @@ /** * An earlier call whose arguments decided the state that a failing call does not allow, with argument values for which - * the failing call would have been allowed + * the failing call is allowed whatever else holds * * @param call * the deciding call @@ -94,20 +94,31 @@ private static Optional> valuesAllowing(TypeChecker tc, Stat to = to.changeOldMentions(call.previous().get().getName(), OBJECT); Map free = new LinkedHashMap<>(); // fresh name -> name shown + Map> types = new LinkedHashMap<>(); // fresh name -> type RefinedFunction function = call.function(); for (Variable parameter : function.getArguments()) - to = leaveFree(context, to, parameter.getName(), parameter.getType(), parameter.getName(), free, + 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 ? leaveFree(context, to, Keys.WILDCARD, function.getType(), RESULT, free, invocation) + to = returnsValue + ? leaveFree(context, to, Keys.WILDCARD, function.getType(), RESULT, free, types, invocation) : to.substituteVariable(Keys.WILDCARD, OBJECT); Predicate before = call.previous().map(VariableInstance::getRefinement).orElse(new Predicate()); + Predicate after = Predicate.createConjunction(before, to); Predicate allowed = required.stream().map(p -> p.substituteVariable(Keys.THIS, OBJECT)) .reduce(Predicate.createLit("false", Types.BOOLEAN), Predicate::createDisjunction); - Optional witness = new StateSolver(tc, invocation.getPosition()) - .witness(Predicate.createConjunction(before, to), allowed); - return witness.map(model -> model.assignments().stream().filter(a -> free.containsKey(a.first())).collect( + StateSolver solver = new StateSolver(tc, invocation.getPosition()); + Optional witness = solver.witness(after, allowed); + if (witness.isEmpty()) + return Optional.empty(); + List> values = witness.get().assignments().stream() + .filter(a -> free.containsKey(a.first())).toList(); + // the values must allow the call whatever else holds, not only in the solver's example + Optional pinned = pinned(values, types); + if (pinned.isEmpty() || !solver.implies(Predicate.createConjunction(after, pinned.get()), allowed)) + return Optional.empty(); + return Optional.of(values.stream().collect( Collectors.toMap(a -> free.get(a.first()), Pair::second, (a, b) -> a, LinkedHashMap::new))); } finally { context.exitContext(); @@ -116,12 +127,31 @@ private static Optional> valuesAllowing(TypeChecker tc, Stat /** Renames {@code name} in {@code predicate} to a fresh variable with no refinement, if it is mentioned */ private static Predicate leaveFree(Context context, Predicate predicate, String name, CtTypeReference type, - String shownAs, Map free, CtElement invocation) { + String shownAs, Map free, Map> types, CtElement invocation) { if (!predicate.getVariableNames().contains(name)) return predicate; String fresh = "#" + shownAs; context.addVarToContext(fresh, type, new Predicate(), invocation); free.put(fresh, shownAs); + types.put(fresh, type); return predicate.substituteVariable(name, fresh); } + + /** That each variable has its value, or nothing if a value cannot be written as a literal */ + private static Optional pinned(List> values, + Map> types) { + Predicate pinned = new Predicate(); + for (Pair value : values) { + // the solver writes negative numbers as (- n) + String literal = value.second().replaceAll("^\\(-\\s*(.*)\\)$", "-$1"); + try { + Predicate equals = Predicate.createEquals(Predicate.createVar(value.first()), + Predicate.createLit(literal, types.get(value.first()).toString())); + pinned = Predicate.createConjunction(pinned, equals); + } catch (IllegalArgumentException e) { + return Optional.empty(); + } + } + return Optional.of(pinned); + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/SolverEffects.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/SolverEffects.java new file mode 100644 index 00000000..e98347d7 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/SolverEffects.java @@ -0,0 +1,200 @@ +package liquidjava.processor.state_machine; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.Optional; +import java.util.Set; +import java.util.stream.Collectors; + +import liquidjava.diagnostics.DebugLog; +import liquidjava.diagnostics.errors.LJError; +import liquidjava.processor.context.Context; +import liquidjava.processor.context.ObjectState; +import liquidjava.processor.refinement_checker.TypeChecker; +import liquidjava.rj_language.Predicate; +import liquidjava.utils.constants.Keys; +import spoon.reflect.declaration.CtElement; +import spoon.reflect.reference.CtTypeReference; + +/** + * The {@link CallVariant.Effects} of a call, asked of the SMT solver only when a hint needs them, and then remembered. + * The solver sees the object before and after the call, the call's parameters and its result under names nothing else + * uses, so what the program knows about variables with the same names does not matter. + */ +final class SolverEffects implements CallVariant.Effects { + + static final String BEFORE = "#state_before"; + static final String AFTER = "#state_after"; + + /** + * The variables the predicates mention, by name, with their types + * + * @param states + * the states of the class + * @param stateSets + * the states of each state set on its own, in the order the sets are declared + * @param type + * the class of the object + * @param free + * the parameters and the result, by their names in the predicates + * @param element + * where the variables are declared + */ + record Scope(TypeChecker tc, StateSolver solver, List states, List> stateSets, + CtTypeReference type, Map> free, CtElement element) { + } + + private final Scope scope; + private final List changes; + /** The variant's condition, also assumed before the call unless it is on the result */ + private final Predicate condition; + private final boolean onResult; + /** The return refinement of a method without state refinements, or null */ + private final Predicate query; + /** The effects with any arguments, whose entries a condition on the result does not change, or null */ + private final CallVariant.Effects any; + + private final Map> entries = new HashMap<>(); + private final Map>>> afters = new HashMap<>(); + + /** + * @param changes + * the state refinements that have a {@code from}, in the names of {@code scope} + */ + SolverEffects(Scope scope, List changes, Predicate condition, boolean onResult, + CallVariant.Effects any) { + this(scope, changes, condition, onResult, null, any); + } + + /** The effects of checking the result of a method without state refinements, given its return refinement */ + static SolverEffects ofQuery(Scope scope, Predicate returnRefinement, Predicate condition) { + return new SolverEffects(scope, List.of(), condition, true, returnRefinement, null); + } + + private SolverEffects(Scope scope, List changes, Predicate condition, boolean onResult, + Predicate query, CallVariant.Effects any) { + this.scope = scope; + this.changes = changes; + this.condition = condition; + this.onResult = onResult; + this.query = query; + this.any = any; + } + + @Override + public int refinements() { + return query != null ? 1 : changes.size(); + } + + @Override + public boolean changesState(int index) { + return query == null && changes.get(index).hasTo(); + } + + @Override + public CallVariant.Entry entry(int index, State state) { + if (query != null) + return CallVariant.Entry.HOLDS; // no state refinement: allowed in every state + if (onResult && any != null) + return any.entry(index, state); // the result is not known before the call + return entries.computeIfAbsent(index, i -> new HashMap<>()).computeIfAbsent(state, s -> { + Optional entry = withScope(() -> { + Predicate before = before(s); + Predicate from = changes.get(index).getFrom().substituteVariable(Keys.THIS, BEFORE); + if (scope.solver().implies(before, from)) + return CallVariant.Entry.HOLDS; + return scope.solver().compatible(before, from) ? CallVariant.Entry.UNDECIDED : CallVariant.Entry.FAILS; + }); + return entry.orElse(CallVariant.Entry.UNDECIDED); + }); + } + + @Override + public Set after(int index, State state) { + Map>> known = afters.computeIfAbsent(index, i -> new HashMap<>()); + if (!known.containsKey(state)) { + // a condition on the result only narrows the states the call can lead to + Set candidates = onResult && any != null ? any.after(index, state) : Set.copyOf(scope.states()); + known.put(state, candidates == null ? Optional.empty() : computeAfter(index, state, candidates)); + } + return known.get(state).orElse(null); + } + + private Optional> computeAfter(int index, State state, Set candidates) { + return withScope(() -> { + State s = state; + if (query != null) { + Predicate known = Predicate.createConjunction(before(s), + Predicate.createConjunction(query.substituteVariable(Keys.THIS, BEFORE), condition)); + return possibleStates(Set.of(s), known, BEFORE); + } + ObjectState change = changes.get(index); + if (!change.hasTo()) + return Set.of(s); + Predicate to = change.getTo().substituteVariable(Keys.THIS, AFTER).changeOldMentions(BEFORE, AFTER); + Predicate known = Predicate.createConjunction(before(s), to); + if (onResult) + known = Predicate.createConjunction(known, condition); + Set next = possibleStates(candidates, known, AFTER); + // no state at all: the condition contradicts the refinement here, so nothing can be claimed + return next.isEmpty() && !onResult ? null : next; + }); + } + + /** + * The {@code candidates} that {@code variable} can be in when {@code known} holds. Many candidates are first + * narrowed down by the states possible in each state set on its own, which takes fewer questions than asking about + * every combination. + */ + private Set possibleStates(Set candidates, Predicate known, String variable) throws LJError { + List> sets = scope.stateSets(); + int setStates = sets.stream().mapToInt(List::size).sum(); + List ordered = scope.states().stream().filter(candidates::contains).toList(); + if (ordered.size() <= setStates) + return scope.solver().possibleStates(ordered, known, variable); + List> possible = new ArrayList<>(); + for (int k = 0; k < sets.size(); k++) { + int set = k; + List values = sets.get(k).stream() + .filter(v -> ordered.stream().anyMatch(c -> c.names().get(set).equals(v.names().get(0)))).toList(); + possible.add(scope.solver().possibleStates(values, known, variable).stream().map(v -> v.names().get(0)) + .collect(Collectors.toSet())); + } + List combined = ordered.stream().filter(c -> { + for (int k = 0; k < sets.size(); k++) + if (!possible.get(k).contains(c.names().get(k))) + return false; + return true; + }).toList(); + return scope.solver().possibleStates(combined, known, variable); + } + + /** What is known before the call in {@code state} */ + private Predicate before(State state) { + Predicate before = state.predicate().substituteVariable(Keys.THIS, BEFORE); + return onResult ? before : Predicate.createConjunction(before, condition); + } + + private interface SolverQuery { + T ask() throws LJError; + } + + /** Asks the solver with the variables of {@link #scope} declared; nothing if it fails */ + private Optional withScope(SolverQuery query) { + Context context = scope.tc().getContext(); + context.enterContext(); + try { + context.addVarToContext(BEFORE, scope.type(), new Predicate(), scope.element()); + context.addVarToContext(AFTER, scope.type(), new Predicate(), scope.element()); + scope.free().forEach((name, type) -> context.addVarToContext(name, type, new Predicate(), scope.element())); + return Optional.ofNullable(query.ask()); + } catch (RuntimeException e) { // including an LJError from the solver + DebugLog.warn("Could not compute the effect of a call: " + e.getMessage()); + return Optional.empty(); + } finally { + context.exitContext(); + } + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java index 524b079a..54722827 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java @@ -14,6 +14,7 @@ import liquidjava.processor.context.ObjectState; import liquidjava.processor.context.RefinedFunction; +import liquidjava.rj_language.Predicate; /** * The typestate of a class as a finite state machine, built by {@link StateMachineBuilder} @@ -29,9 +30,12 @@ * @param complete * whether every method that can change the state of the object is in {@code methods}; only then can the * machine tell that a state cannot be reached or that no call is allowed + * @param variants + * the ways to call the methods whose state refinements also depend on their arguments or result, and the + * boolean methods whose result tells which state the object is in */ public record StateMachine(List states, List methods, List transitions, - Map> constructors, boolean complete) { + Map> constructors, boolean complete, List variants) { /** How many sets of states a search visits before giving up */ private static final int MAX_SEARCHED = 1000; @@ -41,6 +45,12 @@ public record StateMachine(List states, List methods, Li methods = List.copyOf(methods); transitions = List.copyOf(transitions); constructors = Collections.unmodifiableMap(new LinkedHashMap<>(constructors)); + variants = List.copyOf(variants); + } + + public StateMachine(List states, List methods, List transitions, + Map> constructors, boolean complete) { + this(states, methods, transitions, constructors, complete, List.of()); } public boolean models(RefinedFunction method) { @@ -59,9 +69,103 @@ public boolean allows(Set current, RefinedFunction method) { return preservesState || calls.stream().map(Transition::change).distinct().count() <= 1; } + /** + * Whether {@code variant} can be called when the object can be in any of {@code current}. Like in the verifier, the + * state refinement applied is the first whose {@code from} holds in all of them, and a method that keeps the state + * needs each of them to satisfy some {@code from}. If the machine cannot tell, the call is not allowed. + */ + public boolean allows(Set current, CallVariant variant) { + if (variant.effects() == null) + return allows(current, variant.method()); + return applied(current, variant.effects()).isPresent(); + } + + /** + * The states the object can be in after calling {@code variant}, which must be allowed in all of {@code current} + */ + public Set after(Set current, CallVariant variant) { + if (variant.effects() == null) + return after(current, variant.method()); + CallVariant.Effects effects = variant.effects(); + List applied = applied(current, effects).orElseThrow(); + return ordered(current.stream().flatMap(s -> applied.stream() + .filter(i -> effects.entry(i, s) == CallVariant.Entry.HOLDS).flatMap(i -> effects.after(i, s).stream())) + .toList()); + } + + /** The calls whose result, checked right after them, tells which state the object is in */ + public List guards() { + return variants.stream().filter(v -> v.kind() == CallVariant.Kind.RESULT).toList(); + } + + /** The indexes of the state refinements applied to a call made in any of {@code current}, if it is allowed */ + private Optional> applied(Set current, CallVariant.Effects effects) { + if (current.isEmpty()) + return Optional.empty(); + List indexes = new ArrayList<>(); + for (int i = 0; i < effects.refinements(); i++) + indexes.add(i); + List applied; + if (indexes.stream().noneMatch(effects::changesState)) { + boolean everyState = current.stream() + .allMatch(s -> indexes.stream().anyMatch(i -> effects.entry(i, s) == CallVariant.Entry.HOLDS)); + if (!everyState) + return Optional.empty(); + applied = indexes; + } else { + Optional first = firstApplying(current, effects); + if (first.isEmpty()) + return Optional.empty(); + applied = List.of(first.get()); + } + // the states after the call must be known too + for (State s : current) + for (int i : applied) + if (effects.entry(i, s) == CallVariant.Entry.HOLDS && effects.after(i, s) == null) + return Optional.empty(); + return Optional.of(applied); + } + + private static Optional firstApplying(Set current, CallVariant.Effects effects) { + for (int i = 0; i < effects.refinements(); i++) { + int index = i; + List entries = current.stream().map(s -> effects.entry(index, s)).toList(); + if (entries.contains(CallVariant.Entry.UNDECIDED)) + return Optional.empty(); // whether the verifier applies it depends on more than the state + if (entries.stream().allMatch(CallVariant.Entry.HOLDS::equals)) + return Optional.of(i); + } + return Optional.empty(); + } + + /** + * The calls a sequence can be made of when the object can be in any of {@code current}: the methods in the machine, + * and the others with any arguments or with arguments meeting a condition that changes where they lead + */ + private List steps(Set current) { + List steps = new ArrayList<>(); + for (RefinedFunction method : methods) + if (allows(current, method)) + steps.add(new CallVariant(method, CallVariant.Kind.ANY, new Predicate(), null)); + for (CallVariant variant : variants) { + if (variant.kind() == CallVariant.Kind.RESULT || !allows(current, variant)) + continue; + Set reached = after(current, variant); + boolean sameAsAnyArguments = variant.kind() == CallVariant.Kind.ARGUMENTS && variants.stream() + .anyMatch(v -> v.method().equals(variant.method()) && v.kind() == CallVariant.Kind.ANY + && allows(current, v) && after(current, v).equals(reached)); + if (!reached.isEmpty() && !sameAsAnyArguments) + steps.add(variant); + } + return steps; + } + /** The methods that can be called when the object can be in any of {@code current} */ public List allowedIn(Set current) { - return methods.stream().filter(m -> allows(current, m)).toList(); + List allowed = new ArrayList<>(methods.stream().filter(m -> allows(current, m)).toList()); + variants.stream().filter(v -> v.kind() == CallVariant.Kind.ANY && allows(current, v)).map(CallVariant::method) + .filter(m -> !allowed.contains(m)).forEach(allowed::add); + return allowed; } /** The states where {@code method} can be called */ @@ -75,30 +179,35 @@ public Set after(Set current, RefinedFunction method) { } /** - * The shortest sequences of calls that take an object in any of {@code current} to where {@code call} is allowed + * The shortest sequences of calls that take an object in any of {@code current} to where {@code call} is allowed. A + * call of a method whose state refinements depend on its arguments has the condition on them that the sequence + * needs, if any; a sequence that needs none is preferred. * * @return at most {@code limit} sequences, all of the same length; none if there is no such sequence; nothing if * the search gave up */ - public Optional>> shortestPaths(Set current, RefinedFunction call, int limit) { - Map, List>> level = Map.of(current, List.of(List.of())); + public Optional>> shortestPaths(Set current, RefinedFunction call, int limit) { + Map, List>> level = Map.of(current, List.of(List.of())); Set> visited = new HashSet<>(level.keySet()); while (!level.isEmpty()) { - Map, List>> next = new LinkedHashMap<>(); + Map, List>> next = new LinkedHashMap<>(); level.forEach((states, paths) -> { - for (RefinedFunction method : allowedIn(states)) { - Set reached = after(states, method); + for (CallVariant step : steps(states)) { + Set reached = after(states, step); if (visited.contains(reached)) continue; - List> reachedPaths = next.computeIfAbsent(reached, k -> new ArrayList<>()); - paths.stream().limit(limit - reachedPaths.size()).map(path -> append(path, method)) + List> reachedPaths = next.computeIfAbsent(reached, k -> new ArrayList<>()); + paths.stream().limit(limit - reachedPaths.size()).map(path -> append(path, step)) .forEach(reachedPaths::add); } }); - List> found = next.entrySet().stream().filter(e -> allows(e.getKey(), call)) - .flatMap(e -> e.getValue().stream()).limit(limit).toList(); - if (!found.isEmpty()) - return Optional.of(found); + List> found = next.entrySet().stream().filter(e -> allows(e.getKey(), call)) + .flatMap(e -> e.getValue().stream()).toList(); + if (!found.isEmpty()) { + List> unconditioned = found.stream() + .filter(p -> p.stream().noneMatch(v -> v.kind() == CallVariant.Kind.ARGUMENTS)).toList(); + return Optional.of((unconditioned.isEmpty() ? found : unconditioned).stream().limit(limit).toList()); + } visited.addAll(next.keySet()); if (visited.size() > MAX_SEARCHED) return Optional.empty(); @@ -151,8 +260,8 @@ private Optional transition(State from, RefinedFunction method) { return transitions.stream().filter(t -> t.from().equals(from) && t.method().equals(method)).findFirst(); } - private static List append(List path, RefinedFunction method) { - List extended = new ArrayList<>(path); + private static List append(List path, CallVariant method) { + List extended = new ArrayList<>(path); extended.add(method); return extended; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java index 9a83e0b3..0a833817 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java @@ -7,6 +7,7 @@ import java.util.LinkedHashMap; import java.util.List; import java.util.Map; +import java.util.Objects; import java.util.Optional; import java.util.Set; import java.util.stream.Collectors; @@ -17,10 +18,17 @@ import liquidjava.processor.context.GhostState; import liquidjava.processor.context.ObjectState; import liquidjava.processor.context.RefinedFunction; +import liquidjava.processor.context.Variable; import liquidjava.processor.refinement_checker.TypeChecker; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.FunctionInvocation; +import liquidjava.rj_language.ast.Ite; +import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.utils.Utils; import liquidjava.utils.constants.Keys; +import liquidjava.utils.constants.Types; import spoon.reflect.declaration.CtClass; import spoon.reflect.declaration.CtElement; import spoon.reflect.declaration.CtMethod; @@ -33,9 +41,11 @@ /** * Builds the {@link StateMachine} of a class from its {@code @StateSet}s and {@code @StateRefinement}s, and those of * its supertypes, which it inherits. Every transition is proven by the SMT solver, so the machine never contains a call - * that would not verify. Methods whose state refinements mention anything besides the states of {@code this} - * (parameters, return values, other ghosts) are left out, and the machine is then marked incomplete, as it is when a - * subclass has state refinements of its own or an inherited refinement may not be the one the verifier applies. + * that would not verify. Methods whose state refinements also mention their parameters or result are kept as + * {@link CallVariant}s, whose effects the solver works out only when a hint needs them, and boolean methods whose + * return refinement relates their result to the state are kept as checks of that result. The machine is incomplete if a + * method has variants or is left out because its refinements mention anything else, as it is when a subclass has state + * refinements of its own or an inherited refinement may not be the one the verifier applies. */ public class StateMachineBuilder { @@ -43,17 +53,25 @@ public class StateMachineBuilder { private static final int MAX_STATES = 16; // two objects of the class, before and after a call, that the rest of the program knows nothing about - private static final String BEFORE = "#state_before"; - private static final String AFTER = "#state_after"; + private static final String BEFORE = SolverEffects.BEFORE; + private static final String AFTER = SolverEffects.AFTER; + // the parameters and result of a call, under names nothing else uses + private static final String ARGUMENT = "#argument_"; + private static final String RESULT = "#result"; private final TypeChecker tc; private final StateSolver solver; private final List states; + private final List ghostStates; + private final CtElement element; - private StateMachineBuilder(TypeChecker tc, StateSolver solver, List states) { + private StateMachineBuilder(TypeChecker tc, StateSolver solver, List states, List ghostStates, + CtElement element) { this.tc = tc; this.solver = solver; this.states = states; + this.ghostStates = ghostStates; + this.element = element; } /** Whether the transitions of {@code function} can be part of a machine: they only depend on the state of this */ @@ -74,7 +92,8 @@ public static Optional build(TypeChecker tc, StateSolver solver, S throws LJError { CtTypeReference type = tc.getFactory().Type().createReference(className); List> supertypes = supertypesOf(type); - List states = statesOf(ghostStatesOf(tc.getContext(), type, supertypes), false); + List ghostStates = ghostStatesOf(tc.getContext(), type, supertypes); + List states = statesOf(ghostStates, false); if (states.isEmpty() || states.size() > MAX_STATES) return Optional.empty(); Context context = tc.getContext(); @@ -82,7 +101,8 @@ public static Optional build(TypeChecker tc, StateSolver solver, S try { context.addVarToContext(BEFORE, type, new Predicate(), element); context.addVarToContext(AFTER, type, new Predicate(), element); - return Optional.of(new StateMachineBuilder(tc, solver, states).build(type, supertypes)); + StateMachineBuilder builder = new StateMachineBuilder(tc, solver, states, ghostStates, element); + return Optional.of(builder.build(type, supertypes)); } finally { context.exitContext(); } @@ -173,6 +193,14 @@ private static List statesOf(List ghostStates, boolean withNo return combinations; } + /** The states of each state set of the class on its own, in the order the sets are declared */ + private List> stateSets() { + return ghostStates.stream().filter(g -> g.getParent() != null) + .collect(Collectors.groupingBy(g -> g.getParent().getQualifiedName(), LinkedHashMap::new, + Collectors.mapping(StateMachineBuilder::inState, Collectors.toList()))) + .values().stream().toList(); + } + private static State inState(GhostState ghostState) { return new State(List.of(ghostState.getName()), Predicate.createInvocation(ghostState.getQualifiedName(), Predicate.createVar(Keys.THIS))); @@ -196,9 +224,11 @@ private StateMachine build(CtTypeReference type, List> sup List methods = new ArrayList<>(); List transitions = new ArrayList<>(); Map> constructors = new LinkedHashMap<>(); + List variants = new ArrayList<>(); boolean complete = !subclassChangesState(className, type, inherited); for (RefinedFunction function : tc.getContext().getCtxFunctions()) { - if (!function.hasStateChange()) + boolean query = !function.hasStateChange() && isQuery(function); + if (!function.hasStateChange() && !query) continue; boolean constructor = CtExecutableReference.CONSTRUCTOR_NAME.equals(function.getName()); boolean own = className.equals(function.getTargetClass()); @@ -216,7 +246,17 @@ private StateMachine build(CtTypeReference type, List> sup boolean applies = own ? appliesToOwnType(function, type, supertypes) : resolvesTo(function, type, supertypes) && publiclyInherited(function); if (!applies) { + if (!query) + complete = false; + continue; + } + if (query) { + variants.addAll(queryVariants(function, type)); + continue; + } + if (!canModel(function)) { complete = false; + variants.addAll(variantsOf(function, type)); continue; } Optional> calls = transitionsOf(function); @@ -227,7 +267,141 @@ private StateMachine build(CtTypeReference type, List> sup complete = false; } } - return new StateMachine(states, methods, transitions, constructors, complete); + return new StateMachine(states, methods, transitions, constructors, complete, variants); + } + + /** + * Whether {@code function} is a boolean method without state refinements whose return refinement relates its result + * to the states of this, e.g. {@code _ == true --> hasMore(this)} + */ + private boolean isQuery(RefinedFunction function) { + Predicate ret = function.getRefReturn(); + if (ret == null || !returnsBoolean(function) + || CtExecutableReference.CONSTRUCTOR_NAME.equals(function.getName())) + return false; + List names = ret.getVariableNames(); + return names.contains(Keys.WILDCARD) && !ret.getStateInvocations(ghostStates).isEmpty() + && names.stream().allMatch(n -> n.equals(Keys.THIS) || n.equals(Keys.WILDCARD)); + } + + /** The checks of the result of a query: true and false */ + private List queryVariants(RefinedFunction function, CtTypeReference type) { + SolverEffects.Scope scope = new SolverEffects.Scope(tc, solver, states, stateSets(), type, + Map.of(RESULT, function.getType()), element); + Predicate ret = function.getRefReturn().substituteVariable(Keys.WILDCARD, RESULT); + return resultConditions().stream().map(c -> new CallVariant(function, CallVariant.Kind.RESULT, c, + SolverEffects.ofQuery(scope, ret, c.substituteVariable(Keys.WILDCARD, RESULT)))).toList(); + } + + /** + * The ways to call {@code function}, whose state refinements also mention its parameters or result: with any + * arguments; with arguments that meet each condition on them that its refinements test, and with arguments that do + * not; and, for a boolean result its refinements mention, checking that the result is true or false. Nothing if the + * refinements mention anything else. + */ + private List variantsOf(RefinedFunction function, CtTypeReference type) { + Map renamed = new LinkedHashMap<>(); + Map> free = new LinkedHashMap<>(); + for (Variable parameter : function.getArguments()) { + renamed.put(parameter.getName(), ARGUMENT + parameter.getName()); + free.put(ARGUMENT + parameter.getName(), parameter.getType()); + } + if (returnsValue(function)) { + renamed.put(Keys.WILDCARD, RESULT); + free.put(RESULT, function.getType()); + } + List changes = function.getAllStates().stream().filter(ObjectState::hasFrom).toList(); + List predicates = changes.stream().flatMap(c -> Stream.of(c.getFrom(), c.getTo())) + .filter(Objects::nonNull).toList(); + Set known = new HashSet<>(renamed.keySet()); + known.add(Keys.THIS); + if (!predicates.stream().flatMap(p -> p.getVariableNames().stream()).allMatch(known::contains)) + return List.of(); + + List renamedChanges = changes.stream() + .map(c -> new ObjectState(rename(c.getFrom(), renamed), c.hasTo() ? rename(c.getTo(), renamed) : null)) + .toList(); + SolverEffects.Scope scope = new SolverEffects.Scope(tc, solver, states, stateSets(), type, free, element); + SolverEffects any = new SolverEffects(scope, renamedChanges, new Predicate(), false, null); + List variants = new ArrayList<>(); + variants.add(new CallVariant(function, CallVariant.Kind.ANY, new Predicate(), any)); + Set parameters = function.getArguments().stream().map(Variable::getName).collect(Collectors.toSet()); + for (Predicate condition : argumentConditions(predicates, parameters)) + variants.add(new CallVariant(function, CallVariant.Kind.ARGUMENTS, condition, + new SolverEffects(scope, renamedChanges, rename(condition, renamed), false, null))); + boolean resultMentioned = predicates.stream().anyMatch(p -> p.getVariableNames().contains(Keys.WILDCARD)); + if (returnsBoolean(function) && resultMentioned) + for (Predicate condition : resultConditions()) + variants.add(new CallVariant(function, CallVariant.Kind.RESULT, condition, + new SolverEffects(scope, renamedChanges, rename(condition, renamed), true, any))); + return variants; + } + + private static List resultConditions() { + Predicate result = Predicate.createVar(Keys.WILDCARD); + return List.of(result, result.negate()); + } + + /** + * The conditions on the parameters that {@code predicates} test, and their negations: the conditions of + * {@code c ? a : b}, the left sides of {@code -->} and the operands of {@code &&} that mention parameters and + * nothing else + */ + private static List argumentConditions(List predicates, Set parameters) { + List tested = new ArrayList<>(); + predicates.forEach(p -> collectTested(p.getExpression(), tested)); + Map conditions = new LinkedHashMap<>(); + for (Expression condition : tested) { + List mentioned = new ArrayList<>(); + condition.getVariableNames(mentioned); + if (mentioned.isEmpty() || !parameters.containsAll(mentioned) || invokesFunction(condition)) + continue; + for (Expression e : List.of(condition.clone(), negation(condition))) + conditions.putIfAbsent(e.toString(), new Predicate(e)); + } + return List.copyOf(conditions.values()); + } + + private static void collectTested(Expression e, List tested) { + if (e instanceof Ite ite) + tested.add(ite.getCondition()); + else if (e instanceof BinaryExpression b && (b.getOperator().equals("-->") || b.getOperator().equals("&&"))) + tested.add(b.getFirstOperand()); + if (e instanceof BinaryExpression b && b.getOperator().equals("&&")) + tested.add(b.getSecondOperand()); + e.getChildren().forEach(child -> collectTested(child, tested)); + } + + private static boolean invokesFunction(Expression e) { + return e instanceof FunctionInvocation + || e.getChildren().stream().anyMatch(StateMachineBuilder::invokesFunction); + } + + private static final Map NEGATED_COMPARISONS = Map.of("==", "!=", "!=", "==", "<", ">=", ">=", "<", + ">", "<=", "<=", ">"); + + /** The negation of {@code e}, written without {@code !} when it is a comparison or a negation */ + private static Expression negation(Expression e) { + if (e instanceof BinaryExpression b && NEGATED_COMPARISONS.containsKey(b.getOperator())) + return new BinaryExpression(b.getFirstOperand().clone(), NEGATED_COMPARISONS.get(b.getOperator()), + b.getSecondOperand().clone()); + if (e instanceof UnaryExpression u && u.getOp().equals("!")) + return u.getExpression().clone(); + return new UnaryExpression("!", e.clone()); + } + + private static Predicate rename(Predicate p, Map renamed) { + for (Map.Entry e : renamed.entrySet()) + p = p.substituteVariable(e.getKey(), e.getValue()); + return p; + } + + private static boolean returnsBoolean(RefinedFunction function) { + return function.getType() != null && Types.BOOLEAN.equals(function.getType().toString()); + } + + private static boolean returnsValue(RefinedFunction function) { + return function.getType() != null && !"void".equals(function.getType().toString()); } /** Whether a subclass has state refinements of its own, which the machine does not include */ 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 47eede86..c6d7ee87 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -53,8 +53,9 @@ void finalStateSuggestsCreatingANewObject() { } @Test - void transitionDependingOnArgumentsPreventsClaimingStateIsFinal() { - assertHints("ErrorStateHintIncomplete.java"); + 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")); } @Test @@ -147,8 +148,11 @@ void unknownStateDoesNotSuggestACallThatNeedsAnotherUnknownState() { @Test void unknownStateOfAnExternalClassNamesOnlyTheCheckedStateSet() { - assertHints("classes/state_hint_undo_manager_error", new Hint(Kind.NEEDED_STATE, - "The state of undoManager is unknown here, and this call needs it to be redoable")); + assertHints("classes/state_hint_undo_manager_error", + new Hint(Kind.NEEDED_STATE, + "The state of undoManager is unknown here, and this call needs it to be redoable"), + new Hint(Kind.GUARD, + "Guard this call with if (undoManager.canRedo()): when it returns true, undoManager is redoable")); } @Test @@ -175,12 +179,20 @@ void statesAreNamedOnlyInTheStateSetsThatMatter() { @Test void failedCheckOfTheReceiverIsNotAnUnknownState() { List errors = errors("classes/state_hint_checked_error", 3); - assertHints(errors.get(0), new Hint(Kind.NEEDED_STATE, - "What is known here does not decide the state of it, and this call needs it to be hasMore")); - assertHints(errors.get(1), new Hint(Kind.NEEDED_STATE, - "What is known here does not decide the state of same, and this call needs it to be hasMore")); - assertHints(errors.get(2), new Hint(Kind.NEEDED_STATE, - "The state of input is unknown here, and this call needs it to be hasMore")); + // the check is suggested even where it was made with the opposite result + assertHints(errors.get(0), + new Hint(Kind.NEEDED_STATE, + "What is known here does not decide the state of it, and this call needs it to be hasMore"), + new Hint(Kind.GUARD, "Guard this call with if (it.hasNext()): when it returns true, it is hasMore")); + assertHints(errors.get(1), + new Hint(Kind.NEEDED_STATE, + "What is known here does not decide the state of same, and this call needs it to be hasMore"), + new Hint(Kind.GUARD, + "Guard this call with if (same.hasNext()): when it returns true, same is hasMore")); + assertHints(errors.get(2), + new Hint(Kind.NEEDED_STATE, "The state of input is unknown here, and this call needs it to be hasMore"), + new Hint(Kind.GUARD, + "Guard this call with if (input.hasNext()): when it returns true, input is hasMore")); assertEquals(List.of(Optional.empty(), Optional.empty(), Optional.of(ErrorCategory.UNKNOWN)), errors.stream().map(LJError::getCategory).toList()); } @@ -241,6 +253,86 @@ void deciderIsTheLastCallThatChangedTheCheckedStateSet() { "param.setTilingMode(int) on line 25 decides the state of param: with mode == 2, this call would be allowed")); } + @Test + void checksAreSuggestedOnlyWhenTheRefinementsProveThem() { + List errors = errors("ErrorStateHintGuards.java", 11); + assertHints(errors.get(0), + new Hint(Kind.NEEDED_STATE, + "The state of c is unknown here, and this call needs it to be open. " + + "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(long)): 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")); + assertHints(errors.get(3), + new Hint(Kind.NEEDED_STATE, "The state of w is unknown here, and this call needs it to be accept")); + assertHints(errors.get(4), + new Hint(Kind.GUARD, "Guard this call with if (w.canWrite()): when it returns true, w is accept"), + new Hint(Kind.AVAILABLE_CALLS, "In state start, w can call: canWrite() (and possibly others)")); + assertHints(errors.get(5), new Hint(Kind.NEEDED_STATE, + "The state of b is unknown here, and this call needs it to be undoable and redoable")); + assertHints(errors.get(6), + new Hint(Kind.NEEDED_STATE, "The state of p is unknown here, and this call needs it to be armed")); + assertHints(errors.get(7), + new Hint(Kind.NEEDED_STATE, "The state of m is unknown here, and this call needs it to be s1")); + assertHints(errors.get(8), + new Hint(Kind.NEEDED_STATE, "The state of t is unknown here, and this call needs it to be fresh. " + + "Objects created with new GuardToken() start in such a state")); + assertHints(errors.get(9), + new Hint(Kind.AVAILABLE_CALLS, "In state live, r can call: read() (and possibly others)")); + assertHints(errors.get(10), + new Hint(Kind.NEEDED_STATE, "The state of g is unknown here, and this call needs it to be running")); + } + + @Test + void argumentConditionsAreSuggestedOnlyWhenEveryArgumentMeetingThemWorks() { + List 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"), + 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"), + 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"), + 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)) + assertHints(error, + new Hint(Kind.AVAILABLE_CALLS, "In state b, l can call: set(int) (and possibly others)")); + assertHints(errors.get(5), + new Hint(Kind.AVAILABLE_CALLS, "In state small, s can call: grow(int) (and possibly others)")); + assertHints(errors.get(6), + new Hint(Kind.AVAILABLE_CALLS, "In state empty, b can call: fill(ConditionBin) (and possibly others)")); + } + + @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"), + new Hint(Kind.AVAILABLE_CALLS, + "In state startCompression, wParam can call: setCompressionMode(int) (and possibly others)")); + } + + @Test + void checksOfTheStudysUndoManagerAreSuggestedOneAfterTheOther() { + List errors = errors("classes/state_hint_study_undo_manager_error", 2); + assertHints(errors.get(0), + new Hint(Kind.NEEDED_STATE, + "The state of undoManager is unknown here, and this call needs it to be redoable"), + new Hint(Kind.GUARD, + "Guard this call with if (undoManager.canRedo()): when it returns true, undoManager is redoable")); + assertHints(errors.get(1), new Hint(Kind.GUARD, + "Guard this call with if (undoManager.canUndo()): when it returns true, undoManager is undoable"), + new Hint(Kind.AVAILABLE_CALLS, + "In state undoable and notRedoable or notUndoable and notRedoable, undoManager can call: " + + "canUndo(), canRedo() (and possibly others)")); + } + @Test void classWithoutStateSetKeepsTheGeneralHint() { assertHints("ErrorUnconstrainedStateRefinement.java", Hint.general( diff --git a/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java b/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java index 24d4db72..3d2d25e1 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java @@ -1,14 +1,19 @@ package liquidjava.processor.state_machine; import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertFalse; +import static org.junit.jupiter.api.Assertions.assertTrue; import java.util.ArrayList; +import java.util.HashMap; +import java.util.HashSet; import java.util.List; import java.util.Map; import java.util.Set; import org.junit.jupiter.api.Test; +import liquidjava.processor.context.RefinedFunction; import liquidjava.rj_language.Predicate; class StateMachineTest { @@ -92,6 +97,82 @@ void statesOfOneSetAreNamedInDeclarationOrder() { machine(states).describe(Set.of(states.get(3), states.get(1)))); } + // three states of one set, for calls whose effects are given + private static final State A = state("a"); + private static final State B = state("b"); + private static final State C = state("c"); + private static final List ABC = List.of(A, B, C); + + @Test + void firstRefinementWhoseFromHoldsInEveryStateIsApplied() { + // a -> b, then a or c -> c: in a or c the verifier applies the second, as no single state tells it apart + CallVariant call = variant(new Effects(true, Map.of(A, Set.of(B))), + new Effects(true, Map.of(A, Set.of(C), C, Set.of(C)))); + StateMachine machine = machine(ABC, call); + assertTrue(machine.allows(Set.of(A, C), call)); + assertEquals(Set.of(C), machine.after(Set.of(A, C), call)); + assertEquals(Set.of(B), machine.after(Set.of(A), call)); + assertFalse(machine.allows(Set.of(B), call)); + } + + @Test + void refinementThatMayOrMayNotApplyBeforeTheApplicableOneAllowsNothing() { + Effects first = new Effects(true, Map.of(A, Set.of(B))); + first.undecided.add(C); + CallVariant call = variant(first, new Effects(true, Map.of(A, Set.of(C), C, Set.of(C)))); + assertFalse(machine(ABC, call).allows(Set.of(A, C), call)); + } + + @Test + void callThatKeepsTheStateNeedsEachStateToSatisfySomeFrom() { + CallVariant call = variant(new Effects(false, Map.of(A, Set.of(A))), new Effects(false, Map.of(C, Set.of(C)))); + StateMachine machine = machine(ABC, call); + assertEquals(Set.of(A, C), machine.after(Set.of(A, C), call)); + assertFalse(machine.allows(Set.of(A, B), call)); + } + + @Test + void callWhoseStatesAfterAreUnknownIsNotAllowed() { + Map> after = new HashMap<>(); + after.put(A, null); + CallVariant call = variant(new Effects(true, after)); + assertFalse(machine(ABC, call).allows(Set.of(A), call)); + } + + /** Effects given by hand: the states where each refinement's from holds, and the states after the call from each */ + private record Effects(boolean changesState, Map> after, Set undecided) { + Effects(boolean changesState, Map> after) { + this(changesState, after, new HashSet<>()); + } + } + + private static CallVariant variant(Effects... refinements) { + CallVariant.Effects effects = new CallVariant.Effects() { + public int refinements() { + return refinements.length; + } + + public boolean changesState(int index) { + return refinements[index].changesState(); + } + + public CallVariant.Entry entry(int index, State state) { + Effects e = refinements[index]; + return e.after().containsKey(state) ? CallVariant.Entry.HOLDS + : e.undecided().contains(state) ? CallVariant.Entry.UNDECIDED : CallVariant.Entry.FAILS; + } + + public Set after(int index, State state) { + return refinements[index].after().get(state); + } + }; + return new CallVariant(new RefinedFunction(), CallVariant.Kind.ANY, new Predicate(), effects); + } + + private static StateMachine machine(List states, CallVariant variant) { + return new StateMachine(states, List.of(), List.of(), Map.of(), false, List.of(variant)); + } + private static StateMachine machine(List states) { return new StateMachine(states, List.of(), List.of(), Map.of(), true); } From 9f90bd59ab081421459d70a7f398da983a84913a Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 4 Nov 2026 11:43:27 +0000 Subject: [PATCH 2/2] Write guard checks with the parameters' names, so the suggested if compiles Co-Authored-By: Claude Opus 5.5 --- .../java/liquidjava/diagnostics/hints/StateHints.java | 8 +++++++- .../test/java/liquidjava/api/tests/TestStateHints.java | 2 +- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java index 48fd7d52..3ce503ef 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java @@ -152,7 +152,7 @@ private List guard(Set current, RefinedFunction call) { return List.of(); CallVariant guard = guards.get(0); boolean negated = guard.negatedResult(); - String check = (negated ? "!" : "") + call(guard.method()); + 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()); return List.of(new Hint(Kind.GUARD, message)); @@ -208,6 +208,12 @@ 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 step of a sequence, with the condition on its arguments if it has one, e.g. * {@code p.setMode(int) with mode == 2} 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 c6d7ee87..c1b3fa47 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -262,7 +262,7 @@ 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(long)): when it returns true, l is locked"), + new Hint(Kind.GUARD, "Guard this call with if (l.tryLock(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"));