Remote Concolic Multiverse Debugging

In Figure 1 we show our prototype being used to debug a temperature dashboard application, shown in the left pane of the debugger. See Appendix C in the extended version [41] for a full screenshot of our debugger.

This program reads a temperature sensor to control 3 LEDs, leading to three logical paths in the execution. If the temperature is higher than 70 degrees, a red LED will turn on. If the temperature is between 50 and 70 degrees an orange warning LED turns on. Below 50 the LED is set to green. In this relatively simple example, the temperature is measured using an analog sensor that varies its resistance based on temperature. The resulting analog input signal is then converted into degrees Celsius.

This simple program contains a subtle bug that is hard to discover with traditional debuggers. Instead of reading the temperature sensor once and then using this value, the program reads the temperature multiple times (line 37 and 40). This can lead to situations where the lights are incorrectly switched on or off given the last sensor value. In addition to these glitches, reading out the sensor multiple times per iteration slows down the program and consumes more battery power. Using our debugger, these issues can be identified.

Figure 1 illustrates the different stages of a remote concolic multiverse debugging session over our example program. After loading the debugger and the program, the first line of the source code is highlighted as shown on the left. The multiverse tree at this point is only a single root node, the entry point of the program (pane 1, Figure 1). Stepping forward extends the current path as shown in pane 2 (Figure 1). Every edge in this path is a single WebAssembly instruction, and edges for primitive calls are labeled with the name and provided arguments.

Imagine the programmer places a breakpoint just before reading the temperature sensor (line 21) and lets the program run until this point. After the breakpoint is hit, when using a traditional remote debugger, the programmer would proceed through the program code with an arbitrary temperature value (i.e. the current temperature). Alternatively the developer might manually heat or cool down³³3Such as in this GitHub issue where a bug is reproduced using ice packs https://github.com/tobyweston/temperature-machine/issues/13. the sensor to guide the program execution.

In contrast, our concolic multiverse debugger helps guide a programmer’s exploration using its concolic execution. The developer can simply ask the debugger for interesting future execution paths by pressing the “Suggest paths” button (source view, Figure 1). The debugger then uses concolic execution to identify all future execution paths within a user configurable bound (number of instructions and/or number of nondeterministic operations). The possible paths found by the analysis are added to the multiverse tree view (pane 3, Figure 1), showing each of the possible executions as a new branch. Compared with remote debugging, this feature frees developers from having to manually find the necessary sensor values for specific control flow paths, either through trial and error or by manually analysing the program which quickly becomes too complicated as the program’s complexity increases.

Each choice point in our visualisation corresponds with a call to a nondeterministic input primitive, we label the edges starting from a choice point with the corresponding input values. This gives developers a clear overview of how the input values influence the program’s behavior. For instance, in pane 3 (Figure 1), the concolic analysis found two possible branches after executing the chip_analog_read(12) primitive, with input values 224 and 1913.

Subsequently, the developer can manually explore the effects of the nondeterministic input, by choosing one of the branches added by the concolic analysis. Developers do not have to change the temperature manually to change the input value to correspond to their desired branch. Instead, the debugger provides a mocking functionality through the “mock” button, which launches a new pop-up window. In the pop-up, developers can specify the return value for a specific input primitive and its specific arguments. In our example, the developer changes the return value for reading pin 12, to 224, steps forward to the next analog read instruction, mocks it to read value 77, reaching the state shown in pane 4 (Figure 1). During execution the debugger uses the mocked values instead of the actual sensor value.

While mocking is an essential feature for exploration, it takes quite some manual effort to provide all the right sensor values when exploring the multiverse graph. To make it easier to navigate the graph, the developer can simply click on a node and press the “Slide” button, to slide to that particular execution state, thereby entering the desired branch. When sliding to an entirely new branch with different parents, the debugger restarts the program and mocks the right values at each choice point automatically. Pane 5 (Figure 1) shows how the debugger highlights the path that will be taken from the root node to the selected node (highlighted with a white circle), before the Slide button is pressed. Note, this operation does not modify the tree, even when restarting the program. All previous branches remain visible.

