runtimeverification / runtimeverification/mir-semantics

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

Open
#667 0 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Dominant language
Python
Stars
52
Forks
5
PR merge metrics
No merged PRs in 30d

Description

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.

Contributor guide

No contributing guide indexed for this repository

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Research direction

Start in kmir/src/kmir/kdist/mir-semantics/kmir.md at the getBlocksAux(IntrinsicFunction(_)) rule around line 421. Inspect how IntrinsicFunction and regular function bodies are represented, then determine how bodyless and body-bearing intrinsics should be distinguished. Done means both cases are handled without breaking the existing empty-list behavior for intrinsics with no body.

Written by the indexing model from the issue text.

Assessment

Tech stack
rust
Domain
compilers
Issue type
Bug
Difficulty
4/5
Estimated time
3-5 days
Activity status
Stale
Clarity
Mostly clear
Newbie friendliness
42/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.