From 6612c29758e6155d1eb54791876698bcda27925f Mon Sep 17 00:00:00 2001 From: Ulf Norell Date: Mon, 24 Jun 2019 11:44:07 +0200 Subject: [PATCH] Type check Bytes.to_X builtins --- src/aeso_ast_infer_types.erl | 78 ++++++++++++++++++++++++++++------- src/aeso_pretty.erl | 1 + src/aeso_syntax.erl | 2 +- test/aeso_compiler_tests.erl | 3 +- test/contracts/bytes_to_x.aes | 8 ++++ 5 files changed, 75 insertions(+), 17 deletions(-) create mode 100644 test/contracts/bytes_to_x.aes diff --git a/src/aeso_ast_infer_types.erl b/src/aeso_ast_infer_types.erl index cd8d829..d792ec9 100644 --- a/src/aeso_ast_infer_types.erl +++ b/src/aeso_ast_infer_types.erl @@ -486,6 +486,12 @@ global_env() -> {"none", Bits}, {"all", Bits}]) }, + %% Bytes + BytesScope = #scope + { funs = MkDefs( + [{"to_int", Fun1(Bytes(any), Int)}, + {"to_str", Fun1(Bytes(any), String)}]) }, + %% Conversion IntScope = #scope{ funs = MkDefs([{"to_str", Fun1(Int, String)}]) }, AddressScope = #scope{ funs = MkDefs([{"to_str", Fun1(Address, String)}, @@ -504,6 +510,7 @@ global_env() -> , ["Crypto"] => CryptoScope , ["String"] => StringScope , ["Bits"] => BitsScope + , ["Bytes"] => BytesScope , ["Int"] => IntScope , ["Address"] => AddressScope } }. @@ -916,8 +923,8 @@ lookup_name(Env, As, Id, Options) -> Freshen = proplists:get_value(freshen, Options, false), check_stateful(Env, Id, Ty), Ty1 = case Ty of - {type_sig, _, _, _, _} -> freshen_type(typesig_to_fun_t(Ty)); - _ when Freshen -> freshen_type(Ty); + {type_sig, _, _, _, _} -> freshen_type(As, typesig_to_fun_t(Ty)); + _ when Freshen -> freshen_type(As, Ty); _ -> Ty end, {set_qname(QId, Id), Ty1} @@ -1218,7 +1225,7 @@ infer_block(Env, _, [E], BlockType) -> [check_expr(Env, E, BlockType)]; infer_block(Env, Attrs, [Def={letfun, Ann, _, _, _, _}|Rest], BlockType) -> {{Name, TypeSig}, LetFun} = infer_letfun(Env, Def), - FunT = freshen_type(typesig_to_fun_t(TypeSig)), + FunT = freshen_type(Ann, typesig_to_fun_t(TypeSig)), NewE = bind_var({id, Ann, Name}, FunT, Env), [LetFun|infer_block(NewE, Attrs, Rest, BlockType)]; infer_block(Env, _, [{letval, Attrs, Pattern, Type, E}|Rest], BlockType) -> @@ -1358,14 +1365,17 @@ when_option(Opt, Do) -> create_constraints() -> create_named_argument_constraints(), + create_bytes_constraints(), create_field_constraints(). solve_constraints(Env) -> solve_named_argument_constraints(Env), + solve_bytes_constraints(Env), solve_field_constraints(Env). destroy_and_report_unsolved_constraints(Env) -> destroy_and_report_unsolved_field_constraints(Env), + destroy_and_report_unsolved_bytes_constraints(Env), destroy_and_report_unsolved_named_argument_constraints(Env). %% -- Named argument constraints -- @@ -1414,6 +1424,37 @@ destroy_and_report_unsolved_named_argument_constraints(Env) -> destroy_named_argument_constraints(), ok. +%% -- Bytes constraints -- + +-type byte_constraint() :: {is_bytes, utype()}. + +create_bytes_constraints() -> + ets_new(bytes_constraints, [bag]). + +get_bytes_constraints() -> + ets_tab2list(bytes_constraints). + +-spec add_bytes_constraint(byte_constraint()) -> ok. +add_bytes_constraint(Constraint) -> + ets_insert(bytes_constraints, Constraint). + +solve_bytes_constraints(_Env) -> + ok. + +destroy_bytes_constraints() -> + ets_delete(bytes_constraints). + +destroy_and_report_unsolved_bytes_constraints(Env) -> + [ check_bytes_constraint(Env, C) || C <- get_bytes_constraints() ], + destroy_bytes_constraints(). + +check_bytes_constraint(Env, {is_bytes, Type}) -> + Type1 = unfold_types_in_type(Env, instantiate(Type)), + case Type1 of + {bytes_t, _, _} -> ok; + _ -> type_error({cannot_unify, Type1, {bytes_t, [], any}, {at, Type}}) + end. + %% -- Field constraints -- create_field_constraints() -> @@ -1840,26 +1881,31 @@ create_freshen_tvars() -> destroy_freshen_tvars() -> ets_delete(freshen_tvars). -freshen_type(Type) -> +freshen_type(Ann, Type) -> create_freshen_tvars(), - Type1 = freshen(Type), + Type1 = freshen(Ann, Type), destroy_freshen_tvars(), Type1. -freshen({tvar, As, Name}) -> +freshen(Type) -> + freshen(aeso_syntax:get_ann(Type), Type). + +freshen(Ann, {tvar, _, Name}) -> NewT = case ets_lookup(freshen_tvars, Name) of - [] -> - fresh_uvar(As); - [{Name, T}] -> - T + [] -> fresh_uvar(Ann); + [{Name, T}] -> T end, ets_insert(freshen_tvars, {Name, NewT}), NewT; -freshen(T) when is_tuple(T) -> - list_to_tuple(freshen(tuple_to_list(T))); -freshen([A|B]) -> - [freshen(A)|freshen(B)]; -freshen(X) -> +freshen(Ann, {bytes_t, _, any}) -> + X = fresh_uvar(Ann), + add_bytes_constraint({is_bytes, X}), + X; +freshen(Ann, T) when is_tuple(T) -> + list_to_tuple(freshen(Ann, tuple_to_list(T))); +freshen(Ann, [A | B]) -> + [freshen(Ann, A) | freshen(Ann, B)]; +freshen(_, X) -> X. %% Dereferences all uvars and replaces the uninstantiated ones with a @@ -2044,6 +2090,7 @@ pp_error(Err) -> io_lib:format("Unknown error: ~p\n", [Err]). pp_when({todo, What}) -> io_lib:format("[TODO] ~p\n", [What]); +pp_when({at, Ann}) -> io_lib:format("at ~s\n", [pp_loc(Ann)]); pp_when({check_typesig, Name, Inferred, Given}) -> io_lib:format("when checking the definition of ~s\n" " inferred type: ~s\n" @@ -2196,6 +2243,7 @@ pp({tvar, _, Name}) -> Name; pp({tuple_t, _, Cpts}) -> ["(", pp(Cpts), ")"]; +pp({bytes_t, _, any}) -> "bytes(_)"; pp({bytes_t, _, Len}) -> ["bytes(", integer_to_list(Len), ")"]; pp({app_t, _, T, []}) -> diff --git a/src/aeso_pretty.erl b/src/aeso_pretty.erl index fdcd06d..8762cf7 100644 --- a/src/aeso_pretty.erl +++ b/src/aeso_pretty.erl @@ -233,6 +233,7 @@ type({app_t, _, Type, Args}) -> beside(type(Type), tuple_type(Args)); type({tuple_t, _, Args}) -> tuple_type(Args); +type({bytes_t, _, any}) -> text("bytes(_)"); type({bytes_t, _, Len}) -> text(lists:concat(["bytes(", Len, ")"])); type({named_arg_t, _, Name, Type, _Default}) -> diff --git a/src/aeso_syntax.erl b/src/aeso_syntax.erl index 7f45aa8..5c9e81c 100644 --- a/src/aeso_syntax.erl +++ b/src/aeso_syntax.erl @@ -59,7 +59,7 @@ -type type() :: {fun_t, ann(), [named_arg_t()], [type()], type()} | {app_t, ann(), type(), [type()]} | {tuple_t, ann(), [type()]} - | {bytes_t, ann(), integer()} + | {bytes_t, ann(), integer() | any} | id() | qid() | con() | qcon() %% contracts | tvar(). diff --git a/test/aeso_compiler_tests.erl b/test/aeso_compiler_tests.erl index 8d95522..f2095df 100644 --- a/test/aeso_compiler_tests.erl +++ b/test/aeso_compiler_tests.erl @@ -115,7 +115,8 @@ compilable_contracts() -> "address_literals", "bytes_equality", "address_chain", - "namespace_bug" + "namespace_bug", + "bytes_to_x" ]. not_yet_compilable(fate) -> diff --git a/test/contracts/bytes_to_x.aes b/test/contracts/bytes_to_x.aes new file mode 100644 index 0000000..f6bfea2 --- /dev/null +++ b/test/contracts/bytes_to_x.aes @@ -0,0 +1,8 @@ + +contract BytesToX = + + function to_int(b : bytes(42)) : int = Bytes.to_int(b) + function to_str(b : bytes(12)) : string = + String.concat(Bytes.to_str(b), Bytes.to_str(#ffff)) + function to_str_big(b : bytes(65)) : string = + Bytes.to_str(b)