2014 | OriginalPaper | Buchkapitel
Practical Floating-Point Tests with Integer Code
verfasst von : Anthony Romano
Erschienen in: Verification, Model Checking, and Abstract Interpretation
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Testing integer software with symbolic execution is wellestablished but floating-point remains a specialty feature. Modern symbolic floating-point tactics include concretization, lexical analysis, floating-point solvers, and intricate theories, but mostly ignore the default integer-only capabilities. If a symbolic executor is already highperformance, then software-emulation, common to integer-only machines, becomes a compelling choice for symbolic floating-point.
We propose a software floating-point emulation extension for symbolic execution of binary programs. First, supporting a soft floating-point library requires little effort, so multiple models are cheap; our executor has five distinct open source soft floating-point code bases. For integrity, test cases from symbolic execution of library code itself are hardware validated; mismatches with hardware appear in every tested library, a justin- time compiler, a machine decoder, and several floating-point solvers. In practice, the executor finds program faults involving floating-point in hundreds of Linux binaries.