Inferring State (Part V) / Day 30

Today was a productive day: some important lessons were learned. First, return values from methods that are not also stored in a variable are not considered by the JPF VM to be a StoreInstruction. This means that I was looking for variables to take the values that methods, like roll(), would return. I couldn't find them, and then I realized this was the case. I modified the BiasedDie example to assign the return value to a variable first, in order to check it better—but this may not be the case in arbitrary code. I’m mentioning it here (as well as making it an issue) so that I look into it later. Second, and much more concerning, I discovered that variables can take on different values in the same JPF state! So I was initially looking for a specific value for each variable in each state, but that’s not the case. This is a bit disconcerting, as it means I’m not doing enough to determine the “state”. I need to do more than look for specific values: I need to look into how JPF characterizes or abstracts a state, and find a way to transfer that to PRISM. That seems much harder, and I left it to tomorrow. Today, code-wise, I did get VarRecorder to work, and now I have a small hash table of states, variables, and their possible values. With this, and a bit of work, I could probably transfer this information to PRISM. I’m concerned that the hash table will not scale well, but I want to get past this problem, so for now I’m going to run with this and find some time to do scalability testing. I figure that if it doesn't scale well, I’ll see if I can pass state information into PRISM directly and on-the-fly, so that scaling is only limited by PRISM’s capabilities: one that I wouldn't be able to overcome anyways.

Unfortunately, as I’m writing this, Toronto has suffered severe storms bad enough to cause some minor street-level  flood downtown (not near me), but worse, to knock out power in many areas: myself included. I'm posting this a day late now from a coffee shop: the next post might also be similarly delayed.