[DMS-34] motoko-san: add basic support for Nat

src/viper/trans.ml

@@ -485,6 +485,8 @@ and exp ctxt e =
        !!(BoolLitE b)
     | M.IntLit i ->
        !!(IntLitE i)
+    | M.NatLit i ->
+       !!(IntLitE i)
     | _ ->
        unsupported e.at (Arrange.exp e)
     end
@@ -526,9 +528,7 @@ and rets t_opt =
     (match T.normalize t.note with
      | T.Tup [] -> []
      | T.Async (T.Fut, _, _) -> []
-     | T.Prim T.Int  -> [(!!! (Source.no_region) "$Res", !!! (Source.no_region) IntT)]
-     | T.Prim T.Bool -> [(!!! (Source.no_region) "$Res", !!! (Source.no_region) BoolT)]
-     | _ -> unsupported t.at (Arrange.typ t)
+     | typ -> [(!!! (Source.no_region) "$Res", tr_typ typ)]
     )
 
 and id id = { it = id.it; at = id.at; note = NoInfo }
@@ -540,5 +540,6 @@ and tr_typ typ =
 and tr_typ' typ =
   match T.normalize typ with
   | 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
   | _ -> unsupported Source.no_region (Mo_types.Arrange_type.typ (T.normalize typ))

test/viper/nats.mo

@@ -0,0 +1,27 @@
+// @verify
+
+actor Nats {
+
+  var x = 42 : Nat;
+
+  public func getZero() : async Nat {
+    return 0;
+  };
+
+  public func getX() : async Nat {
+    return x;
+  };
+
+  public func double() : async () {
+    x := x * 2;
+  };
+
+  public func natToInt(n : Nat) : async Int {
+    return n;
+  };
+
+  public func add(n : Nat, m : Int) : async Int {
+    return n + m;
+  };
+
+};

test/viper/ok/nats.silicon.ok

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

test/viper/ok/nats.vpr.ok

@@ -0,0 +1,65 @@
+define $Perm($Self) ((true && acc(($Self).x,write)))
+define $Inv($Self) (true)
+method __init__($Self: Ref)
+
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { 
+      ($Self).x := 42 
+    }
+field x: Int
+method getZero($Self: Ref)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { 
+      $Res := 0
+      goto $Ret
+      label $Ret 
+    }
+method getX($Self: Ref)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { 
+      $Res := ($Self).x
+      goto $Ret
+      label $Ret 
+    }
+method double($Self: Ref)
+
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { 
+      ($Self).x := (($Self).x * 2)
+      label $Ret 
+    }
+method natToInt($Self: Ref, n: Int)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { 
+      $Res := n
+      goto $Ret
+      label $Ret 
+    }
+method add($Self: Ref, n: Int, m: Int)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { 
+      $Res := (n + m)
+      goto $Ret
+      label $Ret 
+    }