@sohah
There's a bug in the code that computes local variable inputs to a region. The problem is with the algorithm you are using to figure out which variables consist of local variable inputs to a region.
For every use in every statement in the region, your algorithm checks if that use's corresponding stack slot, if there is one, has been seen in another use before. If it has never been seen, your algorithm concludes this use must be a input.
This algorithm isn't correct because it doesn't take into account that a used variable may have been defined in the same region. The algorithm should check if a use's corresponding stack slot, if there is one, has not been seen before and if the used Wala variable wasn't defined in the same region, then it must be a local input variable.
Here's the same bug explained with an example.
public double fieldDoubleTest(int x) {
AA aa = new AA(4.0);
aa.myDouble = 2.0;
double ret;
if (x > 0) {
aa.myDouble = 11.0;
ret = aa.myDouble + 1.0;
} else {
aa.myDouble = 12.0;
ret = aa.myDouble + 2.0;
}
return ret;
}This code uses fields but still works as a demonstrative example. Please find the corresponding Wala CFG here for reference.
Here's this region's static summary:
if (@w2<=@w8) {
putfield 4.< Application, LAA, myDouble, <Primordial,D> > = 13
14 = getfield < Application, LAA, myDouble, <Primordial,D> > 4
@w15 := @w14+@w7;
} else {
putfield 4.< Application, LAA, myDouble, <Primordial,D> > = 9
10 = getfield < Application, LAA, myDouble, <Primordial,D> > 4
@w12 := @w10+@w11;
}
@w16 := (Gamma @w2<=@w8 @w15 @w12); As you can see, the assignment containing the gamma at the end uses w15. w15 corresponds to stack slot 3 in the Java bytecode. w15 is also defined in this region.
When computing inputs for this region, ExprRegionInputVisitor concludes that w15 must be an input because it sees a Wala variable being used with stack slot 3 for the first time when w15 is used in the gamma expression. But because w15 was defined in the region, it is not an input to the region. We should change ExprRegionInputVisitor to also take such defs into account when finding local variable inputs.
@sohah
There's a bug in the code that computes local variable inputs to a region. The problem is with the algorithm you are using to figure out which variables consist of local variable inputs to a region.
For every use in every statement in the region, your algorithm checks if that use's corresponding stack slot, if there is one, has been seen in another use before. If it has never been seen, your algorithm concludes this use must be a input.
This algorithm isn't correct because it doesn't take into account that a used variable may have been defined in the same region. The algorithm should check if a use's corresponding stack slot, if there is one, has not been seen before and if the used Wala variable wasn't defined in the same region, then it must be a local input variable.
Here's the same bug explained with an example.
This code uses fields but still works as a demonstrative example. Please find the corresponding Wala CFG here for reference.
Here's this region's static summary:
As you can see, the assignment containing the gamma at the end uses w15. w15 corresponds to stack slot 3 in the Java bytecode. w15 is also defined in this region.
When computing inputs for this region, ExprRegionInputVisitor concludes that w15 must be an input because it sees a Wala variable being used with stack slot 3 for the first time when w15 is used in the gamma expression. But because w15 was defined in the region, it is not an input to the region. We should change ExprRegionInputVisitor to also take such defs into account when finding local variable inputs.