As the outlined debug session shows, the concolic multiverse debugger improves on the common remote debugging experience by making it easier to explore multiple execution paths and gives the developer a clear visual overview of choice points in the program. Exploring different execution paths is made easier by the sliding feature, allowing developers to go from one branch to another, and by the mocking feature, which allows the debugger to easily mock any input action. However, the advantages go beyond this.

The concolic analysis coupled with the tree visualisation can already point out the cause of a bug at a glance. For instance, when the branches provided by the analysis differ from what is expected, this usually points to a mistake in the program’s logic. This is certainly the case in our example, where one expects a single choice point with three options for the current temperature. However, the trace shows two choice points with two branches each. This is a consequence of reading the analog sensor value twice in the if statement (lines 37 and 40) instead of reading it once, and storing it in a variable. As a result the temperature value can differ between the two if statements, which can potentially cause strange behavior.

Although the debugger can be viewed as a single monolithic unit, it is more practical to conceptualize it as comprising three distinct components: the WebAssembly virtual machine (VM), which defines the foundational language semantics; the server, which operates as the remote debugger on the microcontroller; and the client running on a desktop computer, which interacts with the server to facilitate debugging. We begin by outlining the WebAssembly configuration, followed by a detailed discussion of the server configuration. Next, we examine the client configuration, and give an overview of the complete remote concolic debugger setup. In later sections, we delve into the semantics of both the server and the client components.

Figure 7 shows the semantics describing the communication between the server and the client in the debugger. These rules also specify when the server can take a single step. Each rule is defined as a transition (denoted by $\to$) over the pair of client and server configurations $C|S$.

Whenever the server puts a message for the client in its outbox the Server-To-Client rule applies which causes the client to process this message using the client transition relation $\rightsquigarrow$. The server-to-client communication has priority over all rules in the system, therefore on the client outgoing messages are always sent after processing all incoming messages.

When the server has no outgoing messages and the client has one or more messages in its outbox compatible ($\approx$) with the current state of the server, the message is processed by the server (denoted by ${\hookrightarrow }_{d,i}$) as shown in the Client-To-Server rule. This compatibility relation essentially means the client can only send messages when the server is in the Paused state. The only exception to this rule is the $\mathrm{𝑝𝑎𝑢𝑠𝑒}$ message, which can only be sent to the server when it is in the Running state⁴⁴4Note that in our semantics the user can easily bring the debugger in a stuck state by sending an incompatible message, we consider such scenarios to be part of a bug in the frontend of the debugger.. This lets the client pause the server at any time.

When all message queues of the server and client are empty, the Server-Step rule applies and the server can take a single step under the ${\hookrightarrow }_{d,i}$ relation. In the following section we will focus on how this reduction relation is defined.

Note that in our semantics, we have chosen to make all operations synchronous, the server is blocked while the client processes messages. This decision is primarily motivated by clarity, as asynchronous semantics would be more difficult to understand and reason about.

Having discussed the global communication rules, we can now focus on local client and server reduction rules. We start our overview with the reduction relation of the server ${\hookrightarrow }_{d,i}$.

The server has two states: Running or Paused, the rules for both cases are similar. In the Running state, the server will execute the program while keeping track of a counter tracking the number of executed instructions since the last synchronisation with the client. Whenever an input primitive is executed, a so-called $\mathrm{𝑝𝑟𝑖𝑚}(c_{instr},v)$ message is sent to the client. This message contains the counter and the return value of the nondeterministic input primitive. After sending this message the server will reset the counter to $0$. The full rules for this behaviour can be found in Appendix A.1 of the extended version [41].

The Paused rules are similar but instead always notify the client of every executed instruction so that the client knows exactly where in the program the server is. The rules shown in Figure 8 define the semantics in the Paused state. The server can go into the Paused state by hitting a breakpoint or because the developer sent a $pause$ message to the microcontroller. When switching to the Paused mode the client will be notified how many instructions were executed since the last synchronisation with the client.

