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..3ce503ef 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 ? "!" : "") + 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)); + } + + 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,22 @@ 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} + */ + 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..c1b3fa47 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(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")); + 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); }