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.

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

Simple CLI frontend for macaw-*-symbolic #389

Closed
langston-barrett opened this issue Jul 3, 2024 · 5 comments
Closed

Simple CLI frontend for macaw-*-symbolic #389

langston-barrett opened this issue Jul 3, 2024 · 5 comments
Labels
symbolic-execution Issues relating to macaw-symbolic and symbolic execution

Comments

@langston-barrett
Copy link
Contributor

Ocassionally, I have a question about macaw-*-symbolic's semantics. The only way I can verify my hypotheses is to run a higher-level tool built on top of Macaw. However, such tools generally have a considerable amount of code related to features other than simply executing machine code, obfuscating the results (e.g., is the problem in Macaw, or in the higher-level tool?).

It would be great if the various macaw-*-symbolic packages had simple command-line interfaces that would just load binaries and start at main with a sensible initial memory and register state. Ideally, these could also support macaw-syntax S-expression programs, a la crucible-cli. We'd likely want to make a generic library (macaw-cli), with instantiations for each particular architecture.

@RyanGlScott
Copy link
Contributor

I would love to have this. Having a tool that just runs macaw-symbolic on binaries (even if it's very barebones) would effectively give us a Crux frontend for binaries. But even if we don't go that far, having a macaw-cli-* tool that only supports S-expression programs would also be very useful.

@RyanGlScott RyanGlScott added the symbolic-execution Issues relating to macaw-symbolic and symbolic execution label Jul 3, 2024
@RyanGlScott
Copy link
Contributor

#423 adds a macaw-x86-cli frontend, which currently only supports Crucible S-expression programs. (See also #390, which aims to ingest binaries.)

@RyanGlScott
Copy link
Contributor

@langston-barrett intends not to pursue a binary frontend for macaw-x86-cli (see #390 (comment)), so I believe this issue can now be closed. If there is additional follow-up work to do to improve macaw-x86-cli, let's file separate issues.

@langston-barrett
Copy link
Contributor Author

FWIW, I think the need for/utility of such a CLI is independent of my intent to implement it in the near-term, i.e., we might consider keeping this issue open even though #390 didn't end up being its solution. However, since we are probably several steps away from a satisfying solution, I can definitely also understand wanting to keep the issue tracker clear of vague, longer-term plans.

@langston-barrett
Copy link
Contributor Author

To expand a bit on the utility of a CLI that ingests binaries, even when we already have one that ingests S-expression programs:

  1. Developing it would hopefully push us in the direction of higher-level, easier-to-use library APIs, and provide an in-repo client of our APIs
  2. It would be useful for debugging patterns that come up in compiler-produced code. In theory, one could print out the Crucible CFG from macaw-symbolic and write an equivalent one in the S-expression syntax, this might be considerably more time-consuming than just copying a small snippet of C code that produces the pattern in question and compiling it (especially given our lack of syntactic sugar, symbolic-syntax: Syntactic sugar #349)
  3. The S-expression syntax is not complete with respect to the language extension's syntactic forms (symbolic-syntax: Concrete syntax for the remaining Macaw syntax formers #346), so not all test-cases can be written in this syntax. Furthermore, architecture-specific extensions don't include syntax for all the architecture-specific operations (x86-cli: Testcase with some x86_64-specific functionality #428), and there are so many of these that we might not realistically support them all in any near-term future.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
symbolic-execution Issues relating to macaw-symbolic and symbolic execution
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants