From 98e402a9869124832d0607542147434e4235b8a0 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 23:31:27 +0000 Subject: [PATCH 1/7] Report loop-head states with the trace With loopStateMatching set, the instrumentation finds the targets of backward jumps (with an empty operand stack) and probes them with a LOOP_HEAD instruction that carries the values of the locals defined there. The probe goes through the processor, so it is handled after the jump that led to the head has been recorded. LoopStateMatcher hashes the program state at the head: the head, its locals, the static fields of the initialized application classes (every application class now records the start of its initialization in ClassInits), and the heap reachable from them, encoded as a graph. There is no hash unless the head's method is the only application frame, the target runs a single thread, no shadow value is symbolic, and the heap holds only application objects, application enum constants, arrays and plain Objects. The hashes reach the explorer with the next branch (BranchDTO.loopStates). Co-Authored-By: Claude Opus 5.5 --- .../java/de/uzl/its/swat/config/Config.java | 4 + .../instruction/InstructionClassAdapter.java | 38 ++ .../instruction/InstructionMethodAdapter.java | 25 ++ .../symbolic/SymbolicInstructionVisitor.java | 19 + .../InstructionLoggingDispatcher.java | 6 + .../symbolic/dispatcher/NopDispatcher.java | 3 + .../SymbolicInstructionDispatcher.java | 7 + .../swat/symbolic/instruction/IVisitor.java | 2 + .../swat/symbolic/instruction/LOOP_HEAD.java | 31 ++ .../swat/symbolic/loopstate/ClassInits.java | 26 ++ .../swat/symbolic/loopstate/LoopHeads.java | 194 ++++++++++ .../symbolic/loopstate/LoopStateMatcher.java | 332 ++++++++++++++++++ .../swat/symbolic/loopstate/package-info.java | 8 + .../AbstractInstructionProcessor.java | 4 + .../processor/DummyInstructionProcessor.java | 3 + .../processor/InstructionProcessor.java | 2 + .../uzl/its/swat/symbolic/shadow/JVMHeap.java | 4 + .../swat/symbolic/shadow/ShadowContext.java | 5 + .../swat/symbolic/trace/BranchElement.java | 3 + .../its/swat/symbolic/trace/DTOBuilder.java | 3 +- .../symbolic/trace/SymbolicTraceHandler.java | 17 + .../swat/symbolic/trace/dto/BranchDTO.java | 10 + .../de/uzl/its/swat/thread/ThreadContext.java | 9 + .../de/uzl/its/swat/thread/ThreadHandler.java | 10 + .../symbolic/loopstate/LoopHeadsTest.groovy | 73 ++++ 25 files changed, 837 insertions(+), 1 deletion(-) create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/instruction/LOOP_HEAD.java create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/loopstate/ClassInits.java create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/loopstate/LoopHeads.java create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/loopstate/LoopStateMatcher.java create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/loopstate/package-info.java create mode 100644 symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/loopstate/LoopHeadsTest.groovy diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/config/Config.java b/symbolic-executor/src/main/java/de/uzl/its/swat/config/Config.java index 2f9a014e..5db06a76 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/config/Config.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/config/Config.java @@ -229,6 +229,9 @@ public class Config { // Fontus options // ------------------------------------ @Getter private boolean useStringInterning; + /** Probe loop heads and report their concrete states with the trace (see symbolic/loopstate). */ + @Getter private boolean loopStateMatching; + private static final boolean DEFAULT_LOOP_STATE_MATCHING = false; private static final boolean DEFAULT_STRING_INTERNING = true; @Getter private String stringProxy; private static final String DEFAULT_STRING_PROXY = "Ljava/lang/String;"; @@ -446,6 +449,7 @@ private void readProperties() { // Fontus options // ------------------------------------ useStringInterning = readBoolean("useStringInterning", DEFAULT_STRING_INTERNING); + loopStateMatching = readBoolean("loopStateMatching", DEFAULT_LOOP_STATE_MATCHING); stringProxy = readString("stringProxy", DEFAULT_STRING_PROXY); } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/InstructionClassAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/InstructionClassAdapter.java index 60bba95d..44af9465 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/InstructionClassAdapter.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/InstructionClassAdapter.java @@ -8,6 +8,9 @@ import org.objectweb.asm.Opcodes; import org.objectweb.asm.commons.JSRInlinerAdapter; import org.objectweb.asm.commons.TryCatchBlockSorter; +import org.objectweb.asm.tree.MethodNode; +import de.uzl.its.swat.config.Config; +import de.uzl.its.swat.symbolic.loopstate.LoopHeads; /** * A visitor to visit a Java class. The methods of this class must be called in the following order: @@ -17,6 +20,8 @@ */ public class InstructionClassAdapter extends ClassVisitor { private final String cname; + /** Whether the class has a static initializer (see visitEnd). */ + private boolean hasClinit = false; /** * Constructor that calls the super from the default ClassVisitor * @@ -61,6 +66,9 @@ public void visit( public MethodVisitor visitMethod( int access, String name, String desc, String signature, String[] exceptions) { MethodVisitor mv = cv.visitMethod(access, name, desc, signature, exceptions); + if (name.equals("")) { + hasClinit = true; + } if (cname.equals("de/uzl/its/swat/instrument/svcomp/Verifier") && !name.equals("assume")) { return mv; } @@ -82,9 +90,39 @@ public MethodVisitor visitMethod( name, desc, cname); + if (Config.instance().isLoopStateMatching() && !cname.startsWith("de/uzl/its/swat/")) { + // Collect the method to find its loop heads, then hand it on + return new MethodNode(Opcodes.ASM9, access, name, desc, signature, exceptions) { + @Override + public void visitEnd() { + super.visitEnd(); + ima.setLoopHeads(LoopHeads.analyze(cname, this)); + accept(ima); + } + }; + } return ima; } return null; } + + /** + * With loop-state matching, gives a class without a static initializer one that records its + * initialization (see ClassInits), as the existing ones do. + */ + @Override + public void visitEnd() { + if (Config.instance().isLoopStateMatching() && !hasClinit && !cname.startsWith("de/uzl/its/swat/")) { + MethodVisitor mv = cv.visitMethod(Opcodes.ACC_STATIC, "", "()V", null, null); + if (mv != null) { + mv.visitCode(); + LoopHeads.emitClassInit(mv, cname); + mv.visitInsn(Opcodes.RETURN); + mv.visitMaxs(1, 0); + mv.visitEnd(); + } + } + super.visitEnd(); + } } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/InstructionMethodAdapter.java b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/InstructionMethodAdapter.java index b24ee90c..3f6bfde7 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/InstructionMethodAdapter.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/instrument/instruction/InstructionMethodAdapter.java @@ -9,6 +9,7 @@ import de.uzl.its.swat.instrument.TryCatchBlock; import de.uzl.its.swat.instrument.Utils; import de.uzl.its.swat.metadata.ClassDepot; +import de.uzl.its.swat.symbolic.loopstate.LoopHeads; import java.lang.reflect.Field; import java.lang.reflect.Method; @@ -110,6 +111,9 @@ public void visitCode() { instrumentationState.setMid(mIdx); if (methodName.equals("")) { + if (config.isLoopStateMatching() && !owner.startsWith("de/uzl/its/swat/")) { + LoopHeads.emitClassInit(mv, owner); + } int cIdx = classDepot.getClassIndex(this.owner); String clinit_desc = "(JIJ)V"; // (long iid, int cIdx, long invokeId) addJpushInsn(mv, instrumentationState.incAndGetId()); @@ -131,6 +135,27 @@ public void visitCode() { private static void addJpushInsn(MethodVisitor mv, long val) { Utils.addJpushInsn(mv, val); } + + /** The method's loop heads (see LoopHeads), by the label that starts each. */ + private java.util.Map loopHeads = java.util.Map.of(); + + public void setLoopHeads(java.util.Map loopHeads) { + this.loopHeads = loopHeads; + } + + /** + * At a loop head, probes the state. The probe goes through the processor like an instruction, + * so the symbolic execution, which lags one instruction behind, handles it once the jump that + * led here has been recorded. + */ + @Override + public void visitLabel(Label label) { + super.visitLabel(label); + LoopHeads.Head head = loopHeads.get(label); + if (head != null) { + LoopHeads.emitProbe(mv, config.getInstrumentationDispatcher(), instrumentationState.incAndGetId(), head); + } + } /** Push a value onto the stack. */ private static void addBipushInsn(MethodVisitor mv, int val) { Utils.addBipushInsn(mv, val); 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..79675ee7 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 @@ -15,6 +15,7 @@ import de.uzl.its.swat.metadata.ClassDepot; import de.uzl.its.swat.metadata.ClassDepotRuntime; import de.uzl.its.swat.symbolic.instruction.*; +import de.uzl.its.swat.symbolic.loopstate.LoopStateMatcher; import de.uzl.its.swat.symbolic.invoke.InvocationHandler; import de.uzl.its.swat.symbolic.processor.InstructionProcessor; import de.uzl.its.swat.symbolic.processor.SymbolicInstructionProcessor; @@ -3633,6 +3634,24 @@ public void visitLOOP_END(LOOP_END inst) throws SymbolicInstructionException { public void visitSPECIAL(SPECIAL inst) throws SymbolicInstructionException { } + /** + * Reports the state at a loop head with the next branch, if it has one (see LoopStateMatcher). + * + * @param inst The LOOP_HEAD probe + */ + public void visitLOOP_HEAD(LOOP_HEAD inst) throws SymbolicInstructionException { + try { + long id = currentThread().getId(); + String state = LoopStateMatcher.stateOf(inst, stack, ThreadHandler.getStaticFields(id), + ThreadHandler.getActiveThreadContextIds().size()); + if (state != null) { + symbolicTraceHandler.addLoopState(state); + } + } catch (Throwable t) { + throw new SymbolicInstructionException(inst, t); + } + } + /** * Creates a multidimensional array of references. Currently, no symbolic handling here because * arrays are not of primitive type? See: started = new TreeSet<>(); + + private ClassInits() {} + + public static synchronized void started(String internalName) { + started.add(internalName); + } + + /** The classes, in name order. */ + static synchronized String[] snapshot() { + return started.toArray(new String[0]); + } +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/loopstate/LoopHeads.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/loopstate/LoopHeads.java new file mode 100644 index 00000000..6085559a --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/loopstate/LoopHeads.java @@ -0,0 +1,194 @@ +package de.uzl.its.swat.symbolic.loopstate; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.IdentityHashMap; +import java.util.List; +import java.util.Map; +import java.util.concurrent.ConcurrentHashMap; +import org.objectweb.asm.Label; +import org.objectweb.asm.MethodVisitor; +import org.objectweb.asm.Opcodes; +import org.objectweb.asm.Type; +import org.objectweb.asm.tree.AbstractInsnNode; +import org.objectweb.asm.tree.InsnList; +import org.objectweb.asm.tree.JumpInsnNode; +import org.objectweb.asm.tree.LabelNode; +import org.objectweb.asm.tree.LookupSwitchInsnNode; +import org.objectweb.asm.tree.MethodNode; +import org.objectweb.asm.tree.TableSwitchInsnNode; +import org.objectweb.asm.tree.analysis.Analyzer; +import org.objectweb.asm.tree.analysis.AnalyzerException; +import org.objectweb.asm.tree.analysis.BasicInterpreter; +import org.objectweb.asm.tree.analysis.BasicValue; +import org.objectweb.asm.tree.analysis.Frame; + +/** + * The loop heads of the instrumented methods: the targets of backward jumps at which the operand + * stack is empty. For each the instrumentation records which locals are defined there and of what + * kind, so that the probe it inserts can pass their values (see {@link #emitProbe}). + */ +public final class LoopHeads { + + /** Value kinds of a local: the JVM computational types. */ + public static final char INT = 'I', LONG = 'J', FLOAT = 'F', DOUBLE = 'D', REFERENCE = 'A'; + + /** + * A loop head. + * + * @param name stable name: owner, method name and descriptor, and the head's position among the + * method's heads + * @param owner internal name of the class + * @param method name of the method + * @param slots the local slots defined at the head + * @param kinds the kind of each slot + */ + public record Head(String name, String owner, String method, int[] slots, char[] kinds) {} + + private static final Map heads = new ConcurrentHashMap<>(); + + private LoopHeads() {} + + public static Head get(String name) { + return heads.get(name); + } + + /** + * Finds the loop heads of a method. Returns them keyed by the label the method node replays + * (LabelNode.getLabel()), or an empty map if the method cannot be analysed. + */ + public static Map analyze(String owner, MethodNode mn) { + Map result = new IdentityHashMap<>(); + if (mn.instructions.size() == 0 || mn.name.equals("")) { + return result; + } + InsnList insns = mn.instructions; + List targets = new ArrayList<>(); + Map seen = new IdentityHashMap<>(); + for (AbstractInsnNode n : insns) { + List jumps = new ArrayList<>(); + if (n instanceof JumpInsnNode j) { + if (j.getOpcode() == Opcodes.JSR) { + return result; // subroutines: the analysis below does not apply + } + jumps.add(j.label); + } else if (n instanceof TableSwitchInsnNode t) { + jumps.add(t.dflt); + jumps.addAll(t.labels); + } else if (n instanceof LookupSwitchInsnNode l) { + jumps.add(l.dflt); + jumps.addAll(l.labels); + } + int at = insns.indexOf(n); + for (LabelNode target : jumps) { + if (insns.indexOf(target) < at && seen.put(target, Boolean.TRUE) == null) { + targets.add(target); + } + } + } + if (targets.isEmpty()) { + return result; + } + Frame[] frames; + try { + frames = new Analyzer<>(new BasicInterpreter()).analyze(owner, mn); + } catch (AnalyzerException | RuntimeException e) { + return result; + } + targets.sort((a, b) -> Integer.compare(insns.indexOf(a), insns.indexOf(b))); + int ordinal = 0; + for (LabelNode target : targets) { + Frame f = frames[insns.indexOf(target)]; + int position = ordinal++; + if (f == null || f.getStackSize() != 0) { + continue; // unreachable, or values on the operand stack the probe cannot see + } + List slots = new ArrayList<>(); + StringBuilder kinds = new StringBuilder(); + boolean usable = true; + for (int i = 0; i < f.getLocals(); i++) { + BasicValue v = f.getLocal(i); + if (v == null || v == BasicValue.UNINITIALIZED_VALUE) { + continue; // never read before it is written again + } + if (v == BasicValue.RETURNADDRESS_VALUE) { + usable = false; + break; + } + char kind = switch (v.getType().getSort()) { + case Type.BOOLEAN, Type.CHAR, Type.BYTE, Type.SHORT, Type.INT -> INT; + case Type.LONG -> LONG; + case Type.FLOAT -> FLOAT; + case Type.DOUBLE -> DOUBLE; + case Type.OBJECT, Type.ARRAY -> REFERENCE; + default -> 0; + }; + if (kind == 0) { + usable = false; + break; + } + slots.add(i); + kinds.append(kind); + } + if (!usable) { + continue; + } + String name = owner + "." + mn.name + mn.desc + "#" + position; + Head head = new Head(name, owner, mn.name, + slots.stream().mapToInt(Integer::intValue).toArray(), kinds.toString().toCharArray()); + heads.put(name, head); + result.put(target.getLabel(), head); + } + return result; + } + + /** + * Emits the probe of a loop head: LOOP_HEAD(iid, name, locals), where locals holds the values + * of the head's locals, primitives boxed. + */ + public static void emitProbe(MethodVisitor mv, String dispatcher, long iid, Head head) { + mv.visitLdcInsn(iid); + mv.visitLdcInsn(head.name()); + push(mv, head.slots().length); + mv.visitTypeInsn(Opcodes.ANEWARRAY, "java/lang/Object"); + for (int k = 0; k < head.slots().length; k++) { + mv.visitInsn(Opcodes.DUP); + push(mv, k); + int slot = head.slots()[k]; + switch (head.kinds()[k]) { + case INT -> box(mv, Opcodes.ILOAD, slot, "java/lang/Integer", "I"); + case LONG -> box(mv, Opcodes.LLOAD, slot, "java/lang/Long", "J"); + case FLOAT -> box(mv, Opcodes.FLOAD, slot, "java/lang/Float", "F"); + case DOUBLE -> box(mv, Opcodes.DLOAD, slot, "java/lang/Double", "D"); + default -> mv.visitVarInsn(Opcodes.ALOAD, slot); + } + mv.visitInsn(Opcodes.AASTORE); + } + mv.visitMethodInsn(Opcodes.INVOKESTATIC, dispatcher, "LOOP_HEAD", + "(JLjava/lang/String;[Ljava/lang/Object;)V", false); + } + + private static void box(MethodVisitor mv, int load, int slot, String owner, String desc) { + mv.visitVarInsn(load, slot); + mv.visitMethodInsn(Opcodes.INVOKESTATIC, owner, "valueOf", "(" + desc + ")L" + owner + ";", false); + } + + private static void push(MethodVisitor mv, int value) { + if (value >= -1 && value <= 5) { + mv.visitInsn(Opcodes.ICONST_0 + value); + } else if (value <= Short.MAX_VALUE) { + mv.visitIntInsn(Opcodes.SIPUSH, value); + } else { + mv.visitLdcInsn(value); + } + } + + /** + * Emits the call that records the start of a class's initialization, see {@link ClassInits}. + */ + public static void emitClassInit(MethodVisitor mv, String owner) { + mv.visitLdcInsn(owner); + mv.visitMethodInsn(Opcodes.INVOKESTATIC, Type.getInternalName(ClassInits.class), "started", + "(Ljava/lang/String;)V", false); + } +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/loopstate/LoopStateMatcher.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/loopstate/LoopStateMatcher.java new file mode 100644 index 00000000..452fe05c --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/loopstate/LoopStateMatcher.java @@ -0,0 +1,332 @@ +package de.uzl.its.swat.symbolic.loopstate; + +import de.uzl.its.swat.common.Util; +import de.uzl.its.swat.symbolic.instruction.LOOP_HEAD; +import de.uzl.its.swat.symbolic.shadow.Frame; +import de.uzl.its.swat.symbolic.shadow.ShadowContext; +import de.uzl.its.swat.symbolic.value.Value; +import ch.qos.logback.classic.Logger; +import de.uzl.its.swat.common.logging.GlobalLogger; +import java.io.DataOutputStream; +import java.io.IOException; +import java.io.OutputStream; +import java.lang.reflect.Array; +import java.lang.reflect.Field; +import java.lang.reflect.Modifier; +import java.security.DigestOutputStream; +import java.security.MessageDigest; +import java.security.NoSuchAlgorithmException; +import java.util.Arrays; +import java.util.Collection; +import java.util.Comparator; +import java.util.IdentityHashMap; +import java.util.List; +import java.util.Map; + +/** + * Hashes the program state at a loop head. + * + *

The state is everything the rest of the execution depends on, apart from the inputs still to + * be read: the loop head, the locals defined there, the static fields of the initialized + * application classes, the set of those classes, and the heap reachable from all of these. The + * hash is only computed when the state is fully known and fully concrete; otherwise there is none: + * + *

    + *
  • the head's method is the only application frame on the stack (the frames below it run no + * application code after it returns) and the target runs no other thread; + *
  • no shadow value of the head's locals, of another shadow frame, of a static field or of the + * shadow heap is symbolic. A concrete state is then the same on every execution that takes + * the same branches up to the head, whatever its inputs; + *
  • the reachable heap consists of application objects, enum constants of application enums, + * arrays and plain {@code Object}s only. Strings, boxed values and library objects are not + * hashed, since part of their identity (interning, caches) or content lies outside the + * reachable heap. + *
+ * + * The heap is encoded as a graph, by the order in which a depth-first walk from the roots meets + * its objects, so two states have the same encoding iff their reachable heaps are isomorphic with + * equal contents. Floating-point values are encoded by their bits. + * + *

Why a branch that follows a repeated state need not be flipped (the explorer side): order the + * executions by the number of branches, then by their branch outcomes (lexicographically), then by + * the number of loop-head states they pass. Take a smallest execution that violates the property + * and suppose it passes, before some branch, a state S that some executed path reached earlier in + * this order. The executed prefix up to S, followed by the rest of the violating execution after + * S, is an execution too (the state is the same, and the inputs read afterwards are fresh), it + * violates the property as well, and it is smaller. So a smallest violating execution never passes + * a state that was reached earlier in this order, and the search still finds it with those + * branches left unflipped. + */ +public final class LoopStateMatcher { + + /** Larger reachable heaps are not hashed. */ + private static final int MAX_OBJECTS = 20_000; + + private static final String SWAT_PACKAGE = "de/uzl/its/swat/"; + + private LoopStateMatcher() {} + + /** Thrown when the state cannot be hashed. */ + private static final class Unhashable extends Exception { + Unhashable() { + super(null, null, false, false); + } + } + + private static final Unhashable UNHASHABLE = new Unhashable(); + + private static final Logger logger = GlobalLogger.getSymbolicExecutionLogger(); + + /** Logs why a state is not hashed. */ + private static Unhashable unhashable(String why) { + logger.debug("[LOOP STATE] Not hashed: {}", why); + return UNHASHABLE; + } + + /** + * Returns the hash of the state at a loop head, or null if it has none (see the class comment). + * + * @param inst the probe of the head + * @param shadow the thread's shadow stack and heap + * @param shadowStatics the shadow static fields by class name + * @param threads the number of target threads + */ + public static String stateOf( + LOOP_HEAD inst, ShadowContext shadow, Map[]> shadowStatics, int threads) { + LoopHeads.Head head = LoopHeads.get(inst.head); + if (head == null || threads != 1 || inst.locals.length != head.slots().length) { + logger.debug("[LOOP STATE] Not hashed: unknown head or several threads"); + return null; + } + try { + checkStack(head); + checkShadow(head, shadow, shadowStatics); + String h = hash(head, inst.locals); + logger.debug("[LOOP STATE] {}: {}", inst.head, h); + return h; + } catch (Unhashable e) { + return null; + } + } + + /** The head's method must be the only application frame on the stack. */ + private static void checkStack(LoopHeads.Head head) throws Unhashable { + List app = StackWalker.getInstance().walk(s -> s + .map(f -> f.getClassName().replace('.', '/')) + .filter(LoopStateMatcher::isApplicationClassName) + .limit(2) + .toList()); + if (app.size() != 1 || !app.get(0).equals(head.owner())) { + throw unhashable("other application frames on the stack"); + } + } + + private static void checkShadow(LoopHeads.Head head, ShadowContext shadow, + Map[]> shadowStatics) throws Unhashable { + Frame active = shadow.getActiveFrame(); + // The entry method runs in the initial frame + boolean entry = active.getClassName().equals(ShadowContext.getINITIAL_FRAME_NAME()) + && shadow.getFrameStack().size() == 1; + boolean same = head.owner().equals(active.getClassName()) && head.method().equals(active.getMethodName()); + if (!(entry || same) || !active.getOperandStack().isEmpty()) { + throw unhashable("shadow frame out of step"); + } + List> locals = active.getLocals(); + for (int slot : head.slots()) { + if (slot < locals.size()) { + requireConcrete(locals.get(slot)); + } + } + for (Frame frame : shadow.getFrameStack()) { + if (frame != active) { + requireConcrete(frame.getLocals()); + requireConcrete(frame.getOperandStack()); + } + } + for (Map.Entry[]> e : shadowStatics.entrySet()) { + if (e.getKey() != null && !e.getKey().startsWith(SWAT_PACKAGE)) { + requireConcrete(Arrays.asList(e.getValue())); + } + } + requireConcrete(shadow.heapValues()); + } + + private static void requireConcrete(Collection> values) throws Unhashable { + for (Value v : values) { + requireConcrete(v); + } + } + + private static void requireConcrete(Value v) throws Unhashable { + if (v == null) { + return; + } + boolean symbolic; + try { + symbolic = v.isSymbolic(); + } catch (Throwable t) { + symbolic = true; // unknown counts as symbolic + } + if (symbolic) { + throw unhashable("symbolic value"); + } + } + + private static boolean isApplicationClassName(String internalName) { + return !internalName.startsWith(SWAT_PACKAGE) && Util.shouldInstrument(internalName); + } + + private static boolean isApplicationClass(Class c) { + return c.getClassLoader() != null && !c.isHidden() && isApplicationClassName(c.getName().replace('.', '/')); + } + + private static String hash(LoopHeads.Head head, Object[] locals) throws Unhashable { + MessageDigest md; + try { + md = MessageDigest.getInstance("SHA-256"); + } catch (NoSuchAlgorithmException e) { + throw unhashable("no SHA-256"); + } + try (DataOutputStream out = new DataOutputStream(new DigestOutputStream(OutputStream.nullOutputStream(), md))) { + Encoder enc = new Encoder(out); + out.writeUTF(head.name()); + for (int k = 0; k < locals.length; k++) { + out.writeInt(head.slots()[k]); + enc.local(head.kinds()[k], locals[k]); + } + String[] classes = ClassInits.snapshot(); + out.writeInt(classes.length); + for (String name : classes) { + if (name.startsWith(SWAT_PACKAGE)) { + continue; + } + out.writeUTF(name); + Class c = load(name); + for (Field f : sortedFields(c, true)) { + out.writeUTF(f.getName()); + enc.field(f, null); + } + } + } catch (IOException | ReflectiveOperationException | RuntimeException | LinkageError e) { + throw unhashable("reflection failed"); + } + byte[] digest = md.digest(); + StringBuilder sb = new StringBuilder(32); + for (int i = 0; i < 16; i++) { + sb.append(String.format("%02x", digest[i])); + } + return sb.toString(); + } + + private static Class load(String internalName) throws ClassNotFoundException { + String name = internalName.replace('/', '.'); + ClassLoader context = Thread.currentThread().getContextClassLoader(); + try { + return Class.forName(name, false, context != null ? context : ClassLoader.getSystemClassLoader()); + } catch (ClassNotFoundException e) { + return Class.forName(name, false, ClassLoader.getSystemClassLoader()); + } + } + + private static Field[] sortedFields(Class c, boolean statics) { + Field[] fields = Arrays.stream(c.getDeclaredFields()) + .filter(f -> Modifier.isStatic(f.getModifiers()) == statics) + .sorted(Comparator.comparing(Field::getName)) + .toArray(Field[]::new); + for (Field f : fields) { + f.setAccessible(true); + } + return fields; + } + + /** Writes values and the heap graph reachable from them. */ + private static final class Encoder { + private final DataOutputStream out; + private final IdentityHashMap ids = new IdentityHashMap<>(); + + Encoder(DataOutputStream out) { + this.out = out; + } + + void local(char kind, Object value) throws IOException, Unhashable, IllegalAccessException { + switch (kind) { + case LoopHeads.INT -> out.writeInt((Integer) value); + case LoopHeads.LONG -> out.writeLong((Long) value); + case LoopHeads.FLOAT -> out.writeInt(Float.floatToRawIntBits((Float) value)); + case LoopHeads.DOUBLE -> out.writeLong(Double.doubleToRawLongBits((Double) value)); + default -> ref(value); + } + } + + void field(Field f, Object owner) throws IOException, Unhashable, IllegalAccessException { + Class t = f.getType(); + if (t == int.class) out.writeInt(f.getInt(owner)); + else if (t == long.class) out.writeLong(f.getLong(owner)); + else if (t == boolean.class) out.writeBoolean(f.getBoolean(owner)); + else if (t == byte.class) out.writeByte(f.getByte(owner)); + else if (t == char.class) out.writeChar(f.getChar(owner)); + else if (t == short.class) out.writeShort(f.getShort(owner)); + else if (t == float.class) out.writeInt(Float.floatToRawIntBits(f.getFloat(owner))); + else if (t == double.class) out.writeLong(Double.doubleToRawLongBits(f.getDouble(owner))); + else ref(f.get(owner)); + } + + void ref(Object o) throws IOException, Unhashable, IllegalAccessException { + if (o == null) { + out.writeByte('N'); + return; + } + Integer id = ids.get(o); + if (id != null) { + out.writeByte('R'); + out.writeInt(id); + return; + } + if (ids.size() >= MAX_OBJECTS) { + throw unhashable("heap too large"); + } + ids.put(o, ids.size()); + Class c = o.getClass(); + if (c.isArray()) { + out.writeByte('Y'); + out.writeUTF(c.getName()); + int n = Array.getLength(o); + out.writeInt(n); + Class e = c.getComponentType(); + if (o instanceof int[] a) for (int v : a) out.writeInt(v); + else if (o instanceof long[] a) for (long v : a) out.writeLong(v); + else if (o instanceof boolean[] a) for (boolean v : a) out.writeBoolean(v); + else if (o instanceof byte[] a) out.write(a); + else if (o instanceof char[] a) for (char v : a) out.writeChar(v); + else if (o instanceof short[] a) for (short v : a) out.writeShort(v); + else if (o instanceof float[] a) for (float v : a) out.writeInt(Float.floatToRawIntBits(v)); + else if (o instanceof double[] a) for (double v : a) out.writeLong(Double.doubleToRawLongBits(v)); + else if (!e.isPrimitive()) for (Object v : (Object[]) o) ref(v); + else throw unhashable("unknown array type"); + return; + } + if (c == Object.class) { + out.writeByte('O'); + return; + } + if (!isApplicationClass(c)) { + throw unhashable("non-application object"); + } + out.writeByte('C'); + out.writeUTF(c.getName()); + for (Class k = c; k != Object.class; k = k.getSuperclass()) { + if (k == Enum.class) { + // name and ordinal are final and fixed by the constant + out.writeInt(((Enum) o).ordinal()); + break; + } + if (k == null || !isApplicationClass(k)) { + throw unhashable("non-application superclass"); + } + for (Field f : sortedFields(k, false)) { + field(f, o); + } + } + } + } +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/loopstate/package-info.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/loopstate/package-info.java new file mode 100644 index 00000000..3a30b921 --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/loopstate/package-info.java @@ -0,0 +1,8 @@ +/** + * Loop-head state matching: at the target of every backward jump the executor hashes the program + * state, provided no part of it is symbolic, and reports the hash with the next branch. The + * explorer does not flip a branch that follows a state it has already reached on a shorter (or + * equally long, but earlier ordered) path: whatever that branch could still lead to is reachable + * from the earlier occurrence as well (see LoopStateMatcher). + */ +package de.uzl.its.swat.symbolic.loopstate; diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/processor/AbstractInstructionProcessor.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/processor/AbstractInstructionProcessor.java index 848d95f0..068b079d 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/processor/AbstractInstructionProcessor.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/processor/AbstractInstructionProcessor.java @@ -766,6 +766,10 @@ public void LOOP_BEGIN(long iid) { processInstruction(new LOOP_BEGIN(iid)); } + public void LOOP_HEAD(long iid, String head, Object[] locals) { + processInstruction(new LOOP_HEAD(iid, head, locals)); + } + public void LOOP_END(long iid) { processInstruction(new LOOP_END(iid)); } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/processor/DummyInstructionProcessor.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/processor/DummyInstructionProcessor.java index d99826ab..08155f17 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/processor/DummyInstructionProcessor.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/processor/DummyInstructionProcessor.java @@ -376,6 +376,9 @@ public void MAKE_SYMBOLIC(long iid) {} @Override public void LOOP_BEGIN(long iid) {} + @Override + public void LOOP_HEAD(long iid, String head, Object[] locals) {} + @Override public void LOOP_END(long iid) {} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/processor/InstructionProcessor.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/processor/InstructionProcessor.java index 7963aa73..f7a828f1 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/processor/InstructionProcessor.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/processor/InstructionProcessor.java @@ -373,6 +373,8 @@ void INVOKEDYNAMIC( void LOOP_BEGIN(long iid); + void LOOP_HEAD(long iid, String head, Object[] locals); + void LOOP_END(long iid); void SPECIAL(long iid, int i); diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/JVMHeap.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/JVMHeap.java index b18efde5..37911184 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/JVMHeap.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/JVMHeap.java @@ -20,6 +20,10 @@ public void put(int hashCode, Value value) { objects.put(hashCode, value); } + public java.util.Collection> values() { + return java.util.Collections.unmodifiableCollection(objects.values()); + } + public Value get(int hashCode) { return objects.get(hashCode); } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/ShadowContext.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/ShadowContext.java index 5516d0a8..54580208 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/ShadowContext.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/shadow/ShadowContext.java @@ -49,6 +49,11 @@ public void putToHeap(int hashCode, Value value) { heap.put(hashCode, value); } + /** All values of the shadow heap. */ + public java.util.Collection> heapValues() { + return heap.values(); + } + public Value getFromHeap(int hashCode) { return heap.get(hashCode); } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/BranchElement.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/BranchElement.java index 08399f79..2dcd5d47 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/BranchElement.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/BranchElement.java @@ -31,6 +31,9 @@ final class BranchElement extends Element { @lombok.Setter private java.util.List pushes = java.util.List.of(); // Recorded in application code that library code called back (see ShadowContext.inCallback). @lombok.Setter private boolean callback; + // The loop-head states the execution reached since the previous branch, in order (see + // LoopStateMatcher). + @lombok.Setter private java.util.List loopStates = java.util.List.of(); /** * Constructs a branch element. diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java index e272cf71..72886e39 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java @@ -143,7 +143,8 @@ private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace, StatsStorage } } trace.add(new BranchDTO(be.getIid(), constraint, be.isBranched(), be.isConcreteOnly()) - .place(be.getKey(), be.getPops(), be.getPushes(), be.isCallback())); + .place(be.getKey(), be.getPops(), be.getPushes(), be.isCallback()) + .loopStates(be.getLoopStates())); } else if (el instanceof SpecialElement se) { trace.add(new BranchDTO(se.getIid(), se.getInst())); } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java index d8e1b62c..ed4d49b7 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java @@ -64,9 +64,25 @@ public void checkAndSetBranch(boolean result, BooleanFormula constraint, long ii // check if the path constraint contains a free/ symbolic variable place(current, iid, suffix); + takeLoopStates(current); symbolicTrace.addTraceElement(current); } + /** The loop-head states reached since the last branch (see LoopStateMatcher). */ + private final List loopStates = new ArrayList<>(); + + /** Records the state at a loop head; it is reported with the next branch. */ + public void addLoopState(String state) { + loopStates.add(state); + } + + private void takeLoopStates(BranchElement branch) { + if (!loopStates.isEmpty()) { + branch.setLoopStates(List.copyOf(loopStates)); + loopStates.clear(); + } + } + /** Records where a branch is: its key and the change of the frame stack since the last branch. */ private static void place(BranchElement branch, long iid, String suffix) throws NoThreadContextException { String key = BranchKeys.keyOf(iid); @@ -96,6 +112,7 @@ public void addConcreteBranch(boolean result, long iid) throws NoThreadContextEx .getFormulaManager().getBooleanFormulaManager(); BranchElement branch = new BranchElement(result, bmgr.makeTrue(), iid, true); place(branch, iid, ""); + takeLoopStates(branch); symbolicTrace.addTraceElement(branch); } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/BranchDTO.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/BranchDTO.java index 5a917bb2..d8df3327 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/BranchDTO.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/BranchDTO.java @@ -32,6 +32,16 @@ public class BranchDTO { @com.fasterxml.jackson.annotation.JsonInclude(com.fasterxml.jackson.annotation.JsonInclude.Include.NON_DEFAULT) private boolean callback; + // See BranchElement: the loop-head states reached since the previous branch. + @SuppressWarnings("unused") + @com.fasterxml.jackson.annotation.JsonInclude(com.fasterxml.jackson.annotation.JsonInclude.Include.NON_EMPTY) + private java.util.List loopStates; + + public BranchDTO loopStates(java.util.List loopStates) { + this.loopStates = loopStates; + return this; + } + public BranchDTO place(String key, int pops, java.util.List pushes, boolean callback) { this.key = key; this.pops = pops; diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadContext.java b/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadContext.java index 38c571d8..b94a0408 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadContext.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadContext.java @@ -191,6 +191,15 @@ public void setStaticField(int cIdx, int fIdx, Value value) statics.get(cIdx)[fIdx] = value; } + /** The shadow values of the static fields accessed so far, keyed by class name. */ + public java.util.Map[]> getStaticFields() { + java.util.Map[]> byName = new java.util.HashMap<>(); + for (java.util.Map.Entry[]> e : statics.entrySet()) { + byName.put(classDepot.getClassName(e.getKey()), e.getValue()); + } + return byName; + } + public Value getStaticField(int classIndex, int runtimeFieldIndex) throws ThreadAlreadyEnabledException, ThreadAlreadyDisabledException, NoThreadContextException, ClassNotFoundException { SWATAssert.check(runtimeFieldIndex >= 0, "Field ID must be non-negative"); diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadHandler.java b/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadHandler.java index b83a3e8d..dcfab2a6 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadHandler.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/thread/ThreadHandler.java @@ -364,6 +364,16 @@ public static void setStaticField( } } + /** The shadow values of the static fields, by class: those the thread has accessed so far. */ + public static java.util.Map[]> getStaticFields(long id) throws NoThreadContextException { + ThreadContext context = threadContextHashMap.get(id); + if (context != null) { + return context.getStaticFields(); + } else { + throw new NoThreadContextException(id); + } + } + public static Value getStaticField(long id, int classIndex, int runtimeFieldIndex) throws ThreadAlreadyEnabledException, ThreadAlreadyDisabledException, NoThreadContextException, ClassNotFoundException { ThreadContext context = threadContextHashMap.get(id); diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/loopstate/LoopHeadsTest.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/loopstate/LoopHeadsTest.groovy new file mode 100644 index 00000000..92dd657a --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/loopstate/LoopHeadsTest.groovy @@ -0,0 +1,73 @@ +package de.uzl.its.swat.symbolic.loopstate + +import org.objectweb.asm.Label +import org.objectweb.asm.Opcodes +import org.objectweb.asm.tree.MethodNode +import spock.lang.Specification + +class LoopHeadsTest extends Specification { + + /** static void m(int n, long l) { int x = 0; while (x < n) { x++; } } */ + private static MethodNode countingLoop(boolean valueOnStack) { + MethodNode mn = new MethodNode(Opcodes.ASM9, Opcodes.ACC_STATIC, "m", "(IJ)V", null, null) + Label head = new Label() + Label end = new Label() + mn.visitCode() + mn.visitInsn(Opcodes.ICONST_0) + mn.visitVarInsn(Opcodes.ISTORE, 3) + if (valueOnStack) { + mn.visitInsn(Opcodes.ICONST_0) + } + mn.visitLabel(head) + mn.visitVarInsn(Opcodes.ILOAD, 3) + mn.visitVarInsn(Opcodes.ILOAD, 0) + mn.visitJumpInsn(Opcodes.IF_ICMPGE, end) + mn.visitIincInsn(3, 1) + mn.visitJumpInsn(Opcodes.GOTO, head) + mn.visitLabel(end) + if (valueOnStack) { + mn.visitInsn(Opcodes.POP) + } + mn.visitInsn(Opcodes.RETURN) + mn.visitMaxs(3, 4) + mn.visitEnd() + return mn + } + + def "finds the target of a backward jump and the locals defined there"() { + when: + def heads = LoopHeads.analyze("Fixture", countingLoop(false)) + + then: + heads.size() == 1 + def head = heads.values().first() + head.name() == "Fixture.m(IJ)V#0" + head.slots() as List == [0, 1, 3] + head.kinds() as List == ['I' as char, 'J' as char, 'I' as char] + LoopHeads.get(head.name()) == head + } + + def "skips a head with values on the operand stack"() { + expect: + LoopHeads.analyze("Fixture2", countingLoop(true)).isEmpty() + } + + def "a method without backward jumps has no heads"() { + given: + MethodNode mn = new MethodNode(Opcodes.ASM9, Opcodes.ACC_STATIC, "f", "(I)I", null, null) + Label skip = new Label() + mn.visitCode() + mn.visitVarInsn(Opcodes.ILOAD, 0) + mn.visitJumpInsn(Opcodes.IFEQ, skip) + mn.visitInsn(Opcodes.ICONST_1) + mn.visitInsn(Opcodes.IRETURN) + mn.visitLabel(skip) + mn.visitInsn(Opcodes.ICONST_0) + mn.visitInsn(Opcodes.IRETURN) + mn.visitMaxs(1, 1) + mn.visitEnd() + + expect: + LoopHeads.analyze("Fixture3", mn).isEmpty() + } +} From 1a4e0462d5f125671b3e51a654369f252149368b Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 23:31:27 +0000 Subject: [PATCH 2/7] Leave out branches below a repeated loop-head state The tree positions each loop-head state of a trace by (branches before it, their outcomes as a binary number, states before it) and keeps the smallest position of every state. dfs() does not offer a branch, nor any branch below it, that follows a state already reached at a smaller position: a smallest violating execution never passes such a state, since cutting out the part between the two occurrences gives a smaller one (see LoopStateMatcher). --no-loop-state-matching turns this off. Co-Authored-By: Claude Opus 5.5 --- symbolic-explorer/SymbolicExplorer.py | 1 + .../data/BinaryExecutionTree/Node.py | 4 + .../data/BinaryExecutionTree/Tree.py | 48 ++++++++++ symbolic-explorer/data/trace/Branch.py | 5 +- symbolic-explorer/driver/SVCompDriver.py | 2 + .../parse/DataTransferObjects.py | 2 + symbolic-explorer/parse/TraceParser.py | 3 +- symbolic-explorer/strategy/DFS.py | 6 ++ symbolic-explorer/strategy/StrategyService.py | 2 + .../tests/test_loop_state_matching.py | 95 +++++++++++++++++++ 10 files changed, 166 insertions(+), 2 deletions(-) create mode 100644 symbolic-explorer/tests/test_loop_state_matching.py diff --git a/symbolic-explorer/SymbolicExplorer.py b/symbolic-explorer/SymbolicExplorer.py index be21affd..761e50d8 100755 --- a/symbolic-explorer/SymbolicExplorer.py +++ b/symbolic-explorer/SymbolicExplorer.py @@ -136,6 +136,7 @@ def init_args(parser: argparse.ArgumentParser): parser.add_argument("--sa-retry-without", action="store_true", help="On a SAFE verdict reached with static pre-analysis, disable it and explore again (guards against false SAFE from incomplete SA)", default=False) parser.add_argument("--sa-no-callback-targets", action="store_true", help="Do not count library calls as possible asserts when application code that library code may call back (overrides of library methods, lambdas) can reach an assert. Unsound: an assert reached only through such a callback can then give a false SAFE", default=False) parser.add_argument("--sa-rank-distance", action="store_true", help="Try branches closest to an assert (by static pre-analysis graph distance) first, instead of in plain DFS order", default=False) + parser.add_argument("--no-loop-state-matching", action="store_true", help="Flip branches below a loop-head state that was already reached at a smaller position too (the executor reports loop-head states if its config sets loopStateMatching)", default=False) parser.add_argument("--solver-rlimit", type=int, default=0, help="Z3 resource limit (rlimit) for the first query of each branch in sv-comp mode; a branch that runs out is retried later with a growing limit. 0 (default): unlimited") parser.add_argument("--parallel-sa", action="store_true", help="Run the static pre-analysis in the background and use it once it is ready (sv-comp mode). By default exploration waits for it: running it in parallel makes runs nondeterministic", default=False) diff --git a/symbolic-explorer/data/BinaryExecutionTree/Node.py b/symbolic-explorer/data/BinaryExecutionTree/Node.py index 5a1fd91b..72068c60 100755 --- a/symbolic-explorer/data/BinaryExecutionTree/Node.py +++ b/symbolic-explorer/data/BinaryExecutionTree/Node.py @@ -62,6 +62,9 @@ def __init__(self, parent: Optional['Node'], trace: list, inputs: List[Input], u self.pops = 0 self.pushes = () self.callback = False # in a callback from library code: no counterpart in the SA graph + # Only for 'Branch' nodes: the loop-head states reached before this branch, since the + # previous one, each with its position (see Tree.register_loop_states). + self.loop_states = () # Validate trace argument if trace is None or len(trace) == 0: @@ -92,6 +95,7 @@ def __init__(self, parent: Optional['Node'], trace: list, inputs: List[Input], u self.pops = branch.pops self.pushes = branch.pushes self.callback = branch.callback + self.loop_states = getattr(branch, 'positioned_loop_states', ()) self.constraint[branch.trace_id] = branch.constraint # Determine whether the branch was taken or skipped and assign child if branch.has_branched: diff --git a/symbolic-explorer/data/BinaryExecutionTree/Tree.py b/symbolic-explorer/data/BinaryExecutionTree/Tree.py index 978dc99e..11f5e13b 100755 --- a/symbolic-explorer/data/BinaryExecutionTree/Tree.py +++ b/symbolic-explorer/data/BinaryExecutionTree/Tree.py @@ -10,6 +10,9 @@ logger = log.get_logger() class Tree: + # Whether dfs() leaves out the branches below a repeated loop-head state (--no-loop-state-matching). + LOOP_STATE_MATCHING = True + """ Represents a binary execution tree used to model decision points in an execution flow. @@ -48,6 +51,11 @@ def __init__(self, endpoint_id: Union[str, int]): # [SWAT Exception]s) that make the verdict untrustworthy. These cannot ride the trace # because they halt the executor JVM before it sends one, so they are surfaced here. self.execution_errors: list = [] + # Loop-head state matching: for each state hash, the smallest position at which an + # executed path reached it (see register_loop_states). + self.loop_state_first: dict[str, tuple] = {} + # Branches the last dfs() left out because of a repeated loop-head state. + self.loop_state_pruned = 0 def record_inputs(self, inputs: List[Input]): @@ -138,8 +146,48 @@ def add(self, trace: list[Branch | Special], inputs: List[Input], ufs: List[UF]) inputs (any): The inputs associated with the branch being added. ufs (any): The UFs associated with the branch being added. """ + self.register_loop_states(trace) self.root = self.add_recursive(None, self.root, trace.copy(), inputs, ufs) + def register_loop_states(self, trace: list[Branch | Special]): + """ + Positions the loop-head states of a trace and records the smallest position of each. + + The position of a state is (d, k, m): d branches precede it, k is the outcomes of those + branches read as a binary number (taken = 1, the first branch the most significant bit), and + m states precede it. Positions compare lexicographically. The state goes with the branch + that follows it: that branch, and every branch below it, needs no flip if the same state was + reached at a smaller position (see dominated_by_loop_state and the executor's + LoopStateMatcher for why). Two paths through the same tree node have the same prefix, so + the node's positions do not depend on the trace that created it. + """ + d, k, m = 0, 0, 0 + for element in trace: + if not isinstance(element, Branch): + continue + states = getattr(element, 'loop_states', ()) + if states: + positioned = [] + for state in states: + position = (d, k, m) + m += 1 + positioned.append((state, position)) + first = self.loop_state_first.get(state) + if first is None or position < first: + self.loop_state_first[state] = position + element.positioned_loop_states = tuple(positioned) + d += 1 + k = 2 * k + (1 if element.has_branched else 0) + + def dominated_by_loop_state(self, node: Node) -> bool: + """Whether a state reached before this branch was reached at a smaller position already.""" + if not Tree.LOOP_STATE_MATCHING: + return False + for state, position in node.loop_states: + if self.loop_state_first.get(state, position) < position: + return True + return False + def add_recursive(self, parent: Optional[Node], node: Optional[Union[Node, Leaf]], trace: list[Branch | Special], inputs: List[Input], ufs: List[UF]): """ Recursively adds nodes or leaves to the tree. diff --git a/symbolic-explorer/data/trace/Branch.py b/symbolic-explorer/data/trace/Branch.py index afc93cc8..1e623c06 100755 --- a/symbolic-explorer/data/trace/Branch.py +++ b/symbolic-explorer/data/trace/Branch.py @@ -14,7 +14,8 @@ class Branch: """ def __init__(self, id: int, trace_id: str, has_branched: bool, constraint: str, concrete_only: bool = False, - key: str | None = None, pops: int = 0, pushes: tuple = (), callback: bool = False): + key: str | None = None, pops: int = 0, pushes: tuple = (), callback: bool = False, + loop_states: tuple = ()): """ Initializes a new instance of the Branch class. @@ -37,6 +38,8 @@ def __init__(self, id: int, trace_id: str, has_branched: bool, constraint: str, self.pushes = pushes # In application code that library code called back, which the SA graph does not have. self.callback = callback + # The loop-head states reached since the previous branch (see Tree.register_loop_states). + self.loop_states = loop_states def __str__(self): return f'[(B) - {self.id} - ({"T" if self.has_branched else "F"})]' \ No newline at end of file diff --git a/symbolic-explorer/driver/SVCompDriver.py b/symbolic-explorer/driver/SVCompDriver.py index a6c70f11..f54d2ea5 100644 --- a/symbolic-explorer/driver/SVCompDriver.py +++ b/symbolic-explorer/driver/SVCompDriver.py @@ -12,6 +12,7 @@ from data.Database import Database from data.BinaryExecutionTree.Node import Node +from data.BinaryExecutionTree.Tree import Tree from strategy.StrategyService import StrategyService from data.StaticAnalysisGraph.SAGraph import SAGraph @@ -98,6 +99,7 @@ def __init__(self, args): self.solver_limit_hits = 0 # queries that ran out of their resource limit # How often each branch (by gid) ran out of its resource limit; each time multiplies it. self.rlimit_level: dict[int, int] = {} + Tree.LOOP_STATE_MATCHING = not getattr(args, 'no_loop_state_matching', False) @contextmanager def pushd(self, dirname): diff --git a/symbolic-explorer/parse/DataTransferObjects.py b/symbolic-explorer/parse/DataTransferObjects.py index 68be5da1..f8eede33 100644 --- a/symbolic-explorer/parse/DataTransferObjects.py +++ b/symbolic-explorer/parse/DataTransferObjects.py @@ -19,6 +19,8 @@ class TraceItem(BaseModel): pushes: list[Optional[str]] = [] # Recorded in application code that library code called back: not in the SA graph. callback: bool = False + # Hashes of the loop-head states the execution reached since the previous branch, in order. + loopStates: list[str] = [] class UFItem(BaseModel): definition: str diff --git a/symbolic-explorer/parse/TraceParser.py b/symbolic-explorer/parse/TraceParser.py index 8b005c7d..08eb934c 100755 --- a/symbolic-explorer/parse/TraceParser.py +++ b/symbolic-explorer/parse/TraceParser.py @@ -23,7 +23,8 @@ def parse_trace(trace: List[TraceItem], trace_id: str) -> List[Branch | Special] key=branch.key, pops=branch.pops, pushes=tuple(branch.pushes), - callback=branch.callback)) + callback=branch.callback, + loop_states=tuple(branch.loopStates))) else: _trace.append(Special(id=branch.iid, trace_id=trace_id, diff --git a/symbolic-explorer/strategy/DFS.py b/symbolic-explorer/strategy/DFS.py index b8d52078..20ad5830 100755 --- a/symbolic-explorer/strategy/DFS.py +++ b/symbolic-explorer/strategy/DFS.py @@ -50,6 +50,12 @@ def dfs(visited: set[Node], tree, node: Node | Leaf | None, solved_branches: set else: assert node.kind == "Branch" + # A state this path reached before the branch was reached at a smaller position already: + # nothing below can be reached only from here (Tree.register_loop_states). + if getattr(node, 'loop_states', ()) and tree.dominated_by_loop_state(node): + tree.loop_state_pruned += 1 + return possible_nodes + # The frames entered and left since the previous branch, which happened before this one. if sa_index is not None: trace_stack = apply_stack_delta(trace_stack, node.pops, node.pushes, sa_index) diff --git a/symbolic-explorer/strategy/StrategyService.py b/symbolic-explorer/strategy/StrategyService.py index 9afe6927..a9e051d0 100755 --- a/symbolic-explorer/strategy/StrategyService.py +++ b/symbolic-explorer/strategy/StrategyService.py @@ -26,6 +26,8 @@ def select_branch(**kwargs): # ties, and branches without SA information (ranked last), keep their DFS order. distances = {} if kwargs.get("rank_by_distance", False) else None possible_branches = dfs(visited, tree, tree.root, db.get_solutions().keys(), db.get_unsat_branches(), kwargs.get("sa_node", None), distances=distances) + if tree.loop_state_pruned: + logger.info(f'[DFS] Left out {tree.loop_state_pruned} subtrees below a repeated loop-head state') if distances: possible_branches.sort(key=lambda n: distances.get(n, math.inf)) # dfs records where the SA walk fell out of step on its tree, which is a copy. diff --git a/symbolic-explorer/tests/test_loop_state_matching.py b/symbolic-explorer/tests/test_loop_state_matching.py new file mode 100644 index 00000000..39e7954c --- /dev/null +++ b/symbolic-explorer/tests/test_loop_state_matching.py @@ -0,0 +1,95 @@ +""" +Unit tests for loop-head state matching: Tree positions the loop-head states the executor reports +with a trace, and dfs() leaves out the branches below a state that was reached at a smaller +position already. + +Run from symbolic-explorer/: + python3 -m unittest tests.test_loop_state_matching -v +""" + +import os +import sys +import unittest + +sys.path.insert(0, os.path.join(os.path.dirname(__file__), '..')) + +from data.BinaryExecutionTree.Tree import Tree +from data.trace.Branch import Branch +from strategy.DFS import dfs + +SYMBOLIC = '(declare-fun Z_0 () Bool)(assert Z_0)' + + +def trace(trace_id, *steps): + """Steps are (iid, taken) or (iid, taken, states).""" + branches = [] + for step in steps: + iid, taken = step[0], step[1] + states = step[2] if len(step) > 2 else () + branches.append(Branch(id=iid, trace_id=trace_id, has_branched=taken, constraint=SYMBOLIC, + loop_states=tuple(states))) + return branches + + +def open_branches(tree): + tree.loop_state_pruned = 0 + return sorted(n.id for n in dfs(set(), tree, tree.root, set(), set())) + + +class LoopStateMatchingTest(unittest.TestCase): + + def setUp(self): + Tree.LOOP_STATE_MATCHING = True + + def tearDown(self): + Tree.LOOP_STATE_MATCHING = True + + def test_positions(self): + tree = Tree(0) + t = trace('t1', (1, True, ['A']), (2, False), (3, True, ['B', 'A'])) + tree.add(t, [], []) + # (branches before, their outcomes as a binary number, states before) + self.assertEqual(tree.loop_state_first, {'A': (0, 0, 0), 'B': (2, 0b10, 1)}) + self.assertEqual(tree.root.branched.skipped.loop_states, (('B', (2, 0b10, 1)), ('A', (2, 0b10, 2)))) + + def test_repeated_state_on_one_path(self): + tree = Tree(0) + # A loop whose state repeats: the second visit of A comes before branch 3 + tree.add(trace('t1', (1, True, ['A']), (2, True), (3, True, ['A']), (4, True)), [], []) + self.assertEqual(open_branches(tree), [1, 2]) + self.assertEqual(tree.loop_state_pruned, 1) + + def test_state_reached_earlier_on_another_path(self): + tree = Tree(0) + tree.add(trace('t1', (1, True), (2, True), (3, True, ['S']), (4, True)), [], []) + self.assertEqual(open_branches(tree), [1, 2, 3, 4]) + # Another path reaches S after one branch: below the first occurrence nothing is new + tree.add(trace('t2', (1, False, []), (5, True, ['S']), (6, True)), [], []) + self.assertEqual(open_branches(tree), [2, 5, 6]) + + def test_same_depth_ordered_by_outcomes(self): + tree = Tree(0) + tree.add(trace('t1', (1, True), (2, True, ['S']), (3, True)), [], []) + tree.add(trace('t2', (1, False), (4, True, ['S']), (5, True)), [], []) + # Both after one branch; the path with outcome 0 (not taken) comes first + self.assertEqual(open_branches(tree), [4, 5]) + + def test_equal_positions_do_not_prune(self): + tree = Tree(0) + tree.add(trace('t1', (1, True, ['S']), (2, True, ['S'])), [], []) + # the second visit is after a branch, the first not: only the second is dominated + self.assertEqual(open_branches(tree), [1]) + tree2 = Tree(0) + tree2.add(trace('t1', (1, True, ['S']), (2, True)), [], []) + tree2.add(trace('t2', (1, True, ['S']), (2, False)), [], []) + self.assertEqual(open_branches(tree2), [1]) + + def test_disabled(self): + Tree.LOOP_STATE_MATCHING = False + tree = Tree(0) + tree.add(trace('t1', (1, True, ['A']), (2, True), (3, True, ['A']), (4, True)), [], []) + self.assertEqual(open_branches(tree), [1, 2, 3, 4]) + + +if __name__ == '__main__': + unittest.main() From b138c9d469555781ff8e1db44c6b2ec052456321 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 23:31:27 +0000 Subject: [PATCH 3/7] Enable loop-state matching in the SV-COMP configuration Co-Authored-By: Claude Opus 5.5 --- targets/sv-comp/sv-comp.cfg | 3 +++ 1 file changed, 3 insertions(+) diff --git a/targets/sv-comp/sv-comp.cfg b/targets/sv-comp/sv-comp.cfg index d66a6727..533c3a8d 100644 --- a/targets/sv-comp/sv-comp.cfg +++ b/targets/sv-comp/sv-comp.cfg @@ -29,3 +29,6 @@ constraintsOnly=false solver.mode=HTTP svcomp.randomInputs=false + +# Report loop-head states with the trace; the explorer prunes below repeated ones +loopStateMatching=true From 44a5a243bdaf2cc7adc49e96c464814c112cbcf4 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 23:33:33 +0000 Subject: [PATCH 4/7] Bound the time a run spends on loop-head states A run stops hashing once it has spent a second on it, or once a state repeats on its path (the explorer leaves out everything after the repeat anyway). Reporting fewer states only means fewer branches are left out. Co-Authored-By: Claude Opus 5.5 --- .../symbolic/loopstate/LoopStateMatcher.java | 28 +++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/loopstate/LoopStateMatcher.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/loopstate/LoopStateMatcher.java index 452fe05c..dc4691b0 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/loopstate/LoopStateMatcher.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/loopstate/LoopStateMatcher.java @@ -64,6 +64,20 @@ public final class LoopStateMatcher { private static final String SWAT_PACKAGE = "de/uzl/its/swat/"; + /** + * Time one run may spend on hashing. Leaving out a state is always sound (no branch is left + * out because of it), so once the budget is used up the run reports no more states. + */ + private static final long BUDGET_NANOS = 1_000_000_000L; + + private static long spentNanos = 0; + + /** The states this run reported. */ + private static final java.util.Set seen = new java.util.HashSet<>(); + + /** Whether the run reports no more states: the budget is used up or a state repeated. */ + private static boolean stopped = false; + private LoopStateMatcher() {} /** Thrown when the state cannot be hashed. */ @@ -93,19 +107,33 @@ private static Unhashable unhashable(String why) { */ public static String stateOf( LOOP_HEAD inst, ShadowContext shadow, Map[]> shadowStatics, int threads) { + if (stopped) { + return null; + } LoopHeads.Head head = LoopHeads.get(inst.head); if (head == null || threads != 1 || inst.locals.length != head.slots().length) { logger.debug("[LOOP STATE] Not hashed: unknown head or several threads"); return null; } + long start = System.nanoTime(); try { checkStack(head); checkShadow(head, shadow, shadowStatics); String h = hash(head, inst.locals); logger.debug("[LOOP STATE] {}: {}", inst.head, h); + if (!seen.add(h)) { + // The explorer leaves out everything after a repeat on this path anyway + stopped = true; + } return h; } catch (Unhashable e) { return null; + } finally { + spentNanos += System.nanoTime() - start; + if (spentNanos > BUDGET_NANOS) { + logger.debug("[LOOP STATE] Time budget used up, no more states this run"); + stopped = true; + } } } From 22e3844977d5158e756d6d024f134144da313f7e Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Mon, 19 Oct 2026 15:41:54 +0000 Subject: [PATCH 5/7] Count a symbolic array length as symbolic An Object[] created with a symbolic length kept isSymbolic() false as long as its elements were concrete, and a primitive array only looked at its element formula. Both now also count a symbolic size. Besides loop-state matching, this makes an unmodelled call that receives such an array a symbolic call (context loss), as it should be. Co-Authored-By: Claude Opus 5.5 --- .../value/reference/array/AbstractArrayValue.java | 2 +- .../value/reference/array/ObjectArrayValue.java | 11 +++++++++++ 2 files changed, 12 insertions(+), 1 deletion(-) diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/array/AbstractArrayValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/array/AbstractArrayValue.java index 361c8f06..8ee1e4fa 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/array/AbstractArrayValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/array/AbstractArrayValue.java @@ -256,7 +256,7 @@ public BooleanFormula getBounds(boolean upper) { @Override public boolean isSymbolic() { - return !context.getFormulaManager().extractVariables(formula).isEmpty(); + return !context.getFormulaManager().extractVariables(formula).isEmpty() || size.isSymbolic(); } @Override diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/array/ObjectArrayValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/array/ObjectArrayValue.java index 1910f6c8..416093a8 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/array/ObjectArrayValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/array/ObjectArrayValue.java @@ -1,6 +1,7 @@ package de.uzl.its.swat.symbolic.value.reference.array; import de.uzl.its.swat.common.exceptions.NoThreadContextException; +import de.uzl.its.swat.common.exceptions.NotImplementedException; import de.uzl.its.swat.symbolic.value.Value; import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.IntValue; import de.uzl.its.swat.symbolic.value.reference.ObjectValue; @@ -88,4 +89,14 @@ public IntValue getSize() { public String toString() { return "[" + className + " @" + Integer.toHexString(address) + " (" + size + " x 1" + ")"; } + + /** Symbolic if an element is, or if the length is (e.g. {@code new Object[n]} for a symbolic n). */ + @Override + @SuppressWarnings({"rawtypes", "unchecked"}) + public boolean isSymbolic(java.util.Set visited) throws NotImplementedException, RuntimeException { + if (!visited.contains(this) && size != null && size.isSymbolic()) { + return true; + } + return super.isSymbolic(visited); + } } From ca0f2a5a00a0cdb3e7cb5eb174a583e01f8ebc74 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Mon, 19 Oct 2026 15:41:54 +0000 Subject: [PATCH 6/7] Stop reporting loop states after a call into untracked code A library call (or an access to a static field of an untracked class) can read or change state outside the hashed state: a System property, the thread interrupt flag, the statics of a class in an excluded package. A run therefore reports no more loop-head states once it makes such a call, apart from the Verifier, Math/StrictMath and the static helpers of Double/Float/Integer/Long (without getInteger/getLong). Every reported state then has a prefix without such calls. Co-Authored-By: Claude Opus 5.5 --- .../symbolic/SymbolicInstructionVisitor.java | 7 +++ .../symbolic/loopstate/LoopStateMatcher.java | 49 +++++++++++++++++++ 2 files changed, 56 insertions(+) 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 79675ee7..20c28c2b 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 @@ -1307,6 +1307,7 @@ public void visitGETFIELD(GETFIELD inst) throws SymbolicInstructionException { */ public void visitGETSTATIC(GETSTATIC inst) throws SymbolicInstructionException { try { + LoopStateMatcher.staticField(classDepot.getClassName(inst.cIdx)); Value val; val = fetchStaticField(inst); if (val == PlaceHolder.instance) { @@ -2335,6 +2336,7 @@ private void recordThrowingCall(long iid, String owner, String name, String desc */ public void visitINVOKEINTERFACE(INVOKEINTERFACE inst) throws SymbolicInstructionException { try { + LoopStateMatcher.call(inst.owner, inst.name, false); stack.newStackFrame(inst.desc, inst.owner, inst.name, true, inst.iid); if (stack.getNextInst() instanceof INVOKEMETHOD_END) { @@ -2372,6 +2374,7 @@ public void visitINVOKEINTERFACE(INVOKEINTERFACE inst) throws SymbolicInstructio */ public void visitINVOKESPECIAL(INVOKESPECIAL inst) throws SymbolicInstructionException { try { + LoopStateMatcher.call(inst.owner, inst.name, false); stack.newStackFrame(inst.desc, inst.owner, inst.name, true, inst.iid); if (stack.getNextInst() instanceof INVOKEMETHOD_END) { @@ -2407,6 +2410,7 @@ public void visitINVOKESPECIAL(INVOKESPECIAL inst) throws SymbolicInstructionExc */ public void visitINVOKESTATIC(INVOKESTATIC inst) throws SymbolicInstructionException { try { + LoopStateMatcher.call(inst.owner, inst.name, true); stack.newStackFrame(inst.desc, inst.owner, inst.name, false, inst.iid); if (stack.getNextInst() instanceof INVOKEMETHOD_END) { @@ -2441,6 +2445,7 @@ public void visitINVOKESTATIC(INVOKESTATIC inst) throws SymbolicInstructionExcep */ public void visitINVOKEVIRTUAL(INVOKEVIRTUAL inst) throws SymbolicInstructionException { try { + LoopStateMatcher.call(inst.owner, inst.name, false); if (previousWasUnpack && isStaticMethod(inst.owner, inst.name, inst.desc)) { // A static method called through Method.invoke: the instrumentation invokes it like // an instance method, with Method.invoke's (null) receiver below the arguments. @@ -2489,6 +2494,7 @@ public void visitINVOKEVIRTUAL(INVOKEVIRTUAL inst) throws SymbolicInstructionExc */ public void visitINVOKEDYNAMIC(INVOKEDYNAMIC inst) throws SymbolicInstructionException { try { + LoopStateMatcher.invokeDynamic(); stack.newStackFrame(inst.desc, inst.owner, inst.name, false, inst.iid); if (stack.getNextInst() instanceof INVOKEMETHOD_END) { @@ -3435,6 +3441,7 @@ private void setStaticField(Value value, int cIdx, String name) */ public void visitPUTSTATIC(PUTSTATIC inst) throws SymbolicInstructionException { try { + LoopStateMatcher.staticField(classDepot.getClassName(inst.cIdx)); Value value; if (inst.desc.startsWith("D") || inst.desc.startsWith("J")) { value = stack.popWideOperand(); diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/loopstate/LoopStateMatcher.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/loopstate/LoopStateMatcher.java index dc4691b0..4074e46f 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/loopstate/LoopStateMatcher.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/loopstate/LoopStateMatcher.java @@ -137,6 +137,53 @@ public static String stateOf( } } + /** + * Notes a method call of the run. A call into code that is not tracked, other than a few pure + * methods, may read or change state outside the hashed state (a System property, the interrupt + * flag, the static fields of a class in an excluded package): the run reports no more states. + * Every state a run reports thus has a prefix without such calls, so the hidden state is the + * initial one wherever it is reported. + */ + public static void call(String owner, String name, boolean isStatic) { + if (!stopped && !isPureCall(owner.replace('.', '/'), name, isStatic)) { + logger.debug("[LOOP STATE] Call to {}.{}, no more states this run", owner, name); + stopped = true; + } + } + + /** An invokedynamic call site (lambdas, string concatenation) runs library code. */ + public static void invokeDynamic() { + stopped = true; + } + + /** Notes an access to a static field: one of an untracked class is state outside the hash. */ + public static void staticField(String owner) { + if (!stopped && owner != null) { + String name = owner.replace('.', '/'); + if (!name.startsWith(SWAT_PACKAGE) && !isApplicationClassName(name)) { + logger.debug("[LOOP STATE] Static field of {}, no more states this run", owner); + stopped = true; + } + } + } + + private static boolean isPureCall(String owner, String name, boolean isStatic) { + if (owner.startsWith(SWAT_PACKAGE) || isApplicationClassName(owner)) { + return true; // tracked code (SWAT's Verifier included) + } + switch (owner) { + case "org/sosy_lab/sv_benchmarks/Verifier", "java/lang/Math", "java/lang/StrictMath": + return true; + case "java/lang/Object": + return name.equals(""); + case "java/lang/Double", "java/lang/Float", "java/lang/Integer", "java/lang/Long": + // getInteger and getLong read System properties + return isStatic && !name.equals("getInteger") && !name.equals("getLong"); + default: + return false; + } + } + /** The head's method must be the only application frame on the stack. */ private static void checkStack(LoopHeads.Head head) throws Unhashable { List app = StackWalker.getInstance().walk(s -> s @@ -236,6 +283,8 @@ private static String hash(LoopHeads.Head head, Object[] locals) throws Unhashab } } } catch (IOException | ReflectiveOperationException | RuntimeException | LinkageError e) { + // Includes a class whose initialization failed: reflection on it throws + // NoClassDefFoundError, and its state cannot be read, so it must stay unhashable. throw unhashable("reflection failed"); } byte[] digest = md.digest(); From 730db3a05e951d09c0c7e7e32fc4c7716a2ceeff Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Mon, 19 Oct 2026 15:41:54 +0000 Subject: [PATCH 7/7] Add loop-state matching soundness tasks Six VIOLATION tasks where a loop-state match would hide the violation: a symbolic Object[] length (valid-assert, no-runtime-exception, unbounded loop), a System property, the interrupt flag, and a class in an excluded package. build.sh now compiles a task's sources in package subfolders too. Co-Authored-By: Claude Opus 5.5 --- targets/sv-comp/swat-benchmarks/README.md | 6 +++++ .../loop-state/excluded-package_false.yml | 9 +++++++ .../excluded-package_false/Main.java | 12 ++++++++++ .../com/google/loopstate/Counter.java | 7 ++++++ .../java/loop-state/interrupt-flag_false.yml | 9 +++++++ .../loop-state/interrupt-flag_false/Main.java | 19 +++++++++++++++ .../loop-state/objarray-length-nre_false.yml | 9 +++++++ .../objarray-length-nre_false/Main.java | 22 +++++++++++++++++ .../objarray-length-unbounded_false.yml | 9 +++++++ .../objarray-length-unbounded_false/Main.java | 21 ++++++++++++++++ .../java/loop-state/objarray-length_false.yml | 9 +++++++ .../objarray-length_false/Main.java | 24 +++++++++++++++++++ .../java/loop-state/system-property_false.yml | 9 +++++++ .../system-property_false/Main.java | 13 ++++++++++ .../sv-comp/swat-benchmarks/scripts/build.sh | 2 +- 15 files changed, 179 insertions(+), 1 deletion(-) create mode 100644 targets/sv-comp/swat-benchmarks/java/loop-state/excluded-package_false.yml create mode 100644 targets/sv-comp/swat-benchmarks/java/loop-state/excluded-package_false/Main.java create mode 100644 targets/sv-comp/swat-benchmarks/java/loop-state/excluded-package_false/com/google/loopstate/Counter.java create mode 100644 targets/sv-comp/swat-benchmarks/java/loop-state/interrupt-flag_false.yml create mode 100644 targets/sv-comp/swat-benchmarks/java/loop-state/interrupt-flag_false/Main.java create mode 100644 targets/sv-comp/swat-benchmarks/java/loop-state/objarray-length-nre_false.yml create mode 100644 targets/sv-comp/swat-benchmarks/java/loop-state/objarray-length-nre_false/Main.java create mode 100644 targets/sv-comp/swat-benchmarks/java/loop-state/objarray-length-unbounded_false.yml create mode 100644 targets/sv-comp/swat-benchmarks/java/loop-state/objarray-length-unbounded_false/Main.java create mode 100644 targets/sv-comp/swat-benchmarks/java/loop-state/objarray-length_false.yml create mode 100644 targets/sv-comp/swat-benchmarks/java/loop-state/objarray-length_false/Main.java create mode 100644 targets/sv-comp/swat-benchmarks/java/loop-state/system-property_false.yml create mode 100644 targets/sv-comp/swat-benchmarks/java/loop-state/system-property_false/Main.java diff --git a/targets/sv-comp/swat-benchmarks/README.md b/targets/sv-comp/swat-benchmarks/README.md index 758a2cf9..1089ad24 100644 --- a/targets/sv-comp/swat-benchmarks/README.md +++ b/targets/sv-comp/swat-benchmarks/README.md @@ -39,6 +39,12 @@ every pair the assert is `if (x > 1000 && x < HI) assert false;` with HI = 10000 1001 (SAFE), and it is only reached after flipping an input-dependent branch that the risky construct sits on. Each task's comment says what it tests. +`loop-state`: hand-written VIOLATION tasks against loop-head state matching, each a case where a +match would hide a violation: an `Object[]` whose length is symbolic (also under +`no-runtime-exception`, and with an unbounded loop), state held by the JDK (a System property, the +thread interrupt flag), and a class in a package SWAT does not instrument. None may come out SAFE; +the unbounded variant may time out. + `real-tools` (`scripts/tools.py`, harnesses in `scripts/tools/`): harnesses around unmodified GNU java-getopt 1.0.13 (`getopt-minitar`, a tar-like CLI) and opencsv 2.3's `CSVParser` (`opencsv-import`). The tools are not in the repository: `scripts/fetch_tools.sh` downloads their diff --git a/targets/sv-comp/swat-benchmarks/java/loop-state/excluded-package_false.yml b/targets/sv-comp/swat-benchmarks/java/loop-state/excluded-package_false.yml new file mode 100644 index 00000000..fbe9560d --- /dev/null +++ b/targets/sv-comp/swat-benchmarks/java/loop-state/excluded-package_false.yml @@ -0,0 +1,9 @@ +format_version: '2.0' +input_files: + - ../common/ + - excluded-package_false/ +properties: + - property_file: ../properties/valid-assert.prp + expected_verdict: false +options: + language: Java diff --git a/targets/sv-comp/swat-benchmarks/java/loop-state/excluded-package_false/Main.java b/targets/sv-comp/swat-benchmarks/java/loop-state/excluded-package_false/Main.java new file mode 100644 index 00000000..a4cba08f --- /dev/null +++ b/targets/sv-comp/swat-benchmarks/java/loop-state/excluded-package_false/Main.java @@ -0,0 +1,12 @@ +// Loop-state matching: Counter lives in a package SWAT does not instrument (com/google), so its +// static field is outside the hashed state. +import org.sosy_lab.sv_benchmarks.Verifier; +import com.google.loopstate.Counter; + +public class Main { + public static void main(String[] args) { + while (Verifier.nondetBoolean()) { + if (Counter.inc() == 3) assert false; + } + } +} diff --git a/targets/sv-comp/swat-benchmarks/java/loop-state/excluded-package_false/com/google/loopstate/Counter.java b/targets/sv-comp/swat-benchmarks/java/loop-state/excluded-package_false/com/google/loopstate/Counter.java new file mode 100644 index 00000000..84b406e8 --- /dev/null +++ b/targets/sv-comp/swat-benchmarks/java/loop-state/excluded-package_false/com/google/loopstate/Counter.java @@ -0,0 +1,7 @@ +package com.google.loopstate; + +public class Counter { + public static int c; + + public static int inc() { return ++c; } +} diff --git a/targets/sv-comp/swat-benchmarks/java/loop-state/interrupt-flag_false.yml b/targets/sv-comp/swat-benchmarks/java/loop-state/interrupt-flag_false.yml new file mode 100644 index 00000000..1fb419c0 --- /dev/null +++ b/targets/sv-comp/swat-benchmarks/java/loop-state/interrupt-flag_false.yml @@ -0,0 +1,9 @@ +format_version: '2.0' +input_files: + - ../common/ + - interrupt-flag_false/ +properties: + - property_file: ../properties/valid-assert.prp + expected_verdict: false +options: + language: Java diff --git a/targets/sv-comp/swat-benchmarks/java/loop-state/interrupt-flag_false/Main.java b/targets/sv-comp/swat-benchmarks/java/loop-state/interrupt-flag_false/Main.java new file mode 100644 index 00000000..b082f7d9 --- /dev/null +++ b/targets/sv-comp/swat-benchmarks/java/loop-state/interrupt-flag_false/Main.java @@ -0,0 +1,19 @@ +// Loop-state matching: the thread interrupt flag is state outside the hash. Two paths reach the +// same hashed state with the flag clear and set; Thread.interrupted() later tells them apart. +import org.sosy_lab.sv_benchmarks.Verifier; + +public class Main { + public static void main(String[] args) { + if (Verifier.nondetBoolean()) { + if (Verifier.nondetBoolean()) { args = args; } // smaller position: flag clear + } else { + Thread.currentThread().interrupt(); // larger position: flag set, same hashed state + if (Verifier.nondetBoolean()) { args = args; } + } + for (int i = 0; i < 2; i++) { + if (Verifier.nondetBoolean()) { + if (Thread.interrupted()) assert false; + } + } + } +} diff --git a/targets/sv-comp/swat-benchmarks/java/loop-state/objarray-length-nre_false.yml b/targets/sv-comp/swat-benchmarks/java/loop-state/objarray-length-nre_false.yml new file mode 100644 index 00000000..0f9a043a --- /dev/null +++ b/targets/sv-comp/swat-benchmarks/java/loop-state/objarray-length-nre_false.yml @@ -0,0 +1,9 @@ +format_version: '2.0' +input_files: + - ../common/ + - objarray-length-nre_false/ +properties: + - property_file: ../properties/no-runtime-exception.prp + expected_verdict: false +options: + language: Java diff --git a/targets/sv-comp/swat-benchmarks/java/loop-state/objarray-length-nre_false/Main.java b/targets/sv-comp/swat-benchmarks/java/loop-state/objarray-length-nre_false/Main.java new file mode 100644 index 00000000..21393e2c --- /dev/null +++ b/targets/sv-comp/swat-benchmarks/java/loop-state/objarray-length-nre_false/Main.java @@ -0,0 +1,22 @@ +// As objarray-length_false, under no-runtime-exception: the violation is an IllegalStateException. +import org.sosy_lab.sv_benchmarks.Verifier; + +public class Main { + public static void main(String[] args) { + int n = Verifier.nondetInt(); + if (n < 0 || n > 3) return; + Object[] a = new Object[n]; // the shadow length stays symbolic + n = 0; // n dead: only a.length carries the input + // javac: a true condition falls through (outcome 0), so the then-side has the smaller position + if (Verifier.nondetBoolean()) { + if (a.length != 0) return; // the smaller path pins a.length == 0 + } else { + if (Verifier.nondetBoolean()) { n = 0; } // same number of branches, a.length unconstrained + } + for (int i = 0; i < 2; i++) { // bounded: the baseline explores everything + if (Verifier.nondetBoolean()) { + if (a.length == 2) throw new IllegalStateException(); + } + } + } +} diff --git a/targets/sv-comp/swat-benchmarks/java/loop-state/objarray-length-unbounded_false.yml b/targets/sv-comp/swat-benchmarks/java/loop-state/objarray-length-unbounded_false.yml new file mode 100644 index 00000000..817594a6 --- /dev/null +++ b/targets/sv-comp/swat-benchmarks/java/loop-state/objarray-length-unbounded_false.yml @@ -0,0 +1,9 @@ +format_version: '2.0' +input_files: + - ../common/ + - objarray-length-unbounded_false/ +properties: + - property_file: ../properties/valid-assert.prp + expected_verdict: false +options: + language: Java diff --git a/targets/sv-comp/swat-benchmarks/java/loop-state/objarray-length-unbounded_false/Main.java b/targets/sv-comp/swat-benchmarks/java/loop-state/objarray-length-unbounded_false/Main.java new file mode 100644 index 00000000..a8727c68 --- /dev/null +++ b/targets/sv-comp/swat-benchmarks/java/loop-state/objarray-length-unbounded_false/Main.java @@ -0,0 +1,21 @@ +// As objarray-length_false, with an unbounded loop: a wrong match gives SAFE where the search can +// never finish otherwise. +import org.sosy_lab.sv_benchmarks.Verifier; + +public class Main { + public static void main(String[] args) { + int n = Verifier.nondetInt(); + if (n < 0 || n > 3) return; + Object[] a = new Object[n]; + n = 0; // n dead: only a.length carries the input + // javac: a true condition falls through (outcome 0), so the then-side has the smaller position + if (Verifier.nondetBoolean()) { + if (a.length != 0) return; // the smaller path pins a.length == 0 + } else { + if (Verifier.nondetBoolean()) { n = 0; } // same number of branches, a.length unconstrained + } + while (Verifier.nondetBoolean()) { + if (a.length == 2) assert false; + } + } +} diff --git a/targets/sv-comp/swat-benchmarks/java/loop-state/objarray-length_false.yml b/targets/sv-comp/swat-benchmarks/java/loop-state/objarray-length_false.yml new file mode 100644 index 00000000..fe5eccb1 --- /dev/null +++ b/targets/sv-comp/swat-benchmarks/java/loop-state/objarray-length_false.yml @@ -0,0 +1,9 @@ +format_version: '2.0' +input_files: + - ../common/ + - objarray-length_false/ +properties: + - property_file: ../properties/valid-assert.prp + expected_verdict: false +options: + language: Java diff --git a/targets/sv-comp/swat-benchmarks/java/loop-state/objarray-length_false/Main.java b/targets/sv-comp/swat-benchmarks/java/loop-state/objarray-length_false/Main.java new file mode 100644 index 00000000..6098ac25 --- /dev/null +++ b/targets/sv-comp/swat-benchmarks/java/loop-state/objarray-length_false/Main.java @@ -0,0 +1,24 @@ +// Loop-state matching: the length of new Object[n] stays symbolic after n is dead, so the state at +// the loop head is not concrete and must not be matched (a path that pins a.length == 0 would +// otherwise cut off one that can reach a.length == 2). +import org.sosy_lab.sv_benchmarks.Verifier; + +public class Main { + public static void main(String[] args) { + int n = Verifier.nondetInt(); + if (n < 0 || n > 3) return; + Object[] a = new Object[n]; // the shadow length stays symbolic + n = 0; // n dead: only a.length carries the input + // javac: a true condition falls through (outcome 0), so the then-side has the smaller position + if (Verifier.nondetBoolean()) { + if (a.length != 0) return; // the smaller path pins a.length == 0 + } else { + if (Verifier.nondetBoolean()) { n = 0; } // same number of branches, a.length unconstrained + } + for (int i = 0; i < 2; i++) { // bounded: the baseline explores everything + if (Verifier.nondetBoolean()) { + if (a.length == 2) assert false; + } + } + } +} diff --git a/targets/sv-comp/swat-benchmarks/java/loop-state/system-property_false.yml b/targets/sv-comp/swat-benchmarks/java/loop-state/system-property_false.yml new file mode 100644 index 00000000..6cafe71f --- /dev/null +++ b/targets/sv-comp/swat-benchmarks/java/loop-state/system-property_false.yml @@ -0,0 +1,9 @@ +format_version: '2.0' +input_files: + - ../common/ + - system-property_false/ +properties: + - property_file: ../properties/valid-assert.prp + expected_verdict: false +options: + language: Java diff --git a/targets/sv-comp/swat-benchmarks/java/loop-state/system-property_false/Main.java b/targets/sv-comp/swat-benchmarks/java/loop-state/system-property_false/Main.java new file mode 100644 index 00000000..33649e7e --- /dev/null +++ b/targets/sv-comp/swat-benchmarks/java/loop-state/system-property_false/Main.java @@ -0,0 +1,13 @@ +// Loop-state matching: the loop keeps its counter in a System property, outside the hashed state. +// A run stops reporting states once it calls into the library. +import org.sosy_lab.sv_benchmarks.Verifier; + +public class Main { + public static void main(String[] args) { + while (Verifier.nondetBoolean()) { + int c = Integer.getInteger("loopstate.c", 0) + 1; + System.setProperty("loopstate.c", Integer.toString(c)); + if (c == 3) assert false; + } + } +} diff --git a/targets/sv-comp/swat-benchmarks/scripts/build.sh b/targets/sv-comp/swat-benchmarks/scripts/build.sh index 8b299598..55aed04d 100755 --- a/targets/sv-comp/swat-benchmarks/scripts/build.sh +++ b/targets/sv-comp/swat-benchmarks/scripts/build.sh @@ -21,6 +21,6 @@ for suite in $suites; do cp="$cp:$lib" done find "$JAVA_DIR/$suite" -mindepth 1 -maxdepth 1 -type d ! -name 'lib-*' \ - | xargs -r -P 32 -I{} sh -c "find {} -name '*.class' -delete && javac $JAVAC_FLAGS -cp '$cp' -d {} {}/*.java" + | xargs -r -P 32 -I{} sh -c "find {} -name '*.class' -delete && javac $JAVAC_FLAGS -cp '$cp' -d {} \$(find {} -name '*.java')" done echo "Built $(find "$JAVA_DIR" -name Main.class | wc -l) tasks."