Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

crux-mir-comp: Support nightly-2023-01-23 #1891

Merged
merged 3 commits into from
Jul 14, 2023
Merged

Conversation

RyanGlScott
Copy link
Contributor

@RyanGlScott RyanGlScott commented Jul 7, 2023

This patch bumps the crucible submodule to bring in the changes from GaloisInc/crucible#1096 and updates the code in crucible-mir-comp and crux-mir-comp accordingly. Some highlights:

  • All of the crux-mir-comp test cases now use crux::test instead of crux_test.
  • All of the crux-mir-comp test cases now scrub out the values of crate hash disambiguators to make their output more stable.
  • The overrides in crux-mir-comp no longer depend on the specific disambiguator values being used, which makes them work with the sometimes unpredictable hash values used for crate disambiguators.
  • I have added a tyToShape case for TyStr to handle new kinds of static values that arise in the new Rust nightly (mostly coming from constant values in the fmt crate). The code for this case is nearly identical to that in the TySlice case.
  • There are now static values of type TyFnPtr in the new Rust nightly (mostly coming from constant values in the fmt crate), so in order to handle them in clobberGlobals, I needed to add a FnPtrShape data constructor to TypeShape. This is mostly a quick hack, since I implemented all other functionality for FnPtrShape with calls to error. Nevertheless, that is enough to make all of the tests pass. We can always fill out the calls to error later if need be.

@RyanGlScott RyanGlScott marked this pull request as draft July 7, 2023 20:12
Copy link
Contributor

@spernsteiner spernsteiner left a comment

Choose a reason for hiding this comment

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

Looks good to me

crux-mir-comp/DESIGN.md Outdated Show resolved Hide resolved
crux-mir-comp/DESIGN.md Outdated Show resolved Hide resolved
This patch bumps the `crucible` submodule to bring in the changes from
GaloisInc/crucible#1096 and updates the code in `crucible-mir-comp` and
`crux-mir-comp` accordingly. Some highlights:

* All of the `crux-mir-comp` test cases now use `crux::test` instead of
  `crux_test`.
* All of the `crux-mir-comp` test cases now scrub out the values of crate hash
  disambiguators to make their output more stable.
* The overrides in `crux-mir-comp` no longer depend on the specific
  disambiguator values being used, which makes them work with the sometimes
  unpredictable hash values used for crate disambiguators.
* I have added a `tyToShape` case for `TyStr` to handle new kinds of static
  values that arise in the new Rust nightly (mostly coming from constant values
  in the `fmt` crate). The code for this case is nearly identical to that in the
  `TySlice` case.
* There are now static values of type `TyFnPtr` in the new Rust nightly (mostly
  coming from constant values in the `fmt` crate), so in order to handle them
  in `clobberGlobals`, I needed to add a `FnPtrShape` data constructor to
  `TypeShape`. This is mostly a quick hack, since I implemented all other
  functionality for `FnPtrShape` with calls to `error`. Nevertheless, that is
  enough to make all of the tests pass. We can always fill out the calls to
  `error` later if need be.
@RyanGlScott RyanGlScott marked this pull request as ready for review July 14, 2023 18:14
@RyanGlScott RyanGlScott added the ready-to-merge If at least one person approves this PR, automatically merge it when CI finishes successfully. label Jul 14, 2023
@mergify mergify bot merged commit fe3e6ff into master Jul 14, 2023
38 checks passed
@mergify mergify bot deleted the crux-mir-nightly-2023-01-23 branch July 14, 2023 21:42
@RyanGlScott RyanGlScott added the crucible/mir Related to crucible-mir verification label Aug 21, 2023
This pull request was closed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
crucible/mir Related to crucible-mir verification ready-to-merge If at least one person approves this PR, automatically merge it when CI finishes successfully.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants