direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Inhalt des Dokuments


Classifying and Formally Verifying Integer Constant Folding
Zitatschlüssel glesner03classifying
Autor Sabine Glesner and Jan Olaf Blech
Buchtitel Proceedings of the Workshop COCV 2003: Compiler Optimization meets Compiler Verification
Jahr 2003
Adresse Warsaw, Poland
Jahrgang 82
Nummer 2
Monat Apr
Herausgeber Jens Knoop and Wolf Zimmermann
Verlag Electronic Notes in Theoretical Computer Science (ENTCS), Vol. 82, No. 2
Organisation ETAPS Conferences
Zusammenfassung 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.
Typ der Publikation Conference Article
Download Bibtex Eintrag

Zusatzinformationen / Extras


Schnellnavigation zur Seite über Nummerneingabe