Changes needed to benchmark tracing

Author: MaartenS11

src/main/kotlin/be/ugent/topl/mio/concolic/Analyse.kt

@@ -16,7 +16,7 @@ data class SymbolicValueMapping(val primitive: String, val arg: Int, val value:
 
 data class ConcolicAnalysisResult(val paths: List<SymbolicValueMapping>)
 
-fun analyse(wdcliPath: String, wasmFile: String, jsonSnapshot: String, maxInstructions: Int = 50, maxSymbolicVariables: Int = -1, maxIterations: Int = -1, stopPc: Int = -1): ConcolicAnalysisResult {
+fun analyse(wdcliPath: String, wasmFile: String, jsonSnapshot: String, maxInstructions: Int = 50, maxSymbolicVariables: Int = -1, maxIterations: Int = -1, stopPc: Int = -1): ConcolicAnalysisResult? {
     val woodState = WOODState.fromLine(jsonSnapshot)
     val messages = woodState.toBinary(io = false, overrides = false).map { it.trim('\n', ' ') }
     for (msg in messages) {
@@ -47,7 +47,7 @@ fun analyse(wdcliPath: String, wasmFile: String, jsonSnapshot: String, maxInstru
         println(line)
     }
     println("Error occurred while running the following command: \"${command.joinToString(" ")}\"")
-    throw Exception("Failed to get result from analysis")
+    return null
 }
 
 fun process(r: ConcolicAnalysisResult): MultiverseNode {

src/main/kotlin/be/ugent/topl/mio/debugger/Debugger.kt

@@ -19,17 +19,17 @@ open class Debugger(private val connection: Connection, start: Boolean = true, p
     private val requestQueue: Queue<Int> = LinkedList()
     var printListener: ((String) -> Unit)? = null
     private val messageQueue = MessageQueue {
-        for (msg in it) {
+        /*for (msg in it) {
             if (msg.startsWith("EMU: ")) {
                 this.printListener?.invoke(msg.substring(5))
             }
-        }
+        }*/
     }
     private val readThread  = thread(start) {
         while (!Thread.currentThread().isInterrupted) {
             while (connection.bytesAvailable() == 0) {
                 try {
-                    Thread.sleep(10)
+                    Thread.sleep(5)
                 } catch (_: InterruptedException) {
                     Thread.currentThread().interrupt()
                     break
@@ -38,6 +38,7 @@ open class Debugger(private val connection: Connection, start: Boolean = true, p
 
             val readBuffer = ByteArray(connection.bytesAvailable())
             connection.read(readBuffer)
+            //print(String(readBuffer))
             messageQueue.push(String(readBuffer), true)
 
             while (true) {
@@ -48,16 +49,17 @@ open class Debugger(private val connection: Connection, start: Boolean = true, p
                 if (checkpointMessage == null)
                     break;
 
+                break // ignore checkpoints
                 val payloadStr = checkpointMessage.second.groups[1]!!.value
 
                 try {
                     val checkpoint = ObjectMapper().registerKotlinModule().readValue(payloadStr, Checkpoint::class.java)
                     //println(checkpoint)
 
                     if (checkpoint.instructions_executed == 0 && checkpoints.size > 0) {
-                        if (checkpoint.snapshot.pc != checkpoints.last()!!.snapshot.pc) {
+                        /*if (checkpoint.snapshot.pc != checkpoints.last()!!.snapshot.pc) {
                             throw RuntimeException("Received a checkpoint with a different pc but with 0 executed instructions since the last checkpoint!")
-                        }
+                        }*/
                         System.err.println("WARNING: Received a checkpoint that we already have!")
                         continue
                     }
@@ -213,7 +215,7 @@ open class Debugger(private val connection: Connection, start: Boolean = true, p
     }
     fun stepUntil(cond: (WOODDumpResponse) -> Boolean) {
         stepInto()
-        while (!cond(checkpoints.last()!!.snapshot)) {
+        while (!cond(snapshotFull().second)) {
             stepInto()
         }
     }
@@ -241,6 +243,7 @@ open class Debugger(private val connection: Connection, start: Boolean = true, p
     }
 
     fun printCheckpoints(binaryInfo: WasmInfo? = null) {
+        return
         println("Checkpoints:")
         for (checkpoint in checkpoints) {
             if (checkpoint == null) {

src/main/kotlin/be/ugent/topl/mio/debugger/MultiverseDebugger.kt

@@ -299,7 +299,8 @@ class MultiverseDebugger(
         if (graph.currentNode.children.isEmpty() && change > 0 && checkpoint?.fidx_called != null) {
             val newNode = if (isAfterChoicePoint(checkpoint.snapshot.pc!!)) {
                 PrimitiveNode(wasmBinary.metadata.primitive_fidx_mapping[checkpoint.fidx_called], checkpoint.args!![0]).apply {
-                    values.add(checkpoint.snapshot.stack!!.last().value.toInt())
+                    values.add(checkpoint.returns!!.first())
+                    //values.add(checkpoint.snapshot.stack!!.last().value.toInt())
                 }
             } else {
                 DeterministicPrimitiveNode(wasmBinary.metadata.primitive_fidx_mapping[checkpoint.fidx_called], checkpoint.args!!)
@@ -315,7 +316,8 @@ class MultiverseDebugger(
         // Don't add new nodes if we are walking on an existing graph section.
         if (graph.currentNode.children.isNotEmpty()) {
             if (checkpoint != null && isAfterChoicePoint(checkpoint.snapshot.pc!!)) {
-                val stackValue = checkpoint.snapshot.stack!!.last()
+                //val stackValue = checkpoint.snapshot.stack!!.last()
+                val stackValue = WasmStackValue(0, "", checkpoint.returns!!.first().toLong())
                 val intValue = stackValue.value.toInt()
                 if (graph.currentNode is PrimitiveNode) {
                     if (!graph.currentNode.values.contains(intValue)) {
@@ -362,7 +364,13 @@ class MultiverseDebugger(
         return pc in wasmBinary.metadata.after_choicepoints
     }
 
-    fun predictFuture(maxInstructions: Int = 50, maxSymbolicVariables: Int = -1, maxIterations: Int = -1, stopPc: Int = -1): Boolean {
+    enum class AnalysisOutcome {
+        Failed,
+        NoPaths,
+        Success
+    }
+
+    fun predictFuture(maxInstructions: Int = 50, maxSymbolicVariables: Int = -1, maxIterations: Int = -1, stopPc: Int = -1): AnalysisOutcome {
         val result = analyse(
             symbolicWdcliPath,
             wasmBinary.file.absolutePath,
@@ -372,16 +380,19 @@ class MultiverseDebugger(
             maxIterations,
             stopPc
         )
+        if (result == null) {
+            return AnalysisOutcome.Failed
+        }
         if (result.paths.isEmpty()) {
-            return false
+            return AnalysisOutcome.NoPaths
         }
 
         val concolicGraphRoot = processPaths(result.paths)
         // Remove current future and add newly predicted future, otherwise you will get a split timeline between the
         // previously predicted future and the newly predicted future.
         graph.replaceCurrentNode(concolicGraphRoot)
         graphUpdated()
-        return true
+        return AnalysisOutcome.Success
     }
 
     // TODO: Remove/move/improve

src/main/kotlin/be/ugent/topl/mio/ui/GraphPanel.kt

@@ -62,7 +62,7 @@ class GraphPanel(private val graph: MultiverseGraph) : JPanel(),
 
         drawPaths(g, width - 100, graph.rootNode)
         //drawGraphNew(g)
-        println("Height ${leafCounter.getLeafCount(graph.rootNode)}")
+        //println("Height ${leafCounter.getLeafCount(graph.rootNode)}")
     }
 
     val leafCounter = LeafCounter(graph)
@@ -130,6 +130,12 @@ class GraphPanel(private val graph: MultiverseGraph) : JPanel(),
                 x += node.edgeLength
             }
 
+            /*println(associatedScrollPane?.horizontalScrollBar!!.value)
+            if (x < associatedScrollPane?.horizontalScrollBar!!.value) {
+                println("Cull")
+                return Pair(Point(0, 0), 0)
+            }*/
+
             val result = drawGraph(g, currentNode, x + currentNode.edgeLength, y)
             renderedWidth = Integer.max(renderedWidth, x + node.edgeLength + 500)
             var newPoint = result.first
@@ -341,6 +347,7 @@ class GraphPanel(private val graph: MultiverseGraph) : JPanel(),
         val delta = Point(e.x - startPos.x, e.y - startPos.y)
         associatedScrollPane?.horizontalScrollBar?.value -= delta.x
         associatedScrollPane?.verticalScrollBar?.value -= delta.y
+        //repaint()
     }
 
     override fun mouseMoved(e: MouseEvent) {

src/main/kotlin/be/ugent/topl/mio/ui/InteractiveDebugger.kt

@@ -41,7 +41,7 @@ class InteractiveDebugger(
     private val wasmFile: String = "/home/maarten/Documents/School/Thesis/thesis-git/wardbg/simple-sym-test.wasm",
     private val config: DebuggerConfig
 ) : JFrame("WARDuino Debugger") {
-    private val binaryInfo = getBinaryInfo(symbolicWdcliPath, File(wasmFile).absolutePath)
+    private val binaryInfo = getBinaryInfo(config.wdcliPath, File(wasmFile).absolutePath)
     private val debugger = MultiverseDebugger(
         connection,
         WasmBinary(File(wasmFile), binaryInfo),
@@ -387,8 +387,8 @@ class InteractiveDebugger(
         }
 
         //val snapshot = debugger.currentSnapshot!!
-        val snapshot = debugger.checkpoints.last()!!.snapshot
-        //val snapshot = debugger.snapshotFull().second
+        //val snapshot = debugger.checkpoints.last()!!.snapshot
+        val snapshot = debugger.snapshotFull().second
         watchWindow.update(snapshot)
 
         if (sourceMapping == null)
@@ -474,6 +474,7 @@ class MultiversePanel(private val multiverseDebugger: MultiverseDebugger, config
     private val mockPanel = OverridesPanel()
     private val concolicButton = JButton("Suggest interesting paths")
     private var maxInstructions = 50
+    private var maxSymbolicVars = 50
     private val concolicOptionsButton = JButton().apply {
         val gearIcon = FlatSVGIcon(MultiverseDebugger::javaClass.javaClass.getResource("/settings-gear.svg"))
         gearIcon.colorFilter = FlatSVGIcon.ColorFilter()
@@ -483,6 +484,9 @@ class MultiversePanel(private val multiverseDebugger: MultiverseDebugger, config
             JOptionPane.showInputDialog("Instruction limit", maxInstructions)?.let {
                 maxInstructions = it.toInt()
             }
+            JOptionPane.showInputDialog("Max symbolic variables", maxInstructions)?.let {
+                maxSymbolicVars = it.toInt()
+            }
         }
     }
     private val customButton = JButton("Mock").apply {
@@ -512,10 +516,15 @@ class MultiversePanel(private val multiverseDebugger: MultiverseDebugger, config
         concolicButton.addActionListener {
             val w = BlockingWindow(null, "Analysing program")
             w.location = Point(this.location.x + this.width/2 - w.width/2, this.location.y + this.height/2 - w.height/2)
-            w.run({ multiverseDebugger.predictFuture(maxInstructions) }) { graphChanged ->
-                if (!graphChanged) {
+            w.run({
+                multiverseDebugger.predictFuture(maxInstructions, maxSymbolicVars)
+            }) { graphChanged ->
+                if (graphChanged == MultiverseDebugger.AnalysisOutcome.NoPaths) {
                     JOptionPane.showMessageDialog(this, "No future branching paths could be found")
                 }
+                else if (graphChanged == MultiverseDebugger.AnalysisOutcome.Failed) {
+                    JOptionPane.showMessageDialog(this, "Program analysis failed!")
+                }
             }
         }
 
@@ -723,6 +732,7 @@ class MultiversePanel(private val multiverseDebugger: MultiverseDebugger, config
     }
 
     fun graphChanged() {
+        //graphPanel.leafCounter.calculateLeafCounts()
         graphPanel.repaint()
         graphPanel.revalidate()
         //customButton.isEnabled = multiverseDebugger.graph.currentNode is PrimitiveNode
@@ -765,6 +775,9 @@ class WatchWindow : JTable() {
     fun update(snapshot: WOODDumpResponse) {
         tableModel.rowCount = 0
         tableModel.addRow(arrayOf("pc", "i32", String.format("0x%x", snapshot.pc)))
+        if (snapshot.globals == null) {
+            return
+        }
         for (global in snapshot.globals!!) {
             tableModel.addRow(arrayOf("global ${global.idx}", global.type, global.value))
         }

src/main/kotlin/be/ugent/topl/mio/ui/LeafCounter.kt

@@ -11,21 +11,24 @@ class LeafCounter(private val graph: MultiverseGraph) {
         println("Calculating leaf counts")
         val time = System.currentTimeMillis()
         cachedHeights.clear()
+        val completedNodes = mutableSetOf<MultiverseNode>()
         val stack = mutableListOf(graph.rootNode)
         while (stack.isNotEmpty()) {
             val currentNode = stack.last()
             if (currentNode.children.isEmpty()) {
-                cachedHeights[currentNode] = 1
+                //cachedHeights[currentNode] = 1
+                completedNodes.add(currentNode)
             }
             // We already calculated the height of our children -> calculate our height!
-            else if (cachedHeights.contains(currentNode.children.first())) {
+            else if (completedNodes.contains(currentNode.children.first())) {
                 var heightSum = 0
                 for (child in currentNode.children) {
-                    heightSum += cachedHeights[child]!!
+                    heightSum += cachedHeights.getOrDefault(child, 1)
                 }
                 cachedHeights[currentNode] = heightSum
+                completedNodes.add(currentNode)
             }
-            if (cachedHeights.containsKey(currentNode)) {
+            if (completedNodes.contains(currentNode)) {
                 stack.removeLast()
             }
             stack.addAll(currentNode.children)
@@ -34,6 +37,6 @@ class LeafCounter(private val graph: MultiverseGraph) {
     }
 
     fun getLeafCount(node: MultiverseNode): Int {
-        return cachedHeights[node]!!
+        return cachedHeights.getOrDefault(node, 1)
     }
 }

src/main/kotlin/be/ugent/topl/mio/woodstate/WOODState.kt

@@ -156,6 +156,7 @@ data class Checkpoint(
     val instructions_executed: Int,
     val fidx_called: Int?,
     val args: List<Int>?,
+    val returns: List<Int>?,
     val snapshot: WOODDumpResponse
 )
 

src/test/kotlin/DebuggerTestBase.kt

@@ -16,7 +16,9 @@ abstract class DebuggerTestBase {
         val connection = if (emulator) ProcessConnection(wdcliPath, getFile(file).path, "--no-socket") else SerialConnection(config.port ?: throw RuntimeException("Port was not configured!"))
         val debugger = Debugger(connection)
         if (!emulator) {
-            debugger.updateModule(getFile(file).absolutePath)
+            debugger.pause()
+            debugger.reset()
+            //debugger.updateModule(getFile(file).absolutePath)
         } else {
             debugger.pause()
         }