From e734381a6e606354034111dc855be9a8e454ce71 Mon Sep 17 00:00:00 2001 From: Krizhan Mariampillai Date: Wed, 30 Jan 2019 05:38:15 -0500 Subject: [PATCH] Updated Buffer and Matcher Classes (#171) --- src/classes/java/nio/Buffer.java | 18 ++++++++ src/classes/java/nio/ByteBuffer.java | 21 +++++---- src/classes/java/text/NumberFormat.java | 6 +++ src/classes/java/util/regex/Matcher.java | 7 +++ .../jpf/vm/JPF_java_util_regex_Matcher.java | 31 ++++++++++--- .../jpf/test/java/nio/ByteBufferTest.java | 44 +++++++++++++++++++ .../jpf/test/java/text/DecimalFormatTest.java | 3 ++ 7 files changed, 115 insertions(+), 15 deletions(-) create mode 100644 src/tests/gov/nasa/jpf/test/java/nio/ByteBufferTest.java diff --git a/src/classes/java/nio/Buffer.java b/src/classes/java/nio/Buffer.java index 0dadad7..46158e8 100644 --- a/src/classes/java/nio/Buffer.java +++ b/src/classes/java/nio/Buffer.java @@ -18,9 +18,26 @@ 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; } diff --git a/src/classes/java/nio/ByteBuffer.java b/src/classes/java/nio/ByteBuffer.java index e0c99a7..fa99a65 100644 --- a/src/classes/java/nio/ByteBuffer.java +++ b/src/classes/java/nio/ByteBuffer.java @@ -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; diff --git a/src/classes/java/text/NumberFormat.java b/src/classes/java/text/NumberFormat.java index 1848723..3a2f96e 100644 --- a/src/classes/java/text/NumberFormat.java +++ b/src/classes/java/text/NumberFormat.java @@ -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); } diff --git a/src/classes/java/util/regex/Matcher.java b/src/classes/java/util/regex/Matcher.java index 515318e..468ae84 100644 --- a/src/classes/java/util/regex/Matcher.java +++ b/src/classes/java/util/regex/Matcher.java @@ -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(); 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 ebf9a21..968f07a 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 @@ -39,6 +39,16 @@ public class JPF_java_util_regex_Matcher extends NativePeer { matchers = new HashMap(); } + 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 index 0000000..5caea25 --- /dev/null +++ b/src/tests/gov/nasa/jpf/test/java/nio/ByteBufferTest.java @@ -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.(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)); + } + } + +} diff --git a/src/tests/gov/nasa/jpf/test/java/text/DecimalFormatTest.java b/src/tests/gov/nasa/jpf/test/java/text/DecimalFormatTest.java index 4812659..05fc224 100644 --- a/src/tests/gov/nasa/jpf/test/java/text/DecimalFormatTest.java +++ b/src/tests/gov/nasa/jpf/test/java/text/DecimalFormatTest.java @@ -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()); } } -- 2.34.1