Updated Buffer and Matcher Classes (#171)
authorKrizhan Mariampillai <krizhanmariampillai@gmail.com>
Wed, 30 Jan 2019 10:38:15 +0000 (05:38 -0500)
committercyrille-artho <cyrille-artho@users.noreply.github.com>
Wed, 30 Jan 2019 10:38:15 +0000 (11:38 +0100)
src/classes/java/nio/Buffer.java
src/classes/java/nio/ByteBuffer.java
src/classes/java/text/NumberFormat.java
src/classes/java/util/regex/Matcher.java
src/peers/gov/nasa/jpf/vm/JPF_java_util_regex_Matcher.java
src/tests/gov/nasa/jpf/test/java/nio/ByteBufferTest.java [new file with mode: 0644]
src/tests/gov/nasa/jpf/test/java/text/DecimalFormatTest.java

index 0dadad7..46158e8 100644 (file)
 package java.nio;
 
 public abstract class Buffer {
+
        protected int position;
        protected int capacity;
        protected int limit;
+       protected int mark = -1;
+
+
+       // Todo: There exists other missing methods in this class
+       // which may throw NoSuchMethodException errors to users
+       // For example checkBounds has yet to be implemented
+       Buffer(int mark, int pos, int lim, int cap) {
+               if (cap < 0)
+                       throw new IllegalArgumentException("Negative capacity: " + cap);
+               this.capacity = cap;
+               limit(lim);
+               position(pos);
+               if (mark >= 0 && mark <= pos){
+                       this.mark = mark;
+               }
+       }
 
        public final int capacity() {
                return capacity;
@@ -53,6 +70,7 @@ public abstract class Buffer {
        public final Buffer clear(){
                position = 0;
                limit = capacity;
+               mark = -1;
                return this;
        }
 
index e0c99a7..fa99a65 100644 (file)
@@ -19,12 +19,13 @@ package java.nio;
 
 public class ByteBuffer extends Buffer {
        byte[] array;
+       int offset;
 
        public static ByteBuffer allocate(int i) {
                if (i < 0) {
                        throw new IllegalArgumentException();
                }
-               ByteBuffer newBuffer = new ByteBuffer(i);
+               ByteBuffer newBuffer = new ByteBuffer(-1, 0, i, i, new byte[i], 0);
                return newBuffer;
        }
 
@@ -32,14 +33,18 @@ public class ByteBuffer extends Buffer {
                return allocate(capacity);
        }
 
-       protected ByteBuffer(int i) {
-               capacity = i;
-               this.clear();
-               array = new byte[i];
+       ByteBuffer(int mark, int pos, int lim, int cap, byte[] hb, int offset) {
+               super(mark, pos, lim, cap);
+               this.array = hb;
+               this.offset = offset;
+       }
+
+       ByteBuffer(int mark, int pos, int lim, int cap) {
+               this(mark, pos, lim, cap, null, 0);
        }
 
        public ByteBuffer duplicate() {
-               ByteBuffer copy = new ByteBuffer(capacity);
+               ByteBuffer copy = new ByteBuffer(-1, 0, capacity, capacity, new byte[capacity], 0);
                copy.array = array;
                return copy;
        }
@@ -50,7 +55,7 @@ public class ByteBuffer extends Buffer {
 
        public ByteBuffer slice() {
                int remaining = limit - position;
-               ByteBuffer copy = new ByteBuffer(remaining);
+               ByteBuffer copy = new ByteBuffer(-1, 0, remaining, remaining, new byte[remaining], 0);
                copy.array = array;
                return copy;
        }
@@ -280,7 +285,7 @@ public class ByteBuffer extends Buffer {
        }
 
        public static ByteBuffer wrap(byte[] outMess) {
-               ByteBuffer byteBuffer = new ByteBuffer(outMess.length);
+               ByteBuffer byteBuffer = new ByteBuffer(-1, 0, outMess.length, outMess.length, new byte[outMess.length], 0);
                byteBuffer.clear();
                System.arraycopy(outMess, 0 , byteBuffer.array, 0, outMess.length);
                return byteBuffer;
index 1848723..3a2f96e 100644 (file)
@@ -18,6 +18,8 @@
 
 package java.text;
 
+import java.util.Locale;
+
 public abstract class NumberFormat extends Format {
 
   static final int INTEGER_STYLE=0;
@@ -31,6 +33,10 @@ public abstract class NumberFormat extends Format {
     return new DecimalFormat(NUMBER_STYLE);
   }
 
+  public static NumberFormat getNumberInstance(Locale locale) {
+    return new DecimalFormat(NUMBER_STYLE);
+  }
+
   public static NumberFormat getInstance() {
     return new DecimalFormat(NUMBER_STYLE);
   }
index 515318e..468ae84 100644 (file)
@@ -92,6 +92,13 @@ public class Matcher {
 
   public native Matcher useAnchoringBounds(boolean b);
 
+  public Matcher usePattern(Pattern newPattern){
+    this.pattern = newPattern;
+    return updatePattern();
+  }
+
+  public native Matcher updatePattern();
+
   public native int regionStart();
 
   public native int regionEnd();
index ebf9a21..968f07a 100644 (file)
@@ -39,6 +39,16 @@ public class JPF_java_util_regex_Matcher extends NativePeer {
     matchers = new HashMap<Integer,Matcher>();
   }
 
+  Pattern getPatternFromMatcher(MJIEnv env, int objref) {
+    int patRef = env.getReferenceField(objref, "pattern");
+
+    int regexRef = env.getReferenceField(patRef, "regex");
+    String regex = env.getStringObject(regexRef);
+    int flags = env.getIntField(patRef, "flags");
+
+    return Pattern.compile(regex, flags);
+  }
+
   void putInstance (MJIEnv env, int objref, Matcher matcher) {
     int id = env.getIntField(objref,  "id");
     matchers.put(id, matcher);
@@ -52,13 +62,7 @@ public class JPF_java_util_regex_Matcher extends NativePeer {
   
   @MJI
   public void register____V (MJIEnv env, int objref) {
-    int patRef = env.getReferenceField(objref, "pattern");
-    
-    int regexRef = env.getReferenceField(patRef, "regex");
-    String regex = env.getStringObject(regexRef);
-    int flags = env.getIntField(patRef, "flags");
-    
-    Pattern pat = Pattern.compile(regex, flags);
+    Pattern pat = getPatternFromMatcher(env, objref);
 
     int inputRef = env.getReferenceField(objref, "input");
     String input = env.getStringObject(inputRef);
@@ -208,6 +212,19 @@ public class JPF_java_util_regex_Matcher extends NativePeer {
     return objref;
   }
 
+  @MJI
+  public int updatePattern____Ljava_util_regex_Matcher_2(MJIEnv env, int objref) {
+    //We get the newly updated pattern
+    Pattern pat = getPatternFromMatcher(env, objref);
+
+    //We update the matcher with the new pattern
+    Matcher matcher = getInstance(env, objref);
+    matcher = matcher.usePattern(pat);
+    putInstance(env, objref, matcher);
+
+    return objref;
+  }
+
   @MJI
   public int toString____Ljava_lang_String_2 (MJIEnv env, int objref) {
     Matcher matcher = getInstance(env, objref);
diff --git a/src/tests/gov/nasa/jpf/test/java/nio/ByteBufferTest.java b/src/tests/gov/nasa/jpf/test/java/nio/ByteBufferTest.java
new file mode 100644 (file)
index 0000000..5caea25
--- /dev/null
@@ -0,0 +1,44 @@
+/*
+ * 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.nio;
+
+import gov.nasa.jpf.util.test.TestJPF;
+import org.junit.Test;
+
+import java.util.Random;
+import java.util.Scanner;
+
+public class ByteBufferTest extends TestJPF {
+
+       /**
+        * This test case checks to see if the missing
+        * class java.nio.Buffer.<init>(IIII)V issue
+        * is resolved and fails otherwise
+        */
+       @Test
+       public void testBufferConstructor() {
+               if (verifyNoPropertyViolation()) {
+                       Random random = new Random();
+                       byte[] bytes = new byte[8];
+                       random.nextBytes(bytes);
+                       new Scanner(new String(bytes));
+               }
+       }
+
+}
index 4812659..05fc224 100644 (file)
@@ -26,6 +26,7 @@ import java.text.DecimalFormatSymbols;
 import java.text.FieldPosition;
 import java.text.NumberFormat;
 import java.text.ParsePosition;
+import java.util.Locale;
 
 import org.junit.Test;
 
@@ -64,6 +65,8 @@ public class DecimalFormatTest extends TestJPF {
       assertTrue(format.isParseIntegerOnly());
       format = NumberFormat.getNumberInstance();
       assertFalse(format.isParseIntegerOnly());
+      format = NumberFormat.getNumberInstance(Locale.ENGLISH);
+      assertFalse(format.isParseIntegerOnly());
     }
   }