Break the dependecy between constraints and env

This commit is contained in:
Gaith Hallak 2023-05-06 14:07:14 +03:00
parent b98af0fab6
commit 8475b024df
3 changed files with 113 additions and 118 deletions

View File

@ -73,6 +73,9 @@ potential_unused_variables(A, B, C) -> aeso_tc_warnings:potential_unused_variabl
potential_unused_function(A, B, C, D) -> aeso_tc_warnings:potential_unused_function(A, B, C, D).
mk_warning(A) -> aeso_tc_warnings:mk_warning(A).
used_stateful(A) -> aeso_tc_warnings:used_stateful(A).
used_variable(A, B, C) -> aeso_tc_warnings:used_variable(A, B, C).
register_function_call(A, B) -> aeso_tc_warnings:register_function_call(A, B).
used_constant(A, B) -> aeso_tc_warnings:used_constant(A, B).
warn_potential_negative_spend(A, B, C) -> aeso_tc_warnings:warn_potential_negative_spend(A, B, C).
warn_potential_division_by_zero(A, B, C) -> aeso_tc_warnings:warn_potential_division_by_zero(A, B, C).
potential_unused_return_value(A) -> aeso_tc_warnings:potential_unused_return_value(A).
@ -1060,10 +1063,10 @@ infer_expr(_Env, Body={id, As, "???"}) ->
type_error({hole_found, As, T}),
{typed, As, Body, T};
infer_expr(Env, Id = {Tag, As, _}) when Tag == id; Tag == qid ->
{QName, Type} = aeso_tc_env:lookup_name(Env, As, Id),
{QName, Type} = lookup_name(Env, As, Id),
{typed, As, QName, Type};
infer_expr(Env, Id = {Tag, As, _}) when Tag == con; Tag == qcon ->
{QName, Type} = aeso_tc_env:lookup_name(Env, As, Id, [freshen]),
{QName, Type} = lookup_name(Env, As, Id, [freshen]),
{typed, As, QName, Type};
infer_expr(Env, {tuple, As, Cpts}) ->
NewCpts = [infer_expr(Env, C) || C <- Cpts],
@ -1582,3 +1585,61 @@ get_oracle_type({qid, _, ["Oracle", "check"]}, [OType| _], _ ) -> OTyp
get_oracle_type({qid, _, ["Oracle", "check_query"]}, [OType| _], _ ) -> OType;
get_oracle_type({qid, _, ["Oracle", "respond"]}, [OType| _], _ ) -> OType;
get_oracle_type(_Fun, _Args, _Ret) -> false.
lookup_name(Env, As, Name) ->
lookup_name(Env, As, Name, []).
lookup_name(Env, As, Id, Options) ->
case aeso_tc_env:lookup_env(Env, term, As, qname(Id)) of
false ->
type_error({unbound_variable, Id}),
{Id, fresh_uvar(As)};
{QId, {_, Ty}} ->
NS = aeso_tc_env:namespace(Env),
CurFn = aeso_tc_env:current_function(Env),
%% Variables and functions cannot be used when CurFn is `none`.
%% i.e. they cannot be used in toplevel constants
[ begin
when_warning(
warn_unused_variables,
fun() -> used_variable(NS, name(CurFn), QId) end),
when_warning(
warn_unused_functions,
fun() -> register_function_call(NS ++ qname(CurFn), QId) end)
end || CurFn =/= none ],
when_warning(warn_unused_constants, fun() -> used_constant(NS, QId) end),
Freshen = proplists:get_value(freshen, Options, false),
check_stateful(Env, Id, Ty),
Ty1 = case Ty of
{type_sig, _, _, _, _, _} -> aeso_tc_constraints:freshen_type_sig(As, Ty);
_ when Freshen -> aeso_tc_constraints:freshen_type(As, Ty);
_ -> Ty
end,
{set_qname(QId, Id), Ty1}
end.
check_stateful(Env, Id, Type = {type_sig, _, _, _, _, _}) ->
IsStatefulType = aeso_syntax:get_ann(stateful, Type, false),
IsStatefulType andalso (check_stateful_not_in_guard(Env, Id) andalso check_stateful_in_stateful_fun(Env, Id)),
ok;
check_stateful(Env, _Id, _Type) ->
when_warning(warn_unused_stateful, fun() -> used_stateful(aeso_tc_env:current_function(Env)) end),
ok.
check_stateful_not_in_guard(Env, Id) ->
case aeso_tc_env:in_guard(Env) of
false -> true;
true ->
type_error({stateful_not_allowed_in_guards, Id}),
false
end.
check_stateful_in_stateful_fun(Env, Id) ->
case aeso_tc_env:stateful(Env) of
true -> true;
false ->
type_error({stateful_not_allowed, Id, aeso_tc_env:current_function(Env)}),
false
end.

