Tests for collections and bug fixes of approximations

approximations/build.gradle.kts

@@ -1,20 +1,26 @@
 plugins {
     java
     `maven-publish`
+    id("org.springframework.boot") version "3.2.0" apply false
 }
 
 repositories {
     mavenCentral()
     maven("https://jitpack.io")
 }
 
-private val jacodbPackage = "com.github.UnitTestBot.jacodb"
-private val jacodbVersion = "890624770b" // jacodb neo branch
+private val jacodbPackage = "org.jacodb"
+private val jacodbVersion = "00164e304b" // 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")
+    // Fixes "unknown enum constant 'When.MAYBE'" warning
+    compileOnly("com.google.code.findbugs:jsr305:3.0.2")
 }
 
 group = "org.usvm.approximations.java.stdlib"
@@ -28,6 +34,8 @@ tasks.withType<JavaCompile> {
     options.compilerArgs.add("-source")
     options.compilerArgs.add("1.8")
     options.compilerArgs.add("-Xlint:unchecked")
+    options.compilerArgs.add("-Xlint:all")
+    options.compilerArgs.add("-Werror")
 }
 
 publishing {

approximations/src/main/java/decoders/java/lang/SecurityManager_Decoder.java

@@ -10,7 +10,7 @@
 import java.util.Collections;
 import java.util.List;
 
-@SuppressWarnings("ForLoopReplaceableByForEach")
+@SuppressWarnings({"ForLoopReplaceableByForEach", "removal"})
 @DecoderFor(SecurityManager.class)
 public final class SecurityManager_Decoder implements ObjectDecoder {
     private volatile JcMethod cached_SecurityManager_ctor = null;

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

@@ -46,7 +46,7 @@ public <T> T createInstance(final JcClassOrInterface approx,
 
                         List<JcParameter> params = m.getParameters();
                         if (params.size() != 1) continue;
-                        if (!"java.lang.Object".equals(params.get(0).getType().getTypeName())) continue;
+                        //if (!"java.lang.Object".equals(params.get(0).getType().getTypeName())) continue;
 
                         cached_ArrayList_add = m_add = m;
                     }
@@ -68,7 +68,7 @@ public <T> void initializeInstance(final JcClassOrInterface approx,
         JcField f_storage = cached_ArrayList_storage;
         // TODO: add synchronization if needed
         if (f_storage == null) {
-            final List<JcField> fields = approx.getDeclaredFields();
+            final List<JcField> fields = getAllFields(approx);
             for (int i = 0, c = fields.size(); i < c; i++) {
                 JcField f = fields.get(i);
                 if ("storage".equals(f.getName())) {
@@ -93,4 +93,21 @@ public <T> void initializeInstance(final JcClassOrInterface approx,
             decoder.invokeMethod(cached_ArrayList_add, args);
         }
     }
+
+    public List<JcField> getAllFields(JcClassOrInterface type) {
+        List<JcClassOrInterface> typesToCheck = new ArrayList<>();
+        typesToCheck.add(type);
+        List<JcField> allFields = new ArrayList<>();
+        while (!typesToCheck.isEmpty()) {
+            int lastIndex = typesToCheck.size() - 1;
+            JcClassOrInterface current = typesToCheck.remove(lastIndex);
+            allFields.addAll(current.getDeclaredFields());
+
+            JcClassOrInterface superClass = current.getSuperClass();
+            if (superClass != null) {
+                typesToCheck.add(superClass);
+            }
+        }
+        return allFields;
+    }
 }

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

@@ -153,7 +153,7 @@ public <T> void initializeInstance(final JcClassOrInterface approximation,
             decoder.invokeMethod(m_add, args);
 
             map.remove(key);
-            length -= 1;
+            length--;
         }
     }
 }

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

@@ -153,7 +153,7 @@ public <T> void initializeInstance(final JcClassOrInterface approximation,
             decoder.invokeMethod(m_add, args);
 
             map.remove(key);
-            length -= 1;
+            length--;
         }
     }
 }

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

@@ -35,7 +35,7 @@ public <T> T createInstance(final JcClassOrInterface approximation,
 
                 if ("value".equals(name)) {
                     f_value = f;
-                } else if ("present".equals(name)) {
+                } else if ("isPresent".equals(name)) {
                     f_present = f;
                 }
 
@@ -92,4 +92,4 @@ public <T> void initializeInstance(final JcClassOrInterface approximation,
                                        final DecoderApi<T> decoder) {
         // nothing
     }
-}
+}

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

