Interprocedural herbrand equalities

Markus Müller-Olm; Helmut Seidl; Bernhard Steffen

doi:10.1007/978-3-540-31987-0_4

Interprocedural herbrand equalities

Markus Müller-Olm
, Helmut Seidl
, Bernhard Steffen

Informatics 2 - Chair of Formal Languages, Compiler Construction, Software Construction

pro3dure medical GmbH

Research output: Contribution to journal › Conference article › peer-review

13 Scopus citations

Abstract

We present an aggressive interprocedural analysis for inferring value equalities which are independent of the concrete interpretation of the operator symbols. These equalities, called Herbrand equalities, are therefore an ideal basis for truly machine-independent optimizations as they hold on every machine. Besides a general correctness theorem, covering arbitrary call-by-value parameters and local and global variables, we also obtain two new completeness results: one by constraining the analysis problem to Herbrand constants, and one by allowing side-effect-free functions only. Thus if we miss a constant/equality in these two scenarios, then there exists a separating interpretation of the operator symbols.

Original language	English
Pages (from-to)	31-45
Number of pages	15
Journal	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	3444
DOIs	https://doi.org/10.1007/978-3-540-31987-0_4
State	Published - 2005
Event	14th European Symposium on Programming, ESOP 2005, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005 - Edinburgh, United Kingdom Duration: 4 Apr 2005 → 8 Apr 2005

Access to Document

10.1007/978-3-540-31987-0_4

Cite this

@article{52a0c951bc264cb293cab28bb43df3fe,

title = "Interprocedural herbrand equalities",

abstract = "We present an aggressive interprocedural analysis for inferring value equalities which are independent of the concrete interpretation of the operator symbols. These equalities, called Herbrand equalities, are therefore an ideal basis for truly machine-independent optimizations as they hold on every machine. Besides a general correctness theorem, covering arbitrary call-by-value parameters and local and global variables, we also obtain two new completeness results: one by constraining the analysis problem to Herbrand constants, and one by allowing side-effect-free functions only. Thus if we miss a constant/equality in these two scenarios, then there exists a separating interpretation of the operator symbols.",

author = "Markus M{\"u}ller-Olm and Helmut Seidl and Bernhard Steffen",

year = "2005",

doi = "10.1007/978-3-540-31987-0\_4",

language = "English",

volume = "3444",

pages = "31--45",

journal = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

issn = "0302-9743",

publisher = "Springer Science and Business Media Deutschland GmbH",

note = "14th European Symposium on Programming, ESOP 2005, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005 ; Conference date: 04-04-2005 Through 08-04-2005",

}

TY - JOUR

T1 - Interprocedural herbrand equalities

AU - Müller-Olm, Markus

AU - Seidl, Helmut

AU - Steffen, Bernhard

PY - 2005

Y1 - 2005

N2 - We present an aggressive interprocedural analysis for inferring value equalities which are independent of the concrete interpretation of the operator symbols. These equalities, called Herbrand equalities, are therefore an ideal basis for truly machine-independent optimizations as they hold on every machine. Besides a general correctness theorem, covering arbitrary call-by-value parameters and local and global variables, we also obtain two new completeness results: one by constraining the analysis problem to Herbrand constants, and one by allowing side-effect-free functions only. Thus if we miss a constant/equality in these two scenarios, then there exists a separating interpretation of the operator symbols.

AB - We present an aggressive interprocedural analysis for inferring value equalities which are independent of the concrete interpretation of the operator symbols. These equalities, called Herbrand equalities, are therefore an ideal basis for truly machine-independent optimizations as they hold on every machine. Besides a general correctness theorem, covering arbitrary call-by-value parameters and local and global variables, we also obtain two new completeness results: one by constraining the analysis problem to Herbrand constants, and one by allowing side-effect-free functions only. Thus if we miss a constant/equality in these two scenarios, then there exists a separating interpretation of the operator symbols.

UR - https://www.scopus.com/pages/publications/24644508567

U2 - 10.1007/978-3-540-31987-0_4

DO - 10.1007/978-3-540-31987-0_4

M3 - Conference article

AN - SCOPUS:24644508567

SN - 0302-9743

VL - 3444

SP - 31

EP - 45

JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

T2 - 14th European Symposium on Programming, ESOP 2005, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005

Y2 - 4 April 2005 through 8 April 2005

ER -

Interprocedural herbrand equalities

Abstract

Access to Document

Other files and links

Fingerprint

Cite this