Model JDK container calls and System.arraycopy; containers holding symbolic values count as symbolic

symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java

@@ -21,6 +21,8 @@
 import de.uzl.its.swat.symbolic.shadow.Frame;
 import de.uzl.its.swat.symbolic.shadow.ShadowContext;
 import de.uzl.its.swat.symbolic.trace.SymbolicTraceHandler;
+import de.uzl.its.swat.symbolic.value.ContainerPlaceHolder;
+import de.uzl.its.swat.symbolic.invoke.java.util.CollectionInvocation;
 import de.uzl.its.swat.symbolic.value.PlaceHolder;
 import de.uzl.its.swat.symbolic.value.Value;
 import de.uzl.its.swat.symbolic.value.ValueFactory;
@@ -1350,7 +1352,11 @@ public void visitGETVALUE_Object(GETVALUE_Object<?> inst) throws SymbolicInstruc
                 stack.pushOperand(ValueFactory.getLambdaObjectValue(inst.v, parentAddress, key));
             } else */
 
-            if (peek instanceof PlaceHolder placeHolder) {
+            if (peek instanceof ContainerPlaceHolder containerPlaceHolder) {
+                stack.popOperand();
+                stack.pushOperand(CollectionInvocation.resolve(
+                        containerPlaceHolder, inst.val, inst.address, stack, symbolicTraceHandler));
+            } else if (peek instanceof PlaceHolder placeHolder) {
 
                 // remove the placeholder value
                 stack.popOperand();

symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/InvocationHandler.java

@@ -7,6 +7,7 @@
 import de.uzl.its.swat.common.exceptions.ValueConversionException;
 import de.uzl.its.swat.common.logging.GlobalLogger;
 import de.uzl.its.swat.common.logging.records.InvocationEntry;
+import de.uzl.its.swat.symbolic.invoke.java.util.CollectionInvocation;
 import de.uzl.its.swat.symbolic.trace.SymbolicTraceHandler;
 import de.uzl.its.swat.symbolic.value.PlaceHolder;
 import de.uzl.its.swat.symbolic.value.Value;
@@ -67,6 +68,13 @@ private static boolean hasSymbolicElement(Value<?, ?> v) throws NotImplementedEx
         Type[] types = Type.getArgumentTypes(desc);
         logger.trace("Invoking method {} in class {} with arguments {}", name, owner, arguments);
 
+        // JDK containers: modelled calls only move references, see CollectionInvocation
+        Value<?, ?> containerResult = CollectionInvocation.invoke(
+                owner, name, desc, arguments.toArray(new Value[0]), isInstance, instance, invokeId);
+        if (containerResult != null) {
+            return containerResult;
+        }
+
         // We do that first to include the pointer in instance invocation cases
         boolean containsSymbolicArgument = arguments.stream().anyMatch(v -> {
             try {

symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/StaticInvocation.java

@@ -15,6 +15,7 @@
 import de.uzl.its.swat.symbolic.invoke.java.lang.MathInvocation;
 import de.uzl.its.swat.symbolic.invoke.java.lang.ShortInvocation;
 import de.uzl.its.swat.symbolic.invoke.java.lang.StringInvocation;
+import de.uzl.its.swat.symbolic.invoke.java.lang.SystemInvocation;
 import de.uzl.its.swat.symbolic.invoke.java.util.ObjectsInvocation;
 import de.uzl.its.swat.symbolic.trace.SymbolicTraceHandler;
 import de.uzl.its.swat.symbolic.value.PlaceHolder;
@@ -53,6 +54,7 @@ public final class StaticInvocation {
                             name, args, desc, symbolicStateHandler);
                     case "java/lang/Double" -> DoubleInvocation.invokeStaticMethod(
                             name, args, desc, symbolicStateHandler);
+                    case "java/lang/System" -> SystemInvocation.invokeStaticMethod(name, args, desc);
                     case "java/util/Objects" -> ObjectsInvocation.invokeStaticMethod(
                             name, args, desc, symbolicStateHandler);
                     default -> PlaceHolder.instance;

symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/SystemInvocation.java

@@ -0,0 +1,87 @@
+package de.uzl.its.swat.symbolic.invoke.java.lang;
+
+import de.uzl.its.swat.common.exceptions.NotImplementedException;
+import de.uzl.its.swat.symbolic.value.PlaceHolder;
+import de.uzl.its.swat.symbolic.value.Value;
+import de.uzl.its.swat.symbolic.value.VoidValue;
+import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.IntValue;
+import de.uzl.its.swat.symbolic.value.reference.array.AbstractArrayValue;
+import de.uzl.its.swat.symbolic.value.reference.array.ArrayArrayValue;
+import de.uzl.its.swat.symbolic.value.reference.array.ObjectArrayValue;
+import java.lang.reflect.Array;
+import org.objectweb.asm.Type;
+
+public final class SystemInvocation {
+
+    /** Longer copies are not modelled: each element adds a store to the array formula. */
+    static final int MAX_ARRAYCOPY_LENGTH = 4096;
+
+    private SystemInvocation() {}
+
+    public static Value<?, ?> invokeStaticMethod(String name, Value<?, ?>[] args, Type[] desc)
+            throws NotImplementedException {
+        if (name.equals("arraycopy") && args.length == 5) {
+            return invokeArraycopy(args);
+        }
+        return PlaceHolder.instance;
+    }
+
+    /**
+     * {@code System.arraycopy(src, srcPos, dest, destPos, length)} with concrete positions and
+     * length: the shadow elements are copied as the JVM copies the elements, as if through a
+     * temporary array. The model runs after the concrete call returned, so the arguments were
+     * valid.
+     */
+    @SuppressWarnings({"unchecked", "rawtypes"})
+    private static Value<?, ?> invokeArraycopy(Value<?, ?>[] args) throws NotImplementedException {
+        for (int i : new int[] {1, 3, 4}) {
+            if (!(args[i] instanceof IntValue) || args[i].isSymbolic()) return PlaceHolder.instance;
+        }
+        int srcPos = ((IntValue) args[1]).concrete;
+        int destPos = ((IntValue) args[3]).concrete;
+        int length = ((IntValue) args[4]).concrete;
+        if (length < 0 || length > MAX_ARRAYCOPY_LENGTH) {
+            return PlaceHolder.instance;
+        }
+        Value<?, ?> src = args[0];
+        Value<?, ?> dest = args[2];
+
+        if (src instanceof ObjectArrayValue s && dest instanceof ObjectArrayValue d) {
+            Value<?, ?>[] from = s.getFields();
+            Value<?, ?>[] to = d.getFields();
+            if (from == null || to == null || srcPos + length > from.length || destPos + length > to.length) {
+                return PlaceHolder.instance;
+            }
+            System.arraycopy(from, srcPos, to, destPos, length);
+            return VoidValue.instance;
+        }
+
+        if (!(src instanceof AbstractArrayValue s) || !(dest instanceof AbstractArrayValue d)
+                || src.getClass() != dest.getClass() || src instanceof ArrayArrayValue<?>) {
+            return PlaceHolder.instance;
+        }
+        if (s.concrete == null || d.concrete == null
+                || srcPos + length > Array.getLength(s.concrete) || destPos + length > Array.getLength(d.concrete)) {
+            return PlaceHolder.instance;
+        }
+        // The shadow of an array seen through GETVALUE keeps the real array as its concrete value,
+        // which the call has already updated; its concrete values must not be written again.
+        boolean destIsLive = System.identityHashCode(d.concrete) == d.getAddress();
+        Object liveValues = null;
+        if (destIsLive) {
+            liveValues = Array.newInstance(d.concrete.getClass().getComponentType(), length);
+            System.arraycopy(d.concrete, destPos, liveValues, 0, length);
+        }
+        Value<?, ?>[] elements = new Value[length];
+        for (int k = 0; k < length; k++) {
+            elements[k] = s.getElement(new IntValue(s.getContext(), srcPos + k));
+        }
+        for (int k = 0; k < length; k++) {
+            d.storeElement(new IntValue(d.getContext(), destPos + k), elements[k]);
+        }
+        if (destIsLive) {
+            System.arraycopy(liveValues, 0, d.concrete, destPos, length);
+        }
+        return VoidValue.instance;
+    }
+}