[DMS-3,9] Motoko san/arrays #5

GoPavel · 2024-04-23T23:40:16Z

No description provided.

int-index · 2024-04-24T10:50:03Z

src/viper/trans.ml

@@ -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")) ]


This is temporary, right? We need to decide how to ship the viper lib with moc (probably ask the Dfinity team)

Right, it's temporary. But I think it should be in this shape.
We will discuss with Dfinity team

Tweaked path since it wasn't working for the test runner.
Now lib/ should be next to .mo file.

int-index · 2024-04-24T10:51:49Z

src/viper/trans.ml

 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) ->


I was about to suggest moving this logic to assign_stmt, but I see you have a TODO for that

int-index · 2024-04-24T11:01:51Z

src/viper/syntax.ml

@@ -90,8 +92,21 @@ and stmt' =

 and typ = (typ', info) Source.annotated_phrase

+
+and mut = Const | Mut


Is this flag for future use? Looks like the translation ignores it.

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)

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.

int-index · 2024-04-24T11:03:58Z

src/viper/trans.ml

        ])
  | 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 *)


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?

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.

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

gromakovsky · 2024-04-24T11:33:17Z

src/viper/trans.ml

@@ -485,6 +571,9 @@ and exp ctxt e =
       !!(BoolLitE b)
    | M.IntLit i ->
       !!(IntLitE i)
+    (* TODO: support Nat type *)


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)

int-index · 2024-04-29T17:43:41Z

src/viper/trans.ml

@@ -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))


This call to T.normalize looks redundant, because tr_typ' already does normalization.

int-index · 2024-04-29T17:45:29Z

Looks like the build is still failing due to path-related issues

error: builder for '/nix/store/sb8fp5h5xnal5z6gaca8wzss2zadl15j-test-viper.drv' failed with exit code 2;
       last 25 log lines:
       > +++ private.silicon.ret (actual)
       > @@ -0,0 +1 @@
       > +Return code 1
       > --- private.silicon (expected)
       > +++ private.silicon (actual)
       > @@ -0,0 +1 @@
       > +  [0] Parse error: file "/build/test-viper-src/viper/_out/viper_lib/array.vpr" does not exist (private.vpr@1.1)
       > simple-funs:ln: failed to create symbolic link '_out/viper_lib': File exists
       >  [tc] [vpr] [silicon]
       > --- simple-funs.silicon.ret (expected)
       > +++ simple-funs.silicon.ret (actual)
       > @@ -0,0 +1 @@
       > +Return code 1
       > --- simple-funs.silicon (expected)
       > +++ simple-funs.silicon (actual)
       > @@ -1,2 +1 @@
       > -Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (array.vpr@2.1)
       > -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (array.vpr@3.1)
       > +  [0] Parse error: file "/build/test-viper-src/viper/_out/viper_lib/array.vpr" does not exist (simple-funs.vpr@1.1)
       > unsupported:ln: failed to create symbolic link '_out/viper_lib': File exists
       >  [tc] [vpr]
       > Some tests failed:
       > array.mo assertions.mo async.mo claim-broken.mo claim-reward-naive.mo claim-simple.mo claim.mo counter.mo invariant.mo loop-invariant.mo method-call.mo nats.mo private.mo simple-funs.mo
       > make: *** [Makefile:5: all] Error 1
       > make: Leaving directory '/build/test-viper-src/viper'
       For full logs, run 'nix log /nix/store/sb8fp5h5xnal5z6gaca8wzss2zadl15j-test-viper.drv'.

I can confirm locally, nix-build does not work. Let's try a different approach and simply inline the array code without any imports. I'll do that.

int-index · 2024-04-29T18:55:54Z

src/viper/syntax.ml

 and typ' =
  | IntT
  | BoolT
  | RefT
+  | ArrayT of mut * typ'


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)

int-index · 2024-04-29T20:24:06Z

src/viper/trans.ml

+
+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


Why not use the preexisting self helper function to get the self-var from the ctxt?

int-index · 2024-04-29T23:25:10Z

OK, I've addressed my own comments and submitted #8.

GoPavel · 2024-04-30T14:27:34Z

see newer version of this PR in the #8

int-index reviewed Apr 24, 2024

View reviewed changes

gromakovsky reviewed Apr 24, 2024

View reviewed changes

GoPavel changed the title ~~Motoko san/arrays~~ [DMS-3,9] Motoko san/arrays Apr 24, 2024

GoPavel added 14 commits April 25, 2024 16:18

motoko-san: Enhance viper macro support

fe9d03d

+ support several parameters + support untyped argument e.g. for field_name parameter

motoko-san: add ArrayT into viper

de64939

motoko-san: support build-in prelude in viper

2e801b2

motoko-san: support translation of arrays

168c51d

motoko-san: add infering permition of function arguments

ae2f4e2

motoko-san: add test for arrays + viper lib

70e5d6d

squash! motoko-san: add test for arrays + viper lib

d2b8e91

fixup: cleanup comments

7e61161

fixup! motoko-san: support build-in prelude in viper

c5992d0

motoko-san: support array.size()

c5e40ac

motoko-san: refactor assign_stmt

3b228e0

Make it possible to return multiple instructions (for arrays)

fixup: refactor array assignment

1f03d38

fixup! motoko-san: add test for arrays + viper lib

5fb4f45

GoPavel force-pushed the motoko-san/arrays branch from d5ae98b to 5fb4f45 Compare April 25, 2024 14:23

GoPavel added 2 commits April 26, 2024 15:28

fixup! motoko-san: add test for arrays + viper lib

dbf0fc1

fixup! motoko-san: add test for arrays + viper lib

7940973

int-index reviewed Apr 29, 2024

View reviewed changes

int-index mentioned this pull request Apr 29, 2024

[DMS-3] [DMS-9] motoko-san: array support #8

Merged

GoPavel closed this Apr 30, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[DMS-3,9] Motoko san/arrays #5

[DMS-3,9] Motoko san/arrays #5

GoPavel commented Apr 23, 2024

int-index Apr 24, 2024

GoPavel Apr 24, 2024

GoPavel Apr 25, 2024

int-index Apr 24, 2024

GoPavel Apr 25, 2024

int-index Apr 24, 2024

GoPavel Apr 24, 2024

GoPavel Apr 24, 2024

int-index Apr 24, 2024 •

edited

Loading

GoPavel Apr 24, 2024

GoPavel Apr 25, 2024

gromakovsky Apr 24, 2024

int-index Apr 29, 2024

int-index commented Apr 29, 2024

int-index Apr 29, 2024

int-index Apr 29, 2024

int-index commented Apr 29, 2024

GoPavel commented Apr 30, 2024

		@@ -90,8 +92,21 @@ and stmt' =

		and typ = (typ', info) Source.annotated_phrase


		and mut = Const \| Mut

[DMS-3,9] Motoko san/arrays #5

[DMS-3,9] Motoko san/arrays #5

Conversation

GoPavel commented Apr 23, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

int-index Apr 24, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

int-index commented Apr 29, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

int-index commented Apr 29, 2024

GoPavel commented Apr 30, 2024

int-index Apr 24, 2024 •

edited

Loading