Re: How to verify that optimizations preserve semantics

Stephan,


> I was wondering how compiler optimisations can be verified,
> i.e. whether they perform always valid code modifications? How is it
> done in practice?


Do you want an academic or realistic answer? ;-)


In theory, you can use model checking to prove equivalence between a
high-level specification of an optimisation and its implementation. This
is tricky and, so far, has only been done for a few "real"
optimisations. For simplified languages and compilers you can also try
proving equivalence of the source code of your application and the
generated machine code.


In practice, you use regression testing against a test suite such as
SuperTest or similar. If your compiler passes the regression test you
assume it's probably ok and release it. If your customers discover more
bugs you'd try to come up with the smallest possible test case that
still exhibits this bug, fix it in your compiler and include the test
case in your regression suite for future tests.


Cheers,


        Bjoern

Return to the comp.compilers page.
Search the comp.compilers archives again.