Unsound interprocedural Array_bounds analysis when array is modified

[julbinb]

solved_ArraySwap.dsg.zip
Here is a Java version of bucket_swap.js from DAI's benchmarks:

public class ArraySwap {
    static boolean swap(int[] array, int i, int j) {
        int temp;
        if (i < 0 || i >= array.length || j < 0 || j >= array.length) {
            return false;
        }
        temp = array[i];
        array[i] = array[j];
        array[j] = temp;
        return true;
    }
    
    public static void main(String[] args) {
        int[] numberArray = {1, 8, 10};//;1, 8, 8, 8, 10, 10};
        boolean mustTrue = numberArray[1] == 8;
        
        // test cases "swap only accepts valid positions"
        boolean test1 = swap(numberArray, 0, 2);
        boolean test2 = swap(numberArray, 0, 1);
        
        // the analysis is unsound: it reports true here
        boolean mustFalse = numberArray[1] == 8;
        
        // test cases "swap accepts bad positions"
        boolean test3 = swap(numberArray, 42, 1);
    }
}

Interprocedural analysis with Array_bounds computes mustFalse to be true.

Looking at the DAIG of swap, I see that elements of the input array are removed from the abstract memory when the array is modified. And then in the main function, abstract memory remains the same, "forgetting" the fact the array has changed.

[UPD] The DSG is attached.

[bennostein]

I can repro this -- thanks for the test case! That domain should be smarter in how it applies procedure summaries at return sites. It's able to deal with mutation on fields of the receiver but isn't correctly handling mutations on arguments. I'll try to get that ironed out soon when I get the time!