This is very nice! However, am i right in understanding that the magic is
in knowing the text of the program--the fact that there are untaken
branches? If so, this is not simply a 'behavioral' verification...it knows
about the construction of the code and not just its behavior. Maybe I was
unclear.
On the other line of development, Rob Pike's coverage analyzer would be
handy that way too.
On Thu, Nov 24, 2016 at 9:13 PM, Jesper Louis Andersen <
jesper.louis.ander...@gmail.com> wrote:
>
>
> On Thu, Nov 24, 2016 at 8:23 PM Michael Jones <michael.jo...@gmail.com>
> wrote:
>
>>
>>
>> It would be a miracle if a behavioral tester found a difference here, as
>> intel can attest. You can test every input or you can prove equality.
>> Nothing else means equal.
>>
>>
>>
>
> Not in a modern world. Here is an Erlang program, which does the same as
> your example:
>
> -spec a(integer()) -> number() | undefined.
> a(X) ->
> if
> X == 25638625386 -> exit({error, 42});
> X /= 0 -> 1 / X;
> true -> undefined
> end.
>
> Random testing is unlikely to find this particular bug, but the concept of
> concolic testing is more clever. In Erlang we have a tool, CuTer, which
> performs concolic testing of programs. Running this on our example with
> some seed value (the input 3) immediately finds the problem in seconds:
>
> [jlouis@lady-of-pain tmp]$ cuter z a '[3]' --recompile
> Compiling z.erl ... OK
> Testing z:a/1 ...
> .xxxxxxxx
> z:a(25638625386)
> xxxxxxxxxxxxxx
> === Inputs That Lead to Runtime Errors ===
> #1 z:a(25638625386)
>
> How does it work? In the above if-expression, we note that the seed value
> of 3 took the branch behind 'X /= 0'. If we pick the branch 'X ==
> 25638625386' and then ask an SMT solver (Z3 is what Cuter uses by default)
> if it can find something you can plug into X to make this go through.
>
> In the more general case, we have traversed many such branch-decisions
> down to a certain depth. We can then invert one of the branch decisions and
> ask the SMT solver to find results which follows the path down to that
> branch, and then goes in another direction, due to the inversion. The
> reason an SMT solver is needed is because some of the earlier branch
> decisions might make it non-trivial to find one that forces a new path deep
> down in the decision tree. We get expressions of the form (X > 5) AND (X !=
> 37) AND (Y < 7) AND (Y + X == 25) and ask the solver for values X and Y
> such that the expression is satisfied. Since we inverted one of the branch
> decisions, a sat of this expression gives us a new path to explore. We can
> continue forcing out new branches down to a certain depth.
>
> Here is another function:
>
> -spec b(pos_integer(), pos_integer(), pos_integer()) -> {ok,
> pos_integer()}.
> b(X, Y, Z) ->
> case lists:sum([X,Y,Z]) of
> 4321 -> exit(argh);
> Sum -> {ok, Sum}
> end.
>
> which is given values X, Y and Z summing to 4321 is an error:
>
> [jlouis@lady-of-pain tmp]$ cuter z b '[3,2,1]' --recompile
> Compiling z.erl ... OK
> Testing z:b/3 ...
> .xxxxxx
> z:b(1, 4281, 39)
> xxxx
> === Inputs That Lead to Runtime Errors ===
> #1 z:b(1, 4281, 39)
>
> You are now in a territory where random testing is unlikely to find
> anything. At least not naive random testing with uniform distributions. But
> if you can ask the system (through profiling) what branch decisions were
> taken, SMT solvers can produce inputs which forces us to take different
> branches. In turn, they pick a specimen for each code block and makes sure
> every possible code block is traversed.
>
> Another solution is to use a profiler, see that X = 25638625386 is never
> hit and then write a generator like this (Erlang QuickCheck)
>
> my_int() ->
> frequency([
> {1, 25638625386},
> {1000, int()}]).
>
> which will generate the nasty case 1/1001 times. Combined with suffix
> trees over what probalistic paths the generator has hit, this also forces
> out this value[0]
>
> [0] Many computer games use the same trick. If a given ability were truly
> random, some games would feel unfair. Hence, the distribution is
> pseudo-random to make sure the given event happens at least with a certain
> probability. See http://dota2.gamepedia.com/Pseudo-random_distribution for
> instance, for Dota 2's variant.
>
>
--
Michael T. Jones
michael.jo...@gmail.com
--
You received this message because you are subscribed to the Google Groups
"golang-nuts" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to golang-nuts+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