@@ -36,7 +36,7 @@ public <T> T createInstance(final JcClassOrInterface approx,
                 // NOTE: this is an example on how to join discovery process for multiple targets
                 if ("value".equals(name)) {
                     f_value = f;
-                } else if ("present".equals(name)) {
+                } else if ("isPresent".equals(name)) {
                     f_present = f;
                 }
                 if (f_value != null && f_present != null)

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

@@ -35,7 +35,7 @@ public <T> T createInstance(final JcClassOrInterface approx,
 
                 if ("value".equals(name)) {
                     f_value = f;
-                } else if ("present".equals(name)) {
+                } else if ("isPresent".equals(name)) {
                     f_present = f;
                 }
 

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

@@ -0,0 +1,17 @@
+package encoders.java.util;
+
+import generated.java.util.map.AbstractMap_EntryImpl;
+import org.usvm.api.encoder.EncoderFor;
+import org.usvm.api.encoder.ObjectEncoder;
+import stub.java.util.map.AbstractMap_Entry;
+
+import java.util.Map;
+
+@EncoderFor(AbstractMap_Entry.class)
+public class AbstractMap_Entry_Encoder implements ObjectEncoder {
+
+    @Override
+    public Object encode(Object list) {
+        return new AbstractMap_EntryImpl<>((Map.Entry<?, ?>) list);
+    }
+}

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

@@ -0,0 +1,18 @@
+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.ArrayList;
+
+@EncoderFor(ArrayList.class)
+public class ArrayList_Encoder implements ObjectEncoder {
+
+    @Override
+    public Object encode(Object list) {
+        ArrayListImpl<Object> result = new ArrayListImpl<>();
+        result.addAll(((ArrayList<?>) list).stream().toList());
+        return result;
+    }
+}

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

@@ -0,0 +1,18 @@
+package encoders.java.util;
+
+import generated.java.util.map.ConcurrentHashMapImpl;
+import org.usvm.api.encoder.EncoderFor;
+import org.usvm.api.encoder.ObjectEncoder;
+
+import java.util.concurrent.ConcurrentHashMap;
+
+@EncoderFor(ConcurrentHashMap.class)
+public class ConcurrentHashMap_Encoder implements ObjectEncoder {
+
+    @SuppressWarnings("unchecked")
+    @Override
+    public Object encode(Object object) {
+        ConcurrentHashMap<Object, Object> map = (ConcurrentHashMap<Object, Object>) object;
+        return new ConcurrentHashMapImpl<>(map);
+    }
+}

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

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

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

@@ -0,0 +1,20 @@
+package encoders.java.util;
+
+import generated.java.util.set.HashSetImpl;
+import org.usvm.api.encoder.EncoderFor;
+import org.usvm.api.encoder.ObjectEncoder;
+
+import java.util.Arrays;
+import java.util.HashSet;
+import java.util.Set;
+
+@EncoderFor(HashSet.class)
+public class HashSet_Encoder implements ObjectEncoder {
+
+    @Override
+    public Object encode(Object object) {
+        HashSetImpl<Object> result = new HashSetImpl<>();
+        result.addAll(Arrays.asList(((Set<?>) object).toArray()));
+        return result;
+    }
+}

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

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

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

@@ -0,0 +1,14 @@
+package encoders.java.util;
+
+import generated.java.lang.StringImpl;
+import org.usvm.api.encoder.EncoderFor;
+import org.usvm.api.encoder.ObjectEncoder;
+
+@EncoderFor(java.lang.String.class)
+public class String_Encoder implements ObjectEncoder {
+
+    @Override
+    public Object encode(Object object) {
+        return new StringImpl(((String) object).getBytes());
+    }
+}

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

@@ -0,0 +1,14 @@
+package encoders.java.util;
+
+import generated.java.lang.ThreadLocalImpl;
+import org.usvm.api.encoder.EncoderFor;
+import org.usvm.api.encoder.ObjectEncoder;
+
+@EncoderFor(java.lang.ThreadLocal.class)
+public class ThreadLocal_Encoder implements ObjectEncoder {
+
+    @Override
+    public Object encode(Object object) {
+        return new ThreadLocalImpl<>();
+    }
+}