[LLVMdev] Correctness of Optimization Phases

[Aaron Gray]

>> Prooving correctness of a compiler is really an NP problem. This goes for
>> any compiler backend. All you can do is have enough test cases.
> No. To be in NP it would be necessary for a Non-deterministic
> Polynomial algorithm to exist. There is no such algorithm. The problem
> is undecidable.

Thanks for putting me right.

> It doesn't means that it is impossible to prove the correctness of a
> compiler. It means that no algorithm can do it.

Formal proof using Z would probably be the best means of attack.

>>From a practical point of view, I think that the original question was:
>
> Are the different optimizations "expected" to work in any order or do
> they have some inter dependencies?
> (I don't know the answer)

Yes.

Testing non optimized test programs against optimized either using JIT or a 
set platform might be a way forward.

Another means of attack might be an approach simular to generative fuzzing.

Aaron