Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Enable Dialyzer and ETC cross checks #429

Merged
merged 6 commits into from
Jul 14, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
deps
*.o
*.beam
*.erltypes
*.plt
/.dialyzer_plt
*~
Expand Down
10 changes: 9 additions & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -107,7 +107,7 @@ clean:
rm -rf bin/gradualizer ebin cover test/*.beam

.PHONY: tests eunit compile-tests cli-tests
tests: build_test_data eunit cli-tests
tests: check_name_clashes build_test_data eunit cli-tests

test_erls=$(wildcard test/*.erl)
test_beams=$(test_erls:test/%.erl=test/%.beam)
Expand Down Expand Up @@ -212,6 +212,14 @@ DIALYZER_OPTS ?= -Werror_handling -Wrace_conditions
dialyze: app $(DIALYZER_PLT)
dialyzer $(DIALYZER_OPTS) ebin

.PHONY: dialyze-tests
dialyze-tests: app $(DIALYZER_PLT)
dialyzer $(DIALYZER_OPTS) $(test_data_erls)

Comment on lines +215 to +218
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can we run this in CI to maintain expected results? I.e. to prevent name clashes from being introduced again.

Are there any dialyzer errors in the tests?

Copy link
Collaborator Author

@erszcz erszcz Jul 13, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm, we probably could, but the errors do not overlap completely, so we would need to come up with some should-pass/should-fail/known-problems mapping mechanism. I don't think we can run it just to detect name clashes, we would also have to check the error code and determine which is returned why.

Below is an interesting case:

-spec f1() -> boolean().
f1() ->
true andalso g1().
-spec g1() -> any().
g1() -> 3.

Dialyzer reports:

andalso_any.erl:5:2: Invalid type specification for function andalso_any:f1/0. The success typing is
          () -> 3

Whereas Gradualizer is fine with it, because any() is compatible with every other type. AFAIU a full-blown gradual typing system according to Siek and Taha would inject a dynamic check in such a place.

Dialyzer infers the type of an integer literal, but it couldn't do so if the value was not a literal.
Gradualizer just believes the spec, even with --infer, and checks against it, so it assumes everything is fine.

I imagine there are more cases like this, but haven't analysed all of them yet. The current summary is available at https://gist.github.com/erszcz/4d43a77464c87a514e71eecf2811af63#file-check-2022-07-13_170833-tsv.

Copy link
Collaborator

@zuiderkwast zuiderkwast Jul 13, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Interesting. Yes, dializer does a full inference, while gradualizer is silent on purpose in this case.

Regarding Siek & Taha: Since Erlang/BEAM is a dynamic language, there are already runtime checks for everything anyway. The runtime catches it and raises an exception such as badarg. The paper speaks about the case where a dynamic type is added to a statically language without runtime type checks. This is my interpretation anyway.

Could we check for unique module filenames in another way then? Just some simple shell script?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Since Erlang/BEAM is a dynamic language, there are already runtime checks for everything anyway.

I agree. However, I think the mentioned example shows unsoundness of the type system. Let's consider this (and the following) paragraph from https://papl.cs.brown.edu/2014/safety-soundness.html#%28part._type-soundness%29:

The central result we wish to have for a given type-system is called soundness. It says this. Suppose we are given an expression (or program) e. We type-check it and conclude that its type is t. When we run e, let us say we obtain the value v. Then v will also have type t.

In our case the type checker will pretend that f1() -> boolean(), but in fact it turns out to be f1() -> integer() upon evaluation.

Could we check for unique module filenames in another way then? Just some simple shell script?

I think we can use some find | sort | uniq magic to do it. I'll come up with something tomorrow.

Copy link
Collaborator

@zuiderkwast zuiderkwast Jul 14, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Are you saying Gradualizer (or any sound gradual type system) should insert an assertion to make sure g1() in your example above returns a boolean? This is to ensure we get a runtime type error rather than a value of the wrong type...? So f1 above is translated into something like this:

-spec f1() -> boolean(). 
f1() -> 
    true andalso (begin G1 = g1(), ?assert(is_boolean(G1)), G1 end).

This is interesting. I didn't think about it in this way before.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this is explained in a simple way in the introduction of Max S. New, Dustin Jamner, and Amal Ahmed. 2020. Graduality and Parametricity: Together Again for the First
Time. Proc. ACM Program. Lang. 4, POPL, Article 46 (January 2020), 32 pages. https://doi.org/10.1145/3371114

image

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Are you saying Gradualizer (or any sound gradual type system) should insert an assertion to make sure g1() in your example above returns a boolean?

I think so. The fragment you quote is aligned with what I remembered from the paper 👍

-spec f1() -> boolean(). 
f1() -> 
    true andalso (begin G1 = g1(), ?assert(is_boolean(G1)), G1 end).

So f1 above is translated into something like this [...]

Yes, more or less. Their paper didn't cover Erlang, obviously, and the semantics of the language start to matter at this point. I'd type the Erlang andalso as andalso(boolean(), any()) -> any() based on the below:

1> 3 andalso 5.
** exception error: bad argument: 3
2> false andalso 5.
false
3> true andalso 5.
5

So I think the inserted assertion, due to the spec we declare for f1, should enclose the application of andalso:

-spec f1() -> boolean(). 
f1() ->
  R = true andalso g1(),
  ?assert(is_boolean(R)),
  R.

However, I don't think we can consider this a goal for Gradualizer given it's not part of a compiler. Perhaps one day it could rewrite .beam files... but that's a far fetched goal. I think there are more tangible and important milestones before that.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@josefs What do you think about our conclusions above? The example functions f1 and g1...

However, I don't think we can consider this a goal for Gradualizer given it's not part of a compiler. Perhaps one day it could rewrite .beam files... but that's a far fetched goal.

True, but without this I don't believe we have soundness and the types can't really be trusted. I always regarded gradualizer an experiment. The next experiment could be "Gradual Erlang", a language which looks like Erlang and compiles to Erlang with assertions inserted....

Copy link
Collaborator Author

@erszcz erszcz Aug 11, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Interesting comment that A andalso B actually is syntactic sugar for case A of true -> B ... - erlang/otp#5456 (comment).

Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As you noted @zuiderkwast, inserting checks when the typechecker coerces to/from any() is referred to as "sound gradual typing" in the literature. My intention with Gradualizer was to refrain from doing it, simply because I thought that it would be too much work. Adding coercions has the advantage that runtime type errors would be reported earlier and in places that are often easier to understand.

In some implementations is required to insert these coercions because not doing so would lead to a crash/segfault/undefined behaviour. But since we're relying on executing things on top of BEAM we don't have such problems.

There are quite a few papers on measuring the cost of these coercions and there are example programs for which they are quite expensive. Those examples typically involve having any() embedded in some structure so that the coercions have to traverse the structure.

I don't have anything in principle against adding these kinds of coercions. But from an efficiency point of view it might be preferrable to have this not be the default behaviour and have a flag that enables it.

.PHONY: check_name_clashes
check_name_clashes:
test/check_name_clashes.sh

# DIALYZER_PLT is a variable understood directly by Dialyzer.
# Exit status 2 = warnings were emitted
$(DIALYZER_PLT):
Expand Down
26 changes: 26 additions & 0 deletions test/check_name_clashes.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
#!/usr/bin/env bash

#set -x

if [ x$(uname) == x"Darwin" ]; then
BASENAME=basename
else
BASENAME="basename -a"
fi

UNIQ=$(find test/should_pass test/should_fail test/known_problems/*/ -name \*.erl \
| xargs $BASENAME \
| sort \
| uniq -c \
| sort -n \
| tail -1)

