`BugReport` should not be written directly

[tothtamas28]

Related: runtimeverification/pyk#693 (comment)

Consider https://github.com/runtimeverification/pyk/blob/41706ef5081585a4c71f7fccb4dea2d7a3796421/src/pyk/kore/rpc.py#L250

Here, in order to group calls to multiple clients that correspond to the same proof, along with bug_report, an additional optional argument bug_report_id is passed. If the argument is missing, a default value is calculated from the object id.

This means the class that produces bug report content is responsible for defining where to write data within the tar file. A more flexible design would be to let the caller define bug report structure by abstracting the target directory for the producer using a handle:

# BugReport defines which file to write
bug_report = BugReport('bug-report')

# BugReporter is a handle for writing in a certain directory within the file
bug_reporter = bug_report.reporter('AssertTest.test_assert_true') 

# The handle is passed to the class that produces bug report content
client = JsonRpcClient(..., bug_reporter=bug_reporter)

Then the producer is no longer concerned about where to write things:

class JsonRpcClient(...):
    def request(self, ...):
        # The producer can use the handle to create artifacts
        self.bug_reporter.add_command(...)

The private interface between BugReport and BugReporter should implement locking to prevent race conditions.

[gtrepta]

I've drafted a PR runtimeverification/pyk#770 with my solution. @tothtamas28 let me know if this is along the lines of what you expect.