Details

Autor(en) / Beteiligte

• FURR, Michael
• FOSTER, Jeffrey S

Titel

Checking Type Safety of Foreign Function Calls

Ist Teil von

• ACM transactions on programming languages and systems, 2008-07, Vol.30 (4), p.1-63

Ort / Verlag

New York, NY: Association for Computing Machinery

Erscheinungsjahr

2008

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• Foreign function interfaces (FFIs) allow components in different languages to communicate directly with each other. While FFIs are useful, they often require writing tricky low-level code and include little or no static safety checking, thus providing a rich source of hard-to-find programming errors. In this article, we study the problem of enforcing type safety across the OCaml-to-C FFI and the Java Native Interface (JNI). We present O-Saffire and J-Saffire, a pair of multilingual type inference systems that ensure C code that uses these FFIs accesses high-level data safely. Our inference systems use representational types to model C's low-level view of OCaml and Java values, and singleton types to track integers, strings, memory offsets, and type tags through C. J-Saffire, our Java system, uses a polymorphic flow-insensitive, unification-based analysis. Polymorphism is important because it allows us to precisely model user-defined wrapper functions and the more than 200 JNI functions. O-Saffire, our OCaml system, uses a monomorphic flow-sensitive analysis because, while polymorphism is much less important for the OCaml FFI flow-sensitivity is critical to track conditional branches, which are used when pattern matching OCaml data in C. O-Saffire also tracks garbage collection information to ensure that local C pointers to the OCaml heap are registered properly, which is not necessary for the JNI. We have applied O-Saffire and J-Saffire to a set of benchmarks and found many bugs and questionable coding practices. These results suggest that static checking of FFIs can be a valuable tool in writing correct multilingual software.