runtimeverification / k

K Framework Tools 7.0
BSD 3-Clause "New" or "Revised" License
444 stars 147 forks source link

Being implementing fuzzing #4453

Closed gtrepta closed 3 months ago

gtrepta commented 3 months ago

This introduces the most basic functionality for doing fuzz testing of a property in K.

It adds a function fuzz to the ktool.kfuzz pyk module which takes the location of an llvm-kompiled definition, a template configuration in kore containing input variables to be randomized, a strategy for substituting those variables (so far, only with integers using kintegers), and either a function to check the resulting kore or a flag to check the exit code of the interpreter. It will invoke hypothesis to randomize the inputs and run the interpreter.