Temporary measure: break cycles by timing out

[erszcz]

Current master branch is known to fall into infinite loops on some forms. It's evidenced by the property tests and real-world issues like #360. EDIT: please see #383 (comment) for the explanation why this is crossed out.

This PR tries to improve the UX and facilitate dogfooding by a temporary measure of forcibly breaking infinite loops after a timeout and therefore turning situations of hogging the CPU or never terminating into warning messages.

When Gradualizer is run interactively from the CLI or as a Rebar plugin, it's easy to conclude that it's stuck on a given file. However, it's still problematic when it gets stuck, as it prevents us from assessing the number of forms in the project which cause it to loop.

When Gradualizer is run as a background integration task, the only means of realising that it's stuck is the lack of diagnostics and the sound of fans cooling down the CPU.

This PR improves the situation in both of the above cases:

• it allows to finish the CLI / Rebar plugin run and assess the number of Timeout warnings to understand how many forms causing Gradualizer to fail are present in real-world code,
• it allows to finish a background run and only mark some forms in the editor with the Timeout diagnostic, providing valuable feedback on other forms which do not time out and are successfully type checked.

[erszcz]

Current master branch is known to fall into infinite loops on some forms.

I have taken another look at it and I have to correct the above. I couldn't find evidence about the current master branch looping on real world code. Only on synthetic, generated recursive types in property tests.

Below is a comparison between 3 branches:

• upstream-master, i.e. this repo's master branch
• erszcz-master, i.e. my forks master branch with WIP: Fix list exhaustiveness checking regressions #359 and this PR merged in
• erszcz-gradient, my branch with just this PR merged in, currently used by https://github.com/esl/gradient

The test file contains 3 problems I identified when dogfooding with Gradualizer as a background diagnostics provider for ErlangLS or by running make gradualize:

• functions f, g, and h are the regressions introduced when extending exhaustiveness checking to non-trivial types - these are already mentioned in WIP: Fix list exhaustiveness checking regressions #359
• function type_/1 which case matches on a relatively big and complex union type type_() - this checks if exhaustiveness checking, also on types with string()s and lists, works
• function format_binding_type/2 which returns a deep list: io_lib:chars() which causes WIP: Fix list exhaustiveness checking regressions #359 to loop

The results are that:

• upstream-master doesn't loop on io_lib:chars(), but it has the regressions
• erszcz-master fixes the regressions, but it loops on io_lib:chars(), therefore to maintain usability it requires this PR
• erszcz-gradient doesn't loop on io_lib:chars(), but it has the regressions; as expected from the above two points, the fact that it has this PR merged in doesn't change anything

I also did a similar test of the code from #360 - the results are here: https://gist.github.com/erszcz/4323e97860e67da290f52e2b0998a863 (search for timeout). The only timing out function here is inputs:get_input_filename/2. This function operates on file names, specifically it refers to type file:name_all(), which similarly to io_lib:chars() also is a deep list. This suggests #359 loops on deep lists.

---

The test file in full detail:

-module(syntax).

f( Needle, [Needle | _]) -> ok;
f( Needle, [_ | Haystack]) -> f(Needle, Haystack);
f(_Needle, []) -> ok.

-spec g([a | b]) -> ok.
g([a | _Haystack]) -> ok;
g([_ | Haystack]) -> g(Haystack);
g([]) -> ok.

-spec h([a | b]) -> ok.
h([a | _Haystack]) -> ok;
h([]) -> ok;
h([_ | Haystack]) -> h(Haystack).

%%
%%' Datatypes
%%

-type ty() :: {var, index(), context_size()}
            | {id, string()}
            | {arr, ty(), ty()}
            | unit
            | {record, [{string(), ty()}]}
            | {rec, string(), ty()}
            | {variant, [{string(), ty()}]}
            | bool
            | string
            | float
            | nat.

-type info() :: {pos_integer(), pos_integer()}.

-type token() :: {atom(), info()}
               | {atom(), info(), string()}.

-type index() :: non_neg_integer().
-type context_size() :: non_neg_integer().

-type term_() :: {true, info()}
               | {false, info()}
               | {if_, info(), term_(), term_(), term_()}
               | {case_, info(), term_(), [{string(), {string(), term_()}}]}
               | {tag, info(), string(), term_(), ty()}
               | {var, info(), index(), context_size()}
               | {abs, info(), string(), ty(), term_()}
               | {app, info(), term_(), term_()}
               | {let_, info(), string(), term_(), term_()}
               | {fix, info(), term_()}
               | {string, info(), string()}
               | {unit, info()}
               | {ascribe, info(), term_(), ty()}
               | {proj, info(), term_(), string()}
               | {record, info(), [{string(), term_()}]}
               | {float, info(), float()}
               | {timesfloat, info(), term_(), term_()}
               | {zero, info()}
               | {succ, info(), term_()}
               | {pred, info(), term_()}
               | {is_zero, info(), term_()}
               | {inert, info(), ty()}.
