diff --git a/.github/workflows/gradle.yml b/.github/workflows/gradle.yml index 3fe6698..5e71e2e 100644 --- a/.github/workflows/gradle.yml +++ b/.github/workflows/gradle.yml @@ -2,9 +2,9 @@ name: Build and Test on: push: - branches: [ master, main, gradle-support ] + branches: [ master, main, java-11-work ] pull_request: - branches: [ master, main, gradle-support ] + branches: [ master, main, java-11-work ] jobs: build: diff --git a/build.gradle b/build.gradle index b31c238..86ebab6 100644 --- a/build.gradle +++ b/build.gradle @@ -147,6 +147,28 @@ tasks.withType(JavaCompile).configureEach { } +tasks.register('compareMetaInf', Task) { + doLast { + def jpfCoreJar = jpf.Jar.getFullPath() + def jpfCoreDir = new File(jpfCoreJar).parent + def jpfCoreClassesJar = "${jpfCoreDir}/jpf-classes.jar" + def jpfNasClassesJar = "${buildDir}/libs/jpf-nas-classes.jar" + + println "=== JPF-Core META-INF ===" + exec { + commandLine 'jar', 'tf', jpfCoreClassesJar + standardOutput = System.out + } + + println "\n=== JPF-NAS META-INF ===" + exec { + commandLine 'jar', 'tf', jpfNasClassesJar + standardOutput = System.out + } + } +} + + test { dependsOn tasks.named('jar') dependsOn tasks.named('modelJar') @@ -168,16 +190,6 @@ test { forkEvery = 1 } -jar { - dependsOn tasks.named('modelJar') - archiveBaseName = 'jpf-nas' - from sourceSets.main.output - manifest { - attributes( - 'Implementation-Title': 'Java Pathfinder NAS extension', - ) - } -} artifacts { archives tasks.named('jar') @@ -203,4 +215,4 @@ publishing { artifactId = 'jpf-nas-examples' } } -} +} \ No newline at end of file diff --git a/jpf.properties b/jpf.properties index 2405f5f..8347250 100644 --- a/jpf.properties +++ b/jpf.properties @@ -3,15 +3,15 @@ jpf-nas = ${config_path} @using jpf-core jpf-nas.classpath = \ - ${jpf-nas}/build/modules\ - ${jpf-nas}/build/libs/jpf-nas-classes.jar;\ - ${jpf-nas}/build/classes/java/main;\ - ${jpf-nas}/build/classes/java/test;\ - ${jpf-nas}/build/classes/java/examples + ${jpf-nas}/build/classes/java/main:\ + ${jpf-nas}/build/classes/java/test:\ + ${jpf-nas}/build/classes/java/examples:\ + ${jpf-nas}/build/classes/modules:\ + ${jpf-nas}/build/libs/jpf-nas-classes.jar jpf-nas.native_classpath = \ - ${jpf-nas}/build/libs/jpf-nas.jar;\ - ${jpf-nas}/lib/*.jar + ${jpf-nas}/build/libs/jpf-nas.jar:\ + ${jpf-nas}/lib/*.jar jpf-nas.peer_packages = nas.java.net vm.class = nas.NasVM @@ -20,3 +20,4 @@ vm.process_finalizers = true vm.nas.initiating_target = -1 target=nas.util.test.TestNasJPF +vm.serializer.class = gov.nasa.jpf.vm.serialize.CFSerializer \ No newline at end of file diff --git a/src/classes/modules/java.base/java/net/ServerSocket.java b/src/classes/modules/java.base/java/net/ServerSocket.java index a5b9904..628467d 100644 --- a/src/classes/modules/java.base/java/net/ServerSocket.java +++ b/src/classes/modules/java.base/java/net/ServerSocket.java @@ -4,11 +4,22 @@ /** * Model class for java.net.ServerSocket - * + * * @author Nastaran Shafiei */ public class ServerSocket implements java.io.Closeable { + static { + System.out.println("DEBUG: JPF ServerSocket MODEL CLASS loaded successfully!"); + try { + System.out.println("DEBUG: ServerSocket model class location: " + + ServerSocket.class.getProtectionDomain().getCodeSource().getLocation()); + } catch (UnsupportedOperationException e) { + System.out.println("DEBUG: ServerSocket model class location: [JPF environment - getProtectionDomain not supported]"); + } + } + + /** * The implementation of this Socket. */ @@ -26,11 +37,12 @@ public class ServerSocket implements java.io.Closeable { /** * This creates a 'bound' socket which is ready for ServerSocket.accept() to * be called. - * + * * @param port * the local port on which this socket listen for connections */ public ServerSocket (int port) throws IOException { + System.out.println("DEBUG: ServerSocket MODEL CLASS constructor called with port: " + port); CheckForAddressAlreadyInUse(port); SocketImpl.checkPort(port); impl = new SocketImpl(); @@ -41,6 +53,7 @@ public ServerSocket (int port) throws IOException { private native void CheckForAddressAlreadyInUse (int port); void setBound () { + System.out.println("DEBUG: ServerSocket MODEL CLASS setBound() called"); this.bound = true; } @@ -49,9 +62,9 @@ void setBound () { * ServerSocket.bind() before ServerSocket.accept() is invoked */ public ServerSocket () throws IOException { - + System.out.println("DEBUG: ServerSocket MODEL CLASS default constructor called"); } - + private Object lock = new Object(); private Socket acceptedSocket; @@ -65,11 +78,12 @@ public ServerSocket () throws IOException { * socket which represents its end of the connection */ public Socket accept () throws IOException { + System.out.println("DEBUG: ServerSocket MODEL CLASS accept() called"); if (isClosed()) { throw new SocketException("Socket is closed"); - } + } // TODO: check for the "unbound" state - + // The IO buffers of this socket are shared natively with the client socket // at the other end acceptedSocket = new Socket(); @@ -87,14 +101,16 @@ public boolean isClosed () { // TODO: Throws IOException, if an I/O error occurs when closing the socket @Override public native synchronized void close (); - + private int timeout; public void setSoTimeout(int timeout) { + System.out.println("DEBUG: ServerSocket MODEL CLASS setSoTimeout() called with timeout: " + timeout); this.timeout = timeout; } - + @Override protected void finalize() throws Throwable{ + System.out.println("DEBUG: ServerSocket MODEL CLASS finalize() called"); close(); } -} +} \ No newline at end of file diff --git a/src/classes/modules/java.base/java/net/Socket.java b/src/classes/modules/java.base/java/net/Socket.java index 82c6799..5983f9e 100644 --- a/src/classes/modules/java.base/java/net/Socket.java +++ b/src/classes/modules/java.base/java/net/Socket.java @@ -4,28 +4,38 @@ import java.io.InputStream; import java.io.OutputStream; -/** +/** * Model class for java.net.Socket - * + * * @author Nastaran Shafiei */ public class Socket implements java.io.Closeable { + static { + System.out.println("DEBUG: JPF Socket MODEL CLASS loaded successfully!"); + try { + System.out.println("DEBUG: Socket model class location: " + + Socket.class.getProtectionDomain().getCodeSource().getLocation()); + } catch (UnsupportedOperationException e) { + System.out.println("DEBUG: Socket model class location: [JPF environment - getProtectionDomain not supported]"); + } + } + private SocketInputStream input = null; private SocketOutputStream output = null; - + /** - * This is used to make JPF account for connection objects when state matching. This - * keep the hash value of this socket connection object, and it is updated upon any - * internal change to the connection + * This is used to make JPF account for connection objects when state matching. + * Keep the hash value of this socket connection object, and it is updated upon any + * internal change to the connection */ private int hash; - + /** * The implementation of this Socket. */ - SocketImpl impl; - + SocketImpl impl; + /** * Various states of this socket. */ @@ -38,13 +48,16 @@ public class Socket implements java.io.Closeable { private Thread waitingThread; public Socket() { + System.out.println("DEBUG: Socket MODEL CLASS default constructor called"); impl = new SocketImpl(); impl.setSocket(this); impl.bind(-1); this.setIOStream(); + System.out.println("DEBUG: Socket() constructor completed, hash=" + hash); } public Socket(String host, int port) throws UnknownHostException, IOException { + System.out.println("DEBUG: Socket MODEL CLASS constructor called with host=" + host + ", port=" + port); SocketImpl.checkPort(port); impl = new SocketImpl(); impl.setSocket(this); @@ -53,87 +66,95 @@ public Socket(String host, int port) throws UnknownHostException, IOException { impl.port = port; this.setIOStream(); connect(host, port); + System.out.println("DEBUG: Socket(host, port) constructor completed, connected=" + connected); } private void setIOStream() { + System.out.println("DEBUG: Socket MODEL CLASS setIOStream() called"); this.input = new SocketInputStream(this); this.output = new SocketOutputStream(this); } - public Socket(InetAddress address, int port) throws UnknownHostException, IOException { - this(address.getHostName(), port); - } - private native void connect(String host, int port) throws IOException; + public int getHash() { + System.out.println("DEBUG: Socket MODEL CLASS getHash() called, returning hash=" + hash); return this.hash; } + public void connect(SocketAddress endpoint) throws IOException { + System.out.println("DEBUG: Socket MODEL CLASS connect(SocketAddress) called"); connect(endpoint, 0); } - + public void connect(SocketAddress endpoint, int timeout) throws IOException { - // TODO: for timeout, look at wait() implementation + System.out.println("DEBUG: Socket MODEL CLASS connect(SocketAddress, timeout=" + timeout + ") called"); String host = ((InetSocketAddress)endpoint).getHostName(); int port = ((InetSocketAddress)endpoint).getPort(); connect(host, port); } void setBound() { + System.out.println("DEBUG: Socket MODEL CLASS setBound() called"); bound = true; } public InputStream getInputStream() throws IOException { + System.out.println("DEBUG: Socket MODEL CLASS getInputStream() called, closed=" + closed + ", connected=" + connected); if (isClosed()) { throw new SocketException("Socket is closed"); } else if (!isConnected()) { throw new SocketException("Socket is not connected"); } - + assert(!isClosed()); assert(isConnected()); - + return input; } public OutputStream getOutputStream() throws IOException { + System.out.println("DEBUG: Socket MODEL CLASS getOutputStream() called, closed=" + closed + ", connected=" + connected); if (isClosed()) { throw new SocketException("Socket is closed"); } else if (!isConnected()) { throw new SocketException("Socket is not connected"); } - + assert(!isClosed()); assert(isConnected()); - + return output; } - + /** * Returns the closed state of the socket. */ public boolean isClosed() { return this.closed; } - + /** * Returns the connection state of the socket. */ public native boolean isConnected(); - - // TODO: Any thread currently blocked in an I/O operation upon this socket - // will throw a SocketException. - // TODO: Throws IOException, if an I/O error occurs when closing the socket + @Override public native void close() throws IOException; - + private int timeout; public void setSoTimeout(int timeout) { + System.out.println("DEBUG: Socket MODEL CLASS setSoTimeout(" + timeout + ") called"); this.timeout = timeout; } - + @Override protected void finalize() throws Throwable{ + System.out.println("DEBUG: Socket MODEL CLASS finalize() called"); close(); } + + public Socket(InetAddress address, int port) throws UnknownHostException, IOException { + this(address.getHostName(), port); + } } diff --git a/src/peers/nas/java/net/JPF_java_net_ServerSocket.java b/src/peers/nas/java/net/JPF_java_net_ServerSocket.java index 0fdb8d6..7a66aff 100644 --- a/src/peers/nas/java/net/JPF_java_net_ServerSocket.java +++ b/src/peers/nas/java/net/JPF_java_net_ServerSocket.java @@ -34,6 +34,15 @@ public String getServerHost (MJIEnv env, int serverSocketRef) { return host; } + @MJI + public void CheckForAddressAlreadyInUse__I__V (MJIEnv env, int serverSocketRef, int port) { + boolean inUse = connections.isAddressInUse(getServerHost(env, serverSocketRef), port); + if (inUse) { + env.throwException("java.net.BindException", "Address already in use"); + } + } + + public int getServerPort (MJIEnv env, int serverSocketRef) { int implRef = env.getElementInfo(serverSocketRef).getReferenceField("impl"); int port = env.getElementInfo(implRef).getIntField("localPort"); diff --git a/src/peers/nas/java/net/JPF_java_net_Socket.java b/src/peers/nas/java/net/JPF_java_net_Socket.java index a8a7158..0b4c5af 100644 --- a/src/peers/nas/java/net/JPF_java_net_Socket.java +++ b/src/peers/nas/java/net/JPF_java_net_Socket.java @@ -44,28 +44,46 @@ protected boolean hostExists(MJIEnv env, String host) { @MJI public void $init____V(MJIEnv env, int socketRef) { try { - // Try to set fields normally + // Normal initialization env.setBooleanField(socketRef, "bound", false); env.setBooleanField(socketRef, "connected", false); env.setBooleanField(socketRef, "closed", false); env.setIntField(socketRef, "timeout", 0); + synchronized (JPF_java_net_Socket.class) { env.setIntField(socketRef, "hash", hashCounter++); } + // Ensure lock is never null int lock = env.newObject("java.lang.Object"); - env.setReferenceField(socketRef, "lock", lock); + if (lock != MJIEnv.NULL) { + env.setReferenceField(socketRef, "lock", lock); + } - } catch (Exception e) { + } catch (Exception e) { System.out.println("Socket initialization: using minimal mode with fallback hash storage"); synchronized (JPF_java_net_Socket.class) { - fallbackHashes.put(socketRef, hashCounter++); + int initialHash = hashCounter++; + fallbackHashes.put(socketRef, initialHash); + } + + // Always ensure critical references are non-null + try { + int fallbackLock = env.newObject("java.lang.Object"); + if (fallbackLock != MJIEnv.NULL) { + env.setReferenceField(socketRef, "lock", fallbackLock); + } + } catch (Exception lockEx) { + System.out.println("WARNING: Could not create lock object: " + lockEx.getMessage()); } } } + + + protected boolean waitForServerAccept(MJIEnv env, int socketRef, int port, String host) { // check if such serverSocket exists at all, if so client.connect needs to block int existingServer = connections.getServerSocketRef(port, host); @@ -439,7 +457,7 @@ private void updateSocketHash(MJIEnv env, int socketRef, int data, HashUpdateTyp int currentHash = env.getIntField(socketRef, "hash"); int newHash; - switch(type) { + switch (type) { case STATE_CHANGE: newHash = currentHash + 1; break; @@ -456,8 +474,7 @@ private void updateSocketHash(MJIEnv env, int socketRef, int data, HashUpdateTyp // Use fallback storage int currentHash = fallbackHashes.getOrDefault(socketRef, 0); int newHash; - - switch(type) { + switch (type) { case STATE_CHANGE: newHash = currentHash + 1; break; @@ -469,10 +486,21 @@ private void updateSocketHash(MJIEnv env, int socketRef, int data, HashUpdateTyp } fallbackHashes.put(socketRef, newHash); + + // **ADD THIS: Sync fallback back to real field** + try { + env.setIntField(socketRef, "hash", newHash); + System.out.println("DEBUG: Successfully synced hash " + newHash + " to field"); + } catch (Exception syncEx) { + // ignore if field doesn't exist + System.out.println("DEBUG: Failed to sync hash to field: " + syncEx.getMessage()); + } + System.out.println("Fallback hash updated: " + currentHash + " -> " + newHash + " (type: " + type + ", data: " + data + ")"); } } + @MJI public int getOutputStream____Ljava_io_OutputStream_2(MJIEnv env, int socketRef) { try { @@ -514,17 +542,20 @@ public static void updateSocketHashForDataWrite(MJIEnv env, int socketRef, int d int currentHash = fallbackHashes.getOrDefault(socketRef, 0); int newHash = currentHash ^ data; fallbackHashes.put(socketRef, newHash); - System.out.println("Fallback hash updated for data write: " + currentHash + " -> " + newHash + " (data: " + data + ")"); - // to sync back to field periodically + // **CRITICAL FIX: Sync fallback back to real field** try { env.setIntField(socketRef, "hash", newHash); - System.out.println("DEBUG: Successfully synced fallback hash to socket field"); + System.out.println("DEBUG: Successfully synced hash " + newHash + " to field"); } catch (Exception syncEx) { + System.out.println("DEBUG: Failed to sync hash to field: " + syncEx.getMessage()); } + + System.out.println("Fallback hash updated for data write: " + currentHash + " -> " + newHash + " (data: " + data + ")"); } } + // method to update socket connection status private void setConnected(MJIEnv env, int socketRef, boolean connected) { try { diff --git a/src/tests/net/nas/SocketTest.java b/src/tests/net/nas/SocketTest.java index c0bf0b8..b1e5327 100644 --- a/src/tests/net/nas/SocketTest.java +++ b/src/tests/net/nas/SocketTest.java @@ -1,13 +1,11 @@ package net.nas; +import java.io.File; import java.io.IOException; import java.io.InputStream; import java.io.OutputStream; import java.lang.reflect.Field; -import java.net.ServerSocket; -import java.net.Socket; -import java.net.SocketException; -import java.net.SocketTimeoutException; +import java.net.*; import nas.util.test.TestNasJPF; @@ -18,43 +16,43 @@ public class SocketTest extends TestNasJPF { String[] args = { "+search.multiple_errors = true", - "+vm.process_finalizers = true", - "+vm.nas.initiating_target = 0" - }; - + "+vm.process_finalizers = true", + "+vm.nas.initiating_target = 0" + }; + int port = 1024; final String HOST = "localhost"; - + @Test public void testEstablishingConnection() throws IOException { if (mpVerifyNoPropertyViolation(2, args)) { - + switch(getProcessId()) { - case 0: - ServerSocket serverSocket = new ServerSocket(port); - serverSocket.setSoTimeout(10); - Socket sock1 = null; - try { - sock1 = serverSocket.accept(); - } catch(SocketTimeoutException e) { - // gets here if no request is coming after a certain amount of time - assertNull(sock1); - } - break; - - case 1: - Socket sock2; - try { - sock2 = new Socket(HOST, port); - assertTrue(sock2.isConnected()); - } catch(IOException e) { - // gets here if there was no server accepting the connection request - } - break; + case 0: + ServerSocket serverSocket = new ServerSocket(port); + serverSocket.setSoTimeout(10); + Socket sock1 = null; + try { + sock1 = serverSocket.accept(); + } catch(SocketTimeoutException e) { + // gets here if no request is coming after a certain amount of time + assertNull(sock1); + } + break; + + case 1: + Socket sock2; + try { + sock2 = new Socket(HOST, port); + assertTrue(sock2.isConnected()); + } catch(IOException e) { + // gets here if there was no server accepting the connection request + } + break; } } } - + /** * Blocking accept with timeout throws SocketTimeoutException */ @@ -80,82 +78,82 @@ private int getHash(Socket sock) throws Exception { } } - + @Test public void testHash() throws Exception { if (mpVerifyNoPropertyViolation(2, args)) { - + switch(getProcessId()) { - case 0: - ServerSocket serverSocket = new ServerSocket(port); - Socket sock1 = serverSocket.accept(); - - int h1 = getHash(sock1); - assertTrue(h1!=0); - - OutputStream socketOutput = sock1.getOutputStream(); - - try { - socketOutput.write(10); - int h2 = getHash(sock1); - assertTrue(h1!=h2); - } catch(SocketException e) { - // attempting to write on a close connection - } - - break; - case 1: - Socket sock2; - try { - sock2 = new Socket(HOST, port); - - - } catch(IOException e) { - // gets here if there was no server accepting the connection request - System.out.println("never stablished!!"); - } - break; + case 0: + ServerSocket serverSocket = new ServerSocket(port); + Socket sock1 = serverSocket.accept(); + + int h1 = getHash(sock1); + assertTrue(h1!=0); + + OutputStream socketOutput = sock1.getOutputStream(); + + try { + socketOutput.write(10); + int h2 = getHash(sock1); + assertTrue(h1!=h2); + } catch(SocketException e) { + // attempting to write on a close connection + } + + break; + case 1: + Socket sock2; + try { + sock2 = new Socket(HOST, port); + + + } catch(IOException e) { + // gets here if there was no server accepting the connection request + System.out.println("never stablished!!"); + } + break; } } } - + @Test public void testTimedoutRead() throws IOException { if (mpVerifyNoPropertyViolation(2, args)) { - + switch(getProcessId()) { - case 0: - ServerSocket serverSocket = new ServerSocket(port); - Socket sock1 = serverSocket.accept(); - assertTrue(sock1.isConnected()); - break; - - case 1: - Socket sock2 = null; - try { - sock2 = new Socket(HOST, port); - sock2.setSoTimeout(10); - assertTrue(sock2.isConnected()); - } catch(IOException e) { - // gets here if there was no server accepting the connection request - return; - } - - try { - InputStream in = sock2.getInputStream(); - in.read(); - //assertTrue(isOtherEndClosed()); - } catch(SocketTimeoutException e) { - return; - } catch(SocketException e) { - return; - } - - break; + case 0: + ServerSocket serverSocket = new ServerSocket(port); + Socket sock1 = serverSocket.accept(); + assertTrue(sock1.isConnected()); + break; + + case 1: + Socket sock2 = null; + try { + sock2 = new Socket(HOST, port); + sock2.setSoTimeout(10); + assertTrue(sock2.isConnected()); + } catch(IOException e) { + // gets here if there was no server accepting the connection request + return; + } + + try { + InputStream in = sock2.getInputStream(); + in.read(); + //assertTrue(isOtherEndClosed()); + } catch(SocketTimeoutException e) { + return; + } catch(SocketException e) { + return; + } + + break; } } } - + static class FinalizeServer { @Override protected void finalize() throws Throwable { @@ -164,8 +162,8 @@ protected void finalize() throws Throwable { System.out.println("DONE!"); } } - - // This is testing finalizer threads. It should belong to jpf-core, but I add it here + + // This is testing finalizer threads. It should belong to jpf-core, but I add it here // since it needs support for ServerSocket.accept(). // here we make sure that MultiProcessVM does not ignore deadlocks in finalizers. @Test @@ -174,4 +172,5 @@ public void testDeadlockForBlockedFinalizer_MulitProcessVM() { new FinalizeServer(); } } -} + +} \ No newline at end of file