Java 11 work

.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:

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'
         }
     }
-}
+}

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

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();
   }
-}
+}

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);
+  }
 }

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");