• DigitalDesigns (20/20) Jun 04 2018 Does D have any methods of validating code in a natural manner
• Petar Kirov [ZombineDev] (5/25) Jun 04 2018 Perhaps not quite what you're looking for, but I think you would
• DigitalDesigns (19/49) Jun 05 2018 Sorta, but not fuzzing because that is too spare. Rather than
• Kagamin (2/6) Jun 05 2018 Something like HACL? https://github.com/mitls/hacl-c

DigitalDesigns <DigitalDesigns gmail.com> writes:

Does D have any methods of validating code in a natural manner 
besides unit tests and contracts?

I'm specifically thinking of validating mathematical calculations 
and boolean operations that could depend on very improbable 
scenarios but are technically invalid logic.

These issues tend to creep up in calculations that involve 
floating points due to various reasons or comparisons that 
mistakenly use > for >= or vice versa.

If I have a variable such as a buffer which has a length and an 
offset in to that buffer is calculated using double precision 
then rounding errors could cause the offset to except the length 
and create an access violation.

To be able to theoretically test all the possibilities all valid 
inputs would need to be checked. One can setup unit tests to test 
these possibilities but it can be difficult to cover all cases in 
even a semi-complex program.

Just curious if something exists that allows for mathematical 
validation such code in an relatively canonical way. This isn't 
too hard for pure functions but dealing with non-pure functions 
can be a pain.

Petar Kirov [ZombineDev] <petar.p.kirov gmail.com> writes:

On Monday, 4 June 2018 at 15:48:35 UTC, DigitalDesigns wrote:
 Does D have any methods of validating code in a natural manner 
 besides unit tests and contracts?

 I'm specifically thinking of validating mathematical 
 calculations and boolean operations that could depend on very 
 improbable scenarios but are technically invalid logic.

 These issues tend to creep up in calculations that involve 
 floating points due to various reasons or comparisons that 
 mistakenly use > for >= or vice versa.

 If I have a variable such as a buffer which has a length and an 
 offset in to that buffer is calculated using double precision 
 then rounding errors could cause the offset to except the 
 length and create an access violation.

 To be able to theoretically test all the possibilities all 
 valid inputs would need to be checked. One can setup unit tests 
 to test these possibilities but it can be difficult to cover 
 all cases in even a semi-complex program.

 Just curious if something exists that allows for mathematical 
 validation such code in an relatively canonical way. This isn't 
 too hard for pure functions but dealing with non-pure functions 
 can be a pain.

Perhaps not quite what you're looking for, but I think you would 
be interested in the LLVM fuzzing part of Johan Engelen's talk at 
DConf 2018:
https://www.youtube.com/watch?v=GMKvYrjaaoU (at around 34:30).

DigitalDesigns <DigitalDesigns gmail.com> writes:

On Tuesday, 5 June 2018 at 06:45:31 UTC, Petar Kirov [ZombineDev] 
wrote:
 On Monday, 4 June 2018 at 15:48:35 UTC, DigitalDesigns wrote:
 Does D have any methods of validating code in a natural manner 
 besides unit tests and contracts?

 I'm specifically thinking of validating mathematical 
 calculations and boolean operations that could depend on very 
 improbable scenarios but are technically invalid logic.

 These issues tend to creep up in calculations that involve 
 floating points due to various reasons or comparisons that 
 mistakenly use > for >= or vice versa.

 If I have a variable such as a buffer which has a length and 
 an offset in to that buffer is calculated using double 
 precision then rounding errors could cause the offset to 
 except the length and create an access violation.

 To be able to theoretically test all the possibilities all 
 valid inputs would need to be checked. One can setup unit 
 tests to test these possibilities but it can be difficult to 
 cover all cases in even a semi-complex program.

 Just curious if something exists that allows for mathematical 
 validation such code in an relatively canonical way. This 
 isn't too hard for pure functions but dealing with non-pure 
 functions can be a pain.

 Perhaps not quite what you're looking for, but I think you 
 would be interested in the LLVM fuzzing part of Johan Engelen's 
 talk at DConf 2018:
 https://www.youtube.com/watch?v=GMKvYrjaaoU (at around 34:30).

Sorta, but not fuzzing because that is too spare. Rather than 
picking a random point in a billion dimensional vector space bit 
is sort of works only on the surface of possible values. Which he 
addresses initially being the problem and is similar to what I'm 
looking for.

The idea though is problems almost always occur on edge cases so 
there is no need to check everything inside an interval but only 
the edge cases.

if (x < 10)

one only needs to check if x = 9, 10, 11 but not 4, 5, etc.

Of course, in more complex cases it might be difficult to 
determine this so maybe the method in the video is more general 
purpose. It seems to have the capabilities to have a bit more 
intelligent checking though so yeah, this seems to be what I was 
looking for!

Thanks!



In any case

Kagamin <spam here.lot> writes:

On Monday, 4 June 2018 at 15:48:35 UTC, DigitalDesigns wrote:
 Just curious if something exists that allows for mathematical 
 validation such code in an relatively canonical way. This isn't 
 too hard for pure functions but dealing with non-pure functions 
 can be a pain.

Something like HACL? https://github.com/mitls/hacl-c