Adds TreeSet approximation

approximations/src/main/java/decoders/java/util/TreeSet_Decoder.java

@@ -0,0 +1,138 @@
+package decoders.java.util;
+
+import org.jacodb.api.jvm.*;
+import org.usvm.api.SymbolicMap;
+import org.usvm.api.decoder.DecoderApi;
+import org.usvm.api.decoder.DecoderFor;
+import org.usvm.api.decoder.ObjectData;
+import org.usvm.api.decoder.ObjectDecoder;
+
+import java.util.ArrayList;
+import java.util.List;
+import java.util.TreeSet;
+
+import static org.usvm.api.decoder.DecoderUtils.findStorageField;
+
+@DecoderFor(TreeSet.class)
+public final class TreeSet_Decoder implements ObjectDecoder {
+    private volatile JcMethod[] cachedMethods = null;
+    private volatile JcMethod cached_TreeSet_ctor = null;
+    private volatile JcMethod cached_TreeSet_add = null;
+    private volatile JcField cached_TreeSet_storage = null;
+    private volatile JcField cached_Map_map = null;
+    private volatile JcField cached_HashMapContainer_map = null;
+
+    @Override
+    public <T> T createInstance(final JcClassOrInterface approximation,
+                                final ObjectData<T> approximationData,
+                                final DecoderApi<T> decoder) {
+        JcMethod ctor = cached_TreeSet_ctor;
+        // TODO: add synchronization if needed
+        if (ctor == null) {
+            final List<JcMethod> 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<JcParameter> params = m.getParameters();
+                    if (!params.isEmpty()) continue;
+                    cached_TreeSet_ctor = ctor = m;
+                    break;
+                }
+            }
+        }
+
+        final List<T> args = new ArrayList<>();
+        return decoder.invokeMethod(ctor, args);
+    }
+
+    @Override
+    public <T> void initializeInstance(final JcClassOrInterface approximation,
+                                       final ObjectData<T> approximationData,
+                                       final T outputInstance,
+                                       final DecoderApi<T> decoder) {
+        JcField f_ts_storage = cached_TreeSet_storage;
+        // TODO: add synchronization if needed
+        if (f_ts_storage == null) {
+            cached_TreeSet_storage = f_ts_storage = findStorageField(approximation);
+        }
+
+        final ObjectData<T> storageData = approximationData.getObjectField(f_ts_storage);
+        if (storageData == null)
+            return;
+
+        JcMethod m_add = cached_TreeSet_add;
+        // TODO: add synchronization if needed
+        if (m_add == null) {
+            final JcMethod[] methods = cachedMethods;
+            for (int i = 0, c = methods.length; i != c; i++) {
+                JcMethod m = methods[i];
+
+                if (!"add".equals(m.getName())) continue;
+                List<JcParameter> params = m.getParameters();
+                if (params.size() != 1) continue;
+                if (!"java.lang.Object".equals(params.get(0).getType().getTypeName())) continue;
+
+                m_add = m;
+                break;
+            }
+            cached_TreeSet_add = m_add;
+        }
+
+        JcField f_m_map = cached_Map_map;
+        // TODO: add synchronization if needed
+        if (f_m_map == null) {
+            JcClasspath cp = approximation.getClasspath();
+            {
+                List<JcField> 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<JcField> 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;
+                    }
+                }
+            }
+        }
+
+        final ObjectData<T> rtMapContainerData = storageData.getObjectField(f_m_map);
+        if (rtMapContainerData == null)
+            return;
+
+        final SymbolicMap<T, T> map = rtMapContainerData.decodeSymbolicMapField(cached_HashMapContainer_map);
+        if (map == null)
+            return;
+
+        int length = map.size();
+        if (length == Integer.MAX_VALUE)
+            return;
+
+        while (length > 0) {
+            T key = map.anyKey();
+
+            List<T> args = new ArrayList<>();
+            args.add(outputInstance);
+            args.add(key);
+            decoder.invokeMethod(m_add, args);
+
+            map.remove(key);
+            length--;
+        }
+    }
+}

approximations/src/main/java/encoders/java/util/TreeSet_Encoder.java