View File

@ -13,6 +13,8 @@
, add_field_constraint/5
, add_dependent_type_constraint/5
, add_record_create_constraint/3
, freshen_type/2
, freshen_type_sig/2
]).
%% -- Duplicated types -------------------------------------------------------
@ -51,12 +53,6 @@ is_first_order(A) -> aeso_tc_type_utils:is_first_order(A).
app_t(A, B, C) -> aeso_tc_type_utils:app_t(A, B, C).
fresh_uvar(A) -> aeso_tc_type_utils:fresh_uvar(A).
%% -------
freshen(A) -> aeso_tc_env:freshen(A).
create_freshen_tvars() -> aeso_tc_env:create_freshen_tvars().
destroy_freshen_tvars() -> aeso_tc_env:destroy_freshen_tvars().
%% ---------------------------------------------------------------------------
-type env() :: aeso_tc_env:env().
@ -555,3 +551,51 @@ solve_for_uvar(Env, UVar = {uvar, Attrs, _}, Fields0) ->
{StillPossible, _} ->
{ambiguous_record, Fields, StillPossible}
end.
create_freshen_tvars() ->
aeso_tc_ets_manager:ets_new(freshen_tvars, [set]).
destroy_freshen_tvars() ->
aeso_tc_ets_manager:ets_delete(freshen_tvars).
freshen(Type) ->
freshen(aeso_syntax:get_ann(Type), Type).
freshen(Ann, {tvar, _, Name}) ->
NewT = case aeso_tc_ets_manager:ets_lookup(freshen_tvars, Name) of
[] -> fresh_uvar(Ann);
[{Name, T}] -> T
end,
aeso_tc_ets_manager:ets_insert(freshen_tvars, {Name, NewT}),
NewT;
freshen(Ann, {bytes_t, _, any}) ->
X = fresh_uvar(Ann),
aeso_tc_constraints:add_is_bytes_constraint(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.
freshen_type(Ann, Type) ->
create_freshen_tvars(),
Type1 = freshen(Ann, Type),
destroy_freshen_tvars(),
Type1.
freshen_type_sig(Ann, TypeSig = {type_sig, _, Constr, _, _, _}) ->
FunT = freshen_type(Ann, aeso_tc_type_utils:typesig_to_fun_t(TypeSig)),
apply_typesig_constraint(Ann, Constr, FunT),
FunT.
apply_typesig_constraint(_Ann, none, _FunT) -> ok;
apply_typesig_constraint(Ann, address_to_contract, {fun_t, _, [], [_], Type}) ->
aeso_tc_constraints:add_is_contract_constraint(Type, {address_to_contract, Ann});
apply_typesig_constraint(Ann, bytes_concat, {fun_t, _, [], [A, B], C}) ->
aeso_tc_constraints:add_add_bytes_constraint(Ann, concat, A, B, C);
apply_typesig_constraint(Ann, bytes_split, {fun_t, _, [], [C], {tuple_t, _, [A, B]}}) ->
aeso_tc_constraints:add_add_bytes_constraint(Ann, split, A, B, C);
apply_typesig_constraint(Ann, bytecode_hash, {fun_t, _, _, [Con], _}) ->
aeso_tc_constraints:add_is_contract_constraint(Con, {bytecode_hash, Ann}).

View File

@ -54,8 +54,6 @@
]).
-export([ lookup_env/4
, lookup_name/3
, lookup_name/4
, lookup_type/2
, lookup_record_field/2
, lookup_record_field/3
@ -68,13 +66,6 @@
, empty_env/0
]).
%% Freshening
-export([ fresh_uvar/1
, freshen/1
, create_freshen_tvars/0
, destroy_freshen_tvars/0
]).
-export([destroy_and_report_type_errors/1]).
-export_type([env/0]).
@ -153,7 +144,6 @@ name(A) -> aeso_tc_name_manip:name(A).
qname(A) -> aeso_tc_name_manip:qname(A).
qid(A, B) -> aeso_tc_name_manip:qid(A, B).
qcon(A, B) -> aeso_tc_name_manip:qcon(A, B).
set_qname(A, B) -> aeso_tc_name_manip:set_qname(A, B).
%% -------
@ -163,10 +153,6 @@ type_error(A) -> aeso_tc_errors:type_error(A).
warn_potential_shadowing(A, B, C) -> aeso_tc_warnings:warn_potential_shadowing(A, B, C).
used_include(A) -> aeso_tc_warnings:used_include(A).
used_variable(A, B, C) -> aeso_tc_warnings:used_variable(A, B, C).
used_stateful(A) -> aeso_tc_warnings:used_stateful(A).
register_function_call(A, B) -> aeso_tc_warnings:register_function_call(A, B).
used_constant(A, B) -> aeso_tc_warnings:used_constant(A, B).
%% -------
@ -581,54 +567,6 @@ lookup_env1(#env{ namespace = Current, used_namespaces = UsedNamespaces, scopes
end
end.
lookup_name(Env, As, Name) ->
lookup_name(Env, As, Name, []).
lookup_name(Env = #env{ namespace = NS, current_function = CurFn }, As, Id, Options) ->
case lookup_env(Env, term, As, qname(Id)) of
false ->
type_error({unbound_variable, Id}),
{Id, fresh_uvar(As)};
{QId, {_, Ty}} ->
%% Variables and functions cannot be used when CurFn is `none`.
%% i.e. they cannot be used in toplevel constants
[ begin
when_warning(
warn_unused_variables,
fun() -> used_variable(NS, name(CurFn), QId) end),
when_warning(
warn_unused_functions,
fun() -> register_function_call(NS ++ qname(CurFn), QId) end)
end || CurFn =/= none ],
when_warning(warn_unused_constants, fun() -> used_constant(NS, QId) end),
Freshen = proplists:get_value(freshen, Options, false),
check_stateful(Env, Id, Ty),
Ty1 = case Ty of
{type_sig, _, _, _, _, _} -> freshen_type_sig(As, Ty);
_ when Freshen -> freshen_type(As, Ty);
_ -> Ty
end,
{set_qname(QId, Id), Ty1}
end.
check_stateful(#env{ in_guard = true }, Id, Type = {type_sig, _, _, _, _, _}) ->
case aeso_syntax:get_ann(stateful, Type, false) of
false -> ok;
true ->
type_error({stateful_not_allowed_in_guards, Id})
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{ current_function = Fun }, _Id, _Type) ->
when_warning(warn_unused_stateful, fun() -> used_stateful(Fun) end),
ok.
-spec lookup_record_field(env(), name()) -> [field_info()].
lookup_record_field(Env, FieldName) ->
maps:get(FieldName, Env#env.fields, []).
@ -1001,51 +939,3 @@ unqualify1(NS, Xs) ->
_ -> Xs
catch _:_ -> Xs
end.
create_freshen_tvars() ->
aeso_tc_ets_manager:ets_new(freshen_tvars, [set]).
destroy_freshen_tvars() ->
aeso_tc_ets_manager:ets_delete(freshen_tvars).
freshen_type(Ann, Type) ->
create_freshen_tvars(),
Type1 = freshen(Ann, Type),
destroy_freshen_tvars(),
Type1.
freshen(Type) ->
freshen(aeso_syntax:get_ann(Type), Type).
freshen(Ann, {tvar, _, Name}) ->
NewT = case aeso_tc_ets_manager:ets_lookup(freshen_tvars, Name) of
[] -> fresh_uvar(Ann);
[{Name, T}] -> T
end,
aeso_tc_ets_manager:ets_insert(freshen_tvars, {Name, NewT}),
NewT;
freshen(Ann, {bytes_t, _, any}) ->
X = fresh_uvar(Ann),
aeso_tc_constraints:add_is_bytes_constraint(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.
freshen_type_sig(Ann, TypeSig = {type_sig, _, Constr, _, _, _}) ->
FunT = freshen_type(Ann, aeso_tc_type_utils:typesig_to_fun_t(TypeSig)),
apply_typesig_constraint(Ann, Constr, FunT),
FunT.
apply_typesig_constraint(_Ann, none, _FunT) -> ok;
apply_typesig_constraint(Ann, address_to_contract, {fun_t, _, [], [_], Type}) ->
aeso_tc_constraints:add_is_contract_constraint(Type, {address_to_contract, Ann});
apply_typesig_constraint(Ann, bytes_concat, {fun_t, _, [], [A, B], C}) ->
aeso_tc_constraints:add_add_bytes_constraint(Ann, concat, A, B, C);
apply_typesig_constraint(Ann, bytes_split, {fun_t, _, [], [C], {tuple_t, _, [A, B]}}) ->
aeso_tc_constraints:add_add_bytes_constraint(Ann, split, A, B, C);
apply_typesig_constraint(Ann, bytecode_hash, {fun_t, _, _, [Con], _}) ->
aeso_tc_constraints:add_is_contract_constraint(Con, {bytecode_hash, Ann}).