motoko-san: Generate fields

src/pipeline/pipeline.ml

@@ -511,7 +511,7 @@ let viper_files' parsefn files : viper_result =
   let u = CompUnit.comp_unit_of_prog false prog in
   let reqs = Viper.Common.init_reqs () in
   let* v = Viper.Trans.unit reqs (Viper.Prep.prep_unit u) in
-  let s = Viper.Pretty.prog_mapped "" reqs v in
+  let s = Viper.Pretty.prog_mapped "" (Viper.Prelude.prelude reqs) v in
   Diag.return s
 
 let viper_files files : viper_result =

src/viper/common.ml

@@ -20,9 +20,17 @@ module IntSet = Set.Make(struct
   let compare = compare
 end)
 
+module StrMap = Map.Make(String)
+
 (* Requirements arising from the translated code. In trans.ml we collect those
    requirements, in prelude.ml we generate definitons to satisfy them. *)
-type reqs = { tuple_arities : IntSet.t ref }
-
-let init_reqs () = { tuple_arities = ref IntSet.empty }
+type reqs =
+  { tuple_arities : IntSet.t ref
+  ; typed_fields : Syntax.typ StrMap.t ref
+  }
+
+let init_reqs () =
+  { tuple_arities = ref IntSet.empty
+  ; typed_fields = ref StrMap.empty
+  }
 

src/viper/prelude.ml

@@ -48,14 +48,15 @@ adt Option[T] {
   Some(some$0: T)
 }|prelude}
 
-let prelude_typed_references : string = {prelude|/* Typed references */
-field $int: Int
-field $bool: Bool
-field $ref: Ref
-field $array: Array
-field $option_int: Option[Int]
-field $option_bool: Option[Bool]
-field $option_array: Option[Array]|prelude}
+let pp_typed_field (name, typ) =
+  Format.asprintf "@[<2>field %s:@ %a@]"
+      name
+      Pretty.pp_typ typ
+
+let prelude_typed_references typed_fields : string =
+  String.concat "\n"
+  ("/* Typed references */" ::
+    List.map pp_typed_field (StrMap.bindings typed_fields))
 
 let prelude reqs: string =
   String.concat "\n"
@@ -64,6 +65,6 @@ let prelude reqs: string =
     prelude_array_encoding;
     prelude_tuple_encoding !(reqs.tuple_arities);
     prelude_option_encoding;
-    prelude_typed_references;
+    prelude_typed_references !(reqs.typed_fields);
     "/* END PRELUDE */"
   ]

src/viper/prelude.mli

@@ -0,0 +1 @@
+val prelude : Common.reqs -> string

src/viper/pretty.ml

@@ -1,6 +1,5 @@
 open Source
 open Syntax
-open Prelude
 
 open Format
 
@@ -257,11 +256,11 @@ and pp_fldacc ppf fldacc =
 and pp_loop_inv ppf inv =
     fprintf ppf "invariant %a" pp_exp inv
 
-let prog_mapped file tuple_arities p =
+let prog_mapped file prelude p =
     marks := [];
     let b = Buffer.create 16 in
     let ppf = Format.formatter_of_buffer b in
-    Format.fprintf ppf "@[%s@]@.@.@[%a@]" (prelude tuple_arities) 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
@@ -298,4 +297,4 @@ let prog_mapped file tuple_arities p =
         List.fold_left tighten None mapping in
     Buffer.contents b, lookup
 
-let prog tuple_arities p = fst (prog_mapped "" tuple_arities p)
+let prog prelude p = fst (prog_mapped "" prelude p)

src/viper/trans.ml

@@ -173,6 +173,11 @@ let rec strip_par_p (p : M.pat) : M.pat =
   | M.ParP p' -> strip_par_p p'
   | _         -> p
 
