QPQ-AG/sophia
11
0
Fork 0
Code Issues 43 Pull Requests 7 Actions Packages Projects Releases 16 Wiki Activity

Merge pull request #69 from aeternity/PT-162578475-stateful

Browse Source 
Check stateful annotations
This commit is contained in:
Ulf Norell
2019-05-15 15:44:37 +02:00
committed by GitHub
parent d4238c0bdc cf5a8aeb5f
commit 8eaafa736c
24 changed files with 246 additions and 176 deletions
Download Patch File Download Diff File Expand all files Collapse all files
src/aeso_ast_infer_types.erl
+83 -7
View File
@@ -104,6 +104,8 @@
, fields = #{} :: #{ name() => [field_info()] } %% fields are global
, namespace = [] :: qname()
, in_pattern = false :: boolean()
, stateful = false :: boolean()
, current_function = none :: none | aeso_syntax:id()
}).
-type env() :: #env{}.
@@ -197,7 +199,7 @@ bind_state(Env) ->
false -> {id, Ann, "event"} %% will cause type error if used(?)
end,
Env1 = bind_funs([{"state", State},
{"put", {fun_t, Ann, [], [State], Unit}}], Env),
{"put", {type_sig, [stateful | Ann], [], [State], Unit}}], Env),
%% We bind Chain.event in a local 'Chain' namespace.
pop_scope(
@@ -357,11 +359,12 @@ global_env() ->
Pair = fun(A, B) -> {tuple_t, Ann, [A, B]} end,
Fun = fun(Ts, T) -> {type_sig, Ann, [], Ts, T} end,
Fun1 = fun(S, T) -> Fun([S], T) end,
TVar = fun(X) -> {tvar, Ann, "'" ++ X} end,
StateFun = fun(Ts, T) -> {type_sig, [stateful|Ann], [], Ts, T} end,
TVar = fun(X) -> {tvar, Ann, "'" ++ X} end,
SignId = {id, Ann, "signature"},
SignDef = {bytes, Ann, <<0:64/unit:8>>},
Signature = {named_arg_t, Ann, SignId, SignId, {typed, Ann, SignDef, SignId}},
SignFun = fun(Ts, T) -> {type_sig, Ann, [Signature], Ts, T} end,
SignFun = fun(Ts, T) -> {type_sig, [stateful|Ann], [Signature], Ts, T} end,
TTL = {qid, Ann, ["Chain", "ttl"]},
Fee = Int,
[A, Q, R, K, V] = lists:map(TVar, ["a", "q", "r", "k", "v"]),
@@ -390,7 +393,7 @@ global_env() ->
ChainScope = #scope
{ funs = MkDefs(
%% Spend transaction.
[{"spend", Fun([Address, Int], Unit)},
[{"spend", StateFun([Address, Int], Unit)},
%% Chain environment
{"balance", Fun1(Address, Int)},
{"block_hash", Fun1(Int, Int)},
@@ -420,7 +423,7 @@ global_env() ->
{ funs = MkDefs(
[{"register", SignFun([Address, Fee, TTL], Oracle(Q, R))},
{"query_fee", Fun([Oracle(Q, R)], Fee)},
{"query", Fun([Oracle(Q, R), Q, Fee, TTL, TTL], Query(Q, R))},
{"query", StateFun([Oracle(Q, R), Q, Fee, TTL, TTL], Query(Q, R))},
{"get_question", Fun([Oracle(Q, R), Query(Q, R)], Q)},
{"respond", SignFun([Oracle(Q, R), Query(Q, R), R], Unit)},
{"extend", SignFun([Oracle(Q, R), TTL], Unit)},
@@ -602,6 +605,8 @@ infer_contract(Env, What, Defs) ->
SCCs = aeso_utils:scc(DepGraph),
%% io:format("Dependency sorted functions:\n ~p\n", [SCCs]),
{Env4, Defs1} = check_sccs(Env3, FunMap, SCCs, []),
%% Check that `init` doesn't read or write the state
check_state_dependencies(Env4, Defs1),
destroy_and_report_type_errors(Env4),
{Env4, TypeDefs ++ Decls ++ Defs1}.
@@ -862,7 +867,9 @@ infer_letrec(Env, Defs) ->
[print_typesig(S) || S <- TypeSigs],
{TypeSigs, NewDefs}.
infer_letfun(Env, {letfun, Attrib, Fun = {id, NameAttrib, Name}, Args, What, Body}) ->
infer_letfun(Env0, {letfun, Attrib, Fun = {id, NameAttrib, Name}, Args, What, Body}) ->
Env = Env0#env{ stateful = aeso_syntax:get_ann(stateful, Attrib, false),
current_function = Fun },
check_unique_arg_names(Fun, Args),
ArgTypes = [{ArgName, check_type(Env, arg_type(T))} || {arg, _, ArgName, T} <- Args],
ExpectedType = check_type(Env, arg_type(What)),
@@ -904,6 +911,7 @@ lookup_name(Env, As, Id, Options) ->
{Id, fresh_uvar(As)};
{QId, {_, Ty}} ->
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);
@@ -912,6 +920,61 @@ lookup_name(Env, As, Id, Options) ->
{set_qname(QId, Id), Ty1}
end.
check_stateful(#env{ stateful = false, current_function = Fun }, Id, Type = {type_sig, _, _, _, _}) ->
case aeso_syntax:get_ann(stateful, Type, false) of
false -> ok;
true ->
type_error({stateful_not_allowed, Id, Fun})
end;
check_stateful(_Env, _Id, _Type) -> ok.
%% Hack: don't allow passing the 'value' named arg if not stateful. This only
%% works since the user can't create functions with named arguments.
check_stateful_named_arg(#env{ stateful = false, current_function = Fun }, {id, _, "value"}, Default) ->
case Default of
{int, _, 0} -> ok;
_ -> type_error({value_arg_not_allowed, Default, Fun})
end;
check_stateful_named_arg(_, _, _) -> ok.
%% Check that `init` doesn't read or write the state
check_state_dependencies(Env, Defs) ->
Top = Env#env.namespace,
GetState = Top ++ ["state"],
SetState = Top ++ ["put"],
Init = Top ++ ["init"],
UsedNames = fun(X) -> [{Xs, Ann} || {{term, Xs}, Ann} <- aeso_syntax_utils:used(X)] end,
Funs = [ {Top ++ [Name], Fun} || Fun = {letfun, _, {id, _, Name}, _Args, _Type, _Body} <- Defs ],
Deps = maps:from_list([{Name, UsedNames(Def)} || {Name, Def} <- Funs]),
case maps:get(Init, Deps, false) of
false -> ok; %% No init, so nothing to check
_ ->
[ type_error({init_depends_on_state, state, Chain})
|| Chain <- get_call_chains(Deps, Init, GetState) ],
[ type_error({init_depends_on_state, put, Chain})
|| Chain <- get_call_chains(Deps, Init, SetState) ],
ok
end.
%% Compute all paths (not sharing intermediate nodes) from Start to Stop in Graph.
get_call_chains(Graph, Start, Stop) ->
get_call_chains(Graph, #{}, queue:from_list([{Start, [], []}]), Stop, []).
get_call_chains(Graph, Visited, Queue, Stop, Acc) ->
case queue:out(Queue) of
{empty, _} -> lists:reverse(Acc);
{{value, {Stop, Ann, Path}}, Queue1} ->
get_call_chains(Graph, Visited, Queue1, Stop, [lists:reverse([{Stop, Ann} | Path]) | Acc]);
{{value, {Node, Ann, Path}}, Queue1} ->
case maps:is_key(Node, Visited) of
true -> get_call_chains(Graph, Visited, Queue1, Stop, Acc);
false ->
Calls = maps:get(Node, Graph, []),
NewQ = queue:from_list([{New, Ann1, [{Node, Ann} | Path]} || {New, Ann1} <- Calls]),
get_call_chains(Graph, Visited#{Node => true}, queue:join(Queue1, NewQ), Stop, Acc)
end
end.
check_expr(Env, Expr, Type) ->
E = {typed, _, _, Type1} = infer_expr(Env, Expr),
unify(Env, Type1, Type, {check_expr, Expr, Type1, Type}),
@@ -1072,6 +1135,7 @@ infer_expr(Env, {lam, Attrs, Args, Body}) ->
infer_named_arg(Env, NamedArgs, {named_arg, Ann, Id, E}) ->
CheckedExpr = {typed, _, _, ArgType} = infer_expr(Env, E),
check_stateful_named_arg(Env, Id, E),
add_named_argument_constraint(
#named_argument_constraint{
args = NamedArgs,
@@ -1821,7 +1885,7 @@ create_type_errors() ->
ets_new(type_errors, [bag]).
destroy_and_report_type_errors(Env) ->
Errors = ets_tab2list(type_errors),
Errors = lists:reverse(ets_tab2list(type_errors)),
%% io:format("Type errors now: ~p\n", [Errors]),
PPErrors = [ pp_error(unqualify(Env, Err)) || Err <- Errors ],
ets_delete(type_errors),
@@ -1940,6 +2004,18 @@ pp_error({namespace, _Pos, {con, Pos, Name}, _Def}) ->
pp_error({repeated_arg, Fun, Arg}) ->
io_lib:format("Repeated argument ~s to function ~s (at ~s).\n",
[Arg, pp(Fun), pp_loc(Fun)]);
pp_error({stateful_not_allowed, Id, Fun}) ->
io_lib:format("Cannot reference stateful function ~s (at ~s)\nin the definition of non-stateful function ~s.\n",
[pp(Id), pp_loc(Id), pp(Fun)]);
pp_error({value_arg_not_allowed, Value, Fun}) ->
io_lib:format("Cannot pass non-zero value argument ~s (at ~s)\nin the definition of non-stateful function ~s.\n",
[pp_expr("", Value), pp_loc(Value), pp(Fun)]);
pp_error({init_depends_on_state, Which, [_Init | Chain]}) ->
WhichCalls = fun("put") -> ""; ("state") -> ""; (_) -> ", which calls" end,
io_lib:format("The init function should return the initial state as its result and cannot ~s the state,\nbut it calls\n~s",
[if Which == put -> "write"; true -> "read" end,
[ io_lib:format(" - ~s (at ~s)~s\n", [Fun, pp_loc(Ann), WhichCalls(Fun)])
|| {[_, Fun], Ann} <- Chain]]);
pp_error(Err) ->
io_lib:format("Unknown error: ~p\n", [Err]).
src/aeso_compiler.erl
+1 -1
View File
@@ -188,7 +188,7 @@ insert_call_function(Code, FunName, Args, Options) ->
[ Code,
"\n\n",
lists:duplicate(Ind, " "),
"function __call() = ", FunName, "(", string:join(Args, ","), ")\n"
"stateful function __call() = ", FunName, "(", string:join(Args, ","), ")\n"
]).
-spec insert_init_function(string(), options()) -> string().
src/aeso_syntax.erl
+1 -1
View File
@@ -25,7 +25,7 @@
-type ann_origin() :: system | user.
-type ann_format() :: '?:' | hex | infix | prefix | elif.
-type ann() :: [{line, ann_line()} | {col, ann_col()} | {format, ann_format()} | {origin, ann_origin()}].
-type ann() :: [{line, ann_line()} | {col, ann_col()} | {format, ann_format()} | {origin, ann_origin()} | stateful | private].
-type name() :: string().
-type id() :: {id, ann(), name()}.
src/aeso_syntax_utils.erl
+18 -16
View File
@@ -98,29 +98,31 @@ fold(Alg = #alg{zero = Zero, plus = Plus, scoped = Scoped}, Fun, K, X) ->
%% Name dependencies
used_ids(E) ->
[ X || {term, [X]} <- used(E) ].
[ X || {{term, [X]}, _} <- used(E) ].
used_types(T) ->
[ X || {type, [X]} <- used(T) ].
[ X || {{type, [X]}, _} <- used(T) ].
-type entity() :: {term, [string()]}
| {type, [string()]}
| {namespace, [string()]}.
-spec entity_alg() -> alg([entity()]).
-spec entity_alg() -> alg(#{entity() => aeso_syntax:ann()}).
entity_alg() ->
IsBound = fun({K, _}) -> lists:member(K, [bound_term, bound_type]) end,
Unbind = fun(bound_term) -> term; (bound_type) -> type end,
Remove = fun(Keys, Map) -> lists:foldl(fun maps:remove/2, Map, Keys) end,
Scoped = fun(Xs, Ys) ->
{Bound, Others} = lists:partition(IsBound, Ys),
Bound = [E || E <- maps:keys(Ys), IsBound(E)],
Others = Remove(Bound, Ys),
Bound1 = [ {Unbind(Tag), X} || {Tag, X} <- Bound ],
lists:umerge(Xs -- Bound1, Others)
maps:merge(Remove(Bound1, Xs), Others)
end,
#alg{ zero = []
, plus = fun lists:umerge/2
#alg{ zero = #{}
, plus = fun maps:merge/2
, scoped = Scoped }.
-spec used(_) -> [entity()].
-spec used(_) -> [{entity(), aeso_syntax:ann()}].
used(D) ->
Kind = fun(expr) -> term;
(bind_expr) -> bound_term;
@@ -128,14 +130,14 @@ used(D) ->
(bind_type) -> bound_type
end,
NS = fun(Xs) -> {namespace, lists:droplast(Xs)} end,
NotBound = fun({Tag, _}) -> not lists:member(Tag, [bound_term, bound_type]) end,
NotBound = fun({{Tag, _}, _}) -> not lists:member(Tag, [bound_term, bound_type]) end,
Xs =
fold(entity_alg(),
fun(K, {id, _, X}) -> [{Kind(K), [X]}];
(K, {qid, _, Xs}) -> [{Kind(K), Xs}, NS(Xs)];
(K, {con, _, X}) -> [{Kind(K), [X]}];
(K, {qcon, _, Xs}) -> [{Kind(K), Xs}, NS(Xs)];
(_, _) -> []
end, decl, D),
maps:to_list(fold(entity_alg(),
fun(K, {id, Ann, X}) -> #{{Kind(K), [X]} => Ann};
(K, {qid, Ann, Xs}) -> #{{Kind(K), Xs} => Ann, NS(Xs) => Ann};
(K, {con, Ann, X}) -> #{{Kind(K), [X]} => Ann};
(K, {qcon, Ann, Xs}) -> #{{Kind(K), Xs} => Ann, NS(Xs) => Ann};
(_, _) -> #{}
end, decl, D)),
lists:filter(NotBound, Xs).