TL;DR – The AndersenWaveDiff implementation of SVF handles positive-weight cycles by making the structure object involved field-insensitive!
Let’s look at how these positive-weight-cycles look like in the IR Representation, and the cycle that shows up in SVF.
The IR for the above C code is shown below. Note the BitCast Instructions that are used to assign to and from the void pointer q.
%a = alloca %struct.aggr, align 8
%p = alloca %struct.aggr*, align 8
%q = alloca i8*, align 8
store i32 0, i32* %retval, align 4
%0 = bitcast %struct.aggr* %a to i8*
store i8* %0, i8** %q, align 8
%1 = load i8*, i8** %q, align 8
%2 = bitcast i8* %1 to %struct.aggr*
store %struct.aggr* %2, %struct.aggr** %p, align 8
%3 = load %struct.aggr*, %struct.aggr** %p, align 8
%f2 = getelementptr inbounds %struct.aggr, %struct.aggr* %3, i32 0, i32 1
%4 = bitcast i32** %f2 to i8*
store i8* %4, i8** %q, align 8
The initial constraint Graph for the above example is shown in Figure 8. The BitCast Instructions are specified as CopyEdges. The rest of the IR instructions are handled as expected.
Figure 8
After solving the AddrEdges, and the CopyEdge 9 → 17, we get Figure 9.
Figure 9
Solving, the CopyEdges 9 → 17, 19 → 20, and the StoreEdges, 17 → 13, 20 → 12, and the LoadEdge 13→ 19, gives this constraint graph
Finally, solving edges LoadEdges, 11 → 22, and StoreEdge 24 → 13, we get the constraint graph shown in Figure 10.
Figure 10
As you can see, this has a cycle 14 → 19 → 20 → 12 → 22 → gep-edge → 23 → 24 → 14. This is how a positive weight cycle (PWC) looks in the SVF’s Constraint Graph.
Because, there’s a GepEdge for the struct obj 10, then object will become field-insensitive. Then the cycle will be collapsed into the final constraint graph shown in Figure 11. Note that the GepEdge is gone.
Figure 11
Tapti Palit 