-
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
Conversation
src/viper/trans.ml
Outdated
@@ -121,11 +156,17 @@ let rec extract_concurrency (seq : seqn) : stmt' list * seqn = | |||
let conc, stmts = List.fold_left extr ([], []) stmts in | |||
rev conc, { seq with it = fst seq.it, rev stmts } | |||
|
|||
let prelude = | |||
let (!!) p = !!! Source.no_region p in | |||
[ !! (ImportI (!! "../../src/viper/lib/array.vpr")) ] |
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.
This is temporary, right? We need to decide how to ship the viper lib with moc
(probably ask the Dfinity team)
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.
Right, it's temporary. But I think it should be in this shape.
We will discuss with Dfinity team
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.
Tweaked path since it wasn't working for the test runner.
Now lib/
should be next to .mo
file.
src/viper/trans.ml
Outdated
and dec ctxt d = | ||
let (!!) p = !!! (d.at) p in | ||
match d.it with | ||
(* TODO AnnotE could be nested *) | ||
| M.VarD (x, {it=M.AnnotE ({it=M.ArrayE (mut, es); note; _}, _); _}) | ||
| M.LetD ({it=M.VarP x;_}, {it=M.AnnotE ({it=M.ArrayE (mut, es); note; _}, _); _}, None) -> |
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.
I was about to suggest moving this logic to assign_stmt
, but I see you have a TODO for that
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.
Fixed
@@ -90,8 +92,21 @@ and stmt' = | |||
|
|||
and typ = (typ', info) Source.annotated_phrase | |||
|
|||
|
|||
and mut = Const | Mut |
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 be array_acc_var
which is a macro for forall ... 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.
]) | ||
| M.WhileE(e, s1) -> | ||
let (invs, s1') = extract_loop_invariants s1 in | ||
let invs' = List.map (fun inv -> exp ctxt inv) invs in | ||
!!([], | ||
[ !!(WhileS(exp ctxt e, invs', stmt ctxt s1')) ]) | ||
(* TODO: remove by Motoko->Motoko transformation *) |
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.
Could you give an example of the Motoko->Motoko transformation that you want?
As I understand it, this clause deals with arr := [1,2,3]
. What should it be transformed to?
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.
arr := [1, 2, 3]
could be transformed into
let t1 := [1, 2, 3]
arr := t1
So all array literal will be allocated once and have fresh name.
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.
Also note that arr := [...]
could not produced just by array_alloc
. We have to use temporary variable t1
.
Otherwise two assignment could produce inconsistent:
arr := []
arr := [1]
translated (without temporary declaration) to:
inhale len(arr) == 0 && array_acc_mut(arr)
exhale array_acc_mut(arr) // we cannot exhale len(arr) == 0
inhale len(arr) == 1 && array_acc_mut(arr)
assert 1 == 0
reassignment arr := t1
solve this problem
src/viper/trans.ml
Outdated
@@ -485,6 +571,9 @@ and exp ctxt e = | |||
!!(BoolLitE b) | |||
| M.IntLit i -> | |||
!!(IntLitE i) | |||
(* TODO: support Nat type *) |
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.
You can add [DMS-34] reference in the comment.
+ support several parameters + support untyped argument e.g. for field_name parameter
problem: currently dec_field is not translating init expression and field permission, which make hard extending it for arrays. solution: move generating init and perms into function dec_field (renamed to unit_decl because contains not only field e.g. functions as well)
Make it possible to return multiple instructions (for arrays)
d5ae98b
to
5fb4f45
Compare
@@ -542,4 +633,6 @@ and tr_typ' typ = | |||
| T.Prim T.Int -> IntT | |||
| T.Prim T.Nat -> IntT (* Viper has no native support for Nat, so translate to Int *) | |||
| T.Prim T.Bool -> BoolT | |||
| T.Array (T.Mut typ) -> ArrayT (Mut , tr_typ' (T.normalize typ)) |
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.
This call to T.normalize
looks redundant, because tr_typ'
already does normalization.
Looks like the build is still failing due to path-related issues
I can confirm locally, |
and typ' = | ||
| IntT | ||
| BoolT | ||
| RefT | ||
| ArrayT of mut * typ' |
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.
Having thought about this some more, I don't think this is right. This is supposed to be the Viper type, and the Array
domain defined in array.vpr
is not parameterized by anything. So this type should be simply ArrayT
(no of
)
|
||
and unit_decl' ctxt (d : M.dec_field') at = | ||
let self_id = !!! (Source.no_region) "$Self" in | ||
let self_var at = !!! at (LocalVar (!!! at self_id.it, !!! at RefT)) 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.
Why not use the preexisting self
helper function to get the self-var from the ctxt?
OK, I've addressed my own comments and submitted #8. |
see newer version of this PR in the #8 |
No description provided.