Title: PrediPrune: Reducing Verification Overhead in Souper with Machine Learning Driven Pruning Show Chinese title

Title: PrediPrune：通过机器学习驱动的剪枝减少Souper中的验证开销

Abstract: Souper is a powerful enumerative superoptimizer that enhances the runtime performance of programs by optimizing LLVM intermediate representation (IR) code. However, its verification process, which relies on a computationally expensive SMT solver to validate optimization candidates, must explore a large search space. This large search space makes the verification process particularly expensive, increasing the burden to incorporate Souper into compilation tools. We propose PrediPrune, a stochastic candidate pruning strategy that effectively reduces the number of invalid candidates passed to the SMT solver. By utilizing machine learning techniques to predict the validity of candidates based on features extracted from the code, PrediPrune prunes unlikely candidates early, decreasing the verification workload. When combined with the state-of-the-art approach (Dataflow), PrediPrune decreases compilation time by 51% compared to the Baseline and by 12% compared to using only Dataflow, emphasizing the effectiveness of the combined approach that integrates a purely ML-based method (PrediPrune) with a purely non-ML based (Dataflow) method. Additionally, PrediPrune offers a flexible interface to trade-off compilation time and optimization opportunities, allowing end users to adjust the balance according to their needs. Show Chinese abstract

Abstract: Souper是一个强大的枚举超优化器，它通过优化LLVM中间表示（IR）代码来提高程序的运行时性能。 然而，其验证过程依赖于计算成本高昂的SMT求解器来验证优化候选，必须探索一个大的搜索空间。 这个大的搜索空间使得验证过程特别昂贵，增加了将Souper集成到编译工具中的负担。 我们提出了PrediPrune，一种随机候选剪枝策略，能够有效减少传递给SMT求解器的无效候选数量。 通过利用机器学习技术，根据从代码中提取的特征预测候选的有效性，PrediPrune在早期剪枝不太可能的候选，从而减少验证工作量。 当与最先进的方法（Dataflow）结合使用时，PrediPrune相比基线方法将编译时间减少了51%，相比仅使用Dataflow的方法减少了12%，强调了将纯基于机器学习的方法（PrediPrune）与纯非机器学习方法（Dataflow）相结合的组合方法的有效性。 此外，PrediPrune提供了一个灵活的接口，可以在编译时间和优化机会之间进行权衡，允许最终用户根据需要调整平衡。