Implement appendTail and appendReplacement methods in Matcher

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);
 }

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;
+  }
 }

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());
+    }
+  }
+}