%% TAPL `term' type, but `term()' is a builtin type in Erlang,
%% hence the name `term_()'.

-type binding() :: name_bind
                 | ty_var_bind
                 | {var_bind, ty()}
                 | {tm_abb_bind, term_(), ty() | none}
                 | {ty_abb_bind, ty()}.

-type context() :: [{string(), binding()}].

-type command() :: {eval, info(), term()}
                 | {bind, info(), string(), binding()}.

%%.
%%' Constructors
%%

-spec ty(ty()) -> ty().
ty(Ty) ->
    case Ty of
        {var, _, _} -> Ty;
        %{id, _} -> Ty;
        {arr, _, _} -> Ty;
        unit -> Ty;
        {record, _} -> Ty;
        {rec, _, _} -> Ty;
        {variant, _} -> Ty;
        bool -> Ty;
        string -> Ty;
        float -> Ty;
        nat -> Ty
    end.

-spec info(token()) -> info().
info({_, Info}) -> Info;
info({_, Info, _Chars}) -> Info.

%% This function might seem useless, since it "doesn't do anything",
%% but in fact it gives us two guarantees:
%% - thanks to Gradualizer it provides compile-time warnings if we build an invalid term_()
%% - it fails fast (aka crashes) at runtime if we try to build an invalid term_()
-spec term_(term_()) -> term_().
term_(T) ->
    case T of
        {true, _} -> T;
        %{false, _} -> T;
        {if_, _, _, _, _} -> T;
        {case_, _, _, _} -> T;
        {tag, _, _, _, _} -> T;
        {var, _, _, _} -> T;
        {abs, _, _, _, _} -> T;
        {app, _, _, _} -> T;
        {let_, _, _, _, _} -> T;
        {fix, _, _} -> T;
        {string, _, _} -> T;
        {unit, _} -> T;
        {ascribe, _, _, _} -> T;
        {proj, _, _, _} -> T;
        {record, _, _} -> T;
        {float, _, _} -> T;
        {timesfloat, _, _, _} -> T;
        {zero, _} -> T;
        {succ, _, _} -> T;
        {pred, _, _} -> T;
        {is_zero, _, _} -> T;
        {inert, _, _} -> T
    end.

-spec binding(binding()) -> binding().
binding(B) ->
    case B of
        name_bind -> B;
        ty_var_bind -> B;
        {var_bind, _} -> B;
        {tm_abb_bind, _, _} -> B;
        {ty_abb_bind, _} -> B
    end.

-spec command(command()) -> command().
command(C) ->
    case C of
        {eval, _, _} -> C;
        {bind, _, _, _} -> C
    end.

%%.

-spec format_binding_type(context(), binding()) -> io_lib:chars().
%-spec format_binding_type(context(), binding()) -> string().
format_binding_type(Ctx, B) ->
    case B of
        name_bind -> "";
        ty_var_bind -> "";
        {var_bind, TyT} ->
            io_lib:format(": ~ts", [zxcqwe]);
        {tm_abb_bind, T, MaybeTyT} ->
            case MaybeTyT of
                none -> [": ", "asdzxc"];
                TyT -> [": ", "qwe123"]
            end;
        {ty_abb_bind, _} -> ":: *"
    end.

Results:

$ find bin -name gradualizer.\*
bin/gradualizer.upstream-master
bin/gradualizer.erszcz-gradient
bin/gradualizer.erszcz-master
$ for GRADUALIZER in $(find bin -name gradualizer.\*); do ($GRADUALIZER --version; $GRADUALIZER syntax_example.erl) | tee $(basename $GRADUALIZER).log; echo; done
Gradualizer v0.1.3-108-g5be0f94
syntax_example.erl: The clause on line 5 at column 1 cannot be reached
syntax_example.erl: The pattern [_ | Haystack] on line 9 at column 3 does not have type:
[]
syntax_example.erl: The clause on line 15 at column 1 cannot be reached
syntax_example.erl: Nonexhaustive patterns on line 84 at column 9
Example values which are not covered:
	{id, []}
syntax_example.erl: Nonexhaustive patterns on line 108 at column 9
Example values which are not covered:
	{false, {0, 0}}

Gradualizer v0.1.3-117-g26acc93
syntax_example.erl: The clause on line 5 at column 1 cannot be reached
syntax_example.erl: The pattern [_ | Haystack] on line 9 at column 3 does not have type:
[]
syntax_example.erl: The clause on line 15 at column 1 cannot be reached
syntax_example.erl: Nonexhaustive patterns on line 84 at column 9
Example values which are not covered:
	{id, []}
syntax_example.erl: Nonexhaustive patterns on line 108 at column 9
Example values which are not covered:
	{false, {0, 0}}

Gradualizer v0.1.3-150-gef2dbb7
syntax_example.erl: Nonexhaustive patterns on line 84 at column 9
Example values which are not covered:
	{id, []}
syntax_example.erl: Nonexhaustive patterns on line 108 at column 9
Example values which are not covered:
	{false, {0, 0}}
syntax_example.erl: Timeout checking function format_binding_type/2 on line 153 at column 1
This is most likely a bug in Gradualizer.
Please report it at https://github.com/josefs/Gradualizer/issues

[zuiderkwast]

If this would be part of the standard library (as it is in Elixir) I'd be fine using it. Porting it and including it here seems like lots of added complexity though. Isn't it enough to use spawn_link or spawn_monitor and set a timeout?

%% Pseudo-code
TypecheckerPid = spawn_link(fun () -> type_check(Froms, self()) end),
receive
    {typechecker_done, Result} -> Result;
after Timeout ->
    kill(TypecheckerPid),
    {timeout, Forms)
end.

[erszcz]

It worked pretty well for me, but we now have a hand rolled timeout/3 if you prefer 🤷‍♂️

[erszcz]

@zuiderkwast you must've got some sixth sense 😆 It turned out the task.erl would return with a timeout, so other forms would be checked and reported, but at the same time the async task would go rogue and hog the CPU in an infinite loop anyway. I've now tested in ErlangLS with the hand-rolled spawn_monitor and timeout and the CPU is way less busy 👍

[erszcz]

@zuiderkwast This is ready with the fix you suggested. Do you have any further comments?

[zuiderkwast]

I think {timeout, Form} would be enough, to keep the error format simpler.