Static Program Equivalence Checking Across Aggressive Compiler Optimizations