Oracle chaining sketch

Open kripken opened this issue 2 years ago • 1 comments

Once open I'll add a comment with a link to the relevant part.

Aug 02 '23 19:08 kripken

@tlively The key part of the code is here:

https://github.com/WebAssembly/binaryen/pull/5853/files#diff-4d9d6d08d863caa22d1fa86a99f2b7d37d1013d36c98e177aca6edd6eaff54e1R2070-R2074

    // Start with an empty base oracle, infer TNH once in the middle, and a
    // second time.
    auto base = std::make_shared<Oracle>(wasm, options);
    auto mid = std::make_shared<TNHOracle>(wasm, options, base);
    tnhOracle = std::make_unique<TNHOracle>(wasm, options, mid);

The TNH oracle gets a "previous oracle" that it uses as a base to improve upon. Adding more oracles in the chain is just a matter of adding one line. We could interleave TNH and other oracles in this way, in particular.

Atm though some simple experiments don't show a big benefit to this. One issue is that we look at RefCast types in the TNH oracle, and those are just updated in the GUFA pass itself, after the oracles are all done. So one needs to run all of GUFA more than once, and just running it that way seems good enough for now.

Aug 02 '23 19:08 kripken