Once the debugger is paused, the client can instruct the server to step through the execution by sending $step$ or $mock$ messages. When stepping, the server differentiates between normal instructions, calls to output primitives, and calls to input primitives as reflected in the Dbg-Step, Dbg-Step-Prim-Out and Dbg-Step-Prim-In rules. When taking a step over a regular instruction or a call to an output primitive, the server notifies the client that one deterministic step was taken using $\mathrm{𝑒𝑥𝑒𝑐𝑢𝑡𝑒𝑑}(1)$. When stepping over a call to a nondeterministic input primitive, the client is notified of the value returned using $\mathrm{𝑝𝑟𝑖𝑚}(1,v)$. For the primitives $\lfloor p(v_a^{\ast })\rfloor$ is used to indicate the operation is performed outside of the system. In this case the value $v$ is produced outside of the system and can be nondeterministic.

The Dbg-Mock rule allows the developer to pick which execution should be explored by controlling the execution of nondeterministic primitives. Instead of executing the primitive, the debugger replaces the arguments $v_a$ to the call with the supplied value $v$ and removes the $\text{call}e$ from the execution stack. An important requirement here is that $v$ must be a value that the primitive can produce in the underlying language semantics. With this rule alone, a developer has to manually choose the value to be explored. However, it is often complicated to figure out which values are needed to explore specific execution paths such as in the basic example in the previous section. In Section 5, we explain how we automatically generate the necessary values removing the need to enumerate countless options.

The Dbg-Play, Dbg-Inspect and Dbg-Reset rules of the debugger, detailed in Appendix A.4 of the extended version [41], respectively transition the debugger to the running state, request a snapshot and restart execution from the start of the program.

The client in this system does most of the heavy lifting since it does not run on the microcontroller. Instead the client has a message queue that processes messages received from the microcontroller (server). Using these messages the debugger constructs the navigable multiverse tree. The tree has the structure described in Figure 5 as previously explained in Section 4.1.3. Every node in the tree can have zero or more children. The edges of the tree are marked with debugging operations used to navigate the tree. For deterministic nodes the $step$ operation is used, for nondeterministic nodes $mock$ will be used. This tree and the current node is stored alongside the incoming and outgoing messages in the debugger state.

In order to integrate concolic execution into a live debugging session, we cannot follow the usual strategies of current concolic execution engines. Firstly, our analysis begins not from the start of the program or an existing concolic state (as in online concolic execution) but instead starts from the concrete execution state of a program running on a microcontroller.

Secondly, we are working with embedded systems where concolic execution cannot run locally. As a result, the analysis must be performed remotely. To initiate the analysis from the current execution state of the microcontroller, the state needs to be transferred to the client performing the concolic execution. The custom virtual machine enables this state transfer by sending an $inspect$ message to the debugging server, as previously described. When receiving this message the server serializes its state and transfers it to the client. However, this is purely a concrete state without any symbolic components. To start the analysis from this concrete state, the debugger first needs to transform it into a so-called concolic state in which every concrete element has a symbolic counterpart. Using the newly created concolic state, the analysis can start from the current execution state in the debugger.

For our debugger, we developed our own concolic execution engine for WebAssembly based on the semantics described in [27]. To ensure that our theoretical model aligns with our practical implementation, which leverages an existing concrete execution engine during concolic execution, we adjusted the formalization. By doing so the concolic rules re-use the concrete ${\hookrightarrow }_i$ rules just like in the implementation. This approach results in both server and client VMs using the same codebase for concrete execution. However, on the server side, we compile the code in a way that excludes the concolic execution functionality.

To start we describe the components of this execution engine shown in Figure 13. The core configuration for the concolic semantics is very similar to the core of the previously described debugger semantics. It consists of a collection of locals, globals, a stack and memory. These are part of the concrete state $K$. Unlike the concrete execution, each of these components now has a symbolic counterpart that we denote using $\widehat{y}$ for a component $y$. The symbolic locals ($\widehat{\rho }$), globals ($\widehat{\mathrm{\delta }}$), stack ($\widehat{st}$) and memory ($\widehat{\mu }$) are all defined similarly to their concrete counterparts but now map an index to a symbolic expression instead of a concrete value. We previously defined concrete values as $v$, we now define symbolic expressions as $\widehat{s}$. A symbolic expression can be a concrete value, a symbolic variable $\widehat{x}$ or a unary, binary or tertiary operation on symbolic expressions. These are symbolic expressions and not values because it is not always possible to calculate the result of an expression when working symbolically.

