Implement std::hint::black_box intrinsic support in KMIR by Stevengre · Pull Request #659 · runtimeverification/mir-semantics

Stevengre · 2025-08-21T10:42:05Z

This PR implements support for Rust intrinsic functions in the MIR semantics, starting with the black_box intrinsic. Intrinsic functions are compiler built-ins that don't have regular MIR bodies and require special handling in the formal semantics.

Key Changes

Core Implementation

Python Layer (kmir.py, smir.py):
- Extended functions() method to recognize and handle intrinsic functions from SMIR
- Added mapping of intrinsic symbols to IntrinsicFunction K terms
- Intrinsics are identified by IntrinsicSym in the function symbols

K Semantics

mono.md: Added IntrinsicFunction(Symbol) constructor to MonoItemKind
kmir.md:
- Added special execution path for intrinsic functions that bypasses normal call setup
- Implemented #execIntrinsic mechanism for direct intrinsic execution
- Added black_box implementation as identity function

Testing & Documentation

Added comprehensive test suite for intrinsic functions
Created developer documentation:
- docs/dev/adding-intrinsics.md: Guide for adding new intrinsic support
Added test utilities for SMIR generation and parsing
Included integration tests demonstrating black_box usage

Implementation Details

The intrinsic function support follows this flow:

SMIR parser identifies functions with IntrinsicSym symbols
Python layer creates IntrinsicFunction K terms for these functions
K semantics intercepts intrinsic calls and routes them to #execIntrinsic
Each intrinsic has its own execution rule (currently only black_box)

Future Work

This PR establishes the foundation for supporting additional Rust intrinsics. The modular design makes it straightforward to add new intrinsics by:

Adding execution rules in kmir.md
Writing corresponding tests in tests/rust/intrinsic/
Following the patterns established in this PR

The test infrastructure refactoring also provides a solid foundation for expanding test coverage across the entire MIR semantics implementation.

This commit introduces a new test file `intrinsic-blackbox.rs` that demonstrates the use of `std::hint::black_box` to prevent compiler optimizations on the `add_one` function. The test asserts that the function correctly returns the expected value when wrapped in `black_box`, ensuring its execution is preserved during optimization.

This commit introduces a new Makefile target `generate-tests-smir` for generating SMIR JSON files from Rust source files located in the `tests/rust/` directory. It also adds a `clean-tests-smir` target to remove generated files and a `regenerate-tests-smir` target to clean and regenerate all SMIR JSON files. Additionally, new utility functions in `utils.py` facilitate the retrieval of test files and expected output paths for testing. A new test file `test_smir.py` is added to validate the `function_symbols_reverse` functionality using the generated SMIR JSON data. The README is updated to include instructions for adding new tests and using the Makefile targets.

This commit refactors the test utilities in `utils.py` by adding a new function `filter_test_files` to filter test files based on regex patterns. It also updates the `get_test_files` function for improved readability. In `test_smir.py`, the test structure is modified to utilize the new filtering function, allowing for more flexible test parameterization. The `_test_smir_property` function is introduced to streamline the testing of SMIR properties, enhancing code maintainability and clarity.

This commit refactors the `_make_function_map` method in the `KMIR` class to return a dictionary of function types and their corresponding bodies, improving clarity and usability. The method is renamed to `functions` to better reflect its purpose. Additionally, a new private method `_make_function_map` is introduced to facilitate the mapping of types to their bodies using the refactored `functions` method. In `SMIRInfo`, the `function_symbols_reverse` method is updated to ensure it correctly handles symbols with multiple types, enhancing robustness. New integration and unit tests are added to validate the functionality of the refactored methods using actual SMIR JSON data, ensuring comprehensive coverage and correctness.

- Add IntrinsicFunction(MIRString) variant to MonoItemKind syntax - This enables representation of compiler intrinsic functions in K semantics - Required for implementing std::hint::black_box and other intrinsics 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

- Enhance _make_function_map to handle IntrinsicSym entries - Automatically detect and map intrinsic functions from SMIR data - Create IntrinsicFunction entries for functions with IntrinsicSym - Enables Python layer to properly recognize compiler intrinsics 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

- Add #getBlocksAux rule for IntrinsicFunction pattern matching - Implement #setUpCalleeData rule for intrinsic function calls - Add #execIntrinsic syntax and infrastructure for intrinsic execution - Implement std::hint::black_box as identity function - Add comprehensive documentation section for intrinsic functions - Support bypassing normal function call setup for intrinsics 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

- Add all tests from /tests directory to EXEC_DATA - Include blackbox.rs intrinsic test in integration testing - Use TEST_FILES from utils for comprehensive test coverage - Enable automated testing of std::hint::black_box implementation 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

- Add comprehensive execution state for black_box test case - Shows successful intrinsic execution with value 11 passed through - Validates black_box identity function semantics - Ensures test regression detection for intrinsic functionality 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

- Add CLAUDE.md with essential project setup instructions - Include documentation about reading docs/ before actions - Specify file update requirements for docs/ - Add git commit guidelines for state preservation - Establish coding standards and best practices 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

