View Source Dialyzer

Introduction

Scope

Dialyzer is a static analysis tool that identifies software discrepancies, such as definite type errors, code that is unreachable because of programming error, and unnecessary tests in single Erlang modules or an entire codebase.

Dialyzer can be called from the command line and from Erlang.

The Persistent Lookup Table

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. Note that this consistency check is performed automatically the next time you run Dialyzer with this PLT. Use option --check_plt to perform the consistency check 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.

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

Using Dialyzer from the Command Line

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

Using Dialyzer from Erlang

Dialyzer can also be used directly from Erlang. See dialyzer.

Dialyzer's Model of Analysis

Dialyzer operates somewhere between a classical type checker and a more general static-analysis tool: It checks and consumes function specs, yet does not 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.

How Dialyzer Uses Function Specifications

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 are 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. However, if they do overlap, 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 that 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 some_module:foo
          (integer()) -> string()
 But the spec is some_module: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 some_module:bar
          ('a' | 'b') -> <<_:8>>
 But the spec is some_module: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')

Feedback and Bug Reports

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