Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Split out crucible-mir from crux-mir #1065

Closed
RyanGlScott opened this issue Mar 13, 2023 · 0 comments · Fixed by #1066
Closed

Split out crucible-mir from crux-mir #1065

RyanGlScott opened this issue Mar 13, 2023 · 0 comments · Fixed by #1066
Assignees
@RyanGlScott
Labels
crucible crux MIR Issues relating to Rust/MIR support technical debt

Comments

@RyanGlScott
Copy link
Contributor

RyanGlScott commented Mar 13, 2023 •
edited
Loading

Currently, crux-mir is a mega-library that contains both the code needed to (1) simulate MIR code with crucible, and (2) define a crux frontent for MIR. This arrangement is somewhat painful for code that wants to do (1) without needing (2), however. I propose that we:

  • Create a new crucible-mir library, which exports most of the current code in today's crux-mir. This library would not have a dependency on crux.
  • Change crux-mir to depend on crucible-mir, and have it export any additional functionality that requires crux.

One interesting case is generateMIR in Mir.Generate, which runs mir-json on the input to generate JSON. This is really only needed for crux-mir's purposes, so this function deserves to live in crux-mir, not crucible-mir. On the other hand, the parseMir and translateMIR functions in that module make sense to put in crucible-mir, so we should create a new module for them.

See GaloisInc/saw-script#1839 for the corresponding issue on the SAW side.
@RyanGlScott RyanGlScott added crucible crux technical debt MIR Issues relating to Rust/MIR support labels Mar 13, 2023
@RyanGlScott RyanGlScott self-assigned this Mar 13, 2023
@RyanGlScott RyanGlScott mentioned this issue Mar 13, 2023
Closed
RyanGlScott added a commit that referenced this issue Mar 13, 2023
@RyanGlScott
Split out crucible-mir from crux-mir
57caee6 
For the most part, most code was moved wholesale from `crux-mir` with only
minor changes (I removed redundant imports to more easily determine which
library dependencies could be dropped in `crucible-mir`). The most unusual
change was creating a new `Mir.ParseTranslate` module in `crucible-mir`, which
contains the `parseMIR` and `translateMIR` functions previously defined in
`Mir.Generate` (now a `crux-mir` module that only exports `generateMIR`).

Fixes #1065.
RyanGlScott added a commit that referenced this issue Mar 13, 2023
@RyanGlScott
Split out crucible-mir from crux-mir
82367aa 
For the most part, most code was moved wholesale from `crux-mir` with only
minor changes (I removed redundant imports to more easily determine which
library dependencies could be dropped in `crucible-mir`). The most unusual
change was creating a new `Mir.ParseTranslate` module in `crucible-mir`, which
contains the `parseMIR` and `translateMIR` functions previously defined in
`Mir.Generate` (now a `crux-mir` module that only exports `generateMIR`).

Fixes #1065.
@RyanGlScott RyanGlScott mentioned this issue Mar 13, 2023
Merged
RyanGlScott added a commit that referenced this issue Mar 14, 2023
@RyanGlScott
Split out crucible-mir from crux-mir (#1066)
4b8e481 
For the most part, most code was moved wholesale from `crux-mir` with only
minor changes (I removed redundant imports to more easily determine which
library dependencies could be dropped in `crucible-mir`). The most unusual
change was creating a new `Mir.ParseTranslate` module in `crucible-mir`, which
contains the `parseMIR` and `translateMIR` functions previously defined in
`Mir.Generate` (now a `crux-mir` module that only exports `generateMIR`).

Fixes #1065.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@RyanGlScott RyanGlScott

Labels
crucible crux MIR Issues relating to Rust/MIR support technical debt
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Split out crucible-mir from crux-mir GaloisInc/crucible
1 participant
@RyanGlScott