User defined types?

[ioolkos]

Hello! I have a small confusion about user defined types. How are they currently handled by cutEr? Am I correct in assuming they are ignored?

-type three()                 :: 0..2.
-spec three(three()) -> any().    % does not generate correct input

vs

-spec three(0..2) -> any().    % generates correct input

[ioolkos]

OK, from the "Concolic Testing @ Smart Programming Day 2016" presentation (Slide 19), https://www.sics.se/SSW2016/speakers/konstantinos-sagonas the conclusion seems to be that user defined types should be supported.

Trying to research more then.

[aggelgian]

Hello!

User defined types are indeed supported. In fact, the example you mentioned can be handled by CutEr.

Consider the following code:

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

-type three() :: 0..2.

-spec f(three()) -> any().
f(X) ->
  case X of
    1 -> error(bug);
    4 -> error(unreachable_bug);
    _ -> ok
  end.

CutEr's output is

aggelgian@lambda:~/git-repos/cuter$ cuter userdef f '[0]' -r
Compiling userdef.erl ... ok
Testing userdef:f/1 ...
.
userdef:f(1)
x
=== Inputs That Lead to Runtime Errors ===
#1 userdef:f(1)

As you can see, userdef:f(4) is not reported as the relevant branch is unreachable when the function's spec is taken into consideration.

[ioolkos]

Excellent, thanks for this clear example, @aggelgian.

Knowing this for sure will hopefully help me get my examples sorted out.

[ioolkos]

@aggelgian I took your example & ran it. This is what I'm seeing, contrary to your output above.

-> Have I a misconfiguer cutEr install? -> Is the install documentation up-to-date?

➜  cuter_tests cuter userdef f '[0]' -r
Compiling userdef.erl ... ok
Testing userdef:f/1 ...
.[SOLVER ERROR] {"python -u /home/afa/Erlang/cuter/priv/cuter_interface.py --smt",
                [{{'__s',"0.0.3.121"},0}],
                "/home/afa/Erlang/cuter_tests/temp/execexec1/run.trace",
                1}
Proccess <0.59.0> exited with {{solving,
                                   {unexpected_info,
                                       {'EXIT',#Port<0.1102>,normal}}},
                               {gen_fsm,sync_send_event,
                                   [<0.64.0>,check_model,500000]}}
Shutting down the execution...
Stopping poller <0.58.0>...

No Runtime Errors Occured
➜  cuter_tests cuter userdef f '[0]' -r --z3py
Compiling userdef.erl ... ok
Testing userdef:f/1 ...
.
userdef:f(1)

userdef:f(4)

=== Inputs That Lead to Runtime Errors ===
#1 userdef:f(1)
#2 userdef:f(4)
➜  cuter_tests 

[ioolkos]

OK, for some reason my system had a Z3 install with version 4.4.1. I updated that to 4.5.0, and now the example works as expected (although not with --z3py)

[kostis]

The --z3py option is currently there mainly(*) as a fallback if the SMTlib-based translation of the constraints, which was only added quite recently, does not work on some example for some reason. Resort to it only if you see a crash with the default options of the tool.

(*) It's also kept for the time being for debugging purposes and for being able to measure performance differences.

[ioolkos]

Good, thanks, this is very helpful context for me.