Support to throw StringIndexOutOfBoundsException in methods subString and charAt GSoC 2025 by saifk16 · Pull Request #133 · SymbolicPathFinder/jpf-symbc

saifk16 · 2025-08-29T17:02:10Z

This PR supports subString and charAt to properly handle StringIndexOutOfBoundsException

Configuration Updates (jpf-sv-comp)

Added proper handling for search.multiple_errors configuration based on RUNTIME_EXCEPTION_MODE
Enhanced error detection logic to handle ClassNotFoundException scenarios
Improved result classification for SAFE/UNSAFE/UNKNOWN states

charAt
Path 0: Index < 0 → StringIndexOutOfBoundsException
Path 1: Index >= string.length() → StringIndexOutOfBoundsException
Path 2: Valid execution path
Added support for StringBuilder.charAt() operations

substring
Single parameter: 3 paths (index < 0, index > length, valid execution path)
Two parameters: 6 paths (beginIndex < 0, endIndex < 0, endIndex > length, beginIndex > length, endIndex < beginIndex, valid execution path)

Test cases were added for both of the methods in the folder rte and the script was also refined.

saifk16 · 2025-08-29T17:14:19Z

@sohah ma'am this pr is created for the substring() and charAt() support and is ready for a review.
Thanks.

sohah

HI @saifk16 , I have a few comments on this PR. Can you please fix and let me know. Thanks!

sohah · 2025-09-02T08:12:01Z

jpf-sv-comp

  grep "java.lang.*Exception" $LOG > /dev/null
  JAVA_EXCEPTION=$?

+  grep "java.lang.ClassNotFoundException" $LOG > /dev/null


I could not comment on lines 100-106, so I am writting a comment about them here. The conditions within this if-statement could be optimized. I think you should check for assertion, and print unsafe. if that does not match check for no errors and print safe. If we have a java-exception or anything else, this should be unknown. I mean how can we print safe when SPF just raised an exception in the reach safety mode? That doesn't seem right. Can you give me an example of when you want to print a safe when SPF had an exception in the reachsafety mode?

That was a mistake, thank you for noticing actually I was testing that if condition with the exception things, It will be corrected in the recent commit. Thanks

This is done.

sohah · 2025-09-02T08:16:02Z

jpf-sv-comp

+  elif [ $CLASS_NOT_FOUND -eq 0 ]; then
+    echo "UNKNOWN"


This is problemetic, how can we have ClassNotFoundException, that just means we are unable to access the class during rutime, so this means there is something wrong in the compilation/build process that we then see this error. This check should not be part of the script, and if we are running into these issues then we should resolve them, because that must be a bug that is causing this to happen.

Actually when we were checking this was happening two times in the verification tasks:

StaticCharMethods05 because of this Scanner scanner = new Scanner(Verifier.nondetString());

and in radians because of double rad = java.lang.Math.toRadians(deg);

Both of them are not present in the respective classes in the jpf-symbc so because of that we get these errors

gov.nasa.jpf.vm.NoUncaughtExceptionsProperty java.lang.ClassNotFoundException: class not found: java.lang.NoSuchMethodException!! at Main.main(Main.java:34) ====================================================== snapshot #1 thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: at Main.main(Main.java:34) ====================================================== results error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.ClassNotFoundException: class not found:..."

@saifk16 This is another bug that we should not have. Please open an issue with it, but the script should not have this change.

Hello ma'am what should I print then, for these two varification task, SAFE, UNSAFE, UN KNOWN?

@saifk16 , have you addressed this yet? I think it should be unknown

no ma'am this is not addressed till now I was waiting for your reply yes ma'am according to the script it was reported to be unknown earlier but was removed later on, I think I need to specially check for this and report unknown

sohah · 2025-09-02T08:20:46Z

jpf-symbc/src/examples/rte/rte.jpf

