Provably Sound Nullness Analysis of Java Code