TY - GEN
T1 - ILEA
T2 - OOPSLA 2007: 22nd International Conference on Object-Oriented Programming, Systems, Languages, and Applications
AU - Gang, Tan
AU - Morrisett, Greg
N1 - Copyright:
Copyright 2011 Elsevier B.V., All rights reserved.
PY - 2007
Y1 - 2007
N2 - Java bug finders perform static analysis to find implementation mistakes that can lead to exploits and failures; Java compilers perform static analysis for optimization. If Java programs contain foreign function calls to C libraries, however, static analysis is forced to make either optimistic or pessimistic assumptions about the foreign function calls, since models of the C libraries are typically not available. We propose ILEA (stands for Inter-LanguagE Analysis), which is a framework that enables existing Java analyses to understand the behavior of C code. Our framework includes: (1) a novel specification language, which extends the Java Virtual Machine Language (JVML) with a few primitives that approximate the effects that the C code might have; (2) an automatic specification extractor, which builds models of the C code. Comparing to other possible specification languages, our language is expressive, yet facilitates construction of automatic specification extractors. Furthermore, because the specification language is based on the JVML, existing Java analyses can be easily migrated to utilize specifications in the language. We also demonstrate the utility of the specifications generated, by modifying an existing nonnull analysis to identify null-related bugs in Java applications that contain C libraries. Our preliminary experiments identified dozens of null-related bugs.
AB - Java bug finders perform static analysis to find implementation mistakes that can lead to exploits and failures; Java compilers perform static analysis for optimization. If Java programs contain foreign function calls to C libraries, however, static analysis is forced to make either optimistic or pessimistic assumptions about the foreign function calls, since models of the C libraries are typically not available. We propose ILEA (stands for Inter-LanguagE Analysis), which is a framework that enables existing Java analyses to understand the behavior of C code. Our framework includes: (1) a novel specification language, which extends the Java Virtual Machine Language (JVML) with a few primitives that approximate the effects that the C code might have; (2) an automatic specification extractor, which builds models of the C code. Comparing to other possible specification languages, our language is expressive, yet facilitates construction of automatic specification extractors. Furthermore, because the specification language is based on the JVML, existing Java analyses can be easily migrated to utilize specifications in the language. We also demonstrate the utility of the specifications generated, by modifying an existing nonnull analysis to identify null-related bugs in Java applications that contain C libraries. Our preliminary experiments identified dozens of null-related bugs.
UR - http://www.scopus.com/inward/record.url?scp=42149191939&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=42149191939&partnerID=8YFLogxK
U2 - 10.1145/1297027.1297031
DO - 10.1145/1297027.1297031
M3 - Conference contribution
AN - SCOPUS:42149191939
SN - 9781595937865
T3 - Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA
SP - 39
EP - 56
BT - OOPSLA
Y2 - 21 October 2007 through 25 October 2007
ER -