Skip to content

Commit

Permalink
Fix/bugfixes (#25)
Browse files Browse the repository at this point in the history
* Fix issue with typer not inferring the type of all functions

* Temporary fix for dialyzer API change

* Minor change in how file paths are managed

* Unzip modules for peer nodes

* Remove unnecessary comments

* Update README

* Make module names unique to avoid namespace collisions
  • Loading branch information
EarlPitts authored Mar 11, 2024
1 parent b33fe40 commit 7b3f4a0
Show file tree
Hide file tree
Showing 11 changed files with 117 additions and 66 deletions.
4 changes: 2 additions & 2 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -19,15 +19,15 @@ clean:

test: FORCE
erlc ${TEST_COMPILE_OPTIONS} -I include -o ${TARGET_DIR} src/check_equiv.erl
erlc ${TEST_COMPILE_OPTIONS} -I include -o ${TARGET_DIR} src/utils.erl
erlc ${TEST_COMPILE_OPTIONS} -I include -o ${TARGET_DIR} src/equivchecker_utils.erl
erlc ${TEST_COMPILE_OPTIONS} -I include -o ${TARGET_DIR} src/typing.erl
erlc ${TEST_COMPILE_OPTIONS} -I include -o ${TARGET_DIR} src/slicing.erl
erlc ${TEST_COMPILE_OPTIONS} -I include -o ${TARGET_DIR} src/functions.erl
erlc ${TEST_COMPILE_OPTIONS} -I include -o ${TARGET_DIR} test/scoping_tests.erl
erlc ${TEST_COMPILE_OPTIONS} -I include -o ${TARGET_DIR} test/typing_tests.erl
erlc ${TEST_COMPILE_OPTIONS} -I include -o ${TARGET_DIR} src/config.erl
erlc ${TEST_COMPILE_OPTIONS} -I include -o ${TARGET_DIR} src/diff.erl
erlc ${TEST_COMPILE_OPTIONS} -I include -o ${TARGET_DIR} src/testing.erl
erlc ${TEST_COMPILE_OPTIONS} -I include -o ${TARGET_DIR} src/equivchecker_testing.erl
erlc ${TEST_COMPILE_OPTIONS} -I include -o ${TARGET_DIR} src/repo.erl
erlc ${TEST_COMPILE_OPTIONS} -I include -o ${TARGET_DIR} src/cli.erl
erl -eval 'scoping_tests:test(), typing_tests:test(), init:stop()' -noshell
Expand Down
5 changes: 5 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -44,3 +44,8 @@ It's possible to get the output formatted as JSON:
Statistical information about the tests can be generated with `-s` or `--statistics`:

`$ equivchecker --statistics`

## Acknowledgments

We would like to thank the [Erlang Ecosystem Foundation](https://erlef.org/) for generously funding the development of this project.
Their support has been invaluable and has allowed us to bring this project to life.
78 changes: 55 additions & 23 deletions include/dialyzer.hrl
Original file line number Diff line number Diff line change
Expand Up @@ -33,44 +33,46 @@
%% Warning classification
%%--------------------------------------------------------------------

-define(WARN_RETURN_NO_RETURN, warn_return_no_exit).
-define(WARN_RETURN_ONLY_EXIT, warn_return_only_exit).
-define(WARN_NOT_CALLED, warn_not_called).
-define(WARN_NON_PROPER_LIST, warn_non_proper_list).
-define(WARN_FUN_APP, warn_fun_app).
-define(WARN_MATCHING, warn_matching).
-define(WARN_OPAQUE, warn_opaque).
-define(WARN_FAILING_CALL, warn_failing_call).
-define(WARN_BEHAVIOUR, warn_behaviour).
-define(WARN_BIN_CONSTRUCTION, warn_bin_construction).
-define(WARN_CONTRACT_TYPES, warn_contract_types).
-define(WARN_CONTRACT_SYNTAX, warn_contract_syntax).
-define(WARN_CALLGRAPH, warn_callgraph).
-define(WARN_CONTRACT_EXTRA_RETURN, warn_contract_extra_return).
-define(WARN_CONTRACT_MISSING_RETURN, warn_contract_missing_return).
-define(WARN_CONTRACT_NOT_EQUAL, warn_contract_not_equal).
-define(WARN_CONTRACT_RANGE, warn_contract_range).
-define(WARN_CONTRACT_SUBTYPE, warn_contract_subtype).
-define(WARN_CONTRACT_MISSING_RETURN, warn_contract_missing_return).
-define(WARN_CONTRACT_SUPERTYPE, warn_contract_supertype).
-define(WARN_CONTRACT_EXTRA_RETURN, warn_contract_extra_return).
-define(WARN_CONTRACT_RANGE, warn_contract_range).
-define(WARN_CALLGRAPH, warn_callgraph).
-define(WARN_UNMATCHED_RETURN, warn_umatched_return).
-define(WARN_BEHAVIOUR, warn_behaviour).
-define(WARN_CONTRACT_SYNTAX, warn_contract_syntax).
-define(WARN_CONTRACT_TYPES, warn_contract_types).
-define(WARN_FAILING_CALL, warn_failing_call).
-define(WARN_FUN_APP, warn_fun_app).
-define(WARN_MAP_CONSTRUCTION, warn_map_construction).
-define(WARN_MATCHING, warn_matching).
-define(WARN_NON_PROPER_LIST, warn_non_proper_list).
-define(WARN_NOT_CALLED, warn_not_called).
-define(WARN_OPAQUE, warn_opaque).
-define(WARN_OVERLAPPING_CONTRACT, warn_overlapping_contract).
-define(WARN_RETURN_NO_RETURN, warn_return_no_exit).
-define(WARN_RETURN_ONLY_EXIT, warn_return_only_exit).
-define(WARN_UNDEFINED_CALLBACK, warn_undefined_callbacks).
-define(WARN_UNKNOWN, warn_unknown).
-define(WARN_MAP_CONSTRUCTION, warn_map_construction).
-define(WARN_UNMATCHED_RETURN, warn_umatched_return).

%%
%% The following type has double role:
%% 1. It is the set of warnings that will be collected.
%% 2. It is also the set of tags for warnings that will be returned.
%%
-type dial_warn_tag() :: ?WARN_BEHAVIOUR | ?WARN_BIN_CONSTRUCTION
| ?WARN_CALLGRAPH | ?WARN_CONTRACT_NOT_EQUAL
| ?WARN_CALLGRAPH | ?WARN_CONTRACT_EXTRA_RETURN
| ?WARN_CONTRACT_MISSING_RETURN | ?WARN_CONTRACT_NOT_EQUAL
| ?WARN_CONTRACT_RANGE | ?WARN_CONTRACT_SUBTYPE
| ?WARN_CONTRACT_SUPERTYPE | ?WARN_CONTRACT_SYNTAX
| ?WARN_CONTRACT_TYPES | ?WARN_FAILING_CALL
| ?WARN_FUN_APP | ?WARN_MAP_CONSTRUCTION
| ?WARN_MATCHING | ?WARN_NON_PROPER_LIST
| ?WARN_NOT_CALLED | ?WARN_OPAQUE
| ?WARN_RETURN_NO_RETURN
| ?WARN_OVERLAPPING_CONTRACT | ?WARN_RETURN_NO_RETURN
| ?WARN_RETURN_ONLY_EXIT | ?WARN_UNDEFINED_CALLBACK
| ?WARN_UNKNOWN | ?WARN_UNMATCHED_RETURN.

Expand Down Expand Up @@ -108,7 +110,7 @@
%%--------------------------------------------------------------------

-type anal_type() :: 'succ_typings' | 'plt_build'.
-type anal_type1() :: anal_type() | 'plt_add' | 'plt_check' | 'plt_remove'.
-type anal_type1() :: anal_type() | 'plt_add' | 'plt_check' | 'plt_remove' | 'incremental'.
-type contr_constr() :: {'subtype', erl_types:erl_type(), erl_types:erl_type()}.
-type contract_pair() :: {erl_types:erl_type(), [contr_constr()]}.
-type dial_define() :: {atom(), term()}.
Expand All @@ -124,6 +126,7 @@
| 'no_return'
| 'no_undefined_callbacks'
| 'no_underspecs'
| 'no_unknown'
| 'no_unused'
| 'underspecs'
| 'unknown'
Expand All @@ -142,15 +145,23 @@
| {'plts', [FileName :: file:filename()]}
| {'include_dirs', [DirName :: file:filename()]}
| {'output_file', FileName :: file:filename()}
| {'metrics_file', FileName :: file:filename()}
| {'module_lookup_file', FileName :: file:filename()}
| {'output_plt', FileName :: file:filename()}
| {'check_plt', boolean()}
| {'analysis_type', 'succ_typings' |
'plt_add' |
'plt_build' |
'plt_check' |
'plt_remove'}
'plt_remove' |
'incremental'}
| {'warnings', [warn_option()]}
| {'get_warnings', boolean()}
| {'use_spec', boolean()}
| {'filename_opt', filename_opt()}
| {'callgraph_file', file:filename()}
| {'mod_deps_file', file:filename()}
| {'warning_files_rec', [DirName :: file:filename()]}
| {'error_location', error_location()}.
-type dial_options() :: [dial_option()].
-type filename_opt() :: 'basename' | 'fullpath'.
Expand All @@ -172,7 +183,21 @@
-define(ERROR_LOCATION, column).

-type doc_plt() :: 'undefined' | dialyzer_plt:plt().
-record(plt_info, {files :: [dialyzer_plt:file_md5()], mod_deps :: dict:dict()}).
-record(plt_info, {files :: [dialyzer_cplt:file_md5()],
mod_deps = dict:new() :: dialyzer_callgraph:mod_deps()}).
-record(iplt_info, {files :: [dialyzer_iplt:module_md5()],
mod_deps = dict:new() :: dialyzer_callgraph:mod_deps(),
warning_map = none :: 'none' | dialyzer_iplt:warning_map(),
legal_warnings = none :: none | dial_warn_tags()}).

-record(plt, {info :: ets:tid(), %% {mfa() | integer(), ret_args_types()}
types :: ets:tid(), %% {module(), erl_types:type_table()}
contracts :: ets:tid(), %% {mfa(), #contract{}}
callbacks :: ets:tid(), %% {module(),
%% [{mfa(),
%% dialyzer_contracts:file_contract()}]
exported_types :: ets:tid() %% {module(), sets:set()}
}).

-record(analysis, {analysis_pid :: pid() | 'undefined',
type = succ_typings :: anal_type(),
Expand All @@ -187,15 +212,18 @@
timing = false :: boolean() | 'debug',
timing_server = none :: dialyzer_timing:timing_server(),
callgraph_file = "" :: file:filename(),
mod_deps_file = "" :: file:filename(),
solvers :: [solver()]}).

-record(options, {files = [] :: [file:filename()],
files_rec = [] :: [file:filename()],
warning_files = [] :: [file:filename()],
warning_files_rec = [] :: [file:filename()],
analysis_type = succ_typings :: anal_type1(),
timing = false :: boolean() | 'debug',
defines = [] :: [dial_define()],
from = byte_code :: start_from(),
get_warnings = maybe :: boolean() | 'maybe',
get_warnings = 'maybe' :: boolean() | 'maybe',
init_plts = [] :: [file:filename()],
include_dirs = [] :: [file:filename()],
output_plt = none :: 'none' | file:filename(),
Expand All @@ -208,14 +236,18 @@
filename_opt = basename :: filename_opt(),
indent_opt = ?INDENT_OPT :: iopt(),
callgraph_file = "" :: file:filename(),
mod_deps_file = "" :: file:filename(),
check_plt = true :: boolean(),
error_location = ?ERROR_LOCATION :: error_location(),
metrics_file = none :: none | file:filename(),
module_lookup_file = none :: none | file:filename(),
solvers = [] :: [solver()]}).

-record(contract, {contracts = [] :: [contract_pair()],
args = [] :: [erl_types:erl_type()],
forms = [] :: [{_, _}]}).


%%--------------------------------------------------------------------

-define(timing(Server, Msg, Var, Expr),
Expand Down
19 changes: 16 additions & 3 deletions src/check_equiv.erl
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,17 @@ compile(Modules, DirName, Seed) ->
])
end, Modules).

% This is a hack, see https://github.com/harp-project/EquivcheckEr/issues/26 for details
unzip_modules() ->
{ok, [_,_,_,{archive,Archive}]} = escript:extract(escript:script_name(),[]),
{ok, Files} = zip:unzip(Archive,[memory]),
{_, Bin} = lists:keyfind("equivchecker/ebin/equivchecker_testing.beam", 1, Files),
{_, Bin2} = lists:keyfind("equivchecker/ebin/equivchecker_utils.beam", 1, Files),
file:write_file(filename:join([?ORIGINAL_BIN_FOLDER, "equivchecker_testing.beam"]), Bin),
file:write_file(filename:join([?REFACTORED_BIN_FOLDER, "equivchecker_testing.beam"]), Bin),
file:write_file(filename:join([?ORIGINAL_BIN_FOLDER, "equivchecker_utils.beam"]), Bin2),
file:write_file(filename:join([?REFACTORED_BIN_FOLDER, "equivchecker_utils.beam"]), Bin2).

start_nodes() ->
% TODO Handle error, use other port if its already used
{_, Orig, _} = peer:start(#{name => orig, connection => 33001, args => ["-pa", ?ORIGINAL_BIN_FOLDER]}),
Expand All @@ -33,7 +44,7 @@ stop_nodes(Orig, Refac) ->
% the token list and AST for each
-spec read_sources(filename()) -> {filename(), file_info()}.
read_sources(FileName) ->
Source = utils:read(FileName),
Source = equivchecker_utils:read(FileName),
{_, Tokens, _} = erl_scan:string(Source),
{ok, AST} = epp_dodger:quick_parse_file(FileName),

Expand All @@ -45,7 +56,7 @@ get_typeinfo(Dir) ->

check_equiv(OrigDir, RefacDir) ->
Configs = config:load_config(),
% typing:ensure_plt(Configs),
typing:ensure_plt(Configs),

DiffOutput = os:cmd("diff -x '.git' -u0 -br " ++ OrigDir ++ " " ++ RefacDir),
Diffs = diff:diff(DiffOutput),
Expand Down Expand Up @@ -79,13 +90,15 @@ check_equiv(OrigDir, RefacDir) ->
compile(OrigFiles, ?ORIGINAL_BIN_FOLDER, Seed),
compile(RefacFiles, ?REFACTORED_BIN_FOLDER, Seed),

unzip_modules(),

{OrigNode, RefacNode} = start_nodes(),

% This is needed because PropEr needs the source for constructing the generator
{ok, Dir} = file:get_cwd(),
file:set_cwd(OrigDir),

Result = testing:run_tests(FunsToTest, OrigNode, RefacNode, Types, CallGraph),
Result = equivchecker_testing:run_tests(FunsToTest, OrigNode, RefacNode, Types, CallGraph),

file:set_cwd(Dir),
stop_nodes(OrigNode, RefacNode),
Expand Down
4 changes: 2 additions & 2 deletions src/cli.erl
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,7 @@ show_result(Result, false, false) ->
Formatted = format_results(Result,false),
io:format("Results: ~p~n", [Formatted]);
show_result(Result, false, true) ->
{FailCounts, Average} = utils:statistics(),
{FailCounts, Average} = equivchecker_utils:statistics(),
Formatted = format_results(Result,false),
io:format("Results: ~p~n", [Formatted]),
io:format("Number of functions that failed: ~p~n", [length(FailCounts)]),
Expand All @@ -100,7 +100,7 @@ show_result(Result, true, false) ->
Formatted = format_results(Result,true),
io:format("~s\n", [jsone:encode(Formatted,[{indent, 2}, {space, 1}])]);
show_result(Result, true, true) ->
{FailCounts, Average} = utils:statistics(),
{FailCounts, Average} = equivchecker_utils:statistics(),
Stats = #{failed_count => length(FailCounts), average_test_count => Average},
Output = #{statistics => Stats, results => format_results(Result,true)},
io:format("~s\n", [jsone:encode(Output,[{indent, 2}, {space, 1}])]).
Expand Down
8 changes: 3 additions & 5 deletions src/config.erl
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@

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

-define(CONF_DEFAULT_LOC, "/equivcheckrc").
-define(CONF_DEFAULT_LOC, "equivcheckrc").
-define(SEPARATOR, " "). % Separates the config key from the value in the config file

-spec update_config(config(), string(), string()) -> config().
Expand Down Expand Up @@ -41,8 +41,7 @@ serialize(Config) ->

-spec load_config() -> config().
load_config() -> % TODO non-default location as argument
ConfigDir = os:getenv("XDG_CONFIG_HOME"),
FileName = ConfigDir ++ ?CONF_DEFAULT_LOC,
FileName = filename:basedir(user_config, ?CONF_DEFAULT_LOC),
case filelib:is_file(FileName) of
true ->
{_, File} = file:read_file(FileName),
Expand All @@ -53,6 +52,5 @@ load_config() -> % TODO non-default location as argument

-spec save_config(config()) -> atom().
save_config(Config) ->
ConfigDir = os:getenv("XDG_CONFIG_HOME"),
FileName = ConfigDir ++ ?CONF_DEFAULT_LOC,
FileName = filename:basedir(user_config, ?CONF_DEFAULT_LOC),
file:write_file(FileName, binary:list_to_bin(serialize(Config))).
2 changes: 1 addition & 1 deletion src/diff.erl
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,7 @@ parse_diff(DiffStr) ->
extract_file(DiffLine) ->
Options = [global, {capture, [1,2], list}],
{match, [[OrigFile, RefacFile]]} = re:run(DiffLine, ".*?(/.*?\.erl).*?(/.*?\.erl)", Options),
utils:common_filename_postfix(OrigFile, RefacFile).
equivchecker_utils:common_filename_postfix(OrigFile, RefacFile).

% Checks if the given file in the diff output is erlang source code
-spec is_erl_source([diff_line()]) -> boolean().
Expand Down
20 changes: 10 additions & 10 deletions src/testing.erl → src/equivchecker_testing.erl
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(testing).
-module(equivchecker_testing).

-type type() :: string().

Expand All @@ -19,15 +19,15 @@ run_tests([], _, _, _, _, Results) ->
run_tests(Functions, OrigNode, RefacNode, Types, CallGraph, Results) ->
% proper:quickchek/2 stops the server, so it has to be started every time
proper_typeserver:start(),
ProperOpts = [long_result, {on_output, fun(X,Y) -> utils:count_tests(X,Y) end}],
ProperOpts = [long_result, {on_output, fun(X,Y) -> equivchecker_utils:count_tests(X,Y) end}],

% Convert type information to PropEr type
FunctionsTyped = lists:map(fun({FileName, {M,F,A}, ArgTypes}) -> {FileName, {M, F, A}, convert_type(FileName, M, ArgTypes)} end, Functions),

% A result is a tuple: {Module, Function, Counterexample}
% If no counterexample is found, the third value is 'true' instead
lists:map(fun(Function) ->
spawn(testing, test_function, [Function, OrigNode, RefacNode, ProperOpts, self()])
spawn(equivchecker_testing, test_function, [Function, OrigNode, RefacNode, ProperOpts, self()])
end, FunctionsTyped),

Res = collect_results(length(FunctionsTyped), []),
Expand All @@ -48,17 +48,17 @@ collect_results(Num, Res) ->

% -spec eval_func(pid(), atom(), atom(), [term()]) -> {atom(), term()}.
eval_func(M, F, A, Pid) ->
L = utils:start_capture(Pid),
L = equivchecker_utils:start_capture(Pid),
RetVal = try erlang:apply(M, F, A) of
Val -> {normal, Val}
catch
error:Error -> error
end,
Pid ! {self(), RetVal},
utils:stop_capture(L).
equivchecker_utils:stop_capture(L).

eval_proc(M, F, A) ->
Pid = spawn(testing, eval_func, [M, F, A, self()]),
Pid = spawn(equivchecker_testing, eval_func, [M, F, A, self()]),
receive
{Pid, Res} -> Res
end,
Expand All @@ -78,11 +78,11 @@ get_messages(L) ->
% sends back the result to this process
-spec prop_same_output(pid(), pid(), atom(), atom(), [term()]) -> boolean().
prop_same_output(OrigNode, RefacNode, M, F, A) ->
{Val1,IO1} = peer:call(OrigNode, testing, eval_proc, [M, F, A], ?PEER_TIMEOUT),
{Val2,IO2} = peer:call(RefacNode, testing, eval_proc, [M, F, A], ?PEER_TIMEOUT),
{Val1,IO1} = peer:call(OrigNode, equivchecker_testing, eval_proc, [M, F, A], ?PEER_TIMEOUT),
{Val2,IO2} = peer:call(RefacNode, equivchecker_testing, eval_proc, [M, F, A], ?PEER_TIMEOUT),

Out1 = {Val1,utils:remove_pid(IO1)},
Out2 = {Val2,utils:remove_pid(IO2)},
Out1 = {Val1,equivchecker_utils:remove_pid(IO1)},
Out2 = {Val2,equivchecker_utils:remove_pid(IO2)},

Out1 =:= Out2.

Expand Down
6 changes: 3 additions & 3 deletions src/utils.erl → src/equivchecker_utils.erl
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
-module(utils).
-module(equivchecker_utils).

-compile(export_all).

Expand Down Expand Up @@ -77,7 +77,7 @@ dummy_group_leader() ->
-spec disable_output() -> pid().
disable_output() ->
Old = group_leader(),
New = spawn(utils, dummy_group_leader, []),
New = spawn(equivchecker_utils, dummy_group_leader, []),
group_leader(New, self()),
Old.

Expand All @@ -104,7 +104,7 @@ capture_group_leader(Pid) ->
-spec start_capture(pid()) -> {pid()}.
start_capture(Pid) ->
Old = group_leader(),
New = spawn(utils, capture_group_leader, [Pid]),
New = spawn(equivchecker_utils, capture_group_leader, [Pid]),
group_leader(New, self()),
Old.

Expand Down
Loading

0 comments on commit 7b3f4a0

Please sign in to comment.