CIL

CIL: intermediate language and tools for analysis and transformation of C programs. This paper describes the C Intermediate Language: a highlevel representation along with a set of tools that permit easy analysis and source-to-source transformation of C programs. Compared to C, CIL has fewer constructs. It breaks down certain complicated constructs of C into simpler ones, and thus it works at a lower level than abstract-syntax trees. But CIL is also more high-level than typical intermediate languages (e.g., three-address code) designed for compilation. As a result, what we have is a representation that makes it easy to analyze and manipulate C programs, and emit them in a form that resembles the original source. Moreover, it comes with a front-end that translates to CIL not only ANSI C programs but also those using Microsoft C or GNU C extensions. We describe the structure of CIL with a focus on how it disambiguates those features of C that we found to be most confusing for program analysis and transformation. We also describe a whole-program merger based on structural type equality, allowing a complete project to be viewed as a single compilation unit. As a representative application of CIL, we show a transformation aimed at making code immune to stack-smashing attacks. We are currently using CIL as part of a system that analyzes and instruments C programs with run-time checks to ensure type safety. CIL has served us very well in this project, and we believe it can usefully be applied in other situations as well.


References in zbMATH (referenced in 32 articles )

Showing results 1 to 20 of 32.
Sorted by year (citations)

1 2 next

  1. Kojima, Kensuke; Imanishi, Akifumi; Igarashi, Atsushi: Automated verification of functional correctness of race-free GPU programs (2018)
  2. Lauko, Henrich; Ročkai, Petr; Barnat, Jiří: Symbolic computation via program transformation (2018)
  3. Abal, Iago; Brabrand, Claus; Wąsowski, Andrzej: Effective bug finding in C programs with shape and effect abstractions (2017)
  4. Jiang, Jiahong; Chen, Liqian; Wu, Xueguang; Wang, Ji: Block-wise abstract interpretation by combining abstract domains with SMT (2017)
  5. Kirchner, Florent; Kosmatov, Nikolai; Prevosto, Virgile; Signoles, Julien; Yakobowski, Boris: Frama-C: a software analysis perspective (2015) ioport
  6. Zakharov, I.; Mandrykin, M.; Mutilin, V.; Novikov, E.; Petrenko, A.; Khoroshilov, A.: Configurable toolset for static verification of operating systems kernel modules (2015) ioport
  7. Groce, Alex; Havelund, Klaus; Holzmann, Gerard; Joshi, Rajeev; Xu, Ru-Gang: Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning (2014)
  8. Hills, Mark; Chen, Feng; Roşu, Grigore: A rewriting logic approach to static checking of units of measurement in C (2012) ioport
  9. Jeannet, Bertrand; Sotin, Pascal: Inferring effective types for static analysis of C programs (2012)
  10. Mandrykin, M. U.; Mutilin, V. S.; Novikov, E. M.; Khoroshilov, A. V.; Shved, P. E.: Using Linux device drivers for static verification tools benchmarking (2012) ioport
  11. Seyster, Justin; Dixit, Ketan; Huang, Xiaowan; Grosu, Radu; Havelund, Klaus; Smolka, Scott A.; Stoller, Scott D.; Zadok, Erez: \textscInterAspect: aspect-oriented instrumentation with GCC (2012)
  12. Shved, P. E.; Mutilin, V. S.; Mandrykin, M. U.: Experience of improving the BLAST static verification tool (2012)
  13. Boldo, Sylvie; Marché, Claude: Formal verification of numerical programs: from C annotated programs to mechanical proofs (2011)
  14. Dos Reis, Gabriel; Stroustrup, Bjarne: A principled, complete, and efficient representation of C++ (2011)
  15. Gay, David; Galenson, Joel; Naik, Mayur; Yelick, Kathy: Yada: straightforward parallel programming (2011) ioport
  16. Kerneis, Gabriel; Chroboczek, Juliusz: Continuation-passing C, compiling threads to events through continuations (2011)
  17. Krishnamoorthy, Saparya; Hsiao, Michael S.; Lingappan, Loganathan: Strategies for scalable symbolic execution-driven test generation for programs (2011)
  18. Wang, Chao; Kundu, Sudipta; Limaye, Rhishikesh; Ganai, Malay; Gupta, Aarti: Symbolic predictive analysis for concurrent programs (2011)
  19. Usui, Takayuki; Behrends, Reimer; Evans, Jacob; Smaragdakis, Yannis: Adaptive locks: combining transactions and locks for efficient concurrency (2010)
  20. Blazy, Sandrine; Leroy, Xavier: Mechanized semantics for the clight subset of the C language (2009)

1 2 next