Unsoundness in flow sensitive alias algorithm due to strong updates

[amordahl]

Here's another issue (different cause than #501) with flow sensitive aliasing:

Test Case

Mutant of Callbacks/Button5.apk in DroidBench, in which the source and sink statements are switched in sendMessage():

    public void sendMessage(View view){
    ((Button)view).setHint(imei);  
    Log.i("DroidBench", ((Button)view).getHint().toString());  //sink on second call to sendMessage(), second click of button
    }

While the original Button5 only has a leak if the button is clicked twice, here we have a taint on any click of the button.

Issue

I think the issue is in StrongUpdatePropagationRule.java on line 79:

 // x = y && x.f tainted -> no taint propagated. This must only check the precise
// variable which gets replaced, but not any potential strong aliases
else if (assignStmt.getLeftOp() instanceof Local) {
    if (getAliasing().mustAlias((Local) assignStmt.getLeftOp(), source.getAccessPath().getPlainValue(),
            stmt)) {
        killAll.value = true;
        return null;
    }
}

which will kill a taint if we see that x = y and x.f is tainted. If y and x are aliases (as they are in the test case, when we have a cast ($r2 = (Button) $r1), the taint should not be killed. Again, like in #501, I'm unsure of whether this is the actual problem or whether there is some other machinery that's supposed to be re-propagating the taint to x, but I was able to step through the debugger and check that this is where the taint that should be propagated to the sink was killed.

[StevenArzt]

That's interesting. If we have x.f tainted and a statement x = y, the taint must be killed, because x.f points to another object after the statement. Consequently, we cannot assume that x.f is still tainted. Only in case y.f is tainted as well, the taint needs to be kept. Maybe this is the missing corner case here? Can you please double-check?