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

CMake是一款知名的、独立于平台的软件构建自动化工具。当出现构建问题时，开发人员通常必须手动分析CMake脚本以确定如何构建文件或库。这种手动过程既容易出错，又耗时。该项目将开发Cybolic，这是一种分析CMake的正式方法和工具。该项目的新奇之处在于自动化和可扩展的算法，使Cybolic对开发人员来说是实用和有用的。该项目的影响是，开源Cybolic工具将改进依赖CMake的软件的调试和构建过程，并将使目前必须手动分析CMake脚本的用户受益。该项目将把Cybolic构建为一种符号执行技术，将CMake代码转换为表示构建条件的逻辑公式，这些条件是文件和编译标志的构建选项上的映射。这些生成条件可以帮助开发人员执行许多任务，例如查找从未使用过的孤立代码节、文件或编译选项，以及确定哪些修补程序或代码更改会影响编译配置。该项目将专注于(I)将Cybolic应用到基于CMake的大型复杂项目中，(Ii)应用Cybolic来检测真实世界的构建问题，(Iii)将Cybolic与流行的集成开发环境(IDE)(如Visual Studio(VS)代码)集成，以提高其可用性和采用率。这个项目的发现将被用于研究人员的课程和指导和推广活动。这个奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

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.