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

Add a concrete syntax for macaw #247

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

Add a concrete syntax for macaw #247

wants to merge 1 commit into from

Conversation

travitch
Copy link
Contributor

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.

-- * @(instruction-start addr decoded-asm-text)@
-- * @(write-memory addr mem-rep value)@
-- * @(cond-write-memory cond addr mem-rep value)@
-- * @(reg := rhs)@
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 =
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
data ParserState arch ids =
newtype ParserState arch ids =

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants