Filtering equivalent changes from dependency updates with CBMC

Sammanfattning: Background. Open source dependencies have become ubiquitous in software development and the risk of regressions during an update are a key concern facing developers. Change impact analysis (CIA) can be used to assess the effects of a dependency update and aid in addressing this challenge. The manual effort required for CIA has created a need to reduce the amount of data that is considered during a compatibility assessment. Formal (mathematical) methods for equivalence analysis have been prolific in previous attempts at minimizing the amount of data that needs to be analyzed. C bounded model checker (CBMC) is an established tool that can perform equivalence verification and a gap in knowledge exists regarding its usefulness for assessing update compatibility. Objectives. The objective of the study was to evaluate how well CBMC could filter out equivalent changes from impact assessments and the relevance of this for dependency updates. A tool named Equivalent update filter (EUF) was developed in the study to tackle this problem. Effectiveness of the tool was assessed based on, (1) the size of reductions that were made possible through filtering, (2) the relevance of the auto-generated verification resources created to perform analysis and (3) the correctness of the results during equivalence analysis. Methods. To assess the reduction capabilities of EUF a controlled experiment regarding the effect of CBMC based equivalence analysis upon impact assessment sizes was conducted. Updates for the experiment were derived from random commit pairs among three C dependencies with established industry use. The relevance of EUF's auto-generated verification resources were measured through an ordinal scale that highlighted the prevalence of different properties in a dependency that would prevent sound equivalence analysis. Soundness of the reductions suggested by EUF was investigated through a comparison with a manually labeled set of updates. Results. The developed filtering approach was able decrease impact assessment sizes by 1 % on average. Considerable differences were observed between the dependencies in the study in regards to analysis time. For each update, 11 % of the auto-generated verification resources were found to be useful for equivalence analysis on average.EUF's classification of equivalent changes was measured to have an accuracy of 67 % in relation to the base truth of manually labeled updates. Conclusions. The study showed that EUF and by extension, CBMC based equivalence analysis, has potential to be useful in dependency compatibility assessments. Follow up studies on different verification engines and with improved methodologies would be necessary to motivate practical use.