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

[langston-barrett]

Fixes #344. Will require merging and bumping the Crucible submodule to bring in https://github.com/GaloisInc/crucible/pull/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]

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 https://github.com/GaloisInc/macaw/pull/345#discussion_r1380091648. 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 https://github.com/GaloisInc/macaw/pull/345#discussion_r1380262025) 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 https://github.com/GaloisInc/macaw/pull/345#discussion_r1380186676. I think we should omit fresh-vec.