Loop-head state matching for concrete loop states

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);
     }
 

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("<clinit>")) {
+            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, "<clinit>", "()V", null, null);
+            if (mv != null) {
+                mv.visitCode();
+                LoopHeads.emitClassInit(mv, cname);
+                mv.visitInsn(Opcodes.RETURN);
+                mv.visitMaxs(1, 0);
+                mv.visitEnd();
+            }
+        }
+        super.visitEnd();
+    }
 }

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("<clinit>")) {
+            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<Label, LoopHeads.Head> loopHeads = java.util.Map.of();
+
+    public void setLoopHeads(java.util.Map<Label, LoopHeads.Head> 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);

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: <a

symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/dispatcher/InstructionLoggingDispatcher.java

@@ -3556,6 +3556,12 @@ public static void MAKE_SYMBOLIC(long iid) throws NoThreadContextException {
      * @param iid The unique instruction ID set during instrumentation.
      */
     @SuppressWarnings("unused")
+    public static void LOOP_HEAD(long iid, String head, Object[] locals) throws NoThreadContextException {
+    Logger logger = ThreadHandler.getShadowStateLogger(-1);
+    logger.info("LOOP_HEAD {} {}", iid, head);
+}
+
+    @SuppressWarnings("unused")
     public static void LOOP_BEGIN(long iid) throws NoThreadContextException {
     Logger logger = ThreadHandler.getShadowStateLogger(-1);
     logger.info("LOOP_BEGIN {}", iid);

symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/dispatcher/NopDispatcher.java

@@ -3012,6 +3012,9 @@ public static void MAKE_SYMBOLIC(long iid) {}
     @SuppressWarnings("unused")
     public static void LOOP_BEGIN(long iid) {}
 
+    @SuppressWarnings("unused")
+    public static void LOOP_HEAD(long iid, String head, Object[] locals) {}
+
 
     /**
      * Method used to interact between the concrete and symbolic execution. The call to this method

symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/dispatcher/SymbolicInstructionDispatcher.java

@@ -3554,6 +3554,13 @@ public static void MAKE_SYMBOLIC(long iid) {
      *
      * @param iid The unique instruction ID set during instrumentation.
      */
+    @SuppressWarnings("unused")
+    public static void LOOP_HEAD(long iid, String head, Object[] locals) {
+        InstructionProcessor instructionProcessor =
+                ThreadHandler.getProcessor(Thread.currentThread().getId());
+        instructionProcessor.LOOP_HEAD(iid, head, locals);
+    }
+
     @SuppressWarnings("unused")
     public static void LOOP_BEGIN(long iid) {
         InstructionProcessor instructionProcessor =

symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/instruction/IVisitor.java

@@ -359,6 +359,8 @@ public interface IVisitor {
 
     void visitLOOP_BEGIN(LOOP_BEGIN inst) throws SymbolicInstructionException;
 
+    void visitLOOP_HEAD(LOOP_HEAD inst) throws SymbolicInstructionException;
+
     void visitLOOP_END(LOOP_END inst) throws SymbolicInstructionException;
 
     void visitSPECIAL(SPECIAL inst) throws SymbolicInstructionException;

symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/instruction/LOOP_HEAD.java

@@ -0,0 +1,31 @@
+package de.uzl.its.swat.symbolic.instruction;
+
+import de.uzl.its.swat.common.exceptions.SymbolicInstructionException;
+
+/**
+ * LOOP_HEAD - Probe at the target of a backward jump, carrying the concrete values of the locals
+ * defined there (see {@link de.uzl.its.swat.symbolic.loopstate.LoopHeads}).
+ */
+public class LOOP_HEAD extends Instruction {
+
+    /** The loop head's stable name: class, method and position (see LoopHeads). */
+    public final String head;
+
+    /** The values of the head's locals, in the order LoopHeads lists their slots. */
+    public final Object[] locals;
+
+    public LOOP_HEAD(long iid, String head, Object[] locals) {
+        super(iid);
+        this.head = head;
+        this.locals = locals;
+    }
+
+    public void accept(IVisitor visitor) throws SymbolicInstructionException {
+        visitor.visitLOOP_HEAD(this);
+    }
+
+    @Override
+    public String toString() {
+        return genericToString("[LOOP HEAD] " + head);
+    }
+}

symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/loopstate/ClassInits.java

@@ -0,0 +1,26 @@
+package de.uzl.its.swat.symbolic.loopstate;
+
+import java.util.Set;
+import java.util.TreeSet;
+
+/**
+ * The application classes whose initialization has started. The instrumentation calls
+ * {@link #started} first thing in every application class's static initializer (and adds one to a
+ * class that has none), so the set is exact: a class missing from it is uninitialized, its static
+ * fields still hold their defaults and its initializer is still to run.
+ */
+public final class ClassInits {
+
+    private static final Set<String> 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]);
+    }
+}