fix: prevent duplicate module initialization in C codegen

[iyassou]

This PR fixes a bug in the C code generator where importing the same module through multiple paths or with different visibility/meta flags caused it to be initialized multiple times at runtime. Previously these duplicate imports resulted in redundant C declarations and repeated initialization calls within the same function body. By deduplicating the list of initialization functions during the emission phase, the compiler now guarantees exactly one initialization call per module per phase. A regression test has been added to the module test suite to verify the absence of both duplicate C declarations and duplicate initialization calls within individual function scopes.

Context

I stumbled onto this while working through Functional Programming in Lean. I noticed identical lines and blocks of code in some .lake/build/ir/*.c files when working with modules and traced this to a lack of deduplication between the function declarations and bodies during the C emission phase.

Bug

When a module is imported via different visibility/meta flags the compiler would emit redundant declarations, and identical initialization calls in the same function scope. Steps to reproduce:

#!/usr/bin/env bash
lake new bug lib
cd bug
cat > Bug/Basic.lean << 'EOF'
module
def foo := "bar"
EOF
cat > Bug.lean << 'EOF'
module
import Bug.Basic  
meta import Bug.Basic  
EOF
lake build

.lake/build/ir/Bug.c with duplicates highlighted

(expand/collapse)

// Lean compiler output
// Module: Bug
// Imports: public import Init public meta import Init import Bug.Basic meta import Bug.Basic
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
#ifdef __cplusplus
extern "C" {
#endif
lean_object* runtime_initialize_Init(uint8_t builtin);          // <-------------------------------
lean_object* runtime_initialize_bug_Bug_Basic(uint8_t builtin); // <-------------------------------
static bool _G_runtime_initialized = false;
LEAN_EXPORT lean_object* runtime_initialize_bug_Bug(uint8_t builtin) {
lean_object * res;
if (_G_runtime_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_runtime_initialized = true;
res = runtime_initialize_Init(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_bug_Bug_Basic(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
lean_object* runtime_initialize_Init(uint8_t builtin);          // <-------------------------------
lean_object* runtime_initialize_bug_Bug_Basic(uint8_t builtin); // <-------------------------------
static bool _G_meta_initialized = false;
LEAN_EXPORT lean_object* meta_initialize_bug_Bug(uint8_t builtin) {
lean_object * res;
if (_G_meta_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_meta_initialized = true;
res = runtime_initialize_Init(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = runtime_initialize_bug_Bug_Basic(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
lean_object* initialize_Init(uint8_t builtin);          // < - - - - - - - - - - - - - - - - - - -
lean_object* initialize_Init(uint8_t builtin);          // < - - - - - - - - - - - - - - - - - - -
lean_object* initialize_bug_Bug_Basic(uint8_t builtin); // < - - - - - - - - - - - - - - - - - - -
lean_object* initialize_bug_Bug_Basic(uint8_t builtin); // < - - - - - - - - - - - - - - - - - - -
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_bug_Bug(uint8_t builtin) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init(builtin);               // < ===============================================
if (lean_io_result_is_error(res)) return res; // < ===============================================
lean_dec_ref(res);                            // < ===============================================
res = initialize_Init(builtin);               // < * * * * * * * * * * * * * * * * * * * * * * * *
if (lean_io_result_is_error(res)) return res; // < * * * * * * * * * * * * * * * * * * * * * * * *
lean_dec_ref(res);                            // < * * * * * * * * * * * * * * * * * * * * * * * *
res = initialize_bug_Bug_Basic(builtin);      // < ===============================================
if (lean_io_result_is_error(res)) return res; // < ===============================================
lean_dec_ref(res);                            // < ===============================================
res = initialize_bug_Bug_Basic(builtin);      // < * * * * * * * * * * * * * * * * * * * * * * * *
if (lean_io_result_is_error(res)) return res; // < * * * * * * * * * * * * * * * * * * * * * * * *
lean_dec_ref(res);                            // < * * * * * * * * * * * * * * * * * * * * * * * *
res = runtime_initialize_bug_Bug(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = meta_initialize_bug_Bug(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return initialize_bug_Bug(builtin);
}
#ifdef __cplusplus
}
#endif

.lake/build/ir/Bug/Basic.c with duplicates highlighted:

(expand/collapse)

// Lean compiler output
// Module: Bug.Basic
// Imports: public import Init public meta import Init
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
#ifdef __cplusplus
extern "C" {
#endif
static const lean_string_object lp_bug___private_Bug_Basic_0__foo___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 4, .m_capacity = 4, .m_length = 3, .m_data = "bar"};
static const lean_object* lp_bug___private_Bug_Basic_0__foo___closed__0 = (const lean_object*)&lp_bug___private_Bug_Basic_0__foo___closed__0_value;
LEAN_EXPORT const lean_object* lp_bug___private_Bug_Basic_0__foo = (const lean_object*)&lp_bug___private_Bug_Basic_0__foo___closed__0_value;
lean_object* runtime_initialize_Init(uint8_t builtin); // <----------------------------------------
static bool _G_runtime_initialized = false;
LEAN_EXPORT lean_object* runtime_initialize_bug_Bug_Basic(uint8_t builtin) {
lean_object * res;
if (_G_runtime_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_runtime_initialized = true;
res = runtime_initialize_Init(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
lean_object* runtime_initialize_Init(uint8_t builtin); // <----------------------------------------
static bool _G_meta_initialized = false;
LEAN_EXPORT lean_object* meta_initialize_bug_Bug_Basic(uint8_t builtin) {
lean_object * res;
if (_G_meta_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_meta_initialized = true;
res = runtime_initialize_Init(builtin);
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
lean_object* initialize_Init(uint8_t builtin); // < - - - - - - - - - - - - - - - - - - - - - - - -
lean_object* initialize_Init(uint8_t builtin); // < - - - - - - - - - - - - - - - - - - - - - - - -
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_bug_Bug_Basic(uint8_t builtin) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init(builtin);                  // < =============================================
if (lean_io_result_is_error(res)) return res;    // < =============================================
lean_dec_ref(res);                               // < =============================================
res = initialize_Init(builtin);                  // < * * * * * * * * * * * * * * * * * * * * * * *
if (lean_io_result_is_error(res)) return res;    // < * * * * * * * * * * * * * * * * * * * * * * *
lean_dec_ref(res);                               // < * * * * * * * * * * * * * * * * * * * * * * *
res = runtime_initialize_bug_Bug_Basic(builtin); // < =============================================
if (lean_io_result_is_error(res)) return res;    // < =============================================
lean_dec_ref(res);                               // < =============================================
res = meta_initialize_bug_Bug_Basic(builtin);    // < * * * * * * * * * * * * * * * * * * * * * * *
if (lean_io_result_is_error(res)) return res;    // < * * * * * * * * * * * * * * * * * * * * * * *
lean_dec_ref(res);                               // < * * * * * * * * * * * * * * * * * * * * * * *
return initialize_bug_Bug_Basic(builtin);
}
#ifdef __cplusplus
}
#endif

Cause

src/Lean/Compiler/LCNF/EmitC.lean generates the C code. Its main:

def main : EmitM Unit := do
  emitFileHeader
  emitFnDecls
  emitFns
  if (← getEnv).header.isModule then
    emitInitFn (phases := .runtime)
    emitInitFn (phases := .comptime)
    emitLegacyInitFn
  else
    emitInitFn (phases := .all)
  emitMainFnIfNeeded
  emitFileFooter

and emitInitFn:

def emitInitFn (phases : IRPhases) : EmitM Unit := do
  let env ← getEnv
  let impInitFns ← env.imports.filterMapM fun imp => do
    if phases != .all && imp.isMeta != (phases == .comptime) then
      return none
    let some idx := env.getModuleIdx? imp.module
      | throwError "(internal) import without module index" -- should be unreachable
    let pkg? := env.getModulePackageByIdx? idx
    let fn := mkModuleInitializationFunctionName (phases := if phases == .all then .all else if imp.isMeta then .runtime else phases) imp.module pkg?
    emitLn s!"lean_object* {fn}(uint8_t builtin);"
    return some fn
  -- [...]
  impInitFns.forM fun fn => do
    -- [...]

The uniqueness of the elements of env.imports isn't checked, and since module identity is determined by name as shown by env.getModuleIdx?

def getModuleIdx? (env : Environment) (moduleName : Name) : Option ModuleIdx :=
  env.header.moduleName2Idx[moduleName]?

this results in impInitFns potentially containing duplicate module names, and therefore multiple initializations being emitted within a function's body. The same issue occurs in emitLegacyInitFn:

def emitLegacyInitFn : EmitM Unit := do
  let env ← getEnv
  let impInitFns ← env.imports.filterMapM fun imp => do
    let some idx := env.getModuleIdx? imp.module
      | throwError "(internal) import without module index" -- should be unreachable
    let pkg? := env.getModulePackageByIdx? idx
    let fn := mkModuleInitializationFunctionName imp.module pkg?
    emitLn s!"lean_object* {fn}(uint8_t builtin);"
    return some fn
  -- [...]
  impInitFns.forM fun fn => do
    - [...]

The duplicate declarations outside of function bodies occur because the calls to emitInitFn and emitLegacyInitFn in main don't share their work.

Proposed Fix

• Separating the emission of declarations and function bodies from the collection of the latter.
• Deduplicating the joint collection of declarations.
• Removing duplicates from impInitFns before emitting.

Implementation Notes

The factored getInitFn uses List.eraseDups to eliminate duplicates, and so does the new main function:

def getInitFns (phases : IRPhases) : EmitM (List String) := do
  let env ← getEnv
  let impInitFns ← env.imports.filterMapM fun imp => do
    if phases != .all && imp.isMeta != (phases == .comptime) then
      return none
    let some idx := env.getModuleIdx? imp.module
      | throwError "(internal) import without module index" -- should be unreachable
    let pkg? := env.getModulePackageByIdx? idx
    let fn := mkModuleInitializationFunctionName (phases := if phases == .all then .all else if imp.isMeta then .runtime else phases) imp.module pkg?
    return some fn
  -- The same module may appear multiple times in `env.imports` with different visibility/meta
  -- flags. The C initialisation function however corresponds to the module itself, so each module
  -- should be initialised at most once.
  return impInitFns.toList.eraseDups

-- [...]

def main : EmitM Unit := do
  emitFileHeader
  emitFnDecls
  emitFns
  if (← getEnv).header.isModule then
    let runtimeInitFns ← getInitFns (phases := .runtime)
    let comptimeInitFns ← getInitFns (phases := .comptime)
    let legacyInitFns ← getInitFns (phases := .all)
    let allInitFns := (runtimeInitFns ++ comptimeInitFns ++ legacyInitFns).eraseDups
    emitInitFnDecls allInitFns
    emitInitFnBody (phases := .runtime) runtimeInitFns
    emitInitFnBody (phases := .comptime) comptimeInitFns
    emitLegacyInitFnBody legacyInitFns
  else
    let initFns ← getInitFns (phases := .all)
    emitInitFnDecls initFns
    emitInitFnBody (phases := .all) initFns
  emitMainFnIfNeeded
  emitFileFooter

I initially used an Std.HashSet for the deduplication since List.eraseDups is $O(N^2)$. I switched to the latter because the former makes the order of emitted C code non-deterministic, and because after examining env.imports.size across the entire test suite (4215 tests at the time of writing), $N$ is on the smaller side:

I'm not entirely sure how this compares to real-world Lean usage, so would appreciate feedback on that front.

The data was obtained by modifying EmitC.lean::emitCForDecls:

public def emitCForDecls (modName : Name) (decls : Array Name) : CoreM String := do
  let (localDecls, otherModuleDecls) ← collectUsedDecls decls
  let env ← getEnv
  -- // <mod>
  let timestamp ← IO.monoMsNow
  let logFile : System.FilePath := "/path/to/imports.log"
  let handle ← IO.FS.Handle.mk logFile IO.FS.Mode.append
  handle.putStrLn s!"[{timestamp}] ({modName} : {env.imports.size})"
  -- // </mod>
  let indexMap := getImpureDeclIndices env decls
  let localDecls := localDecls.qsort fun l r => indexMap[l.name]! < indexMap[r.name]!
  let (_, { buf, .. }) ←
    main
      |>.run { localDecls, otherModuleDecls, modName }
      |>.run {}
      |>.run (phase := .impure)
  return buf

Testing

I added a regression test to tests/lake/tests/module/test.sh that reuses the existing PromoteImport and PromoteMetaImport modules to assert that no duplicate C declarations exist, and that no duplicate res = ... initialization calls exist within the same C function body using awk. Crucially, all pre-existing tests still pass.

Notes

• I didn't notice any significant or measurable performance changes when running the whole test suite: both the old and dedup-ed versions ran in practically identical times.
• I noticed that the legacy initialization function emits C code that calls itself at the very end. There's a static bool guard that prevents infinite recursion, but I'm confused by the need for the recursive call in the first place. Does anybody know why it's there?

[iyassou]

awaiting-review