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

src/viper/prelude.ml

@@ -0,0 +1,17 @@
+let prelude : string = {prelude|/* BEGIN PRELUDE */
+domain Array {
+  function $loc(a: Array, i: Int): Ref
+  function $size(a: Array): Int
+  function $first(r: Ref): Array
+  function $second(r: Ref): Int
+  axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i }
+  axiom $size_nonneg { forall a: Array :: $size(a) >= 0 }
+}
+define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t)
+define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2)
+define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+field $int: Int
+field $bool: Bool
+field $ref: Ref
+field $array: Array
+/* END PRELUDE */|prelude}

src/viper/pretty.ml

@@ -1,5 +1,6 @@
 open Source
 open Syntax
+open Prelude
 
 open Format
 
@@ -92,15 +93,18 @@ and pp_typ ppf t =
   | IntT -> pr ppf "Int"
   | BoolT -> pr ppf "Bool"
   | RefT -> pr ppf "Ref"
+  | ArrayT -> pr 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
+  | FldE s ->
+     fprintf ppf "%s" s
+  | CallE (m, es) ->
+     fprintf ppf "@[%s(%a)@]" m (pp_print_list pp_exp ~pp_sep:comma) es
   | NotE e ->
      fprintf ppf "@[(!%a)@]" pp_exp e
   | MinusE e ->
@@ -213,7 +217,7 @@ let prog_mapped file p =
     marks := [];
     let b = Buffer.create 16 in
     let ppf = Format.formatter_of_buffer b in
-    Format.fprintf ppf "@[%a@]" pp_prog p;
+    Format.fprintf ppf "@[%s@]@.@.@[%a@]" prelude pp_prog p;
     Format.pp_print_flush ppf ();
     let in_file { left; right } =
       let left, right = { left with file }, { right with file } in

src/viper/syntax.ml

@@ -49,7 +49,8 @@ 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
+  | FldE of string               (* top-level field name, e.g. to be passed as a macro argument *)
+  | CallE of string * exp list   (* macro or func call *)
 
 and perm = (perm', info) Source.annotated_phrase
 
@@ -94,4 +95,5 @@ and typ' =
   | IntT
   | BoolT
   | RefT
+  | ArrayT