- Fix flake8 B907: Use !r conversion flag for string formatting - Apply black formatting to Python files 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

- Create docs/dev/ directory for developer guides - Add comprehensive guide for adding new intrinsics with correct workflow - Add testing guide with common commands and patterns - Document the iterative development process for intrinsic implementation - Include examples and expected behavior patterns 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

…tion

- Introduce a section for pre-task preparation, emphasizing the importance of reading documentation and understanding the codebase structure. - Update the Python code modification instructions to include formatting checks before verifying code quality.

- Change the representation of intrinsic functions from MIRString to Symbol in the KMIR codebase. - Modify related documentation to reflect the new syntax for intrinsic function execution and definitions. - Ensure consistency across the semantic definitions for intrinsic functions in both mono and kdist contexts.

- Update test state files to reflect the new representation of intrinsic functions as Symbols instead of MIRStrings. - Ensure consistency across various test cases, including arithmetic, arrays, and references, by adding the black_box intrinsic function. - Modify expected outputs in tests to align with the recent changes in intrinsic function handling. This change enhances the accuracy of intrinsic function testing and maintains alignment with the latest updates in the KMIR codebase.

- Refactor the functions method to include parsing of intrinsic functions directly within the KMIR class. - Update the expected output for intrinsic functions in the integration tests to reflect the new parsing logic. - Ensure that intrinsic functions are correctly represented in the test cases, maintaining consistency with recent changes in the KMIR codebase. This update improves the handling and testing of intrinsic functions, aligning with the latest developments in the project.

- Clean up unnecessary whitespace in the functions method of the KMIR class. - Ensure consistent formatting for improved readability and maintainability of the code. This minor update enhances the overall code quality without altering functionality.

jberthold

Can we please separate moving the test files to the new tests/ directory from the cahnge to implement the black_box intrinsic and intrinsic support?

