From: Cyrille Artho <artho@kth.se>
Date: Fri, 23 Nov 2018 13:52:15 +0000 (+0100)
Subject: Fixed out-of-bounds cases for substring.
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=b592174fd5484cb641f1039a4eccc8af6e8c525f

Fixed out-of-bounds cases for substring.
---

diff --git a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_String.java b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_String.java
index eae561c..556bb7c 100644
--- a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_String.java
+++ b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_String.java
@@ -32,7 +32,8 @@ import java.util.Locale;
  * MJI NativePeer class for java.lang.String library abstraction
  */
 public class JPF_java_lang_String extends NativePeer {
-
+  final static String sioobe = "java.lang.StringIndexOutOfBoundsException";
+  final static String sioor = "String index out of range: ";
   
   @MJI
   public int init___3CII__Ljava_lang_String_2 (MJIEnv env, int objRef, int valueRef, int offset, int count) {
@@ -145,8 +146,7 @@ public class JPF_java_lang_String extends NativePeer {
     if (index >= 0 && index < data.length) {
       return data[index];
     }
-    env.throwException("java.lang.StringIndexOutOfBoundsException",
-		       "String index out of range: " + index);
+    env.throwException(sioobe, sioor + index);
     return '\0';
   }
 
@@ -379,14 +379,24 @@ public class JPF_java_lang_String extends NativePeer {
   @MJI
   public int substring__I__Ljava_lang_String_2 (MJIEnv env, int objRef, int beginIndex) {
     String obj = env.getStringObject(objRef);
-    String result = obj.substring(beginIndex);
-    return env.newString(result);
-
+    return substring__II__Ljava_lang_String_2(env, objRef, beginIndex, obj.length());
   }
 
   @MJI
   public int substring__II__Ljava_lang_String_2 (MJIEnv env, int objRef, int beginIndex, int endIndex) {
+    if (beginIndex > endIndex) {
+      env.throwException(sioobe, sioor + (endIndex - beginIndex));
+      return 0;
+    }
+    if (beginIndex < 0) {
+      env.throwException(sioobe, sioor + beginIndex);
+      return 0;
+    }
     String obj = env.getStringObject(objRef);
+    if (endIndex > obj.length()) {
+      env.throwException(sioobe, sioor + endIndex);
+      return 0;
+    }
     String result = obj.substring(beginIndex, endIndex);
     return env.newString(result);
 
diff --git a/src/tests/gov/nasa/jpf/test/java/lang/StringTest.java b/src/tests/gov/nasa/jpf/test/java/lang/StringTest.java
index 0cd9394..7d6b709 100644
--- a/src/tests/gov/nasa/jpf/test/java/lang/StringTest.java
+++ b/src/tests/gov/nasa/jpf/test/java/lang/StringTest.java
@@ -187,6 +187,54 @@ public class StringTest extends TestJPF {
 		}
 	}
 
+	@Test
+	public void testSubstringOutOfBounds0() {
+		boolean passed = false;
+		if (verifyNoPropertyViolation()){
+		    try {
+		      " ".substring(0, 1);
+		      passed = true;
+		      " ".substring(0, 2);
+		    } catch (StringIndexOutOfBoundsException e) {
+		      assert(passed);
+		      return;
+		    }
+		    assert false;
+		}
+	}
+
+	@Test
+	public void testSubstringOutOfBounds1() {
+		boolean passed = false;
+		if (verifyNoPropertyViolation()){
+		    try {
+		      " ".substring(0, 1);
+		      passed = true;
+		      " ".substring(1, 0);
+		    } catch (StringIndexOutOfBoundsException e) {
+		      assert(passed);
+		      return;
+		    }
+		    assert false;
+		}
+	}
+
+	@Test
+	public void testSubstringOutOfBoundsNeg() {
+		boolean passed = false;
+		if (verifyNoPropertyViolation()){
+		    try {
+		      assert("".substring(0).equals(""));
+		      passed = true;
+		      " ".substring(-1);
+		    } catch (StringIndexOutOfBoundsException e) {
+		      assert(passed);
+		      return;
+		    }
+		    assert false;
+		}
+	}
+
 	@Test
   @SuppressWarnings("deprecation")
   public void testConstructors(){