From 1ce95b32aca3febd857d002d881a51155f766e52 Mon Sep 17 00:00:00 2001 From: Ulf Norell Date: Fri, 30 Aug 2019 10:21:36 +0200 Subject: [PATCH 1/4] Add checks for polymorphic/higher order oracles and higher order entrypoints (FATE) --- src/aeso_ast_to_fcode.erl | 49 +++++++++++++++++++++++++++++++++++++-- 1 file changed, 47 insertions(+), 2 deletions(-) diff --git a/src/aeso_ast_to_fcode.erl b/src/aeso_ast_to_fcode.erl index 16fe99e..3f0c960 100644 --- a/src/aeso_ast_to_fcode.erl +++ b/src/aeso_ast_to_fcode.erl @@ -282,10 +282,13 @@ decl_to_fcode(Env = #{ functions := Funs }, {letfun, Ann, {id, _, Name}, Args, R Attrs = get_attributes(Ann), FName = lookup_fun(Env, qname(Env, Name)), FArgs = args_to_fcode(Env, Args), + FRet = type_to_fcode(Env, Ret), FBody = expr_to_fcode(Env#{ vars => [X || {X, _} <- FArgs] }, Body), + [ ensure_first_order_entrypoint(Ann, FArgs, FRet) + || aeso_syntax:get_ann(entrypoint, Ann, false) ], Def = #{ attrs => Attrs, args => FArgs, - return => type_to_fcode(Env, Ret), + return => FRet, body => FBody }, NewFuns = Funs#{ FName => Def }, Env#{ functions := NewFuns }. @@ -510,7 +513,7 @@ expr_to_fcode(Env, _Type, {app, _Ann, {Op, _}, [A]}) when is_atom(Op) -> end; %% Function calls -expr_to_fcode(Env, Type, {app, _Ann, Fun = {typed, _, _, {fun_t, _, NamedArgsT, _, _}}, Args}) -> +expr_to_fcode(Env, Type, {app, _, Fun = {typed, _, _, {fun_t, _, NamedArgsT, _, _}}, Args}) -> Args1 = get_named_args(NamedArgsT, Args), FArgs = [expr_to_fcode(Env, Arg) || Arg <- Args1], case expr_to_fcode(Env, Fun) of @@ -524,11 +527,13 @@ expr_to_fcode(Env, Type, {app, _Ann, Fun = {typed, _, _, {fun_t, _, NamedArgsT, %% Get the type of the oracle from the args or the expression itself OType = get_oracle_type(B, Type, Args1), {oracle, QType, RType} = type_to_fcode(Env, OType), + validate_oracle_type(aeso_syntax:get_ann(Fun), QType, RType), TypeArgs = [{lit, {typerep, QType}}, {lit, {typerep, RType}}], builtin_to_fcode(B, FArgs ++ TypeArgs); {builtin_u, B, _} when B =:= aens_resolve -> %% Get the type we are assuming the name resolves to AensType = type_to_fcode(Env, Type), + validate_aens_resolve_type(aeso_syntax:get_ann(Fun), AensType), TypeArgs = [{lit, {typerep, AensType}}], builtin_to_fcode(B, FArgs ++ TypeArgs); {builtin_u, B, _Ar} -> builtin_to_fcode(B, FArgs); @@ -604,6 +609,46 @@ get_oracle_type(oracle_check, _Type, [{typed, _, _Expr, OType}]) -> get_oracle_type(oracle_check_query, _Type, [{typed, _, _Expr, OType} | _]) -> OType; get_oracle_type(oracle_respond, _Type, [_, {typed, _,_Expr, OType} | _]) -> OType. +validate_oracle_type(Ann, QType, RType) -> + ensure_monomorphic(QType, {polymorphic_query_type, Ann, QType}), + ensure_monomorphic(RType, {polymorphic_response_type, Ann, RType}), + ensure_first_order(QType, {higher_order_query_type, Ann, QType}), + ensure_first_order(RType, {higher_order_response_type, Ann, RType}), + ok. + +validate_aens_resolve_type(Ann, {variant, [[], [Type]]}) -> + ensure_monomorphic(Type, {polymorphic_aens_resolve, Ann, Type}), + ensure_first_order(Type, {higher_order_aens_resolve, Ann, Type}), + ok. + +ensure_first_order_entrypoint(Ann, Args, Ret) -> + [ ensure_first_order(T, {higher_order_entrypoint_argument, Ann, X, T}) + || {X, T} <- Args ], + ensure_first_order(Ret, {higher_order_entrypoint_return, Ann, Ret}), + ok. + +ensure_monomorphic(Type, Err) -> + case is_monomorphic(Type) of + true -> ok; + false -> fcode_error(Err) + end. + +ensure_first_order(Type, Err) -> + case is_first_order(Type) of + true -> ok; + false -> fcode_error(Err) + end. + +is_monomorphic({tvar, _}) -> false; +is_monomorphic(Ts) when is_list(Ts) -> lists:all(fun is_monomorphic/1, Ts); +is_monomorphic(Tup) when is_tuple(Tup) -> is_monomorphic(tuple_to_list(Tup)); +is_monomorphic(_) -> true. + +is_first_order({function, _, _}) -> false; +is_first_order(Ts) when is_list(Ts) -> lists:all(fun is_first_order/1, Ts); +is_first_order(Tup) when is_tuple(Tup) -> is_first_order(tuple_to_list(Tup)); +is_first_order(_) -> true. + %% -- Pattern matching -- -spec alts_to_fcode(env(), ftype(), var_name(), [aeso_syntax:alt()]) -> fsplit(). From 6fd39d4cb19651ddee556307f62631782a9e5d53 Mon Sep 17 00:00:00 2001 From: Ulf Norell Date: Fri, 30 Aug 2019 11:13:13 +0200 Subject: [PATCH 2/4] Add checks for polymorphic/higher order oracles and higher order entrypoints (AEVM) --- src/aeso_ast_to_icode.erl | 72 ++++++++++++++++++++------------ test/contracts/complex_types.aes | 2 +- test/contracts/test.aes | 5 ++- test/contracts/tuple_match.aes | 2 +- 4 files changed, 50 insertions(+), 31 deletions(-) diff --git a/src/aeso_ast_to_icode.erl b/src/aeso_ast_to_icode.erl index ca1433a..c245e29 100644 --- a/src/aeso_ast_to_icode.erl +++ b/src/aeso_ast_to_icode.erl @@ -93,6 +93,8 @@ contract_to_icode([{letfun, Attrib, Name, Args, _What, Body={typed,_,_,T}}|Rest] FunAttrs = [ stateful || proplists:get_value(stateful, Attrib, false) ] ++ [ payable || proplists:get_value(payable, Attrib, false) ] ++ [ private || is_private(Attrib, Icode) ], + [ check_entrypoint_type(Attrib, Name, Args, T) + || aeso_syntax:get_ann(entrypoint, Attrib, false) ], %% TODO: Handle types FunName = ast_id(Name), %% TODO: push funname to env @@ -105,7 +107,7 @@ contract_to_icode([{letfun, Attrib, Name, Args, _What, Body={typed,_,_,T}}|Rest] #{ state_type := StateType } = Icode, {#tuple{ cpts = [type_value(StateType), ast_body(Body, Icode)] }, {tuple, [typerep, ast_typerep(T, Icode)]}}; - _ -> {ast_body(Body, Icode), ast_typerep(T, Icode)} + _ -> {ast_body(Body, Icode), ast_typerep1(T, Icode)} end, QName = aeso_icode:qualify(Name, Icode), NewIcode = ast_fun_to_icode(ast_id(QName), FunAttrs, FunArgs, FunBody, TypeRep, Icode), @@ -121,7 +123,7 @@ ast_id({id, _, Id}) -> Id; ast_id({qid, _, Id}) -> Id. ast_args([{arg, _, Name, Type}|Rest], Acc, Icode) -> - ast_args(Rest, [{ast_id(Name), ast_type(Type, Icode)}| Acc], Icode); + ast_args(Rest, [{ast_id(Name), ast_typerep1(Type, Icode)}| Acc], Icode); ast_args([], Acc, _Icode) -> lists:reverse(Acc). ast_type(T, Icode) -> @@ -582,7 +584,7 @@ ast_body({block,As,[E|Rest]}, Icode) -> #switch{expr=ast_body(E, Icode), cases=[{#var_ref{name="_"},ast_body({block,As,Rest}, Icode)}]}; ast_body({lam,_,Args,Body}, Icode) -> - #lambda{args=[#arg{name = ast_id(P), type = ast_type(T, Icode)} || {arg,_,P,T} <- Args], + #lambda{args=[#arg{name = ast_id(P), type = ast_typerep1(T, Icode)} || {arg,_,P,T} <- Args], body=ast_body(Body, Icode)}; ast_body({typed,_,{record,Attrs,Fields},{record_t,DefFields}}, Icode) -> %% Compile as a tuple with the fields in the order they appear in the definition. @@ -717,6 +719,22 @@ map_upd(Key, Default, ValFun, Map = {typed, Ann, _, MapType}, Icode) -> Args = [ast_body(Map, Icode), ast_body(Key, Icode), ast_body(Default, Icode), ast_body(ValFun, Icode)], builtin_call(FunName, Args). +check_entrypoint_type(Ann, Name, Args, Ret) -> + Check = fun(T, Err) -> + case is_simple_type(T) of + false -> gen_error(Err); + true -> ok + end end, + [ Check(T, {entrypoint_argument_must_have_simple_type, Ann1, Name, X, T}) + || {arg, Ann1, X, T} <- Args ], + Check(Ret, {entrypoint_must_have_simple_return_type, Ann, Name, Ret}). + +is_simple_type({tvar, _, _}) -> false; +is_simple_type({fun_t, _, _, _, _}) -> false; +is_simple_type(Ts) when is_list(Ts) -> lists:all(fun is_simple_type/1, Ts); +is_simple_type(T) when is_tuple(T) -> is_simple_type(tuple_to_list(T)); +is_simple_type(_) -> true. + is_monomorphic({tvar, _, _}) -> false; is_monomorphic([H|T]) -> is_monomorphic(H) andalso is_monomorphic(T); @@ -757,42 +775,49 @@ make_type_def(Args, Def, Icode = #{ type_vars := TypeEnv }) -> TVars = [ X || {tvar, _, X} <- Args ], fun(Types) -> TypeEnv1 = maps:from_list(lists:zip(TVars, Types)), - ast_typerep(Def, Icode#{ type_vars := maps:merge(TypeEnv, TypeEnv1) }) + ast_typerep1(Def, Icode#{ type_vars := maps:merge(TypeEnv, TypeEnv1) }) end. -spec ast_typerep(aeso_syntax:type()) -> aeb_aevm_data:type(). -ast_typerep(Type) -> ast_typerep(Type, aeso_icode:new([])). +ast_typerep(Type) -> + ast_typerep(Type, aeso_icode:new([])). -ast_typerep({id, _, Name}, Icode) -> +ast_typerep(Type, Icode) -> + case is_simple_type(Type) of + false -> gen_error({not_a_simple_type, Type}); + true -> ast_typerep1(Type, Icode) + end. + +ast_typerep1({id, _, Name}, Icode) -> lookup_type_id(Name, [], Icode); -ast_typerep({qid, _, Name}, Icode) -> +ast_typerep1({qid, _, Name}, Icode) -> lookup_type_id(Name, [], Icode); -ast_typerep({con, _, _}, _) -> +ast_typerep1({con, _, _}, _) -> word; %% Contract type -ast_typerep({bytes_t, _, Len}, _) -> +ast_typerep1({bytes_t, _, Len}, _) -> bytes_t(Len); -ast_typerep({app_t, _, {I, _, Name}, Args}, Icode) when I =:= id; I =:= qid -> - ArgReps = [ ast_typerep(Arg, Icode) || Arg <- Args ], +ast_typerep1({app_t, _, {I, _, Name}, Args}, Icode) when I =:= id; I =:= qid -> + ArgReps = [ ast_typerep1(Arg, Icode) || Arg <- Args ], lookup_type_id(Name, ArgReps, Icode); -ast_typerep({tvar,_,A}, #{ type_vars := TypeVars }) -> +ast_typerep1({tvar,_,A}, #{ type_vars := TypeVars }) -> case maps:get(A, TypeVars, undefined) of undefined -> word; %% We serialize type variables just as addresses in the originating VM. Type -> Type end; -ast_typerep({tuple_t,_,Cpts}, Icode) -> - {tuple, [ast_typerep(C, Icode) || C<-Cpts]}; -ast_typerep({record_t,Fields}, Icode) -> +ast_typerep1({tuple_t,_,Cpts}, Icode) -> + {tuple, [ast_typerep1(C, Icode) || C<-Cpts]}; +ast_typerep1({record_t,Fields}, Icode) -> {tuple, [ begin {field_t, _, _, T} = Field, - ast_typerep(T, Icode) + ast_typerep1(T, Icode) end || Field <- Fields]}; -ast_typerep({fun_t,_,_,_,_}, _Icode) -> +ast_typerep1({fun_t,_,_,_,_}, _Icode) -> function; -ast_typerep({alias_t, T}, Icode) -> ast_typerep(T, Icode); -ast_typerep({variant_t, Cons}, Icode) -> +ast_typerep1({alias_t, T}, Icode) -> ast_typerep1(T, Icode); +ast_typerep1({variant_t, Cons}, Icode) -> {variant, [ begin {constr_t, _, _, Args} = Con, - [ ast_typerep(Arg, Icode) || Arg <- Args ] + [ ast_typerep1(Arg, Icode) || Arg <- Args ] end || Con <- Cons ]}. ttl_t(Icode) -> @@ -841,13 +866,6 @@ type_value({map, K, V}) -> #tuple{ cpts = [#integer{ value = ?TYPEREP_MAP_TAG }, type_value(K), type_value(V)] }. -%% As abort is a built-in in the future it will be illegal to for -%% users to define abort. For the time being strip away all user -%% defined abort functions. - -ast_fun_to_icode("abort", _Atts, _Args, _Body, _TypeRep, Icode) -> - %% Strip away all user defined abort functions. - Icode; ast_fun_to_icode(Name, Attrs, Args, Body, TypeRep, #{functions := Funs} = Icode) -> NewFuns = [{Name, Attrs, Args, Body, TypeRep}| Funs], aeso_icode:set_functions(NewFuns, Icode). diff --git a/test/contracts/complex_types.aes b/test/contracts/complex_types.aes index 613371f..57e19d7 100644 --- a/test/contracts/complex_types.aes +++ b/test/contracts/complex_types.aes @@ -50,7 +50,7 @@ contract ComplexTypes = entrypoint remote_pair(n : int, s : string) : int * string = state.worker.pair(gas = 10000, n, s) - entrypoint map(f, xs) = + function map(f, xs) = switch(xs) [] => [] x :: xs => f(x) :: map(f, xs) diff --git a/test/contracts/test.aes b/test/contracts/test.aes index 04de90f..bd1a130 100644 --- a/test/contracts/test.aes +++ b/test/contracts/test.aes @@ -91,10 +91,11 @@ contract Identity = // } // let id(x) = x // let main(xs) = map(double,xs) - entrypoint z(f,x) = x + function z(f,x) = x function s(n) = (f,x)=>f(n(f,x)) function add(m,n) = (f,x)=>m(f,n(f,x)) - entrypoint main(_) = + + entrypoint main() = let three=s(s(s(z))) add(three,three) (((i)=>i+1),0) diff --git a/test/contracts/tuple_match.aes b/test/contracts/tuple_match.aes index 0bcab8c..b6196e3 100644 --- a/test/contracts/tuple_match.aes +++ b/test/contracts/tuple_match.aes @@ -1,6 +1,6 @@ contract TuplesMatch = - entrypoint tuplify3() = (t) => switch(t) + function tuplify3() = (t) => switch(t) (x, y, z) => 3 entrypoint fst(p : int * string) = From f27ba528d873059cc740d2c5403af23c89ca0d6a Mon Sep 17 00:00:00 2001 From: Ulf Norell Date: Fri, 30 Aug 2019 11:21:26 +0200 Subject: [PATCH 3/4] aebytecode commit --- rebar.config | 2 +- rebar.lock | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/rebar.config b/rebar.config index 7d60a8e..043dc58 100644 --- a/rebar.config +++ b/rebar.config @@ -2,7 +2,7 @@ {erl_opts, [debug_info]}. -{deps, [ {aebytecode, {git, "https://github.com/aeternity/aebytecode.git", {ref,"10cc127"}}} +{deps, [ {aebytecode, {git, "https://github.com/aeternity/aebytecode.git", {ref,"e7f2be7"}}} , {getopt, "1.0.1"} , {eblake2, "1.0.0"} , {jsx, {git, "https://github.com/talentdeficit/jsx.git", diff --git a/rebar.lock b/rebar.lock index 84f3ab4..924dffc 100644 --- a/rebar.lock +++ b/rebar.lock @@ -1,7 +1,7 @@ {"1.1.0", [{<<"aebytecode">>, {git,"https://github.com/aeternity/aebytecode.git", - {ref,"10cc1278831ad7e90138533466ceef4bcafd74a9"}}, + {ref,"e7f2be7ce878b1e22bad287f3342f32579e98599"}}, 0}, {<<"aeserialization">>, {git,"https://github.com/aeternity/aeserialization.git", From 062309e578fc852bc4e37c26fc53e1dd19ae5407 Mon Sep 17 00:00:00 2001 From: Ulf Norell Date: Fri, 30 Aug 2019 14:22:31 +0200 Subject: [PATCH 4/4] Type variables mentioned in local functions should not be flexible (cc #112) --- src/aeso_ast_infer_types.erl | 2 +- test/contracts/local_poly_fail.aes | 7 +++++++ 2 files changed, 8 insertions(+), 1 deletion(-) create mode 100644 test/contracts/local_poly_fail.aes diff --git a/src/aeso_ast_infer_types.erl b/src/aeso_ast_infer_types.erl index 5a07a9f..5e58a45 100644 --- a/src/aeso_ast_infer_types.erl +++ b/src/aeso_ast_infer_types.erl @@ -1327,7 +1327,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(Ann, typesig_to_fun_t(TypeSig)), + FunT = 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) -> diff --git a/test/contracts/local_poly_fail.aes b/test/contracts/local_poly_fail.aes new file mode 100644 index 0000000..189ab23 --- /dev/null +++ b/test/contracts/local_poly_fail.aes @@ -0,0 +1,7 @@ + +contract Fail = + + entrypoint tttt() : bool * int = + let f(x : 'a) : 'a = x + (f(true), f(1)) +