cuter-testing / cuter Goto Github PK

View Code? Open in Web Editor NEW

210.0 210.0 20.0 2.19 MB

A concolic testing tool for the Erlang functional programming language.

License: GNU General Public License v3.0

Python 5.15% Erlang 94.36% Shell 0.06% Makefile 0.22% M4 0.23%

cuter's People

Contributors

Stargazers

Watchers

Forkers

chinnurtb zitsi baha linearregression zv huiqing mcherep anton-b margnus1 mazzespazze ndcroos serperu puzza007 fenollp uldza josefha theotsal ioolkos arachmani neoaggelos laplacekorea

cuter's Issues

Apply function spec to function parameters

Properly encode the type of a function parameter to JSON.
The solver should apply this spec to the parameter.

Support bs_init_writable

This is mentioned here:
https://github.com/aggelgian/cuter/blob/6723f5e67de4d309aa198fd44b84e530cdb961de/src/cuter_eval.erl#L677

Support 'erlang:list_to_integer/1'

Here's an example.

-spec average(A :: string(), B :: string()) -> number().
average(A, B) ->
  A_Int = list_to_integer(A),
  B_Int = list_to_integer(B),
  A_Int+B_Int/2.

Extend term encoding in Z3 to include funs

Extend the current encoding of Erlang terms and add funs.
Add some tests for solving models with funs and recover their values.

This does not involve plugging this representation into the actual solving process.
This is left for another issue.

Minimize the JSON representation of funs

The current representation of funs as JSON strings generates quite large strings. Try to optimize it.

Surprising unsupported MFA

I ran:
cuter hipe_icode_primops type '[unsafe_bor]'
and at the end of the concolic execution, CutEr reported:

=== UNSUPPORTED MFAS ===
erlang:is_function/2
cuter_erlang:unsupported_lt/2

The second of them, somehow seems weird to report here...

