From e9b098b31cc3fec67c077dc84f1b6a0e1c7a3d53 Mon Sep 17 00:00:00 2001 From: Vaivaswatha Nagaraj Date: Tue, 10 Nov 2020 14:43:07 +0530 Subject: [PATCH 1/8] Add substr and concat for ByStr Scilla type --- src/base/BuiltIns.ml | 23 +- src/base/Gas.ml | 19 + src/base/Literal.ml | 6 + tests/eval/good/builtin-eq-bystr.scilexp | 23 +- .../good/gold/builtin-eq-bystr.scilexp.gold | 23 +- tests/typecheck/good/builtin-eq-bystr.scilexp | 24 +- .../good/gold/builtin-eq-bystr.scilexp.gold | 622 +++++++++++++++++- 7 files changed, 722 insertions(+), 18 deletions(-) diff --git a/src/base/BuiltIns.ml b/src/base/BuiltIns.ml index be4ae90e1..a1a62e187 100644 --- a/src/base/BuiltIns.ml +++ b/src/base/BuiltIns.ml @@ -837,6 +837,20 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct | [ ByStrX bs ] -> pure @@ ByStr (Bystrx.to_bystr bs) | _ -> builtin_fail "Crypto.to_bystr" ls + let substr_arity = 3 + + let substr_type = + fun_typ bystr_typ @@ fun_typ uint32_typ @@ fun_typ uint32_typ bystr_typ + + let substr ls _ = + try + match ls with + | [ ByStr x; UintLit (Uint32L s); UintLit (Uint32L e) ] -> + pure + @@ ByStr (Bystr.sub x ~pos:(Uint32.to_int s) ~len:(Uint32.to_int e)) + | _ -> builtin_fail "Crypto.substr" ls + with Invalid_argument msg -> builtin_fail ("Crypto.substr: " ^ msg) ls + let to_uint256_type = tfun_typ "'A" @@ fun_typ (tvar "'A") uint256_typ let to_uint256_arity = 1 @@ -908,11 +922,14 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct match ts with | [ PrimType (Bystrx_typ w1); PrimType (Bystrx_typ w2) ] -> elab_tfun_with_args_no_gas sc (ts @ [ bystrx_typ (w1 + w2) ]) + | [ PrimType Bystr_typ; PrimType Bystr_typ ] -> + elab_tfun_with_args_no_gas sc (ts @ [ bystr_typ ]) | _ -> fail0 "Failed to elaborate" let concat ls _ = match ls with | [ ByStrX bs1; ByStrX bs2 ] -> pure @@ ByStrX (Bystrx.concat bs1 bs2) + | [ ByStr bs1; ByStr bs2 ] -> pure @@ ByStr (Bystr.concat bs1 bs2) | _ -> builtin_fail "Crypto.concat" ls let[@warning "-32"] ec_gen_key_pair_type = @@ -1299,6 +1316,7 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct (* All built-in functions *) let built_in_multidict : builtin -> built_in_record list = function + (* Polymorphic builtins *) | Builtin_eq -> [String.eq_arity, String.eq_type, elab_id, String.eq; BNum.eq_arity, BNum.eq_type, elab_id , BNum.eq; Crypto.eq_arity, Crypto.eq_type, Crypto.eq_elab, Crypto.eq; @@ -1308,8 +1326,9 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct Crypto.concat_arity, Crypto.concat_type, Crypto.concat_elab, Crypto.concat] | Builtin_to_uint256 -> [Crypto.to_uint256_arity, Crypto.to_uint256_type, Crypto.to_uint256_elab, Crypto.to_uint256; Uint.to_uint_arity, Uint.to_uint_type, Uint.to_uint_elab Bits256, Uint.to_uint256] - (* Strings *) - | Builtin_substr -> [String.substr_arity, String.substr_type, elab_id, String.substr] + | Builtin_substr -> [String.substr_arity, String.substr_type, elab_id, String.substr; + Crypto.substr_arity, Crypto.substr_type, elab_id, Crypto.substr + ] | Builtin_strlen -> [String.strlen_arity, String.strlen_type, elab_id, String.strlen] | Builtin_to_string -> [String.to_string_arity, String.to_string_type, String.to_string_elab, String.to_string] diff --git a/src/base/Gas.ml b/src/base/Gas.ml index cc7780126..a7af878e0 100644 --- a/src/base/Gas.ml +++ b/src/base/Gas.ml @@ -320,6 +320,19 @@ module ScillaGas (SR : Rep) (ER : Rep) = struct match (op, types, args) with | Builtin_eq, [ PrimType Bystr_typ; PrimType Bystr_typ ], [ a1; _ ] -> pure @@ GasGasCharge.SizeOf (GI.get_id a1) + | ( Builtin_substr, + [ + PrimType Bystr_typ; + PrimType (Uint_typ Bits32); + PrimType (Uint_typ Bits32); + ], + [ s; i1; i2 ] ) -> + pure + @@ GasGasCharge.MinOf + ( GasGasCharge.SizeOf (GI.get_id s), + GasGasCharge.SumOf + ( GasGasCharge.ValueOf (GI.get_id i1), + GasGasCharge.ValueOf (GI.get_id i2) ) ) | Builtin_eq, [ a1; a2 ], _ when is_bystrx_type a1 && is_bystrx_type a2 && Option.(value_exn (bystrx_width a1) = value_exn (bystrx_width a2)) @@ -369,6 +382,11 @@ module ScillaGas (SR : Rep) (ER : Rep) = struct ( GasGasCharge.SizeOf (GI.get_id prefix), GasGasCharge.SizeOf (GI.get_id addr) ), GasGasCharge.StaticCost base )) + | Builtin_concat, [ PrimType Bystr_typ; PrimType Bystr_typ ], [ s1; s2 ] -> + pure + @@ GasGasCharge.SumOf + ( GasGasCharge.SizeOf (GI.get_id s1), + GasGasCharge.SizeOf (GI.get_id s2) ) | Builtin_concat, [ a1; a2 ], _ when is_bystrx_type a1 && is_bystrx_type a2 -> pure @@ -477,6 +495,7 @@ module ScillaGas (SR : Rep) (ER : Rep) = struct (* Crypto *) (Builtin_eq, [tvar "'A"; tvar "'A"], crypto_coster); (Builtin_to_bystr, [tvar "'A"], crypto_coster); + (Builtin_substr, [bystr_typ; uint32_typ; uint32_typ], crypto_coster); (Builtin_bech32_to_bystr20, [string_typ;string_typ], crypto_coster); (Builtin_bystr20_to_bech32, [string_typ;bystrx_typ address_length], crypto_coster); (Builtin_to_uint256, [tvar "'A"], crypto_coster); diff --git a/src/base/Literal.ml b/src/base/Literal.ml index 34ed7593a..a3648a8ef 100644 --- a/src/base/Literal.ml +++ b/src/base/Literal.ml @@ -79,6 +79,8 @@ module type ScillaLiteral = sig val equal : t -> t -> bool + val sub : t -> pos:int -> len:int -> t + val concat : t -> t -> t end @@ -252,6 +254,8 @@ module MkLiteral (T : ScillaType) = struct val equal : t -> t -> bool + val sub : t -> pos:int -> len:int -> t + val concat : t -> t -> t end @@ -278,6 +282,8 @@ module MkLiteral (T : ScillaType) = struct let equal = String.equal + let sub = String.sub + let concat = ( ^ ) end diff --git a/tests/eval/good/builtin-eq-bystr.scilexp b/tests/eval/good/builtin-eq-bystr.scilexp index 60aa8deae..1225532d9 100644 --- a/tests/eval/good/builtin-eq-bystr.scilexp +++ b/tests/eval/good/builtin-eq-bystr.scilexp @@ -7,4 +7,25 @@ let cc = builtin to_bystr c in let r1 = builtin eq aa bb in let r11 = negb r1 in let r2 = builtin eq aa cc in -andb r11 r2 +let res1 = andb r11 r2 in + +let ab = builtin concat a b in +let ab2 = 0x0f0fbfbf in + +let zero = Uint32 0 in +let one = Uint32 1 in +let two = Uint32 2 in + +let a = builtin to_bystr a in +let a1 = builtin substr a zero one in +let a2 = builtin substr a one one in +let aa1 = builtin substr a zero two in +let aa2 = builtin concat a1 a2 in +let res2 = builtin eq aa1 aa2 in +let res3 = builtin eq aa1 a in +let res4 = andb res2 res3 in + +let res5 = builtin eq ab ab2 in +let res6 = andb res4 res5 in + +res6 diff --git a/tests/eval/good/gold/builtin-eq-bystr.scilexp.gold b/tests/eval/good/gold/builtin-eq-bystr.scilexp.gold index 292a832f5..364aeccdf 100644 --- a/tests/eval/good/gold/builtin-eq-bystr.scilexp.gold +++ b/tests/eval/good/gold/builtin-eq-bystr.scilexp.gold @@ -1,11 +1,26 @@ (True), -{ [r2 -> (True)], +{ [res6 -> (True)], + [res5 -> (True)], + [res4 -> (True)], + [res3 -> (True)], + [res2 -> (True)], + [aa2 -> (ByStr 0x0f0f)], + [aa1 -> (ByStr 0x0f0f)], + [a2 -> (ByStr 0x0f)], + [a1 -> (ByStr 0x0f)], + [a -> (ByStr 0x0f0f)], + [two -> (Uint32 2)], + [one -> (Uint32 1)], + [zero -> (Uint32 0)], + [ab2 -> (ByStr4 0x0f0fbfbf)], + [ab -> (ByStr4 0x0f0fbfbf)], + [res1 -> (True)], + [r2 -> (True)], [r11 -> (True)], [r1 -> (False)], [cc -> (ByStr 0x0f0f)], [bb -> (ByStr 0xbfbf)], [aa -> (ByStr 0x0f0f)], [c -> (ByStr2 0x0f0f)], - [b -> (ByStr2 0xbfbf)], - [a -> (ByStr2 0x0f0f)] } -Gas remaining: 4001726 + [b -> (ByStr2 0xbfbf)] } +Gas remaining: 4001674 diff --git a/tests/typecheck/good/builtin-eq-bystr.scilexp b/tests/typecheck/good/builtin-eq-bystr.scilexp index 60aa8deae..4504634b4 100644 --- a/tests/typecheck/good/builtin-eq-bystr.scilexp +++ b/tests/typecheck/good/builtin-eq-bystr.scilexp @@ -7,4 +7,26 @@ let cc = builtin to_bystr c in let r1 = builtin eq aa bb in let r11 = negb r1 in let r2 = builtin eq aa cc in -andb r11 r2 + +let res1 = andb r11 r2 in + +let ab = builtin concat a b in +let ab2 = 0x0f0fbfbf in + +let zero = Uint32 0 in +let one = Uint32 1 in +let two = Uint32 2 in + +let a = builtin to_bystr a in +let a1 = builtin substr a zero one in +let a2 = builtin substr a one one in +let aa1 = builtin substr a zero two in +let aa2 = builtin concat a1 a2 in +let res2 = builtin eq aa1 aa2 in +let res3 = builtin eq aa1 a in +let res4 = andb res2 res3 in + +let res5 = builtin eq ab ab2 in +let res6 = andb res4 res5 in + +res6 diff --git a/tests/typecheck/good/gold/builtin-eq-bystr.scilexp.gold b/tests/typecheck/good/gold/builtin-eq-bystr.scilexp.gold index 23cec778d..63d541baa 100644 --- a/tests/typecheck/good/gold/builtin-eq-bystr.scilexp.gold +++ b/tests/typecheck/good/gold/builtin-eq-bystr.scilexp.gold @@ -252,18 +252,32 @@ "column": 26 } }, + { + "vname": "res1", + "type": "Bool", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 11, + "column": 5 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 11, + "column": 9 + } + }, { "vname": "andb", "type": "Bool -> Bool -> Bool", "start_location": { "file": "typecheck/good/builtin-eq-bystr.scilexp", - "line": 10, - "column": 1 + "line": 11, + "column": 12 }, "end_location": { "file": "typecheck/good/builtin-eq-bystr.scilexp", - "line": 10, - "column": 5 + "line": 11, + "column": 16 } }, { @@ -271,27 +285,615 @@ "type": "Bool", "start_location": { "file": "typecheck/good/builtin-eq-bystr.scilexp", - "line": 10, + "line": 11, + "column": 17 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 11, + "column": 20 + } + }, + { + "vname": "r2", + "type": "Bool", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 11, + "column": 21 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 11, + "column": 23 + } + }, + { + "vname": "ab", + "type": "ByStr4", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 13, + "column": 5 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 13, + "column": 7 + } + }, + { + "vname": "a", + "type": "ByStr2", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 13, + "column": 25 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 13, + "column": 26 + } + }, + { + "vname": "b", + "type": "ByStr2", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 13, + "column": 27 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 13, + "column": 28 + } + }, + { + "vname": "ab2", + "type": "ByStr4", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 14, + "column": 5 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 14, + "column": 8 + } + }, + { + "vname": "zero", + "type": "Uint32", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 16, + "column": 5 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 16, + "column": 9 + } + }, + { + "vname": "one", + "type": "Uint32", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 17, + "column": 5 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 17, + "column": 8 + } + }, + { + "vname": "two", + "type": "Uint32", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 18, + "column": 5 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 18, + "column": 8 + } + }, + { + "vname": "a", + "type": "ByStr", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 20, + "column": 5 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 20, "column": 6 + } + }, + { + "vname": "a", + "type": "ByStr2", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 20, + "column": 26 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 20, + "column": 27 + } + }, + { + "vname": "a1", + "type": "ByStr", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 21, + "column": 5 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 21, + "column": 7 + } + }, + { + "vname": "a", + "type": "ByStr", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 21, + "column": 25 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 21, + "column": 26 + } + }, + { + "vname": "zero", + "type": "Uint32", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 21, + "column": 27 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 21, + "column": 31 + } + }, + { + "vname": "one", + "type": "Uint32", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 21, + "column": 32 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 21, + "column": 35 + } + }, + { + "vname": "a2", + "type": "ByStr", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 22, + "column": 5 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 22, + "column": 7 + } + }, + { + "vname": "a", + "type": "ByStr", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 22, + "column": 25 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 22, + "column": 26 + } + }, + { + "vname": "one", + "type": "Uint32", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 22, + "column": 27 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 22, + "column": 30 + } + }, + { + "vname": "one", + "type": "Uint32", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 22, + "column": 31 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 22, + "column": 34 + } + }, + { + "vname": "aa1", + "type": "ByStr", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 23, + "column": 5 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 23, + "column": 8 + } + }, + { + "vname": "a", + "type": "ByStr", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 23, + "column": 26 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 23, + "column": 27 + } + }, + { + "vname": "zero", + "type": "Uint32", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 23, + "column": 28 }, "end_location": { "file": "typecheck/good/builtin-eq-bystr.scilexp", - "line": 10, + "line": 23, + "column": 32 + } + }, + { + "vname": "two", + "type": "Uint32", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 23, + "column": 33 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 23, + "column": 36 + } + }, + { + "vname": "aa2", + "type": "ByStr", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 24, + "column": 5 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 24, + "column": 8 + } + }, + { + "vname": "a1", + "type": "ByStr", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 24, + "column": 26 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 24, + "column": 28 + } + }, + { + "vname": "a2", + "type": "ByStr", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 24, + "column": 29 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 24, + "column": 31 + } + }, + { + "vname": "res2", + "type": "Bool", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 25, + "column": 5 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 25, "column": 9 } }, { - "vname": "r2", + "vname": "aa1", + "type": "ByStr", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 25, + "column": 23 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 25, + "column": 26 + } + }, + { + "vname": "aa2", + "type": "ByStr", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 25, + "column": 27 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 25, + "column": 30 + } + }, + { + "vname": "res3", "type": "Bool", "start_location": { "file": "typecheck/good/builtin-eq-bystr.scilexp", - "line": 10, - "column": 10 + "line": 26, + "column": 5 }, "end_location": { "file": "typecheck/good/builtin-eq-bystr.scilexp", - "line": 10, + "line": 26, + "column": 9 + } + }, + { + "vname": "aa1", + "type": "ByStr", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 26, + "column": 23 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 26, + "column": 26 + } + }, + { + "vname": "a", + "type": "ByStr", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 26, + "column": 27 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 26, + "column": 28 + } + }, + { + "vname": "res4", + "type": "Bool", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 27, + "column": 5 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 27, + "column": 9 + } + }, + { + "vname": "andb", + "type": "Bool -> Bool -> Bool", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 27, "column": 12 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 27, + "column": 16 + } + }, + { + "vname": "res2", + "type": "Bool", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 27, + "column": 17 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 27, + "column": 21 + } + }, + { + "vname": "res3", + "type": "Bool", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 27, + "column": 22 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 27, + "column": 26 + } + }, + { + "vname": "res5", + "type": "Bool", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 29, + "column": 5 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 29, + "column": 9 + } + }, + { + "vname": "ab", + "type": "ByStr4", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 29, + "column": 23 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 29, + "column": 25 + } + }, + { + "vname": "ab2", + "type": "ByStr4", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 29, + "column": 26 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 29, + "column": 29 + } + }, + { + "vname": "res6", + "type": "Bool", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 30, + "column": 5 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 30, + "column": 9 + } + }, + { + "vname": "andb", + "type": "Bool -> Bool -> Bool", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 30, + "column": 12 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 30, + "column": 16 + } + }, + { + "vname": "res4", + "type": "Bool", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 30, + "column": 17 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 30, + "column": 21 + } + }, + { + "vname": "res5", + "type": "Bool", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 30, + "column": 22 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 30, + "column": 26 + } + }, + { + "vname": "res6", + "type": "Bool", + "start_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 32, + "column": 1 + }, + "end_location": { + "file": "typecheck/good/builtin-eq-bystr.scilexp", + "line": 32, + "column": 5 } } ], From f386522b7342d7afdf38c1f136fab9e31c55c48a Mon Sep 17 00:00:00 2001 From: Vaivaswatha Nagaraj Date: Fri, 13 Nov 2020 13:45:49 +0530 Subject: [PATCH 2/8] Add builtin to_bystrx --- src/base/BuiltIns.ml | 14 + src/base/Gas.ml | 139 +++++----- src/base/Syntax.ml | 19 +- tests/eval/good/gold/to_bystr.scilexp.gold | 10 +- tests/eval/good/to_bystr.scilexp | 19 +- tests/typecheck/good/Good.ml | 1 + .../typecheck/good/gold/to_bystr.scilexp.gold | 257 ++++++++++++++++++ tests/typecheck/good/to_bystr.scilexp | 19 ++ 8 files changed, 401 insertions(+), 77 deletions(-) create mode 100644 tests/typecheck/good/gold/to_bystr.scilexp.gold create mode 100644 tests/typecheck/good/to_bystr.scilexp diff --git a/src/base/BuiltIns.ml b/src/base/BuiltIns.ml index a1a62e187..0ff91c036 100644 --- a/src/base/BuiltIns.ml +++ b/src/base/BuiltIns.ml @@ -822,6 +822,19 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct let ripemd160hash ls _ = hash_helper ripemd160_hasher "ripemd160hash" address_length ls + (* ByStr -> Option ByStrX *) + let to_bystrx_type x = fun_typ bystr_typ (option_typ (bystrx_typ x)) + + let to_bystrx_arity = 1 + + let to_bystrx x ls _ = + match ls with + | [ ByStr bs ] -> ( + match Bystrx.of_raw_bytes x (Bystr.to_raw_bytes bs) with + | Some l' -> some_lit (ByStrX l') + | None -> pure @@ none_lit (bystrx_typ x) ) + | _ -> builtin_fail "Crypto.to_bystr" ls + (* ByStrX -> ByStr *) let to_bystr_type = tfun_typ "'A" @@ fun_typ (tvar "'A") bystr_typ @@ -1342,6 +1355,7 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct | Builtin_keccak256hash -> [Crypto.hash_arity, Crypto.hash_type,Crypto.hash_elab, Crypto.keccak256hash] | Builtin_ripemd160hash -> [Crypto.hash_arity, Crypto.ripemd160hash_type,Crypto.hash_elab, Crypto.ripemd160hash] | Builtin_to_bystr -> [Crypto.to_bystr_arity, Crypto.to_bystr_type, Crypto.to_bystr_elab, Crypto.to_bystr] + | Builtin_to_bystrx i -> [Crypto.to_bystrx_arity, Crypto.to_bystrx_type i, elab_id, Crypto.to_bystrx i] | Builtin_bech32_to_bystr20 -> [Crypto.bech32_to_bystr20_arity, Crypto.bech32_to_bystr20_type, elab_id, Crypto.bech32_to_bystr20] | Builtin_bystr20_to_bech32 -> [Crypto.bystr20_to_bech32_arity, Crypto.bystr20_to_bech32_type, elab_id, Crypto.bystr20_to_bech32] | Builtin_schnorr_verify -> [Crypto.schnorr_verify_arity, Crypto.schnorr_verify_type, elab_id, Crypto.schnorr_verify] diff --git a/src/base/Gas.ml b/src/base/Gas.ml index a7af878e0..16988ec8e 100644 --- a/src/base/Gas.ml +++ b/src/base/Gas.ml @@ -373,6 +373,8 @@ module ScillaGas (SR : Rep) (ER : Rep) = struct GasGasCharge.ProdOf (GasGasCharge.StaticCost 15, x) )) | Builtin_to_bystr, [ a ], _ when is_bystrx_type a -> pure (GasGasCharge.StaticCost (Option.value_exn (bystrx_width a))) + | Builtin_to_bystrx i, [ PrimType Bystr_typ ], _ -> + pure (GasGasCharge.StaticCost i) | Builtin_bech32_to_bystr20, _, [ prefix; addr ] | Builtin_bystr20_to_bech32, _, [ prefix; addr ] -> let base = 4 in @@ -478,89 +480,85 @@ module ScillaGas (SR : Rep) (ER : Rep) = struct [@@@ocamlformat "disable"] (* built-in op costs are propotional to size of data they operate on. *) - let builtin_records : builtin_record list = [ - (* Strings *) - (Builtin_eq, [string_typ;string_typ], string_coster); - (Builtin_concat, [string_typ;string_typ], string_coster); - (Builtin_substr, [string_typ; tvar "'A"; tvar "'A"], string_coster); - (Builtin_strlen, [string_typ], string_coster); - (Builtin_to_string, [tvar "'A"], string_coster); + let builtin_records_find = function + (* Polymorhpic *) + | Builtin_eq -> [ + ([string_typ;string_typ], string_coster); + ([bnum_typ;bnum_typ], bnum_coster); + ([tvar "'A"; tvar "'A"], crypto_coster); + ([tvar "'A"; tvar "'A"], int_coster) + ]; + | Builtin_substr -> [ + ([string_typ; tvar "'A"; tvar "'A"], string_coster); + ([bystr_typ; uint32_typ; uint32_typ], crypto_coster) + ]; + | Builtin_concat -> [ + ([string_typ;string_typ], string_coster); + ([tvar "'A"; tvar "'A"], crypto_coster) + ]; + | Builtin_to_uint256 -> [ + ([tvar "'A"], crypto_coster); ([tvar "'A"], int_conversion_coster 256) + ]; + + (* Strings *) + | Builtin_strlen -> [([string_typ], string_coster)]; + | Builtin_to_string -> [([tvar "'A"], string_coster)]; (* Block numbers *) - (Builtin_eq, [bnum_typ;bnum_typ], bnum_coster); - (Builtin_blt, [bnum_typ;bnum_typ], bnum_coster); - (Builtin_badd, [bnum_typ;tvar "'A"], bnum_coster); - (Builtin_bsub, [bnum_typ;bnum_typ], bnum_coster); + | Builtin_blt -> [([bnum_typ;bnum_typ], bnum_coster)]; + | Builtin_badd -> [([bnum_typ;tvar "'A"], bnum_coster)]; + | Builtin_bsub -> [([bnum_typ;bnum_typ], bnum_coster)]; (* Crypto *) - (Builtin_eq, [tvar "'A"; tvar "'A"], crypto_coster); - (Builtin_to_bystr, [tvar "'A"], crypto_coster); - (Builtin_substr, [bystr_typ; uint32_typ; uint32_typ], crypto_coster); - (Builtin_bech32_to_bystr20, [string_typ;string_typ], crypto_coster); - (Builtin_bystr20_to_bech32, [string_typ;bystrx_typ address_length], crypto_coster); - (Builtin_to_uint256, [tvar "'A"], crypto_coster); - (Builtin_sha256hash, [tvar "'A"], crypto_coster); - (Builtin_keccak256hash, [tvar "'A"], crypto_coster); - (Builtin_ripemd160hash, [tvar "'A"], crypto_coster); - (Builtin_schnorr_verify, [bystrx_typ pubkey_len; bystr_typ; bystrx_typ signature_len], crypto_coster); - (Builtin_ecdsa_verify, [bystrx_typ Secp256k1Wrapper.pubkey_len; bystr_typ; bystrx_typ Secp256k1Wrapper.signature_len], crypto_coster); - (Builtin_concat, [tvar "'A"; tvar "'A"], crypto_coster); - (Builtin_schnorr_get_address, [bystrx_typ pubkey_len], crypto_coster); - (Builtin_alt_bn128_G1_add, [g1point_type; g1point_type], crypto_coster); - (Builtin_alt_bn128_G1_mul, [g1point_type; scalar_type], crypto_coster); - (Builtin_alt_bn128_pairing_product, [g1g2pair_list_type], crypto_coster); + | Builtin_to_bystr -> [([tvar "'A"], crypto_coster)]; + | Builtin_to_bystrx _ -> [([tvar "'A"], crypto_coster)]; + | Builtin_bech32_to_bystr20 -> [([string_typ;string_typ], crypto_coster)]; + | Builtin_bystr20_to_bech32 -> [([string_typ;bystrx_typ address_length], crypto_coster)]; + | Builtin_sha256hash -> [([tvar "'A"], crypto_coster)]; + | Builtin_keccak256hash -> [([tvar "'A"], crypto_coster)]; + | Builtin_ripemd160hash -> [([tvar "'A"], crypto_coster)]; + | Builtin_schnorr_verify -> [([bystrx_typ pubkey_len; bystr_typ; bystrx_typ signature_len], crypto_coster)]; + | Builtin_ecdsa_verify -> [([bystrx_typ Secp256k1Wrapper.pubkey_len; bystr_typ; bystrx_typ Secp256k1Wrapper.signature_len], crypto_coster)]; + | Builtin_schnorr_get_address -> [([bystrx_typ pubkey_len], crypto_coster)]; + | Builtin_alt_bn128_G1_add -> [([g1point_type; g1point_type], crypto_coster)]; + | Builtin_alt_bn128_G1_mul -> [([g1point_type; scalar_type], crypto_coster)]; + | Builtin_alt_bn128_pairing_product -> [([g1g2pair_list_type], crypto_coster)]; (* Maps *) - (Builtin_contains, [tvar "'A"; tvar "'A"], map_coster); - (Builtin_put, [tvar "'A"; tvar "'A"; tvar "'A"], map_coster); - (Builtin_get, [tvar "'A"; tvar "'A"], map_coster); - (Builtin_remove, [tvar "'A"; tvar "'A"], map_coster); - (Builtin_to_list, [tvar "'A"], map_coster); - (Builtin_size, [tvar "'A"], map_coster); + | Builtin_contains -> [([tvar "'A"; tvar "'A"], map_coster)]; + | Builtin_put -> [([tvar "'A"; tvar "'A"; tvar "'A"], map_coster)]; + | Builtin_get -> [([tvar "'A"; tvar "'A"], map_coster)]; + | Builtin_remove -> [([tvar "'A"; tvar "'A"], map_coster)]; + | Builtin_to_list -> [([tvar "'A"], map_coster)]; + | Builtin_size -> [([tvar "'A"], map_coster)]; (* Integers *) - (Builtin_eq, [tvar "'A"; tvar "'A"], int_coster); - (Builtin_lt, [tvar "'A"; tvar "'A"], int_coster); - (Builtin_add, [tvar "'A"; tvar "'A"], int_coster); - (Builtin_sub, [tvar "'A"; tvar "'A"], int_coster); - (Builtin_mul, [tvar "'A"; tvar "'A"], int_coster); - (Builtin_div, [tvar "'A"; tvar "'A"], int_coster); - (Builtin_rem, [tvar "'A"; tvar "'A"], int_coster); - (Builtin_pow, [tvar "'A"; uint32_typ], int_coster); - (Builtin_isqrt, [tvar "'A"], int_coster); + | Builtin_lt -> [([tvar "'A"; tvar "'A"], int_coster)]; + | Builtin_add -> [([tvar "'A"; tvar "'A"], int_coster)]; + | Builtin_sub -> [([tvar "'A"; tvar "'A"], int_coster)]; + | Builtin_mul -> [([tvar "'A"; tvar "'A"], int_coster)]; + | Builtin_div -> [([tvar "'A"; tvar "'A"], int_coster)]; + | Builtin_rem -> [([tvar "'A"; tvar "'A"], int_coster)]; + | Builtin_pow -> [([tvar "'A"; uint32_typ], int_coster)]; + | Builtin_isqrt -> [([tvar "'A"], int_coster)]; - (Builtin_to_int32, [tvar "'A"], int_conversion_coster 32); - (Builtin_to_int64, [tvar "'A"], int_conversion_coster 64); - (Builtin_to_int128, [tvar "'A"], int_conversion_coster 128); - (Builtin_to_int256, [tvar "'A"], int_conversion_coster 256); - (Builtin_to_uint32, [tvar "'A"], int_conversion_coster 32); - (Builtin_to_uint64, [tvar "'A"], int_conversion_coster 64); - (Builtin_to_uint128, [tvar "'A"], int_conversion_coster 128); - (Builtin_to_uint256, [tvar "'A"], int_conversion_coster 256); + | Builtin_to_int32 -> [([tvar "'A"], int_conversion_coster 32)]; + | Builtin_to_int64 -> [([tvar "'A"], int_conversion_coster 64)]; + | Builtin_to_int128 -> [([tvar "'A"], int_conversion_coster 128)]; + | Builtin_to_int256 -> [([tvar "'A"], int_conversion_coster 256)]; + | Builtin_to_uint32 -> [([tvar "'A"], int_conversion_coster 32)]; + | Builtin_to_uint64 -> [([tvar "'A"], int_conversion_coster 64)]; + | Builtin_to_uint128 -> [([tvar "'A"], int_conversion_coster 128)]; - (Builtin_to_nat, [uint32_typ], to_nat_coster); - ] + | Builtin_to_nat -> [([uint32_typ], to_nat_coster)]; [@@@ocamlformat "enable"] - let builtin_hashtbl = - let open Caml in - let ht : (builtin, builtin_record list) Hashtbl.t = Hashtbl.create 64 in - List.iter - (fun row -> - let opname, _, _ = row in - match Hashtbl.find_opt ht opname with - | Some p -> Hashtbl.add ht opname (row :: p) - | None -> Hashtbl.add ht opname [ row ]) - builtin_records; - ht - let builtin_cost (op, _) arg_types arg_ids = - let matcher (name, types, fcoster) = + let matcher (types, fcoster) = (* The names and type list lengths must match and *) if - [%equal: Syntax.builtin] name op - && List.length types = List.length arg_types + List.length types = List.length arg_types && List.for_all2_exn ~f:(fun t1 t2 -> (* the types should match *) @@ -575,11 +573,8 @@ module ScillaGas (SR : Rep) (ER : Rep) = struct let msg = sprintf "Unable to determine gas cost for \"%s\"" (pp_builtin op) in - let dict = - match Caml.Hashtbl.find_opt builtin_hashtbl op with - | Some rows -> rows - | None -> [] + let%bind _, cost = + tryM (builtin_records_find op) ~f:matcher ~msg:(fun () -> mk_error0 msg) in - let%bind _, cost = tryM dict ~f:matcher ~msg:(fun () -> mk_error0 msg) in pure cost end diff --git a/src/base/Syntax.ml b/src/base/Syntax.ml index 8dcd9c778..81f024e3f 100644 --- a/src/base/Syntax.ml +++ b/src/base/Syntax.ml @@ -46,6 +46,7 @@ type builtin = | Builtin_keccak256hash | Builtin_ripemd160hash | Builtin_to_bystr + | Builtin_to_bystrx of int | Builtin_bech32_to_bystr20 | Builtin_bystr20_to_bech32 | Builtin_schnorr_verify @@ -102,6 +103,7 @@ let pp_builtin b = | Builtin_keccak256hash -> "keccak256hash" | Builtin_ripemd160hash -> "ripemd160hash" | Builtin_to_bystr -> "to_bystr" + | Builtin_to_bystrx i -> "to_bystr" ^ Int.to_string i | Builtin_bech32_to_bystr20 -> "bech32_to_bystr20" | Builtin_bystr20_to_bech32 -> "bystr20_to_bech32" | Builtin_schnorr_verify -> "schnorr_verify" @@ -134,6 +136,7 @@ let pp_builtin b = | Builtin_to_nat -> "to_nat" let parse_builtin s loc = + match s with | "eq" -> Builtin_eq | "concat" -> Builtin_concat @@ -178,7 +181,21 @@ let parse_builtin s loc = | "to_uint64" -> Builtin_to_uint64 | "to_uint128" -> Builtin_to_uint128 | "to_nat" -> Builtin_to_nat - | _ -> raise (SyntaxError (sprintf "\"%s\" is not a builtin" s, loc)) + | _ -> + let err = (SyntaxError (sprintf "\"%s\" is not a builtin" s, loc)) in + (* Check for "bystrx". Not using Str (regex) to keep it fast. *) + try + let n = (String.length "to_bystr") in + if String.equal (String.sub s ~pos:0 ~len:n) "to_bystr" + then + let i = int_of_string (String.sub s ~pos:n ~len:((String.length s) - n)) in + Builtin_to_bystrx i + else + raise err + with + | Invalid_argument _ + | Failure _ -> + raise err (*******************************************************) (* Types of components *) diff --git a/tests/eval/good/gold/to_bystr.scilexp.gold b/tests/eval/good/gold/to_bystr.scilexp.gold index 4337dfd71..217c68e5b 100644 --- a/tests/eval/good/gold/to_bystr.scilexp.gold +++ b/tests/eval/good/gold/to_bystr.scilexp.gold @@ -1,3 +1,7 @@ -(ByStr 0xfb19), -{ [x -> (ByStr2 0xfb19)] } -Gas remaining: 4001753 +(True), +{ [res2 -> (True)], + [xx_opt -> (None)], + [res1 -> (True)], + [y -> (ByStr 0xfb19)], + [x -> (ByStr2 0xfb19)] } +Gas remaining: 4001731 diff --git a/tests/eval/good/to_bystr.scilexp b/tests/eval/good/to_bystr.scilexp index c3fa0e511..f5b9e9136 100644 --- a/tests/eval/good/to_bystr.scilexp +++ b/tests/eval/good/to_bystr.scilexp @@ -1,2 +1,19 @@ let x = 0xfb19 in -builtin to_bystr x +let y = builtin to_bystr x in +let xx_opt = builtin to_bystr2 y in +let res1 = + match xx_opt with + | Some xx => builtin eq x xx + | None => False + end +in + +let xx_opt = builtin to_bystr3 y in +let res2 = + match xx_opt with + | Some xx => False + | None => True + end +in + +andb res1 res2 diff --git a/tests/typecheck/good/Good.ml b/tests/typecheck/good/Good.ml index 27a236a2f..b323a42e4 100644 --- a/tests/typecheck/good/Good.ml +++ b/tests/typecheck/good/Good.ml @@ -208,6 +208,7 @@ module Tests = Scilla_test.Util.DiffBasedTests (struct "zip.scilexp"; "str-nonprint-char-1.scilexp"; "map_value_type_pair.scilexp"; + "to_bystr.scilexp"; ] let exit_code : UnixLabels.process_status = WEXITED 0 diff --git a/tests/typecheck/good/gold/to_bystr.scilexp.gold b/tests/typecheck/good/gold/to_bystr.scilexp.gold new file mode 100644 index 000000000..c95c7a8b9 --- /dev/null +++ b/tests/typecheck/good/gold/to_bystr.scilexp.gold @@ -0,0 +1,257 @@ +{ + "type_info": [ + { + "vname": "x", + "type": "ByStr2", + "start_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 1, + "column": 5 + }, + "end_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 1, + "column": 6 + } + }, + { + "vname": "y", + "type": "ByStr", + "start_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 2, + "column": 5 + }, + "end_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 2, + "column": 6 + } + }, + { + "vname": "x", + "type": "ByStr2", + "start_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 2, + "column": 26 + }, + "end_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 2, + "column": 27 + } + }, + { + "vname": "xx_opt", + "type": "Option (ByStr2)", + "start_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 3, + "column": 5 + }, + "end_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 3, + "column": 11 + } + }, + { + "vname": "y", + "type": "ByStr", + "start_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 3, + "column": 32 + }, + "end_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 3, + "column": 33 + } + }, + { + "vname": "res1", + "type": "Bool", + "start_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 4, + "column": 5 + }, + "end_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 4, + "column": 9 + } + }, + { + "vname": "xx_opt", + "type": "Option (ByStr2)", + "start_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 5, + "column": 9 + }, + "end_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 5, + "column": 15 + } + }, + { + "vname": "xx", + "type": "ByStr2", + "start_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 6, + "column": 10 + }, + "end_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 6, + "column": 12 + } + }, + { + "vname": "x", + "type": "ByStr2", + "start_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 6, + "column": 27 + }, + "end_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 6, + "column": 28 + } + }, + { + "vname": "xx", + "type": "ByStr2", + "start_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 6, + "column": 29 + }, + "end_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 6, + "column": 31 + } + }, + { + "vname": "xx_opt", + "type": "Option (ByStr3)", + "start_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 11, + "column": 5 + }, + "end_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 11, + "column": 11 + } + }, + { + "vname": "y", + "type": "ByStr", + "start_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 11, + "column": 32 + }, + "end_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 11, + "column": 33 + } + }, + { + "vname": "res2", + "type": "Bool", + "start_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 12, + "column": 5 + }, + "end_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 12, + "column": 9 + } + }, + { + "vname": "xx_opt", + "type": "Option (ByStr3)", + "start_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 13, + "column": 9 + }, + "end_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 13, + "column": 15 + } + }, + { + "vname": "xx", + "type": "ByStr3", + "start_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 14, + "column": 10 + }, + "end_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 14, + "column": 12 + } + }, + { + "vname": "andb", + "type": "Bool -> Bool -> Bool", + "start_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 19, + "column": 1 + }, + "end_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 19, + "column": 5 + } + }, + { + "vname": "res1", + "type": "Bool", + "start_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 19, + "column": 6 + }, + "end_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 19, + "column": 10 + } + }, + { + "vname": "res2", + "type": "Bool", + "start_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 19, + "column": 11 + }, + "end_location": { + "file": "typecheck/good/to_bystr.scilexp", + "line": 19, + "column": 15 + } + } + ], + "type": "Bool" +} diff --git a/tests/typecheck/good/to_bystr.scilexp b/tests/typecheck/good/to_bystr.scilexp new file mode 100644 index 000000000..f5b9e9136 --- /dev/null +++ b/tests/typecheck/good/to_bystr.scilexp @@ -0,0 +1,19 @@ +let x = 0xfb19 in +let y = builtin to_bystr x in +let xx_opt = builtin to_bystr2 y in +let res1 = + match xx_opt with + | Some xx => builtin eq x xx + | None => False + end +in + +let xx_opt = builtin to_bystr3 y in +let res2 = + match xx_opt with + | Some xx => False + | None => True + end +in + +andb res1 res2 From d050ef0a04c7a84434d58f4181bf6772faa91d8b Mon Sep 17 00:00:00 2001 From: Vaivaswatha Nagaraj Date: Fri, 13 Nov 2020 13:50:03 +0530 Subject: [PATCH 3/8] make fmt --- src/base/Syntax.ml | 28 ++++++++++++---------------- 1 file changed, 12 insertions(+), 16 deletions(-) diff --git a/src/base/Syntax.ml b/src/base/Syntax.ml index 81f024e3f..80ce354e4 100644 --- a/src/base/Syntax.ml +++ b/src/base/Syntax.ml @@ -136,7 +136,6 @@ let pp_builtin b = | Builtin_to_nat -> "to_nat" let parse_builtin s loc = - match s with | "eq" -> Builtin_eq | "concat" -> Builtin_concat @@ -181,21 +180,18 @@ let parse_builtin s loc = | "to_uint64" -> Builtin_to_uint64 | "to_uint128" -> Builtin_to_uint128 | "to_nat" -> Builtin_to_nat - | _ -> - let err = (SyntaxError (sprintf "\"%s\" is not a builtin" s, loc)) in - (* Check for "bystrx". Not using Str (regex) to keep it fast. *) - try - let n = (String.length "to_bystr") in - if String.equal (String.sub s ~pos:0 ~len:n) "to_bystr" - then - let i = int_of_string (String.sub s ~pos:n ~len:((String.length s) - n)) in - Builtin_to_bystrx i - else - raise err - with - | Invalid_argument _ - | Failure _ -> - raise err + | _ -> ( + let err = SyntaxError (sprintf "\"%s\" is not a builtin" s, loc) in + (* Check for "bystrx". Not using Str (regex) to keep it fast. *) + try + let n = String.length "to_bystr" in + if String.equal (String.sub s ~pos:0 ~len:n) "to_bystr" then + let i = + int_of_string (String.sub s ~pos:n ~len:(String.length s - n)) + in + Builtin_to_bystrx i + else raise err + with Invalid_argument _ | Failure _ -> raise err ) (*******************************************************) (* Types of components *) From c6554af068961f9e5820a606a841977c6a14754c Mon Sep 17 00:00:00 2001 From: Vaivaswatha N Date: Fri, 13 Nov 2020 15:24:42 +0530 Subject: [PATCH 4/8] Update src/base/Syntax.ml Co-authored-by: Anton Trunov --- src/base/Syntax.ml | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/src/base/Syntax.ml b/src/base/Syntax.ml index 80ce354e4..7760e6785 100644 --- a/src/base/Syntax.ml +++ b/src/base/Syntax.ml @@ -184,13 +184,10 @@ let parse_builtin s loc = let err = SyntaxError (sprintf "\"%s\" is not a builtin" s, loc) in (* Check for "bystrx". Not using Str (regex) to keep it fast. *) try - let n = String.length "to_bystr" in - if String.equal (String.sub s ~pos:0 ~len:n) "to_bystr" then - let i = - int_of_string (String.sub s ~pos:n ~len:(String.length s - n)) - in - Builtin_to_bystrx i - else raise err + let osize = String.chop_prefix s ~prefix:"to_bystr" in + match osize with + | Some size -> Builtin_to_bystrx (Int.of_string size) + | None -> raise err with Invalid_argument _ | Failure _ -> raise err ) (*******************************************************) From b18e7adaeefb831619bb8632639c462fe8d24ddf Mon Sep 17 00:00:00 2001 From: Vaivaswatha Nagaraj Date: Fri, 13 Nov 2020 15:35:23 +0530 Subject: [PATCH 5/8] remove unneeded comment --- src/base/Syntax.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/base/Syntax.ml b/src/base/Syntax.ml index 7760e6785..5954171fc 100644 --- a/src/base/Syntax.ml +++ b/src/base/Syntax.ml @@ -182,7 +182,6 @@ let parse_builtin s loc = | "to_nat" -> Builtin_to_nat | _ -> ( let err = SyntaxError (sprintf "\"%s\" is not a builtin" s, loc) in - (* Check for "bystrx". Not using Str (regex) to keep it fast. *) try let osize = String.chop_prefix s ~prefix:"to_bystr" in match osize with From 082d16c39c11994179846459383e2a389997bc08 Mon Sep 17 00:00:00 2001 From: Vaivaswatha N Date: Fri, 13 Nov 2020 15:45:18 +0530 Subject: [PATCH 6/8] Update src/base/Syntax.ml Co-authored-by: Anton Trunov --- src/base/Syntax.ml | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/base/Syntax.ml b/src/base/Syntax.ml index 5954171fc..47832fc66 100644 --- a/src/base/Syntax.ml +++ b/src/base/Syntax.ml @@ -181,13 +181,11 @@ let parse_builtin s loc = | "to_uint128" -> Builtin_to_uint128 | "to_nat" -> Builtin_to_nat | _ -> ( - let err = SyntaxError (sprintf "\"%s\" is not a builtin" s, loc) in try - let osize = String.chop_prefix s ~prefix:"to_bystr" in - match osize with - | Some size -> Builtin_to_bystrx (Int.of_string size) - | None -> raise err - with Invalid_argument _ | Failure _ -> raise err ) + let size = String.chop_prefix_exn s ~prefix:"to_bystr" in + Builtin_to_bystrx (Int.of_string size) + with Invalid_argument _ | Failure _ -> + raise @@ SyntaxError (sprintf "\"%s\" is not a builtin" s, loc) ) (*******************************************************) (* Types of components *) From 58e4c04c54b1859f3f32e3dcb6408b840c0b7861 Mon Sep 17 00:00:00 2001 From: Vaivaswatha Nagaraj Date: Fri, 13 Nov 2020 16:04:02 +0530 Subject: [PATCH 7/8] Add expected fail tests --- tests/typecheck/bad/Bad.ml | 2 ++ tests/typecheck/bad/gold/to_byst.scilexp.gold | 14 ++++++++++++++ tests/typecheck/bad/gold/to_bystrx.scilexp.gold | 14 ++++++++++++++ tests/typecheck/bad/to_byst.scilexp | 3 +++ tests/typecheck/bad/to_bystrx.scilexp | 4 ++++ 5 files changed, 37 insertions(+) create mode 100644 tests/typecheck/bad/gold/to_byst.scilexp.gold create mode 100644 tests/typecheck/bad/gold/to_bystrx.scilexp.gold create mode 100644 tests/typecheck/bad/to_byst.scilexp create mode 100644 tests/typecheck/bad/to_bystrx.scilexp diff --git a/tests/typecheck/bad/Bad.ml b/tests/typecheck/bad/Bad.ml index e205225f0..460c20732 100644 --- a/tests/typecheck/bad/Bad.ml +++ b/tests/typecheck/bad/Bad.ml @@ -188,6 +188,8 @@ module Tests = Scilla_test.Util.DiffBasedTests (struct "str-bad-char-3.scilexp"; "type-renaming-really-bad.scilexp"; "type-renaming-should-be-allowed.scilexp"; + "to_byst.scilexp"; + "to_bystrx.scilexp"; ] let exit_code : UnixLabels.process_status = WEXITED 1 diff --git a/tests/typecheck/bad/gold/to_byst.scilexp.gold b/tests/typecheck/bad/gold/to_byst.scilexp.gold new file mode 100644 index 000000000..d9614bbb5 --- /dev/null +++ b/tests/typecheck/bad/gold/to_byst.scilexp.gold @@ -0,0 +1,14 @@ +{ + "errors": [ + { + "error_message": "Syntax error: \"to_byst\" is not a builtin", + "start_location": { + "file": "typecheck/bad/to_byst.scilexp", + "line": 3, + "column": 9 + }, + "end_location": { "file": "", "line": 0, "column": 0 } + } + ], + "warnings": [] +} \ No newline at end of file diff --git a/tests/typecheck/bad/gold/to_bystrx.scilexp.gold b/tests/typecheck/bad/gold/to_bystrx.scilexp.gold new file mode 100644 index 000000000..31a983b9f --- /dev/null +++ b/tests/typecheck/bad/gold/to_bystrx.scilexp.gold @@ -0,0 +1,14 @@ +{ + "errors": [ + { + "error_message": "Syntax error: \"to_bystrX\" is not a builtin", + "start_location": { + "file": "typecheck/bad/to_bystrx.scilexp", + "line": 3, + "column": 9 + }, + "end_location": { "file": "", "line": 0, "column": 0 } + } + ], + "warnings": [] +} \ No newline at end of file diff --git a/tests/typecheck/bad/to_byst.scilexp b/tests/typecheck/bad/to_byst.scilexp new file mode 100644 index 000000000..9b08aa470 --- /dev/null +++ b/tests/typecheck/bad/to_byst.scilexp @@ -0,0 +1,3 @@ +let x = 0xfb19 in +let y = builtin to_bystr x in +builtin to_byst y diff --git a/tests/typecheck/bad/to_bystrx.scilexp b/tests/typecheck/bad/to_bystrx.scilexp new file mode 100644 index 000000000..88c9bd7e5 --- /dev/null +++ b/tests/typecheck/bad/to_bystrx.scilexp @@ -0,0 +1,4 @@ +let x = 0xfb19 in +let y = builtin to_bystr x in +builtin to_bystrX y + From a9f39e04b7b8b6f5e16d3c1f0b78e608ebad3039 Mon Sep 17 00:00:00 2001 From: Vaivaswatha Nagaraj Date: Fri, 13 Nov 2020 16:19:40 +0530 Subject: [PATCH 8/8] One more failing test --- tests/typecheck/bad/Bad.ml | 1 + tests/typecheck/bad/gold/to_bystr.scilexp.gold | 14 ++++++++++++++ tests/typecheck/bad/to_bystr.scilexp | 3 +++ 3 files changed, 18 insertions(+) create mode 100644 tests/typecheck/bad/gold/to_bystr.scilexp.gold create mode 100644 tests/typecheck/bad/to_bystr.scilexp diff --git a/tests/typecheck/bad/Bad.ml b/tests/typecheck/bad/Bad.ml index 460c20732..96aaf0f83 100644 --- a/tests/typecheck/bad/Bad.ml +++ b/tests/typecheck/bad/Bad.ml @@ -190,6 +190,7 @@ module Tests = Scilla_test.Util.DiffBasedTests (struct "type-renaming-should-be-allowed.scilexp"; "to_byst.scilexp"; "to_bystrx.scilexp"; + "to_bystr.scilexp"; ] let exit_code : UnixLabels.process_status = WEXITED 1 diff --git a/tests/typecheck/bad/gold/to_bystr.scilexp.gold b/tests/typecheck/bad/gold/to_bystr.scilexp.gold new file mode 100644 index 000000000..aa676e2fb --- /dev/null +++ b/tests/typecheck/bad/gold/to_bystr.scilexp.gold @@ -0,0 +1,14 @@ +{ + "errors": [ + { + "error_message": "The usage of the builtin function is incorrect.\n", + "start_location": { + "file": "typecheck/bad/to_bystr.scilexp", + "line": 3, + "column": 20 + }, + "end_location": { "file": "", "line": 0, "column": 0 } + } + ], + "warnings": [] +} \ No newline at end of file diff --git a/tests/typecheck/bad/to_bystr.scilexp b/tests/typecheck/bad/to_bystr.scilexp new file mode 100644 index 000000000..bd76e8798 --- /dev/null +++ b/tests/typecheck/bad/to_bystr.scilexp @@ -0,0 +1,3 @@ +let x = 0xfb19 in +let y = builtin to_bystr x in +builtin to_bystr 20 y