Title: The CoCompiler: DSL Lifting via Relational Compilation Show Chinese title

Title: CoCompiler：通过关系编译的DSL提升

Abstract: Lifting low-level or legacy code into a domain-specific language (DSL) improves our ability to understand it, enables deeper formal reasoning, and facilitates safe modification. We present the CoCompiler, a bidirectional compiler and lifter between C and Lustre, a synchronous dataflow language used for reactive systems. The key insight behind the CoCompiler is that writing a compiler as a relation, rather than as a traditional function, yields a DSL lifter "for free". We implement this idea by rewriting the verified Lustre-to-C compiler V\'elus in the Walrus relational programming language. This solves what we call the vertical lifting problem, translating canonical C into Lustre. To address the complementary horizontal problem-handling real-world C outside the compiler's image-we apply semantic-preserving canonicalization passes in Haskell. The resulting tool, the CoCompiler, supports lifting real reactive C code into Lustre and onward into graphical behavioral models. Our approach is modular, language-agnostic, and fast to implement, demonstrating that relational programming offers a practical foundation for building DSL lifters by repurposing existing compilers. Show Chinese abstract

Abstract: 将低级或遗留代码提升到领域特定语言（DSL）可以提高我们对其的理解能力，使更深入的形式推理成为可能，并促进安全修改。 我们提出了CoCompiler，一个在C语言和Lustre之间的双向编译器和提升器，Lustre是一种用于反应式系统的同步数据流语言。 CoCompiler的关键见解是，将编译器编写为关系而非传统函数，可以“免费”获得DSL提升器。 我们通过在Walrus关系编程语言中重写经过验证的Lustre到C的编译器Vélus来实现这一想法。 这解决了我们称之为垂直提升问题的问题，即将标准C翻译成Lustre。 为了处理互补的水平问题——处理编译器图像之外的真实世界C代码——我们在Haskell中应用保持语义的标准转换过程。 由此产生的工具CoCompiler支持将真实的反应式C代码提升到Lustre，并进一步提升到图形化行为模型。 我们的方法是模块化的、与语言无关的，并且易于快速实现，证明了关系编程通过重新利用现有编译器为构建DSL提升器提供了实用的基础。