Abstract proof trace writer at event level #1136
Conversation
theo25
force-pushed
the
abstract-event-writer
branch
2 times, most recently
from
bcb1c56
to
2b6ede1
Compare
theo25
force-pushed
the
abstract-event-writer
branch
from
2b6ede1
to
1ce3f01
Compare
There was a problem hiding this comment.
I'm having trouble tracking all of these changes, but the high level signature of proof_trace_writer looks good, the tests pass, and you seem happy with it as a stepping stone towards the callbacks, so I don't have any comments. I will let Roberto approve, though. I want another set of eyes on it.
| * Emit an instruction that has no effect and will be removed by optimization | ||
| * passes. | ||
| * | ||
| * We need this workaround because some callsites will try to use | ||
| * llvm::Instruction::insertAfter on the back of the MergeBlock after a proof | ||
| * branch is created. If the MergeBlock has no instructions, this has resulted | ||
| * in a segfault when printing the IR. Adding an effective no-op prevents this. | ||
| */ | ||
| llvm::BinaryOperator *emit_no_op(llvm::BasicBlock *insert_at_end); |
There was a problem hiding this comment.
I understand that this will be deleted by DCE, but is it really impossible to prevent this writing from being in MergeBlock? Can you elaborate a bit more on this?
There was a problem hiding this comment.
So there is an issue with the way github presents the diff for this PR. If you notice this is not my code, it has been just deleted from a different place in the file and moved here verbatim. As such I have no comment on what should be done with it and whatever it is that we may decide, it shouldn't be part of this PR anyway.
There was a problem hiding this comment.
That's pretty awkward indeed.
This PR refactors the proof trace writer to be abstract at the event generation level, rather than the byte stream level. We do this in order to be able to use alternative ways of communicating the proof hints that do not require writing the trace to a file, such as triggering of callback invocations.
The PR can be reviewed commit by commit:
proof_trace_writerand a subclass that writes in a file as before.proof_trace_writerthat operated at the level of writing byte streams.