Prototype `mir_verify` command #1904

RyanGlScott · 2023-08-10T19:48:29Z

This implements just enough scaffolding to support the basics of a mir_verify command and related scaffolding, which is one of the main goals of #1859. When I say "basic", I really do mean that: there are quite a few things that do not work currently. These include:

mir_alloc/mir_points_to do not work yet.
Overrides (unsafe or otherwise) do not work yet.
There is no way to declare variables with struct or enum types.
Likely other things.

These limitations notwithstanding, it is now possible to write MIR specifications for very simple functions such as the ones in the test_mir_verify_basic integration test. I will be adding additional capabilities in subsequent patches.

Most of the code in this patch is not terribly exciting, as lots of it is cargo-culted from the LLVM and JVM backends. Ideally, we would find a way to deduplicate a lot more of this code, but this will not be straightforward without substantial refactoring in SAW. See #379.

In addition to the code itself, I have also expanded the SAW manual to mention the variety of new MIR-related commands added in this patch. Of particular interest is that mir_verify allows you to specify function identifiers in multiple ways, which is provided as a convenience to SAW users. See the manual for more details.

Checks off several boxes in #1859.

RyanGlScott

There are a lot of "plumbing-related" changes in this PR, which makes this a bit of a slog to review. I've made an effort to highlight what I think are the most interesting changes when compared to the existing LLVM/JVM backends.

doc/manual/manual.md

RyanGlScott · 2023-08-10T19:51:54Z

crucible-mir-comp/src/Mir/Compositional/Convert.hs

-- | TypeShape is used to classify MIR `Ty`s and their corresponding
-- CrucibleTypes into a few common cases.  We don't use `Ty` directly because
-- there are some `Ty`s that have identical structure (such as TyRef vs.
-- TyRawPtr) or similar enough structure that we'd rather write only one case
-- (such as `u8` vs `i8` vs `i32`, all primitives/BaseTypes).  And we don't use
-- TypeRepr directly because it's lacking information in some cases (notably
-- `TyAdt`, which is always AnyRepr, concealing the actual field types of the
-- struct).
--
-- In each constructor, the first `M.Ty` is the overall MIR type (e.g., for
-- ArrayShape, this is the TyArray type).  The overall `TypeRepr tp` isn't
-- stored directly, but can be computed with `shapeType`.
-data TypeShape (tp :: CrucibleType) where


It looks like I deleted a bunch of code here, but that's only because it's been moved to the new SAWScript.Crucible.MIR.TypeShape module. I needed to use this code from saw-script, not just crucible-mir-comp, which motivated this move.

RyanGlScott · 2023-08-10T19:52:26Z

crucible-mir-comp/src/Mir/Compositional/MethodSpec.hs

Similarly, this code now lives in SAWScript.Crucible.MIR.MethodSpecIR, as I needed to use the various type family instances in saw-script.

RyanGlScott · 2023-08-10T19:53:27Z

doc/manual/manual.md

+  TopLevel MIRSpec
+~~~~
+
+### Running a MIR-based verification


This manual section is an interesting read, as it describes the conventions that SAW uses when looking up MIR identifiers.

RyanGlScott · 2023-08-10T19:54:33Z

src/SAWScript/Crucible/MIR/ResolveSetupValue.hs

+-- | A pair of a simulation-time MIR value ('RegValue') and its corresponding
+-- type ('TypeShape'), where the @tp@ type parameter is closed over
+-- existentially. SAW's MIR backend passes around 'MIRVal's at simulation time.
+data MIRVal where
+  MIRVal :: TypeShape tp -> RegValue Sym tp -> MIRVal


This is a key data type that is used in many places in the MIR backend.

RyanGlScott · 2023-08-10T19:55:47Z

src/SAWScript/Crucible/MIR/ResolveSetupValue.hs

+toMIRType ::
+  Cryptol.TValue ->
+  Either ToMIRTypeErr Mir.Ty


This describes how to convert Cryptol types (TValues) to MIR types (Mir.Tys).

RyanGlScott · 2023-08-10T19:57:20Z

src/SAWScript/Crucible/MIR/Builtins.hs

