Universität Karlsruhe
Classifying and Formally Verifying Integer Constant Folding
  author={Sabine Glesner and Jan Olaf Blech},
  title=\{Classifying and Formally Verifying Integer Constant Folding},
  booktitle=\{Proceedings of the Workshop COCV 2003: Compiler Optimization meets Compiler Verification},
  organization=\{ETAPS Conferences},
  publisher=\{Electronic Notes in Theoretical Computer Science (ENTCS), Vol. 82, No. 2},
  abstract=\{Constant folding is a well-known optimization of compilers which
evaluates constant expressions already at compile time. Constant
folding is valid only if the results computed by the compiler are
exactly the same as the results which would be computed at run-time by
the target machine arithmetic.  We classify different arithmetics by
deriving a general condition under which a target-machine arithmetic
can be replaced by a compiler arithmetic.  Furthermore, we consider
integer arithmetics as a special case. They can be described by
residue class arithmetics. We show that these arithmetics form a
lattice. Using the order relation in this lattice, we establish a
necessary and sufficient criterion under which constant folding can be
done in a residue class arithmetic that is different from the one of
the target machine.  Concerning formal verification, we have
formalized our proofs in the Isabelle/HOL system. As examples, we
discuss the Java and C integer arithmetics and show which compiler
arithmetics are valid for constant folding. This discussion reveals
also potential sources of incorrect behavior of C compilers.},
  editor=\{Jens Knoop and Wolf Zimmermann},
  address=\{Warsaw, Poland},