+let rec strip_mut_t (t : T.typ) : T.typ =
+  match t with
+  | T.Mut t' -> strip_mut_t t'
+  | _        -> t
+
 let rec unit reqs (u : M.comp_unit) : prog Diag.result =
   Diag.(
     reset_stamps();
@@ -392,7 +397,7 @@ and dec_field' ctxt d =
       let lhs = fun ctxt' -> !!! Source.no_region (FldAcc (fldacc ctxt')) in
       let perms ctxt' at =
             conjoin ([ accE at (self ctxt' at, id x) ]
-                     @ (access_pred (lhs ctxt') t |: [])
+                     @ (access_pred ctxt' (lhs ctxt') t |: [])
                      @ static_invariants at (lhs ctxt') e) at in
       { ctxt with ids = Env.add x.it (Field, t) ctxt.ids },
       Some perms, (* perm *)
@@ -423,9 +428,9 @@ and arg p = match p.it with
         | _ -> unsupported p.at (Arrange.pat p))
   | _ -> unsupported p.at (Arrange.pat p)
 
-and access_pred lhs t =
+and access_pred ctxt lhs t =
   match T.normalize t with
-  | T.Array elem_t -> Some (array_acc Source.no_region lhs elem_t)
+  | T.Array elem_t -> Some (array_acc Source.no_region ctxt lhs elem_t)
   | _ -> None
 
 (* Get access predicates for all local variables in current scope *)
@@ -434,7 +439,7 @@ and local_access_preds ctxt =
   let preds = Env.fold (fun id info preds ->
       match info with
       | (Local, t) ->
-        let pred = access_pred !!(LocalVar (!!id, tr_typ ctxt t)) t in
+        let pred = access_pred ctxt !!(LocalVar (!!id, tr_typ ctxt t)) t in
         pred |: preds
       | _ -> preds)
     ctxt.ids []
@@ -732,9 +737,9 @@ and assign_stmts ctxt at (lval : lvalue) (e : M.exp) : seqn' =
       fld_via_tmp_var ctxt lval t (fun x ->
         let lhs = !!(LocalVar (x, tr_typ ctxt t)) in
         [], [ !!(AssertS !!(GeCmpE (exp ctxt e1, intLitE at 0)))
-            ; !!(InhaleS (array_acc at lhs (array_elem_t t)))
+            ; !!(InhaleS (array_acc at ctxt lhs (array_elem_t t)))
             ; !!(InhaleS (array_size_inv at lhs (exp ctxt e1)))
-            ; !!(InhaleS (array_init_const at lhs (array_elem_t t) (exp ctxt e2))) ]
+            ; !!(InhaleS (array_init_const at ctxt lhs (array_elem_t t) (exp ctxt e2))) ]
       )
     | _ -> unsupported args.at (Arrange.exp args)
     end
@@ -900,7 +905,7 @@ and rets ctxt t_opt =
      | T.Tup [] -> [], []
      | T.Async (T.Fut, _, _) -> [], []
      | typ ->
-        let pred = access_pred !!(LocalVar (!!"$Res", tr_typ ctxt typ)) typ in
+        let pred = access_pred ctxt !!(LocalVar (!!"$Res", tr_typ ctxt typ)) typ in
         pred |: [], [(!!"$Res", tr_typ ctxt typ)]
     )
 
@@ -956,46 +961,54 @@ and tuple_elem_ts t =
   | t -> failwith "tuple_elem_ts: expected tuple type"
 
 (* name of field of typed reference *)
-and typed_field t =
-  match T.normalize t  with
-  | T.Mut elem_t -> typed_field elem_t
-  | T.Prim T.Int  -> "$int"
-  | T.Prim T.Nat  -> "$int"  (* Viper has no native support for Nat, so translate to Int *)
-  | T.Prim T.Bool -> "$bool"
-  | _ -> unsupported Source.no_region (Mo_types.Arrange_type.typ t)
+and typed_field ctxt t =
+  let t' = tr_typ ctxt (strip_mut_t t) in
+  let name = type_field_name t' in
+  ctxt.reqs.typed_fields := StrMap.add name t' !(ctxt.reqs.typed_fields);
+  name
+
+and type_field_name t =
+  match t.it with
+  | IntT  -> "$int"
+  | BoolT -> "$bool"
+  | RefT  -> "$ref"
+  | ArrayT -> "$array"
+  | TupleT ts  -> "$tuple" ^ string_of_int (List.length ts) ^ String.concat "" (List.map type_field_name ts)
+  | OptionT t' -> "$option" ^ type_field_name t'
+  | ConT (con, ts) -> "$c_" ^ con.it ^ String.concat "" (List.map type_field_name ts)
 
 and array_size_inv at lhs n =
   !!! at (EqCmpE (sizeE at lhs, n))
 
-and array_acc at lhs t =
+and array_acc at ctxt lhs t =
   match T.normalize t with
-  | T.Mut _-> arrayAccE at lhs (typed_field t) FullP
-  | _      -> arrayAccE at lhs (typed_field t) WildcardP
+  | T.Mut _-> arrayAccE at lhs (typed_field ctxt t) FullP
+  | _      -> arrayAccE at lhs (typed_field ctxt t) WildcardP
 
 (* Allocate array on the LHS expression.
    Note: array_alloc assumes that the array is uninitialized. Assignment to
    existing arrays must be done via a temporary variable. *)
 and array_alloc at ctxt lhs t es : stmt list =
   let (!!) p = !!! at p in
   let init_array = List.mapi (fun i e ->
-    FieldAssignS (locE at lhs (intLitE at i) (typed_field t), exp ctxt e)) es in
+    FieldAssignS (locE at lhs (intLitE at i) (typed_field ctxt t), exp ctxt e)) es in
   (* InhaleS (!! (FldAcc (locE at lhs (intLitE at i) (typed_field t))) === e)) es in *)
   let reset_perm =
     (match T.normalize t with
      | T.Mut _ -> []
-     | _       -> [ExhaleS (array_acc at lhs t); InhaleS (array_acc at lhs t)])in
-  let stmts = [ InhaleS (array_acc at lhs (T.Mut t))
+     | _       -> [ExhaleS (array_acc at ctxt lhs t); InhaleS (array_acc at ctxt lhs t)])in
+  let stmts = [ InhaleS (array_acc at ctxt lhs (T.Mut t))
               ; InhaleS (array_size_inv at lhs (intLitE at (List.length es)))]
               @ init_array
               @ reset_perm
   in List.map (!!) stmts
 
