Lots of code duplication in src/SAWScript/JVM #379
Labels
subsystem: crucible-jvm
Issues related to Java verification with crucible-jvm
subsystem: crucible-llvm
Issues related to LLVM bitcode verification with crucible-llvm
subsystem: crucible-mir
Issues related to Rust verification with crucible-mir and/or mir-json
tech debt
Issues that document or involve technical debt
type: bug
Issues reporting bugs or unexpected/unwanted behavior
Milestone
Comments
brianhuffman
added
the
subsystem: crucible-jvm
langston-barrett
added a commit
to langston-barrett/saw-script
that referenced
this issue
Jun 7, 2019
langston-barrett
added a commit
to langston-barrett/saw-script
that referenced
this issue
Jun 7, 2019
langston-barrett
added a commit
that referenced
this issue
Jun 11, 2019
* Add a Crucible.Common module for slight code de-duplication Progress on #379 * More deduplication between Crucible(LLVM|JVM)
|
With the merge of #495, the bulk of the remaining work is in |
This was referenced Aug 8, 2019
RyanGlScott
added
the
subsystem: crucible-mir
|
I will be contributing to this as well with the upcoming MIR backend. While I have made an effort to deduplicate a small number of functions that are shared between backends, there remains a grander challenge of figuring out how to deduplicate the common "glue code" that stitches together everything in I don't have any bright ideas for how to do so at the moment. Perhaps we need a type class/data type to abstract over the backend-specific functionality and implement the glue code in terms of this, which could be used across all backends. It's not clear to me what the consequences of this design would be, and I imagine that we'd have to be careful to respect all of the tiny differences among all the backends. |
RyanGlScott
added
the
subsystem: crucible-llvm
RyanGlScott
added a commit
that referenced
this issue
Aug 10, 2023
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
added a commit
that referenced
this issue
Aug 11, 2023
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
added a commit
that referenced
this issue
Aug 17, 2023
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
added a commit
that referenced
this issue
Aug 18, 2023
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
added a commit
that referenced
this issue
Aug 22, 2023
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
added a commit
that referenced
this issue
Aug 22, 2023
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
added a commit
that referenced
this issue
Aug 22, 2023
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.
sauclovian-g
added
the
type: bug
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
The modules implementing the crucible-jvm functionality (
src/SAWScript/JVM/Crucible*.hs) contain a lot of duplicate code that was cut-and-pasted fromsrc/SAWScript/Crucible*.hswith small modifications.This will be problematic to maintain in its current state. The common code needs to be refactored to reduce the duplication.
The text was updated successfully, but these errors were encountered: