Skip to content
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.

Sign up for GitHub

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

Jump to bottom

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

Closed
wants to merge 16 commits into from
Closed

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

Show file tree
Hide file tree
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 Apr 23, 2024
de64939
motoko-san: add ArrayT into viper
GoPavel Apr 23, 2024
2e801b2
motoko-san: support build-in prelude in viper
GoPavel Apr 23, 2024
75dccf4
motoko-san: refactor dec_field
GoPavel Apr 23, 2024
168c51d
motoko-san: support translation of arrays
GoPavel Apr 23, 2024
ae2f4e2
motoko-san: add infering permition of function arguments
GoPavel Apr 23, 2024
70e5d6d
motoko-san: add test for arrays + viper lib
GoPavel Apr 23, 2024
d2b8e91
squash! motoko-san: add test for arrays + viper lib
GoPavel Apr 25, 2024
7e61161
fixup: cleanup comments
GoPavel Apr 25, 2024
c5992d0
fixup! motoko-san: support build-in prelude in viper
GoPavel Apr 25, 2024
c5e40ac
motoko-san: support array.size()
GoPavel Apr 25, 2024
3b228e0
motoko-san: refactor assign_stmt
GoPavel Apr 25, 2024
1f03d38
fixup: refactor array assignment
GoPavel Apr 25, 2024
5fb4f45
fixup! motoko-san: add test for arrays + viper lib
GoPavel Apr 25, 2024
dbf0fc1
fixup! motoko-san: add test for arrays + viper lib
GoPavel Apr 26, 2024
7940973
fixup! motoko-san: add test for arrays + viper lib
GoPavel Apr 26, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 12 additions & 4 deletions src/viper/pretty.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,8 @@ let rec pp_prog ppf p =

and pp_item ppf i =
match i.it with
| ImportI id ->
fprintf ppf "@[<2>import \"%s\"@]" id.it
| FieldI (id, typ) ->
fprintf ppf "@[<2>field %s:@ %a@]"
id.it
Expand Down Expand Up @@ -87,20 +89,26 @@ and pp_returns ppf pars =
fprintf ppf "@[<1> returns (%a)@]"
(pp_print_list ~pp_sep:comma (pp_local)) pars

and pp_typ ppf t =
match t.it with
and pp_typ ppf t = pp_typ' ppf t.it
and pp_typ' ppf t =
match t with
| IntT -> pr ppf "Int"
| BoolT -> pr ppf "Bool"
| RefT -> pr ppf "Ref"
| ArrayT (_, t) -> fprintf ppf "Array"

and pp_exp ppf exp =
match exp.it with
| LocalVar (id, _) ->
fprintf ppf "%s" id.it
| FldAcc fldacc ->
pp_fldacc ppf fldacc
| MacroCall (m, e) ->
fprintf ppf "@[%s(%a)@]" m pp_exp e
| MacroArg id ->
fprintf ppf "%s" id.it
| MacroCall (m, es) ->
fprintf ppf "@[%s(%a)@]" m (pp_print_list pp_exp ~pp_sep:comma) es
| FuncCall (id, es) ->
fprintf ppf "@[%s(%a)@]" id (pp_print_list pp_exp ~pp_sep:comma) es
| NotE e ->
fprintf ppf "@[(!%a)@]" pp_exp e
| MinusE e ->
Expand Down
19 changes: 17 additions & 2 deletions src/viper/syntax.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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

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

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


and mut = Const | Mut
Copy link
Member

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.

Copy link
Author

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)

Copy link
Author

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.


and typ' =
| IntT
| BoolT
| RefT
| ArrayT of mut * typ'
Copy link
Member

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)


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