Skip to content

Commit

Permalink
dialyzer: Introduce nominal types
Browse files Browse the repository at this point in the history
This PR implements [EEP-69: Nominal Types](https://www.erlang.org/eeps/eep-0069)
in Dialyzer. As a side effect, nominal types can encode opaque types. We
changed all opaque-handling logic and improved opaque warnings in
Dialyzer.

All existing Erlang type systems are structural: two types are seen as
equivalent if their structures are the same. Type comparison are based
on the structures of the types, not on how the user explicitly defines
them. For example, in the following example, `meter()` and `foot()` are
equivalent. The two types can be used interchangeably. Neither of them
differ from the basic type `integer()`.

    -type meter() :: integer().
    -type foot() :: integer().

Nominal typing is an alternative type system, where two types are
equivalent if and only if they are declared with the same type name.
The EEP proposes one new syntax `-nominal` for declaring nominal types.
Under nominal typing, `meter()` and `foot()` are no longer compatible.
Whenever a function expects type `meter()`, passing in type `foot()`
would result in a Dialyzer error.

    -nominal meter() :: integer().
    -nominal foot() :: integer().

More nominal type-checking rules can be found in the EEP. It is worth
noting that most work for adding nominal types and type-checking
is in `erl_types.erl`. The rest are changes that removed the previous
opaque type-checking, and added an improved version of it using nominal
type-checking with reworked warnings.

Backwards compatibility for opaque type-checking is **not** preserved
by this PR. Previous opaque warnings can appear with slightly different
wordings. A new kind of opaque warning `opaque_union` is added, together
with a Dialyzer option `no_opaque_union` to turn this kind of warnings
off.

This PR is likely not bug-free, but not having it in master is blocking
other changes to Dialyzer. Once nominal type-checking and the new opaque
type-checking are applied to more codebases, we will fix the bugs as
they appear.

Co-authored-by: John Högberg <[email protected]>
  • Loading branch information
lucioleKi and jhogberg committed Nov 21, 2024
1 parent a6e4a5f commit 17402ff
Show file tree
Hide file tree
Showing 121 changed files with 3,289 additions and 3,603 deletions.
Binary file modified bootstrap/lib/compiler/ebin/beam_core_to_ssa.beam
Binary file not shown.
Binary file modified bootstrap/lib/compiler/ebin/beam_disasm.beam
Binary file not shown.
Binary file modified bootstrap/lib/compiler/ebin/beam_doc.beam
Binary file not shown.
Binary file modified bootstrap/lib/compiler/ebin/beam_ssa.beam
Binary file not shown.
Binary file modified bootstrap/lib/compiler/ebin/beam_ssa_alias.beam
Binary file not shown.
Binary file modified bootstrap/lib/compiler/ebin/beam_ssa_bc_size.beam
Binary file not shown.
Binary file modified bootstrap/lib/compiler/ebin/beam_ssa_dead.beam
Binary file not shown.
Binary file modified bootstrap/lib/compiler/ebin/beam_ssa_opt.beam
Binary file not shown.
Binary file modified bootstrap/lib/compiler/ebin/beam_ssa_pp.beam
Binary file not shown.
Binary file modified bootstrap/lib/compiler/ebin/beam_ssa_pre_codegen.beam
Binary file not shown.
Binary file modified bootstrap/lib/compiler/ebin/beam_ssa_type.beam
Binary file not shown.
10 changes: 6 additions & 4 deletions bootstrap/lib/compiler/ebin/compiler.app
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
% This is an -*- erlang -*- file.
%% %CopyrightBegin%
%%
%% Copyright Ericsson AB 1997-2023. All Rights Reserved.
%% Copyright Ericsson AB 1997-2024. All Rights Reserved.
%%
%% Licensed under the Apache License, Version 2.0 (the "License");
%% you may not use this file except in compliance with the License.
Expand All @@ -19,7 +19,7 @@

{application, compiler,
[{description, "ERTS CXC 138 10"},
{vsn, "8.3.2"},
{vsn, "8.5.2"},
{modules, [
beam_a,
beam_asm,
Expand All @@ -31,6 +31,7 @@
beam_dict,
beam_digraph,
beam_disasm,
beam_doc,
beam_flatten,
beam_jump,
beam_listing,
Expand All @@ -43,11 +44,11 @@
beam_ssa_check,
beam_ssa_codegen,
beam_ssa_dead,
beam_ssa_destructive_update,
beam_ssa_lint,
beam_ssa_opt,
beam_ssa_pp,
beam_ssa_pre_codegen,
beam_ssa_private_append,
beam_ssa_recv,
beam_ssa_share,
beam_ssa_ss,
Expand Down Expand Up @@ -76,12 +77,13 @@
sys_core_fold_lists,
sys_core_inline,
sys_core_prepare,
sys_coverage,
sys_messages,
sys_pre_attributes,
v3_core
]},
{registered, []},
{applications, [kernel, stdlib]},
{env, []},
{runtime_dependencies, ["stdlib-5.0","kernel-8.4","erts-13.0",
{runtime_dependencies, ["stdlib-6.0","kernel-8.4","erts-13.0",
"crypto-5.1"]}]}.
Binary file modified bootstrap/lib/compiler/ebin/v3_core.beam
Binary file not shown.
Binary file modified bootstrap/lib/kernel/ebin/code.beam
Binary file not shown.
Binary file modified bootstrap/lib/kernel/ebin/group.beam
Binary file not shown.
12 changes: 8 additions & 4 deletions bootstrap/lib/kernel/ebin/kernel.app
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
%%
%% %CopyrightBegin%
%%
%% Copyright Ericsson AB 1996-2023. All Rights Reserved.
%% Copyright Ericsson AB 1996-2024. All Rights Reserved.
%%
%% Licensed under the Apache License, Version 2.0 (the "License");
%% you may not use this file except in compliance with the License.
Expand All @@ -22,7 +22,7 @@
{application, kernel,
[
{description, "ERTS CXC 138 10"},
{vsn, "9.0.2"},
{vsn, "10.1.1"},
{modules, [application,
application_controller,
application_master,
Expand Down Expand Up @@ -72,6 +72,7 @@
logger_filters,
logger_formatter,
logger_h_common,
logger_handler,
logger_handler_watcher,
logger_olp,
logger_proxy,
Expand All @@ -88,6 +89,7 @@
user_drv,
user_sup,
prim_tty,
prim_tty_sighandler,
disk_log,
disk_log_1,
disk_log_server,
Expand Down Expand Up @@ -121,6 +123,7 @@
seq_trace,
socket,
standard_error,
trace,
wrap_log_reader]},
{registered, [application_controller,
erl_reply,
Expand Down Expand Up @@ -158,10 +161,11 @@
{net_tickintensity, 4},
{net_ticktime, 60},
{prevent_overlapping_partitions, true},
{shell_docs_ansi,auto}
{shell_docs_ansi,auto},
{shell_history_drop,[]}
]},
{mod, {kernel, []}},
{runtime_dependencies, ["erts-14.0", "stdlib-5.0",
{runtime_dependencies, ["erts-15.1", "stdlib-6.0",
"sasl-3.0", "crypto-5.0"]}
]
}.
Binary file modified bootstrap/lib/kernel/ebin/prim_tty.beam
Binary file not shown.
Binary file modified bootstrap/lib/kernel/ebin/user_drv.beam
Binary file not shown.
Binary file modified bootstrap/lib/stdlib/ebin/beam_lib.beam
Binary file not shown.
Binary file modified bootstrap/lib/stdlib/ebin/edlin_context.beam
Binary file not shown.
Binary file modified bootstrap/lib/stdlib/ebin/erl_anno.beam
Binary file not shown.
Binary file modified bootstrap/lib/stdlib/ebin/erl_lint.beam
Binary file not shown.
Binary file modified bootstrap/lib/stdlib/ebin/erl_parse.beam
Binary file not shown.
Binary file modified bootstrap/lib/stdlib/ebin/erl_scan.beam
Binary file not shown.
Binary file modified bootstrap/lib/stdlib/ebin/qlc_pt.beam
Binary file not shown.
Binary file modified bootstrap/lib/stdlib/ebin/rand.beam
Binary file not shown.
9 changes: 6 additions & 3 deletions bootstrap/lib/stdlib/ebin/stdlib.app
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
%%
%% %CopyrightBegin%
%%
%% Copyright Ericsson AB 1996-2023. All Rights Reserved.
%% Copyright Ericsson AB 1996-2024. All Rights Reserved.
%%
%% Licensed under the Apache License, Version 2.0 (the "License");
%% you may not use this file except in compliance with the License.
Expand All @@ -20,7 +20,7 @@
%%
{application, stdlib,
[{description, "ERTS CXC 138 10"},
{vsn, "5.0.2"},
{vsn, "6.1.2"},
{modules, [argparse,
array,
base64,
Expand All @@ -37,6 +37,7 @@
digraph,
digraph_utils,
edlin,
edlin_key,
edlin_context,
edlin_expand,
edlin_type_suggestion,
Expand Down Expand Up @@ -77,6 +78,7 @@
io_lib_format,
io_lib_fread,
io_lib_pretty,
json,
lists,
log_mf_h,
maps,
Expand All @@ -99,6 +101,7 @@
shell,
shell_default,
shell_docs,
shell_docs_markdown,
slave,
sofs,
string,
Expand All @@ -115,6 +118,6 @@
dets]},
{applications, [kernel]},
{env, []},
{runtime_dependencies, ["sasl-3.0","kernel-9.0","erts-13.1","crypto-4.5",
{runtime_dependencies, ["sasl-3.0","kernel-10.0","erts-15.0","crypto-4.5",
"compiler-5.0"]}
]}.
Binary file modified bootstrap/lib/stdlib/ebin/supervisor.beam
Binary file not shown.
1 change: 1 addition & 0 deletions lib/common_test/src/ct_ssh.erl
Original file line number Diff line number Diff line change
Expand Up @@ -1362,6 +1362,7 @@ init(KeyOrName, {ConnType,Addr,Port}, AllOpts) ->
target=KeyOrName}}
end.

-dialyzer({no_opaque_union, [handle_msg/2]}).
-doc false.
handle_msg(sftp_connect, State) ->
#state{ssh_ref=SSHRef, target=Target} = State,
Expand Down
4 changes: 2 additions & 2 deletions lib/compiler/src/beam_core_to_ssa.erl
Original file line number Diff line number Diff line change
Expand Up @@ -1566,7 +1566,7 @@ partition_intersection([U|_]=Us, [_,_|_]=Cs0, St0) ->
case find_key_intersection(Ps) of
none ->
{Us,Cs0,St0};
Ks ->
{ok, Ks} ->
Cs1 = map(fun(#iclause{pats=[Arg|Args]}=C) ->
{Arg1,Arg2} = partition_keys(Arg, Ks),
C#iclause{pats=[Arg1,Arg2|Args]}
Expand Down Expand Up @@ -1601,7 +1601,7 @@ find_key_intersection(Ps) ->
%% the keys could only make the code worse.
none;
false ->
Intersection
{ok, Intersection}
end
end.

Expand Down
8 changes: 4 additions & 4 deletions lib/compiler/src/beam_disasm.erl
Original file line number Diff line number Diff line change
Expand Up @@ -41,8 +41,8 @@
%%-----------------------------------------------------------------------

-type index() :: non_neg_integer().
-type literals() :: 'none' | gb_trees:tree(index(), term()).
-type types() :: 'none' | gb_trees:tree(index(), term()).
-type literals() :: gb_trees:tree(index(), term()).
-type types() :: gb_trees:tree(index(), term()).
-type symbolic_tag() :: 'a' | 'f' | 'h' | 'i' | 'u' | 'x' | 'y' | 'z'.
-type disasm_tag() :: symbolic_tag() | 'fr' | 'atom' | 'float' | 'literal'.
-type disasm_term() :: 'nil' | {disasm_tag(), _}.
Expand Down Expand Up @@ -254,7 +254,7 @@ disasm_lambdas(<<>>, _, _) -> [].
-spec beam_disasm_types('none' | binary()) -> types().

beam_disasm_types(none) ->
none;
gb_trees:empty();
beam_disasm_types(<<Version:32,Count:32,Table0/binary>>) ->
case beam_types:convert_ext(Version, Table0) of
none ->
Expand All @@ -265,7 +265,7 @@ beam_disasm_types(<<Version:32,Count:32,Table0/binary>>) ->
Res
end;
beam_disasm_types(<<_/binary>>) ->
none.
gb_trees:empty().

disasm_types(Types0, Index) ->
case beam_types:decode_ext(Types0) of
Expand Down
25 changes: 13 additions & 12 deletions lib/compiler/src/beam_doc.erl
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@
deprecated = #{} :: map(),

docformat = ?DEFAULT_FORMAT :: binary(),
moduledoc = {?DEFAULT_MODULE_DOC_LOC, none} :: {integer() | erl_anno:anno(), none | map() | hidden},
moduledoc = {erl_anno:new(?DEFAULT_MODULE_DOC_LOC), none} :: {erl_anno:anno(), none | map() | hidden},
moduledoc_meta = none :: none | #{ _ := _ },

behaviours = [] :: list(module()),
Expand Down Expand Up @@ -110,7 +110,7 @@
%% populates all function / types, callbacks. it is updated on an ongoing basis
%% since a doc attribute `doc ...` is not known in a first pass to be attached
%% to a function / type / callback.
docs = #{} :: #{{Attribute :: function | type | opaque | callback,
docs = #{} :: #{{Attribute :: function | type | opaque | nominal | callback,
FunName :: atom(),
Arity :: non_neg_integer()}
=>
Expand Down Expand Up @@ -145,7 +145,7 @@
%% -doc #{author => "X"}.
%% -doc foo() -> ok.
%%
%% thus, after reading a terminal AST node (spec, type, fun declaration, opaque, callback),
%% thus, after reading a terminal AST node (spec, type, fun declaration, opaque, nominal, callback),
%% the intermediate state saved in the fields below needs to be
%% saved in the `docs` field.

Expand Down Expand Up @@ -459,7 +459,7 @@ track_documentation(_, State) ->
upsert_documentation_from_terminal_item({function, Anno, F, Arity, _}, State) ->
upsert_documentation(function, F, Arity, Anno, State);
upsert_documentation_from_terminal_item({attribute, Anno, TypeOrOpaque, {TypeName, _TypeDef, TypeArgs}},State)
when TypeOrOpaque =:= type; TypeOrOpaque =:= opaque ->
when TypeOrOpaque =:= type; TypeOrOpaque =:= opaque; TypeOrOpaque =:= nominal ->
Arity = length(fun_to_varargs(TypeArgs)),
upsert_documentation(type, TypeName, Arity, Anno, State);
upsert_documentation_from_terminal_item({attribute, Anno, callback, {{CB, Arity}, _Form}}, State) ->
Expand All @@ -470,6 +470,7 @@ upsert_documentation_from_terminal_item(_, State) ->
upsert_documentation(Tag, Name, Arity, Anno, State) when Tag =:= function;
Tag =:= type;
Tag =:= opaque;
Tag =:= nominal;
Tag =:= callback ->
Docs = State#docs.docs,
State1 = case maps:get({Tag, Name, Arity}, Docs, none) of
Expand Down Expand Up @@ -579,7 +580,7 @@ extract_hidden_types0({attribute, _Anno, doc, _}, State) ->
extract_hidden_types0({attribute, _Anno, TypeOrOpaque, {Name, _Type, Args}},
#docs{hidden_status = hidden,
hidden_types = HiddenTypes}=State)
when TypeOrOpaque =:= type; TypeOrOpaque =:= opaque ->
when TypeOrOpaque =:= type; TypeOrOpaque =:= opaque; TypeOrOpaque =:= nominal ->
State#docs{hidden_status = none,
hidden_types = sets:add_element({Name, length(Args)}, HiddenTypes)};
extract_hidden_types0(_, State) ->
Expand All @@ -593,7 +594,7 @@ extract_hidden_types0(_, State) ->
%% #{{TypeName, length(Args)} => Anno}.
%%
extract_type_defs0({attribute, Anno, TypeOrOpaque, {TypeName, _TypeDef, TypeArgs}}, #docs{type_defs = TypeDefs}=State)
when TypeOrOpaque =:= type; TypeOrOpaque =:= opaque ->
when TypeOrOpaque =:= type; TypeOrOpaque =:= opaque; TypeOrOpaque =:= nominal ->
Args = fun_to_varargs(TypeArgs),
Type = {TypeName, length(Args)},
State#docs{type_defs = TypeDefs#{Type => Anno}};
Expand Down Expand Up @@ -660,7 +661,7 @@ update_docstatus(State, V) ->

update_ast(function, #docs{ast_fns=AST}=State, Fn) ->
State#docs{ast_fns = [Fn | AST]};
update_ast(Type,#docs{ast_types=AST}=State, Fn) when Type =:= type; Type =:= opaque->
update_ast(Type,#docs{ast_types=AST}=State, Fn) when Type =:= type; Type =:= opaque; Type =:= nominal->
State#docs{ast_types = [Fn | AST]};
update_ast(callback, #docs{ast_callbacks = AST}=State, Fn) ->
State#docs{ast_callbacks = [Fn | AST]}.
Expand Down Expand Up @@ -873,7 +874,7 @@ extract_documentation0({function, _Anno, F, A, _Body}=AST, State) ->
State1 = remove_exported_type_info({function, F, A}, State),
extract_documentation_from_funs(AST, State1);
extract_documentation0({attribute, _Anno, TypeOrOpaque, _}=AST,State)
when TypeOrOpaque =:= type; TypeOrOpaque =:= opaque ->
when TypeOrOpaque =:= type; TypeOrOpaque =:= opaque; TypeOrOpaque =:= nominal ->
extract_documentation_from_type(AST, State);
extract_documentation0({attribute, _Anno, callback, {{CB, A}, _Form}}=AST, State) ->
State1 = remove_exported_type_info({callback, CB, A}, State),
Expand Down Expand Up @@ -956,7 +957,7 @@ extract_user_types(_Else, Acc) ->

extract_documentation_from_type({attribute, Anno, TypeOrOpaque, {TypeName, _TypeDef, TypeArgs}=Types},
#docs{docs = Docs, exported_types=ExpTypes}=State)
when TypeOrOpaque =:= type; TypeOrOpaque =:= opaque ->
when TypeOrOpaque =:= type; TypeOrOpaque =:= opaque; TypeOrOpaque =:= nominal ->
Args = fun_to_varargs(TypeArgs),
Key = {type, TypeName, length(TypeArgs)},

Expand All @@ -979,9 +980,9 @@ add_last_read_user_type(_Anno, {_TypeName, TypeDef, TypeArgs}, State) ->
Types = extract_user_types([TypeArgs, TypeDef], State),
set_last_read_user_types(State, Types).

%% NOTE: Terminal elements for the documentation, such as `-type`, `-opaque`, `-callback`,
%% and functions always need to reset the state when they finish, so that new
%% new AST items start with a clean slate.
%% NOTE: Terminal elements for the documentation, such as `-type`, `-opaque`,
%% `-nominal`, `-callback`, and functions always need to reset the state when
%% they finish, so that new AST items start with a clean slate.
extract_documentation_from_funs({function, Anno, F, A, [{clause, _, ClauseArgs, _, _}]},
#docs{exported_functions = ExpFuns}=State) ->
case (sets:is_element({F, A}, ExpFuns) orelse State#docs.export_all) of
Expand Down
8 changes: 4 additions & 4 deletions lib/compiler/src/beam_ssa_dead.erl
Original file line number Diff line number Diff line change
Expand Up @@ -240,7 +240,7 @@ shortcut_3(L, From, Bs0, UnsetVars0, St) ->
%% because it refers to a variable defined
%% in this block.
shortcut_unsafe_br(Br, L, Bs, UnsetVars0, St);
UnsetVars ->
{safe, UnsetVars} ->
%% Continue checking whether this br is
%% suitable.
shortcut_test_br(Br, L, Bs, UnsetVars, St)
Expand Down Expand Up @@ -381,16 +381,16 @@ update_unset_vars(L, Is, Br, UnsetVars, #st{skippable=Skippable}) ->
%% to the UnsetVars set would not change
%% the outcome of the tests in
%% is_br_safe/2.
UnsetVars
{safe, UnsetVars}
end;
#b_br{} ->
UnsetVars
{safe, UnsetVars}
end;
false ->
%% Some variables defined in this block are used by
%% successors. We must update the set of unset variables.
SetInThisBlock = [V || #b_set{dst=V} <:- Is],
list_set_union(SetInThisBlock, UnsetVars)
{safe, list_set_union(SetInThisBlock, UnsetVars)}
end.

shortcut_two_way(#b_br{succ=Succ,fail=Fail}, From, Bs0, UnsetVars0, St0) ->
Expand Down
Loading

0 comments on commit 17402ff

Please sign in to comment.