`crux-mir`: Support `nightly-2023-01-23` #1096

RyanGlScott · 2023-07-05T20:53:12Z

This is a fairly large overhaul of crux-mir's and crucible-mir's internals to support a more recent Rust nightly (nightly-2023-01-23). The work is split between myself, @m10f, and @spernsteiner.

There is a lot happening here, so if you want to learn specifics, I'd encourage you to look at individual commits. Some of the broad themes in the patchset include:

Propertly support for Rust's new constant forms
Better support for zero-sized constants
Encoding enum discriminant types so that crucible-mir can know about non-isize discriminant types (e.g., Ordering, which uses an i8 discriminant)
Being much more systematic about which patches we must apply to the Rust standard libraries for Crucible's needs (see the new crux-mir/lib/Patches.md file for explanations of each patch)
A more intelligent way of computing crate disambiguators for looking up known types such as MaybeUninit and Option
Re-enabling the macOS CI for crux-mir, which was previously disabled due to the nightly not working on recent macOSes

This should fix several issues:

- updated libs - changed crux_mir to crux::mir in tests - new lib build script (build.sh) - changes to crux-mir to support changes to rustc (nightly-2023-01-22)

This is in preparation for permitting various translation functions to be called from `transStatics`.

If a static is initialized with a constant value, we now detect and handle this in `translateStatics`.

Adapted from the original patch in 0374310

Previously, only constant arrays of bytes were translatable. This patch lifts that restriction so that constant arrays of arbitrary types can be translated, which is necessary to support some constant arrays used in a newer Rust nightly.

Adapted from the original commit in 52f6f57

This took us a while to debug before we realized what was going on. Let's make the failure obvious.

Originally from commit 42424ae

Originally from commit 69e92cb

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.

spernsteiner

Mostly looks good, aside from a possible correctness issue with the handling of StatementKind::Intrinsic.

crucible-mir/src/Mir/DefId.hs

crucible-mir/src/Mir/Trans.hs

This require a fair bit of refactoring to avoid problematic uses of `textId` that were relying on `defaultDisambiguator`.

Because `Box<T>` no longer uses the same `TypeRep` as `mut *T`, it is not sound to translate `ShallowInitBox` as though it were an identity function. Thankfully, nothing in the test suite actually uses `ShallowInitBox`, so we simply leave it unimplemented for now.

There's not much of a point in checking for the `crux` configuration attribute, since one wouldn't be able to compile these tests with bare `rustc` anyway due to their use of the `crucible` crate.

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 · 2023-07-17T11:08:57Z

It turns out that this broke the nightly crux-mir Docker job, as seen here. Thankfully, I was notified very quickly about this! I've submitted a fix in #1099.

(cherry picked from commit cd84599)

m10f and others added 30 commits July 3, 2023 15:08

Normalize naming and organization of rust crates

73df4f6

WIP mir-json

b121efe

- updated libs - changed crux_mir to crux::mir in tests - new lib build script (build.sh) - changes to crux-mir to support changes to rustc (nightly-2023-01-22)

[WIP] more bugfixes

b4f6235

Update mir-json submodule

82c3cd0

re-add missing libs to linker and libs dir

26d1dc5

build.sh: Set STD_ENV_ARCH

e4e3a65

Add test_output.log

1cc32ba

Remove unneeded RustcRenderedConst newtype

e208e98

initFnState: Remove unused argument

b3e74d1

genFn/transDefine: Replace unused patterns with wildcards

0df0660

Replace currentFn with a more general FnTransContext

14ce2da

This is in preparation for permitting various translation functions to be called from `transStatics`.

Translate statics with constant initializers properly

6f97467

If a static is initialized with a constant value, we now detect and handle this in `translateStatics`.

Add custom op for ctpop

cc8d3f2

lib: Replace RawVec's allocator

0eacf40

Adapted from the original patch in 0374310

Translate more types of ConstArrays

fa7292a

Previously, only constant arrays of bytes were translatable. This patch lifts that restriction so that constant arrays of arbitrary types can be translated, which is necessary to support some constant arrays used in a newer Rust nightly.

Update mir-json submodule

370cacc

patch core::fmt

6b4370f

crux-mir: Note fmt reimplementation in lib/Patches.md

8c590e4

Adapted from the original commit in 52f6f57

Mir.TransCustom: Use {impl} consistently

8a680c4

lib/crucible: Don't loop infinitely in zeroed()