+-- | Check if two 'Mir.Ty's are compatible in SAW. This is a slightly coarser
+-- notion of equality to reflect the fact that MIR's type system is richer than
+-- Cryptol's type system, and some types which would be distinct in MIR are in
+-- fact equal when converted to the equivalent Cryptol types. In particular:
+--
+-- 1. A @u<N>@ type is always compatible with an @i<N>@ type. For instance, @u8@
+--    is compatible with @i8@, and @u16@ is compatible with @i16@. Note that the
+--    bit sizes of both types must be the same. For instance, @u8@ is /not/
+--    compatible with @i16@.
+--
+-- 2. The @usize@/@isize@ types are always compatible with @u<N>@/@i<N>@, where
+--    @N@ is the number of bits corresponding to the 'Mir.SizeBits' type in
+--    "Mir.Intrinsics". (This is a bit unsavory, as the actual size of
+--    @usize@/@isize@ is platform-dependent, but this is the current approach.)
+--
+-- 3. Compatibility applies recursively. For instance, @[ty_1; N]@ is compatible
+--    with @[ty_2; N]@ iff @ty_1@ and @ty_2@ are compatibile. Similarly, a tuple
+--    typle @(ty_1_a, ..., ty_n_a)@ is compatible with @(ty_1_b, ..., ty_n_b)@
+--    iff @ty_1_a@ is compatible with @ty_1_b@, ..., and @ty_n_a@ is compatible
+--    with @ty_n_b@.
+--
+-- See also @checkRegisterCompatibility@ in "SAWScript.Crucible.LLVM.Builtins"
+-- and @registerCompatible@ in "SAWScript.Crucible.JVM.Builtins", which fill a
+-- similar niche in the LLVM and JVM backends, respectively.
+checkCompatibleTys :: Mir.Ty -> Mir.Ty -> Bool
+checkCompatibleTys ty1 ty2 = tyView ty1 == tyView ty2


This function (and everything that it is defined in terms of) is worth a look.

RyanGlScott · 2023-08-10T19:57:46Z

src/SAWScript/Crucible/MIR/Builtins.hs

+-- | Returns the Cryptol type of a MIR type, returning 'Nothing' if it is not
+-- easily expressible in Cryptol's type system or if it is not currently
+-- supported.
+cryptolTypeOfActual :: Mir.Ty -> Maybe Cryptol.Type


This describes how to convert a MIR type (Mir.Ty) to a Cryptol Type.

RyanGlScott · 2023-08-10T19:58:08Z

src/SAWScript/Crucible/MIR/Builtins.hs

+-- | Given a function name @fnName@, attempt to look up its corresponding
+-- 'Mir.DefId'. Currently, the following types of function names are permittd:
+--
+-- * @<crate_name>/<disambiguator>::<function_name>: A fully disambiguated name.
+--
+-- * @<crate_name>::<function_name>: A name without a disambiguator. In this
+--   case, SAW will attempt to look up a disambiguator from the @crateDisambigs@
+--   map. If none can be found, or if there are multiple disambiguators for the
+--   given @<crate_name>@, then this will fail.
+findDefId :: Map Text (NonEmpty Text) -> Text -> TopLevel Mir.DefId
+findDefId crateDisambigs fnName = do


This function implements the MIR identifier lookup logic described in the SAW manual.

RyanGlScott · 2023-08-10T19:58:49Z

src/SAWScript/Crucible/MIR/Override.hs

+valueToSC ::
+  Sym ->
+  MS.ConditionMetadata ->
+  OverrideFailureReason MIR ->
+  Cryptol.TValue ->
+  MIRVal ->
+  OverrideMatcher MIR w Term


This describes how to convert a MIRVal to a SAWCore Term.

bboston7

This broadly looks great! Thanks for pointing out places to focus more on. All of my comments are minor.

Also, Github won't let me put comments far away from your changes, so I'm putting one here:
On line 2359 in the manual the part that says "(or the corresponding JVM statements)" should say something like "(or the corresponding JVM or MIR statements)"

doc/manual/manual.md

intTests/test_mir_verify_conds/Makefile

intTests/test_mir_verify_pop_count/Makefile

saw-remote-api/python/saw_client/__init__.py

