You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Currently, mir-json effectively has two modes of operation:
Compile Rust code against the modified version of the Rust standard libraries that ship with crux-mir (here).
Compile Rust code against the versions of the Rust standard libraries that come included with rustc.
If the CRUX_RUST_LIBRARY_PATH environment variable (or, equivalently, SAW_RUST_LIBRARY_PATH) is defined when invoking mir-json, then mode (1) is chosen. Otherwise, mode (2) is chosen.
The thing is, mode (2) is very rarely what you want. This is because mir-json is almost always used in tandem with crux-mir or SAW, and as a result, you really want to emit MIR JSON that is compatible with Crucible. The Rust standard library code that comes included with rustc does not meet this requirement for two reasons:
It does not include the custom tweaks needed to avoid code that Crucible cannot handle.
It is optimized (unlike the custom standard libraries shipped with crux-mir), which means that inlining functions might expose lower-level functions that Crucible either cannot handle or does not have overrides for.
However, it is far too easy for a mir-json user to forget to define {CRUX,SAW}_RUST_LIBRARY_PATH and accidentally end up in mode (2), which can lead to confusing errors that would not happen under mode (1). (See GaloisInc/crucible#1179 for an example where I fell victim to this confusion myself!)
As a result, I'd like to propose that mir-json should require setting {CRUX,SAW}_RUST_LIBRARY_PATH by default, throwing an error message if they aren't set. It is still possible that a user might want to run crux-mir in mode (2) for debugging purposes, but they should be required to pass an additional flag or environment variable that acknowledges the user knows the risks that they are getting themselves into.
The text was updated successfully, but these errors were encountered:
Currently,
mir-json
effectively has two modes of operation:crux-mir
(here).rustc
.If the
CRUX_RUST_LIBRARY_PATH
environment variable (or, equivalently,SAW_RUST_LIBRARY_PATH
) is defined when invokingmir-json
, then mode (1) is chosen. Otherwise, mode (2) is chosen.The thing is, mode (2) is very rarely what you want. This is because
mir-json
is almost always used in tandem withcrux-mir
or SAW, and as a result, you really want to emit MIR JSON that is compatible with Crucible. The Rust standard library code that comes included withrustc
does not meet this requirement for two reasons:crux-mir
), which means that inlining functions might expose lower-level functions that Crucible either cannot handle or does not have overrides for.However, it is far too easy for a
mir-json
user to forget to define{CRUX,SAW}_RUST_LIBRARY_PATH
and accidentally end up in mode (2), which can lead to confusing errors that would not happen under mode (1). (See GaloisInc/crucible#1179 for an example where I fell victim to this confusion myself!)As a result, I'd like to propose that
mir-json
should require setting{CRUX,SAW}_RUST_LIBRARY_PATH
by default, throwing an error message if they aren't set. It is still possible that a user might want to runcrux-mir
in mode (2) for debugging purposes, but they should be required to pass an additional flag or environment variable that acknowledges the user knows the risks that they are getting themselves into.The text was updated successfully, but these errors were encountered: