Proposal: Introduce a Low-Level Intermediate Representation (LLIR) for CertiCoq

[zoep]

Problem

Currently, adding new backends to CertiCoq is not scalable because each backend requires duplicating low-level translation efforts. This results in:

• Redundant work across different backend implementations.
• Increased complexity in maintaining and verifying multiple translations.

Proposal

To address this, we propose designing a dedicated low-level intermediate representation (LLIR). By introducing LLIR, we can streamline new backend development.

• Instead of each backend handling low-level translation independently, we introduce a single translation pass from λANF to LLIR.
• Backend-specific translations will be reduced to simpler transformations from LLIR to target languages (Clight, WebAssembly, LLVM, etc.). These transformations will be easier to implement, optimize, and formally verify.

Characteristics of LLIR

The exact design of LLIR is under discussion, but it will likely be an imperative, low-level intermediate representation (IR) that remains backend-agnostic. Key characteristics include:

• Variables
  Register-like variable accesses (likely in SSA form)

• Control Flow
  Support for function and procedure calls (direct and indirect). Some forms of structured control flow (if-then-else, switch blocks)

• Data Types
  Primitive types based on machine words.

• Memory Model
  Explicit use of the memory.