src/SAWScript/Crucible/MIR/Builtins.hs

doc/manual/manual.md

src/SAWScript/Crucible/MIR/ResolveSetupValue.hs

src/SAWScript/Crucible/MIR/TypeShape.hs

src/SAWScript/Interpreter.hs

This implements just enough scaffolding to support the basics of a `mir_verify` command and related scaffolding, which is one of the main goals of #1859. When I say "basic", I really do mean that: there are quite a few things that do not work currently. These include: * `mir_alloc`/`mir_points_to` do not work yet. * Overrides (unsafe or otherwise) do not work yet. * There is no way to declare variables with `struct` or `enum` types. * Likely other things. These limitations notwithstanding, it is now possible to write MIR specifications for very simple functions such as the ones in the `test_mir_verify_basic` integration test. I will be adding additional capabilities in subsequent patches. Most of the code in this patch is not terribly exciting, as lots of it is cargo-culted from the LLVM and JVM backends. Ideally, we would find a way to deduplicate a lot more of this code, but this will not be straightforward without substantial refactoring in SAW. See #379. In addition to the code itself, I have also expanded the SAW manual to mention the variety of new MIR-related commands added in this patch. Of particular interest is that `mir_verify` allows you to specify function identifiers in multiple ways, which is provided as a convenience to SAW users. See the manual for more details. Checks off several boxes in #1859.

RyanGlScott requested review from bboston7 and spernsteiner August 10, 2023 19:48

RyanGlScott commented Aug 10, 2023

View reviewed changes

RyanGlScott force-pushed the T1859-basic-mir-verify branch from 5deb6b1 to 359a881 Compare August 11, 2023 13:05

RyanGlScott marked this pull request as ready for review August 11, 2023 13:05

RyanGlScott force-pushed the T1859-basic-mir-verify branch 2 times, most recently from c01a82c to 1e68229 Compare August 18, 2023 18:57

RyanGlScott mentioned this pull request Aug 21, 2023

Support Rust verification in SAW via crucible-mir #1859

Closed

29 tasks

RyanGlScott added the subsystem: crucible-mir Issues related to Rust verification with crucible-mir and/or mir-json label Aug 21, 2023

RyanGlScott force-pushed the T1859-basic-mir-verify branch from 1e68229 to 0e24394 Compare August 22, 2023 16:47

bboston7 approved these changes Aug 22, 2023

View reviewed changes

RyanGlScott force-pushed the T1859-basic-mir-verify branch from 0e24394 to 634b884 Compare August 22, 2023 23:26

RyanGlScott added 4 commits August 22, 2023 19:28

Add Haddocks for verifySimulate commands

113cf39

tyToShape: Remove useless case expression

55adfbe

{llvm,jvm,mir}_assert: Fix mismatched parentheses in :? descriptions

8930c8a

RyanGlScott force-pushed the T1859-basic-mir-verify branch from 634b884 to 8930c8a Compare August 22, 2023 23:28

RyanGlScott added the PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run label Aug 22, 2023

mergify bot merged commit a618ae2 into master Aug 23, 2023
38 checks passed

mergify bot deleted the T1859-basic-mir-verify branch August 23, 2023 03:38

RyanGlScott mentioned this pull request Aug 23, 2023

Support mir_alloc, mir_alloc_mut, and mir_points_to #1916

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Prototype `mir_verify` command #1904

Prototype `mir_verify` command #1904

RyanGlScott commented Aug 10, 2023

RyanGlScott left a comment

RyanGlScott Aug 10, 2023

RyanGlScott Aug 10, 2023

RyanGlScott Aug 10, 2023

RyanGlScott Aug 10, 2023

RyanGlScott Aug 10, 2023

RyanGlScott Aug 10, 2023

RyanGlScott Aug 10, 2023

RyanGlScott Aug 10, 2023

RyanGlScott Aug 10, 2023

bboston7 left a comment

Prototype mir_verify command #1904

Prototype mir_verify command #1904

Conversation

RyanGlScott commented Aug 10, 2023

RyanGlScott left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bboston7 left a comment

Choose a reason for hiding this comment

Prototype `mir_verify` command #1904

Prototype `mir_verify` command #1904