motoko-san: support options

src/viper/pretty.ml

@@ -123,6 +123,7 @@ and pp_typ ppf t =
   | RefT -> pr ppf "Ref"
   | ArrayT -> pr ppf "Array"
   | TupleT -> pr ppf "Tuple"
+  | OptionT t -> fprintf ppf "@[Option[%a]@]" pp_typ t
   | ConT(name, []) -> fprintf ppf "%s" name
   | ConT(name, ts) ->
       fprintf ppf "@[%s[%a]@]"

src/viper/syntax.ml

@@ -101,5 +101,6 @@ and typ' =
   | RefT
   | ArrayT
   | TupleT
+  | OptionT of typ
   | ConT of string * typ list
 

src/viper/trans.ml

@@ -65,6 +65,17 @@ let arrayAccE at lhs field_name perm =
 let prjE at tuple_e ix_e field_name =
   !!! at (CallE ("$prj", [tuple_e; ix_e])), !!! at field_name
 
+let someE at x_e =
+  !!! at (CallE ("Some", [x_e]))
+let noneE at =
+  !!! at (CallE ("None", []))
+let isSomeE at opt_e =
+  !!! at (FldAcc (opt_e, !!! at "isSome"))
+let isNoneE at opt_e =
+  !!! at (FldAcc (opt_e, !!! at "isNone"))
+let fromSomeE at opt_e =
+  !!! at (FldAcc (opt_e, !!! at "some$0"))
+
 let (|:) (x_opt : 'a option) (xs : 'a list) : 'a list =
   match x_opt with
   | None -> xs
@@ -567,6 +578,18 @@ and switch_stmts ctxt at (scrut : M.exp) (cases : M.case list) : seqn' =
 and pat_match ctxt (scrut : M.exp) (p : M.pat) : exp list * (id * T.typ) list * seqn' =
   let (!!) a = !!! (p.at) a in
   match (strip_par_p p).it with
+  | M.LitP lit ->
+    begin match !lit with
+    | M.NullLit -> [isNoneE (p.at) (exp ctxt scrut)], [], ([], [])
+    | _         -> unsupported (p.at) (Arrange.lit !lit)
+    end
+  | M.OptP p' ->
+    let e_scrut = exp ctxt scrut in
+    let cond = isSomeE (p.at) e_scrut in
+    let x, t = unwrap_var_pat p' in
+    let ds = [!!(x, tr_typ t)] in
+    let stmts = [!!(assign_stmt (LValueUninitVar x) (fromSomeE (scrut.at) e_scrut))] in
+    [cond], [(x, t)], (ds, stmts)
   | M.(TupP ps) ->
     let e_scrut = exp ctxt scrut in
     let p_scope = unwrap_tup_vars_pat p in
@@ -682,6 +705,8 @@ and exp ctxt e =
        !!(IntLitE i)
     | M.NatLit i ->
        !!(IntLitE i)
+    | M.NullLit ->
+       noneE (e.at)
     | _ ->
        unsupported e.at (Arrange.exp e)
     end
@@ -717,6 +742,8 @@ and exp ctxt e =
      !!(FldAcc (array_loc ctxt e.at e1 e2 e_t))
   | M.ProjE (e, i) ->
      !!(FldAcc (prjE e.at (exp ctxt e) (intLitE e.at i) (typed_field e_t)))
