better annotated assembly output for assembly-checker

[andres-erbsen]

Currently, the assembly-checker generates annotated output like the following:

add rcx, rax ; #572, #574, #576, #578, #583, #584, #585, #589, #590, #591, #595, #596, #597, #601, #602, #603, #607, #608, #612, #619, #620, #621, #625, #626, #627, #631, #632, #633, #637, #638, #639, #679, #680, #681, #685, #686, #687, #691, #692, #693, #735, #736, #737, #741, #742, #743

This is overwhelmingly verbose and I am not sure what a list this long might even mean.

Would it be possible to generate output like

add rcx, rax ; rcx <- #123=add 64 #100 #105; CF <- #127=addcarry 64 #100 #105; created #123..127

Only changed registers should be printed, and it might be ideal for rhs expressions to be either they were created during symbolic execution of this line of assembly code or perhaps (even better?) if they have not been printed in an annotation before. Even fancier would be to also print PHOAS variable names for indices that have them, or do the same for PHOAS output...

Do you think this would be useful and how reasonable would (some variant of) this be to implement? @JasonGross @ChuyueSun

[andres-erbsen]

Jason tells me that the overwhelmingly long list is a bug. Getting information by PHOAS variables seems difficult given current code structure. For the rest: Wrap SymexNormalInstruction, based on old and new symbolic states generate the printout while folding through instructions. All this might need to be in a thunk or something to not spend time computing it on successful runs, or maybe it doesn't matter.