+runtime.exception=true
+symbolic.lazy=on
+symbolic.jrarrays=true
+veritestingMode = 5


can you please remove this option (veritestingMode), it isn't SPF related.

okay ma'am.

sohah · 2025-09-02T08:23:13Z

jpf-symbc/src/examples/rte/rte.jpf

+recursiveDepth= 200
+singlePathOptimization=true
+listener = .symbc.SymbolicListener
+symbolic.debug=true


Can you also add search.multiple_errors=true and turn off nullPointer.exception?

okay ma'am.

sohah · 2025-09-02T08:33:42Z

jpf-symbc/src/main/gov/nasa/jpf/symbc/bytecode/SymbolicStringHandler.java

+        } else
+            return false;


i think here you are returning a special variable "bresult" to indicate if support was handled or not. So I would use the same variable name here in this return statement.

Actually the code that was present earlier for charAt was using bresult and the method handleChatAt is set to return a boolean can it be void or should it remain boolean type return ?

This was also done

sohah · 2025-09-02T08:53:34Z

jpf-symbc/src/main/gov/nasa/jpf/symbc/bytecode/SymbolicStringHandler.java

+
+            assert pc != null;
+
+			if(currentChocie == 2) {


why the choices are not handled in order. I would expect to see choice 0, 1 then 2. Please fix that

Sorry for that, will be fixed.

sohah · 2025-09-02T08:59:25Z

jpf-symbc/src/main/gov/nasa/jpf/symbc/bytecode/SymbolicStringHandler.java

+            } else if (currentChocie == 4) {
+                if (!rte_flag) {
+                    th.getVM().getSystemState().setIgnored(true);


again why the order of the choices are flipped.
Also can you add comments, short ones to describe what each choice do?

will be fixed, thanks for noticing.

comments were added

sohah · 2025-09-02T09:01:27Z

jpf-symbc/src/main/gov/nasa/jpf/symbc/bytecode/SymbolicStringHandler.java

+                    if(sym_v2 != null) {
+                        if(sym_v1 != null) {
+                            pc._addDet(Comparator.GT, sym_v2, sym_v1);
+                        } else {
+                            int val = s1;
+                            pc._addDet(Comparator.GT, sym_v2, new IntegerConstant(val));
+                        }
+                    } else {
+                        int val2 = s2;
+                        pc._addDet(Comparator.GT, new IntegerConstant(val2), sym_v1);
+                    }
+                    if (!pc.simplify()) {
+                        th.getVM().getSystemState().setIgnored(true);
+                    } else {
+                        th.createAndThrowException("java.lang.StringIndexOutOfBoundsException");


you need to think about some code restructuring because that is a lot of code to have in one method.
Also, I am not sure why you need 6 choices (from 0-5)? This must be wrong.

The substring(beginIndex, endIndex) method needs 6 distinct choices to handle all possible StringIndexOutOfBoundsException scenarios:

Exception Scenarios

Choice 0: beginIndex < 0

When the starting index is negative

Example: "hello".substring(-1, 3) → throws exception

Choice 1: endIndex < 0

When the ending index is negative

Example: "hello".substring(1, -2) → throws exception

Choice 2: beginIndex > string.length()

When starting index exceeds string length

Example: "hello".substring(10, 15) → throws exception

Choice 3: endIndex > string.length()

When ending index exceeds string length

Example: "hello".substring(1, 10) → throws exception

Choice 4: beginIndex > endIndex

When start index is greater than end index

Example: "hello".substring(3, 1) → throws exception

Choice 5: Default Behaviour

Preserves existing code functionality that was present before this exception handling support was added

sohah · 2025-09-02T09:02:12Z

jpf-symbc/src/main/gov/nasa/jpf/symbc/bytecode/SymbolicStringHandler.java

-			return handleSubString2(invInst, th);
+            ChoiceGenerator<?> cg;
+            if (!th.isFirstStepInsn()) { // first time around
+                cg = new PCChoiceGenerator(5);


here you create a 5 choice but the implementation of the method is using 6 choices. Please check.

I will fix that, thank you for looking into this, it should be 6 because of (0-5)

saifk16 · 2025-09-03T12:10:38Z

Hello @sohah ma'am this pr is again available for a review

sohah

@saifk16 , I left you some comments on older review comments, and added an extra one. Can you please fix and let me know when you are done. Thanks!

sohah · 2025-09-03T12:54:48Z

jpf-symbc/src/main/gov/nasa/jpf/symbc/bytecode/SymbolicStringHandler.java

 			//System.out.println("[SymbolicStringHandler] " + sf.toString());
 			sf.setOperandAttr(result);
-            } else if (currentChocie == 4) {
+            } else if (currentChocie == 4) { // beginIndex > endIndex


You do not need this choice, it is already covered with the normal case and will just be unsat.

saifk16 · 2025-09-05T18:25:14Z

Hello @sohah ma'am pr is again available for a review.

sohah

Saif, a few comments are attached in this review. In general I think this code can be optimized there are a lot of duplication, can we write it in a better way?

sohah · 2025-09-09T04:53:42Z

jpf-symbc/src/main/gov/nasa/jpf/symbc/bytecode/SymbolicStringHandler.java

+            int s1 = sf.pop();
+            int s2 = sf.pop();


why do we see stack operation in the middle of the code for preparing the PC!? this should either be right at the top, or right at the end. I wouldj ust place them right after the else.

done moved next to else

sohah · 2025-09-09T04:54:05Z

jpf-symbc/src/main/gov/nasa/jpf/symbc/bytecode/SymbolicStringHandler.java

+
+            assert pc != null;
+
+			if (currentChocie == 0) {


why aren't you making comments to explain what each choice does?

sohah · 2025-09-09T04:54:31Z

jpf-symbc/src/main/gov/nasa/jpf/symbc/bytecode/SymbolicStringHandler.java

+            int s1 = sf.pop();
+            int s2 = sf.pop();


this again is happening in the middle of the pc code

sohah · 2025-09-09T04:54:44Z

jpf-symbc/src/main/gov/nasa/jpf/symbc/bytecode/SymbolicStringHandler.java

+
+            int s1 = sf.pop();
+            int s2 = sf.pop();
+            int s3 = sf.pop();


sohah · 2025-09-09T04:58:26Z

jpf-symbc/src/main/gov/nasa/jpf/symbc/bytecode/SymbolicStringHandler.java

+                if(!rte_flag) {
+                    th.getVM().getSystemState().setIgnored(true);
+                } else {
+                    if(sym_v1 != null) {
+                        pc._addDet(Comparator.LT,  sym_v1, new IntegerConstant(0));
+                    } else {
+                        int val = s1;
+                        pc._addDet(Comparator.LT, new IntegerConstant(val), new IntegerConstant(0));
+                    }
+                    if(!pc.simplify()) {
+                        th.getVM().getSystemState().setIgnored(true);
+                    } else {
+                        th.createAndThrowException("java.lang.StringIndexOutOfBoundsException");


why the formatting of your code is off!? I know we need to automate this, but at least the new parts should be written nicely

sohah · 2025-09-09T05:00:31Z

jpf-symbc/src/main/gov/nasa/jpf/symbc/bytecode/SymbolicStringHandler.java

+                        pc._addDet(Comparator.LT, new IntegerConstant(val), new IntegerConstant(0));
+                    }


why do you need to invoke the solver for a concrete constraint? can't you just check this in the code?

this is done

sohah · 2025-09-09T05:02:30Z

jpf-symbc/src/main/gov/nasa/jpf/symbc/bytecode/SymbolicStringHandler.java

+                            pc._addDet(Comparator.GE,  new IntegerConstant(val), sym_v2._length());
+                        }


this is another concrete constraint

actually symv2._length() is an integer expression here and it is symbolic val is concrete

sohah · 2025-09-09T05:07:10Z

jpf-symbc/src/main/gov/nasa/jpf/symbc/bytecode/SymbolicStringHandler.java

+                        pc._addDet(Comparator.LT, new IntegerConstant(val), new IntegerConstant(0));
+                    }


again concrete constraint

this is fixed

sohah · 2025-09-09T05:16:03Z

jpf-symbc/src/main/gov/nasa/jpf/symbc/bytecode/SymbolicStringHandler.java

+                if(!rte_flag) {
+                    th.getVM().getSystemState().setIgnored(true);


this is SO repeated in every exceptional choice, can we do it only once!

done please check the new method being used, thanks for reviewing ma'am

sohah · 2025-09-09T05:16:27Z

jpf-symbc/src/main/gov/nasa/jpf/symbc/bytecode/SymbolicStringHandler.java

+                    if(!pc.simplify()) {
+                        th.getVM().getSystemState().setIgnored(true);
+                    } else {
+                        th.createAndThrowException("java.lang.StringIndexOutOfBoundsException");


Again this is so repeatitive, can we do it only once!

I had tried a new way looking for ward at your response

f-ei8ht · 2025-09-14T21:22:29Z

@sohah hello ma'am I contributed again to the handler and fixed the repetition and some code at handleCharAt can you please check it and tell if it wrong or right also I have fixed one of the concrete constraint the other one is a mix (concrete and symbolic both values are used) thanks.

sohah · 2025-09-29T17:34:40Z

@saifk16 , I noticed that there is a single comment you haven't replied to it yet. Can you please confirm if it is addressed or not? Thank you

f-ei8ht · 2025-09-29T17:45:56Z

@saifk16 , I noticed that there is a single comment you haven't replied to it yet. Can you please confirm if it is addressed or not? Thank you

Hello @sohah ma'am I have added a comment regarding that left review thanks.

sohah

Hi @saifk16 , thank you for your effort. Here are some more comments, can you please address and let us know.

sohah · 2025-11-24T08:10:37Z

jpf-symbc/src/main/gov/nasa/jpf/symbc/bytecode/SymbolicStringHandler.java

+            } else if (currentChocie == 2) { // previous code valid operation
+                IntegerExpression result = null;
+                if (sym_v1 == null) { // operand 0 is concrete
+                    int val = s1;
+                    result = sym_v2._charAt(new IntegerConstant(val));
+                } else {
+                    if (sym_v2 == null) {
+                        ElementInfo e1 = th.getElementInfo(s2);
+                        String val2 = e1.asString();
+                        sym_v2 = new StringConstant(val2);
+                        result = sym_v2._charAt(sym_v1);
+                    } else {
+                        result = sym_v2._charAt(sym_v1);
+                    }
+                    bresult = true;
+                    //System.out.println("[handleCharAt] Ignoring: " + result.toString());
+                    // th.push(0, false);
+                }
+                sf.push(0, false);
+                sf.setOperandAttr(result);
+            }
+		}
+        return bresult; // not used


Hi @saifk16 , why this code is like it is new code. it should have the git blame of their previous authors. with this it looks like you've added this code when you did not. Can you please track back to the original owner of this code? thank you.

sohah · 2025-11-24T08:21:41Z

jpf-symbc/src/main/gov/nasa/jpf/symbc/bytecode/SymbolicStringHandler.java

@@ -1067,9 +1150,25 @@ public Instruction handleReplace(JVMInvokeInstruction invInst, ThreadInfo th) {
 	public Instruction handleSubString(JVMInvokeInstruction invInst, ThreadInfo th) {


I am unable to make a comment on line 976 that checks for the null case, I think if we are in this choice we should be safe and we should not be checking for null option under these cases, if we do then we are duplicating other work that we've done elsewhere. This comment also applies on lin 1002

sohah · 2025-11-24T08:37:27Z

jpf-symbc/src/main/gov/nasa/jpf/symbc/bytecode/SymbolicStringHandler.java

@@ -1067,9 +1150,25 @@ public Instruction handleReplace(JVMInvokeInstruction invInst, ThreadInfo th) {
 	public Instruction handleSubString(JVMInvokeInstruction invInst, ThreadInfo th) {


also, i am unable to comment on line 1040, why here when both are symbolic, you are only checking one of them not both?

sohah · 2025-11-24T08:39:38Z

jpf-symbc/src/main/gov/nasa/jpf/symbc/bytecode/SymbolicStringHandler.java

+            if (!th.isFirstStepInsn()) { // first time around
+                cg = new PCChoiceGenerator(3);
+                th.getVM().setNextChoiceGenerator(cg);
+                return invInst;
+            } else {
+                handleSubString1(invInst, th);
+                return invInst.getNext(th);
+            }
 		} else {
-			return handleSubString2(invInst, th);
+            ChoiceGenerator<?> cg;
+            if (!th.isFirstStepInsn()) { // first time around
+                cg = new PCChoiceGenerator(5);


can you insert comments why you need 3 choices versus 5 choices, it isn't clear when one gets to read it for the first time.

sohah · 2025-11-24T08:48:11Z

jpf-symbc/src/main/gov/nasa/jpf/symbc/bytecode/SymbolicStringHandler.java

+
+            if (currentChocie == 0) { // beginIndex is less than zero
+                if (!rte_flag) {
+                    th.getVM().getSystemState().setIgnored(true);
+                } else {
+                    if (sym_v2 != null) {
+                        pc._addDet(Comparator.LT, sym_v2, new IntegerConstant(0));
+                        if (!pc.simplify()) {
+                            th.getVM().getSystemState().setIgnored(true);
+                        } else {
+                            th.createAndThrowException("java.lang.StringIndexOutOfBoundsException");
+                        }
+                    } else {
+                        if (s2 < 0) {
+                            th.createAndThrowException("java.lang.StringIndexOutOfBoundsException");
+                        } else {
+                            th.getVM().getSystemState().setIgnored(true);
+                        }
+                    }
+                }
+            } else if (currentChocie == 1) { // beginIndex is greater than the length of string
+                if (!rte_flag) {
+                    th.getVM().getSystemState().setIgnored(true);
+                } else {
+                    if (sym_v3 != null) {
+                        if (sym_v2 != null) {
+                            pc._addDet(Comparator.GT, sym_v2, sym_v3._length());
+                        } else {
+                            int val = s2;
+                            pc._addDet(Comparator.GT, new IntegerConstant(val), sym_v3._length());
+                        }
+                    } else {
+                        ElementInfo e1 = th.getElementInfo(s3);
+                        String val2 = e1.asString();
+                        sym_v3 = new StringConstant(val2);
+                        pc._addDet(Comparator.GT, sym_v2, sym_v3._length());
+                    }
+                    if (!pc.simplify()) {
+                        th.getVM().getSystemState().setIgnored(true);
+                    } else {
+                        th.createAndThrowException("java.lang.StringIndexOutOfBoundsException");
+                    }
+                }
+            } else if (currentChocie == 2) { // endIndex is less than zero
+                if (!rte_flag) {
+                    th.getVM().getSystemState().setIgnored(true);
+                } else {
+                    if (sym_v1 != null) {
+                        pc._addDet(Comparator.LT, sym_v1, new IntegerConstant(0));
+                        if (!pc.simplify()) {
+                            th.getVM().getSystemState().setIgnored(true);
+                        } else {
+                            th.createAndThrowException("java.lang.StringIndexOutOfBoundsException");
+                        }
+                    } else {
+                        if (s1 < 0) {
+                            th.createAndThrowException("java.lang.StringIndexOutOfBoundsException");
+                        } else {
+                            th.getVM().getSystemState().setIgnored(true);
+                        }
+                    }
+                }
+            } else if (currentChocie == 3) { // endIndex is greater than tha length of the string
+                if (!rte_flag) {
+                    th.getVM().getSystemState().setIgnored(true);
+                } else {
+                    if (sym_v3 != null) {
+                        if (sym_v1 != null) {
+                            pc._addDet(Comparator.GT, sym_v1, sym_v3._length());
+                        } else {
+                            int val = s1;
+                            pc._addDet(Comparator.GT, new IntegerConstant(val), sym_v3._length());
+                        }
+                    } else {
+                        ElementInfo e1 = th.getElementInfo(s3);
+                        String val2 = e1.asString();
+                        sym_v3 = new StringConstant(val2);
+                        pc._addDet(Comparator.GT, sym_v1, sym_v3._length());
+                    }
+                    if (!pc.simplify()) {
+                        th.getVM().getSystemState().setIgnored(true);
+                    } else {
+                        th.createAndThrowException("java.lang.StringIndexOutOfBoundsException");
+                    }
+                }
+            } else if (currentChocie == 4) { // previous code, valid operation


my comment on handleSubstring1 and handleSubstring2 is that there are many redundant code which I think can be grouped together for nicer presentation and understanding, like this it is just too repeatitive.

also, the old code should have the names of their authors, right now, they appear with your name, can we restore the old author's names?

f-ei8ht · 2025-11-30T11:40:27Z

okay @sohah ma'am I will restore to the old author names, thanks for your review I will also add some comments and let you know

StringIndexOutOfBounds Exception supprot (substring, charAt) GSoC 2025

58e5732

saifk16 force-pushed the string-index branch from 23ce9b9 to 58e5732 Compare August 29, 2025 17:09

sohah suggested changes Sep 2, 2025

View reviewed changes

saifk16 added 2 commits September 3, 2025 17:33

fixed the script and ordered the choices

11f98af

add comments to the handleSubString(beginIndex, endIndex)

bb35ba7

sohah suggested changes Sep 3, 2025

View reviewed changes

refactored the method handleSubString2

91c6789

sohah reviewed Sep 9, 2025

View reviewed changes

saifk16 added 2 commits September 11, 2025 00:12

refactoring done for format sf.pop

17f9f38

removed concrete addition to pc just check and throw error

6038e77

sohah suggested changes Nov 24, 2025

View reviewed changes

		pc._addDet(Comparator.LT, new IntegerConstant(val), new IntegerConstant(0));
		}

		pc._addDet(Comparator.GE, new IntegerConstant(val), sym_v2._length());
		}

		if(!rte_flag) {
		th.getVM().getSystemState().setIgnored(true);

		@@ -1067,9 +1150,25 @@ public Instruction handleReplace(JVMInvokeInstruction invInst, ThreadInfo th) {
		public Instruction handleSubString(JVMInvokeInstruction invInst, ThreadInfo th) {

Conversation

saifk16 commented Aug 29, 2025

Uh oh!

saifk16 commented Aug 29, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

sohah left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

saifk16 Sep 2, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

sohah Sep 3, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

saifk16 Sep 2, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Exception Scenarios

Choice 0: beginIndex < 0

Choice 1: endIndex < 0

Choice 2: beginIndex > string.length()

Choice 3: endIndex > string.length()

Choice 4: beginIndex > endIndex

Choice 5: Default Behaviour

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

saifk16 commented Aug 29, 2025 •

edited

Loading

saifk16 Sep 2, 2025 •

edited

Loading

sohah Sep 3, 2025 •

edited

Loading

saifk16 Sep 2, 2025 •

edited

Loading

Choice 0: `beginIndex < 0`

Choice 1: `endIndex < 0`

Choice 2: `beginIndex > string.length()`

Choice 3: `endIndex > string.length()`

Choice 4: `beginIndex > endIndex`