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/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; + } +} 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..0a042e90 --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/ContainerContents.java @@ -0,0 +1,223 @@ +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: + * + *

+ * + *

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; + /** 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<>(); + 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; + } + // 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); + } + + /** 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) { 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; + } + } +}