-
Notifications
You must be signed in to change notification settings - Fork 7
Implement parser support #51
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
base: main
Are you sure you want to change the base?
Changes from all commits
6e81a99
b9b15b5
fb7e374
df6cd3f
1027dda
237dacd
958a5b9
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change | ||||||||||||||||||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
|
|
@@ -321,6 +321,7 @@ let parse_annots (m : module_) : Custom.section list = | |||||||||||||||||||||||||||||||||||||||||
| %token VEC_SHUFFLE | ||||||||||||||||||||||||||||||||||||||||||
| %token<Ast.laneidx -> Ast.instr'> VEC_EXTRACT VEC_REPLACE | ||||||||||||||||||||||||||||||||||||||||||
| %token FUNC START TYPE PARAM RESULT LOCAL GLOBAL | ||||||||||||||||||||||||||||||||||||||||||
| %token PAGESIZE | ||||||||||||||||||||||||||||||||||||||||||
| %token TABLE ELEM MEMORY TAG DATA DECLARE OFFSET ITEM IMPORT EXPORT | ||||||||||||||||||||||||||||||||||||||||||
| %token MODULE BIN QUOTE DEFINITION INSTANCE | ||||||||||||||||||||||||||||||||||||||||||
| %token SCRIPT REGISTER INVOKE GET | ||||||||||||||||||||||||||||||||||||||||||
|
|
@@ -465,8 +466,16 @@ subtype : | |||||||||||||||||||||||||||||||||||||||||
| tabletype : | ||||||||||||||||||||||||||||||||||||||||||
| | addrtype limits reftype { fun c -> TableT ($1, $2, $3 c) } | ||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||
| pagetype : | ||||||||||||||||||||||||||||||||||||||||||
| | LPAR PAGESIZE NAT RPAR | ||||||||||||||||||||||||||||||||||||||||||
| { let n = (nat32 $3 $loc($3)) in | ||||||||||||||||||||||||||||||||||||||||||
| if not (Lib.Int32.is_power_of_two_unsigned n) then | ||||||||||||||||||||||||||||||||||||||||||
| error (at $sloc) "invalid custom page size: must be power of two"; | ||||||||||||||||||||||||||||||||||||||||||
| PageT (Int32.to_int (Lib.Int32.log2_unsigned n)) } | ||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||
| memorytype : | ||||||||||||||||||||||||||||||||||||||||||
| | addrtype limits { fun c -> MemoryT ($1, $2, PageT 16) } | ||||||||||||||||||||||||||||||||||||||||||
| | addrtype limits pagetype { fun c -> MemoryT ($1, $2, $3) } | ||||||||||||||||||||||||||||||||||||||||||
|
Comment on lines
+469
to
+478
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Hint: if you declare pagetype inline, then you can factor the empty case into it without having to duplicate rules at use sites:
Suggested change
|
||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||
| limits : | ||||||||||||||||||||||||||||||||||||||||||
| | NAT { {min = nat64 $1 $loc($1); max = None} } | ||||||||||||||||||||||||||||||||||||||||||
|
|
@@ -1125,16 +1134,17 @@ memory_fields : | |||||||||||||||||||||||||||||||||||||||||
| [Import (fst $1, snd $1, ExternMemoryT ($2 c)) @@ loc], [] } | ||||||||||||||||||||||||||||||||||||||||||
| | inline_export memory_fields /* Sugar */ | ||||||||||||||||||||||||||||||||||||||||||
| { fun c x loc -> let mems, data, ims, exs = $2 c x loc in | ||||||||||||||||||||||||||||||||||||||||||
| mems, data, ims, $1 (MemoryX x) c :: exs } | ||||||||||||||||||||||||||||||||||||||||||
| | addrtype LPAR DATA string_list RPAR /* Sugar */ | ||||||||||||||||||||||||||||||||||||||||||
| mems, data, ims, $1 (MemoryX x) c :: exs } | ||||||||||||||||||||||||||||||||||||||||||
|
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
|
||||||||||||||||||||||||||||||||||||||||||
| | addrtype pagetype LPAR DATA string_list RPAR /* Sugar */ | ||||||||||||||||||||||||||||||||||||||||||
|
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. The pagetype needs to be optional (independently of the addrtype) in the presence of inline data, otherwise this would be a breaking change. You'll probably need two productions to handle this without s/r conflict. |
||||||||||||||||||||||||||||||||||||||||||
| { fun c x loc -> | ||||||||||||||||||||||||||||||||||||||||||
| let size = Int64.(div (add (of_int (String.length $4)) 65535L) 65536L) in | ||||||||||||||||||||||||||||||||||||||||||
| let PageT ps = $2 in | ||||||||||||||||||||||||||||||||||||||||||
| let page_size = Int64.shift_left 1L ps in | ||||||||||||||||||||||||||||||||||||||||||
| let size = Int64.(div (add (of_int (String.length $5)) (sub page_size 1L)) page_size) in | ||||||||||||||||||||||||||||||||||||||||||
| let offset = [at_const $1 (0L @@ loc) @@ loc] @@ loc in | ||||||||||||||||||||||||||||||||||||||||||
| [Memory (MemoryT ($1, {min = size; max = Some size}, PageT 16)) @@ loc], | ||||||||||||||||||||||||||||||||||||||||||
| [Data ($4, Active (x, offset) @@ loc) @@ loc], | ||||||||||||||||||||||||||||||||||||||||||
| [Memory (MemoryT ($1, {min = size; max = Some size}, $2)) @@ loc], | ||||||||||||||||||||||||||||||||||||||||||
| [Data ($5, Active (x, offset) @@ loc) @@ loc], | ||||||||||||||||||||||||||||||||||||||||||
| [], [] } | ||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||
| elemkind : | ||||||||||||||||||||||||||||||||||||||||||
| | FUNC { (NoNull, FuncHT) } | ||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||||||||||||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -313,9 +313,17 @@ struct | |
| if n = 1l then acc else loop (Int32.add acc 1l) (Int32.shift_right_logical n 1) in | ||
| loop 0l n | ||
|
|
||
| let log2_unsigned n = | ||
|
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Nit: Redefine log2 in terms of log2_unsigned, as in Int64. |
||
| let rec loop acc n = | ||
| if n = 1l then acc else loop (Int32.add acc 1l) (Int32.shift_right_logical n 1) in | ||
| loop 0l n | ||
|
|
||
| let is_power_of_two n = | ||
| if n < 0l then failwith "is_power_of_two"; | ||
| n <> 0l && Int32.(logand n (sub n 1l)) = 0l | ||
|
|
||
| let is_power_of_two_unsigned n = | ||
| n <> 0l && Int32.(logand n (sub n 1l)) = 0l | ||
| end | ||
|
|
||
| module Int64 = | ||
|
|
||
| Original file line number | Diff line number | Diff line change | ||||||||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
|
|
@@ -105,7 +105,7 @@ let check_limits {min; max} range at msg = | |||||||||||||||||||||||||||||||
| "size minimum must not be greater than maximum" | ||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||
| let check_pagetype (PageT ps) at = | ||||||||||||||||||||||||||||||||
| require (ps = 16 || ps = 0) at "page size must be 1 or 64KiB" | ||||||||||||||||||||||||||||||||
| require (ps = 16 || ps = 0) at "invalid custom page size" | ||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||
| let check_numtype (c : context) (t : numtype) at = | ||||||||||||||||||||||||||||||||
| () | ||||||||||||||||||||||||||||||||
|
|
@@ -200,13 +200,19 @@ let check_globaltype (c : context) (gt : globaltype) at = | |||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||
| let check_memorytype (c : context) (mt : memorytype) at = | ||||||||||||||||||||||||||||||||
| let MemoryT (at_, lim, pt) = mt in | ||||||||||||||||||||||||||||||||
| check_pagetype pt at; | ||||||||||||||||||||||||||||||||
| let sz, s = | ||||||||||||||||||||||||||||||||
| match at_ with | ||||||||||||||||||||||||||||||||
| | I32AT -> 0x1_0000L, "2^16 pages (4 GiB) for i32" | ||||||||||||||||||||||||||||||||
| | I64AT -> 0x1_0000_0000_0000L, "2^48 pages (256 TiB) for i64" | ||||||||||||||||||||||||||||||||
| match pt with | ||||||||||||||||||||||||||||||||
| | PageT 16 -> | ||||||||||||||||||||||||||||||||
| (match at_ with | ||||||||||||||||||||||||||||||||
| | I32AT -> 0x1_0000L, "2^16 pages (4 GiB) for i32" | ||||||||||||||||||||||||||||||||
| | I64AT -> 0x1_0000_0000_0000L, "2^48 pages (256 TiB) for i64") | ||||||||||||||||||||||||||||||||
| | _ -> (* TODO: divide by page size, what about error msg? *) | ||||||||||||||||||||||||||||||||
| (match at_ with | ||||||||||||||||||||||||||||||||
| | I32AT -> 0xFFFF_FFFFL, "2^32 - 1 bytes for i32" | ||||||||||||||||||||||||||||||||
| | I64AT -> 0xFFFF_FFFF_FFFF_FFFFL, "2^64 - 1 bytes for i64") | ||||||||||||||||||||||||||||||||
|
Comment on lines
+205
to
+213
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
|
||||||||||||||||||||||||||||||||
| in | ||||||||||||||||||||||||||||||||
| check_limits lim sz at ("memory size must be at most " ^ s); | ||||||||||||||||||||||||||||||||
| check_pagetype pt at | ||||||||||||||||||||||||||||||||
| check_limits lim sz at ("memory size must be at most " ^ s) | ||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||
| let check_tabletype (c : context) (tt : tabletype) at = | ||||||||||||||||||||||||||||||||
| let TableT (at_, lim, t) = tt in | ||||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.