Alongside the locals, globals, stack and memory the concolic execution engine also has some properties specifically needed for concolic execution. These are the symbolic environment ($\mathrm{\epsilon }$) and the path condition ($\pi$) stored in a concolic program state defined by $K_{cs}$.

Outside of the concolic state our concolic execution engine also keeps track of a multiverse tree which will later be added to the tree in the debugger. This tree denoted with $\widehat{T}$ is very similar to the tree described in Section 4 but now has an additional component which we call the “$pathModels$”. This is a list of path conditions and their associated symbolic environment, denoted by ${(\pi ,\mathrm{\epsilon })}^{\ast }$. This additional information is used by the analysis to continually extend the current multiverse tree with new paths while merging paths that share a common prefix.

Using the previously defined components, we now define the concolic semantics in Figure 14 (defined by ${\Rightarrow }_{cs}$). For brevity we do not list all rules here but give a representative subset.

The concolic semantics define a transition relation between two concolic states $K_{cs}$. All rules follow the following structure: $⟨K,\widehat{\rho },\widehat{\mathrm{\delta }},\widehat{st},\widehat{\mu },\mathrm{\epsilon },\pi ⟩{\Rightarrow }_{cs}⟨K^{\prime },{\widehat{\rho }}^{\prime },{\widehat{\mathrm{\delta }}}^{\prime },{\widehat{st}}^{\prime },{\widehat{\mu }}^{\prime },{\mathrm{\epsilon }}^{\prime },{\pi }^{\prime }⟩$.

We first describe the rule used for simple binary arithmetic instructions, these instructions e.g. $i32.add$ simply take two elements from the stack, apply an operation to them, for example addition and place the result on the stack. In our concolic execution engine this is done by using the underlying concrete semantics to manipulate the concrete stack and applying the symbolic binary operation on two elements of the symbolic stack. In this case symbolic addition. This way we do not need to reimplement the concrete part of our interpreter for every instruction but can instead reuse the existing implementation.

Symbolic-Prim-Fresh is responsible for creating new symbolic variables. When an input primitive is called and the unique symbolic variable ${\widehat{x}}_d$ associated with this call is not in the symbolic environment $\mathrm{\epsilon }$, a new symbolic variable with that name is created and is given an arbitrary concrete value $v$. Note that we assume here that the $id$ function returns a different identifier for different uses of the same call. This symbolic variable is placed in $\mathrm{\epsilon }$.

Symbolic-Prim applies when the symbolic variable ${\widehat{x}}_d$ already exists in the symbolic environment. In this scenario, the concrete value is read from $\mathrm{\epsilon }$. This concrete value is pushed on the concrete stack. The symbolic variable itself is pushed on the symbolic stack.

The If-True rule is essential for building up many of the path conditions. Given that the current instruction is $\text{if}tf{e}_1^{\ast }\text{else}{e}_2^{\ast }\text{ end}$ and the condition on the stack is not $0$, the next instructions will be $e_1^{\ast }$. The concrete part of the state is updated in the same way as normal using the concrete semantics ${\hookrightarrow }_i$. The symbolic part of the state is updated by removing the expression representing the condition $\widehat{s}$ from the stack and updating the path condition to show that the condition $\widehat{s}$ is true.

The If-False rule works analogously except that the condition is false now and the branch will not be taken. Instead the instructions in the else case will be executed. The symbolic stack and path condition are updated accordingly to reflect that the condition is not true in this case.

A traditional concolic execution engine generates a series of models, each representing a unique execution path within the program. However, a multiverse debugger enables interactive exploration of these executions through a graph-based interface. For concolic multiverse debugging, the analysis must not produce a sequence of isolated models but instead construct a tree in which overlapping parts of different executions are merged.

