direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Page Content


Classifying and Formally Verifying Integer Constant Folding
Citation key glesner03classifying
Author Sabine Glesner and Jan Olaf Blech
Title of Book Proceedings of the Workshop COCV 2003: Compiler Optimization meets Compiler Verification
Year 2003
Address Warsaw, Poland
Volume 82
Number 2
Month Apr
Editor Jens Knoop and Wolf Zimmermann
Publisher Electronic Notes in Theoretical Computer Science (ENTCS), Vol. 82, No. 2
Organization ETAPS Conferences
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.
Bibtex Type of Publication Conference Article
Download Bibtex entry

Zusatzinformationen / Extras

Quick Access:

Schnellnavigation zur Seite über Nummerneingabe