VM initialization and creating contracts #46
Conversation
virgil-serbanuta
force-pushed
the
implement-hooks
branch
3 times, most recently
from
f9e0fa4 to
7406e48
Compare
traiansf
force-pushed
the
implement-hooks
branch
from
076c37c to
cef480a
Compare
virgil-serbanuta
force-pushed
the
implement-hooks
branch
from
cef480a to
9026868
Compare
virgil-serbanuta
force-pushed
the
implement-hooks
branch
from
9026868 to
cdac15c
Compare
There was a problem hiding this comment.
Looks good, thanks! I have a few minor questions/comments.
Also, after clicking the merge button but before merging, could we change the generated commit header to be a bit more descriptive? To me, at the moment, the PR title (which is used to auto-populate the commit header), is a bit more broad than the PR contents.
| rule [memLoad-zero-len]: | ||
| <instrs> #memLoad(OFFSET, 0) => b"" | ||
| ... | ||
| </instrs> | ||
| <contractModIdx> MODIDX:Int </contractModIdx> | ||
| <moduleInst> | ||
| <modIdx> MODIDX </modIdx> | ||
| <memAddrs> ListItem(ADDR) </memAddrs> | ||
| ... | ||
| </moduleInst> | ||
| <mems> MEMS </mems> | ||
| requires true | ||
| andBool 0 <=Int ADDR | ||
| andBool ADDR <Int size(MEMS) | ||
| andBool #signed(i32, OFFSET) >=Int 0 | ||
| andBool | ||
| (#let memInst(_, SIZE, _DATA) = MEMS[ADDR] #in | ||
| #signed(i32 , OFFSET) <=Int (SIZE *Int #pageSize()) | ||
| ) |
There was a problem hiding this comment.
Just curious: is this an optimization or is it required because it is not covered by another case? I don't have a strong opinion about it, just curious.
There was a problem hiding this comment.
I thought it was a corner case that should be handled separately, but it wasn't. I included it in the rule below.
| => setContractModIdx | ||
| ~> #resolveCurModuleFuncExport(#getEntryPoint()) | ||
| ~> setSuccessStatus |
There was a problem hiding this comment.
This is a style question, so feel free to resolve it however. On some other added lines, the two arrow styles (=> and ~>) have matching columns. Here, they're different. I'm not sure if this is intended or if, e.g., some editor is mixing whitespace styles.
There was a problem hiding this comment.
I'm not sure if I understand this properly, but I went through all occurrences of ~> in this file and I think that it works like this:
- Here (and in the place below with a similar comment), there are three items in a K list on the RHS of
=>(setContractModIdx, resolveCurModuleFuncExport, setSuccessStatus). Because the K list made of these three is a child of the rewrite, they are indented. - In other places, we have the rewrite as a child of
~>(e.g. the rule at line 136) and there I'm using the following pattern: an operator-like thing (e.g.~>and=>) are printed like this:
term
op term
op term
...
This means that something like (a => b) ~> c would be formatted as one of:
(a => b)
~> c
or
(a
=> b
)
~> c
Arguably, the latter may work better as:
( a
=> b
)
~> c
(with or without spaces before a) since the rewrite is a child of the parenthesis. Is this what you meant? If yes, I can just fix this. (I can also fix it if the issue is different, it's just that I'm not fully sure what you think should be fixed).
There was a problem hiding this comment.
Hmm... I haven't thought about this to the level of detail that you have! Since this is just a style question anyway, let's keep this as is and we can discuss later the possibility of a K coding style.
| #throwException(Code:Int, Reason:String) | ||
| => setStatus(Code) | ||
| ~> #exception(Reason) |
There was a problem hiding this comment.
A similar style comment about arrows as above.
virgil-serbanuta
changed the title
Fixes #15