FMitF: Track II: Cybolic: a symbolic execution technique and tool for analyzing CMake build scripts

CMake is a well-known, platform-independent software build automation tool. When build issues arise, developers often have to manually analyze CMake scripts to determine how files or libraries are built. This manual process is both error-prone and time-consuming. This project will develop Cybolic, a formal method and tool to analyze CMake. The novelties of the project are the automated and scalable algorithms enabling Cybolic to be practical and useful for developers. The project's impacts are that the open-source Cybolic tool will improve the debugging and build process of software relying on CMake and will benefit users who currently have to manually analyze CMake scripts. The project will build the Cybolic as a symbolic execution technique that transforms CMake code into logical formulae representing build conditions, which are mappings of conditions over build options for files and compilation flags. These build conditions can help developers in many tasks, such as finding orphan code sections, files, or compilation options that are never used and determining what patches or code changes affect a compilation configuration. This project will focus on (i) making Cybolic scale to large and complex CMake-based projects, (ii) applying Cybolic to detect real-world build issues, (iii) and integrating Cybolic with popular Integrated Development Environments (IDEs) such as Visual Studio (VS) Code to improve its usability and adoption. The findings from this project will be used in the investigator’s courses and mentoring and outreach activities. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.