Add the Verify mode
#726
Add the Verify mode
#726
Conversation
zhouwfang
changed the title
Verify modeVerify mode design
zhouwfang
force-pushed
the
add-verify-mode
branch
from
75024f7 to
5dd00cf
Compare
crates/interpreter/src/valid.rs
Outdated
| // expected_target.parser += delta_ip; | ||
| // expected_target.branch_table += delta_stp; |
There was a problem hiding this comment.
The remaining question is how to format and read the side table from the custom section of the WASM module.
In terms of the format, how about using the format that was intended for flash storage?
It may not be efficient to keep the whole side table in RAM. How about keeping a parser for it and reading the data on demand?
There was a problem hiding this comment.
More precisely,
[Section ID: 0]
[Section Size: ...]
[Section Name Length: 18]
[Section Name: "Wasefire-SideTable"]
[Indices Array Size (LEB128): num_functions + 1]
[Indices Array: (u16 * (num_functions + 1))]
[Metadata Array Size (LEB128): ...]
[Metadata Array: (u16 * ...)]
There was a problem hiding this comment.
In terms of the format, how about using the format that was intended for flash storage?
Yes, that's the idea, even if we didn't have a proper parsing function yet. That's the format I wrote there (updated below):
side-table := index flatten-metadata (16-bits aligned)
index := u16 u16 ... u16 (N + 1 times where N is the number of functions in the module)
flatten-metadata := metadata metadata ... metadata (N times where `flatten-metadata[i]` starts at byte position `index[i]` and ends at `index[i + 1]`)
metadata := type:u16 parser:(u32 u32) branch-table
branch-table := branch branch ... branch (length is implicitly defined by `index[i + 1]` see above)
branch := delta-ip:u16 delta-stp:u16 val-cnt:u8 pop-cnt:u12
In particular, we shouldn't use LEB128 since u16 is enough and the benefit from using only one byte up to 127 is not worth it.
There was a problem hiding this comment.
I've pushed a commit to better factorize end_label and br_label. It's not finished because similarly to the ValidMode::Branches, we also need ValidMode::BranchTable, which is either prepared or verified. In particular it must be read from ValidMode::patch_branch() for Verify.
zhouwfang
force-pushed
the
add-verify-mode
branch
from
6e65644 to
cda46ed
Compare
crates/interpreter/src/valid.rs
Outdated
| @@ -928,7 +1053,7 @@ impl<'a, 'm, M: ValidMode> Expr<'a, 'm, M> { | |||
| fn branch(&self) -> SideTableBranch<'m> { | |||
| SideTableBranch { | |||
| parser: self.parser.save(), | |||
| branch_table: self.branch_table.save(), | |||
| branch_table: self.branch_table.as_ref().map_or(0, |x| x.next_index()), | |||
There was a problem hiding this comment.
It doesn't work to unwrap? I would expect branch to be only called outside const context.
There was a problem hiding this comment.
No, it could be None. I guess it is because branch_target() is called for Verify.
There was a problem hiding this comment.
It's because of the End instruction for consts. I'm fixing it in the review commit.
crates/interpreter/src/valid.rs
Outdated
| @@ -928,7 +1053,7 @@ impl<'a, 'm, M: ValidMode> Expr<'a, 'm, M> { | |||
| fn branch(&self) -> SideTableBranch<'m> { | |||
| SideTableBranch { | |||
| parser: self.parser.save(), | |||
| branch_table: self.branch_table.save(), | |||
| branch_table: self.branch_table.as_ref().map_or(0, |x| x.next_index()), | |||
There was a problem hiding this comment.
It's because of the End instruction for consts. I'm fixing it in the review commit.
#46