1  Dialyzer

1 Dialyzer

Dialyzer is a static analysis tool that identifies software discrepancies, such as definite type errors, code that has become dead or unreachable because of programming error, and unnecessary tests, in single Erlang modules or entire (sets of) applications.

Dialyzer can be called from the command line, from Erlang, and from a GUI.

It is assumed that the reader is familiar with the Erlang programming language.

Dialyzer stores the result of an analysis in a Persistent Lookup Table (PLT). The PLT can then be used as a starting point for later analyses. It is recommended to build a PLT with the Erlang/OTP applications that you are using, but also to include your own applications that you are using frequently.

The PLT is built using option --build_plt to Dialyzer. The following command builds the recommended minimal PLT for Erlang/OTP:

dialyzer --build_plt --apps erts kernel stdlib mnesia

Dialyzer looks if there is an environment variable called DIALYZER_PLT and places the PLT at this location. If no such variable is set, Dialyzer places the PLT in a file called .dialyzer_plt in the filename:basedir(user_cache, "erlang") folder. The placement can also be specified using the options --plt or --output_plt.

Information can be added to an existing PLT using option --add_to_plt. If you also want to include the Erlang compiler in the PLT and place it in a new PLT, then use the following command:

dialyzer --add_to_plt --apps compiler --output_plt my.plt

Then you can add your favorite application my_app to the new PLT:

dialyzer --add_to_plt --plt my.plt -r my_app/ebin

But you realize that it is unnecessary to have the Erlang compiler in this one:

dialyzer --remove_from_plt --plt my.plt --apps compiler

Later, when you have fixed a bug in your application my_app, you want to update the PLT so that it becomes fresh the next time you run Dialyzer. In this case, run the following command:

dialyzer --check_plt --plt my.plt

Dialyzer then reanalyzes the changed files and the files that depend on these files. Notice that this consistency check is performed automatically the next time you run Dialyzer with this PLT. Option --check_plt is only for doing so without doing any other analysis.

To get information about a PLT, use the following option:

dialyzer --plt_info

To specify which PLT, use option --plt.

To get the output printed to a file, use option --output_file.

Notice that when manipulating the PLT, no warnings are emitted. To turn on warnings during (re)analysis of the PLT, use option --get_warnings.

Dialyzer has a command-line version for automated use. See dialyzer(3).

Dialyzer can also be used directly from Erlang. See dialyzer(3).

The File window displays a listing of the current directory. Click your way to the directories/modules you want to add or type the correct path in the entry.

Mark the directories/modules you want to analyze for discrepancies and click Add. You can either add the .beam and .erl files directly, or add directories that contain these kind of files. Notice that you are only allowed to add the type of files that can be analyzed in the current mode of operation (see below), and that you cannot mix .beam and .erl files.

Dialyzer has two analysis modes: "Byte Code" and "Source Code". They are controlled by the buttons in the top-middle part of the main window, under Analysis Options.

Under the Warnings pull-down menu, there are buttons that control which discrepancies are reported to the user in the Warnings window. By clicking these buttons, you can enable/disable a whole class of warnings. Information about the classes of warnings is found on the "Warnings" item under the Help menu (in the rightmost top corner).

If modules are compiled with inlining, spurious warnings can be emitted. In the Options menu you can choose to ignore inline-compiled modules when analyzing byte code. When starting from source code, this is not a problem because inlining is explicitly turned off by Dialyzer. The option causes Dialyzer to suppress all warnings from inline-compiled modules, as there is currently no way for Dialyzer to find what parts of the code have been produced by inlining.

Once you have chosen the modules or directories you want to analyze, click the Run button to start the analysis. If you for some reason want to stop the analysis while it is running, click the Stop button.

The information from the analysis is displayed in the Log window and the Warnings window.

When analyzing from source, you might have to supply Dialyzer with a list of include directories and macro definitions (as you can do with the erlc flags -I and -D). This can be done either by starting Dialyzer with these flags from the command line as in:

dialyzer -I my_includes -DDEBUG -Dvsn=42 -I one_more_dir

or by adding these explicitly using submenu Manage Macro Definitions or Manage Include Directories in the Options menu.

The File menu includes options to save the contents of the Log window and the Warnings window. Simply choose the options and enter the file to save the contents in.

