License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2021.14
URN: urn:nbn:de:0030-drops-140572
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14057/
Dimovski, Aleksandar S. ;
Apel, Sven
Lifted Static Analysis of Dynamic Program Families by Abstract Interpretation
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.
BibTeX - Entry
@InProceedings{dimovski_et_al:LIPIcs.ECOOP.2021.14,
author = {Dimovski, Aleksandar S. and Apel, Sven},
title = {{Lifted Static Analysis of Dynamic Program Families by Abstract Interpretation}},
booktitle = {35th European Conference on Object-Oriented Programming (ECOOP 2021)},
pages = {14:1--14:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-190-0},
ISSN = {1868-8969},
year = {2021},
volume = {194},
editor = {M{\o}ller, Anders and Sridharan, Manu},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/14057},
URN = {urn:nbn:de:0030-drops-140572},
doi = {10.4230/LIPIcs.ECOOP.2021.14},
annote = {Keywords: Dynamic program families, Static analysis, Abstract interpretation, Decision tree lifted domain}
}
|
Keywords: |
|
Dynamic program families, Static analysis, Abstract interpretation, Decision tree lifted domain |
|
Collection: |
|
35th European Conference on Object-Oriented Programming (ECOOP 2021) |
|
Issue Date: |
|
2021 |
|
Date of publication: |
|
06.07.2021 |
|
Supplementary Material: |
|
Software (ECOOP 2021 Artifact Evaluation approved artifact): https://doi.org/10.4230/DARTS.7.2.6 |