+  | M.OptE e ->
+     someE (e.at) (exp ctxt e)
   | M.TagE (tag, e) ->
      !!(match e.it with
         | M.TupE es -> CallE (tag.it, List.map (exp ctxt) es)
@@ -750,6 +777,7 @@ and tr_typ' typ =
   | _, T.Prim T.Bool -> BoolT
   | _, T.Array _ -> ArrayT     (* Viper arrays are not parameterised by element type *)
   | _, T.Tup   _ -> TupleT     (* Viper tuples are not parameterised by element type *)
+  | _, T.Opt   t -> OptionT (tr_typ t)
   | T.Con (con, ts), _ -> ConT (Mo_types.Cons.name con, List.map tr_typ ts)
   | _, t -> unsupported Source.no_region (Mo_types.Arrange_type.typ t)
 

test/viper/ok/option.silicon.ok

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

test/viper/ok/option.tc.ok

@@ -0,0 +1,7 @@
+option.mo:3.9-3.13: warning [M0194], unused identifier fld1 (delete or rename to wildcard `_` or `_fld1`)
+option.mo:8.13-8.15: warning [M0194], unused identifier t2 (delete or rename to wildcard `_` or `_t2`)
+option.mo:9.13-9.15: warning [M0194], unused identifier t3 (delete or rename to wildcard `_` or `_t3`)
+option.mo:10.13-10.15: warning [M0194], unused identifier t4 (delete or rename to wildcard `_` or `_t4`)
+option.mo:32.19-32.29: warning [M0194], unused identifier passOption (delete or rename to wildcard `_` or `_passOption`)
+option.mo:33.13-33.15: warning [M0194], unused identifier a2 (delete or rename to wildcard `_` or `_a2`)
+option.mo:36.18-36.27: warning [M0194], unused identifier callTuple (delete or rename to wildcard `_` or `_callTuple`)

test/viper/ok/option.vpr.ok

@@ -0,0 +1,133 @@
+/* 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)
+/* Tuple encoding */
+domain Tuple {
+  function $prj(a: Tuple, i: Int): Ref
+  function $prj_inv1(r: Ref): Tuple
+  function $prj_inv2(r: Ref): Int
+  axiom $all_diff_tuple { forall a: Tuple, i: Int :: {$prj(a, i)} $prj_inv1($prj(a, i)) == a && $prj_inv2($prj(a, i)) == i }
+}
+/* Option encoding */
+adt Option[T] {
+  None()
+  Some(some$0: T)
+}
+/* Typed references */
+field $int: Int
+field $bool: Bool
+field $ref: Ref
+field $array: Array
+field $tuple: Tuple
+field $option_int: Option[Int]
+field $option_bool: Option[Bool]
+field $option_array: Option[Array]
+field $option_tuple: Option[Tuple]
+/* END PRELUDE */
+
+define $Perm($Self) (((true && acc(($Self).fld1,write)) && acc(($Self).fld2,write)))
+define $Inv($Self) (true)
+method __init__($Self: Ref)
+
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { 
+      ($Self).fld1 := None();
+      ($Self).fld2 := Some(true); 
+    }
+field fld1: Option[Int]
+field fld2: Option[Bool]
+method localOption($Self: Ref)
+
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { var t1: Option[Int]
+      var t2: Option[Int]
+      var t3: Option[Int]
+      var t4: Option[Int]
+      var a2: Int
+      t1 := None();
+      t2 := Some(42);
+      t3 := None();
+      t4 := Some(32);
+      a2 := 0;
+      if ((t1).isNone)
+         { 
+           a2 := 0; 
+         }else
+         { 
+           if ((t1).isSome)
+              { var x: Int
+                x := (t1).some$0;
+                a2 := x; 
+              }; 
+         };
+      label $Ret; 
+    }
+method getOption($Self: Ref)
+     returns ($Res: Option[Bool])
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    { 
+      $Res := Some(false);
+      goto $Ret;
+      label $Ret; 
+    }
+method takeOption($Self: Ref, a: Option[Int])
+     returns ($Res: Int)
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    { 
+      if ((a).isNone)
+         { 
+           $Res := 0;
+           goto $Ret; 
+         }else
+         { 
+           if ((a).isSome)
+              { var x: Int
+                x := (a).some$0;
+                $Res := x;
+                goto $Ret; 
+              }; 
+         };
+      label $Ret; 
+    }
+method passOption($Self: Ref)
+
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    { var a2: Int
+      a2 := takeOption($Self, None());
+      label $Ret; 
+    }
+method callTuple($Self: Ref)
+
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    { var x: Option[Bool]
+      x := getOption($Self);
+      label $Ret; 
+    }
+method changeField($Self: Ref)
+
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { 
+      ($Self).fld2 := None();
+      label $Ret; 
+    }

test/viper/ok/option.vpr.stderr.ok

@@ -0,0 +1,7 @@
+option.mo:3.9-3.13: warning [M0194], unused identifier fld1 (delete or rename to wildcard `_` or `_fld1`)
+option.mo:8.13-8.15: warning [M0194], unused identifier t2 (delete or rename to wildcard `_` or `_t2`)
+option.mo:9.13-9.15: warning [M0194], unused identifier t3 (delete or rename to wildcard `_` or `_t3`)
+option.mo:10.13-10.15: warning [M0194], unused identifier t4 (delete or rename to wildcard `_` or `_t4`)
+option.mo:32.19-32.29: warning [M0194], unused identifier passOption (delete or rename to wildcard `_` or `_passOption`)
+option.mo:33.13-33.15: warning [M0194], unused identifier a2 (delete or rename to wildcard `_` or `_a2`)
+option.mo:36.18-36.27: warning [M0194], unused identifier callTuple (delete or rename to wildcard `_` or `_callTuple`)

test/viper/option.mo

@@ -0,0 +1,43 @@
+actor Option {
+
+    let fld1: ?Int = null;
+    var fld2: ?Bool = ?true;
+
+    public func localOption(): async () {
+        let t1 = null : ?Int;
+        let t2 = ?42 : ?Int;
+        var t3 = null : ?Int;
+        var t4 = ?32 : ?Int;
+
+        // let a1 = switch t1 { case null 0; case (?x) x};
+        // let a2 = switch t1 { case null null; case (?x) (?(x + 1))};
+        var a2 : Int = 0;
+        switch t1 {
+            case null a2 := 0;
+            case (?x) a2 := x;
+        }
+    };
+
+    private func getOption(): ?Bool {
+        return ?false;
+    };
+
+    private func takeOption(a: ?Int): Int {
+        switch a {
+            case null { return 0 };
+            case (?x) { return x };
+        }
+    };
+
+     private func passOption(): () {
+        let a2 = takeOption(null);
+    };
+
+    private func callTuple(): () {
+        let x = getOption();
+    };
+
+    public func changeField(): async () {
+        fld2 := null;
+    }
+}