This is what happens in the Concolic-Receive rule for the client shown in Figure 12. It will, upon receiving a snapshot by first sending an $inspect$ message, take a concrete state and convert it into a concolic state using $s(K)$ (details in Appendix A.7 of the extended version [41]). Then it uses the $\mathrm{𝑐𝑜𝑛𝑐𝑜𝑙𝑖𝑐}$ function described below to generate a tree of future execution paths. Finally, the resulting tree is attached to the current multiverse tree by replacing the current node with the root of the newly generated tree.

The tree of future execution paths is built iteratively in the $\mathrm{𝑐𝑜𝑛𝑐𝑜𝑙𝑖𝑐}$ function described in Algorithm 1. To achieve this, the main loop of the analysis iteratively expands the multiverse tree after each concolic iteration using the $extendTree$ function.

To expand the existing tree the different symbolic values stored in the model $\mathrm{\epsilon }$ are used to walk through the existing multiverse tree. When walking through the tree, the algorithm adds or follows a path for every executed instruction. The pseudocode does this using the ${\hookrightarrow }_i$ relation⁶⁶6We use ${\hookrightarrow }_i$ here for simplicity, in the actual implementation the number of deterministic instructions between each choice point is simply stored in a counter, so there is no need to re-execute the program.. If the instruction is deterministic, a node connected using a $step$ edge is added or followed. These edges never branch and simply indicate that there is a deterministic instruction that can be stepped over. If the edge does not exist yet, it is created, if it does exist, the edge is followed. If an instruction is nondeterministic, the algorithm will check if the path for this value and path condition is unique or not. If it is not unique, the algorithm will keep following the existing path. If it is unique, a new branch in the tree will be created.

To check if a path is unique with respect to a particular value, it is important to realise that a new path found by a concolic execution engine will always differ from an existing path at some point. As such the tree building algorithm looks for the point where the new model’s path condition branches off from one of the models in the current path (denoted by ${\widehat{T}}_{curr}.pathModels$). This is the point at which the common prefix of two executions end.

To achieve this the algorithm will do a pairwise comparison between the models for each symbolic variable $x_d$ until a point where $x_d$ diverges. The algorithm does this by placing the first $d$ variables of the existing model in the new path condition and vice-versa. At some point one (or both) of these path conditions will no longer hold. At this point the two models diverge. From this point on the algorithm will attach new nodes to the tree, creating a new path, instead of following an existing path.

The formalisation of our technique follows previous works on multiverse debugging, specifically Voyager [44] and MIO [24], where the debugger semantics are defined in terms of the underlying language semantics. This allows debugger correctness with respect to the underlying language to be defined as the combination of soundness and completeness, as proposed by Lauwaerts et al. [24]. Soundness means that the debugger should only be able to explore states possible in the underlying language semantics. Completeness states that every state possible in the underlying language semantics should be explorable in the debugger.

Soundness follows because the debugger’s $step$ operation is defined in terms of the underlying language semantics, and the $mock$ operation can only mock values within the domain of the primitives. Completeness also holds because each underlying language step (${\hookrightarrow }_i$) has a corresponding debugger step ($\to$). For deterministic instructions, the $step$ message can be used. For nondeterministic primitives, the $mock$ message can be used to make the execution in the debugger follow the exact same path as the underlying language semantics. Additionally, even though concolic execution suggests only a subset of possible sensor inputs to reduce the state-space, the debugger remains complete because the user can still manually $mock$ other possible inputs.

A full proof, together with the formal definitions of soundness and completeness, is included in Appendix D of the extended version [41]. This proof differs from MIO due to our trace-based approach and the lack of reversibility. Due to this lack of reversibility we instead rely on restarting the execution entirely to slide to a different universe.

The data presented in Table 1 shows an overview of the state-space reduction for all programs that we tested. We under estimate the state space of a program by taking the path in the program with the most choice points and multiplying the number of options along this path (States). This number estimates the number of states that would be presented to the user in a traditional multiverse debugger. We show the amount of unique paths (Paths) found by our analysis and the maximum number of options (Max opts) presented to the user at any given point in time. For programs that use state from previous iterations we executed the loop twice as this is the minimal iteration count needed to see an effect. For programs that do not use state from previous iterations we limited the analysis to just one loop iteration (Loop iterations). For each of these configurations we also give the time (Time (s)) it took to analyse the program. As the data shows, our technique significantly reduces the state-space for each of the programs we tested⁸⁸8The arduino-while program has two variants, we discuss the reason behind this in more detail later.. In the following sections, we give an overview of these programs and show how remote concolic multiverse debugging helps to debug them.

