crucible{,-llvm}-syntax: Evaluating programs with syntax extensions

[langston-barrett]

Fixes #1115.

• Changes the type of SimulateProgramHooks to bind an ext variable, so hooks can be extension-specific
• Adds a simulation hook that can run an arbitrary override action before simulation (necessary for initializing LLVM memory global variable)
• Adds a exec-crucible-llvm executable based on crucibler - has lots of shared code with crucibler, but is also substantially different, so not sure if more sharing is feasible
• Adds a test for simulating Crucible-LLVM extension statements

[RyanGlScott]

Adds a exec-crucible-llvm executable based on crucibler - has lots of shared code with crucibler, but is also substantially different, so not sure if more sharing is feasible

I might be missing something, but the code in exec-crucible-llvm doesn't seem that different to me. At a glance, the big differences that stand out are:

1. exec-crucible-llvm uses a different ExtensionImpl
2. exec-crucible-llvm uses a different setupHook
3. exec-curcible-llvm uses a different ParserHooks

Am I missing something? If that's it, I could definitely imagine factoring out a large chunk of the functionality that is shared in common between crucibler and exec-crucible-llvm, including the three things above as arguments to the function.

(As a side note, I've never understand why it's named crucibler in the first place. I was going to suggest naming the other tool something like crucibler-llvm, but I'm not sure if it's a convention worth keeping.)

[langston-barrett]

Am I missing something? If that's it, I could definitely imagine factoring out a large chunk of the functionality that is shared in common between crucibler and exec-crucible-llvm, including the three things above as arguments to the function.

No, you're right - I guess the real question is: Where should that shared code go, given that it mostly consists of optparse-applicative setup? I would say probably not in crucible-syntax itself, as there's no reason for library clients to need to build optparse-applicative and that module. Do we want to make a new package (crucible-exec?) for sharing code between crucible-syntax frontends?

[RyanGlScott]

I was thinking of moving most of this functionality to Lang.Crucible.Syntax.Prog. We could have a function of (roughly) this type:

Command -> ExtensionImpl -> ParserHooks -> SimulatorHooks -> IO ()

Where Command is the data type that encodes which of the crucibler/exec-crucible-llvm subcommands you want to run. Then, each executable can instantiate this function as needed and define the necessary optparse-applicative logic to parse command-line arguments into a Command.

[langston-barrett]

I was thinking of moving most of this functionality to Lang.Crucible.Syntax.Prog.

Done.

I don't love this solution, as library clients still need to build code they don't need (Prog.hs), and the CLIs still need to copy-paste code (optparse-applicative setup). But I think it's better than it was before, so thank you for the suggestion!

In the future, it might be nice to create a crucible-cli package or similar that provides the functionality of Prog.hs, in addition to the optparse-applicative bits, and then have crucible-cli, crucible-llvm-cli, etc. executables that are all thin wrappers over the crucible-cli library that instantiate it with the proper syntax extension. In addition to the current functionality (check/simulate/repl), we could also expose reading and then pretty-printing CFGs from actual code (e.g., LLVM bitcode modules), and perhaps add some debugging-oriented execution features that could be used with simulate.

[RyanGlScott]

I'm broadly aligned with the goal of factoring out the CLI-related bits, although we certainly don't have to hold up this PR on that.

Everything else looks great!