-and array_init_const at lhs t x =
+and array_init_const at ctxt lhs t x =
   let (!!) p = !!! at p in
-  !! (CallE ("$array_init", [lhs; !!(FldE (typed_field t)); x]))
+  !! (CallE ("$array_init", [lhs; !!(FldE (typed_field ctxt t)); x]))
 
 and array_loc ctxt at e1 e2 t =
-  locE at (exp ctxt e1) (exp ctxt e2) (typed_field t)
+  locE at (exp ctxt e1) (exp ctxt e2) (typed_field ctxt t)
 
 and label_expr_alloc ~label_id ~label_type ~label_rhs ~label_note at ctxt lhs : seqn' =
   let ctxt =

test/repl/ok/viper.stdout.ok

@@ -18,13 +18,6 @@ adt Option[T] {
   Some(some$0: T)
 }
 /* Typed references */
-field $int: Int
-field $bool: Bool
-field $ref: Ref
-field $array: Array
-field $option_int: Option[Int]
-field $option_bool: Option[Bool]
-field $option_array: Option[Array]
 /* END PRELUDE */
 
 field $message_async: Int

test/viper/array-of-tuples.mo

@@ -0,0 +1,12 @@
+// @verify
+// import Array "mo:base/Array";
+
+actor ArrayOfTuples {
+
+    public func get_tup_arr(): async [(Int, Bool)] {
+      let x1 = (42, true);
+      let x2 = (0, false);
+      return [x1, x2];
+    };
+
+}

test/viper/ok/array-of-tuples.silicon.ok

