Merge pull request #27 from serokell/motoko-san/support-text-type

[DMS-47] Support text type

src/viper/prelude.ml

@@ -48,9 +48,13 @@ adt Option[T] {
   Some(some$0: T)
 }|prelude}
 
+let prelude_text_encoding : string = {prelude|/* Text encoding */
+function $concat(a: Int, b: Int): Int|prelude}
+
 let prelude_typed_references : string = {prelude|/* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]
@@ -64,6 +68,7 @@ let prelude reqs: string =
     prelude_array_encoding;
     prelude_tuple_encoding !(reqs.tuple_arities);
     prelude_option_encoding;
+    prelude_text_encoding;
     prelude_typed_references;
     "/* END PRELUDE */"
   ]

src/viper/trans.ml

@@ -113,6 +113,9 @@ type ctxt =
     ghost_conc : (ctxt -> exp -> exp) list ref;
   }
 
+(* All text literals are injectively mapped into int values *)
+let text_literals : (string, int) Hashtbl.t = Hashtbl.create 32
+
 let add_locals ctxt (locals : (id * T.typ) list) =
   let add (x, t) = Env.add x.it (Local, t) in
   { ctxt with ids = List.fold_right add locals ctxt.ids }
@@ -122,6 +125,17 @@ let self ctxt at =
   | Some id -> !!! at (LocalVar (!!! at id,!!! at RefT))
   | _ -> failwith "no self"
 
+let tr_string_literal at str =
+  let str_id =
+    match Hashtbl.find_opt text_literals str with
+    | None ->
+      let fresh_str_id = Hashtbl.length text_literals in
+      Hashtbl.add text_literals str fresh_str_id;
+      fresh_str_id
+    | Some id -> id
+  in
+  intLitE at str_id
+
 let rec extract_invariants : item list -> (par -> invariants -> invariants) = function
   | [] -> fun _ x -> x
   | { it = InvariantI (s, e); at; _ } :: p ->
@@ -672,8 +686,12 @@ and pat_match ctxt (scrut : M.exp) (p : M.pat) : exp list * (id * T.typ) list *
       let e_scrut = exp ctxt scrut in
       let rhs = !!(IntLitE n) in
       [ !!(EqCmpE (e_scrut, rhs)) ], [], ([], [])
+    | M.TextLit str ->
+      let e_scrut = exp ctxt scrut in
+      let rhs = tr_string_literal p.at str in
+      [ !!(EqCmpE (e_scrut, rhs)) ], [], ([], [])
     | M.PreLit _ -> failwith "Expected PreLit to be eliminated after typing"
-    | _         -> unsupported (p.at) (Arrange.lit !lit)
+    | _          -> unsupported (p.at) (Arrange.lit !lit)
     end
   | M.OptP p' ->
     let e_scrut = exp ctxt scrut in
@@ -812,6 +830,8 @@ and exp ctxt e =
        !!(IntLitE i)
     | M.NullLit ->
        noneE (e.at)
+    | M.TextLit str ->
+      tr_string_literal e.at str
     | _ ->
        unsupported e.at (Arrange.exp e)
     end
@@ -834,6 +854,7 @@ and exp ctxt e =
       | MulOp -> MulE (e1, e2)
       | DivOp -> DivE (e1, e2)
       | ModOp -> ModE (e1, e2)
+      | CatOp -> CallE ("$concat", [e1; e2])
       | _ -> unsupported e.at (Arrange.exp e))
   | M.OrE (e1, e2) ->
      !!(OrE (exp ctxt e1, exp ctxt e2))
@@ -931,6 +952,7 @@ and tr_typ' ctxt typ =
   match typ, 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.Text -> IntT   (* Viper has no native support for Text, so translate to uninterpreted Int values *)
   | _, T.Prim T.Bool -> BoolT
   | _, T.Array _ -> ArrayT     (* Viper arrays are not parameterised by element type *)
   | _, T.Opt   t -> OptionT (tr_typ ctxt t)
@@ -962,6 +984,7 @@ and typed_field 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"
+  | T.Prim T.Text -> "$text"
   | _ -> unsupported Source.no_region (Mo_types.Arrange_type.typ t)
 
 and array_size_inv at lhs n =

test/repl/ok/viper.stdout.ok

@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]

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@42.1)

test/viper/ok/array.vpr.ok

@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]

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@42.13--42.24)
+  [1] Assert might fail. Assertion $Self.u ==> $Self.v > 0 might not hold. (assertions.vpr@60.15--60.44)

test/viper/ok/assertions.vpr.ok

@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[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@65.15--65.42)

test/viper/ok/async.vpr.ok

@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[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@63.20--63.47)

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

@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]

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

@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]

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@34.1)

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

@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]

test/viper/ok/claim.vpr.ok

@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]

test/viper/ok/counter.silicon.ok

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

test/viper/ok/counter.vpr.ok

@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]

test/viper/ok/invariant.silicon.ok

@@ -1 +1 @@
-  [0] Postcondition of __init__ might not hold. Assertion $Self.count > 0 might not hold. (invariant.vpr@36.13--36.24)
+  [0] Postcondition of __init__ might not hold. Assertion $Self.count > 0 might not hold. (invariant.vpr@39.13--39.24)

test/viper/ok/invariant.vpr.ok

@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]

test/viper/ok/label-break-continue.silicon.ok

@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (label-break-continue.vpr@32.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (label-break-continue.vpr@33.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (label-break-continue.vpr@35.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (label-break-continue.vpr@36.1)

test/viper/ok/label-break-continue.vpr.ok

@@ -19,9 +19,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]

test/viper/ok/lits.silicon.ok

@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (lits.vpr@30.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (lits.vpr@31.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (lits.vpr@33.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (lits.vpr@34.1)

test/viper/ok/lits.vpr.ok

@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]

test/viper/ok/loop-invariant.silicon.ok

@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (loop-invariant.vpr@30.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (loop-invariant.vpr@31.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (loop-invariant.vpr@33.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (loop-invariant.vpr@34.1)

test/viper/ok/loop-invariant.vpr.ok

@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]

test/viper/ok/method-call.silicon.ok

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

test/viper/ok/method-call.vpr.ok

@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]

test/viper/ok/nats.silicon.ok

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

test/viper/ok/nats.vpr.ok

@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]

test/viper/ok/odd-even.silicon.ok

@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (odd-even.vpr@30.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (odd-even.vpr@31.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (odd-even.vpr@33.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (odd-even.vpr@34.1)

test/viper/ok/odd-even.vpr.ok

@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]

test/viper/ok/option.silicon.ok

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

test/viper/ok/option.vpr.ok

@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]

test/viper/ok/polymono.silicon.ok

@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (polymono.vpr@30.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (polymono.vpr@31.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (polymono.vpr@33.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (polymono.vpr@34.1)

test/viper/ok/polymono.vpr.ok

@@ -17,9 +17,12 @@ adt Option[T] {
   None()
   Some(some$0: T)
 }
+/* Text encoding */
+function $concat(a: Int, b: Int): Int
 /* Typed references */
 field $int: Int
 field $bool: Bool
+field $text: Int
 field $ref: Ref
 field $array: Array
 field $option_int: Option[Int]