added the static method check in INVOKESTATIC.java

src/main/gov/nasa/jpf/jvm/bytecode/INVOKESTATIC.java

@@ -1,5 +1,5 @@
 /*
- * Copyright (C) 2014, United States Government, as represented by the
+ * Copyright (C) 2024, United States Government, as represented by the
  * Administrator of the National Aeronautics and Space Administration.
  * All rights reserved.
  *
@@ -17,7 +17,6 @@
  */
 package gov.nasa.jpf.jvm.bytecode;
 
-
 import gov.nasa.jpf.vm.ClassInfo;
 import gov.nasa.jpf.vm.ClassLoaderInfo;
 import gov.nasa.jpf.vm.ElementInfo;
@@ -28,7 +27,6 @@
 import gov.nasa.jpf.vm.ThreadInfo;
 import gov.nasa.jpf.vm.Types;
 
-
 /**
  * Invoke a class (static) method
  * ..., [arg1, [arg2 ...]]  => ...
@@ -57,14 +55,13 @@ public String toPostExecString(){
     StringBuilder sb = new StringBuilder();
     sb.append(getMnemonic());
     sb.append(' ');
-    sb.append( invokedMethod.getFullName());
+    sb.append(invokedMethod.getFullName());
 
     if (invokedMethod.isMJI()){
       sb.append(" [native]");
     }
 
     return sb.toString();
-
   }
 
   public StaticElementInfo getStaticElementInfo (){
@@ -88,28 +85,37 @@ public Instruction execute (ThreadInfo ti) {
     if (callee == null) {
       return ti.createAndThrowException("java.lang.NoSuchMethodException", cname + '.' + mname);
     }
+
+    // Added the static method check here
+    if (!callee.isStatic()) {
+        //System.out.println("hererrrererererer");
+        // If the method is not static, throw an exception
+        return ti.createAndThrowException("java.lang.IncompatibleClassChangeError",
+                "Expected static method " + callee.getFullName());
+    }
+
 
-    // this can be actually different than (can be a base)
+    // This can be actually different than (can be a base)
     ClassInfo ciCallee = callee.getClassInfo();
 
     if (ciCallee.initializeClass(ti)) {
-      // do class initialization before continuing
-      // note - this returns the next insn in the topmost clinit that just got pushed
+      // Do class initialization before continuing
+      // Note - this returns the next insn in the topmost clinit that just got pushed
       return ti.getPC();
     }
 
     if (callee.isSynchronized()) {
       ElementInfo ei = ciCallee.getClassObject();
-      ei = ti.getScheduler().updateObjectSharedness(ti, ei, null); // locks most likely belong to shared objects
+      ei = ti.getScheduler().updateObjectSharedness(ti, ei, null); // Locks most likely belong to shared objects
 
       if (reschedulesLockAcquisition(ti, ei)){
         return this;
       }
     }
 
-    setupCallee( ti, callee); // this creates, initializes and pushes the callee StackFrame
+    setupCallee(ti, callee); // This creates, initializes, and pushes the callee StackFrame
 
-    return ti.getPC(); // we can't just return the first callee insn if a listener throws an exception
+    return ti.getPC(); // We can't just return the first callee insn if a listener throws an exception
   }
 
   @Override
@@ -119,7 +125,7 @@ public MethodInfo getInvokedMethod(){
     } else {
       // Hmm, this would be pre-exec, but if the current thread is not the one executing the insn 
       // this might result in false sharedness of the class object
-      return getInvokedMethod( ThreadInfo.getCurrentThread());
+      return getInvokedMethod(ThreadInfo.getCurrentThread());
     }
   }
 
@@ -130,10 +136,10 @@ public MethodInfo getInvokedMethod (ThreadInfo ti){
       if (clsInfo != null){
         MethodInfo callee = clsInfo.getMethod(mname, true);
         if (callee != null){
-          ClassInfo ciCallee = callee.getClassInfo(); // might be a superclass of ci, i.e. not what is referenced in the insn
+          ClassInfo ciCallee = callee.getClassInfo(); // Might be a superclass of ci, i.e. not what is referenced in the insn
 
           if (!ciCallee.isRegistered()){
-            // if it wasn't registered yet, classLoaded listeners didn't have a chance yet to modify it..
+            // If it wasn't registered yet, classLoaded listeners didn't have a chance yet to modify it..
             ciCallee.registerClass(ti);
             // .. and might replace/remove MethodInfos
             callee = clsInfo.getMethod(mname, true);
@@ -145,7 +151,7 @@ public MethodInfo getInvokedMethod (ThreadInfo ti){
     return invokedMethod;
   }
 
-  // can be different thatn the ci - method can be in a superclass
+  // Can be different than the ci - method can be in a superclass
   public ClassInfo getInvokedClassInfo(){
     return getInvokedMethod().getClassInfo();
   }
@@ -163,10 +169,9 @@ public int getArgSize () {
     return argSize;
   }
 
-
   @Override
   public String toString() {
-    // methodInfo not set outside real call context (requires target object)
+    // MethodInfo not set outside real call context (requires target object)
     return "invokestatic " + cname + '.' + mname;
   }
 
@@ -177,7 +182,7 @@ public Object getFieldValue (String id, ThreadInfo ti) {
 
   @Override
   public void accept(JVMInstructionVisitor insVisitor) {
-	  insVisitor.visit(this);
+    insVisitor.visit(this);
   }
 
   @Override
@@ -187,7 +192,7 @@ public Instruction typeSafeClone(MethodInfo mi) {
     try {
       clone = (INVOKESTATIC) super.clone();
 
-      // reset the method that this insn belongs to
+      // Reset the method that this insn belongs to
       clone.mi = mi;
 
       clone.invokedMethod = null;
@@ -200,4 +205,3 @@ public Instruction typeSafeClone(MethodInfo mi) {
     return clone;
   }
 }
-

src/tests/gov/nasa/jpf/jvm/InvokeStaticTest.java

@@ -0,0 +1,47 @@
+package gov.nasa.jpf.jvm;
+
+import org.junit.Test;
+import gov.nasa.jpf.util.test.TestJPF;
+
+public class InvokeStaticTest extends TestJPF {
+
+    static class D {
+        // Initially static method
+        public static String m(String s) {
+            return s;
+        }
+    }
+
+    static class C {
+        public static void main(String[] args) {
+            int i = 123;
+            D.m("foobar");  // This is a valid static method call
+            System.out.println(i);
+        }
+    }
+
+    @Test
+    public void testInvokeStaticSuccess() {
+        // Test should pass if static method invocation works fine
+        if (verifyNoPropertyViolation()) {
+            C.main(new String[0]);
+        }
+    }
+
+    @Test
+    public void testInvokeStaticFailure() {
+        if (verifyUnhandledException("java.lang.IncompatibleClassChangeError")) {
+            // Simulate making D.m() non-static to trigger the error
+            DNonStatic d = new DNonStatic();
+            d.m("foobar");  // This should cause the failure because the method is now non-static
+        }
+    }
+
+    // Simulate a non-static version of class D for this test
+    static class DNonStatic {
+        // Non-static method, which should fail when invoked via INVOKESTATIC
+        public String m(String s) {
+            return s;
+        }
+    }
+}