CI: run the Cranelift verifier.

[cfallin]

This PR adds a GitHub workflow that runs on pushes to main and on PRs. It restores the verifier's SMT query cache from the shared actions cache, runs 'verify.sh rebuild-cache' on top of it, and (on main) republishes the rebuilt cache as the isle-veri-cache.tar.gz asset on the rolling dev release plus a run artifact for use by local developers.

It also adds a script, cranelift/isle/veri/setup/download-cache.sh, so a local user can download the current CI cache from the dev release and verify incrementally on top of it.

Note that the cache needs a unique key per run on main, because a cache entry is immutable once
created. Fortunately we can select the latest key by prefix.

[cfallin]

cc @avanhatt @mmcloughlin

Let's see how long the run takes on the branch...

[cfallin]

Hmm, it seems that new workflows don't run until merge to main -- do I need to merge PRs as part of a debug loop?! That's awfully silly... (good security reasons for this I suppose but still)

[avanhatt]

@cfallin it seems like you can manually trigger without merging to main https://docs.github.com/en/actions/how-tos/manage-workflow-runs/approve-runs-from-forks

[cfallin]

Unfortunately it seems there is no "Approve workflows to run" option, at least for me. I wonder if the set of workflows is somehow fixed based on what is in main so an entirely new workflow isn't picked up... @alexcrichton let us know if there's a better way to test, here!

[alexcrichton]

If it works I'd recommend moving this to main.yml because otherwise we need to reconfigure repository settings to actually gate on this check where if it's in main.yml we can just manage it via the text configuration there.

[github-actions]

Subscribe to Label Action

cc @cfallin, @fitzgen

Details

This issue or pull request has been labeled: "cranelift", "isle"

Thus the following users have been cc'd because of the following labels:

• cfallin: isle
• fitzgen: isle

To subscribe or unsubscribe from this label, edit the .github/subscribe-to-label.json configuration file.

Learn more.

[cfallin]

Cool, the job finishes in 3h58m on a GitHub runner. That's definitely longer than I would have hoped for, but as long as the cache isn't dropped or mass-invalidated by some change it should be OK? (We should merge when the merge queue is otherwise quiet of course...)

[avanhatt]

Woo! 🎉

A few things:

1. It looks like for aarch64, 54 instantiations result in unknown for this timeout/these runners. We may be okay with that, but at that point, we may also want to think about running the fast config that skips known-slow/more likely to be unknown queries? Would also reduce the runtime.
2. Did we also want to verify the covered midend rules in this PR? Looks like from the logs this did a full aarch64 and the sanity-check x64 expansions, but not opt.

[alexcrichton]

Oh, also, as-is this is going to run on every PR which while probably fine we perhaps want to tweak a bit to only run conditionally like we do for most other jobs. If you copy this configuration it'll only run with prtest:full or on the merge queue and if you copy this configuration there will be custom logic of when to trigger on PRs (found here.

do I need to merge PRs as part of a debug loop?! That's awfully silly...

I'll caution that this'll probably need an iteration or two of landing on main to fiddle with the logic around caching and the dev release and such. I agree it's unfortunate, but it's all we've got.

[cfallin]

OK, switching to the aarch64-fast config got the run down to 18 minutes, which is great!

[alexcrichton]

I see the asset on the dev release so looks like that's going well, @cfallin wanna double-check the download script pulls that for local development?

[cfallin]

I see the asset on the dev release so looks like that's going well, @cfallin wanna double-check the download script pulls that for local development?

Yes, the download worked and verification from cache-only worked as well!

$ cranelift/isle/veri/setup/download-cache.sh
############################################################################################################################################################################################################### 100.0%
Installed verifier cache to cranelift/isle/veri/cache/
You can now run ./cranelift/isle/veri/verify.sh (or cache-only / rebuild-cache).

$ time cranelift/isle/veri/verify.sh cache-only aarch64-fast
=== Verifying from cache (read-only, enforcing; no solver) ===
=== veri: cranelift/isle/veri/configs/aarch64-fast.args ===
    Finished `release` profile [optimized] target(s) in 0.07s
     Running `target/release/veri --config cranelift/isle/veri/configs/aarch64-fast.args --cache-source-dir cranelift/isle/veri/cache --cache-mode read-only-enforcing`
[ ... ]
Verification passed: 523
Verification failed: 0
Verification unknown: 0
===============================================================================
========================== Cache statistics ===========================
Mode:            read-only-enforcing
Source:          cranelift/isle/veri/cache
Destination:     (none)
Hits:            1219 (100.0%)
Misses:          0 (0.0%)
New entries:     0
Retained:        0
========================================================================
=== Cache verification passed ===
cranelift/isle/veri/verify.sh cache-only aarch64-fast  6.28s user 1.08s system 324% cpu 2.264 total