There are also buttons to clear the contents of each window.

Dialyzer stores the information of the analyzed functions in a Persistent Lookup Table (PLT), see section The Persistent Lookup Table.

After an analysis, you can inspect this information. In the PLT menu you can choose to either search the PLT or inspect the contents of the whole PLT. The information is presented in EDoc format.

Dialyzer operates somewhere between a classical type checker and a more general static-analysis tool: It checks and consumes function specs, yet doesn't require them, and it can find bugs across modules which consider the dataflow of the programs under analysis. This means Dialyzer can find genuine bugs in complex code, and is pragmatic in the face of missing specs or limited information about the codebase, only reporting issues which it can prove have the potential to cause a genuine issue at runtime. This means Dialyzer will sometimes not report every bug, since it cannot always find this proof.

Dialyzer infers types for all top-level functions in a module. If the module also has a spec given in the source-code, Dialyzer will compare the inferred type to the spec. The comparison checks, for each argument and the return, that the inferred and specified types overlap - which is to say, the types have at least one possible runtime value in common. Notice that Dialyzer does not check that one type contains a subset of values of the other, or that they're precisely equal: This allows Dialyzer to make simplifying assumptions to preserve performance and avoid reporting program flows which could potentially succeed at runtime.

If the inferred and specified types do not overlap, Dialyzer will warn that the spec is invalid with respect to the implementation. If they do overlap, however, Dialyzer will proceed under the assumption that the correct type for the given function is the intersection of the inferred type and the specified type (the rationale being that the user may know something that Dialyzer itself cannot deduce). One implication of this is that if the user gives a spec for a function which overlaps with Dialyzer's inferred type, but is more restrictive, Dialyzer will trust those restrictions. This may then generate an error elsewhere which follows from the erroneously restricted spec.

Examples:

Non-overlapping argument:

-spec foo(boolean()) -> string().
%% Dialyzer will infer: foo(integer()) -> string().
foo(N) ->
    integer_to_list(N).

Since the type of the argument in the spec is different from the type that Dialyzer inferred, Dialyzer will generate the following warning:

some_module.erl:7:2: Invalid type specification for function some_module:foo/1.
 The success typing is t:foo
          (integer()) -> string()
 But the spec is t:foo
          (boolean()) -> string()
 They do not overlap in the 1st argument

Non-overlapping return:

-spec bar(a | b) -> atom().
%% Dialyzer will infer: bar(a | b) -> binary().
bar(a) -> <<"a">>;
bar(b) -> <<"b">>.

Since the return value in the spec and the return value inferred by Dialyzer are different, Dialyzer will generate the following warning:

some_module.erl:11:2: Invalid type specification for function some_module:bar/1.
 The success typing is t:bar
          ('a' | 'b') -> <<_:8>>
 But the spec is t:bar
          ('a' | 'b') -> atom()
 The return types do not overlap

Overlapping spec and inferred type:

-spec baz(a | b) -> non_neg_integer().
%% Dialyzer will infer: baz(b | c | d) -> -1 | 0 | 1.
baz(b) -> -1;
baz(c) -> 0;
baz(d) -> 1.

Dialyzer will "trust" the spec and using the intersection of the spec and inferred type:

baz(b) -> 0 | 1.

Notice how the c and d from the argument to baz/1 and the -1 in the return from the inferred type were dropped once the spec and inferred type were intersected. This could result in warnings being emitted for later functions.

For example, if baz/1 is called like this:

call_baz1(A) ->
    case baz(A) of
        -1 -> negative;
        0 -> zero;
        1 -> positive
    end.

Dialyzer will generate the following warning:

some_module.erl:25:9: The pattern
          -1 can never match the type
          0 | 1

If baz/1 is called like this:

call_baz2() ->
    baz(a).

Dialyzer will generate the following warnings:

some_module.erl:30:1: Function call_baz2/0 has no local return
some_module.erl:31:9: The call t:baz
         ('a') will never return since it differs in the 1st argument
               from the success typing arguments:
         ('b' | 'c' | 'd')

We very much welcome user feedback - even wishlists! If you notice anything weird, especially if Dialyzer reports any discrepancy that is a false positive, please send an error report describing the symptoms and how to reproduce them.

Copyright © 2006-2023 Ericsson AB. All Rights Reserved.