COUNT=$(echo $UNIQ | awk '{print $1}')

if [ "$COUNT" == 1 ]; then
exit 0
else
echo "Name clash in tests:"
find test -name $(echo $UNIQ | awk '{print $2}')
exit 1
fi
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(guard_fail).
-module(guard_should_fail).

-compile([export_all, nowarn_export_all]).

Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(intersection_with_any_fail).
-module(intersection_with_any_should_fail).

-export([any_refined_using_guard/1,
var_as_pattern/1,
Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(rigid_type_variables).
-module(rigid_type_variables_fail).

-compile([export_all, nowarn_export_all]).

Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(rigid_type_variables).
-module(rigid_type_variables_pass).

-compile([export_all, nowarn_export_all]).

Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
-module(arith_op).
-module(arith_op_fail).

-export([failplus/1, faildivvar/1, faildivlit/1, failpositivedivision/1,
faildivprecise/1, failplusprecise/2, failminusprecisepos/2,
failminusnonneg/2, failminuspreciseneg/2,
Expand Down
2 changes: 1 addition & 1 deletion test/should_fail/bc.erl → test/should_fail/bc_fail.erl
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(bc).
-module(bc_fail).
-export([f/0, non_bin_expr/0, integer_signed_wrong/1]).

-spec f() -> binary().
Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(catch_expr).
-module(catch_expr_fail).

-export([foo/1]).

Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(covariant_map_keys).
-module(covariant_map_keys_fail).

-compile([nowarn_unused_function]).
-export([not_good/1]).
Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(intersection_with_any).
-module(intersection_with_any_fail).

-export([intersection_using_constraints/1]).

Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(list_infer).
-module(list_infer_fail).

-gradualizer(infer).
-export([f/0]).
Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(messaging).
-module(messaging_fail).

-export([server1/0, server2/0, server3/0, server4/0]).

Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(named_fun).
-module(named_fun_fail).

-export([bar/0, baz/1]).

Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(named_fun_infer).
-module(named_fun_infer_fail).

-gradualizer(infer).
-export([bar/0, sum/1]).
Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(operator_pattern).
-module(operator_pattern_fail).
-export([n/1, p/1]).

-spec n(non_neg_integer()) -> {}.
Expand Down
2 changes: 2 additions & 0 deletions test/should_fail/record_refinement_fail.erl
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,8 @@ one_field2(_, I) -> I.
-spec refined_field(#refined_field{}) -> #refined_field{f :: integer()}.
refined_field(R) -> R.

%% The refinement in the result type is not handled by Dialyzer - it will error out.
%% Comment it out if trying to run `make dialyze-tests'.
-spec refined_field2(#refined_field{}) -> #refined_field{f :: atom()}.
refined_field2(#refined_field{f = undefined}) -> #refined_field{f = 0};
refined_field2(R) -> R.
Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(record_wildcard).
-module(record_wildcard_fail).

-export([f/0, g/0]).

Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(send).
-module(send_fail).

-export([foo/2, bar/2]).

Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(shortcut_ops).
-module(shortcut_ops_fail).

-compile([export_all, nowarn_export_all]).

Expand Down
7 changes: 0 additions & 7 deletions test/should_fail/tuple_union.erl

This file was deleted.

5 changes: 5 additions & 0 deletions test/should_fail/tuple_union_fail.erl
Original file line number Diff line number Diff line change
@@ -1,7 +1,12 @@
-module(tuple_union_fail).

-export([f/0]).
-export([tuple_union/0]).

-spec f() -> {integer()} | {boolean()}.
f() ->
{apa}.

-spec tuple_union() -> {undefined, binary()} | {integer(), undefined}.
tuple_union() ->
{undefined, undefined}.
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(type_refinement).
-module(type_refinement_fail).
-export([guard_prevents_refinement/2, imprecision_prevents_refinement/2,
multi_pat_fail_1/2,
guard_prevents_refinement2/1,
Expand Down
2 changes: 1 addition & 1 deletion test/should_pass/bc.erl → test/should_pass/bc_pass.erl
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(bc).
-module(bc_pass).

-compile([export_all, nowarn_export_all]).

Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(catch_expr).
-module(catch_expr_pass).

-export([foo/1]).

Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(covariant_map_keys).
-module(covariant_map_keys_pass).

-compile([export_all, nowarn_export_all]).

Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(intersection).
-module(intersection_pass).

-compile([export_all, nowarn_export_all]).

Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(intersection_with_any).
-module(intersection_with_any_pass).

-compile([export_all, nowarn_export_all]).

Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(list_infer).
-module(list_infer_pass).

-gradualizer(infer).
-export([f/0]).
Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(messaging).
-module(messaging_pass).

-export([main/0, server/0, server1/0, server2/0, server3/0, server4/0]).

Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(named_fun_infer).
-module(named_fun_infer_pass).

-gradualizer(infer).
-export([atom_sum/1]).
Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(named_fun).
-module(named_fun_pass).

-export([fac/1, sum/1]).

Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(operator_pattern).
-module(operator_pattern_pass).

-compile([export_all, nowarn_export_all]).

Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(record_wildcard).
-module(record_wildcard_pass).

-export([f/0, g/0, h/1]).

Expand Down
5 changes: 3 additions & 2 deletions test/should_pass/records.erl
Original file line number Diff line number Diff line change
@@ -1,9 +1,10 @@
-module(records).

-export([f/0, g/1, h/0, i/0, j/0, k/0, l/0,
-export([f/0, f/1, g/1, h/0, i/0, j/0, k/0, l/0,
rec_field_subtype/1,
rec_index_subtype/0,
record_as_tuple/1]).
record_as_tuple/1,
nospec_update_bug/1]).

-record(r, {f1 :: atom(),
f2 = 1 :: integer()}).
Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(send).
-module(send_pass).

-export([foo/2, bar/2]).

Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(shortcut_ops).
-module(shortcut_ops_pass).

-compile([export_all, nowarn_export_all]).

Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(tuple_union).
-module(tuple_union_pass).

-export([f/0]).

Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(type_refinement).
-module(type_refinement_pass).

-compile([export_all, nowarn_export_all]).

Expand Down