Document Open Access Logo

Lifted Static Analysis of Dynamic Program Families by Abstract Interpretation

Authors Aleksandar S. Dimovski , Sven Apel

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2021.14.pdf
  • Filesize: 1.14 MB
  • 28 pages

Document Identifiers

Author Details

Aleksandar S. Dimovski
  • Mother Teresa University, Skopje, North Macedonia
Sven Apel
  • Saarland University, Saarland Informatics Campus, 66123 Saarbrücken, Germany

Cite As Get BibTex

Aleksandar S. Dimovski and Sven Apel. Lifted Static Analysis of Dynamic Program Families by Abstract Interpretation. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 14:1-14:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.ECOOP.2021.14

Abstract

Program families (software product lines) are increasingly adopted by industry for building families of related software systems. A program family offers a set of features (configured options) to control the presence and absence of software functionality. Features in program families are often assigned at compile-time, so their values can only be read at run-time. However, today many program families and application domains demand run-time adaptation, reconfiguration, and post-deployment tuning. Dynamic program families (dynamic software product lines) have emerged as an attempt to handle variability at run-time. Features in dynamic program families can be controlled by ordinary program variables, so reads and writes to them may happen at run-time.
Recently, a decision tree lifted domain for analyzing traditional program families with numerical features has been proposed, in which decision nodes contain linear constraints defined over numerical features and leaf nodes contain analysis properties defined over program variables. Decision nodes partition the configuration space of possible feature values, while leaf nodes provide analysis information corresponding to each partition of the configuration space. As features are statically assigned at compile-time, decision nodes can be added, modified, and deleted only when analyzing read accesses of features. In this work, we extend the decision tree lifted domain so that it can be used to efficiently analyze dynamic program families with numerical features. Since features can now be changed at run-time, decision nodes can be modified when handling read and write accesses of feature variables. For this purpose, we define extended transfer functions for assignments and tests as well as a special widening operator to ensure termination of the lifted analysis. To illustrate the potential of this approach, we have implemented a lifted static analyzer, called DSPLNum²Analyzer, for inferring numerical invariants of dynamic program families written in C. An empirical evaluation on benchmarks from SV-COMP indicates that our tool is effective and provides a flexible way of adjusting the precision/cost ratio in static analysis of dynamic program families.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software product lines
  • Theory of computation → Abstraction
  • Software and its engineering → Software functional properties
