Skip to content

Support constant trait objects#240

Merged
RyanGlScott merged 3 commits intomasterfrom
T237-trait-object-constants
Feb 3, 2026
Merged

Support constant trait objects#240
RyanGlScott merged 3 commits intomasterfrom
T237-trait-object-constants

Conversation

@RyanGlScott
Copy link
Contributor

This adds support for compiling constant values that are trait objects (e.g., const X: &dyn Trait = &0u32). Like other references to unsized values, these require adding special cases to make_allocation_body and try_render_ref_opty in order to support:

  • make_allocation_body unpacks the trait object to get the underlying type and then renders the constant based on that type.

  • try_render_ref_opty constructs a special "trait_object" constant that references the allocation body's DefId, along with the DefIds for the trait object's principal trait (trait_id) and vtable (vtable). These DefIds are used on the crucible-mir side to construct a trait object value when translating the MIR JSON into Crucible.

    (Note that trait objects without a principal trait are not yet supported. See Emit vtables for "trivial" trait objects that only contain auto traits #239 for more information on this point.)

Note that because "trait_object" is a new part of the schema, I needed to bump the schema version number to 9.

Fixes #237.

@RyanGlScott RyanGlScott self-assigned this Jan 30, 2026
@RyanGlScott RyanGlScott added the breaking change Changes that will require backwards-incompatible updates to the schema label Jan 30, 2026
RyanGlScott added a commit to GaloisInc/crucible that referenced this pull request Jan 30, 2026
This bumps the `mir-json` submodule to bring in the changes from
GaloisInc/mir-json#240. It also adds `crucible-mir`
support for parsing and translating constant trait object values. (See
GaloisInc/mir-json#237 for the motivation.)

Because these MIR JSON changes require bumping the schema version, we must also
do the same on the `crucible-mir` side.
Comment on lines +14 to +15
* `trait_id`: the `DefId` for the principal trait bound in the trait object.
This plays a similar role as the `trait_id` field in `Dynamic` types.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do you think we could use a type for this field that would be compatible with trait objects without principal types? I think this would give us a better chance of avoiding schema changes when we fix #239.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We'll likely need schema changes in other places anyway for #239. IMO it's better to be consistent for now and switch everything over at the same time.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think there is still a question of how exactly we should implement a fix for #239, and it's possible that the answer to that question could influence what the correct schema for trait_object should be. For instance, will the vtable that we emit for trivial trait objects have a corresponding trait definition? mir-json reserves the name "trait/0::empty[0]" for such traits (see the code here), so perhaps it would suffice to include that as the trait_id? On the other hand, this isn't a principal trait, so perhaps it would be confusing to emit this. In this case, perhaps we should emit null here?

I haven't quite figured out the answer to this question, so it's not yet clear to me what to do here.

Copy link
Contributor Author

@RyanGlScott RyanGlScott Jan 30, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(Oops, I wrote that comment before I saw #240 (comment). Good to know that we came to roughly the same conclusion!)

This adds support for compiling constant values that are trait objects (e.g.,
`const X: &dyn Trait = &0u32`). Like other references to unsized values, these
require adding special cases to `make_allocation_body` and
`try_render_ref_opty` in order to support:

* `make_allocation_body` unpacks the trait object to get the underlying type
  and then renders the constant based on that type.
* `try_render_ref_opty` constructs a special `"trait_object"` constant that
  references the allocation body's `DefId`, along with the `DefId`s for the
  trait object's principal trait (`trait_id`) and vtable (`vtable`). These
  `DefId`s are used on the `crucible-mir` side to construct a trait object
  value when translating the MIR JSON into Crucible.

  (Note that trait objects without a principal trait are not yet supported.
  See #239 for more information on this point.)

Note that because `"trait_object"` is a new part of the schema, I needed to
bump the schema version number to `9`.

Fixes #237.
@RyanGlScott RyanGlScott force-pushed the T237-trait-object-constants branch from a6c067f to 318f8c4 Compare February 2, 2026 19:33
RyanGlScott added a commit to GaloisInc/crucible that referenced this pull request Feb 3, 2026
This bumps the `mir-json` submodule to bring in the changes from
GaloisInc/mir-json#240. It also adds `crucible-mir`
support for parsing and translating constant trait object values. (See
GaloisInc/mir-json#237 for the motivation.)

Because these MIR JSON changes require bumping the schema version, we must also
do the same on the `crucible-mir` side.
RyanGlScott added a commit to GaloisInc/saw-script that referenced this pull request Feb 3, 2026
RyanGlScott added a commit to GaloisInc/saw-script that referenced this pull request Feb 3, 2026
GaloisInc/mir-json#240 bumps the `mir-json` schema
version number to 9, which requires regenerating MIR blobs in the test suite.
RyanGlScott added a commit to GaloisInc/saw-script that referenced this pull request Feb 3, 2026
This brings in the following changes via submodule bumps for the sake of
supporting constant trait objects in the MIR backend:

* GaloisInc/mir-json#240
* GaloisInc/crucible#1736

See GaloisInc/mir-json#237 for the motivation.

In addition, this brings in the following changes to allow `crucible-llvm` to
build after GaloisInc/crucible#1742:

* GaloisInc/llvm-pretty#186 and
  GaloisInc/llvm-pretty#188
* GaloisInc/llvm-pretty-bc-parser#345
RyanGlScott added a commit to GaloisInc/saw-script that referenced this pull request Feb 3, 2026
GaloisInc/mir-json#240 bumps the `mir-json` schema
version number to 9, which requires regenerating MIR blobs in the test suite.
@RyanGlScott RyanGlScott merged commit cf71cd5 into master Feb 3, 2026
6 of 8 checks passed
@RyanGlScott RyanGlScott deleted the T237-trait-object-constants branch February 3, 2026 15:58
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

breaking change Changes that will require backwards-incompatible updates to the schema

Projects

None yet

Development

Successfully merging this pull request may close these issues.

mir-json internal error with constant trait objects (entered unreachable code: dynamic should not occur here)

3 participants