Refactor Cegis Loop

[philzook58]

The cegis loop is currently being refactored to not rebuild the core_theory->IR pass every time but it currently reingests the patch config every time. This should probably only happen once, just like the core_theory translator

[philzook58]

JT seems to think that this extra loading was unnecessary and removed it?

[jtpaasch]

Yes! I did remove it in #67 because I double-checked and it is indeed unnecessary.

When we start the pipeline, we have the patches as sexps in config.

Then, the pipeline call's Pipeline.init, and we pass in the config. Here's what happens:

• In Pipeline.init we call the patch ingester, which takes the sexps from the config and translates them into bir, and stashes that bir in the KB: https://github.com/draperlaboratory/VIBES/blob/main/bap-vibes/src/patch_ingester.ml#L228
• In Pipeline.init we then call compile_ir, which gets the sexps from the KB, and calls compile_one_ir for each patch sexp: https://github.com/draperlaboratory/VIBES/blob/main/bap-vibes/src/compiler.ml#L89
  • In compile_one_ir:
  • We pull out the bir: https://github.com/draperlaboratory/VIBES/blob/main/bap-vibes/src/compiler.ml#L50
  • From the bir we build the ir: https://github.com/draperlaboratory/VIBES/blob/main/bap-vibes/src/compiler.ml#L52
  • We stash the ir in the KB: https://github.com/draperlaboratory/VIBES/blob/main/bap-vibes/src/compiler.ml#L53
• So, to summarize, in Pipeline.init, we load the sexps from config, we use that to build the bir, we use the bir to build the ir, and then we stash the ir in the KB.

Next, the pipeline extracts a seed from the result of all that, which does this:

• It calls Seeder.extract_patch (https://github.com/draperlaboratory/VIBES/blob/main/bap-vibes/src/seeder.ml#L27)
  • That function pulls out the ir from the KB, and adds it to the seed.

Then, the pipeline calls the cegis loop. On each iteration on the loop, it calls Pipeline.create_patched_exe, and we pass it the seed. Here's what happens in create_patched_exe:

• It calls Seeder.init_KB, which uses the seed to seed the KB.
  • In doing that, it puts the ir into the KB.
• It calls Compiler.compile_assembly, which calls compile_one_assembly on each patch: https://github.com/draperlaboratory/VIBES/blob/main/bap-vibes/src/compiler.ml#L103
  • In compile_one_assembly:
  • We pull out the ir from the KB: https://github.com/draperlaboratory/VIBES/blob/main/bap-vibes/src/compiler.ml#L70
  • We use minizinc and previous solutions to find a new solution, and then we create assembly for the solution: https://github.com/draperlaboratory/VIBES/blob/main/bap-vibes/src/compiler.ml#L73
  • We stash the assembly in the KB: https://github.com/draperlaboratory/VIBES/blob/main/bap-vibes/src/compiler.ml#L74
  • The patcher can then use the assembly to create the patched exe.
  • The patch bir is not used in this function.
• So to summarize, in Pipeline.create_patched_exe, we seed our KB with the previously built ir, we use that to build the assembly instructions for the patch, without needing to go back to the bir or the sexps.

It looks to me from all this that each cegis iteration only needs the ir, not the sexps or bir. That's why our system tests are still passing, after we merged the changes in #67 (i.e., that's why our pipeline is still patching our test binaries correctly).

@philzook58 do you want to go through the above reasoning and make sure it makes sense to you, just to make sure I haven't missed something? If so, we can close this issue.

[codyroux]

Ping @philzook58