将线性运动G代码形式化，用于制造工具的不变性检测和差分测试

《Proceedings of the ACM on Programming Languages》：Formalizing Linear Motion G-Code for Invariant Checking and Differential Testing of Fabrication Tools

3D打印流程类比编译器，提出将G代码映射为立方体集合并转换为近似点云的新算法，用于检测切片错误、比较不同切片器效果及评估网格修复工具，在58个真实模型测试中验证有效。

　　

摘要

3D打印的计算制造流程类似于编译器：用户使用计算机辅助设计（CAD）工具设计模型，这些模型会被转换为多边形网格，最终由3D切片软件编译成机器代码。对于传统的编译器和编程语言，已经建立了检查程序不变性的技术。同样，差分测试等方法也常用于发现编译器本身的错误，从而提高其可靠性。

制造流程也可以从类似的技术中受益，但传统方法并不直接适用于该领域使用的表示形式。与传统程序不同，3D模型既以几何对象（如CAD模型或多边形网格）的形式存在，也以最终在硬件上运行的机器代码的形式存在。与传统编译过程一样，机器代码受到许多因素的影响，例如模型本身、所使用的切片软件以及众多用户可配置的参数，这些参数控制着切片过程。

在这项工作中，我们提出了一种新的算法，用于将G代码（许多制造流程中常用的语言）转换为一组长方体，并为这些长方体定义一种近似点云表示形式，以便高效地进行操作。我们的算法开辟了新的应用场景：我们展示了三个用例，说明了它如何实现（1）通过不变性检查定位CAD模型中的错误；（2）在不同切片软件之间进行定量比较；（3）评估网格修复工具的有效性。我们在一个名为GlitchFinder的工具中实现了该算法的原型，并在58个真实的CAD模型上对其进行了测试。测试结果表明，GlitchFinder在识别由微小特征引起的切片问题方面特别有效，能够突出显示常用切片软件（如Cura和PrusaSlicer）对同一模型进行切片时的差异，并能发现网格修复工具（如MeshLab和Meshmixer）在修复过程中引入新错误的情况。