xls
xls copied to clipboard
Check analysis passes during fuzzing
When fuzzing we should verify IR analyses as well. These analyses can come in the form of query engines or other standalone analyses. Couple ways of checking the analysis:
- Run input through the IR sample and extract all intermediate values. Check these values against what the analysis says about each node. For example, you could check that the value is in the expected range indicated by range analysis. This could, of course, be done on the optimized and unoptimized IR.
- Suggested by @taktoa: Add asserts to the graph asserting particular conditions guaranteed by the analysis and then jit and run the inputs though. Upside is that running each set of inputs will be much faster. Downside is that there may be a more limited set of things you can test to keep the graph size manageable. This could be complementary to (1).
My suggestion was actually slightly different: generate the asserted conditions, and then AND them all together and replace the output of the function with that boolean. Then JIT it and bitblast the JITed function.
Also somewhat related to #542 e.g. in the user-requested proof of particular predicates; you could imagine for #1 a rewrite to insert try_prove nodes if that were a supported construct.