Prototype mir_verify command
#1904
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
RyanGlScott
commented
Aug 10, 2023
Comment on lines
-56
to
-68
| -- | 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 |
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
Similarly, this code now lives in SAWScript.Crucible.MIR.MethodSpecIR, as I needed to use the various type family instances in saw-script.
| TopLevel MIRSpec | ||
| ~~~~ | ||
|
|
||
| ### Running a MIR-based verification |
There was a problem hiding this comment.
This manual section is an interesting read, as it describes the conventions that SAW uses when looking up MIR identifiers.
Comment on lines
+67
to
+71
| -- | 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 |
There was a problem hiding this comment.
This is a key data type that is used in many places in the MIR backend.
Comment on lines
+347
to
+349
| toMIRType :: | ||
| Cryptol.TValue -> | ||
| Either ToMIRTypeErr Mir.Ty |
There was a problem hiding this comment.
This describes how to convert Cryptol types (TValues) to MIR types (Mir.Tys).
Comment on lines
+839
to
+866
| -- | 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 |
There was a problem hiding this comment.
This function (and everything that it is defined in terms of) is worth a look.
Comment on lines
+1006
to
+1011
| -- | 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 |
There was a problem hiding this comment.
This describes how to convert a MIR type (Mir.Ty) to a Cryptol Type.
Comment on lines
+1045
to
+1057
| -- | 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 |
There was a problem hiding this comment.
This function implements the MIR identifier lookup logic described in the SAW manual.
Comment on lines
+438
to
+444
| valueToSC :: | ||
| Sym -> | ||
| MS.ConditionMetadata -> | ||
| OverrideFailureReason MIR -> | ||
| Cryptol.TValue -> | ||
| MIRVal -> | ||
| OverrideMatcher MIR w Term |
There was a problem hiding this comment.
This describes how to convert a MIRVal to a SAWCore Term.
RyanGlScott
force-pushed
the
T1859-basic-mir-verify
branch
from
5deb6b1
to
359a881
Compare
RyanGlScott
force-pushed
the
T1859-basic-mir-verify
branch
2 times, most recently
from
c01a82c
to
1e68229
Compare
29 tasks
RyanGlScott
force-pushed
the
T1859-basic-mir-verify
branch
from
1e68229
to
0e24394
Compare
bboston7
approved these changes
Aug 22, 2023
There was a problem hiding this comment.
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)"
RyanGlScott
force-pushed
the
T1859-basic-mir-verify
branch
from
0e24394
to
634b884
Compare
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
force-pushed
the
T1859-basic-mir-verify
branch
from
634b884
to
8930c8a
Compare
RyanGlScott
added
the
ready-to-merge
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This implements just enough scaffolding to support the basics of a
mir_verifycommand 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_todo not work yet.structorenumtypes.These limitations notwithstanding, it is now possible to write MIR specifications for very simple functions such as the ones in the
test_mir_verify_basicintegration 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_verifyallows 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.