diff --git a/liquidjava-example/src/main/java/testSuite/classes/bytebuf_correct/ByteBufTest.java b/liquidjava-example/src/main/java/testSuite/classes/bytebuf_correct/ByteBufTest.java new file mode 100644 index 000000000..7124c64d9 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/bytebuf_correct/ByteBufTest.java @@ -0,0 +1,23 @@ +package testSuite.classes.bytebuf_correct; + +// SO 48582520 — UnsupportedOperationException at ByteBuffer.array() +// https://stackoverflow.com/questions/48582520 +// SO class is already self-contained pure java.nio; only added the package. +import java.nio.ByteBuffer; + +public class ByteBufTest { + + public static final int TEST_BUFFER_SIZE = 128; + + // private ByteBuffer mDirectBuffer; + + public ByteBufTest() { + // FIX (from accepted answer): mDirectBuffer = ByteBuffer.wrap(new byte[TEST_BUFFER_SIZE]); + // or guard with: if (mDirectBuffer.hasArray()) { ... } + ByteBuffer mDirectBuffer = ByteBuffer.wrap(new byte[TEST_BUFFER_SIZE]); + // VIOLATION: a direct buffer is not array-backed -> array() throws + // UnsupportedOperationException. + byte[] buf = mDirectBuffer.array(); + buf[1] = 100; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/bytebuf_correct/ByteBufferRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/bytebuf_correct/ByteBufferRefinements.java new file mode 100644 index 000000000..e18e7deec --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/bytebuf_correct/ByteBufferRefinements.java @@ -0,0 +1,41 @@ +package testSuite.classes.bytebuf_correct; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Ghost; +import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementAlias; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +import java.nio.ByteBuffer; +import java.nio.ByteOrder; +import java.nio.CharBuffer; +import java.nio.ShortBuffer; +import java.nio.IntBuffer; +import java.nio.LongBuffer; +import java.nio.FloatBuffer; +import java.nio.DoubleBuffer; + + +@Ghost("boolean arrayBacked") +@ExternalRefinementsFor("java.nio.ByteBuffer") +public interface ByteBufferRefinements { + + // ---- Backing array access ---- + + @StateRefinement(to="_ ? arrayBacked() : !arrayBacked()") + boolean hasArray(); + + @StateRefinement(from="arrayBacked()") + byte[] array(); + + @StateRefinement(from="arrayBacked()") + int arrayOffset(); + + @Refinement("arrayBacked(_)") + ByteBuffer wrap(byte[] array, int offset, int length); + + @Refinement("arrayBacked(_)") + ByteBuffer wrap(byte[] array); + + } diff --git a/liquidjava-example/src/main/java/testSuite/classes/bytebuf_error/ByteBufTest.java b/liquidjava-example/src/main/java/testSuite/classes/bytebuf_error/ByteBufTest.java new file mode 100644 index 000000000..b547f7940 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/bytebuf_error/ByteBufTest.java @@ -0,0 +1,41 @@ +package testSuite.classes.bytebuf_error; + +// SO 48582520 — UnsupportedOperationException at ByteBuffer.array() +// https://stackoverflow.com/questions/48582520 +// SO class is already self-contained pure java.nio; only added the package. +import java.nio.ByteBuffer; + +public class ByteBufTest { + + public static final int TEST_BUFFER_SIZE = 128; + + // private ByteBuffer mDirectBuffer; + + public ByteBufTest() { + // FIX (from accepted answer): mDirectBuffer = ByteBuffer.wrap(new byte[TEST_BUFFER_SIZE]); + // or guard with: if (mDirectBuffer.hasArray()) { ... } + ByteBuffer mDirectBuffer = ByteBuffer.allocateDirect(TEST_BUFFER_SIZE); + // VIOLATION: a direct buffer is not array-backed -> array() throws + // UnsupportedOperationException. + byte[] buf = mDirectBuffer.array(); // State Refinement Error + buf[1] = 100; + } + + public void test(ByteBuffer mDirectBuffer) { + printBuffer("nativeInitDirectBuffer", mDirectBuffer.array()); // State Refinement Error + } + + private void printBuffer(String tag, byte[] buffer) { + StringBuffer sBuffer = new StringBuffer(); + for (int i = 0; i < buffer.length; i++) { + sBuffer.append(buffer[i]); + sBuffer.append(" "); + } + } + + public static void main(String[] args) throws Exception { + ByteBufTest item = new ByteBufTest(); + ByteBuffer mDirectBuffer = ByteBuffer.allocateDirect(128); + item.test(mDirectBuffer); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/bytebuf_error/ByteBufferRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/bytebuf_error/ByteBufferRefinements.java new file mode 100644 index 000000000..c3e056024 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/bytebuf_error/ByteBufferRefinements.java @@ -0,0 +1,41 @@ +package testSuite.classes.bytebuf_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Ghost; +import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementAlias; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +import java.nio.ByteBuffer; +import java.nio.ByteOrder; +import java.nio.CharBuffer; +import java.nio.ShortBuffer; +import java.nio.IntBuffer; +import java.nio.LongBuffer; +import java.nio.FloatBuffer; +import java.nio.DoubleBuffer; + + +@Ghost("boolean arrayBacked") +@ExternalRefinementsFor("java.nio.ByteBuffer") +public interface ByteBufferRefinements { + + // ---- Backing array access ---- + + @StateRefinement(to="_ ? arrayBacked() : !arrayBacked()") + boolean hasArray(); + + @StateRefinement(from="arrayBacked()") + byte[] array(); + + @StateRefinement(from="arrayBacked()") + int arrayOffset(); + + @Refinement("arrayBacked(_)") + ByteBuffer wrap(byte[] array, int offset, int length); + + @Refinement("arrayBacked(_)") + ByteBuffer wrap(byte[] array); + + } diff --git a/liquidjava-example/src/main/java/testSuite/classes/iterator_queue_error/IteratorRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/iterator_queue_error/IteratorRefinements.java new file mode 100644 index 000000000..3af73c39f --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/iterator_queue_error/IteratorRefinements.java @@ -0,0 +1,28 @@ +package testSuite.classes.iterator_queue_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +/** + * Observer-style iteration over {@link java.util.Scanner} (an iterator-shaped JDK class): + * {@code hasNext} is an informative check (no state change), and {@code next} consumes one + * element, resetting state so a fresh check is required before the next consumption. + * + *

