From b7644e07cf924d565a18407f2574482720d611c7 Mon Sep 17 00:00:00 2001 From: Valentyn Sobol Date: Fri, 29 Dec 2023 13:22:29 +0300 Subject: [PATCH 1/2] Few approximations --- approximations/build.gradle.kts | 9 +- .../generated/java/lang/StringBuffer.java | 40 +-- .../generated/java/lang/StringBuilder.java | 330 +++++++----------- .../java/util/ArrayList_SubList.java | 2 +- .../java/generated/java/util/HashMap.java | 133 +++++++ .../java/generated/java/util/HashSet.java | 2 +- .../generated/java/util/LinkedHashSet.java | 2 +- .../java/util/LinkedList_SubList.java | 2 +- .../java/generated/java/util/Optional.java | 2 +- .../concurrent/atomic/AtomicReference.java | 3 +- .../generated/java/util/regex/Matcher.java | 43 +++ .../generated/java/util/regex/Pattern.java | 25 ++ .../javax/xml/stream/XMLInputFactory.java | 15 + .../javax/xml/xpath/XPathFactory.java | 19 + 14 files changed, 398 insertions(+), 229 deletions(-) create mode 100644 approximations/src/main/java/generated/java/util/HashMap.java create mode 100644 approximations/src/main/java/generated/java/util/regex/Matcher.java create mode 100644 approximations/src/main/java/generated/java/util/regex/Pattern.java create mode 100644 approximations/src/main/java/generated/javax/xml/stream/XMLInputFactory.java create mode 100644 approximations/src/main/java/generated/javax/xml/xpath/XPathFactory.java diff --git a/approximations/build.gradle.kts b/approximations/build.gradle.kts index ed543c07..5551e936 100644 --- a/approximations/build.gradle.kts +++ b/approximations/build.gradle.kts @@ -18,11 +18,14 @@ version = "0.0.0" tasks.withType { //options.release = 8 - //options.compilerArgs.add("--add-exports=java.base/sun.nio.ch=ALL-UNNAMED") + options.compilerArgs.add("--add-exports=java.base/sun.nio.ch=ALL-UNNAMED") + options.compilerArgs.add("--add-exports=java.base/jdk.internal.misc=ALL-UNNAMED") + options.compilerArgs.add("--add-exports=java.xml/com.sun.xml.internal.stream=ALL-UNNAMED") + options.compilerArgs.add("--add-exports=java.xml/com.sun.org.apache.xpath.internal.jaxp=ALL-UNNAMED") options.compilerArgs.add("-target") - options.compilerArgs.add("1.8") + options.compilerArgs.add("11") options.compilerArgs.add("-source") - options.compilerArgs.add("1.8") + options.compilerArgs.add("11") options.compilerArgs.add("-Xlint:unchecked") } diff --git a/approximations/src/main/java/generated/java/lang/StringBuffer.java b/approximations/src/main/java/generated/java/lang/StringBuffer.java index 791d8e2f..b60902df 100644 --- a/approximations/src/main/java/generated/java/lang/StringBuffer.java +++ b/approximations/src/main/java/generated/java/lang/StringBuffer.java @@ -213,7 +213,7 @@ private char _highSurrogate(int codePoint) { private void _appendCharSequence(CharSequence seq) { /* body */ { if (seq == null) { - this.storage = this.storage.concat(LibSLRuntime.toString("null")); + this.storage = this.storage.concat("null" == null ? "null" : "null"); this.length += 4; } else { final int seqLength = seq.length(); @@ -221,7 +221,7 @@ private void _appendCharSequence(CharSequence seq) { int i = 0; for (i = 0; i < seqLength; i += 1) { char currentChar = seq.charAt(i); - this.storage = this.storage.concat(LibSLRuntime.toString(currentChar)); + this.storage = this.storage.concat(String.valueOf(currentChar)); } ; } @@ -264,7 +264,7 @@ private void _delete(int start, int end) { arrayIndex += 1; } ; - this.storage = LibSLRuntime.toString(newStr); + this.storage = new String(newStr); this.length = len; } } @@ -295,7 +295,7 @@ private void _insertCharSequence(int dstOffset, CharSequence s, int len, int sta arrayIndex += 1; } ; - this.storage = LibSLRuntime.toString(newStr); + this.storage = new String(newStr); this.length += countInsertedElements; } } @@ -317,7 +317,7 @@ private String _substring(int start, int end) { newStr_i += 1; } ; - result = LibSLRuntime.toString(newStr); + result = new String(newStr); } return result; } @@ -355,7 +355,7 @@ public synchronized StringBuffer append(CharSequence s, int start, int end) { int i = 0; for (i = start; i < end; i += 1) { char currentChar = seq.charAt(i); - this.storage = this.storage.concat(LibSLRuntime.toString(currentChar)); + this.storage = this.storage.concat(String.valueOf(currentChar)); } ; result = this; @@ -375,7 +375,7 @@ public synchronized StringBuffer append(Object obj) { this.storage = this.storage.concat("null"); this.length += 4; } else { - final String objString = LibSLRuntime.toString(obj); + final String objString = obj == null ? "null" : obj.toString(); this.storage = this.storage.concat(objString); this.length += objString.length(); } @@ -449,7 +449,7 @@ public synchronized StringBuffer append(char c) { StringBuffer result = null; Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); /* body */ { - this.storage = this.storage.concat(LibSLRuntime.toString(c)); + this.storage = this.storage.concat(String.valueOf(c)); this.length += 1; result = this; } @@ -466,7 +466,7 @@ public synchronized StringBuffer append(char[] str) { /* body */ { final int strSize = str.length; this.length += strSize; - this.storage = this.storage.concat(LibSLRuntime.toString(str)); + this.storage = this.storage.concat(new String(str)); result = this; } return result; @@ -492,7 +492,7 @@ public synchronized StringBuffer append(char[] str, int offset, int len) { } ; this.length += len; - this.storage = this.storage.concat(LibSLRuntime.toString(subArray)); + this.storage = this.storage.concat(new String(subArray)); result = this; } return result; @@ -572,14 +572,14 @@ public synchronized StringBuffer appendCodePoint(int codePoint) { /* body */ { if (_isBmpCodePoint(codePoint)) { final char curChar = ((char) codePoint); - this.storage = this.storage.concat(LibSLRuntime.toString(curChar)); + this.storage = this.storage.concat(String.valueOf(curChar)); this.length += 1; } else { if (_isValidCodePoint(codePoint)) { final char[] charsArray = new char[2]; charsArray[0] = _lowSurrogate(codePoint); charsArray[1] = _highSurrogate(codePoint); - this.storage = this.storage.concat(LibSLRuntime.toString(charsArray)); + this.storage = this.storage.concat(new String(charsArray)); this.length += 2; } else { throw new IllegalArgumentException(); @@ -879,7 +879,7 @@ public synchronized StringBuffer insert(int dstOffset, Object obj) { String s = "null"; int len = 4; if (obj != null) { - s = LibSLRuntime.toString(obj); + s = obj.toString(); len = s.length(); } _insertCharSequence(dstOffset, s, len, 0, len); @@ -955,7 +955,7 @@ public synchronized StringBuffer insert(int dstOffset, char c) { arrayIndex += 1; } ; - this.storage = LibSLRuntime.toString(subArray); + this.storage = new String(subArray); this.length += 1; result = this; } @@ -971,7 +971,7 @@ public synchronized StringBuffer insert(int dstOffset, char[] str) { Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); /* body */ { _checkOffset(dstOffset); - final String s = LibSLRuntime.toString(str); + final String s = new String(str); final int len = str.length; _insertCharSequence(dstOffset, s, len, 0, len); result = this; @@ -990,7 +990,7 @@ public synchronized StringBuffer insert(int index, char[] str, int offset, int l _checkOffset(index); final int lenStr = str.length; _checkRangeSIOOBE(offset, offset + len, lenStr); - final String s = LibSLRuntime.toString(str); + final String s = new String(str); _insertCharSequence(index, s, lenStr, offset, offset + len); result = this; } @@ -1150,7 +1150,7 @@ public synchronized StringBuffer replace(int start, int end, String s) { arrayIndex += 1; } ; - this.storage = LibSLRuntime.toString(newStr); + this.storage = new String(newStr); this.length = newLength; result = this; } @@ -1178,7 +1178,7 @@ public synchronized StringBuffer reverse() { j -= 1; } ; - this.storage = LibSLRuntime.toString(newStorage); + this.storage = new String(newStorage); } result = this; } @@ -1208,7 +1208,7 @@ public synchronized void setCharAt(int index, char ch) { arrayIndex += 1; } ; - this.storage = LibSLRuntime.toString(newStr); + this.storage = new String(newStr); } } @@ -1243,7 +1243,7 @@ public synchronized void setLength(int newLength) { } ; } - this.storage = LibSLRuntime.toString(newStr); + this.storage = new String(newStr); this.length = newLength; } } diff --git a/approximations/src/main/java/generated/java/lang/StringBuilder.java b/approximations/src/main/java/generated/java/lang/StringBuilder.java index 472aa33e..f6bbf53e 100644 --- a/approximations/src/main/java/generated/java/lang/StringBuilder.java +++ b/approximations/src/main/java/generated/java/lang/StringBuilder.java @@ -38,34 +38,15 @@ public final class StringBuilder implements LibSLRuntime.Automaton, Serializable Engine.assume(true); } - private byte __$lsl_state = __$lsl_States.Allocated; public String storage; - public int length; - - @LibSLRuntime.AutomatonConstructor - public StringBuilder(Void __$lsl_token, final byte p0, final String p1, final int p2) { - this.__$lsl_state = p0; - this.storage = p1; - this.length = p2; - } - - @LibSLRuntime.AutomatonConstructor - public StringBuilder(final Void __$lsl_token) { - this(__$lsl_token, __$lsl_States.Allocated, "", 0); - } - /** * [CONSTRUCTOR] StringBuilderAutomaton::(StringBuilder) -> void * Source: java/lang/StringBuilder.main.lsl:302 */ public StringBuilder() { - this((Void) null); - Engine.assume(this.__$lsl_state == __$lsl_States.Allocated); - /* body */ { - } - this.__$lsl_state = __$lsl_States.Initialized; + this.storage = ""; } /** @@ -73,15 +54,11 @@ public StringBuilder() { * Source: java/lang/StringBuilder.main.lsl:309 */ public StringBuilder(CharSequence seq) { - this((Void) null); - Engine.assume(this.__$lsl_state == __$lsl_States.Allocated); - /* body */ { - if (seq == null) { - throw new NullPointerException(); - } - _appendCharSequence(seq); + if (seq == null) { + throw new NullPointerException(); } - this.__$lsl_state = __$lsl_States.Initialized; + this.storage = ""; + _appendCharSequence(seq); } /** @@ -89,15 +66,10 @@ public StringBuilder(CharSequence seq) { * Source: java/lang/StringBuilder.main.lsl:318 */ public StringBuilder(String str) { - this((Void) null); - Engine.assume(this.__$lsl_state == __$lsl_States.Allocated); - /* body */ { - if (str == null) { - throw new NullPointerException(); - } - _appendString(str); + if (str == null) { + throw new NullPointerException(); } - this.__$lsl_state = __$lsl_States.Initialized; + this.storage = str; } /** @@ -105,11 +77,7 @@ public StringBuilder(String str) { * Source: java/lang/StringBuilder.main.lsl:327 */ public StringBuilder(int capacity) { - this((Void) null); - Engine.assume(this.__$lsl_state == __$lsl_States.Allocated); - /* body */ { - } - this.__$lsl_state = __$lsl_States.Initialized; + this.storage = ""; } /** @@ -142,7 +110,7 @@ private void _checkRangeSIOOBE(int start, int end, int len) { */ private void _checkIndex(int index) { /* body */ { - if ((index < 0) || (index >= this.length)) { + if ((index < 0) || (index >= this.storage.length())) { throw new StringIndexOutOfBoundsException(); } } @@ -154,7 +122,7 @@ private void _checkIndex(int index) { */ private void _checkOffset(int offset) { /* body */ { - if ((offset < 0) || (offset > this.length)) { + if ((offset < 0) || (offset > this.storage.length())) { throw new StringIndexOutOfBoundsException(); } } @@ -215,15 +183,13 @@ private char _highSurrogate(int codePoint) { private void _appendCharSequence(CharSequence seq) { /* body */ { if (seq == null) { - this.storage = this.storage.concat(LibSLRuntime.toString("null")); - this.length += 4; + this.storage = this.storage.concat("null"); } else { final int seqLength = seq.length(); - this.length += seqLength; int i = 0; for (i = 0; i < seqLength; i += 1) { char currentChar = seq.charAt(i); - this.storage = this.storage.concat(LibSLRuntime.toString(currentChar)); + this.storage = this.storage.concat(String.valueOf(currentChar)); } ; } @@ -238,9 +204,7 @@ private void _appendString(String str) { /* body */ { if (str == null) { str = "null"; - this.length += 4; } else { - this.length += str.length(); } this.storage = this.storage.concat(str); } @@ -252,7 +216,7 @@ private void _appendString(String str) { */ private void _delete(int start, int end) { /* body */ { - final int len = (this.length - end) + start; + final int len = (this.storage.length() - end) + start; char[] newStr = new char[len]; int i = 0; int arrayIndex = 0; @@ -261,13 +225,12 @@ private void _delete(int start, int end) { arrayIndex += 1; } ; - for (i = end; i < this.length; i += 1) { + for (i = end; i < this.storage.length(); i += 1) { newStr[arrayIndex] = this.storage.charAt(i); arrayIndex += 1; } ; - this.storage = LibSLRuntime.toString(newStr); - this.length = len; + this.storage = new String(newStr); } } @@ -279,7 +242,7 @@ private void _insertCharSequence(int dstOffset, CharSequence s, int len, int sta /* body */ { _checkRange(start, end, len); final int countInsertedElements = end - start; - final char[] newStr = new char[this.length + countInsertedElements]; + final char[] newStr = new char[this.storage.length() + countInsertedElements]; int i = 0; int arrayIndex = 0; for (i = 0; i < dstOffset; i += 1) { @@ -292,13 +255,12 @@ private void _insertCharSequence(int dstOffset, CharSequence s, int len, int sta arrayIndex += 1; } ; - for (i = dstOffset; i < this.length; i += 1) { + for (i = dstOffset; i < this.storage.length(); i += 1) { newStr[arrayIndex] = this.storage.charAt(i); arrayIndex += 1; } ; - this.storage = LibSLRuntime.toString(newStr); - this.length += countInsertedElements; + this.storage = new String(newStr); } } @@ -309,7 +271,7 @@ private void _insertCharSequence(int dstOffset, CharSequence s, int len, int sta private String _substring(int start, int end) { String result = null; /* body */ { - _checkRangeSIOOBE(start, end, this.length); + _checkRangeSIOOBE(start, end, this.storage.length()); final int sizeNewString = end - start; final char[] newStr = new char[sizeNewString]; int i = 0; @@ -319,7 +281,7 @@ private String _substring(int start, int end) { newStr_i += 1; } ; - result = LibSLRuntime.toString(newStr); + result = new String(newStr); } return result; } @@ -330,7 +292,7 @@ private String _substring(int start, int end) { */ public StringBuilder append(CharSequence seq) { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { _appendCharSequence(seq); result = this; @@ -344,7 +306,7 @@ public StringBuilder append(CharSequence seq) { */ public StringBuilder append(CharSequence seq, int start, int end) { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { int seqLength = 4; if (seq == null) { @@ -352,11 +314,10 @@ public StringBuilder append(CharSequence seq, int start, int end) { } seqLength = seq.length(); _checkRange(start, end, seqLength); - this.length += end - start; int i = 0; for (i = start; i < end; i += 1) { char currentChar = seq.charAt(i); - this.storage = this.storage.concat(LibSLRuntime.toString(currentChar)); + this.storage = this.storage.concat(String.valueOf(currentChar)); } ; result = this; @@ -369,20 +330,14 @@ public StringBuilder append(CharSequence seq, int start, int end) { * Source: java/lang/StringBuilder.main.lsl:365 */ public StringBuilder append(Object obj) { - StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); - /* body */ { - if (obj == null) { - this.storage = this.storage.concat("null"); - this.length += 4; - } else { - final String objString = LibSLRuntime.toString(obj); - this.storage = this.storage.concat(objString); - this.length += objString.length(); - } - result = this; + Engine.assume(this.storage != null); + if (obj == null) { + this.storage = this.storage.concat("null"); + } else { + final String objString = obj.toString(); + this.storage = this.storage.concat(objString); } - return result; + return this; } /** @@ -390,13 +345,9 @@ public StringBuilder append(Object obj) { * Source: java/lang/StringBuilder.main.lsl:382 */ public StringBuilder append(String str) { - StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); - /* body */ { - _appendString(str); - result = this; - } - return result; + Engine.assume(this.storage != null); + _appendString(str); + return this; } /** @@ -405,14 +356,12 @@ public StringBuilder append(String str) { */ public StringBuilder append(StringBuffer sb) { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { if (sb == null) { this.storage = this.storage.concat("null"); - this.length += 4; } else { - this.storage = this.storage.concat(LibSLRuntime.toString(sb)); - this.length = this.storage.length(); + this.storage = this.storage.concat(sb.toString()); } result = this; } @@ -425,14 +374,12 @@ public StringBuilder append(StringBuffer sb) { */ public StringBuilder append(boolean b) { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { if (b) { this.storage = this.storage.concat("true"); - this.length += 4; } else { this.storage = this.storage.concat("false"); - this.length += 5; } result = this; } @@ -445,10 +392,9 @@ public StringBuilder append(boolean b) { */ public StringBuilder append(char c) { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { - this.storage = this.storage.concat(LibSLRuntime.toString(c)); - this.length += 1; + this.storage = this.storage.concat(String.valueOf(c)); result = this; } return result; @@ -460,11 +406,10 @@ public StringBuilder append(char c) { */ public StringBuilder append(char[] str) { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { final int strSize = str.length; - this.length += strSize; - this.storage = this.storage.concat(LibSLRuntime.toString(str)); + this.storage = this.storage.concat(new String(str)); result = this; } return result; @@ -476,7 +421,7 @@ public StringBuilder append(char[] str) { */ public StringBuilder append(char[] str, int offset, int len) { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { final int end = offset + len; final int strSize = str.length; @@ -489,8 +434,7 @@ public StringBuilder append(char[] str, int offset, int len) { arrayIndex += 1; } ; - this.length += len; - this.storage = this.storage.concat(LibSLRuntime.toString(subArray)); + this.storage = this.storage.concat(new String(subArray)); result = this; } return result; @@ -502,11 +446,10 @@ public StringBuilder append(char[] str, int offset, int len) { */ public StringBuilder append(double d) { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { final String dString = LibSLRuntime.toString(d); this.storage = this.storage.concat(dString); - this.length += dString.length(); result = this; } return result; @@ -518,11 +461,10 @@ public StringBuilder append(double d) { */ public StringBuilder append(float f) { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { final String fString = LibSLRuntime.toString(f); this.storage = this.storage.concat(fString); - this.length += fString.length(); result = this; } return result; @@ -534,11 +476,10 @@ public StringBuilder append(float f) { */ public StringBuilder append(int i) { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { final String iString = LibSLRuntime.toString(i); this.storage = this.storage.concat(iString); - this.length += iString.length(); result = this; } return result; @@ -550,11 +491,10 @@ public StringBuilder append(int i) { */ public StringBuilder append(long lng) { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { final String lngString = LibSLRuntime.toString(lng); this.storage = this.storage.concat(lngString); - this.length += lngString.length(); result = this; } return result; @@ -566,19 +506,17 @@ public StringBuilder append(long lng) { */ public StringBuilder appendCodePoint(int codePoint) { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { if (_isBmpCodePoint(codePoint)) { final char curChar = ((char) codePoint); - this.storage = this.storage.concat(LibSLRuntime.toString(curChar)); - this.length += 1; + this.storage = this.storage.concat(String.valueOf(curChar)); } else { if (_isValidCodePoint(codePoint)) { final char[] charsArray = new char[2]; charsArray[0] = _lowSurrogate(codePoint); charsArray[1] = _highSurrogate(codePoint); - this.storage = this.storage.concat(LibSLRuntime.toString(charsArray)); - this.length += 2; + this.storage = this.storage.concat(new String(charsArray)); } else { throw new IllegalArgumentException(); } @@ -594,7 +532,7 @@ public StringBuilder appendCodePoint(int codePoint) { */ public int compareTo(StringBuilder another) { int result = 0; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { if (another == this) { result = 0; @@ -612,12 +550,12 @@ public int compareTo(StringBuilder another) { */ public StringBuilder delete(int start, int end) { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { - if (end > this.length) { - end = this.length; + if (end > this.storage.length()) { + end = this.storage.length(); } - _checkRangeSIOOBE(start, end, this.length); + _checkRangeSIOOBE(start, end, this.storage.length()); _delete(start, end); result = this; } @@ -630,7 +568,7 @@ public StringBuilder delete(int start, int end) { */ public StringBuilder deleteCharAt(int index) { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { _checkIndex(index); _delete(index, index + 1); @@ -645,7 +583,7 @@ public StringBuilder deleteCharAt(int index) { */ public int indexOf(String str) { int result = 0; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { result = this.storage.indexOf(str, 0); } @@ -658,7 +596,7 @@ public int indexOf(String str) { */ public int indexOf(String str, int fromIndex) { int result = 0; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { result = this.storage.indexOf(str, fromIndex); } @@ -671,7 +609,7 @@ public int indexOf(String str, int fromIndex) { */ public StringBuilder insert(int dstOffset, CharSequence s) { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { _checkOffset(dstOffset); int len = 4; @@ -692,7 +630,7 @@ public StringBuilder insert(int dstOffset, CharSequence s) { */ public StringBuilder insert(int dstOffset, CharSequence s, int start, int end) { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { _checkOffset(dstOffset); int len = 4; @@ -713,13 +651,13 @@ public StringBuilder insert(int dstOffset, CharSequence s, int start, int end) { */ public StringBuilder insert(int dstOffset, Object obj) { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { _checkOffset(dstOffset); String s = "null"; int len = 4; if (obj != null) { - s = LibSLRuntime.toString(obj); + s = obj.toString(); len = s.length(); } _insertCharSequence(dstOffset, s, len, 0, len); @@ -734,7 +672,7 @@ public StringBuilder insert(int dstOffset, Object obj) { */ public StringBuilder insert(int dstOffset, String s) { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { _checkOffset(dstOffset); int len = 4; @@ -755,7 +693,7 @@ public StringBuilder insert(int dstOffset, String s) { */ public StringBuilder insert(int dstOffset, boolean b) { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { _checkOffset(dstOffset); String s = "false"; @@ -776,10 +714,10 @@ public StringBuilder insert(int dstOffset, boolean b) { */ public StringBuilder insert(int dstOffset, char c) { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { _checkOffset(dstOffset); - final char[] subArray = new char[this.length + 1]; + final char[] subArray = new char[this.storage.length() + 1]; final char[] str = this.storage.toCharArray(); int i = 0; int arrayIndex = 0; @@ -790,13 +728,12 @@ public StringBuilder insert(int dstOffset, char c) { ; subArray[i] = c; arrayIndex += 1; - for (i = dstOffset; i < this.length; i += 1) { + for (i = dstOffset; i < this.storage.length(); i += 1) { subArray[arrayIndex] = str[i]; arrayIndex += 1; } ; - this.storage = LibSLRuntime.toString(subArray); - this.length += 1; + this.storage = new String(subArray); result = this; } return result; @@ -808,10 +745,10 @@ public StringBuilder insert(int dstOffset, char c) { */ public StringBuilder insert(int dstOffset, char[] str) { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { _checkOffset(dstOffset); - final String s = LibSLRuntime.toString(str); + final String s = new String(str); final int len = str.length; _insertCharSequence(dstOffset, s, len, 0, len); result = this; @@ -825,10 +762,10 @@ public StringBuilder insert(int dstOffset, char[] str) { */ public StringBuilder insert(int dstOffset, char[] str, int start, int end) { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { _checkOffset(dstOffset); - final String s = LibSLRuntime.toString(str); + final String s = new String(str); final int len = str.length; _checkRangeSIOOBE(start, start + end, len); _insertCharSequence(dstOffset, s, len, start, end); @@ -843,7 +780,7 @@ public StringBuilder insert(int dstOffset, char[] str, int start, int end) { */ public StringBuilder insert(int dstOffset, double d) { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { _checkOffset(dstOffset); String s = LibSLRuntime.toString(d); @@ -860,7 +797,7 @@ public StringBuilder insert(int dstOffset, double d) { */ public StringBuilder insert(int dstOffset, float f) { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { _checkOffset(dstOffset); String s = LibSLRuntime.toString(f); @@ -877,7 +814,7 @@ public StringBuilder insert(int dstOffset, float f) { */ public StringBuilder insert(int dstOffset, int ii) { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { _checkOffset(dstOffset); String s = LibSLRuntime.toString(ii); @@ -894,7 +831,7 @@ public StringBuilder insert(int dstOffset, int ii) { */ public StringBuilder insert(int dstOffset, long l) { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { _checkOffset(dstOffset); String s = LibSLRuntime.toString(l); @@ -911,7 +848,7 @@ public StringBuilder insert(int dstOffset, long l) { */ public int lastIndexOf(String str) { int result = 0; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { result = this.storage.lastIndexOf(str); } @@ -924,7 +861,7 @@ public int lastIndexOf(String str) { */ public int lastIndexOf(String str, int fromIndex) { int result = 0; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { result = this.storage.lastIndexOf(str, fromIndex); } @@ -937,14 +874,14 @@ public int lastIndexOf(String str, int fromIndex) { */ public StringBuilder replace(int start, int end, String s) { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { - if (end > this.length) { - end = this.length; + if (end > this.storage.length()) { + end = this.storage.length(); } - _checkRangeSIOOBE(start, end, this.length); + _checkRangeSIOOBE(start, end, this.storage.length()); final int strLength = s.length(); - final int newLength = (this.length + strLength) - (end - start); + final int newLength = (this.storage.length() + strLength) - (end - start); final char[] newStr = new char[newLength]; int arrayIndex = 0; int i = 0; @@ -958,13 +895,12 @@ public StringBuilder replace(int start, int end, String s) { arrayIndex += 1; } ; - for (i = end; i < this.length; i += 1) { + for (i = end; i < this.storage.length(); i += 1) { newStr[arrayIndex] = this.storage.charAt(i); arrayIndex += 1; } ; - this.storage = LibSLRuntime.toString(newStr); - this.length = newLength; + this.storage = new String(newStr); result = this; } return result; @@ -976,22 +912,22 @@ public StringBuilder replace(int start, int end, String s) { */ public StringBuilder reverse() { StringBuilder result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { - if (this.length != 0) { - Engine.assume(this.length > 0); + if (this.storage.length() != 0) { + Engine.assume(this.storage.length() > 0); final char[] oldStorage = this.storage.toCharArray(); - final char[] newStorage = new char[this.length]; - Engine.assume(newStorage.length == this.length); + final char[] newStorage = new char[this.storage.length()]; + Engine.assume(newStorage.length == this.storage.length()); Engine.assume(oldStorage.length == newStorage.length); - int j = this.length - 1; + int j = this.storage.length() - 1; int i = 0; - for (i = 0; i < this.length; i += 1) { + for (i = 0; i < this.storage.length(); i += 1) { newStorage[j] = oldStorage[i]; j -= 1; } ; - this.storage = LibSLRuntime.toString(newStorage); + this.storage = new String(newStorage); } result = this; } @@ -1003,12 +939,8 @@ public StringBuilder reverse() { * Source: java/lang/StringBuilder.main.lsl:841 */ public String toString() { - String result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); - /* body */ { - result = this.storage; - } - return result; + Engine.assume(this.storage != null); + return this.storage; } /** @@ -1017,9 +949,9 @@ public String toString() { */ public int capacity() { int result = 0; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { - result = this.length; + result = this.storage.length(); } return result; } @@ -1029,7 +961,7 @@ public int capacity() { * Source: java/lang/StringBuilder.main.lsl:858 */ public void ensureCapacity(int minimumCapacity) { - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { Engine.assume(true); } @@ -1041,9 +973,9 @@ public void ensureCapacity(int minimumCapacity) { */ public int length() { int result = 0; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { - result = this.length; + result = this.storage.length(); } return result; } @@ -1054,7 +986,7 @@ public int length() { */ public char charAt(int index) { char result = '?'; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { _checkIndex(index); result = this.storage.charAt(index); @@ -1067,23 +999,22 @@ public char charAt(int index) { * Source: java/lang/StringBuilder.main.lsl:881 */ public void setLength(int newLength) { - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { if (newLength < 0) { throw new StringIndexOutOfBoundsException(); } else { if (newLength == 0) { this.storage = ""; - this.length = 0; } else { int i = 0; final char[] newStr = new char[newLength]; - if (newLength > this.length) { - for (i = 0; i < this.length; i += 1) { + if (newLength > this.storage.length()) { + for (i = 0; i < this.storage.length(); i += 1) { newStr[i] = this.storage.charAt(i); } ; - for (i = this.length; i < newLength; i += 1) { + for (i = this.storage.length(); i < newLength; i += 1) { newStr[i] = 0; } ; @@ -1093,8 +1024,7 @@ public void setLength(int newLength) { } ; } - this.storage = LibSLRuntime.toString(newStr); - this.length = newLength; + this.storage = new String(newStr); } } } @@ -1105,10 +1035,10 @@ public void setLength(int newLength) { * Source: java/lang/StringBuilder.main.lsl:933 */ public void setCharAt(int index, char ch) { - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { _checkIndex(index); - final char[] newStr = new char[this.length]; + final char[] newStr = new char[this.storage.length()]; int arrayIndex = 0; int i = 0; for (i = 0; i < index; i += 1) { @@ -1118,12 +1048,12 @@ public void setCharAt(int index, char ch) { ; newStr[index] = ch; arrayIndex += 1; - for (i = index + 1; i < this.length; i += 1) { + for (i = index + 1; i < this.storage.length(); i += 1) { newStr[arrayIndex] = this.storage.charAt(i); arrayIndex += 1; } ; - this.storage = LibSLRuntime.toString(newStr); + this.storage = new String(newStr); } } @@ -1132,7 +1062,7 @@ public void setCharAt(int index, char ch) { * Source: java/lang/StringBuilder.main.lsl:956 */ public void trimToSize() { - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { Engine.assume(true); } @@ -1144,9 +1074,9 @@ public void trimToSize() { */ public String substring(int start) { String result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { - result = _substring(start, this.length); + result = _substring(start, this.storage.length()); } return result; } @@ -1157,7 +1087,7 @@ public String substring(int start) { */ public String substring(int start, int end) { String result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { result = _substring(start, end); } @@ -1170,7 +1100,7 @@ public String substring(int start, int end) { */ public CharSequence subSequence(int start, int end) { CharSequence result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { result = _substring(start, end); } @@ -1182,9 +1112,9 @@ public CharSequence subSequence(int start, int end) { * Source: java/lang/StringBuilder.main.lsl:985 */ public void getChars(int srcBegin, int srcEnd, char[] dst, int dstBegin) { - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { - _checkRangeSIOOBE(srcBegin, srcEnd, this.length); + _checkRangeSIOOBE(srcBegin, srcEnd, this.storage.length()); int n = srcEnd - srcBegin; final int dstLength = dst.length; _checkRange(dstBegin, dstBegin + n, dstLength); @@ -1204,9 +1134,9 @@ public void getChars(int srcBegin, int srcEnd, char[] dst, int dstBegin) { */ public int codePointCount(int beginIndex, int endIndex) { int result = 0; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { - if ((beginIndex < 0) || (endIndex > this.length) || (beginIndex > endIndex)) { + if ((beginIndex < 0) || (endIndex > this.storage.length()) || (beginIndex > endIndex)) { throw new IndexOutOfBoundsException(); } result = this.storage.codePointCount(beginIndex, endIndex); @@ -1220,7 +1150,7 @@ public int codePointCount(int beginIndex, int endIndex) { */ public int codePointAt(int index) { int result = 0; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { _checkIndex(index); result = this.storage.codePointAt(index); @@ -1234,7 +1164,7 @@ public int codePointAt(int index) { */ public int codePointBefore(int index) { int result = 0; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { index -= 1; _checkIndex(index); @@ -1249,7 +1179,7 @@ public int codePointBefore(int index) { */ public int offsetByCodePoints(int index, int codePointOffset) { int result = 0; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { _checkIndex(index); result = Character.offsetByCodePoints(this.storage, index, codePointOffset); @@ -1263,19 +1193,19 @@ public int offsetByCodePoints(int index, int codePointOffset) { */ public IntStream codePoints() { IntStream result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { - final int[] intStorage = new int[this.length]; + final int[] intStorage = new int[this.storage.length()]; final char[] storageChars = this.storage.toCharArray(); int i = 0; - for (i = 0; i < this.length; i += 1) { + for (i = 0; i < this.storage.length(); i += 1) { intStorage[i] = ((int) storageChars[i]); } ; result = (IntStreamLSL) ((Object) new generated.java.util.stream.IntStreamLSL((Void) null, /* state = */ generated.java.util.stream.IntStreamLSL.__$lsl_States.Initialized, /* storage = */ intStorage, - /* length = */ this.length, + /* length = */ this.storage.length(), /* closeHandlers = */ Engine.makeSymbolicList(), /* isParallel = */ false, /* linkedOrConsumed = */ false @@ -1290,19 +1220,19 @@ public IntStream codePoints() { */ public IntStream chars() { IntStream result = null; - Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); + Engine.assume(this.storage != null); /* body */ { - final int[] intStorage = new int[this.length]; + final int[] intStorage = new int[this.storage.length()]; final char[] storageChars = this.storage.toCharArray(); int i = 0; - for (i = 0; i < this.length; i += 1) { + for (i = 0; i < this.storage.length(); i += 1) { intStorage[i] = ((int) storageChars[i]); } ; result = (IntStreamLSL) ((Object) new generated.java.util.stream.IntStreamLSL((Void) null, /* state = */ generated.java.util.stream.IntStreamLSL.__$lsl_States.Initialized, /* storage = */ intStorage, - /* length = */ this.length, + /* length = */ this.storage.length(), /* closeHandlers = */ Engine.makeSymbolicList(), /* isParallel = */ false, /* linkedOrConsumed = */ false diff --git a/approximations/src/main/java/generated/java/util/ArrayList_SubList.java b/approximations/src/main/java/generated/java/util/ArrayList_SubList.java index 37e6fcb1..358fcdcc 100644 --- a/approximations/src/main/java/generated/java/util/ArrayList_SubList.java +++ b/approximations/src/main/java/generated/java/util/ArrayList_SubList.java @@ -864,7 +864,7 @@ public String toString() { int counter = this.length; for (i = i; i < end; i += 1) { final Object item = rootStorage.get(i); - result = result.concat(LibSLRuntime.toString(item)); + result = result.concat(item == null ? "null" : item.toString()); counter -= 1; if (counter != 0) { result = result.concat(", "); diff --git a/approximations/src/main/java/generated/java/util/HashMap.java b/approximations/src/main/java/generated/java/util/HashMap.java new file mode 100644 index 00000000..6c55ce49 --- /dev/null +++ b/approximations/src/main/java/generated/java/util/HashMap.java @@ -0,0 +1,133 @@ +package generated.java.util; + +import org.jacodb.approximation.annotation.Approximate; +import org.jetbrains.annotations.NotNull; +import org.jetbrains.annotations.Nullable; +import org.usvm.api.Engine; +import org.usvm.api.SymbolicMap; +import runtime.LibSLRuntime; + +import java.io.Serializable; +import java.util.Collection; +import java.util.HashSet; +import java.util.Map; +import java.util.Set; + +@Approximate(java.util.HashMap.class) +public class HashMap implements LibSLRuntime.Automaton, Map, Cloneable, Serializable { + private static final long serialVersionUID = -5024744406713321676L; + + static { + Engine.assume(true); + } + + public SymbolicMap storage = Engine.makeSymbolicMap(); + + public HashMap() { + } + + + public HashMap(int capacity) { + } + + + public HashMap(int capacity, float loadFactor) { + } + + public HashMap(Map m) { + putAll(m); + } + + @Override + public int size() { + Engine.assume(storage != null); + return storage.size(); + } + + @Override + public boolean isEmpty() { + return size() == 0; + } + + @Override + public boolean containsKey(Object key) { + Engine.assume(storage != null); + return storage.containsKey(key); + } + + @Override + public boolean containsValue(Object value) { + Engine.assume(storage != null); + return Engine.makeSymbolicBoolean(); + } + + @Override + public Object get(Object key) { + Engine.assume(storage != null); + + if (!storage.containsKey(key)) { + return null; + } + + return storage.get(key); + } + + @Nullable + @Override + public Object put(Object key, Object value) { + Engine.assume(storage != null); + if (!storage.containsKey(key)) { + storage.set(key, value); + return null; + } + + final Object prev = storage.get(key); + storage.set(key, value); + return prev; + } + + @Override + public Object remove(Object key) { + if (!storage.containsKey(key)) { + storage.remove(key); + return null; + } + + final Object prev = storage.get(key); + storage.remove(key); + return prev; + } + + @Override + public void putAll(@NotNull Map m) { + if (m instanceof java.util.HashMap) { + final HashMap other = (HashMap) m; + final SymbolicMap otherStorage = other.storage; + Engine.assume(otherStorage != null); + storage.merge(otherStorage); + } + } + + @Override + public void clear() { + storage = Engine.makeSymbolicMap(); + } + + @NotNull + @Override + public Set keySet() { + return new HashSet<>(); + } + + @NotNull + @Override + public Collection values() { + return new ArrayList(); + } + + @NotNull + @Override + public Set entrySet() { + return new HashSet<>(); + } +} diff --git a/approximations/src/main/java/generated/java/util/HashSet.java b/approximations/src/main/java/generated/java/util/HashSet.java index 910dc633..1c9c6960 100644 --- a/approximations/src/main/java/generated/java/util/HashSet.java +++ b/approximations/src/main/java/generated/java/util/HashSet.java @@ -726,7 +726,7 @@ public String toString() { while (count != 0) { final Object key = unseen.anyKey(); unseen.remove(key); - result = result.concat(LibSLRuntime.toString(key)); + result = result.concat(key == null ? "null" : key.toString()); if (count > 1) { result = result.concat(", "); } diff --git a/approximations/src/main/java/generated/java/util/LinkedHashSet.java b/approximations/src/main/java/generated/java/util/LinkedHashSet.java index c0dd48c3..56d3c5c2 100644 --- a/approximations/src/main/java/generated/java/util/LinkedHashSet.java +++ b/approximations/src/main/java/generated/java/util/LinkedHashSet.java @@ -714,7 +714,7 @@ public String toString() { while (count != 0) { final Object key = unseen.anyKey(); unseen.remove(key); - result = result.concat(LibSLRuntime.toString(key)); + result = result.concat(key == null ? "null" : key.toString()); if (count > 1) { result = result.concat(", "); } diff --git a/approximations/src/main/java/generated/java/util/LinkedList_SubList.java b/approximations/src/main/java/generated/java/util/LinkedList_SubList.java index 6c8374d9..c7289848 100644 --- a/approximations/src/main/java/generated/java/util/LinkedList_SubList.java +++ b/approximations/src/main/java/generated/java/util/LinkedList_SubList.java @@ -864,7 +864,7 @@ public String toString() { int counter = this.length; for (i = i; i < end; i += 1) { final Object item = rootStorage.get(i); - result = result.concat(LibSLRuntime.toString(item)); + result = result.concat(item == null ? "null" : item.toString()); counter -= 1; if (counter != 0) { result = result.concat(", "); diff --git a/approximations/src/main/java/generated/java/util/Optional.java b/approximations/src/main/java/generated/java/util/Optional.java index 8dc8b612..c6ba8aa9 100644 --- a/approximations/src/main/java/generated/java/util/Optional.java +++ b/approximations/src/main/java/generated/java/util/Optional.java @@ -441,7 +441,7 @@ public String toString() { if (this.value == null) { result = "Optional.empty"; } else { - final String valueStr = LibSLRuntime.toString(this.value); + final String valueStr = this.value.toString(); result = "Optional[".concat(valueStr).concat("]"); } } diff --git a/approximations/src/main/java/generated/java/util/concurrent/atomic/AtomicReference.java b/approximations/src/main/java/generated/java/util/concurrent/atomic/AtomicReference.java index 94da4629..4b34818a 100644 --- a/approximations/src/main/java/generated/java/util/concurrent/atomic/AtomicReference.java +++ b/approximations/src/main/java/generated/java/util/concurrent/atomic/AtomicReference.java @@ -304,7 +304,8 @@ public String toString() { String result = null; Engine.assume(this.__$lsl_state == __$lsl_States.Initialized); /* body */ { - result = LibSLRuntime.toString(this.value); + final Object v = this.value; + result = v == null ? "null" : v.toString(); } return result; } diff --git a/approximations/src/main/java/generated/java/util/regex/Matcher.java b/approximations/src/main/java/generated/java/util/regex/Matcher.java new file mode 100644 index 00000000..2cff2fb0 --- /dev/null +++ b/approximations/src/main/java/generated/java/util/regex/Matcher.java @@ -0,0 +1,43 @@ +package generated.java.util.regex; + +import org.jacodb.approximation.annotation.Approximate; + +import java.util.regex.MatchResult; + +@Approximate(java.util.regex.Matcher.class) +public class Matcher implements MatchResult { + @Override + public int start() { + return 0; + } + + @Override + public int start(int group) { + return 0; + } + + @Override + public int end() { + return 0; + } + + @Override + public int end(int group) { + return 0; + } + + @Override + public String group() { + return null; + } + + @Override + public String group(int group) { + return null; + } + + @Override + public int groupCount() { + return 0; + } +} diff --git a/approximations/src/main/java/generated/java/util/regex/Pattern.java b/approximations/src/main/java/generated/java/util/regex/Pattern.java new file mode 100644 index 00000000..3b36dd9b --- /dev/null +++ b/approximations/src/main/java/generated/java/util/regex/Pattern.java @@ -0,0 +1,25 @@ +package generated.java.util.regex; + +import org.jacodb.approximation.annotation.Approximate; +import org.usvm.api.Engine; + + +@Approximate(java.util.regex.Pattern.class) +public class Pattern { + private String pattern; + + private int flags; + + private Pattern(String p, int f) { + this.pattern = p; + this.flags = f; + } + + public static boolean matches(String regex, CharSequence input) { + return Engine.makeSymbolicBoolean(); + } + + public Matcher matcher(CharSequence input) { + return new Matcher(); + } +} diff --git a/approximations/src/main/java/generated/javax/xml/stream/XMLInputFactory.java b/approximations/src/main/java/generated/javax/xml/stream/XMLInputFactory.java new file mode 100644 index 00000000..7bb1f2f1 --- /dev/null +++ b/approximations/src/main/java/generated/javax/xml/stream/XMLInputFactory.java @@ -0,0 +1,15 @@ +package generated.javax.xml.stream; + +import com.sun.xml.internal.stream.XMLInputFactoryImpl; +import org.jacodb.approximation.annotation.Approximate; + +@Approximate(javax.xml.stream.XMLInputFactory.class) +public class XMLInputFactory { + public static javax.xml.stream.XMLInputFactory newInstance() { + return new XMLInputFactoryImpl(); + } + + public static javax.xml.stream.XMLInputFactory newFactory() { + return new XMLInputFactoryImpl(); + } +} diff --git a/approximations/src/main/java/generated/javax/xml/xpath/XPathFactory.java b/approximations/src/main/java/generated/javax/xml/xpath/XPathFactory.java new file mode 100644 index 00000000..764a43cc --- /dev/null +++ b/approximations/src/main/java/generated/javax/xml/xpath/XPathFactory.java @@ -0,0 +1,19 @@ +package generated.javax.xml.xpath; + +import com.sun.org.apache.xpath.internal.jaxp.XPathFactoryImpl; +import org.jacodb.approximation.annotation.Approximate; + +@Approximate(javax.xml.xpath.XPathFactory.class) +public class XPathFactory { + public static javax.xml.xpath.XPathFactory newInstance() { + return new XPathFactoryImpl(); + } + + public static javax.xml.xpath.XPathFactory newInstance(final String uri) { + return newInstance(); + } + + public static javax.xml.xpath.XPathFactory newInstance(String uri, String factoryClassName, ClassLoader classLoader) { + return newInstance(); + } +} From 0284345b07ab00e01d76a48787351e1f97f56447 Mon Sep 17 00:00:00 2001 From: Valentyn Sobol Date: Sat, 27 Jan 2024 02:20:52 +0300 Subject: [PATCH 2/2] tmp --- .../main/java/generated/java/lang/System.java | 36 ++--- .../src/main/java/generated/java/net/URL.java | 45 ++++++ .../java/generated/java/util/HashMap.java | 2 +- .../util/concurrent/ConcurrentHashMap.java | 139 ++++++++++++++++++ 4 files changed, 204 insertions(+), 18 deletions(-) create mode 100644 approximations/src/main/java/generated/java/net/URL.java create mode 100644 approximations/src/main/java/generated/java/util/concurrent/ConcurrentHashMap.java diff --git a/approximations/src/main/java/generated/java/lang/System.java b/approximations/src/main/java/generated/java/lang/System.java index 1c1cf7ae..719ff168 100644 --- a/approximations/src/main/java/generated/java/lang/System.java +++ b/approximations/src/main/java/generated/java/lang/System.java @@ -20,9 +20,11 @@ import java.lang.UnsatisfiedLinkError; import java.lang.Void; import java.util.Properties; -import jdk.internal.misc.VM; +//import jdk.internal.misc.VM; import org.jacodb.approximation.annotation.Approximate; import org.usvm.api.Engine; +import org.usvm.api.SymbolicIdentityMap; +import org.usvm.api.SymbolicMap; import runtime.LibSLRuntime; import stub.libsl.utils.SymbolicInputStream; @@ -32,7 +34,7 @@ @SuppressWarnings({"all", "unchecked"}) @Approximate(java.lang.System.class) public final class System implements LibSLRuntime.Automaton { - private static final LibSLRuntime.Map propsMap = new LibSLRuntime.Map<>(new LibSLRuntime.HashMapContainer<>()); + private static final SymbolicMap propsMap = Engine.makeSymbolicMap(); private static volatile SecurityManager security = null; @@ -50,7 +52,7 @@ public final class System implements LibSLRuntime.Automaton { private static final long NANOTIME_WARP_MAX = 1000L; - private static final LibSLRuntime.Map identityHashCodeMap = new LibSLRuntime.Map<>(new LibSLRuntime.IdentityMapContainer<>()); + private static final SymbolicIdentityMap identityHashCodeMap = Engine.makeSymbolicIdentityMap(); static { /* SystemAutomaton::() */ { @@ -85,7 +87,7 @@ private System() { */ private static void _initProperties() { /* body */ { - final LibSLRuntime.Map pm = propsMap; + final SymbolicMap pm = propsMap; final int javaVersion = 8; final String userName = "Admin"; pm.set("file.encoding", "Cp1251"); @@ -181,7 +183,7 @@ private static void initPhase1() { /* closed = */ false, /* error = */ false )); - VM.initLevel(1); +// VM.initLevel(1); } } @@ -192,7 +194,7 @@ private static void initPhase1() { private static int initPhase2() { int result = 0; /* body */ { - VM.initLevel(2); +// VM.initLevel(2); result = 0; } return result; @@ -205,8 +207,8 @@ private static int initPhase2() { private static void initPhase3() { /* body */ { security = null; - VM.initLevel(3); - VM.initLevel(4); +// VM.initLevel(3); +// VM.initLevel(4); } } @@ -227,8 +229,8 @@ public static String clearProperty(String key) { if (sm != null) { sm.checkPermission(new java.util.PropertyPermission(key, "write")); } - final LibSLRuntime.Map pm = propsMap; - if (pm.hasKey(key)) { + final SymbolicMap pm = propsMap; + if (pm.containsKey(key)) { result = pm.get(key); pm.remove(key); } @@ -300,8 +302,8 @@ public static String getProperty(String key) { if (sm != null) { sm.checkPropertyAccess(key); } - final LibSLRuntime.Map pm = propsMap; - if (pm.hasKey(key)) { + final SymbolicMap pm = propsMap; + if (pm.containsKey(key)) { result = pm.get(key); } else { result = null; @@ -327,8 +329,8 @@ public static String getProperty(String key, String def) { if (sm != null) { sm.checkPropertyAccess(key); } - final LibSLRuntime.Map pm = propsMap; - if (pm.hasKey(key)) { + final SymbolicMap pm = propsMap; + if (pm.containsKey(key)) { result = pm.get(key); } else { result = def; @@ -379,7 +381,7 @@ public static int identityHashCode(Object x) { if (x == null) { result = 0; } else { - if (identityHashCodeMap.hasKey(x)) { + if (identityHashCodeMap.containsKey(x)) { final Integer value = identityHashCodeMap.get(x); Engine.assume(value != null); result = value.intValue(); @@ -550,8 +552,8 @@ public static String setProperty(String key, String value) { if (sm != null) { sm.checkPermission(new java.util.PropertyPermission(key, "write")); } - final LibSLRuntime.Map pm = propsMap; - if (pm.hasKey(key)) { + final SymbolicMap pm = propsMap; + if (pm.containsKey(key)) { result = pm.get(key); } else { result = null; diff --git a/approximations/src/main/java/generated/java/net/URL.java b/approximations/src/main/java/generated/java/net/URL.java new file mode 100644 index 00000000..9f02ae2a --- /dev/null +++ b/approximations/src/main/java/generated/java/net/URL.java @@ -0,0 +1,45 @@ +package generated.java.net; + +import org.jacodb.approximation.annotation.Approximate; + +import java.net.InetAddress; +import java.net.MalformedURLException; +import java.net.URLStreamHandler; + +@Approximate(java.net.URL.class) +public class URL { + private String protocol; + + private String host; + + private int port = -1; + + private String file; + + private transient String query; + + private String authority; + + private transient String path; + + private transient String userInfo; + + private String ref; + + private transient InetAddress hostAddress; + + public URL(String protocol, String host, int port, String file, + URLStreamHandler handler) throws MalformedURLException { + this.protocol = protocol; + this.host = host; + this.port = port; + this.file = file; + } + + public URL(java.net.URL context, String spec, URLStreamHandler handler) throws MalformedURLException { + protocol = spec; + host = spec; + file = spec; + query = spec; + } +} diff --git a/approximations/src/main/java/generated/java/util/HashMap.java b/approximations/src/main/java/generated/java/util/HashMap.java index 6c55ce49..90c34137 100644 --- a/approximations/src/main/java/generated/java/util/HashMap.java +++ b/approximations/src/main/java/generated/java/util/HashMap.java @@ -88,8 +88,8 @@ public Object put(Object key, Object value) { @Override public Object remove(Object key) { + Engine.assume(storage != null); if (!storage.containsKey(key)) { - storage.remove(key); return null; } diff --git a/approximations/src/main/java/generated/java/util/concurrent/ConcurrentHashMap.java b/approximations/src/main/java/generated/java/util/concurrent/ConcurrentHashMap.java new file mode 100644 index 00000000..87ff0f6d --- /dev/null +++ b/approximations/src/main/java/generated/java/util/concurrent/ConcurrentHashMap.java @@ -0,0 +1,139 @@ +package generated.java.util.concurrent; + + +import generated.java.util.ArrayList; +import org.jacodb.approximation.annotation.Approximate; +import org.jetbrains.annotations.NotNull; +import org.jetbrains.annotations.Nullable; +import org.usvm.api.Engine; +import org.usvm.api.SymbolicMap; +import runtime.LibSLRuntime; + +import java.io.Serializable; +import java.util.Collection; +import java.util.HashSet; +import java.util.Map; +import java.util.Set; + +@Approximate(java.util.concurrent.ConcurrentHashMap.class) +public class ConcurrentHashMap implements LibSLRuntime.Automaton, Map, Cloneable, Serializable { + private static final long serialVersionUID = -5024744406713321676L; + + static { + Engine.assume(true); + } + + public SymbolicMap storage = Engine.makeSymbolicMap(); + + public ConcurrentHashMap() { + } + + + public ConcurrentHashMap(int capacity) { + } + + + public ConcurrentHashMap(int capacity, float loadFactor) { + } + + public ConcurrentHashMap(int initialCapacity, + float loadFactor, int concurrencyLevel) { + } + + public ConcurrentHashMap(Map m) { + putAll(m); + } + + @Override + public int size() { + Engine.assume(storage != null); + return storage.size(); + } + + @Override + public boolean isEmpty() { + return size() == 0; + } + + @Override + public boolean containsKey(Object key) { + Engine.assume(storage != null); + return storage.containsKey(key); + } + + @Override + public boolean containsValue(Object value) { + Engine.assume(storage != null); + return Engine.makeSymbolicBoolean(); + } + + @Override + public Object get(Object key) { + Engine.assume(storage != null); + + if (!storage.containsKey(key)) { + return null; + } + + return storage.get(key); + } + + @Nullable + @Override + public Object put(Object key, Object value) { + Engine.assume(storage != null); + if (!storage.containsKey(key)) { + storage.set(key, value); + return null; + } + + final Object prev = storage.get(key); + storage.set(key, value); + return prev; + } + + @Override + public Object remove(Object key) { + Engine.assume(storage != null); + if (!storage.containsKey(key)) { + return null; + } + + final Object prev = storage.get(key); + storage.remove(key); + return prev; + } + + @Override + public void putAll(@NotNull Map m) { + if (m instanceof java.util.concurrent.ConcurrentHashMap) { + final generated.java.util.concurrent.ConcurrentHashMap other = (generated.java.util.concurrent.ConcurrentHashMap) m; + final SymbolicMap otherStorage = other.storage; + Engine.assume(otherStorage != null); + storage.merge(otherStorage); + } + } + + @Override + public void clear() { + storage = Engine.makeSymbolicMap(); + } + + @NotNull + @Override + public Set keySet() { + return new HashSet<>(); + } + + @NotNull + @Override + public Collection values() { + return new ArrayList(); + } + + @NotNull + @Override + public Set entrySet() { + return new HashSet<>(); + } +}