Formal specs and optimizations in general

[steffahn]

@RalfJung

Basically you are saying there are two LLVM IRs, IR1 and IR2, with the same syntax but different semantics: IR1 has provenance and IR2 doesn't. The given optimization can only be correct in IR2, so at some point in the optimization pipeline there needs to be a clear transition from working with IR1 to working with IR2.

Yep, that was what I meant.

@RalfJung

Who wants to create a bugreport?

@RalfJung

Looks like we need to clarify the docs.

This would be two bug reports then, I guess..
I can do those tomorrow.