The arduino-knock, arduino-touch-sensor-lamp, arduino-switch, arduino-keyboard and arduino-love-o-meter programs only have 2 to 5 paths. While the state-space for these programs is still relatively big, a quick inspection suffices to find good nondeterministic values to choose from. The advantage of using our debugger over existing multiverse debuggers such as MIO [24] is that the user can much more easily explore interesting paths. Exploring a new execution path traditionally requires manually adding each edge through individual $\mathrm{𝑚𝑜𝑐𝑘}$ and $\mathrm{𝑠𝑡𝑒𝑝}$ operations. Additionally the user also has to decide which values they use when mocking from a large amount of options as visible in the left of Figure 18. Using our approach, all future execution paths can be created automatically with a single button press. This results in a tree where each execution path has corresponding inputs to explore it as shown on the right in Figure 18. In the arduino-knock program, this reduces the state-space from ${4096}^2$ paths to just $4$. The program uses a simple if and $2$ values are needed to explore both branches. In two loop iterations this results in $4$ paths. To explore an execution path, one simply clicks on a node in the path and slides to it, performing all the needed mocking and stepping operations along the way. This also allows users to easily explore sequences of values instead of just one singular value at a time as with mocking. For example, using the slide operation on the created paths in the arduino-keyboard program which implements a basic piano, sequences of notes can easily be explored. Furthermore, our analysis helps to point out strange behaviors in programs. For example, the arduino-switch program reads an analog value and maps it from 0 to 3 (inclusive) for use in a switch. Strangely this program has 5 execution paths instead of 4. This is due to the arduino map function which does not constrain the output when the input value is higher than the maximum. Our analysis points this out to the developer. Finally, our analysis also helps in cases where the value needed to mock is unclear, such as in the arduino-love-o-meter where floating points calculations convert an analog value into celsius before performing branching. In this case our analysis calculates the right input values needed to get into the right branch after the conversion. Calculating the needed values by hand would take a significant effort.

The second set of programs have a higher path complexity ranging between 11 to 16 paths. We found that for some of these programs the state-space reduction becomes significant, as it is no longer obvious which input values are needed for full coverage based on a quick inspection of the source code. The main reason is that these programs combine multiple sources of non-determism and keep track of state over multiple loop iterations. This combination makes it much harder to reason about the possible combinations that can occur during execution.

The arduino-crystal-ball has 11 paths because the program implements a magic 8 ball using a random integer from 0 to 8 (exclusive) with a switch case and a button that needs to be pressed and released. This program illustrates how programs using the random function can be more easily debugged because the behaviour of this nondeterministic function can be controlled using the debugger. The arduino-knock-lock program implements a vault door that can be opened by knocking a specific pattern. It has 13 paths in two iterations, this is because it allows users to either not press a button or knock in 3 different ways, this results in 4 paths in the first iteration and $4+3\cdot 3=13$ in the second iteration. This program opens the lock if the door is knocked on 3 times, as such a higher iteration count might be interesting in this program. This is configurable in the debugger. Using our analysis, the user can easily generate the needed values to trigger different kinds of knocks and explore the effect of knocking various different sequences without actually needing to manually knock each sequence. Finally, the arduino-zoetrope program implements a zoetrope which provides the illusion of moving images. It has 16 paths, this is because it has two buttons that can both be pressed or not pressed in each iteration resulting in 4 paths in the first iteration and 16 in the second. Given this program only branches on digital inputs, it is relatively easy to debug. However, this program also showcases an additional aspect of our debugger. To control the motor speed, the program directly uses an analog value read from a potentiometer. Since this is only a single execution path, only a single value is generated. However, using our manual mocking operation, other additional inputs can easily be explored allowing developers to reproduce bugs where a different speed is required. The same applies to many other programs where an input directly controls the output without branching.

We categorize three of the selected programs as high complexity, either due to the many paths generated or due to the larger code base making it more complex to understand quickly. These three programs are the arduino-while example, a gesture controlled robot and the breakout game.

