search

GaloisInc / pate

Patches Assured up to Trace Equivalence
Other
15 stars 2 forks source link

Add Binary Ninja UI to specify trace generation constraints #398

Closed thebendavis closed 3 days ago

jim-carciofini commented 5 days ago

Basically working. From Ben's message in MM:

Remaining in terms of priorities for final polish, summarizing what I'm thinking from the discussion above:

  1. top priority: some way to tell user when "the constraints you requested are impossible to satisfy" which I think is an important part of this workflow. looks like this may need some JSON handling and a message in the UI somewhere (trace text areas?) indicating this result
  2. updating the equivalence condition display as discussed above (keep orig equiv cond, maybe display other info on user constraints when present, reuse existing equiv cond textbox?)
  3. minimizing confusion with replay. I think this is lowest priority since replay isn't a core part of the workflow. I think the smallest simplest thing we could do here is maybe just change the button text from Constrain Trace to Constrain Trace (replay) when we're in replay mode
jim-carciofini commented 3 days ago

All three priorities have been addressed as of 55d94d8.

jim-carciofini commented 3 days ago

There are a few cosmetic cleanups I would like to do. In the mean time it would be good if @ben can verify that things work as he expects.