Keywords
  • Dynamic program families
  • Static analysis
  • Abstract interpretation
  • Decision tree lifted domain

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Sven Apel, Don S. Batory, Christian Kästner, and Gunter Saake. Feature-Oriented Software Product Lines - Concepts and Implementation. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-37521-7.
  2. Sven Apel, Hendrik Speidel, Philipp Wendler, Alexander von Rhein, and Dirk Beyer. Detection of feature interactions using feature-aware verification. In 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), pages 372-375, 2011. URL: https://doi.org/10.1109/ASE.2011.6100075.
  3. Sven Apel, Alexander von Rhein, Philipp Wendler, Armin Größlinger, and Dirk Beyer. Strategies for product-line verification: case studies and experiments. In 35th International Conference on Software Engineering, ICSE '13, pages 482-491, 2013. URL: https://doi.org/10.1109/ICSE.2013.6606594.
  4. Eric Bodden, Társis Tolêdo, Márcio Ribeiro, Claus Brabrand, Paulo Borba, and Mira Mezini. Spl^lift: statically analyzing software product lines in minutes instead of years. In ACM SIGPLAN Conference on PLDI '13, pages 355-364, 2013. URL: https://doi.org/10.1145/2491956.2491976.
  5. Claus Brabrand, Márcio Ribeiro, Társis Tolêdo, Johnni Winther, and Paulo Borba. Intraprocedural dataflow analysis for software product lines. T. Aspect-Oriented Software Development, 10:73-108, 2013. URL: https://doi.org/10.1007/978-3-642-36964-3_3.
  6. Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. The polyranking principle. In Automata, Languages and Programming, 32nd International Colloquium, ICALP 2005, Lisbon, Portugal, July 11-15, 2005, Proceedings, volume 3580 of LNCS, pages 1349-1361. Springer, 2005. URL: https://doi.org/10.1007/11523468_109.
  7. Rafael Capilla, Jan Bosch, Pablo Trinidad, Antonio Ruiz Cortés, and Mike Hinchey. An overview of dynamic software product line architectures and techniques: Observations from research and industry. J. Syst. Softw., 91:3-23, 2014. URL: https://doi.org/10.1016/j.jss.2013.12.038.
  8. Carlos Cetina, Øystein Haugen, Xiaorui Zhang, Franck Fleurey, and Vicente Pelechano. Strategies for variability transformation at run-time. In Software Product Lines, 13th International Conference, SPLC 2009, Proceedings, volume 446 of ACM International Conference Proceeding Series, pages 61-70. ACM, 2009. URL: https://dl.acm.org/citation.cfm?id=1753245.
  9. Junjie Chen and Patrick Cousot. A binary decision tree abstract domain functor. In Static Analysis - 22nd International Symposium, SAS 2015, Proceedings, volume 9291 of LNCS, pages 36-53. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-48288-9_3.
  10. Andreas Classen, Arnaud Hubaux, and Patrick Heymans. A formal semantics for multi-level staged configuration. In Third International Workshop on Variability Modelling of Software-Intensive Systems, Seville, Spain, January 28-30, 2009. Proceedings, volume 29 of ICB Research Report, pages 51-60. Universität Duisburg-Essen, 2009. URL: http://www.vamos-workshop.net/proceedings/VaMoS_2009_Proceedings.pdf.
  11. Paul Clements and Linda Northrop. Software Product Lines: Practices and Patterns. Addison-Wesley, 2001. Google Scholar
  12. Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, pages 238-252. ACM, 1977. URL: https://doi.org/10.1145/512950.512973.
  13. Patrick Cousot and Radhia Cousot. Comparing the galois connection and widening/narrowing approaches to abstract interpretation. In Programming Language Implementation and Logic Programming, 4th International Symposium, PLILP'92, Proceedings, volume 631 of LNCS, pages 269-295. Springer, 1992. URL: https://doi.org/10.1007/3-540-55844-6_142.
  14. Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. The astreé analyzer. In Programming Languages and Systems, 14th European Symposium on Programming, ESOP 2005, Proceedings, volume 3444 of LNCS, pages 21-30. Springer, 2005. URL: https://doi.org/10.1007/978-3-540-31987-0_3.
  15. Patrick Cousot, Radhia Cousot, and Laurent Mauborgne. A scalable segmented decision tree abstract domain. In Time for Verification, Essays in Memory of Amir Pnueli, volume 6200 of LNCS, pages 72-95. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-13754-9_5.
  16. Patrick Cousot and Nicolas Halbwachs. Automatic discovery of linear restraints among variables of a program. In Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages (POPL'78), pages 84-96. ACM Press, 1978. URL: https://doi.org/10.1145/512760.512770.
  17. Ferruccio Damiani, Luca Padovani, and Ina Schaefer. A formal foundation for dynamic delta-oriented software product lines. In Generative Programming and Component Engineering, GPCE'12, pages 1-10. ACM, 2012. URL: https://doi.org/10.1145/2371401.2371403.
  18. Aleksandar S. Dimovski. Lifted static analysis using a binary decision diagram abstract domain. In Proceedings of the 18th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, GPCE 2019, pages 102-114. ACM, 2019. URL: https://doi.org/10.1145/3357765.3359518.
  19. Aleksandar S. Dimovski. A binary decision diagram lifted domain for analyzing program families. Journal of Computer Languages, 63:101032, 2021. URL: https://doi.org/10.1016/j.cola.2021.101032.
  20. Aleksandar S. Dimovski and Sven Apel. Tool artifact for "lifted static analysis of dynamic program families by abstract interpretation". Zenodo, 2021. URL: https://doi.org/10.5281/zenodo.4718697.
  21. Aleksandar S. Dimovski, Sven Apel, and Axel Legay. A decision tree lifted domain for analyzing program families with numerical features. In Fundamental Approaches to Software Engineering - 24th International Conference, FASE 2021, Proceedings, volume 12649 of LNCS, pages 67-86. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-71500-7_4.
  22. Aleksandar S. Dimovski, Sven Apel, and Axel Legay. Program sketching using lifted analysis for numerical program families. In NASA Formal Methods - 13th International Symposium, NFM 2021, Proceedings, volume 12673 of LNCS. Springer, 2021. Google Scholar
  23. Aleksandar S. Dimovski, Claus Brabrand, and Andrzej Wasowski. Variability abstractions: Trading precision for speed in family-based analyses. In 29th European Conference on Object-Oriented Programming, ECOOP 2015, volume 37 of LIPIcs, pages 247-270. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2015.247.
  24. Aleksandar S. Dimovski and Axel Legay. Computing program reliability using forward-backward precondition analysis and model counting. In Fundamental Approaches to Software Engineering - 23rd International Conference, FASE 2020, Proceedings, volume 12076 of LNCS, pages 182-202. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45234-6_9.
  25. Arie Gurfinkel and Sagar Chaki. Boxes: A symbolic abstract domain of boxes. In Static Analysis - 17th International Symposium, SAS 2010. Proceedings, volume 6337 of LNCS, pages 287-303. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15769-1_18.
  26. Robert J. Hall. Fundamental nonmodularity in electronic mail. Automated Software Engineering, 12(1):41-79, 2005. URL: https://doi.org/10.1023/B:AUSE.0000049208.84702.84.
  27. Svein O. Hallsteinsen, Mike Hinchey, Sooyong Park, and Klaus Schmid. 2nd international workshop on dynamic software product lines DSPL 2008. In Software Product Lines, 12th International Conference, SPLC 2008, Limerick, Ireland, September 8-12, 2008, Proceedings, page 381. IEEE Computer Society, 2008. URL: https://doi.org/10.1109/SPLC.2008.69.
  28. Svein O. Hallsteinsen, Mike Hinchey, Sooyong Park, and Klaus Schmid. Dynamic software product lines. Computer, 41(4):93-95, 2008. URL: https://doi.org/10.1109/MC.2008.123.
  29. Svein O. Hallsteinsen, Erlend Stav, Arnor Solberg, and Jacqueline Floch. Using product line techniques to build adaptive systems. In Software Product Lines, 10th International Conference, SPLC 2006, Baltimore, Maryland, USA, August 21-24, 2006, Proceedings, pages 141-150. IEEE Computer Society, 2006. URL: https://doi.org/10.1109/SPLINE.2006.1691586.
  30. Øystein Haugen, Birger Møller-Pedersen, Jon Oldevik, Gøran K. Olsen, and Andreas Svendsen. Adding standardized variability to domain specific languages. In Software Product Lines, 12th International Conference, SPLC 2008, Proceedings, pages 139-148. IEEE Computer Society, 2008. URL: https://doi.org/10.1109/SPLC.2008.25.
  31. Alexander Helleboogh, Danny Weyns, Klaus Schmid, Tom Holvoet, Kurt Schelfthout, and Wim Van Betsbrugge. Adding variants on-the-fly: Modeling meta-variability in dynamic software product lines. In Synamic Software Product Lines, 3rd International Workshop, SSPL 2009, Proceedings, 2009. Google Scholar
  32. Alexandru F. Iosif-Lazar, Jean Melo, Aleksandar S. Dimovski, Claus Brabrand, and Andrzej Wasowski. Effective analysis of c programs by rewriting variability. Programming Journal, 1(1):1, 2017. URL: https://doi.org/10.22152/programming-journal.org/2017/1/1.
  33. Bertrand Jeannet and Antoine Miné. Apron: A library of numerical abstract domains for static analysis. In Computer Aided Verification, 21st International Conference, CAV 2009. Proceedings, volume 5643 of LNCS, pages 661-667. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02658-4_52.
  34. Christian Kästner. Virtual Separation of Concerns: Toward Preprocessors 2.0. PhD thesis, University of Magdeburg, Germany, May 2010. Google Scholar
  35. Gary A. Kildall. A unified approach to global program optimization. In Conference Record of the ACM Symposium on Principles of Programming Languages, (POPL'73), pages 194-206, 1973. URL: https://doi.org/10.1145/512927.512945.
  36. Jan Midtgaard, Aleksandar S. Dimovski, Claus Brabrand, and Andrzej Wasowski. Systematic derivation of correct variability-aware program analyses. Sci. Comput. Program., 105:145-170, 2015. URL: https://doi.org/10.1016/j.scico.2015.04.005.
  37. Antoine Miné. The octagon abstract domain. Higher-Order and Symbolic Computation, 19(1):31-100, 2006. URL: https://doi.org/10.1007/s10990-006-8609-1.
  38. Antoine Miné. Tutorial on static inference of numeric invariants by abstract interpretation. Foundations and Trends in Programming Languages, 4(3-4):120-372, 2017. URL: https://doi.org/10.1561/2500000034.
  39. David Lorge Parnas. On the design and development of program families. IEEE Trans. Software Eng., 2(1):1-9, 1976. URL: https://doi.org/10.1109/TSE.1976.233797.
  40. Christian Prehofer. Feature-oriented programming: A fresh look at objects. In ECOOP'97 - Object-Oriented Programming, 11th European Conference, 1997, Proceedings, volume 1241 of LNCS, pages 419-443. Springer, 1997. URL: https://doi.org/10.1007/BFb0053389.
  41. Marko Rosenmüller, Norbert Siegmund, Sven Apel, and Gunter Saake. Flexible feature binding in software product lines. Autom. Softw. Eng., 18(2):163-197, 2011. URL: https://doi.org/10.1007/s10515-011-0080-5.
  42. Marko Rosenmüller, Norbert Siegmund, Mario Pukall, and Sven Apel. Tailoring dynamic software product lines. In Generative Programming And Component Engineering, Proceedings of the 10th International Conference on Generative Programming and Component Engineering, GPCE 2011, pages 3-12. ACM, 2011. URL: https://doi.org/10.1145/2047862.2047866.
  43. Ina Schaefer, Lorenzo Bettini, Viviana Bono, Ferruccio Damiani, and Nico Tanzarella. Delta-oriented programming of software product lines. In Software Product Lines: Going Beyond - 14th International Conference, SPLC 2010. Proceedings, volume 6287 of LNCS, pages 77-91. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15579-6_6.
  44. Gagandeep Singh, Markus Püschel, and Martin T. Vechev. Making numerical program analysis fast. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015, pages 303-313. ACM, 2015. URL: https://doi.org/10.1145/2737924.2738000.
  45. Caterina Urban. Static Analysis by Abstract Interpretation of Functional Temporal Properties of Programs. PhD thesis, École Normale Supérieure, Paris, France, 2015. URL: https://tel.archives-ouvertes.fr/tel-01176641.
  46. Caterina Urban and Antoine Miné. A decision tree abstract domain for proving conditional termination. In Static Analysis - 21st International Symposium, SAS 2014. Proceedings, volume 8723 of LNCS, pages 302-318. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-10936-7_19.
  47. Alexander von Rhein, Jörg Liebig, Andreas Janker, Christian Kästner, and Sven Apel. Variability-aware static analysis at scale: An empirical study. ACM Trans. Softw. Eng. Methodol., 27(4):18:1-18:33, 2018. URL: https://doi.org/10.1145/3280986.
  48. Alexander von Rhein, Thomas Thüm, Ina Schaefer, Jörg Liebig, and Sven Apel. Variability encoding: From compile-time to load-time variability. J. Log. Algebraic Methods Program., 85(1):125-145, 2016. URL: https://doi.org/10.1016/j.jlamp.2015.06.007.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact