diff --git a/aeneas/src/vst/Parser.v3 b/aeneas/src/vst/Parser.v3 index b70c78bff..5fbf7ad2f 100644 --- a/aeneas/src/vst/Parser.v3 +++ b/aeneas/src/vst/Parser.v3 @@ -152,7 +152,9 @@ component Parser { if (optKeyword(p, "component") != null) return parseComponent(p, file, true); if (optKeyword(p, "type") != null) return parseVariant(p, file, true); if (optKeyword(p, "enum") != null) return parseEnum(p, file, true); + if (optKeyword(p, "packing") != null) return parsePackingDecl(p, file, true); } + if (optKeyword(p, "packing") != null) return parsePackingDecl(p, file, false); } 'l' => { if (optKeyword(p, "layout") != null) return parseLayout(p, file); @@ -204,37 +206,56 @@ component Parser { var size = u8.!(V3.unboxI32(sizeLiteral.val)); return (param, size); } - def parsePackingBits(p: ParserState) -> string { - p.req1('0'); - if (p.curByte == 'b' || p.curByte == 'B') p.eat1(); - else p.error("expected bit pattern"); - - var s = p.curPos, q = p.curPos; - var chars = Vector.new(); - while (q < p.input.length) { - var c = p.input[q]; - if (c == '0' || c == '1' || c == '?' || Char.isIdentStart(c)) chars.put(c); - else if (c != '_') break; - q++; + def parsePackingSize(p: ParserState) -> u8 { + var sizeLiteral = parseIntLiteral(p); + if (sizeLiteral == null) { + p.error("size expected"); + return 0; } - p.advance(q - s); - return chars.array; + else return u8.!(V3.unboxI32(sizeLiteral.val)); } - def parsePacking(p: ParserState) -> VstPacking { + def parsePackingExpr(p: ParserState) -> VstPackingExpr { + var s = p.curPos, q = p.curPos; + var isBitPattern = false; + if (p.peek(0) == '0' && p.peek(1) == 'b') { + // could be a bit pattern, try parsing it + q += 2; + var chars = Vector.new(); + while (q < p.input.length) { + var c = p.input[q]; + if (c == '0' || c == '1' || c == '?' || Char.isIdentStart(c)) chars.put(c); + else if (c != '_') break; + if (c == '?' || Char.isIdentStart(c)) isBitPattern = true; + q++; + } + + if (isBitPattern) { + p.advance(q - s); + return VstPackingExpr.Bits(chars.array); + } + } else if (p.curByte == '(') { + // Tuple + return VstPackingExpr.Tuple(parseList(0, p, '(', COMMA, ')', parsePackingExpr)); + } else if (Char.isIdentStart(p.curByte)) { + // Application or Field + var id = parseIdentVoid(p).name; + if (p.curByte == '(') return VstPackingExpr.App(id, parseList(0, p, '(', COMMA, ')', parsePackingExpr)); + else return VstPackingExpr.Field(id); + } + // Literal + return VstPackingExpr.Literal(parseExpr(p)); + } + def parsePackingDecl(p: ParserState, file: VstFile, isPrivate: bool) -> bool { var id = parseIdentVoid(p).name; var params = parseList(0, p, '(', COMMA, ')', parsePackingParam); - var bits = parsePackingBits(p); - return VstPacking.new(id, params, bits); - } - def parsePacking(p: ParserState) -> VstPacking { - if (Char.isIdentStart(p.curByte)) { - var packingName = parseIdentVoid(p); - var fields = parseTupleExpr(p); - return VstPacking.Params(packingName.name, fields.exprs); - } else { - p.error("expected packing parameter"); - return VstPacking.Bits([]); - } + p.req1(':'); + var size = parsePackingSize(p); + p.req1('='); + var expr = parsePackingExpr(p); + p.req1(';'); + var decl = VstPackingDecl.new(id, params, expr, size); + file.packings.put(decl); + return true; } def parseRepHints(p: ParserState) -> List { var list: List; @@ -252,8 +273,8 @@ component Parser { var result: VstRepHint; match (id.kwClass) { Keywords.KC_PACKING => { - var p = parsePacking(p); - result = VstRepHint.Packing(p); + var e = parsePackingExpr(p); + result = VstRepHint.Packing(e); } 0 => { if (Strings.equal(name, "boxed")) result = VstRepHint.Boxed; diff --git a/aeneas/src/vst/Verifier.v3 b/aeneas/src/vst/Verifier.v3 index da6b962e3..55640a407 100644 --- a/aeneas/src/vst/Verifier.v3 +++ b/aeneas/src/vst/Verifier.v3 @@ -84,6 +84,7 @@ class Verifier(compiler: Compiler, prog: Program) { if (prev != null) layoutDecl.verifier.TypeRedefined(layoutDecl.token); prog.layouts[name] = layoutDecl; } + prog.vst.packings.putv(file.packings); prog.vst.exports.putv(file.exports); } def addInitFor(decl: VstCompound) { diff --git a/aeneas/src/vst/Vst.v3 b/aeneas/src/vst/Vst.v3 index 4ae98a777..fabb2e530 100644 --- a/aeneas/src/vst/Vst.v3 +++ b/aeneas/src/vst/Vst.v3 @@ -8,6 +8,7 @@ class VstModule { def enums = Vector.new(); def exports = Vector.new(); def layouts = Vector.new(); + def packings = Vector.new(); var files: Array; // all files, in order specified on command line var numComponents: int; // total number of components var numStrings: int; // total number of string constants @@ -19,6 +20,7 @@ class VstFile extends ParsedFile { def enums = Vector.new(); def exports = Vector.new(); def layouts = Vector.new(); + def packings = Vector.new(); var synthetic: VstComponent; // declaration for synthesized component var typeEnv: TypeEnv; @@ -378,20 +380,24 @@ class SuperClause { type VstRepHint { case Boxed; case Unboxed; - case Packing(p: VstPacking); + case Packing(p: VstPackingExpr); case Other(hint: string); } type VstPackingExpr { - case Expr(e: Expr); // Either Literal, Variable or Tuple - case ScalarExpr(scalar: VstScalar, params: VstList); + case Bits(rep: string); + case Tuple(l: VstList); + case App(p: Token, args: VstList); + case Field(f: Token); + case Literal(e: Expr); } -class VstScalar extends Decl { +class VstPackingDecl extends Decl { def params: VstList<(Token, u8)>; - def bits: string; + def expr: VstPackingExpr; + def size: u8; - new(token: Token, params: VstList<(Token, u8)>, bits: string) super(token) {} + new(token: Token, params, expr, size) super(token) {} } class VstVisitor { diff --git a/aeneas/src/vst/VstPrinter.v3 b/aeneas/src/vst/VstPrinter.v3 index ef9281678..d2dc4e9eb 100644 --- a/aeneas/src/vst/VstPrinter.v3 +++ b/aeneas/src/vst/VstPrinter.v3 @@ -104,7 +104,7 @@ class Printer(printer: VstPrinter) { Unboxed => Terminal.put("#unboxed"); Packing(p) => { Terminal.put("#packing "); - printPacking(p); + printPackingExpr(p); } Other(s) => Terminal.put1("#%s", s); } @@ -112,16 +112,33 @@ class Printer(printer: VstPrinter) { def printToken(t: Token) { Terminal.put1("%s", t.image); } - def printPacking(p: VstPacking) { + def printPackingExpr(p: VstPackingExpr) { match (p) { Bits(b) => Terminal.put1("0b%s", b); - Params(packingName, params) => { - Terminal.put1("%s(", packingName.image); - printCommaList(params.list, printer.printExpr(_, 1)); + Literal(e) => printer.printExpr(e, 0); + App(p, args) => { + Terminal.put1("%s(", p.image); + printCommaList(args.list, printPackingExpr); Terminal.put(")"); } + Tuple(l) => { + Terminal.put("("); + printCommaList(l.list, printPackingExpr); + Terminal.put(")"); + } + Field(f) => Terminal.put1("%s", f.image); } } + def printPackingParam(param: (Token, u8)) { + Terminal.put2("%s: %d", param.0.image, param.1); + } + def printPacking(p: VstPackingDecl) { + Terminal.put1("packing %s(", p.token.image); + printCommaList(p.params.list, printPackingParam); + Terminal.put1("): %d = ", p.size); + printPackingExpr(p.expr); + Terminal.put(";\n"); + } def simple(name: string, indent: int) { enter(name, indent); exit(); @@ -166,6 +183,7 @@ class VstPrinter extends VstVisitor { def printProgram(prog: Program) { prog.vst.components.apply(p.printComponent); prog.vst.classes.apply(p.printClass); + prog.vst.packings.apply(p.printPacking); } def visitIf(stmt: IfStmt, indent: int) { p.enter("IfStmt", indent); diff --git a/test/variants/parser/packing08.v3 b/test/variants/parser/packing08.v3 index 78a8ac9f5..4a933f9ec 100644 --- a/test/variants/parser/packing08.v3 +++ b/test/variants/parser/packing08.v3 @@ -1,2 +1,2 @@ //@parse -packing MyScalar(a: 16, b: 16) = 0baaaa_aaaa_aaaa_aaaa_bbbb_bbbb_bbbb_bbbb; \ No newline at end of file +packing MyScalar(a: 16, b: 16): 32= 0baaaa_aaaa_aaaa_aaaa_bbbb_bbbb_bbbb_bbbb; \ No newline at end of file diff --git a/test/variants/parser/packing09.v3 b/test/variants/parser/packing09.v3 index a79c2709a..c903f99d7 100644 --- a/test/variants/parser/packing09.v3 +++ b/test/variants/parser/packing09.v3 @@ -1,2 +1,3 @@ //@parse -packing MyScalar(a: 16, b: 16): 32 = 0baaaa_aaaa_aaaa_aaaa_bbbb_bbbb_bbbb_bbbb; \ No newline at end of file +packing MyScalar(a: 16, b: 16): 32 = 0baaaa_aaaa_aaaa_aaaa_bbbb_bbbb_bbbb_bbbb; +packing MyScalar2(a: 16, b: 16): 32 = MyScalar(a, b); \ No newline at end of file diff --git a/test/variants/parser/packing10.v3 b/test/variants/parser/packing10.v3 index 395adba57..b3c140082 100644 --- a/test/variants/parser/packing10.v3 +++ b/test/variants/parser/packing10.v3 @@ -5,4 +5,4 @@ type T #unboxed { #packing 0b0110_wwww_wwww_wwww_ssss_ssss_0000_ssss; } -packing MyScalar(a: 5, b: 16, c: 8) = 0b010x_xxxx_yyyy_yyyy_yyyy_yyyy_zzzz_zzzz; \ No newline at end of file +packing MyScalar(a: 5, b: 16, c: 8): 32 = 0b010x_xxxx_yyyy_yyyy_yyyy_yyyy_zzzz_zzzz; \ No newline at end of file diff --git a/test/variants/parser/packing12.v3 b/test/variants/parser/packing12.v3 new file mode 100644 index 000000000..46f0f6bff --- /dev/null +++ b/test/variants/parser/packing12.v3 @@ -0,0 +1,8 @@ +//@parse +type T #unboxed { + case A(x: u5, y: u16, z: u8, w: u32) #packing ((x, y, z), w); + case B(x: u5, y: u16, z: u8, w: u32) #packing P2(w, (x, y, z)); +} + +packing P(a: 5, b: 16, c: 8): 32 = 0b010x_xxxx_yyyy_yyyy_yyyy_yyyy_zzzz_zzzz; +packing P2(a: 32, b: 32): 64 = 0baaaa_aaaa_aaaa_aaaa_aaaa_aaaa_aaaa_aaaa_bbbb_bbbb_bbbb_bbbb_bbbb_bbbb_bbbb_bbbb; \ No newline at end of file