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

Bump crucible to get the Const_RefRoots fix. #2107

Merged
merged 4 commits into from
Aug 27, 2024
Merged

Conversation

sauclovian-g
Copy link
Contributor

Includes the test from the issue.

Fixes #2064.

@sauclovian-g sauclovian-g added bug crucible/mir Related to crucible-mir verification labels Aug 26, 2024
@RyanGlScott
Copy link
Contributor

Looking good!

Note that the MIR-related test cases in this repo have checked in their MIR JSON files to version control so that the test suite can be ran without needing to install mir-json beforehand. The downside to this approach is that these JSON files are still using the old mir-json schema (prior to the changes in GaloisInc/mir-json#73 and GaloisInc/crucible#1243), so they will no longer parse with the new version of crucible-mir. This can be seen in:

  1. The saw integration tests (failing CI log here)
  2. The saw-remote-api tests (failing CI log here)

(I'm a bit undecided about whether we want to check in all of the MIR JSON files to version control going forward, but that's the way it's currently done.)

In both cases, the most direct solution would be to generate the MIR JSON files. They are located in the following places:

  1. In the saw integration tests: All of the directories that are shown when running the find intTests/ -iname "*.linked-mir.json" command
  2. In the saw-remote-api tests: In this directory

In each location, there should be a Makefile that can be used to regenerate the JSON files. Please let me know if you have any difficulties.

@sauclovian-g
Copy link
Contributor Author

Bleah, I should have thought of that. After all, I noticed the json files were checked in...

(btw there's a third set in the rust tutorial)

It occurs to me, also, that being able to diff them after a change like this might be worth the space overhead of including newlines in the output...

@RyanGlScott
Copy link
Contributor

Ah, one last thing: you'll have to update these lines to reflect the new disambiguator values:

 // Test using fully disambiguated names
-mir_verify m "test/775505e0::id_u8" [] false (id_spec mir_u8) z3;
-mir_verify m "test/775505e0::id_u8[0]" [] false (id_spec mir_u8) z3;
+mir_verify m "test/ff7472fa::id_u8" [] false (id_spec mir_u8) z3;
+mir_verify m "test/ff7472fa::id_u8[0]" [] false (id_spec mir_u8) z3;

(these are the only way to refer to certain objects and rustc itself
has no reason to care about whether the numbers are stable, so they
aren't very)
@sauclovian-g
Copy link
Contributor Author

I have done so. I wouldn't have thought this would have changed much of anything here, though. So I have investigated, which may or may not have been worthwhile; the change from 775505e0 to ff7472fa covers the whole compilation and isn't particularly interesting.

What's different though is that the original has two extra copies of id_array, specialized to take no args and return the array size (one each for the argument type and return type sizes, even though they're the same); these have disappeared. Is this because of a different compiler version (or just because it's Olde), which probably doesn't matter, or reflect something about compiler options or modes, which may?

@RyanGlScott
Copy link
Contributor

tl;dr These changes are benign.

What's different though is that the original has two extra copies of id_array, specialized to take no args and return the array size (one each for the argument type and return type sizes, even though they're the same); these have disappeared.

In more concrete terms: before this PR, id_array was compiled to the following MIR:

fn test/775505e0::id_array[0](_1 : [u32; 5]) -> [u32; 5] {
   let mut _0 : [u32; 5];
   bb0: {
      _0 = use(_1);
      return;
   }
}
fn test/775505e0::id_array[0]::{constant#0}[0]() -> usize {
   let mut _0 : usize;
   bb0: {
      _0 = use(5);
      return;
   }
}
fn test/775505e0::id_array[0]::{constant#1}[0]() -> usize {
   let mut _0 : usize;
   bb0: {
      _0 = use(5);
      return;
   }
}

I believe id_array[0]::{constant#0} and id_array[0]::{constant#1} represent the lengths of the first and second array types, respectively, in id_array's type signature. In this small program, they are not referenced anywhere else in the generated MIR, although it is conceivable that one could cook up a more complicated program where they are needed.

After this PR, however, neither id_array[0]::{constant#0} and id_array[0]::{constant#1} appear at all in the generated MIR. This is expected behavior, and these changes are benign. These changes aren't due to GaloisInc/mir-json#73, but rather due to a different commit (GaloisInc/mir-json#56) that was brought in by recompiling this program with a more recent version of mir-json. (That commit didn't change the JSON schema in any way, so we didn't bother to recompile SAW's test cases at the time.)

As for why that commit changes the MIR JSON output: GaloisInc/mir-json#56 causes saw-rustc only to mark functions as roots when performing dead-code elimination. Since id_array[0]::{constant#0} and id_array[0]::{constant#1} are considered top-level constants rather than functions at the MIR level, they are no longer marked as roots. Moreover, since no other definition references them, they are now discarded during mir-json's dead-code elimination pass.

@sauclovian-g
Copy link
Contributor Author

Good to know, thanks. So I think we can go ahead here...

@sauclovian-g sauclovian-g merged commit 47a7632 into master Aug 27, 2024
34 checks passed
@sauclovian-g sauclovian-g deleted the 2064-const-refroots branch August 27, 2024 18:21
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug crucible/mir Related to crucible-mir verification submodule bump
Projects
None yet
Development

Successfully merging this pull request may close these issues.

MIR override incorrectly rejected when applied to multiple const slice arguments
2 participants