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..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 @@ -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; @@ -1306,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) { @@ -2334,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) { @@ -2371,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) { @@ -2406,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) { @@ -2440,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. @@ -2488,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) { @@ -3434,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(); @@ -3633,6 +3641,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..4074e46f --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/loopstate/LoopStateMatcher.java @@ -0,0 +1,409 @@ +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/"; + + /** + * 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. */ + 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) { + 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; + } + } + } + + /** + * 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 + .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) { + // 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(); + 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/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); + } } 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() + } +} 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() 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 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."