Checking type safety of foreign function calls

ABSTRACT

We present a multi-lingual type inference system for checking type safety across a foreign function interface. The goal of our system is to prevent foreign function calls from introducing type and memory safety violations into an otherwise safe language. Our system targets OCaml's FFI to C, which is relatively lightweight and illustrates some interesting challenges in multi-lingual type inference. The type language in our system embeds OCaml types in C types and vice-versa, which allows us to track type information accurately even through the foreign language, where the original types are lost. Our system uses representational types that can model multiple OCaml types, because C programs can observe that many OCaml types have the same physical representation. Furthermore, because C has a low-level view of OCaml data, our inference system includes a dataflow analysis to track memory offsets and tag information. Finally, our type system includes garbage collection information to ensure that pointers from the FFI to the OCaml heap are tracked properly. We have implemented our inference system and applied it to a small set of benchmarks. Our results show that programmers do misuse these interfaces, and our implementation has found several bugs and questionable coding practices in our benchmarks.

REFERENCES

• 1: ANSI. Programming languages -- C, 1999. ISO/IEC 9899:1999.
• 2: D. M. Beazley. SWIG: An easy to use tool for integrating scripting languages with C and C++,.
• 3: N. Benton and A. Kennedy, editors. BABEL'01: First International Workshop on Multi-Language Infrastructure and Interoperability, volume 59 of Electronic Notes in Theoretical Computer Science, Firenze, Italy, Sept. 2001. http://www.elsevier.nl/locate/entcs/volume59.html.
• 4: M. Blume. No-Longer-Foreign: Teaching an ML compiler to speak C "natively". In Benton and Kennedy babel01. http://www.elsevier.nl/locate/entcs/volume59.html.
• 5: Satish Chandra , Thomas Reps, Physical type checking for C, Proceedings of the 1999 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.66-75, September 06-06, 1999, Toulouse, France
• 6: A. S. Christensen, A. Møller, and M. I. Schwartzbach. Precise Analysis of String Expressions. In R. Cousot, editor, Static Analysis, 10th International Symposium, volume 2694 of Lecture Notes in Computer Science, pages 1--18, San Diego, CA, USA, June 2003. Springer-Verlag.
• 7: R. DeLine and M. Fähndrich. The Fugue Protocol Checker: Is your software Baroque? Technical Report MSR-TR-2004-07, Microsoft Research, Jan. 2004.
• 8: Sigbjorn Finne , Daan Leijen , Erik Meijer , Simon Peyton Jones, Calling hell from heaven and heaven from hell, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.114-125, September 27-29, 1999, Paris, France
• 9: K. Fisher, R. Pucella, and J. Reppy. A framework for interoperability. In Benton and Kennedy {3}. http://www.elsevier.nl/locate/entcs/volume59.html.
• 10: M. Furr and J. S. Foster. Checking Type Safety of Foreign Function Calls. Technical Report CS-TR-4627, University of Maryland, Computer Science Department, Nov. 2004.
• 11: Carl Gould , Zhendong Su , Premkumar Devanbu, Static Checking of Dynamically Generated Queries in Database Applications, Proceedings of the 26th International Conference on Software Engineering, p.645-654, May 23-28, 2004
• 12: David N. Gray , John Hotchkiss , Seth LaForge , Andrew Shalit , Toby Weinberg, Modern languages and Microsoft's component object model, Communications of the ACM, v.41 n.5, p.55-65, May 1998 [doi>10.1145/274946.274957]
• 13: J. Hamilton. Interlanguage Object Sharing with SOM. In Proceedings of the Usenix 1996 Annual Technical Conference, San Diego, California, Jan. 1996.
• 14: Jennifer Hamilton, Language integration in the common language runtime, ACM SIGPLAN Notices, v.38 n.2, February 2003 [doi>10.1145/772970.772973]
• 15: L. Huelsbergen. A Portable C Interface for Standard ML of New Jersey. http://www.smlnj.org//doc/SMLNJ-C/smlnj-c.ps, 1996.
• 16: X. Leroy. The Objective Caml system, Aug. 2004. Release 3.08, http://caml.inria.fr/distrib/ocaml-3.08/ocaml-3.08-refman.pdf.
• 17: Sheng Liang, Java Native Interface: Programmer's Guide and Reference, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 18: Erik Meijer , Nigel Perry , Arjan van Yzendoorn, Scripting .NET Using Mondrian, Proceedings of the 15th European Conference on Object-Oriented Programming, p.150-164, June 18-22, 2001
• 19: George C. Necula , Scott McPeak , Westley Weimer, CCured: type-safe retrofitting of legacy code, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.128-139, January 16-18, 2002, Portland, Oregon
• 20: George C. Necula , Scott McPeak , Shree Prakash Rahul , Westley Weimer, CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs, Proceedings of the 11th International Conference on Compiler Construction, p.213-228, April 08-12, 2002
• 21: D. Rémy, Type checking records and variants in a natural extension of ML, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.77-88, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75284]
• 22: Valery Trifonov , Zhong Shao, Safe and Principled Language Interoperation, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.128-146, March 22-28, 1999

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
        D.2.12 Interoperability
      D.2.4 Software/Program Verification
          Subjects: Validation

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

General Terms:
Languages, Verification

Keywords:
FFI, OCaml, dataflow analysis, flow-sensitive type system, foreign function calls, foreign function interface, multi-lingual type inference, multi-lingual type system, representational type