diff --git a/src/classes/modules/java.base/java/util/regex/Matcher.java b/src/classes/modules/java.base/java/util/regex/Matcher.java index 28566ed8f..3ae49d0f9 100644 --- a/src/classes/modules/java.base/java/util/regex/Matcher.java +++ b/src/classes/modules/java.base/java/util/regex/Matcher.java @@ -160,7 +160,22 @@ public int groupCount() { } - // TODO public native MatchResult toMatchResult();-Done; - // TODO public native StringBuffer appendTail(StringBuffer sb); - // TODO public native Matcher appendReplacement(StringBuffer sb, String replacement); + /** + * Appends the input subsequence after the last match to the given StringBuffer. + * + * @param sb The target string buffer + * @return The target string buffer + */ + public native StringBuffer appendTail(StringBuffer sb); + + /** + * Implements a non-terminal append-and-replace step. + * Reads characters from the input sequence, appends them to the given + * string buffer, and then appends the replacement string. + * + * @param sb The target string buffer + * @param replacement The replacement string + * @return This matcher + */ + public native Matcher appendReplacement(StringBuffer sb, String replacement); } diff --git a/src/peers/gov/nasa/jpf/vm/JPF_java_util_regex_Matcher.java b/src/peers/gov/nasa/jpf/vm/JPF_java_util_regex_Matcher.java index 968f07a07..a4dbb5dbc 100644 --- a/src/peers/gov/nasa/jpf/vm/JPF_java_util_regex_Matcher.java +++ b/src/peers/gov/nasa/jpf/vm/JPF_java_util_regex_Matcher.java @@ -244,4 +244,76 @@ public boolean requireEnd____Z (MJIEnv env, int objref) { Matcher matcher = getInstance( env, objref); return matcher.requireEnd(); } + + @MJI + public int appendTail__Ljava_lang_StringBuffer_2__Ljava_lang_StringBuffer_2(MJIEnv env, int objref, int sbRef) { + Matcher matcher = getInstance(env, objref); + + // Use a host-side StringBuffer to capture the tail content + StringBuffer hostSb = new StringBuffer(); + matcher.appendTail(hostSb); + String tail = hostSb.toString(); + + if (tail.length() > 0) { + // Append the tail to the JPF StringBuffer via direct call + ThreadInfo ti = env.getThreadInfo(); + DirectCallStackFrame frame = ti.getReturnedDirectCall(); + + if (frame == null) { + ClassInfo sbClass = env.getClassInfo(sbRef); + MethodInfo appendMi = sbClass.getMethod("append(Ljava/lang/String;)Ljava/lang/StringBuffer;", false); + + if (appendMi != null) { + int tailRef = env.newString(tail); + frame = appendMi.createDirectCallStackFrame(ti, 1); + int argOffset = frame.setReferenceArgument(0, sbRef, null); + frame.setReferenceArgument(argOffset, tailRef, null); + ti.pushFrame(frame); + env.repeatInvocation(); + return MJIEnv.NULL; + } + } + } + + return sbRef; + } + + @MJI + public int appendReplacement__Ljava_lang_StringBuffer_2Ljava_lang_String_2__Ljava_util_regex_Matcher_2(MJIEnv env, int objref, int sbRef, int replacementRef) { + Matcher matcher = getInstance(env, objref); + + ThreadInfo ti = env.getThreadInfo(); + DirectCallStackFrame frame = ti.getReturnedDirectCall(); + + if (frame == null) { + try { + String replacement = env.getStringObject(replacementRef); + + // Use a host-side StringBuffer to capture the appendReplacement result + StringBuffer hostSb = new StringBuffer(); + matcher.appendReplacement(hostSb, replacement); + String content = hostSb.toString(); + + if (content.length() > 0) { + ClassInfo sbClass = env.getClassInfo(sbRef); + MethodInfo appendMi = sbClass.getMethod("append(Ljava/lang/String;)Ljava/lang/StringBuffer;", false); + + if (appendMi != null) { + int contentRef = env.newString(content); + frame = appendMi.createDirectCallStackFrame(ti, 1); + int argOffset = frame.setReferenceArgument(0, sbRef, null); + frame.setReferenceArgument(argOffset, contentRef, null); + ti.pushFrame(frame); + env.repeatInvocation(); + return MJIEnv.NULL; + } + } + } catch (IllegalStateException e) { + env.throwException("java.lang.IllegalStateException", "No match available"); + return MJIEnv.NULL; + } + } + + return objref; + } } diff --git a/src/tests/gov/nasa/jpf/test/java/util/regex/MatcherAppendTest.java b/src/tests/gov/nasa/jpf/test/java/util/regex/MatcherAppendTest.java new file mode 100644 index 000000000..f261bcc19 --- /dev/null +++ b/src/tests/gov/nasa/jpf/test/java/util/regex/MatcherAppendTest.java @@ -0,0 +1,100 @@ +/* + * Copyright (C) 2014, United States Government, as represented by the + * Administrator of the National Aeronautics and Space Administration. + * All rights reserved. + * + * The Java Pathfinder core (jpf-core) platform is licensed under the + * Apache License, Version 2.0 (the "License"); you may not use this file except + * in compliance with the License. You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0. + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package gov.nasa.jpf.test.java.util.regex; + +import gov.nasa.jpf.util.test.TestJPF; +import org.junit.Test; + +import java.util.regex.Matcher; +import java.util.regex.Pattern; + +/** + * Tests for Matcher.appendTail() and Matcher.appendReplacement() methods. + */ +public class MatcherAppendTest extends TestJPF { + + @Test + public void testAppendReplacementAndTail() { + if (verifyNoPropertyViolation()) { + Pattern p = Pattern.compile("cat"); + Matcher m = p.matcher("one cat two cats in the cat house"); + StringBuffer sb = new StringBuffer(); + while (m.find()) { + m.appendReplacement(sb, "dog"); + } + m.appendTail(sb); + String result = sb.toString(); + assertEquals("one dog two dogs in the dog house", result); + } + } + + @Test + public void testAppendReplacementSingleMatch() { + if (verifyNoPropertyViolation()) { + Pattern p = Pattern.compile("hello"); + Matcher m = p.matcher("say hello world"); + StringBuffer sb = new StringBuffer(); + if (m.find()) { + m.appendReplacement(sb, "hi"); + } + m.appendTail(sb); + assertEquals("say hi world", sb.toString()); + } + } + + @Test + public void testAppendTailNoMatch() { + if (verifyNoPropertyViolation()) { + Pattern p = Pattern.compile("xyz"); + Matcher m = p.matcher("no match here"); + StringBuffer sb = new StringBuffer(); + // No find() called - just appendTail + m.appendTail(sb); + assertEquals("no match here", sb.toString()); + } + } + + @Test + public void testAppendReplacementWithGroupReference() { + if (verifyNoPropertyViolation()) { + Pattern p = Pattern.compile("(\\d+)"); + Matcher m = p.matcher("item1 and item2"); + StringBuffer sb = new StringBuffer(); + while (m.find()) { + m.appendReplacement(sb, "[$1]"); + } + m.appendTail(sb); + assertEquals("item[1] and item[2]", sb.toString()); + } + } + + @Test + public void testAppendReplacementEmptyString() { + if (verifyNoPropertyViolation()) { + Pattern p = Pattern.compile("remove"); + Matcher m = p.matcher("please remove this"); + StringBuffer sb = new StringBuffer(); + while (m.find()) { + m.appendReplacement(sb, ""); + } + m.appendTail(sb); + assertEquals("please this", sb.toString()); + } + } +}