forked from dfinity/motoko
-
Notifications
You must be signed in to change notification settings - Fork 0
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
[DMS-3,9] Motoko san/arrays #5
Closed
Closed
Changes from all commits
Commits
Show all changes
16 commits
Select commit
Hold shift + click to select a range
fe9d03d
motoko-san: Enhance viper macro support
GoPavel de64939
motoko-san: add ArrayT into viper
GoPavel 2e801b2
motoko-san: support build-in prelude in viper
GoPavel 75dccf4
motoko-san: refactor dec_field
GoPavel 168c51d
motoko-san: support translation of arrays
GoPavel ae2f4e2
motoko-san: add infering permition of function arguments
GoPavel 70e5d6d
motoko-san: add test for arrays + viper lib
GoPavel d2b8e91
squash! motoko-san: add test for arrays + viper lib
GoPavel 7e61161
fixup: cleanup comments
GoPavel c5992d0
fixup! motoko-san: support build-in prelude in viper
GoPavel c5e40ac
motoko-san: support array.size()
GoPavel 3b228e0
motoko-san: refactor assign_stmt
GoPavel 1f03d38
fixup: refactor array assignment
GoPavel 5fb4f45
fixup! motoko-san: add test for arrays + viper lib
GoPavel dbf0fc1
fixup! motoko-san: add test for arrays + viper lib
GoPavel 7940973
fixup! motoko-san: add test for arrays + viper lib
GoPavel File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -10,7 +10,7 @@ type prog = (item list, info) Source.annotated_phrase | |
|
||
and item = (item', info) Source.annotated_phrase | ||
and item' = | ||
(* | import path *) | ||
| ImportI of id | ||
| FieldI of id * typ | ||
| MethodI of id * par list * par list * exp list * exp list * seqn option | ||
| InvariantI of string * exp | ||
|
@@ -49,7 +49,9 @@ and exp' = | |
| FldAcc of fldacc | ||
| PermE of perm (* perm_amount *) | ||
| AccE of fldacc * exp (* acc((rcvr: exp).field, (exp: perm_amount)) *) | ||
| MacroCall of string * exp | ||
| MacroCall of string * exp list | ||
| MacroArg of id (* untyped macro argument e.g. "macro(a, f) { a.f }" *) | ||
| FuncCall of string * exp list | ||
|
||
and perm = (perm', info) Source.annotated_phrase | ||
|
||
|
@@ -90,8 +92,21 @@ and stmt' = | |
|
||
and typ = (typ', info) Source.annotated_phrase | ||
|
||
|
||
and mut = Const | Mut | ||
|
||
and typ' = | ||
| IntT | ||
| BoolT | ||
| RefT | ||
| ArrayT of mut * typ' | ||
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. Having thought about this some more, I don't think this is right. This is supposed to be the Viper type, and the |
||
|
||
let type_field = function | ||
| IntT -> "int" | ||
| BoolT -> "bool" | ||
| RefT -> "ref" | ||
| ArrayT _ -> "array" (* TODO *) | ||
|
||
let inner_type = function | ||
| Source.{it=ArrayT (k, t); _} -> t | ||
| Source.{it=t; _} -> t |
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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.
Is this flag for future use? Looks like the translation ignores it.
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.
It's actually used in array utility functions. Check
array_acc
.I use it for identifying which kind of an access predicate should be used. Namely
ArrayT Mut
requires write access into each location so it should bearray_acc_var
which is a macro forforall ... acc(loc(a, i).val, write)
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.
Actually I did it only for convenience. We can eliminate it and pass this information as a separate parameter into utility functions. But I put it this way.