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

Packing Declaration Parsing #219

Merged
merged 7 commits into from
Feb 20, 2024
Merged

Packing Declaration Parsing #219

merged 7 commits into from
Feb 20, 2024

Conversation

btwj
Copy link
Contributor

@btwj btwj commented Feb 13, 2024

Introduces VstPackingDecl and VstPackingExpr, allowing for nested packing expressions and packing literals.

@btwj btwj marked this pull request as ready for review February 14, 2024 19:05
p.error("size expected");
return 0;
}
else return u8.!(V3.unboxI32(sizeLiteral.val));
Copy link
Owner

Choose a reason for hiding this comment

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

I think we want to keep this as a literal, so that it can be checked in the Verifier that it's a reasonable size.

case Other(hint: string);
}

type VstPacking {
type VstPackingExpr {
case Bits(rep: string);
Copy link
Owner

Choose a reason for hiding this comment

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

Should we make a variant here for the bits and store an array of them? E.g.

type PackingBit {
  case Literal(val: u1);
  case Wildcard;
  case Char(ch: byte);
}

aeneas/src/vst/Parser.v3 Outdated Show resolved Hide resolved
@btwj btwj requested a review from titzer February 15, 2024 21:01
Copy link
Owner

@titzer titzer left a comment

Choose a reason for hiding this comment

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

Logic looks good, just needs more tests and a bump of the version number.

@@ -0,0 +1,2 @@
//@parse
Copy link
Owner

Choose a reason for hiding this comment

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

Can you add some negative parsing tests as well? Also, some simpler cases with only one field, some parts are missing, etc?

def printPacking(p: VstPacking) {
def printPackingBits(bits: Array<PackingBit>) {
Terminal.put("0b");
for (bit in bits) {
Copy link
Owner

Choose a reason for hiding this comment

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

Maybe add a _ every four or eight bits?

@btwj btwj requested a review from titzer February 19, 2024 18:23
@titzer titzer merged commit 0c87870 into titzer:master Feb 20, 2024
7 checks passed
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