cuter-testing / cuter

A concolic testing tool for the Erlang functional programming language.
GNU General Public License v3.0
210 stars 20 forks source link

Defining a function with map matches makes all functions of a module uncheckable. #91

Open ferd opened 7 years ago

ferd commented 7 years ago

Try the following module definition:

-module(fail).
-compile(export_all).

id(X) -> X.

%% Remove this function and all works
mapfun(#{year := Y, month := M, day := D}) ->
    #{year => Y, month => M, day => D}.

Then run the following:

1> c(fail, [debug_info]).
{ok,fail}
2> cuter:run(fail, id, [1]).
Testing fail:id/1 ...
fail:id(1)

=== Inputs That Lead to Runtime Errors ===
#1 fail:id(1)
[[1]]

If the function mapfun is removed, everything passes.

If the function mapfun is instead re-defined as:

  mapfun(#{k := _}) ->
      #{}.

The test for fail:id(1) works, but still errors out with:

62> cuter:run(fail, id, [1]).
Testing fail:id/1 ...
Proccess <0.733.0> exited with {{case_clause,
                                 {ok,
                                  {bad_constructor_pattern,
                                   {c_map,
                                    [7,{file,"fail.erl"}],
                                    {c_literal,[],#{}},
                                    [{c_map_pair,
                                      [7,{file,"fail.erl"}],
                                      {c_literal,[],exact},
                                      {c_literal,[7,{file,"fail.erl"}],k},
                                      {c_var,[],cor2}}],
                                    true}}}},
                                [{cuter_cerl,load,4,
                                  [{file,"src/cuter_cerl.erl"},{line,133}]},
                                 {cuter_codeserver,load_mod,2,
                                  [{file,"src/cuter_codeserver.erl"},
                                   {line,367}]},
                                 {cuter_codeserver,handle_call,3,
                                  [{file,"src/cuter_codeserver.erl"},
                                   {line,213}]},
                                 {gen_server,try_handle_call,4,
                                  [{file,"gen_server.erl"},{line,629}]},
                                 {gen_server,handle_msg,5,
                                  [{file,"gen_server.erl"},{line,661}]},
                                 {proc_lib,init_p_do_apply,3,
                                  [{file,"proc_lib.erl"},{line,240}]}]}
Proccess <0.735.0> exited with {{badmatch,[]},
                                [{cuter_analyzer,get_mapping,1,
                                     [{file,"src/cuter_analyzer.erl"},
                                      {line,62}]},
                                 {cuter_poller,retrieve_info,3,
                                     [{file,"src/cuter_poller.erl"},
                                      {line,82}]},
                                 {cuter_poller,loop,1,
                                     [{file,"src/cuter_poller.erl"},
                                      {line,47}]}]}

No Runtime Errors Occured
** exception exit: {noproc,{gen_server,call,[<0.733.0>,get_logs]}}
     in function  gen_server:call/2 (gen_server.erl, line 204)
     in call from cuter:stop_and_report/1 (src/cuter.erl, line 163)

System information:

Operating System: x86_64-unknown-linux-gnu
ERTS: Erlang/OTP 18 [erts-7.1] [source] [64-bit] [smp:8:4] [async-threads:0] [hipe] [kernel-poll:false]
1> cuter:module_info().
[{module,cuter},
 {exports,[{run,3},
           {run,4},
           {run,5},
           {module_info,0},
           {module_info,1}]},
 {attributes,[{vsn,[57691554190785165960347122628729196863]}]},
 {compile,[{options,[{d,'PRIV',
                        "/home/ferd/code/software/cuter/priv"},
                     {d,'PYTHON_PATH',"python"},
                     {d,'EBIN',"/home/ferd/code/software/cuter/ebin"},
                     {outdir,"/home/ferd/code/software/cuter/ebin"},
                     {i,"/home/ferd/code/software/cuter/include"},
                     warnings_as_errors,warn_missing_spec,warn_unused_import,
                     warn_exported_vars,debug_info]},
           {version,"6.0.1"},
           {time,{2016,9,17,3,56,32}},
           {source,"/home/ferd/code/software/cuter/src/cuter.erl"}]},
 {native,false},
 {md5,<<43,102,253,58,153,205,221,74,51,38,241,200,168,7,
        81,63>>}]
kostis commented 7 years ago

Thanks for trying out CutEr and for the bug report @ferd. I can confirm what you report (using 19.0).

As mentioned in my talks, CutEr does not support maps yet (perhaps we should also mention this in the top-level README?). Still, this behavior you show is certainly weird. I suspect something breaks in the Core Erlang passes, due to the presence of the maps, and this error is not caught as a compilation/annotation error of CutEr but is reported as an execution error. Last week we saw something similar (with reporting error for the concolic execution when execution reaches bitstring primops that CutEr currently does not support) and fixing that issue is high on the TODO list. Now we have one more example. Thanks.

kostis commented 7 years ago

Granted that CutEr should report these failures in a better way, but it seems that the root of this issue is related to the fact that the Core Erlang pattern matching compilation fails for modules that contain maps

Erlang/OTP 19 [erts-8.0] [source] [64-bit] [smp:64:64] [async-threads:10] [hipe] [kernel-poll:false]

Eshell V8.0  (abort with ^G)
1> c(fail, [debug_info]).
{ok,fail}
2> c(fail, [debug_info, {core_transform, cerl_pmatch}]).
fail.erl: error in core transform 'cerl_pmatch': {{case_clause,map},
                                        [{cerl_pmatch,expr,2,[]},
                                         {cerl_pmatch,expr,2,[]},
                                         {cerl_pmatch,expr,2,[]},
                                         {cerl_pmatch,expr,2,[]},
                                         {cerl_pmatch,'-expr/2-lc$^0/1-3-',2,
                                          []},
                                         {cerl_pmatch,'-expr/2-lc$^0/1-3-',2,
                                          []},
                                         {cerl_pmatch,expr,2,[]},
                                         {cerl_pmatch,core_transform,2,[]}]}
error

We will try to fix this. In the meantime you may want to use the CutEr option --disable-pmatch for such modules. (However, be aware that the concolic execution will be significantly slower.)

$ cuter fail id '[42]' -r
Compiling fail.erl ... OK
Testing fail:id/1 ...
fail:id(42)

=== Inputs That Lead to Runtime Errors ===
#1 fail:id(42)
$ cuter fail id '[42]' -r --disable-pmatch
Compiling fail.erl ... OK
Testing fail:id/1 ...
.
No Runtime Errors Occured
ioolkos commented 7 years ago

Hi, is there any updates on this issue? I guess --disable-pmatch is still the only way forward here? Thanks for your awesome software & effort! :)

aggelgian commented 7 years ago

Hello @ioolkos,

Yes, this is still the only option. We are currently finishing up on some tasks regarding the support for recursive types in type specifications.

Since there is interest in the maps functionality, we'll discuss with @kostis to re-prioritize this issue. We'll let you know soon! :)

ioolkos commented 7 years ago

Great to hear! thanks :)