@@ -0,0 +1,2 @@
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (array-of-tuples.vpr@25.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (array-of-tuples.vpr@26.1)

test/viper/ok/array-of-tuples.vpr.ok

@@ -0,0 +1,54 @@
+/* BEGIN PRELUDE */
+/* Array encoding */
+domain Array {
+  function $loc(a: Array, i: Int): Ref
+  function $size(a: Array): Int
+  function $loc_inv1(r: Ref): Array
+  function $loc_inv2(r: Ref): Int
+  axiom $all_diff_array { forall a: Array, i: Int :: {$loc(a, i)} $loc_inv1($loc(a, i)) == a && $loc_inv2($loc(a, i)) == i }
+  axiom $size_nonneg { forall a: Array :: $size(a) >= 0 }
+}
+define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
+define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
+/* Tuple encoding */
+adt Tuple$2 [T0, T1] { Tup$2(tup$2$0 : T0, tup$2$1 : T1) }
+/* Option encoding */
+adt Option[T] {
+  None()
+  Some(some$0: T)
+}
+/* Typed references */
+field $tuple2$int$bool: Tuple$2[Int, Bool]
+/* END PRELUDE */
+
+define $Perm($Self) (true)
+define $Inv($Self) (true)
+method __init__($Self: Ref)
+
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { 
+
+    }
+method get_tup_arr($Self: Ref)
+     returns ($Res: Array)
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $array_acc($Res, $tuple2$int$bool, wildcard)
+    ensures $Inv($Self)
+    { var x1: Tuple$2[Int, Bool]
+      var x2: Tuple$2[Int, Bool]
+      x1 := Tup$2(42, true);
+      x2 := Tup$2(0, false);
+      inhale $array_acc($Res, $tuple2$int$bool, write);
+      inhale ($size($Res) == 2);
+      ($loc($Res, 0)).$tuple2$int$bool := x1;
+      ($loc($Res, 1)).$tuple2$int$bool := x2;
+      exhale $array_acc($Res, $tuple2$int$bool, wildcard);
+      inhale $array_acc($Res, $tuple2$int$bool, wildcard);
+      goto $Ret;
+      label $Ret; 
+    }

test/viper/ok/array.silicon.ok

@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (array.vpr@39.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (array.vpr@34.1)

test/viper/ok/array.vpr.ok

@@ -18,13 +18,8 @@ adt Option[T] {
   Some(some$0: T)
 }
 /* Typed references */
-field $int: Int
 field $bool: Bool
-field $ref: Ref
-field $array: Array
-field $option_int: Option[Int]
-field $option_bool: Option[Bool]
-field $option_array: Option[Array]
+field $int: Int
 /* END PRELUDE */
 
 define $Perm($Self) (((((true && (acc(($Self).immut_arr,write) && ($array_acc(

test/viper/ok/assertions.silicon.ok

@@ -1,2 +1,2 @@
-  [0] Postcondition of __init__ might not hold. Assertion $Self.u might not hold. (assertions.vpr@39.13--39.24)
-  [1] Assert might fail. Assertion $Self.u ==> $Self.v > 0 might not hold. (assertions.vpr@57.15--57.44)
+  [0] Postcondition of __init__ might not hold. Assertion $Self.u might not hold. (assertions.vpr@32.13--32.24)
+  [1] Assert might fail. Assertion $Self.u ==> $Self.v > 0 might not hold. (assertions.vpr@50.15--50.44)

test/viper/ok/assertions.vpr.ok

@@ -18,13 +18,6 @@ adt Option[T] {
   Some(some$0: T)
 }
 /* Typed references */
-field $int: Int
-field $bool: Bool
-field $ref: Ref
-field $array: Array
-field $option_int: Option[Int]
-field $option_bool: Option[Bool]
-field $option_array: Option[Array]
 /* END PRELUDE */
 
 field $message_async: Int

test/viper/ok/async.silicon.ok

@@ -1 +1 @@
-  [0] Exhale might fail. Assertion $Self.$message_async <= 1 might not hold. (async.vpr@62.15--62.42)
+  [0] Exhale might fail. Assertion $Self.$message_async <= 1 might not hold. (async.vpr@55.15--55.42)

test/viper/ok/async.vpr.ok

@@ -18,13 +18,6 @@ adt Option[T] {
   Some(some$0: T)
 }
 /* Typed references */
-field $int: Int
-field $bool: Bool
-field $ref: Ref
-field $array: Array
-field $option_int: Option[Int]
-field $option_bool: Option[Bool]
-field $option_array: Option[Array]
 /* END PRELUDE */
 
 field $message_async_4: Int

test/viper/ok/claim-broken.silicon.ok

@@ -1 +1 @@
-  [0] Exhale might fail. Assertion $Self.$message_async == 1 ==> $Self.claimed && $Self.count == 0 might not hold. (claim-broken.vpr@60.20--60.47)
+  [0] Exhale might fail. Assertion $Self.$message_async == 1 ==> $Self.claimed && $Self.count == 0 might not hold. (claim-broken.vpr@53.20--53.47)

test/viper/ok/claim-broken.vpr.ok

@@ -18,13 +18,6 @@ adt Option[T] {
   Some(some$0: T)
 }
 /* Typed references */
-field $int: Int
-field $bool: Bool
-field $ref: Ref
-field $array: Array
-field $option_int: Option[Int]
-field $option_bool: Option[Bool]
-field $option_array: Option[Array]
 /* END PRELUDE */
 
 field $message_async: Int

test/viper/ok/claim-reward-naive.vpr.ok

@@ -18,13 +18,6 @@ adt Option[T] {
   Some(some$0: T)
 }
 /* Typed references */
-field $int: Int
-field $bool: Bool
-field $ref: Ref
-field $array: Array
-field $option_int: Option[Int]
-field $option_bool: Option[Bool]
-field $option_array: Option[Array]
 /* END PRELUDE */
 
 define $Perm($Self) (((true && acc(($Self).claimed,write)) && acc(($Self).count,write)))

test/viper/ok/claim-simple.silicon.ok

@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (claim-simple.vpr@31.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (claim-simple.vpr@24.1)