diff --git a/approximations/build.gradle.kts b/approximations/build.gradle.kts index b22d5130..52cd63a8 100644 --- a/approximations/build.gradle.kts +++ b/approximations/build.gradle.kts @@ -1,7 +1,8 @@ +@file:Suppress("VulnerableLibrariesLocal") + plugins { java `maven-publish` - id("org.springframework.boot") version "3.2.0" apply false } repositories { @@ -10,15 +11,12 @@ repositories { } private val jacodbPackage = "com.github.UnitTestBot.jacodb" -private val jacodbVersion = "00164e304b" // jacodb neo branch +private val jacodbVersion = "453ec7c0b3" // jacodb neo branch dependencies { compileOnly("$jacodbPackage:jacodb-api-jvm:$jacodbVersion") compileOnly("$jacodbPackage:jacodb-approximations:$jacodbVersion") - compileOnly(files(rootDir.resolve("usvm-api/usvm-api.jar"))) - compileOnly("org.springframework.boot:spring-boot-starter-web:3.2.0") - compileOnly("org.springframework.boot:spring-boot-starter-test:3.2.0") - compileOnly("org.springframework.boot:spring-boot-starter-data-jpa:3.2.0") + compileOnly(files(rootDir.resolve("usvm-api/usvm-jvm-api.jar"))) // Fixes "unknown enum constant 'When.MAYBE'" warning compileOnly("com.google.code.findbugs:jsr305:3.0.2") } diff --git a/approximations/src/main/java/decoders/java/lang/Integer_Decoder.java b/approximations/src/main/java/decoders/java/lang/Integer_Decoder.java index 0c5f4a83..dee10d69 100644 --- a/approximations/src/main/java/decoders/java/lang/Integer_Decoder.java +++ b/approximations/src/main/java/decoders/java/lang/Integer_Decoder.java @@ -11,28 +11,28 @@ @DecoderFor(Integer.class) public final class Integer_Decoder implements ObjectDecoder { - private volatile JcMethod cached_Integer_ctor = null; + private volatile JcMethod cached_Integer_valueOf = null; private volatile JcField cached_Integer_value = null; @Override public T createInstance(final JcClassOrInterface approximation, final ObjectData approximationData, final DecoderApi decoder) { - JcMethod ctor = cached_Integer_ctor; + JcMethod valueOf = cached_Integer_valueOf; // TODO: add synchronization if needed - if (ctor == null) { + if (valueOf == null) { // looking for constructor and data field final List methods = approximation.getDeclaredMethods(); for (int i = 0, c = methods.size(); i != c; i++) { JcMethod m = methods.get(i); - if (!m.isConstructor()) continue; + if (!"valueOf".equals(m.getName())) continue; List params = m.getParameters(); if (params.size() != 1) continue; if (!"int".equals(params.get(0).getType().getTypeName())) continue; - cached_Integer_ctor = ctor = m; + cached_Integer_valueOf = valueOf = m; break; } @@ -51,7 +51,7 @@ public T createInstance(final JcClassOrInterface approximation, // assemble into a call final List args = Collections.singletonList(decoder.createIntConst(value)); - return decoder.invokeMethod(ctor, args); + return decoder.invokeMethod(valueOf, args); } @Override diff --git a/approximations/src/main/java/decoders/java/util/AbstractMap_Entry_Decoder.java b/approximations/src/main/java/decoders/java/util/AbstractMap_Entry_Decoder.java new file mode 100644 index 00000000..3735dcc1 --- /dev/null +++ b/approximations/src/main/java/decoders/java/util/AbstractMap_Entry_Decoder.java @@ -0,0 +1,42 @@ +package decoders.java.util; + +import org.jacodb.api.jvm.JcClassOrInterface; +import org.jacodb.api.jvm.JcField; +import org.usvm.api.decoder.*; +import stub.java.util.map.AbstractMap_Entry; + +import java.util.List; + +@DecoderFor(AbstractMap_Entry.class) +public class AbstractMap_Entry_Decoder implements ObjectDecoder { + private volatile JcField cached_Entry_value = null; + + @SuppressWarnings({"ForLoopReplaceableByForEach", "unchecked"}) + @Override + public T createInstance(final JcClassOrInterface approx, + final ObjectData approxData, + final DecoderApi decoder) { + JcField f_value = cached_Entry_value; + // TODO: add synchronization if needed + if (f_value == null) { + final List fields = approx.getDeclaredFields(); + for (int i = 0, c = fields.size(); i < c; i++) { + JcField f = fields.get(i); + if ("value".equals(f.getName())) { + cached_Entry_value = f_value = f; + break; + } + } + } + + T value = approxData.decodeField(f_value); + return (T) new InternalMapEntry(value); + } + + @Override + public void initializeInstance(final JcClassOrInterface approx, + final ObjectData approxData, + final T instance, + final DecoderApi decoder) { + } +} diff --git a/approximations/src/main/java/decoders/java/util/ArrayList_Decoder.java b/approximations/src/main/java/decoders/java/util/ArrayList_Decoder.java index 162bde35..a66f2d15 100644 --- a/approximations/src/main/java/decoders/java/util/ArrayList_Decoder.java +++ b/approximations/src/main/java/decoders/java/util/ArrayList_Decoder.java @@ -14,6 +14,8 @@ import java.util.Collections; import java.util.List; +import static org.usvm.api.decoder.DecoderUtils.findStorageField; + @SuppressWarnings("ForLoopReplaceableByForEach") @DecoderFor(ArrayList.class) public class ArrayList_Decoder implements ObjectDecoder { @@ -46,7 +48,6 @@ public T createInstance(final JcClassOrInterface approx, List params = m.getParameters(); if (params.size() != 1) continue; - if (!"java.lang.Object".equals(params.get(0).getType().getTypeName())) continue; cached_ArrayList_add = m_add = m; } @@ -68,14 +69,7 @@ public void initializeInstance(final JcClassOrInterface approx, JcField f_storage = cached_ArrayList_storage; // TODO: add synchronization if needed if (f_storage == null) { - final List fields = approx.getDeclaredFields(); - for (int i = 0, c = fields.size(); i < c; i++) { - JcField f = fields.get(i); - if ("storage".equals(f.getName())) { - cached_ArrayList_storage = f_storage = f; - break; - } - } + cached_ArrayList_storage = f_storage = findStorageField(approx); } if (approxData.getObjectField(f_storage) == null) diff --git a/approximations/src/main/java/decoders/java/util/HashMap_Decoder.java b/approximations/src/main/java/decoders/java/util/HashMap_Decoder.java new file mode 100644 index 00000000..37b87726 --- /dev/null +++ b/approximations/src/main/java/decoders/java/util/HashMap_Decoder.java @@ -0,0 +1,154 @@ +package decoders.java.util; + +import org.jacodb.api.jvm.*; +import org.usvm.api.SymbolicMap; +import org.usvm.api.decoder.*; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; + +import static org.usvm.api.decoder.DecoderUtils.findStorageField; +import static org.usvm.api.decoder.DecoderUtils.getAllMethods; + +@DecoderFor(HashMap.class) +public class HashMap_Decoder implements ObjectDecoder { + private volatile JcMethod[] cachedMethods = null; + private volatile JcMethod cached_HashMap_ctor = null; + private volatile JcMethod cached_HashMap_put = null; + private volatile JcField cached_HashMap_storage = null; + private volatile JcField cached_Map_map = null; + private volatile JcField cached_HashMapContainer_map = null; + private volatile JcMethod cached_MapEntry_getValue = null; + + @Override + public T createInstance(final JcClassOrInterface approximation, + final ObjectData approximationData, + final DecoderApi decoder) { + JcMethod m_ctor = cached_HashMap_ctor; + // TODO: add synchronization if needed + if (m_ctor == null) { + final List methodList = approximation.getDeclaredMethods(); + final int methodCount = methodList.size(); + JcMethod[] methods = new JcMethod[methodCount]; + cachedMethods = methods = methodList.toArray(methods); + + for (int i = 0; i != methodCount; i++) { + JcMethod m = methods[i]; + + if (m.isConstructor()) { + List params = m.getParameters(); + + // example: looking for java.util.HashMap.HashMap() + if (!params.isEmpty()) continue; + + // update global "cache" and stop the search + cached_HashMap_ctor = m_ctor = m; + break; + } + } + } + + // prepare parameters "in-place" and construct a new call + final ArrayList args = new ArrayList<>(); + return decoder.invokeMethod(m_ctor, args); + } + + @SuppressWarnings("unchecked") + @Override + public void initializeInstance(final JcClassOrInterface approximation, + final ObjectData approximationData, + final T outputInstance, + final DecoderApi decoder) { + JcField f_hs_storage = cached_HashMap_storage; + // TODO: add synchronization if needed + if (f_hs_storage == null) { + cached_HashMap_storage = f_hs_storage = findStorageField(approximation); + } + + // skip empty or erroneous objects + final ObjectData storageData = approximationData.getObjectField(f_hs_storage); + if (storageData == null) + return; + + // get primary method + JcMethod m_put = cached_HashMap_put; + // TODO: add synchronization if needed + if (m_put == null) { + // TODO: add cache + List methodsList = getAllMethods(approximation); + final int methodCount = methodsList.size(); + JcMethod[] methods = new JcMethod[methodCount]; + methodsList.toArray(methods); + for (int i = 0, c = methods.length; i != c; i++) { + JcMethod m = methods[i]; + + if (!"put".equals(m.getName())) continue; + List params = m.getParameters(); + if (params.size() != 2) continue; + + m_put = m; + break; + } + cached_HashMap_put = m_put; + } + + // prepare field references (inlined) + JcField f_m_map = cached_Map_map; + // TODO: add synchronization if needed + if (f_m_map == null) { + JcClasspath cp = approximation.getClasspath(); + { + List fields = cp.findClassOrNull("runtime.LibSLRuntime$Map").getDeclaredFields(); + for (int i = 0, c = fields.size(); i != c; i++) { + JcField field = fields.get(i); + + if ("map".equals(field.getName())) { + cached_Map_map = f_m_map = field; + break; + } + } + } + { + List fields = cp.findClassOrNull("runtime.LibSLRuntime$HashMapContainer").getDeclaredFields(); + for (int i = 0, c = fields.size(); i != c; i++) { + JcField field = fields.get(i); + + if ("map".equals(field.getName())) { + cached_HashMapContainer_map = field; + break; + } + } + } + } + + // get and parse the underlying symbolic map + final ObjectData rtMapContainerData = storageData.getObjectField(f_m_map); + if (rtMapContainerData == null) + return; // ignore invalid container + + final SymbolicMap map = rtMapContainerData.decodeSymbolicMapField(cached_HashMapContainer_map); + if (map == null) + return; // ignore invalid container + + int length = map.size(); + if (length == Integer.MAX_VALUE) + return; // ignore invalid container + + while (length > 0) { + T key = map.anyKey(); + T value = map.get(key); + if (value instanceof InternalMapEntry) { + value = ((InternalMapEntry) value).getValue(); + } + + List args = new ArrayList<>(); + args.add(outputInstance); + args.add(key); + args.add(value); + decoder.invokeMethod(m_put, args); + + map.remove(key); + length--; + } + } +} diff --git a/approximations/src/main/java/decoders/java/util/HashSet_Decoder.java b/approximations/src/main/java/decoders/java/util/HashSet_Decoder.java index 4a7634ed..7fb92e71 100644 --- a/approximations/src/main/java/decoders/java/util/HashSet_Decoder.java +++ b/approximations/src/main/java/decoders/java/util/HashSet_Decoder.java @@ -11,6 +11,8 @@ import java.util.HashSet; import java.util.List; +import static org.usvm.api.decoder.DecoderUtils.findStorageField; + @DecoderFor(HashSet.class) public final class HashSet_Decoder implements ObjectDecoder { private volatile JcMethod[] cachedMethods = null; @@ -65,17 +67,7 @@ public void initializeInstance(final JcClassOrInterface approximation, JcField f_hs_storage = cached_HashSet_storage; // TODO: add synchronization if needed if (f_hs_storage == null) { - final List fields = approximation.getDeclaredFields(); - for (int i = 0, c = fields.size(); i != c; i++) { - JcField field = fields.get(i); - String fieldName = field.getName(); - - if (!"storage".equals(fieldName)) continue; - - // early termination - cached_HashSet_storage = f_hs_storage = field; - break; - } + cached_HashSet_storage = f_hs_storage = findStorageField(approximation); } // skip erroneous objects diff --git a/approximations/src/main/java/decoders/java/util/LinkedHashMap_Decoder.java b/approximations/src/main/java/decoders/java/util/LinkedHashMap_Decoder.java new file mode 100644 index 00000000..7e9db527 --- /dev/null +++ b/approximations/src/main/java/decoders/java/util/LinkedHashMap_Decoder.java @@ -0,0 +1,155 @@ +package decoders.java.util; + +import org.jacodb.api.jvm.*; +import org.usvm.api.SymbolicMap; +import org.usvm.api.decoder.*; + +import java.util.ArrayList; +import java.util.LinkedHashMap; +import java.util.List; + +import static org.usvm.api.decoder.DecoderUtils.findStorageField; +import static org.usvm.api.decoder.DecoderUtils.getAllMethods; + +@DecoderFor(LinkedHashMap.class) +public class LinkedHashMap_Decoder implements ObjectDecoder { + private volatile JcMethod[] cachedMethods = null; + private volatile JcMethod cached_LinkedHashMap_ctor = null; + private volatile JcMethod cached_LinkedHashMap_put = null; + private volatile JcField cached_LinkedHashMap_storage = null; + private volatile JcField cached_Map_map = null; + private volatile JcField cached_HashMapContainer_map = null; + private volatile JcMethod cached_MapEntry_getValue = null; + + @Override + public T createInstance(final JcClassOrInterface approximation, + final ObjectData approximationData, + final DecoderApi decoder) { + JcMethod m_ctor = cached_LinkedHashMap_ctor; + // TODO: add synchronization if needed + if (m_ctor == null) { + final List methodList = approximation.getDeclaredMethods(); + final int methodCount = methodList.size(); + JcMethod[] methods = new JcMethod[methodCount]; + cachedMethods = methods = methodList.toArray(methods); + + for (int i = 0; i != methodCount; i++) { + JcMethod m = methods[i]; + + if (m.isConstructor()) { + List params = m.getParameters(); + + // example: looking for java.util.LinkedHashMap.LinkedHashMap() + if (!params.isEmpty()) continue; + + // update global "cache" and stop the search + cached_LinkedHashMap_ctor = m_ctor = m; + break; + } + } + } + + // prepare parameters "in-place" and construct a new call + final ArrayList args = new ArrayList<>(); + return decoder.invokeMethod(m_ctor, args); + } + + @SuppressWarnings("unchecked") + @Override + public void initializeInstance(final JcClassOrInterface approximation, + final ObjectData approximationData, + final T outputInstance, + final DecoderApi decoder) { + JcField f_hs_storage = cached_LinkedHashMap_storage; + // TODO: add synchronization if needed + if (f_hs_storage == null) { + cached_LinkedHashMap_storage = f_hs_storage = findStorageField(approximation); + } + + // skip empty or erroneous objects + final ObjectData storageData = approximationData.getObjectField(f_hs_storage); + if (storageData == null) + return; + + // get primary method + JcMethod m_put = cached_LinkedHashMap_put; + // TODO: add synchronization if needed + if (m_put == null) { + // TODO: add cache + List methodsList = getAllMethods(approximation); + final int methodCount = methodsList.size(); + JcMethod[] methods = new JcMethod[methodCount]; + methodsList.toArray(methods); + for (int i = 0, c = methods.length; i != c; i++) { + JcMethod m = methods[i]; + + if (!"put".equals(m.getName())) continue; + List params = m.getParameters(); + if (params.size() != 2) continue; + + m_put = m; + break; + } + cached_LinkedHashMap_put = m_put; + } + + // prepare field references (inlined) + JcField f_m_map = cached_Map_map; + // TODO: add synchronization if needed + if (f_m_map == null) { + JcClasspath cp = approximation.getClasspath(); + { + List fields = cp.findClassOrNull("runtime.LibSLRuntime$Map").getDeclaredFields(); + for (int i = 0, c = fields.size(); i != c; i++) { + JcField field = fields.get(i); + + if ("map".equals(field.getName())) { + cached_Map_map = f_m_map = field; + break; + } + } + } + { + List fields = cp.findClassOrNull("runtime.LibSLRuntime$HashMapContainer").getDeclaredFields(); + for (int i = 0, c = fields.size(); i != c; i++) { + JcField field = fields.get(i); + + if ("map".equals(field.getName())) { + cached_HashMapContainer_map = field; + break; + } + } + } + } + + // get and parse the underlying symbolic map + final ObjectData rtMapContainerData = storageData.getObjectField(f_m_map); + if (rtMapContainerData == null) + return; // ignore invalid container + + final SymbolicMap map = rtMapContainerData.decodeSymbolicMapField(cached_HashMapContainer_map); + if (map == null) + return; // ignore invalid container + + int length = map.size(); + if (length == Integer.MAX_VALUE) + return; // ignore invalid container + + while (length > 0) { + T key = map.anyKey(); + T value = map.get(key); + if (value instanceof InternalMapEntry) { + value = ((InternalMapEntry) value).getValue(); + } + + List args = new ArrayList<>(); + args.add(outputInstance); + args.add(key); + args.add(value); + decoder.invokeMethod(m_put, args); + + map.remove(key); + length--; + } + } +} diff --git a/approximations/src/main/java/decoders/java/util/LinkedHashSet_Decoder.java b/approximations/src/main/java/decoders/java/util/LinkedHashSet_Decoder.java index 35c9f296..d30ae40d 100644 --- a/approximations/src/main/java/decoders/java/util/LinkedHashSet_Decoder.java +++ b/approximations/src/main/java/decoders/java/util/LinkedHashSet_Decoder.java @@ -11,8 +11,11 @@ import java.util.LinkedHashSet; import java.util.List; +import static org.usvm.api.decoder.DecoderUtils.findStorageField; + @DecoderFor(LinkedHashSet.class) public class LinkedHashSet_Decoder implements ObjectDecoder { + // TODO: unify with HashSet_Decoder private volatile JcMethod[] cachedMethods = null; private volatile JcMethod cached_LinkedHashSet_ctor = null; private volatile JcMethod cached_LinkedHashSet_add = null; @@ -38,10 +41,8 @@ public T createInstance(final JcClassOrInterface approximation, if (m.isConstructor()) { List params = m.getParameters(); - // example: looking for java.util.LinkedHashSet.LinkedHashSet(int, float) - if (params.size() != 2) continue; - if (!"int".equals(params.get(0).getType().getTypeName())) continue; - if (!"float".equals(params.get(1).getType().getTypeName())) continue; + // example: looking for java.util.LinkedHashSet.LinkedHashSet() + if (!params.isEmpty()) continue; // update global "cache" and stop the search cached_LinkedHashSet_ctor = m_ctor = m; @@ -52,8 +53,6 @@ public T createInstance(final JcClassOrInterface approximation, // prepare parameters "in-place" and construct a new call final ArrayList args = new ArrayList<>(); - args.add(decoder.createIntConst(123)); - args.add(decoder.createFloatConst(0.75f)); return decoder.invokeMethod(m_ctor, args); } @@ -65,17 +64,7 @@ public void initializeInstance(final JcClassOrInterface approximation, JcField f_hs_storage = cached_LinkedHashSet_storage; // TODO: add synchronization if needed if (f_hs_storage == null) { - final List fields = approximation.getDeclaredFields(); - for (int i = 0, c = fields.size(); i != c; i++) { - JcField field = fields.get(i); - String fieldName = field.getName(); - - if ("storage".equals(fieldName)) continue; - - // early termination - cached_LinkedHashSet_storage = f_hs_storage = field; - break; - } + cached_LinkedHashSet_storage = f_hs_storage = findStorageField(approximation); } // skip empty or erroneous objects diff --git a/approximations/src/main/java/decoders/java/util/LinkedList_Decoder.java b/approximations/src/main/java/decoders/java/util/LinkedList_Decoder.java index b2c3896f..429a251a 100644 --- a/approximations/src/main/java/decoders/java/util/LinkedList_Decoder.java +++ b/approximations/src/main/java/decoders/java/util/LinkedList_Decoder.java @@ -12,6 +12,8 @@ import java.util.*; +import static org.usvm.api.decoder.DecoderUtils.findStorageField; + @SuppressWarnings("ForLoopReplaceableByForEach") @DecoderFor(LinkedList.class) public class LinkedList_Decoder implements ObjectDecoder { @@ -66,14 +68,7 @@ public void initializeInstance(final JcClassOrInterface approximation, JcField f_storage = cached_LinkedList_storage; // TODO: add synchronization if needed if (f_storage == null) { - final List fields = approximation.getDeclaredFields(); - for (int i = 0, c = fields.size(); i < c; i++) { - JcField f = fields.get(i); - if ("storage".equals(f.getName())) { - cached_LinkedList_storage = f_storage = f; - break; - } - } + cached_LinkedList_storage = f_storage = findStorageField(approximation); } if (approximationData.getObjectField(f_storage) == null) @@ -91,4 +86,3 @@ public void initializeInstance(final JcClassOrInterface approximation, } } } - diff --git a/approximations/src/main/java/encoders/java/util/AbstractCollection_Encoder.java b/approximations/src/main/java/encoders/java/util/AbstractCollection_Encoder.java new file mode 100644 index 00000000..36077a79 --- /dev/null +++ b/approximations/src/main/java/encoders/java/util/AbstractCollection_Encoder.java @@ -0,0 +1,16 @@ +package encoders.java.util; + +import generated.java.util.list.ArrayListImpl; +import org.usvm.api.encoder.EncoderFor; +import org.usvm.api.encoder.ObjectEncoder; + +import java.util.AbstractCollection; + +@EncoderFor(AbstractCollection.class) +public class AbstractCollection_Encoder implements ObjectEncoder { + + @Override + public Object encode(Object object) { + return new ArrayListImpl<>(); + } +} diff --git a/approximations/src/main/java/encoders/java/util/AbstractMap_Entry_Encoder.java b/approximations/src/main/java/encoders/java/util/AbstractMap_Entry_Encoder.java index 2b79b6cd..0172b5d1 100644 --- a/approximations/src/main/java/encoders/java/util/AbstractMap_Entry_Encoder.java +++ b/approximations/src/main/java/encoders/java/util/AbstractMap_Entry_Encoder.java @@ -11,7 +11,10 @@ public class AbstractMap_Entry_Encoder implements ObjectEncoder { @Override - public Object encode(Object list) { - return new AbstractMap_EntryImpl<>((Map.Entry) list); + public Object encode(Object entry) { + if (entry instanceof AbstractMap_Entry) + return new AbstractMap_EntryImpl<>(null, null); + + return new AbstractMap_EntryImpl<>((Map.Entry) entry); } } diff --git a/approximations/src/main/java/encoders/java/util/ArrayList_Encoder.java b/approximations/src/main/java/encoders/java/util/ArrayList_Encoder.java index 09904b22..99127876 100644 --- a/approximations/src/main/java/encoders/java/util/ArrayList_Encoder.java +++ b/approximations/src/main/java/encoders/java/util/ArrayList_Encoder.java @@ -10,9 +10,8 @@ public class ArrayList_Encoder implements ObjectEncoder { @Override - public Object encode(Object list) { - ArrayListImpl result = new ArrayListImpl<>(); - result.addAll(((ArrayList) list).stream().toList()); - return result; + public Object encode(Object object) { + ArrayList list = (ArrayList) object; + return new ArrayListImpl<>(list); } } diff --git a/approximations/src/main/java/encoders/java/util/HashSet_Encoder.java b/approximations/src/main/java/encoders/java/util/HashSet_Encoder.java index 5c02fc20..8a567327 100644 --- a/approximations/src/main/java/encoders/java/util/HashSet_Encoder.java +++ b/approximations/src/main/java/encoders/java/util/HashSet_Encoder.java @@ -4,7 +4,6 @@ import org.usvm.api.encoder.EncoderFor; import org.usvm.api.encoder.ObjectEncoder; -import java.util.Arrays; import java.util.HashSet; import java.util.Set; @@ -13,8 +12,7 @@ public class HashSet_Encoder implements ObjectEncoder { @Override public Object encode(Object object) { - HashSetImpl result = new HashSetImpl<>(); - result.addAll(Arrays.asList(((Set) object).toArray())); - return result; + Set set = (Set) object; + return new HashSetImpl<>(set); } } diff --git a/approximations/src/main/java/encoders/java/util/LinkedHashSet_Encoder.java b/approximations/src/main/java/encoders/java/util/LinkedHashSet_Encoder.java new file mode 100644 index 00000000..b1df736e --- /dev/null +++ b/approximations/src/main/java/encoders/java/util/LinkedHashSet_Encoder.java @@ -0,0 +1,18 @@ +package encoders.java.util; + +import generated.java.util.set.LinkedHashSetImpl; +import org.usvm.api.encoder.EncoderFor; +import org.usvm.api.encoder.ObjectEncoder; + +import java.util.LinkedHashSet; + +@EncoderFor(LinkedHashSet.class) +public class LinkedHashSet_Encoder implements ObjectEncoder { + + @Override + @SuppressWarnings("unchecked") + public Object encode(Object object) { + LinkedHashSet set = (LinkedHashSet) object; + return new LinkedHashSetImpl<>(set); + } +} diff --git a/approximations/src/main/java/encoders/java/util/LinkedList_Encoder.java b/approximations/src/main/java/encoders/java/util/LinkedList_Encoder.java new file mode 100644 index 00000000..6eb4d251 --- /dev/null +++ b/approximations/src/main/java/encoders/java/util/LinkedList_Encoder.java @@ -0,0 +1,17 @@ +package encoders.java.util; + +import generated.java.util.list.LinkedListImpl; +import org.usvm.api.encoder.EncoderFor; +import org.usvm.api.encoder.ObjectEncoder; + +import java.util.LinkedList; + +@EncoderFor(LinkedList.class) +public class LinkedList_Encoder implements ObjectEncoder { + + @Override + public Object encode(Object object) { + LinkedList list = (LinkedList) object; + return new LinkedListImpl<>(list); + } +} diff --git a/approximations/src/main/java/encoders/java/util/StringBuilder_Encoder.java b/approximations/src/main/java/encoders/java/util/StringBuilder_Encoder.java new file mode 100644 index 00000000..65bd39c2 --- /dev/null +++ b/approximations/src/main/java/encoders/java/util/StringBuilder_Encoder.java @@ -0,0 +1,15 @@ +package encoders.java.util; + +import generated.java.lang.StringBuilderImpl; +import org.usvm.api.encoder.EncoderFor; +import org.usvm.api.encoder.ObjectEncoder; + +@EncoderFor(java.lang.StringBuilder.class) +public class StringBuilder_Encoder implements ObjectEncoder { + + @Override + public Object encode(Object object) { + StringBuilder sb = (StringBuilder) object; + return new StringBuilderImpl(sb.toString()); + } +} diff --git a/approximations/src/main/java/encoders/java/util/String_Encoder.java b/approximations/src/main/java/encoders/java/util/String_Encoder.java index d8c3b59c..3b5c67b6 100644 --- a/approximations/src/main/java/encoders/java/util/String_Encoder.java +++ b/approximations/src/main/java/encoders/java/util/String_Encoder.java @@ -4,11 +4,28 @@ import org.usvm.api.encoder.EncoderFor; import org.usvm.api.encoder.ObjectEncoder; +import java.lang.reflect.Field; + @EncoderFor(java.lang.String.class) public class String_Encoder implements ObjectEncoder { @Override public Object encode(Object object) { - return new StringImpl(((String) object).getBytes()); + String string = (String) object; + Field arrayField; + try { + arrayField = String.class.getDeclaredField("value"); + } catch (NoSuchFieldException e) { + throw new RuntimeException(e); + } + arrayField.setAccessible(true); + boolean isDefault; + try { + isDefault = arrayField.get(string) == null; + } catch (IllegalAccessException e) { + throw new RuntimeException(e); + } + byte[] bytes = isDefault ? new byte[0] : string.getBytes(); + return new StringImpl(bytes); } } diff --git a/approximations/src/main/java/encoders/java/util/ThreadLocal_Encoder.java b/approximations/src/main/java/encoders/java/util/ThreadLocal_Encoder.java index 0f5964a7..ba4e7ce3 100644 --- a/approximations/src/main/java/encoders/java/util/ThreadLocal_Encoder.java +++ b/approximations/src/main/java/encoders/java/util/ThreadLocal_Encoder.java @@ -9,6 +9,6 @@ public class ThreadLocal_Encoder implements ObjectEncoder { @Override public Object encode(Object object) { - return new ThreadLocalImpl<>(); + return new ThreadLocalImpl<>(object); } } diff --git a/approximations/src/main/java/generated/java/lang/IntegerImpl.java b/approximations/src/main/java/generated/java/lang/IntegerImpl.java index 168d659a..3eddf28f 100644 --- a/approximations/src/main/java/generated/java/lang/IntegerImpl.java +++ b/approximations/src/main/java/generated/java/lang/IntegerImpl.java @@ -26,12 +26,6 @@ public final class IntegerImpl implements Comparable, Serializable public static final int BYTES = 4; - public static final char[] digits = { '0', '1', '2', '3', '4', '5', '6', '7', '8', '9', 'a', 'b', 'c', 'd', 'e', 'f', 'g', 'h', 'i', 'j', 'k', 'l', 'm', 'n', 'o', 'p', 'q', 'r', 's', 't', 'u', 'v', 'w', 'x', 'y', 'z' }; - - public static final char[] DigitTens = { '0', '0', '0', '0', '0', '0', '0', '0', '0', '0', '1', '1', '1', '1', '1', '1', '1', '1', '1', '1', '2', '2', '2', '2', '2', '2', '2', '2', '2', '2', '3', '3', '3', '3', '3', '3', '3', '3', '3', '3', '4', '4', '4', '4', '4', '4', '4', '4', '4', '4', '5', '5', '5', '5', '5', '5', '5', '5', '5', '5', '6', '6', '6', '6', '6', '6', '6', '6', '6', '6', '7', '7', '7', '7', '7', '7', '7', '7', '7', '7', '8', '8', '8', '8', '8', '8', '8', '8', '8', '8', '9', '9', '9', '9', '9', '9', '9', '9', '9', '9' }; - - public static final char[] DigitOnes = { '0', '1', '2', '3', '4', '5', '6', '7', '8', '9', '0', '1', '2', '3', '4', '5', '6', '7', '8', '9', '0', '1', '2', '3', '4', '5', '6', '7', '8', '9', '0', '1', '2', '3', '4', '5', '6', '7', '8', '9', '0', '1', '2', '3', '4', '5', '6', '7', '8', '9', '0', '1', '2', '3', '4', '5', '6', '7', '8', '9', '0', '1', '2', '3', '4', '5', '6', '7', '8', '9', '0', '1', '2', '3', '4', '5', '6', '7', '8', '9', '0', '1', '2', '3', '4', '5', '6', '7', '8', '9', '0', '1', '2', '3', '4', '5', '6', '7', '8', '9' }; - public static final int[] sizeTable = { 9, 99, 999, 9999, 99999, 999999, 9999999, 99999999, 999999999, 2147483647 }; static { diff --git a/approximations/src/main/java/generated/java/lang/StringBuilderImpl.java b/approximations/src/main/java/generated/java/lang/StringBuilderImpl.java index 98d52929..63f5819f 100644 --- a/approximations/src/main/java/generated/java/lang/StringBuilderImpl.java +++ b/approximations/src/main/java/generated/java/lang/StringBuilderImpl.java @@ -14,6 +14,7 @@ import java.lang.String; import java.lang.StringBuffer; import java.lang.StringIndexOutOfBoundsException; +import java.util.Arrays; import java.util.stream.IntStream; import generated.java.util.stream.IntStreamImpl; @@ -30,273 +31,389 @@ public final class StringBuilderImpl implements Serializable, Comparable 1073741823) throw new OutOfMemoryError("Requested array size exceeds VM limit"); - this.value = new char[STRING_BUILDER_LENGTH_MAX]; + + this.value = new byte[STRING_BUILDER_LENGTH_MAX]; + this.byteCount = 0; } - private void _appendCharSequence(CharSequence seq, int seqStart, int seqEnd) { - if (seqStart < 0 || seqStart > seqEnd || seqEnd > seq.length()) - throw new IndexOutOfBoundsException(); - int available = this.value.length - this.count; - int len = seqEnd - seqStart; - if (len > available) - len = available; - if (len <= 0) - return; + private static String _getString(CharSequence seq) { + if (seq instanceof String) + return (String) seq; - String str; - if (seq instanceof String) { - str = (String) seq; - } else { - str = LibSLRuntime.toString(seq); + return LibSLRuntime.toString(seq); + } + + private static byte[] _getBytesOfSeq(CharSequence seq) { + if (seq instanceof String) + return ((String) seq).getBytes(); + + if (seq instanceof StringBuilderImpl) { + StringBuilderImpl sb = (StringBuilderImpl) seq; + return Arrays.copyOf(sb.value, sb.byteCount); } - char[] chars = str.toCharArray(); - LibSLRuntime.ArrayActions.copy(chars, seqStart, this.value, this.count, len); - this.count += len; + + return LibSLRuntime.toString(seq).getBytes(); + } + + private static CharSequence _getCharSequence(CharSequence seq) { + if (seq == null) + return "null"; + + return seq; } - private String _asString(int posStart, int posEnd) { - int len = posEnd - posStart; - if (len == 0) - return ""; + private static CharSequence _getCharSequence(Object obj) { + if (obj == null) + return "null"; - char[] symbols = new char[len]; - LibSLRuntime.ArrayActions.copy(this.value, posStart, symbols, 0, len); - return LibSLRuntime.toString(this.value); + return LibSLRuntime.toString(obj); } - public String _asString() { - int len = this.count; - if (len == 0) - return ""; + private static CharSequence _getCharSequence(boolean b) { + if (b) + return "true"; - if (len == this.value.length) - return LibSLRuntime.toString(this.value); + return "false"; + } - char[] symbols = new char[len]; - LibSLRuntime.ArrayActions.copy(this.value, 0, symbols, 0, len); - return LibSLRuntime.toString(this.value); + private int _charPosToBytePos(int charPos) { + return charPos << coder; } - private void _insertCharSequence(int offset, CharSequence seq, int seqStart, int seqEnd) { - if (seqStart < 0 || seqStart > seqEnd || seqEnd > seq.length() || offset > this.count) + private int _bytePosToCharPos(int charPos) { + return charPos >> coder; + } + + private static void _checkRangeBounds(int start, int end, int rightBound) { + if (start < 0 || start > end || end > rightBound) throw new IndexOutOfBoundsException(); + } + + private static void _checkSeqBounds(CharSequence seq, int seqStart, int seqEnd) { + _checkRangeBounds(seqStart, seqEnd, seq.length()); + } + + private void _checkByteOffset(int byteOffset) { + if (byteOffset < 0 || byteOffset > this.byteCount) + throw new IndexOutOfBoundsException(); + } + + private void _checkCharOffset(int charOffset) { + _checkByteOffset(_charPosToBytePos(charOffset)); + } + + private int _getByteSeqLength(int byteOffset, int byteSeqStart, int byteSeqEnd) { + int availableBytes = this.value.length - byteOffset; + int byteSeqLength = byteSeqEnd - byteSeqStart; + if (byteSeqLength > availableBytes) + byteSeqLength = availableBytes; + + return byteSeqLength; + } + + // TODO: unify _appendCharSequence with _appendChars #Approx + private void _appendCharSequence(CharSequence seq, int seqStart, int seqEnd) { + _checkSeqBounds(seq, seqStart, seqEnd); + + int byteSeqStart = _charPosToBytePos(seqStart); + int byteSeqEnd = _charPosToBytePos(seqEnd); + int byteSeqLength = _getByteSeqLength(byteCount, byteSeqStart, byteSeqEnd); + byte[] bytes = _getBytesOfSeq(seq); + LibSLRuntime.ArrayActions.copy(bytes, byteSeqStart, this.value, byteCount, byteSeqLength); + this.byteCount += byteSeqLength; + } + + private void _appendChars(char[] seq, int seqStart, int seqEnd) { + _checkRangeBounds(seqStart, seqEnd, seq.length); + + int byteSeqStart = _charPosToBytePos(seqStart); + int byteSeqEnd = _charPosToBytePos(seqEnd); + int byteSeqLength = _getByteSeqLength(byteCount, byteSeqStart, byteSeqEnd); + byte[] bytes = StringImpl._getBytes(seq); + LibSLRuntime.ArrayActions.copy(bytes, byteSeqStart, this.value, byteCount, byteSeqLength); + this.byteCount += byteSeqLength; + } + + private void _appendCharSequence(CharSequence seq) { + _appendCharSequence(seq, 0, seq.length()); + } + + private StringImpl _asString(int posStart, int posEnd) { + int bytePosStart = _charPosToBytePos(posStart); + int bytePosEnd = _charPosToBytePos(posEnd); + int byteLength = bytePosEnd - bytePosStart; + if (byteLength == 0) + return StringImpl._emptyString; + + if (bytePosStart == 0 && bytePosEnd == this.value.length) + return new StringImpl(this.value); + + byte[] bytes = new byte[byteLength]; + LibSLRuntime.ArrayActions.copy(this.value, bytePosStart, bytes, 0, byteLength); + return new StringImpl(bytes); + } + + public StringImpl _asString() { + return _asString(0, this.byteCount); + } + + // TODO: unify _insertCharSequence with _insertChars #Approx + private void _insertCharSequence(int offset, CharSequence seq, int seqStart, int seqEnd) { + _checkSeqBounds(seq, seqStart, seqEnd); - int available = this.value.length - offset; - int len = seqEnd - seqStart; - if (len > available) - len = available; + int byteOffset = _charPosToBytePos(offset); + _checkByteOffset(byteOffset); - if (len <= 0) + int byteSeqStart = _charPosToBytePos(seqStart); + int byteSeqEnd = _charPosToBytePos(seqEnd); + int availableBytes = this.value.length - byteOffset; + int byteLength = byteSeqEnd - byteSeqStart; + if (byteLength > availableBytes) + byteLength = availableBytes; + + if (byteLength <= 0) return; - int availableForLeftovers = available - len; + int availableForLeftovers = availableBytes - byteLength; if (availableForLeftovers > 0) { - int rightLeftovers = this.count - offset; - if (rightLeftovers > availableForLeftovers) { + int rightLeftovers = this.byteCount - byteOffset; + if (rightLeftovers > availableForLeftovers) rightLeftovers = availableForLeftovers; - } - if (rightLeftovers > 0) { - int rightIndex = offset + 1; - LibSLRuntime.ArrayActions.copy(this.value, rightIndex, this.value, rightIndex + len, rightLeftovers); - } + + if (rightLeftovers > 0) + // Moving bytes, that would be replaced, beyond right bound of insertion + LibSLRuntime.ArrayActions.copy(this.value, byteOffset, this.value, byteOffset + byteLength, rightLeftovers); } - String str; - if (seq instanceof String) { - str = (String) seq; - } else { - str = LibSLRuntime.toString(seq); + + byte[] bytes = _getBytesOfSeq(seq); + LibSLRuntime.ArrayActions.copy(bytes, byteSeqStart, this.value, byteOffset, byteLength); + this.byteCount += byteLength; + } + + @SuppressWarnings("SameParameterValue") + private void _insertChars(int offset, char[] chars, int seqStart, int seqEnd) { + _checkRangeBounds(seqStart, seqEnd, chars.length); + + int byteOffset = _charPosToBytePos(offset); + _checkByteOffset(byteOffset); + + int byteSeqStart = _charPosToBytePos(seqStart); + int byteSeqEnd = _charPosToBytePos(seqEnd); + int availableBytes = this.value.length - byteOffset; + int byteLength = byteSeqEnd - byteSeqStart; + if (byteLength > availableBytes) + byteLength = availableBytes; + + if (byteLength <= 0) + return; + + int availableForLeftovers = availableBytes - byteLength; + if (availableForLeftovers > 0) { + int rightLeftovers = this.byteCount - byteOffset; + if (rightLeftovers > availableForLeftovers) + rightLeftovers = availableForLeftovers; + + if (rightLeftovers > 0) + // Moving bytes, that would be replaced, beyond right bound of insertion + LibSLRuntime.ArrayActions.copy(this.value, byteOffset, this.value, byteOffset + byteLength, rightLeftovers); } - char[] chars = str.toCharArray(); - LibSLRuntime.ArrayActions.copy(chars, seqStart, this.value, offset, len); - this.count += len; + + byte[] bytes = StringImpl._getBytes(chars); + LibSLRuntime.ArrayActions.copy(bytes, byteSeqStart, this.value, byteOffset, byteLength); + this.byteCount += byteLength; + } + + private void _insertCharSequence(int offset, CharSequence seq) { + _insertCharSequence(offset, seq, 0, seq.length()); } private void _deleteChars(int start, int end) { - if (start < 0 || start > end || end > this.count) - throw new IndexOutOfBoundsException(); + int byteStart = _charPosToBytePos(start); + int byteEnd = _charPosToBytePos(end); + _checkRangeBounds(byteStart, byteEnd, this.byteCount); - int leftovers = this.count - end; + int leftovers = this.byteCount - byteEnd; if (leftovers > 0) - LibSLRuntime.ArrayActions.copy(this.value, end, this.value, start, leftovers); - this.count -= end - start; + LibSLRuntime.ArrayActions.copy(this.value, byteEnd, this.value, byteStart, leftovers); + int deletedBytesSize = byteEnd - byteStart; + this.byteCount -= deletedBytesSize; } @SuppressWarnings("DataFlowIssue") private void _assumeInvariants() { Engine.assume(this.value != null); Engine.assume(this.value.length <= STRING_BUILDER_LENGTH_MAX); - Engine.assume(this.count <= this.value.length); - Engine.assume(this.count >= 0); + Engine.assume(this.byteCount <= this.value.length); + Engine.assume(this.byteCount >= 0); + Engine.assume(this.coder == StringImpl._currentCoder()); } public StringBuilderImpl append(CharSequence seq) { _assumeInvariants(); - if (seq == null) { - _appendCharSequence("null", 0, 4); - } else { - _appendCharSequence(seq, 0, seq.length()); - } + seq = _getCharSequence(seq); + _appendCharSequence(seq); return this; } - @SuppressWarnings("ReplaceNullCheck") public StringBuilderImpl append(CharSequence seq, int start, int end) { _assumeInvariants(); - if (seq == null) { - _appendCharSequence("null", start, end); - } else { - _appendCharSequence(seq, start, end); - } + seq = _getCharSequence(seq); + _appendCharSequence(seq, start, end); + return this; } public StringBuilderImpl append(Object obj) { _assumeInvariants(); - if (obj == null) { - _appendCharSequence("null", 0, 4); - } else { - String seq = LibSLRuntime.toString(obj); - _appendCharSequence(seq, 0, seq.length()); - } + CharSequence seq = _getCharSequence(obj); + _appendCharSequence(seq); + return this; } public StringBuilderImpl append(String str) { _assumeInvariants(); - if (str == null) { - _appendCharSequence("null", 0, 4); - } else { - _appendCharSequence(str, 0, str.length()); - } + CharSequence seq = _getCharSequence(str); + _appendCharSequence(seq); + return this; } public StringBuilderImpl append(StringBuffer sb) { _assumeInvariants(); - if (sb == null) { - _appendCharSequence("null", 0, 4); - } else { - String seq = LibSLRuntime.toString(sb); - _appendCharSequence(seq, 0, seq.length()); - } + CharSequence seq = _getCharSequence(sb); + _appendCharSequence(seq); + return this; } public StringBuilderImpl append(boolean x) { _assumeInvariants(); - if (x) { - _appendCharSequence("true", 0, 4); - } else { - _appendCharSequence("false", 0, 5); - } + CharSequence seq = _getCharSequence(x); + _appendCharSequence(seq); + return this; } public StringBuilderImpl append(char x) { _assumeInvariants(); - if (this.count < this.value.length) { - value[this.count] = x; - this.count++; + if (this.byteCount < this.value.length) { + StringImpl._addCharToBytes(value, byteCount, x); + this.byteCount++; } + return this; } - public StringBuilderImpl append(char[] str) { + public StringBuilderImpl append(char[] chars) { _assumeInvariants(); - String seq = LibSLRuntime.toString(str); - _appendCharSequence(seq, 0, seq.length()); + _appendChars(chars, 0, chars.length); + return this; } - public StringBuilderImpl append(char[] str, int offset, int len) { + public StringBuilderImpl append(char[] chars, int offset, int len) { _assumeInvariants(); - String seq = LibSLRuntime.toString(str); - _appendCharSequence(seq, offset, len); + _appendChars(chars, offset, len); + return this; } public StringBuilderImpl append(double x) { _assumeInvariants(); String seq = LibSLRuntime.toString(x); - _appendCharSequence(seq, 0, seq.length()); + _appendCharSequence(seq); + return this; } public StringBuilderImpl append(float x) { _assumeInvariants(); String seq = LibSLRuntime.toString(x); - _appendCharSequence(seq, 0, seq.length()); + _appendCharSequence(seq); + return this; } public StringBuilderImpl append(int x) { _assumeInvariants(); String seq = LibSLRuntime.toString(x); - _appendCharSequence(seq, 0, seq.length()); + _appendCharSequence(seq); + return this; } public StringBuilderImpl append(long x) { _assumeInvariants(); String seq = LibSLRuntime.toString(x); - _appendCharSequence(seq, 0, seq.length()); + _appendCharSequence(seq); + return this; } public StringBuilderImpl appendCodePoint(int codePoint) { + // TODO: support code points #Approx _assumeInvariants(); - int cnt = this.count; + int cnt = this.byteCount; int len = this.value.length; if (Character.isBmpCodePoint(codePoint)) { if (cnt + 1 <= len) { - value[cnt] = ((char) codePoint); - this.count = cnt + 1; + value[cnt] = (byte) codePoint; + this.byteCount = cnt + 1; } } else { if (Character.isValidCodePoint(codePoint)) { if (cnt + 2 <= len) { - value[cnt + 1] = Character.lowSurrogate(codePoint); - value[cnt] = Character.highSurrogate(codePoint); - this.count = cnt + 2; + value[cnt + 1] = (byte) Character.lowSurrogate(codePoint); + value[cnt] = (byte) Character.highSurrogate(codePoint); + this.byteCount = cnt + 2; } } else { throw new IllegalArgumentException(); @@ -307,24 +424,27 @@ public StringBuilderImpl appendCodePoint(int codePoint) { public int capacity() { _assumeInvariants(); - return this.value.length; + return _bytePosToCharPos(this.value.length); } public char charAt(int index) { + // TODO: fix #Approx _assumeInvariants(); - if (index < 0 || index >= this.count) + index = _charPosToBytePos(index); + if (index < 0 || index >= this.byteCount) throw new StringIndexOutOfBoundsException(); - return value[index]; + return StringImpl._bytesToChar(value, index); } @NotNull public IntStream chars() { + // TODO: fix #Approx _assumeInvariants(); - int len = this.count; + int len = this.byteCount; int[] intValues = new int[len]; for (int i = 0; i < len; i++) { - intValues[i] = value[i]; + intValues[i] = StringImpl._bytesToChar(value, i); } return new IntStreamImpl(intValues); @@ -332,36 +452,40 @@ public IntStream chars() { public int codePointAt(int index) { _assumeInvariants(); - if (index < 0 || index >= this.count) + if (index < 0 || index >= this.byteCount) throw new StringIndexOutOfBoundsException(index); - return Character.codePointAt(this.value, index, this.count); + // TODO: support code points #Approx + return 0; } public int codePointBefore(int index) { _assumeInvariants(); int i = index - 1; - if (i < 0 || i >= this.count) + if (i < 0 || i >= this.byteCount) throw new StringIndexOutOfBoundsException(index); - return Character.codePointBefore(this.value, index, 0); + // TODO: support code points #Approx + return 0; } public int codePointCount(int beginIndex, int endIndex) { _assumeInvariants(); - if (beginIndex < 0 || beginIndex > endIndex || endIndex > this.count) + if (beginIndex < 0 || beginIndex > endIndex || endIndex > this.byteCount) throw new IndexOutOfBoundsException(); - return Character.codePointCount(this.value, beginIndex, endIndex - beginIndex); + // TODO: support code points #Approx + return 0; } @NotNull public IntStream codePoints() { + // TODO: support code points #Approx _assumeInvariants(); - int len = this.count; + int len = this.byteCount; int[] intValues = new int[len]; for (int i = 0; i < len; i++) { - intValues[i] = value[i]; + intValues[i] = StringImpl._bytesToChar(value, i); } return new IntStreamImpl(intValues); } @@ -371,20 +495,23 @@ public int compareTo(@NotNull StringBuilderImpl another) { if (another == this) return 0; - String thisString = _asString(); - String anotherString = another._asString(); + // TODO: implement compareTo in StringImpl #Approx + String thisString = _asString().toString(); + String anotherString = another._asString().toString(); return thisString.compareTo(anotherString); } public StringBuilderImpl delete(int start, int end) { _assumeInvariants(); _deleteChars(start, end); + return this; } public StringBuilderImpl deleteCharAt(int index) { _assumeInvariants(); _deleteChars(index, index + 1); + return this; } @@ -393,8 +520,9 @@ public void ensureCapacity(int minimumCapacity) { } public void getChars(int srcBegin, int srcEnd, char[] dst, int dstBegin) { + // TODO: fix #Approx _assumeInvariants(); - if (srcBegin < 0 || srcBegin > srcEnd || srcEnd > this.count) + if (srcBegin < 0 || srcBegin > srcEnd || srcEnd > this.byteCount) throw new StringIndexOutOfBoundsException(); int len = srcEnd - srcBegin; if (dst == null) @@ -403,83 +531,76 @@ public void getChars(int srcBegin, int srcEnd, char[] dst, int dstBegin) { throw new IndexOutOfBoundsException(); if (len > 0) LibSLRuntime.ArrayActions.copy(this.value, srcBegin, dst, dstBegin, len); + + LibSLRuntime.not_implemented(); } public char[] getValue() { _assumeInvariants(); - return this.value; + return StringImpl._getChars(this.value); } public int indexOf(String str) { _assumeInvariants(); - return _asString().indexOf(str); + // TODO: implement indexOf in StringImpl #Approx + return _asString().toString().indexOf(str); } public int indexOf(String str, int fromIndex) { _assumeInvariants(); - return _asString().indexOf(str, fromIndex); + // TODO: implement indexOf in StringImpl #Approx + return _asString().toString().indexOf(str, fromIndex); } public StringBuilderImpl insert(int dstOffset, CharSequence s) { _assumeInvariants(); - if (s == null) { - _insertCharSequence(dstOffset, "null", 0, 4); - } else { - _insertCharSequence(dstOffset, s, 0, s.length()); - } + _insertCharSequence(dstOffset, s); + return this; } - @SuppressWarnings("ReplaceNullCheck") public StringBuilderImpl insert(int dstOffset, CharSequence s, int start, int end) { _assumeInvariants(); - if (s == null) { - _insertCharSequence(dstOffset, "null", start, end); - } else { - _insertCharSequence(dstOffset, s, start, end); - } + _insertCharSequence(dstOffset, s, start, end); + return this; } public StringBuilderImpl insert(int dstOffset, Object obj) { _assumeInvariants(); - if (obj == null) { - _insertCharSequence(dstOffset, "null", 0, 4); - } else { - String s = LibSLRuntime.toString(obj); - _insertCharSequence(dstOffset, s, 0, s.length()); - } + CharSequence seq = _getCharSequence(obj); + _insertCharSequence(dstOffset, seq); + return this; } public StringBuilderImpl insert(int dstOffset, String s) { _assumeInvariants(); - if (s == null) { - _insertCharSequence(dstOffset, "null", 0, 4); - } else { - _insertCharSequence(dstOffset, s, 0, s.length()); - } + _insertCharSequence(dstOffset, s); + return this; } public StringBuilderImpl insert(int dstOffset, boolean x) { _assumeInvariants(); - String s = LibSLRuntime.toString(x); - _insertCharSequence(dstOffset, s, 0, s.length()); + CharSequence seq = _getCharSequence(x); + _insertCharSequence(dstOffset, seq); + return this; } public StringBuilderImpl insert(int dstOffset, char x) { _assumeInvariants(); - String s = LibSLRuntime.toString(x); - _insertCharSequence(dstOffset, s, 0, 1); + CharSequence seq = _getCharSequence(x); + _insertCharSequence(dstOffset, seq, 0, 1); + return this; } public StringBuilderImpl insert(int dstOffset, char[] x) { _assumeInvariants(); - String s = LibSLRuntime.toString(x); - _insertCharSequence(dstOffset, s, 0, s.length()); + _insertChars(dstOffset, x, 0, x.length); + return this; } @@ -487,118 +608,122 @@ public StringBuilderImpl insert(int index, char[] str, int offset, int len) { _assumeInvariants(); char[] arr = new char[len]; LibSLRuntime.ArrayActions.copy(str, offset, arr, 0, len); - String s = LibSLRuntime.toString(arr); - _insertCharSequence(index, s, 0, len); + _insertChars(index, arr, 0, len); + return this; } public StringBuilderImpl insert(int dstOffset, double x) { _assumeInvariants(); String s = LibSLRuntime.toString(x); - _insertCharSequence(dstOffset, s, 0, s.length()); + _insertCharSequence(dstOffset, s); + return this; } public StringBuilderImpl insert(int dstOffset, float x) { _assumeInvariants(); String s = LibSLRuntime.toString(x); - _insertCharSequence(dstOffset, s, 0, s.length()); + _insertCharSequence(dstOffset, s); + return this; } public StringBuilderImpl insert(int dstOffset, int x) { _assumeInvariants(); String s = LibSLRuntime.toString(x); - _insertCharSequence(dstOffset, s, 0, s.length()); + _insertCharSequence(dstOffset, s); + return this; } public StringBuilderImpl insert(int dstOffset, long x) { _assumeInvariants(); String s = LibSLRuntime.toString(x); - _insertCharSequence(dstOffset, s, 0, s.length()); + _insertCharSequence(dstOffset, s); + return this; } public int lastIndexOf(String str) { _assumeInvariants(); - return _asString().lastIndexOf(str, this.count); + return _asString().toString().lastIndexOf(str, this.byteCount); } public int lastIndexOf(String str, int fromIndex) { _assumeInvariants(); - return _asString().lastIndexOf(str, fromIndex); + return _asString().toString().lastIndexOf(str, fromIndex); } public int length() { _assumeInvariants(); - return this.count; + return this.byteCount; } public int offsetByCodePoints(int index, int codePointOffset) { _assumeInvariants(); - if (index < 0 || index > this.count) + if (index < 0 || index > this.byteCount) throw new IndexOutOfBoundsException(); - return Character.offsetByCodePoints(this.value, 0, this.count, index, codePointOffset); + // TODO: support code points #Approx + return 0; } public StringBuilderImpl replace(int start, int end, String s) { _assumeInvariants(); _deleteChars(start, end); - if (s == null) { - _insertCharSequence(start, "null", 0, 4); - } else { - _insertCharSequence(start, s, 0, s.length()); - } + _insertCharSequence(start, s); + return this; } public StringBuilderImpl reverse() { _assumeInvariants(); - if (this.count == 0) - return this; - - boolean hasSurrogates = false; - int n = this.count - 1; - for (int i = (n - 1) >> 1; i > -1; i--) { - int k = n - i; - char cj = value[i]; - char ck = value[k]; - value[i] = ck; - value[k] = cj; - if (Character.isSurrogate(cj) || Character.isSurrogate(ck)) { - hasSurrogates = true; - } - } - if (!hasSurrogates) + if (this.byteCount == 0) return this; - for (int i = 0; i < n; i++) { - char c2 = value[i]; - if (Character.isLowSurrogate(c2)) { - char c1 = value[i + 1]; - if (Character.isHighSurrogate(c1)) { - value[i] = c1; - i++; - value[i] = c2; - } - } - } + // TODO: implement #Approx +// boolean hasSurrogates = false; +// int n = this.byteCount - 1; +// for (int i = (n - 1) >> 1; i > -1; i--) { +// int k = n - i; +// byte cj = value[i]; +// byte ck = value[k]; +// value[i] = ck; +// value[k] = cj; +// if (Character.isSurrogate(cj) || Character.isSurrogate(ck)) { +// hasSurrogates = true; +// } +// } +// if (!hasSurrogates) +// return this; +// +// for (int i = 0; i < n; i++) { +// char c2 = value[i]; +// if (Character.isLowSurrogate(c2)) { +// char c1 = value[i + 1]; +// if (Character.isHighSurrogate(c1)) { +// value[i] = c1; +// i++; +// value[i] = c2; +// } +// } +// } return this; } public void setCharAt(int index, char x) { _assumeInvariants(); - if (index < 0 || index >= this.count) + if (index < 0 || index >= this.byteCount) throw new StringIndexOutOfBoundsException(); - value[index] = x; + StringImpl._addCharToBytes(value, index, x); } public void setLength(int newLength) { _assumeInvariants(); + newLength = _charPosToBytePos(newLength); int maxLength = this.value.length; if (newLength > maxLength) newLength = maxLength; @@ -606,46 +731,49 @@ public void setLength(int newLength) { if (newLength < 0) throw new StringIndexOutOfBoundsException(); - if (newLength < this.count) { - this.count = newLength; + if (newLength < this.byteCount) { + this.byteCount = newLength; return; } - if (newLength > this.count) { - LibSLRuntime.ArrayActions.fillRange(this.value, this.count, newLength, ((char) 0)); - this.count = newLength; + if (newLength > this.byteCount) { + LibSLRuntime.ArrayActions.fillRange(this.value, this.byteCount, newLength, ((byte) 0)); + this.byteCount = newLength; } } @NotNull public CharSequence subSequence(int start, int end) { _assumeInvariants(); - if (start < 0 || start > end || end > this.count) + // TODO: fix #Approx + if (start < 0 || start > end || end > this.byteCount) throw new StringIndexOutOfBoundsException(); - return _asString(start, end); + return _asString(start, end).toString(); } public String substring(int start) { _assumeInvariants(); - if (start < 0 || start > this.count) + // TODO: fix #Approx + if (start < 0 || start > this.byteCount) throw new StringIndexOutOfBoundsException(); - return _asString(start, this.count); + return _asString(start, this.byteCount).toString(); } public String substring(int start, int end) { _assumeInvariants(); - if (start < 0 || start > end || end > this.count) + // TODO: fix #Approx + if (start < 0 || start > end || end > this.byteCount) throw new StringIndexOutOfBoundsException(); - return _asString(start, end); + return _asString(start, end).toString(); } @NotNull public String toString() { _assumeInvariants(); - return _asString(); + return _asString().toString(); } public void trimToSize() { diff --git a/approximations/src/main/java/generated/java/lang/StringImpl.java b/approximations/src/main/java/generated/java/lang/StringImpl.java index c730a8a7..9cafde84 100644 --- a/approximations/src/main/java/generated/java/lang/StringImpl.java +++ b/approximations/src/main/java/generated/java/lang/StringImpl.java @@ -3,12 +3,13 @@ import java.io.Serializable; import java.lang.Object; import java.lang.StringIndexOutOfBoundsException; +import java.util.Arrays; import org.jacodb.approximation.annotation.Approximate; import org.usvm.api.Engine; import runtime.LibSLRuntime; -@SuppressWarnings("unused") +@SuppressWarnings({"unused", "overrides"}) @Approximate(java.lang.String.class) public class StringImpl implements Serializable { @@ -17,38 +18,161 @@ public class StringImpl implements Serializable { private static final int STRING_LENGTH_MAX = 50; - public byte[] value; + static final byte UTF16 = 1; - public int length; + static final byte LATIN1 = 0; - public StringImpl(byte[] value, int length) { + static final boolean COMPACT_STRINGS; + + static { + // Enforce coder == UTF8 + COMPACT_STRINGS = true; + } + + private final byte[] value; + + // TODO: everywhere add assume 'coder == LATIN1' #Approx + private final byte coder; + + public static StringImpl _emptyString = new StringImpl(new byte[] {}); + + public static byte _currentCoder() { + return COMPACT_STRINGS ? LATIN1 : UTF16; + } + + private int _charPosToBytePos(int charPos) { + return charPos << coder; + } + + private int _bytePosToCharPos(int charPos) { + return charPos >> coder; + } + + private static void _checkOffset(int offset, int length) { + if (offset < 0 || offset >= length) + throw new IndexOutOfBoundsException(); + } + + public static byte[] _charToBytes(char value) { + if (COMPACT_STRINGS) { + byte[] bytes = new byte[1]; + Engine.assume(value <= 0xFF); + bytes[0] = (byte) value; + return bytes; + } + + byte[] bytes = new byte[2]; + bytes[0] = (byte) value; + bytes[1] = (byte) (value >> 8); + return bytes; + } + + private static char _charFrom2Bytes(byte fst, byte snd) { + return (char) (((char) fst) | (((char) snd) << 8)); + } + + public static char _charFromByte(byte b) { + return (char) (((int) b) & 0xFF); + } + + public static char _bytesToChar(byte[] bytes, int bytePos) { + if (COMPACT_STRINGS) + return _charFromByte(bytes[bytePos]); + + return _charFrom2Bytes(bytes[bytePos], bytes[bytePos + 1]); + } + + public static void _addCharToBytes(byte[] bytes, int index, char value) { + if (COMPACT_STRINGS) { + Engine.assume(value <= 0xFF); + bytes[index] = (byte) value; + } else { + bytes[index++] = (byte) value; + bytes[index] = (byte) (value >> 8); + } + } + + public static byte[] _getBytes(char[] chars) { + int size = chars.length << _currentCoder(); + byte[] bytes = new byte[size]; + if (COMPACT_STRINGS) { + for (int i = 0; i < chars.length; i++) { + char c = chars[i]; + Engine.assume(c <= 0xFF); + bytes[i] = (byte) chars[i]; + } + } else { + int byteIndex = 0; + for (char c : chars) { + bytes[byteIndex++] = (byte) c; + bytes[byteIndex] = (byte) (c >> 8); + byteIndex++; + } + } + + return bytes; + } + + public static char[] _getChars(byte[] bytes) { + int size = bytes.length >> _currentCoder(); + char[] chars = new char[size]; + if (COMPACT_STRINGS) { + for (int i = 0; i < bytes.length; i++) { + byte c = bytes[i]; + chars[i] = _charFromByte(bytes[i]); + } + } else { + int byteIndex = 0; + for (int i = 0; i < chars.length; i++) { + char c = _charFrom2Bytes(bytes[byteIndex], bytes[byteIndex + 1]); + chars[i] = c; + byteIndex += 2; + } + } + + return chars; + } + + private StringImpl(byte[] value, byte coder) { + Engine.assume(coder == _currentCoder()); this.value = value; - this.length = length; + this.coder = coder; } public StringImpl() { - this(new byte[0], 0); + this(new byte[0], _currentCoder()); } public StringImpl(StringImpl original) { - this(original.value, original.length); + this(original.value, original.coder); } public StringImpl(byte[] bytes) { - int len = bytes.length; - this.length = len; - this.value = new byte[len]; - LibSLRuntime.ArrayActions.copy(bytes, 0, this.value, 0, len); + this(bytes, 0, bytes.length); } - public static java.lang.String copyValueOf(char[] data) { - return LibSLRuntime.toString(data); + private static void _checkBoundsOffCount(int offset, int count, int length) { + if (offset < 0 || count < 0 || offset > length - count) { + throw new StringIndexOutOfBoundsException(); + } } - public static java.lang.String copyValueOf(char[] data, int offset, int count) { + public StringImpl(byte[] bytes, int offset, int length) { + _checkBoundsOffCount(offset, length, bytes.length); + this.value = new byte[length]; + this.coder = _currentCoder(); + LibSLRuntime.ArrayActions.copy(bytes, offset, this.value, 0, length); + } + + public static StringImpl copyValueOf(char[] data) { + byte[] bytes = _getBytes(data); + return new StringImpl(bytes); + } + + public static StringImpl copyValueOf(char[] data, int offset, int count) { char[] segment = new char[count]; LibSLRuntime.ArrayActions.copy(data, offset, segment, 0, count); - return LibSLRuntime.toString(segment); + return copyValueOf(segment); } public static java.lang.String valueOf(Object x) { @@ -59,18 +183,18 @@ public static java.lang.String valueOf(boolean x) { return LibSLRuntime.toString(x); } - public static java.lang.String valueOf(char x) { - return LibSLRuntime.toString(x); + public static StringImpl valueOf(char x) { + byte[] bytes = _charToBytes(x); + return new StringImpl(bytes); } - public static java.lang.String valueOf(char[] data) { - return LibSLRuntime.toString(data); + public static StringImpl valueOf(char[] data) { + byte[] bytes = _getBytes(data); + return new StringImpl(bytes); } - public static java.lang.String valueOf(char[] data, int offset, int count) { - char[] segment = new char[count]; - LibSLRuntime.ArrayActions.copy(data, offset, segment, 0, count); - return LibSLRuntime.toString(segment); + public static StringImpl valueOf(char[] data, int offset, int count) { + return copyValueOf(data, offset, count); } public static java.lang.String valueOf(double x) { @@ -90,50 +214,110 @@ public static java.lang.String valueOf(long x) { } @SuppressWarnings("DataFlowIssue") + private void _assumeInvariants(StringImpl obj) { + Engine.assume(obj.coder == _currentCoder()); + Engine.assume(obj.value != null); + int len = obj.value.length >> obj.coder; + Engine.assume(len >= 0); + // TODO: add Engine.assumeSymbolic(instance, bool) #ASAP + Engine.assume(len <= STRING_LENGTH_MAX); + } + + private void _assumeInvariants() { + _assumeInvariants(this); + } + + boolean isLatin1() { + _assumeInvariants(); + return _currentCoder() == LATIN1; + } + + byte coder() { + _assumeInvariants(); + return coder; + } + + public int length() { + _assumeInvariants(); + return value.length >> coder; + } + + public char charAt(int index) { + _assumeInvariants(); + + int byteIndex = _charPosToBytePos(index); + _checkOffset(byteIndex, this.value.length); + + return _bytesToChar(this.value, byteIndex); + } + public StringImpl concat(StringImpl str) { - Engine.assume(this.value != null); - Engine.assume(this.value.length <= STRING_LENGTH_MAX); - Engine.assume(this.length == this.value.length); + _assumeInvariants(); + _assumeInvariants(str); + byte[] otherVal = str.value; int otherLen = otherVal.length; if (otherLen == 0) return this; - int newLength = this.length + otherLen; + int newLength = this.value.length + otherLen; byte[] newValue = new byte[newLength]; - LibSLRuntime.ArrayActions.copy(this.value, 0, newValue, 0, this.length); - LibSLRuntime.ArrayActions.copy(otherVal, 0, newValue, this.length, otherLen); - return new StringImpl(newValue, newLength); + LibSLRuntime.ArrayActions.copy(this.value, 0, newValue, 0, this.value.length); + LibSLRuntime.ArrayActions.copy(otherVal, 0, newValue, this.value.length, otherLen); + return new StringImpl(newValue); } - @SuppressWarnings("DataFlowIssue") public byte[] getBytes() { - Engine.assume(this.value != null); - Engine.assume(this.value.length <= STRING_LENGTH_MAX); - Engine.assume(this.length == this.value.length); - return this.value; + _assumeInvariants(); + return Arrays.copyOf(this.value, this.value.length); } - @SuppressWarnings("DataFlowIssue") public void getBytes(int srcBegin, int srcEnd, byte[] dst, int dstBegin) { - if (srcBegin < 0) + _assumeInvariants(); + + int srcByteBegin = _charPosToBytePos(srcBegin); + int srcByteEnd = _charPosToBytePos(srcEnd); + int dstByteBegin = _charPosToBytePos(dstBegin); + + if (srcByteBegin < 0) throw new StringIndexOutOfBoundsException(srcBegin); - if (this.length < srcEnd) + + if (this.value.length < srcByteEnd) throw new StringIndexOutOfBoundsException(srcEnd); - int count = srcEnd - srcBegin; + + int count = srcByteEnd - srcByteBegin; if (count < 0) throw new StringIndexOutOfBoundsException(count); - Engine.assume(this.value != null); - Engine.assume(this.value.length <= STRING_LENGTH_MAX); - Engine.assume(this.length == this.value.length); - LibSLRuntime.ArrayActions.copy(this.value, srcBegin, dst, dstBegin, count); + + LibSLRuntime.ArrayActions.copy(this.value, srcByteBegin, dst, dstByteBegin, count); } - public boolean isEmpty() { - return this.length == 0; + public static boolean latin1Equals(byte[] value, byte[] other) { + if (value.length == other.length) { + for(int i = 0; i < value.length; ++i) { + if (value[i] != other[i]) { + return false; + } + } + + return true; + } else { + return false; + } } - public int length() { - return this.length; + public boolean equals(Object anObject) { + _assumeInvariants(); + if (this == anObject) { + return true; + } else { + if (anObject instanceof StringImpl) { + StringImpl aString = (StringImpl)anObject; + _assumeInvariants(aString); + return (!COMPACT_STRINGS || this.coder == aString.coder) && latin1Equals(this.value, aString.value); + } + + return false; + } } } diff --git a/approximations/src/main/java/generated/java/lang/SystemHelpersImpl.java b/approximations/src/main/java/generated/java/lang/SystemHelpersImpl.java new file mode 100644 index 00000000..2b15ae13 --- /dev/null +++ b/approximations/src/main/java/generated/java/lang/SystemHelpersImpl.java @@ -0,0 +1,10 @@ +package generated.java.lang; + +import org.jacodb.approximation.annotation.Approximate; +import runtime.LibSLRuntime; + +@Approximate(stub.java.lang.SystemHelpers.class) +public class SystemHelpersImpl { + + public static final LibSLRuntime.Map identityHashCodeMap = new LibSLRuntime.Map<>(new LibSLRuntime.IdentityMapContainer<>()); +} diff --git a/approximations/src/main/java/generated/java/lang/SystemImpl.java b/approximations/src/main/java/generated/java/lang/SystemImpl.java index b91d594a..03267058 100644 --- a/approximations/src/main/java/generated/java/lang/SystemImpl.java +++ b/approximations/src/main/java/generated/java/lang/SystemImpl.java @@ -17,18 +17,18 @@ import org.jacodb.approximation.annotation.Approximate; import org.usvm.api.Engine; import runtime.LibSLRuntime; +import stub.java.lang.SystemHelpers; @SuppressWarnings({"unused", "removal"}) @Approximate(java.lang.System.class) public final class SystemImpl { - private static final LibSLRuntime.Map propsMap = new LibSLRuntime.Map<>(new LibSLRuntime.HashMapContainer<>()); - private static volatile SecurityManager security = null; + private static Properties props; - private static Properties props = null; + private static volatile SecurityManager security = null; @SuppressWarnings("FieldMayBeFinal") - private static Console console = null; + private static Console cons = null; public static InputStream in = null; @@ -36,12 +36,6 @@ public final class SystemImpl { public static PrintStream err = null; - private static final long NANOTIME_BEGINNING_OF_TIME = 1000L; - - private static final long NANOTIME_WARP_MAX = 1000L; - - private static final LibSLRuntime.Map identityHashCodeMap = new LibSLRuntime.Map<>(new LibSLRuntime.IdentityMapContainer<>()); - static { initPhase1(); initPhase2(); @@ -50,71 +44,88 @@ public final class SystemImpl { private SystemImpl() { } + private static void _initProperty(LibSLRuntime.Map pm, Properties properties, String key, String value) { + pm.set(key, value); + switch (key) { + // Do not add private system properties to the Properties + case "sun.nio.MaxDirectMemorySize": + case "sun.nio.PageAlignDirectMemory": + // used by java.lang.Integer.IntegerCache + case "java.lang.Integer.IntegerCache.high": + // used by sun.launcher.LauncherHelper + case "sun.java.launcher.diag": + // used by jdk.internal.loader.ClassLoaders + case "jdk.boot.class.path.append": + break; + default: + properties.put(key, value); + } + } + private static void _initProperties() { - LibSLRuntime.Map pm = propsMap; + props = new Properties(); int javaVersion = 8; String userName = "Admin"; - pm.set("file.encoding", "Cp1251"); - pm.set("sun.io.unicode.encoding", "UnicodeLittle"); - pm.set("sun.jnu.encoding", "Cp1251"); - pm.set("sun.stderr.encoding", "cp866"); - pm.set("sun.stdout.encoding", "cp866"); + props.setProperty("file.encoding", "Cp1251"); + props.setProperty("sun.io.unicode.encoding", "UnicodeLittle"); + props.setProperty("sun.jnu.encoding", "Cp1251"); + props.setProperty("sun.stderr.encoding", "cp866"); + props.setProperty("sun.stdout.encoding", "cp866"); String[] versionStrings = { "0", "1", "2", "3", "4", "5", "6", "7", "8", "9", "10", "11", "12", "13", "14", "15" }; String versionString = versionStrings[javaVersion]; - pm.set("java.specification.name", "Java Platform API Specification"); - pm.set("java.specification.vendor", "Oracle Corporation"); - pm.set("java.specification.version", versionString); - pm.set("java.vm.info", "mixed mode"); - pm.set("java.vm.name", "OpenJDK 64-Bit Server VM"); - pm.set("java.vm.specification.name", "Java Virtual Machine Specification"); - pm.set("java.vm.specification.vendor", "Oracle Corporation"); - pm.set("java.vm.specification.version", versionString); - pm.set("java.vm.vendor", "Eclipse Adoptium"); - pm.set("java.vm.version", versionString.concat(".0.362+9")); - pm.set("java.library.path", "C:\\Program Files\\Eclipse Adoptium\\jdk-8.0.362.9-hotspot\\bin;C:\\Windows\\Sun\\Java\\bin;C:\\Windows\\system32;."); - pm.set("java.home", "C:\\Program Files\\Eclipse Adoptium\\jdk-8.0.362.9-hotspot"); - pm.set("sun.boot.library.path", "C:\\Program Files\\Eclipse Adoptium\\jdk-8.0.362.9-hotspot\\bin"); - pm.set("java.io.tmpdir", "T:\\Temp\\"); - pm.set("java.class.path", "."); + props.setProperty("java.specification.name", "Java Platform API Specification"); + props.setProperty("java.specification.vendor", "Oracle Corporation"); + props.setProperty("java.specification.version", versionString); + props.setProperty("java.vm.info", "mixed mode"); + props.setProperty("java.vm.name", "OpenJDK 64-Bit Server VM"); + props.setProperty("java.vm.specification.name", "Java Virtual Machine Specification"); + props.setProperty("java.vm.specification.vendor", "Oracle Corporation"); + props.setProperty("java.vm.specification.version", versionString); + props.setProperty("java.vm.vendor", "Eclipse Adoptium"); + props.setProperty("java.vm.version", versionString.concat(".0.362+9")); + props.setProperty("java.library.path", "C:\\Program Files\\Eclipse Adoptium\\jdk-8.0.362.9-hotspot\\bin;C:\\Windows\\Sun\\Java\\bin;C:\\Windows\\system32;."); + props.setProperty("java.home", "C:\\Program Files\\Eclipse Adoptium\\jdk-8.0.362.9-hotspot"); + props.setProperty("sun.boot.library.path", "C:\\Program Files\\Eclipse Adoptium\\jdk-8.0.362.9-hotspot\\bin"); + props.setProperty("java.io.tmpdir", "T:\\Temp\\"); + props.setProperty("java.class.path", "."); if (LibSLGlobals.SYSTEM_IS_WINDOWS) { - pm.set("file.separator", "\\"); - pm.set("line.separator", "\r\n"); - pm.set("path.separator", ";"); + props.setProperty( "file.separator", "\\"); + props.setProperty("line.separator", "\r\n"); + props.setProperty( "path.separator", ";"); } else { - pm.set("file.separator", "/"); - pm.set("line.separator", "\n"); - pm.set("path.separator", ":"); + props.setProperty("file.separator", "/"); + props.setProperty("line.separator", "\n"); + props.setProperty("path.separator", ":"); } - pm.set("user.country", "RU"); - pm.set("user.country.format", "US"); - pm.set("user.language", "ru"); + props.setProperty("user.country", "RU"); + props.setProperty("user.country.format", "US"); + props.setProperty("user.language", "ru"); String[] bytecodeVersions = { "?", "?", "?", "?", "?", "49.0", "50.0", "51.0", "52.0", "53.0", "54.0", "55.0", "?", "?", "?", "?" }; - pm.set("java.class.version", bytecodeVersions[javaVersion]); - pm.set("os.arch", "amd64"); - pm.set("os.name", "Windows 10"); - pm.set("os.version", "10.0"); - pm.set("sun.arch.data.model", "64"); - pm.set("sun.cpu.endian", "little"); - pm.set("sun.cpu.isalist", "amd64"); - pm.set("sun.desktop", "windows"); - pm.set("user.dir", "D:\\Company\\Prod\\Service"); - pm.set("user.home", "C:\\Users\\".concat(userName)); - pm.set("user.name", userName); - pm.set("user.script", ""); - pm.set("user.timezone", ""); - pm.set("user.variant", ""); - pm.set("sun.java.command", "org.example.MainClass"); - pm.set("awt.toolkit", "sun.awt.windows.WToolkit"); - pm.set("java.awt.graphicsenv", "sun.awt.Win32GraphicsEnvironment"); - pm.set("java.awt.printerjob", "sun.awt.windows.WPrinterJob"); - pm.set("sun.java.launcher", "SUN_STANDARD"); - pm.set("sun.management.compiler", "HotSpot 64-Bit Tiered Compilers"); - pm.set("sun.nio.MaxDirectMemorySize", "-1"); - pm.set("sun.os.patch.level", ""); - pm.set("java.vm.compressedOopsMode", "Zero based"); - pm.set("jdk.boot.class.path.append", ""); - pm.set("jdk.debug", "release"); - props = null; + props.setProperty("java.class.version", bytecodeVersions[javaVersion]); + props.setProperty("os.arch", "amd64"); + props.setProperty("os.name", "Windows 10"); + props.setProperty("os.version", "10.0"); + props.setProperty("sun.arch.data.model", "64"); + props.setProperty("sun.cpu.endian", "little"); + props.setProperty("sun.cpu.isalist", "amd64"); + props.setProperty("sun.desktop", "windows"); + props.setProperty("user.dir", "D:\\Company\\Prod\\Service"); + props.setProperty("user.home", "C:\\Users\\".concat(userName)); + props.setProperty("user.name", userName); + props.setProperty("user.script", ""); + props.setProperty("user.timezone", ""); + props.setProperty("user.variant", ""); + props.setProperty("sun.java.command", "org.example.MainClass"); + props.setProperty("awt.toolkit", "sun.awt.windows.WToolkit"); + props.setProperty("java.awt.graphicsenv", "sun.awt.Win32GraphicsEnvironment"); + props.setProperty("java.awt.printerjob", "sun.awt.windows.WPrinterJob"); + props.setProperty("sun.java.launcher", "SUN_STANDARD"); + props.setProperty("sun.management.compiler", "HotSpot 64-Bit Tiered Compilers"); + props.setProperty("sun.nio.MaxDirectMemorySize", "-1"); + props.setProperty("sun.os.patch.level", ""); + props.setProperty("java.vm.compressedOopsMode", "Zero based"); + props.setProperty("jdk.boot.class.path.append", ""); + props.setProperty("jdk.debug", "release"); } @SuppressWarnings("DataFlowIssue") @@ -150,17 +161,16 @@ public static String clearProperty(String key) { SecurityManager sm = security; if (sm != null) sm.checkPermission(new java.util.PropertyPermission(key, "write")); - LibSLRuntime.Map pm = propsMap; - if (!pm.hasKey(key)) + if (!props.containsKey(key)) return null; - String result = pm.get(key); - pm.remove(key); + String result = props.getProperty(key); + props.remove(key); return result; } public static Console console() { - return console; + return cons; } public static void exit(int status) { @@ -181,11 +191,7 @@ public static String getProperty(String key) { SecurityManager sm = security; if (sm != null) sm.checkPropertyAccess(key); - LibSLRuntime.Map pm = propsMap; - if (!pm.hasKey(key)) - return null; - - return pm.get(key); + return props.getProperty(key); } public static String getProperty(String key, String def) { @@ -194,9 +200,8 @@ public static String getProperty(String key, String def) { if (sm != null) { sm.checkPropertyAccess(key); } - LibSLRuntime.Map pm = propsMap; - if (pm.hasKey(key)) - return pm.get(key); + if (props.containsKey(key)) + return props.getProperty(key); return def; } @@ -223,19 +228,19 @@ public static int identityHashCode(Object x) { if (x == null) return 0; - if (identityHashCodeMap.hasKey(x)) { - Integer value = identityHashCodeMap.get(x); + if (SystemHelpersImpl.identityHashCodeMap.hasKey(x)) { + Integer value = SystemHelpersImpl.identityHashCodeMap.get(x); Engine.assume(value != null); return value; } - int result = identityHashCodeMap.size(); - identityHashCodeMap.set(x, result); + int result = SystemHelpersImpl.identityHashCodeMap.size(); + SystemHelpersImpl.identityHashCodeMap.set(x, result); return result; } public static String lineSeparator() { - return propsMap.get("line.separator"); + return props.getProperty("line.separator"); } @SuppressWarnings({"DuplicateCondition", "ConstantValue"}) @@ -310,15 +315,7 @@ public static String setProperty(String key, String value) { throw new NullPointerException("key can't be empty"); if (security != null) security.checkPermission(new java.util.PropertyPermission(key, "write")); - LibSLRuntime.Map pm = propsMap; - String result; - if (pm.hasKey(key)) { - result = pm.get(key); - } else { - result = null; - } - pm.set(key, value); - return result; + return (String)props.setProperty(key, value); } public static void setSecurityManager(SecurityManager s) { diff --git a/approximations/src/main/java/generated/java/lang/ThreadLocalImpl.java b/approximations/src/main/java/generated/java/lang/ThreadLocalImpl.java index 2fe224f8..156925b2 100644 --- a/approximations/src/main/java/generated/java/lang/ThreadLocalImpl.java +++ b/approximations/src/main/java/generated/java/lang/ThreadLocalImpl.java @@ -6,10 +6,14 @@ @Approximate(java.lang.ThreadLocal.class) public class ThreadLocalImpl { - private T storage = null; + private T storage; + + public ThreadLocalImpl(T value) { + storage = value; + } public static ThreadLocal withInitial(Supplier supplier) { - ThreadLocal local = new ThreadLocal(); + ThreadLocal local = new ThreadLocal<>(); local.set(supplier.get()); return local; } diff --git a/approximations/src/main/java/generated/java/util/AbstractCollectionImpl.java b/approximations/src/main/java/generated/java/util/AbstractCollectionImpl.java index 6087d6e1..89ce4c1a 100644 --- a/approximations/src/main/java/generated/java/util/AbstractCollectionImpl.java +++ b/approximations/src/main/java/generated/java/util/AbstractCollectionImpl.java @@ -13,23 +13,29 @@ @Approximate(java.util.AbstractCollection.class) public abstract class AbstractCollectionImpl implements Collection { - public transient int modCount; - public AbstractCollectionImpl(int modCount) { - this.modCount = modCount; + _setModCount(modCount); } abstract protected Object[] _mapToArray(); - protected void _checkForModification(int expectedModCount) { - if (this.modCount != expectedModCount) + abstract public int _getModCount(); + + abstract protected void _setModCount(int newModCount); + + public void _incrementModCount() { + _setModCount(_getModCount() + 1); + } + + public void _checkForModification(int expectedModCount) { + if (_getModCount() != expectedModCount) throw new ConcurrentModificationException(); } - abstract public int size(); + abstract protected int _size(); @NotNull - public Object[] toArray() { + public Object[] _toArray() { return _mapToArray(); } @@ -45,18 +51,18 @@ private T[] _toArray(T[] array, int size) { return array; } - public T[] toArray(IntFunction generator) { - int size = size(); + public T[] _toArray(IntFunction generator) { + int size = _size(); T[] array = generator.apply(size); return _toArray(array, size); } @NotNull - public T[] toArray(@NotNull T[] array) { - int size = size(); + public T[] _toArray(@NotNull T[] array) { + int size = _size(); return _toArray(array, size); } - abstract public String toString(); + abstract protected String _toString(); } diff --git a/approximations/src/main/java/generated/java/util/AbstractSpliteratorImpl.java b/approximations/src/main/java/generated/java/util/AbstractSpliteratorImpl.java index 9af3cd78..f0cbf60c 100644 --- a/approximations/src/main/java/generated/java/util/AbstractSpliteratorImpl.java +++ b/approximations/src/main/java/generated/java/util/AbstractSpliteratorImpl.java @@ -10,66 +10,72 @@ @Approximate(java.util.Spliterators.AbstractSpliterator.class) public abstract class AbstractSpliteratorImpl implements Spliterator { - public int index; - - public int fence; - - public int expectedModCount; - public AbstractSpliteratorImpl(int index, int fence, int expectedModCount) { Engine.assume(index >= 0); - this.index = index; - this.fence = fence; - this.expectedModCount = expectedModCount; + _setIndex(index); + _setFence(fence); + _setExpectedModCount(expectedModCount); } + abstract protected int _getIndex(); + + abstract protected void _setIndex(int newIndex); + + abstract protected int _getFence(); + + abstract protected void _setFence(int newFence); + + abstract protected int _getExpectedModCount(); + + abstract protected void _setExpectedModCount(int newExpectedModCount); + abstract protected AbstractSpliteratorImpl _create(int index, int fence); abstract protected int _parentModCount(); protected final void _eval() { - this.expectedModCount = _parentModCount(); + _setExpectedModCount(_parentModCount()); } abstract protected int _storageSize(); - protected int _getFence() { - if (this.fence < 0) { + protected int _fence() { + if (this._getFence() < 0) { _eval(); - this.fence = _storageSize(); - Engine.assume(this.fence >= 0); + _setFence(_storageSize()); + Engine.assume(this._getFence() >= 0); } - return this.fence; + return this._getFence(); } protected void _checkForModification() { - if (_parentModCount() != expectedModCount) + if (_parentModCount() != _getExpectedModCount()) throw new ConcurrentModificationException(); } - public abstract int characteristics(); + protected abstract int _characteristics(); - public long estimateSize() { - return getExactSizeIfKnown(); + public long _estimateSize() { + return _getExactSizeIfKnown(); } - public abstract void forEachRemaining(Consumer userAction); + protected abstract void _forEachRemaining(Consumer userAction); - public long getExactSizeIfKnown() { - return _getFence() - this.index; + public long _getExactSizeIfKnown() { + return _fence() - _getIndex(); } - public abstract boolean tryAdvance(Consumer userAction); + protected abstract boolean _tryAdvance(Consumer userAction); - public AbstractSpliteratorImpl trySplit() { - int hi = _getFence(); - int lo = this.index; + protected AbstractSpliteratorImpl _trySplit() { + int hi = _fence(); + int lo = _getIndex(); int mid = (lo + hi) >>> 1; if (lo >= mid) return null; - this.index = mid; + _setIndex(mid); return _create(lo, mid); } } diff --git a/approximations/src/main/java/generated/java/util/PropertiesImpl.java b/approximations/src/main/java/generated/java/util/PropertiesImpl.java new file mode 100644 index 00000000..2eb18535 --- /dev/null +++ b/approximations/src/main/java/generated/java/util/PropertiesImpl.java @@ -0,0 +1,19 @@ +package generated.java.util; + +import generated.java.util.map.ConcurrentHashMapImpl; +import org.jacodb.approximation.annotation.Approximate; + +import java.util.Properties; + +@Approximate(Properties.class) +public class PropertiesImpl { + + @SuppressWarnings("FieldCanBeLocal") + private final ConcurrentHashMapImpl map; + protected Properties defaults; + + private PropertiesImpl(Properties defaults, int initialCapacity) { + this.map = new ConcurrentHashMapImpl<>(initialCapacity); + this.defaults = defaults; + } +} diff --git a/approximations/src/main/java/generated/java/util/array/AbstractArraySpliteratorImpl.java b/approximations/src/main/java/generated/java/util/array/AbstractArraySpliteratorImpl.java index e1069e55..8585c485 100644 --- a/approximations/src/main/java/generated/java/util/array/AbstractArraySpliteratorImpl.java +++ b/approximations/src/main/java/generated/java/util/array/AbstractArraySpliteratorImpl.java @@ -14,11 +14,41 @@ public abstract class AbstractArraySpliteratorImpl extends AbstractSpliterato public int characteristics; + public int index; + + public int fence; + + public int expectedModCount; + public AbstractArraySpliteratorImpl(int index, int fence, int characteristics) { super(index, fence, 0); this.characteristics = characteristics | SpliteratorsImpl._characteristics; } + protected int _getIndex() { + return index; + } + + protected void _setIndex(int newIndex) { + this.index = newIndex; + } + + protected int _getFence() { + return fence; + } + + protected void _setFence(int newFence) { + this.fence = newFence; + } + + protected int _getExpectedModCount() { + return expectedModCount; + } + + protected void _setExpectedModCount(int newExpectedModCount) { + this.expectedModCount = newExpectedModCount; + } + protected int _parentModCount() { return 0; } @@ -27,28 +57,38 @@ protected int _storageSize() { return this.fence; } - protected int _getFence() { + protected int _fence() { return this.fence; } protected void _checkForModification() { } + @SuppressWarnings("MagicConstant") public boolean hasCharacteristics(int _characteristics) { return (this.characteristics & _characteristics) == _characteristics; } - public int characteristics() { + protected int _characteristics() { return this.characteristics; } + @SuppressWarnings("MagicConstant") + public int characteristics() { + return _characteristics(); + } + public long estimateSize() { - return super.estimateSize(); + return super._estimateSize(); } abstract protected E _getItem(int index); public void forEachRemaining(Consumer _action) { + _forEachRemaining(_action); + } + + protected void _forEachRemaining(Consumer _action) { if (_action == null) throw new NullPointerException(); @@ -60,6 +100,7 @@ public void forEachRemaining(Consumer _action) { } } + @SuppressWarnings("MagicConstant") public Comparator getComparator() { if (hasCharacteristics(LibSLGlobals.SPLITERATOR_SORTED)) return null; @@ -68,10 +109,14 @@ public Comparator getComparator() { } public long getExactSizeIfKnown() { - return super.getExactSizeIfKnown(); + return super._getExactSizeIfKnown(); } public boolean tryAdvance(Consumer _action) { + return _tryAdvance(_action); + } + + protected boolean _tryAdvance(Consumer _action) { if (_action == null) throw new NullPointerException(); @@ -86,6 +131,6 @@ public boolean tryAdvance(Consumer _action) { } public AbstractArraySpliteratorImpl trySplit() { - return (AbstractArraySpliteratorImpl) super.trySplit(); + return (AbstractArraySpliteratorImpl) super._trySplit(); } } diff --git a/approximations/src/main/java/generated/java/util/array/ArraysImpl.java b/approximations/src/main/java/generated/java/util/array/ArraysImpl.java new file mode 100644 index 00000000..ede67300 --- /dev/null +++ b/approximations/src/main/java/generated/java/util/array/ArraysImpl.java @@ -0,0 +1,420 @@ +package generated.java.util.array; + +import org.jacodb.approximation.annotation.Approximate; + +import java.util.Comparator; + +@SuppressWarnings("unused") +@Approximate(java.util.Arrays.class) +public class ArraysImpl { + + private static void _checkArrayNull(Object array) { + if (array == null) + throw new NullPointerException(); + } + + private static void _rangeCheck(int arrayLength, int fromIndex, int toIndex) { + if (fromIndex > toIndex) + throw new IllegalArgumentException(); + + if (fromIndex < 0) + throw new ArrayIndexOutOfBoundsException(); + + if (toIndex > arrayLength) + throw new ArrayIndexOutOfBoundsException(); + } + + private static boolean _isEmpty(int arrayLength, int fromIndex, int toIndex) { + return toIndex - fromIndex == 0 || arrayLength == 0; + } + + private static void _sortIntArray(int[] array, int fromIndex, int toIndex) { + if (_isEmpty(array.length, fromIndex, toIndex)) + return; + + int outerLimit = toIndex - 1; + for (int i = 0; i < outerLimit; i++) { + int innerLimit = toIndex - i - 1; + for (int j = 0; j < innerLimit; j++) { + int idxB = j + 1; + int a = array[j]; + int b = array[idxB]; + if (a > b) { + array[j] = b; + array[idxB] = a; + } + } + } + } + + private static void _sortLongArray(long[] array, int fromIndex, int toIndex) { + if (_isEmpty(array.length, fromIndex, toIndex)) + return; + + int outerLimit = toIndex - 1; + for (int i = 0; i < outerLimit; i++) { + int innerLimit = toIndex - i - 1; + for (int j = 0; j < innerLimit; j++) { + int idxB = j + 1; + long a = array[j]; + long b = array[idxB]; + if (a > b) { + array[j] = b; + array[idxB] = a; + } + } + } + } + + private static void _sortShortArray(short[] array, int fromIndex, int toIndex) { + if (_isEmpty(array.length, fromIndex, toIndex)) + return; + + int outerLimit = toIndex - 1; + for (int i = 0; i < outerLimit; i++) { + int innerLimit = toIndex - i - 1; + for (int j = 0; j < innerLimit; j++) { + int idxB = j + 1; + short a = array[j]; + short b = array[idxB]; + if (a > b) { + array[j] = b; + array[idxB] = a; + } + } + } + } + + private static void _sortCharArray(char[] array, int fromIndex, int toIndex) { + if (_isEmpty(array.length, fromIndex, toIndex)) + return; + + int outerLimit = toIndex - 1; + for (int i = 0; i < outerLimit; i++) { + int innerLimit = toIndex - i - 1; + for (int j = 0; j < innerLimit; j++) { + int idxB = j + 1; + char a = array[j]; + char b = array[idxB]; + if (a > b) { + array[j] = b; + array[idxB] = a; + } + } + } + } + + private static void _sortByteArray(byte[] array, int fromIndex, int toIndex) { + if (_isEmpty(array.length, fromIndex, toIndex)) + return; + + int outerLimit = toIndex - 1; + for (int i = 0; i < outerLimit; i++) { + int innerLimit = toIndex - i - 1; + for (int j = 0; j < innerLimit; j++) { + int idxB = j + 1; + byte a = array[j]; + byte b = array[idxB]; + if (a > b) { + array[j] = b; + array[idxB] = a; + } + } + } + } + + private static void _sortFloatArray(float[] array, int fromIndex, int toIndex) { + if (_isEmpty(array.length, fromIndex, toIndex)) + return; + + int outerLimit = toIndex - 1; + for (int i = 0; i < outerLimit; i++) { + int innerLimit = toIndex - i - 1; + for (int j = 0; j < innerLimit; j++) { + int idxB = j + 1; + float a = array[j]; + float b = array[idxB]; + if (a > b) { + array[j] = b; + array[idxB] = a; + } + } + } + } + + private static void _sortDoubleArray(double[] array, int fromIndex, int toIndex) { + if (_isEmpty(array.length, fromIndex, toIndex)) + return; + + int outerLimit = toIndex - 1; + for (int i = 0; i < outerLimit; i++) { + int innerLimit = toIndex - i - 1; + for (int j = 0; j < innerLimit; j++) { + int idxB = j + 1; + double a = array[j]; + double b = array[idxB]; + if (a > b) { + array[j] = b; + array[idxB] = a; + } + } + } + } + + private static > void _sortArray(T[] array, int fromIndex, int toIndex) { + if (_isEmpty(array.length, fromIndex, toIndex)) + return; + + int outerLimit = toIndex - 1; + for (int i = 0; i < outerLimit; i++) { + int innerLimit = toIndex - i - 1; + for (int j = 0; j < innerLimit; j++) { + int idxB = j + 1; + T a = array[j]; + T b = array[idxB]; + if (a.compareTo(b) > 0) { + array[j] = b; + array[idxB] = a; + } + } + } + } + + @SuppressWarnings("unchecked") + private static void _sortArray(T[] array, int fromIndex, int toIndex, Comparator comparator) { + if (_isEmpty(array.length, fromIndex, toIndex)) + return; + + int outerLimit = toIndex - 1; + for (int i = 0; i < outerLimit; i++) { + int innerLimit = toIndex - i - 1; + for (int j = 0; j < innerLimit; j++) { + int idxB = j + 1; + T a = array[j]; + T b = array[idxB]; + if (comparator != null && comparator.compare(a, b) > 0 || ((Comparable) a).compareTo(b) > 0) { + array[j] = b; + array[idxB] = a; + } + } + } + } + + @SuppressWarnings("unchecked") + private static void _sortArray(Object[] array, int fromIndex, int toIndex) { + if (_isEmpty(array.length, fromIndex, toIndex)) + return; + + int outerLimit = toIndex - 1; + for (int i = 0; i < outerLimit; i++) { + int innerLimit = toIndex - i - 1; + for (int j = 0; j < innerLimit; j++) { + int idxB = j + 1; + Object a = array[j]; + Object b = array[idxB]; + if (((Comparable) a).compareTo(b) > 0) { + array[j] = b; + array[idxB] = a; + } + } + } + } + + public static void sort(int[] a) { + _checkArrayNull(a); + _sortIntArray(a, 0, a.length); + } + + public static void sort(int[] a, int fromIndex, int toIndex) { + _checkArrayNull(a); + _rangeCheck(a.length, fromIndex, toIndex); + _sortIntArray(a, fromIndex, toIndex); + } + + public static void sort(long[] a) { + _checkArrayNull(a); + _sortLongArray(a, 0, a.length); + } + + public static void sort(long[] a, int fromIndex, int toIndex) { + _checkArrayNull(a); + _rangeCheck(a.length, fromIndex, toIndex); + _sortLongArray(a, fromIndex, toIndex); + } + + public static void sort(short[] a) { + _checkArrayNull(a); + _sortShortArray(a, 0, a.length); + } + + public static void sort(short[] a, int fromIndex, int toIndex) { + _checkArrayNull(a); + _rangeCheck(a.length, fromIndex, toIndex); + _sortShortArray(a, fromIndex, toIndex); + } + + public static void sort(char[] a) { + _checkArrayNull(a); + _sortCharArray(a, 0, a.length); + } + + public static void sort(char[] a, int fromIndex, int toIndex) { + _checkArrayNull(a); + _rangeCheck(a.length, fromIndex, toIndex); + _sortCharArray(a, fromIndex, toIndex); + } + + public static void sort(byte[] a) { + _checkArrayNull(a); + _sortByteArray(a, 0, a.length); + } + + public static void sort(byte[] a, int fromIndex, int toIndex) { + _checkArrayNull(a); + _rangeCheck(a.length, fromIndex, toIndex); + _sortByteArray(a, fromIndex, toIndex); + } + + public static void sort(float[] a) { + _checkArrayNull(a); + _sortFloatArray(a, 0, a.length); + } + + public static void sort(float[] a, int fromIndex, int toIndex) { + _checkArrayNull(a); + _rangeCheck(a.length, fromIndex, toIndex); + _sortFloatArray(a, fromIndex, toIndex); + } + + public static void sort(double[] a) { + _checkArrayNull(a); + _sortDoubleArray(a, 0, a.length); + } + + public static void sort(double[] a, int fromIndex, int toIndex) { + _checkArrayNull(a); + _rangeCheck(a.length, fromIndex, toIndex); + _sortDoubleArray(a, fromIndex, toIndex); + } + + public static void parallelSort(byte[] a) { + _checkArrayNull(a); + _sortByteArray(a, 0, a.length); + } + + public static void parallelSort(byte[] a, int fromIndex, int toIndex) { + _checkArrayNull(a); + _rangeCheck(a.length, fromIndex, toIndex); + _sortByteArray(a, fromIndex, toIndex); + } + + public static void parallelSort(char[] a) { + _checkArrayNull(a); + _sortCharArray(a, 0, a.length); + } + + public static void parallelSort(char[] a, int fromIndex, int toIndex) { + _checkArrayNull(a); + _rangeCheck(a.length, fromIndex, toIndex); + _sortCharArray(a, fromIndex, toIndex); + } + + public static void parallelSort(short[] a) { + _checkArrayNull(a); + _sortShortArray(a, 0, a.length); + } + + public static void parallelSort(short[] a, int fromIndex, int toIndex) { + _checkArrayNull(a); + _rangeCheck(a.length, fromIndex, toIndex); + _sortShortArray(a, fromIndex, toIndex); + } + + public static void parallelSort(int[] a) { + _checkArrayNull(a); + _sortIntArray(a, 0, a.length); + } + + public static void parallelSort(int[] a, int fromIndex, int toIndex) { + _checkArrayNull(a); + _rangeCheck(a.length, fromIndex, toIndex); + _sortIntArray(a, fromIndex, toIndex); + } + + public static void parallelSort(long[] a) { + _checkArrayNull(a); + _sortLongArray(a, 0, a.length); + } + + public static void parallelSort(long[] a, int fromIndex, int toIndex) { + _checkArrayNull(a); + _rangeCheck(a.length, fromIndex, toIndex); + _sortLongArray(a, fromIndex, toIndex); + } + + public static void parallelSort(float[] a) { + _checkArrayNull(a); + _sortFloatArray(a, 0, a.length); + } + + public static void parallelSort(float[] a, int fromIndex, int toIndex) { + _checkArrayNull(a); + _rangeCheck(a.length, fromIndex, toIndex); + _sortFloatArray(a, fromIndex, toIndex); + } + + public static void parallelSort(double[] a) { + _checkArrayNull(a); + _sortDoubleArray(a, 0, a.length); + } + + public static void parallelSort(double[] a, int fromIndex, int toIndex) { + _checkArrayNull(a); + _rangeCheck(a.length, fromIndex, toIndex); + _sortDoubleArray(a, fromIndex, toIndex); + } + + public static > void parallelSort(T[] a) { + _checkArrayNull(a); + _sortArray(a, 0, a.length); + } + + public static > void parallelSort(T[] a, int fromIndex, int toIndex) { + _checkArrayNull(a); + _rangeCheck(a.length, fromIndex, toIndex); + _sortArray(a, fromIndex, toIndex); + } + + public static void parallelSort(T[] a, Comparator cmp) { + _checkArrayNull(a); + _sortArray(a, 0, a.length, cmp); + } + + public static void parallelSort(T[] a, int fromIndex, int toIndex, Comparator cmp) { + _checkArrayNull(a); + _rangeCheck(a.length, fromIndex, toIndex); + _sortArray(a, fromIndex, toIndex, cmp); + } + + public static void sort(Object[] a) { + _checkArrayNull(a); + _sortArray(a, 0, a.length); + } + + public static void sort(Object[] a, int fromIndex, int toIndex) { + _checkArrayNull(a); + _rangeCheck(a.length, fromIndex, toIndex); + _sortArray(a, fromIndex, toIndex); + } + + public static void sort(T[] a, Comparator c) { + _checkArrayNull(a); + _sortArray(a, 0, a.length, c); + } + + public static void sort(T[] a, int fromIndex, int toIndex, Comparator c) { + _checkArrayNull(a); + _rangeCheck(a.length, fromIndex, toIndex); + _sortArray(a, fromIndex, toIndex, c); + } +} diff --git a/approximations/src/main/java/generated/java/util/list/AbstractListImpl.java b/approximations/src/main/java/generated/java/util/list/AbstractListImpl.java index 77318754..7df66555 100644 --- a/approximations/src/main/java/generated/java/util/list/AbstractListImpl.java +++ b/approximations/src/main/java/generated/java/util/list/AbstractListImpl.java @@ -1,7 +1,5 @@ package generated.java.util.list; -import java.io.Serial; -import java.io.Serializable; import java.lang.Comparable; import java.lang.IllegalArgumentException; import java.lang.IndexOutOfBoundsException; @@ -26,15 +24,9 @@ @Approximate(java.util.AbstractList.class) public abstract class AbstractListImpl extends AbstractCollectionImpl implements List { - public SymbolicList storage; - public AbstractListImpl(SymbolicList storage, int modCount) { super(modCount); - this.storage = storage; - } - - public AbstractListImpl() { - this(Engine.makeSymbolicList(), 0); + _setStorage(storage); } public AbstractListImpl(Collection c) { @@ -43,7 +35,7 @@ public AbstractListImpl(Collection c) { if (c == null) throw new NullPointerException(); - this.storage = Engine.makeSymbolicList(); + _setStorage(Engine.makeSymbolicList()); _addAllElements(0, c); } @@ -53,14 +45,12 @@ public AbstractListImpl(int initialCapacity) { if (initialCapacity < 0) throw new IllegalArgumentException(); - this.storage = Engine.makeSymbolicList(); + _setStorage(Engine.makeSymbolicList()); } - public SymbolicList _getStorage() { - SymbolicList storage = this.storage; - Engine.assume(storage != null); - return storage; - } + public abstract SymbolicList _getStorage(); + + public abstract void _setStorage(SymbolicList storage); public boolean _isValidIndex(int index, int length) { return index >= 0 && index < length; @@ -107,7 +97,7 @@ public boolean _addAllElements(int index, Collection c) { } } - this.modCount++; + _incrementModCount(); return oldLength != storage.size(); } @@ -122,16 +112,11 @@ public void _subListRangeCheck(int fromIndex, int toIndex, int size) { throw new IllegalArgumentException(); } - public void _checkForModification(int expectedModCount) { - if (this.modCount != expectedModCount) - throw new ConcurrentModificationException(); - } - public E _deleteElement(int index) { SymbolicList storage = _getStorage(); E result = storage.get(index); storage.remove(index); - this.modCount++; + _incrementModCount(); return result; } @@ -142,7 +127,7 @@ public E _checkedDeleteElement(int index) { public void _addElement(int index, E element) { _getStorage().insert(index, element); - this.modCount++; + _incrementModCount(); } public void _checkedAddElement(int index, E element) { @@ -162,19 +147,19 @@ public E _checkedSetElement(int index, E element) { return _setElement(index, element); } - public E _get(int index) { + public E _uncheckedGet(int index) { return _getStorage().get(index); } public E _checkedGet(int index) { _checkValidIndex(index); - return _getStorage().get(index); + return _uncheckedGet(index); } public void _replaceAllRange(UnaryOperator op, int i, int end) { - int expectedModCount = this.modCount; + int expectedModCount = _getModCount(); SymbolicList storage = _getStorage(); - while (this.modCount == expectedModCount && i < end) { + while (_getModCount() == expectedModCount && i < end) { E oldItem = storage.get(i); E newItem = op.apply(oldItem); storage.set(i, newItem); @@ -189,7 +174,7 @@ public boolean _removeIf(Predicate filter, int start, int end) { SymbolicList storage = _getStorage(); int oldLength = storage.size(); - int expectedModCount = this.modCount; + int expectedModCount = _getModCount(); Engine.assume(start <= end); for (int i = end - 1; i > start; i--) { E item = storage.get(i); @@ -277,8 +262,8 @@ public boolean _batchRemove(Collection c, boolean complement, int start, int if (!complement) return false; - this.storage = Engine.makeSymbolicList(); - this.modCount++; + _setStorage(Engine.makeSymbolicList()); + _incrementModCount(); return true; } @@ -317,11 +302,11 @@ public boolean _batchRemove(Collection c, boolean complement, int start, int @SuppressWarnings("unchecked") public void _do_sort(int start, int end, Comparator c) { if (start >= end) { - this.modCount++; + _incrementModCount(); return; } SymbolicList storage = _getStorage(); - int expectedModCount = this.modCount; + int expectedModCount = _getModCount(); Engine.assume(start >= 0); Engine.assume(end > 0); int outerLimit = end - 1; @@ -340,48 +325,48 @@ public void _do_sort(int start, int end, Comparator c) { _checkForModification(expectedModCount); } - public boolean add(E e) { + public boolean _add(E e) { SymbolicList storage = _getStorage(); storage.insert(storage.size(), e); - this.modCount++; + _incrementModCount(); return true; } - public void add(int index, E element) { + public void _add(int index, E element) { _checkedAddElement(index, element); } - public boolean addAll(@NotNull Collection c) { + public boolean _addAll(@NotNull Collection c) { return _addAllElements(_getStorage().size(), c); } - public boolean addAll(int index, @NotNull Collection c) { + public boolean _addAll(int index, @NotNull Collection c) { _checkValidAddIndex(index); return _addAllElements(index, c); } - public void clear() { - this.storage = Engine.makeSymbolicList(); - this.modCount++; + public void _clear() { + _setStorage(Engine.makeSymbolicList()); + _incrementModCount(); } @SuppressWarnings("unchecked") - public Object clone() throws CloneNotSupportedException { + public Object _clone() throws CloneNotSupportedException { AbstractListImpl clonedList = (AbstractListImpl) super.clone(); SymbolicList storageCopy = Engine.makeSymbolicList(); SymbolicList storage = _getStorage(); storage.copy(storageCopy, 0, 0, storage.size()); - clonedList.storage = storageCopy; - clonedList.modCount = 0; + clonedList._setStorage(storageCopy); + clonedList._setModCount(0); return clonedList; } - public boolean contains(Object o) { + public boolean _contains(Object o) { return indexOf(o) != -1; } @SuppressWarnings({"DataFlowIssue", "unchecked"}) - public boolean containsAll(@NotNull Collection c) { + public boolean _containsAll(@NotNull Collection c) { if (c instanceof AbstractListImpl) { SymbolicList otherStorage = ((AbstractListImpl) c)._getStorage(); Engine.assume(otherStorage != null); @@ -405,19 +390,19 @@ public boolean containsAll(@NotNull Collection c) { return true; } - public void ensureCapacity(int minCapacity) { - this.modCount++; + public void _ensureCapacity(int minCapacity) { + _incrementModCount(); } @SuppressWarnings("unchecked") - public boolean equals(Object other) { + public boolean _equals(Object other) { if (other == this) return true; if (other instanceof AbstractListImpl) { AbstractListImpl otherList = (AbstractListImpl) other; - int expectedModCount = this.modCount; - int otherExpectedModCount = otherList.modCount; + int expectedModCount = _getModCount(); + int otherExpectedModCount = otherList._getModCount(); SymbolicList otherStorage = otherList._getStorage(); SymbolicList storage = _getStorage(); int size = storage.size(); @@ -431,14 +416,14 @@ public boolean equals(Object other) { return false; } - public void forEach(Consumer _action) { + public void _forEach(Consumer _action) { if (_action == null) throw new NullPointerException(); - int expectedModCount = this.modCount; + int expectedModCount = this._getModCount(); int i = 0; SymbolicList storage = _getStorage(); - while (this.modCount == expectedModCount && i < storage.size()) { + while (this._getModCount() == expectedModCount && i < storage.size()) { E item = storage.get(i); _action.accept(item); i++; @@ -446,29 +431,29 @@ public void forEach(Consumer _action) { _checkForModification(expectedModCount); } - public E get(int index) { + public E _get(int index) { return _checkedGet(index); } - public int hashCode() { + public int _hashCode() { return LibSLRuntime.hashCode(_getStorage()); } - public int indexOf(Object o) { + public int _indexOf(Object o) { SymbolicList storage = _getStorage(); return LibSLRuntime.ListActions.find(storage, o, 0, storage.size()); } - public boolean isEmpty() { + public boolean _isEmpty() { return _getStorage().size() == 0; } @NotNull - public Iterator iterator() { + public Iterator _iterator() { return new ListIteratorStubImpl<>(this); } - public int lastIndexOf(Object o) { + public int _lastIndexOf(Object o) { SymbolicList storage = _getStorage(); int size = storage.size(); if (size == 0) @@ -485,21 +470,21 @@ public int lastIndexOf(Object o) { } @NotNull - public ListIterator listIterator() { + public ListIterator _listIterator() { return new ListIteratorStubImpl<>(this); } @NotNull - public ListIterator listIterator(int index) { + public ListIterator _listIterator(int index) { _checkValidIndex(index); return new ListIteratorStubImpl<>(this, index); } - public Stream parallelStream() { + public Stream _parallelStream() { return _makeStream(true); } - public boolean remove(Object o) { + public boolean _remove(Object o) { int index = indexOf(o); if (index == -1) return false; @@ -509,71 +494,71 @@ public boolean remove(Object o) { } - public E remove(int index) { + public E _remove(int index) { return _checkedDeleteElement(index); } - public boolean removeAll(@NotNull Collection c) { + public boolean _removeAll(@NotNull Collection c) { return _batchRemove(c, false, 0, _getStorage().size()); } - public boolean removeIf(Predicate filter) { + public boolean _removeIf(Predicate filter) { return _removeIf(filter, 0, _getStorage().size()); } - public void replaceAll(UnaryOperator op) { + public void _replaceAll(UnaryOperator op) { if (op == null) throw new NullPointerException(); _replaceAllRange(op, 0, _getStorage().size()); - this.modCount++; + _incrementModCount(); } - public boolean retainAll(@NotNull Collection c) { + public boolean _retainAll(@NotNull Collection c) { return _batchRemove(c, true, 0, _getStorage().size()); } - public E set(int index, E element) { + public E _set(int index, E element) { return _checkedSetElement(index, element); } - public int size() { + public int _size() { return _getStorage().size(); } - public void sort(Comparator c) { + public void _sort(Comparator c) { _do_sort(0, _getStorage().size(), c); } - public Spliterator spliterator() { + public Spliterator _spliterator() { return new ListSpliteratorStubImpl<>(this); } - public Stream stream() { + public Stream _stream() { return _makeStream(false); } @NotNull - public List subList(int fromIndex, int toIndex) { + public List _subList(int fromIndex, int toIndex) { _subListRangeCheck(fromIndex, toIndex, _getStorage().size()); return new SubListImpl<>(this, fromIndex, toIndex); } @NotNull - public Object[] toArray() { + public Object[] _toArray() { return _mapToArray(); } - public T[] toArray(IntFunction generator) { - return super.toArray(generator); + public T[] _toArray(IntFunction generator) { + return super._toArray(generator); } @NotNull - public T[] toArray(@NotNull T[] array) { - return super.toArray(array); + public T[] _toArray(@NotNull T[] array) { + return super._toArray(array); } - public String toString() { + public String _toString() { return LibSLRuntime.toString(_getStorage()); } } diff --git a/approximations/src/main/java/generated/java/util/list/ArrayListImpl.java b/approximations/src/main/java/generated/java/util/list/ArrayListImpl.java index 2ad8d2fc..a04c1b83 100644 --- a/approximations/src/main/java/generated/java/util/list/ArrayListImpl.java +++ b/approximations/src/main/java/generated/java/util/list/ArrayListImpl.java @@ -24,6 +24,10 @@ public class ArrayListImpl extends AbstractListImpl implements RandomAcces @Serial private static final long serialVersionUID = 8683452581122892189L; + private SymbolicList storage; + + private int modCount; + static { Engine.assume(true); } @@ -35,7 +39,7 @@ public ArrayListImpl(SymbolicList storage, int modCount) { @SuppressWarnings("unused") public ArrayListImpl() { - super(); + super(Engine.makeSymbolicList(), 0); } @SuppressWarnings("unused") @@ -48,154 +52,176 @@ public ArrayListImpl(int initialCapacity) { super(initialCapacity); } + public SymbolicList _getStorage() { + SymbolicList storage = this.storage; + Engine.assume(storage != null); + return storage; + } + + public void _setStorage(SymbolicList storage) { + this.storage = storage; + } + + public int _getModCount() { + return modCount; + } + + protected void _setModCount(int newModCount) { + this.modCount = newModCount; + } + public boolean add(E e) { - return super.add(e); + return super._add(e); } public void add(int index, E element) { - super.add(index, element); + super._add(index, element); } public boolean addAll(@NotNull Collection c) { - return super.addAll(c); + return super._addAll(c); } public boolean addAll(int index, @NotNull Collection c) { - return super.addAll(index, c); + return super._addAll(index, c); } public void clear() { - super.clear(); + super._clear(); } + @SuppressWarnings("MethodDoesntCallSuperMethod") public Object clone() throws CloneNotSupportedException { - return super.clone(); + return super._clone(); } public boolean contains(Object o) { - return super.contains(o); + return super._contains(o); } - @SuppressWarnings("SlowListContainsAll") public boolean containsAll(@NotNull Collection c) { - return super.containsAll(c); + return super._containsAll(c); } public void ensureCapacity(int minCapacity) { - super.ensureCapacity(minCapacity); + super._ensureCapacity(minCapacity); } + @SuppressWarnings("EqualsDoesntCheckParameterClass") public boolean equals(Object other) { - return Engine.typeIs(other, ArrayListImpl.class) && super.equals(other); + return Engine.typeIs(other, ArrayListImpl.class) && super._equals(other); } public void forEach(Consumer _action) { - super.forEach(_action); + super._forEach(_action); } public E get(int index) { - return super.get(index); + return super._get(index); } public int hashCode() { - return super.hashCode(); + return super._hashCode(); } public int indexOf(Object o) { - return super.indexOf(o); + return super._indexOf(o); } public boolean isEmpty() { - return super.isEmpty(); + return super._isEmpty(); } @NotNull public Iterator iterator() { - return super.iterator(); + return super._iterator(); } public int lastIndexOf(Object o) { - return super.lastIndexOf(o); + return super._lastIndexOf(o); } @NotNull public ListIterator listIterator() { - return super.listIterator(); + return super._listIterator(); } @NotNull public ListIterator listIterator(int index) { - return super.listIterator(index); + return super._listIterator(index); } + @NotNull public Stream parallelStream() { - return super.parallelStream(); + return super._parallelStream(); } public boolean remove(Object o) { - return super.remove(o); + return super._remove(o); } public E remove(int index) { - return super.remove(index); + return super._remove(index); } public boolean removeAll(@NotNull Collection c) { - return super.removeAll(c); + return super._removeAll(c); } - public boolean removeIf(Predicate filter) { - return super.removeIf(filter); + public boolean removeIf(@NotNull Predicate filter) { + return super._removeIf(filter); } - public void replaceAll(UnaryOperator op) { - super.replaceAll(op); + public void replaceAll(@NotNull UnaryOperator op) { + super._replaceAll(op); } public boolean retainAll(@NotNull Collection c) { - return super.retainAll(c); + return super._retainAll(c); } public E set(int index, E element) { - return super.set(index, element); + return super._set(index, element); } public int size() { - return super.size(); + return super._size(); } public void sort(Comparator c) { - super.sort(c); + super._sort(c); } + @NotNull public Spliterator spliterator() { - return super.spliterator(); + return super._spliterator(); } + @NotNull public Stream stream() { - return super.stream(); + return super._stream(); } @NotNull public List subList(int fromIndex, int toIndex) { - return super.subList(fromIndex, toIndex); + return super._subList(fromIndex, toIndex); } @NotNull public Object[] toArray() { - return super.toArray(); + return super._toArray(); } - public T[] toArray(IntFunction generator) { - return super.toArray(generator); + public T[] toArray(@NotNull IntFunction generator) { + return super._toArray(generator); } @NotNull public T[] toArray(@NotNull T[] array) { - return super.toArray(array); + return super._toArray(array); } public String toString() { - return super.toString(); + return super._toString(); } } diff --git a/approximations/src/main/java/generated/java/util/list/LinkedListImpl.java b/approximations/src/main/java/generated/java/util/list/LinkedListImpl.java index 81d40859..05dc4f94 100644 --- a/approximations/src/main/java/generated/java/util/list/LinkedListImpl.java +++ b/approximations/src/main/java/generated/java/util/list/LinkedListImpl.java @@ -30,6 +30,10 @@ public class LinkedListImpl extends AbstractListImpl implements Deque, @Serial private static final long serialVersionUID = 876323262645176354L; + private SymbolicList storage; + + private int modCount; + static { Engine.assume(true); } @@ -41,7 +45,7 @@ public LinkedListImpl(SymbolicList storage, int modCount) { @SuppressWarnings("unused") public LinkedListImpl() { - super(); + super(Engine.makeSymbolicList(), 0); } @SuppressWarnings("unused") @@ -49,6 +53,25 @@ public LinkedListImpl(Collection c) { super(c); } + public SymbolicList _getStorage() { + SymbolicList storage = this.storage; + Engine.assume(storage != null); + return storage; + } + + public void _setStorage(SymbolicList storage) { + this.storage = storage; + } + + public int _getModCount() { + return modCount; + } + + protected void _setModCount(int newModCount) { + this.modCount = newModCount; + } + + private E _unlinkFirst() { if (!_isValidIndex(0)) throw new NoSuchElementException(); @@ -60,23 +83,23 @@ private E _getFirstElement() { if (!_isValidIndex(0)) throw new NoSuchElementException(); - return _get(0); + return _uncheckedGet(0); } public boolean add(E e) { - return super.add(e); + return super._add(e); } public void add(int index, E element) { - super.add(index, element); + super._add(index, element); } public boolean addAll(@NotNull Collection c) { - return super.addAll(c); + return super._addAll(c); } public boolean addAll(int index, @NotNull Collection c) { - return super.addAll(index, c); + return super._addAll(index, c); } public void addFirst(E e) { @@ -88,20 +111,20 @@ public void addLast(E e) { } public void clear() { - super.clear(); + super._clear(); } + @SuppressWarnings("MethodDoesntCallSuperMethod") public Object clone() throws CloneNotSupportedException { - return super.clone(); + return super._clone(); } public boolean contains(Object o) { - return super.contains(o); + return super._contains(o); } - @SuppressWarnings("SlowListContainsAll") public boolean containsAll(@NotNull Collection c) { - return super.containsAll(c); + return super._containsAll(c); } @NotNull @@ -113,16 +136,17 @@ public E element() { return _getFirstElement(); } + @SuppressWarnings("EqualsDoesntCheckParameterClass") public boolean equals(Object o) { - return Engine.typeIs(o, LinkedListImpl.class) && super.equals(o); + return Engine.typeIs(o, LinkedListImpl.class) && super._equals(o); } public void forEach(Consumer _action) { - super.forEach(_action); + super._forEach(_action); } public E get(int index) { - return super.get(index); + return super._get(index); } public E getFirst() { @@ -130,38 +154,38 @@ public E getFirst() { } public E getLast() { - return super.get(_getStorage().size() - 1); + return super._get(_getStorage().size() - 1); } public int hashCode() { - return super.hashCode(); + return super._hashCode(); } public int indexOf(Object o) { - return super.indexOf(o); + return super._indexOf(o); } public boolean isEmpty() { - return super.isEmpty(); + return super._isEmpty(); } @NotNull public Iterator iterator() { - return super.iterator(); + return super._iterator(); } public int lastIndexOf(Object o) { - return super.lastIndexOf(o); + return super._lastIndexOf(o); } @NotNull public ListIterator listIterator() { - return super.listIterator(); + return super._listIterator(); } @NotNull public ListIterator listIterator(int index) { - return super.listIterator(index); + return super._listIterator(index); } public boolean offer(E e) { @@ -178,15 +202,16 @@ public boolean offerLast(E e) { return true; } + @NotNull public Stream parallelStream() { - return super.parallelStream(); + return super._parallelStream(); } public E peek() { if (isEmpty()) return null; - return _get(0); + return _uncheckedGet(0); } public E peekFirst() { @@ -198,7 +223,7 @@ public E peekLast() { if (size == 0) return null; - return _get(size - 1); + return _uncheckedGet(size - 1); } public E poll() { @@ -233,15 +258,15 @@ public E remove() { } public boolean remove(Object o) { - return super.remove(o); + return super._remove(o); } public E remove(int index) { - return super.remove(index); + return super._remove(index); } public boolean removeAll(@NotNull Collection c) { - return super.removeAll(c); + return super._removeAll(c); } public E removeFirst() { @@ -252,8 +277,8 @@ public boolean removeFirstOccurrence(Object o) { return remove(o); } - public boolean removeIf(Predicate filter) { - return super.removeIf(filter); + public boolean removeIf(@NotNull Predicate filter) { + return super._removeIf(filter); } public E removeLast() { @@ -289,54 +314,56 @@ public boolean removeLastOccurrence(Object o) { return false; } - public void replaceAll(UnaryOperator op) { - super.replaceAll(op); + public void replaceAll(@NotNull UnaryOperator op) { + super._replaceAll(op); } public boolean retainAll(@NotNull Collection c) { - return super.retainAll(c); + return super._retainAll(c); } public E set(int index, E element) { - return super.set(index, element); + return super._set(index, element); } public int size() { - return super.size(); + return super._size(); } public void sort(Comparator c) { - super.sort(c); + super._sort(c); } + @NotNull public Spliterator spliterator() { - return super.spliterator(); + return super._spliterator(); } + @NotNull public Stream stream() { - return super.stream(); + return super._stream(); } @NotNull public List subList(int fromIndex, int toIndex) { - return super.subList(fromIndex, toIndex); + return super._subList(fromIndex, toIndex); } @NotNull public Object[] toArray() { - return super.toArray(); + return super._toArray(); } - public T[] toArray(IntFunction generator) { - return super.toArray(generator); + public T[] toArray(@NotNull IntFunction generator) { + return super._toArray(generator); } @NotNull public T[] toArray(@NotNull T[] a) { - return super.toArray(a); + return super._toArray(a); } public String toString() { - return super.toString(); + return super._toString(); } } diff --git a/approximations/src/main/java/generated/java/util/list/ListIteratorStubImpl.java b/approximations/src/main/java/generated/java/util/list/ListIteratorStubImpl.java index b97694fd..e79010bb 100644 --- a/approximations/src/main/java/generated/java/util/list/ListIteratorStubImpl.java +++ b/approximations/src/main/java/generated/java/util/list/ListIteratorStubImpl.java @@ -31,7 +31,7 @@ public ListIteratorStubImpl(AbstractListImpl list, int index, int expectedMod } public ListIteratorStubImpl(AbstractListImpl list, int index) { - this(list, index, list.modCount); + this(list, index, list._getModCount()); } public ListIteratorStubImpl(AbstractListImpl list) { @@ -45,7 +45,7 @@ protected AbstractListImpl _getList() { } protected int _parentModCount() { - return _getList().modCount; + return _getList()._getModCount(); } protected int _getSize(SymbolicList storage) { @@ -100,11 +100,11 @@ public void remove() { _checkForModification(); AbstractListImpl list = _getList(); SymbolicList storage = list._getStorage(); - list.modCount++; + list._incrementModCount(); storage.remove(this.lastRet); this.cursor = this.lastRet; this.lastRet = -1; - this.expectedModCount = list.modCount; + this.expectedModCount = list._getModCount(); } public void set(E e) { @@ -120,11 +120,12 @@ public void add(E e) { _checkForModification(); AbstractListImpl list = _getList(); SymbolicList storage = list._getStorage(); - list.modCount++; + list._incrementModCount(); + // TODO: use ArrayList.add(e) storage.insert(this.cursor, e); this.cursor++; this.lastRet = -1; - this.expectedModCount = list.modCount; + this.expectedModCount = list._getModCount(); } public void forEachRemaining(Consumer userAction) { diff --git a/approximations/src/main/java/generated/java/util/list/ListSpliteratorStubImpl.java b/approximations/src/main/java/generated/java/util/list/ListSpliteratorStubImpl.java index 0ee02268..21d739da 100644 --- a/approximations/src/main/java/generated/java/util/list/ListSpliteratorStubImpl.java +++ b/approximations/src/main/java/generated/java/util/list/ListSpliteratorStubImpl.java @@ -14,6 +14,12 @@ public class ListSpliteratorStubImpl extends AbstractSpliteratorImpl { public AbstractListImpl list; + public int index; + + public int fence; + + public int expectedModCount; + protected ListSpliteratorStubImpl(AbstractListImpl list, int index, int fence, int expectedModCount) { super(index, fence, expectedModCount); Engine.assume(list != null); @@ -30,32 +36,61 @@ private AbstractListImpl _getList() { return result; } + protected int _getIndex() { + return index; + } + + protected void _setIndex(int newIndex) { + this.index = newIndex; + } + + protected int _getFence() { + return fence; + } + + protected void _setFence(int newFence) { + this.fence = newFence; + } + + protected int _getExpectedModCount() { + return expectedModCount; + } + + protected void _setExpectedModCount(int newExpectedModCount) { + this.expectedModCount = newExpectedModCount; + } + protected ListSpliteratorStubImpl _create(int index, int fence) { return new ListSpliteratorStubImpl<>(this.list, index, fence, this.expectedModCount); } protected int _parentModCount() { - return _getList().modCount; + return _getList()._getModCount(); } protected int _storageSize() { return _getList()._getStorage().size(); } - public int characteristics() { + protected int _characteristics() { return LibSLGlobals.SPLITERATOR_ORDERED | LibSLGlobals.SPLITERATOR_SIZED | LibSLGlobals.SPLITERATOR_SUBSIZED; } + @SuppressWarnings("MagicConstant") + public int characteristics() { + return _characteristics(); + } + public long estimateSize() { - return super.estimateSize(); + return super._estimateSize(); } - public void forEachRemaining(Consumer _action) { + protected void _forEachRemaining(Consumer _action) { if (_action == null) throw new NullPointerException(); SymbolicList storage = _getList()._getStorage(); - int fence = _getFence(); + int fence = _fence(); for (int i = this.index; i < fence; i++) { E item = storage.get(i); _action.accept(item); @@ -64,15 +99,19 @@ public void forEachRemaining(Consumer _action) { _checkForModification(); } + public void forEachRemaining(Consumer _action) { + _forEachRemaining(_action); + } + public long getExactSizeIfKnown() { - return super.getExactSizeIfKnown(); + return super._getExactSizeIfKnown(); } - public boolean tryAdvance(Consumer _action) { + protected boolean _tryAdvance(Consumer _action) { if (_action == null) throw new NullPointerException(); - int fence = _getFence(); + int fence = _fence(); int current = this.index; if (current >= fence) return false; @@ -86,7 +125,11 @@ public boolean tryAdvance(Consumer _action) { return true; } + public boolean tryAdvance(Consumer _action) { + return _tryAdvance(_action); + } + public ListSpliteratorStubImpl trySplit() { - return (ListSpliteratorStubImpl) super.trySplit(); + return (ListSpliteratorStubImpl) super._trySplit(); } } diff --git a/approximations/src/main/java/generated/java/util/list/SubListImpl.java b/approximations/src/main/java/generated/java/util/list/SubListImpl.java index 7aab3c14..b9dc94e3 100644 --- a/approximations/src/main/java/generated/java/util/list/SubListImpl.java +++ b/approximations/src/main/java/generated/java/util/list/SubListImpl.java @@ -37,6 +37,7 @@ public final class SubListImpl extends AbstractListImpl implements RandomA @SuppressWarnings("DataFlowIssue") private SubListImpl(AbstractListImpl list, SubListImpl parent, int offset, int length, int modCount) { + super(null, 0); Engine.assume(list != null); Engine.assume(offset >= 0); Engine.assume(length >= 0); @@ -52,6 +53,21 @@ public SubListImpl(AbstractListImpl list, int fromIndex, int toIndex) { this(list, null, fromIndex, toIndex - fromIndex, 0); } + public SymbolicList _getStorage() { + return null; + } + + public void _setStorage(SymbolicList storage) { + } + + public int _getModCount() { + return modCount; + } + + protected void _setModCount(int newModCount) { + this.modCount = newModCount; + } + public AbstractListImpl _getList() { AbstractListImpl result = this.list; Engine.assume(result != null); @@ -83,7 +99,7 @@ public boolean _addAllElements(int index, Collection c) { public void _updateSizeAndModCount(int sizeChange) { this.length += sizeChange; AbstractListImpl list = _getList(); - this.modCount = list.modCount; + this.modCount = list._getModCount(); SubListImpl parentSubList = this.parentSubList; while (parentSubList != null) { parentSubList.length += sizeChange; @@ -176,14 +192,14 @@ public void clear() { for (int i = start; i > end; i--) { rootStorage.remove(i); } - list.modCount++; + list._incrementModCount(); _updateSizeAndModCount(-size); } @SuppressWarnings("unchecked") public Object clone() throws CloneNotSupportedException { SubListImpl cloned = (SubListImpl) super.clone(); - cloned.list = (AbstractListImpl) this.list.clone(); + cloned.list = (AbstractListImpl) this.list._clone(); cloned.parentSubList = (SubListImpl) this.parentSubList.clone(); cloned.modCount = 0; return cloned; @@ -255,7 +271,7 @@ public void forEach(Consumer _action) { Engine.assume(this.length > 0); AbstractListImpl list = _getList(); SymbolicList rootStorage = list._getStorage(); - int expectedModCount = list.modCount; + int expectedModCount = list._getModCount(); this.modCount = expectedModCount; int end = _endIndex(); list._checkForModification(expectedModCount); @@ -327,6 +343,7 @@ public ListIterator listIterator(int index) { return new SubListIteratorStubImpl<>(this, index); } + @NotNull public Stream parallelStream() { return _makeStream(true); } @@ -359,7 +376,7 @@ public boolean removeAll(@NotNull Collection c) { return _batchRemove(c, false); } - public boolean removeIf(Predicate filter) { + public boolean removeIf(@NotNull Predicate filter) { AbstractListImpl list = _getList(); list._checkForModification(this.modCount); if (isEmpty()) @@ -376,7 +393,8 @@ public boolean removeIf(Predicate filter) { return false; } - public void replaceAll(UnaryOperator operator) { + @SuppressWarnings("ConstantValue") + public void replaceAll(@NotNull UnaryOperator operator) { if (operator == null) throw new NullPointerException(); @@ -407,13 +425,15 @@ public int size() { public void sort(Comparator c) { AbstractListImpl list = _getList(); list._do_sort(this.offset, _endIndex(), c); - this.modCount = list.modCount; + this.modCount = list._getModCount(); } + @NotNull public Spliterator spliterator() { return new SubListSpliteratorStubImpl<>(this); } + @NotNull public Stream stream() { return _makeStream(false); } @@ -428,16 +448,16 @@ public List subList(int fromIndex, int toIndex) { @NotNull public Object[] toArray() { - return super.toArray(); + return super._toArray(); } - public T[] toArray(IntFunction generator) { - return super.toArray(generator); + public T[] toArray(@NotNull IntFunction generator) { + return super._toArray(generator); } @NotNull public T[] toArray(@NotNull T[] array) { - return super.toArray(array); + return super._toArray(array); } public String toString() { diff --git a/approximations/src/main/java/generated/java/util/map/AbstractMapImpl.java b/approximations/src/main/java/generated/java/util/map/AbstractMapImpl.java index a7c3ba1b..5645eb93 100644 --- a/approximations/src/main/java/generated/java/util/map/AbstractMapImpl.java +++ b/approximations/src/main/java/generated/java/util/map/AbstractMapImpl.java @@ -13,27 +13,20 @@ @Approximate(java.util.AbstractMap.class) public abstract class AbstractMapImpl implements Map { - public LibSLRuntime.Map> storage; - - public transient int modCount; - - final boolean isHashMap; - - static LibSLRuntime.Map.Container> createContainer(boolean isHashMap) { + static LibSLRuntime.Map.Container> _createContainer(boolean isHashMap) { if (isHashMap) return new LibSLRuntime.HashMapContainer<>(); return new LibSLRuntime.IdentityMapContainer<>(); } - static LibSLRuntime.Map> createStorage(boolean isHashMap) { - return new LibSLRuntime.Map<>(createContainer(isHashMap)); + static LibSLRuntime.Map> _createStorage(boolean isHashMap) { + return new LibSLRuntime.Map<>(_createContainer(isHashMap)); } public AbstractMapImpl(boolean isHashMap) { - this.storage = createStorage(isHashMap); - this.modCount = 0; - this.isHashMap = isHashMap; + _setStorage(_createStorage(isHashMap)); + _setModCount(0); } public AbstractMapImpl(boolean isHashMap, Map m) { @@ -45,11 +38,11 @@ public AbstractMapImpl(boolean isHashMap, int initialCapacity) { if (initialCapacity < 0) throw new IllegalArgumentException(); - this.storage = createStorage(isHashMap); - this.modCount = 0; - this.isHashMap = isHashMap; + _setStorage(_createStorage(isHashMap)); + _setModCount(0); } + @SuppressWarnings("ExpressionComparedToItself") public AbstractMapImpl(boolean isHashMap, int initialCapacity, float loadFactor) { if (initialCapacity < 0) throw new IllegalArgumentException(); @@ -57,15 +50,22 @@ public AbstractMapImpl(boolean isHashMap, int initialCapacity, float loadFactor) if (loadFactor <= 0 || loadFactor != loadFactor) throw new IllegalArgumentException(); - this.storage = createStorage(isHashMap); - this.modCount = 0; - this.isHashMap = isHashMap; + _setStorage(_createStorage(isHashMap)); + _setModCount(0); } - public LibSLRuntime.Map> _getStorage() { - LibSLRuntime.Map> result = this.storage; - Engine.assume(result != null); - return result; + public abstract LibSLRuntime.Map> _getStorage(); + + public abstract void _setStorage(LibSLRuntime.Map> storage); + + abstract protected int _getModCount(); + + abstract protected void _setModCount(int newModCount); + + abstract protected boolean _isHashMap(); + + protected void _incrementModCount() { + _setModCount(_getModCount() + 1); } @SuppressWarnings("unchecked") @@ -89,25 +89,25 @@ private void _addAllElements(Map m) { Entry entry = new AbstractMap_EntryImpl<>(key, value); storage.set(key, entry); } - this.modCount++; + _incrementModCount(); } } public void _checkForModification(int expectedModCount) { - if (this.modCount != expectedModCount) + if (_getModCount() != expectedModCount) throw new ConcurrentModificationException(); } - public void clear() { - this.modCount++; - this.storage = createStorage(this.isHashMap); + public void _clear() { + _incrementModCount(); + _setStorage(_createStorage(_isHashMap())); } @SuppressWarnings("unchecked") - public Object clone() throws CloneNotSupportedException { + public Object _clone() throws CloneNotSupportedException { AbstractMapImpl clonedMap = (AbstractMapImpl) super.clone(); - clonedMap.storage = _getStorage().duplicate(); - clonedMap.modCount = 0; + clonedMap._setStorage(_getStorage().duplicate()); + clonedMap._setModCount(0); return clonedMap; } @@ -145,14 +145,14 @@ private void _update(K key, Map.Entry entry, V newValue) { } @SuppressWarnings("ConstantValue") - public V compute(K key, @NotNull BiFunction remappingFunction) { + public V _compute(K key, @NotNull BiFunction remappingFunction) { if (remappingFunction == null) throw new NullPointerException(); Map.Entry entry = _getEntry(key); V oldValue = _getEntryValueIfNotNull(entry); - int expectedModCount = this.modCount; + int expectedModCount = _getModCount(); V newValue = remappingFunction.apply(key, oldValue); _checkForModification(expectedModCount); _update(key, entry, newValue); @@ -161,7 +161,7 @@ public V compute(K key, @NotNull BiFunction r } @SuppressWarnings("ConstantValue") - public V computeIfAbsent(K key, @NotNull Function mappingFunction) { + public V _computeIfAbsent(K key, @NotNull Function mappingFunction) { if (mappingFunction == null) throw new NullPointerException(); @@ -171,7 +171,7 @@ public V computeIfAbsent(K key, @NotNull Function mappin if (oldValue != null) return oldValue; - int expectedModCount = this.modCount; + int expectedModCount = _getModCount(); V newValue = mappingFunction.apply(key); _checkForModification(expectedModCount); _update(key, entry, newValue); @@ -180,7 +180,7 @@ public V computeIfAbsent(K key, @NotNull Function mappin } @SuppressWarnings("ConstantValue") - public V computeIfPresent(K key, @NotNull BiFunction remappingFunction) { + public V _computeIfPresent(K key, @NotNull BiFunction remappingFunction) { if (remappingFunction == null) throw new NullPointerException(); @@ -190,7 +190,7 @@ public V computeIfPresent(K key, @NotNull BiFunction> storage = _getStorage(); return storage.size() != 0 && storage.hasKey((K) key); } - public boolean containsValue(Object value) { + public boolean _containsValue(Object value) { LibSLRuntime.Map> storage = _getStorage(); int storageSize = storage.size(); if (storageSize == 0) @@ -226,12 +226,12 @@ public boolean containsValue(Object value) { } @NotNull - public Set> entrySet() { + public Set> _entrySet() { return new Map_EntrySetImpl<>(this); } @SuppressWarnings({"unchecked", "ConstantValue"}) - public boolean equals(Object other) { + public boolean _equals(Object other) { if (other == this) return true; @@ -268,7 +268,7 @@ public boolean equals(Object other) { return true; } - public void forEach(BiConsumer userAction) { + public void _forEach(BiConsumer userAction) { if (userAction == null) throw new NullPointerException(); @@ -278,7 +278,7 @@ public void forEach(BiConsumer userAction) { return; Engine.assume(storageSize > 0); - int expectedModCount = this.modCount; + int expectedModCount = _getModCount(); LibSLRuntime.Map> unseen = storage.duplicate(); for (int i = 0; i < storageSize; i++) { K curKey = unseen.anyKey(); @@ -291,30 +291,30 @@ public void forEach(BiConsumer userAction) { } @SuppressWarnings("unchecked") - public V get(Object key) { + public V _get(Object key) { return _getEntryValueIfNotNull(_getEntry((K) key)); } @SuppressWarnings("unchecked") - public V getOrDefault(Object key, V defaultValue) { + public V _getOrDefault(Object key, V defaultValue) { return _getEntryValueIfNotNull(_getEntry((K) key), defaultValue); } - public int hashCode() { + public int _hashCode() { return LibSLRuntime.hashCode(_getStorage()); } - public boolean isEmpty() { + public boolean _isEmpty() { return _getStorage().size() == 0; } @NotNull - public Set keySet() { + public Set _keySet() { return new Map_KeySetImpl<>(this); } @SuppressWarnings("ConstantValue") - public V merge(K key, @NotNull V value, @NotNull BiFunction remappingFunction) { + public V _merge(K key, @NotNull V value, @NotNull BiFunction remappingFunction) { if (value == null) throw new NullPointerException(); @@ -329,7 +329,7 @@ public V merge(K key, @NotNull V value, @NotNull BiFunction entry = new AbstractMap_EntryImpl<>(key, value); storage.set(key, entry); - this.modCount++; + _incrementModCount(); return value; } - public V put(K key, V value) { - this.modCount++; + public V _put(K key, V value) { LibSLRuntime.Map> storage = _getStorage(); if (storage.hasKey(key)) { Map.Entry entry = storage.get(key); @@ -359,19 +358,20 @@ public V put(K key, V value) { Map.Entry entry = new AbstractMap_EntryImpl<>(key, value); storage.set(key, entry); + _incrementModCount(); return null; } @SuppressWarnings("ConstantValue") - public void putAll(@NotNull Map m) { + public void _putAll(@NotNull Map m) { if (m == null) throw new NullPointerException(); _addAllElements(m); } - public V putIfAbsent(K key, V value) { + public V _putIfAbsent(K key, V value) { LibSLRuntime.Map> storage = _getStorage(); if (storage.hasKey(key)) { Map.Entry entry = storage.get(key); @@ -380,20 +380,20 @@ public V putIfAbsent(K key, V value) { Map.Entry entry = new AbstractMap_EntryImpl<>(key, value); storage.set(key, entry); - this.modCount++; + _incrementModCount(); return null; } @SuppressWarnings("unchecked") - public V remove(Object key) { + public V _remove(Object key) { K typedKey = (K) key; LibSLRuntime.Map> storage = _getStorage(); if (storage.hasKey(typedKey)) { Map.Entry entry = storage.get(typedKey); V result = entry.getValue(); storage.remove(typedKey); - this.modCount++; + _incrementModCount(); return result; } @@ -401,7 +401,7 @@ public V remove(Object key) { } @SuppressWarnings("unchecked") - public boolean remove(Object key, Object value) { + public boolean _remove(Object key, Object value) { K typedKey = (K) key; LibSLRuntime.Map> storage = _getStorage(); if (storage.hasKey(typedKey)) { @@ -409,7 +409,7 @@ public boolean remove(Object key, Object value) { V curValue = entry.getValue(); if (LibSLRuntime.equals(curValue, value)) { storage.remove(typedKey); - this.modCount++; + _incrementModCount(); return true; } } @@ -417,7 +417,7 @@ public boolean remove(Object key, Object value) { return false; } - public V replace(K key, V value) { + public V _replace(K key, V value) { LibSLRuntime.Map> storage = _getStorage(); if (storage.hasKey(key)) { Map.Entry entry = storage.get(key); @@ -429,7 +429,7 @@ public V replace(K key, V value) { return null; } - public boolean replace(K key, V oldValue, V newValue) { + public boolean _replace(K key, V oldValue, V newValue) { LibSLRuntime.Map> storage = _getStorage(); if (storage.hasKey(key)) { Map.Entry entry = storage.get(key); @@ -443,7 +443,7 @@ public boolean replace(K key, V oldValue, V newValue) { return false; } - public void replaceAll(BiFunction function) { + public void _replaceAll(BiFunction function) { if (function == null) throw new NullPointerException(); @@ -453,7 +453,7 @@ public void replaceAll(BiFunction function) { return; Engine.assume(size > 0); - int expectedModCount = this.modCount; + int expectedModCount = _getModCount(); LibSLRuntime.Map> unseen = storage.duplicate(); for (int i = 0; i < size; i++) { K key = unseen.anyKey(); @@ -464,11 +464,11 @@ public void replaceAll(BiFunction function) { _checkForModification(expectedModCount); } - public int size() { + public int _size() { return _getStorage().size(); } - public String toString() { + public String _toString() { LibSLRuntime.Map> storage = _getStorage(); int size = storage.size(); if (size == 0) @@ -492,7 +492,7 @@ public String toString() { } @NotNull - public Collection values() { + public Collection _values() { return new Map_ValuesImpl<>(this); } diff --git a/approximations/src/main/java/generated/java/util/map/ConcurrentHashMapImpl.java b/approximations/src/main/java/generated/java/util/map/ConcurrentHashMapImpl.java index 3074b9d5..a2c35753 100644 --- a/approximations/src/main/java/generated/java/util/map/ConcurrentHashMapImpl.java +++ b/approximations/src/main/java/generated/java/util/map/ConcurrentHashMapImpl.java @@ -3,6 +3,7 @@ import org.jacodb.approximation.annotation.Approximate; import org.jetbrains.annotations.NotNull; import org.usvm.api.Engine; +import runtime.LibSLRuntime; import java.io.Serial; import java.io.Serializable; @@ -19,6 +20,10 @@ public class ConcurrentHashMapImpl extends AbstractMapImpl implement @Serial private static final long serialVersionUID = 7249069246763182397L; + private LibSLRuntime.Map> storage; + + private int modCount; + static { Engine.assume(true); } @@ -28,7 +33,7 @@ public ConcurrentHashMapImpl() { super(true); } - public ConcurrentHashMapImpl(Map m) { + public ConcurrentHashMapImpl(Map m) { super(true, m); } @@ -42,114 +47,138 @@ public ConcurrentHashMapImpl(int initialCapacity, float loadFactor) { super(true, initialCapacity, loadFactor); } + public LibSLRuntime.Map> _getStorage() { + LibSLRuntime.Map> result = this.storage; + Engine.assume(result != null); + return result; + } + + public void _setStorage(LibSLRuntime.Map> storage) { + this.storage = storage; + } + + protected int _getModCount() { + return modCount; + } + + protected void _setModCount(int newModCount) { + this.modCount = newModCount; + } + + protected boolean _isHashMap() { + return true; + } + public void clear() { - super.clear(); + super._clear(); } + @SuppressWarnings("MethodDoesntCallSuperMethod") public Object clone() throws CloneNotSupportedException { - return super.clone(); + return super._clone(); } public V compute(K key, @NotNull BiFunction remappingFunction) { - return super.compute(key, remappingFunction); + return super._compute(key, remappingFunction); } public V computeIfAbsent(K key, @NotNull Function mappingFunction) { - return super.computeIfAbsent(key, mappingFunction); + return super._computeIfAbsent(key, mappingFunction); } public V computeIfPresent(K key, @NotNull BiFunction remappingFunction) { - return super.computeIfPresent(key, remappingFunction); + return super._computeIfPresent(key, remappingFunction); } public boolean containsKey(Object key) { - return super.containsKey(key); + return super._containsKey(key); } public boolean containsValue(Object value) { - return super.containsValue(value); + return super._containsValue(value); } @NotNull public Set> entrySet() { - return super.entrySet(); + return super._entrySet(); } + @SuppressWarnings("EqualsDoesntCheckParameterClass") public boolean equals(Object other) { - return Engine.typeIs(other, ConcurrentHashMapImpl.class) && super.equals(other); + return Engine.typeIs(other, ConcurrentHashMapImpl.class) && super._equals(other); } public void forEach(BiConsumer userAction) { - super.forEach(userAction); + super._forEach(userAction); } public V get(Object key) { - return super.get(key); + return super._get(key); } public V getOrDefault(Object key, V defaultValue) { - return super.getOrDefault(key, defaultValue); + return super._getOrDefault(key, defaultValue); } public int hashCode() { - return super.hashCode(); + return super._hashCode(); } public boolean isEmpty() { - return super.isEmpty(); + return super._isEmpty(); } @NotNull public Set keySet() { - return super.keySet(); + return super._keySet(); } public V merge(K key, @NotNull V value, @NotNull BiFunction remappingFunction) { - return super.merge(key, value, remappingFunction); + return super._merge(key, value, remappingFunction); } public V put(K key, V value) { - return super.put(key, value); + return super._put(key, value); } public void putAll(@NotNull Map m) { - super.putAll(m); + super._putAll(m); } public V putIfAbsent(@NotNull K key, V value) { - return super.putIfAbsent(key, value); + return super._putIfAbsent(key, value); } public V remove(Object key) { - return super.remove(key); + return super._remove(key); } public boolean remove(@NotNull Object key, Object value) { - return super.remove(key, value); + return super._remove(key, value); } public V replace(@NotNull K key, @NotNull V value) { - return super.replace(key, value); + return super._replace(key, value); } public boolean replace(@NotNull K key, @NotNull V oldValue, @NotNull V newValue) { - return super.replace(key, oldValue, newValue); + return super._replace(key, oldValue, newValue); } public void replaceAll(BiFunction function) { - super.replaceAll(function); + super._replaceAll(function); } public int size() { - return super.size(); + return super._size(); } public String toString() { - return super.toString(); + return super._toString(); } @NotNull public Collection values() { - return super.values(); + return super._values(); } } diff --git a/approximations/src/main/java/generated/java/util/map/HashMapImpl.java b/approximations/src/main/java/generated/java/util/map/HashMapImpl.java index 3788bf1d..571c7c6c 100644 --- a/approximations/src/main/java/generated/java/util/map/HashMapImpl.java +++ b/approximations/src/main/java/generated/java/util/map/HashMapImpl.java @@ -14,6 +14,7 @@ import org.jacodb.approximation.annotation.Approximate; import org.jetbrains.annotations.NotNull; import org.usvm.api.Engine; +import runtime.LibSLRuntime; @Approximate(java.util.HashMap.class) public class HashMapImpl extends AbstractMapImpl implements Cloneable, Serializable { @@ -21,6 +22,10 @@ public class HashMapImpl extends AbstractMapImpl implements Cloneabl @Serial private static final long serialVersionUID = 362498820763181265L; + private LibSLRuntime.Map> storage; + + private int modCount; + static { Engine.assume(true); } @@ -44,114 +49,138 @@ public HashMapImpl(int initialCapacity, float loadFactor) { super(true, initialCapacity, loadFactor); } + public LibSLRuntime.Map> _getStorage() { + LibSLRuntime.Map> result = this.storage; + Engine.assume(result != null); + return result; + } + + public void _setStorage(LibSLRuntime.Map> storage) { + this.storage = storage; + } + + protected int _getModCount() { + return modCount; + } + + protected void _setModCount(int newModCount) { + this.modCount = newModCount; + } + + protected boolean _isHashMap() { + return true; + } + public void clear() { - super.clear(); + super._clear(); } + @SuppressWarnings("MethodDoesntCallSuperMethod") public Object clone() throws CloneNotSupportedException { - return super.clone(); + return super._clone(); } public V compute(K key, @NotNull BiFunction remappingFunction) { - return super.compute(key, remappingFunction); + return super._compute(key, remappingFunction); } public V computeIfAbsent(K key, @NotNull Function mappingFunction) { - return super.computeIfAbsent(key, mappingFunction); + return super._computeIfAbsent(key, mappingFunction); } public V computeIfPresent(K key, @NotNull BiFunction remappingFunction) { - return super.computeIfPresent(key, remappingFunction); + return super._computeIfPresent(key, remappingFunction); } public boolean containsKey(Object key) { - return super.containsKey(key); + return super._containsKey(key); } public boolean containsValue(Object value) { - return super.containsValue(value); + return super._containsValue(value); } @NotNull public Set> entrySet() { - return super.entrySet(); + return super._entrySet(); } + @SuppressWarnings("EqualsDoesntCheckParameterClass") public boolean equals(Object other) { - return Engine.typeIs(other, HashMapImpl.class) && super.equals(other); + return Engine.typeIs(other, HashMapImpl.class) && super._equals(other); } public void forEach(BiConsumer userAction) { - super.forEach(userAction); + super._forEach(userAction); } public V get(Object key) { - return super.get(key); + return super._get(key); } public V getOrDefault(Object key, V defaultValue) { - return super.getOrDefault(key, defaultValue); + return super._getOrDefault(key, defaultValue); } public int hashCode() { - return super.hashCode(); + return super._hashCode(); } public boolean isEmpty() { - return super.isEmpty(); + return super._isEmpty(); } @NotNull public Set keySet() { - return super.keySet(); + return super._keySet(); } public V merge(K key, @NotNull V value, @NotNull BiFunction remappingFunction) { - return super.merge(key, value, remappingFunction); + return super._merge(key, value, remappingFunction); } public V put(K key, V value) { - return super.put(key, value); + return super._put(key, value); } public void putAll(@NotNull Map m) { - super.putAll(m); + super._putAll(m); } public V putIfAbsent(K key, V value) { - return super.putIfAbsent(key, value); + return super._putIfAbsent(key, value); } public V remove(Object key) { - return super.remove(key); + return super._remove(key); } public boolean remove(Object key, Object value) { - return super.remove(key, value); + return super._remove(key, value); } public V replace(K key, V value) { - return super.replace(key, value); + return super._replace(key, value); } public boolean replace(K key, V oldValue, V newValue) { - return super.replace(key, oldValue, newValue); + return super._replace(key, oldValue, newValue); } public void replaceAll(BiFunction function) { - super.replaceAll(function); + super._replaceAll(function); } public int size() { - return super.size(); + return super._size(); } public String toString() { - return super.toString(); + return super._toString(); } @NotNull public Collection values() { - return super.values(); + return super._values(); } } diff --git a/approximations/src/main/java/generated/java/util/map/LinkedHashMapImpl.java b/approximations/src/main/java/generated/java/util/map/LinkedHashMapImpl.java index 791058b4..8b989fea 100644 --- a/approximations/src/main/java/generated/java/util/map/LinkedHashMapImpl.java +++ b/approximations/src/main/java/generated/java/util/map/LinkedHashMapImpl.java @@ -77,8 +77,9 @@ public Set> entrySet() { return super.entrySet(); } + @SuppressWarnings("EqualsDoesntCheckParameterClass") public boolean equals(Object other) { - return Engine.typeIs(other, LinkedHashMapImpl.class) && super.equals(other); + return Engine.typeIs(other, LinkedHashMapImpl.class) && super._equals(other); } public void forEach(BiConsumer userAction) { diff --git a/approximations/src/main/java/generated/java/util/map/Map_ContentsImpl.java b/approximations/src/main/java/generated/java/util/map/Map_ContentsImpl.java index 45166aa2..c00a1d45 100644 --- a/approximations/src/main/java/generated/java/util/map/Map_ContentsImpl.java +++ b/approximations/src/main/java/generated/java/util/map/Map_ContentsImpl.java @@ -24,30 +24,35 @@ public Map_ContentsImpl(AbstractMapImpl map) { this.map = map; } + public int _getModCount() { + return 0; + } + + protected void _setModCount(int newModCount) { + } + @SuppressWarnings("DataFlowIssue") - LibSLRuntime.Map> getStorage() { + LibSLRuntime.Map> _getStorage() { Engine.assume(this.map != null); return this.map._getStorage(); } abstract Content _contentByKey(LibSLRuntime.Map> storage, K key); - @SuppressWarnings("ConstantValue") protected Object[] _mapToArray() { - LibSLRuntime.Map> storage = getStorage(); - int storageSize = storage.size(); - Object[] result = new Object[storageSize]; - if (storageSize == 0) - return result; - - Engine.assume(storageSize > 0); + ArrayList items = new ArrayList<>(); + LibSLRuntime.Map> storage = _getStorage(); LibSLRuntime.Map> unseen = storage.duplicate(); - for (int i = 0; i < storageSize; i++) { + while (true) { K curKey = unseen.anyKey(); - result[i] = _contentByKey(storage, curKey); + if (!unseen.hasKey(curKey)) { + break; + } unseen.remove(curKey); + items.add(_contentByKey(storage, curKey)); } - return result; + + return items.toArray(); } public boolean add(Content e) { @@ -65,7 +70,7 @@ public void clear() { abstract boolean _containsInStorage(LibSLRuntime.Map> storage, Object o); public boolean contains(Object obj) { - LibSLRuntime.Map> storage = getStorage(); + LibSLRuntime.Map> storage = _getStorage(); if (storage.size() == 0) return false; @@ -100,7 +105,7 @@ public boolean equals(Object other) { if (c == null) return false; - if (getStorage().size() != c.size()) + if (_getStorage().size() != c.size()) return false; return containsAll(c); @@ -110,13 +115,13 @@ public void forEach(Consumer userAction) { if (userAction == null) throw new NullPointerException(); - LibSLRuntime.Map> storage = getStorage(); + LibSLRuntime.Map> storage = _getStorage(); int size = storage.size(); if (size == 0) return; Engine.assume(size > 0); - int expectedModCount = this.map.modCount; + int expectedModCount = this.map._getModCount(); LibSLRuntime.Map> unseen = storage.duplicate(); for (int i = 0; i < size; i++) { K key = unseen.anyKey(); @@ -127,18 +132,19 @@ public void forEach(Consumer userAction) { } public int hashCode() { - return LibSLRuntime.hashCode(getStorage()); + return LibSLRuntime.hashCode(_getStorage()); } public boolean isEmpty() { - return getStorage().size() == 0; + return _getStorage().size() == 0; } @NotNull public Iterator iterator() { - return new Map_Contents_IteratorImpl<>(this, getStorage().duplicate(), this.map.modCount); + return new Map_Contents_IteratorImpl<>(this, _getStorage().duplicate(), this.map._getModCount()); } + @NotNull @SuppressWarnings("unchecked") public Stream parallelStream() { Content[] items = (Content[]) _mapToArray(); @@ -152,7 +158,7 @@ public boolean removeAll(@NotNull Collection c) { if (c == null) throw new NullPointerException(); - LibSLRuntime.Map> storage = getStorage(); + LibSLRuntime.Map> storage = _getStorage(); int startStorageSize = storage.size(); int cSize = c.size(); if (startStorageSize == 0 || cSize == 0) @@ -164,7 +170,7 @@ public boolean removeAll(@NotNull Collection c) { K key = unseen.anyKey(); if (c.contains(_contentByKey(storage, key))) { storage.remove(key); - this.map.modCount++; + this.map._incrementModCount(); } unseen.remove(key); } @@ -179,11 +185,12 @@ public boolean removeAll(@NotNull Collection c) { return startStorageSize != storage.size(); } - public boolean removeIf(Predicate filter) { + @SuppressWarnings("ConstantValue") + public boolean removeIf(@NotNull Predicate filter) { if (filter == null) throw new NullPointerException(); - LibSLRuntime.Map> storage = getStorage(); + LibSLRuntime.Map> storage = _getStorage(); int startStorageSize = storage.size(); if (startStorageSize == 0) return false; @@ -193,7 +200,7 @@ public boolean removeIf(Predicate filter) { K curKey = unseen.anyKey(); if (filter.test(_contentByKey(storage, curKey))) { storage.remove(curKey); - this.map.modCount++; + this.map._incrementModCount(); } unseen.remove(curKey); } @@ -206,7 +213,7 @@ public boolean retainAll(@NotNull Collection c) { if (c == null) throw new NullPointerException(); - LibSLRuntime.Map> storage = getStorage(); + LibSLRuntime.Map> storage = _getStorage(); int startStorageSize = storage.size(); int cSize = c.size(); if (startStorageSize == 0 || cSize == 0) @@ -217,21 +224,27 @@ public boolean retainAll(@NotNull Collection c) { K curKey = unseen.anyKey(); if (!c.contains(_contentByKey(storage, curKey))) { storage.remove(curKey); - this.map.modCount++; + this.map._incrementModCount(); } } return startStorageSize != storage.size(); } + protected int _size() { + return this.map._size(); + } + public int size() { - return this.map.size(); + return _size(); } + @NotNull public Spliterator spliterator() { return new Map_Contents_SpliteratorImpl<>(this); } + @NotNull @SuppressWarnings("unchecked") public Stream stream() { Content[] items = (Content[]) _mapToArray(); @@ -240,20 +253,20 @@ public Stream stream() { @NotNull public Object[] toArray() { - return super.toArray(); + return super._toArray(); } - public T[] toArray(IntFunction generator) { - return super.toArray(generator); + public T[] toArray(@NotNull IntFunction generator) { + return super._toArray(generator); } @NotNull public T[] toArray(@NotNull T[] array) { - return super.toArray(array); + return super._toArray(array); } - public String toString() { - LibSLRuntime.Map> storage = getStorage(); + protected String _toString() { + LibSLRuntime.Map> storage = _getStorage(); int size = storage.size(); if (size == 0) return "[]"; @@ -272,4 +285,8 @@ public String toString() { return result.concat("]"); } + + public String toString() { + return _toString(); + } } diff --git a/approximations/src/main/java/generated/java/util/map/Map_ContentsSetImpl.java b/approximations/src/main/java/generated/java/util/map/Map_ContentsSetImpl.java index aeb1d5f6..1154a835 100644 --- a/approximations/src/main/java/generated/java/util/map/Map_ContentsSetImpl.java +++ b/approximations/src/main/java/generated/java/util/map/Map_ContentsSetImpl.java @@ -65,6 +65,7 @@ public Iterator iterator() { return super.iterator(); } + @NotNull public Stream parallelStream() { return super.parallelStream(); } @@ -73,7 +74,7 @@ public boolean removeAll(@NotNull Collection c) { return super.removeAll(c); } - public boolean removeIf(Predicate filter) { + public boolean removeIf(@NotNull Predicate filter) { return super.removeIf(filter); } @@ -85,10 +86,12 @@ public int size() { return super.size(); } + @NotNull public Spliterator spliterator() { return new Map_ContentsSet_SpliteratorImpl<>(this); } + @NotNull public Stream stream() { return super.stream(); } @@ -98,7 +101,7 @@ public Object[] toArray() { return super.toArray(); } - public T[] toArray(IntFunction generator) { + public T[] toArray(@NotNull IntFunction generator) { return super.toArray(generator); } diff --git a/approximations/src/main/java/generated/java/util/map/Map_Contents_IteratorImpl.java b/approximations/src/main/java/generated/java/util/map/Map_Contents_IteratorImpl.java index 258d5a3a..3d7714c8 100644 --- a/approximations/src/main/java/generated/java/util/map/Map_Contents_IteratorImpl.java +++ b/approximations/src/main/java/generated/java/util/map/Map_Contents_IteratorImpl.java @@ -43,10 +43,11 @@ private AbstractMapImpl _getMap() { } protected int _parentModCount() { - return _getMap().modCount; + return _getMap()._getModCount(); } private boolean _isEmpty() { + // TODO: make via 'contains(unseen.anyKey) == false' return this.unseen.size() == 0; } @@ -91,9 +92,9 @@ public void remove() { _checkForModification(); AbstractMapImpl map = _getMap(); map._getStorage().remove(key); - map.modCount++; + map._incrementModCount(); this.unseen.remove(key); - this.expectedModCount = map.modCount; + this.expectedModCount = map._getModCount(); this.currentKey = null; } } diff --git a/approximations/src/main/java/generated/java/util/map/Map_Contents_SpliteratorImpl.java b/approximations/src/main/java/generated/java/util/map/Map_Contents_SpliteratorImpl.java index bb3ac0e3..7bf870bc 100644 --- a/approximations/src/main/java/generated/java/util/map/Map_Contents_SpliteratorImpl.java +++ b/approximations/src/main/java/generated/java/util/map/Map_Contents_SpliteratorImpl.java @@ -22,6 +22,12 @@ public class Map_Contents_SpliteratorImpl extends AbstractSpliter SymbolicList unseenKeys; + public int index; + + public int fence; + + public int expectedModCount; + Map_Contents_SpliteratorImpl( Map_ContentsImpl contents, SymbolicList seenKeys, @@ -40,6 +46,30 @@ public Map_Contents_SpliteratorImpl(Map_ContentsImpl contents) { this(contents, Engine.makeSymbolicList(), null, 0, -1, 0); } + protected int _getIndex() { + return index; + } + + protected void _setIndex(int newIndex) { + this.index = newIndex; + } + + protected int _getFence() { + return fence; + } + + protected void _setFence(int newFence) { + this.fence = newFence; + } + + protected int _getExpectedModCount() { + return expectedModCount; + } + + protected void _setExpectedModCount(int newExpectedModCount) { + this.expectedModCount = newExpectedModCount; + } + protected AbstractSpliteratorImpl _create(int index, int fence) { return null; } @@ -67,26 +97,31 @@ private AbstractMapImpl _getMap() { } protected int _parentModCount() { - return _getMap().modCount; + return _getMap()._getModCount(); } protected int _storageSize() { - return _getContents().getStorage().size(); + return _getContents()._getStorage().size(); } protected int _defaultCharacteristics() { return 0; } - public int characteristics() { + protected int _characteristics() { if (this.fence < 0 || this.index == 0 && this.fence == _storageSize()) return LibSLGlobals.SPLITERATOR_SIZED | _defaultCharacteristics(); return _defaultCharacteristics(); } + @SuppressWarnings("MagicConstant") + public int characteristics() { + return _characteristics(); + } + public long estimateSize() { - return super.estimateSize(); + return super._estimateSize(); } private int _checkSizeOfUnseenKeys() { @@ -106,7 +141,7 @@ private int _checkSizeOfSeenKeys() { } private LibSLRuntime.Map> _removeSeenKeys() { - LibSLRuntime.Map> storage = _getContents().getStorage().duplicate(); + LibSLRuntime.Map> storage = _getContents()._getStorage().duplicate(); int size = _checkSizeOfSeenKeys(); for (int i = 0; i < size; i++) { K key = seenKeys.get(i); @@ -116,16 +151,16 @@ private LibSLRuntime.Map> _removeSeenKeys() { return storage; } - public void forEachRemaining(Consumer userAction) { + protected void _forEachRemaining(Consumer userAction) { if (userAction == null) throw new NullPointerException(); - int fence = _getFence(); + int fence = _fence(); Map_ContentsImpl contents = _getContents(); if (unseenKeys != null) { _checkSizeOfSeenKeys(); int size = _checkSizeOfUnseenKeys(); - LibSLRuntime.Map> storage = contents.getStorage(); + LibSLRuntime.Map> storage = contents._getStorage(); for (int i = 0; i < size; i++) { K key = unseenKeys.get(i); userAction.accept(contents._contentByKey(storage, key)); @@ -145,15 +180,19 @@ public void forEachRemaining(Consumer userAction) { _checkForModification(); } + public void forEachRemaining(Consumer userAction) { + _forEachRemaining(userAction); + } + public long getExactSizeIfKnown() { - return super.getExactSizeIfKnown(); + return super._getExactSizeIfKnown(); } - public boolean tryAdvance(Consumer userAction) { + protected boolean _tryAdvance(Consumer userAction) { if (userAction == null) throw new NullPointerException(); - int hi = _getFence(); + int hi = _fence(); if (this.index >= hi) return false; @@ -162,7 +201,7 @@ public boolean tryAdvance(Consumer userAction) { _checkSizeOfSeenKeys(); _checkSizeOfUnseenKeys(); K key = unseenKeys.get(0); - LibSLRuntime.Map> storage = contents.getStorage(); + LibSLRuntime.Map> storage = contents._getStorage(); userAction.accept(contents._contentByKey(storage, key)); unseenKeys.remove(0); seenKeys.insert(this.index, key); @@ -179,8 +218,12 @@ public boolean tryAdvance(Consumer userAction) { return true; } + public boolean tryAdvance(Consumer userAction) { + return _tryAdvance(userAction); + } + public Map_Contents_SpliteratorImpl trySplit() { - int hi = _getFence(); + int hi = _fence(); int lo = this.index; int mid = (hi + lo) >>> 1; if (lo >= mid) diff --git a/approximations/src/main/java/generated/java/util/map/Map_EntrySetImpl.java b/approximations/src/main/java/generated/java/util/map/Map_EntrySetImpl.java index 92c18664..cd5a86f1 100644 --- a/approximations/src/main/java/generated/java/util/map/Map_EntrySetImpl.java +++ b/approximations/src/main/java/generated/java/util/map/Map_EntrySetImpl.java @@ -78,6 +78,7 @@ public Iterator> iterator() { return super.iterator(); } + @NotNull public Stream> parallelStream() { return super.parallelStream(); } @@ -89,12 +90,12 @@ public boolean remove(Object o) { Map.Entry typedOtherEntry = (Map.Entry) o; K key = typedOtherEntry.getKey(); - LibSLRuntime.Map> storage = getStorage(); + LibSLRuntime.Map> storage = _getStorage(); if (storage.hasKey(key)) { Map.Entry entry = storage.get(key); if (LibSLRuntime.equals(entry, typedOtherEntry)) { storage.remove(key); - this.map.modCount++; + this.map._incrementModCount(); return true; } } @@ -106,7 +107,7 @@ public boolean removeAll(@NotNull Collection c) { return super.removeAll(c); } - public boolean removeIf(Predicate> filter) { + public boolean removeIf(@NotNull Predicate> filter) { return super.removeIf(filter); } @@ -118,10 +119,12 @@ public int size() { return super.size(); } + @NotNull public Spliterator> spliterator() { return super.spliterator(); } + @NotNull public Stream> stream() { return super.stream(); } @@ -131,7 +134,7 @@ public Object[] toArray() { return super.toArray(); } - public T[] toArray(IntFunction generator) { + public T[] toArray(@NotNull IntFunction generator) { return super.toArray(generator); } diff --git a/approximations/src/main/java/generated/java/util/map/Map_KeySetImpl.java b/approximations/src/main/java/generated/java/util/map/Map_KeySetImpl.java index 4caa9c6d..7f0b23ad 100644 --- a/approximations/src/main/java/generated/java/util/map/Map_KeySetImpl.java +++ b/approximations/src/main/java/generated/java/util/map/Map_KeySetImpl.java @@ -70,6 +70,7 @@ public Iterator iterator() { return super.iterator(); } + @NotNull public Stream parallelStream() { return super.parallelStream(); } @@ -77,10 +78,10 @@ public Stream parallelStream() { @SuppressWarnings("unchecked") public boolean remove(Object key) { K typedKey = (K) key; - LibSLRuntime.Map> storage = getStorage(); + LibSLRuntime.Map> storage = _getStorage(); if (storage.hasKey(typedKey)) { storage.remove(typedKey); - this.map.modCount++; + this.map._incrementModCount(); return true; } @@ -91,7 +92,7 @@ public boolean removeAll(@NotNull Collection c) { return super.removeAll(c); } - public boolean removeIf(Predicate filter) { + public boolean removeIf(@NotNull Predicate filter) { return super.removeIf(filter); } @@ -103,10 +104,12 @@ public int size() { return super.size(); } + @NotNull public Spliterator spliterator() { return super.spliterator(); } + @NotNull public Stream stream() { return super.stream(); } @@ -116,7 +119,7 @@ public Object[] toArray() { return super.toArray(); } - public T[] toArray(IntFunction generator) { + public T[] toArray(@NotNull IntFunction generator) { return super.toArray(generator); } diff --git a/approximations/src/main/java/generated/java/util/map/Map_ValuesImpl.java b/approximations/src/main/java/generated/java/util/map/Map_ValuesImpl.java index 9ce4255b..e983829f 100644 --- a/approximations/src/main/java/generated/java/util/map/Map_ValuesImpl.java +++ b/approximations/src/main/java/generated/java/util/map/Map_ValuesImpl.java @@ -39,7 +39,7 @@ public void clear() { } boolean _containsInStorage(LibSLRuntime.Map> storage, Object value) { - LibSLRuntime.Map> unseen = getStorage().duplicate(); + LibSLRuntime.Map> unseen = _getStorage().duplicate(); int size = unseen.size(); Engine.assume(size > 0); for (int i = 0; i < size; i++) { @@ -76,12 +76,13 @@ public Iterator iterator() { return super.iterator(); } + @NotNull public Stream parallelStream() { return super.parallelStream(); } public boolean remove(Object value) { - LibSLRuntime.Map> storage = getStorage(); + LibSLRuntime.Map> storage = _getStorage(); LibSLRuntime.Map> unseen = storage.duplicate(); int size = unseen.size(); Engine.assume(size >= 0); @@ -91,7 +92,7 @@ public boolean remove(Object value) { V curValue = entry.getValue(); if (LibSLRuntime.equals(curValue, value)) { storage.remove(key); - this.map.modCount++; + this.map._incrementModCount(); return true; } @@ -105,7 +106,7 @@ public boolean removeAll(@NotNull Collection c) { return super.removeAll(c); } - public boolean removeIf(Predicate filter) { + public boolean removeIf(@NotNull Predicate filter) { return super.removeIf(filter); } @@ -117,10 +118,12 @@ public int size() { return super.size(); } + @NotNull public Spliterator spliterator() { return super.spliterator(); } + @NotNull public Stream stream() { return super.stream(); } @@ -130,7 +133,7 @@ public Object[] toArray() { return super.toArray(); } - public T[] toArray(IntFunction generator) { + public T[] toArray(@NotNull IntFunction generator) { return super.toArray(generator); } diff --git a/approximations/src/main/java/generated/java/util/set/AbstractSetImpl.java b/approximations/src/main/java/generated/java/util/set/AbstractSetImpl.java index 78116933..e2b487a3 100644 --- a/approximations/src/main/java/generated/java/util/set/AbstractSetImpl.java +++ b/approximations/src/main/java/generated/java/util/set/AbstractSetImpl.java @@ -21,29 +21,24 @@ @Approximate(java.util.AbstractSet.class) public abstract class AbstractSetImpl extends AbstractCollectionImpl implements Set { - public LibSLRuntime.Map storage; - - private boolean isHashSet; - - private static LibSLRuntime.Map.Container createContainer(boolean isHashSet) { + private static LibSLRuntime.Map.Container _createContainer(boolean isHashSet) { if (isHashSet) return new LibSLRuntime.HashMapContainer<>(); return new LibSLRuntime.IdentityMapContainer<>(); } - private static LibSLRuntime.Map createStorage(boolean isHashSet) { - return new LibSLRuntime.Map<>(createContainer(isHashSet)); + private static LibSLRuntime.Map _createStorage(boolean isHashSet) { + return new LibSLRuntime.Map<>(_createContainer(isHashSet)); } - public AbstractSetImpl(LibSLRuntime.Map storage, int modCount, boolean isHashSet) { + public AbstractSetImpl(LibSLRuntime.Map storage, int modCount) { super(modCount); - this.storage = storage; - this.isHashSet = isHashSet; + _setStorage(storage); } public AbstractSetImpl(boolean isHashSet) { - this(createStorage(isHashSet), 0, isHashSet); + this(_createStorage(isHashSet), 0); } @SuppressWarnings("unused") @@ -59,11 +54,10 @@ public AbstractSetImpl(boolean isHashSet, int initialCapacity) { if (initialCapacity < 0) throw new IllegalArgumentException(); - this.storage = createStorage(isHashSet); - this.isHashSet = isHashSet; + _setStorage(_createStorage(isHashSet)); } - @SuppressWarnings("unused") + @SuppressWarnings({"unused", "ExpressionComparedToItself"}) public AbstractSetImpl(boolean isHashSet, int initialCapacity, float loadFactor) { super(0); @@ -73,8 +67,7 @@ public AbstractSetImpl(boolean isHashSet, int initialCapacity, float loadFactor) if (loadFactor <= 0 || loadFactor != loadFactor) throw new IllegalArgumentException(); - this.storage = createStorage(isHashSet); - this.isHashSet = isHashSet; + _setStorage(_createStorage(isHashSet)); } @SuppressWarnings("unused") @@ -83,13 +76,13 @@ public AbstractSetImpl(int initialCapacity, float loadFactor, boolean dummy) { LibSLRuntime.error("Private constructor call"); } - public LibSLRuntime.Map _getStorage() { - LibSLRuntime.Map storage = this.storage; - Engine.assume(storage != null); - return storage; - } + public abstract LibSLRuntime.Map _getStorage(); - private void _add(E key) { + public abstract void _setStorage(LibSLRuntime.Map storage); + + abstract protected boolean _isHashSet(); + + private void _internalAdd(E key) { _getStorage().set(key, LibSLGlobals.SOMETHING); } @@ -105,12 +98,12 @@ public boolean _addAllElements(Collection c) { } else { for (E key : c) { if (!storage.hasKey(key)) - _add(key); + _internalAdd(key); } } if (lengthBeforeAdd != storage.size()) { - this.modCount++; + _incrementModCount(); return true; } @@ -118,15 +111,18 @@ public boolean _addAllElements(Collection c) { } protected Object[] _mapToArray() { - int size = _getStorage().size(); - Object[] items = new Object[size]; + ArrayList items = new ArrayList<>(); LibSLRuntime.Map unseen = _getStorage().duplicate(); - for (int i = 0; i < size; i++) { + while (true) { E key = unseen.anyKey(); + if (!unseen.hasKey(key)) { + break; + } unseen.remove(key); - items[i] = key; + items.add(key); } - return items; + + return items.toArray(); } @SuppressWarnings("unchecked") @@ -135,9 +131,9 @@ public Stream _makeStream(boolean parallel) { return new StreamStubImpl<>(items, parallel); } - public boolean add(E obj) { + public boolean _add(E obj) { LibSLRuntime.Map storage = _getStorage(); - this.modCount++; + _incrementModCount(); if (storage.hasKey(obj)) return false; @@ -145,69 +141,69 @@ public boolean add(E obj) { return true; } - public void clear() { - this.storage = createStorage(this.isHashSet); - this.modCount++; + public void _clear() { + _setStorage(_createStorage(_isHashSet())); + _incrementModCount(); } @SuppressWarnings("unchecked") - public Object clone() throws CloneNotSupportedException { + public Object _clone() throws CloneNotSupportedException { AbstractSetImpl clonedSet = (AbstractSetImpl) super.clone(); - clonedSet.modCount = 0; - clonedSet.storage = _getStorage().duplicate(); + clonedSet._setModCount(0); + clonedSet._setStorage(_getStorage().duplicate()); return clonedSet; } @SuppressWarnings("unchecked") - public boolean contains(Object obj) { + public boolean _contains(Object obj) { if (isEmpty()) return false; return _getStorage().hasKey((E) obj); } - public boolean isEmpty() { + public boolean _isEmpty() { return _getStorage().size() == 0; } @NotNull - public Iterator iterator() { + public Iterator _iterator() { LibSLRuntime.Map unseenKeys = _getStorage().duplicate(); - return new Set_IteratorImpl<>(this.modCount, unseenKeys, this, null); + return new Set_IteratorImpl<>(_getModCount(), unseenKeys, this, null); } @SuppressWarnings("unchecked") - public boolean remove(Object elem) { + public boolean _remove(Object elem) { E typedElem = (E) elem; LibSLRuntime.Map storage = _getStorage(); if (storage.hasKey(typedElem)) { storage.remove(typedElem); - this.modCount++; + _incrementModCount(); return true; } return false; } - public int size() { + public int _size() { return _getStorage().size(); } - public Spliterator spliterator() { + public Spliterator _spliterator() { return new Set_SpliteratorImpl<>(this); } @SuppressWarnings("unchecked") - public boolean equals(Object other) { + public boolean _equals(Object other) { if (other == this) return true; if (!(other instanceof Set)) return false; - int expectedModCount = this.modCount; + int expectedModCount = _getModCount(); AbstractSetImpl otherSet = (AbstractSetImpl) other; - int otherExpectedModCount = otherSet.modCount; + int otherExpectedModCount = otherSet._getModCount(); LibSLRuntime.Map otherStorage = otherSet._getStorage(); LibSLRuntime.Map storage = _getStorage(); @@ -221,17 +217,17 @@ public boolean equals(Object other) { return result; } - public int hashCode() { + public int _hashCode() { return LibSLRuntime.hashCode(_getStorage()); } @SuppressWarnings({"ConstantValue", "unchecked"}) - public boolean removeAll(@NotNull Collection c) { + public boolean _removeAll(@NotNull Collection c) { if (c == null) { throw new NullPointerException(); } - int expectedModCount = this.modCount; + int expectedModCount = _getModCount(); int otherSize = c.size(); LibSLRuntime.Map storage = _getStorage(); int lengthBeforeRemoving = storage.size(); @@ -254,26 +250,26 @@ public boolean removeAll(@NotNull Collection c) { } } _checkForModification(expectedModCount); - this.modCount++; + _incrementModCount(); return lengthBeforeRemoving != storage.size(); } @NotNull - public Object[] toArray() { - return super.toArray(); + public Object[] _toArray() { + return super._toArray(); } @NotNull - public T[] toArray(@NotNull T[] array) { - return super.toArray(array); + public T[] _toArray(@NotNull T[] array) { + return super._toArray(array); } - public T[] toArray(IntFunction generator) { - return super.toArray(generator); + public T[] _toArray(IntFunction generator) { + return super._toArray(generator); } @SuppressWarnings("unchecked") - public boolean containsAll(@NotNull Collection c) { + public boolean _containsAll(@NotNull Collection c) { LibSLRuntime.Map storage = _getStorage(); for (Object key : c) { if (!storage.hasKey((E) key)) @@ -283,12 +279,12 @@ public boolean containsAll(@NotNull Collection c) { return true; } - public boolean addAll(@NotNull Collection c) { + public boolean _addAll(@NotNull Collection c) { return _addAllElements(c); } @SuppressWarnings("ConstantValue") - public boolean retainAll(@NotNull Collection c) { + public boolean _retainAll(@NotNull Collection c) { if (c == null) throw new NullPointerException(); @@ -304,20 +300,20 @@ public boolean retainAll(@NotNull Collection c) { i++; } if (lengthBeforeAdd != storage.size()) { - this.modCount++; + _incrementModCount(); return true; } return false; } - public boolean removeIf(Predicate filter) { + public boolean _removeIf(Predicate filter) { if (filter == null) throw new NullPointerException(); LibSLRuntime.Map storage = _getStorage(); int lengthBeforeAdd = storage.size(); - int expectedModCount = this.modCount; + int expectedModCount = _getModCount(); LibSLRuntime.Map unseenKeys = storage.duplicate(); int i = 0; while (i < lengthBeforeAdd) { @@ -329,20 +325,20 @@ public boolean removeIf(Predicate filter) { } _checkForModification(expectedModCount); if (lengthBeforeAdd != storage.size()) { - this.modCount++; + _incrementModCount(); return true; } return false; } - public void forEach(Consumer userAction) { + public void _forEach(Consumer userAction) { if (userAction == null) throw new NullPointerException(); LibSLRuntime.Map storage = _getStorage(); int count = storage.size(); - int expectedModCount = this.modCount; + int expectedModCount = _getModCount(); LibSLRuntime.Map unseenKeys = storage.duplicate(); int i = 0; while (i < count) { @@ -354,15 +350,15 @@ public void forEach(Consumer userAction) { _checkForModification(expectedModCount); } - public Stream stream() { + public Stream _stream() { return _makeStream(false); } - public Stream parallelStream() { + public Stream _parallelStream() { return _makeStream(true); } - public String toString() { + public String _toString() { LibSLRuntime.Map storage = _getStorage(); int count = storage.size(); if (count == 0) diff --git a/approximations/src/main/java/generated/java/util/set/HashSetImpl.java b/approximations/src/main/java/generated/java/util/set/HashSetImpl.java index 722abe06..3c2601b4 100644 --- a/approximations/src/main/java/generated/java/util/set/HashSetImpl.java +++ b/approximations/src/main/java/generated/java/util/set/HashSetImpl.java @@ -14,6 +14,7 @@ import org.jacodb.approximation.annotation.Approximate; import org.jetbrains.annotations.NotNull; import org.usvm.api.Engine; +import runtime.LibSLRuntime; @Approximate(java.util.HashSet.class) public class HashSetImpl extends AbstractSetImpl implements Cloneable, Serializable { @@ -21,6 +22,10 @@ public class HashSetImpl extends AbstractSetImpl implements Cloneable, Ser @Serial private static final long serialVersionUID = -5024744406713321676L; + private LibSLRuntime.Map storage; + + private int modCount; + static { Engine.assume(true); } @@ -46,98 +51,125 @@ private HashSetImpl(int initialCapacity, float loadFactor, boolean dummy) { super(initialCapacity, loadFactor, dummy); } + public LibSLRuntime.Map _getStorage() { + LibSLRuntime.Map storage = this.storage; + Engine.assume(storage != null); + return storage; + } + + public void _setStorage(LibSLRuntime.Map storage) { + this.storage = storage; + } + + protected boolean _isHashSet() { + return true; + } + + public int _getModCount() { + return modCount; + } + + protected void _setModCount(int newModCount) { + this.modCount = newModCount; + } + public boolean add(E obj) { - return super.add(obj); + return super._add(obj); } public void clear() { - super.clear(); + super._clear(); } + @SuppressWarnings("MethodDoesntCallSuperMethod") public Object clone() throws CloneNotSupportedException { - return super.clone(); + return super._clone(); } public boolean contains(Object obj) { - return super.contains(obj); + return super._contains(obj); } public boolean isEmpty() { - return super.isEmpty(); + return super._isEmpty(); } @NotNull public Iterator iterator() { - return super.iterator(); + return super._iterator(); } public boolean remove(Object elem) { - return super.remove(elem); + return super._remove(elem); } public int size() { - return super.size(); + return super._size(); } + @NotNull public Spliterator spliterator() { - return super.spliterator(); + return super._spliterator(); } + @SuppressWarnings("EqualsDoesntCheckParameterClass") public boolean equals(Object other) { - return Engine.typeIs(other, HashSetImpl.class) && super.equals(other); + return Engine.typeIs(other, HashSetImpl.class) && super._equals(other); } public int hashCode() { - return super.hashCode(); + return super._hashCode(); } public boolean removeAll(@NotNull Collection c) { - return super.removeAll(c); + return super._removeAll(c); } @NotNull public Object[] toArray() { - return super.toArray(); + return super._toArray(); } @NotNull public T[] toArray(@NotNull T[] a) { - return super.toArray(a); + return super._toArray(a); } - public T[] toArray(IntFunction generator) { - return super.toArray(generator); + public T[] toArray(@NotNull IntFunction generator) { + return super._toArray(generator); } public boolean containsAll(@NotNull Collection c) { - return super.containsAll(c); + return super._containsAll(c); } public boolean addAll(@NotNull Collection c) { - return super.addAll(c); + return super._addAll(c); } public boolean retainAll(@NotNull Collection c) { - return super.retainAll(c); + return super._retainAll(c); } - public boolean removeIf(Predicate filter) { - return super.removeIf(filter); + public boolean removeIf(@NotNull Predicate filter) { + return super._removeIf(filter); } public void forEach(Consumer userAction) { - super.forEach(userAction); + super._forEach(userAction); } + @NotNull public Stream stream() { - return super.stream(); + return super._stream(); } + @NotNull public Stream parallelStream() { - return super.parallelStream(); + return super._parallelStream(); } public String toString() { - return super.toString(); + return super._toString(); } } diff --git a/approximations/src/main/java/generated/java/util/set/LinkedHashSetImpl.java b/approximations/src/main/java/generated/java/util/set/LinkedHashSetImpl.java index 46fe05df..d44705b4 100644 --- a/approximations/src/main/java/generated/java/util/set/LinkedHashSetImpl.java +++ b/approximations/src/main/java/generated/java/util/set/LinkedHashSetImpl.java @@ -73,12 +73,14 @@ public int size() { return super.size(); } + @NotNull public Spliterator spliterator() { return super.spliterator(); } + @SuppressWarnings("EqualsDoesntCheckParameterClass") public boolean equals(Object other) { - return Engine.typeIs(other, LinkedHashSetImpl.class) && super.equals(other); + return Engine.typeIs(other, LinkedHashSetImpl.class) && super._equals(other); } public int hashCode() { @@ -99,7 +101,7 @@ public T[] toArray(@NotNull T[] a) { return super.toArray(a); } - public T[] toArray(IntFunction generator) { + public T[] toArray(@NotNull IntFunction generator) { return super.toArray(generator); } @@ -115,7 +117,7 @@ public boolean retainAll(@NotNull Collection c) { return super.retainAll(c); } - public boolean removeIf(Predicate filter) { + public boolean removeIf(@NotNull Predicate filter) { return super.removeIf(filter); } @@ -123,10 +125,12 @@ public void forEach(Consumer userAction) { super.forEach(userAction); } + @NotNull public Stream stream() { return super.stream(); } + @NotNull public Stream parallelStream() { return super.parallelStream(); } diff --git a/approximations/src/main/java/generated/java/util/set/Set_IteratorImpl.java b/approximations/src/main/java/generated/java/util/set/Set_IteratorImpl.java index 450cd3e0..98158b54 100644 --- a/approximations/src/main/java/generated/java/util/set/Set_IteratorImpl.java +++ b/approximations/src/main/java/generated/java/util/set/Set_IteratorImpl.java @@ -40,7 +40,7 @@ private AbstractSetImpl _getSet() { } protected int _parentModCount() { - return _getSet().modCount; + return _getSet()._getModCount(); } private boolean _isEmpty() { @@ -85,9 +85,9 @@ public void remove() { _checkForModification(); AbstractSetImpl set = _getSet(); set._getStorage().remove(key); - set.modCount++; + set._incrementModCount(); this.unseen.remove(key); - this.expectedModCount = set.modCount; + this.expectedModCount = set._getModCount(); this.currentKey = null; } } diff --git a/approximations/src/main/java/generated/java/util/set/Set_SpliteratorImpl.java b/approximations/src/main/java/generated/java/util/set/Set_SpliteratorImpl.java index 2afb32fe..7acad512 100644 --- a/approximations/src/main/java/generated/java/util/set/Set_SpliteratorImpl.java +++ b/approximations/src/main/java/generated/java/util/set/Set_SpliteratorImpl.java @@ -22,6 +22,12 @@ public final class Set_SpliteratorImpl extends AbstractSpliteratorImpl { SymbolicList unseenKeys; + public int index; + + public int fence; + + public int expectedModCount; + Set_SpliteratorImpl( AbstractSetImpl set, SymbolicList seenKeys, @@ -40,6 +46,30 @@ public Set_SpliteratorImpl(AbstractSetImpl set) { this(set, Engine.makeSymbolicList(), null, 0, -1, 0); } + protected int _getIndex() { + return index; + } + + protected void _setIndex(int newIndex) { + this.index = newIndex; + } + + protected int _getFence() { + return fence; + } + + protected void _setFence(int newFence) { + this.fence = newFence; + } + + protected int _getExpectedModCount() { + return expectedModCount; + } + + protected void _setExpectedModCount(int newExpectedModCount) { + this.expectedModCount = newExpectedModCount; + } + protected AbstractSpliteratorImpl _create(int index, int fence) { return null; } @@ -51,22 +81,27 @@ private AbstractSetImpl _getSet() { } protected int _parentModCount() { - return _getSet().modCount; + return _getSet()._getModCount(); } protected int _storageSize() { return _getSet()._getStorage().size(); } - public int characteristics() { + protected int _characteristics() { if (this.fence < 0 || this.index == 0 && this.fence == _storageSize()) return LibSLGlobals.SPLITERATOR_SIZED | LibSLGlobals.SPLITERATOR_DISTINCT; return LibSLGlobals.SPLITERATOR_DISTINCT; } + @SuppressWarnings("MagicConstant") + public int characteristics() { + return _characteristics(); + } + public long estimateSize() { - return super.estimateSize(); + return super._estimateSize(); } private int _checkSizeOfUnseenKeys() { @@ -96,11 +131,11 @@ private LibSLRuntime.Map _removeSeenKeys() { return storage; } - public void forEachRemaining(Consumer userAction) { + protected void _forEachRemaining(Consumer userAction) { if (userAction == null) throw new NullPointerException(); - int fence = _getFence(); + int fence = _fence(); if (unseenKeys != null) { _checkSizeOfSeenKeys(); int size = _checkSizeOfUnseenKeys(); @@ -123,15 +158,19 @@ public void forEachRemaining(Consumer userAction) { _checkForModification(); } + public void forEachRemaining(Consumer userAction) { + _forEachRemaining(userAction); + } + public long getExactSizeIfKnown() { - return super.getExactSizeIfKnown(); + return super._getExactSizeIfKnown(); } - public boolean tryAdvance(Consumer userAction) { + protected boolean _tryAdvance(Consumer userAction) { if (userAction == null) throw new NullPointerException(); - int hi = _getFence(); + int hi = _fence(); if (this.index >= hi) return false; @@ -155,8 +194,12 @@ public boolean tryAdvance(Consumer userAction) { return true; } - public Set_SpliteratorImpl trySplit() { - int hi = _getFence(); + public boolean tryAdvance(Consumer userAction) { + return _tryAdvance(userAction); + } + + protected Set_SpliteratorImpl _trySplit() { + int hi = _fence(); int lo = this.index; int mid = (hi + lo) >>> 1; if (lo >= mid) @@ -176,4 +219,8 @@ public Set_SpliteratorImpl trySplit() { this.index = mid; return new Set_SpliteratorImpl<>(this.set, newSeenKeys, newUnseenKeys, lo, mid, this.expectedModCount); } + + public Set_SpliteratorImpl trySplit() { + return _trySplit(); + } } diff --git a/approximations/src/main/java/generated/java/util/stream/BaseStreamImpl.java b/approximations/src/main/java/generated/java/util/stream/BaseStreamImpl.java index df1dbe22..656bea4c 100644 --- a/approximations/src/main/java/generated/java/util/stream/BaseStreamImpl.java +++ b/approximations/src/main/java/generated/java/util/stream/BaseStreamImpl.java @@ -39,19 +39,19 @@ protected SymbolicList _getCloseHandlers() { } protected StreamStubImpl _copyToObjStream(T[] storage) { - return new StreamStubImpl<>(storage, _getCloseHandlers(), isParallel, linkedOrConsumed); + return new StreamStubImpl<>(storage, _getCloseHandlers(), isParallel, false); } protected IntStreamImpl _copyToIntStream(int[] storage) { - return new IntStreamImpl(storage, _getCloseHandlers(), isParallel, linkedOrConsumed); + return new IntStreamImpl(storage, _getCloseHandlers(), isParallel, false); } protected LongStreamImpl _copyToLongStream(long[] storage) { - return new LongStreamImpl(storage, _getCloseHandlers(), isParallel, linkedOrConsumed); + return new LongStreamImpl(storage, _getCloseHandlers(), isParallel, false); } protected DoubleStreamImpl _copyToDoubleStream(double[] storage) { - return new DoubleStreamImpl(storage, _getCloseHandlers(), isParallel, linkedOrConsumed); + return new DoubleStreamImpl(storage, _getCloseHandlers(), isParallel, false); } public void evaluate() { diff --git a/approximations/src/main/java/generated/java/util/stream/DoubleStreamImpl.java b/approximations/src/main/java/generated/java/util/stream/DoubleStreamImpl.java index c5779c9b..f9bd64a0 100644 --- a/approximations/src/main/java/generated/java/util/stream/DoubleStreamImpl.java +++ b/approximations/src/main/java/generated/java/util/stream/DoubleStreamImpl.java @@ -68,7 +68,7 @@ protected int _getLength() { } private DoubleStreamImpl _copy(double[] storage) { - return new DoubleStreamImpl(storage, _getCloseHandlers(), isParallel, linkedOrConsumed); + return new DoubleStreamImpl(storage, _getCloseHandlers(), isParallel, false); } private DoubleStreamImpl _copy() { diff --git a/approximations/src/main/java/generated/java/util/stream/IntStreamImpl.java b/approximations/src/main/java/generated/java/util/stream/IntStreamImpl.java index 04f57a43..d00243ff 100644 --- a/approximations/src/main/java/generated/java/util/stream/IntStreamImpl.java +++ b/approximations/src/main/java/generated/java/util/stream/IntStreamImpl.java @@ -66,7 +66,7 @@ protected int _getLength() { } private IntStreamImpl _copy(int[] storage) { - return new IntStreamImpl(storage, _getCloseHandlers(), isParallel, linkedOrConsumed); + return new IntStreamImpl(storage, _getCloseHandlers(), isParallel, false); } private IntStreamImpl _copy() { diff --git a/approximations/src/main/java/generated/java/util/stream/LongStreamImpl.java b/approximations/src/main/java/generated/java/util/stream/LongStreamImpl.java index b7ba0843..9628acd3 100644 --- a/approximations/src/main/java/generated/java/util/stream/LongStreamImpl.java +++ b/approximations/src/main/java/generated/java/util/stream/LongStreamImpl.java @@ -66,7 +66,7 @@ protected int _getLength() { } private LongStreamImpl _copy(long[] storage) { - return new LongStreamImpl(storage, _getCloseHandlers(), isParallel, linkedOrConsumed); + return new LongStreamImpl(storage, _getCloseHandlers(), isParallel, false); } private LongStreamImpl _copy() { diff --git a/approximations/src/main/java/generated/java/util/stream/StreamStubImpl.java b/approximations/src/main/java/generated/java/util/stream/StreamStubImpl.java index c404dd87..6fb83caf 100644 --- a/approximations/src/main/java/generated/java/util/stream/StreamStubImpl.java +++ b/approximations/src/main/java/generated/java/util/stream/StreamStubImpl.java @@ -78,7 +78,7 @@ protected int _getLength() { } private StreamStubImpl _copy(T[] storage) { - return new StreamStubImpl<>(storage, _getCloseHandlers(), isParallel, linkedOrConsumed); + return new StreamStubImpl<>(storage, _getCloseHandlers(), isParallel, false); } private StreamStubImpl _copy() { diff --git a/approximations/src/main/java/generated/org/apache/commons/logging/LogImpl.java b/approximations/src/main/java/generated/org/apache/commons/logging/LogImpl.java deleted file mode 100644 index 10629579..00000000 --- a/approximations/src/main/java/generated/org/apache/commons/logging/LogImpl.java +++ /dev/null @@ -1,56 +0,0 @@ -package generated.org.apache.commons.logging; - -import org.jacodb.approximation.annotation.Approximate; - -@SuppressWarnings("unused") -@Approximate(org.apache.commons.logging.Log.class) -public class LogImpl { - - final boolean isFatalEnabled() { - return false; - } - - final boolean isErrorEnabled() { - return false; - } - - final boolean isWarnEnabled() { - return false; - } - - final boolean isInfoEnabled() { - return false; - } - - final boolean isDebugEnabled() { - return false; - } - - final boolean isTraceEnabled() { - return false; - } - - final void fatal(Object message) { } - - final void fatal(Object message, Throwable t) { } - - final void error(Object message) { } - - final void error(Object message, Throwable t) { } - - final void warn(Object message) { } - - final void warn(Object message, Throwable t) { } - - final void info(Object message) { } - - final void info(Object message, Throwable t) { } - - final void debug(Object message) { } - - final void debug(Object message, Throwable t) { } - - final void trace(Object message) { } - - final void trace(Object message, Throwable t) { } -} diff --git a/approximations/src/main/java/generated/org/springframework/boot/ClassUtilsImpl.java b/approximations/src/main/java/generated/org/springframework/boot/ClassUtilsImpl.java deleted file mode 100644 index 2828168e..00000000 --- a/approximations/src/main/java/generated/org/springframework/boot/ClassUtilsImpl.java +++ /dev/null @@ -1,19 +0,0 @@ -package generated.org.springframework.boot; - -import org.jacodb.approximation.annotation.Approximate; -import org.springframework.util.ClassUtils; - -@Approximate(ClassUtils.class) -public abstract class ClassUtilsImpl { - - private static String getMainPackageName() { - throw new IllegalStateException("'getMainPackageName' should be approximated"); - } - - public static String getPackageName(Class clazz) { - if (clazz.getName().equals("StartSpringTestClass")) - return ClassUtilsImpl.getMainPackageName(); - - return clazz.getPackageName(); - } -} diff --git a/approximations/src/main/java/generated/org/springframework/boot/ErrorsMethodArgumentResolverImpl.java b/approximations/src/main/java/generated/org/springframework/boot/ErrorsMethodArgumentResolverImpl.java deleted file mode 100644 index 475effc1..00000000 --- a/approximations/src/main/java/generated/org/springframework/boot/ErrorsMethodArgumentResolverImpl.java +++ /dev/null @@ -1,28 +0,0 @@ -package generated.org.springframework.boot; - -import org.jacodb.approximation.annotation.Approximate; -import org.springframework.core.MethodParameter; -import org.springframework.lang.Nullable; -import org.springframework.ui.ModelMap; -import org.springframework.util.Assert; -import org.springframework.util.CollectionUtils; -import org.springframework.web.bind.support.WebDataBinderFactory; -import org.springframework.web.context.request.NativeWebRequest; -import org.springframework.web.method.support.ModelAndViewContainer; - -@SuppressWarnings("unused") -@Approximate(org.springframework.web.method.annotation.ErrorsMethodArgumentResolver.class) -public class ErrorsMethodArgumentResolverImpl { - - @SuppressWarnings("RedundantThrows") - public Object resolveArgument(MethodParameter parameter, @Nullable ModelAndViewContainer mavContainer, NativeWebRequest webRequest, @Nullable WebDataBinderFactory binderFactory) throws Exception { - Assert.state(mavContainer != null, "Errors/BindingResult argument only supported on regular handler methods"); - ModelMap model = mavContainer.getModel(); - String lastKey = CollectionUtils.lastElement(model.keySet()); - if (lastKey != null) { - return model.get(lastKey); - } else { - throw new IllegalStateException("An Errors/BindingResult argument is expected to be declared immediately after the model attribute, the @RequestBody or the @RequestPart arguments to which they apply: " + parameter.getMethod()); - } - } -} diff --git a/approximations/src/main/java/generated/org/springframework/boot/LogFactoryImpl.java b/approximations/src/main/java/generated/org/springframework/boot/LogFactoryImpl.java deleted file mode 100644 index 28c01808..00000000 --- a/approximations/src/main/java/generated/org/springframework/boot/LogFactoryImpl.java +++ /dev/null @@ -1,17 +0,0 @@ -package generated.org.springframework.boot; - -import org.apache.commons.logging.Log; -import org.apache.commons.logging.impl.NoOpLog; -import org.jacodb.approximation.annotation.Approximate; - -@Approximate(org.apache.commons.logging.LogFactory.class) -public abstract class LogFactoryImpl { - - public static Log getLog(Class clazz) { - return new NoOpLog(); - } - - public static Log getLog(String name) { - return new NoOpLog(); - } -} diff --git a/approximations/src/main/java/generated/org/springframework/boot/MergedContextConfigurationImpl.java b/approximations/src/main/java/generated/org/springframework/boot/MergedContextConfigurationImpl.java deleted file mode 100644 index 5a183dac..00000000 --- a/approximations/src/main/java/generated/org/springframework/boot/MergedContextConfigurationImpl.java +++ /dev/null @@ -1,26 +0,0 @@ -package generated.org.springframework.boot; - -import org.jacodb.approximation.annotation.Approximate; -import org.springframework.lang.Nullable; -import org.springframework.test.context.ContextCustomizer; -import org.springframework.test.context.MergedContextConfiguration; - -import java.util.Collections; -import java.util.Set; - -@Approximate(MergedContextConfiguration.class) -public class MergedContextConfigurationImpl { - - private static final Set EMPTY_CONTEXT_CUSTOMIZERS = Collections.emptySet(); - - private static Set processContextCustomizers( - @Nullable Set contextCustomizers - ) { - if (contextCustomizers == null) - return EMPTY_CONTEXT_CUSTOMIZERS; - - contextCustomizers.removeIf(it -> it.getClass().getName().contains("TypeExcludeFiltersContextCustomizer")); - - return contextCustomizers; - } -} diff --git a/approximations/src/main/java/generated/org/springframework/boot/PathVariableMethodArgumentResolverImpl.java b/approximations/src/main/java/generated/org/springframework/boot/PathVariableMethodArgumentResolverImpl.java deleted file mode 100644 index 91da2d61..00000000 --- a/approximations/src/main/java/generated/org/springframework/boot/PathVariableMethodArgumentResolverImpl.java +++ /dev/null @@ -1,20 +0,0 @@ -package generated.org.springframework.boot; - -import org.jacodb.approximation.annotation.Approximate; -import org.springframework.core.MethodParameter; -import org.springframework.lang.Nullable; -import org.springframework.web.bind.support.WebDataBinderFactory; -import org.springframework.web.context.request.NativeWebRequest; -import org.springframework.web.method.support.ModelAndViewContainer; - -import static generated.org.springframework.boot.SymbolicValueFactory.createSymbolic; - -@Approximate(org.springframework.web.servlet.mvc.method.annotation.PathVariableMethodArgumentResolver.class) -public class PathVariableMethodArgumentResolverImpl { - - public final Object resolveArgument(MethodParameter parameter, @Nullable ModelAndViewContainer mavContainer, - NativeWebRequest webRequest, @Nullable WebDataBinderFactory binderFactory) throws Exception { - Class paramType = parameter.getParameterType(); - return createSymbolic(paramType); - } -} diff --git a/approximations/src/main/java/generated/org/springframework/boot/RequestParamMethodArgumentResolverImpl.java b/approximations/src/main/java/generated/org/springframework/boot/RequestParamMethodArgumentResolverImpl.java deleted file mode 100644 index 6751c96a..00000000 --- a/approximations/src/main/java/generated/org/springframework/boot/RequestParamMethodArgumentResolverImpl.java +++ /dev/null @@ -1,20 +0,0 @@ -package generated.org.springframework.boot; - -import org.jacodb.approximation.annotation.Approximate; -import org.springframework.core.MethodParameter; -import org.springframework.lang.Nullable; -import org.springframework.web.bind.support.WebDataBinderFactory; -import org.springframework.web.context.request.NativeWebRequest; -import org.springframework.web.method.support.ModelAndViewContainer; - -import static generated.org.springframework.boot.SymbolicValueFactory.createSymbolic; - -@Approximate(org.springframework.web.method.annotation.RequestParamMethodArgumentResolver.class) -public class RequestParamMethodArgumentResolverImpl { - - public final Object resolveArgument(MethodParameter parameter, @Nullable ModelAndViewContainer mavContainer, - NativeWebRequest webRequest, @Nullable WebDataBinderFactory binderFactory) throws Exception { - Class paramType = parameter.getParameterType(); - return createSymbolic(paramType); - } -} diff --git a/approximations/src/main/java/generated/org/springframework/boot/SpringApplicationImpl.java b/approximations/src/main/java/generated/org/springframework/boot/SpringApplicationImpl.java deleted file mode 100644 index 1c26d62f..00000000 --- a/approximations/src/main/java/generated/org/springframework/boot/SpringApplicationImpl.java +++ /dev/null @@ -1,74 +0,0 @@ -package generated.org.springframework.boot; - -import jakarta.servlet.Filter; -import org.jacodb.approximation.annotation.Approximate; -import org.springframework.boot.ApplicationArguments; -import org.springframework.boot.ApplicationContextFactory; -import org.springframework.boot.context.logging.LoggingApplicationListener; -import org.springframework.context.ApplicationListener; -import org.springframework.context.ConfigurableApplicationContext; -import org.springframework.test.web.servlet.MockMvc; -import org.springframework.test.web.servlet.setup.DefaultMockMvcBuilder; -import org.springframework.test.web.servlet.setup.MockMvcBuilders; -import org.springframework.web.context.WebApplicationContext; - -import java.util.*; - -import static org.springframework.test.web.servlet.request.MockMvcRequestBuilders.*; - -@Approximate(org.springframework.boot.SpringApplication.class) -public class SpringApplicationImpl { - - private List> listeners; - - private ApplicationContextFactory applicationContextFactory = ApplicationContextFactory.DEFAULT; - - private boolean registerShutdownHook = true; - - private Map>> allControllerPaths() { - return new HashMap<>(); - } - - protected void afterRefresh(ConfigurableApplicationContext context, ApplicationArguments args) { - startAnalysis(); - Object[] beans = context.getBeansOfType(Filter.class).values().toArray(); - Filter[] filters = Arrays.copyOf(beans, beans.length, Filter[].class); - DefaultMockMvcBuilder builder = MockMvcBuilders.webAppContextSetup((WebApplicationContext) context); - for (Filter filter : filters) { - builder.addFilter(filter); - } - MockMvc mockMvc = builder.build(); - Map>> allPaths = allControllerPaths(); - try { - for (String controllerName : allPaths.keySet()) { - Map> paths = allPaths.get(controllerName); - for (String path : paths.keySet()) { - List properties = paths.get(path); - String kind = (String) properties.get(0); - Integer paramCount = (Integer) properties.get(1); - Object[] pathArgs = new Object[paramCount]; - if (kind.equals("get")) - mockMvc.perform(get(path, pathArgs)); - if (kind.equals("post")) - mockMvc.perform(post(path, pathArgs)); - if (kind.equals("put")) - mockMvc.perform(put(path, pathArgs)); - if (kind.equals("delete")) - mockMvc.perform(delete(path, pathArgs)); - if (kind.equals("patch")) - mockMvc.perform(patch(path, pathArgs)); - } - } - } catch (Exception e) { - throw new RuntimeException(e); - } - } - - private void startAnalysis() { } - - public void setListeners(Collection> listeners) { - registerShutdownHook = false; - listeners.removeIf(it -> it instanceof LoggingApplicationListener); - this.listeners = new ArrayList<>(listeners); - } -} diff --git a/approximations/src/main/java/generated/org/springframework/boot/StartSpring.java b/approximations/src/main/java/generated/org/springframework/boot/StartSpring.java deleted file mode 100644 index 41c9969a..00000000 --- a/approximations/src/main/java/generated/org/springframework/boot/StartSpring.java +++ /dev/null @@ -1,11 +0,0 @@ -package generated.org.springframework.boot; - -import org.springframework.test.context.TestContextManager; - -public class StartSpring { - - public static void startSpring() { - TestContextManager b = new TestContextManager(TestClass.class); - b.getTestContext().getApplicationContext(); - } -} diff --git a/approximations/src/main/java/generated/org/springframework/boot/SymbolicValueFactory.java b/approximations/src/main/java/generated/org/springframework/boot/SymbolicValueFactory.java deleted file mode 100644 index 57055eff..00000000 --- a/approximations/src/main/java/generated/org/springframework/boot/SymbolicValueFactory.java +++ /dev/null @@ -1,24 +0,0 @@ -package generated.org.springframework.boot; - -import org.usvm.api.Engine; - -public class SymbolicValueFactory { - public static Object createSymbolic(Class type) { - if (type == boolean.class) - return Engine.makeSymbolicBoolean(); - if (type == int.class) - return Engine.makeSymbolicInt(); - if (type == long.class) - return Engine.makeSymbolicLong(); - if (type == float.class) - return Engine.makeSymbolicFloat(); - if (type == byte.class) - return Engine.makeSymbolicByte(); - if (type == char.class) - return Engine.makeSymbolicChar(); - if (type == short.class) - return Engine.makeSymbolicShort(); - - return Engine.makeNullableSymbolic(type); - } -} diff --git a/approximations/src/main/java/generated/org/springframework/boot/TestClass.java b/approximations/src/main/java/generated/org/springframework/boot/TestClass.java deleted file mode 100644 index d66f59e8..00000000 --- a/approximations/src/main/java/generated/org/springframework/boot/TestClass.java +++ /dev/null @@ -1,12 +0,0 @@ -package generated.org.springframework.boot; - -import org.springframework.beans.factory.annotation.Autowired; -import org.springframework.boot.test.autoconfigure.web.servlet.WebMvcTest; -import org.springframework.test.web.servlet.MockMvc; - -@WebMvcTest -public class TestClass { - - @Autowired - private MockMvc mockMvc; -} diff --git a/approximations/src/main/java/generated/org/springframework/boot/TestContextManagerImpl.java b/approximations/src/main/java/generated/org/springframework/boot/TestContextManagerImpl.java deleted file mode 100644 index f50b2741..00000000 --- a/approximations/src/main/java/generated/org/springframework/boot/TestContextManagerImpl.java +++ /dev/null @@ -1,57 +0,0 @@ -package generated.org.springframework.boot; - -import org.jacodb.approximation.annotation.Approximate; -import org.springframework.test.context.TestContext; -import org.springframework.test.context.TestContextBootstrapper; -import org.springframework.test.context.TestContextManager; -import org.springframework.test.context.TestExecutionListener; -import org.springframework.util.ClassUtils; -import org.springframework.util.ReflectionUtils; - -import java.lang.reflect.Constructor; -import java.util.ArrayList; -import java.util.Collections; -import java.util.List; - -@Approximate(TestContextManager.class) -public class TestContextManagerImpl { - - private final TestContext testContext; - - private final List testExecutionListeners = new ArrayList<>(8); - - private static TestContext copyTestContext(TestContext testContext) { - Constructor constructor = - ClassUtils.getConstructorIfAvailable(testContext.getClass(), testContext.getClass()); - - if (constructor != null) { - try { - ReflectionUtils.makeAccessible(constructor); - return constructor.newInstance(testContext); - } - catch (Exception ignored) { - } - } - - // Fallback to original instance - return testContext; - } - - public TestContextManagerImpl(TestContextBootstrapper testContextBootstrapper) { - this.testContext = testContextBootstrapper.buildTestContext(); - registerTestExecutionListeners(testContextBootstrapper.getTestExecutionListeners()); - } - - public final TestContext getTestContext() { - return this.testContext; - } - - public void registerTestExecutionListeners(List testExecutionListeners) { - registerTestExecutionListeners(testExecutionListeners.toArray(new TestExecutionListener[0])); - } - - public void registerTestExecutionListeners(TestExecutionListener... testExecutionListeners) { - Collections.addAll(this.testExecutionListeners, testExecutionListeners); - } - -} diff --git a/approximations/src/main/java/runtime/LibSLRuntime.java b/approximations/src/main/java/runtime/LibSLRuntime.java index fb03400d..67122554 100644 --- a/approximations/src/main/java/runtime/LibSLRuntime.java +++ b/approximations/src/main/java/runtime/LibSLRuntime.java @@ -5,6 +5,7 @@ import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; +import generated.java.lang.StringImpl; import org.usvm.api.Engine; import org.usvm.api.SymbolicIdentityMap; import org.usvm.api.SymbolicList; @@ -87,7 +88,6 @@ public static int getUniqueId() { //} } - private static final int BUFF_SIZE_BYTE = 4; private static final int BUFF_SIZE_SHORT = 6; private static final int BUFF_SIZE_INT = 11; @@ -97,38 +97,46 @@ public static String toString(final boolean v) { return v ? "true" : "false"; } - @SuppressWarnings("ConstantConditions") - public static String toString(byte v) { - if (v == 0) return "0"; - if (v == Byte.MIN_VALUE) return "-128"; - if (v == Byte.MAX_VALUE) return "127"; - // TODO: add more common cases - - Engine.assume(v > Byte.MIN_VALUE); - Engine.assume(v < Byte.MAX_VALUE); + private static byte digitToByte(long i) { + return (byte) ('0' + i); + } - final char[] chars = new char[BUFF_SIZE_BYTE]; + private static String numberToString(long n, int buffSize) { + byte[] bytes = new byte[buffSize]; - final boolean isNegative = v < 0; + final boolean isNegative = n < 0; if (isNegative) - v = (byte) -v; + n = -n; int len = 0; - int pos = BUFF_SIZE_BYTE; - while (v != 0) { + int pos = buffSize; + while (n != 0) { pos--; len++; - chars[pos] = (char) ('0' + (v % 10)); - v /= 10; + bytes[pos] = digitToByte(n % 10); + n /= 10; } if (isNegative) { pos--; len++; - chars[pos] = '-'; + bytes[pos] = '-'; } - return new String(chars, pos, len); + return new String(bytes, pos, len); + } + + @SuppressWarnings("ConstantConditions") + public static String toString(byte v) { + if (v == 0) return "0"; + if (v == Byte.MIN_VALUE) return "-128"; + if (v == Byte.MAX_VALUE) return "127"; + // TODO: add more common cases + + Engine.assume(v > Byte.MIN_VALUE); + Engine.assume(v < Byte.MAX_VALUE); + + return numberToString(v, BUFF_SIZE_BYTE); } @SuppressWarnings("ConstantConditions") @@ -141,28 +149,7 @@ public static String toString(short v) { Engine.assume(v > Short.MIN_VALUE); Engine.assume(v < Short.MAX_VALUE); - final char[] chars = new char[BUFF_SIZE_SHORT]; - - final boolean isNegative = v < 0; - if (isNegative) - v = (short) -v; - - int len = 0; - int pos = BUFF_SIZE_SHORT; - while (v != 0) { - pos--; - len++; - chars[pos] = (char) ('0' + (v % 10)); - v /= 10; - } - - if (isNegative) { - pos--; - len++; - chars[pos] = '-'; - } - - return new String(chars, pos, len); + return numberToString(v, BUFF_SIZE_SHORT); } @SuppressWarnings("ConstantConditions") @@ -175,28 +162,7 @@ public static String toString(int v) { Engine.assume(v > Integer.MIN_VALUE); Engine.assume(v < Integer.MAX_VALUE); - final char[] chars = new char[BUFF_SIZE_INT]; - - final boolean isNegative = v < 0; - if (isNegative) - v = -v; - - int len = 0; - int pos = BUFF_SIZE_INT; - while (v != 0) { - pos--; - len++; - chars[pos] = (char) ('0' + (v % 10)); - v /= 10; - } - - if (isNegative) { - pos--; - len++; - chars[pos] = '-'; - } - - return new String(chars, pos, len); + return numberToString(v, BUFF_SIZE_INT); } @SuppressWarnings("ConstantConditions") @@ -209,40 +175,18 @@ public static String toString(long v) { Engine.assume(v > Long.MIN_VALUE); Engine.assume(v < Long.MAX_VALUE); - final char[] chars = new char[BUFF_SIZE_LONG]; - - final boolean isNegative = v < 0; - if (isNegative) - v = -v; - - int len = 0; - int pos = BUFF_SIZE_LONG; - while (v != 0) { - pos--; - len++; - chars[pos] = (char) ('0' + (v % 10)); - v /= 10; - } - - if (isNegative) { - pos--; - len++; - chars[pos] = '-'; - } - - return new String(chars, pos, len); + return numberToString(v, BUFF_SIZE_LONG); } - public static String toString(final char v) { - return String.valueOf(v); + public static String toString(char v) { + return new String(StringImpl._charToBytes(v)); } // TODO: do we need more variants for other primitive array types? - public static String toString(final char[] v) { - return new String(v); + public static String toString(char[] v) { + return new String(StringImpl._getBytes(v)); } - private static final float FLOAT_MULTIPLIER_REGULAR = 1e+6f; // 8 decimal positions private static final int FLOAT_MULTIPLIER_REGULAR_count = 6; private static final int FLOAT_MULTIPLIER_REGULAR_int = (int) FLOAT_MULTIPLIER_REGULAR; diff --git a/approximations/src/main/java/stub/java/lang/SystemHelpers.java b/approximations/src/main/java/stub/java/lang/SystemHelpers.java new file mode 100644 index 00000000..7dadc5ae --- /dev/null +++ b/approximations/src/main/java/stub/java/lang/SystemHelpers.java @@ -0,0 +1,8 @@ +package stub.java.lang; + +import runtime.LibSLRuntime; + +public final class SystemHelpers { + +// public static final LibSLRuntime.Map identityHashCodeMap = null; +} diff --git a/approximations/src/main/java/stub/java/util/array/AbstractArraySpliterator.java b/approximations/src/main/java/stub/java/util/array/AbstractArraySpliterator.java index 659d9058..729a1d93 100644 --- a/approximations/src/main/java/stub/java/util/array/AbstractArraySpliterator.java +++ b/approximations/src/main/java/stub/java/util/array/AbstractArraySpliterator.java @@ -32,7 +32,7 @@ public boolean hasCharacteristics(int _characteristics) { throw new LinkageError(); } - public int characteristics() { + public int _characteristics() { throw new LinkageError(); } @@ -42,7 +42,7 @@ public long estimateSize() { abstract protected E _getItem(int index); - public void forEachRemaining(Consumer _action) { + public void _forEachRemaining(Consumer _action) { throw new LinkageError(); } @@ -54,7 +54,7 @@ public long getExactSizeIfKnown() { throw new LinkageError(); } - public boolean tryAdvance(Consumer _action) { + public boolean _tryAdvance(Consumer _action) { throw new LinkageError(); } diff --git a/approximations/src/main/java/stub/java/util/list/ListIteratorStub.java b/approximations/src/main/java/stub/java/util/list/ListIteratorStub.java index 79bb2ea1..33331294 100644 --- a/approximations/src/main/java/stub/java/util/list/ListIteratorStub.java +++ b/approximations/src/main/java/stub/java/util/list/ListIteratorStub.java @@ -17,7 +17,7 @@ public ListIteratorStub(AbstractListImpl list, int index, int expectedModCoun } public ListIteratorStub(AbstractListImpl list, int index) { - this(list, index, list.modCount); + this(list, index, list._getModCount()); throw new LinkageError(); } diff --git a/approximations/src/main/java/stub/java/util/map/Map_Contents.java b/approximations/src/main/java/stub/java/util/map/Map_Contents.java index e59fe8b9..aff2dfb6 100644 --- a/approximations/src/main/java/stub/java/util/map/Map_Contents.java +++ b/approximations/src/main/java/stub/java/util/map/Map_Contents.java @@ -91,7 +91,7 @@ public boolean retainAll(@NotNull Collection c) { throw new LinkageError(); } - public int size() { + public int _size() { throw new LinkageError(); } @@ -117,7 +117,7 @@ public T[] toArray(@NotNull T[] array) { throw new LinkageError(); } - public String toString() { + public String _toString() { throw new LinkageError(); } } diff --git a/usvm-api/usvm-api.jar b/usvm-api/usvm-api.jar deleted file mode 100644 index fb9607f8..00000000 Binary files a/usvm-api/usvm-api.jar and /dev/null differ diff --git a/usvm-api/usvm-jvm-api.jar b/usvm-api/usvm-jvm-api.jar new file mode 100644 index 00000000..ab191534 Binary files /dev/null and b/usvm-api/usvm-jvm-api.jar differ