Skip to content

Some intrinsics may have bodies - update semantics to handle this case #667

@Stevengre

Description

@Stevengre

Description

Currently, the K semantics assumes that intrinsic functions have no body, as seen in
kmir/src/kmir/kdist/mir-semantics/kmir.md:421:

  rule #getBlocksAux(IntrinsicFunction(_)) => .List // intrinsics have no body

However, this assumption may not always be true. As noted by @dkcumming, some intrinsics can have bodies in Rust's SMIR
representation. The semantics should be updated to handle both cases:

  1. Intrinsics without bodies (current assumption)
  2. Intrinsics with bodies (edge case that has been encountered before)

Current Behavior

The semantics unconditionally returns an empty list for IntrinsicFunction items when getting blocks, which would fail if an
intrinsic actually has a body.

Expected Behavior

The semantics should check whether an intrinsic has a body and handle both cases appropriately:

  • If no body: return .List (current behavior)
  • If body exists: process the body blocks normally

Possible Solution

Consider modifying the rule to check for body existence, potentially:

  1. Add body information to the IntrinsicFunction constructor
  2. Or have a separate handling path for intrinsics with bodies
  3. Or unify the handling with regular functions when a body is present

Context

Priority

Medium - This is a correctness issue that could cause failures when encountering intrinsics with bodies, though it may not be
common.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions