Inferring State / Day 25

Today's goal was to determine what state is referenced by each integer label returned by jpf-probabilistic. To this end, there were a few methods that could possibly do this. First, and easiest, but probably also least useful, was to augment the listener to look for specific variables within the code. However, there are drawbacks: 1) it appears you can only target variables at the class level (that is, variables defined in a smaller scope, say within a Java method, cannot be targeted through this method); I could be wrong, but the FieldSpec documentation in JPF didn't seem to support more than this, and 2) you need to know the variables beforehand so that you can manually enter them into the .jpf file you are verifying (this could be mitigated by writing a tool to look at the code and add all of these to the .jpf file, but it seems like this much work is not ideal before verifying arbitrary code). Second, and perhaps even easier, is to have JPF report on all variables as they are updated, and keep an internal representation of their values. This could get complicated (especially for large programs), and it has the added downside of also reporting system variables that are called, so this is not optimal. Some combination of the two might be best, or the second method with some filtering. I think for this to work (easily), we may need to pre-process the code that we want to verify and pass that to the listener so that it limits its work, or find some way to target only some classes/methods/variables--I feel like this might very well be possible, but I need to look into it more. I'm going to look into more methods tomorrow as well.