From c2a4c508087354cedc3c83e61c8a23265ca343f9 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 22:23:45 +0000 Subject: [PATCH 1/4] Model reference-only calls on JDK containers Calls on ArrayList, LinkedList, Vector, Stack, ArrayDeque, HashMap, LinkedHashMap and Hashtable that only store or return references (add, get, put with a concrete key, iterator, entrySet, toArray, ...) are modelled: the shadow of a stored value is kept in the container's ContainerContents, and a returned element is matched to it by address once the concrete result is known (GETVALUE_Object). Views, iterators and entries share the contents of their container. Collections.singleton, enumeration, unmodifiable* and Arrays.asList are modelled the same way. A container that may hold a symbolic value now counts as symbolic, so a call that is not modelled (contains, indexOf, sort, toString, ...) still records context loss. A returned element that cannot be matched while the container may hold a symbolic value records context loss as well. ObjectValue.isSymbolic(visited) walked fields only, so a String, boxed value or primitive array held in a field never counted as symbolic; it now uses the value's own isSymbolic(). Co-Authored-By: Claude Opus 5.5 --- .../symbolic/SymbolicInstructionVisitor.java | 8 +- .../symbolic/invoke/InvocationHandler.java | 8 + .../java/util/CollectionInvocation.java | 416 ++++++++++++++++++ .../symbolic/value/ContainerPlaceHolder.java | 50 +++ .../value/reference/ContainerContents.java | 220 +++++++++ .../symbolic/value/reference/ObjectValue.java | 21 + 6 files changed, 722 insertions(+), 1 deletion(-) create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/util/CollectionInvocation.java create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/ContainerPlaceHolder.java create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/ContainerContents.java diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java index 771f7759..2df5873c 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/SymbolicInstructionVisitor.java +++ b/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(); diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/InvocationHandler.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/InvocationHandler.java index d89f7cc2..c755833d 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/InvocationHandler.java +++ b/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 { diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/util/CollectionInvocation.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/util/CollectionInvocation.java new file mode 100644 index 00000000..9647eb0d --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/util/CollectionInvocation.java @@ -0,0 +1,416 @@ +package de.uzl.its.swat.symbolic.invoke.java.util; + +import ch.qos.logback.classic.Logger; +import de.uzl.its.swat.common.exceptions.NoThreadContextException; +import de.uzl.its.swat.common.exceptions.NotImplementedException; +import de.uzl.its.swat.common.logging.GlobalLogger; +import de.uzl.its.swat.common.logging.records.InvocationEntry; +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.value.ContainerPlaceHolder.Result; +import de.uzl.its.swat.symbolic.value.PlaceHolder; +import de.uzl.its.swat.symbolic.value.Value; +import de.uzl.its.swat.symbolic.value.ValueFactory; +import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.IntValue; +import de.uzl.its.swat.symbolic.value.reference.ContainerContents; +import de.uzl.its.swat.symbolic.value.reference.ContainerContents.Kind; +import de.uzl.its.swat.symbolic.value.reference.ObjectValue; +import de.uzl.its.swat.symbolic.value.reference.array.AbstractArrayValue; +import de.uzl.its.swat.symbolic.value.reference.array.ObjectArrayValue; +import de.uzl.its.swat.symbolic.value.reference.lang.BoxedValue; +import de.uzl.its.swat.symbolic.value.reference.lang.StringValue; +import de.uzl.its.swat.thread.ThreadHandler; +import java.util.HashMap; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +/** + * Models of JDK containers ({@code java.util} lists, deques and hash maps, their views and + * iterators, and a few {@code Collections}/{@code Arrays} factories) that only move references: + * storing an element, copying a container, returning an element, a view or an iterator. + * + *

The concrete call still runs; the model records the shadow of what goes in (the {@link + * ContainerContents} of the container's shadow) and, for a call that returns a reference, picks + * the shadow of what comes out when the concrete result is known ({@link #resolve}). A call that + * inspects the elements ({@code contains}, {@code indexOf}, {@code remove(Object)}, sorting, + * {@code equals}, {@code hashCode}, {@code toString}, streams, ...) is not modelled: a container + * holding a symbolic value counts as symbolic, so such a call records context loss as before. + * + *

Hashed parts are modelled only while they are concrete: a map key must not be symbolic, and a + * map whose stored keys have become symbolic is not modelled any more. Index arguments must be + * concrete too. Anything else falls back to the generic handling of a missing invocation. + */ +public final class CollectionInvocation { + private static final Logger logger = GlobalLogger.getSymbolicExecutionLogger(); + + /** The JDK classes whose shadow tracks contents, with the calls modelled on them. */ + private static final Map KIND_BY_CLASS = new HashMap<>(); + + static { + for (String c : List.of("ArrayList", "LinkedList", "Vector", "Stack", "ArrayDeque")) { + KIND_BY_CLASS.put("java/util/" + c, Kind.LIST); + } + for (String c : List.of("HashMap", "LinkedHashMap", "Hashtable")) { + KIND_BY_CLASS.put("java/util/" + c, Kind.MAP); + } + } + + private enum Op { + INIT, // a new, empty container + STORE, // stores argument `arg` (lists) or the value `arg` under key `key` (maps) + COPY, // stores what the container in argument `arg` holds + ELEMENT, // returns an element + STORE_ELEMENT, // STORE, then returns an element (set, put, Stack.push) + VIEW, // returns a view or iterator of the container + ARRAY, // returns a new Object[] with the elements + PLAIN // returns a primitive or nothing and only depends on concrete state + } + + /** + * @param op what the call does + * @param arg the argument stored or copied, -1 for none + * @param key the map-key argument, which must be concrete, -1 for none + * @param initFirst whether the call is a constructor that starts with empty contents + */ + private record Model(Op op, int arg, int key, boolean initFirst) {} + + private static final Map LIST = new HashMap<>(); + private static final Map MAP = new HashMap<>(); + private static final Map VIEW = new HashMap<>(); + + private static void put(Map table, Op op, int arg, int key, String... sigs) { + for (String sig : sigs) table.put(sig, new Model(op, arg, key, sig.startsWith(""))); + } + + static { + put(LIST, Op.INIT, -1, -1, "()V", "(I)V"); + put(LIST, Op.COPY, 0, -1, "(Ljava/util/Collection;)V", "addAll(Ljava/util/Collection;)Z"); + put(LIST, Op.COPY, 1, -1, "addAll(ILjava/util/Collection;)Z"); + put(LIST, Op.STORE, 0, -1, + "add(Ljava/lang/Object;)Z", "addLast(Ljava/lang/Object;)V", "addFirst(Ljava/lang/Object;)V", + "offer(Ljava/lang/Object;)Z", "offerLast(Ljava/lang/Object;)Z", "offerFirst(Ljava/lang/Object;)Z", + "push(Ljava/lang/Object;)V", "addElement(Ljava/lang/Object;)V", + "insertElementAt(Ljava/lang/Object;I)V", "setElementAt(Ljava/lang/Object;I)V"); + put(LIST, Op.STORE, 1, -1, "add(ILjava/lang/Object;)V"); + put(LIST, Op.STORE_ELEMENT, 1, -1, "set(ILjava/lang/Object;)Ljava/lang/Object;"); + put(LIST, Op.STORE_ELEMENT, 0, -1, "push(Ljava/lang/Object;)Ljava/lang/Object;"); + put(LIST, Op.ELEMENT, -1, -1, + "get(I)Ljava/lang/Object;", "getFirst()Ljava/lang/Object;", "getLast()Ljava/lang/Object;", + "element()Ljava/lang/Object;", "peek()Ljava/lang/Object;", "peekFirst()Ljava/lang/Object;", + "peekLast()Ljava/lang/Object;", "poll()Ljava/lang/Object;", "pollFirst()Ljava/lang/Object;", + "pollLast()Ljava/lang/Object;", "pop()Ljava/lang/Object;", "remove()Ljava/lang/Object;", + "remove(I)Ljava/lang/Object;", "removeFirst()Ljava/lang/Object;", "removeLast()Ljava/lang/Object;", + "firstElement()Ljava/lang/Object;", "lastElement()Ljava/lang/Object;", + "elementAt(I)Ljava/lang/Object;"); + put(LIST, Op.VIEW, -1, -1, + "iterator()Ljava/util/Iterator;", "listIterator()Ljava/util/ListIterator;", + "listIterator(I)Ljava/util/ListIterator;", "descendingIterator()Ljava/util/Iterator;", + "elements()Ljava/util/Enumeration;", "subList(II)Ljava/util/List;"); + put(LIST, Op.ARRAY, -1, -1, "toArray()[Ljava/lang/Object;"); + put(LIST, Op.PLAIN, -1, -1, + "size()I", "isEmpty()Z", "clear()V", "trimToSize()V", "ensureCapacity(I)V"); + + put(MAP, Op.INIT, -1, -1, "()V", "(I)V", "(IF)V"); + put(MAP, Op.COPY, 0, -1, "(Ljava/util/Map;)V", "putAll(Ljava/util/Map;)V"); + put(MAP, Op.STORE_ELEMENT, 1, 0, + "put(Ljava/lang/Object;Ljava/lang/Object;)Ljava/lang/Object;", + "putIfAbsent(Ljava/lang/Object;Ljava/lang/Object;)Ljava/lang/Object;"); + put(MAP, Op.ELEMENT, -1, 0, + "get(Ljava/lang/Object;)Ljava/lang/Object;", "remove(Ljava/lang/Object;)Ljava/lang/Object;", + "getOrDefault(Ljava/lang/Object;Ljava/lang/Object;)Ljava/lang/Object;"); + put(MAP, Op.PLAIN, -1, 0, "containsKey(Ljava/lang/Object;)Z"); + put(MAP, Op.VIEW, -1, -1, + "keySet()Ljava/util/Set;", "values()Ljava/util/Collection;", "entrySet()Ljava/util/Set;", + "keys()Ljava/util/Enumeration;", "elements()Ljava/util/Enumeration;"); + put(MAP, Op.PLAIN, -1, -1, "size()I", "isEmpty()Z", "clear()V"); + + put(VIEW, Op.PLAIN, -1, -1, + "hasNext()Z", "hasMoreElements()Z", "hasPrevious()Z", "nextIndex()I", "previousIndex()I", + "size()I", "isEmpty()Z", "remove()V"); + put(VIEW, Op.ELEMENT, -1, -1, + "next()Ljava/lang/Object;", "nextElement()Ljava/lang/Object;", "previous()Ljava/lang/Object;", + "getKey()Ljava/lang/Object;", "getValue()Ljava/lang/Object;", "get(I)Ljava/lang/Object;"); + put(VIEW, Op.VIEW, -1, -1, "iterator()Ljava/util/Iterator;", "listIterator()Ljava/util/ListIterator;"); + put(VIEW, Op.ARRAY, -1, -1, "toArray()[Ljava/lang/Object;"); + } + + private CollectionInvocation() {} + + /** + * Applies the model of a call that was not instrumented. + * + * @return the return value of the call, or {@code null} if the call is not modelled + */ + public static Value invoke( + String owner, + String name, + String desc, + Value[] args, + boolean isInstance, + ObjectValue instance, + long invokeId) throws NotImplementedException { + if (isInstance) { + if (instance == null || instance.isNullValue()) { + return null; + } + ContainerContents contents = instance.getContents(); + Kind kind = contents != null ? contents.kind : kindOf(instance); + if (kind == null) { + return null; + } + Model model = (switch (kind) { + case LIST -> LIST; + case MAP -> MAP; + case VIEW -> VIEW; + }).get(name + desc); + if (model == null) { + return null; + } + return apply(model, kind, owner, name, desc, args, instance, invokeId); + } + if (owner.equals("java/util/Collections") || owner.equals("java/util/Arrays")) { + return invokeStatic(owner, name, desc, args, invokeId); + } + return null; + } + + private static Kind kindOf(ObjectValue instance) { + if (instance.className == null || instance instanceof AbstractArrayValue) { + return null; + } + return KIND_BY_CLASS.get(instance.className.replace('.', '/')); + } + + private static Value apply( + Model model, + Kind kind, + String owner, + String name, + String desc, + Value[] args, + ObjectValue instance, + long invokeId) throws NotImplementedException { + // Every argument the model does not store must be concrete: indices, sizes, keys + for (int i = 0; i < args.length; i++) { + if (i != model.arg() && args[i].isSymbolic()) { + return null; + } + } + ContainerContents contents = instance.getContents(); + if (model.initFirst() || contents == null) { + contents = new ContainerContents(kind); + } + if (kind == Kind.MAP && contents.keysSymbolic(new HashSet<>())) { + return null; + } + Value stored = model.arg() >= 0 ? args[model.arg()] : null; + if (model.op() == Op.COPY) { + ContainerContents source = sourceOf(stored, kind == Kind.MAP); + if (source == null) { + return null; + } + contents.addSource(source); + } + if (model.op() == Op.STORE || model.op() == Op.STORE_ELEMENT) { + if (model.key() >= 0) { + contents.addKey(args[model.key()]); + } + contents.addValue(stored); + } + instance.setContents(contents); + InvocationEntry call = new InvocationEntry(owner, name, desc, true, invokeId, true); + logger.debug("Modelled container call {}.{}{} on {}", owner, name, desc, instance); + return switch (model.op()) { + case INIT, STORE, COPY, PLAIN -> PlaceHolder.instance; + case ELEMENT, STORE_ELEMENT -> { + if (contents.kind == Kind.VIEW && contents.yieldsEntries && !name.startsWith("get")) { + yield new ContainerPlaceHolder(Result.VIEW, contents, false, List.of(), call); + } + List> candidates = + name.equals("getOrDefault") || name.equals("push") ? List.of(args[args.length - 1]) : List.of(); + yield new ContainerPlaceHolder(Result.ELEMENT, contents, false, candidates, call); + } + case VIEW -> new ContainerPlaceHolder( + Result.VIEW, contents, name.equals("entrySet") || contents.yieldsEntries, List.of(), call); + case ARRAY -> new ContainerPlaceHolder(Result.ARRAY, contents, false, List.of(), call); + }; + } + + private static Value invokeStatic(String owner, String name, String desc, Value[] args, long invokeId) + throws NotImplementedException { + InvocationEntry call = new InvocationEntry(owner, name, desc, false, invokeId, true); + if (owner.equals("java/util/Arrays")) { + if (name.equals("asList") && desc.equals("([Ljava/lang/Object;)Ljava/util/List;") + && args[0] instanceof ObjectArrayValue array) { + ContainerContents view = new ContainerContents(Kind.VIEW); + view.addSource(array); + return new ContainerPlaceHolder(Result.VIEW, view, false, List.of(), call); + } + return null; + } + switch (name + desc) { + case "singleton(Ljava/lang/Object;)Ljava/util/Set;", + "singletonList(Ljava/lang/Object;)Ljava/util/List;" -> { + ContainerContents view = new ContainerContents(Kind.VIEW); + view.addValue(args[0]); + return new ContainerPlaceHolder(Result.VIEW, view, false, List.of(), call); + } + case "enumeration(Ljava/util/Collection;)Ljava/util/Enumeration;", + "unmodifiableCollection(Ljava/util/Collection;)Ljava/util/Collection;", + "unmodifiableList(Ljava/util/List;)Ljava/util/List;", + "unmodifiableSet(Ljava/util/Set;)Ljava/util/Set;", + "unmodifiableMap(Ljava/util/Map;)Ljava/util/Map;" -> { + ContainerContents source = sourceOf(args[0], false); + if (source == null) { + return null; + } + return new ContainerPlaceHolder(Result.VIEW, source, source.yieldsEntries, List.of(), call); + } + default -> { + return null; + } + } + } + + /** + * The contents of a container argument that is copied or viewed: its recorded contents, or + * empty contents for a container that holds nothing symbolic. {@code null} (not modelled) for + * an untracked container that is symbolic, or, when the copy goes into a map, for a source that + * is not a map or whose keys may be symbolic. + */ + private static ContainerContents sourceOf(Value arg, boolean intoMap) throws NotImplementedException { + if (!(arg instanceof ObjectValue ov) || ov.isNullValue()) { + return null; + } + ContainerContents source = ov.getContents(); + if (source == null) { + return ov.isSymbolic() ? null : new ContainerContents(Kind.VIEW); + } + if (intoMap && (source.kind != Kind.MAP || source.keysSymbolic(new HashSet<>()))) { + return null; + } + return source; + } + + /** + * Picks the shadow of the object a modelled call returned, once the concrete object is known. + * + *

+ */ + public static Value resolve( + ContainerPlaceHolder ph, + Object concrete, + int address, + ShadowContext stack, + SymbolicTraceHandler symbolicTraceHandler) throws Exception { + if (address == ObjectValue.ADDRESS_NULL || concrete == null) { + return ValueFactory.createNULLValue(); + } + switch (ph.result) { + case ELEMENT -> { + Value match = ph.contents.lookup(address); + if (match == null) { + for (Value c : ph.candidates) { + if (c instanceof ObjectValue ov && ov.getAddress() == address) match = c; + } + } + if (match != null && matches(match, concrete)) { + return match; + } + Value recovered = recover(concrete, address, stack); + if (ph.contents.isSymbolic(new HashSet<>())) { + recordContextLoss(ph.call, symbolicTraceHandler); + } + return recovered; + } + case VIEW -> { + Value recovered = recover(concrete, address, stack); + if (recovered instanceof ObjectValue ov + && !(ov instanceof StringValue) + && !(ov instanceof BoxedValue) + && !(ov instanceof AbstractArrayValue) + && !(ov instanceof ObjectArrayValue)) { + if (ov.getContents() == null) { + ov.setContents(ContainerContents.viewOf(ph.contents, ph.yieldsEntries)); + } else { + ov.getContents().addSource(ph.contents); + } + } else if (ph.contents.isSymbolic(new HashSet<>())) { + recordContextLoss(ph.call, symbolicTraceHandler); + } + return recovered; + } + case ARRAY -> { + if (!(concrete instanceof Object[] elements)) { + return recover(concrete, address, stack); + } + long threadId = Thread.currentThread().getId(); + IntValue size = new IntValue(ThreadHandler.getSolverContext(threadId), elements.length); + ObjectArrayValue array = ValueFactory.createObjectArrayValue("java/lang/Object", size); + array.setAddress(address); + boolean unmatched = false; + for (int i = 0; i < elements.length; i++) { + if (elements[i] == null) { + array.storeElement(new IntValue(size.context, i), ValueFactory.createNULLValue()); + continue; + } + Value match = ph.contents.lookup(System.identityHashCode(elements[i])); + if (match != null && matches(match, elements[i])) { + array.storeElement(new IntValue(size.context, i), match); + } else { + // left unset: read back like any element of an untracked array + unmatched = true; + } + } + if (unmatched && ph.contents.isSymbolic(new HashSet<>())) { + recordContextLoss(ph.call, symbolicTraceHandler); + } + stack.putToHeap(address, array); + return array; + } + } + return recover(concrete, address, stack); + } + + /** Whether a stored shadow can stand for the concrete object (guards against address reuse). */ + private static boolean matches(Value shadow, Object concrete) { + if (shadow instanceof StringValue s) { + return concrete instanceof String && concrete.equals(s.concrete); + } + if (shadow instanceof ObjectValue ov && ov.className != null && !(ov instanceof BoxedValue) + && !(ov instanceof AbstractArrayValue) && !(ov instanceof ObjectArrayValue)) { + return ov.className.replace('.', '/').equals(concrete.getClass().getName().replace('.', '/')); + } + return true; + } + + /** What {@code GETVALUE_Object} does for the result of an unmodelled call. */ + private static Value recover(Object concrete, int address, ShadowContext stack) throws Exception { + Value heap = stack.getFromHeap(address); + if (heap != null) { + return heap; + } + Value created = ValueFactory.createObjectValue(concrete, address); + stack.putToHeap(address, created); + return created; + } + + private static void recordContextLoss(InvocationEntry call, SymbolicTraceHandler symbolicTraceHandler) + throws NoThreadContextException { + logger.warn("Result of {}.{}{} could not be matched to a stored shadow, causes context loss", + call.owner(), call.name(), call.desc()); + symbolicTraceHandler.recordSymbolicContextLoss(); + long threadId = Thread.currentThread().getId(); + ThreadHandler.recordMissingInvocation(threadId, call); + ThreadHandler.recordContextLossInvocation(threadId, call); + } +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/ContainerPlaceHolder.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/ContainerPlaceHolder.java new file mode 100644 index 00000000..258d66f9 --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/ContainerPlaceHolder.java @@ -0,0 +1,50 @@ +package de.uzl.its.swat.symbolic.value; + +import de.uzl.its.swat.common.logging.records.InvocationEntry; +import de.uzl.its.swat.symbolic.value.reference.ContainerContents; +import java.util.List; + +/** + * The return value of a modelled call on a JDK container that returns a reference. The concrete + * object is only known when the value is read back ({@code GETVALUE_Object}); the shadow is chosen + * there, see {@code CollectionInvocation.resolve}. + */ +public class ContainerPlaceHolder extends PlaceHolder { + + public enum Result { + /** An element (or map key/value) of {@link #contents}. */ + ELEMENT, + /** A view, iterator, enumeration or entry backed by {@link #contents}. */ + VIEW, + /** A new object array holding elements of {@link #contents} ({@code toArray()}). */ + ARRAY + } + + public final Result result; + public final ContainerContents contents; + /** Whether a returned view yields map entries. */ + public final boolean yieldsEntries; + /** Arguments the call may return as they are (e.g. the default of {@code getOrDefault}). */ + public final List> candidates; + /** The call, recorded as the culprit if the result cannot be matched to a shadow. */ + public final InvocationEntry call; + + public ContainerPlaceHolder( + Result result, + ContainerContents contents, + boolean yieldsEntries, + List> candidates, + InvocationEntry call) { + super(false); + this.result = result; + this.contents = contents; + this.yieldsEntries = yieldsEntries; + this.candidates = candidates; + this.call = call; + } + + @Override + public String toString() { + return "ContainerPlaceHolder (" + result + ")"; + } +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/ContainerContents.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/ContainerContents.java new file mode 100644 index 00000000..8b4041ed --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/ContainerContents.java @@ -0,0 +1,220 @@ +package de.uzl.its.swat.symbolic.value.reference; + +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.reference.array.ObjectArrayValue; +import de.uzl.its.swat.symbolic.value.reference.lang.BoxedValue; +import de.uzl.its.swat.symbolic.value.reference.lang.StringValue; +import java.util.ArrayList; +import java.util.Collections; +import java.util.HashMap; +import java.util.IdentityHashMap; +import java.util.List; +import java.util.Map; +import java.util.Set; + +/** + * The shadow values a JDK container (a {@code java.util} collection or map, or a view, iterator or + * entry derived from one) has been given through modelled calls. A container is not instrumented, + * so its fields stay empty in the shadow; the shadow of what it holds is kept here instead. + * + *

The record only grows: removals are not tracked, so it over-approximates the contents. That + * is enough for its two uses: + * + *

    + *
  • {@link #isSymbolic} makes a container that may hold a symbolic value count as symbolic, + * so an unmodelled call that gets it still records context loss; + *
  • {@link #lookup} gives back the shadow of an element a modelled read returned, found by the + * address of the concrete object. + *
+ * + *

Contents can have sources: the contents of another container (a copy, a view) or an object + * array (the array behind {@code Arrays.asList}). Their values count as values of this container. + */ +public class ContainerContents { + + /** What the container is, which decides the calls that are modelled on it. */ + public enum Kind { + /** A list, queue or deque: elements are only stored and returned, never compared. */ + LIST, + /** A hash map: the keys are hashed and compared, the values are only stored and returned. */ + MAP, + /** A view, iterator, enumeration or map entry, or an immutable container: only read. */ + VIEW + } + + /** Marks an address under which different shadows were stored. */ + private static final Value AMBIGUOUS = new PlaceHolder(false); + + public final Kind kind; + /** Whether the elements of this view are map entries (an entry set and its iterators). */ + public final boolean yieldsEntries; + + /** Mutable shadows (objects, arrays, containers), whose symbolic state can change later. */ + private final List> mutables = new ArrayList<>(); + /** Whether a value-typed (String, boxed) element was symbolic when it was stored. */ + private boolean symbolicImmutable = false; + /** Map keys; a modelled store only accepts keys that are not symbolic. */ + private final List> keys = new ArrayList<>(); + + private final Map> byAddress = new HashMap<>(); + private final List> addressUnknown = new ArrayList<>(); + private final List sources = new ArrayList<>(); + + public ContainerContents(Kind kind) { + this(kind, false); + } + + public ContainerContents(Kind kind, boolean yieldsEntries) { + this.kind = kind; + this.yieldsEntries = yieldsEntries; + } + + /** A view of {@code source}: a read-only container that holds what the source holds. */ + public static ContainerContents viewOf(ContainerContents source, boolean yieldsEntries) { + ContainerContents view = new ContainerContents(Kind.VIEW, yieldsEntries); + view.addSource(source); + return view; + } + + public void addValue(Value value) throws NotImplementedException { + if (value == null) { + return; + } + if (isValueTyped(value)) { + symbolicImmutable = symbolicImmutable || value.isSymbolic(); + } else if (value instanceof ObjectValue ov && !ov.isNullValue()) { + mutables.add(value); + } else if (!(value instanceof ObjectValue)) { + symbolicImmutable = symbolicImmutable || value.isSymbolic(); + } + index(value); + } + + public void addKey(Value key) throws NotImplementedException { + if (key == null) { + return; + } + keys.add(key); + index(key); + } + + /** Adds the contents of another container, or the elements of an object array. */ + public void addSource(Object source) { + if (source != this && (source instanceof ContainerContents || source instanceof ObjectArrayValue)) { + for (Object s : sources) { + if (s == source) return; + } + sources.add(source); + } + } + + /** Whether a symbolic value may be stored in the container (keys included). */ + public boolean isSymbolic(Set> visited) throws NotImplementedException { + return isSymbolic(visited, Collections.newSetFromMap(new IdentityHashMap<>())); + } + + private boolean isSymbolic(Set> visited, Set seen) throws NotImplementedException { + if (!seen.add(this)) { + return false; + } + if (symbolicImmutable) { + return true; + } + for (Value v : mutables) { + if (v.isSymbolic(visited)) return true; + } + if (keysSymbolic(visited)) { + return true; + } + for (Object s : sources) { + if (s instanceof ContainerContents c && c.isSymbolic(visited, seen)) return true; + if (s instanceof ObjectArrayValue a && seen.add(a) && a.isSymbolic(visited)) return true; + } + return false; + } + + /** Whether a map key stored here (not in the sources) has become symbolic. */ + public boolean keysSymbolic(Set> visited) throws NotImplementedException { + for (Value k : keys) { + if (k.isSymbolic(visited)) return true; + } + return false; + } + + /** + * The shadow of the value with this address that was stored in the container or one of its + * sources, or {@code null} if there is none or there are several different ones. + */ + public Value lookup(int address) { + Value found = lookup(address, Collections.newSetFromMap(new IdentityHashMap<>())); + return found == AMBIGUOUS ? null : found; + } + + private Value lookup(int address, Set seen) { + if (!seen.add(this)) { + return null; + } + resolvePendingAddresses(); + Value found = byAddress.get(address); + for (Object s : sources) { + Value candidate = null; + if (s instanceof ContainerContents c) { + candidate = c.lookup(address, seen); + } else if (s instanceof ObjectArrayValue a && seen.add(a)) { + candidate = lookupInArray(a, address); + } + found = merge(found, candidate); + } + return found; + } + + private static Value lookupInArray(ObjectArrayValue array, int address) { + Value found = null; + Value[] elements = array.getFields(); + if (elements == null) { + return null; + } + for (Value e : elements) { + if (e instanceof ObjectValue ov && ov.getAddress() == address) { + found = merge(found, e); + } + } + return found; + } + + private static Value merge(Value a, Value b) { + if (a == null) return b; + if (b == null || a == b) return a; + return AMBIGUOUS; + } + + private void index(Value value) { + if (!(value instanceof ObjectValue ov) || ov.isNullValue()) { + return; + } + if (ov.getAddress() == ObjectValue.ADDRESS_UNKNOWN) { + addressUnknown.add(value); + } else { + byAddress.merge(ov.getAddress(), value, ContainerContents::merge); + } + } + + /** Values stored before their address was known are indexed once it is. */ + private void resolvePendingAddresses() { + if (addressUnknown.isEmpty()) { + return; + } + List> pending = new ArrayList<>(addressUnknown); + addressUnknown.clear(); + for (Value v : pending) { + index(v); + } + } + + /** Strings and boxed values: their shadow is fixed once created. */ + private static boolean isValueTyped(Value value) { + return value instanceof StringValue || value instanceof BoxedValue; + } +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/ObjectValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/ObjectValue.java index 8a23a94f..0842cded 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/ObjectValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/ObjectValue.java @@ -38,6 +38,8 @@ public class ObjectValue extends Value { // For array object, fields are the content of the array. // For plain object, fields are the instance variables. @Setter @Getter private Value[] fields; + // For uninstrumented JDK containers: the shadow of what modelled calls stored in them. + @Setter @Getter private ContainerContents contents; @Getter private IntValue nFields; private BooleanFormulaManager bfm; @@ -271,10 +273,17 @@ public boolean isSymbolic() throws NotImplementedException { @Override public boolean isSymbolic(Set> visited) throws NotImplementedException, RuntimeException { + // Strings, boxed values and primitive arrays decide on their formula, not on fields + if (OVERRIDES_IS_SYMBOLIC.get(getClass())) { + return isSymbolic(); + } // If this object is already being checked, return false to avoid recursion if (!visited.add(this)) { return false; } + if (contents != null && contents.isSymbolic(visited)) { + return true; + } return fields != null && Arrays.stream(fields) .filter(Objects::nonNull) .anyMatch(field -> { @@ -286,6 +295,18 @@ public boolean isSymbolic(Set> visited) throws NotImplementedExcepti }); } + /** Whether a subclass has its own {@code isSymbolic()}, which the field walk must use. */ + private static final ClassValue OVERRIDES_IS_SYMBOLIC = new ClassValue<>() { + @Override + protected Boolean computeValue(Class type) { + try { + return type.getMethod("isSymbolic").getDeclaringClass() != ObjectValue.class; + } catch (NoSuchMethodException e) { + return false; + } + } + }; + @Override public ImmutableSet getSymbolicVariables() throws NotImplementedException, RuntimeException { if (fields == null) { From 1bca0a5157c58da53cc96787a8781305fae04eb6 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 22:29:22 +0000 Subject: [PATCH 2/4] Model System.arraycopy with concrete positions and length The shadow elements are copied from the source array to the destination array (primitive arrays: as stores into the array formula; object arrays: the element shadows). Symbolic positions or lengths, copies longer than 4096 elements and arrays of arrays stay unmodelled. Co-Authored-By: Claude Opus 5.5 --- .../symbolic/invoke/StaticInvocation.java | 2 + .../invoke/java/lang/SystemInvocation.java | 87 +++++++++++++++++++ 2 files changed, 89 insertions(+) create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/SystemInvocation.java diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/StaticInvocation.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/StaticInvocation.java index 21b2849f..a644382b 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/StaticInvocation.java +++ b/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; diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/SystemInvocation.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/SystemInvocation.java new file mode 100644 index 00000000..112089f3 --- /dev/null +++ b/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; + } +} From 5a33932905ed58125d66dc67bf794433d9496c37 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 22:29:22 +0000 Subject: [PATCH 3/4] Test the JDK container and arraycopy models Co-Authored-By: Claude Opus 5.5 --- .../symbolic/JdkContainerAgentSpec.groovy | 84 +++++++++++++ .../reference/ContainerContentsTest.groovy | 112 ++++++++++++++++++ .../resources/targets/collections/Main.java | 86 ++++++++++++++ 3 files changed, 282 insertions(+) create mode 100644 symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/JdkContainerAgentSpec.groovy create mode 100644 symbolic-executor/src/test/groovy/de/uzl/its/value/reference/ContainerContentsTest.groovy create mode 100644 symbolic-executor/src/test/resources/targets/collections/Main.java diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/JdkContainerAgentSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/JdkContainerAgentSpec.groovy new file mode 100644 index 00000000..fb9d2395 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/JdkContainerAgentSpec.groovy @@ -0,0 +1,84 @@ +package de.uzl.its.swat.symbolic + +import com.fasterxml.jackson.databind.ObjectMapper +import spock.lang.Shared +import spock.lang.Specification +import spock.lang.Unroll + +import javax.tools.ToolProvider +import java.nio.file.Files +import java.nio.file.Path +import java.util.concurrent.TimeUnit + +/** + * L2 (forked agent): symbolic values that go through modelled JDK container calls stay symbolic + * without context loss; calls that inspect a container holding a symbolic value still record it. + * Runs via the {@code agentTest} Gradle task (needs the agent jar from {@code copyJar}). + */ +class JdkContainerAgentSpec extends Specification { + + static final Path AGENT_JAR = Path.of("lib", "symbolic-executor.jar").toAbsolutePath() + static final Path NATIVE_LIBS = Path.of("..", "libs", "java-library-path").toAbsolutePath() + static final Path TARGET = Path.of("src", "test", "resources", "targets", "collections").toAbsolutePath() + static final Path VERIFIER = Path.of("src", "test", "resources", "targets", "svcomp", "org").toAbsolutePath() + + @Shared Path classes + + def setupSpec() { + assert Files.isRegularFile(AGENT_JAR): "agent jar missing, run copyJar first: ${AGENT_JAR}" + classes = Files.createTempDirectory("swat-container-agent-spec") + def sources = ([TARGET, VERIFIER].collectMany { root -> + Files.walk(root).filter { it.toString().endsWith(".java") }.collect { it.toString() } + }) + def err = new ByteArrayOutputStream() + int rc = ToolProvider.getSystemJavaCompiler().run(null, null, err, + (["-source", "1.8", "-target", "1.8", "-g", "-d", classes.toString()] + sources) as String[]) + assert rc == 0: "javac failed: ${err}" + } + + def cleanupSpec() { + classes?.toFile()?.deleteDir() + } + + @Unroll + def "a symbolic string kept in a container stays symbolic (#scenario)"() { + when: + Map trace = run(scenario) + + then: + !trace.symbolicContextLoss + trace.trace.any { !it.concreteOnly && it.constraint?.contains("String_0") } + + where: + scenario << ["list", "iterator", "map", "array", "arraycopy"] + } + + @Unroll + def "a call that inspects a container holding a symbolic value records context loss (#scenario)"() { + expect: + run(scenario).symbolicContextLoss + + where: + scenario << ["contains", "symbolicKey", "heldByUnmodelled"] + } + + private Map run(String scenario) { + def java = Path.of(System.getProperty("java.home"), "bin", "java").toString() + def cmd = [java, + "-javaagent:${AGENT_JAR}".toString(), + "-Djava.library.path=${NATIVE_LIBS}".toString(), + "-Dconfig.path=/nonexistent/swat.cfg", + "-Dinstrumentation.transformer=SV_COMP", + "-Dsolver.mode=PRINT", + "-DexitOnError=false", + "-DlogShadowStateToConsole=false", + "-cp", classes.toString(), "-ea", "Main", scenario] + def proc = new ProcessBuilder(cmd).directory(classes.toFile()).redirectErrorStream(true).start() + def out = proc.inputStream.text + assert proc.waitFor(5, TimeUnit.MINUTES): "target did not finish:\n${out}" + int start = out.indexOf("\n{\n") + int end = out.indexOf("\n}\n", start) + assert start >= 0 && end > start: "no trace JSON in output:\n${out}" + return new ObjectMapper().readValue(out.substring(start + 1, end + 2), Map) + } +} diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/ContainerContentsTest.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/ContainerContentsTest.groovy new file mode 100644 index 00000000..89e6db3f --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/value/reference/ContainerContentsTest.groovy @@ -0,0 +1,112 @@ +package de.uzl.its.value.reference + +import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.IntValue +import de.uzl.its.swat.symbolic.value.reference.ContainerContents +import de.uzl.its.swat.symbolic.value.reference.ObjectValue +import de.uzl.its.swat.symbolic.value.reference.lang.StringValue +import de.uzl.its.swat.thread.ThreadHandler +import org.sosy_lab.java_smt.api.SolverContext +import spock.lang.Specification + +import static java.lang.Thread.currentThread + +class ContainerContentsTest extends Specification { + + SolverContext context + + def setup() { + ThreadHandler.init() + if (ThreadHandler.hasThreadContext(currentThread().id)) { + ThreadHandler.removeThreadContext(currentThread().id) + } + ThreadHandler.addThreadContext(currentThread().id, "Test-Thread", -2) + context = ThreadHandler.getSolverContext(currentThread().id) + } + + private StringValue symbolicString(int address) { + def s = new StringValue(context, "abc", address) + s.MAKE_SYMBOLIC() + return s + } + + private ObjectValue container(String className) { + return new ObjectValue(context, className, new IntValue(context, 0), 42) + } + + def "an object whose field holds a symbolic string is symbolic"() { + given: + def o = new ObjectValue(context, "Foo", new IntValue(context, 1), 7) + o.setField(0, symbolicString(8)) + + expect: + o.isSymbolic() + } + + def "a container holding a symbolic value is symbolic, also through a view of it"() { + given: + def list = container("java/util/ArrayList") + list.setContents(new ContainerContents(ContainerContents.Kind.LIST)) + list.getContents().addValue(new StringValue(context, "c", 9)) + def view = container("java/util/ArrayList\$Itr") + view.setContents(ContainerContents.viewOf(list.getContents(), false)) + + expect: + !list.isSymbolic() + !view.isSymbolic() + + when: + list.getContents().addValue(symbolicString(10)) + + then: + list.isSymbolic() + view.isSymbolic() + } + + def "a stored value is found by address, also through a view, unless addresses collide"() { + given: + def contents = new ContainerContents(ContainerContents.Kind.LIST) + def s = symbolicString(11) + contents.addValue(s) + def view = ContainerContents.viewOf(contents, false) + + expect: + contents.lookup(11).is(s) + view.lookup(11).is(s) + contents.lookup(12) == null + + when: + contents.addValue(new StringValue(context, "abc", 11)) + + then: + contents.lookup(11) == null + } + + def "a value stored before its address was known is found once it is"() { + given: + def contents = new ContainerContents(ContainerContents.Kind.LIST) + def o = new ObjectValue(context, "Foo", new IntValue(context, 0)) + contents.addValue(o) + + when: + o.setAddress(13) + + then: + contents.lookup(13).is(o) + } + + def "a map key that becomes symbolic is reported"() { + given: + def contents = new ContainerContents(ContainerContents.Kind.MAP) + def key = new ObjectValue(context, "Foo", new IntValue(context, 1), 14) + contents.addKey(key) + + expect: + !contents.keysSymbolic(new HashSet<>()) + + when: + key.setField(0, symbolicString(15)) + + then: + contents.keysSymbolic(new HashSet<>()) + } +} diff --git a/symbolic-executor/src/test/resources/targets/collections/Main.java b/symbolic-executor/src/test/resources/targets/collections/Main.java new file mode 100644 index 00000000..9d031082 --- /dev/null +++ b/symbolic-executor/src/test/resources/targets/collections/Main.java @@ -0,0 +1,86 @@ +import java.util.ArrayList; +import java.util.Arrays; +import java.util.HashMap; +import java.util.Iterator; +import java.util.LinkedList; +import java.util.List; +import java.util.Map; +import org.sosy_lab.sv_benchmarks.Verifier; + +/** + * Target for the agent test of the JDK container models. The first argument picks a scenario; + * each one ends in a branch on the symbolic string, after the string went through a container. + */ +public class Main { + static void branch(Object o) { + if (((String) o).startsWith("x")) { + System.out.println("x"); + } + } + + public static void main(String[] args) { + String s = Verifier.nondetString(); + switch (args[0]) { + case "list": { + LinkedList l = new LinkedList<>(); + l.addLast(s); + l.addFirst("a"); + branch(l.getLast()); + break; + } + case "iterator": { + List l = new ArrayList<>(); + l.add(s); + List copy = new ArrayList<>(l); + for (Iterator it = copy.iterator(); it.hasNext(); ) { + branch(it.next()); + } + break; + } + case "map": { + Map m = new HashMap<>(); + m.put("k", s); + for (Map.Entry e : m.entrySet()) { + if (e.getKey().equals("k")) branch(e.getValue()); + } + branch(m.get("k")); + break; + } + case "array": { + List l = new ArrayList<>(); + l.add(s); + Object[] a = l.toArray(); + branch(Arrays.asList(a).get(0)); + break; + } + case "contains": { + List l = new ArrayList<>(); + l.add(s); + if (l.contains("x")) System.out.println("x"); + break; + } + case "symbolicKey": { + Map m = new HashMap<>(); + m.put(s, "v"); + branch(m.get("k") == null ? "y" : "x"); + break; + } + case "heldByUnmodelled": { + List l = new ArrayList<>(); + l.add(s); + branch(String.join(",", l)); + break; + } + case "arraycopy": { + int[] a = new int[4]; + int[] b = new int[4]; + a[1] = s.length(); + System.arraycopy(a, 0, b, 0, 4); + if (b[1] > 2) System.out.println("long"); + break; + } + default: + break; + } + } +} From a5740d71504e566d2aa46422fb30d05e6384e1ad Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 23:25:56 +0000 Subject: [PATCH 4/4] Recheck only mutable map keys for symbolic state String and boxed keys were concrete when stored and cannot change, so walking them on every modelled map call only costs time. Co-Authored-By: Claude Opus 5.5 --- .../swat/symbolic/value/reference/ContainerContents.java | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/ContainerContents.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/ContainerContents.java index 8b4041ed..0a042e90 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/ContainerContents.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/ContainerContents.java @@ -55,7 +55,7 @@ public enum Kind { private final List> mutables = new ArrayList<>(); /** Whether a value-typed (String, boxed) element was symbolic when it was stored. */ private boolean symbolicImmutable = false; - /** Map keys; a modelled store only accepts keys that are not symbolic. */ + /** Mutable map keys; a modelled store only accepts keys that are not symbolic. */ private final List> keys = new ArrayList<>(); private final Map> byAddress = new HashMap<>(); @@ -96,7 +96,10 @@ public void addKey(Value key) throws NotImplementedException { if (key == null) { return; } - keys.add(key); + // A String or boxed key was concrete when stored and stays so; only mutable keys are rechecked + if (!isValueTyped(key)) { + keys.add(key); + } index(key); }