{@code java.util.Iterator} itself is an interface, and external refinements only attach to + * classes — Scanner gives us the same API in a class form. + */ +@StateSet({"hasMore", "inNext", "notInNext"}) +@ExternalRefinementsFor("java.util.Iterator") +public interface IteratorRefinements { + + @StateRefinement(to = "_ --> hasMore()") + boolean hasNext(); + + @StateRefinement(from = "hasMore()", to = "inNext()") + N next(); + + @StateRefinement(from="inNext()", to="notInNext()") + void remove(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/iterator_queue_error/IteratorRemoveBeforeNext.java b/liquidjava-example/src/main/java/testSuite/classes/iterator_queue_error/IteratorRemoveBeforeNext.java new file mode 100644 index 000000000..c16c52e2c --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/iterator_queue_error/IteratorRemoveBeforeNext.java @@ -0,0 +1,64 @@ +package testSuite.classes.iterator_queue_error; + +// SO 22361194 — "Iterator.remove() IllegalStateException" +// https://stackoverflow.com/questions/22361194 +// Faithful to the question body. The asker's own (unshown) types are given +// minimal stand-ins so the original structure compiles: +// - the queues qev1/qev2/qcv1/qcv2 -> a small Queue exposing enqueue()/iterator() +// - CInteger -> the nested class below +// The asker catches UnsupportedOperationException, but iterator().remove() +// before next() actually throws IllegalStateException — so the catch does NOT +// fire. That mismatch is reproduced verbatim from the post. +import java.util.ArrayList; +import java.util.Date; +import java.util.Iterator; + +public class IteratorRemoveBeforeNext { + + static class Queue implements Iterable { + private final ArrayList items = new ArrayList<>(); + void enqueue(T item) { items.add(item); } + public Iterator iterator() { return items.iterator(); } + } + + static class CInteger { + final int value; + CInteger(int value) { this.value = value; } + } + + public static void main(String[] args) { + Queue qev1 = new Queue<>(); + Queue qev2 = new Queue<>(); + Queue qcv1 = new Queue<>(); + Queue qcv2 = new Queue<>(); + Object ci = new CInteger(0); + + try { + // VIOLATION: remove() before next() -> IllegalStateException + // (NOT UnsupportedOperationException, so this catch does not fire). + Iterator it = qev1.iterator(); + it.remove(); // State Refinement Error + } catch (UnsupportedOperationException e) { + System.out.println("Calling Iterator.remove() and throwing exception."); + } + + qev1.enqueue(ci); + qev2.enqueue(ci); + qcv1.enqueue(ci); + qcv2.enqueue(ci); + + for (int i = 1; i < 5; i++) { + if (i % 2 == 0) { + qev1.enqueue(new CInteger(i + 1)); + qev2.enqueue(new CInteger(i + 1)); + qcv1.enqueue(new CInteger(i + 1)); + qcv2.enqueue(new CInteger(i + 1)); + } else { + qev1.enqueue(new Date(i * i)); + qev2.enqueue(new Date(i * i)); + qcv1.enqueue(new Date(i * i)); + qcv2.enqueue(new Date(i * i)); + } + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ConnectionRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ConnectionRefinements.java new file mode 100644 index 000000000..b036c5ce9 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ConnectionRefinements.java @@ -0,0 +1,21 @@ +package testSuite.classes.resultset_forward_correct; +import java.sql.PreparedStatement; +import java.sql.ResultSet; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; + + +@ExternalRefinementsFor("java.sql.Connection") +public interface ConnectionRefinements { + + // Default statements are forward-only: the produced ResultSet cannot scroll backwards. + @Refinement("setBackwards(_) == false") + PreparedStatement prepareStatement(String sql); + + // Explicit type decides scrollability: only TYPE_FORWARD_ONLY forbids backward scrolling. + @Refinement("resultSetType == ResultSet.TYPE_FORWARD_ONLY ? setBackwards(_) == false : setBackwards(_) == true") + PreparedStatement prepareStatement(String sql, int resultSetType, + int resultSetConcurrency); + + } diff --git a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/PreparedStatementRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/PreparedStatementRefinements.java new file mode 100644 index 000000000..ce33d6a57 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/PreparedStatementRefinements.java @@ -0,0 +1,21 @@ +package testSuite.classes.resultset_forward_correct; + +import java.sql.ResultSet; +import java.sql.SQLException; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Ghost; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + + +@Ghost("boolean setBackwards") +@ExternalRefinementsFor("java.sql.PreparedStatement") +public interface PreparedStatementRefinements { + + // The ResultSet inherits the statement's scrollability: backward-capable statements + // yield an allowsBackward ResultSet, forward-only statements yield an onlyForward one. + @Refinement("setBackwards(this) ? allowsBackward(_) : onlyForward(_)") + ResultSet executeQuery(); +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetRefinements.java new file mode 100644 index 000000000..04d59decb --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetRefinements.java @@ -0,0 +1,22 @@ +package testSuite.classes.resultset_forward_correct; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"onlyForward", "allowsBackward"}) +@StateSet({"beforeRow", "onRow", "endRows"}) + +@ExternalRefinementsFor("java.sql.ResultSet") +public interface ResultSetRefinements { + + @StateRefinement(to = "_ ? onRow(this) : endRows(this)") + boolean next(); + + @StateRefinement(from = "onRow(this)") + float getFloat(String columnIndex); + + @StateRefinement(from = "allowsBackward()") + void beforeFirst(); + +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java new file mode 100644 index 000000000..f865a82c9 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java @@ -0,0 +1,65 @@ +package testSuite.classes.resultset_forward_correct; + + +// SO 6367737 — "ResultSet: Exception: set type is TYPE_FORWARD_ONLY -- why?" +// https://stackoverflow.com/questions/6367737 +// Counting rows by iterating, then calling rs.beforeFirst() to rewind and iterate +// again. A default ResultSet is TYPE_FORWARD_ONLY, so the backward scroll throws: +// java.sql.SQLException: Result set type is TYPE_FORWARD_ONLY +// at ...JdbcOdbcResultSet.beforeFirst(...) +// Kept as close to the question as possible; the SO lines are wrapped in a method +// taking a Connection. Pure java.sql; compiles with no JDBC driver present. +import java.sql.Connection; +import java.sql.PreparedStatement; +import java.sql.ResultSet; +import java.sql.SQLException; +import java.sql.Statement; + +public class ResultSetTests { + + int login(Connection con, String username, String password) throws SQLException { + int typeID = 0; + + PreparedStatement pstat = + con.prepareStatement("select typeid from users where username=? and password=?", ResultSet.TYPE_SCROLL_INSENSITIVE, ResultSet.CONCUR_READ_ONLY); + ResultSet rs = pstat.executeQuery(); + + rs.beforeFirst(); // State Refinement Error + + return typeID; + } + + int login2(Connection con, String username, String password) throws SQLException { + int typeID = 0; + PreparedStatement pstat = + con.prepareStatement("select typeid from users where username=? and password=?", ResultSet.TYPE_SCROLL_INSENSITIVE, ResultSet.CONCUR_READ_ONLY); + pstat.setString(1, username); + pstat.setString(2, password); + ResultSet rs = pstat.executeQuery(); + int rowCount = 0; + while (rs.next()) { + rowCount++; + } + rs.beforeFirst(); // State Refinement Error + if (rowCount >= 1) { + while (rs.next()) { + typeID = rs.getInt(1); + } + } + return typeID; + } + + float readAverage(Connection conn) throws SQLException { + Statement parentstmt = conn.createStatement(); + ResultSet parentMessage = + parentstmt.executeQuery("SELECT SUM(IMPORTANCE) AS IMPAVG FROM MAIL"); + // FIX (from accepted answer): parentMessage.next(); + // VIOLATION: cursor is before the first row; getFloat() with no next(). + if( parentMessage.next()) { + float avgsum = parentMessage.getFloat("IMPAVG"); + return avgsum; + } else { + return 0.0f; + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ConnectionRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ConnectionRefinements.java new file mode 100644 index 000000000..c582138e7 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ConnectionRefinements.java @@ -0,0 +1,21 @@ +package testSuite.classes.resultset_forward_error; +import java.sql.PreparedStatement; +import java.sql.ResultSet; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; + + +@ExternalRefinementsFor("java.sql.Connection") +public interface ConnectionRefinements { + + // Default statements are forward-only: the produced ResultSet cannot scroll backwards. + @Refinement("setBackwards(_) == false") + PreparedStatement prepareStatement(String sql); + + // Explicit type decides scrollability: only TYPE_FORWARD_ONLY forbids backward scrolling. + @Refinement("resultSetType == ResultSet.TYPE_FORWARD_ONLY ? setBackwards(_) == false : setBackwards(_) == true") + PreparedStatement prepareStatement(String sql, int resultSetType, + int resultSetConcurrency); + + } diff --git a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/PreparedStatementRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/PreparedStatementRefinements.java new file mode 100644 index 000000000..27f6446e3 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/PreparedStatementRefinements.java @@ -0,0 +1,21 @@ +package testSuite.classes.resultset_forward_error; + +import java.sql.ResultSet; +import java.sql.SQLException; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Ghost; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + + +@Ghost("boolean setBackwards") +@ExternalRefinementsFor("java.sql.PreparedStatement") +public interface PreparedStatementRefinements { + + // The ResultSet inherits the statement's scrollability: backward-capable statements + // yield an allowsBackward ResultSet, forward-only statements yield an onlyForward one. + @Refinement("setBackwards(this) ? allowsBackward(_) : onlyForward(_) && beforeRow(_)") + ResultSet executeQuery(); +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetRefinements.java new file mode 100644 index 000000000..ae550bbdf --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetRefinements.java @@ -0,0 +1,22 @@ +package testSuite.classes.resultset_forward_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"onlyForward", "allowsBackward"}) +@StateSet({"beforeRow", "onRow", "endRows"}) + +@ExternalRefinementsFor("java.sql.ResultSet") +public interface ResultSetRefinements { + + @StateRefinement(to = "_ ? onRow(this) : endRows(this)") + boolean next(); + + @StateRefinement(from = "onRow(this)") + float getFloat(String columnIndex); + + @StateRefinement(from = "allowsBackward()") + void beforeFirst(); + +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetTests.java b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetTests.java new file mode 100644 index 000000000..508b09a82 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetTests.java @@ -0,0 +1,70 @@ +package testSuite.classes.resultset_forward_error; + + +// SO 6367737 — "ResultSet: Exception: set type is TYPE_FORWARD_ONLY -- why?" +// https://stackoverflow.com/questions/6367737 +// Counting rows by iterating, then calling rs.beforeFirst() to rewind and iterate +// again. A default ResultSet is TYPE_FORWARD_ONLY, so the backward scroll throws: +// java.sql.SQLException: Result set type is TYPE_FORWARD_ONLY +// at ...JdbcOdbcResultSet.beforeFirst(...) +// Kept as close to the question as possible; the SO lines are wrapped in a method +// taking a Connection. Pure java.sql; compiles with no JDBC driver present. +import java.sql.Connection; +import java.sql.PreparedStatement; +import java.sql.ResultSet; +import java.sql.SQLException; +import java.sql.Statement; + +public class ResultSetTests { + + int login(Connection con, String username, String password) throws SQLException { + int typeID = 0; + + PreparedStatement pstat = + con.prepareStatement("select typeid from users where username=? and password=?"); + ResultSet rs = pstat.executeQuery(); + + // The default ResultSet is TYPE_FORWARD_ONLY, so the next line cannot rewind: + // beforeFirst() requires a scrollable (allowsBackward) ResultSet. + // FIX (accepted answers): request a scrollable result set, e.g. + // con.prepareStatement(sql, ResultSet.TYPE_SCROLL_INSENSITIVE, + // ResultSet.CONCUR_READ_ONLY); + // or drop the rewind and read typeID inside the single forward pass. + rs.beforeFirst(); // State Refinement Error + + return typeID; + } + + int login2(Connection con, String username, String password) throws SQLException { + int typeID = 0; + PreparedStatement pstat = + con.prepareStatement("select typeid from users where username=? and password=?"); + pstat.setString(1, username); + pstat.setString(2, password); + ResultSet rs = pstat.executeQuery(); + int rowCount = 0; + while (rs.next()) { + rowCount++; + } + // VIOLATION: beforeFirst() scrolls backward, illegal on a TYPE_FORWARD_ONLY + // result set -> SQLException: Result set type is TYPE_FORWARD_ONLY. + rs.beforeFirst(); // State Refinement Error + if (rowCount >= 1) { + while (rs.next()) { + typeID = rs.getInt(1); + } + } + return typeID; + } + + + float readAverage(Connection conn) throws SQLException { + Statement parentstmt = conn.createStatement(); + ResultSet parentMessage = + parentstmt.executeQuery("SELECT SUM(IMPORTANCE) AS IMPAVG FROM MAIL"); + // FIX (from accepted answer): parentMessage.next(); + // VIOLATION: cursor is before the first row; getFloat() with no next(). + float avgsum = parentMessage.getFloat("IMPAVG"); // State Refinement Error + return avgsum; + } +}