Data-flow analysis for interrupt-driven microcontroller software

Enhancing traditional data-flow analysis with new techniques for dealing with concurrency and volatile data provides significant additional precision on interrupt-driven microcontroller code. This dissertation presents a whole-program analysis for C code that generalizes and extends traditional abstract interpretation techniques. Interatomic concurrent data-flow (ICD), a novel technique, allows the analysis to understand interrupt-driven concurrent control flow and increase the amount of trackable shared data. The analysis leverages system information to track data through volatile variables when safe to do so. Several subanalyses concurrently run inside the main analysis in order to further increase their precision through synergy. The analysis supports "conditional X propagation," a generalization of the well-known conditional constant propagation algorithm where X is a supplied abstract value domain. The main contributions of this dissertation are a presentation of new data-flow analysis techniques, an implementation description (cXprop), and evaluations of the new techniques.;Three examples illustrate the utility of the new techniques in the analysis. First, cXprop reduces microcontroller code size by an average of 12%, static data size by an average of 2.5%, estimated dynamic data size by an average 1.8%, and duty cycle by an average of 8.3%. Second, a platform for introducing memory safety to legacy microcontroller applications utilizes cXprop as a race detector and whole-program optimizer. CXprop enables the platform to be sound in the presence of interrupt-driven concurrency and practical on tiny microcontroller-based systems. Third, an extension of cXprop performs offline compression for on-chip RAM. The analysis provides information about limited bitwidth use for statically allocated global variables. A transformation then reduces the variables to the limited bitwidth, resulting in an average savings of 22% RAM.