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.
--
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.
