Simple CLI for macaw-symbolic #390
Conversation
langston-barrett
force-pushed
the
lb/cli
branch
3 times, most recently
from
f5652b2 to
ed41178
Compare
| import Data.Macaw.Discovery qualified as MD | ||
| import Data.Macaw.Memory.ElfLoader.PLTStubs qualified as MPLT | ||
| import Data.Macaw.Symbolic qualified as MS | ||
| import Data.Macaw.Symbolic.Testing qualified as MST |
There was a problem hiding this comment.
We are now using Data.Macaw.Symbolic.Testing for reasons beyond just simple testing. I wonder if we should consider migrating the name to something more appropriate. (Data.Macaw.Symbolic.Driver, perhaps?)
There was a problem hiding this comment.
I've also observed that Data.Macaw.Symbolic.Testing has some peculiar conventions that we may not want to use in macaw-cli. For instance, Data.Macaw.Symbolic.Testing won't take assumptions into account when checking an entrypoint function unless it begins with the prefix "test_and_verify_", so most functions won't check if they use the memory model in valid ways. This seems undesirable for macaw-cli's needs.
Perhaps we could factor out the code used in common between Data.Macaw.Symbolic.Testing and the new module we use to power macaw-cli (be it named Data.Macaw.Symbolic.Driver or something else).
|
@langston-barrett, what are your plans for this PR now that #423 has landed? #423 only adds support for S-expression programs, whereas this PR is about binaries. Do you want to extend |
I don't have further plans for this PR; as we've discussed in other forums, we should likely work towards a CLI that ingests binaries, but the testing harness code I'ver reused here is actually not reusable enough to suit this purpose. Instead, we should do a larger refactor of Macaw's APIs to make it easier to create frontends, and spend more effort creating one that has all of the conventions and functionality we actually think it should. |
Fixes #389.