Skip to main content

28.03.2023

On multi-language abstraction: Towards a static analysis of multi-language programs

verfasst von: Samuele Buro, Roy Crole, Isabella Mastroeni

Erschienen in: Formal Methods in System Design

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Modern software development rarely takes place within a single programming language. Often, programmers appeal to cross-language interoperability. Examples are exploitation of novel features of one language within another, and cross-language code reuse. Our previous works developed a theory of so-called multi-languages, which arise by combining existing languages, defining a precise notion of (algebraic) multi-language semantics. As regards static analysis, the heterogeneity of the multi-language context opens up new and unexplored scenarios. In this paper, we provide a general theory for the combination of abstract interpretations of existing languages, regardless of their inherent nature, in order to gain an abstract semantics of multi-language programs. As a part of this general theory, we show that formal properties of interest of multi-language abstractions (e.g., soundness and completeness) boil down to the features of the interoperability mechanism that binds the underlying languages together. We extend many of the standard concepts of abstract interpretation to the framework of multi-languages.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
1
A commercial static code analyser for Java (version 3.2.0.1227: for Linux 64 bit).
 
Literatur
1.
Zurück zum Zitat Ramsey N (2006) ML module mania: a type-safe, separately compiled, extensible interpreter. Electron Notes Theor Comput Sci 148(2):181–209CrossRef Ramsey N (2006) ML module mania: a type-safe, separately compiled, extensible interpreter. Electron Notes Theor Comput Sci 148(2):181–209CrossRef
2.
Zurück zum Zitat Juneau J, Baker J, Wierzbicki F, Soto L, Ng V (2010) The definitive guide to Jython: python for the java platform, 1st edn. Apress, BerkelyCrossRef Juneau J, Baker J, Wierzbicki F, Soto L, Ng V (2010) The definitive guide to Jython: python for the java platform, 1st edn. Apress, BerkelyCrossRef
3.
Zurück zum Zitat Liang S (1999) Java native interface: programmer’s guide and reference, 1st edn. Addison-Wesley Longman Publishing Co. Inc., Boston Liang S (1999) Java native interface: programmer’s guide and reference, 1st edn. Addison-Wesley Longman Publishing Co. Inc., Boston
4.
Zurück zum Zitat Buro S, Mastroeni I (2019) On the multi-language construction. In: European symposium on programming. Springer, pp 293–321 Buro S, Mastroeni I (2019) On the multi-language construction. In: European symposium on programming. Springer, pp 293–321
5.
Zurück zum Zitat Chisnall D (2013) The challenge of cross-language interoperability. Commun ACM 56(12):50–56CrossRef Chisnall D (2013) The challenge of cross-language interoperability. Commun ACM 56(12):50–56CrossRef
6.
Zurück zum Zitat Perconti JT, Ahmed A (2014) Verifying an open compiler using multi-language semantics. In: Proceedings of the 23rd European symposium on programming languages and systems, pp 128–148. Springer, Berlin Perconti JT, Ahmed A (2014) Verifying an open compiler using multi-language semantics. In: Proceedings of the 23rd European symposium on programming languages and systems, pp 128–148. Springer, Berlin
7.
Zurück zum Zitat Ahmed A, Blume M (2011) An equivalence-preserving cps translation via multi-language semantics. SIGPLAN Not 46(9):431–444CrossRefMATH Ahmed A, Blume M (2011) An equivalence-preserving cps translation via multi-language semantics. SIGPLAN Not 46(9):431–444CrossRefMATH
8.
Zurück zum Zitat Furr M, Foster JS (2005) Checking type safety of foreign function calls. SIGPLAN Not. 40(6):62–72CrossRef Furr M, Foster JS (2005) Checking type safety of foreign function calls. SIGPLAN Not. 40(6):62–72CrossRef
9.
Zurück zum Zitat Gray KE (2008) Safe cross-language inheritance. In: Vitek J (ed) ECOOP 2008–object-oriented programming. Springer, Berlin, pp 52–75CrossRef Gray KE (2008) Safe cross-language inheritance. In: Vitek J (ed) ECOOP 2008–object-oriented programming. Springer, Berlin, pp 52–75CrossRef
10.
Zurück zum Zitat Patterson D, Perconti J, Dimoulas C, Ahmed A (2017) Funtal: reasonably mixing a functional language with assembly. In: Proceedings of the 38th ACM SIGPLAN conference on programming language design and implementation. ACM, New York, pp 495–509 Patterson D, Perconti J, Dimoulas C, Ahmed A (2017) Funtal: reasonably mixing a functional language with assembly. In: Proceedings of the 38th ACM SIGPLAN conference on programming language design and implementation. ACM, New York, pp 495–509
11.
Zurück zum Zitat Matthews J, Findler RB (2009) Operational semantics for multi-language programs. ACM Trans Program Lang Syst 31(3):12–11244CrossRefMATH Matthews J, Findler RB (2009) Operational semantics for multi-language programs. ACM Trans Program Lang Syst 31(3):12–11244CrossRefMATH
12.
Zurück zum Zitat Campbell G, Papapetrou PP (2013) SonarQube in action. Manning Publications Co., Shelter Island Campbell G, Papapetrou PP (2013) SonarQube in action. Manning Publications Co., Shelter Island
13.
Zurück zum Zitat Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on principles of programming languages, pp 238–252 Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on principles of programming languages, pp 238–252
15.
Zurück zum Zitat Buro S, Crole RL, Mastroeni I (2020) On multi-language abstraction—towards a static analysis of multi-language programs. In: Pichardie D, Sighireanu M (eds) Proceedings of static analysis—27th international symposium, SAS 2020, virtual event, November 18-20, 2020, Lecture Notes in Computer Science, vol 12389. Springer, pp 310–332 Buro S, Crole RL, Mastroeni I (2020) On multi-language abstraction—towards a static analysis of multi-language programs. In: Pichardie D, Sighireanu M (eds) Proceedings of static analysis—27th international symposium, SAS 2020, virtual event, November 18-20, 2020, Lecture Notes in Computer Science, vol 12389. Springer, pp 310–332
16.
Zurück zum Zitat Goguen JA, Meseguer J (1992) Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoret Comput Sci 105(2):217–273MathSciNetCrossRefMATH Goguen JA, Meseguer J (1992) Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoret Comput Sci 105(2):217–273MathSciNetCrossRefMATH
19.
Zurück zum Zitat Cohen H, Frey G, Avanzi R, Doche C, Lange T, Nguyen K, Vercauteren F (2005) Handbook of elliptic and hyperelliptic curve cryptography. CRC Press, Boca RatonCrossRefMATH Cohen H, Frey G, Avanzi R, Doche C, Lange T, Nguyen K, Vercauteren F (2005) Handbook of elliptic and hyperelliptic curve cryptography. CRC Press, Boca RatonCrossRefMATH
20.
21.
Zurück zum Zitat Cousot P, Giacobazzi R, Ranzato F (2019) A\(^2\)i: abstract\(^2\) interpretation. Proc ACM Program Lang 3(POPL):1–31CrossRef Cousot P, Giacobazzi R, Ranzato F (2019) A\(^2\)i: abstract\(^2\) interpretation. Proc ACM Program Lang 3(POPL):1–31CrossRef
22.
Zurück zum Zitat Amato G, Meo MC, Scozzari F (2020) On collecting semantics for program analysis. Theoret Comput Sci Amato G, Meo MC, Scozzari F (2020) On collecting semantics for program analysis. Theoret Comput Sci
23.
Zurück zum Zitat Spoto F, Jensen T (2003) Class analyses as abstract interpretations of trace semantics. ACM Trans Program Lang Syst 25(5):578–630CrossRef Spoto F, Jensen T (2003) Class analyses as abstract interpretations of trace semantics. ACM Trans Program Lang Syst 25(5):578–630CrossRef
24.
Zurück zum Zitat Bjørner N, Gurfinkel A (2015) Property directed polyhedral abstraction. In: International workshop on verification, model checking, and abstract interpretation. Springer, pp 263–281 Bjørner N, Gurfinkel A (2015) Property directed polyhedral abstraction. In: International workshop on verification, model checking, and abstract interpretation. Springer, pp 263–281
25.
Zurück zum Zitat Kochems J, Ong C (2011) Improved functional flow and reachability analyses using indexed linear tree grammars. In: 22nd International conference on rewriting techniques and applications (RTA’11). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik Kochems J, Ong C (2011) Improved functional flow and reachability analyses using indexed linear tree grammars. In: 22nd International conference on rewriting techniques and applications (RTA’11). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik
26.
Zurück zum Zitat Giacobazzi R, Ranzato F (1997) Completeness in abstract interpretation: a domain perspective. In: International conference on algebraic methodology and software technology. Springer, pp 231–245 Giacobazzi R, Ranzato F (1997) Completeness in abstract interpretation: a domain perspective. In: International conference on algebraic methodology and software technology. Springer, pp 231–245
27.
Zurück zum Zitat Cousot P (2002) Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theoret Comput Sci 277(1–2):47–103MathSciNetCrossRefMATH Cousot P (2002) Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theoret Comput Sci 277(1–2):47–103MathSciNetCrossRefMATH
28.
Zurück zum Zitat Mastroeni I, Pasqua M (2017) Hyperhierarchy of semantics-a formal framework for hyperproperties verification. In: International static analysis symposium. Springer, pp 232–252 Mastroeni I, Pasqua M (2017) Hyperhierarchy of semantics-a formal framework for hyperproperties verification. In: International static analysis symposium. Springer, pp 232–252
29.
Zurück zum Zitat Pasqua M (2019) Hyper static analysis of programs—an abstract interpretation-based framework for hyperproperties verification. PhD thesis, University of Verona Pasqua M (2019) Hyper static analysis of programs—an abstract interpretation-based framework for hyperproperties verification. PhD thesis, University of Verona
30.
Zurück zum Zitat Rival X, Yi K (2019) Introduction to Static Analysis Rival X, Yi K (2019) Introduction to Static Analysis
31.
Zurück zum Zitat Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on principles of programming languages, pp 84–96 Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on principles of programming languages, pp 84–96
32.
Zurück zum Zitat Arceri V, Mastroeni I (2019) Static program analysis for string manipulation languages. Electron Proc Theoret Comput Sci 299:19–33CrossRef Arceri V, Mastroeni I (2019) Static program analysis for string manipulation languages. Electron Proc Theoret Comput Sci 299:19–33CrossRef
37.
Zurück zum Zitat Monat R, Ouadjaout A, Miné A (2021) A multilanguage static analysis of python programs with native C extensions. In: Dragoi C, Mukherjee S, Namjoshi KS (eds) Static analysis—28th international symposium, SAS 2021, USA. Lecture Notes in Computer Science, vol 12913, pp 323–345 Monat R, Ouadjaout A, Miné A (2021) A multilanguage static analysis of python programs with native C extensions. In: Dragoi C, Mukherjee S, Namjoshi KS (eds) Static analysis—28th international symposium, SAS 2021, USA. Lecture Notes in Computer Science, vol 12913, pp 323–345
38.
Zurück zum Zitat Gordon AD, Syme D (2001) Typing a multi-language intermediate code. Conference Record of POPL 2001: the 28th ACM SIGPLAN-SIGACT symposium on principles of programming languages. London, UK, January 17–19, 2001. ACM, New York, pp 248–260 Gordon AD, Syme D (2001) Typing a multi-language intermediate code. Conference Record of POPL 2001: the 28th ACM SIGPLAN-SIGACT symposium on principles of programming languages. London, UK, January 17–19, 2001. ACM, New York, pp 248–260
39.
Zurück zum Zitat Grimmer M, Schatz R, Seaton C, Würthinger T, Luján M (2018) Cross-language interoperability in a multi-language runtime. ACM Trans Program Lang Syst 40(2):8–1843CrossRef Grimmer M, Schatz R, Seaton C, Würthinger T, Luján M (2018) Cross-language interoperability in a multi-language runtime. ACM Trans Program Lang Syst 40(2):8–1843CrossRef
40.
Zurück zum Zitat Barrett E, Bolz CF, Tratt L (2015) Approaches to interpreter composition. Comput Lang Syst Struct 44:199–217 Barrett E, Bolz CF, Tratt L (2015) Approaches to interpreter composition. Comput Lang Syst Struct 44:199–217
42.
Zurück zum Zitat Buro S, Mastroeni I, Crole RL (2020) Equational logic and categorical semantics for multi-languages. In: In-press (accepted for Publication at 36th international conference on mathematical foundations of programming semantics—MFPS 2020) Buro S, Mastroeni I, Crole RL (2020) Equational logic and categorical semantics for multi-languages. In: In-press (accepted for Publication at 36th international conference on mathematical foundations of programming semantics—MFPS 2020)
43.
Zurück zum Zitat Buro S, Mastroeni I, Crole RL (2020) Equational logic and set-theoretic models for multi-languages. In: In-press (accepted for Publication at 21st Italian Conference on Theoretical Computer Science — ICTCS 2020) Buro S, Mastroeni I, Crole RL (2020) Equational logic and set-theoretic models for multi-languages. In: In-press (accepted for Publication at 21st Italian Conference on Theoretical Computer Science — ICTCS 2020)
44.
Zurück zum Zitat Tan G, Morrisett G (2007) Ilea: inter-language analysis across Java and C. SIGPLAN Not 42(10):39–56CrossRef Tan G, Morrisett G (2007) Ilea: inter-language analysis across Java and C. SIGPLAN Not 42(10):39–56CrossRef
45.
Zurück zum Zitat Li S, Tan G (2014) Finding reference-counting errors in python/c programs with affine analysis. In: European conference on object-oriented programmings. Springer, pp 80–104 Li S, Tan G (2014) Finding reference-counting errors in python/c programs with affine analysis. In: European conference on object-oriented programmings. Springer, pp 80–104
47.
Zurück zum Zitat Li S, Tan G (2009) Finding bugs in exceptional situations of jni programs. In: Proceedings of the 16th ACM conference on computer and communications security, pp 442–452 Li S, Tan G (2009) Finding bugs in exceptional situations of jni programs. In: Proceedings of the 16th ACM conference on computer and communications security, pp 442–452
48.
Zurück zum Zitat Cousot P (1997) Types as abstract interpretations. In: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on principles of programming languages, pp 316–331 Cousot P (1997) Types as abstract interpretations. In: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on principles of programming languages, pp 316–331
Metadaten
Titel
On multi-language abstraction: Towards a static analysis of multi-language programs
verfasst von
Samuele Buro
Roy Crole
Isabella Mastroeni
Publikationsdatum
28.03.2023
Verlag
Springer US
Erschienen in
Formal Methods in System Design
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-022-00405-8

Premium Partner