search

GaloisInc / pate

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

binja: Check for missing sync in target7 #389

Closed thebendavis closed 1 month ago

thebendavis commented 2 months ago

Once #388 is complete, make sure we see the synchronization/merge points we expect in the Binary Ninja UI for target7

jim-carciofini commented 1 month ago

The graph for each function entry now flows to a return node, except for a few tail call nodes that flow to a "None" node that is a sink. Looking at hooking those up to the return node.

jim-carciofini commented 1 month ago

I asked @danmatichuk (in Mattermost) if he could add the return info to the tail call nodes. No response yet. I committed a fix (fb5c224) that gets rid of spurious "None" CFAR nodes following "Tail Call" nodes. Now "Tail Call" nodes are sinks. As far as I can tell, the function return information is not in the data I get from the verifier for Tail Call nodes. If we want to link up the "Tail Call" nodes to the function return nodes, I need that data. What do others think?

jim-carciofini commented 1 month ago

Ben commented in Mattermost:

great - thanks for the fix re: those None nodes! I'll let Dan chime in regarding whether there is more data available we want to wire in, but IMO tail calls as sinks in the PATE overview graph seems sufficient and lack of anything "beyond" it doesn't seem to negatively impact the operator's understanding of the GirdIDPS example at least

thebendavis commented 1 month ago

Closing - in an offline discussion we determined that with these recent fixes we are now satisfied with the rendering of tail calls.