…ction (#657) - Updated documentation to explain how to directly access elements of an Aggregate when #traverseProjection becomes stuck. - Introduced a new rule for handling single-element aggregates in the semantics. - Added a new test case for closure access to a struct, ensuring correct behavior. - Updated integration tests to include the new failure case for closure access to structs.

- Update CLAUDE.md to reflect changes in test directories. - Remove the utils.py file as it contained unused functions for test file management. - Modify integration and unit tests to directly reference test data without relying on the removed utility functions. - Adjust expected output paths in tests to align with the new structure. This refactor streamlines the test organization and improves maintainability by eliminating unnecessary code.

…seProjection - Removed outdated explanations regarding direct access to single-element aggregates. - Clarified the importance of the new rule for unwrapping single-element aggregates in the context of closures accessing struct fields. - Enhanced the overall clarity of the documentation to better reflect the current behavior and requirements. This update ensures that the documentation accurately represents the functionality and rationale behind the changes made in previous commits.

- Deleted the testing.md file, which contained instructions and structure for running unit and integration tests. - This removal reflects the current state of the project and streamlines the documentation by eliminating redundant information. This change helps maintain clarity and relevance in the project's documentation.

- Changed the depth parameter for the 'intrinsic-blackbox' entry in EXEC_DATA from None to 1000. - Adjusted the test parameterization in test_prove_termination to exclude the 'intrinsic-blackbox' name, streamlining the test cases. These updates enhance the clarity and focus of the integration tests, ensuring they accurately reflect the intended test scenarios.

jberthold · 2025-08-25T23:34:32Z

                          [ group(mir-enum)
                          , symbol(MonoItemKind::MonoItemGlobalAsm)
                          ]
+                      | IntrinsicFunction(Symbol) [ symbol(IntrinsicFunction) ]


Two comments:

(minor) The symbol should have a prefix MonoItemKind: to keep the conventions.

(major) This change steps away from modelling the json contents in the K sorts. Previously, all sorts used by kmir-ast.md were present in the json directly. To change this, we could use a different sort (with constructors Function(Symbol, Body) and Intrinsic(Symbol) in the function table at runtime.

jberthold · 2025-08-25T23:41:21Z

We have an older open PR in stable-mir-json that relates to the intrinsics: https://github.com/runtimeverification/stable-mir-json/pull/85/files

jberthold

As discussed, let's make a ticket for refactoring and merge this

dkcumming · 2025-08-28T03:18:43Z

  // other item kinds are not expected or supported
  rule #getBlocksAux(monoItemStatic(_, _, _)) => .List // should not occur in calls
  rule #getBlocksAux(monoItemGlobalAsm(_)) => .List // not supported
+  rule #getBlocksAux(IntrinsicFunction(_)) => .List // intrinsics have no body


@Stevengre @jberthold This is not necessarily true, some intrinsics will have a body. I don't have anything on hand for this now but we ran into intrinsics with a body in the past.

Sorry, I just add an #667 to track this problem. But I may need better understanding about this whole figure of mir. Maybe I can review the issues in stable-mir-json and mir-semantics (or not. because we need to focus on p-token?) But I still think we need an issue as a milestone goal for the p-token engagement and attach all the related works to it to track our progress?

Just some thinking...

This PR implements support for Rust intrinsic functions in the MIR semantics, starting with the black_box intrinsic. Intrinsic functions are compiler built-ins that don't have regular MIR bodies and require special handling in the formal semantics. Key Changes Core Implementation - Python Layer (kmir.py, smir.py): - Extended functions() method to recognize and handle intrinsic functions from SMIR - Added mapping of intrinsic symbols to IntrinsicFunction K terms - Intrinsics are identified by IntrinsicSym in the function symbols K Semantics - mono.md: Added IntrinsicFunction(Symbol) constructor to MonoItemKind - kmir.md: - Added special execution path for intrinsic functions that bypasses normal call setup - Implemented #execIntrinsic mechanism for direct intrinsic execution - Added black_box implementation as identity function Testing & Documentation - Added comprehensive test suite for intrinsic functions - Created developer documentation: - docs/dev/adding-intrinsics.md: Guide for adding new intrinsic support - Added test utilities for SMIR generation and parsing - Included integration tests demonstrating black_box usage Implementation Details The intrinsic function support follows this flow: 1. SMIR parser identifies functions with IntrinsicSym symbols 2. Python layer creates IntrinsicFunction K terms for these functions 3. K semantics intercepts intrinsic calls and routes them to #execIntrinsic 4. Each intrinsic has its own execution rule (currently only black_box) Future Work This PR establishes the foundation for supporting additional Rust intrinsics. The modular design makes it straightforward to add new intrinsics by: 1. Adding execution rules in kmir.md 2. Writing corresponding tests in tests/rust/intrinsic/ 3. Following the patterns established in this PR The test infrastructure refactoring also provides a solid foundation for expanding test coverage across the entire MIR semantics implementation. --------- Co-authored-by: Claude <noreply@anthropic.com>

Stevengre added 4 commits August 21, 2025 14:27

Stevengre self-assigned this Aug 21, 2025

Stevengre and others added 6 commits August 25, 2025 14:41

Stevengre changed the title ~~Support for intrinsic blackbox~~ Implement std::hint::black_box intrinsic support in KMIR Aug 25, 2025

Stevengre marked this pull request as ready for review August 25, 2025 06:48

Stevengre and others added 8 commits August 25, 2025 15:11

Fix code formatting and linting issues

ba0328e

- Fix flake8 B907: Use !r conversion flag for string formatting - Apply black formatting to Python files 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

Remove TODO comment for intrinsic function handling in KMIR documenta…

c5efc9a

…tion

Stevengre requested review from dkcumming and jberthold August 25, 2025 09:19

jberthold reviewed Aug 25, 2025

View reviewed changes

Comment thread CLAUDE.md Outdated

Comment thread CLAUDE.md

Comment thread tests/README.md Outdated

Stevengre force-pushed the jh/intrinsic-blackbox branch from 8298d4b to 26303ce Compare August 25, 2025 11:55

Stevengre added 4 commits August 25, 2025 20:17

use traditional way to manage tests

233d07e

Stevengre added 3 commits August 25, 2025 20:40

Merge branch 'master' into jh/intrinsic-blackbox

d9113b9

Remove unnecessary blank line from Makefile to improve readability.

035c631

Stevengre requested a review from jberthold August 25, 2025 12:47

update-expected-output

a03620b

jberthold reviewed Aug 25, 2025

View reviewed changes

jberthold approved these changes Aug 26, 2025

View reviewed changes

use the known keys and

cf8455b

Stevengre mentioned this pull request Aug 26, 2025

Refactor IntrinsicFunction handling to align with stable-mir-json and existing development patterns #661

Open

Stevengre merged commit 07a5f48 into master Aug 26, 2025
5 checks passed

Stevengre deleted the jh/intrinsic-blackbox branch August 26, 2025 03:26

dkcumming reviewed Aug 28, 2025

View reviewed changes

Stevengre mentioned this pull request Aug 28, 2025

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

Open

Navigation Menu

Uh oh!

Implement std::hint::black_box intrinsic support in KMIR - #659

Implement std::hint::black_box intrinsic support in KMIR#659
Stevengre merged 28 commits into
masterfrom
jh/intrinsic-blackbox

Stevengre commented Aug 21, 2025 •

edited

Loading

Uh oh!

jberthold left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jberthold Aug 25, 2025

Uh oh!

jberthold commented Aug 25, 2025

Uh oh!

jberthold left a comment

Uh oh!

Uh oh!

dkcumming Aug 28, 2025

Uh oh!

Stevengre Aug 28, 2025 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

Stevengre commented Aug 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jberthold left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jberthold Aug 25, 2025

Choose a reason for hiding this comment

Uh oh!

jberthold commented Aug 25, 2025

Uh oh!

jberthold left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

dkcumming Aug 28, 2025

Choose a reason for hiding this comment

Uh oh!

Stevengre Aug 28, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Stevengre commented Aug 21, 2025 •

edited

Loading

Stevengre Aug 28, 2025 •

edited

Loading