Inferring State (Parts VIII & IX) / Days 33 & 34

Day 33 - Thursday July 11
Today was spent implementing the ideas of the last post: the idea that within a certain state, a choice generator may be invoked several times, and that this results in transitions from a state to itself. This was not entirely correct, from the looks of it: the transitions can go back to a similar state, but the choice generator won't make a new choice for that particular choice call--it will execute the program in this state until a new choice is necessary (which may be the same choice). For example, consider the following code:

if(makeChoice()){
   variable = 1;
} else {
   variable = 2;
}

In this case, if the choice returns true so that variable is set to 1, then that might cause JPF to create a new state, where variable takes on a value of one (and of course, the search object determines when a new state is created or when one is re-used). If the choice returns false, then the variable is set to 2, but in this example, this would likely not create a new state--JPF (or, rather, the search object) will reuse the state that it was in before reaching the branching code.

So basically, looking at probabilities does not define the abstractions over the state variables (there are none) or the set of possible values, but it does provide the probabilities for these transitions, so it's still useful to get this information from the Probabilistic search object.

Day 34 - Friday July 12
Despite the ideas changing a bit in the last few days rather quickly, I always kept in mind that the end goal was to make sure that in a given JPF state, we also have the explicit state of the variables, as well as the transitions between states, and the probabilities that each transition was taken. The transitions were easy; the states a bit harder. The transitions, as alluded to in the last couple of posts can be exactly determined by the Probabilistic Search object and the listener's we're already using. The states were harder: defining what they were was hard: there's no way in JPF (at least not one that I know of) to ask it what the value of a variable in the SUT is in a given state (that would be a great extension!). So instead you need to track them by observing the instructions that JPF executes, looking out for the store instructions that modify a variable's value, and record those. And you need to make sure you're aware of when the state changes, and what it changes to. A small hiccup comes when it's realized that although instructions are executed in a transition, a transition doesn't know what state it's leading to until it completes and the search object tells the VM. So you need to store the result of the execution outside of the transition or the VM and then clean it up by putting those results in whatever state you now know you're in. I'm a bit concerned this will lead to greater memory bottlenecks, but for now it works.

The upside of monitoring instructions like this is that every explicit state of the SUT can be monitored: anytime a variable changes, we're aware. So that means when a state changes it's values, we can choose to either keep this information as a set, for example in state X, we know variable a = {1, 0} for exactly one of these values, or we can generate new (non-JPF-SystemState) "sub-states" that make it explicit: in state X, variable a = 1, but in state X.1, variable a = 0. The "set" method was in use early in the week but I wasn't satisfied, so now jpf-prism works with the latter system. The benefits of this is now that I track that a transition from a state to itself changes a variable in that state (and how it changes), but also if a transition into or out of state X is from anywhere in X, or in exactly X.Y (some substate). So now I exactly know the execution trace of the SUT. The disadvantage is that I'm storing much more information: in addition to tracking what state preceded another, I also now store a new substate for every value a variable can take. This will undoubtedly increase memory overhead.