Skip to content

inline_functions reverts when the CALLER contains an imported-function call (by-body modeling has no body for imports) — v1.1.4 #153

@avrabe

Description

@avrabe

Summary

On loom v1.1.4 (cc66f398, after #151), inline_functions now correctly inlines i64 callees (thanks!) — but it reverts the inline whenever the caller contains a call to an imported function. The by-body call modeling introduced in #151 has no body for an import, so verification of the surrounding inline fails and the whole inline is reverted.

This blocks the gale C↔Rust seam dissolution: z_impl_k_sem_give inlines gale_k_sem_give_decide but also calls 5 env:: kernel imports (k_spin_lock, z_unpend_first_thread, arch_thread_return_value_set, z_ready_thread, z_reschedule), so the inline is always reverted.

Reproduction — the import call is the trigger (not i64/u64)

Reverts — caller has an imported call + inlines an i64-returning local callee:

(module
  (import "env" "ext" (func $ext))
  (func $dec (param i32) (result i64) (i64.extend_i32_u (local.get 0)))
  (func $z (export "z") (param i32) (result i64)
    (call $ext)                       ;; <-- imported call in the caller
    (call $dec (local.get 0))))
loom optimize v1.wat --passes inline --stats
  (no effect: inline)
🔁 Verification Reverts:  inline_functions  1 reverted

Inlines fine — same i64 work, no imported call (even with u64 pack/unpack):

(module
  (func $dec (param i32 i32) (result i64)
    (i64.or (i64.extend_i32_u (local.get 0))
            (i64.shl (i64.extend_i32_u (local.get 1)) (i64.const 32))))
  (func $z (export "z") (param i32) (result i32)
    (local $r i64)
    (local.set $r (call $dec (local.get 0) (i32.const 5)))
    (i32.wrap_i64 (i64.shr_u (local.get $r) (i64.const 32)))))
Instructions: 15 → 23   ✅ Optimization complete!   (inlined, no revert)

Trivial i64 (add1) also inlines now. The differentiator is solely the imported call in the caller. Real case: merged.both.wasm (WAT in synth#167 gist) reverts identically.

Ask

Model an imported call as an opaque/uninterpreted effect (a fresh unconstrained result + a havoc of observable state) in the by-body verification, rather than requiring a body — so the inline of other functions in the same caller can still be proven and kept. Without this, the verified inliner can't optimize any function that calls into the host (i.e., essentially every kernel primitive), and the LTO-parity seam dissolution stays closed.

Environment

  • loom v1.1.4 (cc66f398), --passes inline
  • imported-call repro above; real case = merged.both.wasm

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugSomething isn't working

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions