Add a concrete syntax for macaw #247
Conversation
travitch
force-pushed
the
tr/macaw-syntax
branch
from
73a77af to
a56553b
Compare
| -- * @(instruction-start addr decoded-asm-text)@ | ||
| -- * @(write-memory addr mem-rep value)@ | ||
| -- * @(cond-write-memory cond addr mem-rep value)@ | ||
| -- * @(reg := rhs)@ |
There was a problem hiding this comment.
The Lisper in me is somewhat weirded out by the fact that this is (reg := rhs) and not (:= reg rhs), especially since this is (AFAICT) the only operator that is given infix treatment.
| , nonceGen :: PN.NonceGenerator (ST ids) ids | ||
| } | ||
|
|
||
| data ParserState arch ids = |
There was a problem hiding this comment.
| data ParserState arch ids = | |
| newtype ParserState arch ids = |
There was a problem hiding this comment.
I'll do that if the parser state doesn't gain any additional fields by the time I'm done with the implementation
| | AddressWord !Natural -- ^ An arbitrary address rendered in hex ('ArchAddrWord') | ||
| | SegmentOffset !Natural -- ^ A segment offset address rendered in hex (validation against the Memory object is required) | ||
| | Integer_ !Integer -- ^ Literal integers | ||
| | Natural_ !Natural -- ^ Literal naturals |
There was a problem hiding this comment.
What exactly is the difference between a Natural and an Integer? Is an Integer just a Natural with a ± sign? I ask since there are some operations that seem to require an Integer rather than a Natural argument, such as bv, whose second argument must be an Integer. Does this imply that bv 8 +0 is legal but bv 8 0 is illegal?
There was a problem hiding this comment.
I haven't decided yet. There are a bunch of places where a negative number is not legal but where I don't want to have partial cases due to range checks on Integer. My current thought is that I would require a sign on Integer (even for positive numbers), making all unsigned values Natural.
I think your observation about bv is good (and pointing out an error in the code): I would prefer that it be (bv 8 0) (i.e., the actual value is also a Natural).
Note that this entire syntax is not really meant for human consumption at all. This will all be machine generated and machine parsed. It is only textual so that I don't go crazy debugging it, so I don't mind if it is ugly.
travitch
force-pushed
the
tr/macaw-syntax
branch
from
a56553b to
05e8df0
Compare
This will enable caching analysis results in a text format that can be parsed much more efficiently than re-running the entire fixed point analysis.
travitch
force-pushed
the
tr/macaw-syntax
branch
from
05e8df0 to
922cf45
Compare
This will enable caching analysis results in a text format that can be parsed
much more efficiently than re-running the entire fixed point analysis.