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

CMake是一个著名的、平台无关的软件构建自动化工具。当出现构建问题时，开发人员通常必须手动分析CMake脚本以确定如何构建文件或库。这个手动过程既容易出错又耗时。这个项目将开发一个形式化的方法和工具来分析CMake。该项目的新颖之处在于自动化和可扩展的算法，使Cybolic对开发人员实用和有用。该项目的影响是，开源的Cybolic工具将改善依赖CMake的软件的调试和构建过程，并将使目前必须手动分析CMake脚本的用户受益。该项目将把Cybolic作为一种符号执行技术构建，将CMake代码转换为表示构建条件的逻辑公式，构建条件是文件和编译标志的构建选项上的条件映射。这些构建条件可以帮助开发人员完成许多任务，例如查找从未使用过的孤立代码段、文件或编译选项，以及确定哪些补丁或代码更改会影响编译配置。该项目将专注于（i）将Cybolic扩展到大型和复杂的基于CMake的项目，（ii）应用Cybolic来检测现实世界的构建问题，（iii）将Cybolic与流行的集成开发环境（IDE）（如Visual Studio（VS）Code）集成，以提高其可用性和采用率。该项目的研究结果将用于研究人员的课程和指导和推广活动。该奖项反映了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.