macaw-symbolic-syntax: Concrete syntax for macaw-symbolic CFGs

[langston-barrett]

Fixes #344. Will require merging and bumping the Crucible submodule to bring in GaloisInc/crucible#1113.

[langston-barrett]

From a conversation with @RyanGlScott:

• The Pointer type now exists in crucible-llvm-syntax and macaw-symbolic-syntax. We should try to unify the surface syntax so that at least simple overrides (e.g., the identity function on pointers) could be shared between them.
• We decided we still like the notion of type aliases that are instantiated for particular target triples. Eventually, we may choose to have more pre-baked target triples in addition to x86_64 Linux.
• We should make the parser match the language extension datatype as closely as possible. This means that we should leave out operations like fresh-vec. Ideally, the crucible-llvm-syntax and macaw-symbolic-syntax parsers would be extensible, so operations such as this would be possible to add in downstream packages.

@RyanGlScott Which parts of the above would you like to see done in this PR vs. deferred?

[RyanGlScott]

This is fantastic. Thanks for digging through ambient-verifier and extracting this out!

(We ended up reviewing some of this patch synchronously, but I wrote some of these comments prior to the synchronous review. I've opted to keep the comments as-is, so if I ask questions below that were already answered during the review, that's why.)

[RyanGlScott]

Oops, we posted our comments at almost the exact same time. To respond to your specific questions:

• The Pointer type now exists in crucible-llvm-syntax and macaw-symbolic-syntax. We should try to unify the surface syntax so that at least simple overrides (e.g., the identity function on pointers) could be shared between them.

See #345 (comment). I don't have a clear sense for how much work it would take to consolidate the two Pointer types, so if it looks daunting, I'm fine with deferring that for later. (There's also a question of whether we'd want to do this at all—I'm on the fence on that point.)

• We decided we still like the notion of type aliases that are instantiated for particular target triples. Eventually, we may choose to have more pre-baked target triples in addition to x86_64 Linux.

Spot on. I suggested (in #345 (comment)) adding one for AArch32 Linux, since we have a more pressing need for that, but I'm fine with deferring other target triples.

• We should make the parser match the language extension datatype as closely as possible. This means that we should leave out operations like fresh-vec. Ideally, the crucible-llvm-syntax and macaw-symbolic-syntax parsers would be extensible, so operations such as this would be possible to add in downstream packages.

Right, see #345 (comment). I think we should omit fresh-vec.