[nils-loose]

What changes

JDK container models (CollectionInvocation, ContainerContents, ContainerPlaceHolder).
Calls on ArrayList, LinkedList, Vector, Stack, ArrayDeque, HashMap, LinkedHashMap and Hashtable that only move references are modelled. These are add/addLast/push/set, get/getLast/poll/remove(int), put/get/remove/containsKey with a concrete key, addAll/putAll and the copy constructors, iterator/listIterator/keySet/values/entrySet, toArray(), size/isEmpty/clear. The same goes for their views, iterators, entries and enumerations, and for Collections.singleton*/enumeration/unmodifiable* and Arrays.asList.

• The concrete call still runs. The shadow of each stored value is kept in the container's ContainerContents.
• A returned element is matched to that stored shadow by address once the concrete result is known (GETVALUE_Object). A view or iterator shares the contents of its container.
• Soundness:
  • A container that may hold a symbolic value now counts as symbolic. A call that inspects elements is not modelled (contains, indexOf, remove(Object), retainAll, sort, toString, streams, ...), so it still records context loss.
  • A symbolic map key, a symbolic index and a symbolic untracked source all stay unmodelled.
  • If a returned element cannot be matched while the container may hold a symbolic value, that records context loss too.

ObjectValue.isSymbolic(visited) walked fields only. As a result, a String, a boxed value or a primitive array held in a field never counted as symbolic, and an object holding one went into an unmodelled call without context loss. It now uses the value's own isSymbolic().

System.arraycopy is modelled when the positions and the length are concrete. Primitive arrays get stores into the array formula. Object arrays copy the element shadows. Longer than 4096 elements, or arrays of arrays, stay unmodelled.

Measured

Setup: sv-comp.cfg, nosa, 300 s, 15 GB, against baseline-results.jsonl.

Runs: 500.

• 257 are the KB runs with context-loss-collections, context-loss-other-jdk, jdk-container-issymbolic-ignores-elements or worker-threads-not-tracked, plus all of securibench.
• 163 are all other runs with a java.util/System missing invocation, or a correct SAFE with an object-taking missing invocation.
• 80 are random other correct runs.

Result: +44, -0, net +44, 0 new wrong verdicts. CPU over the 500 runs: 6615 s base, 6461 s new.

task	property	base	new
securibench Collections1-8, 10, 12, 13 (11 tasks)	no-runtime-exception	unknown	SAFE
securibench Collections8	valid-assert	unknown	SAFE
securibench Session1, Session2, Session3	no-runtime-exception	unknown	SAFE
securibench Basic26, Basic33, Basic34, Inter12	no-runtime-exception	unknown	SAFE
argv-tasks GraphFragment_true	both	unknown	SAFE
argv-tasks GraphFragment_false	no-runtime-exception	unknown	SAFE

Tests

• JdkContainerAgentSpec (L2, agentTest):
  • a symbolic string through a list, an iterator, a map entry set, toArray/asList, and arraycopy stays symbolic without context loss;
  • contains, a symbolic map key, and String.join over a list holding it all record context loss.
• ContainerContentsTest (L0): isSymbolic through fields and views, lookup by address, ambiguity, late addresses, keys that become symbolic.
• The default executor tests pass.

Known limits

• Removals are not tracked. The contents only grow, which over-approximates and so is sound.
• HashSet/TreeMap/PriorityQueue, toArray(T[]), List.of, forEach/streams are not modelled.
• Still unmodelled from context-loss-other-jdk:
  • URLDecoder, regex, StringReader/BufferedReader, URLEncoder;
  • StringTokenizer: it needs branching on the delimiter positions of a symbolic string, and the loops over tokens are unbounded anyway.
• Worker threads are not addressed.
• Element shadows are matched by identityHashCode, as the shadow heap does. A collision or ambiguity falls back to context loss.

🤖 Generated with Claude Code

[nils-loose]

Included in dev through #92 (merge commit 534c182), together with the fixes for interactions between PRs. This PR stays as the record of the change and its measured flips.