dwango/fialyzer

[WIP] Faster Implementation of Dialyzer

fialyzer

Faster Implementation of Dialyzer

How to Use

Using Docker

docker run --rm -v $(pwd):/home/opam/fialyzer yoshihiro503/fialyzer --plt <plt_file> <beam_files>

Commandline Options

Option	Description
--plt <plt_file>	Use the specified plt as the initial plt (optional)
--debug	Print debug logs (optional)
--help	Display this list of options

How to Build (for developers)

Prerequisite

• ocaml-4.07.0 or higher
• opam-2.0.0 or higher
• GMP
• Perl
• odoc (optional, for make odoc)
• Erlang/OTP (optional, for make test)
• Docker (optional, for make pdf)

Build

# If you prefer to use per-package environment, do:
$ opam switch create fialyzer ocaml-base-compiler.4.07.1
$ eval $(opam env)

# Clone repo:
$ git clone [email protected]:dwango/fialyzer.git
$ cd fialyzer

# Install dependencies:
$ opam pin add -y fialyzer .

# Build package:
$ make

fialyzer's Issues

Plt: erl_type: support BinaryTag type

Read PLT file and take BinaryTag types generated from following type contracts:

-spec foo() -> binary().
-spec bar() -> bitstring().
-spec baz(<<_:M, _:_*N>>) -> ok.

Plt: erl_type: support Matchstate Tag type

https://github.com/erlang/otp/blob/OTP-21.1.1/lib/hipe/cerl/erl_types.erl#L349

Plt: erl_type: suppor int-range and int-set type

support following types:

• -1 | 0 | 1
• 1..255

Extend derivation rule to support list pattern

e.g.

case x of
  [X|XS] -> ...;
  [] -> ...
end

introduce mli signatures

Pretty print `type`

Support local fun ref

ref: #78

Support match expr

ref: #78

Pattern = Expression form is called match expression and = operator is called match operator.
(NOTICE: case E of ... end is case expression, not match expression)

but match expr is so crazy...

Erlang/OTP 21 [erts-10.1.3] [source] [64-bit] [smp:4:4] [ds:4:4:10] [async-threads:1] [hipe] [dtrace]

Eshell V10.1.3  (abort with ^G)
1> {A, B} = {1, [Z = 2]}, Z.
2

Implement sup and inf of two types

blackbox tests with PLT

Currently, it cannot specify PLT file to run blackbox-tests.
We have to make it possible to specify PLT file because PLT is needed to test various codes.

Refactor AST-related things

Decided in the previous fialyzer weekly meeting.

• Rename ast_intf.ml to ast.ml
  • expr, spec_fun, decl_fun, module_,
• Create type.ml
  • Move typ and constraint (constraint_)

Support map pattern

translate Abstract Format to internal AST

introduce the translator:

val code_to_expr : Abstract_format.t -> expr Result.t

Support fun expr

ref #78

read spec annotations

Plt: convert Erl_type.t to Type.t

introduce common utility module

support BIF

Fialyzer should know type signatures of BIF (Built-In Function).
see https://github.com/erlang/otp/blob/OTP-21.1.3/lib/dialyzer/src/dialyzer_typesig.erl#L1246-L1737

derivation rule [CASE]

Solve: recursive execution of `solve`

refactroing: rename `sol`

rename sol -> solution for readability

constraint solver

introduce the solve function:

type sol = (type_var, typ) Map.t
val solve : sol -> constraint_ -> sol Result.t

CUI: handle expected errors

• No such beam file
• unbound variable V
• unknown MFA call
• type errors

MFA should be record

Currently, the data constructor MFA is defined as follows:

type expr =
   ...
    | MFA of expr * expr * expr

However, using 3-tuple of expr is not good for readability. So, I think that it should be:

type expr =
     | MFA of { module_name: expr, function_name: expr, arity: expr }

How do you think? @yoshihiro503 @amutake

Plt module

Abstract

introduce Plt module that treat dialyzer plt file.

type t
val from_file : filename -> (t, exn) Result.t

Related link

• dialyzer_plt.erl
• abstract_term_format

solve subtyping constraint

implement the function:

val solve_sub : sol -> type -> type -> sol Result.t

Commandline interface

implement [Letrec] rule

implement a derivation rule [Letrec]

Support map-related expression

#{a => b} and Map#{a => b}

Rename ast_intf to ast

Rename related module names also.

Show line number (Constant, Var)

Currenlty, fialyzer doesn't show line number. To do so, Ast.expr should have line number.
At first, add line number support for Constant and Var.

Add blackbox tests

Add a LYSE example into blackbox-test

https://learnyousomeerlang.com/dialyzer#type-inference-and-discrepancies

-module(discrep1).
-export([run/0]).
 
run() -> some_op(5, you).
 
some_op(A, B) -> A + B.

PatStruct should be supported

Currently, ast_intf.ml has PatStruct of string list * expr, which means struct pattern. However, it cannot be implemented since it seems that obeam doesn't support such pattern currently.

Support list comprehension

list comprehension [E_0 || Q_1, ..., Q_k]

support derivation for multiple applications

Support big int literal

fix:
https://github.com/dwango/fialyzer/blob/master/lib/from_erlang.ml#L13

Ast_intf: remove TyConstraint from typ

type typ =
...
    | TyConstraint of typ * constraint_

I thought that this variant of typ was necessary for implementing the type derivation, but apparently it seems unnecessary.
see also: https://github.com/erlang/otp/blob/OTP-21.1.3/lib/dialyzer/src/dialyzer_typesig.erl#L340-L372

Plt: erl_type: support VarTag type

Support various patterns in top-level functions

Currently, variable pattern and universal pattern in top-level function is only supported.
This issue is about adding support for map, literal, tuple, and list pattern.

Support list expression

Add two variants to Ast_intf.expr

• ListNil
• ListCons of expr * expr

and fix conversions From_erlang.expr_of_erlang_expr

• string literal should be ListCons or ListNil
• [] shold be ListNil
• [<expr> | <expr>] and [<expr>, ...] shold be ListCons

Don't support:

• list patterns
• list comprehension expression

solve disjunctions of constraints

For solving constraints generated by case expressions.

solve_eq with union type

Install obeam from opam instead of submodule

https://opam.ocaml.org/packages/obeam/ 🎉

Plt: erl_type: support TupleSetTag type

{'ok', integer()} | {'error', term()}

Support list pattern

Add constructors PatNil and PatCons to type pattern'.

Logging

type derivation

introduce the function:

val derive : context -> expr -> (constraint * type) Result.t

Support literal pattern

Disable unwrapping Fialyzer module