Provide builtin to reinterpret ascii byte strings as strings (#919)

* Provide builtin to reinterpret ascii byte strings as strings

* make fmt

src/base/BuiltIns.ml

@@ -181,6 +181,29 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct
       in
       pure @@ StringLit s
 
+    let to_ascii_arity = 1
+
+    let to_ascii_type = tfun_typ "'A" (fun_typ (tvar "'A") string_typ)
+
+    let to_ascii_elab _ ts =
+      match ts with
+      | [ PrimType pt ] -> (
+          match pt with
+          | Bystrx_typ _ | Bystr_typ ->
+              elab_tfun_with_args_no_gas to_ascii_type ts
+          | _ -> fail0 "Failed to elaborate" )
+      | _ -> fail0 "Failed to elaborate"
+
+    let to_ascii ls _ =
+      let%bind s =
+        match ls with
+        | [ ByStr x ] -> pure @@ Bystr.to_raw_bytes x
+        | [ ByStrX x ] -> pure @@ Bystrx.to_raw_bytes x
+        | _ -> builtin_fail (sprintf "String.to_ascii") ls
+      in
+      if validate_string_literal s then pure @@ StringLit s
+      else fail0 "String.to_ascii: Not printable"
+
     let strrev_arity = 1
 
     let strrev_type = tfun_typ "'A" (fun_typ (tvar "'A") (tvar "'A"))
@@ -1433,6 +1456,7 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct
                           ]
       | Builtin_strlen -> [String.strlen_arity, String.strlen_type, String.strlen_elab, String.strlen]
       | Builtin_to_string -> [String.to_string_arity, String.to_string_type, String.to_string_elab, String.to_string]
+      | Builtin_to_ascii -> [String.to_ascii_arity, String.to_ascii_type, String.to_ascii_elab, String.to_ascii]
       | Builtin_strrev -> [ String.strrev_arity, String.strrev_type, String.strrev_elab, String.strrev ]
       | Builtin_to_bystrx i -> [
         Crypto.to_bystrx_arity, Crypto.to_bystrx_type i, elab_id, Crypto.to_bystrx i;

src/base/Gas.ml

@@ -312,7 +312,8 @@ module ScillaGas (SR : Rep) (ER : Rep) = struct
                    GasGasCharge.ValueOf (GI.get_id i2) ) )
     | Builtin_strlen, [ s ] -> pure @@ GasGasCharge.SizeOf (GI.get_id s)
     | Builtin_strrev, [ s ] -> pure @@ GasGasCharge.SizeOf (GI.get_id s)
-    | Builtin_to_string, [ l ] -> pure @@ GasGasCharge.SizeOf (GI.get_id l)
+    | Builtin_to_string, [ l ] | Builtin_to_ascii, [ l ] ->
+        pure @@ GasGasCharge.SizeOf (GI.get_id l)
     | _ -> fail0 @@ "Gas cost error for string built-in"
 
   let crypto_coster op args types =
@@ -512,6 +513,7 @@ module ScillaGas (SR : Rep) (ER : Rep) = struct
     (* Strings *)
     | Builtin_strlen -> [([string_typ], string_coster); ([bystr_typ], string_coster);];
     | Builtin_to_string -> [([tvar "'A"], string_coster)];
+    | Builtin_to_ascii -> [([tvar "'A"], string_coster)];
 
     (* Block numbers *)
     | Builtin_blt -> [([bnum_typ;bnum_typ], bnum_coster)];

src/base/Syntax.ml

@@ -39,6 +39,7 @@ type builtin =
   | Builtin_strlen
   | Builtin_strrev
   | Builtin_to_string
+  | Builtin_to_ascii
   | Builtin_blt
   | Builtin_badd
   | Builtin_bsub
@@ -98,6 +99,7 @@ let pp_builtin b =
   | Builtin_strlen -> "strlen"
   | Builtin_strrev -> "strrev"
   | Builtin_to_string -> "to_string"
+  | Builtin_to_ascii -> "to_ascii"
   | Builtin_blt -> "blt"
   | Builtin_badd -> "badd"
   | Builtin_bsub -> "bsub"
@@ -147,6 +149,7 @@ let parse_builtin s loc =
   | "strlen" -> Builtin_strlen
   | "strrev" -> Builtin_strrev
   | "to_string" -> Builtin_to_string
+  | "to_ascii" -> Builtin_to_ascii
   | "blt" -> Builtin_blt
   | "badd" -> Builtin_badd
   | "bsub" -> Builtin_bsub

tests/eval/bad/Bad.ml

@@ -57,6 +57,7 @@ let explist =
     "let-error.scilexp";
     "list_to_map.scilexp";
     "string_error1.scilexp";
+    "string_error2.scilexp";
     "substr_err1.scilexp";
   ]
 

tests/eval/bad/gold/string_error2.scilexp.gold

@@ -0,0 +1,11 @@
+{
+  "gas_remaining": "4001754",
+  "errors": [
+    {
+      "error_message": "String.to_ascii: Not printable",
+      "start_location": { "file": "", "line": 0, "column": 0 },
+      "end_location": { "file": "", "line": 0, "column": 0 }
+    }
+  ],
+  "warnings": []
+}

tests/eval/bad/string_error2.scilexp

@@ -0,0 +1,2 @@
+let x = 0x11 in
+builtin to_ascii x

tests/eval/good/builtin-strings.scilexp

@@ -48,4 +48,7 @@ let bs_rev = builtin strrev bs in
 let bsx_rev = builtin strrev bsx in
 let s1_rev = builtin strrev s1 in
 
+let ascii_bs = 0x756e6c6f636b in
+let ascii = builtin to_ascii ascii_bs in
+
 res

tests/eval/good/gold/builtin-strings.scilexp.gold

@@ -1,5 +1,7 @@
 (String "scilla is awesome"),
-{ [s1_rev -> (String "emosewa si allics")],
+{ [ascii -> (String "unlock")],
+  [ascii_bs -> (ByStr6 0x756e6c6f636b)],
+  [s1_rev -> (String "emosewa si allics")],
   [bsx_rev -> (ByStr 0xab1212)],
   [bs_rev -> (ByStr3 0xab1212)],
   [len2 -> (Uint32 14)],
@@ -31,4 +33,4 @@
   [fsubstr -> <closure>],
   [fconcat -> <closure>],
   [feq -> <closure>] }
-Gas remaining: 4001457
+Gas remaining: 4001448