The arduino-while program first calibrates a sensor at runtime when a button is pressed. Subsequently, it reads an analog value and runs it through a formula with hardcoded values. It then clamps the result between 0 and 255 using two if statements. Interestingly, this program generates an abnormally large number of paths. The amount of states for this program are so excessive that we had to limit the number of concolic iterations for the analysis to finish in a reasonable time. This abnormally large number of paths can be attributed to the calibration step used in this program which first reads an analog value which later serves as a threshold in the program. Because this sensor value is used to determine the branching conditions, the concolic analysis can keep finding new paths by simply choosing a different sensor value in the calibration, resulting in a nearly infinite number of paths.

Our work overcomes this issue by letting the user first run the program and calibrate the sensor value and then debug the rest of the application given the chosen calibration. This way, once the user chooses the path that will be taken depending on this unknown value, the value is already chosen and only few options remain. Our work enables this by employing a dynamic approach that starts the analysis from the current program state in the debugger instead of using a static analysis that does not take the current program state into account. To show the number of paths after choosing a calibration value, we also evaluated a version of this program without the calibration called arduino-while-no-calibrate which can be found in Appendix E.2 of the extended version [41]. This is equivalent to choosing a calibration value in the debugger and then running the analysis. As shown in Table 1, this drastically reduces the number of options, from a nearly infinite collection of options to just 3 paths once the calibration phase is over. These three paths are a result of the clamping operation, either the value is within the bounds, below the minimum or above the maximum value.

The gesture-robot program implements a gesture detector to remotely control a robot. The remote works using an accelerometer, analog values are read to get the acceleration on the x and y axis. Based on these values the remote can make the robot drive forwards, backwards, turn left, right or stay idle.

This program uses a chain of four conditional if else branches with an else at the end. Each if condition reads in a new x and y axis acceleration value, when both these values are within the required threshold the robot performs the associated action. Each if statement has 3 options, either both x and y are within bounds, only one is or none are. For two of these the program falls back to the next if statement which then again has 3 options, in the end this results in $1+2\cdot (1+2\cdot (1+2\cdot (1+2)))=31$ possible paths. Each of these paths is correctly discovered by our concolic analysis. The main complexity of the gesture-robot application stems from the way the program is written. The program reads in a new sensor value whenever a sensor value is needed instead of storing sensor values in local variables. As a result it is possible for sensor values to change in between reading values causing strange unpredictable behavior. Our debugger makes the excessive number of possibilities clear to the developer and allows them to take action. Additionally, besides helpful to point out these issues, the analysis allows the developer to easily test all the possible gestures without having to manually perform each action in the real world.

The breakout game listed in Appendix E.3 of the extended version [41] implements a simple breakout game where an analog joystick determines the position of the paddle. When analyzing this program for 259 loop iterations, the point where the ball will reach the bottom of the screen, the analysis determined that there are only three paths. One in which the paddle is on the left of the ball, one where it hits the paddle and one where it is on the right of the paddle. The analysis also found that in a large portion of the program, the position of the joystick does not matter, resulting in a single execution path. This is the case when the ball is not near the paddle and the paddle can thus not hit the ball. Using the provided paths, the developer can easily test certain game scenarios such as behavior at very high scores which might be very difficult to reach for a developer. Due to the complexity and size of this program we believe this program showcases that the analysis can be effective over a larger program with a large number of iterations. Additionally, while the snapshot based approach of MIO [24] works well for most programs, we noticed a large reduction in overhead when using our trace-based debugger for this particular program. In a test on the breakout program, it took around 1.9s to execute $50000$ instructions without tracing. When using our trace-based approach the execution time went up to 2s. However, MIO’s checkpointing policy (which in this case takes checkpoints every $\pm 2$ instructions) increased the execution time to around 5 minutes for this particular program. This shows that the overhead of our trace-based approach is significantly less than MIO for programs that perform very frequent IO operations. However, while the overhead of forward execution is significantly reduced, the time to step back has increased as it requires re-executing the program. A more in depth analysis is provided in Appendix F of the extended version [41].