3 months of waiting...

[sarn]

On Monday, 10 February 2020 at 11:23:16 UTC, Joseph Rushton 
Wakeling wrote:
> On Saturday, 8 February 2020 at 17:21:04 UTC, Jonathan Marler 
> wrote:
>> for 32-bit floats it doesn't take too long to do an exhaustive 
>> test (maybe 30 minutes or so).  I did this with my port of the 
>> "ryu" float to string implementation 
>> (https://github.com/dragon-lang/mar/blob/master/src/mar/ryu.d).
>>  That being said, an exhaustive 64-bit test may not finish 
>> until the inevitable heat death of the universe :)
>
> It feels intuitively that there's got to be a more effective 
> way of approaching this than brute-forcing all the cases, or 
> randomly selecting a sufficient subset.
>
> I would anticipate that there has to be a well-defined subset 
> of cases such that, if the formatter works for those, it'll 
> work for everything else.
>
> (Yes, I get that in this case you're trying to compare the 
> behaviour of 2 different functions, but I think the principle 
> should still apply.)

KLEE (which I mentioned earlier in the thread) uses constraints 
solvers to prove/disapprove assertions over all possible code 
paths.  KLEE float uses the IEEE floating point theory in the Z3 
solver.

When you run KLEE against some code, you can get it to generate 
example inputs for each code path, which can be used as a 
regression suite.  A regression suite like that is weaker than 
running KLEE again, but stronger than the typical code coverage 
test suite because it has code *path* coverage.