0653a31

This took us a while to debug before we realized what was going on. Let's make the failure obvious.

crux-mir: Regenerate test_output.log

592b2a1

crucible-mir: Translate all ConstTuples, not just unit tuples

c1f8060

crucible-mir: Translate constant tuples

0bba133

crucible-mir: Add seqcst variants of some atomic intrinsics

b639790

crucible-mir: Add some more {extern}s to custom ops

07add62

Regenerate test_output.log

b57531c

Reapply "implement HashMap in terms of Vec"

6aebf2d

Originally from commit 42424ae

Implement ptr::invalid/invalid_mut in terms of casts

70e1387

Reapply "Avoid pointer arithmetic in slice iterators"

93c8031

Originally from commit 69e92cb

Stub out ThreadLocalRef

e7415d0

RyanGlScott added 5 commits July 5, 2023 17:08

CI: Use up-to-date Rust nightly

ed718aa

crux-mir/lib/Patches.md: Fill in some TODOs

42a3606

crucible-mir: Parenthesize some equality constraints

ef8fc37

crucible-mir: Avoid some failable do-block matches on ST

9ae78ed

crucible-mir: More parentheses

ee39bf0

RyanGlScott mentioned this pull request Jul 6, 2023

Run crux-mir-comp's test suite in CI GaloisInc/saw-script#1887

Open

Use crux::test instead of crux_test

e0d77af

RyanGlScott mentioned this pull request Jul 7, 2023

crux-mir-comp: Support nightly-2023-01-23 GaloisInc/saw-script#1891

Merged

spernsteiner reviewed Jul 13, 2023

View reviewed changes

RyanGlScott added 8 commits July 13, 2023 14:10

crucible-mir: Remove some commented-out old code

c8eb7b6

crucible-mir: Document reasoning for some evalRval cases

b794aca

crux-mir: Add test case for ConstKind::Unevaluated

8c11bca

Properly implement transStatement case for StmtIntrinsic

0afbb96

crucible-mir: Expunge defaultDisambiguator and anything that uses it

d2ff2cc

This require a fair bit of refactoring to avoid problematic uses of `textId` that were relying on `defaultDisambiguator`.

Bump mir-json submodule

e8ac077

crux-mir: Use simpler #[crux::test] attribute for symbolic tests

0515e64

There's not much of a point in checking for the `crux` configuration attribute, since one wouldn't be able to compile these tests with bare `rustc` anyway due to their use of the `crucible` crate.

RyanGlScott mentioned this pull request Jul 13, 2023

Support nightly-2023-01-23 GaloisInc/mir-json#49

Merged

RyanGlScott marked this pull request as ready for review July 14, 2023 18:11

RyanGlScott merged commit b4546ce into master Jul 14, 2023

RyanGlScott deleted the crux-mir-nightly-2023-01-23-merge branch July 14, 2023 18:11

This was referenced Jul 14, 2023

crux-mir supported toolchain version too old #1059

Closed

Support Rust verification in SAW via crucible-mir GaloisInc/saw-script#1859

Closed

This was referenced Dec 5, 2023

crux-mir: Restore --no-model-internal-atomics #1148

Open

crux-mir: Support cross-compiling libs to wasm32 target #1147

Merged

RyanGlScott added a commit that referenced this pull request Feb 1, 2024

Mention #1096 in the {crucible,crux}-mir CHANGELOGs

cd84599

RyanGlScott added a commit that referenced this pull request Feb 6, 2024

Mention #1096 in the {crucible,crux}-mir CHANGELOGs

0f275cd

(cherry picked from commit cd84599)

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

`crux-mir`: Support `nightly-2023-01-23` #1096

`crux-mir`: Support `nightly-2023-01-23` #1096

RyanGlScott commented Jul 5, 2023 •

edited

Loading

spernsteiner left a comment

RyanGlScott commented Jul 17, 2023

crux-mir: Support nightly-2023-01-23 #1096

crux-mir: Support nightly-2023-01-23 #1096

Conversation

RyanGlScott commented Jul 5, 2023 • edited Loading

spernsteiner left a comment

Choose a reason for hiding this comment

RyanGlScott commented Jul 17, 2023

`crux-mir`: Support `nightly-2023-01-23` #1096

`crux-mir`: Support `nightly-2023-01-23` #1096

RyanGlScott commented Jul 5, 2023 •

edited

Loading