How to handle SOLVER ERRORS?

[ioolkos]

Hello... This is more of a general question: how should one go about solver errors?

Is there something I can do about it? (change parameters/input/source code?) This is possibly similar to https://github.com/aggelgian/cuter/issues/25 ?

Example:

[SOLVER ERROR] {"python -u /home/afa/Erlang/cuter/priv/cuter_interface.py --smt",
                [{{'__s',"0.0.1.12855"},
                  {mqtt_publish,undefined,
                                [<<>>,<<>>,<<>>],
                                2,false,true,<<>>}}],
                "/home/afa/Erlang/temp/execexec82/run.trace",
                22}
Proccess <0.63.0> exited with {{solving,
                                   {unexpected_info,
                                       {'EXIT',#Port<0.9449>,normal}}},
                               {gen_fsm,sync_send_event,
                                   [<0.1620.0>,check_model,500000]}}
Shutting down the execution
` ` ` 

[kostis]

In contrast to #25 which contained a command to reproduce the [SOLVER ERROR] this issue does not. Why?

[ioolkos]

Point taken, I wasn't helpful.

I conclude that SOLVER ERRORS are unexpected behaviour that I can do something about. To me right now, they might have been expected behaviour as well, telling me that solver possibilities are exhausted or my code is stupid... :)

[aggelgian]

Well such errors generally indicate an internal error of the tool. In such cases, please provide a small example that triggers this behaviour so we can debug it.

[kostis]

One point I was trying to make with my previous post in this thread is that if you look deeply into #25 you will see that that issue was fixed. This was possible because there was a concrete example to reproduce and debug this.

[ioolkos]

Thanks for your remarks! I'm currently not able to transform this to a small example, so I'll close this now and will get back with specific contained examples as I find them.

Just to be transparent, the following was my original issue. Of course I do not expect anyone to look into this for me!

➜  vernemq git:(master) ✗ cuter vmq_parser serialise '[<<>>]' -pa /home/afa/Erlang/vernemq/_build/default/lib/*/ebin -d 30 -s 3 -p 3
Testing vmq_parser:serialise/1 ...

WARNING: The spec of {vmq_parser,serialise,1} uses the unsupported type iolist!
  It has been generalized to any().

vmq_parser:serialise(<<>>)
xx.xxx..xx.xxxxxxxxxxx.xxxxx..xxxx...xxxxxxxxxxxxxxxxxxxx...xxxxxxxxxxxxxxxxxx...xxxxxxxxx.xx.xxxxxxxxx.xxxx..xxxxxxxxxx...x.xxxxxxxxxxxxxxx.xx.xxxxxxxxxxxx...x.xxxxxxxxxxxx[SOLVER ERROR] {"python -u /home/afa/Erlang/cuter/priv/cuter_interface.py --smt",
                [{{'__s',"0.0.1.3286"},
                  {mqtt_publish,undefined,
                                [<<>>,<<>>,<<>>],
                                2,false,true,<<>>}}],
                "/home/afa/Erlang/vernemq/temp/execexec31/run.trace",
                20}
Proccess <0.61.0> exited with {{solving,
                                   {unexpected_info,
                                       {'EXIT',#Port<0.8066>,normal}}},
                               {gen_fsm,sync_send_event,
                                   [<0.337.0>,check_model,500000]}}
Shutting down the execution...
Stopping poller <0.57.0>...
Stopping poller <0.58.0>...
Stopping poller <0.59.0>...
xx=== Inputs That Lead to Runtime Errors ===
#1 vmq_parser:serialise(<<>>)

=== BIFs Currently without Symbolic Interpretation ===
erlang:iolist_size/1

[kostis]

Just to be transparent, the following was my original issue. Of course I do not expect anyone to look into this for me!

FYI: This is exactly the type of stuff we want to look into, but we strongly prefer minimized code bases that we can test and experiment with.

[ioolkos]

This is as far as I managed to zoom in for the SOLVER ERROR above. cuter minimal1 test '[[<<>>,<<>>,<<>>]]'

-module(minimal1).
-export([test/1]).

-define(HIGHBIT, 2#10000000).
-define(LOWBITS, 2#01111111).

%-spec test4(topic()) -> binary() | iolist().
%test4(Topic) ->
%        Var = utf8(vmq_topic:unword(Topic)),
%        LenBytes = serialise_len(iolist_size(Var)),
%        LenBytes.

% cuter minimal1 test '[[<<>>,<<>>,<<>>]]'
test(Topic) ->
         utf8("//"),
         serialise_len(4).

serialise_len(N) when N =< ?LOWBITS ->
    <<0:1, N:7>>;
serialise_len(N) ->
    <<1:1, (N rem ?HIGHBIT):7, (serialise_len(N div ?HIGHBIT))/binary>>.

utf8(<<>>) -> <<>>;
utf8(undefined) -> <<>>;
utf8(empty) -> <<0:16/big>>; %% for test purposes, useful if you want to encode an empty string..
utf8(IoList) when is_list(IoList) ->
    [<<(iolist_size(IoList)):16/big>>, IoList];
utf8(Bin) when is_binary(Bin) ->
<<(byte_size(Bin)):16/big, Bin/binary>>.

[kostis]

Your example program does not make too much sense because the argument of test/1 is not really used anywhere. Still, CutEr should not be crashing in programs, independently of whether these programs make sense or not.

Anyway, a smaller version of your program appears below:

-module(minimal).
-export([test/1]).

%% ./cuter minimal test '[42]' -r
test(_) ->
    utf8("//"),
    serialise_len(4).

utf8(IoList) when is_list(IoList) ->
    [<<(iolist_size(IoList)):16>>, IoList].

serialise_len(N) when N =< 2#0111 ->
    <<0:1, N:7>>.

[ioolkos]

Still, CutEr should not be crashing in programs, independently of whether these programs make sense or not.

Phew! :)

I'll practice to come up with better "shrinked" examples. I've seen a couple more of those solver errors, so there's room... :)