@@ -0,0 +1,19 @@
+package encoders.java.util;
+
+import generated.java.util.set.TreeSetImpl;
+import org.usvm.api.encoder.EncoderFor;
+import org.usvm.api.encoder.ObjectEncoder;
+
+import java.util.Set;
+import java.util.TreeSet;
+
+@EncoderFor(TreeSet.class)
+public class TreeSet_Encoder implements ObjectEncoder {
+
+    @Override
+    @SuppressWarnings("unchecked")
+    public Object encode(Object object) {
+        Set<Object> set = (Set<Object>) object;
+        return new TreeSetImpl<>(set);
+    }
+}

approximations/src/main/java/generated/java/util/set/TreeSetImpl.java

@@ -0,0 +1,163 @@
+package generated.java.util.set;
+
+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;
+import java.util.Collection;
+import java.util.Iterator;
+import java.util.Spliterator;
+import java.util.TreeSet;
+import java.util.function.Consumer;
+import java.util.function.IntFunction;
+import java.util.function.Predicate;
+import java.util.stream.Stream;
+
+@Approximate(TreeSet.class)
+public class TreeSetImpl<E> extends AbstractSetImpl<E> implements Cloneable, Serializable {
+
+    @Serial
+    private static final long serialVersionUID = -2479143000061671589L;
+
+    private LibSLRuntime.Map<E, Object> storage;
+
+    private int modCount;
+
+    static {
+        Engine.assume(true);
+    }
+
+    public TreeSetImpl() {
+        super(true);
+    }
+
+    public TreeSetImpl(Collection<? extends E> c) {
+        super(true, c);
+    }
+
+    public TreeSetImpl(int initialCapacity) {
+        super(true, initialCapacity);
+    }
+
+    public TreeSetImpl(int initialCapacity, float loadFactor) {
+        super(true, initialCapacity, loadFactor);
+    }
+
+    @SuppressWarnings("unused")
+    private TreeSetImpl(int initialCapacity, float loadFactor, boolean dummy) {
+        super(initialCapacity, loadFactor, dummy);
+    }
+
+    public LibSLRuntime.Map<E, Object> _getStorage() {
+        LibSLRuntime.Map<E, Object> storage = this.storage;
+        Engine.assume(storage != null);
+        return storage;
+    }
+
+    public void _setStorage(LibSLRuntime.Map<E, Object> 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 e) { return super._add(e); }
+
+    public void clear() { super._clear(); }
+
+    @SuppressWarnings("MethodDoesntCallSuperMethod")
+    public Object clone() throws CloneNotSupportedException {
+        return super._clone();
+    }
+
+    public boolean contains(Object obj) {
+        return super._contains(obj);
+    }
+
+    public boolean isEmpty() {
+        return super._isEmpty();
+    }
+
+    @NotNull
+    public Iterator<E> iterator() {
+        return super._iterator();
+    }
+
+    public boolean remove(Object elem) {
+        return super._remove(elem);
+    }
+
+    public int size() {
+        return super._size();
+    }
+
+    @NotNull
+    public Spliterator<E> spliterator() {
+        return super._spliterator();
+    }
+
+    @SuppressWarnings("EqualsDoesntCheckParameterClass")
+    public boolean equals(Object other) {
+        return Engine.typeIs(other, TreeSetImpl.class) && super._equals(other);
+    }
+
+    public int hashCode() {
+        return super._hashCode();
+    }
+
+    public boolean removeAll(@NotNull Collection<?> c) {
+        return super._removeAll(c);
+    }
+
+    @NotNull
+    public Object[] toArray() {
+        return super._toArray();
+    }
+
+    @NotNull
+    public <T> T[] toArray(@NotNull T[] a) {
+        return super._toArray(a);
+    }
+
+    public <T> T[] toArray(@NotNull IntFunction<T[]> generator) {
+        return super._toArray(generator);
+    }
+
+    public boolean containsAll(@NotNull Collection<?> c) {
+        return super._containsAll(c);
+    }
+
+    public boolean addAll(@NotNull Collection<? extends E> c) {
+        return super._addAll(c);
+    }
+
+    public boolean retainAll(@NotNull Collection<?> c) {
+        return super._retainAll(c);
+    }
+
+    public boolean removeIf(@NotNull Predicate<? super E> filter) {
+        return super._removeIf(filter);
+    }
+
+    public void forEach(Consumer<? super E> userAction) {
+        super._forEach(userAction);
+    }
+
+    @NotNull
+    public Stream<E> stream() {
+        return super._stream();
+    }
+
+    @NotNull
+    public Stream<E> parallelStream() {
+        return super._parallelStream();
+    }
+
+    public String toString() {
+        return super._toString();
+    }
+}