In looking at the code (https://github.com/aggelgian/cuter/blob/master/src/cuter_erlang.erl#L580), I also noticed that the spec of this function also mentions bitstring() as a type for its arguments, even though CutEr currently supports bitstrings. Create a lt_bitstring/2?

Pretty print funs

Pretty print funs where needed during the execution.

Support bnot/1

CutEr crash when testing github.com/duomark/epocxy cxy_synch

cuter:run(cxy_synch, before_task, [3, fun() -> io:format("~p", [4]) end]).
Testing cxy_synch:before_task/2 ...
444Proccess <0.79.0> exited with {{badmatch,
{{value,
{{15,"#Ref<0.0.0.419>"},
{file_descriptor,prim_file,
{#Port<0.1641>,315360760}}}},
{[],[]}}},
[{cuter_merger,merge_next_file_from_waiting,1,
[{file,"src/cuter_merger.erl"},{line,210}]},
{cuter_analyzer,process_raw_execution_info,1,
[{file,"src/cuter_analyzer.erl"},{line,85}]},
{cuter_poller,retrieve_info,3,
[{file,"src/cuter_poller.erl"},{line,86}]},
{cuter_poller,loop,1,
[{file,"src/cuter_poller.erl"},{line,47}]}]}

No Runtime Errors Occured

=== BIFs Currently without Symbolic Interpretation ===
erlang:process_flag/2
erlang:self/0
erlang:make_ref/0
[]

https://github.com/duomark/epocxy/blob/master/src/cxy_synch.erl#L44-L46

Add the term representation with support for funs to the solving process

This requires feature #34 to be implemented.

The goal is to use the representation created at #34 and plug in the actual solver process.
This requires

CutEr to log function applications with funs.
Compile funs before using them for running testcases.

Bug in Z3 encoding

When testing

-module(foo).
-export([g/1]).

-spec g(integer() | [integer()]) -> <<>>.
g(42) -> error(bug);
g([]) -> <<>>;
g(L) -> g(tl(L)).

the following error occurs

aggelgian@lambda:~/git-repos/cuter$ cuter foo g '[1]' -r
Compiling foo.erl ... OK
Testing foo:g/1 ...
foo:g(1)

foo:g(42)
.[SOLVER ERROR] {"python -u /home/aggelgian/git-repos/cuter/priv/cuter_interface.py",
                [{{'__s',"0.0.4.40"},1}],
                "/home/aggelgian/git-repos/cuter/temp/execexec1/run.trace",3}
Proccess <0.35.0> exited with {{solving,
                                   {unexpected_info,
                                       {'EXIT',#Port<0.1636>,normal}}},
                               {gen_fsm,sync_send_event,
                                   [<0.46.0>,check_model,500000]}}

Support `erlang:bxor/2`

Support `erlang:get/0` and `erlang:get/1`

(Process dictionary)

Support 'erlang:phash/2', 'erlang:trunc/1', 'erlang:get/1' and 'erlang:put/2'

Code example

-spec test_02(Proplist :: [{atom(), atom()}]) -> atom().
test_02([]) ->
  ok;
test_02(Proplist) ->
  Keys = proplists:get_keys(Proplist),
  Index = random:uniform(length(Keys)),
  lists:nth(Index, Keys).

=== BIFs Currently without Symbolic Interpretation ===
erlang:phash/2
erlang:trunc/1
erlang:get/1
erlang:put/2

Refactor functional tests

Refactor functional tests and add the option to validate the errors instead of just checking them against a stored execution trace.

Use -pa and -pz paths to the compilation of erl files

When invoking the cuter script the paths specified with -pa and -pz are not also used when compiling the erl file.

Set up the file structure for the smt parser

Restructure the directory doc/smt2 for the development of the SMT parser.

Update tests to work for Z3 4.4.2

Some unit and functional tests fail when using Z3 v4.4.2 instead of v4.4.1.

The model in those testcases is too general and the problem is that solver chooses another valid solution.
The tests need to be made aware of the version of the underlying solver.

[cuter script]: be able to analyze .beam files in the code path

Currently, the cuter script does not seem to know about debug-compiled modules that are in the standard code path:

$ cuter lists last '[[1,2]]'
Cannot locate lists.erl ...

This is a bit annoying. It obviously does not need to re-compile the module or refuse to perform the concolic execution of this function. Instead, it should just load the .beam file and go ahead and do it.

This should be fixed. Incidentally, it should do the same with any .beam file that is, or is specified using the -pa option (#14) in the code path.

Support `erlang:phash/2`

Pretty print trace files

We need a way to pretty print trace files with constraints.

To that end, I need to update cuter_print.py and add some guidance on how to use it in the wiki.

Bug when testing mochinjson2

I get the error

[SOLVER ERROR] {"python -u /home/aggelgian/git-repos/cuter/priv/cuter_interface.py",
                [{{'__s',"0.0.1.15586"},[false,<<>>]}],
                "/home/aggelgian/git-repos/cuter/temp/execexec161/run.trace",
                28}
Proccess <0.38.0> exited with {{solving,
                                   {unexpected_info,
                                       {'EXIT',#Port<0.3056>,normal}}},
                               {gen_fsm,sync_send_event,
                                   [<0.1010.0>,check_model,500000]}}

while running

cuter mochijson2 encode '[[]]' -s 4 -p 4

It seems that the assertion at line 101 of cuter_z3.py is violated.

Introduce an option to append directories to code path

Support an option similar to Erlang's -pa flag.

A scenario that this is needed:

-module(foo).
-export([f/1]).

-spec f(bar:t()) -> ok.
f(_) -> ok.

and the module bar is not loaded.

CutEr false positive

CutEr reports inputs that don't lead to runtime errors when testing the following code

-module(bar).
-compile(export_all).

-spec simple(A :: string()) -> ok.
simple(A) ->
  try 
    _ = list_to_integer(A),
    erlang:error("Error")
  catch
    error:badarg ->
      ok
  end.

1> cuter:run(bar, simple, ["1"], 25, [{number_of_pollers,1}, verbose_execution_info, disable_pmatch]).
Testing bar:simple/1 ...

WARNING: Encountered an unsupported type while parsing the types in Core Erlang forms!
  Form: {type,[604],map,any}

bar:simple("1") ... RUNTIME ERROR
bar:simple([]) ... ok
x
bar:simple("-") ... RUNTIME ERROR
x
bar:simple("+") ... RUNTIME ERROR
x
bar:simple([0]) ... ok
xxxxxxxxx
bar:simple("9") ... RUNTIME ERROR
x
bar:simple([45,0]) ... ok
bar:simple([43,0]) ... ok
xxxx
bar:simple("-0") ... RUNTIME ERROR
xxxxxxxxxxxx
bar:simple("+0") ... RUNTIME ERROR
xxxxxxxxxxxxxxxxxxx
bar:simple("-9") ... RUNTIME ERROR
xx
bar:simple("+9") ... RUNTIME ERROR
xxxx
Solver Statistics ...
  - Solved models   : 11
  - Unsolved models : 54

=== Inputs That Lead to Runtime Errors ===
#1 bar:simple("1")
#2 bar:simple("-")
#3 bar:simple("+")
#4 bar:simple("9")
#5 bar:simple("-0")
#6 bar:simple("+0")
#7 bar:simple("-9")
#8 bar:simple("+9")
[["1"],["-"],["+"],["9"],["-0"],["+0"],["-9"],["+9"]]

However, bar:simple("-") and bar:simple("+") don't lead to runtime errors.

Support `erlang:is_map/1`

crash: SOLVER ERROR

I get the following crash -- the cd command refers to the dir where Erlang/OTP resides:

$ cd otp/lib/hipe/ebin
$ cuter hipe_icode_primops pp '[standard_io, 42]'
Testing hipe_icode_primops:pp/2 ...
  ...
xxxxx[SOLVER ERROR] {"python -u /home/kostis/HiPE/cuter/priv/cuter_interface.py",
                [{{'__s',"0.0.16.103"},standard_io},
                 {{'__s',"0.0.16.104"},{apply_N,0}}],
                "/home/kostis/HiPE/otp/lib/hipe/ebin/temp/execexec6/run.trace",
                12}
Proccess <0.35.0> exited with {{solving,
                                   {unexpected_info,
                                       {'EXIT',#Port<0.1524>,normal}}},
                               {gen_fsm,sync_send_event,
                                   [<0.208.0>,check_model,500000]}}

Use argparse module in cuter script

Replace the getopt module with argparse.

support 'erlang:self/0'

Support `erlang:bor/2`

Make TravisCI builds faster

Try to cache the compilation of Z3.

Support type `iodata()`

This simple module demonstrates the issue

-module(cuter_test).

-export([test/1]).

-spec test(iodata()) -> iodata().
test(Input) ->
    Input.

Running cuter gives the output:

$ cuter cuter_test test '["asdf"]' -v
Testing cuter_test:test/1 ...

WARNING: The spec of {cuter_test,test,1} uses the unsupported type iodata!
  It has been generalized to any().

cuter_test:test(asdf) ... ok

Solver Statistics ...
  - Solved models   : 0
  - Unsolved models : 0

No Runtime Errors Occured

Erroneous runtime error reported

Consider the following command against the module below:

cuter uni to_upper '[[]]' -r -d 4

If the first clause of to_upper/1 is commented out, CutEr reports no error, as it should:

Compiling uni.erl ... OK
Testing uni:to_upper/1 ...
.x.x..xxx...
No Runtime Errors Occured

However, if one uncomments this clause, execution erroneously reports:

Compiling uni.erl ... OK
Testing uni:to_upper/1 ...
uni:to_upper([])
xx
=== Inputs That Lead to Runtime Errors ===
#1 uni:to_upper([])

which is weird because this call does not fail.

-module(uni).
-export([to_upper/1]).

-spec to_upper(string()) -> string().
%% to_upper(S) when is_binary(S) ->
%%   unicode:characters_to_binary(to_upper(unicode:characters_to_list(S)));
to_upper(S) when is_list(S) ->
  [char_to_upper(C) || C <- S];
to_upper(C) when is_integer(C) ->
  char_to_upper(C).

char_to_upper(16#0061) -> 16#0041;
char_to_upper(16#0062) -> 16#0042;
char_to_upper(C) -> C.

Clean Up the repo

The purpose is to clean up the repo from committed unneeded files as well as files that are generated at runtime.

Prepare the solver's backend for multiple solvers

Refactor and prepare the Python backend for multiple solvers.

Support `erlang:'band'/2`

Support `byte_size/1' and `bit_size/1'

A program that shows the need for this is the following:

-module(b).
-export([byte_sz/1, bit_sz/1]).

-spec byte_sz(bitstring()) -> ok.
byte_sz(Bits) ->
  case byte_size(Bits) of
    Sz when Sz < 42 -> ok
  end.

-spec bit_sz(bitstring()) -> ok.
bit_sz(Bits) ->
  case bit_size(Bits) of
    Sz when Sz < 42 -> ok
  end.

Spec related failure when running bson-erlang

Testing bson.erl from bson-erlang fails with:

aggelgian@lambda:~/git-repos/bson-erlang/ebin$ cuter bson lookup '[foo, bar]'
Testing bson:lookup/2 ...
Proccess <0.32.0> exited with {bad_return_value,
                                  {unsupported,{type,"\"",map,any}}}
Proccess <0.34.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}]}]}

Request for support nonempty_improper_list() type

When I tried to test a piece of code here
https://github.com/jj1bdx/exsplus116/blob/ba2429466925b1baeb5a81d183b67e092c548994/src/exsplus116.erl#L55
An error message showed up rendering the type into any().
The usage of nonempty_improper_list() was for a optimization which actually also exists in the rand module:
https://github.com/erlang/otp/blob/OTP-18.2.4/lib/stdlib/src/rand.erl#L257

(I know this is a rare case but I will raise an issue FYI for your further decision.)

kenji@silverblade[1043]% ~/src/cuter/cuter exsplus116 next '[[287716055029699555|144656421928717457]]' -d 50 -s 4 -p 4   Testing exsplus116:next/1 ...

WARNING: The spec of {exsplus116,next,1} uses the unsupported type nonempty_improper_list!
  It has been generalized to any().

.
exsplus116:next(0)

exsplus116:next([0])

=== Inputs That Lead to Runtime Errors ===
#1 exsplus116:next(0)
#2 exsplus116:next([0])

=== BIFs Currently without Symbolic Interpretation ===
erlang:'bsl'/2
erlang:'bxor'/2
erlang:'bsr'/2
erlang:'band'/2

Support `erlang:'bsl'/2`

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

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>>}]

Bug when applying funs to other funs

CutEr fails when testing

f(F) ->
  G = fun length/1,
  %  G = fun(_) -> 1 end, % also the same
  case F(G) of
    42 -> error(bug);
    _ -> ok
  end.

with

cuter foo f '[fun(_) -> 1 end]'

Support `erlang:iolist_to_binary/1`

I am trying to test some function in mochiweb_html and nothing happens, most likely due to this BIF being unsupported:

$ cuter mochiweb_html tokens '[<<>>]'
Testing mochiweb_html:tokens/1 ...
.
NO RUNTIME ERRORS OCCURED

=== UNSUPPORTED MFAS ===
erlang:iolist_to_binary/1

Also, make sure that MFAs of modules that are whitelisted are never included in the unsupported list.

Recreate funs represented as JSON strings

Enable cuter_json to reconstruct funs that are encoded as JSON strings.