From c4735d464b44eadf1833ee4579622e63995056ae Mon Sep 17 00:00:00 2001 From: Mahmoud Khawaja Date: Sun, 16 Mar 2025 03:54:59 +0200 Subject: [PATCH 1/7] Added check to accept version 61, throw error for higher --- src/main/gov/nasa/jpf/jvm/ClassFile.java | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/main/gov/nasa/jpf/jvm/ClassFile.java b/src/main/gov/nasa/jpf/jvm/ClassFile.java index 9e331b84..68115f99 100644 --- a/src/main/gov/nasa/jpf/jvm/ClassFile.java +++ b/src/main/gov/nasa/jpf/jvm/ClassFile.java @@ -46,6 +46,7 @@ public class ClassFile extends BinaryClassSource { public static final int METHOD_HANDLE = 15; public static final int METHOD_TYPE = 16; public static final int INVOKE_DYNAMIC = 18; + private static final int MAX_SUPPORTED_VERSION = 61; public static final int REF_GETFIELD = 1; public static final int REF_GETSTATIC = 2; @@ -944,6 +945,10 @@ public void parse( ClassFileReader reader) throws ClassParseException { // we don't do much with the version numbers yet int minor = readU2(); int major = readU2(); + if (major > MAX_SUPPORTED_VERSION) { + // this will throw ClassParseException if the major version java 18 or higher + error("Unsupported class file version: " + major); + } // get the const pool int cpCount = readU2(); From ca050e77faa21473004ae410b0320056c0af00a2 Mon Sep 17 00:00:00 2001 From: Mahmoud Khawaja Date: Sun, 16 Mar 2025 04:31:09 +0200 Subject: [PATCH 2/7] removed the duplicated DEPRECATED_ATTR --- src/main/gov/nasa/jpf/jvm/ClassFile.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/gov/nasa/jpf/jvm/ClassFile.java b/src/main/gov/nasa/jpf/jvm/ClassFile.java index 68115f99..9078ddc4 100644 --- a/src/main/gov/nasa/jpf/jvm/ClassFile.java +++ b/src/main/gov/nasa/jpf/jvm/ClassFile.java @@ -219,7 +219,7 @@ public String getRequestedTypeName(){ public static final String BOOTSTRAP_METHOD_ATTR = "BootstrapMethods"; protected final static String[] stdClassAttrs = { - SOURCE_FILE_ATTR, DEPRECATED_ATTR, INNER_CLASSES_ATTR, DEPRECATED_ATTR, SIGNATURE_ATTR, + SOURCE_FILE_ATTR, DEPRECATED_ATTR, INNER_CLASSES_ATTR, SIGNATURE_ATTR, RUNTIME_INVISIBLE_ANNOTATIONS_ATTR, RUNTIME_VISIBLE_ANNOTATIONS_ATTR, RUNTIME_VISIBLE_TYPE_ANNOTATIONS_ATTR, ENCLOSING_METHOD_ATTR, BOOTSTRAP_METHOD_ATTR }; From 529d00fc413474820fee76a4f9edd3625ca2698e Mon Sep 17 00:00:00 2001 From: Mahmoud Khawaja Date: Wed, 19 Mar 2025 08:47:00 +0200 Subject: [PATCH 3/7] Add Java 17 class file version check and unit tests --- .../gov/nasa/jpf/jvm/FileVersionTest.java | 52 +++++++++++++++++++ .../jpf/jvm/resources/TestClassJava17.java | 4 ++ .../jpf/jvm/resources/TestClassJava21.java | 4 ++ 3 files changed, 60 insertions(+) create mode 100644 src/tests/gov/nasa/jpf/jvm/FileVersionTest.java create mode 100644 src/tests/gov/nasa/jpf/jvm/resources/TestClassJava17.java create mode 100644 src/tests/gov/nasa/jpf/jvm/resources/TestClassJava21.java diff --git a/src/tests/gov/nasa/jpf/jvm/FileVersionTest.java b/src/tests/gov/nasa/jpf/jvm/FileVersionTest.java new file mode 100644 index 00000000..5d31a1a7 --- /dev/null +++ b/src/tests/gov/nasa/jpf/jvm/FileVersionTest.java @@ -0,0 +1,52 @@ +package gov.nasa.jpf.jvm; + +import gov.nasa.jpf.util.test.TestJPF; +import gov.nasa.jpf.vm.ClassParseException; +import org.junit.Test; + +import java.io.*; + +public class FileVersionTest extends TestJPF { + + private static final String RESOURCES_PATH = "resources/"; + private static final String JAVA17_CLASS = RESOURCES_PATH + "TestClassJava17.class"; + private static final String JAVA21_CLASS = RESOURCES_PATH + "TestClassJava21.class"; + + // loading a .class file into a byte array + private byte[] loadClassFile(String resourceName) throws IOException { + try (InputStream is = getClass().getResourceAsStream(resourceName)) { + if (is == null) throw new IOException("Resource not found: " + resourceName); + + ByteArrayOutputStream bos = new ByteArrayOutputStream(); + // we choose here buffer size 1024 cause its enough to read most .class files in one or two iterations + // smaller buffer size like 256 will require more operations and larger buffers will waster memory + // i'm not sure which is suitable for this since the test classes we complied is empty but i think both could work + byte[] buffer = new byte[1024]; + int bytesRead; + while ((bytesRead = is.read(buffer)) != -1) { + bos.write(buffer, 0, bytesRead); + } + return bos.toByteArray(); + } + } + + @Test + public void testSupportedVersionJava17() throws IOException { + byte[] classData = loadClassFile(JAVA17_CLASS); + + ClassFile classFile = new ClassFile(classData); + + assertTrue("Java 17 class file should be parsed successfully", true); + } + + /* + @Test(expected = ClassParseException.class) + public void testUnsupportedVersionJava21() throws IOException { + byte[] classData = loadClassFile(JAVA21_CLASS); + + ClassFile classFile = new ClassFile(classData); + // this should throw exception if we used any version other than java 17 + // which mean the test passes + } + */ +} \ No newline at end of file diff --git a/src/tests/gov/nasa/jpf/jvm/resources/TestClassJava17.java b/src/tests/gov/nasa/jpf/jvm/resources/TestClassJava17.java new file mode 100644 index 00000000..9bae4935 --- /dev/null +++ b/src/tests/gov/nasa/jpf/jvm/resources/TestClassJava17.java @@ -0,0 +1,4 @@ +package gov.nasa.jpf.jvm.resources; + +public class TestClassJava17 { +} diff --git a/src/tests/gov/nasa/jpf/jvm/resources/TestClassJava21.java b/src/tests/gov/nasa/jpf/jvm/resources/TestClassJava21.java new file mode 100644 index 00000000..4ec92fde --- /dev/null +++ b/src/tests/gov/nasa/jpf/jvm/resources/TestClassJava21.java @@ -0,0 +1,4 @@ +package gov.nasa.jpf.jvm.resources; + +public class TestClassJava21 { +} From f7a361b25c3e0f3d2d24dc3ed8d73f1ee1ea3fe9 Mon Sep 17 00:00:00 2001 From: Mahmoud Khawaja Date: Wed, 19 Mar 2025 09:03:52 +0200 Subject: [PATCH 4/7] Add .class files for class version check --- .../nasa/jpf/jvm/resources/TestClassJava17.class | Bin 0 -> 221 bytes .../nasa/jpf/jvm/resources/TestClassJava21.class | Bin 0 -> 221 bytes 2 files changed, 0 insertions(+), 0 deletions(-) create mode 100644 src/tests/gov/nasa/jpf/jvm/resources/TestClassJava17.class create mode 100644 src/tests/gov/nasa/jpf/jvm/resources/TestClassJava21.class diff --git a/src/tests/gov/nasa/jpf/jvm/resources/TestClassJava17.class b/src/tests/gov/nasa/jpf/jvm/resources/TestClassJava17.class new file mode 100644 index 0000000000000000000000000000000000000000..c30a4af6d25e84fcd6d00a036bc6d357e4bf2a44 GIT binary patch literal 221 zcmZ8by9&ZU5S%kFjS($u1?|+r!^%c&0u~}#80;_c3<-HiUjJn!Soi^cl(kVLoo{1I|1F8iLI>R6omEe&`e1396=@kt6I!J#8=8nt@I}&-mC;M{6pxWtGGV~8YB9CS4%FGdNL?82VpjyzNGYmpe2_A{W=O;ImUcsQRgCr<649awNG0s^M%pBoH^fAwAnR#*-)MWVQTh!^8z@Sp~ dFj}fb*daD*IH1j+V2?&N32PZp2)lG!uzpq0EqMR{ literal 0 HcmV?d00001 From 1ddfeac13f818df0a387b5e85cca7bdd4ffefdcb Mon Sep 17 00:00:00 2001 From: Mahmoud Khawaja Date: Thu, 20 Mar 2025 05:46:45 +0200 Subject: [PATCH 5/7] updated the tests --- .../gov/nasa/jpf/jvm/FileVersionTest.java | 25 +++++++++++------- .../jpf/jvm/resources/TestClassJava17.class | Bin 221 -> 231 bytes .../jpf/jvm/resources/TestClassJava21.class | Bin 221 -> 231 bytes 3 files changed, 15 insertions(+), 10 deletions(-) diff --git a/src/tests/gov/nasa/jpf/jvm/FileVersionTest.java b/src/tests/gov/nasa/jpf/jvm/FileVersionTest.java index 5d31a1a7..a67b6dcd 100644 --- a/src/tests/gov/nasa/jpf/jvm/FileVersionTest.java +++ b/src/tests/gov/nasa/jpf/jvm/FileVersionTest.java @@ -30,23 +30,28 @@ private byte[] loadClassFile(String resourceName) throws IOException { } } + private int getMajorVersion(byte[] classData) { + int major = ((classData[6] & 0xff) << 8) | (classData[7] & 0xff); + return major; + } + @Test - public void testSupportedVersionJava17() throws IOException { + public void testSupportedVersionJava17() throws IOException, ClassParseException { byte[] classData = loadClassFile(JAVA17_CLASS); - + System.out.println(getMajorVersion(classData)); ClassFile classFile = new ClassFile(classData); - - assertTrue("Java 17 class file should be parsed successfully", true); + ClassFileReader reader = new ClassFileReaderAdapter(); + // this should pass with no exceptions + classFile.parse(reader); } - /* @Test(expected = ClassParseException.class) - public void testUnsupportedVersionJava21() throws IOException { + public void testUnsupportedVersionJava21() throws IOException, ClassParseException { byte[] classData = loadClassFile(JAVA21_CLASS); - + System.out.println(getMajorVersion(classData)); ClassFile classFile = new ClassFile(classData); - // this should throw exception if we used any version other than java 17 - // which mean the test passes + ClassFileReader reader = new ClassFileReaderAdapter(); + // this should throw ClassParseException + classFile.parse(reader); } - */ } \ No newline at end of file diff --git a/src/tests/gov/nasa/jpf/jvm/resources/TestClassJava17.class b/src/tests/gov/nasa/jpf/jvm/resources/TestClassJava17.class index c30a4af6d25e84fcd6d00a036bc6d357e4bf2a44..cb37025e5e843cf36a53c1999ec5f3b31c0a555c 100644 GIT binary patch delta 37 scmcc1_?&TqowQbZewlt=VsWB=RzaG6R#~ooQEG91X;E@&@kIYV00?>xTL1t6 delta 27 icmaFPc$aa4ouEQ`ewlt=VsWB=RzaG6R$1=E$UXp!#|lRP diff --git a/src/tests/gov/nasa/jpf/jvm/resources/TestClassJava21.class b/src/tests/gov/nasa/jpf/jvm/resources/TestClassJava21.class index 19e2ec0bdaa63493461c610a23ed5319de92d1a1..d08fca59a5576a7a735e2c4a6bc70baf28ce01df 100644 GIT binary patch delta 37 scmcc1_?&TqowQbZewlt=VsWB=RzaG6R#~ooQEG91X;E@&@kIYV00?>xTL1t6 delta 27 icmaFPc$aa4ouEQ`ewlt=VsWB=RzaG6R$1=E$UXp!#|lRP From 77728d03d796cf446ee72e344b8eb8e41076f088 Mon Sep 17 00:00:00 2001 From: Mahmoud Khawaja Date: Fri, 21 Mar 2025 16:01:44 +0200 Subject: [PATCH 6/7] Add resource directory for .class files and update build.gradle to include them in the test classpath --- build.gradle | 8 ++++++++ src/tests/gov/nasa/jpf/jvm/FileVersionTest.java | 11 ++--------- .../nasa/jpf/jvm/resources/TestClassJava17.class | Bin 231 -> 0 bytes .../nasa/jpf/jvm/resources/TestClassJava17.java | 4 ---- .../nasa/jpf/jvm/resources/TestClassJava21.class | Bin 231 -> 0 bytes .../nasa/jpf/jvm/resources/TestClassJava21.java | 4 ---- 6 files changed, 10 insertions(+), 17 deletions(-) delete mode 100644 src/tests/gov/nasa/jpf/jvm/resources/TestClassJava17.class delete mode 100644 src/tests/gov/nasa/jpf/jvm/resources/TestClassJava17.java delete mode 100644 src/tests/gov/nasa/jpf/jvm/resources/TestClassJava21.class delete mode 100644 src/tests/gov/nasa/jpf/jvm/resources/TestClassJava21.java diff --git a/build.gradle b/build.gradle index ad5a7a43..a4d7246d 100644 --- a/build.gradle +++ b/build.gradle @@ -366,3 +366,11 @@ tasks.register('runPolDet', Exec) { } defaultTasks "buildJars" + +sourceSets { + test { + resources { + srcDirs = ['src/tests/resources'] + } + } +} \ No newline at end of file diff --git a/src/tests/gov/nasa/jpf/jvm/FileVersionTest.java b/src/tests/gov/nasa/jpf/jvm/FileVersionTest.java index a67b6dcd..1b7748f4 100644 --- a/src/tests/gov/nasa/jpf/jvm/FileVersionTest.java +++ b/src/tests/gov/nasa/jpf/jvm/FileVersionTest.java @@ -8,9 +8,8 @@ public class FileVersionTest extends TestJPF { - private static final String RESOURCES_PATH = "resources/"; - private static final String JAVA17_CLASS = RESOURCES_PATH + "TestClassJava17.class"; - private static final String JAVA21_CLASS = RESOURCES_PATH + "TestClassJava21.class"; + private static final String JAVA17_CLASS = "/TestClassJava17.class"; + private static final String JAVA21_CLASS = "/TestClassJava21.class"; // loading a .class file into a byte array private byte[] loadClassFile(String resourceName) throws IOException { @@ -30,15 +29,10 @@ private byte[] loadClassFile(String resourceName) throws IOException { } } - private int getMajorVersion(byte[] classData) { - int major = ((classData[6] & 0xff) << 8) | (classData[7] & 0xff); - return major; - } @Test public void testSupportedVersionJava17() throws IOException, ClassParseException { byte[] classData = loadClassFile(JAVA17_CLASS); - System.out.println(getMajorVersion(classData)); ClassFile classFile = new ClassFile(classData); ClassFileReader reader = new ClassFileReaderAdapter(); // this should pass with no exceptions @@ -48,7 +42,6 @@ public void testSupportedVersionJava17() throws IOException, ClassParseException @Test(expected = ClassParseException.class) public void testUnsupportedVersionJava21() throws IOException, ClassParseException { byte[] classData = loadClassFile(JAVA21_CLASS); - System.out.println(getMajorVersion(classData)); ClassFile classFile = new ClassFile(classData); ClassFileReader reader = new ClassFileReaderAdapter(); // this should throw ClassParseException diff --git a/src/tests/gov/nasa/jpf/jvm/resources/TestClassJava17.class b/src/tests/gov/nasa/jpf/jvm/resources/TestClassJava17.class deleted file mode 100644 index cb37025e5e843cf36a53c1999ec5f3b31c0a555c..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 231 zcmZ8b!4APd6r9ykig0jsaH9tsCl_2K4k8>h?%P^TH`PkF`d>~G2Or?0#M>Udm(0t& z$xP<+eZ2uJ(RERS<-qQsjs`M_nu&nN_Gj23|NG1x;1ouY?CpQ diff --git a/src/tests/gov/nasa/jpf/jvm/resources/TestClassJava17.java b/src/tests/gov/nasa/jpf/jvm/resources/TestClassJava17.java deleted file mode 100644 index 9bae4935..00000000 --- a/src/tests/gov/nasa/jpf/jvm/resources/TestClassJava17.java +++ /dev/null @@ -1,4 +0,0 @@ -package gov.nasa.jpf.jvm.resources; - -public class TestClassJava17 { -} diff --git a/src/tests/gov/nasa/jpf/jvm/resources/TestClassJava21.class b/src/tests/gov/nasa/jpf/jvm/resources/TestClassJava21.class deleted file mode 100644 index d08fca59a5576a7a735e2c4a6bc70baf28ce01df..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 231 zcmZ8bF$%&!5S%m7XjHVYwXo9^9$Jeaf`y0{2K!4qLynk8F6LiWf`t$8QQ}@ocVU*< zVTSp9UvB^_bY0Y7Ij}pZqruQuq7*z4X~YkKl3~HnSj1^uEE%lv Date: Fri, 21 Mar 2025 16:20:17 +0200 Subject: [PATCH 7/7] added .class files --- src/tests/resources/TestClassJava17.class | Bin 0 -> 221 bytes src/tests/resources/TestClassJava21.class | Bin 0 -> 221 bytes 2 files changed, 0 insertions(+), 0 deletions(-) create mode 100644 src/tests/resources/TestClassJava17.class create mode 100644 src/tests/resources/TestClassJava21.class diff --git a/src/tests/resources/TestClassJava17.class b/src/tests/resources/TestClassJava17.class new file mode 100644 index 0000000000000000000000000000000000000000..c30a4af6d25e84fcd6d00a036bc6d357e4bf2a44 GIT binary patch literal 221 zcmZ8by9&ZU5S%kFjS($u1?|+r!^%c&0u~}#80;_c3<-HiUjJn!Soi^cl(kVLoo{1I|1F8iLI>R6omEe&`e1396=@kt6I!J#8=8nt@I}&-mC;M{6pxWtGGV~8YB9CS4%FGdNL?82VpjyzNGYmpe2_A{W=O;ImUcsQRgCr<649awNG0s^M%pBoH^fAwAnR#*-)MWVQTh!^8z@Sp~ dFj}fb*daD*IH1j+V2?&N32PZp2)lG!uzpq0EqMR{ literal 0 HcmV?d00001